Improve sizeof rewriting performance

Simply constraints further before calling Z3 to improve performance of
sizeof re-writing.

8 files changed, 44 insertions, 24 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 55f8c61c..36263615 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -321,10 +321,23 @@ let rec constraint_simp (NC_aux (nc_aux, l)) =
        | NC_aux (nc, _), NC_aux (NC_true, _) -> NC_true
        | _, _ -> NC_or (nc1, nc2)
        end
+
     | NC_bounded_ge (nexp1, nexp2) ->
-       NC_bounded_ge (nexp_simp nexp1, nexp_simp nexp2)
+       let nexp1, nexp2 = nexp_simp nexp1, nexp_simp nexp2 in
+       begin match nexp1, nexp2 with
+       | Nexp_aux (Nexp_constant c1, _), Nexp_aux (Nexp_constant c2, _) ->
+          if Big_int.greater_equal c1 c2 then NC_true else NC_false
+       | _, _ -> NC_bounded_ge (nexp1, nexp2)
+       end
+
     | NC_bounded_le (nexp1, nexp2) ->
-       NC_bounded_le (nexp_simp nexp1, nexp_simp nexp2)
+       let nexp1, nexp2 = nexp_simp nexp1, nexp_simp nexp2 in
+       begin match nexp1, nexp2 with
+       | Nexp_aux (Nexp_constant c1, _), Nexp_aux (Nexp_constant c2, _) ->
+          if Big_int.less_equal c1 c2 then NC_true else NC_false
+       | _, _ -> NC_bounded_le (nexp1, nexp2)
+       end
+
     | _ -> nc_aux
   in
   NC_aux (nc_aux, l)
diff --git a/src/constraint.ml b/src/constraint.ml
index 7ead0cc8..b00c0a4e 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -53,6 +53,8 @@ open Ast
 open Ast_util
 open Util
 
+let opt_smt_verbose = ref false
+
 (* SMTLIB v2.0 format is based on S-expressions so we have a
    lightweight representation of those here. *)
 type sexpr = List of (sexpr list) | Atom of string
@@ -185,7 +187,9 @@ let call_z3' l vars constraints : smt_result =
   let problems = [constraints] in
   let z3_file = smtlib_of_constraints l vars constraints in
 
-  (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); *)
+  if !opt_smt_verbose then
+    prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file)
+  else ();
 
   let rec input_lines chan = function
     | 0 -> []
diff --git a/src/constraint.mli b/src/constraint.mli
index 51088245..fa318c35 100644
--- a/src/constraint.mli
+++ b/src/constraint.mli
@@ -52,6 +52,8 @@ module Big_int = Nat_big_num
 open Ast
 open Ast_util
 
+val opt_smt_verbose : bool ref
+
 type smt_result = Unknown | Sat | Unsat
 
 val load_digests : unit -> unit
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 17b4b515..16597b3a 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -795,6 +795,10 @@ let typ_of_string str =
   let typ = to_ast_typ initial_ctx typ in
   typ
 
+let constraint_of_string str =
+  let atyp = Parser.typ_eof Lexer.token (Lexing.from_string str) in
+  to_ast_constraint initial_ctx atyp
+
 let extern_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, (fun _ -> Some (string_of_id id)), false))
 let val_spec_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, (fun _ -> None), false))
 
diff --git a/src/initial_check.mli b/src/initial_check.mli
index 25187e4c..9d2beab2 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -92,3 +92,4 @@ val val_spec_of_string : id -> string -> unit def
 
 val exp_of_string : string -> unit exp
 val typ_of_string : string -> typ
+val constraint_of_string : string -> n_constraint
diff --git a/src/isail.ml b/src/isail.ml
index 18c59e0b..baeacdb5 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -273,6 +273,9 @@ let handle_input' input =
          | ":canon" ->
             let typ = Initial_check.typ_of_string arg in
             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))
          | ":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/sail.ml b/src/sail.ml
index 59190d15..f88fff5a 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -239,6 +239,9 @@ let options = Arg.align ([
   ( "-dtc_verbose",
     Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity),
     "<verbosity> (debug) verbose typechecker output: 0 is silent");
+  ( "-dsmt_verbose",
+    Arg.Set Constraint.opt_smt_verbose,
+    " (debug) print SMTLIB constraints sent to Z3");
   ( "-dno_cast",
     Arg.Set opt_dno_cast,
     " (debug) typecheck without any implicit casting");
diff --git a/src/type_check.ml b/src/type_check.ml
index ba7b2acb..97979b8c 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -682,12 +682,11 @@ end = struct
     | Nexp_id _ -> ()
     | Nexp_var kid when KidSet.mem kid exs -> ()
     | Nexp_var kid ->
-       begin
-         match get_typ_var kid env with
-         | K_int -> ()
-         | kind -> typ_error l ("Constraint is badly formed, "
-                                ^ string_of_kid kid ^ " has kind "
-                                ^ string_of_kind_aux kind ^ " but should have kind Int")
+       begin match get_typ_var kid env with
+       | K_int -> ()
+       | kind -> typ_error l ("Constraint is badly formed, "
+                              ^ string_of_kid kid ^ " has kind "
+                              ^ string_of_kind_aux kind ^ " but should have kind Int")
        end
     | Nexp_constant _ -> ()
     | Nexp_app (id, nexps) ->
@@ -700,12 +699,11 @@ end = struct
   and wf_order env (Ord_aux (ord_aux, l) as ord) =
     match ord_aux with
     | Ord_var kid ->
-       begin
-         match get_typ_var kid env with
-         | K_order -> ()
-         | kind -> typ_error l ("Order is badly formed, "
-                                ^ string_of_kid kid ^ " has kind "
-                                ^ string_of_kind_aux kind ^ " but should have kind Order")
+       begin match get_typ_var kid env with
+       | K_order -> ()
+       | kind -> typ_error l ("Order is badly formed, "
+                              ^ string_of_kid kid ^ " has kind "
+                              ^ string_of_kind_aux kind ^ " but should have kind Order")
        end
     | Ord_inc | Ord_dec -> ()
   and wf_constraint ?exs:(exs=KidSet.empty) env (NC_aux (nc_aux, l) as nc) =
@@ -1294,17 +1292,9 @@ let solve env (Nexp_aux (_, l) as nexp) =
 
 let prove 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) = Env.expand_constraint_synonyms env nc in
+  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));
-  let compare_const f (Nexp_aux (n1, _)) (Nexp_aux (n2, _)) =
-    match n1, n2 with
-    | Nexp_constant c1, Nexp_constant c2 when f c1 c2 -> true
-    | _, _ -> false
-  in
   match nc_aux with
-  | NC_equal (nexp1, nexp2) when compare_const Big_int.equal (nexp_simp nexp1) (nexp_simp nexp2) -> true
-  | NC_bounded_le (nexp1, nexp2) when compare_const Big_int.less_equal (nexp_simp nexp1) (nexp_simp nexp2) -> true
-  | NC_bounded_ge (nexp1, nexp2) when compare_const Big_int.greater_equal (nexp_simp nexp1) (nexp_simp nexp2) -> true
   | NC_true -> true
   | _ -> prove_z3 env nc