SMT: Allow partial specializations

Change specialisation so we only specialize integer parameters when
they are constant. This makes ensures that the integer-specialised
code is always type-correct.

4 files changed, 17 insertions, 14 deletions

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 895c440b..98de75b0 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -150,11 +150,11 @@ let smt_value vl ctyp =
   | VL_bool b, _ -> Bool_lit b
   | VL_int n, CT_constant m -> bvint (required_width n) n
   | VL_int n, CT_fint sz -> bvint sz n
+  | VL_int n, CT_lint -> bvint !lint_size n
   | VL_bit Sail2_values.B0, CT_bit -> Bin "0"
   | VL_bit Sail2_values.B1, CT_bit -> Bin "1"
   | VL_unit, _ -> Var "unit"
-
-  | vl, _ -> failwith ("Bad literal " ^ string_of_value vl)
+  | vl, _ -> failwith ("Cannot translate literal to SMT " ^ string_of_value vl)
 
 let zencode_ctor ctor_id unifiers =
   match unifiers with
@@ -426,15 +426,18 @@ let builtin_shift shiftop env vbits vshift ret_ctyp =
 let builtin_not_bits env v ret_ctyp =
   match cval_ctyp v, ret_ctyp with
   | CT_lbits _, CT_fbits (n, _) ->
-     Fn ("bvnot", [Extract (n - 1, 0, Fn ("contents", [smt_cval env v]))])
+     bvnot (Extract (n - 1, 0, Fn ("contents", [smt_cval env v])))
 
   | CT_lbits _, CT_lbits _ ->
      let bv = smt_cval env v in
      let len = Fn ("len", [bv]) in
      Fn ("Bits", [len; Fn ("bvand", [bvmask len; bvnot (Fn ("contents", [bv]))])])
-    
+
+  | CT_fbits (n, _), CT_fbits (m, _) when n = m ->
+     bvnot (smt_cval env v)
+
   | _, _ -> builtin_type_error "not_bits" [v] (Some ret_ctyp)
-       
+
 let builtin_or_bits env v1 v2 ret_ctyp =
   match cval_ctyp v1, cval_ctyp v2 with
   | CT_fbits (n, _), CT_fbits (m, _) ->
@@ -464,7 +467,7 @@ let builtin_and_bits env v1 v2 ret_ctyp =
      Fn ("Bits", [Fn ("len", [smt1]); bvand (Fn ("contents", [smt1])) (Fn ("contents", [smt2]))])
 
   | _ -> failwith "Cannot compile or_bits"
-       
+
 let builtin_append env v1 v2 ret_ctyp =
   match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
   | CT_fbits (n, _), CT_fbits (m, _), CT_fbits (o, _) ->
@@ -1224,11 +1227,11 @@ let smt_cdef props name_file env all_cdefs = function
         let out_chan = open_out (name_file (string_of_id function_id)) in
         output_string out_chan "(set-logic QF_AUFBVDT)\n";
 
-        let stack' = Stack.create () in
+        (* let stack' = Stack.create () in
         Stack.iter (fun def -> Stack.push def stack') stack;
-        Stack.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") stack';
-        (* let queue = optimize_smt stack in
-        Queue.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") queue; *)
+        Stack.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") stack'; *)
+        let queue = optimize_smt stack in
+        Queue.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") queue;
 
         output_string out_chan "(check-sat)\n"
 
diff --git a/src/sail.ml b/src/sail.ml
index 7d9d9d3b..575ffbdf 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -423,7 +423,7 @@ let target name out_name ast type_envs =
      let props = Property.find_properties ast in
      Bindings.bindings props |> List.map fst |> IdSet.of_list |> Specialize.add_initial_calls;
      let ast_smt, type_envs = Specialize.(specialize typ_ord_specialization ast type_envs) in
-     (* let ast_smt, type_envs = Specialize.(specialize' 1 int_specialization_with_externs ast_smt type_envs) in *)
+     let ast_smt, type_envs = Specialize.(specialize' 2 int_specialization_with_externs ast_smt type_envs) in
      let name_file =
        match !opt_file_out with
        | Some f -> fun str -> f ^ "_" ^ str ^ ".smt2"
diff --git a/src/specialize.ml b/src/specialize.ml
index 05f675b2..7aee3dd0 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -79,7 +79,7 @@ let int_specialization = {
 
 let int_specialization_with_externs = {
     is_polymorphic = is_int_kopt;
-    instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp _, _) -> true | _ -> false);
+    instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp (Nexp_aux (Nexp_constant _, _)), _) -> true | _ -> false);
     extern_filter = (fun _ -> false)
   }
 
@@ -391,7 +391,7 @@ let specialize_id_valspec spec instantiations id ast =
        let kopts, constraints = quant_split typq in
        let constraints = instantiate_constraints safe_instantiation constraints in
        let constraints = instantiate_constraints reverse constraints in
-       let kopts = List.filter (fun kopt -> not (spec.is_polymorphic kopt)) kopts in
+       let kopts = List.filter (fun kopt -> not (spec.is_polymorphic kopt && KBindings.mem (kopt_kid kopt) safe_instantiation)) kopts in
        let typq =
          if List.length (typ_frees @ int_frees) = 0 && List.length kopts = 0 then
            mk_typquant []
diff --git a/src/value.ml b/src/value.ml
index 82647860..6f5148e4 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -100,7 +100,7 @@ let coerce_bit = function
 let is_bit = function
   | V_bit _ -> true
   | _ -> false
-       
+
 let rec string_of_value = function
   | V_vector vs when List.for_all is_bit vs -> Sail_lib.string_of_bits (List.map coerce_bit vs)
   | V_vector vs -> "[" ^ Util.string_of_list ", " string_of_value vs ^ "]"