diff options
| author | Kathy Gray | 2016-09-13 14:07:09 +0100 |
|---|---|---|
| committer | Kathy Gray | 2016-09-13 14:07:17 +0100 |
| commit | e354b3dfac6ce4bd2dda99edc3fa2c91ed4c5b88 (patch) | |
| tree | c28cf94d42ee04f92dd214bf068f3ae2cbfae412 /src/lem_interp/interp.lem | |
| parent | b4323d7b1ac849d555ea699503bd67510142f8c3 (diff) | |
Add optional address to memv events
Diffstat (limited to 'src/lem_interp/interp.lem')
| -rw-r--r-- | src/lem_interp/interp.lem | 15 |
1 files changed, 11 insertions, 4 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), |