summaryrefslogtreecommitdiff
path: root/src/lem_interp
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp')
-rw-r--r--src/lem_interp/interp.lem3
-rw-r--r--src/lem_interp/interp_ast.lem1
-rw-r--r--src/lem_interp/interp_inter_imp.lem45
-rw-r--r--src/lem_interp/interp_interface.lem9
-rw-r--r--src/lem_interp/interp_utilities.lem2
-rw-r--r--src/lem_interp/pretty_interp.ml1
-rw-r--r--src/lem_interp/printing_functions.ml2
-rw-r--r--src/lem_interp/run_interp_model.ml4
-rw-r--r--src/lem_interp/sail_impl_base.lem5
9 files changed, 58 insertions, 14 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 24f624e3..4de1e869 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -359,6 +359,7 @@ type action =
| Write_mem of id * value * maybe (nat * nat) * value
| Write_ea of id * value
| Write_memv of id * value * value
+ | Excl_res of id * value
| Barrier of id * value
| Footprint of id * value
| Nondet of list (exp tannot) * tag
@@ -2242,6 +2243,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
mk_hole_frame (Write_mem (id_of_string name_ext) v Nothing wv)
else if has_eamem_effect effects
then mk_thunk_frame (Write_ea (id_of_string name_ext) v)
+ else if has_exmem_effect effects
+ then mk_thunk_frame (Excl_res (id_of_string name_ext) v)
else if has_wmv_effect effects
then let (wv,v) =
match v with
diff --git a/src/lem_interp/interp_ast.lem b/src/lem_interp/interp_ast.lem
index 64fb14b2..6091e8b1 100644
--- a/src/lem_interp/interp_ast.lem
+++ b/src/lem_interp/interp_ast.lem
@@ -121,6 +121,7 @@ type base_effect_aux = (* effect *)
| BE_rmem (* read memory *)
| BE_wmem (* write memory *)
| BE_eamem (* signal effective address for writing memory *)
+ | BE_exmem (* determine if a store-exclusive (ARM) is going to succeed *)
| BE_wmv (* write memory, sending only value *)
| BE_barr (* memory barrier *)
| BE_depend (* dynamic footprint *)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 72bf0bcc..3e71ba37 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -430,6 +430,8 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
(Ivh_error (Interp_interface.Internal_error ("Write memory request in a " ^ errk_str)), events_out)
| (Interp.Action (Interp.Write_ea _ _) _,_,_) ->
(Ivh_error (Interp_interface.Internal_error ("Write ea request in a " ^ errk_str)), events_out)
+ | (Interp.Action (Interp.Excl_res _ _) _,_,_) ->
+ (Ivh_error (Interp_interface.Internal_error ("Exclusive result request in a " ^ errk_str)), events_out)
| (Interp.Action (Interp.Write_memv _ _ _) _,_,_) ->
(Ivh_error (Interp_interface.Internal_error ("Write memory value request in a " ^ errk_str)), events_out)
| _ -> (Ivh_error (Interp_interface.Internal_error ("Non expected action in a " ^ errk_str)), events_out)
@@ -443,19 +445,19 @@ let call_external_functions direction outcome =
| Just f -> Just (f value) end
| _ -> Nothing end
-let build_context defs reads writes write_eas write_vals barriers externs =
+let build_context defs reads writes write_eas write_vals barriers excl_res externs =
(*TODO add externs to to_top_env*)
match Interp.to_top_env call_external_functions defs with
| (_,((Interp.Env _ _ dir _ _ _ _ _) as context)) ->
Context context (if Interp.is_inc(dir) then D_increasing else D_decreasing)
- reads writes write_eas write_vals barriers externs end
+ reads writes write_eas write_vals barriers excl_res externs end
let translate_address top_level end_flag thunk_name registers address =
let (Address bytes i) = address in
let mode = make_mode true false in
let int_mode = mode.internal_mode in
- let (Context top_env direction _ _ _ _ _ _) = top_level in
+ let (Context top_env direction _ _ _ _ _ _ _) = top_level in
let intern_val = intern_mem_value mode direction (memory_value_of_address end_flag address) in
let val_str = Interp.string_of_value intern_val in
let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
@@ -499,7 +501,7 @@ let intern_instruction direction (name,parms) =
let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers instruction =
let mode = make_mode true false in
let int_mode = mode.internal_mode in
- let (Context top_env direction _ _ _ _ _ _) = top_level in
+ let (Context top_env direction _ _ _ _ _ _ _) = top_level in
let intern_val = intern_instruction direction instruction in
let val_str = Interp.string_of_value intern_val in
let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
@@ -641,7 +643,7 @@ end
let interp_value_to_instr_external top_level instr =
- let (Context (Interp.Env _ instructions _ _ _ _ _ _) _ _ _ _ _ _ _) = top_level in
+ let (Context (Interp.Env _ instructions _ _ _ _ _ _) _ _ _ _ _ _ _ _) = top_level in
match instr with
| Interp.V_ctor (Id_aux (Id i) _) _ _ parm ->
match (find_instruction i instructions) with
@@ -666,7 +668,7 @@ let interp_value_to_instr_external top_level instr =
let decode_to_instruction top_level registers value : instruction_or_decode_error =
let mode = make_interpreter_mode true false in
- let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _ _ _) = top_level in
+ let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _ _ _ _) = top_level in
let intern_val = intern_opcode direction value in
let val_str = Interp.string_of_value intern_val in
let (arg,_) = Interp.to_exp mode Interp.eenv intern_val in
@@ -703,7 +705,7 @@ end
let decode_to_istate (top_level:context) registers (value:opcode) : i_state_or_error =
- let (Context top_env _ _ _ _ _ _ _) = top_level in
+ let (Context top_env _ _ _ _ _ _ _ _) = top_level in
match decode_to_instruction top_level registers value with
| IDE_instr instr instrv ->
let mode = make_interpreter_mode true false in
@@ -718,7 +720,7 @@ let decode_to_istate (top_level:context) registers (value:opcode) : i_state_or_e
let instr_external_to_interp_value top_level instr =
- let (Context _ direction _ _ _ _ _ _) = top_level in
+ let (Context _ direction _ _ _ _ _ _ _) = top_level in
let (name,parms) = instr in
let get_value (_,typ,v) =
@@ -745,7 +747,7 @@ let instr_external_to_interp_value top_level instr =
val instruction_to_istate : context -> instruction -> instruction_state
let instruction_to_istate (top_level:context) (((name, parms) as instr):instruction) : instruction_state =
let mode = make_interpreter_mode true false in
- let (Context top_env _ _ _ _ _ _ _) = top_level in
+ let (Context top_env _ _ _ _ _ _ _ _) = top_level in
let ast_node = fst (Interp.to_exp mode Interp.eenv (instr_external_to_interp_value top_level instr)) in
(IState
(Interp.Thunk_frame
@@ -755,7 +757,7 @@ let instruction_to_istate (top_level:context) (((name, parms) as instr):instruct
top_level)
let rec interp_to_outcome mode context thunk =
- let (Context _ direction mem_reads mem_writes mem_write_eas mem_write_vals barriers spec_externs) = context in
+ let (Context _ direction mem_reads mem_writes mem_write_eas mem_write_vals barriers excl_res spec_externs) = context in
let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
match thunk () with
| (Interp.Value _,lm,le) -> (Done,lm)
@@ -813,7 +815,15 @@ let rec interp_to_outcome mode context thunk =
Write_ea write_k (Address_lifted location address_int) length tracking (IState next_state context)
else Error "Memory address for write is not 64 bits"
| _ -> Error ("Memory function " ^ i ^ " to signal impending write, not found") end, lm)
- | Interp.Write_memv (Id_aux (Id i) _) address_val write_val ->
+ | Interp.Excl_res (Id_aux (Id i) _) loc_val ->
+ (match excl_res with
+ | (Just (i', ER return)) ->
+ Excl_res (fun b ->
+ match return with
+ | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context)
+ | Just return_bool -> return_bool (IState next_state context) b end)
+ | _ -> Error ("Exclusive result function, not provided") end, lm)
+ | Interp.Write_memv (Id_aux (Id i) _) address_val write_val ->
(match List.lookup i mem_write_vals with
| (Just (MV parmf return)) ->
let (value, v_tracking) =
@@ -899,7 +909,7 @@ 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
+ let (Context _ direction externs reads writes write_eas write_vals barriers excl_res) = context in
let unknown_reg size =
<| rv_bits = (List.replicate size Bitl_unknown);
rv_start = 0;
@@ -935,6 +945,11 @@ let rec ie_loop mode register_values (IState interp_state context) =
| (Write_ea write_k loc length tracking i_state, _) ->
let (events,analysis_data) = ie_loop mode register_values i_state in
((E_write_ea write_k loc length tracking)::events,analysis_data)
+ | (Excl_res i_state_fun, _) ->
+ let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in
+ let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in
+ (*TODO: consider if lm and lm should be merged*)
+ (E_excl_res :: (events ++ events'), analysis_data)
| (Write_memv opt_address value tracking i_state_fun, _) ->
let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in
let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in
@@ -995,6 +1010,8 @@ let rec outcome_to_outcome pp_instruction_state mode =
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.Excl_res k ->
+ Sail_impl_base.Excl_res (fun v -> state_to_outcome_s mode (k v))
| 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 ->
@@ -1078,6 +1095,7 @@ 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_excl_res -> Nothing
| E_write_memv _ _ _ -> Nothing
| E_barrier bk -> Just (IK_barrier bk)
| E_footprint -> Nothing
@@ -1093,6 +1111,7 @@ let regs_in_of_event : event -> list reg_name = function
| E_read_mem _ _ _ _ -> []
| E_write_mem _ _ _ _ _ _ -> []
| E_write_ea _ _ _ _ -> []
+ | E_excl_res -> []
| E_write_memv _ _ _ -> []
| E_barrier _ -> []
| E_footprint -> []
@@ -1106,6 +1125,7 @@ let regs_out_of_event : event -> list reg_name = function
| E_read_mem _ _ _ _ -> []
| E_write_mem _ _ _ _ _ _ -> []
| E_write_ea _ _ _ _ -> []
+ | E_excl_res -> []
| E_write_memv _ _ _ -> []
| E_barrier _ -> []
| E_footprint -> []
@@ -1123,6 +1143,7 @@ let regs_feeding_memory_access_address_of_event : event -> list reg_name = funct
| E_write_mem _ _ _ None _ _ -> []
| E_write_ea wk _ _ (Just rs) -> rs
| E_write_ea wk _ _ None -> []
+ | E_excl_res -> []
| E_write_memv _ _ _ -> []
| E_barrier bk -> []
| E_footprint -> []
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 3ef6abb8..77572de9 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -185,11 +185,13 @@ type memory_write = MW of write_kind * memory_parameter_transformer * (maybe (in
and memory_writes = list (string * memory_write)
and memory_write_val = MV of optional_memory_transformer * (maybe (instruction_state -> bool -> instruction_state))
and memory_write_vals = list (string * memory_write_val)
+and excl_res_t = ER of maybe (instruction_state -> bool -> instruction_state)
+and excl_res = maybe (string * excl_res_t)
(* Definition information needed to run an instruction *)
and context =
Context of Interp.top_level * direction *
- memory_reads * memory_writes * memory_write_eas * memory_write_vals * barriers * external_functions
+ memory_reads * memory_writes * memory_write_eas * memory_write_vals * barriers * excl_res * external_functions
(* An instruction in flight *)
and instruction_state = IState of interpreter_state * context
@@ -204,6 +206,9 @@ type outcome =
| Write_mem of write_kind * address_lifted * nat * maybe (list reg_name)
* memory_value * maybe (list reg_name) * (bool -> instruction_state)
+(* Request the result of store-exclusive *)
+| Excl_res of (bool -> instruction_state)
+
(* Tell the system a write is imminent, at address lifted tainted by register list, of size nat *)
| Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * instruction_state
@@ -248,7 +253,7 @@ type outcome =
(* Functions to build up the initial state for interpretation *)
-val build_context : specification -> memory_reads -> memory_writes -> memory_write_eas -> memory_write_vals -> barriers -> external_functions -> context
+val build_context : specification -> memory_reads -> memory_writes -> memory_write_eas -> memory_write_vals -> barriers -> excl_res -> external_functions -> context
val initial_instruction_state : context -> string -> list register_value -> instruction_state
(* string is a function name, list of value are the parameters to that function *)
diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem
index 86042d61..2c338ff7 100644
--- a/src/lem_interp/interp_utilities.lem
+++ b/src/lem_interp/interp_utilities.lem
@@ -119,6 +119,7 @@ let rec has_effect which efcts =
| (BE_wmem,BE_wmem) -> true
| (BE_wmv,BE_wmv) -> true
| (BE_eamem,BE_eamem) -> true
+ | (BE_exmem,BE_exmem) -> true
| (BE_barr,BE_barr) -> true
| (BE_undef,BE_undef) -> true
| (BE_unspec,BE_unspec) -> true
@@ -131,6 +132,7 @@ let has_rmem_effect = has_effect BE_rmem
let has_barr_effect = has_effect BE_barr
let has_wmem_effect = has_effect BE_wmem
let has_eamem_effect = has_effect BE_eamem
+let has_exmem_effect = has_effect BE_exmem
let has_wmv_effect = has_effect BE_wmv
let has_depend_effect = has_effect BE_depend
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index 7d182258..855658b4 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -125,6 +125,7 @@ let doc_effect (BE_aux (e,_)) =
| BE_wmem -> "wmem"
| BE_wmv -> "wmv"
| BE_eamem -> "eamem"
+ | BE_exmem -> "exmem"
| BE_barr -> "barr"
| BE_depend -> "depend"
| BE_undef -> "undef"
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 4922a59a..01c828dd 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -434,6 +434,8 @@ let rec format_events = function
" Write_ea at " ^ (memory_value_to_string E_big_endian location) ^ ", based on registers " ^
format_tracking tracking ^ " across " ^ (string_of_int length) ^ " bytes\n" ^
(format_events events)
+ | E_excl_res::events ->
+ " Excl_res\n" ^ (format_events events)
| (E_write_memv(_, value, v_tracking))::events ->
" Write_memv of " ^ (memory_value_to_string E_big_endian value) ^ ", based on registers " ^
format_tracking v_tracking ^ "\n" ^
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 8be5354a..600699ec 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -377,6 +377,10 @@ let run
| Write_ea1(_,(Address_lifted(location,_)), size,_,next) ->
show "write_announce" (memory_value_to_string !default_endian location) left ((string_of_int size) ^ " bytes");
(step next, env, next)
+ | Excl_res1(next_thunk) ->
+ show "exclusive_result" "" "" "";
+ let next = next_thunk true in
+ (step next,env',next)
| Barrier1(bkind,next) ->
show "mem_barrier" "" "" "";
(step next, env, next)
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 02d53896..fad04a51 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -780,6 +780,7 @@ 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_excl_res
| E_write_memv of maybe address_lifted * memory_value * maybe (list reg_name)
| E_barrier of barrier_kind
| E_footprint
@@ -797,6 +798,7 @@ let eventCompare e1 e2 =
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_excl_res, E_excl_res) -> EQ
| (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
@@ -806,6 +808,7 @@ let eventCompare e1 e2 =
| (E_read_mem _ _ _ _, _) -> LT
| (E_write_mem _ _ _ _ _ _, _) -> LT
| (E_write_ea _ _ _ _, _) -> LT
+ | (E_excl_res, _) -> LT
| (E_write_memv _ _ _, _) -> LT
| (E_barrier _, _) -> LT
| (E_read_reg _, _) -> LT
@@ -839,6 +842,8 @@ type outcome 'a =
| 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 the result of store-exclusive *)
+ | Excl_res of (bool -> 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))
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-13 20:23:27 +0000