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

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

Clean up error types and assert/expect syntax

- Replace "expect" with infix "or_fail"
- Reduce uvm_error to 3 error types, with a generic parameter for
  undefined behavior error messages
- Use option instead of InvalidStep error type in scheduler
parent 296c77dc
......@@ -3,7 +3,7 @@ struct
open HolKernel Parse Term boolLib bossLib
open listTheory llistTheory optionTheory pred_setTheory finite_mapTheory sptreeTheory
open listSyntax stringSyntax sptreeSyntax
open monadsTheory uvmTypesTheory uvmMemoryTheory
open monadsTheory uvmTypesTheory uvmErrorsTheory uvmMemoryTheory
val lhdtl_lunfold = prove(
``LHD (LUNFOLD f x) = OPTION_MAP SND (f x)
......@@ -15,7 +15,7 @@ struct
sptreeSyntax.temp_add_sptree_printer();
computeLib.add_funs[
SING, CHOICE_SING, EMPTY_DEF, IN_APP, INSERT_applied,
OPTION_MAP_DEF, OPTION_MAP2_DEF, OPTION_BIND_def, OPTION_CHOICE_def,
OPTION_MAP_DEF, OPTION_MAP2_DEF, OPTION_BIND_def, OPTION_CHOICE_def, OPTION_GUARD_def,
lhdtl_lunfold, prefix_type_cases,
bind_left_monad_left_id, bind_left_monad_right_id, bind_left_monad_assoc]
)
......@@ -23,7 +23,7 @@ struct
fun parens q = [QUOTE "("] @ q @ [QUOTE ")"]
fun to_env (bundle : term) : term =
EVAL ``^bundle empty_env`` |> concl |> rhs
EVAL ``lift_value_error (^bundle empty_env)`` |> concl |> rhs
fun start_at (func_name : string) (args : term frag list) (env : term) : term =
Term(`
......
......@@ -35,15 +35,16 @@ struct
(kty : hol_type)
(vty : hol_type)
(key : term) : term =
infer_comb("expect", [
infer_comb("option_CASE", [
infer_comb("FLOOKUP", [
infer_comb("environment_" ^ field_name, [t_env], mk_fmap_ty(kty, vty)),
key
], mk_type("option", [vty])),
infer_comb("InvalidIR",
(* TODO: Include key in error message *)
[fromMLstring (field_name ^ " lookup failed")],
ty_err)
infer_comb("INR", [infer_comb("Impossible",
[fromMLstring (
"lookup " ^ term_to_string key ^ " in " ^ field_name ^ " failed")],
ty_err)], or_error vty),
mk_const("INL", vty --> or_error vty)
], or_error vty)
fun get_env_type (name : string) : term =
......
......@@ -76,7 +76,7 @@ struct
end
(* Reads an SSA variable, replacing global variables with constants using the
given context. Returns a term of type ``:ssa_or_const or_error``.
given context. Returns a term of type ``:ssa_or_const + value_error``.
*)
fun ssa_var _ (Local, v) = mk_return(mk_comb(t_Var, mk_ssa v))
| ssa_var (env : env_context) (Global, v) = #get_global env v
......@@ -143,7 +143,7 @@ struct
| _ => raise ParseError(inst ^ " lhs contains non-SSA-var")
(* Parses a list of tokens into a Mu IR instruction. Returns a term of type
``:instruction or_error``.
``:instruction + value_error``.
*)
fun parse_inst (env : env_context) (tokens : uir_token list) : term =
let
......@@ -357,7 +357,7 @@ struct
end
(* Parses a list of tokens into a Mu IR terminating instruction. Returns a
term of type ``:ssavar terminst or_error``.
term of type ``:ssavar terminst + value_error``.
*)
fun parse_terminst (env : env_context) (tokens : uir_token list) : term =
let
......
......@@ -21,7 +21,7 @@ struct
get_type = fn _ => ``ARB``,
get_funcsig = fn name =>
case name of
"sig" => ``OK (<| arg_types := []; return_types := [] |>): funcsig or_error``
"sig" => ``OK (<| arg_types := []; return_types := [] |>): funcsig + value_error``
| _ => ``ARB``,
get_global = fn _ => ``ARB``
}
......@@ -36,7 +36,7 @@ struct
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_err = ``:value_error``
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)
......
......@@ -12,7 +12,7 @@ struct
open TypeParser
fun invalid_ir (m : string) = infer_comb("INR",
[infer_comb("InvalidIR", [fromMLstring m], ty_err)],
[infer_comb("Impossible", [fromMLstring m], ty_err)],
or_error (ty_list ty_val))
fun parse_value [Int n] =
......
open HolKernel Parse boolLib bossLib
open uvmTypesTheory
open stringTheory
open monadsTheory
open monadsLib
......@@ -8,74 +7,70 @@ open syntaxSugarTheory
val _ = new_theory "uvmErrors"
(* The "error" type is used with the sum type monad (in monadsTheory) to create
a short-circuiting error monad used throughout the formalization.
When undefined or impossible behavior occurs, the remainder of the execution
is undefined, and the error monad short-circuits the execution and reports an
error message for debugging purposes.
*)
val _ = Datatype`
gen_uvm_error =
| TypeMismatch string uvm_type uvm_type
| NotInt string uvm_type
| NotRef uvm_type
| NotIRef uvm_type
| NotCallable uvm_type
| ReadOutOfBounds uvm_type num
| WriteOutOfBounds uvm_type num
| UnallocatedMemory 'addr
| NullReference
| DivideByZero
| UndefinedBehavior string (* for all other kinds of undefined behavior *)
| NoSuchFunction 'func_name
| InvalidIR string
| InvalidState string
| InvalidStep
error =
(* Undefined behavior has occurred, and the rest of the execution is unknown.
The generic parameter allows more information about the undefined behavior
to be included in the error object, for debugging purposes. *)
| UndefBehavior 'undefined_type
(* For code paths that should never be reachable by well-formed programs.
Should be provable that no well-formed program can produce this error. *)
| Impossible string
(* For code paths that are not yet implemented. Should be removed in the final
version of the formalization. *)
| NotImplemented string
`
val _ = define_sum("errorM",
"OK", ``:α``,
"Fail", ``:(β, γ) gen_uvm_error``)
val _ = overload_on("OK", ``INL : α -> α + ε error``)
val _ = overload_on("Fail", ``INR : ε error -> α + ε error``)
val _ = overload_on("✔", ``OK``)
val _ = overload_on("✘", ``Fail``)
val assert_def = Define`
assert (cond : bool) (err : (α, β) gen_uvm_error) : (one, α, β) errorM =
if cond then OK () else Fail err
`
(* The infix "or_fail" operator throws an error if the option on its left side
is NONE. It can be combined with "assert", which converts a boolean to an
option.
*)
val assert_OK = Q.store_thm("assert_OK[simp]",
`assert T e = OK ()`,
rw[assert_def])
(* tight_equality (450) < 455 < CONS (490) *)
val _ = set_fixity "or_fail" (Infix (NONASSOC, 455))
val assert_Fail = Q.store_thm("assert_Fail[simp]",
`assert F e = Fail e`,
rw[assert_def])
val _ = overload_on("or_fail", ``λx e. option_CASE x (Fail e) OK``)
val _ = overload_on("assert", ``OPTION_GUARD``)
val assert_OK_proves = Q.store_thm("assert_OK_proves[simp]",
`(assert P e = OK ()) = P`,
rw[assert_def])
val assert_type_eq_def = Define`
assert_type_eq (t1 : uvm_type) (t2 : uvm_type) (msg : string) =
assert (t1 = t2) (TypeMismatch msg t1 t2)
`
(* The UndefBehavior error message can be mapped over, allowing different kinds
of errors to be merged.
*)
val expect_def = Define`
(* expect : α option -> uvm_error -> α or_error *)
(expect NONE err = Fail err)
(expect (SOME x) _ = OK x)
val lift_err_msg_def = Define`
lift_err_msg (f : 'm1 -> 'm2) (Fail (UndefBehavior msg) : α + 'm1 error)
: α + 'm2 error =
Fail (UndefBehavior (f msg))
lift_err_msg _ (Fail (Impossible msg)) = Fail (Impossible msg)
lift_err_msg _ (Fail (NotImplemented msg)) = Fail (NotImplemented msg)
lift_err_msg _ (OK x) = OK x
`
val expect_OK = Q.store_thm("expect_OK[simp]",
`expect (SOME y) e = OK y`,
simp[expect_def]);
(* Because assert and or_fail are extremely common, theorems about their basic
functionality are included in the default simpset.
*)
val expect_Fail = Q.store_thm("expect_Fail[simp]",
`expect NONE e = Fail e`,
simp[expect_def]);
val or_fail_OK_proves = Q.store_thm("or_fail_OK_proves[simp]",
`opt e. (opt or_fail e = OK x) = (opt = SOME x)`,
Cases >> rw[])
val expect_OK_proves = Q.store_thm("expect_OK_proves[simp]",
`(expect opt e = OK x) = (opt = SOME x)`,
Cases_on `opt` >> rw[expect_def])
val assert_OK_proves = store_thm("assert_OK_proves[simp]",
``P e. (assert P or_fail e = OK ()) = P``,
Cases >> rw[])
val _ = export_theory()
......@@ -79,7 +79,7 @@ val _ = Datatype`
`
val exec_bin_op_def = Define`
exec_bin_op ADD : value -> value -> value or_error = int_binop $+
exec_bin_op ADD : value -> value -> value + value_error = int_binop $+
exec_bin_op SUB = int_binop $-
exec_bin_op MUL = int_binop $*
exec_bin_op SDIV = K (K (Fail (NotImplemented "SDIV")))
......@@ -207,7 +207,7 @@ val _ = Datatype`
`
val get_callee_def = Define`
get_callee (callee : ssa_or_const) : (ssavar + func_name) or_error =
get_callee (callee : ssa_or_const) : (ssavar + func_name) + value_error =
case callee of
| Var v => return (INL v)
| Const _ c _ => liftM (INR o SND) (get_funcref_data c)
......@@ -768,7 +768,7 @@ val empty_env_def = Define`
for example, if the bundle refers to a name that is not defined in the input
environment, or if the input environment causes a type mismatch.
*)
val _ = type_abbrev("bundle", ``:environment -> environment or_error``)
val _ = type_abbrev("bundle", ``:environment -> environment + value_error``)
(* Utility function for BundleParser *)
val generate_function_def = Define`
......
......@@ -22,6 +22,19 @@ val _ = new_theory "uvmInstructionSemantics"
val _ = monadsyntax.add_monadsyntax()
val _ = reveal "C"
val _ = Datatype`
uvm_error_message =
| ValErr string value_error_message
| MemErr addr mem_error_message
| NoSuchFunction func_name
| FrameNotReady frame_id
| UncaughtException (value + addr mem_error)
`
val _ = type_abbrev("or_error", ``:α + uvm_error_message error``)
val _ = overload_on("lift_value_error", ``lift_err_msg (UNCURRY ValErr)``)
val _ = overload_on("lift_mem_error", ``lift_err_msg (UNCURRY MemErr)``)
(* reg_reader is a reader monad over a memory region. It provides syntax sugar
for operations on a thread's registers. *)
val _ = type_abbrev("reg_reader", ``:(num -> value or_error) -> α or_error``)
......@@ -44,7 +57,7 @@ val getc_def = Define`
val run_reg_reader_def = Define`
run_reg_reader (r : α reg_reader) (regs : mem_region) : α or_error =
r (λn. FST <$> expect (lookup n regs) (InvalidState "undefined register"))
r (λn. FST <$> (lookup n regs or_fail Impossible "undefined register"))
`
val _ = Datatype`
......@@ -127,7 +140,7 @@ val eval_expr_def = Define`
| SUB => return $-
| MUL => return $*
| _ => K (Fail (NotImplemented "most binops"));
return <$> K (int_binop op v1 v2)
return <$> K (lift_value_error (int_binop op v1 v2))
od
eval_expr ssa (CmpOp op _ v1 v2) = (
if (op = EQ op = NE) then do
......@@ -137,7 +150,7 @@ val eval_expr_def = Define`
od else do
v1 <- HD (getc ssa v1);
v2 <- HD (getc ssa v2);
c <- K (compare_unsigned_values v1 v2);
c <- K (lift_value_error (compare_unsigned v1 v2));
b <- case op of
| UGE => return (c = Equal c = Greater)
| UGT => return (c = Greater)
......@@ -147,16 +160,18 @@ val eval_expr_def = Define`
return [IntV 1 (if b then 1 else 0)]
od)
eval_expr ssa (ConvOp REFCAST ty1 ty2 v) =
(case ty1, ty2 of
(let type_mismatch ty1 ty2 =
K (Fail (UndefBehavior (ValErr "REFCAST" (NotType ty1 ty2)))) in
case ty1, ty2 of
| Ref (Type Void), Ref (Type t) => (
HD (getc ssa v) >>= λv. case v of
| RefV _ a => return [RefV t a]
| _ => K (Fail (TypeMismatch "REFCAST" ty1 (type_of_value v))))
| _ => type_mismatch ty1 (type_of v))
| Ref (Type t), Ref (Type Void) => (
HD (getc ssa v) >>= λv. case v of
| RefV _ a => return [RefV t a]
| _ => K (Fail (TypeMismatch "REFCAST" ty1 (type_of_value v))))
| _ => K (Fail (TypeMismatch "REFCAST" ty1 ty2)))
| _ => type_mismatch ty1 (type_of v))
| _ => type_mismatch ty1 ty2)
eval_expr _ (ConvOp _ _ _ _) =
K (Fail (NotImplemented "non-REFCAST conversions"))
(* TODO: Select *)
......@@ -165,23 +180,27 @@ val eval_expr_def = Define`
eval_expr ssa (ExtractValue ty off v) =
(let members = member_types (SOME off) ty in
let sizeof = LENGTH o component_types NONE in do
K (assert (off < LENGTH members) (ReadOutOfBounds ty off));
K (assert (off < LENGTH members)
or_fail UndefBehavior (ValErr "EXTRACTVALUE" (OutOfBounds ty off)));
vs <- sequence (getc ssa v);
let out = TAKE (sizeof (EL off members))
(DROP (SUM (MAP sizeof (TAKE off members))) vs) in
K (assert (¬NULL out) (ReadOutOfBounds ty off)) *>
K (assert (¬NULL out)
or_fail UndefBehavior (ValErr "EXTRACTVALUE" (OutOfBounds ty off))) *>
return out
od)
eval_expr ssa (InsertValue ty off base el) =
(let members = member_types (SOME off) ty in
let sizeof = LENGTH o component_types NONE in do
K (assert (off < LENGTH members) (WriteOutOfBounds ty off));
K (assert (off < LENGTH members)
or_fail UndefBehavior (ValErr "INSERTVALUE" (OutOfBounds ty off)));
vs <- sequence (getc ssa base);
vs' <- sequence (getc ssa el);
let out =
(TAKE (SUM (MAP sizeof (TAKE off members))) vs) ++ vs' ++
(DROP (SUM (MAP sizeof (TAKE (SUC off) members))) vs) in
K (assert (LENGTH vs = LENGTH out) (WriteOutOfBounds ty off)) *>
K (assert (LENGTH vs = LENGTH out)
or_fail UndefBehavior (ValErr "INSERTVALUE" (OutOfBounds ty off))) *>
return out
od)(*
∧ eval_expr get (ExtractElement ty ity v i) = do
......@@ -203,32 +222,33 @@ val eval_expr_def = Define`
K (Fail (NotImplemented "SHUFFLEVECTOR"))
eval_expr ssa (GetIRef _ ref) = do
rv <- HD (getc ssa ref);
irv <- K (get_iref rv);
irv <- K (lift_value_error (get_iref rv));
return [irv]
od
eval_expr ssa (GetFieldIRef _ _ n ref) = do
rv <- HD (getc ssa ref);
rv' <- K (get_field_iref rv n);
rv' <- K (lift_value_error (get_field_iref rv n));
return [rv']
od
eval_expr ssa (GetElementIRef _ _ _ ref idx) = do
rv <- HD (getc ssa ref);
iv <- HD (getc ssa idx);
rv' <- K (get_element_iref rv iv);
rv' <- K (lift_value_error (get_element_iref rv iv));
return [rv']
od
eval_expr ssa (ShiftIRef _ _ _ ref off) = do
eval_expr ssa (ShiftIRef _ _ _ ref ofv) = do
rv <- HD (getc ssa ref);
iv <- HD (getc ssa off);
rv' <- K (shift_iref rv iv);
iv <- HD (getc ssa ofv);
rv' <- K (lift_value_error (shift_iref rv iv));
return [rv']
od
eval_expr ssa (GetVarPartIRef _ _ ref) = do
rv <- HD (getc ssa ref);
ia <- K (get_iref_addr rv);
case ia.ty of
| Hybrid fts _ => return <$> K (get_field_iref rv (LENGTH fts))
| _ => K (Fail (InvalidIR "GETVARPARTIREF of non-hybrid"))
ia <- K (lift_value_error (get_iref_addr rv));
K (case ia.ty of
| Hybrid fts _ => return <$>
lift_value_error (get_field_iref rv (LENGTH fts))
| ty => Fail (UndefBehavior (ValErr "GETVARPARTIREF" (NotHybrid ty))))
od
`
......@@ -237,7 +257,7 @@ val compile_inst_def = Define`
compile_inst (ssa : ssa_map) (Assign vs e) : opn list =
[Nm (CURRY ZIP (vs >>= MAP FST o ssa) <$> eval_expr ssa e)]
compile_inst (ssa : ssa_map) (Load dst _ _ src ord) : opn list =
(let lds = MAP2 (λs d. Ld (s >>= K o get_iref_addr) (FST d))
(let lds = MAP2 (λs d. Ld (s >>= K o lift_value_error o get_iref_addr) (FST d))
(get ssa src) (ssa dst) in
case ord of
| NOT_ATOMIC => lds
......@@ -245,17 +265,19 @@ val compile_inst_def = Define`
| CONSUME => do ld <- lds; [ld; Rec] od
| ACQUIRE => do ld <- lds; [ld; Rec] od
| SEQ_CST => do ld <- lds; [Com; Rec; ld; Rec] od
| _ => [Nm (K (Fail (InvalidIR "unsupported memory order for LOAD")))])
| _ => [Nm (K (Fail (Impossible "unsupported memory order for LOAD")))])
compile_inst ssa (Store src _ _ dst ord) =
(let sts = MAP2
(λd s. St ($, <$> (d >>= K o get_iref_addr) <*> s))
(get ssa dst) (getc ssa src) in
(let sts = MAP2 (λd s. St do
d <- d; s <- s;
ia <- K (lift_value_error (get_iref_addr d));
return (ia, s)
od) (get ssa dst) (getc ssa src) in
case ord of
| NOT_ATOMIC => sts
| RELAXED => sts
| RELEASE => do st <- sts; [Com; st] od
| SEQ_CST => do st <- sts; [Com; st] od
| _ => [St (K (Fail (InvalidIR "unsupported memory order for STORE")))])
| _ => [St (K (Fail (Impossible "unsupported memory order for STORE")))])
compile_inst _ (CmpXchg _ _ _ _ _ _ _ _ _ _) =
[Nm (K (Fail (NotImplemented "CMPXCHG")))]
compile_inst _ (AtomicRMW _ _ _ _ _ _ _) =
......@@ -267,11 +289,17 @@ val compile_inst_def = Define`
compile_inst ssa (Alloca dst ty) =
[Cmd (return (DoStackAlloc ty NONE (FST (HD (ssa dst)))))]
compile_inst ssa (NewHybrid dst ty _ len) =
[Cmd ((λn. DoHeapAlloc ty (SOME n) (FST (HD (ssa dst))))
<$> (HD (getc ssa len) >>= K o get_int_as_num "NEWHYBRID"))]
[Cmd (do
lenv <- HD (getc ssa len);
n <- K (lift_value_error (get_int_as_num "NEWHYBRID" lenv));
return (DoHeapAlloc ty (SOME n) (FST (HD (ssa dst))))
od)]
compile_inst ssa (AllocaHybrid dst ty _ len) =
[Cmd ((λn. DoStackAlloc ty (SOME n) (FST (HD (ssa dst))))
<$> (HD (getc ssa len) >>= K o get_int_as_num "ALLOCAHYBRID"))]
[Cmd (do
lenv <- HD (getc ssa len);
n <- K (lift_value_error (get_int_as_num "ALLOCAHYBRID" lenv));
return (DoStackAlloc ty (SOME n) (FST (HD (ssa dst))))
od)]
compile_inst ssa (NewThread dst stk tloc nsc) =
[(* TODO: this*)]
`
......@@ -296,7 +324,7 @@ val compile_terminst_def = Define`
case cdata.name of
| INL n => do
ref <- HD (get ssa n);
(sig, name) <- K (get_funcref_data ref);
(sig, name) <- K (lift_value_error (get_funcref_data ref));
(* TODO: Assert sig = cdata.signature *)
return name
od
......@@ -315,7 +343,7 @@ val compile_terminst_def = Define`
case cdata.name of
| INL n => do
ref <- HD (get ssa n);
(sig, name) <- K (get_funcref_data ref);
(sig, name) <- K (lift_value_error (get_funcref_data ref));
(* TODO: Assert sig = cdata.signature *)
return name
od
......@@ -327,10 +355,13 @@ val compile_terminst_def = Define`
compile_terminst lbl ssa (Branch1 (b, vs)) =
[Cmd (DoJump <$> return (lbl b) <*> sequence (vs >>= getc ssa))]
compile_terminst lbl ssa (Branch2 p d1 d2) =
[Cmd (HD (getc ssa p) >>= K o get_int1_as_bool >>= λis1.
let compile_dest = lbl ## C LIST_BIND (getc ssa) in
let (b, vs) = if is1 then compile_dest d1 else compile_dest d2 in
DoJump <$> return b <*> sequence vs)]
[Cmd (do
bv <- HD (getc ssa p);
is1 <- K (lift_value_error (get_int1_as_bool bv));
let compile_dest = lbl ## (λx. x >>= getc ssa) in
let (b, vs) = if is1 then compile_dest d1 else compile_dest d2 in
DoJump <$> return b <*> sequence vs
od)]
compile_terminst lbl ssa (Switch _ p default cases) =
[Cmd (HD (getc ssa p) >>= λpv.
let (b, vs) = (lbl ## I) (option_CASE (ALOOKUP cases pv) default I) in
......
......@@ -25,9 +25,11 @@ val _ = reveal "C"
val _ = define_num_newtype("thread_id", "ThreadID", "t")
val _ = define_num_newtype("frame_id", "FrameID", "f")
val _ = define_num_newtype("stack_id", "StackID", "s")
val _ = define_num_newtype("action_id", "ActionID", "a")
(*val _ = define_num_newtype("action_id", "ActionID", "a")*)
val _ = Datatype `ssavar = SSA string`
val _ = overload_on("%", ``SSA``)
val _ = Datatype `func_name = Func string`
val _ = Datatype `func_version = FuncVersion func_name num`
val _ = Datatype `alloc = Global | Heap | Stack stack_id frame_id`
......@@ -35,10 +37,6 @@ val _ = Datatype `alloc = Global | Heap | Stack stack_id frame_id`
val _ = type_abbrev("addr", ``:alloc # num``)
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 _ = overload_on("%", ``SSA``)
val alloc_lt_def = Define`
(alloc_lt Global Heap T)
......@@ -55,6 +53,16 @@ val addr_lt_def = Define`
a1 = a2 n1 < n2 alloc_lt a1 a2
`
val _ = Datatype`
mem_error_message =
| Unallocated
| BadOffset (uvm_type list) num
| LoadWrongType (uvm_type list) uvm_type
| StoreWrongType (uvm_type list) value
`
val _ = type_abbrev("mem_error", ``:('addr # mem_error_message) error``)
(* A memory cell is a triple representing a typed location holding a single
scalar value. The elements of the triple are:
......@@ -94,7 +102,7 @@ val new_mem_cells_def = Define`
(ty : uvm_type)
(next_loc : α -> num # α)
(loc_src : α)
: ((num, mem_cell) alist # α) or_error =
: ((num, mem_cell) alist # α) + ε error =
let (ctys, loc_src') = mem_cell_types sz ty next_loc loc_src in
C $, loc_src' <$>
mapM (λ(n, t). $, n o C $, t <$> zero_value (HD (FST t))) ctys
......@@ -106,28 +114,19 @@ val region_alloc_def = Define`
(ty : uvm_type)
(next_loc : α -> num # α)
(loc_src : α)
: (num # α # mem_region) or_error = do
: (num # α # mem_region) + ε error = do
(cells, loc_src) <- new_mem_cells sz ty next_loc loc_src;
assert (¬EXISTS (domain region o FST) cells)
(InvalidState "double allocation");
or_fail Impossible "double allocation";
OK (FST (HD cells), loc_src, union region (fromAList cells))
od
`
val num_str_def = TotalDefn.tDefine "num_str" `
num_str 0 = "0" num_str 1 = "1" num_str 2 = "2" num_str 3 = "3"
num_str 4 = "4" num_str 5 = "5" num_str 6 = "6" num_str 7 = "7"
num_str 8 = "8" num_str 9 = "9"
num_str n = STRCAT (num_str (n DIV 10)) (num_str (n MOD 10))
` (WF_REL_TAC `$<` >> rw[] >> `v MOD 10 < 10` by simp[] >> simp[])
val mem_region_set_value_def = Define`
mem_region_set_value (name : string) (n : num) (v : value) (r : mem_region)
: mem_region or_error =
let loc = name ++ " location #" ++ num_str n in
let ty = type_of_value v in do
(_, tys, ns) <- expect (lookup n r) (InvalidState ("unallocated: " ++ loc));
assert (ty = HD tys) (TypeMismatch loc ty (HD tys));
mem_region_set_value (n : num) (v : value) (r : mem_region)
: mem_region + num mem_error = do
(_, tys, ns) <- lookup n r or_fail UndefBehavior (n, Unallocated);
assert (type_of v = HD tys) or_fail UndefBehavior (n, StoreWrongType tys v);
return (insert n (v, tys, ns) r)
od
`
......@@ -168,7 +167,7 @@ val mem_cell_ok_def = Define`
(* At least enough offsets for the largest type *)
LENGTH (component_types (SOME 0) (LAST tys)) SUC (LENGTH offs)
(* Value should be of the smallest (scalar) type *)
type_of_value v = HD tys
type_of v = HD tys
`
val mem_region_ok_def = Define`
......@@ -200,7 +199,7 @@ val new_address_space_def = Define`
`