diff options
| -rw-r--r-- | src/lem_interp/interp.lem | 22 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 4 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 2 | ||||
| -rw-r--r-- | src/lem_interp/run_interp_model.ml | 23 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf.ml | 2 |
5 files changed, 40 insertions, 13 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 1e30a0dc..3e9fa6dc 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -2271,8 +2271,20 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( | Just v -> if is_top_level then ((Error l "Writes must be to reg or registers",l_mem,l_env),Nothing) else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env))) - | Nothing -> ((Error l ("Undefined id " ^ (get_id id)),l_mem,l_env),Nothing) - end) + | Nothing -> + let regf = + match in_env regs name with (*pull the regform with the most specific type annotation from env *) + | Just(V_register regform) -> regform + | _ -> Assert_extra.failwith "Register not known in regenv" end in + let start_pos = reg_start_pos regf in + let reg_size = reg_size regf in + let request = + (Action (Write_reg regf Nothing + (if is_top_level then (update_vector_start default_dir start_pos reg_size value) else value)) + (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top), + l_mem,l_env) in + if is_top_level then (request,Nothing) + else (request,Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env))) end) | Tag_extern _ -> let regf = match in_env regs name with (*pull the regform with the most specific type annotation from env *) @@ -2468,7 +2480,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value, (add_to_env (id,(V_boxref c typ)) l_env)),Nothing) end - else ((Error l ("Undefined id " ^ (get_id id)),l_mem,l_env),Nothing) + else ((Error l ("LEXP:cast1: Undefined id " ^ (get_id id)),l_mem,l_env),Nothing) | v -> if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing) else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env))) @@ -2489,7 +2501,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value, (add_to_env (id,(V_boxref c typ)) l_env)),Nothing) end - else ((Error l ("Undefined id " ^ (get_id id)),l_mem,l_env),Nothing) + else ((Error l ("LEXP:cast2: Undefined id " ^ (get_id id)),l_mem,l_env),Nothing) | v -> if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing) else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env))) @@ -2510,7 +2522,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( ((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value, (add_to_env (id,(V_boxref c typ)) l_env)),Nothing) end - else ((Error l ("Undefined id " ^ (get_id id)),l_mem,l_env),Nothing) + else ((Error l ("LEXP:cast3: Undefined id " ^ (get_id id)),l_mem,l_env),Nothing) | v -> if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing) else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env))) diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index e9161382..8f9bc422 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -231,6 +231,10 @@ let rec slice_reg_value v start stop = (if inc then (stop - v.rv_start) else (v.rv_start - stop)) v.rv_bits); rv_start = (if inc then start else ((stop - start) + 1)) |> +let update_reg_value_slice reg_name v start stop v2 = + let v_internal = intern_reg_value v in + let v2_internal = intern_reg_value v2 in + extern_reg_value reg_name (Interp.fupdate_vector_slice v_internal v2_internal start stop) let initial_instruction_state top_level main args = let e_args = match args with diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index ae64f96c..ad60699e 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -885,6 +885,8 @@ val instruction_to_istate : context -> instruction -> instruction_state (*i_stat (* Slice a register value into a smaller vector, starting at first number (wrt the indices of the register value, not raw positions in its list of bits) and going to second (inclusive) according to order. *) val slice_reg_value : register_value -> nat -> nat -> register_value +(*Create a new register value where the contents of nat to nat are replaced by the second register_value *) +val update_reg_value_slice : reg_name -> register_value -> nat -> nat -> register_value -> register_value (* Big step of the interpreter, to the next request for an external action *) diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml index ff5dea0b..f1310240 100644 --- a/src/lem_interp/run_interp_model.ml +++ b/src/lem_interp/run_interp_model.ml @@ -61,7 +61,7 @@ let slice register_vector (start,stop) = (*Interface turns start and stop into forms for increasing because ppcmem only speaks increasing, so here we turn it back *) let startd = register_vector.rv_start_internal- start in - let stopd = startd - stop in + let stopd = startd - (stop - start) in (*let _ = Printf.eprintf "slice decreasing with %i, %i, %i\n" startd stopd register_vector.rv_start in*) slice_reg_value {register_vector with rv_start=register_vector.rv_start_internal} startd stopd @@ -90,7 +90,16 @@ let rec list_update_list index start stop es vals = then e :: (list_update_list (Nat_big_num.add index big_num_unit) start stop es xs) else x :: (list_update_list (Nat_big_num.add index big_num_unit) start stop (e::es) xs) -let fupdate_slice original e (start,stop) = assert false +let fupdate_slice reg_name original e (start,stop) = + if original.rv_dir = D_increasing + then update_reg_value_slice reg_name original start stop e + else + (*Interface turns start and stop into forms for + increasing because ppcmem only speaks increasing, so here we turn it back *) + let startd = original.rv_start_internal- start in + let stopd = startd - (stop - start) in + (*let _ = Printf.eprintf "fupdate_slice: starts at %i, %i -> %i,%i -> %i\n" original.rv_start_internal start startd stop stopd in*) + update_reg_value_slice reg_name {original with rv_start=original.rv_start_internal} startd stopd e let combine_slices (start, stop) (inner_start,inner_stop) = (start + inner_start, start + inner_stop) @@ -105,14 +114,14 @@ let rec perform_action ((reg, mem) as env) = function | Read_reg0(Reg_f_slice(id, _,_,_, range, mini_range), _) -> (Some(slice (slice (Reg.find id reg) range) mini_range),env) | Write_reg0(Reg0(id,_,_,_), value, _) -> (None, (Reg.add id value reg,mem)) - | Write_reg0(Reg_slice(id,_,_,range),value, _) - | Write_reg0(Reg_field(id,_,_,_,range),value,_)-> + | Write_reg0((Reg_slice(id,_,_,range) as reg_n),value, _) + | Write_reg0((Reg_field(id,_,_,_,range) as reg_n),value,_)-> let old_val = Reg.find id reg in - let new_val = fupdate_slice old_val value range in + let new_val = fupdate_slice reg_n old_val value range in (None, (Reg.add id new_val reg, mem)) - | Write_reg0(Reg_f_slice(id,_,_,_,range,mini_range),value,_) -> + | Write_reg0((Reg_f_slice(id,_,_,_,range,mini_range) as reg_n),value,_) -> let old_val = Reg.find id reg in - let new_val = fupdate_slice old_val value (combine_slices range mini_range) in + let new_val = fupdate_slice reg_n old_val value (combine_slices range mini_range) in (None,(Reg.add id new_val reg,mem)) | Read_mem0(_,location, length, _,_) -> let address = match address_of_address_lifted location with diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml index bad09b6d..d32e2e3d 100644 --- a/src/lem_interp/run_with_elf.ml +++ b/src/lem_interp/run_with_elf.ml @@ -488,7 +488,7 @@ let mips_register_data_all = [ ("LO", (D_decreasing, 64, 0)); (* control registers *) ("CP0Status", (D_decreasing, 32, 0)); - ("CP0Cause", (D_decreasing, 32, 0)); + ("CP0Cause", (D_decreasing, 32, 31)); ("CP0EPC", (D_decreasing, 64, 0)); ] |