summaryrefslogtreecommitdiff
path: root/src/jib/jib_smt_fuzz.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/jib/jib_smt_fuzz.ml')
-rw-r--r--src/jib/jib_smt_fuzz.ml255
1 files changed, 255 insertions, 0 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 11:00:36 +0000