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

Commit 7d497e28 authored by Adam Nelson's avatar Adam Nelson
Browse files

Add undef values and make error handling use them

parent 53777e5d
......@@ -23,7 +23,7 @@ struct
fun parens q = [QUOTE "("] @ q @ [QUOTE ")"]
fun to_env (bundle : term) : term =
EVAL ``lift_value_error (^bundle empty_env)`` |> concl |> rhs
EVAL ``lift_type_error (^bundle empty_env)`` |> concl |> rhs
fun start_at (func_name : string) (args : term frag list) (env : term) : term =
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 + value_error``.
given context. Returns a term of type ``:ssa_or_const + type_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 + value_error``.
``:instruction + type_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 + value_error``.
term of type ``:ssavar terminst + type_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 + value_error``
"sig" => ``OK (<| arg_types := []; return_types := [] |>): funcsig + type_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 = ``:value_error``
val ty_err = ``:type_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)
......
......@@ -10,7 +10,9 @@ val _ = set_fixity "≺" (Infix(NONASSOC, 450))
val _ = set_fixity "≼" (Infix(NONASSOC, 450))
val _ = overload_on("∁", ``COMPL``)
val _ = Unicode.unicode_version{tmnm="CONS", u="∷"}
(* Unicode ∷ disabled because it prevented [] list syntax from working... *)
(* val _ = Unicode.unicode_version{tmnm="CONS", u="∷"} *)
val _ = TeX_notation {hol="%", TeX=("\\%", 1)}
(* For some reason HOL doesn't define this symbol by default... *)
......
......@@ -17,5 +17,11 @@ val _ = state1 |> run_finite_schedule `[ExecInst; ExecInst]`
val _ = state1 |> run_schedule `cycle [ExecInst]`
|> expect_result `OK (NOR [IntV 8 5])`
(* Test with undefined input *)
val state_undef = bundle1 |> to_env |> start_at "add_two" `[UndefV (Int 8)]`
val _ = state_undef |> run_finite_schedule `[ExecInst; ExecInst]`
|> expect_result `OK (NOR [UndefV (Int 8)])`
val _ = export_theory()
......@@ -79,7 +79,7 @@ val _ = Datatype`
`
val exec_bin_op_def = Define`
exec_bin_op ADD : value -> value -> value + value_error = int_binop $+
exec_bin_op ADD : value -> value -> value + type_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,10 +207,10 @@ val _ = Datatype`
`
val get_callee_def = Define`
get_callee (callee : ssa_or_const) : (ssavar + func_name) + value_error =
get_callee (callee : ssa_or_const) : (ssavar + func_name) + type_error =
case callee of
| Var v => return (INL v)
| Const _ c _ => liftM (INR o SND) (get_funcref_data c)
| Const _ c _ => INR o SND o THE <$> get_funcref_data c
`
(* Type for expressions, instructions which do not contain a reference to their
......@@ -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 + value_error``)
val _ = type_abbrev("bundle", ``:environment -> environment + type_error``)
(* Utility function for BundleParser *)
val generate_function_def = Define`
......
......@@ -16,6 +16,7 @@ open optionTheory
open pairTheory
open pred_setTheory
open sptreeTheory
open ternaryComparisonsTheory
open lcsymtacs
val _ = new_theory "uvmInstructionSemantics"
......@@ -24,16 +25,20 @@ 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)
| TypeMismatch string type_mismatch
| MemoryError addr mem_error_message
| OutOfBounds string uvm_type num
| UndefReference uvm_type
| UndefHybridSize uvm_type
| UndefBranch
| 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)``)
val _ = overload_on("lift_type_error", ``lift_err_msg (UNCURRY TypeMismatch)``)
val _ = overload_on("lift_mem_error", ``lift_err_msg (UNCURRY MemoryError)``)
(* reg_reader is a reader monad over a memory region. It provides syntax sugar
for operations on a thread's registers. *)
......@@ -140,7 +145,7 @@ val eval_expr_def = Define`
| SUB => return $-
| MUL => return $*
| _ => K (Fail (NotImplemented "most binops"));
return <$> K (lift_value_error (int_binop op v1 v2))
return <$> K (lift_type_error (int_binop op v1 v2))
od
eval_expr ssa (CmpOp op _ v1 v2) = (
if (op = EQ op = NE) then do
......@@ -150,18 +155,23 @@ val eval_expr_def = Define`
od else do
v1 <- HD (getc ssa v1);
v2 <- HD (getc ssa v2);
c <- K (lift_value_error (compare_unsigned v1 v2));
b <- case op of
| UGE => return (c = Equal c = Greater)
| UGT => return (c = Greater)
| ULE => return (c = Equal c = Less)
| ULT => return (c = Less)
| _ => K (Fail (NotImplemented "most cmpops"));
return [IntV 1 (if b then 1 else 0)]
co <- K (lift_type_error (compare_unsigned v1 v2));
case co of
| SOME c => do
b <- case op of
| UGE => return (c = EQUAL c = GREATER)
| UGT => return (c = GREATER)
| ULE => return (c = EQUAL c = LESS)
| ULT => return (c = LESS)
| _ => K (Fail (NotImplemented "most cmpops"));
return [IntV 1 (if b then 1 else 0)]
od
| NONE => return [UndefV (Int 1)]
od)
eval_expr ssa (ConvOp REFCAST ty1 ty2 v) =
(* TODO: handle undefined values here *)
(let type_mismatch ty1 ty2 =
K (Fail (UndefBehavior (ValErr "REFCAST" (NotType ty1 ty2)))) in
K (Fail (UndefBehavior (TypeMismatch "REFCAST" (NotType ty1 ty2)))) in
case ty1, ty2 of
| Ref (Type Void), Ref (Type t) => (
HD (getc ssa v) >>= λv. case v of
......@@ -181,26 +191,26 @@ val eval_expr_def = Define`
(let members = member_types (SOME off) ty;
sizeof = LENGTH o component_types NONE in do
K (assert (off < LENGTH members)
or_fail UndefBehavior (ValErr "EXTRACTVALUE" (OutOfBounds ty off)));
or_fail UndefBehavior (OutOfBounds "EXTRACTVALUE" 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)
or_fail UndefBehavior (ValErr "EXTRACTVALUE" (OutOfBounds ty off))) *>
or_fail UndefBehavior (OutOfBounds "EXTRACTVALUE" ty off)) *>
return out
od)
eval_expr ssa (InsertValue ty off base el) =
(let members = member_types (SOME off) ty;
sizeof = LENGTH o component_types NONE in do
K (assert (off < LENGTH members)
or_fail UndefBehavior (ValErr "INSERTVALUE" (OutOfBounds ty off)));
or_fail UndefBehavior (OutOfBounds "INSERTVALUE" 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)
or_fail UndefBehavior (ValErr "INSERTVALUE" (OutOfBounds ty off))) *>
or_fail UndefBehavior (OutOfBounds "INSERTVALUE" ty off)) *>
return out
od)(*
∧ eval_expr get (ExtractElement ty ity v i) = do
......@@ -222,33 +232,35 @@ val eval_expr_def = Define`
K (Fail (NotImplemented "SHUFFLEVECTOR"))
eval_expr ssa (GetIRef _ ref) = do
rv <- HD (getc ssa ref);
irv <- K (lift_value_error (get_iref rv));
irv <- K (lift_type_error (get_iref rv));
return [irv]
od
eval_expr ssa (GetFieldIRef _ _ n ref) = do
rv <- HD (getc ssa ref);
rv' <- K (lift_value_error (get_field_iref rv n));
rv' <- K (lift_type_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 (lift_value_error (get_element_iref rv iv));
rv' <- K (lift_type_error (get_element_iref rv iv));
return [rv']
od
eval_expr ssa (ShiftIRef _ _ _ ref ofv) = do
rv <- HD (getc ssa ref);
iv <- HD (getc ssa ofv);
rv' <- K (lift_value_error (shift_iref rv iv));
rv' <- K (lift_type_error (shift_iref rv iv));
return [rv']
od
eval_expr ssa (GetVarPartIRef _ _ ref) = do
rv <- HD (getc ssa ref);
ia <- K (lift_value_error (get_iref_addr rv));
ao <- K (lift_type_error (get_iref_addr rv));
ia <- K (ao or_fail UndefBehavior (UndefReference (type_of 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))))
lift_type_error (get_field_iref rv (LENGTH fts))
| ty =>
Fail (UndefBehavior (TypeMismatch "GETVARPARTIREF" (NotHybrid ty))))
od
`
......@@ -257,8 +269,11 @@ 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 lift_value_error o get_iref_addr) (FST d))
(get ssa src) (ssa dst) in
(let lds = MAP2 (λs d. Ld (do
s <- s;
ia_opt <- K (lift_type_error (get_iref_addr s));
K (ia_opt or_fail UndefBehavior (UndefReference (type_of s)))
od) (FST d)) (get ssa src) (ssa dst) in
case ord of
| NOT_ATOMIC => lds
| RELAXED => lds
......@@ -269,7 +284,8 @@ val compile_inst_def = Define`
compile_inst ssa (Store src _ _ dst ord) =
(let sts = MAP2 (λd s. St do
d <- d; s <- s;
ia <- K (lift_value_error (get_iref_addr d));
ia_opt <- K (lift_type_error (get_iref_addr d));
ia <- K (ia_opt or_fail UndefBehavior (UndefReference (type_of d)));
return (ia, s)
od) (get ssa dst) (getc ssa src) in
case ord of
......@@ -291,13 +307,15 @@ val compile_inst_def = Define`
compile_inst ssa (NewHybrid dst ty _ len) =
[Cmd (do
lenv <- HD (getc ssa len);
n <- K (lift_value_error (get_int_as_num "NEWHYBRID" lenv));
n_opt <- K (lift_type_error (get_int_as_num "NEWHYBRID" lenv));
n <- K (n_opt or_fail UndefBehavior (UndefHybridSize ty));
return (DoHeapAlloc ty (SOME n) (FST (HD (ssa dst))))
od)]
compile_inst ssa (AllocaHybrid dst ty _ len) =
[Cmd (do
lenv <- HD (getc ssa len);
n <- K (lift_value_error (get_int_as_num "ALLOCAHYBRID" lenv));
n_opt <- K (lift_type_error (get_int_as_num "ALLOCAHYBRID" lenv));
n <- K (n_opt or_fail UndefBehavior (UndefHybridSize ty));
return (DoStackAlloc ty (SOME n) (FST (HD (ssa dst))))
od)]
compile_inst ssa (NewThread dst stk tloc nsc) =
......@@ -325,7 +343,9 @@ val compile_terminst_def = Define`
case cdata.name of
| INL n => do
ref <- HD (get ssa n);
(sig, name) <- K (lift_value_error (get_funcref_data ref));
fn_opt <- K (lift_type_error (get_funcref_data ref));
(sig, name) <-
K (fn_opt or_fail UndefBehavior (UndefReference (type_of ref)));
(* TODO: Assert sig = cdata.signature *)
return name
od
......@@ -345,7 +365,9 @@ val compile_terminst_def = Define`
case cdata.name of
| INL n => do
ref <- HD (get ssa n);
(sig, name) <- K (lift_value_error (get_funcref_data ref));
fn_opt <- K (lift_type_error (get_funcref_data ref));
(sig, name) <-
K (fn_opt or_fail UndefBehavior (UndefReference (type_of ref)));
(* TODO: Assert sig = cdata.signature *)
return name
od
......@@ -359,7 +381,8 @@ val compile_terminst_def = Define`
compile_terminst lbl ssa (Branch2 p d1 d2) =
[Cmd (do
bv <- HD (getc ssa p);
is1 <- K (lift_value_error (get_int1_as_bool bv));
is1_opt <- K (lift_type_error (get_int1_as_bool bv));
is1 <- K (is1_opt or_fail UndefBehavior UndefBranch);
let compile_dest = lbl ## (λx. x >>= getc ssa);
(b, vs) = if is1 then compile_dest d1 else compile_dest d2
in DoJump <$> return b <*> sequence vs
......
......@@ -86,15 +86,14 @@ val mem_cell_types_def = Define`
(next_loc : α -> num # α)
(loc_src : α)
: (num, uvm_type list # num list) alist # α =
let ts = component_types sz ty in
let (locs, loc_src) = FOLDL
(λ(ns, s) _. (C SNOC ns ## I) (next_loc s)) ([], loc_src) ts in
(GENLIST
(λn. let sz = if n = 0 then sz else NONE in
let locs' = DROP n locs in
let offsets = TL (TAKE (LENGTH (component_types sz ty)) locs') in
(HD locs', EL n ts, offsets))
(LENGTH ts), loc_src)
let ts = component_types sz ty;
(locs, loc_src) = FOLDL
(λ(ns, s) _. (C SNOC ns ## I) (next_loc s)) ([], loc_src) ts
in (GENLIST
(λn. let sz = if n = 0 then sz else NONE; locs' = DROP n locs;
offsets = TL (TAKE (LENGTH (component_types sz ty)) locs')
in (HD locs', EL n ts, offsets))
(LENGTH ts), loc_src)
`
val new_mem_cells_def = Define`
......@@ -173,21 +172,20 @@ val mem_cell_ok_def = Define`
val mem_region_ok_def = Define`
mem_region_ok (region : mem_region) (
let offset_ok off expected_tys =
(OPTION_MAP (FST o SND) (lookup off region) = SOME expected_tys) in
let offsets_ok (_, tys, offs) =
let offset_tys = TL (component_types (SOME (LENGTH offs)) (LAST tys)) in
EVERY2 offset_ok offs offset_tys in
wf region EVERY (mem_cell_ok offsets_ok) (toList region))
(OPTION_MAP (FST o SND) (lookup off region) = SOME expected_tys);
offsets_ok (_, tys, offs) =
let offset_tys = TL (component_types (SOME (LENGTH offs)) (LAST tys))
in EVERY2 offset_ok offs offset_tys
in wf region EVERY (mem_cell_ok offsets_ok) (toList region))
`
val memory_ok_def = Define`
memory_ok mem
let region_ok (n, r) = (mem_region_ok r k. k domain r k < n) in
mem_region_ok mem.globals
wf mem.stack
region_ok mem.heap
EVERY region_ok (toList mem.stack)
let region_ok (n, r) = (mem_region_ok r k. k domain r k < n)
in mem_region_ok mem.globals
wf mem.stack
region_ok mem.heap
EVERY region_ok (toList mem.stack)
`
val new_address_space_def = Define`
......@@ -200,8 +198,9 @@ val new_address_space_def = Define`
val new_memory_def = Define`
new_memory (globals : (string # uvm_type) list) : memory + ε error =
let global_locs = GENLIST I (LENGTH globals) in
let loc_gen = LUNFOLD (λn. SOME (SUC n, n)) (LENGTH globals) in do
let global_locs = GENLIST I (LENGTH globals);
loc_gen = LUNFOLD (λn. SOME (SUC n, n)) (LENGTH globals)
in do
(_, globals) <-
FOLDL (λaccum (loc, ty). do
(loc_gen, region) <- accum;
......@@ -263,8 +262,9 @@ val memory_stack_alloc_def = Define`
(sz : num option)
(ty : uvm_type)
: (memory # addr) + ε error =
let key = stack_id_dest sid frame_id_dest fid in
let (n, s) = option_CASE (lookup key mem.stack) (0, LN) I in do
let key = stack_id_dest sid frame_id_dest fid;
(n, s) = option_CASE (lookup key mem.stack) (0, LN) I
in do
(allocated, s') <- region_alloc s sz ty (λn. n, SUC n) n;
return ((mem with stack updated_by insert key s'),
(Stack sid fid, allocated))
......@@ -309,8 +309,8 @@ val buffer_dequeue_def = Define`
val get_iaddr_cell_addrs_def = Define`
get_iaddr_cell_addrs (mem : memory) (ia : iaddr) : addr list + addr mem_error =
let region = get_region mem (FST ia.base) in
let base = SND ia.base in do
let region = get_region mem (FST ia.base); base = SND ia.base
in do
(_, base_tys, base_offs_tl) <- lookup base region
or_fail UndefBehavior (ia.base, Unallocated);
base_offs <- return (base::base_offs_tl);
......
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment