diff options
| -rw-r--r-- | src/lem_interp/interp.lem | 58 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 25 | ||||
| -rw-r--r-- | src/lem_interp/interp_utilities.lem | 16 | ||||
| -rw-r--r-- | src/lem_interp/printing_functions.ml | 8 |
4 files changed, 75 insertions, 32 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index e0473707..10d93c30 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -218,6 +218,8 @@ type action = | Write_reg of reg_form * maybe (nat * nat) * value | Read_mem of id * value * maybe (nat * nat) | Write_mem of id * value * maybe (nat * nat) * value + | Write_ea of id * value + | Write_memv of id * value | Barrier of id * value | Footprint of id * value | Write_next_IA of value (* Perhaps not needed? *) @@ -1875,33 +1877,31 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = | Tag_extern opt_name -> let effects = (match effect with | Effect_aux(Effect_set es) _ -> es | _ -> [] end) in let name_ext = match opt_name with | Just s -> s | Nothing -> name end in - if has_rmem_effect effects - then - (Action (Read_mem (id_of_string name_ext) v Nothing) + let mk_hole_frame act = + (Action act (Hole_frame (Id_aux (Id "0") l) - (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) t_level le lm Top), lm, le) + (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) t_level le lm Top), lm, le) in + let mk_thunk_frame act = + (Action act + (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level le lm Top), lm, le) in + if has_rmem_effect effects + then mk_hole_frame (Read_mem (id_of_string name_ext) v Nothing) else if has_barr_effect effects - then - (Action (Barrier (id_of_string name_ext) v) - (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level le lm Top), lm, le) + then mk_thunk_frame (Barrier (id_of_string name_ext) v) else if has_depend_effect effects - then - (Action (Footprint (id_of_string name_ext) v) - (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level le lm Top), lm, le) + then mk_thunk_frame (Footprint (id_of_string name_ext) v) else if has_wmem_effect effects - then - let (wv,v) = - match v with - | V_tuple params_list -> - let reved = List.reverse params_list in - (List_extra.head reved,V_tuple (List.reverse (List_extra.tail reved))) end in - (Action (Write_mem (id_of_string name_ext) v Nothing wv) - (Hole_frame (Id_aux (Id "0") l) - (E_aux (E_id (Id_aux (Id "0") l)) (l, intern_annot annot)) t_level le lm Top),lm,le) - else - (Action (Call_extern name_ext v) - (Hole_frame (Id_aux (Id "0") l) - (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) t_level le lm Top), lm, le) + then let (wv,v) = + match v with + | V_tuple params_list -> + let reved = List.reverse params_list in + (List_extra.head reved,V_tuple (List.reverse (List_extra.tail reved))) end in + mk_hole_frame (Write_mem (id_of_string name_ext) v Nothing wv) + else if has_eamem_effect effects + then mk_hole_frame (Write_ea (id_of_string name_ext) v) + else if has_wmv_effect effects + then mk_hole_frame (Write_memv (id_of_string name_ext) v) + else mk_hole_frame (Call_extern name_ext v) | _ -> (Error l (String.stringAppend "Tag not empty, spec, ctor, or extern on function call " name),lm,le) end) | out -> out end) @@ -2004,6 +2004,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (match a with | (Action (Write_reg regf range value) stack) -> a | (Action (Write_mem id a_ range value) stack) -> a + | (Action (Write_memv _ _) stack) -> a | _ -> update_stack a (add_to_top_frame (fun e env -> let (ev,env') = (to_exp mode env v) in @@ -2174,9 +2175,14 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( | (Value v,lm,le) -> (match tag with | Tag_extern _ -> - let request = (Action (Write_mem id v Nothing value) - (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env lm Top), - lm,l_env) in + let request = + let effects = (match ef with | Effect_aux(Effect_set es) _ -> es | _ -> [] end) in + let act = if has_wmem_effect effects then (Write_mem id v Nothing value) + else if has_wmv_effect effects then (Write_memv id value) + else Assert_extra.failwith "LEXP_memory with neither wmem or wmv event" in + (Action act + (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env lm Top), + lm,l_env) in if is_top_level then (request,Nothing) else (request, diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 91fc4141..92e5402c 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -467,6 +467,27 @@ let rec interp_to_outcome mode context thunk = else Error "Memory address on write is not 64 bits" | _ -> Error ("Memory " ^ i ^ " function with write kind not found") end + | Interp.Write_ea (Id_aux (Id i) _) loc_val -> + match List.lookup i mem_write_eas with + | (Just (MEA write_k f)) -> + let (location, length, tracking) = (f mode loc_val) in + if (List.length location) = 8 + then let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with + | Just bs -> Just (integer_of_byte_list bs) + | _ -> Nothing end in + 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 " ^ i ^ " function to signal impending write, not found") end + | Interp.Write_memv (Id_aux (Id i) _) write_val -> + match List.lookup i mem_write_vals with + | (Just (MV return)) -> + let (value, v_tracking) = (extern_mem_value mode write_val) in + Write_memv value v_tracking + (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 ("Memory " ^ i ^ " function with write value kind not found") end | Interp.Barrier (Id_aux (Id i) _) lval -> match List.lookup i barriers with | Just barrier -> @@ -562,6 +583,10 @@ let rec ie_loop mode register_values (IState interp_state context) = (ie_loop mode register_values (i_state_fun (unknown_mem length))) | Write_mem write_k loc length tracking value v_tracking i_state_fun -> (E_write_mem write_k loc length tracking value v_tracking)::(ie_loop mode register_values (i_state_fun true)) + | Write_ea write_k loc length tracking i_state -> + (E_write_ea write_k loc length tracking)::(ie_loop mode register_values i_state) + | Write_memv value tracking i_state_fun -> + (E_write_memv value tracking)::(ie_loop mode register_values (i_state_fun true)) | Barrier barrier_k i_state -> (E_barrier barrier_k)::(ie_loop mode register_values i_state) | Footprint i_state -> diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem index e80a2323..b808208b 100644 --- a/src/lem_interp/interp_utilities.lem +++ b/src/lem_interp/interp_utilities.lem @@ -66,12 +66,14 @@ let rec has_effect which efcts = | [] -> false | (BE_aux e _)::efcts -> match (which,e) with - | (BE_rreg,BE_rreg) -> true - | (BE_wreg,BE_wreg) -> true - | (BE_rmem,BE_rmem) -> true - | (BE_wmem,BE_wmem) -> true - | (BE_barr,BE_barr) -> true - | (BE_undef,BE_undef) -> true + | (BE_rreg,BE_rreg) -> true + | (BE_wreg,BE_wreg) -> true + | (BE_rmem,BE_rmem) -> true + | (BE_wmem,BE_wmem) -> true + | (BE_wmv,BE_wmv) -> true + | (BE_eamem,BE_eamem) -> true + | (BE_barr,BE_barr) -> true + | (BE_undef,BE_undef) -> true | (BE_unspec,BE_unspec) -> true | (BE_nondet,BE_nondet) -> true | (BE_depend,BE_depend) -> true @@ -81,6 +83,8 @@ let rec has_effect which efcts = 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_wmv_effect = has_effect BE_wmv let has_depend_effect = has_effect BE_depend let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml index e275af83..e8104c7b 100644 --- a/src/lem_interp/printing_functions.ml +++ b/src/lem_interp/printing_functions.ml @@ -371,6 +371,14 @@ let rec format_events = function format_tracking tracking ^ ", writing " ^ (memory_value_to_string E_big_endian value) ^ ", based on " ^ format_tracking v_tracking ^ " across " ^ (string_of_int length) ^ " bytes\n" ^ (format_events events) + | (E_write_ea(write_kind,(Address_lifted (location,_)), length, tracking))::events -> + " 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_write_memv(value, v_tracking))::events -> + " Write_ea of " ^ (memory_value_to_string E_big_endian value) ^ ", based on registers " ^ + format_tracking v_tracking ^ "\n" ^ + (format_events events) | ((E_barrier b_kind)::events) -> " Memory_barrier occurred\n" ^ (format_events events) |