Add optional address to memv events

4 files changed, 31 insertions, 17 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index bf2feedf..23d5c021 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -262,7 +262,7 @@ type action =
  | 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
+ | Write_memv of id * value * value
  | Barrier of id * value
  | Footprint of id * value
  | Nondet of list (exp tannot) * tag
@@ -2125,7 +2125,14 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
           else if has_eamem_effect effects
           then mk_thunk_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)
+          then let (wv,v) =
+                 match v with
+                 | V_tuple [p;v] -> (v,p)
+                 | V_tuple params_list ->
+                   let reved= List.reverse params_list in
+                   (List_extra.head reved,V_tuple (List.reverse (List_extra.tail reved)))
+                 | _ -> (v,unitv) end in
+               mk_hole_frame (Write_memv (id_of_string name_ext) v wv)
           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)
@@ -2258,7 +2265,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
+                  | (Action (Write_memv _ _ _) stack) -> a
                   | _ -> update_stack a (add_to_top_frame 
                                            (fun e env -> 
                                              let (ev,env') = (to_exp mode env v) in
@@ -2529,7 +2536,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level
            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 if has_wmv_effect effects then (Write_memv id v 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),
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index e400ecec..8b81b83f 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -384,7 +384,7 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
       (Ivh_error (Internal_error ("Write memory request in a " ^ errk_str)), events_out)
     | (Interp.Action (Interp.Write_ea _ _) _,_,_) ->
       (Ivh_error (Internal_error ("Write ea request in a " ^ errk_str)), events_out)
-    | (Interp.Action (Interp.Write_memv _ _) _,_,_) ->
+    | (Interp.Action (Interp.Write_memv _ _ _) _,_,_) ->
       (Ivh_error (Internal_error ("Write memory value request in a " ^ errk_str)), events_out)
     | _ -> (Ivh_error (Internal_error ("Non expected action in a " ^ errk_str)), events_out)
 end
@@ -731,14 +731,20 @@ 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) _) write_val ->
+        | Interp.Write_memv (Id_aux (Id i) _) address_val write_val ->
           (match List.lookup i mem_write_vals with
-            | (Just (MV return)) -> 
+            | (Just (MV parmf return)) -> 
               let (value, v_tracking) = 
                 match (Interp.detaint write_val) with
                   | Interp.V_tuple[_;v] -> (extern_mem_value mode (Interp.retaint write_val v))
                   | _ -> (extern_mem_value mode write_val) end in
-              Write_memv value v_tracking 
+               let location_opt = match parmf mode address_val with
+                  | Nothing -> Nothing
+                  | Just mv -> let address_int = match (maybe_all (List.map byte_of_byte_lifted mv)) with
+                      | Just bs -> Just (integer_of_byte_list bs)
+                      | _ -> Nothing end in Just (Address_lifted mv address_int) end
+               in
+               Write_memv location_opt value v_tracking 
                 (fun b -> 
                   match return with
                     | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context)
@@ -844,11 +850,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)
-    | (Write_memv value tracking i_state_fun, _) ->
+    | (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
       (*TODO: consider if lm and lm should be merged*)
-      ((E_write_memv value tracking)::(events++events'),analysis_data)
+      ((E_write_memv opt_address value tracking)::(events++events'),analysis_data)
     | (Barrier barrier_k i_state, _) ->
       let (events,analysis_data) = ie_loop mode register_values i_state in
       ((E_barrier barrier_k)::events,analysis_data)
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index bbff6a66..0f9dff80 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -482,13 +482,14 @@ type external_functions = list (string * (Interp.value -> Interp.value))
 (*Maps between the memory functions as preceived from a Sail spec and the values needed for actions in the memory model*)
 type barriers = list (string * barrier_kind)
 type memory_parameter_transformer = interp_mode -> Interp.value -> (memory_value * nat * maybe (list reg_name))
+type optional_memory_transformer = interp_mode -> Interp.value -> maybe memory_value
 type memory_read = MR of read_kind * memory_parameter_transformer
 type memory_reads  = list (string * memory_read)
 type memory_write_ea = MEA of write_kind * memory_parameter_transformer
 type memory_write_eas = list (string * memory_write_ea)
 type memory_write = MW of write_kind * memory_parameter_transformer * (maybe (instruction_state -> bool -> instruction_state))
 and memory_writes = list (string * memory_write)
-and memory_write_val = MV of maybe (instruction_state -> bool -> instruction_state)
+and memory_write_val = MV of optional_memory_transformer * (maybe (instruction_state -> bool -> instruction_state))
 and memory_write_vals = list (string * memory_write_val)
 
 (* Definition information needed to run an instruction *)
@@ -509,7 +510,7 @@ type outcome =
 (* Tell the system a write is imminent, at address lifted tanted by register list, of size nat *)
 | Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * instruction_state
 (* Request to write memory at last signaled address. Memory value should be 8* the size given in ea signal *)
-| Write_memv of memory_value * maybe (list reg_name) * (bool -> instruction_state)
+| Write_memv of maybe address_lifted * memory_value * maybe (list reg_name) * (bool -> instruction_state)
 (* Request a memory barrier *)
 | Barrier of barrier_kind * instruction_state
 (* Tell the system to dynamically recalculate dependency footprint *)
@@ -539,7 +540,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_write_memv of memory_value * 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
@@ -827,7 +828,7 @@ let ~{ocaml} 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_write_memv mv1 tr1, E_write_memv mv2 tr2) -> compare (mv1,tr1) (mv2,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)
@@ -836,7 +837,7 @@ let ~{ocaml} eventCompare e1 e2 =
   | (E_read_mem _ _ _ _, _) -> LT
   | (E_write_mem _ _ _ _ _ _, _) -> LT
   | (E_write_ea _ _ _ _, _) -> LT
-  | (E_write_memv _ _, _) -> LT
+  | (E_write_memv _ _ _, _) -> LT
   | (E_barrier _, _) -> LT
   | (E_read_reg _, _) -> LT
   | (E_write_reg _ _, _) -> LT
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index ad423fd9..a1c49796 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -385,8 +385,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_write_memv(value, v_tracking))::events ->
-    "     Write_ea of " ^ (memory_value_to_string E_big_endian value) ^ ", based on registers " ^
+  | (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" ^
       (format_events events)
   | ((E_barrier b_kind)::events) ->