Commit 0142a14c authored by Adam Nelson's avatar Adam Nelson
Browse files

Add multiple stacks, separate stacks from threads

parent e6a34aa8
......@@ -137,7 +137,7 @@ struct
mk_abs(t_gls, infer_comb("CONS",
[mk_pair(t_gln, t_ty), t_gls], ty_list ty_gl)),
add_env_const name t_ty (infer_comb("RefV",
[t_ty, infer_comb("GlobalAddr", [t_gln], ty_addr)], ty_val))
[t_ty, mk_some(infer_comb("GlobalAddr", [t_gln], ty_addr))], ty_val))
], ty_env)),
parse_type env ty)
end
......
......@@ -49,6 +49,13 @@ 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))
]
val ty_ssa = mk_type("ssavar", [])
val ty_blabel = mk_type("block_label", [])
fun or_const ty = ``:^ty or_const``
......@@ -57,6 +64,9 @@ struct
val t_Const = mk_const("INR", ty_val --> or_const ty_ssa)
val t_SSA = mk_const("SSA", ty_str --> ty_ssa)
fun mk_ssa s = mk_comb(t_SSA, fromMLstring s)
fun mk_some x =
let val ty = type_of x
in mk_comb(mk_const("SOME", ty --> mk_type("option", [ty])), x) end
fun ir_const (name : string) (ty : hol_type) : term =
mk_thy_const { Thy="uvmIR", Name=name, Ty=ty }
......@@ -79,7 +89,7 @@ struct
mk_lift(t_Const, mk_bind(ty, mk_pattern_fn[
(ty_pat "FuncRef" [t_rt, t_sig],
mk_return(infer_comb("FuncRefV",
[t_rt, t_sig, infer_comb("Func", [fromMLstring v], ty_funcn)],
[t_rt, t_sig, mk_some(infer_comb("Func", [fromMLstring v], ty_funcn))],
ty_val))),
(mk_var("ty", ty_type),
(#get_global env) v)]))
......@@ -314,7 +324,9 @@ struct
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),
("exceptional_dest", dest l2 a2)
("exceptional_dest", mk_lift(
mk_const("SOME", ty_dest --> mk_type("option", [ty_dest])),
dest l2 a2))
])
| exc_clause _ = raise ParseError "invalid syntax for EXC clause"
val ty_inst = mk_type("terminst", [ty_ssa])
......
......@@ -25,6 +25,7 @@ sig
val or_error : hol_type -> hol_type
val infer_comb : string * term list * hol_type -> term
val mk_some : term -> term
val mk_return : term -> term
val mk_bind : term * term -> term
val mk_sequence : term list * hol_type -> term
......
......@@ -29,9 +29,11 @@ struct
val ty_sig = mk_type("funcsig", [])
val ty_addr = mk_type("addr", [])
val ty_funcn = mk_type("func_name", [])
val ty_sid = mk_type("stack_id", [])
val ty_tid = mk_type("thread_id", [])
val ty_iaddr = mk_type("gen_iaddr", [ty_addr])
val ty_err = mk_type("gen_uvm_error", [ty_addr, ty_funcn])
val ty_val = mk_type("gen_value", [ty_addr, ty_funcn])
val ty_val = mk_type("gen_value", [ty_addr, ty_funcn, ty_sid, ty_tid])
fun ty_list ty = mk_type("list", [ty])
fun or_error ty = sumSyntax.mk_sum(ty, ty_err)
......@@ -51,6 +53,10 @@ struct
})
in list_mk_comb(f, args) end
fun mk_some x =
let val ty = type_of x
in mk_comb(mk_const("SOME", ty --> mk_type("option", [ty])), x) end
fun mk_return t = infer_comb("INL", [t], or_error (type_of t))
fun mk_bind(lhs, rhs) =
......
......@@ -30,7 +30,7 @@ struct
in mk_pattern_fn[
(ty_pat "Ref" [mk_comb(t_Type, t_ty)],
mk_return(infer_comb("RefV",
[t_ty, mk_const("NullAddr", ty_addr)],
[t_ty, mk_const("NONE", mk_type("option", [ty_addr]))],
ty_val))),
(t_ty,
invalid_ir "NULL constant has non-ref type")]
......
......@@ -26,7 +26,7 @@ val global_cell_test = uir_bundle`
} // .
` |> to_env |> start_at "main" `[IntV 8 4w]`
|> run_schedule `single_thread_seq_cst_schedule`
|> expect_result `OK (NOR, [IntV 8 4w])`
|> expect_result `OK (NOR [IntV 8 4w])`
val heap_alloc_test = uir_bundle`
.typedef @i8 = int<8>
......@@ -41,7 +41,7 @@ val heap_alloc_test = uir_bundle`
} // .
` |> to_env |> start_at "main" `[IntV 8 4w]`
|> run_schedule `single_thread_seq_cst_schedule`
|> expect_result `OK (NOR, [IntV 8 4w])`
|> expect_result `OK (NOR [IntV 8 4w])`
val stack_alloc_test = uir_bundle`
.typedef @i8 = int<8>
......@@ -56,7 +56,7 @@ val stack_alloc_test = uir_bundle`
} // .
` |> to_env |> start_at "main" `[IntV 8 4w]`
|> run_schedule `single_thread_seq_cst_schedule`
|> expect_result `OK (NOR, [IntV 8 4w])`
|> expect_result `OK (NOR [IntV 8 4w])`
val _ = export_theory()
......@@ -28,10 +28,10 @@ val bundle1 = uir_bundle`
val state1 = bundle1 |> to_env |> start_at "add_two" `[IntV 8 3w]`
val _ = state1 |> run_finite_schedule `[Proceed (Thread 0) NONE]`
|> expect_result `OK (NOR, [IntV 8 5w])`
|> expect_result `OK (NOR [IntV 8 5w])`
val _ = state1 |> run_schedule `cycle [Proceed (Thread 0) NONE]`
|> expect_result `OK (NOR, [IntV 8 5w])`
|> expect_result `OK (NOR [IntV 8 5w])`
val _ = export_theory()
......@@ -69,7 +69,7 @@ val _ =
convention := Mu
|> <|
normal_dest := (BlockLabel "n", []);
exceptional_dest := (BlockLabel "e", [])
exceptional_dest := SOME (BlockLabel "e", [])
|>``);
(* Equality testing for basic blocks and functions is nigh-impossible, so
......
......@@ -37,12 +37,12 @@ val fact_rec = uir_bundle`
val fact2_rec_test =
fact_rec |> start_at "fact" `[IntV 16 2w]`
|> run_schedule `cycle [Proceed (Thread 0) NONE]`
|> expect_result `OK (NOR, [IntV 16 2w])`
|> expect_result `OK (NOR [IntV 16 2w])`
val fact5_rec_test =
fact_rec |> start_at "fact" `[IntV 16 5w]`
|> run_schedule `cycle [Proceed (Thread 0) NONE]`
|> expect_result `OK (NOR, [IntV 16 120w])`
|> expect_result `OK (NOR [IntV 16 120w])`
val fact_iter = uir_bundle`
.typedef @i16 = int<16>
......@@ -66,12 +66,12 @@ val fact_iter = uir_bundle`
val fact2_iter_test =
fact_iter |> start_at "fact" `[IntV 16 2w]`
|> run_schedule `cycle [Proceed (Thread 0) NONE]`
|> expect_result `OK (NOR, [IntV 16 2w])`
|> expect_result `OK (NOR [IntV 16 2w])`
val fact5_iter_test =
fact_iter |> start_at "fact" `[IntV 16 5w]`
|> run_schedule `cycle [Proceed (Thread 0) NONE]`
|> expect_result `OK (NOR, [IntV 16 120w])`
|> expect_result `OK (NOR [IntV 16 120w])`
val _ = export_theory()
......@@ -25,8 +25,8 @@ fun assert_parse(s, t, vq) =
val _ =
assert_parse("1", ``Int 8``, `IntV 8 1w`);
assert_parse("91", ``Int 32``, `IntV 32 91w`);
assert_parse("NULL", ``Ref (Type Void)``, `RefV Void NullAddr`);
assert_parse("NULL", ``Ref (Type (Int 8))``, `RefV (Int 8) NullAddr`);
assert_parse("NULL", ``Ref (Type Void)``, `RefV Void NONE`);
assert_parse("NULL", ``Ref (Type (Int 8))``, `RefV (Int 8) NONE`);
assert_parse("{5 6}", ``Array (Int 8) 2``, `ArrayV (Int 8) [IntV 8 5w; IntV 8 6w]`);
(*
(* FIXME: This doesn't parse yet; something's wrong with take_one_value *)
......
......@@ -17,6 +17,7 @@ val _ = Datatype`
| ReadOutOfBounds uvm_type num
| WriteOutOfBounds uvm_type num
| UnallocatedMemory 'addr
| NullReference
| DivideByZero
| UndefinedBehavior string (* for all other kinds of undefined behavior *)
......
......@@ -147,7 +147,7 @@ val _ = type_abbrev("destination", ``:block_label # σ destarg list``)
val _ = Datatype`
resumption_data = <|
normal_dest : σ destination ;
exceptional_dest : σ destination
exceptional_dest : σ destination option
|> ;
calldata = <|
......@@ -167,8 +167,7 @@ val get_callee_def = Define`
get_callee (callee : ssavar or_const) : (ssavar + func_name) or_error =
case callee of
| Var v => return (INL v)
| Const (FuncRefV _ _ name) => return (INR name)
| Const v => Fail (NotCallable (type_of_value v))
| Const c => liftM (INR o SND) (get_funcref_data c)
`
(* Type for expressions, instructions which do not contain a reference to their
......@@ -326,10 +325,7 @@ val _ = Datatype`
| NewThread
σ (* output: threadref *)
(σ option) (* threadlocal *)
(σ new_stack_clause)
| CommInst
(σ list) (* output variable(s) *)
(σ comm_inst_args) ;
(σ new_stack_clause) ;
terminst =
| Ret (σ or_const list)
......@@ -356,7 +352,8 @@ val _ = Datatype`
(σ new_stack_clause)
cur_stack_clause
(σ resumption_data)
| TermCommInst
| CommInst
comm_inst
(σ comm_inst_args)
(σ resumption_data)
| ExcClause
......@@ -375,8 +372,11 @@ val _ = Datatype`
wpid = WPID num ;
comm_inst =
| CI_NewStack (* @uvm.new_stack *)
| CI_CurrentStack (* @uvm.current_stack *) ;
comm_inst_args = <|
inst: string;
flag_list: string list;
type_list: uvm_type list;
func_sig_list: sig_name list;
......@@ -406,7 +406,6 @@ val map_calldata_def = Define`
val map_comm_inst_args_def = Define`
map_comm_inst_args (f : α -> β) (a : α comm_inst_args) : β comm_inst_args = <|
inst := a.inst ;
flag_list := a.flag_list ;
type_list := a.type_list ;
func_sig_list := a.func_sig_list ;
......@@ -414,6 +413,11 @@ val map_comm_inst_args_def = Define`
|>
`
val map_dest_def = Define`
map_dest (f : α -> β) : α destination -> β destination =
I ## (MAP o lift_left o lift_left) f
`
val map_expr_def = Define`
map_expr (f : α -> β) (expr : α expression) : β expression =
case expr of
......@@ -461,38 +465,35 @@ val map_inst_def = Define`
case nsc of
| PassValues vs => PassValues (MAP (f ## I) vs)
| ThrowExc e => ThrowExc (f e))
| CommInst vs args => CommInst (MAP f vs) (map_comm_inst_args f args)
`
val map_terminst_def = Define`
map_terminst (f : α -> β) (inst : α terminst) : β terminst =
let map_dest : α destination -> β destination =
I ## (MAP o lift_left o lift_left) f in
let map_rd : α resumption_data -> β resumption_data =
λrd. <|
normal_dest := map_dest rd.normal_dest ;
exceptional_dest := map_dest rd.exceptional_dest
normal_dest := map_dest f rd.normal_dest ;
exceptional_dest := OPTION_MAP (map_dest f) rd.exceptional_dest
|> in
case inst of
| Ret vals => Ret (MAP (lift_left f) vals)
| Throw vals => Throw (MAP (lift_left f) vals)
| Call cd rd => Call (map_calldata f cd) (map_rd rd)
| TailCall cd => TailCall (map_calldata f cd)
| Branch1 dst => Branch1 (map_dest dst)
| Branch1 dst => Branch1 (map_dest f dst)
| Branch2 cond dst1 dst2 =>
Branch2 (lift_left f cond) (map_dest dst1) (map_dest dst2)
Branch2 (lift_left f cond) (map_dest f dst1) (map_dest f dst2)
| Switch t cond dst branches =>
Switch t (lift_left f cond) (map_dest dst) (map_dest o_f branches)
Switch t (lift_left f cond) (map_dest f dst) (map_dest f o_f branches)
| Watchpoint wpdst tys rd =>
Watchpoint (OPTION_MAP (I ## map_dest) wpdst) tys (map_rd rd)
| WPBranch id dst1 dst2 => WPBranch id (map_dest dst1) (map_dest dst2)
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) (
case nsc of
| PassValues vs => PassValues (MAP (f ## I) vs)
| ThrowExc e => ThrowExc (f e)
) csc (map_rd rd)
| TermCommInst args rd => TermCommInst (map_comm_inst_args f args) (map_rd rd)
| CommInst ci args rd => CommInst ci (map_comm_inst_args f args) (map_rd rd)
| ExcClause inst rd => ExcClause (map_inst f inst) (map_rd rd)
`
......@@ -545,7 +546,6 @@ val inst_vars_def = Define`
| PassValues vs => set (MAP FST vs)
| ThrowExc e => {e}
), {v}
| CommInst vs ci => BIGUNION (IMAGE left_set (set ci.arg_list)), set vs
`
val inst_input_vars_def = Define`inst_input_vars i = FST (inst_vars i)`
......@@ -569,7 +569,10 @@ val terminst_vars_def = Define`
let dest_vars : α destination -> α set =
λ(_, args) v. MEM (PassVar (Var v)) args in
let rd_vars : α resumption_data -> α set =
λrd. dest_vars rd.normal_dest dest_vars rd.exceptional_dest in
λrd. dest_vars rd.normal_dest (
case rd.exceptional_dest of
| SOME d => dest_vars d
| NONE => {}) in
case inst of
| Ret vals => {}, flat_left_set vals
| Throw vals => {}, flat_left_set vals
......@@ -589,7 +592,7 @@ val terminst_vars_def = Define`
| PassValues vs => set (MAP FST vs)
| ThrowExc e => {e}
) rd_vars rd
| TermCommInst ci rd => flat_left_set ci.arg_list, rd_vars rd
| CommInst ci args rd => flat_left_set args.arg_list, rd_vars rd
| ExcClause inst rd => inst_input_vars inst, rd_vars rd
`
......@@ -664,89 +667,95 @@ local
open optionTheory
open finite_mapTheory
open pred_setTheory
val lift_I = Q.prove(`lift_left I = I`, metis_tac[lift_left_id, I_THM])
val pair_I = Q.prove(`(I ## I) = I`, metis_tac[PAIR, PAIR_MAP, I_THM])
val pair_map_def = Q.prove(`(f ## g) = λp. (f (FST p), g (SND p))`,
val lift_I = prove(``lift_left I = I``, metis_tac[lift_left_id, I_THM])
val pair_I = prove(``(I ## I) = I``, metis_tac[PAIR, PAIR_MAP, I_THM])
val pair_map_def = prove(``(f ## g) = λp. (f (FST p), g (SND p))``,
metis_tac[PAIR, PAIR_MAP])
val pair_fst_compose = Q.prove(`f o g ## I = (f ## I) o (g ## I)`,
val pair_fst_compose = prove(``f o g ## I = (f ## I) o (g ## I)``,
rw[pair_map_def, o_DEF])
val pair_map_I = Q.prove(`(I ## MAP I) = I`, metis_tac[pair_I, I_THM, MAP_ID])
val pair_map_I = prove(``(I ## MAP I) = I``, metis_tac[pair_I, I_THM, MAP_ID])
val option_map_I = prove(``x. OPTION_MAP I x = x``, Cases >> rw[OPTION_MAP_DEF])
in
(* The mapping functions should obey the functor laws:
- `map I x = x`
- `map (f o g) x = map f (map g x)`
*)
val map_calldata_id = Q.store_thm(
"map_calldata_id[simp]",
`map_calldata I x = x`,
val map_calldata_id = store_thm("map_calldata_id[simp]",
``map_calldata I x = x``,
simp[map_calldata_def, lift_I, theorem "calldata_component_equality"])
val map_calldata_compose = Q.store_thm(
"map_calldata_compose[simp]",
`map_calldata (f o g) x = map_calldata f (map_calldata g x)`,
val map_calldata_compose = store_thm("map_calldata_compose[simp]",
``map_calldata (f o g) x = map_calldata f (map_calldata g x)``,
simp[map_calldata_def, theorem "calldata_component_equality"] >>
metis_tac[lift_left_compose, o_THM, MAP_o])
val map_comm_inst_args_id = Q.store_thm(
"map_comm_inst_args_id[simp]",
`map_comm_inst_args I x = x`,
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 = Q.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)`,
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_expr_id = Q.store_thm(
"map_expr_id[simp]",
`map_expr I x = x`,
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])
val map_expr_id = store_thm("map_expr_id[simp]",
``map_expr I x = x``,
Cases_on `x` >> simp[map_expr_def, lift_I])
val map_expr_compose = Q.store_thm(
"map_expr_compose[simp]",
`map_expr (f o g) x = map_expr f (map_expr g x)`,
val map_expr_compose = store_thm("map_expr_compose[simp]",
``map_expr (f o g) x = map_expr f (map_expr g x)``,
Cases_on `x` >> simp[map_expr_def] >>
metis_tac[lift_left_compose, o_THM, MAP_o])
val map_inst_id = Q.store_thm(
"map_inst_id[simp]",
`map_inst I x = x`,
val map_inst_id = store_thm("map_inst_id[simp]",
``map_inst I x = x``,
Cases_on `x` >> simp[map_inst_def, lift_I, pair_I] >>
rename1 `OPTION_MAP I opt = opt` >> Cases_on `opt` >> simp[] >>
Cases_on `n` >> simp[])
val map_inst_compose = Q.store_thm(
"map_inst_compose[simp]",
`map_inst (f o g) x = map_inst f (map_inst g x)`,
val map_inst_compose = store_thm("map_inst_compose[simp]",
``map_inst (f o g) x = map_inst f (map_inst g x)``,
Cases_on `x` >>
simp[map_inst_def, MAP_o, lift_left_compose, OPTION_MAP_COMPOSE]
>- (metis_tac[map_expr_compose, lift_left_compose, o_THM])
>- (Cases_on `n` >> simp[pair_fst_compose, MAP_MAP_o]))
val map_terminst_id = Q.store_thm(
"map_terminst_id[simp]",
`map_terminst I x = x`,
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` >>
simp[map_terminst_def, lift_I, pair_I, pair_map_I,
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]
>- (rename1 `OPTION_MAP I opt = opt` >> Cases_on `opt` >> simp[])
>- (Cases_on `n` >> simp[]))
val map_inst_compose = Q.store_thm(
"map_inst_compose[simp]",
`map_inst (f o g) x = map_inst f (map_inst g x)`,
val map_terminst_compose = store_thm("map_terminst_compose[simp]",
``map_terminst (f o g) x = map_terminst f (map_terminst g x)``,
Cases_on `x` >>
simp[map_terminst_def, lift_left_compose, MAP_o, OPTION_MAP_COMPOSE,
theorem "resumption_data_component_equality"])
rw[map_terminst_def, lift_left_compose, MAP_o, OPTION_MAP_COMPOSE,
theorem "resumption_data_component_equality",
prove(
``x. MAP (lift_left (f o g)) x = MAP (lift_left f) (MAP (lift_left g) x)``,
metis_tac[MAP_MAP_o, lift_left_compose, o_DEF]),
prove(
``map_dest (f o g) = map_dest f o map_dest g``,
metis_tac[map_dest_compose, o_DEF])]
>- (Cases_on `o'` >> simp[OPTION_MAP_DEF, pair_map_def])
>- (Cases_on `n` >> simp[] >> rw[pair_fst_compose, MAP_MAP_o]))
(* The mapping functions should map all variables included in an expression or
instruction's variable set(s).
*)
val map_expr_vars = Q.store_thm(
"map_expr_vars",
`expr_vars (map_expr f x) = IMAGE f (expr_vars x)`,
val map_expr_vars = store_thm("map_expr_vars",
``expr_vars (map_expr f x) = IMAGE f (expr_vars x)``,
Cases_on `x` >> simp[map_expr_def, expr_vars_def])
val map_inst_vars = Q.store_thm(
"map_inst_vars",
`FST (inst_vars (map_inst f x)) = IMAGE f (FST (inst_vars x))
SND (inst_vars (map_inst f x)) = IMAGE f (SND (inst_vars x))`,
val map_inst_vars = store_thm("map_inst_vars",
``FST (inst_vars (map_inst f x)) = IMAGE f (FST (inst_vars x))
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,
left_set_image, map_comm_inst_args_def, LIST_TO_SET_MAP,
......
......@@ -14,63 +14,27 @@ val _ = add_monadsyntax()
val _ = ParseExtras.tight_equality()
val _ = define_num_newtype("thread_id", "Thread")
val _ = define_num_newtype("stack_id", "Stack")
val _ = define_num_newtype("block_id", "Block")
val _ = define_num_newtype("action_id", "Action")
val _ = define_num_newtype("frame_id", "Frame")
val _ = Datatype`
stack_id = Stack thread_id action_id ;
ssavar = SSA string ;
global_name = Global string ;
func_name = Func string ;
func_version = FuncVersion func_name num ;
addr =
| NullAddr
| GlobalAddr global_name
| StackAddr thread_id stack_id frame_id action_id
| StackAddr stack_id thread_id action_id
| HeapAddr thread_id action_id
`
val _ = type_abbrev("value", ``:(addr, func_name) gen_value``)
val _ = type_abbrev("value", ``:(addr, func_name, stack_id, thread_id) gen_value``)
val _ = type_abbrev("iaddr", ``:addr gen_iaddr``)
val _ = type_abbrev("uvm_error", ``:(addr, func_name) gen_uvm_error``)
val _ = type_abbrev("or_error", ``:α + uvm_error``)
val _ = type_abbrev("register", ``:ssavar # frame_id``)
val zero_value_def = TotalDefn.tDefine "zero_value" `
zero_value Void _ = Fail (InvalidIR "cannot allocate void")
zero_value (Int sz) _ = return (IntV sz 0w)
zero_value Float _ = return (FloatV 0w)
zero_value Double _ = return (DoubleV 0w)
zero_value (Ref _) _ = return (RefV Void NullAddr)
zero_value (IRef rt _) _ = return (
IRefV rt <| base := NullAddr; offsets := []; base_ty := Void; ty := Void |>)
zero_value (WeakRef _) _ = Fail (NotImplemented "weakref")
zero_value (FuncRef rt sig) _ = return (FuncRefV rt sig (Func ""))
zero_value ThreadRef _ = Fail (NotImplemented "threadref")
zero_value StackRef _ = Fail (NotImplemented "stackref")
zero_value TagRef64 _ = Fail (NotImplemented "tagref64")
zero_value (Array t n) _ = do
el <- zero_value t NONE;
return (ArrayV t (GENLIST (K el) n))
od
zero_value (Vector t n) _ = do
el <- zero_value t NONE;
return (VectorV t (GENLIST (K el) n))
od
zero_value (Hybrid fts vt) (SOME len) = do
fvs <- sequence (MAP (λt. zero_value t NONE >>= λv. return (v, t)) fts);
vv <- zero_value vt NONE;
return (HybridV fvs vt (GENLIST (K vv) len))
od
zero_value (Struct fx ts) _ = do
vs <- sequence (MAP (λt. zero_value t NONE >>= λv. return (v, t)) ts);
return (StructV fx vs)
od
` (WF_REL_TAC `measure (uvm_type_size o FST)` >> rw[] >> metis_tac[
uvmTypesTheory.uvm_type_size_mem,
arithmeticTheory.ADD_COMM,
arithmeticTheory.LESS_IMP_LESS_ADD])
val _ = type_abbrev("register", ``:ssavar # block_id``)
val _ = Datatype`
location =
......@@ -114,16 +78,16 @@ val _ = Datatype`
arguments are defined as records.
*)
action =
| LoadAction location memory_order
| StoreAction location memory_order (value symbolic)
| CmpXchgAction cmp_xchg_action_args
| AtomicRMWAction atomic_rmw_action_args
| FenceAction memory_order
| NewAction uvm_type (num option symbolic)
| AllocaAction uvm_type stack_id frame_id (num option symbolic)
| FreeAction uvm_type addr
| GlobalInitAction global_name uvm_type
| NewThreadAction func_name (value symbolic list) ;
| DoLoad location memory_order
| DoStore location memory_order (value symbolic)
| DoCmpXchg cmp_xchg_action_args
| DoAtomicRMW atomic_rmw_action_args
| DoFence memory_order
| DoNew uvm_type (num option symbolic)
| DoAlloca uvm_type stack_id (num option symbolic)
| DoFree uvm_type addr
| DoGlobalInit global_name uvm_type
| DoNewThread func_name (value symbolic list) ;
message = Message thread_id action_id action ;
......@@ -217,6 +181,7 @@ val sequence_option_def = Define`
`
val sequence_oe_def = Define`
sequence_oe : α option or_error list -> α list option or_error =
lift_left sequence_option o sequence_left
`
......@@ -234,34 +199,34 @@ val iaddrs_of_message_def = Define`
let set_of = lift_oe (λx. {x}) in
let empty = return (SOME ) in
case action of
|