diff options
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/anf.ml | 8 | ||||
| -rw-r--r-- | src/jib/jib_compile.ml | 153 | ||||
| -rw-r--r-- | src/jib/jib_smt.ml | 325 | ||||
| -rw-r--r-- | src/jib/jib_smt.mli | 10 | ||||
| -rw-r--r-- | src/jib/jib_smt_fuzz.ml | 255 | ||||
| -rw-r--r-- | src/jib/jib_ssa.mli | 2 |
6 files changed, 561 insertions, 192 deletions
diff --git a/src/jib/anf.ml b/src/jib/anf.ml index bd4813ed..5165904d 100644 --- a/src/jib/anf.ml +++ b/src/jib/anf.ml @@ -556,8 +556,8 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = | E_lit lit -> mk_aexp (ae_lit lit (typ_of exp)) | E_block [] -> - Util.warn (Reporting.loc_to_string l - ^ "\n\nTranslating empty block (possibly assigning to an uninitialized variable at the end of a block?)"); + Reporting.warn "" l + "Translating empty block (possibly assigning to an uninitialized variable at the end of a block?)"; mk_aexp (ae_lit (L_aux (L_unit, l)) (typ_of exp)) | E_block exps -> let exps, last = split_block l exps in @@ -752,9 +752,5 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = (* Sizeof nodes removed by sizeof rewriting pass *) raise (Reporting.err_unreachable l __POS__ "encountered E_constraint node when converting to ANF") - | E_nondet _ -> - (* We don't compile E_nondet nodes *) - raise (Reporting.err_unreachable l __POS__ "encountered E_nondet node when converting to ANF") - | E_internal_return _ | E_internal_plet _ -> raise (Reporting.err_unreachable l __POS__ "encountered unexpected internal node when converting to ANF") diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index 90c0022d..0518b9c5 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -1184,6 +1184,89 @@ let fix_early_return ret instrs = let letdef_count = ref 0 +let compile_funcl ctx id pat guard exp = + (* Find the function's type. *) + let quant, Typ_aux (fn_typ, _) = + try Env.get_val_spec id ctx.local_env with Type_error _ -> Env.get_val_spec id ctx.tc_env + in + let arg_typs, ret_typ = match fn_typ with + | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ + | _ -> assert false + in + + (* Handle the argument pattern. *) + let fundef_label = label "fundef_fail_" in + let orig_ctx = ctx in + (* The context must be updated before we call ctyp_of_typ on the argument types. *) + let ctx = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in + + let arg_ctyps = List.map (ctyp_of_typ ctx) arg_typs in + let ret_ctyp = ctyp_of_typ ctx ret_typ in + + (* Compile the function arguments as patterns. *) + let arg_setup, compiled_args, arg_cleanup = compile_arg_pats ctx fundef_label pat arg_ctyps in + let ctx = + (* We need the primop analyzer to be aware of the function argument types, so put them in ctx *) + List.fold_left2 (fun ctx (id, _) ctyp -> { ctx with locals = Bindings.add id (Immutable, ctyp) ctx.locals }) ctx compiled_args arg_ctyps + in + + let guard_instrs = match guard with + | Some guard -> + let guard_aexp = ctx.optimize_anf ctx (no_shadow (pat_ids pat) (anf guard)) in + let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard_aexp in + let guard_label = label "guard_" in + let gs = ngensym () in + [iblock ( + [idecl CT_bool gs] + @ guard_setup + @ [guard_call (CL_id (gs, CT_bool))] + @ guard_cleanup + @ [ijump (V_id (gs, CT_bool)) guard_label; + imatch_failure (); + ilabel guard_label] + )] + | None -> [] + in + + (* Optimize and compile the expression to ANF. *) + let aexp = ctx.optimize_anf ctx (no_shadow (pat_ids pat) (anf exp)) in + + let setup, call, cleanup = compile_aexp ctx aexp in + let destructure, destructure_cleanup = + compiled_args |> List.map snd |> combine_destructure_cleanup |> fix_destructure fundef_label + in + + let instrs = arg_setup @ destructure @ guard_instrs @ setup @ [call (CL_id (return, ret_ctyp))] @ cleanup @ destructure_cleanup @ arg_cleanup in + let instrs = fix_early_return (CL_id (return, ret_ctyp)) instrs in + let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in + + if Id.compare (mk_id !opt_debug_function) id = 0 then + let header = + Printf.sprintf "Sail IR for %s %s(%s) : (%s) -> %s" Util.("function" |> red |> clear) (string_of_id id) + (Util.string_of_list ", " string_of_id (List.map fst compiled_args)) + (Util.string_of_list ", " (fun ctyp -> Util.(string_of_ctyp ctyp |> yellow |> clear)) arg_ctyps) + Util.(string_of_ctyp ret_ctyp |> yellow |> clear) + in + prerr_endline (Util.header header (List.length arg_ctyps + 2)); + prerr_endline (Pretty_print_sail.to_string PPrint.(separate_map hardline pp_instr instrs)) + else (); + + if !opt_debug_flow_graphs then + begin + let instrs = Jib_optimize.(instrs |> optimize_unit |> flatten_instrs) in + let root, _, cfg = Jib_ssa.control_flow_graph instrs in + let idom = Jib_ssa.immediate_dominators cfg root in + let _, cfg = Jib_ssa.ssa instrs in + let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") in + Jib_ssa.make_dot out_chan cfg; + close_out out_chan; + let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".dom.gv") in + Jib_ssa.make_dominators_dot out_chan idom cfg; + close_out out_chan; + end; + + [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx + (** Compile a Sail toplevel definition into an IR definition **) let rec compile_def n total ctx def = match def with @@ -1243,76 +1326,16 @@ and compile_def' n total ctx = function | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) -> Util.progress "Compiling " (string_of_id id) n total; + compile_funcl ctx id pat None exp - (* Find the function's type. *) - let quant, Typ_aux (fn_typ, _) = - try Env.get_val_spec id ctx.local_env with Type_error _ -> Env.get_val_spec id ctx.tc_env - in - let arg_typs, ret_typ = match fn_typ with - | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ - | _ -> assert false - in - - (* Handle the argument pattern. *) - let fundef_label = label "fundef_fail_" in - let orig_ctx = ctx in - (* The context must be updated before we call ctyp_of_typ on the argument types. *) - let ctx = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in - - let arg_ctyps = List.map (ctyp_of_typ ctx) arg_typs in - let ret_ctyp = ctyp_of_typ ctx ret_typ in - - (* Compile the function arguments as patterns. *) - let arg_setup, compiled_args, arg_cleanup = compile_arg_pats ctx fundef_label pat arg_ctyps in - let ctx = - (* We need the primop analyzer to be aware of the function argument types, so put them in ctx *) - List.fold_left2 (fun ctx (id, _) ctyp -> { ctx with locals = Bindings.add id (Immutable, ctyp) ctx.locals }) ctx compiled_args arg_ctyps - in - - (* Optimize and compile the expression to ANF. *) - let aexp = no_shadow (pat_ids pat) (anf exp) in - let aexp = ctx.optimize_anf ctx aexp in - - let setup, call, cleanup = compile_aexp ctx aexp in - let destructure, destructure_cleanup = - compiled_args |> List.map snd |> combine_destructure_cleanup |> fix_destructure fundef_label - in - - let instrs = arg_setup @ destructure @ setup @ [call (CL_id (return, ret_ctyp))] @ cleanup @ destructure_cleanup @ arg_cleanup in - let instrs = fix_early_return (CL_id (return, ret_ctyp)) instrs in - let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in - - if Id.compare (mk_id !opt_debug_function) id = 0 then - let header = - Printf.sprintf "Sail IR for %s %s(%s) : (%s) -> %s" Util.("function" |> red |> clear) (string_of_id id) - (Util.string_of_list ", " string_of_id (List.map fst compiled_args)) - (Util.string_of_list ", " (fun ctyp -> Util.(string_of_ctyp ctyp |> yellow |> clear)) arg_ctyps) - Util.(string_of_ctyp ret_ctyp |> yellow |> clear) - in - prerr_endline (Util.header header (List.length arg_ctyps + 2)); - prerr_endline (Pretty_print_sail.to_string PPrint.(separate_map hardline pp_instr instrs)) - else (); - - if !opt_debug_flow_graphs then - begin - let instrs = Jib_optimize.(instrs |> optimize_unit |> flatten_instrs) in - let root, _, cfg = Jib_ssa.control_flow_graph instrs in - let idom = Jib_ssa.immediate_dominators cfg root in - let _, cfg = Jib_ssa.ssa instrs in - let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") in - Jib_ssa.make_dot out_chan cfg; - close_out out_chan; - let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".dom.gv") in - Jib_ssa.make_dominators_dot out_chan idom cfg; - close_out out_chan; - end; - - [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx + | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_when (pat, guard, exp), _)), _)]), _)) -> + Util.progress "Compiling " (string_of_id id) n total; + compile_funcl ctx id pat (Some guard) exp | DEF_fundef (FD_aux (FD_function (_, _, _, []), (l, _))) -> raise (Reporting.err_general l "Encountered function with no clauses") - | DEF_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) -> + | DEF_fundef (FD_aux (FD_function (_, _, _, _ :: _ :: _), (l, _))) -> raise (Reporting.err_general l "Encountered function with multiple clauses") (* All abbreviations should expanded by the typechecker, so we don't diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 0d70695b..07cab66b 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -88,6 +88,7 @@ type ctx = { arg_stack : (int * string) Stack.t; ast : Type_check.tannot defs; events : smt_exp Stack.t EventMap.t ref; + node : int; pathcond : smt_exp Lazy.t; use_string : bool ref; use_real : bool ref @@ -112,6 +113,7 @@ let initial_ctx () = { arg_stack = Stack.create (); ast = Defs []; events = ref EventMap.empty; + node = -1; pathcond = lazy (Bool_lit true); use_string = ref false; use_real = ref false; @@ -210,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) @@ -258,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 @@ -327,7 +335,7 @@ let add_pathcond_event ctx ev = let overflow_check ctx smt = if not !opt_ignore_overflow then ( - Util.warn "Adding overflow check in generated SMT"; + Reporting.warn "Overflow check in generated SMT for" ctx.pragma_l ""; add_event ctx Overflow smt ) @@ -382,7 +390,7 @@ let builtin_gteq = builtin_int_comparison "bvsge" Big_int.greater_equal (* ***** Arithmetic operations: lib/arith.sail ***** *) -(** [force_size n m exp] takes a smt expression assumed to be a +(** [force_size ctx n m exp] takes a smt expression assumed to be a integer (signed bitvector) of length m and forces it to be length n by either sign extending it or truncating it as required *) let force_size ?checked:(checked=true) ctx n m smt = @@ -402,6 +410,16 @@ let force_size ?checked:(checked=true) ctx n m smt = if checked then overflow_check ctx check else (); Extract (n - 1, 0, smt) +(** [unsigned_size ctx n m exp] is much like force_size, but it + assumes that the bitvector is unsigned *) +let unsigned_size ?checked:(checked=true) ctx n m smt = + if n = m then + smt + else if n > m then + Fn ("concat", [bvzero (n - m); smt]) + else + failwith "bad arguments to unsigned_size" + let int_size ctx = function | CT_constant n -> required_width n | CT_fint sz -> sz @@ -420,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 @@ -438,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 -> @@ -493,6 +510,53 @@ let builtin_pow2 ctx v ret_ctyp = | _ -> builtin_type_error ctx "pow2" [v] (Some ret_ctyp) +let builtin_max_int ctx v1 v2 ret_ctyp = + match cval_ctyp v1, cval_ctyp v2 with + | CT_constant n, CT_constant m -> + bvint (int_size ctx ret_ctyp) (max n m) + + | ctyp1, ctyp2 -> + let ret_sz = int_size ctx ret_ctyp in + let smt1 = force_size ctx ret_sz (int_size ctx ctyp1) (smt_cval ctx v1) in + let smt2 = force_size ctx ret_sz (int_size ctx ctyp2) (smt_cval ctx v2) in + Ite (Fn ("bvslt", [smt1; smt2]), + smt2, + smt1) + +let builtin_min_int ctx v1 v2 ret_ctyp = + match cval_ctyp v1, cval_ctyp v2 with + | CT_constant n, CT_constant m -> + bvint (int_size ctx ret_ctyp) (min n m) + + | ctyp1, ctyp2 -> + let ret_sz = int_size ctx ret_ctyp in + let smt1 = force_size ctx ret_sz (int_size ctx ctyp1) (smt_cval ctx v1) in + let smt2 = force_size ctx ret_sz (int_size ctx ctyp2) (smt_cval ctx v2) in + Ite (Fn ("bvslt", [smt1; smt2]), + smt1, + smt2) + +let builtin_eq_bits ctx v1 v2 = + match cval_ctyp v1, cval_ctyp v2 with + | CT_fbits (n, _), CT_fbits (m, _) -> + let o = max n m in + let smt1 = unsigned_size ctx o n (smt_cval ctx v1) in + let smt2 = unsigned_size ctx o n (smt_cval ctx v2) in + Fn ("=", [smt1; smt2]) + + | CT_lbits _, CT_lbits _ -> + Fn ("=", [smt_cval ctx v1; smt_cval ctx v2]) + + | CT_lbits _, CT_fbits (n, _) -> + let smt2 = unsigned_size ctx (lbits_size ctx) n (smt_cval ctx v2) in + Fn ("=", [Fn ("contents", [smt_cval ctx v1]); smt2]) + + | CT_fbits (n, _), CT_lbits _ -> + let smt1 = unsigned_size ctx (lbits_size ctx) n (smt_cval ctx v1) in + Fn ("=", [smt1; Fn ("contents", [smt_cval ctx v2])]) + + | _ -> builtin_type_error ctx "eq_bits" [v1; v2] None + let builtin_zeros ctx v ret_ctyp = match cval_ctyp v, ret_ctyp with | _, CT_fbits (n, _) -> bvzero n @@ -514,7 +578,7 @@ let builtin_ones ctx cval = function Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; bvones (lbits_size ctx)])]); | ret_ctyp -> builtin_type_error ctx "ones" [cval] (Some ret_ctyp) -(* [bvzeint esz cval] (BitVector Zero Extend INTeger), takes a cval +(* [bvzeint ctx esz cval] (BitVector Zero Extend INTeger), takes a cval which must be an integer type (either CT_fint, or CT_lint), and produces a bitvector which is either zero extended or truncated to exactly esz bits. *) @@ -773,11 +837,10 @@ let builtin_replicate_bits ctx v1 v2 ret_ctyp = let smt = smt_cval ctx v1 in Fn ("concat", List.init (Big_int.to_int c) (fun _ -> smt)) - (*| CT_fbits (n, _), ctyp2, CT_lbits _ -> - let len = Fn ("bvmul", [bvint ctx.lbits_index (Big_int.of_int n); - Extract (ctx.lbits_index - 1, 0, smt_cval ctx v2)]) - in - assert false*) + | CT_fbits (n, _), _, CT_fbits (m, _) -> + let smt = smt_cval ctx v1 in + let c = m / n in + Fn ("concat", List.init c (fun _ -> smt)) | _ -> builtin_type_error ctx "replicate_bits" [v1; v2] (Some ret_ctyp) @@ -791,7 +854,12 @@ let builtin_sail_truncate ctx v1 v2 ret_ctyp = assert (Big_int.to_int c = m && m < lbits_size ctx); Extract (Big_int.to_int c - 1, 0, Fn ("contents", [smt_cval ctx v1])) - | _ -> builtin_type_error ctx "sail_truncate" [v2; v2] (Some ret_ctyp) + | CT_fbits (n, _), _, CT_lbits _ -> + let smt1 = unsigned_size ctx (lbits_size ctx) n (smt_cval ctx v1) in + let smt2 = bvzeint ctx ctx.lbits_index v2 in + Fn ("Bits", [smt2; Fn ("bvand", [bvmask ctx smt2; smt1])]) + + | _ -> builtin_type_error ctx "sail_truncate" [v1; v2] (Some ret_ctyp) let builtin_sail_truncateLSB ctx v1 v2 ret_ctyp = match cval_ctyp v1, cval_ctyp v2, ret_ctyp with @@ -927,7 +995,6 @@ let builtin_sqrt_real ctx root v = let smt_builtin ctx name args ret_ctyp = match name, args, ret_ctyp with - | "eq_bits", [v1; v2], CT_bool -> Fn ("=", [smt_cval ctx v1; smt_cval ctx v2]) | "eq_anything", [v1; v2], CT_bool -> Fn ("=", [smt_cval ctx v1; smt_cval ctx v2]) (* lib/flow.sail *) @@ -946,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 @@ -955,6 +1023,9 @@ let smt_builtin ctx name args ret_ctyp = | "abs_int", [v], _ -> builtin_abs_int ctx v ret_ctyp | "pow2", [v], _ -> builtin_pow2 ctx v ret_ctyp + | "max_int", [v1; v2], _ -> builtin_max_int ctx v1 v2 ret_ctyp + | "min_int", [v1; v2], _ -> builtin_min_int ctx v1 v2 ret_ctyp + (* All signed and unsigned bitvector comparisons *) | "slt_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvslt" ctx v1 v2 ret_ctyp | "ult_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvult" ctx v1 v2 ret_ctyp @@ -966,6 +1037,7 @@ let smt_builtin ctx name args ret_ctyp = | "ugteq_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvuge" ctx v1 v2 ret_ctyp (* lib/vector_dec.sail *) + | "eq_bits", [v1; v2], CT_bool -> builtin_eq_bits ctx v1 v2 | "zeros", [v], _ -> builtin_zeros ctx v ret_ctyp | "sail_zeros", [v], _ -> builtin_zeros ctx v ret_ctyp | "ones", [v], _ -> builtin_ones ctx v ret_ctyp @@ -1022,7 +1094,8 @@ let writes = ref (-1) let builtin_write_mem ctx wk addr_size addr data_size data = incr writes; let name = "W" ^ string_of_int !writes in - [Write_mem (name, smt_cval ctx wk, smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr), smt_cval ctx data, smt_ctyp ctx (cval_ctyp data))], + [Write_mem (name, ctx.node, Lazy.force ctx.pathcond, smt_cval ctx wk, + smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr), smt_cval ctx data, smt_ctyp ctx (cval_ctyp data))], Var (name ^ "_ret") let ea_writes = ref (-1) @@ -1030,7 +1103,8 @@ let ea_writes = ref (-1) let builtin_write_mem_ea ctx wk addr_size addr data_size = incr ea_writes; let name = "A" ^ string_of_int !ea_writes in - [Write_mem_ea (name, smt_cval ctx wk, smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr), smt_cval ctx data_size, smt_ctyp ctx (cval_ctyp data_size))], + [Write_mem_ea (name, ctx.node, Lazy.force ctx.pathcond, smt_cval ctx wk, + smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr), smt_cval ctx data_size, smt_ctyp ctx (cval_ctyp data_size))], Enum "unit" let reads = ref (-1) @@ -1038,15 +1112,16 @@ let reads = ref (-1) let builtin_read_mem ctx rk addr_size addr data_size ret_ctyp = incr reads; let name = "R" ^ string_of_int !reads in - [Read_mem (name, smt_ctyp ctx ret_ctyp, smt_cval ctx rk, smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr))], - Var (name ^ "_ret") + [Read_mem (name, ctx.node, Lazy.force ctx.pathcond, smt_ctyp ctx ret_ctyp, smt_cval ctx rk, + smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr))], + Read_res name let excl_results = ref (-1) let builtin_excl_res ctx = incr excl_results; let name = "E" ^ string_of_int !excl_results in - [Excl_res name], + [Excl_res (name, ctx.node, Lazy.force ctx.pathcond)], Var (name ^ "_ret") let barriers = ref (-1) @@ -1054,7 +1129,7 @@ let barriers = ref (-1) let builtin_barrier ctx bk = incr barriers; let name = "B" ^ string_of_int !barriers in - [Barrier (name, smt_cval ctx bk)], + [Barrier (name, ctx.node, Lazy.force ctx.pathcond, smt_cval ctx bk)], Enum "unit" let rec smt_conversion ctx from_ctyp to_ctyp x = @@ -1064,6 +1139,8 @@ let rec smt_conversion ctx from_ctyp to_ctyp x = bvint sz c | CT_constant c, CT_lint -> bvint ctx.lint_size c + | CT_fint sz, CT_lint -> + force_size ctx ctx.lint_size sz x | _, _ -> failwith (Printf.sprintf "Cannot perform conversion from %s to %s" (string_of_ctyp from_ctyp) (string_of_ctyp to_ctyp)) let define_const ctx id ctyp exp = Define_const (zencode_name id, smt_ctyp ctx ctyp, exp) @@ -1295,8 +1372,8 @@ let smt_ssanode ctx cfg preds = | Phi (id, ctyp, ids) -> let get_pi n = match get_vertex cfg n with - | Some ((ssanodes, _), _, _) -> - List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes) + | Some ((ssa_elems, _), _, _) -> + List.concat (List.map (function Pi guards -> guards | _ -> []) ssa_elems) | None -> failwith "Predecessor node does not exist" in let pis = List.map get_pi (IntSet.elements preds) in @@ -1360,8 +1437,8 @@ let rec get_pathcond n cfg ctx = let open Jib_ssa in let get_pi m = match get_vertex cfg m with - | Some ((ssanodes, _), _, _) -> - V_call (Band, List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes)) + | Some ((ssa_elems, _), _, _) -> + V_call (Band, List.concat (List.map (function Pi guards -> guards | _ -> []) ssa_elems)) | None -> failwith "Node does not exist" in match get_vertex cfg n with @@ -1533,7 +1610,7 @@ let smt_instr ctx = end else if not extern then let smt_args = List.map (smt_cval ctx) args in - [define_const ctx id ret_ctyp (Fn (zencode_id function_id, smt_args))] + [define_const ctx id ret_ctyp (Ctor (zencode_id function_id, smt_args))] else failwith ("Unrecognised function " ^ string_of_id function_id) @@ -1569,7 +1646,7 @@ let smt_instr ctx = | instr -> failwith ("Cannot translate: " ^ Pretty_print_sail.to_string (pp_instr instr)) -let smt_cfnode all_cdefs ctx ssanodes = +let smt_cfnode all_cdefs ctx ssa_elems = let open Jib_ssa in function | CF_start inits -> @@ -1619,8 +1696,8 @@ module Make_optimizer(S : Sequence) = struct | Some n -> Hashtbl.replace uses var (n + 1) | None -> Hashtbl.add uses var 1 end - | Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> () - | Fn (f, exps) -> + | Enum _ | Read_res _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> () + | Fn (_, exps) | Ctor (_, exps) -> List.iter uses_in_exp exps | Ite (cond, t, e) -> uses_in_exp cond; uses_in_exp t; uses_in_exp e @@ -1644,19 +1721,20 @@ module Make_optimizer(S : Sequence) = struct end | (Declare_datatypes _ | Declare_tuple _) as def -> Stack.push def stack' - | Write_mem (_, wk, addr, _, data, _) as def -> - uses_in_exp wk; uses_in_exp addr; uses_in_exp data; + | Write_mem (_, _, active, wk, addr, _, data, _) as def -> + uses_in_exp active; uses_in_exp wk; uses_in_exp addr; uses_in_exp data; Stack.push def stack' - | Write_mem_ea (_, wk, addr, _, data_size, _) as def -> - uses_in_exp wk; uses_in_exp addr; uses_in_exp data_size; + | Write_mem_ea (_, _, active, wk, addr, _, data_size, _) as def -> + uses_in_exp active; uses_in_exp wk; uses_in_exp addr; uses_in_exp data_size; Stack.push def stack' - | Read_mem (_, _, rk, addr, _) as def -> - uses_in_exp rk; uses_in_exp addr; + | Read_mem (_, _, active, _, rk, addr, _) as def -> + uses_in_exp active; uses_in_exp rk; uses_in_exp addr; Stack.push def stack' - | Barrier (_, bk) as def -> - uses_in_exp bk; + | Barrier (_, _, active, bk) as def -> + uses_in_exp active; uses_in_exp bk; Stack.push def stack' - | Excl_res _ as def -> + | Excl_res (_, _, active) as def -> + uses_in_exp active; Stack.push def stack' | Assert exp as def -> uses_in_exp exp; @@ -1666,35 +1744,46 @@ module Make_optimizer(S : Sequence) = struct Stack.fold remove_unused () stack; let vars = Hashtbl.create (Stack.length stack') in + let kinds = Hashtbl.create (Stack.length stack') in let seq = S.create () in let constant_propagate = function | Declare_const _ as def -> S.add def seq | Define_const (var, typ, exp) -> - begin match Hashtbl.find_opt uses var, simp_smt_exp vars exp with + let exp = simp_smt_exp vars kinds exp in + begin match Hashtbl.find_opt uses var, simp_smt_exp vars kinds exp with | _, (Bin _ | Bool_lit _) -> Hashtbl.add vars var exp | _, Var _ when !opt_propagate_vars -> Hashtbl.add vars var exp + | _, (Ctor (str, _)) -> + Hashtbl.add kinds var str; + S.add (Define_const (var, typ, exp)) seq | Some 1, _ -> Hashtbl.add vars var exp | Some _, exp -> S.add (Define_const (var, typ, exp)) seq | None, _ -> assert false end - | Write_mem (name, wk, addr, addr_ty, data, data_ty) -> - S.add (Write_mem (name, simp_smt_exp vars wk, simp_smt_exp vars addr, addr_ty, simp_smt_exp vars data, data_ty)) seq - | Write_mem_ea (name, wk, addr, addr_ty, data_size, data_size_ty) -> - S.add (Write_mem_ea (name, simp_smt_exp vars wk, simp_smt_exp vars addr, addr_ty, simp_smt_exp vars data_size, data_size_ty)) seq - | Read_mem (name, typ, rk, addr, addr_typ) -> - S.add (Read_mem (name, typ, simp_smt_exp vars rk, simp_smt_exp vars addr, addr_typ)) seq - | Barrier (name, bk) -> - S.add (Barrier (name, simp_smt_exp vars bk)) seq - | Excl_res name -> - S.add (Excl_res name) seq + | Write_mem (name, node, active, wk, addr, addr_ty, data, data_ty) -> + S.add (Write_mem (name, node, simp_smt_exp vars kinds active, simp_smt_exp vars kinds wk, + simp_smt_exp vars kinds addr, addr_ty, simp_smt_exp vars kinds data, data_ty)) + seq + | Write_mem_ea (name, node, active, wk, addr, addr_ty, data_size, data_size_ty) -> + S.add (Write_mem_ea (name, node, simp_smt_exp vars kinds active, simp_smt_exp vars kinds wk, + simp_smt_exp vars kinds addr, addr_ty, simp_smt_exp vars kinds data_size, data_size_ty)) + seq + | Read_mem (name, node, active, typ, rk, addr, addr_typ) -> + S.add (Read_mem (name, node, simp_smt_exp vars kinds active, typ, simp_smt_exp vars kinds rk, + simp_smt_exp vars kinds addr, addr_typ)) + seq + | Barrier (name, node, active, bk) -> + S.add (Barrier (name, node, simp_smt_exp vars kinds active, simp_smt_exp vars kinds bk)) seq + | Excl_res (name, node, active) -> + S.add (Excl_res (name, node, simp_smt_exp vars kinds active)) seq | Assert exp -> - S.add (Assert (simp_smt_exp vars exp)) seq + S.add (Assert (simp_smt_exp vars kinds exp)) seq | (Declare_datatypes _ | Declare_tuple _) as def -> S.add def seq | Define_fun _ -> assert false @@ -1815,18 +1904,18 @@ let smt_instr_list name ctx all_cdefs instrs = List.iter (fun n -> begin match get_vertex cfg n with | None -> () - | Some ((ssanodes, cfnode), preds, succs) -> + | Some ((ssa_elems, cfnode), preds, succs) -> let muxers = - ssanodes |> List.map (smt_ssanode ctx cfg preds) |> List.concat + ssa_elems |> List.map (smt_ssanode ctx cfg preds) |> List.concat in - let ctx = { ctx with pathcond = lazy (get_pathcond n cfg ctx) } in - let basic_block = smt_cfnode all_cdefs ctx ssanodes cfnode in + let ctx = { ctx with node = n; pathcond = lazy (get_pathcond n cfg ctx) } in + let basic_block = smt_cfnode all_cdefs ctx ssa_elems cfnode in push_smt_defs stack muxers; - push_smt_defs stack basic_block; + push_smt_defs stack basic_block end ) visit_order; - stack + stack, cfg let smt_cdef props lets name_file ctx all_cdefs = function | CDEF_spec (function_id, arg_ctyps, ret_ctyp) when Bindings.mem function_id props -> @@ -1853,7 +1942,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function |> remove_pointless_goto in - let stack = smt_instr_list (string_of_id function_id) ctx all_cdefs instrs in + let stack, _ = smt_instr_list (string_of_id function_id) ctx all_cdefs instrs in let query = smt_query ctx pragma.query in push_smt_defs stack [Assert (Fn ("not", [query]))]; diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli index f6198a37..2680f937 100644 --- a/src/jib/jib_smt.mli +++ b/src/jib/jib_smt.mli @@ -52,6 +52,7 @@ open Ast open Ast_util open Jib open Jib_util +open Jib_ssa open Smtlib val opt_ignore_overflow : bool ref @@ -59,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 @@ -95,8 +98,9 @@ type ctx = { src/property.ml for the event types *) events : smt_exp Stack.t EventMap.t ref; (** When generating SMT for an instruction pathcond will contain - the global path conditional of the containing block in the + the global path conditional of the containing block/node in the control flow graph *) + node : int; pathcond : smt_exp Lazy.t; (** Set if we need to use strings or real numbers in the generated SMT, which then requires set-logic ALL or similar depending on @@ -116,7 +120,9 @@ val compile : Type_check.Env.t -> Type_check.tannot defs -> cdef list * ctx val smt_header : ctx -> cdef list -> smt_def list -val smt_instr_list : string -> ctx -> cdef list -> instr list -> smt_def Stack.t +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 type 'a t 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/jib/jib_ssa.mli b/src/jib/jib_ssa.mli index dadb20fd..3357bc11 100644 --- a/src/jib/jib_ssa.mli +++ b/src/jib/jib_ssa.mli @@ -61,7 +61,7 @@ val make : initial_size:int -> unit -> 'a array_graph module IntSet : Set.S with type elt = int val get_cond : 'a array_graph -> int -> Jib.cval - + val get_vertex : 'a array_graph -> int -> ('a * IntSet.t * IntSet.t) option val iter_graph : ('a -> IntSet.t -> IntSet.t -> unit) -> 'a array_graph -> unit |