diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 6 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri.ml | 12 |
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 |