diff options
| -rw-r--r-- | mips/mips_prelude.sail | 10 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 23 | ||||
| -rw-r--r-- | src/lem_interp/run_interp_model.ml | 4 | ||||
| -rw-r--r-- | src/type_check.ml | 10 | ||||
| -rw-r--r-- | src/type_internal.ml | 21 |
5 files changed, 39 insertions, 29 deletions
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index bf9d8cc0..011c9c0d 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -367,11 +367,11 @@ function unit incrementCP0Count() = { (* XXX Sail does not allow reading fields here :-( *) let (bit[32])status = CP0Status in let (bit[32])cause = CP0Cause in - let (bit[8]) ims = status[15..8] in - let (bit[8]) ips = cause[15..8] in - let ie = status[0] in - let exl = status[1] in - let erl = status[2] in + let (bit[8]) ims = CP0Status.IM (*status[15..8]*) in + let (bit[8]) ips = CP0Cause.IP (*cause[15..8] *) in + let ie = CP0Status.IE in + let exl = CP0Status.EXL (*status[1]*) in + let erl = CP0Status.ERL (*status[2]*) in if ((~(exl)) & (~(erl)) & ie & ((ips & ims) != 0x00)) then exit (SignalException(Int)); } diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index d7a86b7e..a2988ee5 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -236,13 +236,15 @@ let rec extern_ifield_value i_name field_name v ftyp = match (v,ftyp) with ^ " given non-externable " ^ (Interp.string_of_value v) ^ " ftyp is " ^ show ftyp) end -let rec slice_reg_value v start stop = +let rec slice_reg_value v start stop = +(* let _ = Interp.debug_print ("slice_reg_value " ^ show v.rv_start_internal ^ " " ^ show v.rv_start ^ " " ^ show start ^ " " ^ show stop) in*) let inc = v.rv_dir = D_increasing in let r_internal_start = if inc then start else (stop - start) + 1 in let r_start = if inc then r_internal_start else start in - <| v with rv_bits = (Interp.from_n_to_n +(* let _ = Interp.debug_print (" " ^ " " ^ if inc then "Inc " else "dec " ^ show (List.length (Interp.from_n_to_n (if inc then (start - v.rv_start_internal) else (v.rv_start_internal - start)) - (if inc then (stop - v.rv_start_internal) else (v.rv_start_internal - stop)) v.rv_bits); + (if inc then (stop - v.rv_start_internal) else (v.rv_start_internal - stop)) v.rv_bits)) ^ " " ^ show (List.length v.rv_bits) ^ " " ^ show (v.rv_start_internal - start) ^ " " ^ show (v.rv_start_internal - stop) ^ "\n") in*) + <| v with rv_bits = (Interp.from_n_to_n (start - v.rv_start) (stop - v.rv_start) v.rv_bits); rv_start = r_start; rv_start_internal = r_internal_start |> @@ -257,11 +259,12 @@ 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 (lift_reg_name_to_whole reg_name 0) - (if start = stop then - (Interp.fupdate_vec v_internal start v2_internal) - else - (Interp.fupdate_vector_slice v_internal v2_internal start stop)) + <| (extern_reg_value (lift_reg_name_to_whole reg_name 0) + (if start = stop then + (Interp.fupdate_vec v_internal start v2_internal) + else + (Interp.fupdate_vector_slice v_internal v2_internal start stop))) + with rv_start = v.rv_start; rv_start_internal = v.rv_start_internal |> (*TODO: Only find some sub piece matches, need to look for field/slice sub pieces*) (*TODO immediate: this will be impacted by need to change slicing *) @@ -273,7 +276,8 @@ let rec find_reg_name reg = function if i = n && size = size2 then (Just v) else find_reg_name reg registers | (Reg_slice i _ _ (p1,p2), Reg n _ _ _) -> if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers - | (Reg_field i _ _ f (p1,p2), Reg n _ _ _) -> + | (Reg_field i _ _ f (p1,p2), Reg n _ _ _) -> +(* let _ = Interp.debug_print ("find_reg_name " ^ i ^ " field case " ^ show p1 ^ " " ^ show p2 ^ "\n") in*) if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers | (Reg_slice i _ _ (p1,p2), Reg_slice n _ _ (p3,p4)) -> if i=n @@ -360,6 +364,7 @@ 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 +(* let _ = Interp.debug_print ("Register read of " ^ rname ^ " returning value " ^ (Interp.string_of_value value) ^ "\n") in *) 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,_,_) -> diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml index 9df5cdc3..034fd991 100644 --- a/src/lem_interp/run_interp_model.ml +++ b/src/lem_interp/run_interp_model.ml @@ -61,8 +61,8 @@ let slice register_vector (start,stop) = 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 - 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 +(* let _ = Printf.eprintf "slice decreasing with %i, %i, %i\n" startd stopd register_vector.rv_start in*) + slice_reg_value register_vector start stop let big_num_unit = of_int 1 diff --git a/src/type_check.ml b/src/type_check.ml index 27b705d8..277b5790 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2057,19 +2057,19 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))), Env(d_env,orig_env (*Envmap.insert t_env (id,tannot)*),b_env,tp_env) | _ , _-> - (*let _ = Printf.eprintf "checking %s, not in env\n%!" id in*) + let _ = Printf.eprintf "checking %s, not in env\n%!" id in let t_env = if is_rec then Envmap.insert t_env (id,tannot) else t_env in let funcls,cs_ef = check t_env t_param_env None in let cses,ef = ((fun (cses,efses) -> (cses,(List.fold_right union_effects efses pure_e))) (List.split cs_ef)) in let cs = if List.length funcls = 1 then cses else [BranchCons(Fun l, None, cses)] in - (*let _ = Printf.eprintf "unresolved constraints are %s\n%!" (constraints_to_string cs) in*) + let _ = Printf.eprintf "unresolved constraints are %s\n%!" (constraints_to_string cs) in let (cs',map) = resolve_constraints cs in - (*let _ = Printf.eprintf "checking tannot for %s 2 remaining constraints are %s\n" - id (constraints_to_string cs') in*) + let _ = Printf.eprintf "checking tannot for %s 2 remaining constraints are %s\n" + id (constraints_to_string cs') in let tannot = check_tannot l (match map with | None -> tannot | Some m -> add_map_tannot m tannot) None cs' ef in - (*let _ = Printf.eprintf "done funcheck case2\n" in*) + let _ = Printf.eprintf "done funcheck case2\n" in (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))), Env(d_env,(if is_rec then t_env else Envmap.insert t_env (id,tannot)),b_env,tp_env) diff --git a/src/type_internal.ml b/src/type_internal.ml index c2f01d3a..eb5e7898 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1248,7 +1248,7 @@ let rec nexp_gt_compare eq_ok n1 n2 = match n1.nexp,n2.nexp with | Nconst i, Nconst j | N2n(_,Some i), N2n(_,Some j)-> if ge_test i j then Yes else No | Npos_inf, _ | _, Nneg_inf -> Yes - | Nuvar _, Npos_inf | Nneg_inf, Nuvar _ -> Maybe + | Nuvar _, Npos_inf | Nneg_inf, Nuvar _ -> if eq_ok then Maybe else No | Nneg_inf, _ | _, Npos_inf -> No | Ninexact, _ | _, Ninexact -> Maybe | N2n(n1,_), N2n(n2,_) -> nexp_gt_compare eq_ok n1 n2 @@ -3833,17 +3833,17 @@ let rec simple_constraint_check in_env cs = ("Type constraint mismatch: constraint of " ^ n_to_string n1 ^ " >= " ^ n_to_string n2 ^ " arising from here requires " ^ string_of_big_int i1 ^ " to be greater than or equal to " ^ string_of_big_int i2) - | Npos_inf, _ | _, Nneg_inf -> check cs - | Ninexact, _ | _, Ninexact -> check cs + | Npos_inf, Nconst _ | Nconst _, Nneg_inf -> check cs | Nconst _ ,Npos_inf -> eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires " ^ (n_to_string n1') ^ " to be greater than or equal to infinity") - | Nneg_inf,Nuvar _ -> +(* | Nneg_inf,Nuvar _ -> if equate_n n2' n1' then check cs else (GtEq(co,enforce,n1',n2')::check cs) | Nneg_inf, _ -> eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires negative infinity to be >= to " - ^ (n_to_string n2')) + ^ (n_to_string n2')) *) + | Nuvar _, _ | _, Nuvar _ -> GtEq(co,enforce, n1, n2)::(check cs) | _,_ -> (match nexp_ge n1' n2' with | Yes -> check cs @@ -3891,7 +3891,8 @@ let rec simple_constraint_check in_env cs = then check cs else eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires " ^ string_of_big_int i1 ^ " to be less than or equal to " ^ string_of_big_int i2) - | _, Npos_inf | Nneg_inf, _ -> check cs +(* | _, Npos_inf | Nneg_inf, _ -> check cs*) + | Nuvar _, _ | _, Nuvar _ -> LtEq(co,enforce, n1, n2)::(check cs) | _,_ -> (match nexp_ge n2' n1' with | Yes -> check cs @@ -4017,8 +4018,9 @@ let check_range_consistent require_lt require_gt guarantee_lt guarantee_gt = | None,None,None,None | Some _, None, None, None | None, Some _ , None, None | None, None, Some _ , None | None, None, None, Some _ | Some _, Some _,None,None | None,None,Some _,Some _ (*earlier check should ensure these*) - -> () + -> let _ = Printf.eprintf "check_range_consistent in nil case\n" in () | Some(crlt,rlt), Some(crgt,rgt), Some(cglt,glt), Some(cggt,ggt) -> + let _ = Printf.eprintf "check_range_consistent is in the checking case\n" in if tri_to_bl (nexp_ge rlt glt) (*Can we guarantee the up is less than the required up*) then if tri_to_bl (nexp_ge rlt ggt) (*Can we guarantee the lw is less than the required up*) then if tri_to_bl (nexp_ge glt rgt) (*Can we guarantee the up is greater than the required lw*) @@ -4028,9 +4030,12 @@ let check_range_consistent require_lt require_gt guarantee_lt guarantee_gt = else assert false else assert false else assert false - | _ -> assert false + | _ -> + let _ = Printf.eprintf "check_range_consistent is in the partial case\n" in + assert false let check_ranges cs = + let _ = Printf.eprintf "In check_ranges with %i constraints\n" (constraint_size cs) in let nuvars = get_all_nuvars_cs cs in let nus_with_cs = List.map (fun n -> (n,contains_nuvar n cs)) (Var_set.elements nuvars) in let nus_with_iso_cs = List.map (fun (n,ncs) -> (n,isolate_constraint n ncs)) nus_with_cs in |