diff options
| -rw-r--r-- | src/lem_interp/interp.lem | 11 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 9 | ||||
| -rw-r--r-- | src/lem_interp/printing_functions.ml | 2 | ||||
| -rw-r--r-- | src/lem_interp/run_interp_model.ml | 4 | ||||
| -rw-r--r-- | src/type_check.ml | 13 |
5 files changed, 22 insertions, 17 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 0abc6220..92fa4ec0 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -583,7 +583,6 @@ let access_vector v n = | V_lit (L_aux L_zero _) -> v | V_lit (L_aux L_one _ ) -> v | V_vector m dir vs -> - (*let _ = debug_print ("access_vector given " ^ string_of_value v ^ " where dir was " ^ (if is_inc(dir) then "increasing" else "decreaseing") ^ " and start is " ^ show m ^ " and index is " ^ show n ^ "\n") in*) list_nth vs (if is_inc(dir) then (n - m) else (m - n)) | V_vector_sparse _ _ _ vs d -> match (List.lookup n vs) with @@ -702,7 +701,7 @@ val fupdate_vector_slice : value -> value -> nat -> nat -> value let fupdate_vector_slice vec replace start stop = let fupdate_vec_help vec replace = (match (vec,replace) with - | (V_vector m dir vals,V_vector _ dir' reps) -> + | (V_vector m dir vals,V_vector r_m dir' reps) -> V_vector m dir (replace_is vals (if dir=dir' then reps else (List.reverse reps)) @@ -761,7 +760,7 @@ let update_vector_slice track vector value start stop mem = ^ " and " ^ string_of_value value) end -let update_vector_start default_dir new_start expected_size v = +let update_vector_start default_dir new_start expected_size v = retaint v (match detaint v with | V_lit (L_aux L_zero _) -> V_vector new_start default_dir [v] @@ -1908,13 +1907,11 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (interp_main mode t_level l_env lm e2) (fun v2 lm le -> let append v1 v2 = (match (v1,v2) with - | (V_vector m dir vals1, V_vector _ _ vals2) -> + | (V_vector _ dir vals1, V_vector _ _ vals2) -> let vals = vals1++vals2 in let len = List.length vals in if is_inc(dir) - then V_vector m dir vals - else if m > len - then V_vector m dir vals + then V_vector 0 dir vals else V_vector (len-1) dir vals | (V_vector m dir vals1, V_vector_sparse _ len _ vals2 d) -> let original_len = List.length vals1 in diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 914cc6a5..d7a86b7e 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -247,10 +247,17 @@ let rec slice_reg_value v start stop = rv_start_internal = r_internal_start |> +let lift_reg_name_to_whole reg_name size = match reg_name with + | Reg _ _ _ _ -> reg_name + | Reg_slice name start dir _ -> Reg name start size dir + | Reg_field name start dir _ _ -> Reg name start size dir + | Reg_f_slice name start dir _ _ _ -> Reg name start size dir +end + 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 + extern_reg_value (lift_reg_name_to_whole reg_name 0) (if start = stop then (Interp.fupdate_vec v_internal start v2_internal) else diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml index 7cef082e..ad423fd9 100644 --- a/src/lem_interp/printing_functions.ml +++ b/src/lem_interp/printing_functions.ml @@ -155,7 +155,7 @@ let bit_lifteds_to_string (bls: bit_lifted list) (show_length_and_start:bool) (s let register_value_to_string rv = - bit_lifteds_to_string rv.rv_bits true (Some rv.rv_start) false + bit_lifteds_to_string rv.rv_bits true (Some rv.rv_start_internal) false let memory_value_to_string endian mv = let bls = List.concat(List.map (fun (Byte_lifted bs) -> bs) (if endian = E_big_endian then mv else (List.rev mv))) in diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml index 9abf0442..9df5cdc3 100644 --- a/src/lem_interp/run_interp_model.ml +++ b/src/lem_interp/run_interp_model.ml @@ -97,8 +97,8 @@ let fupdate_slice reg_name original e (start,stop) = 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 _ = 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 startd stopd e let combine_slices (start, stop) (inner_start,inner_stop) = (start + inner_start, start + inner_stop) diff --git a/src/type_check.ml b/src/type_check.ml index 4642a5a6..27b705d8 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1154,15 +1154,16 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux( check_exp envs imp_param true {t=Tapp("vector",[TA_nexp base1;TA_nexp rise1;TA_ord ord;TA_typ item_t])} v1 in let (v2',t2',_,cs_2,_,ef_2) = check_exp envs imp_param true {t=Tapp("vector",[TA_nexp base2;TA_nexp rise2;TA_ord ord;TA_typ item_t])} v2 in - let ti = {t=Tapp("vector",[TA_nexp base1;TA_nexp (mk_add rise1 rise2);TA_ord ord; TA_typ item_t])} in - let cs_loc = match ord.order with - | Odec -> [] (* (*This should probably be handled by casts*)[GtEq((Expr l),Require,base1,mk_add rise1 rise2)] *) - | _ -> [] in + let result_rise = mk_add rise1 rise2 in + let result_base = match ord.order with + | Odec -> mk_sub result_rise n_one + | _ -> n_zero in + let ti = {t=Tapp("vector",[TA_nexp result_base;TA_nexp result_rise;TA_ord ord; TA_typ item_t])} in let sub_effects = union_effects ef_1 ef_2 in let (t,cs_c,ef_c,e') = type_coerce (Expr l) d_env Require false true b_env ti - (E_aux(E_vector_append(v1',v2'),(l,constrained_annot_efr ti cs_loc sub_effects))) expect_t in - (e',t,t_env,cs_loc@cs_1@cs_2,nob,(union_effects ef_c sub_effects)) + (E_aux(E_vector_append(v1',v2'),(l,simple_annot_efr ti sub_effects))) expect_t in + (e',t,t_env,cs_1@cs_2,nob,(union_effects ef_c sub_effects)) | E_list(es) -> let item_t = match expect_t.t with | Tapp("list",[TA_typ i]) -> i |