Support new write memory events

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)