To protect your data, the CISO officer has suggested users to enable GitLab 2FA as soon as possible.

Commit d4b31059 authored by Adam Nelson's avatar Adam Nelson
Browse files

Clean up exec_terminst, remove $-variables

The current version of the Mu specification does not use $-variables to
pass return values from terminsts to the normal destination of an EXC
clause, instead allowing terminsts to have normal SSA return values
that may be referenced in the EXC clause. This commit updates the
formalism to match.

Several other refactorings are included, such as making exec_terminst
only return modified stacks, using a simpler representation of common
instructions, and defining prefix/infix operators for SSA variables and
registers in HOL.
parent 535fca59
......@@ -49,11 +49,8 @@ struct
"SEQ_CST"
]
val ty_ci = mk_type("comm_inst", [])
val comm_insts = [
("uvm.new_stack", mk_const("CI_NewStack", ty_ci)),
("uvm.current_stack", mk_const("CI_CurrentStack", ty_ci))
"uvm.new_stack", "uvm.current_stack"
]
val ty_ssa = mk_type("ssavar", [])
......@@ -125,6 +122,26 @@ struct
| _ => raise ParseError "expected newStackClause (PASS_VALUES or THROW_EXC)"
end
fun lhs0 (lhs : uir_token) (inst : string) =
case lhs of
Parens [] => ()
| _ => raise ParseError(inst ^ " does not return a value")
fun lhs1 (lhs : uir_token) (inst : string) =
case lhs of
SSA (Local, v) => mk_return(mk_ssa v)
| Parens [SSA (Local, v)] => mk_return(mk_ssa v)
| _ => raise ParseError(inst ^ " returns exactly 1 value")
fun lhs_n (lhs : uir_token) (inst : string) =
case lhs of
(SSA (Local, v)) => mk_list([mk_ssa v], ty_ssa)
| (Parens vs) =>
let fun var (SSA (Local, v)) = mk_ssa v
| var _ = raise ParseError(inst ^ " lhs contains non-SSA-var")
in mk_list(map var vs, ty_ssa) end
| _ => raise ParseError(inst ^ " lhs contains non-SSA-var")
(* Parses a list of tokens into a Mu IR instruction. Returns a term of type
``:ssavar instruction or_error``.
*)
......@@ -152,25 +169,8 @@ struct
| ssa_noconst (Global, v) = raise ParseError(
"global name @" ^ v ^ " used in illegal location")
val (lhs, rhs) = case tokens of l::Eq::r => (l, r) | _ => (Parens [], tokens)
fun lhs0 (inst : string) =
case lhs of
Parens [] => ()
| _ => raise ParseError(inst ^ " does not return a value")
fun lhs1 (inst : string) =
case lhs of
SSA (Local, v) => mk_return(mk_ssa v)
| Parens [SSA (Local, v)] => mk_return(mk_ssa v)
| _ => raise ParseError(inst ^ " returns exactly 1 value")
fun lhs_n (inst : string) =
case lhs of
(SSA (Local, v)) => mk_list([mk_ssa v], ty_ssa)
| (Parens vs) =>
let fun var (SSA (Local, v)) = mk_ssa v
| var _ = raise ParseError(inst ^ " lhs contains non-SSA-var")
in mk_list(map var vs, ty_ssa) end
| _ => raise ParseError("expected SSA var(s) before = " ^ inst)
fun mk_assign(inst : string, expr : term) =
ir_ap("Assign", [mk_return (lhs_n inst), expr], ty_inst)
ir_ap("Assign", [mk_return (lhs_n lhs inst), expr], ty_inst)
in case rhs of
(* Identity instruction *)
[Word "ID", Type ty, SSA i] =>
......@@ -211,34 +211,34 @@ struct
[t_ref, parse_type env ty, ssa_var env t_void opnd], ty_expr))
(* Load *)
| [Word "LOAD", Type ty, SSA src] => ir_ap("Load",
[lhs1 "LOAD", t_ref, parse_type env ty, ssa_noconst src, t_na], ty_inst)
[lhs1 lhs "LOAD", t_ref, parse_type env ty, ssa_noconst src, t_na], ty_inst)
| [Word "LOAD", Word "PTR", Type ty, SSA src] => ir_ap("Load",
[lhs1 "LOAD", t_ptr, parse_type env ty, ssa_noconst src, t_na], ty_inst)
[lhs1 lhs "LOAD", t_ptr, parse_type env ty, ssa_noconst src, t_na], ty_inst)
| [Word "LOAD", Word ord, Type ty, SSA src] => ir_ap("Load", [
lhs1 "LOAD", t_ref, parse_type env ty, ssa_noconst src,
lhs1 lhs "LOAD", t_ref, parse_type env ty, ssa_noconst src,
mk_return(parse_mem_order ord)
], ty_inst)
| [Word "LOAD", Word "PTR", Word ord, Type ty, SSA src] => ir_ap("Load", [
lhs1 "LOAD", t_ptr, parse_type env ty, ssa_noconst src,
lhs1 lhs "LOAD", t_ptr, parse_type env ty, ssa_noconst src,
mk_return(parse_mem_order ord)
], ty_inst)
(* Store *)
| [Word "STORE", Type ty, SSA dst, SSA src] =>
let val _ = lhs0 "STORE"
let val _ = lhs0 lhs "STORE"
val ty' = parse_type env ty
in ir_ap("Store", [
ssa_var env ty' src, t_ref, ty', ssa_noconst dst, t_na
], ty_inst)
end
| [Word "STORE", Word "PTR", Type ty, SSA dst, SSA src] =>
let val _ = lhs0 "STORE"
let val _ = lhs0 lhs "STORE"
val ty' = parse_type env ty
in ir_ap("Store", [
ssa_var env ty' src, t_ptr, ty', ssa_noconst dst, t_na
], ty_inst)
end
| [Word "STORE", Word ord, Type ty, SSA dst, SSA src] =>
let val _ = lhs0 "STORE"
let val _ = lhs0 lhs "STORE"
val ty' = parse_type env ty
in ir_ap("Store", [
ssa_var env ty' src, t_ref, ty', ssa_noconst dst,
......@@ -246,7 +246,7 @@ struct
], ty_inst)
end
| [Word "STORE", Word "PTR", Word ord, Type ty, SSA dst, SSA src] =>
let val _ = lhs0 "STORE"
let val _ = lhs0 lhs "STORE"
val ty' = parse_type env ty
in ir_ap("Store", [
ssa_var env ty' src, t_ptr, ty', ssa_noconst dst,
......@@ -258,18 +258,18 @@ struct
ir_ap("Fence", [mk_return(parse_mem_order ord)], ty_inst)
(* New, Alloca *)
| [Word "NEW", Type ty] =>
ir_ap("New", [lhs1 "NEW", parse_type env ty], ty_inst)
ir_ap("New", [lhs1 lhs "NEW", parse_type env ty], ty_inst)
| [Word "ALLOCA", Type ty] =>
ir_ap("Alloca", [lhs1 "ALLOCA", parse_type env ty], ty_inst)
ir_ap("Alloca", [lhs1 lhs "ALLOCA", parse_type env ty], ty_inst)
| [Word "NEWHYBRID", Type tys, SSA len] =>
let val (t1, t2) = two_tys tys in
ir_ap("NewHybrid", [lhs1 "NEWHYBRID", t1, t2, ssa_var env t2 len],
ir_ap("NewHybrid", [lhs1 lhs "NEWHYBRID", t1, t2, ssa_var env t2 len],
ty_inst)
end
| [Word "ALLOCAHYBRID", Type tys, SSA len] =>
let val (t1, t2) = two_tys tys in
ir_ap("AllocaHybrid", [
lhs1 "ALLOCAHYBRID", t1, t2, ssa_var env t2 len
lhs1 lhs "ALLOCAHYBRID", t1, t2, ssa_var env t2 len
], ty_inst)
end
(* New Thread *)
......@@ -277,7 +277,9 @@ struct
let val (nsc, nil) = parse_new_stack_clause env rest in
case nil of
[] => ir_ap("NewThread", [
lhs1 "NEWTHREAD", ssa_var env (mk_return ``StackRef``) stack, t_null, nsc
lhs1 lhs "NEWTHREAD",
ssa_var env (mk_return ``StackRef``) stack,
t_null, nsc
], ty_inst)
| _ => raise ParseError "invalid arguments for NEWTHREAD"
end
......@@ -330,34 +332,28 @@ struct
fun param (SSA v) = ssa_var env (mk_return(mk_const("Void", ty_type))) v
| param _ = raise ParseError "expected SSA variable"
fun params vs = mk_sequence(map param vs, or_const ty_ssa)
val ty_destarg = ``:ssavar destarg``
val ty_dest = ``:ssavar destination``
val x = mk_var("x", ty_list ty_destarg)
val x = mk_var("x", ty_list (or_const ty_ssa))
fun dest label vs = mk_lift(
mk_abs(x, mk_pair(infer_comb("BlockLabel",
[fromMLstring label], ty_blabel), x)),
mk_sequence(map(
fn (SSA v) => mk_lift(
mk_const("INL", or_const ty_ssa --> ty_destarg),
param (SSA v))
| (RetVal n) => mk_return(
infer_comb("INR", [lift_num ty_num n], ty_destarg))
| _ => raise ParseError "expected SSA variable or $-value"
) vs, ty_destarg))
params vs)
fun calldata(fsig, callee, args) =
let val fsig' = parse_funcsig env fsig in
lift_record(mk_type("calldata", [ty_ssa]), [
("name", mk_bind(
ssa_var env (mk_lift(
infer_comb("FuncRef", [mk_const("REF", ty_reft)],
ty_sig --> ty_type),
parse_funcsig env fsig
ty_sig --> ty_type), fsig'
)) callee,
mk_const("get_callee",
or_const ty_ssa --> or_error (mk_sum(ty_ssa, ty_funcn))))),
("signature", fsig'),
("args", params args),
("convention",
mk_return(mk_const("Mu", mk_type("callconvention", []))))
])
end
fun exc_clause [SSA (Local, l1), Parens a1, SSA (Local, l2), Parens a2] =
lift_record(mk_type("resumption_data", [ty_ssa]), [
("normal_dest", dest l1 a1),
......@@ -372,8 +368,18 @@ struct
| [Word "THROW", v] => ir_ap("Throw", [param v], ty_inst)
| [Word "CALL", Type _, SSA _, Parens _] =>
raise ParseError "terminating CALL must have an EXC clause"
| [_, Eq, Word "CALL", Type _, SSA _, Parens _] =>
raise ParseError "terminating CALL must have an EXC clause"
| [Word "CALL", Type fsig, SSA callee, Parens args, Word "EXC", Parens exc] =>
ir_ap("Call", [calldata(fsig, callee, args), exc_clause exc], ty_inst)
ir_ap("Call", [
mk_return(mk_list([], ty_ssa)),
calldata(fsig, callee, args),
exc_clause exc], ty_inst)
| [lhs, Eq, Word "CALL", Type fsig, SSA callee, Parens args, Word "EXC", Parens exc] =>
ir_ap("Call", [
mk_return(lhs_n lhs "CALL"),
calldata(fsig, callee, args),
exc_clause exc], ty_inst)
| [Word "TAILCALL", Type fsig, SSA callee, Parens args] =>
ir_ap("TailCall", [calldata(fsig, callee, args)], ty_inst)
| [Word "BRANCH", SSA (Local, label), Parens vs] =>
......
......@@ -39,44 +39,56 @@ fun assert_parse_terminst(s, i) =
val _ =
assert_parse_inst("ID <int<8>> %bar",
``Assign [] (Id (Int 8) (Var (SSA "bar")))``);
``Assign [] (Id (Int 8) (Var %"bar"))``);
assert_parse_inst("%foo = ID <int<8>> %bar",
``Assign [SSA "foo"] (Id (Int 8) (Var (SSA "bar")))``);
``Assign [%"foo"] (Id (Int 8) (Var %"bar"))``);
assert_parse_inst("(%foo %bar) = ID <int<8>> %baz",
``Assign [SSA "foo"; SSA "bar"] (Id (Int 8) (Var (SSA "baz")))``);
``Assign [%"foo"; %"bar"] (Id (Int 8) (Var %"baz"))``);
assert_parse_inst("ADD <int<8>> %a %b",
``Assign [] (BinOp ADD (Int 8) (Var (SSA "a")) (Var (SSA "b")))``);
``Assign [] (BinOp ADD (Int 8) (Var %"a") (Var %"b"))``);
assert_parse_inst("UGT <int<8>> %a %b",
``Assign [] (CmpOp UGT (Int 8) (Var (SSA "a")) (Var (SSA "b")))``);
``Assign [] (CmpOp UGT (Int 8) (Var %"a") (Var %"b"))``);
assert_parse_inst("TRUNC <int<8> int<16>> %a",
``Assign [] (ConvOp TRUNC (Int 8) (Int 16) (Var (SSA "a")))``);
``Assign [] (ConvOp TRUNC (Int 8) (Int 16) (Var %"a"))``);
assert_parse_inst("%th = NEWTHREAD %st THROW_EXC %ex",
``NewThread (SSA "th") (Var (SSA "st")) (Const (RefV Void NONE))
(ThrowExc (Var (SSA "ex")))``);
``NewThread (%"th") (Var %"st") (Const (RefV Void NONE))
(ThrowExc (Var %"ex"))``);
assert_parse_inst("%th = NEWTHREAD %st PASS_VALUES <int<8> int<16>> (%a %b)",
``NewThread (SSA "th") (Var (SSA "st")) (Const (RefV Void NONE))
(PassValues [(Var (SSA "a"), Int 8); (Var (SSA "b"), Int 16)])``);
assert_parse_terminst("RET (%foo %bar)", ``Ret [Var (SSA "foo"); Var (SSA "bar")]``);
assert_parse_terminst("THROW %foo", ``Throw (Var (SSA "foo"))``);
``NewThread (%"th") (Var %"st") (Const (RefV Void NONE))
(PassValues [(Var %"a", Int 8); (Var %"b", Int 16)])``);
assert_parse_terminst("RET (%foo %bar)", ``Ret [Var %"foo"; Var %"bar"]``);
assert_parse_terminst("THROW %foo", ``Throw (Var %"foo")``);
assert_parse_terminst("BRANCH %label(%a %b)",
``Branch1 (BlockLabel "label", [PassVar (Var (SSA "a")); PassVar (Var (SSA "b"))])``);
``Branch1 (BlockLabel "label", [Var %"a"; Var %"b"])``);
assert_parse_terminst("BRANCH2 %cond %t() %f()",
``Branch2 (Var (SSA "cond")) (BlockLabel "t", []) (BlockLabel "f", [])``);
``Branch2 (Var %"cond") (BlockLabel "t", []) (BlockLabel "f", [])``);
assert_parse_terminst("TAILCALL <(int<8>) -> ()> %fn (%arg)",
``TailCall <|
name := INL (SSA "fn");
args := [Var (SSA "arg")];
name := INL %"fn";
args := [Var %"arg"];
signature := <|arg_types := [Int 8]; return_types := []|>;
convention := Mu
|>``);
assert_parse_terminst("CALL <(int<8>) -> ()> %fn (%arg) EXC (%n() %e())",
``Call <|
name := INL (SSA "fn");
args := [Var (SSA "arg")];
``Call [] <|
name := INL %"fn";
args := [Var %"arg"];
signature := <|arg_types := [Int 8]; return_types := []|>;
convention := Mu
|> <|
normal_dest := (BlockLabel "n", []);
exceptional_dest := SOME (BlockLabel "e", [])
|>``);
assert_parse_terminst("%x = CALL <(int<8>) -> (int<8>)> %fn (%arg) EXC (%n(%x) %e())",
``Call [%"x"] <|
name := INL %"fn";
args := [Var %"arg"];
signature := <|arg_types := [Int 8]; return_types := [Int 8]|>;
convention := Mu
|> <|
normal_dest := (BlockLabel "n", [Var %"x"]);
exceptional_dest := SOME (BlockLabel "e", [])
|>``);
(* Equality testing for basic blocks and functions is nigh-impossible, so
instead just run the parsing functions and make sure they don't throw.
......@@ -97,7 +109,7 @@ val _ =
BRANCH2 %is1 %done() %recur(%n)
%recur(<int<8>> %n):
%minus1 = SUB <int<8>> %n %one
CALL <(int<8>) -> (int<8>)> %fact (%minus1) EXC (%mul(%n $0) %done())
%x = CALL <(int<8>) -> (int<8>)> %fact (%minus1) EXC (%mul(%n %x) %done())
%mul(<int<8>> %m <int<8>> %n):
%result = MUL <int<8>> %m %n
RET (%result)
......
......@@ -25,7 +25,7 @@ val fact_rec = uir_bundle`
%minus1 = SUB <@i16> %n @one // .
// CALL requires an exception clause, but fact can't throw an exception
// so the (unreachable) exception clause goes to %done.
CALL <@fact_sig> @fact (%minus1) EXC (%mul(%n $0) %done()) // .
%m = CALL <@fact_sig> @fact (%minus1) EXC (%mul(%n %m) %done()) // .
%mul(<@i16> %m <@i16> %n):
%result = MUL <@i16> %m %n
RET (%result)
......
......@@ -130,19 +130,8 @@ val _ = define_sum("or_const",
"Var", ``:σ``,
"Const", ``:value``)
(* Either a variable or a $-notation return value index
$-notation is used for the destinations of CALL, to pass return values that
don't get assigned SSA variables. e.g.,
CALL m(...args...) EXC(%ndbl(%x, $2) %hbl($1, %a))
*)
val _ = define_sum("destarg",
"PassVar", ``:σ or_const``,
"PassReturnVal", ``:num``)
(* A block label with arguments *)
val _ = type_abbrev("destination", ``:block_label # σ destarg list``)
val _ = type_abbrev("destination", ``:block_label # σ or_const list``)
val _ = Datatype`
resumption_data = <|
......@@ -153,6 +142,7 @@ val _ = Datatype`
calldata = <|
name : σ + func_name ; (* allowing for indirect calls *)
args : σ or_const list ;
signature : funcsig ;
convention : callconvention
|> ;
......@@ -331,7 +321,7 @@ val _ = Datatype`
terminst =
| Ret (σ or_const list)
| Throw (σ or_const)
| Call (σ calldata) (σ resumption_data)
| Call (σ list) (σ calldata) (σ resumption_data)
| TailCall (σ calldata)
| Branch1 (σ destination)
| Branch2 (σ or_const) (σ destination) (σ destination)
......@@ -349,13 +339,14 @@ val _ = Datatype`
(σ resumption_data)
| WPBranch wpid (σ destination) (σ destination)
| SwapStack
σ (* swappee - stackref *)
(σ list)
(σ or_const) (* swappee - stackref *)
(σ or_const new_stack_clause)
cur_stack_clause
(σ resumption_data)
| CommInst
comm_inst
(σ comm_inst_args)
(σ list)
(σ comminst)
(σ resumption_data)
| ExcClause
(σ instruction)
......@@ -373,24 +364,22 @@ val _ = Datatype`
wpid = WPID num ;
comm_inst =
| CI_NewStack (* @uvm.new_stack *)
| CI_CurrentStack (* @uvm.current_stack *) ;
comm_inst_args = <|
flag_list: string list;
type_list: uvm_type list;
func_sig_list: sig_name list;
arg_list: σ or_const list
|> ;
new_stack_clause =
| PassValues ((σ # uvm_type) list)
| ThrowExc σ ;
cur_stack_clause =
| RetWith (uvm_type list)
| KillOld
| KillOld ;
comminst =
| NewStack funcsig (σ or_const)
| CurrentStack
`
val comminst_return_types_def = Define`
comminst_return_types (NewStack _ _) = [StackRef]
comminst_return_types CurrentStack = [StackRef]
`
(* Map functions: map the SSA variables in expressions, instructions, etc. to
......@@ -401,22 +390,14 @@ val map_calldata_def = Define`
map_calldata (f : α -> β) (cd : α calldata) : β calldata = <|
name := f <$> cd.name ;
args := MAP (lift_left f) cd.args ;
signature := cd.signature ;
convention := cd.convention
|>
`
val map_comm_inst_args_def = Define`
map_comm_inst_args (f : α -> β) (a : α comm_inst_args) : β comm_inst_args = <|
flag_list := a.flag_list ;
type_list := a.type_list ;
func_sig_list := a.func_sig_list ;
arg_list := MAP (lift_left f) a.arg_list
|>
`
val map_dest_def = Define`
map_dest (f : α -> β) : α destination -> β destination =
I ## (MAP o lift_left o lift_left) f
I ## (MAP o lift_left) f
`
val map_new_stack_clause_def = Define`
......@@ -474,6 +455,11 @@ val map_inst_def = Define`
NewThread (f v) (f <$> s) (f <$> tl) (map_new_stack_clause f nsc)
`
val map_comminst_def = Define`
map_comminst f (NewStack sig fref) = NewStack sig (f <$> fref)
map_comminst f CurrentStack = CurrentStack
`
val map_terminst_def = Define`
map_terminst (f : α -> β) (inst : α terminst) : β terminst =
let map_rd : α resumption_data -> β resumption_data =
......@@ -484,7 +470,7 @@ val map_terminst_def = Define`
case inst of
| Ret vals => Ret (MAP (lift_left f) vals)
| Throw v => Throw (f <$> v)
| Call cd rd => Call (map_calldata f cd) (map_rd rd)
| Call vs cd rd => Call (MAP f vs) (map_calldata f cd) (map_rd rd)
| TailCall cd => TailCall (map_calldata f cd)
| Branch1 dst => Branch1 (map_dest f dst)
| Branch2 cond dst1 dst2 =>
......@@ -494,9 +480,9 @@ val map_terminst_def = Define`
| Watchpoint wpdst tys rd =>
Watchpoint (OPTION_MAP (I ## map_dest f) wpdst) tys (map_rd rd)
| WPBranch id dst1 dst2 => WPBranch id (map_dest f dst1) (map_dest f dst2)
| SwapStack v nsc csc rd =>
SwapStack (f v) (map_new_stack_clause f nsc) csc (map_rd rd)
| CommInst ci args rd => CommInst ci (map_comm_inst_args f args) (map_rd rd)
| SwapStack vs v nsc csc rd =>
SwapStack (MAP f vs) (f <$> v) (map_new_stack_clause f nsc) csc (map_rd rd)
| CommInst vs ci rd => CommInst (MAP f vs) (map_comminst f ci) (map_rd rd)
| ExcClause inst rd => ExcClause (map_inst f inst) (map_rd rd)
`
......@@ -539,9 +525,9 @@ val inst_vars_def = Define`
inst_vars (CmpXchg v1 v2 _ _ _ _ _ loc exp des) =
({loc} left_set exp left_set des, {v1; v2})
inst_vars (AtomicRMW v _ _ _ _ loc opnd) = ({loc} left_set opnd, {v})
inst_vars (Fence _) = ({}, {})
inst_vars (New v _) = ({}, {v})
inst_vars (Alloca v _) = ({}, {v})
inst_vars (Fence _) = (, )
inst_vars (New v _) = (, {v})
inst_vars (Alloca v _) = (, {v})
inst_vars (NewHybrid v _ _ len) = (left_set len, {v})
inst_vars (AllocaHybrid v _ _ len) = (left_set len, {v})
inst_vars (NewThread v s tl nsc) =
......@@ -554,6 +540,11 @@ val inst_output_vars_def = Define`inst_output_vars i = SND (inst_vars i)`
val inst_all_vars_def = Define`inst_all_vars i = let (a, b) = inst_vars i in a b`
val comminst_vars_def = Define`
comminst_vars (NewStack _ fref) = left_set fref
comminst_vars CurrentStack =
`
(* Given a terminal instruction, returns a pair of sets (input variables, passed
variables). The union of these sets is the set of all variables referenced by
the instruction.
......@@ -567,28 +558,28 @@ val terminst_vars_def = Define`
terminst_vars (inst : α terminst) : α set # α set =
let flat_left_set = λl. BIGUNION (IMAGE left_set (set l)) in
let dest_vars : α destination -> α set =
λ(_, args) v. MEM (PassVar (Var v)) args in
λ(_, args) v. MEM (Var v) args in
let rd_vars : α resumption_data -> α set =
λrd. dest_vars rd.normal_dest (
case rd.exceptional_dest of
| SOME d => dest_vars d
| NONE => {}) in
| NONE => ) in
case inst of
| Ret vals => {}, flat_left_set vals
| Throw v => {}, left_set v
| Call cd rd => left_set cd.name, flat_left_set cd.args rd_vars rd
| Ret vals => , flat_left_set vals
| Throw v => , left_set v
| Call vs cd rd => left_set cd.name, set vs flat_left_set cd.args rd_vars rd
| TailCall cd => left_set cd.name, flat_left_set cd.args
| Branch1 dst => {}, dest_vars dst
| Branch1 dst => , dest_vars dst
| Branch2 cond dst1 dst2 => left_set cond, dest_vars dst1 dest_vars dst2
| Switch _ cond def_dst branches =>
left_set cond,
dest_vars def_dst λvr.vl. vr dest_vars (branches ' vl)
| Watchpoint NONE _ rd => {}, rd_vars rd
| Watchpoint (SOME (id, dst)) _ rd => {}, dest_vars dst rd_vars rd
| WPBranch id dst1 dst2 => {}, dest_vars dst1 dest_vars dst2
| SwapStack id nsc _ rd =>
{id}, new_stack_clause_vars nsc rd_vars rd
| CommInst ci args rd => flat_left_set args.arg_list, rd_vars rd
| Watchpoint NONE _ rd => , rd_vars rd
| Watchpoint (SOME (id, dst)) _ rd => , dest_vars dst rd_vars rd
| WPBranch id dst1 dst2 => , dest_vars dst1 dest_vars dst2
| SwapStack vs id nsc _ rd =>
left_set id, set vs new_stack_clause_vars nsc rd_vars rd
| CommInst vs ci rd => comminst_vars ci, set vs rd_vars rd
| ExcClause inst rd => inst_input_vars inst, rd_vars rd
`
......@@ -684,22 +675,13 @@ in
simp[map_calldata_def, theorem "calldata_component_equality"] >>
metis_tac[lift_left_compose, o_THM, MAP_o])
val map_comm_inst_args_id = store_thm("map_comm_inst_args_id[simp]",
``map_comm_inst_args I x = x``,
simp[map_comm_inst_args_def, lift_I, theorem "comm_inst_args_component_equality"])
val map_comm_inst_args_compose = store_thm("map_comm_inst_args_compose[simp]",
``map_comm_inst_args (f o g) x = map_comm_inst_args f (map_comm_inst_args g x)``,
simp[map_comm_inst_args_def, theorem "comm_inst_args_component_equality"] >>
metis_tac[lift_left_compose, o_THM, MAP_o])
val map_dest_id = store_thm("map_dest_id[simp]",
``map_dest I x = x``,
simp[map_dest_def, lift_I, pair_I, pair_map_I])
val map_dest_compose = store_thm("map_dest_compose[simp]",
``map_dest (f o g) x = map_dest f (map_dest g x)``,
simp[map_dest_def, pair_map_def] >>
metis_tac[MAP_MAP_o, lift_left_compose, o_DEF]
)
metis_tac[MAP_MAP_o, lift_left_compose, o_DEF])
val map_new_stack_clause_id = store_thm("map_new_stack_clause_id[simp]",
``map_new_stack_clause I x = x``,
......@@ -728,13 +710,19 @@ in
simp[map_inst_def, MAP_o, lift_left_compose, OPTION_MAP_COMPOSE]
>- (metis_tac[map_expr_compose, lift_left_compose, o_THM]))
val map_comminst_id = store_thm("map_comminst_id[simp]",
``map_comminst I x = x``,
Cases_on `x` >> simp[map_comminst_def])
val map_comminst_compose = store_thm("map_comminst_compose[simp]",
``map_comminst (f o g) x = map_comminst f (map_comminst g x)``,
Cases_on `x` >> simp[map_comminst_def])
val map_terminst_id = store_thm("map_terminst_id[simp]",
``map_terminst I x = x``,
`map_dest I = I` by metis_tac[map_dest_id, I_THM] >>
Cases_on `x` >>
fs[map_terminst_def, lift_I, pair_I, pair_map_I, option_map_I,
I_THM, theorem "resumption_data_component_equality"]
fs[map_terminst_def, lift_I, pair_I, pair_map_I, option_map_I, I_THM,
theorem "resumption_data_component_equality"]
>- metis_tac[I_THM, o_f_FAPPLY, o_f_FDOM, fmap_EQ_THM])
val map_terminst_compose = store_thm("map_terminst_compose[simp]",
``map_terminst (f o g) x = map_terminst f (map_terminst g x)``,
......@@ -760,7 +748,7 @@ in
SND (inst_vars (map_inst f x)) = IMAGE f (SND (inst_vars x))``,
Cases_on `x` >>
simp[map_inst_def, inst_vars_def, map_expr_vars, left_set_def,
map_new_stack_clause_def, left_set_image, map_comm_inst_args_def,
map_new_stack_clause_def, left_set_image,
LIST_TO_SET_MAP, IMAGE_BIGUNION, IMAGE_COMPOSE]
>- metis_tac[left_set_def, lift_left_def, left_set_image, o_THM,
IMAGE_BIGUNION, IMAGE_COMPOSE]
......
......@@ -6,6 +6,7 @@ open uvmErrorsTheory
open DefineUtils
open monadsyntax
open listTheory
open Parse
val _ = new_theory "uvmMemory"
......@@ -36,6 +37,19 @@ val _ = type_abbrev("uvm_error", ``:(addr, func_name) gen_uvm_error``)
val _ = type_abbrev("or_error", ``:α + uvm_error``)
val _ = type_abbrev("register", ``:ssavar # block_id``)
val _ = add_rule {term_name = "%",
fixity = Prefix 780,
pp_elements = [TOK "%"],
paren_style = OnlyIfNecessary,
block_style = (AroundEachPhrase, (PP.CONSISTENT, 0))}