summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--aarch64/Makefile10
-rw-r--r--aarch64/no_vector/spec.sail20
-rw-r--r--src/c_backend.ml6
-rw-r--r--src/constraint.ml30
-rw-r--r--src/isail.ml2
-rw-r--r--src/monomorphise.ml103
-rw-r--r--src/pretty_print_coq.ml6
-rw-r--r--src/pretty_print_lem.ml2
-rw-r--r--src/rewrites.ml6
-rw-r--r--src/type_check.ml48
-rw-r--r--src/type_check.mli2
-rw-r--r--test/mono/builtins.sail2
-rw-r--r--test/mono/varpatterns.sail6
13 files changed, 141 insertions, 102 deletions
diff --git a/aarch64/Makefile b/aarch64/Makefile
index aa4d5301..365e23bd 100644
--- a/aarch64/Makefile
+++ b/aarch64/Makefile
@@ -5,13 +5,13 @@ SAIL_LIB_DIR:=$(SAIL_DIR)/lib
SAIL:=$(SAIL_DIR)/sail
aarch64.c: no_vector.sail
- $(SAIL) $^ -c -O -undefined_gen -no_lexp_bounds_check -memo_z3 1> aarch64.c
+ $(SAIL) $(SAIL_FLAGS) $^ -c -O -undefined_gen -no_lexp_bounds_check -memo_z3 1> aarch64.c
aarch64_c: aarch64.c
gcc -O2 $^ -o aarch64_c -lgmp -I $(SAIL_DIR)/lib
aarch64: no_vector.sail
- $(SAIL) $^ -o aarch64 -ocaml -undefined_gen -no_lexp_bounds_check -memo_z3
+ $(SAIL) $(SAIL_FLAGS) $^ -o aarch64 -ocaml -undefined_gen -no_lexp_bounds_check -memo_z3
aarch64_full: full.sail
$(SAIL) $^ -o aarch64_full -ocaml -undefined_gen -no_lexp_bounds_check -memo_z3
@@ -23,5 +23,11 @@ aarch64_types.lem: aarch64.lem
Aarch64.thy: aarch64_extras.lem aarch64_types.lem aarch64.lem
lem -isa -outdir . -lib Sail=$(SAIL_DIR)/src/gen_lib -lib Sail=$(SAIL_DIR)/src/lem_interp $^
+clean:
+ rm -rf _sbuild/
+ rm -f aarch64
+ rm -f aarch64.c
+ rm -f aarch64.lem
+
LOC_FILES:=prelude.sail full/spec.sail decode_start.sail full/decode.sail decode_end.sail main.sail
include ../etc/loc.mk
diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail
index 610884a4..fc53e03e 100644
--- a/aarch64/no_vector/spec.sail
+++ b/aarch64/no_vector/spec.sail
@@ -6336,7 +6336,7 @@ function AArch64_CheckS2Permission (perms, vaddress, ipaddress, 'level, acctype,
}
function AArch64_CheckAndUpdateDescriptor_SecondStage (result, fault, vaddress, acctype, iswrite, s2fs1walk, hwupdatewalk__arg) = {
- hwupdatewalk = hwupdatewalk__arg;
+ hwupdatewalk : bool = hwupdatewalk__arg;
hw_update_AF : bool = undefined;
if result.AF then
if fault.typ == Fault_None then hw_update_AF = true
@@ -6703,7 +6703,7 @@ function AArch64_SecondStageTranslate (S1, vaddress, acctype, iswrite, wasaligne
}
function AArch64_CheckAndUpdateDescriptor (result, fault, secondstage, vaddress, acctype, iswrite, s2fs1walk, hwupdatewalk__arg) = {
- hwupdatewalk = hwupdatewalk__arg;
+ hwupdatewalk : bool = hwupdatewalk__arg;
hw_update_AF : bool = undefined;
if result.AF then if fault.typ == Fault_None then hw_update_AF = true else if ConstrainUnpredictable(Unpredictable_AFUPDATE) == Constraint_TRUE then hw_update_AF = true else hw_update_AF = false else ();
hw_update_AP : bool = undefined;
@@ -6740,7 +6740,7 @@ function AArch64_StateMatch (SSC__arg, HMC__arg, PxC__arg, linked__arg, LBN, isb
HMC = HMC__arg;
PxC = PxC__arg;
SSC = SSC__arg;
- linked = linked__arg;
+ linked : bool = linked__arg;
c : Constraint = undefined;
if (((((((HMC @ SSC) @ PxC) & 0b11100) == 0b01100 | (((HMC @ SSC) @ PxC) & 0b11101) == 0b10000 | (((HMC @ SSC) @ PxC) & 0b11101) == 0b10100 | ((HMC @ SSC) @ PxC) == 0b11010 | ((HMC @ SSC) @ PxC) == 0b11101 | (((HMC @ SSC) @ PxC) & 0b11110) == 0b11110) | (HMC == 0b0 & PxC == 0b00) & (~(isbreakpnt) | ~(HaveAArch32EL(EL1)))) | (SSC == 0b01 | SSC == 0b10) & ~(HaveEL(EL3))) | (((HMC @ SSC) != 0b000 & (HMC @ SSC) != 0b111) & ~(HaveEL(EL3))) & ~(HaveEL(EL2))) | ((HMC @ SSC) @ PxC) == 0b11100 & ~(HaveEL(EL2)) then {
__tmp_5 : bits(5) = undefined;
@@ -9202,7 +9202,7 @@ function aarch64_memory_single_general_register (acctype, 'datasize, extend_type
let 'dbytes = ex_int(datasize / 8);
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
- wback = wback__arg;
+ wback : bool = wback__arg;
offset : bits(64) = ExtendReg(m, extend_type, shift);
address : bits(64) = undefined;
data : bits('datasize) = undefined;
@@ -9258,7 +9258,7 @@ function aarch64_memory_single_general_immediate_unsigned (acctype, 'datasize, m
let 'dbytes = ex_int(datasize / 8);
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
- wback = wback__arg;
+ wback : bool = wback__arg;
address : bits(64) = undefined;
data : bits('datasize) = undefined;
wb_unknown : bool = false;
@@ -9313,7 +9313,7 @@ function aarch64_memory_single_general_immediate_signed_postidx (acctype, 'datas
let 'dbytes = ex_int(datasize / 8);
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
- wback = wback__arg;
+ wback : bool = wback__arg;
address : bits(64) = undefined;
data : bits('datasize) = undefined;
wb_unknown : bool = false;
@@ -9364,7 +9364,7 @@ function aarch64_memory_single_general_immediate_signed_postidx (acctype, 'datas
val aarch64_memory_single_general_immediate_signed_pac : (int, bits(64), int, bool, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg}
function aarch64_memory_single_general_immediate_signed_pac ('n, offset, 't, use_key_a, wback__arg) = {
- wback = wback__arg;
+ wback : bool = wback__arg;
address : bits(64) = undefined;
data : bits(64) = undefined;
wb_unknown : bool = false;
@@ -9400,7 +9400,7 @@ function aarch64_memory_single_general_immediate_signed_offset_unpriv (acctype,
let 'dbytes = ex_int(datasize / 8);
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
- wback = wback__arg;
+ wback : bool = wback__arg;
address : bits(64) = undefined;
data : bits('datasize) = undefined;
wb_unknown : bool = false;
@@ -9455,7 +9455,7 @@ function aarch64_memory_single_general_immediate_signed_offset_normal (acctype,
let 'dbytes = ex_int(datasize / 8);
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
- wback = wback__arg;
+ wback : bool = wback__arg;
address : bits(64) = undefined;
data : bits('datasize) = undefined;
wb_unknown : bool = false;
@@ -9611,7 +9611,7 @@ val aarch64_memory_pair_general_postidx : forall ('datasize : Int).
function aarch64_memory_pair_general_postidx (acctype, datasize, memop, n, offset, postindex, signed, t, t2, wback__arg) = let 'dbytes = ex_int(datasize / 8) in {
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
- wback = wback__arg;
+ wback : bool = wback__arg;
address : bits(64) = undefined;
data1 : bits('datasize) = undefined;
data2 : bits('datasize) = undefined;
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 65702764..79d4693a 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -150,7 +150,7 @@ let rec ctyp_of_typ ctx typ =
when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 ->
CT_int64
| n, m when ctx.optimize_z3 ->
- if prove ctx.local_env (nc_lteq (nconstant min_int64) n) && prove ctx.local_env (nc_lteq m (nconstant max_int64)) then
+ if prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) then
CT_int64
else
CT_int
@@ -171,7 +171,7 @@ let rec ctyp_of_typ ctx typ =
let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in
begin match nexp_simp n with
| Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_fbits (Big_int.to_int n, direction)
- | n when ctx.optimize_z3 && prove ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits direction
+ | n when ctx.optimize_z3 && prove __POS__ ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits direction
| _ -> CT_lbits direction
end
@@ -541,7 +541,7 @@ let analyze_primop' ctx id args typ =
| Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 ->
AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_int64))
- | n, m when prove ctx.local_env (nc_lteq (nconstant min_int64) n) && prove ctx.local_env (nc_lteq m (nconstant max_int64)) ->
+ | n, m when prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) ->
AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_int64))
| _ -> no_change
end
diff --git a/src/constraint.ml b/src/constraint.ml
index b00c0a4e..af024ce3 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -208,12 +208,21 @@ let call_z3' l vars constraints : smt_result =
with
| Not_found ->
begin
- let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".sat" in
+ let (input_file, tmp_chan) =
+ try Filename.open_temp_file "constraint_" ".sat" with
+ | Sys_error msg -> raise (Reporting.err_general l ("Could not open temp file when calling Z3: " ^ msg))
+ in
output_string tmp_chan z3_file;
close_out tmp_chan;
- let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
- let z3_output = List.combine problems (input_lines z3_chan (List.length problems)) in
- let _ = Unix.close_process_in z3_chan in
+ let z3_output =
+ try
+ let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
+ let z3_output = List.combine problems (input_lines z3_chan (List.length problems)) in
+ let _ = Unix.close_process_in z3_chan in
+ z3_output
+ with
+ | exn -> raise (Reporting.err_general l ("Error when calling z3: " ^ Printexc.to_string exn))
+ in
Sys.remove input_file;
try
let (problem, _) = List.find (fun (_, result) -> result = "unsat") z3_output in
@@ -250,9 +259,16 @@ let rec solve_z3 l vars constraints var =
let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".sat" in
output_string tmp_chan z3_file;
close_out tmp_chan;
- let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
- let z3_output = String.concat " " (input_all z3_chan) in
- let _ = Unix.close_process_in z3_chan in
+ let z3_output =
+ try
+ let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
+ let z3_output = String.concat " " (input_all z3_chan) in
+ let _ = Unix.close_process_in z3_chan in
+ z3_output
+ with
+ | exn ->
+ raise (Reporting.err_general l ("Got error when calling z3: " ^ Printexc.to_string exn))
+ in
Sys.remove input_file;
let regexp = {|(define-fun v|} ^ Util.zencode_string (string_of_kid var) ^ {| () Int[ ]+\([0-9]+\))|} in
try
diff --git a/src/isail.ml b/src/isail.ml
index baeacdb5..d8876cf0 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -275,7 +275,7 @@ let handle_input' input =
print_endline (string_of_typ (Type_check.canonicalize !interactive_env typ))
| ":prove" ->
let nc = Initial_check.constraint_of_string arg in
- print_endline (string_of_bool (Type_check.prove !interactive_env nc))
+ print_endline (string_of_bool (Type_check.prove __POS__ !interactive_env nc))
| ":v" | ":verbose" ->
Type_check.opt_tc_debug := (!Type_check.opt_tc_debug + 1) mod 3;
print_endline ("Verbosity: " ^ string_of_int !Type_check.opt_tc_debug)
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 4bb1876c..fc2a9de6 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -100,36 +100,36 @@ let subst_nexp substs nexp =
| Nexp_app (id,args) -> re (Nexp_app (id,List.map s_snexp args))
in s_snexp substs nexp
-let rec subst_nc substs (NC_aux (nc,l) as n_constraint) =
- let snexp nexp = subst_nexp substs nexp in
- let snc nc = subst_nc substs nc in
- let re nc = NC_aux (nc,l) in
- match nc with
- | NC_equal (n1,n2) -> re (NC_equal (snexp n1, snexp n2))
- | NC_bounded_ge (n1,n2) -> re (NC_bounded_ge (snexp n1, snexp n2))
- | NC_bounded_le (n1,n2) -> re (NC_bounded_le (snexp n1, snexp n2))
- | NC_not_equal (n1,n2) -> re (NC_not_equal (snexp n1, snexp n2))
- | NC_set (kid,is) ->
- begin
- match KBindings.find kid substs with
- | Nexp_aux (Nexp_constant i,_) ->
- if List.exists (fun j -> Big_int.equal i j) is then re NC_true else re NC_false
- | nexp ->
- raise (Reporting.err_general l
- ("Unable to substitute " ^ string_of_nexp nexp ^
- " into set constraint " ^ string_of_n_constraint n_constraint))
- | exception Not_found -> n_constraint
- end
- | NC_or (nc1,nc2) -> re (NC_or (snc nc1, snc nc2))
- | NC_and (nc1,nc2) -> re (NC_and (snc nc1, snc nc2))
- | NC_true
- | NC_false
+let subst_nc, subst_src_typ, subst_src_typ_arg =
+ let rec subst_nc substs (NC_aux (nc,l) as n_constraint) =
+ let snexp nexp = subst_nexp substs nexp in
+ let snc nc = subst_nc substs nc in
+ let re nc = NC_aux (nc,l) in
+ match nc with
+ | NC_equal (n1,n2) -> re (NC_equal (snexp n1, snexp n2))
+ | NC_bounded_ge (n1,n2) -> re (NC_bounded_ge (snexp n1, snexp n2))
+ | NC_bounded_le (n1,n2) -> re (NC_bounded_le (snexp n1, snexp n2))
+ | NC_not_equal (n1,n2) -> re (NC_not_equal (snexp n1, snexp n2))
+ | NC_set (kid,is) ->
+ begin
+ match KBindings.find kid substs with
+ | Nexp_aux (Nexp_constant i,_) ->
+ if List.exists (fun j -> Big_int.equal i j) is then re NC_true else re NC_false
+ | nexp ->
+ raise (Reporting.err_general l
+ ("Unable to substitute " ^ string_of_nexp nexp ^
+ " into set constraint " ^ string_of_n_constraint n_constraint))
+ | exception Not_found -> n_constraint
+ end
+ | NC_or (nc1,nc2) -> re (NC_or (snc nc1, snc nc2))
+ | NC_and (nc1,nc2) -> re (NC_and (snc nc1, snc nc2))
+ | NC_true
+ | NC_false
-> n_constraint
-
-
-
-let subst_src_typ substs t =
- let rec s_styp substs ((Typ_aux (t,l)) as ty) =
+ | NC_var kid -> re (NC_var kid)
+ | NC_app (f, args) ->
+ re (NC_app (f, List.map (s_starg substs) args))
+ and s_styp substs ((Typ_aux (t,l)) as ty) =
let re t = Typ_aux (t,l) in
match t with
| Typ_id _
@@ -148,7 +148,8 @@ let subst_src_typ substs t =
| A_nexp ne -> A_aux (A_nexp (subst_nexp substs ne),l)
| A_typ t -> A_aux (A_typ (s_styp substs t),l)
| A_order _ -> targ
- in s_styp substs t
+ | A_bool nc -> A_aux (A_bool (subst_nc substs nc), l)
+ in subst_nc, s_styp, s_starg
let make_vector_lit sz i =
let f j = if Big_int.equal (Big_int.modulus (Big_int.shift_right i (sz-j-1)) (Big_int.of_int 2)) Big_int.zero then '0' else '1' in
@@ -727,8 +728,10 @@ let fabricate_nexp_exist env l typ kids nc typ' =
when Kid.compare kid kid'' = 0 &&
Kid.compare kid kid''' = 0 ->
nint 32
- | _ -> raise (Reporting.err_general l
- ("Undefined value at unsupported type " ^ string_of_typ typ))
+ | ([], _, typ) -> nint 32
+ | (kids, nc, typ) ->
+ raise (Reporting.err_general l
+ ("Undefined value at unsupported type " ^ string_of_typ typ ^ " with " ^ Util.string_of_list ", " string_of_kid kids))
let fabricate_nexp l tannot =
match destruct_tannot tannot with
@@ -756,7 +759,7 @@ let reduce_cast typ exp l annot =
| E_aux (E_lit (L_aux (L_num n,_)),_), Some ([kopt],nc,typ'') when atom_typ_kid (kopt_kid kopt) typ'' ->
let nc_env = Env.add_typ_var l kopt env in
let nc_env = Env.add_constraint (nc_eq (nvar (kopt_kid kopt)) (nconstant n)) nc_env in
- if prove nc_env nc
+ if prove __POS__ nc_env nc
then exp
else raise (Reporting.err_unreachable l __POS__
("Constant propagation error: literal " ^ Big_int.to_string n ^
@@ -1176,7 +1179,7 @@ let apply_pat_choices choices =
let is_env_inconsistent env ksubsts =
let env = KBindings.fold (fun k nexp env ->
Env.add_constraint (nc_eq (nvar k) nexp) env) ksubsts env in
- prove env nc_false
+ prove __POS__ env nc_false
let split_defs all_errors splits defs =
let no_errors_happened = ref true in
@@ -1663,7 +1666,7 @@ let split_defs all_errors splits defs =
let substs = bindings_from_list substs, ksubsts in
fst (const_prop_exp ref_vars substs Bindings.empty exp)
in
-
+
(* Split a variable pattern into every possible value *)
let split var pat_l annot =
@@ -1686,7 +1689,7 @@ let split_defs all_errors splits defs =
else raise (Fatal_error error)
in
match ty with
- | Typ_id (Id_aux (Id "bool",_)) ->
+ | Typ_id (Id_aux (Id "bool",_)) | Typ_app (Id_aux (Id "atom_bool", _), [_]) ->
[P_aux (P_lit (L_aux (L_true,new_l)),(l,annot)),[var, E_aux (E_lit (L_aux (L_true,new_l)),(new_l,annot))],[],[];
P_aux (P_lit (L_aux (L_false,new_l)),(l,annot)),[var, E_aux (E_lit (L_aux (L_false,new_l)),(new_l,annot))],[],[]]
@@ -2259,7 +2262,7 @@ let replace_with_the_value bound_nexps (E_aux (_,(l,_)) as exp) =
let replace_size size =
(* TODO: pick simpler nexp when there's a choice (also in pretty printer) *)
let is_equal nexp =
- prove env (NC_aux (NC_equal (size,nexp), Parse_ast.Unknown))
+ prove __POS__ env (NC_aux (NC_equal (size,nexp), Parse_ast.Unknown))
in
if is_nexp_constant size then size else
match List.find is_equal bound_nexps with
@@ -2345,9 +2348,9 @@ in *)
| i -> IntSet.singleton i
| exception Not_found ->
(* Look for equivalent nexps, but only in consistent type env *)
- if prove env (NC_aux (NC_false,Unknown)) then IntSet.empty else
+ if prove __POS__ env (NC_aux (NC_false,Unknown)) then IntSet.empty else
match List.find (fun (nexp,i) ->
- prove env (NC_aux (NC_equal (nexp,size),Unknown))) nexp_list with
+ prove __POS__ env (NC_aux (NC_equal (nexp,size),Unknown))) nexp_list with
| _, i -> IntSet.singleton i
| exception Not_found -> IntSet.empty
end
@@ -2848,11 +2851,15 @@ let rec deps_of_nc kid_deps (NC_aux (nc,l)) =
| NC_true
| NC_false
-> dempty
+ | NC_app (Id_aux (Id "mod", _), [A_aux (A_nexp nexp1, _); A_aux (A_nexp nexp2, _)])
+ -> dmerge (deps_of_nexp l kid_deps [] nexp1) (deps_of_nexp l kid_deps [] nexp2)
+ | NC_var _ | NC_app _
+ -> dempty
-let deps_of_typ l kid_deps arg_deps typ =
+and deps_of_typ l kid_deps arg_deps typ =
deps_of_tyvars l kid_deps arg_deps (tyvars_of_typ typ)
-let deps_of_typ_arg l fn_id env arg_deps (A_aux (aux, _)) =
+and deps_of_typ_arg l fn_id env arg_deps (A_aux (aux, _)) =
match aux with
| A_nexp (Nexp_aux (Nexp_var kid,_))
when List.exists (fun k -> Kid.compare kid k == 0) env.top_kids ->
@@ -2861,7 +2868,7 @@ let deps_of_typ_arg l fn_id env arg_deps (A_aux (aux, _)) =
| A_order _ -> InFun dempty
| A_typ typ -> InFun (deps_of_typ l env.kid_deps arg_deps typ)
| A_bool nc -> InFun (deps_of_nc env.kid_deps nc)
-
+
let mk_subrange_pattern vannot vstart vend =
let (len,ord,typ) = vector_typ_args_of (Env.base_typ_of (env_of_annot vannot) (typ_of_annot vannot)) in
match ord with
@@ -2936,7 +2943,11 @@ let simplify_size_nexp env typ_env (Nexp_aux (ne,l) as nexp) =
| Some n -> nconstant n
| None ->
let is_equal kid =
- prove typ_env (NC_aux (NC_equal (Nexp_aux (Nexp_var kid,Unknown), nexp),Unknown))
+ (* AA: top_kids should be changed to top_kopts so we don't end
+ up trying to prove v == nexp for a non-Int v. *)
+ try
+ prove __POS__ typ_env (NC_aux (NC_equal (Nexp_aux (Nexp_var kid,Unknown), nexp),Unknown))
+ with _ -> false
in
match ne with
| Nexp_var _
@@ -3935,7 +3946,7 @@ let simplify_size_nexp env quant_kids (Nexp_aux (_,l) as nexp) =
| Some n -> Some (nconstant n)
| None ->
let is_equal kid =
- prove env (NC_aux (NC_equal (Nexp_aux (Nexp_var kid,Unknown), nexp),Unknown))
+ prove __POS__ env (NC_aux (NC_equal (Nexp_aux (Nexp_var kid,Unknown), nexp),Unknown))
in
match List.find is_equal quant_kids with
| kid -> Some (Nexp_aux (Nexp_var kid,Generated l))
@@ -4198,7 +4209,7 @@ let replace_nexp_in_typ env typ orig new_nexp =
and aux_targ (A_aux (ta,l) as typ_arg) =
match ta with
| A_nexp nexp ->
- if prove env (nc_eq nexp orig)
+ if prove __POS__ env (nc_eq nexp orig)
then true, A_aux (A_nexp new_nexp,l)
else false, typ_arg
| A_typ typ ->
@@ -4227,7 +4238,7 @@ let fresh_nexp_kid nexp =
let rewrite_toplevel_nexps (Defs defs) =
let find_nexp env nexp_map nexp =
- let is_equal (kid,nexp') = prove env (nc_eq nexp nexp') in
+ let is_equal (kid,nexp') = prove __POS__ env (nc_eq nexp nexp') in
List.find is_equal nexp_map
in
let rec rewrite_typ_in_spec env nexp_map (Typ_aux (t,ann) as typ_full) =
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 18e288dd..b408c6eb 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -542,7 +542,7 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) =
| Some n -> mk_typ (nconstant n)
| None ->
let is_equal nexp =
- prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
+ prove __POS__ env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with
| nexp -> mk_typ nexp
| exception Not_found -> None
@@ -837,7 +837,7 @@ let similar_nexps ctxt env n1 n2 =
by tracking which existential kids are equal to bound kids. *)
| Nexp_var k1, Nexp_var k2 ->
Kid.compare k1 k2 == 0 ||
- (prove env (nc_eq (nvar k1) (nvar k2)) && (
+ (prove __POS__ env (nc_eq (nvar k1) (nvar k2)) && (
not (KidSet.mem k1 ctxt.bound_nvars) ||
not (KidSet.mem k2 ctxt.bound_nvars)))
| Nexp_constant c1, Nexp_constant c2 -> Nat_big_num.equal c1 c2
@@ -895,7 +895,7 @@ let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) =
| Typ_app(Id_aux (Id "atom", _), [A_aux (A_nexp nexp,_)]),
Typ_app(Id_aux (Id "range", _), [A_aux(A_nexp low,_);
A_aux(A_nexp high,_)]) ->
- Type_check.prove env (nc_and (nc_eq nexp low) (nc_eq nexp high))
+ Type_check.prove __POS__ env (nc_and (nc_eq nexp low) (nc_eq nexp high))
| _ -> false
(* Get a more general type for an annotation/expression - i.e.,
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index ea34ef3d..90ae2dba 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -356,7 +356,7 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) =
| Some n -> mk_typ (nconstant n)
| None ->
let is_equal nexp =
- prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
+ prove __POS__ env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with
| nexp -> mk_typ nexp
| exception Not_found -> None
diff --git a/src/rewrites.ml b/src/rewrites.ml
index e87847bd..ea8ccaf9 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -332,18 +332,18 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
let extract_typ_var l env nexp (id, (_, typ)) =
let var = E_aux (E_id id, (l, mk_tannot env typ no_effect)) in
match destruct_atom_nexp env typ with
- | Some size when prove env (nc_eq size nexp) -> Some var
+ | Some size when prove __POS__ env (nc_eq size nexp) -> Some var
(* AA: This next case is a bit of a hack... is there a more
general way to deal with trivial nexps that are offset by
constants? This will resolve a 'n - 1 sizeof when 'n is in
scope. *)
- | Some size when prove env (nc_eq (nsum size (nint 1)) nexp) ->
+ | Some size when prove __POS__ env (nc_eq (nsum size (nint 1)) nexp) ->
let one_exp = infer_exp env (mk_lit_exp (L_num (Big_int.of_int 1))) in
Some (E_aux (E_app (mk_id "add_atom", [var; one_exp]), (gen_loc l, mk_tannot env (atom_typ (nsum size (nint 1))) no_effect)))
| _ ->
begin
match destruct_vector env typ with
- | Some (len, _, _) when prove env (nc_eq len nexp) ->
+ | Some (len, _, _) when prove __POS__ env (nc_eq len nexp) ->
Some (E_aux (E_app (mk_id "length", [var]), (l, mk_tannot env (atom_typ len) no_effect)))
| _ -> None
end
diff --git a/src/type_check.ml b/src/type_check.ml
index 97979b8c..cb20ae2e 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1290,10 +1290,15 @@ let solve env (Nexp_aux (_, l) as nexp) =
let constr = List.fold_left nc_and (nc_eq (nvar (mk_kid "solve#")) nexp) (Env.get_constraints env) in
Constraint.solve_z3 l vars constr (mk_kid "solve#")
-let prove env nc =
+let debug_pos (file, line, _, _) =
+ "(" ^ file ^ "/" ^ string_of_int line ^ ") "
+
+let prove pos env nc =
typ_print (lazy (Util.("Prove " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc));
let (NC_aux (nc_aux, _) as nc) = constraint_simp (Env.expand_constraint_synonyms env nc) in
- typ_debug ~level:2 (lazy (Util.("Prove " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc));
+ if !Constraint.opt_smt_verbose then
+ prerr_endline (Util.("Prove " |> red |> clear) ^ debug_pos pos ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc)
+ else ();
match nc_aux with
| NC_true -> true
| _ -> prove_z3 env nc
@@ -1480,7 +1485,7 @@ and unify_nexp l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (nexp_au
if KidSet.is_empty (KidSet.inter (nexp_frees nexp1) goals)
then
begin
- if prove env (NC_aux (NC_equal (nexp1, nexp2), Parse_ast.Unknown))
+ if prove __POS__ env (NC_aux (NC_equal (nexp1, nexp2), Parse_ast.Unknown))
then KBindings.empty
else unify_error l ("Nexp " ^ string_of_nexp nexp1 ^ " and " ^ string_of_nexp nexp2 ^ " are not equal")
end
@@ -1513,7 +1518,7 @@ and unify_nexp l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (nexp_au
mod(m, C) = 0 && C != 0 --> (C * n = m <--> n = m / C)
to help us unify multiplications and divisions.
- let valid n c = prove env (nc_eq (napp (mk_id "mod") [n; c]) (nint 0)) && prove env (nc_neq c (nint 0)) in
+ let valid n c = prove __POS__ env (nc_eq (napp (mk_id "mod") [n; c]) (nint 0)) && prove __POS__ env (nc_neq c (nint 0)) in
if KidSet.is_empty (nexp_frees n1b) && valid nexp2 n1b then
unify_nexp l env goals n1a (napp (mk_id "div") [nexp2; n1b])
else if KidSet.is_empty (nexp_frees n1a) && valid nexp2 n1a then
@@ -1521,7 +1526,7 @@ and unify_nexp l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (nexp_au
if KidSet.is_empty (nexp_frees n1a) then
begin
match nexp_aux2 with
- | Nexp_times (n2a, n2b) when prove env (NC_aux (NC_equal (n1a, n2a), Parse_ast.Unknown)) ->
+ | Nexp_times (n2a, n2b) when prove __POS__ env (NC_aux (NC_equal (n1a, n2a), Parse_ast.Unknown)) ->
unify_nexp l env goals n1b n2b
| Nexp_constant c2 ->
begin
@@ -1535,7 +1540,7 @@ and unify_nexp l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (nexp_au
else if KidSet.is_empty (nexp_frees n1b) then
begin
match nexp_aux2 with
- | Nexp_times (n2a, n2b) when prove env (NC_aux (NC_equal (n1b, n2b), Parse_ast.Unknown)) ->
+ | Nexp_times (n2a, n2b) when prove __POS__ env (NC_aux (NC_equal (n1b, n2b), Parse_ast.Unknown)) ->
unify_nexp l env goals n1a n2a
| _ -> unify_error l ("Cannot unify Int expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2)
end
@@ -1751,14 +1756,14 @@ let rec subtyp l env typ1 typ2 =
(* Special cases for two numeric (atom) types *)
| Some (kids1, nc1, nexp1), Some ([], _, nexp2) ->
let env = add_existential l (List.map (mk_kopt K_int) kids1) nc1 env in
- if prove env (nc_eq nexp1 nexp2) then () else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
+ if prove __POS__ env (nc_eq nexp1 nexp2) then () else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
| Some (kids1, nc1, nexp1), Some (kids2, nc2, nexp2) ->
let env = add_existential l (List.map (mk_kopt K_int) kids1) nc1 env in
let env = add_typ_vars l (List.map (mk_kopt K_int) (KidSet.elements (KidSet.inter (nexp_frees nexp2) (KidSet.of_list kids2)))) env in
let kids2 = KidSet.elements (KidSet.diff (KidSet.of_list kids2) (nexp_frees nexp2)) in
if not (kids2 = []) then typ_error l ("Universally quantified constraint generated: " ^ Util.string_of_list ", " string_of_kid kids2) else ();
let env = Env.add_constraint (nc_eq nexp1 nexp2) env in
- if prove env nc2 then ()
+ if prove __POS__ env nc2 then ()
else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
| _, _ ->
match typ_aux1, typ_aux2 with
@@ -1794,17 +1799,17 @@ let rec subtyp l env typ1 typ2 =
in
let nc = List.fold_left (fun nc (kid, uvar) -> constraint_subst kid uvar nc) nc (KBindings.bindings unifiers) in
let env = List.fold_left unifier_constraint env (KBindings.bindings unifiers) in
- if prove env nc then ()
+ if prove __POS__ env nc then ()
else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
| None, None -> typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
and subtyp_arg l env (A_aux (aux1, _) as arg1) (A_aux (aux2, _) as arg2) =
typ_print (lazy (("Subtype arg " |> Util.green |> Util.clear) ^ string_of_typ_arg arg1 ^ " and " ^ string_of_typ_arg arg2));
match aux1, aux2 with
- | A_nexp n1, A_nexp n2 when prove env (nc_eq n1 n2) -> ()
+ | A_nexp n1, A_nexp n2 when prove __POS__ env (nc_eq n1 n2) -> ()
| A_typ typ1, A_typ typ2 -> subtyp l env typ1 typ2
| A_order ord1, A_order ord2 when ord_identical ord1 ord2 -> ()
- | A_bool nc1, A_bool nc2 when prove env (nc_and (nc_or (nc_not nc1) nc2) (nc_or (nc_not nc2) nc1)) -> ()
+ | A_bool nc1, A_bool nc2 when prove __POS__ env (nc_and (nc_or (nc_not nc1) nc2) (nc_or (nc_not nc2) nc1)) -> ()
| _, _ -> typ_error l "Mismatched argument types in subtype check"
let typ_equality l env typ1 typ2 =
@@ -2101,7 +2106,7 @@ let rec add_constraints constrs env =
let solve_quant env = function
| QI_aux (QI_id _, _) -> false
- | QI_aux (QI_const nc, _) -> prove env nc
+ | QI_aux (QI_const nc, _) -> prove __POS__ env nc
(* When doing implicit type coercion, for performance reasons we want
to filter out the possible casts to only those that could
@@ -2274,12 +2279,12 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
check_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ()))) typ
| E_app (f, [E_aux (E_constraint nc, _)]), _ when string_of_id f = "_prove" ->
Env.wf_constraint env nc;
- if prove env nc
+ if prove __POS__ env nc
then annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ
else typ_error l ("Cannot prove " ^ string_of_n_constraint nc)
| E_app (f, [E_aux (E_constraint nc, _)]), _ when string_of_id f = "_not_prove" ->
Env.wf_constraint env nc;
- if prove env nc
+ if prove __POS__ env nc
then typ_error l ("Can prove " ^ string_of_n_constraint nc)
else annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ
| E_app (f, [E_aux (E_cast (typ, exp), _)]), _ when string_of_id f = "_check" ->
@@ -2390,7 +2395,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
| E_vector vec, _ ->
let (len, ord, vtyp) = destruct_vec_typ l env typ in
let checked_items = List.map (fun i -> crule check_exp env i vtyp) vec in
- if prove env (nc_eq (nint (List.length vec)) (nexp_simp len)) then annot_exp (E_vector checked_items) typ
+ if prove __POS__ env (nc_eq (nint (List.length vec)) (nexp_simp len)) then annot_exp (E_vector checked_items) typ
else typ_error l "List length didn't match" (* FIXME: improve error message *)
| E_lit (L_aux (L_undef, _) as lit), _ ->
if is_typ_monomorphic typ || Env.polymorphic_undefineds env
@@ -3047,10 +3052,10 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
let nexp1, env = bind_numeric l (typ_of inferred_exp1) env in
let nexp2, env = bind_numeric l (typ_of inferred_exp2) env in
begin match ord with
- | Ord_aux (Ord_inc, _) when !opt_no_lexp_bounds_check || prove env (nc_lteq nexp1 nexp2) ->
+ | Ord_aux (Ord_inc, _) when !opt_no_lexp_bounds_check || prove __POS__ env (nc_lteq nexp1 nexp2) ->
let len = nexp_simp (nsum (nminus nexp2 nexp1) (nint 1)) in
annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (vector_typ len ord elem_typ)
- | Ord_aux (Ord_dec, _) when !opt_no_lexp_bounds_check || prove env (nc_gteq nexp1 nexp2) ->
+ | Ord_aux (Ord_dec, _) when !opt_no_lexp_bounds_check || prove __POS__ env (nc_gteq nexp1 nexp2) ->
let len = nexp_simp (nsum (nminus nexp1 nexp2) (nint 1)) in
annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (vector_typ len ord elem_typ)
| _ -> typ_error l ("Could not infer length of vector slice assignment " ^ string_of_lexp lexp)
@@ -3066,7 +3071,7 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
when Id.compare id (mk_id "vector") = 0 ->
let inferred_exp = infer_exp env exp in
let nexp, env = bind_numeric l (typ_of inferred_exp) env in
- if !opt_no_lexp_bounds_check || prove env (nc_and (nc_lteq (nint 0) nexp) (nc_lteq nexp (nexp_simp (nminus len (nint 1))))) then
+ if !opt_no_lexp_bounds_check || prove __POS__ env (nc_and (nc_lteq (nint 0) nexp) (nc_lteq nexp (nexp_simp (nminus len (nint 1))))) then
annot_lexp (LEXP_vector (inferred_v_lexp, inferred_exp)) elem_typ
else
typ_error l ("Vector assignment not provably in bounds " ^ string_of_lexp lexp)
@@ -3126,7 +3131,8 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
| Unbound -> typ_error l ("Identifier " ^ string_of_id v ^ " is unbound")
end
| E_lit lit -> annot_exp (E_lit lit) (infer_lit env lit)
- | E_sizeof nexp -> annot_exp (E_sizeof nexp) (mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (A_nexp nexp)])))
+ | E_sizeof nexp ->
+ annot_exp (E_sizeof nexp) (mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (A_nexp nexp)])))
| E_constraint nc ->
Env.wf_constraint env nc;
annot_exp (E_constraint nc) (atom_bool_typ nc)
@@ -4425,7 +4431,7 @@ let mk_synonym typq typ_arg =
in
fun env args ->
let typ_arg, ncs = subst_args kopts args in
- if List.for_all (prove env) ncs
+ if List.for_all (prove __POS__ env) ncs
then typ_arg
else typ_error Parse_ast.Unknown ("Could not prove constraints " ^ string_of_list ", " string_of_n_constraint ncs
^ " in type synonym " ^ string_of_typ_arg typ_arg
@@ -4537,7 +4543,7 @@ and check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
let initial_env =
Env.empty
- |> Env.add_prover prove
+ |> Env.add_prover (prove __POS__)
(* |> Env.add_typ_synonym (mk_id "atom") (fun _ args -> mk_typ (Typ_app (mk_id "range", args @ args))) *)
(* Internal functions for Monomorphise.AtomToItself *)
diff --git a/src/type_check.mli b/src/type_check.mli
index c470e9c4..d1061826 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -301,7 +301,7 @@ val check_fundef : Env.t -> 'a fundef -> tannot def list * Env.t
val check_val_spec : Env.t -> 'a val_spec -> tannot def list * Env.t
-val prove : Env.t -> n_constraint -> bool
+val prove : (string * int * int * int) -> Env.t -> n_constraint -> bool
val solve : Env.t -> nexp -> Big_int.num option
diff --git a/test/mono/builtins.sail b/test/mono/builtins.sail
index 99447d42..770259be 100644
--- a/test/mono/builtins.sail
+++ b/test/mono/builtins.sail
@@ -43,7 +43,7 @@ function test(b) = {
assert(x != y, "!= by propagation");
assert(slice(x, 0, 4) == slice(x',0,4), "propagated slice == runtime slice");
assert(0x3 == slice(y, 4, 4), "literal vs propagated middle slice");
- assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }), "UInt propagation vs literal");
+ assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt propagation vs literal");
assert(shl_int(5,2) == shl_int(launder_int(5),2), "shl_int");
}
diff --git a/test/mono/varpatterns.sail b/test/mono/varpatterns.sail
index 9de412ac..b2c9e7ee 100644
--- a/test/mono/varpatterns.sail
+++ b/test/mono/varpatterns.sail
@@ -35,7 +35,7 @@ val test : bool -> unit effect {escape}
function test(b) = {
let 'n : {|8,16|} = if b then 8 else 16;
let x : bits('n) = match 'n { 8 => 0x12, 16 => 0x1234 };
- assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }), "UInt");
+ assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt");
}
val test2 : bool -> unit effect {escape}
@@ -43,7 +43,7 @@ val test2 : bool -> unit effect {escape}
function test2(b) = {
let 'n = (if b then 8 else 16) : {|8,16|};
let x : bits('n) = match 'n { 8 => 0x12, 16 => 0x1234 };
- assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }), "UInt");
+ assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt");
}
val test_mult : {|4,8|} -> unit effect {escape}
@@ -51,7 +51,7 @@ val test_mult : {|4,8|} -> unit effect {escape}
function test_mult('m) = {
let 'n = 2 * 'm;
let x : bits('n) = match 'n { 8 => 0x12, 16 => 0x1234 };
- assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }), "UInt");
+ assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt");
}
val run : unit -> unit effect {escape}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:52:45 +0000