diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 313 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 59 | ||||
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 121 |
3 files changed, 353 insertions, 140 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index dbc8e0e6..cbd56240 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -833,58 +833,6 @@ let rec interp_to_outcome mode context thunk = end ) end -let interp mode (IState interp_state context) = - match interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode interp_state Nothing) with - | (o,_) -> o -end - -val state_to_outcome_s : (instruction_state -> unit -> (string * string)) -> interp_mode -> instruction_state -> Sail_impl_base.outcome_s unit -val outcome_to_outcome : (instruction_state -> unit -> (string * string)) -> interp_mode -> Interp_interface.outcome -> Sail_impl_base.outcome unit - -let rec outcome_to_outcome pp_instruction_state mode = - let state_to_outcome_s = state_to_outcome_s pp_instruction_state in - function - | Interp_interface.Read_mem rk addr size _ k -> - Sail_impl_base.Read_mem (rk,addr,size) (fun v -> state_to_outcome_s mode (k v)) - | Interp_interface.Write_mem rk addr size _ mv _ k -> - failwith "Write_mem not supported anymore" - | Interp_interface.Write_ea wk addr size _ state -> - Sail_impl_base.Write_ea (wk,addr,size) (state_to_outcome_s mode state) - | Interp_interface.Write_memv _ mv _ k -> - Sail_impl_base.Write_memv mv (fun v -> state_to_outcome_s mode (k v)) - | Interp_interface.Barrier bk state -> - Sail_impl_base.Barrier bk (state_to_outcome_s mode state) - | Interp_interface.Footprint state -> - Sail_impl_base.Footprint (state_to_outcome_s mode state) - | Interp_interface.Read_reg r k -> - Sail_impl_base.Read_reg r (fun v -> state_to_outcome_s mode (k v)) - | Interp_interface.Write_reg r rv state -> - Sail_impl_base.Write_reg (r,rv) (state_to_outcome_s mode state) - | Interp_interface.Nondet_choice _ _ -> - failwith "Nondet_choice not supported yet" - | Interp_interface.Escape _ _ -> - Sail_impl_base.Escape Nothing - | Interp_interface.Fail maybestring -> - Sail_impl_base.Fail maybestring - | Interp_interface.Internal maybestring maybeprint state -> - Sail_impl_base.Internal (maybestring,maybeprint) (state_to_outcome_s mode state) - | Interp_interface.Analysis_non_det _ _ -> - failwith "Analysis_non_det outcome returned" - | Interp_interface.Done -> - Sail_impl_base.Done () - | Interp_interface.Error message -> - failwith ("Interpreter error: " ^ message) -end - -and state_to_outcome_s pp_instruction_state mode state = - let next_outcome' = interp mode state in - let next_outcome = outcome_to_outcome pp_instruction_state mode next_outcome' in - (next_outcome, Just (pp_instruction_state state)) - -val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> instruction -> Sail_impl_base.outcome_s unit -let initial_outcome_s_of_instruction pp_instruction_state context mode instruction = - let state = instruction_to_istate context instruction in - state_to_outcome_s pp_instruction_state mode state (*Update slice potentially here*) @@ -895,6 +843,13 @@ let reg_size = function | Reg_f_slice i _ _ f _ (p1,p2) -> if p1 < p2 then p2-p1 +1 else p1-p2+1 end + +let interp mode (IState interp_state context) = + match interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode interp_state Nothing) with + | (o,_) -> o +end + + (*ie_loop returns a tuple of event list, and a tuple ofinternal interpreter memory, bool to indicate normal or exceptional termination*) let rec ie_loop mode register_values (IState interp_state context) = let (Context _ direction externs reads writes write_eas write_vals barriers) = context in @@ -968,12 +923,71 @@ let rec ie_loop mode register_values (IState interp_state context) = | _ -> Assert_extra.failwith "interp_to_outcome may have produced a nondet action" end ;; +val interp_exhaustive : maybe (list (reg_name * register_value)) -> instruction_state -> list event let interp_exhaustive register_values i_state = let mode = make_mode_exhaustive E_big_endian in match ie_loop mode register_values i_state with | (events,_) -> events end + +val state_to_outcome_s : + (instruction_state -> unit -> (string * string)) -> + interp_mode -> instruction_state -> Sail_impl_base.outcome_s unit +val outcome_to_outcome : + (instruction_state -> unit -> (string * string)) -> + interp_mode -> Interp_interface.outcome -> Sail_impl_base.outcome unit + +let rec outcome_to_outcome pp_instruction_state mode = + let state_to_outcome_s = + state_to_outcome_s pp_instruction_state in + function + | Interp_interface.Read_mem rk addr size _ k -> + Sail_impl_base.Read_mem (rk,addr,size) (fun v -> state_to_outcome_s mode (k v)) + | Interp_interface.Write_mem rk addr size _ mv _ k -> + failwith "Write_mem not supported anymore" + | Interp_interface.Write_ea wk addr size _ state -> + Sail_impl_base.Write_ea (wk,addr,size) (state_to_outcome_s mode state) + | Interp_interface.Write_memv _ mv _ k -> + Sail_impl_base.Write_memv mv (fun v -> state_to_outcome_s mode (k v)) + | Interp_interface.Barrier bk state -> + Sail_impl_base.Barrier bk (state_to_outcome_s mode state) + | Interp_interface.Footprint state -> + Sail_impl_base.Footprint (state_to_outcome_s mode state) + | Interp_interface.Read_reg r k -> + Sail_impl_base.Read_reg r (fun v -> state_to_outcome_s mode (k v)) + | Interp_interface.Write_reg r rv state -> + Sail_impl_base.Write_reg (r,rv) (state_to_outcome_s mode state) + | Interp_interface.Nondet_choice _ _ -> + failwith "Nondet_choice not supported yet" + | Interp_interface.Escape _ _ -> + Sail_impl_base.Escape Nothing + | Interp_interface.Fail maybestring -> + Sail_impl_base.Fail maybestring + | Interp_interface.Internal maybestring maybeprint state -> + Sail_impl_base.Internal (maybestring,maybeprint) (state_to_outcome_s mode state) + | Interp_interface.Analysis_non_det _ _ -> + failwith "Analysis_non_det outcome returned" + | Interp_interface.Done -> + Sail_impl_base.Done () + | Interp_interface.Error message -> + failwith ("Interpreter error: " ^ message) +end + +and state_to_outcome_s pp_instruction_state mode state = + let next_outcome' = interp mode state in + let next_outcome = outcome_to_outcome pp_instruction_state mode next_outcome' in + (next_outcome, + Just ((pp_instruction_state state), + (fun env -> interp_exhaustive (Just env) state)) + ) + +val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> instruction -> Sail_impl_base.outcome_s unit +let initial_outcome_s_of_instruction pp_instruction_state context mode instruction = + let state = instruction_to_istate context instruction in + state_to_outcome_s pp_instruction_state mode state + + (*This code is no longer uptodate. If no one is using it, then we don't need to fix it If someone is using it, this will let me know*) (*let rec rr_ie_loop mode i_state = @@ -1006,3 +1020,198 @@ If someone is using it, this will let me know*) let rr_interp_exhaustive mode i_state events = let (events',outcome) = rr_ie_loop mode i_state in ((events ++ events'),outcome) *) + + +let instruction_kind_of_event : event -> maybe instruction_kind = function + | E_read_mem rk _ _ _ -> Just (IK_mem_read rk) + | E_write_mem wk _ _ _ _ _ -> Just (IK_mem_write wk) + | E_write_ea wk _ _ _ -> Just (IK_mem_write wk) + | E_write_memv _ _ _ -> Nothing + | E_barrier bk -> Just (IK_barrier bk) + | E_footprint -> Nothing + | E_read_reg _ -> Nothing + | E_write_reg _ _ -> Nothing + | E_error s -> failwith ("instruction_kind_of_event error: "^s) + | E_escape -> Nothing (*failwith ("instruction_kind_of_event escape")*) + end +(* TODO: how can we decide, looking only at the output of interp_exhaustive, + that an instruction is a conditional branch? *) + +let regs_in_of_event : event -> list reg_name = function + | E_read_mem _ _ _ _ -> [] + | E_write_mem _ _ _ _ _ _ -> [] + | E_write_ea _ _ _ _ -> [] + | E_write_memv _ _ _ -> [] + | E_barrier _ -> [] + | E_footprint -> [] + | E_read_reg r -> [r] + | E_write_reg _ _ -> [] + | E_error s -> failwith ("regs_in_of_event "^s) + | E_escape -> [] (*failwith ("regs_in_of_event escape")*) + end + +let regs_out_of_event : event -> list reg_name = function + | E_read_mem _ _ _ _ -> [] + | E_write_mem _ _ _ _ _ _ -> [] + | E_write_ea _ _ _ _ -> [] + | E_write_memv _ _ _ -> [] + | E_barrier _ -> [] + | E_footprint -> [] + | E_read_reg _ -> [] + | E_write_reg r _ -> [r] + | E_error s -> failwith ("regs_out_of_event "^s) + | E_escape -> [] (*failwith ("regs_out_of_event escape")*) + end + + +let regs_feeding_memory_access_address_of_event : event -> list reg_name = function + | E_read_mem _ _ _ (Just rs) -> rs + | E_read_mem _ _ _ None -> [] + | E_write_mem _ _ _ (Just rs) _ _ -> rs + | E_write_mem _ _ _ None _ _ -> [] + | E_write_ea wk _ _ (Just rs) -> rs + | E_write_ea wk _ _ None -> [] + | E_write_memv _ _ _ -> [] + | E_barrier bk -> [] + | E_footprint -> [] + | E_read_reg _ -> [] + | E_write_reg _ _ -> [] + | E_error s -> failwith ("regs_feeding_memory_access_address_of_event " ^ s) + | E_escape -> [] (*failwith ("regs_feeding_memory_access_address_of_event escape")*) +end + +let nia_address_of_event nia_reg (event: event) : maybe (maybe address) = + (* return Nothing for unknown/undef *) + match event with + | E_write_reg reg reg_value -> + if register_base_name reg = register_base_name nia_reg then + let al = match address_lifted_of_register_value reg_value with + | Just al -> al + | Nothing -> failwith "nia_register_of_event: NIA read not 64 bits" + end in + Just (address_of_address_lifted al) + else Nothing + | _ -> Nothing + end + +let nias_of_instruction + thread_ism + (nia_address: list (maybe address)) (* Nothing for unknown/undef*) + (regs_in: list reg_name) + (instruction: instruction) + : list nia + = + let (instruction_name, instruction_fields) = instruction in + + let unknown_nia_address = List.elem Nothing nia_address in + + let nias = [NIA_concrete_address addr | forall (addr MEM (List.mapMaybe id nia_address)) | true] in + + (* it's a fact of the Power2.06B instruction pseudocode that in the B and Bc + cases there should be no Unknown values in nia_values, while in the Bclr + and Bcctr cases nia_values will just be Unknown and the semantics should + match the comments in the machineDefTypes definition of nia *) + (* All our other analysis is on the pseudocode directly, which is arguably + pleasingly robust. We could replace the nias pattern match on + instruction_name with something in that style if the exhaustive interpreter + announced register dependencies to register writes (easy) and if it could + check the form of the register writes to LR and CTR matches the + machineDefTypes nia definition *) + match (thread_ism, instruction_name) with + | ("PPCGEN_ism", "B") -> + let () = ensure (not unknown_nia_address) + "unexpected unknown/undefined address in nia_values" in + nias + | ("PPCGEN_ism", "Bc") -> + let () = ensure (not unknown_nia_address) + "unexpected unknown/undefined address in nia_values" in + NIA_successor :: nias + | ("PPCGEN_ism", "Bclr") -> [ NIA_successor; NIA_LR ] + | ("PPCGEN_ism", "Bcctr") -> [ NIA_successor; NIA_CTR ] + | ("PPCGEN_ism", "Sc") -> + let () = ensure (not unknown_nia_address) + "unexpected unknown/undefined address in nia_values" in + match instruction_fields with + | [(_, _, lev)] -> + (* LEV field is 7 bits long, pad it with false at beginning *) + if lev = [Bitc_zero;Bitc_one;Bitc_one;Bitc_one;Bitc_one;Bitc_one;Bitc_one] + (* (Interp_inter_imp.integer_of_byte_list (Interp_inter_imp.to_bytes (false :: bl))) = 63 *) + then [] + else [NIA_successor] + | _ -> [ NIA_successor ] + end + + (* AARch64 label branch (i.e. address must be known) although + these instructions take the address as an offset from PC, in here + we see the absolute address as it was extracted from the micro ops + just before write to PC *) + | ("AArch64HandSail", "BranchImmediate") -> nias + | ("AArch64HandSail", "BranchConditional") -> NIA_successor :: nias + | ("AArch64HandSail", "CompareAndBranch") -> NIA_successor :: nias + | ("AArch64HandSail", "TestBitAndBranch") -> NIA_successor :: nias + + (* AArch64 calculated address branch *) + | ("AArch64HandSail", "BranchRegister") -> + (* do some parsing of the ast fields to figure out which register holds + the branching address i.e. find n in "BR <Xn>". The ast constructor + from armV8.sail: (reg_index,BranchType) BranchRegister; *) + let n_integer = + match instruction_fields with + | [(_, _, n); _] -> integer_of_bit_list n + | _ -> fail + end + in + let () = ensure (0 <= n_integer && n_integer <= 31) + "expected register number from 0 to 31" + in + if n_integer = 31 then + nias (* BR XZR *) + else + (* look for Xn (which we actually call Rn) in regs_in *) + let n_reg = "R" ^ (String_extra.stringFromInteger n_integer) in + [NIA_register r | forall (r MEM regs_in) + | match r with + | (Reg name _ _ _) -> name = n_reg + | _ -> false + end] + + | ("AArch64LitmusSail", "CtrlDep") -> NIA_successor :: nias + + | ("MIPS_ism", "B") -> fail + + | _ -> + let () = ensure (not unknown_nia_address) + "unexpected unknown/undefined address in nia_values" in + [ NIA_successor ] + end + +let interp_instruction_analysis + (interp_exhaustive : ((list (reg_name * register_value)) -> list event)) + instruction nia_reg ism environment = + + let es = interp_exhaustive environment in + + let regs_in = List.concatMap regs_in_of_event es in + let regs_out = List.concatMap regs_out_of_event es in + + let regs_feeding_address = List.concatMap regs_feeding_memory_access_address_of_event es in + + let nia_address = List.mapMaybe (nia_address_of_event nia_reg) es in + + let nias = nias_of_instruction ism nia_address regs_in instruction in + + let dia = DIA_none in (* FIX THIS! *) + + + let inst_kind = + match List.mapMaybe instruction_kind_of_event es with + | [] -> if List.length nias > 1 then IK_cond_branch else IK_simple + | inst_kind :: inst_kinds -> + let () = ensure (forall (inst_kind' MEM inst_kinds). inst_kind' = inst_kind) + "multiple instruction kinds" in + let () = ensure (List.length nias > 1 --> inst_kind = IK_cond_branch) + "multiple NIAs must be IK_cond_branch" in + inst_kind + end in + + (regs_in, regs_out, regs_feeding_address, nias, dia, inst_kind) diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index bf6c6779..1de2de77 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -188,65 +188,6 @@ type outcome = (*Interpreter error*) | Error of string -type event = -| E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name) -| E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name) -| E_write_ea of write_kind * address_lifted * nat * maybe (list reg_name) -| E_write_memv of maybe address_lifted * memory_value * maybe (list reg_name) -| E_barrier of barrier_kind -| E_footprint -| E_read_reg of reg_name -| E_write_reg of reg_name * register_value -| E_escape -| E_error of string - - -let ~{ocaml} eventCompare e1 e2 = - match (e1,e2) with - | (E_read_mem rk1 v1 i1 tr1, E_read_mem rk2 v2 i2 tr2) -> - compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) - | (E_write_mem wk1 v1 i1 tr1 v1' tr1', E_write_mem wk2 v2 i2 tr2 v2' tr2') -> - compare ((wk1,v1,i1),(tr1,v1',tr1')) ((wk2,v2,i2),(tr2,v2',tr2')) - | (E_write_ea wk1 a1 i1 tr1, E_write_ea wk2 a2 i2 tr2) -> - compare (wk1, (a1, i1, tr1)) (wk2, (a2, i2, tr2)) - | (E_write_memv _ mv1 tr1, E_write_memv _ mv2 tr2) -> compare (mv1,tr1) (mv2,tr2) - | (E_barrier bk1, E_barrier bk2) -> compare bk1 bk2 - | (E_read_reg r1, E_read_reg r2) -> compare r1 r2 - | (E_write_reg r1 v1, E_write_reg r2 v2) -> compare (r1,v1) (r2,v2) - | (E_error s1, E_error s2) -> compare s1 s2 - | (E_escape,E_escape) -> EQ - | (E_read_mem _ _ _ _, _) -> LT - | (E_write_mem _ _ _ _ _ _, _) -> LT - | (E_write_ea _ _ _ _, _) -> LT - | (E_write_memv _ _ _, _) -> LT - | (E_barrier _, _) -> LT - | (E_read_reg _, _) -> LT - | (E_write_reg _ _, _) -> LT - | _ -> GT - end -let inline {ocaml} eventCompare = defaultCompare - -let ~{ocaml} eventLess b1 b2 = eventCompare b1 b2 = LT -let ~{ocaml} eventLessEq b1 b2 = eventCompare b1 b2 <> GT -let ~{ocaml} eventGreater b1 b2 = eventCompare b1 b2 = GT -let ~{ocaml} eventGreaterEq b1 b2 = eventCompare b1 b2 <> LT - -let inline {ocaml} eventLess = defaultLess -let inline {ocaml} eventLessEq = defaultLessEq -let inline {ocaml} eventGreater = defaultGreater -let inline {ocaml} eventGreaterEq = defaultGreaterEq - -instance (Ord event) - let compare = eventCompare - let (<) = eventLess - let (<=) = eventLessEq - let (>) = eventGreater - let (>=) = eventGreaterEq -end - -instance (SetType event) - let setElemCompare = compare -end (* Functions to build up the initial state for interpretation *) diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 9679b658..76ac1797 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -418,35 +418,6 @@ they just have particular nias (and will be IK_simple *) (* | IK_uncond_branch *) | IK_simple -(* the address_lifted types should go away here and be replaced by address *) -type with_pp 'o = 'o * maybe (unit -> (string * string)) -type outcome 'a = - (* Request to read memory, value is location to read, integer is size to read, - followed by registers that were used in computing that size *) - | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_pp (outcome 'a)) - (* Tell the system a write is imminent, at address lifted, of size nat *) - | Write_ea of (write_kind * address_lifted * nat) * (with_pp (outcome 'a)) - (* Request to write memory at last signalled address. Memory value should be 8 - times the size given in ea signal *) - | Write_memv of memory_value * (bool -> with_pp (outcome 'a)) - (* Request a memory barrier *) - | Barrier of barrier_kind * with_pp (outcome 'a) - (* Tell the system to dynamically recalculate dependency footprint *) - | Footprint of with_pp (outcome 'a) - (* Request to read register, will track dependency when mode.track_values *) - | Read_reg of reg_name * (register_value -> with_pp (outcome 'a)) - (* Request to write register *) - | Write_reg of (reg_name * register_value) * with_pp (outcome 'a) - | Escape of maybe string - (*Result of a failed assert with possible error message to report*) - | Fail of maybe string - | Internal of (maybe string * maybe (unit -> string)) * with_pp (outcome 'a) - | Done of 'a - | Error of string - -type outcome_s 'a = with_pp (outcome 'a) -(* first string : output of instruction_stack_to_string - second string: output of local_variables_to_string *) let ~{ocaml} read_kindCompare rk1 rk2 = match (rk1, rk2) with @@ -744,6 +715,98 @@ instance (Ord barrier_kind) let (>=) = barrier_kindGreaterEq end + +type event = +| E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name) +| E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name) +| E_write_ea of write_kind * address_lifted * nat * maybe (list reg_name) +| E_write_memv of maybe address_lifted * memory_value * maybe (list reg_name) +| E_barrier of barrier_kind +| E_footprint +| E_read_reg of reg_name +| E_write_reg of reg_name * register_value +| E_escape +| E_error of string + + +let ~{ocaml} eventCompare e1 e2 = + match (e1,e2) with + | (E_read_mem rk1 v1 i1 tr1, E_read_mem rk2 v2 i2 tr2) -> + compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) + | (E_write_mem wk1 v1 i1 tr1 v1' tr1', E_write_mem wk2 v2 i2 tr2 v2' tr2') -> + compare ((wk1,v1,i1),(tr1,v1',tr1')) ((wk2,v2,i2),(tr2,v2',tr2')) + | (E_write_ea wk1 a1 i1 tr1, E_write_ea wk2 a2 i2 tr2) -> + compare (wk1, (a1, i1, tr1)) (wk2, (a2, i2, tr2)) + | (E_write_memv _ mv1 tr1, E_write_memv _ mv2 tr2) -> compare (mv1,tr1) (mv2,tr2) + | (E_barrier bk1, E_barrier bk2) -> compare bk1 bk2 + | (E_read_reg r1, E_read_reg r2) -> compare r1 r2 + | (E_write_reg r1 v1, E_write_reg r2 v2) -> compare (r1,v1) (r2,v2) + | (E_error s1, E_error s2) -> compare s1 s2 + | (E_escape,E_escape) -> EQ + | (E_read_mem _ _ _ _, _) -> LT + | (E_write_mem _ _ _ _ _ _, _) -> LT + | (E_write_ea _ _ _ _, _) -> LT + | (E_write_memv _ _ _, _) -> LT + | (E_barrier _, _) -> LT + | (E_read_reg _, _) -> LT + | (E_write_reg _ _, _) -> LT + | _ -> GT + end +let inline {ocaml} eventCompare = defaultCompare + +let ~{ocaml} eventLess b1 b2 = eventCompare b1 b2 = LT +let ~{ocaml} eventLessEq b1 b2 = eventCompare b1 b2 <> GT +let ~{ocaml} eventGreater b1 b2 = eventCompare b1 b2 = GT +let ~{ocaml} eventGreaterEq b1 b2 = eventCompare b1 b2 <> LT + +let inline {ocaml} eventLess = defaultLess +let inline {ocaml} eventLessEq = defaultLessEq +let inline {ocaml} eventGreater = defaultGreater +let inline {ocaml} eventGreaterEq = defaultGreaterEq + +instance (Ord event) + let compare = eventCompare + let (<) = eventLess + let (<=) = eventLessEq + let (>) = eventGreater + let (>=) = eventGreaterEq +end + +instance (SetType event) + let setElemCompare = compare +end + + +(* the address_lifted types should go away here and be replaced by address *) +type with_aux 'o = 'o * maybe ((unit -> (string * string)) * ((list (reg_name * register_value)) -> list event)) +type outcome 'a = + (* Request to read memory, value is location to read, integer is size to read, + followed by registers that were used in computing that size *) + | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_aux (outcome 'a)) + (* Tell the system a write is imminent, at address lifted, of size nat *) + | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome 'a)) + (* Request to write memory at last signalled address. Memory value should be 8 + times the size given in ea signal *) + | Write_memv of memory_value * (bool -> with_aux (outcome 'a)) + (* Request a memory barrier *) + | Barrier of barrier_kind * with_aux (outcome 'a) + (* Tell the system to dynamically recalculate dependency footprint *) + | Footprint of with_aux (outcome 'a) + (* Request to read register, will track dependency when mode.track_values *) + | Read_reg of reg_name * (register_value -> with_aux (outcome 'a)) + (* Request to write register *) + | Write_reg of (reg_name * register_value) * with_aux (outcome 'a) + | Escape of maybe string + (*Result of a failed assert with possible error message to report*) + | Fail of maybe string + | Internal of (maybe string * maybe (unit -> string)) * with_aux (outcome 'a) + | Done of 'a + | Error of string + +type outcome_s 'a = with_aux (outcome 'a) +(* first string : output of instruction_stack_to_string + second string: output of local_variables_to_string *) + (** operations and coercions on basic values *) val word8_to_bitls : word8 -> list bit_lifted |