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

Commit 535fca59 authored by Adam Nelson's avatar Adam Nelson
Browse files

Add SwapStack to threadSemantics

parent ba4f1d11
......@@ -529,17 +529,21 @@ val exec_terminst_def = Define`
case n of
| INR name => return name
| INL _ => SND <$> (expect guess InvalidStep >>= get_funcref_data) in
let const_or_guess = λvalue.
case value of
| Const v => return v
| Var _ => (case guess of SOME v => return v | NONE => Fail InvalidStep) in
let proceed = λargs next_stack. do
(next_stack, state) <- resume_stack next_stack args state;
case next_stack.id of (Stack n) =>
return (LUPDATE next_stack n stacks, state)
od in
let get_current_stack = λstate stacks.
case state.stack_id of Stack n =>
let get_stack = λsid stacks.
case sid of Stack n =>
if n < LENGTH stacks
then return (EL n stacks)
else Fail (InvalidState "stack index out of bounds") in
get_current_stack state stacks >>= λcurrent_stack.
get_stack state.stack_id stacks >>= λcurrent_stack.
case current_stack.frames of
| [] => Fail (InvalidState "stack is empty")
| fr::rest => (
......@@ -580,13 +584,8 @@ val exec_terminst_def = Define`
|> in
proceed (NOR []) (current_stack with frames := fr::rest)
| Branch2 cond dest1 dest2 => do
cond_bool <-
case cond of
| Const v => get_int1_as_bool v
| Var _ => (
case guess of
| SOME (IntV 1 _) => get_int1_as_bool (THE guess)
| _ => Fail InvalidStep);
cond_value <- const_or_guess cond;
cond_bool <- get_int1_as_bool cond_value;
let fr = fr with state := READY <|
normal_dest := if cond_bool then dest1 else dest2;
exceptional_dest := NONE
......@@ -594,13 +593,9 @@ val exec_terminst_def = Define`
proceed (NOR []) (current_stack with frames := fr::rest)
od
| Switch ty param default_dest branches => do
param_value <-
case param of
| Const v => return v
| Var _ => (
case guess of
| SOME v => assert (type_of_value v = ty) InvalidStep >> return v
| _ => Fail InvalidStep);
param_value <- const_or_guess param;
assert (type_of_value param_value = ty)
(TypeMismatch "SWITCH" ty (type_of_value param_value));
let fr = fr with state := READY <|
normal_dest := case FLOOKUP branches param_value of
| SOME dest => dest
......@@ -609,9 +604,28 @@ val exec_terminst_def = Define`
|> in
proceed (NOR []) (current_stack with frames := fr::rest)
od
| SwapStack st nsc csc rd => do
stack_ref <- const_or_guess (Var st);
sid <- get_stackref_id stack_ref;
last_stack <- get_stack state.stack_id stacks;
next_stack <- get_stack sid stacks;
let last_stack = last_stack with frames updated_by (λf. case f of
| fr::rest => (fr with state := (case csc of
(* TODO: Assert that 'tys' is valid *)
| RetWith tys => READY rd
| KillOld => DEAD NONE))::rest) in
let args = case nsc of
| PassValues vs => NOR (MAP (sym_value state o FST) vs)
| ThrowExc e => EXC (sym_value state e) in do
(next_stack, state) <- resume_stack next_stack args state;
case last_stack.id of Stack m =>
case next_stack.id of Stack n =>
return (LUPDATE next_stack n (LUPDATE last_stack m stacks), state)
od
od
| CommInst ci args rd => do
(stacks, state, res) <- (exec_comm_inst ci args env guess stacks state);
current_stack <- get_current_stack state stacks;
current_stack <- get_stack state.stack_id stacks;
case current_stack.frames of
| hd::tl => (
case hd.state of
......@@ -622,16 +636,17 @@ val exec_terminst_def = Define`
| _ => return (stacks, state)
od
| _ => Fail (NotImplemented "not all terminsts are implemented"))
(* TODO: Watchpoint, WPBranch, SwapStack, ExcClause *)
(* TODO: Watchpoint, WPBranch, ExcClause *)
`
val exec_terminst_follows = store_thm("exec_terminst_follows",
``exec_terminst env i guess k0 s0 = OK (k1, s1) state_follows s0 s1``,
rw[exec_terminst_def] >>
Cases_on_each [`i`, `guess`, `s0.stack_id`, `current_stack.frames`, `t`, `y0`,
`(q:stack).id`, `r`, `r'`, `current_stack'.frames`, `s1.stack_id`,
`h'.state`, `h''.state`, `q'.stack_id`, `y0`, `q''.id`] >>
metis_tac[resume_stack_follows, exec_comm_inst_follows, state_follows_refl])
simp[exec_terminst_def] >>
REPEAT (
CASE_TAC >> REPEAT CASE_TAC >> rw[] >>
Cases_on_each [`y0`, `y0'`, `r'`] >> fs[] >>
TRY (metis_tac[resume_stack_follows, exec_comm_inst_follows, state_follows_refl]) >>
REPEAT (POP_ASSUM MP_TAC)))
val _ = export_theory()
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