write all or part of fields out of translate_address (instead of just all)

fix bug in interp_to_value_helper

2 files changed, 13 insertions, 5 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 8e54d1cb..3a826f8e 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -321,7 +321,7 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
       match List.lookup i (Interp_lib.library_functions direction) with
         | Nothing -> (Ivh_error (Internal_error ("External function not available " ^ i)), events_out)
         | Just f  -> 
-          interp_to_value_helper arg ivh_mode err_str instr direction registers events false
+          interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen
                                  (fun _ -> Interp.resume mode stack (Just (f value)))
       end
     | (Interp.Action (Interp.Fail v) stack, _, _) ->
@@ -348,13 +348,13 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
             | Nothing -> err_value
             | Just v ->
               let value = intern_reg_value v in
-              interp_to_value_helper arg ivh_mode err_str instr direction registers events false
+              interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen
                 (fun _ -> Interp.resume mode stack (Just value)) end end)      
     | (Interp.Action (Interp.Write_reg r slice value) stack,_,_) ->
       let ext_reg = extern_reg r slice in
       let reg_value = extern_reg_value ext_reg value in
       interp_to_value_helper arg ivh_mode err_str instr direction registers ((E_write_reg ext_reg reg_value)::events)
-        false (fun _ -> Interp.resume mode stack Nothing)
+        exn_seen (fun _ -> Interp.resume mode stack Nothing)
     | (Interp.Action (Interp.Read_mem _ _ _) _,_,_) ->
       (Ivh_error (Internal_error ("Read memory request in a " ^ errk_str)), events_out)
     | (Interp.Action (Interp.Write_mem _ _ _ _) _,_,_) ->
diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml
index 579809e1..94bd2932 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -961,8 +961,16 @@ let rec write_events = function
   | [] -> ()
   | e::events ->
     (match e with
-     | E_write_reg (r,v) ->
-       reg := (Reg.add (id_of_reg_name r) v !reg)
+     | E_write_reg (Reg0(id,_,_,_), value) -> reg := Reg.add id value !reg
+     | E_write_reg ((Reg_slice(id,_,_,range) as reg_n),value) 
+     | E_write_reg ((Reg_field(id,_,_,_,range) as reg_n),value)->
+       let old_val = Reg.find id !reg in
+       let new_val = fupdate_slice reg_n old_val value range in
+       reg := Reg.add id new_val !reg
+     | E_write_reg((Reg_f_slice(id,_,_,_,range,mini_range) as reg_n),value) ->
+       let old_val = Reg.find id !reg in
+       let new_val = fupdate_slice reg_n old_val value (combine_slices range mini_range) in
+       reg := Reg.add id new_val !reg
      | _ -> failwith "Only register write events expected");
     write_events events