SMT: Add a fuzzing tool for the SMT builtins

7 files changed, 341 insertions, 67 deletions

diff --git a/src/interpreter.ml b/src/interpreter.ml
index db4f45f6..def0963f 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -549,7 +549,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
      wrap (E_block (E_aux (E_assign (lexp, exp), annot) :: body))
   | E_var (lexp, exp, body) ->
      wrap (E_block [E_aux (E_assign (lexp, exp), annot); body])
-     
+
   | E_assign (lexp, exp) when not (is_value exp) -> step exp >>= fun exp' -> wrap (E_assign (lexp, exp'))
   | E_assign (LEXP_aux (LEXP_memory (id, args), _), exp) -> wrap (E_app (id, args @ [exp]))
   | E_assign (LEXP_aux (LEXP_field (lexp, id), ul), exp) ->
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 4217ef8e..56029c5f 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -212,7 +212,7 @@ let bvpint sz x =
     let padding_size = sz - String.length bin in
     if padding_size < 0 then
       raise (Reporting.err_general Parse_ast.Unknown
-               (Printf.sprintf "Count not create a %d-bit integer with value %s.\nTry increasing the maximum integer size"
+               (Printf.sprintf "Could not create a %d-bit integer with value %s.\nTry increasing the maximum integer size"
                   sz (Big_int.to_string x)));
     let padding = String.make (sz - String.length bin) '0' in
     Bin (padding ^ bin)
@@ -260,65 +260,71 @@ let zencode_ctor ctor_id unifiers =
      Util.zencode_string (string_of_id ctor_id ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)
 
 let rec smt_cval ctx cval =
-  match cval with
-  | V_lit (vl, ctyp) -> smt_value ctx vl ctyp
-  | V_id (Name (id, _) as ssa_id, _) ->
-     begin match Type_check.Env.lookup_id id ctx.tc_env with
-     | Enum _ -> Enum (zencode_id id)
-     | _ -> Var (zencode_name ssa_id)
-     end
-  | V_id (ssa_id, _) -> Var (zencode_name ssa_id)
-  | V_call (Neq, [cval1; cval2]) ->
-     Fn ("not", [Fn ("=", [smt_cval ctx cval1; smt_cval ctx cval2])])
-  | V_call (Bvor, [cval1; cval2]) ->
-     Fn ("bvor", [smt_cval ctx cval1; smt_cval ctx cval2])
-  | V_call (Bit_to_bool, [cval]) ->
-     Fn ("=", [smt_cval ctx cval; Bin "1"])
-  | V_call (Bnot, [cval]) ->
-     Fn ("not", [smt_cval ctx cval])
-  | V_call (Band, cvals) ->
-     smt_conj (List.map (smt_cval ctx) cvals)
-  | V_call (Bor, cvals) ->
-     smt_disj (List.map (smt_cval ctx) cvals)
-  | V_ctor_kind (union, ctor_id, unifiers, _) ->
-     Fn ("not", [Tester (zencode_ctor ctor_id unifiers, smt_cval ctx union)])
-  | V_ctor_unwrap (ctor_id, union, unifiers, _) ->
-     Fn ("un" ^ zencode_ctor ctor_id unifiers, [smt_cval ctx union])
-  | V_field (union, field) ->
-     begin match cval_ctyp union with
-     | CT_struct (struct_id, _) ->
-        Fn (zencode_upper_id struct_id ^ "_" ^ field, [smt_cval ctx union])
-     | _ -> failwith "Field for non-struct type"
-     end
-  | V_struct (fields, ctyp) ->
-     begin match ctyp with
-     | CT_struct (struct_id, field_ctyps) ->
-        let set_field (field, cval) =
-          match Util.assoc_compare_opt Id.compare field field_ctyps with
-          | None -> failwith "Field type not found"
-          | Some ctyp when ctyp_equal (cval_ctyp cval) ctyp ->
-             smt_cval ctx cval
-          | _ -> failwith "Type mismatch when generating struct for SMT"
-        in
-        Fn (zencode_upper_id struct_id, List.map set_field fields)
-     | _ -> failwith "Struct does not have struct type"
-     end
-  | V_tuple_member (frag, len, n) ->
-     ctx.tuple_sizes := IntSet.add len !(ctx.tuple_sizes);
-     Fn (Printf.sprintf "tup_%d_%d" len n, [smt_cval ctx frag])
-  | V_ref (Name (id, _), _) ->
-     let rmap = CTMap.filter (fun ctyp regs -> List.exists (fun reg -> Id.compare reg id = 0) regs) ctx.register_map in
-     assert (CTMap.cardinal rmap = 1);
-     begin match CTMap.min_binding_opt rmap with
-     | Some (ctyp, regs) ->
-        begin match Util.list_index (fun reg -> Id.compare reg id = 0) regs with
-        | Some i ->
-           bvint (required_width (Big_int.of_int (List.length regs))) (Big_int.of_int i)
-        | None -> assert false
+  match cval_ctyp cval with
+  | CT_constant n ->
+     bvint (required_width n) n
+  | _ ->
+     match cval with
+     | V_lit (vl, ctyp) -> smt_value ctx vl ctyp
+     | V_id (Name (id, _) as ssa_id, _) ->
+        begin match Type_check.Env.lookup_id id ctx.tc_env with
+        | Enum _ -> Enum (zencode_id id)
+        | _ -> Var (zencode_name ssa_id)
         end
-     | _ -> assert false
-     end
-  | cval -> failwith ("Unrecognised cval " ^ string_of_cval cval)
+     | V_id (ssa_id, _) -> Var (zencode_name ssa_id)
+     | V_call (Neq, [cval1; cval2]) ->
+        Fn ("not", [Fn ("=", [smt_cval ctx cval1; smt_cval ctx cval2])])
+     | V_call (Bvor, [cval1; cval2]) ->
+        Fn ("bvor", [smt_cval ctx cval1; smt_cval ctx cval2])
+     | V_call (Bit_to_bool, [cval]) ->
+        Fn ("=", [smt_cval ctx cval; Bin "1"])
+     | V_call (Eq, [cval1; cval2]) ->
+        Fn ("=", [smt_cval ctx cval1; smt_cval ctx cval2])
+     | V_call (Bnot, [cval]) ->
+        Fn ("not", [smt_cval ctx cval])
+     | V_call (Band, cvals) ->
+        smt_conj (List.map (smt_cval ctx) cvals)
+     | V_call (Bor, cvals) ->
+        smt_disj (List.map (smt_cval ctx) cvals)
+     | V_ctor_kind (union, ctor_id, unifiers, _) ->
+        Fn ("not", [Tester (zencode_ctor ctor_id unifiers, smt_cval ctx union)])
+     | V_ctor_unwrap (ctor_id, union, unifiers, _) ->
+        Fn ("un" ^ zencode_ctor ctor_id unifiers, [smt_cval ctx union])
+     | V_field (union, field) ->
+        begin match cval_ctyp union with
+        | CT_struct (struct_id, _) ->
+           Fn (zencode_upper_id struct_id ^ "_" ^ field, [smt_cval ctx union])
+        | _ -> failwith "Field for non-struct type"
+        end
+     | V_struct (fields, ctyp) ->
+        begin match ctyp with
+        | CT_struct (struct_id, field_ctyps) ->
+           let set_field (field, cval) =
+             match Util.assoc_compare_opt Id.compare field field_ctyps with
+             | None -> failwith "Field type not found"
+             | Some ctyp when ctyp_equal (cval_ctyp cval) ctyp ->
+                smt_cval ctx cval
+             | _ -> failwith "Type mismatch when generating struct for SMT"
+           in
+           Fn (zencode_upper_id struct_id, List.map set_field fields)
+        | _ -> failwith "Struct does not have struct type"
+        end
+     | V_tuple_member (frag, len, n) ->
+        ctx.tuple_sizes := IntSet.add len !(ctx.tuple_sizes);
+        Fn (Printf.sprintf "tup_%d_%d" len n, [smt_cval ctx frag])
+     | V_ref (Name (id, _), _) ->
+        let rmap = CTMap.filter (fun ctyp regs -> List.exists (fun reg -> Id.compare reg id = 0) regs) ctx.register_map in
+        assert (CTMap.cardinal rmap = 1);
+        begin match CTMap.min_binding_opt rmap with
+        | Some (ctyp, regs) ->
+           begin match Util.list_index (fun reg -> Id.compare reg id = 0) regs with
+           | Some i ->
+              bvint (required_width (Big_int.of_int (List.length regs))) (Big_int.of_int i)
+           | None -> assert false
+           end
+        | _ -> assert false
+        end
+     | cval -> failwith ("Unrecognised cval " ^ string_of_cval cval)
 
 let add_event ctx ev smt =
   let stack = event_stack ctx ev in
@@ -432,13 +438,6 @@ let builtin_arith fn big_int_fn padding ctx v1 v2 ret_ctyp =
   | CT_constant c1, CT_constant c2, _ ->
      bvint (int_size ctx ret_ctyp) (big_int_fn c1 c2)
 
-  | ctyp, CT_constant c, _ ->
-     let n = int_size ctx ctyp in
-     force_size ctx (int_size ctx ret_ctyp) n (Fn (fn, [smt_cval ctx v1; bvint n c]))
-  | CT_constant c, ctyp, _ ->
-     let n = int_size ctx ctyp in
-     force_size ctx (int_size ctx ret_ctyp) n (Fn (fn, [bvint n c; smt_cval ctx v2]))
-
   | ctyp1, ctyp2, _ ->
      let ret_sz = int_size ctx ret_ctyp in
      let smt1 = smt_cval ctx v1 in
@@ -450,6 +449,12 @@ let builtin_add_int = builtin_arith "bvadd" Big_int.add (fun x -> x + 1)
 let builtin_sub_int = builtin_arith "bvsub" Big_int.sub (fun x -> x + 1)
 let builtin_mult_int = builtin_arith "bvmul" Big_int.mul (fun x -> x * 2)
 
+let builtin_sub_nat ctx v1 v2 ret_ctyp =
+  let result = builtin_arith "bvsub" Big_int.sub (fun x -> x + 1) ctx v1 v2 ret_ctyp in
+  Ite (Fn ("bvslt", [result; bvint (int_size ctx ret_ctyp) Big_int.zero]),
+       bvint (int_size ctx ret_ctyp) Big_int.zero,
+       result)
+
 let builtin_negate_int ctx v ret_ctyp =
   match cval_ctyp v, ret_ctyp with
   | _, CT_constant c ->
@@ -1008,6 +1013,7 @@ let smt_builtin ctx name args ret_ctyp =
   (* lib/arith.sail *)
   | "add_int", [v1; v2], _ -> builtin_add_int ctx v1 v2 ret_ctyp
   | "sub_int", [v1; v2], _ -> builtin_sub_int ctx v1 v2 ret_ctyp
+  | "sub_nat", [v1; v2], _ -> builtin_sub_nat ctx v1 v2 ret_ctyp
   | "mult_int", [v1; v2], _ -> builtin_mult_int ctx v1 v2 ret_ctyp
   | "neg_int", [v], _ -> builtin_negate_int ctx v ret_ctyp
   | "shl_int", [v1; v2], _ -> builtin_shl_int ctx v1 v2 ret_ctyp
diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli
index 910388b6..2680f937 100644
--- a/src/jib/jib_smt.mli
+++ b/src/jib/jib_smt.mli
@@ -60,6 +60,8 @@ val opt_auto : bool ref
 val opt_debug_graphs : bool ref
 val opt_propagate_vars : bool ref
 
+val zencode_name : name -> string
+
 module IntSet : Set.S with type elt = int
 module EventMap : Map.S with type key = Property.event
 
@@ -118,6 +120,8 @@ val compile : Type_check.Env.t -> Type_check.tannot defs -> cdef list * ctx
 
 val smt_header : ctx -> cdef list -> smt_def list
 
+val smt_query : ctx -> Property.query -> smt_exp
+
 val smt_instr_list : string -> ctx -> cdef list -> instr list -> smt_def Stack.t * (ssa_elem list * cf_node) Jib_ssa.array_graph
 
 module type Sequence = sig
diff --git a/src/jib/jib_smt_fuzz.ml b/src/jib/jib_smt_fuzz.ml
new file mode 100644
index 00000000..37ae753f
--- /dev/null
+++ b/src/jib/jib_smt_fuzz.ml
@@ -0,0 +1,255 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Ast
+open Ast_util
+open Jib
+open Jib_smt
+open Jib_util
+open Smtlib
+
+let gen_value (Typ_aux (aux, _) as typ) =
+  match aux with
+  | Typ_id id when string_of_id id = "bit" ->
+     Some (
+         if Random.bool () then
+           mk_lit_exp L_zero, V_lit (VL_bit Sail2_values.B0, CT_bit)
+         else
+           mk_lit_exp L_one, V_lit (VL_bit Sail2_values.B1, CT_bit)
+       )
+
+  | Typ_app (id, _) when string_of_id id = "atom_bool" ->
+     Some (
+         if Random.bool () then
+           mk_lit_exp L_true, V_lit (VL_bool true, CT_bool)
+         else
+           mk_lit_exp L_false, V_lit (VL_bool false, CT_bool)
+       )
+
+  | Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_constant n, _)), _)]) when string_of_id id = "atom" ->
+     Some (
+         if Random.bool () then
+           mk_lit_exp (L_num n), V_lit (VL_int n, CT_constant n)
+         else
+           let n = Big_int.of_int (Random.int 32) in
+           let n = if Random.bool () then n else Big_int.negate n in
+           match Random.int 3 with
+           | 0 ->
+              mk_lit_exp (L_num n), V_lit (VL_int n, CT_fint 64)
+           | 1 ->
+              mk_lit_exp (L_num n), V_lit (VL_int n, CT_lint)
+           | _ ->
+              mk_lit_exp (L_num n), V_lit (VL_int n, CT_constant n)
+       )
+
+  | Typ_app (id, _) when string_of_id id = "atom" ->
+     Some (
+         let n = Big_int.of_int (Random.int 32) in
+         let n = if Random.bool () then n else Big_int.negate n in
+         match Random.int 3 with
+         | 0 ->
+            mk_lit_exp (L_num n), V_lit (VL_int n, CT_fint 64)
+         | 1 ->
+            mk_lit_exp (L_num n), V_lit (VL_int n, CT_lint)
+         | _ ->
+            mk_lit_exp (L_num n), V_lit (VL_int n, CT_constant n)
+       )
+
+  | _ ->
+     None
+
+let rec gen_ret_ctyp (Typ_aux (aux, _)) =
+  match aux with
+  | Typ_id id when string_of_id id = "bool" ->
+     Some CT_bool
+  | Typ_app (id, _) when string_of_id id = "atom" ->
+     if Random.bool () then Some (CT_fint 64) else Some CT_lint
+  | Typ_app (id, _) when string_of_id id = "atom_bool" ->
+     Some CT_bool
+  | Typ_id id when string_of_id id = "nat" ->
+     Some CT_lint
+  | Typ_id id when string_of_id id = "int" ->
+     Some CT_lint
+  | Typ_exist (_, _, typ) ->
+     gen_ret_ctyp typ
+  | _ -> None
+
+let gen_assertion ctyp value id =
+  let open Smtlib in
+  let open Value in
+  match ctyp, value with
+  | CT_bool, V_bool b ->
+     [icopy Parse_ast.Unknown (CL_id (Return (-1), CT_bool)) (V_call (Eq, [V_id (id, ctyp); V_lit (VL_bool b, ctyp)]))]
+  | CT_lint, V_int n ->
+     [icopy Parse_ast.Unknown (CL_id (Return (-1), CT_bool)) (V_call (Eq, [V_id (id, ctyp); V_lit (VL_int n, ctyp)]))]
+  | CT_fint 64, V_int n ->
+     [icopy Parse_ast.Unknown (CL_id (Return (-1), CT_bool)) (V_call (Eq, [V_id (id, ctyp); V_lit (VL_int n, ctyp)]))]
+  | _ ->
+     assert false
+
+let rec run frame =
+  match frame with
+  | Interpreter.Done (state, v) -> Some v
+  | Interpreter.Step (lazy_str, _, _, _) ->
+     run (Interpreter.eval_frame frame)
+  | Interpreter.Break frame ->
+     run (Interpreter.eval_frame frame)
+  | Interpreter.Fail (_, _, _, _, msg) ->
+     None
+  | Interpreter.Effect_request (out, state, stack, eff) ->
+     run (Interpreter.default_effect_interp state eff)
+
+exception Skip_iteration of string;;
+
+let fuzz_cdef ctx all_cdefs = function
+  | CDEF_spec (id, arg_ctyps, ret_ctyp) when not (string_of_id id = "and_bool" || string_of_id id = "or_bool") ->
+     let open Type_check in
+     let open Interpreter in
+     if Env.is_extern id ctx.tc_env "smt" then (
+       let extern = Env.get_extern id ctx.tc_env "smt" in
+       let typq, (Typ_aux (aux, _) as typ) = Env.get_val_spec id ctx.tc_env in
+       let istate = initial_state ctx.ast ctx.tc_env Value.primops in
+       let header = smt_header ctx all_cdefs in
+       prerr_endline (Util.("Fuzz: " |> cyan |> clear) ^ string_of_id id ^ " = \"" ^ extern ^ "\" : " ^ string_of_typ typ);
+
+       match aux with
+       | Typ_fn (arg_typs, ret_typ, _) ->
+          let iterations = ref 0 in
+          let max_iterations = 100 in
+          let continue = ref true in
+          let skipped = ref 0 in
+
+          while !iterations < max_iterations && !continue do
+            begin try
+              begin match List.map gen_value arg_typs |> Util.option_all, gen_ret_ctyp ret_typ with
+              | Some values, Some ret_ctyp ->
+                 let ctx = { ctx with events = ref EventMap.empty; pragma_l = id_loc id; arg_stack = Stack.create () } in
+                 let call =
+                   try mk_exp (E_app (id, List.map fst values)) |> infer_exp ctx.tc_env with
+                   | Type_error _ -> raise (Skip_iteration ("Type error for: " ^ Util.string_of_list ", " string_of_exp (List.map fst values)))
+                 in
+                 let result =
+                   match run (Step (lazy "", istate, return call, [])) with
+                   | Some v -> v
+                   | None ->
+                      raise (Skip_iteration ("Interpreter error for: " ^ Util.string_of_list ", " string_of_exp (List.map fst values)))
+                 in
+
+                 let jib =
+                   let gs = Jib_compile.ngensym () in
+                   [ifuncall (CL_id (gs, ret_ctyp)) id (List.map snd values)]
+                   @ gen_assertion ret_ctyp result gs
+                   @ [iend ()]
+                 in
+                 let smt_defs =
+                   try fst (smt_instr_list extern ctx all_cdefs jib) with
+                   | _ ->
+                      raise (Skip_iteration ("SMT error for: " ^ Util.string_of_list ", " string_of_exp (List.map fst values)))
+                 in
+                 let smt_defs = Stack.fold (fun xs x -> x :: xs) [] smt_defs in
+                 let query = Assert (Fn ("not", [smt_query ctx Property.default_query])) in
+
+                 let fname, out_chan = Filename.open_temp_file (Util.zencode_string (string_of_id id)) ".smt2" in
+                 if !(ctx.use_string) || !(ctx.use_real) then
+                   output_string out_chan "(set-logic ALL)\n"
+                 else
+                   output_string out_chan "(set-logic QF_AUFBVDT)\n";
+                 List.iter (fun smt -> output_string out_chan (string_of_smt_def smt ^ "\n")) (header @ smt_defs @ [query]);
+                 output_string out_chan "(check-sat)\n";
+                 close_out out_chan;
+
+                 let in_chan = Printf.ksprintf Unix.open_process_in "cvc4 --lang=smt2.6 %s" fname in
+                 let lines = ref [] in
+                 begin
+                   try
+                     while true do
+                       lines := input_line in_chan :: !lines
+                     done
+                   with
+                   | End_of_file -> ()
+                 end;
+                 let _ = Unix.close_process_in in_chan in
+                 let solver_output = List.rev !lines |> String.concat "\n" |> parse_sexps in
+                 begin match solver_output with
+                 | [Atom "unsat"] -> ()
+                 | _ ->
+                    prerr_endline (Util.("SMT check failed:" |> red |> clear)
+                                   ^ "\n" ^ Util.string_of_list ", " string_of_exp (List.map fst values)
+                                   ^ " : " ^ Util.string_of_list ", " string_of_ctyp (List.map (fun v -> cval_ctyp (snd v)) values)
+                                   ^ " -> " ^ string_of_ctyp ret_ctyp
+                                   ^ " = " ^ Value.string_of_value result
+                                   ^ "\nFilename: " ^ fname);
+                    continue := false
+                 end
+              | _, _ ->
+                 prerr_endline Util.("Could not generate values for function types" |> yellow |> clear);
+                 continue := false
+              end
+            with
+            | Skip_iteration str ->
+               incr skipped
+            end;
+            incr iterations
+          done;
+          if !continue then
+            prerr_endline (Util.("ok" |> green |> clear) ^ Printf.sprintf " (%d/%d skipped)" !skipped max_iterations)
+
+       | _ ->
+          raise (Reporting.err_general (id_loc id) "Function prototype must have a function type")
+     ) else ()
+
+  | _ -> ()
+
+let fuzz seed env ast =
+  Random.init seed;
+
+  let cdefs, ctx = compile env ast in
+
+  List.iter (fuzz_cdef ctx cdefs) cdefs
diff --git a/src/property.mli b/src/property.mli
index 8005f91a..66a732b9 100644
--- a/src/property.mli
+++ b/src/property.mli
@@ -104,6 +104,8 @@ type query =
    | Q_and of query list
    | Q_or of query list
 
+val default_query : query
+
 type pragma = {
     query : query;
     litmus : string list;
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 84f23c77..cbbd72d4 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -5024,6 +5024,7 @@ let rewrites_target tgt =
   | "c" -> rewrites_c
   | "ir" -> rewrites_c @ [("properties", [])]
   | "smt" -> rewrites_c @ [("properties", [])]
+  | "smtfuzz" -> rewrites_c @ [("properties", [])]
   | "sail" -> []
   | "latex" -> []
   | "interpreter" -> rewrites_interpreter
diff --git a/src/sail.ml b/src/sail.ml
index 19db5289..eae7c4cf 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -348,6 +348,9 @@ let options = Arg.align ([
   ( "-dprofile",
     Arg.Set Profile.opt_profile,
     " (debug) provide basic profiling information for rewriting passes within Sail");
+  ( "-dsmtfuzz",
+    set_target "smtfuzz",
+    " (debug) fuzz sail SMT builtins");
   ( "-v",
     Arg.Set opt_print_version,
     " print version");
@@ -479,6 +482,9 @@ let target name out_name ast type_envs =
      flush output_chan;
      if close then close_out output_chan else ()
 
+  | Some "smtfuzz" ->
+     Jib_smt_fuzz.fuzz 0 type_envs ast
+
   | Some "smt" ->
      let open Ast_util in
      let props = Property.find_properties ast in