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

Commit 02bc6f3e authored by Adam Nelson's avatar Adam Nelson
Browse files

Add exceptions, REFCAST

parent 7142aea2
......@@ -505,6 +505,19 @@ struct
mk_sequence(get_args arg_tokens [], mk_prod(ty_ssa, ty_type))),
("body",
mk_sequence(map (parse_inst env) inst_lines, inst_ty)),
("exc",
mk_return(mk_const("NONE", mk_type("option", [ty_ssa])))),
("exit", parse_terminst env terminst_line),
("keepalives", mk_return(mk_list([], ty_ssa)))
]))
| [SSA (Local, label), Parens arg_tokens, Brackets [SSA (Local, exc)], Colon] =>
(label, lift_record(mk_type("bblock", [ty_ssa]), [
("args",
mk_sequence(get_args arg_tokens [], mk_prod(ty_ssa, ty_type))),
("body",
mk_sequence(map (parse_inst env) inst_lines, inst_ty)),
("exc",
mk_return(infer_comb("SOME", [mk_ssa exc], mk_type("option", [ty_ssa])))),
("exit", parse_terminst env terminst_line),
("keepalives", mk_return(mk_list([], ty_ssa)))
]))
......
......@@ -23,5 +23,10 @@ val stack_alloc_test = load_uir_file "uir/stack-store-load.uir"
|> run_schedule `single_thread_seq_cst_schedule`
|> expect_result `OK (NOR [IntV 8 4w])`
val throw_exc_test = load_uir_file "uir/throw.uir"
|> to_env |> start_at "catch" `[]`
|> run_schedule `single_thread_seq_cst_schedule`
|> expect_result `OK (NOR [IntV 8 2w])`
val _ = export_theory()
// Allocates, throws, and catches an exception.
.typedef @i8 = int<8>
.const @one <@i8> = 1
.const @two <@i8> = 2
.funcsig @intfn = () -> (@i8)
.funcsig @voidfn = () -> ()
.funcdef @throw VERSION %v1 <@voidfn> {
%entry():
%exc = NEW <@i8>
%i = GETIREF <@i8> %exc
STORE <@i8> %i @two
THROW %exc
}
.funcdef @catch VERSION %v1 <@voidfn> {
%entry():
CALL <@voidfn> @throw () EXC (%nocatch() %catch())
%catch() [%exc]:
%eint = REFCAST <ref<void> ref<@i8>> %exc
%from = GETIREF <@i8> %eint
%val = LOAD <@i8> %from
RET (%val)
%nocatch():
RET (@one)
}
......@@ -598,6 +598,7 @@ val terminst_all_vars_def = Define`terminst_all_vars i = let (a, b) = terminst_v
val _ = Datatype`
bblock = <|
args: (σ # uvm_type) list;
exc: σ option;
body: σ instruction list;
exit: σ terminst;
keepalives: σ list
......
......@@ -24,9 +24,8 @@ val _ = reveal "C" (* The C (flip) combinator is used in this theory *)
fun Cases_on_each qs = List.foldl
(fn (q, tac) => tac >> TRY (Cases_on q >> fs[])) (fs[]) qs
(* Evaluates a binary operation symbolically, producing a deferred computation
that can only be resolved once all of the registers that it depends on have
also been resolved.
(* Evaluates a binary operation, returning the result. Returns an error if the
values `v1`, `v2` are incorrectly typed, or if the result is undefined.
*)
val eval_bop_def = Define`
eval_bop bop v1 v2 : value list or_error = lift_left (C CONS [])
......@@ -60,6 +59,27 @@ val eval_cmp_def = Define`
| _ => Fail (NotImplemented "signed and FP ops")
`
(* Evaluates a conversion operation, returning the converted value. Returns
an error if the types are not compatible with the conversion, or if the
input value is not of the expected type.
*)
val eval_conv_def = Define`
eval_conv conv v ty1 ty2 : value list or_error =
case conv of
| REFCAST => (
case ty1, ty2 of
| Ref (Type Void), Ref (Type t) => (
case v of
| RefV _ a => return [RefV t a]
| _ => Fail (TypeMismatch "REFCAST" ty1 (type_of_value v)))
| Ref (Type t), Ref (Type Void) => (
case v of
| RefV _ a => return [RefV t a]
| _ => Fail (TypeMismatch "REFCAST" ty1 (type_of_value v)))
| _ => Fail (TypeMismatch "REFCAST" ty1 ty2))
| _ => Fail (NotImplemented "non-REFCAST conversions")
`
(* Evaluates an expression in a given thread, returning the values it produces.
Returns an error if the expression is ill-typed or if it produces undefined
behavior (such as division by zero).
......@@ -83,6 +103,10 @@ val eval_expr_def = Define`
assert_type_eq ty (type_of_value v2) "CmpOp rhs";
eval_cmp cmp v1 v2
od) <$> sym_value s v1 <*> sym_value s v2
| ConvOp conv ty1 ty2 v => (λv. do
assert_type_eq ty1 (type_of_value v) "ConvOp";
eval_conv conv v ty1 ty2
od) <$> sym_value s v
(* TODO: Select *)
| Select _ _ _ _ _ => pure (Fail (NotImplemented "SELECT"))
| ExtractValue ty off v => (λv. do
......@@ -221,7 +245,7 @@ val exec_inst_def = Define`
let sid = symbolic_error_join (get_stackref_id <$> sym_value th s) in
let vals = case nsc of
| PassValues vs => NOR (MAP (sym_value th o FST) vs)
| ThrowExc exc => EXC (sym_value th exc) in
| ThrowExc exc => EXC [] (sym_value th exc) in
add_register (v, await (Memory (SOME th.tid) id)) th
:> liftM (λth. (th, SOME (DoNewThread sid vals)));
case action of
......@@ -279,7 +303,7 @@ val exec_terminst_def = Define`
let rv = NOR (MAP (sym_value th) vals)
in return_stack (pop_and_resume_stack current_stack rv exec_inst th)
| Throw v =>
let rv = EXC (sym_value th v)
let rv = EXC [] (sym_value th v)
in return_stack (pop_and_resume_stack current_stack rv exec_inst th)
| Call vs cd rd => do
name <- fn_name cd.name;
......@@ -333,7 +357,7 @@ val exec_terminst_def = Define`
in update_stack_state last_stack fs);
let args = case nsc of
| PassValues vs => NOR (MAP (sym_value th o FST) vs)
| ThrowExc e => EXC (sym_value th e)
| ThrowExc e => EXC [] (sym_value th e)
in if th.stack_id = sid then
return_stack (resume_stack last_stack args exec_inst th)
else do
......
......@@ -109,7 +109,7 @@ val _ = Datatype`
resume_values =
| NOR (α list)
| EXC α ;
| EXC (α list) α ;
cmp_xchg_action_args = <|
addr: location;
......
......@@ -234,7 +234,7 @@ val has_terminated_def = Define`
EVERY (λth. NULL th.outbox (
case thread_current_frame_state th.tid state of
| SOME (DEAD (SOME (NOR vs))) => EVERY (resolvable_in state.memory) vs
| SOME (DEAD (SOME (EXC v))) => resolvable_in state.memory v
| SOME (DEAD (SOME (EXC vs e))) => EVERY (resolvable_in state.memory) (e::vs)
| SOME (DEAD NONE) => T
| _ => F
)) (MAP THE (FILTER IS_SOME state.threads))
......@@ -246,8 +246,9 @@ val get_return_values_def = Define`
| SOME (DEAD (SOME (NOR vs))) =>
NOR o MAP THE <$>
sequence_left (MAP (resolve_symbolic state.memory) vs)
| SOME (DEAD (SOME (EXC v))) =>
EXC o THE <$> resolve_symbolic state.memory v
| SOME (DEAD (SOME (EXC vs e))) =>
EXC <$> (MAP THE <$> sequence_left (MAP (resolve_symbolic state.memory) vs))
<*> (THE <$> resolve_symbolic state.memory e)
| SOME (DEAD NONE) => Fail (UndefinedBehavior "no return value")
| _ => Fail (InvalidState "schedule exhausted")
`
......
......@@ -188,6 +188,7 @@ val get_block_def = Define`
block <- expect (FLOOKUP fn.blocks label) (InvalidIR "block not found");
let reg = λv. (v, th.block_id) in return <|
args := MAP (reg ## I) block.args;
exc := OPTION_MAP reg block.exc;
body := MAP (map_inst reg) block.body;
exit := map_terminst reg block.exit;
keepalives := MAP reg block.keepalives
......@@ -275,26 +276,37 @@ val resume_frame_def = Define`
let initial_action_id = th.action_id in
let th = th with <| block_id updated_by block_id_suc |> in
case fr.state of
| READY ia rd => (
case res of
| NOR args => do
block <- get_block (FST rd.normal_dest) fr.fn th;
assert (LENGTH (SND rd.normal_dest) = LENGTH block.args)
(InvalidIR "block arity mismatch");
th <- FOLDL (λs r. s >>= add_register r) (return th)
(ZIP (MAP FST block.args, insert_resume_args rd.normal_dest ia args th));
th <- FOLDL (λs i. s >>= exec_inst i) (return th) block.body;
th <- FOLDL (λs a. s >>= enqueue_action a) (return th)
(LIST_BIND th.outbox (λm.
case m of
| (id, DoAlloca ty sid _) =>
if initial_action_id id
then [DoFree ty (StackAddr sid th.tid id)]
else []
| _ => []));
return (fr with state := ACTIVE block.exit, th)
od
| EXC _ => Fail (NotImplemented "exceptions"))
| READY ia rd => do
(args, exc, dest) <-
case res of
| NOR args => return (args, NONE, rd.normal_dest)
| EXC args exc =>
let exc = symbolic_error_join (
(λe. case e of
| RefV _ a => return (RefV Void a)
| _ => Fail (TypeMismatch "exception"
(Ref (Type Void)) (type_of_value e))) <$> exc) in
expect rd.exceptional_dest (UndefinedBehavior "uncaught exception")
:> liftM (λdest. (args, SOME exc, dest));
block <- get_block (FST dest) fr.fn th;
assert (LENGTH (SND dest) = LENGTH block.args)
(InvalidIR "block arity mismatch");
th <- case exc, block.exc of
| SOME v, SOME r => add_register (r, v) th
| _ => return th;
th <- FOLDL (λs r. s >>= add_register r) (return th)
(ZIP (MAP FST block.args, insert_resume_args dest ia args th));
th <- FOLDL (λs i. s >>= exec_inst i) (return th) block.body;
th <- FOLDL (λs a. s >>= enqueue_action a) (return th)
(LIST_BIND th.outbox (λm.
case m of
| (id, DoAlloca ty sid _) =>
if initial_action_id id
then [DoFree ty (StackAddr sid th.tid id)]
else []
| _ => []));
return (fr with state := ACTIVE block.exit, th)
od
| _ => Fail (InvalidState "cannot resume a non-ready frame")
`
......@@ -302,16 +314,21 @@ val resume_frame_follows = store_thm("resume_frame_follows",
``(i t0 t1. exec i t0 = OK t1 thread_follows t0 t1)
resume_frame f0 r exec t0 = OK (f1, t1)
thread_follows t0 t1``,
rw[resume_frame_def] >>
Cases_on `f0.state` >> fs[] >>
Cases_on `r` >> fs[] >>
rw[resume_frame_def] >> Cases_on `f0.state` >> fs[] >>
Cases_on `r` >> fs[] >> rw[] >> fs[] >>
Q.ABBREV_TAC `t0' = t0 with block_id updated_by block_id_suc` >>
`thread_follows th' t1` by metis_tac[enqueue_action_follows, foldl_follows] >>
`thread_follows th th'` by metis_tac[foldl_follows] >>
`thread_follows t0' th` by metis_tac[add_register_follows, foldl_follows] >>
`thread_follows t0 t0'` suffices_by metis_tac[thread_follows_trans] >>
Q.UNABBREV_TAC `t0'` >>
rw[thread_follows_def] >> fs[])
`thread_follows t0 t0'`
by (Q.UNABBREV_TAC `t0'` >> rw[thread_follows_def] >> fs[])
>- (`thread_follows t0' th thread_follows th th' thread_follows th' t1`
suffices_by metis_tac[thread_follows_trans] >>
metis_tac[enqueue_action_follows, add_register_follows, foldl_follows])
>- (Cases_on `y0` >> Cases_on `r` >> fs[APP_DEF] >>
`thread_follows t0' th`
by (Cases_on `q'` >> Cases_on `block.exc` >> fs[] >>
metis_tac[add_register_follows, thread_follows_refl]) >>
`thread_follows th th' thread_follows th' th'' thread_follows th'' t1`
suffices_by metis_tac[thread_follows_trans] >>
metis_tac[enqueue_action_follows, add_register_follows, foldl_follows]))
local val foldl_propagates_ok = prove(
``(r. propagates thread_ok (f r))
......@@ -325,10 +342,15 @@ in val resume_frame_ok = store_thm("resume_frame_ok",
f r. propagates thread_ok (lift_left SND o resume_frame f r exec)``,
rw[] >> rw[propagates_def, resume_frame_def] >> POP_ASSUM MP_TAC >>
REPEAT CASE_TAC >> rw[] >> fs[] >>
`thread_ok (a with block_id updated_by block_id_suc)` suffices_by
metis_tac[foldl_propagates_ok, add_register_ok, enqueue_action_ok] >>
rw[thread_ok_def] >> fs[thread_ok_def] >>
metis_tac[block_id_lt_suc, block_id_lt_trans])
`thread_ok (a with block_id updated_by block_id_suc)`
by (rw[thread_ok_def] >> fs[thread_ok_def] >>
metis_tac[block_id_lt_suc, block_id_lt_trans])
>- metis_tac[foldl_propagates_ok, add_register_ok, enqueue_action_ok]
>- (Cases_on `y0'` >> Cases_on `r'` >> Cases_on `q'` >> fs[APP_DEF] >>
Cases_on `block.exc` >> fs[] >> rw[]
>- metis_tac[foldl_propagates_ok, add_register_ok, enqueue_action_ok]
>- (`thread_ok th` by metis_tac[add_register_ok, propagates_def] >>
metis_tac[foldl_propagates_ok, add_register_ok, enqueue_action_ok])))
end
val resume_stack_def = Define`
......@@ -365,7 +387,8 @@ val resume_stack_stack_ok = store_thm("resume_stack_stack_ok",
``r exec t. propagates stack_ok (λs. FST <$> resume_stack s r exec t)``,
rw[propagates_def, stack_ok_def, resume_stack_def] >> Cases_on `s.frames` >>
fs[] >> Cases_on `y0` >> Cases_on `y0'` >> fs[resume_frame_def] >> rw[] >>
REPEAT (POP_ASSUM MP_TAC) >> REPEAT CASE_TAC >> rw[] >> fs[])
REPEAT (POP_ASSUM MP_TAC) >> REPEAT CASE_TAC >> rw[APP_DEF] >> fs[] >>
rw[] >> fs[])
val update_stack_state_def = Define`
update_stack_state (s : stack) (fs : frame_state) : stack or_error =
......
......@@ -291,12 +291,12 @@ val (canconvert_rules, canconvert_ind, canconvert_cases) = Hol_reln`
canconvert M BITCAST (IRef PTR ty) (Int n))
(* refcast cases *)
(ty. canconvert M BITCAST (Ref (Type Void)) (Ref ty))
(ty. canconvert M BITCAST (Ref ty) (Ref (Type Void)))
(ty. canconvert M REFCAST (Ref (Type Void)) (Ref ty))
(ty. canconvert M REFCAST (Ref ty) (Ref (Type Void)))
(fx1 fx2 tys1 tys2.
(* FIXME: Equivalence is MUCH harder than this w.r.t. fixpoints *)
(tys1 <<= tys2 tys2 <<= tys1)
canconvert M BITCAST (Ref (Type (Struct fx1 tys1)))
canconvert M REFCAST (Ref (Type (Struct fx1 tys1)))
(Ref (Type (Struct fx2 tys2))))
`
......
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