diff --git a/src/lib/smt_exp.ml b/src/lib/smt_exp.ml index b78ea60fc..70988a0b9 100644 --- a/src/lib/smt_exp.ml +++ b/src/lib/smt_exp.ml @@ -237,7 +237,7 @@ let rec simp vars exp = | Tester (ctor, exp) -> Tester (ctor, simp vars exp) | Unwrap (ctor, b, exp) -> Unwrap (ctor, b, simp vars exp) | Field (struct_id, field_id, exp) -> Field (struct_id, field_id, simp vars exp) - | Empty_list | Bool_lit _ | Bitvec_lit _ | Real_lit _ | String_lit _ | Enum _ -> exp + | Empty_list | Bool_lit _ | Bitvec_lit _ | Real_lit _ | String_lit _ | Enum _ | Hd _ | Tl _ -> exp type smt_def = | Define_fun of string * (string * smt_typ) list * smt_typ * smt_exp @@ -286,6 +286,7 @@ let rec pp_smt_exp = | Tester (kind, exp) -> parens (string (Printf.sprintf "(_ is %s)" kind) ^^ space ^^ pp_smt_exp exp) | SignExtend (_, i, exp) -> parens (string (Printf.sprintf "(_ sign_extend %d)" i) ^^ space ^^ pp_smt_exp exp) | ZeroExtend (_, i, exp) -> parens (string (Printf.sprintf "(_ zero_extend %d)" i) ^^ space ^^ pp_smt_exp exp) + | Store (_, _, arr, index, x) -> parens (string "store" ^^ space ^^ separate_map space pp_smt_exp [arr; index; x]) let pp_smt_def = let open PPrint in @@ -324,109 +325,6 @@ let string_of_smt_def def = Pretty_print_sail.to_string (pp_smt_def def) form of s-expression based representation. Therefore we define a simple parser for s-expressions using monadic parser combinators. *) -type sexpr = List of sexpr list | Atom of string - -let rec string_of_sexpr = function - | List sexprs -> "(" ^ Util.string_of_list " " string_of_sexpr sexprs ^ ")" - | Atom str -> str - -open Parser_combinators - -let lparen = token (function Str.Delim "(" -> Some () | _ -> None) -let rparen = token (function Str.Delim ")" -> Some () | _ -> None) -let atom = token (function Str.Text str -> Some str | _ -> None) - -let rec sexp toks = - let parse = - pchoose - (atom >>= fun str -> preturn (Atom str)) - ( lparen >>= fun _ -> - plist sexp >>= fun xs -> - rparen >>= fun _ -> preturn (List xs) - ) - in - parse toks - -let parse_sexps input = - let delim = Str.regexp "[ \n\t]+\\|(\\|)" in - let tokens = Str.full_split delim input in - let non_whitespace = function Str.Delim d when String.trim d = "" -> false | _ -> true in - let tokens = List.filter non_whitespace tokens in - match plist sexp tokens with Ok (result, _) -> Some result | Fail -> None - -let parse_sexpr_int width = function - | List [Atom "_"; Atom v; Atom m] when int_of_string m = width && String.length v > 2 && String.sub v 0 2 = "bv" -> - let v = String.sub v 2 (String.length v - 2) in - Some (Big_int.of_string v) - | Atom v when String.length v > 2 && String.sub v 0 2 = "#b" -> - let v = String.sub v 2 (String.length v - 2) in - Some (Big_int.of_string ("0b" ^ v)) - | Atom v when String.length v > 2 && String.sub v 0 2 = "#x" -> - let v = String.sub v 2 (String.length v - 2) in - Some (Big_int.of_string ("0x" ^ v)) - | _ -> None - -let rec value_of_sexpr sexpr = - let open Jib in - let open Value in - function - | CT_fbits width -> begin - match parse_sexpr_int width sexpr with - | Some value -> mk_vector (Sail_lib.get_slice_int' (width, value, 0)) - | None -> failwith ("Cannot parse sexpr as bitvector: " ^ string_of_sexpr sexpr) - end - | CT_struct (_, fields) -> begin - match sexpr with - | List (Atom name :: smt_fields) -> - V_record - (List.fold_left2 - (fun m (field_id, ctyp) sexpr -> StringMap.add (string_of_id field_id) (value_of_sexpr sexpr ctyp) m) - StringMap.empty fields smt_fields - ) - | _ -> failwith ("Cannot parse sexpr as struct " ^ string_of_sexpr sexpr) - end - | CT_enum (_, members) -> begin - match sexpr with - | Atom name -> begin - match List.find_opt (fun member -> Util.zencode_string (string_of_id member) = name) members with - | Some member -> V_member (string_of_id member) - | None -> - failwith - ("Could not find enum member for " ^ name ^ " in " ^ Util.string_of_list ", " string_of_id members) - end - | _ -> failwith ("Cannot parse sexpr as enum " ^ string_of_sexpr sexpr) - end - | CT_bool -> begin - match sexpr with - | Atom "true" -> V_bool true - | Atom "false" -> V_bool false - | _ -> failwith ("Cannot parse sexpr as bool " ^ string_of_sexpr sexpr) - end - | CT_fint width -> begin - match parse_sexpr_int width sexpr with - | Some value -> V_int value - | None -> failwith ("Cannot parse sexpr as fixed-width integer: " ^ string_of_sexpr sexpr) - end - | ctyp -> failwith ("Unsupported type in sexpr: " ^ Jib_util.string_of_ctyp ctyp) - -let rec find_arg id ctyp arg_smt_names = function - | List [Atom "define-fun"; Atom str; List []; _; value] :: _ - when Util.assoc_compare_opt Id.compare id arg_smt_names = Some (Some str) -> - (id, value_of_sexpr value ctyp) - | _ :: sexps -> find_arg id ctyp arg_smt_names sexps - | [] -> (id, V_unit) - -let build_counterexample args arg_ctyps arg_smt_names model = - List.map2 (fun id ctyp -> find_arg id ctyp arg_smt_names model) args arg_ctyps - -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) - type counterexample_solver = Cvc5 | Cvc4 | Z3 let counterexample_command = function Cvc5 -> "cvc5 --lang=smt2.6" | Cvc4 -> "cvc4 --lang=smt2.6" | Z3 -> "z3" @@ -434,55 +332,169 @@ let counterexample_command = function Cvc5 -> "cvc5 --lang=smt2.6" | Cvc4 -> "cv let counterexample_solver_from_name name = match String.lowercase_ascii name with "cvc4" -> Some Cvc4 | "cvc5" -> Some Cvc5 | "z3" -> Some Z3 | _ -> None -let check_counterexample ~env ~ast ~solver ~file_name ~function_id ~args ~arg_ctyps ~arg_smt_names = - let open Printf in - let open Ast in - print_endline ("Checking counterexample: " ^ file_name); - let in_chan = ksprintf Unix.open_process_in "%s %s" (counterexample_command solver) file_name in - let lines = ref [] in - begin - try - while true do - lines := input_line in_chan :: !lines - done - with End_of_file -> () - end; - let solver_output = List.rev !lines |> String.concat "\n" in - begin - match parse_sexps solver_output with - | Some (Atom "sat" :: (List (Atom "model" :: model) | List model) :: _) -> - let open Value in - let open Interpreter in - print_endline (sprintf "Solver found counterexample: %s" Util.("ok" |> green |> clear)); - let counterexample = build_counterexample args arg_ctyps arg_smt_names model in - List.iter (fun (id, v) -> print_endline (" " ^ string_of_id id ^ " -> " ^ string_of_value v)) counterexample; - let istate = initial_state ast env !primops in - let annot = (Parse_ast.Unknown, Type_check.mk_tannot env bool_typ) in - let call = - E_aux - ( E_app - ( function_id, - List.map - (fun (_, v) -> E_aux (E_internal_value v, (Parse_ast.Unknown, Type_check.empty_tannot))) - counterexample - ), - annot - ) - in - let result = run (Step (lazy "", istate, return call, [])) in - begin - match result with - | Some (V_bool false) | None -> - ksprintf print_endline "Replaying counterexample: %s" Util.("ok" |> green |> clear) - | _ -> () - end - | Some (Atom "unsat" :: _) -> - print_endline "Solver could not find counterexample"; - print_endline "Solver output:"; - print_endline solver_output - | _ -> - print_endline "Unexpected solver output:"; - print_endline solver_output - end; - let _ = Unix.close_process_in in_chan in - () +module type COUNTEREXAMPLE_CONFIG = sig + val max_unknown_integer_width : int +end + +module Counterexample (Config : COUNTEREXAMPLE_CONFIG) = struct + type sexpr = List of sexpr list | Atom of string + + let rec string_of_sexpr = function + | List sexprs -> "(" ^ Util.string_of_list " " string_of_sexpr sexprs ^ ")" + | Atom str -> str + + open Parser_combinators + + let lparen = token (function Str.Delim "(" -> Some () | _ -> None) + let rparen = token (function Str.Delim ")" -> Some () | _ -> None) + let atom = token (function Str.Text str -> Some str | _ -> None) + + let rec sexp toks = + let parse = + pchoose + (atom >>= fun str -> preturn (Atom str)) + ( lparen >>= fun _ -> + plist sexp >>= fun xs -> + rparen >>= fun _ -> preturn (List xs) + ) + in + parse toks + + let parse_sexps input = + let delim = Str.regexp "[ \n\t]+\\|(\\|)" in + let tokens = Str.full_split delim input in + let non_whitespace = function Str.Delim d when String.trim d = "" -> false | _ -> true in + let tokens = List.filter non_whitespace tokens in + match plist sexp tokens with Ok (result, _) -> Some result | Fail -> None + + let parse_sexpr_int width = function + | List [Atom "_"; Atom v; Atom m] when int_of_string m = width && String.length v > 2 && String.sub v 0 2 = "bv" -> + let v = String.sub v 2 (String.length v - 2) in + Some (Big_int.of_string v) + | Atom v when String.length v > 2 && String.sub v 0 2 = "#b" -> + let v = String.sub v 2 (String.length v - 2) in + Some (Big_int.of_string ("0b" ^ v)) + | Atom v when String.length v > 2 && String.sub v 0 2 = "#x" -> + let v = String.sub v 2 (String.length v - 2) in + Some (Big_int.of_string ("0x" ^ v)) + | _ -> None + + let rec value_of_sexpr sexpr = + let open Jib in + let open Value in + function + | CT_fbits width -> begin + match parse_sexpr_int width sexpr with + | Some value -> mk_vector (Sail_lib.get_slice_int' (width, value, 0)) + | None -> failwith ("Cannot parse sexpr as bitvector: " ^ string_of_sexpr sexpr) + end + | CT_struct (_, fields) -> begin + match sexpr with + | List (Atom name :: smt_fields) -> + V_record + (List.fold_left2 + (fun m (field_id, ctyp) sexpr -> StringMap.add (string_of_id field_id) (value_of_sexpr sexpr ctyp) m) + StringMap.empty fields smt_fields + ) + | _ -> failwith ("Cannot parse sexpr as struct " ^ string_of_sexpr sexpr) + end + | CT_enum (_, members) -> begin + match sexpr with + | Atom name -> begin + match List.find_opt (fun member -> Util.zencode_string (string_of_id member) = name) members with + | Some member -> V_member (string_of_id member) + | None -> + failwith + ("Could not find enum member for " ^ name ^ " in " ^ Util.string_of_list ", " string_of_id members) + end + | _ -> failwith ("Cannot parse sexpr as enum " ^ string_of_sexpr sexpr) + end + | CT_bool -> begin + match sexpr with + | Atom "true" -> V_bool true + | Atom "false" -> V_bool false + | _ -> failwith ("Cannot parse sexpr as bool " ^ string_of_sexpr sexpr) + end + | CT_fint width -> begin + match parse_sexpr_int width sexpr with + | Some value -> V_int value + | None -> failwith ("Cannot parse sexpr as fixed-width integer: " ^ string_of_sexpr sexpr) + end + | CT_lint -> begin + match parse_sexpr_int Config.max_unknown_integer_width sexpr with + | Some value -> V_int value + | None -> failwith ("Cannot parse sexpr as integer: " ^ string_of_sexpr sexpr) + end + | ctyp -> failwith ("Unsupported type in sexpr: " ^ Jib_util.string_of_ctyp ctyp) + + let rec find_arg id ctyp arg_smt_names = function + | List [Atom "define-fun"; Atom str; List []; _; value] :: _ + when Util.assoc_compare_opt Id.compare id arg_smt_names = Some (Some str) -> + (id, value_of_sexpr value ctyp) + | _ :: sexps -> find_arg id ctyp arg_smt_names sexps + | [] -> (id, V_unit) + + let build_counterexample args arg_ctyps arg_smt_names model = + List.map2 (fun id ctyp -> find_arg id ctyp arg_smt_names model) args arg_ctyps + + 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) + + let check ~env ~ast ~solver ~file_name ~function_id ~args ~arg_ctyps ~arg_smt_names = + let open Printf in + let open Ast in + print_endline ("Checking counterexample: " ^ file_name); + let in_chan = ksprintf Unix.open_process_in "%s %s" (counterexample_command solver) file_name in + let lines = ref [] in + begin + try + while true do + lines := input_line in_chan :: !lines + done + with End_of_file -> () + end; + let solver_output = List.rev !lines |> String.concat "\n" in + begin + match parse_sexps solver_output with + | Some (Atom "sat" :: (List (Atom "model" :: model) | List model) :: _) -> + let open Value in + let open Interpreter in + print_endline (sprintf "Solver found counterexample: %s" Util.("ok" |> green |> clear)); + let counterexample = build_counterexample args arg_ctyps arg_smt_names model in + List.iter (fun (id, v) -> print_endline (" " ^ string_of_id id ^ " -> " ^ string_of_value v)) counterexample; + let istate = initial_state ast env !primops in + let annot = (Parse_ast.Unknown, Type_check.mk_tannot env bool_typ) in + let call = + E_aux + ( E_app + ( function_id, + List.map + (fun (_, v) -> E_aux (E_internal_value v, (Parse_ast.Unknown, Type_check.empty_tannot))) + counterexample + ), + annot + ) + in + let result = run (Step (lazy "", istate, return call, [])) in + begin + match result with + | Some (V_bool false) | None -> + ksprintf print_endline "Replaying counterexample: %s" Util.("ok" |> green |> clear) + | _ -> () + end + | Some (Atom "unsat" :: _) -> + print_endline "Solver could not find counterexample"; + print_endline "Solver output:"; + print_endline solver_output + | _ -> + print_endline "Unexpected solver output:"; + print_endline solver_output + end; + let _ = Unix.close_process_in in_chan in + () +end diff --git a/src/lib/smt_gen.ml b/src/lib/smt_gen.ml index 9efd8f30c..f323dfd83 100644 --- a/src/lib/smt_gen.ml +++ b/src/lib/smt_gen.ml @@ -80,6 +80,8 @@ let zencode_uid (id, ctyps) = type checks = { overflows : smt_exp list; strings_used : bool; reals_used : bool } +let get_overflows c = c.overflows + let empty_checks = { overflows = []; strings_used = false; reals_used = false } let append_checks c1 c2 = @@ -224,6 +226,7 @@ module type CONFIG = sig val max_unknown_bitvector_width : int val max_unknown_generic_vector_length : int val union_ctyp_classify : ctyp -> bool + val register_ref : string -> smt_exp end module type PRIMOP_GEN = sig @@ -255,7 +258,7 @@ let undefined_enabled = function Undefined_disable -> false | _ -> true module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct let lint_size = Config.max_unknown_integer_width let lbits_size = Config.max_unknown_bitvector_width - let lbits_index = required_width (Big_int.of_int (lbits_size - 1)) + let lbits_index = required_width (Big_int.of_int lbits_size) let int_size = function | CT_constant n -> required_width n @@ -299,7 +302,7 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct | VL_real str, _ -> let* _ = real_used in return (if str.[0] = '-' then Fn ("-", [Real_lit (String.sub str 1 (String.length str - 1))]) else Real_lit str) - | VL_ref str, _ -> return (Fn ("reg_ref", [String_lit str])) + | VL_ref str, _ -> return (Config.register_ref str) | _ -> let* l = current_location in Reporting.unreachable l __POS__ @@ -485,10 +488,30 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct else if sz1 > sz2 then Fn (fn, [sv1; SignExtend (sz1, sz1 - sz2, sv2)]) else Fn (fn, [SignExtend (sz2, sz2 - sz1, sv1); sv2]) ) - | CT_constant c, CT_fint sz -> return (Fn (fn, [bvint sz c; sv2])) - | CT_fint sz, CT_constant c -> return (Fn (fn, [sv1; bvint sz c])) - | CT_constant c, CT_lint -> return (Fn (fn, [bvint lint_size c; sv2])) - | CT_lint, CT_constant c -> return (Fn (fn, [sv1; bvint lint_size c])) + | CT_constant c, CT_fint sz -> + let constant_sz = required_width c in + if constant_sz <= sz then return (Fn (fn, [bvint sz c; sv2])) + else + let* sv2 = signed_size ~checked:false ~into:constant_sz ~from:sz sv2 in + return (Fn (fn, [bvint constant_sz c; sv2])) + | CT_fint sz, CT_constant c -> + let constant_sz = required_width c in + if constant_sz <= sz then return (Fn (fn, [sv1; bvint sz c])) + else + let* sv1 = signed_size ~checked:false ~into:constant_sz ~from:sz sv1 in + return (Fn (fn, [sv1; bvint constant_sz c])) + | CT_constant c, CT_lint -> + let constant_sz = required_width c in + if constant_sz <= lint_size then return (Fn (fn, [bvint lint_size c; sv2])) + else + let* sv2 = signed_size ~checked:false ~into:constant_sz ~from:lint_size sv2 in + return (Fn (fn, [bvint constant_sz c; sv2])) + | CT_lint, CT_constant c -> + let constant_sz = required_width c in + if constant_sz <= lint_size then return (Fn (fn, [sv1; bvint lint_size c])) + else + let* sv1 = signed_size ~checked:false ~into:constant_sz ~from:lint_size sv1 in + return (Fn (fn, [sv1; bvint constant_sz c])) | CT_fint sz, CT_lint when sz < lint_size -> return (Fn (fn, [SignExtend (lint_size, lint_size - sz, sv1); sv2])) | CT_lint, CT_fint sz when sz < lint_size -> return (Fn (fn, [sv1; SignExtend (lint_size, lint_size - sz, sv2)])) | _, _ -> builtin_type_error fn [v1; v2] None @@ -530,6 +553,10 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct let shift = Fn ("concat", [bvzero (lbits_size - lbits_index); len]) in bvnot (bvshl all_ones shift) + let wf_lbits bv = + let mask = bvnot (bvmask (Fn ("len", [bv]))) in + Fn ("=", [bvand mask (Fn ("contents", [bv])); bvzero lbits_size]) + let builtin_shift shiftop vbits vshift ret_ctyp = match cval_ctyp vbits with | CT_fbits n -> @@ -594,22 +621,19 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct | CT_fbits n, _, CT_fbits m -> let* bv = smt_cval vbits in return (Fn ("concat", [bvzero (m - n); bv])) - | CT_fbits n, CT_fint m, CT_lbits -> - let* bv = smt_cval vbits in - return (Fn ("concat", [bvzero (m - n); bv])) | CT_lbits, _, CT_fbits m -> let* bv = smt_cval vbits in return (Extract (m - 1, 0, Fn ("contents", [bv]))) - (* - | CT_fbits n, CT_lbits -> - assert (lbits_size ctx >= n); - let vbits = - if lbits_size ctx = n then smt_cval ctx vbits - else if lbits_size ctx > n then Fn ("concat", [bvzero (lbits_size ctx - n); smt_cval ctx vbits]) - else assert false - in - Fn ("Bits", [bvzeint ctx ctx.lbits_index vlen; vbits]) - *) + | CT_fbits n, _, CT_lbits -> + let* bits = + if lbits_size = n then smt_cval vbits + else if lbits_size > n then + let* unextended = smt_cval vbits in + return (Fn ("concat", [bvzero (lbits_size - n); unextended])) + else assert false + in + let* len = bvzeint lbits_index vlen in + return (Fn ("Bits", [len; bits])) | CT_lbits, CT_lint, CT_lbits -> let* len = smt_cval vlen in let* bv = smt_cval vbits in @@ -765,13 +789,17 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct match (cval_ctyp v1, cval_ctyp v2, ret_ctyp) with | CT_fbits n, CT_fbits m, CT_fbits o -> assert (n + m = o); - let* smt1 = smt_cval v1 in - let* smt2 = smt_cval v2 in - return (Fn ("concat", [smt1; smt2])) + if n = 0 then smt_cval v2 + else if m = 0 then smt_cval v1 + else + let* smt1 = smt_cval v1 in + let* smt2 = smt_cval v2 in + return (Fn ("concat", [smt1; smt2])) + | CT_fbits n, CT_lbits, CT_lbits when n = 0 -> smt_cval v2 | CT_fbits n, CT_lbits, CT_lbits -> let* smt1 = smt_cval v1 in let* smt2 = smt_cval v2 in - let x = Fn ("concat", [bvzero (lbits_size - n); smt1]) in + let x = if lbits_size = n then smt1 else Fn ("concat", [bvzero (lbits_size - n); smt1]) in let shift = Fn ("concat", [bvzero (lbits_size - lbits_index); Fn ("len", [smt2])]) in return (Fn @@ -786,28 +814,23 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct let* smt1 = smt_cval v1 in let* smt2 = smt_cval v2 in return (Extract (m - 1, 0, Fn ("concat", [Fn ("contents", [smt1]); smt2]))) - (* | CT_lbits, CT_fbits n, CT_lbits -> - let smt1 = smt_cval ctx v1 in - let smt2 = smt_cval ctx v2 in - Fn - ( "Bits", - [ - bvadd (bvint ctx.lbits_index (Big_int.of_int n)) (Fn ("len", [smt1])); - Extract (lbits_size ctx - 1, 0, Fn ("concat", [Fn ("contents", [smt1]); smt2])); - ] - ) + let* smt1 = smt_cval v1 in + let* smt2 = smt_cval v2 in + return + (Fn + ( "Bits", + [ + bvadd (bvint lbits_index (Big_int.of_int n)) (Fn ("len", [smt1])); + Extract (lbits_size - 1, 0, Fn ("concat", [Fn ("contents", [smt1]); smt2])); + ] + ) + ) | CT_fbits n, CT_fbits m, CT_lbits -> - let smt1 = smt_cval ctx v1 in - let smt2 = smt_cval ctx v2 in - Fn - ( "Bits", - [ - bvint ctx.lbits_index (Big_int.of_int (n + m)); - unsigned_size ctx (lbits_size ctx) (n + m) (Fn ("concat", [smt1; smt2])); - ] - ) - *) + let* smt1 = smt_cval v1 in + let* smt2 = smt_cval v2 in + let* appended = unsigned_size ~into:lbits_size ~from:(n + m) (Fn ("concat", [smt1; smt2])) in + return (Fn ("Bits", [bvint lbits_index (Big_int.of_int (n + m)); appended])) | CT_lbits, CT_lbits, CT_lbits -> let* smt1 = smt_cval v1 in let* smt2 = smt_cval v2 in @@ -816,14 +839,12 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct return (Fn ("Bits", [bvadd (Fn ("len", [smt1])) (Fn ("len", [smt2])); bvor (bvshl x shift) (Fn ("contents", [smt2]))]) ) - (* | CT_lbits, CT_lbits, CT_fbits n -> - let smt1 = smt_cval ctx v1 in - let smt2 = smt_cval ctx v2 in - let x = Fn ("contents", [smt1]) in - let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); Fn ("len", [smt2])]) in - unsigned_size ctx n (lbits_size ctx) (bvor (bvshl x shift) (Fn ("contents", [smt2]))) - *) + let* smt1 = smt_cval v1 in + let* smt2 = smt_cval v2 in + let x = Fn ("contents", [smt1]) in + let shift = Fn ("concat", [bvzero (lbits_size - lbits_index); Fn ("len", [smt2])]) in + unsigned_size ~into:n ~from:lbits_size (bvor (bvshl x shift) (Fn ("contents", [smt2]))) | _ -> builtin_type_error "append" [v1; v2] (Some ret_ctyp) let builtin_sail_truncate v1 v2 ret_ctyp = @@ -897,7 +918,7 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct let* vec = smt_cval vec in let* i = bind (smt_cval i) - (unsigned_size ~checked:false ~into:(required_width (Big_int.of_int (len - 1)) - 1) ~from:(int_size i_ctyp)) + (unsigned_size ~checked:false ~into:(required_width (Big_int.of_int (len - 1))) ~from:(int_size i_ctyp)) in return (Fn ("select", [vec; i])) (* @@ -976,7 +997,7 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct let* x = smt_cval x in let* i = bind (smt_cval i) - (unsigned_size ~checked:false ~into:(required_width (Big_int.of_int (len - 1)) - 1) ~from:(int_size i_ctyp)) + (unsigned_size ~checked:false ~into:(required_width (Big_int.of_int (len - 1))) ~from:(int_size i_ctyp)) in return (Store (Fixed len, store_fn, vec, i, x)) (* @@ -1071,25 +1092,70 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct return (bvshl (bvone lint_size) v) | _ -> builtin_type_error "pow2" [v] (Some ret_ctyp) - (* Technically, there's no bvclz in SMTLIB, but we can't generate - anything nice, so leave it in case a backend like SystemVerilog - can do better *) let builtin_count_leading_zeros v ret_ctyp = - let* l = current_location in + let ret_sz = int_size ret_ctyp in + let rec lzcnt sz smt = + if sz == 1 then + Ite + ( Fn ("=", [Extract (0, 0, smt); Bitvec_lit [Sail2_values.B0]]), + bvint ret_sz (Big_int.of_int 1), + bvint ret_sz Big_int.zero + ) + else ( + assert (sz land (sz - 1) = 0); + let hsz = sz / 2 in + Ite + ( Fn ("=", [Extract (sz - 1, hsz, smt); bvzero hsz]), + Fn ("bvadd", [bvint ret_sz (Big_int.of_int hsz); lzcnt hsz (Extract (hsz - 1, 0, smt))]), + lzcnt hsz (Extract (sz - 1, hsz, smt)) + ) + ) + in + let smallest_greater_power_of_two n = + let m = ref 1 in + while !m < n do + m := !m lsl 1 + done; + assert (!m land (!m - 1) = 0); + !m + in + let* smt = smt_cval v in match cval_ctyp v with + | CT_fbits sz when sz land (sz - 1) = 0 -> return (lzcnt sz smt) | CT_fbits sz -> - let bvclz = Primop_gen.count_leading_zeros l sz in - let* bv = smt_cval v in - unsigned_size ~max_value:sz ~into:(int_size ret_ctyp) ~from:sz (Fn (bvclz, [bv])) + let padded_sz = smallest_greater_power_of_two sz in + let padding = bvzero (padded_sz - sz) in + return + (Fn + ("bvsub", [lzcnt padded_sz (Fn ("concat", [padding; smt])); bvint ret_sz (Big_int.of_int (padded_sz - sz))]) + ) | CT_lbits -> - let bvclz = Primop_gen.count_leading_zeros l lbits_size in - let* bv = smt_cval v in - let contents_clz = Fn (bvclz, [Fn ("contents", [bv])]) in - let* len = unsigned_size ~into:lbits_size ~from:lbits_index (Fn ("len", [bv])) in - let lz = bvsub contents_clz (bvsub (bvpint lbits_size (Big_int.of_int lbits_size)) len) in - unsigned_size ~max_value:lbits_size ~into:(int_size ret_ctyp) ~from:lbits_size lz + return + (Fn + ( "bvsub", + [ + lzcnt lbits_size (Fn ("contents", [smt])); + Fn + ( "bvsub", + [ + bvint ret_sz (Big_int.of_int lbits_size); + Fn ("concat", [bvzero (ret_sz - lbits_index); Fn ("len", [smt])]); + ] + ); + ] + ) + ) | _ -> builtin_type_error "count_leading_zeros" [v] (Some ret_ctyp) + let unary_smt op v _ = + let* smt = smt_cval v in + return (Fn (op, [smt])) + + let binary_smt op v1 v2 _ = + let* smt1 = smt_cval v1 in + let* smt2 = smt_cval v2 in + return (Fn (op, [smt1; smt2])) + let arity_error = let* l = current_location in raise (Reporting.unreachable l __POS__ "Trying to generate primitive with incorrect number of arguments") @@ -1106,30 +1172,11 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct Some (fun args ret_ctyp -> match args with [v1; v2; v3] -> f v1 v2 v3 ret_ctyp | _ -> arity_error) let builtin ?(allow_io = true) ?(undefined = Undefined_disable) = function - | "eq_bit" -> - binary_primop_simple (fun v1 v2 -> - let* smt1 = smt_cval v1 in - let* smt2 = smt_cval v2 in - return (Fn ("=", [smt1; smt2])) - ) - | "eq_bool" -> - binary_primop_simple (fun v1 v2 -> - let* smt1 = smt_cval v1 in - let* smt2 = smt_cval v2 in - return (Fn ("=", [smt1; smt2])) - ) - | "eq_string" -> - binary_primop_simple (fun v1 v2 -> - let* smt1 = smt_cval v1 in - let* smt2 = smt_cval v2 in - return (Fn ("=", [smt1; smt2])) - ) + | "eq_bit" -> binary_primop (binary_smt "=") + | "eq_bool" -> binary_primop (binary_smt "=") + | "eq_string" -> binary_primop (binary_smt "=") | "eq_int" -> binary_primop_simple builtin_eq_int - | "not" -> - unary_primop_simple (fun v -> - let* v = smt_cval v in - return (Fn ("not", [v])) - ) + | "not" -> unary_primop (unary_smt "not") | "lt" -> binary_primop_simple builtin_lt | "lteq" -> binary_primop_simple builtin_lteq | "gt" -> binary_primop_simple builtin_gt @@ -1177,6 +1224,16 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct | "length" -> unary_primop builtin_length | "replicate_bits" -> binary_primop builtin_replicate_bits | "count_leading_zeros" -> unary_primop builtin_count_leading_zeros + | "eq_real" -> binary_primop (binary_smt "=") + | "neg_real" -> unary_primop (unary_smt "-") + | "add_real" -> binary_primop (binary_smt "+") + | "sub_real" -> binary_primop (binary_smt "-") + | "mult_real" -> binary_primop (binary_smt "*") + | "div_real" -> binary_primop (binary_smt "/") + | "lt_real" -> binary_primop (binary_smt "<") + | "gt_real" -> binary_primop (binary_smt ">") + | "lteq_real" -> binary_primop (binary_smt "<=") + | "gteq_real" -> binary_primop (binary_smt ">=") | "concat_str" -> binary_primop_simple (fun str1 str2 -> let* str1 = smt_cval str1 in @@ -1219,13 +1276,13 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct let* bv = smt_cval bv in return (Fn (op, [bv])) ) - | "sail_assert" -> + | "sail_assert" when allow_io -> binary_primop_simple (fun b msg -> let* b = smt_cval b in let* msg = smt_cval msg in return (Fn ("sail_assert", [b; msg])) ) - | "reg_deref" -> + | "reg_deref" when allow_io -> unary_primop_simple (fun reg_ref -> match cval_ctyp reg_ref with | CT_ref ctyp -> diff --git a/src/lib/smt_gen.mli b/src/lib/smt_gen.mli index 8f59b9094..d0c00c28d 100644 --- a/src/lib/smt_gen.mli +++ b/src/lib/smt_gen.mli @@ -78,6 +78,8 @@ open Jib features like strings or real numbers. *) type checks +val get_overflows : checks -> Smt_exp.smt_exp list + (** We generate primitives in a monad that accumulates any required dynamic checks, and contains the location information for any error messages. *) @@ -148,6 +150,9 @@ module type CONFIG = sig contain. This is abstracted into a classify function that the instantiator of this module can supply. *) val union_ctyp_classify : ctyp -> bool + + (** How we handle register references differs between backends *) + val register_ref : string -> Smt_exp.smt_exp end (** Some Sail primitives we can't directly convert to pure SMT @@ -185,6 +190,8 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) : sig val generic_vector_length : ctyp -> int + val wf_lbits : Smt_exp.smt_exp -> Smt_exp.smt_exp + (** Create an SMT expression that converts an expression of the jib type [from] into an SMT expression for the jib type [into]. Note that this function assumes that the input is of the correct diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index d7e6ddc4e..6de64f77f 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -4748,8 +4748,9 @@ let initial_env = ( TypQ_aux (TypQ_tq [QI_aux (QI_id (mk_kopt K_int (mk_kid "n")), Parse_ast.Unknown)], Parse_ast.Unknown), function_typ [atom_typ (nvar (mk_kid "n"))] (app_typ (mk_id "itself") [mk_typ_arg (A_nexp (nvar (mk_kid "n")))]) ) - (* __assume is used by property.ml to add guards for SMT generation, + (* sail_assume is used by property.ml to add guards for SMT generation, but which don't affect flow-typing. *) + |> Env.add_extern (mk_id "sail_assume") { pure = true; bindings = [("_", "sail_assume")] } |> Env.add_val_spec (mk_id "sail_assume") (TypQ_aux (TypQ_no_forall, Parse_ast.Unknown), function_typ [bool_typ] unit_typ) diff --git a/src/sail_smt_backend/jib_smt.ml b/src/sail_smt_backend/jib_smt.ml index 6fd5b4334..b47591042 100644 --- a/src/sail_smt_backend/jib_smt.ml +++ b/src/sail_smt_backend/jib_smt.ml @@ -124,15 +124,25 @@ module Make_optimizer (S : Sequence) = struct | Some n -> NameHashtbl.replace uses var (n + 1) | None -> NameHashtbl.add uses var 1 end - | Enum _ | Bitvec_lit _ | Bool_lit _ | String_lit _ | Real_lit _ -> () + | Enum _ | Bitvec_lit _ | Bool_lit _ | String_lit _ | Real_lit _ | Empty_list -> () | Fn (_, exps) -> List.iter uses_in_exp exps | Field (_, _, exp) -> uses_in_exp exp | Ite (cond, t, e) -> uses_in_exp cond; uses_in_exp t; uses_in_exp e - | Extract (_, _, exp) | Unwrap (_, _, exp) | Tester (_, exp) | SignExtend (_, _, exp) | ZeroExtend (_, _, exp) -> + | Extract (_, _, exp) + | Unwrap (_, _, exp) + | Tester (_, exp) + | SignExtend (_, _, exp) + | ZeroExtend (_, _, exp) + | Hd (_, exp) + | Tl (_, exp) -> uses_in_exp exp + | Store (_, _, arr, index, x) -> + uses_in_exp arr; + uses_in_exp index; + uses_in_exp x in let remove_unused () = function @@ -211,7 +221,9 @@ module type CONFIG = sig end module Make (Config : CONFIG) = struct - let lbits_index_width = required_width (Big_int.of_int (Config.max_unknown_bitvector_width - 1)) + open Jib_visitor + + let lbits_index_width = required_width (Big_int.of_int Config.max_unknown_bitvector_width) let vector_index_width = required_width (Big_int.of_int (Config.max_unknown_generic_vector_length - 1)) module Smt = @@ -221,6 +233,19 @@ module Make (Config : CONFIG) = struct let max_unknown_bitvector_width = Config.max_unknown_bitvector_width let max_unknown_generic_vector_length = Config.max_unknown_generic_vector_length let union_ctyp_classify _ = true + let register_ref reg_name = + let id = mk_id reg_name in + let rmap = + CTMap.filter (fun ctyp regs -> List.exists (fun reg -> Id.compare reg id = 0) regs) Config.register_map + in + assert (CTMap.cardinal rmap = 1); + 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 -> Smt_gen.bvint (required_width (Big_int.of_int (List.length regs))) (Big_int.of_int i) + | None -> assert false + end + | _ -> assert false end) (struct let print_bits l = function _ -> Reporting.unreachable l __POS__ "print_bits" @@ -235,7 +260,7 @@ module Make (Config : CONFIG) = struct let count_leading_zeros l = function _ -> Reporting.unreachable l __POS__ "count_leading_zeros" - let fvector_store l _len = function _ -> Reporting.unreachable l __POS__ "fvector_store" + let fvector_store l _ _ = "store" let is_empty l = function _ -> Reporting.unreachable l __POS__ "is_empty" @@ -257,7 +282,9 @@ module Make (Config : CONFIG) = struct let smt_unit = mk_enum "Unit" ["Unit"] let smt_lbits = - mk_record "Bits" [("size", Bitvec lbits_index_width); ("bits", Bitvec Config.max_unknown_bitvector_width)] + mk_record "Bits" [("len", Bitvec lbits_index_width); ("bits", Bitvec Config.max_unknown_bitvector_width)] + + let rec wf_smt_ctyp = function CT_lbits -> Some (fun exp -> Smt.wf_lbits exp) | _ -> None let rec smt_ctyp = function | CT_constant n -> return (Bitvec (required_width n)) @@ -443,12 +470,12 @@ module Make (Config : CONFIG) = struct return () let define_const id ctyp exp = - let* ctyp = smt_ctyp ctyp in - return (Define_const (id, ctyp, exp)) + let* ty = smt_ctyp ctyp in + return (Define_const (id, ty, exp)) let declare_const id ctyp = - let* ctyp = smt_ctyp ctyp in - return (Declare_const (id, ctyp)) + let* ty = smt_ctyp ctyp in + return (Declare_const (id, ty)) let singleton = Smt_gen.fmap (fun x -> [x]) @@ -491,6 +518,14 @@ module Make (Config : CONFIG) = struct end | _ -> assert false + let builtin_sqrt_real root v = + let* smt = Smt.smt_cval v in + return + [ + Declare_const (root, Real); + Assert (Fn ("and", [Fn ("=", [smt; Fn ("*", [Var root; Var root])]); Fn (">=", [Var root; Real_lit "0.0"])])); + ] + (* For a basic block (contained in a control-flow node / cfnode), we turn the instructions into a sequence of define-const and declare-const expressions. Because we are working with a SSA graph, @@ -502,11 +537,34 @@ module Make (Config : CONFIG) = struct | I_funcall (CR_one (CL_id (id, ret_ctyp)), extern, (function_id, _), args) -> if ctx_is_extern function_id ctx then ( let name = ctx_get_extern function_id ctx in - match Smt.builtin name with - | Some generator -> - let* value = generator args ret_ctyp in - singleton (define_const id ret_ctyp value) - | None -> failwith ("No generator " ^ string_of_id function_id) + if name = "sail_assert" then ( + match args with + | [assertion; _] -> + let* smt = Smt.smt_cval assertion in + let* _ = add_event state Assertion (Fn ("not", [smt])) in + return [] + | _ -> Reporting.unreachable l __POS__ "Bad arguments for assertion" + ) + else if name = "sail_assume" then ( + match args with + | [assumption] -> + let* smt = Smt.smt_cval assumption in + let* _ = add_event state Assumption smt in + return [] + | _ -> Reporting.unreachable l __POS__ "Bad arguments for assertion" + ) + else if name = "sqrt_real" then ( + match args with + | [v] -> builtin_sqrt_real id v + | _ -> Reporting.unreachable l __POS__ "Bad arguments for sqrt_real" + ) + else ( + match Smt.builtin ~allow_io:false name with + | Some generator -> + let* value = generator args ret_ctyp in + singleton (define_const id ret_ctyp value) + | None -> failwith ("No generator " ^ string_of_id function_id) + ) ) else if extern && string_of_id function_id = "internal_vector_init" then singleton (declare_const id ret_ctyp) else if extern && string_of_id function_id = "internal_vector_update" then begin @@ -533,11 +591,16 @@ module Make (Config : CONFIG) = struct let* smt = Smt.smt_cval cval in let write, ctyp = rmw_write clexp in singleton (define_const write ctyp (rmw_modify smt clexp)) - | I_decl (ctyp, id) -> + | I_decl (ctyp, id) -> begin begin match l with Unique (n, _) -> Stack.push (n, zencode_name id) state.arg_stack | _ -> () end; - singleton (declare_const id ctyp) + let* ty = smt_ctyp ctyp in + let wf_pred = wf_smt_ctyp ctyp in + match wf_pred with + | Some p -> return [Declare_const (id, ty); Assert (p (Var id))] + | None -> return [Declare_const (id, ty)] + end | I_clear _ -> return [] (* Should only appear as terminators for basic blocks. *) | I_jump _ | I_goto _ | I_end _ | I_exit _ | I_undefined _ -> @@ -547,8 +610,8 @@ module Make (Config : CONFIG) = struct let generate_reg_decs inits cdefs = let rec go acc = function | CDEF_aux (CDEF_register (id, ctyp, _), _) :: cdefs when not (NameMap.mem (Name (id, 0)) inits) -> - let* ctyp = smt_ctyp ctyp in - go (Declare_const (Name (id, 0), ctyp) :: acc) cdefs + let* smt_typ = smt_ctyp ctyp in + go (Declare_const (Name (id, 0), smt_typ) :: acc) cdefs | _ :: cdefs -> go acc cdefs | [] -> return (List.rev acc) in @@ -651,21 +714,30 @@ module Make (Config : CONFIG) = struct let state = { events = ref EventMap.empty; cfg; node = -1; arg_stack = Stack.create () } in - let* _ = - Smt_gen.iterM - (fun n -> - match get_vertex cfg n with - | None -> return () - | Some ((ssa_elems, cfnode), preds, succs) -> - let* muxers = Smt_gen.fmap List.concat (mapM (smt_ssanode cfg preds) ssa_elems) in - let state = { state with node = n } in - let* basic_block = smt_cfnode all_cdefs ctx state cfnode in - push_smt_defs stack muxers; - push_smt_defs stack basic_block; - return () - ) - visit_order - in + List.iter + (fun n -> + match get_vertex cfg n with + | None -> () + | Some ((ssa_elems, cfnode), preds, succs) -> + let pathcond, checks = + Smt_gen.run + (let* muxers = Smt_gen.fmap List.concat (mapM (smt_ssanode cfg preds) ssa_elems) in + let state = { state with node = n } in + let* basic_block = smt_cfnode all_cdefs ctx state cfnode in + push_smt_defs stack muxers; + push_smt_defs stack basic_block; + get_pathcond state.node state.cfg + ) + Parse_ast.Unknown + in + if not Config.ignore_overflow then ( + let overflow_stack = event_stack state Overflow in + List.iter + (fun overflow_smt -> Stack.push (Fn ("and", [pathcond; overflow_smt])) overflow_stack) + (Smt_gen.get_overflows checks) + ) + ) + visit_order; return (stack, state) @@ -791,7 +863,108 @@ module Make (Config : CONFIG) = struct end | [] -> acc + (* For generating SMT when we have a reg_deref(r : register(t)) + function, we have to expand it into a if-then-else cascade that + checks if r is any one of the registers with type t, and reads that + register if it is. We also do a similar thing for *r = x + *) + class expand_reg_deref_visitor env : jib_visitor = + object + inherit empty_jib_visitor + + method! vcval _ = SkipChildren + method! vctyp _ = SkipChildren + method! vclexp _ = SkipChildren + + method! vinstr = + function + | I_aux (I_funcall (CR_one (CL_addr (CL_id (id, ctyp))), false, function_id, args), (_, l)) -> begin + match ctyp with + | CT_ref reg_ctyp -> begin + match CTMap.find_opt reg_ctyp Config.register_map with + | Some regs -> + let end_label = label "end_reg_write_" in + let try_reg r = + let next_label = label "next_reg_write_" in + [ + ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label; + ifuncall l (CL_id (name r, reg_ctyp)) function_id args; + igoto end_label; + ilabel next_label; + ] + in + ChangeTo (iblock (List.concat (List.map try_reg regs) @ [ilabel end_label])) + | None -> + raise (Reporting.err_general l ("Could not find any registers with type " ^ string_of_ctyp reg_ctyp)) + end + | _ -> + raise + (Reporting.err_general l "Register reference assignment must take a register reference as an argument") + end + | I_aux (I_funcall (CR_one clexp, false, function_id, [reg_ref]), (_, l)) as instr -> + let open Type_check in + begin + match + if Env.is_extern (fst function_id) env "smt" then Some (Env.get_extern (fst function_id) env "smt") + else None + with + | Some "reg_deref" -> begin + match cval_ctyp reg_ref with + | CT_ref reg_ctyp -> begin + (* Not find all the registers with this ctyp *) + match CTMap.find_opt reg_ctyp Config.register_map with + | Some regs -> + let end_label = label "end_reg_deref_" in + let try_reg r = + let next_label = label "next_reg_deref_" in + [ + ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); reg_ref])) next_label; + icopy l clexp (V_id (name r, reg_ctyp)); + igoto end_label; + ilabel next_label; + ] + in + ChangeTo (iblock (List.concat (List.map try_reg regs) @ [ilabel end_label])) + | None -> + raise + (Reporting.err_general l + ("Could not find any registers with type " ^ string_of_ctyp reg_ctyp) + ) + end + | _ -> + raise + (Reporting.err_general l "Register dereference must have a register reference as an argument") + end + | _ -> SkipChildren + end + | I_aux (I_copy (CL_addr (CL_id (id, ctyp)), cval), (_, l)) -> begin + match ctyp with + | CT_ref reg_ctyp -> begin + match CTMap.find_opt reg_ctyp Config.register_map with + | Some regs -> + let end_label = label "end_reg_write_" in + let try_reg r = + let next_label = label "next_reg_write_" in + [ + ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label; + icopy l (CL_id (name r, reg_ctyp)) cval; + igoto end_label; + ilabel next_label; + ] + in + ChangeTo (iblock (List.concat (List.map try_reg regs) @ [ilabel end_label])) + | None -> + raise (Reporting.err_general l ("Could not find any registers with type " ^ string_of_ctyp reg_ctyp)) + end + | _ -> + raise + (Reporting.err_general l "Register reference assignment must take a register reference as an argument") + end + | _ -> DoChildren + end + let generate_smt ~properties ~name_file ~smt_includes ctx cdefs = + let cdefs = visit_cdefs (new expand_reg_deref_visitor ctx.tc_env) cdefs in smt_cdefs [] properties [] name_file ctx cdefs smt_includes cdefs end diff --git a/src/sail_smt_backend/sail_plugin_smt.ml b/src/sail_smt_backend/sail_plugin_smt.ml index 2cabd79da..5161fed49 100644 --- a/src/sail_smt_backend/sail_plugin_smt.ml +++ b/src/sail_smt_backend/sail_plugin_smt.ml @@ -74,6 +74,8 @@ let opt_smt_auto_solver = ref Smt_exp.Cvc5 let opt_smt_includes : string list ref = ref [] let opt_smt_ignore_overflow = ref false let opt_smt_unknown_integer_width = ref 128 +let opt_smt_unknown_bitvector_width = ref 64 +let opt_smt_unknown_generic_vector_width = ref 32 let set_smt_auto_solver arg = let open Smt_exp in @@ -91,23 +93,20 @@ let smt_options = Arg.String (fun n -> opt_smt_unknown_integer_width := int_of_string n), " set a bound of n on the maximum integer bitwidth for generated SMT (default 128)" ); - ] -(* - ("-smt_propagate_vars", Arg.Set Jib_smt.opt_propagate_vars, " propgate variables through generated SMT"); + ("-smt_propagate_vars", Arg.Unit (fun () -> ()), " (deprecated) propgate variables through generated SMT"); ( "-smt_bits_size", - Arg.String (fun n -> opt_default_lbits_index := int_of_string n), - " set a bound of 2 ^ n for bitvector bitwidth in generated SMT (default 8)" + Arg.String (fun n -> opt_smt_unknown_bitvector_width := int_of_string n), + " set a size bound of n for unknown-length bitvectors in generated SMT (default 64)" ); ( "-smt_vector_size", - Arg.String (fun n -> Jib_smt.opt_default_vector_index := int_of_string n), + Arg.String (fun n -> opt_smt_unknown_generic_vector_width := int_of_string n), " set a bound of 2 ^ n for generic vectors in generated SMT (default 5)" ); ( "-smt_include", - Arg.String (fun i -> opt_includes_smt := i :: !opt_includes_smt), + Arg.String (fun i -> opt_smt_includes := i :: !opt_smt_includes), " insert additional file in SMT output" ); ] -*) let smt_rewrites = let open Rewrites in @@ -158,17 +157,20 @@ let smt_target _ _ out_file ast effect_info env = let cdefs, ctx, register_map = Jib_smt.compile ~unroll_limit:10 env effect_info ast_smt in let module SMTGen = Jib_smt.Make (struct let max_unknown_integer_width = !opt_smt_unknown_integer_width - let max_unknown_bitvector_width = 64 - let max_unknown_generic_vector_length = 32 + let max_unknown_bitvector_width = !opt_smt_unknown_bitvector_width + let max_unknown_generic_vector_length = !opt_smt_unknown_generic_vector_width let register_map = register_map let ignore_overflow = !opt_smt_ignore_overflow end) in + let module Counterexample = Smt_exp.Counterexample (struct + let max_unknown_integer_width = !opt_smt_unknown_integer_width + end) in let generated_smt = SMTGen.generate_smt ~properties ~name_file ~smt_includes:!opt_smt_includes ctx cdefs in if !opt_smt_auto then List.iter (fun ({ file_name; function_id; args; arg_ctyps; arg_smt_names } : SMTGen.generated_smt_info) -> - Smt_exp.check_counterexample ~env:ctx.tc_env ~ast ~solver:!opt_smt_auto_solver ~file_name ~function_id ~args - ~arg_ctyps ~arg_smt_names + Counterexample.check ~env:ctx.tc_env ~ast ~solver:!opt_smt_auto_solver ~file_name ~function_id ~args ~arg_ctyps + ~arg_smt_names ) generated_smt; () diff --git a/src/sail_smt_backend/smtlib.ml b/src/sail_smt_backend/smtlib.ml deleted file mode 100644 index 89c91dfae..000000000 --- a/src/sail_smt_backend/smtlib.ml +++ /dev/null @@ -1,750 +0,0 @@ -(****************************************************************************) -(* Sail *) -(* *) -(* Sail and the Sail architecture models here, comprising all files and *) -(* directories except the ASL-derived Sail code in the aarch64 directory, *) -(* are subject to the BSD two-clause licence below. *) -(* *) -(* The ASL derived parts of the ARMv8.3 specification in *) -(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *) -(* *) -(* Copyright (c) 2013-2021 *) -(* 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 *) -(* Alastair Reid (Arm Ltd) *) -(* *) -(* All rights reserved. *) -(* *) -(* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous *) -(* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA *) -(* KTF funding, and donations from Arm. This project has received *) -(* funding from the European Research Council (ERC) under the European *) -(* Union’s Horizon 2020 research and innovation programme (grant *) -(* agreement No 789108, ELVER). *) -(* *) -(* This software was developed by SRI International and the University of *) -(* Cambridge Computer Laboratory (Department of Computer Science and *) -(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *) -(* and FA8750-10-C-0237 ("CTSRD"). *) -(* *) -(* 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 Libsail - -open Ast -open Ast_util - -type counterexample_solver = Cvc5 | Cvc4 | Z3 - -let counterexample_command = function Cvc5 -> "cvc5 --lang=smt2.6" | Cvc4 -> "cvc4 --lang=smt2.6" | Z3 -> "z3" - -let counterexample_solver_from_name name = - match String.lowercase_ascii name with "cvc4" -> Some Cvc4 | "cvc5" -> Some Cvc5 | "z3" -> Some Z3 | _ -> None - -let opt_auto_solver = ref Cvc5 - -type smt_typ = - | Bitvec of int - | Bool - | String - | Real - | Datatype of string * (string * (string * smt_typ) list) list - | Tuple of smt_typ list - | Array of smt_typ * smt_typ - -let rec smt_typ_compare t1 t2 = - match (t1, t2) with - | Bitvec n, Bitvec m -> compare n m - | Bool, Bool -> 0 - | String, String -> 0 - | Real, Real -> 0 - | Datatype (name1, _), Datatype (name2, _) -> String.compare name1 name2 - | Tuple ts1, Tuple ts2 -> Util.lex_ord_list smt_typ_compare ts1 ts2 - | Array (t11, t12), Array (t21, t22) -> - let c = smt_typ_compare t11 t21 in - if c = 0 then smt_typ_compare t12 t22 else c - | Bitvec _, _ -> 1 - | _, Bitvec _ -> -1 - | Bool, _ -> 1 - | _, Bool -> -1 - | String, _ -> 1 - | _, String -> -1 - | Real, _ -> 1 - | _, Real -> -1 - | Datatype _, _ -> 1 - | _, Datatype _ -> -1 - | Tuple _, _ -> 1 - | _, Tuple _ -> -1 - -let rec smt_typ_equal t1 t2 = - match (t1, t2) with - | Bitvec n, Bitvec m -> n = m - | Bool, Bool -> true - | Datatype (name1, ctors1), Datatype (name2, ctors2) -> - let field_equal (field_name1, typ1) (field_name2, typ2) = field_name1 = field_name2 && smt_typ_equal typ1 typ2 in - let ctor_equal (ctor_name1, fields1) (ctor_name2, fields2) = - ctor_name1 = ctor_name2 - && List.length fields1 = List.length fields2 - && List.for_all2 field_equal fields1 fields2 - in - name1 = name2 && List.length ctors1 = List.length ctors2 && List.for_all2 ctor_equal ctors1 ctors2 - | _, _ -> false - -let mk_enum name elems = Datatype (name, List.map (fun elem -> (elem, [])) elems) - -let mk_record name fields = Datatype (name, [(name, fields)]) - -let mk_variant name ctors = Datatype (name, List.map (fun (ctor, ty) -> (ctor, [("un" ^ ctor, ty)])) ctors) - -type smt_exp = - | Bool_lit of bool - | Bitvec_lit of Sail2_values.bitU list - | Real_lit of string - | String_lit of string - | Var of string - | Shared of string - | Read_res of string - | Enum of string - | Fn of string * smt_exp list - | Ctor of string * smt_exp list - | Ite of smt_exp * smt_exp * smt_exp - | SignExtend of int * smt_exp - | Extract of int * int * smt_exp - | Tester of string * smt_exp - | Syntactic of smt_exp * smt_exp list - | Struct of string * (string * smt_exp) list - | Field of string * smt_exp - (* Used by sail-axiomatic, should never be generated by sail -smt! *) - | Forall of (string * smt_typ) list * smt_exp - -let rec fold_smt_exp f = function - | Fn (name, args) -> f (Fn (name, List.map (fold_smt_exp f) args)) - | Ctor (name, args) -> f (Ctor (name, List.map (fold_smt_exp f) args)) - | Ite (cond, t, e) -> f (Ite (fold_smt_exp f cond, fold_smt_exp f t, fold_smt_exp f e)) - | SignExtend (n, exp) -> f (SignExtend (n, fold_smt_exp f exp)) - | Extract (n, m, exp) -> f (Extract (n, m, fold_smt_exp f exp)) - | Tester (ctor, exp) -> f (Tester (ctor, fold_smt_exp f exp)) - | Forall (binders, exp) -> f (Forall (binders, fold_smt_exp f exp)) - | Syntactic (exp, exps) -> f (Syntactic (fold_smt_exp f exp, List.map (fold_smt_exp f) exps)) - | Field (name, exp) -> f (Field (name, fold_smt_exp f exp)) - | Struct (name, fields) -> f (Struct (name, List.map (fun (field, exp) -> (field, fold_smt_exp f exp)) fields)) - | (Bool_lit _ | Bitvec_lit _ | Real_lit _ | String_lit _ | Var _ | Shared _ | Read_res _ | Enum _) as exp -> f exp - -let smt_conj = function [] -> Bool_lit true | [x] -> x | xs -> Fn ("and", xs) - -let smt_disj = function [] -> Bool_lit false | [x] -> x | xs -> Fn ("or", xs) - -let extract i j x = Extract (i, j, x) - -let bvnot x = Fn ("bvnot", [x]) -let bvand x y = Fn ("bvand", [x; y]) -let bvor x y = Fn ("bvor", [x; y]) -let bvneg x = Fn ("bvneg", [x]) -let bvadd x y = Fn ("bvadd", [x; y]) -let bvmul x y = Fn ("bvmul", [x; y]) -let bvudiv x y = Fn ("bvudiv", [x; y]) -let bvurem x y = Fn ("bvurem", [x; y]) -let bvshl x y = Fn ("bvshl", [x; y]) -let bvlshr x y = Fn ("bvlshr", [x; y]) -let bvult x y = Fn ("bvult", [x; y]) - -let bvzero n = Bitvec_lit (Sail2_operators_bitlists.zeros (Big_int.of_int n)) - -let bvones n = Bitvec_lit (Sail2_operators_bitlists.ones (Big_int.of_int n)) - -let simp_equal x y = - match (x, y) with Bitvec_lit bv1, Bitvec_lit bv2 -> Some (Sail2_operators_bitlists.eq_vec bv1 bv2) | _, _ -> None - -let simp_and xs = - let xs = List.filter (function Bool_lit true -> false | _ -> true) xs in - match xs with - | [] -> Bool_lit true - | [x] -> x - | _ -> if List.exists (function Bool_lit false -> true | _ -> false) xs then Bool_lit false else Fn ("and", xs) - -let simp_or xs = - let xs = List.filter (function Bool_lit false -> false | _ -> true) xs in - match xs with - | [] -> Bool_lit false - | [x] -> x - | _ -> if List.exists (function Bool_lit true -> true | _ -> false) xs then Bool_lit true else Fn ("or", xs) - -let rec all_bitvec_lit = function Bitvec_lit _ :: rest -> all_bitvec_lit rest | [] -> true | _ :: _ -> false - -let rec merge_bitvec_lit = function - | Bitvec_lit b :: rest -> b @ merge_bitvec_lit rest - | [] -> [] - | _ :: _ -> assert false - -let simp_fn = function - | Fn ("not", [Fn ("not", [exp])]) -> exp - | Fn ("not", [Bool_lit b]) -> Bool_lit (not b) - | Fn ("contents", [Fn ("Bits", [_; contents])]) -> contents - | Fn ("len", [Fn ("Bits", [len; _])]) -> len - | Fn ("or", xs) -> simp_or xs - | Fn ("and", xs) -> simp_and xs - | Fn ("=>", [Bool_lit true; y]) -> y - | Fn ("=>", [Bool_lit false; y]) -> Bool_lit true - | Fn ("bvsub", [Bitvec_lit bv1; Bitvec_lit bv2]) -> Bitvec_lit (Sail2_operators_bitlists.sub_vec bv1 bv2) - | Fn ("bvadd", [Bitvec_lit bv1; Bitvec_lit bv2]) -> Bitvec_lit (Sail2_operators_bitlists.add_vec bv1 bv2) - | Fn ("concat", xs) when all_bitvec_lit xs -> Bitvec_lit (merge_bitvec_lit xs) - | Fn ("=", [x; y]) as exp -> begin match simp_equal x y with Some b -> Bool_lit b | None -> exp end - | exp -> exp - -let simp_ite = function - | Ite (cond, Bool_lit true, Bool_lit false) -> cond - | Ite (cond, Bool_lit x, Bool_lit y) when x = y -> Bool_lit x - | Ite (_, Var v, Var v') when v = v' -> Var v - | Ite (Bool_lit true, then_exp, _) -> then_exp - | Ite (Bool_lit false, _, else_exp) -> else_exp - | exp -> exp - -let rec simp_smt_exp vars kinds = function - | Var v -> begin match Hashtbl.find_opt vars v with Some exp -> simp_smt_exp vars kinds exp | None -> Var v end - | (Read_res _ | Shared _ | Enum _ | Bitvec_lit _ | Bool_lit _ | String_lit _ | Real_lit _) as exp -> exp - | Field (field, exp) -> - let exp = simp_smt_exp vars kinds exp in - begin - match exp with Struct (_, fields) -> List.assoc field fields | _ -> Field (field, exp) - end - | Struct (name, fields) -> Struct (name, List.map (fun (field, exp) -> (field, simp_smt_exp vars kinds exp)) fields) - | Fn (f, exps) -> - let exps = List.map (simp_smt_exp vars kinds) exps in - simp_fn (Fn (f, exps)) - | Ctor (f, exps) -> - let exps = List.map (simp_smt_exp vars kinds) exps in - simp_fn (Ctor (f, exps)) - | Ite (cond, t, e) -> - let cond = simp_smt_exp vars kinds cond in - let t = simp_smt_exp vars kinds t in - let e = simp_smt_exp vars kinds e in - simp_ite (Ite (cond, t, e)) - | Extract (i, j, exp) -> - let exp = simp_smt_exp vars kinds exp in - begin - match exp with - | Bitvec_lit bv -> - Bitvec_lit (Sail2_operators_bitlists.subrange_vec_dec bv (Big_int.of_int i) (Big_int.of_int j)) - | _ -> Extract (i, j, exp) - end - | Tester (str, exp) -> - let exp = simp_smt_exp vars kinds exp in - begin - match exp with - | Var v -> begin - match Hashtbl.find_opt kinds v with - | Some str' when str = str' -> Bool_lit true - | Some str' -> Bool_lit false - | None -> Tester (str, exp) - end - | _ -> Tester (str, exp) - end - | Syntactic (exp, _) -> exp - | SignExtend (i, exp) -> - let exp = simp_smt_exp vars kinds exp in - begin - match exp with - | Bitvec_lit bv -> Bitvec_lit (Sail2_operators_bitlists.sign_extend bv (Big_int.of_int (i + List.length bv))) - | _ -> SignExtend (i, exp) - end - | Forall (binders, exp) -> Forall (binders, exp) - -type read_info = { - name : string; - node : int; - active : smt_exp; - kind : smt_exp; - addr_type : smt_typ; - addr : smt_exp; - ret_type : smt_typ; - doc : string; -} - -type write_info = { - name : string; - node : int; - active : smt_exp; - kind : smt_exp; - addr_type : smt_typ; - addr : smt_exp; - data_type : smt_typ; - data : smt_exp; - doc : string; -} - -type barrier_info = { name : string; node : int; active : smt_exp; kind : smt_exp; doc : string } - -type branch_info = { name : string; node : int; active : smt_exp; addr_type : smt_typ; addr : smt_exp; doc : string } - -type cache_op_info = { - name : string; - node : int; - active : smt_exp; - kind : smt_exp; - addr_type : smt_typ; - addr : smt_exp; - doc : string; -} - -type smt_def = - | Define_fun of string * (string * smt_typ) list * smt_typ * smt_exp - | Declare_fun of string * smt_typ list * smt_typ - | Declare_const of string * smt_typ - | Define_const of string * smt_typ * smt_exp - (* Same as Define_const, but it'll never be removed by simplification *) - | Preserve_const of string * smt_typ * smt_exp - | Write_mem of write_info - | Write_mem_ea of string * int * smt_exp * smt_exp * smt_exp * smt_typ * smt_exp * smt_typ - | Read_mem of read_info - | Barrier of barrier_info - | Branch_announce of branch_info - | Cache_maintenance of cache_op_info - | Excl_res of string * int * smt_exp - | Declare_datatypes of string * (string * (string * smt_typ) list) list - | Declare_tuple of int - | Assert of smt_exp - -let smt_def_map_exp f = function - | Define_fun (name, args, ty, exp) -> Define_fun (name, args, ty, f exp) - | Declare_fun (name, args, ty) -> Declare_fun (name, args, ty) - | Declare_const (name, ty) -> Declare_const (name, ty) - | Define_const (name, ty, exp) -> Define_const (name, ty, f exp) - | Preserve_const (name, ty, exp) -> Preserve_const (name, ty, f exp) - | Write_mem w -> Write_mem { w with active = f w.active; kind = f w.kind; addr = f w.addr; data = f w.data } - | Write_mem_ea (name, node, active, wk, addr, addr_ty, data_size, data_size_ty) -> - Write_mem_ea (name, node, f active, f wk, f addr, addr_ty, f data_size, data_size_ty) - | Read_mem r -> Read_mem { r with active = f r.active; kind = f r.kind; addr = f r.addr } - | Barrier b -> Barrier { b with active = f b.active; kind = f b.kind } - | Cache_maintenance m -> Cache_maintenance { m with active = f m.active; kind = f m.kind; addr = f m.addr } - | Branch_announce c -> Branch_announce { c with active = f c.active; addr = f c.addr } - | Excl_res (name, node, active) -> Excl_res (name, node, f active) - | Declare_datatypes (name, ctors) -> Declare_datatypes (name, ctors) - | Declare_tuple n -> Declare_tuple n - | Assert exp -> Assert (f exp) - -let smt_def_iter_exp f = function - | Define_fun (name, args, ty, exp) -> f exp - | Define_const (name, ty, exp) -> f exp - | Preserve_const (name, ty, exp) -> f exp - | Write_mem w -> - f w.active; - f w.kind; - f w.addr; - f w.data - | Write_mem_ea (name, node, active, wk, addr, addr_ty, data_size, data_size_ty) -> - f active; - f wk; - f addr; - f data_size - | Read_mem r -> - f r.active; - f r.kind; - f r.addr - | Barrier b -> - f b.active; - f b.kind - | Cache_maintenance m -> - f m.active; - f m.kind; - f m.addr - | Branch_announce c -> - f c.active; - f c.addr - | Excl_res (name, node, active) -> f active - | Assert exp -> f exp - | Declare_fun _ | Declare_const _ | Declare_tuple _ | Declare_datatypes _ -> () - -let declare_datatypes = function Datatype (name, ctors) -> Declare_datatypes (name, ctors) | _ -> assert false - -(** For generating SMT with multiple threads (i.e. for litmus tests), - we suffix all the variables in the generated SMT with a thread - identifier to avoid any name clashes between the two threads. *) - -let suffix_variables_exp sfx = - fold_smt_exp (function Var v -> Var (v ^ sfx) | Read_res v -> Read_res (v ^ sfx) | exp -> exp) - -let suffix_variables_read_info sfx (r : read_info) = - let suffix exp = suffix_variables_exp sfx exp in - { r with name = r.name ^ sfx; active = suffix r.active; kind = suffix r.kind; addr = suffix r.addr } - -let suffix_variables_write_info sfx (w : write_info) = - let suffix exp = suffix_variables_exp sfx exp in - { - w with - name = w.name ^ sfx; - active = suffix w.active; - kind = suffix w.kind; - addr = suffix w.addr; - data = suffix w.data; - } - -let suffix_variables_barrier_info sfx (b : barrier_info) = - let suffix exp = suffix_variables_exp sfx exp in - { b with name = b.name ^ sfx; active = suffix b.active; kind = suffix b.kind } - -let suffix_variables_branch_info sfx (c : branch_info) = - let suffix exp = suffix_variables_exp sfx exp in - { c with name = c.name ^ sfx; active = suffix c.active; addr = suffix c.addr } - -let suffix_variables_cache_op_info sfx (m : cache_op_info) = - let suffix exp = suffix_variables_exp sfx exp in - { m with name = m.name ^ sfx; kind = suffix m.kind; active = suffix m.active; addr = suffix m.addr } - -let suffix_variables_def sfx = function - | Define_fun (name, args, ty, exp) -> - Define_fun (name ^ sfx, List.map (fun (arg, ty) -> (sfx ^ arg, ty)) args, ty, suffix_variables_exp sfx exp) - | Declare_fun (name, tys, ty) -> Declare_fun (name ^ sfx, tys, ty) - | Declare_const (name, ty) -> Declare_const (name ^ sfx, ty) - | Define_const (name, ty, exp) -> Define_const (name ^ sfx, ty, suffix_variables_exp sfx exp) - | Preserve_const (name, ty, exp) -> Preserve_const (name, ty, suffix_variables_exp sfx exp) - | Write_mem w -> Write_mem (suffix_variables_write_info sfx w) - | Write_mem_ea (name, node, active, wk, addr, addr_ty, data_size, data_size_ty) -> - Write_mem_ea - ( name ^ sfx, - node, - suffix_variables_exp sfx active, - suffix_variables_exp sfx wk, - suffix_variables_exp sfx addr, - addr_ty, - suffix_variables_exp sfx data_size, - data_size_ty - ) - | Read_mem r -> Read_mem (suffix_variables_read_info sfx r) - | Barrier b -> Barrier (suffix_variables_barrier_info sfx b) - | Cache_maintenance m -> Cache_maintenance (suffix_variables_cache_op_info sfx m) - | Branch_announce c -> Branch_announce (suffix_variables_branch_info sfx c) - | Excl_res (name, node, active) -> Excl_res (name ^ sfx, node, suffix_variables_exp sfx active) - | Declare_datatypes (name, ctors) -> Declare_datatypes (name, ctors) - | Declare_tuple n -> Declare_tuple n - | Assert exp -> Assert (suffix_variables_exp sfx exp) - -let pp_sfun str docs = - let open PPrint in - parens (separate space (string str :: docs)) - -let rec pp_smt_typ = - let open PPrint in - function - | Bool -> string "Bool" - | String -> string "String" - | Real -> string "Real" - | Bitvec n -> string (Printf.sprintf "(_ BitVec %d)" n) - | Datatype (name, _) -> string name - | Tuple tys -> pp_sfun ("Tup" ^ string_of_int (List.length tys)) (List.map pp_smt_typ tys) - | Array (ty1, ty2) -> pp_sfun "Array" [pp_smt_typ ty1; pp_smt_typ ty2] - -let pp_str_smt_typ (str, ty) = - let open PPrint in - parens (string str ^^ space ^^ pp_smt_typ ty) - -let rec pp_smt_exp = - let open PPrint in - function - | Bool_lit b -> string (string_of_bool b) - | Real_lit str -> string str - | String_lit str -> string ("\"" ^ str ^ "\"") - | Bitvec_lit bv -> string (Sail2_values.show_bitlist_prefix '#' bv) - | Var str -> string str - | Shared str -> string str - | Read_res str -> string (str ^ "_ret") - | Enum str -> string str - | Fn (str, exps) -> parens (string str ^^ space ^^ separate_map space pp_smt_exp exps) - | Field (str, exp) -> parens (string str ^^ space ^^ pp_smt_exp exp) - | Struct (str, fields) -> parens (string str ^^ space ^^ separate_map space (fun (_, exp) -> pp_smt_exp exp) fields) - | Ctor (str, exps) -> parens (string str ^^ space ^^ separate_map space pp_smt_exp exps) - | Ite (cond, then_exp, else_exp) -> - parens (separate space [string "ite"; pp_smt_exp cond; pp_smt_exp then_exp; pp_smt_exp else_exp]) - | Extract (i, j, exp) -> parens (string (Printf.sprintf "(_ extract %d %d)" i j) ^^ space ^^ pp_smt_exp exp) - | Tester (kind, exp) -> parens (string (Printf.sprintf "(_ is %s)" kind) ^^ space ^^ pp_smt_exp exp) - | SignExtend (i, exp) -> parens (string (Printf.sprintf "(_ sign_extend %d)" i) ^^ space ^^ pp_smt_exp exp) - | Syntactic (exp, _) -> pp_smt_exp exp - | Forall (binders, exp) -> - parens (string "forall" ^^ space ^^ parens (separate_map space pp_str_smt_typ binders) ^^ space ^^ pp_smt_exp exp) - -let pp_smt_def = - let open PPrint in - let open Printf in - function - | Define_fun (name, args, ty, exp) -> - parens - (string "define-fun" ^^ space ^^ string name ^^ space - ^^ parens (separate_map space pp_str_smt_typ args) - ^^ space ^^ pp_smt_typ ty ^//^ pp_smt_exp exp - ) - | Declare_fun (name, args, ty) -> - parens - (string "declare-fun" ^^ space ^^ string name ^^ space - ^^ parens (separate_map space pp_smt_typ args) - ^^ space ^^ pp_smt_typ ty - ) - | Declare_const (name, ty) -> pp_sfun "declare-const" [string name; pp_smt_typ ty] - | Define_const (name, ty, exp) | Preserve_const (name, ty, exp) -> - pp_sfun "define-const" [string name; pp_smt_typ ty; pp_smt_exp exp] - | Write_mem w -> - pp_sfun "define-const" [string (w.name ^ "_kind"); string "Zwrite_kind"; pp_smt_exp w.kind] - ^^ hardline - ^^ pp_sfun "define-const" [string (w.name ^ "_active"); pp_smt_typ Bool; pp_smt_exp w.active] - ^^ hardline - ^^ pp_sfun "define-const" [string (w.name ^ "_data"); pp_smt_typ w.data_type; pp_smt_exp w.data] - ^^ hardline - ^^ pp_sfun "define-const" [string (w.name ^ "_addr"); pp_smt_typ w.addr_type; pp_smt_exp w.addr] - ^^ hardline - ^^ pp_sfun "declare-const" [string (w.name ^ "_ret"); pp_smt_typ Bool] - | Write_mem_ea (name, _, active, wk, addr, addr_ty, data_size, data_size_ty) -> - pp_sfun "define-const" [string (name ^ "_kind"); string "Zwrite_kind"; pp_smt_exp wk] - ^^ hardline - ^^ pp_sfun "define-const" [string (name ^ "_active"); pp_smt_typ Bool; pp_smt_exp active] - ^^ hardline - ^^ pp_sfun "define-const" [string (name ^ "_size"); pp_smt_typ data_size_ty; pp_smt_exp data_size] - ^^ hardline - ^^ pp_sfun "define-const" [string (name ^ "_addr"); pp_smt_typ addr_ty; pp_smt_exp addr] - | Read_mem r -> - pp_sfun "define-const" [string (r.name ^ "_kind"); string "Zread_kind"; pp_smt_exp r.kind] - ^^ hardline - ^^ pp_sfun "define-const" [string (r.name ^ "_active"); pp_smt_typ Bool; pp_smt_exp r.active] - ^^ hardline - ^^ pp_sfun "define-const" [string (r.name ^ "_addr"); pp_smt_typ r.addr_type; pp_smt_exp r.addr] - ^^ hardline - ^^ pp_sfun "declare-const" [string (r.name ^ "_ret"); pp_smt_typ r.ret_type] - | Barrier b -> - pp_sfun "define-const" [string (b.name ^ "_kind"); string "Zbarrier_kind"; pp_smt_exp b.kind] - ^^ hardline - ^^ pp_sfun "define-const" [string (b.name ^ "_active"); pp_smt_typ Bool; pp_smt_exp b.active] - | Cache_maintenance m -> - pp_sfun "define-const" [string (m.name ^ "_active"); pp_smt_typ Bool; pp_smt_exp m.active] - ^^ hardline - ^^ pp_sfun "define-const" [string (m.name ^ "_kind"); string "Zcache_op_kind"; pp_smt_exp m.kind] - ^^ hardline - ^^ pp_sfun "define-const" [string (m.name ^ "_addr"); pp_smt_typ m.addr_type; pp_smt_exp m.addr] - | Branch_announce c -> - pp_sfun "define-const" [string (c.name ^ "_active"); pp_smt_typ Bool; pp_smt_exp c.active] - ^^ hardline - ^^ pp_sfun "define-const" [string (c.name ^ "_addr"); pp_smt_typ c.addr_type; pp_smt_exp c.addr] - | Excl_res (name, _, active) -> - pp_sfun "declare-const" [string (name ^ "_res"); pp_smt_typ Bool] - ^^ hardline - ^^ pp_sfun "define-const" [string (name ^ "_active"); pp_smt_typ Bool; pp_smt_exp active] - | Declare_datatypes (name, ctors) -> - let pp_ctor (ctor_name, fields) = - match fields with [] -> parens (string ctor_name) | _ -> pp_sfun ctor_name (List.map pp_str_smt_typ fields) - in - pp_sfun "declare-datatypes" - [Printf.ksprintf string "((%s 0))" name; parens (parens (separate_map space pp_ctor ctors))] - | Declare_tuple n -> - let par = separate_map space string (Util.list_init n (fun i -> "T" ^ string_of_int i)) in - let fields = separate space (Util.list_init n (fun i -> Printf.ksprintf string "(tup_%d_%d T%d)" n i i)) in - pp_sfun "declare-datatypes" - [ - Printf.ksprintf string "((Tup%d %d))" n n; - parens - (parens - (separate space - [string "par"; parens par; parens (parens (ksprintf string "tup%d" n ^^ space ^^ fields))] - ) - ); - ] - | Assert exp -> pp_sfun "assert" [pp_smt_exp exp] - -let string_of_smt_def def = Pretty_print_sail.to_string (pp_smt_def def) - -let output_smt_defs out_chan smt = List.iter (fun def -> output_string out_chan (string_of_smt_def def ^ "\n")) smt - -(**************************************************************************) -(* 2. Parser for SMT solver output *) -(**************************************************************************) - -(* Output format from each SMT solver does not seem to be completely - standardised, unlike the SMTLIB input format, but usually is some - form of s-expression based representation. Therefore we define a - simple parser for s-expressions using monadic parser combinators. *) - -type sexpr = List of sexpr list | Atom of string - -let rec string_of_sexpr = function - | List sexprs -> "(" ^ Util.string_of_list " " string_of_sexpr sexprs ^ ")" - | Atom str -> str - -open Parser_combinators - -let lparen = token (function Str.Delim "(" -> Some () | _ -> None) -let rparen = token (function Str.Delim ")" -> Some () | _ -> None) -let atom = token (function Str.Text str -> Some str | _ -> None) - -let rec sexp toks = - let parse = - pchoose - (atom >>= fun str -> preturn (Atom str)) - ( lparen >>= fun _ -> - plist sexp >>= fun xs -> - rparen >>= fun _ -> preturn (List xs) - ) - in - parse toks - -let parse_sexps input = - let delim = Str.regexp "[ \n\t]+\\|(\\|)" in - let tokens = Str.full_split delim input in - let non_whitespace = function Str.Delim d when String.trim d = "" -> false | _ -> true in - let tokens = List.filter non_whitespace tokens in - match plist sexp tokens with Ok (result, _) -> result | Fail -> failwith "Parse failure" - -let parse_sexpr_int width = function - | List [Atom "_"; Atom v; Atom m] when int_of_string m = width && String.length v > 2 && String.sub v 0 2 = "bv" -> - let v = String.sub v 2 (String.length v - 2) in - Some (Big_int.of_string v) - | Atom v when String.length v > 2 && String.sub v 0 2 = "#b" -> - let v = String.sub v 2 (String.length v - 2) in - Some (Big_int.of_string ("0b" ^ v)) - | Atom v when String.length v > 2 && String.sub v 0 2 = "#x" -> - let v = String.sub v 2 (String.length v - 2) in - Some (Big_int.of_string ("0x" ^ v)) - | _ -> None - -let rec value_of_sexpr sexpr = - let open Jib in - let open Value in - function - | CT_fbits width -> begin - match parse_sexpr_int width sexpr with - | Some value -> mk_vector (Sail_lib.get_slice_int' (width, value, 0)) - | None -> failwith ("Cannot parse sexpr as bitvector: " ^ string_of_sexpr sexpr) - end - | CT_struct (_, fields) -> begin - match sexpr with - | List (Atom name :: smt_fields) -> - V_record - (List.fold_left2 - (fun m (field_id, ctyp) sexpr -> StringMap.add (string_of_id field_id) (value_of_sexpr sexpr ctyp) m) - StringMap.empty fields smt_fields - ) - | _ -> failwith ("Cannot parse sexpr as struct " ^ string_of_sexpr sexpr) - end - | CT_enum (_, members) -> begin - match sexpr with - | Atom name -> begin - match List.find_opt (fun member -> Util.zencode_string (string_of_id member) = name) members with - | Some member -> V_member (string_of_id member) - | None -> - failwith - ("Could not find enum member for " ^ name ^ " in " ^ Util.string_of_list ", " string_of_id members) - end - | _ -> failwith ("Cannot parse sexpr as enum " ^ string_of_sexpr sexpr) - end - | CT_bool -> begin - match sexpr with - | Atom "true" -> V_bool true - | Atom "false" -> V_bool false - | _ -> failwith ("Cannot parse sexpr as bool " ^ string_of_sexpr sexpr) - end - | CT_fint width -> begin - match parse_sexpr_int width sexpr with - | Some value -> V_int value - | None -> failwith ("Cannot parse sexpr as fixed-width integer: " ^ string_of_sexpr sexpr) - end - | ctyp -> failwith ("Unsupported type in sexpr: " ^ Jib_util.string_of_ctyp ctyp) - -let rec find_arg id ctyp arg_smt_names = function - | List [Atom "define-fun"; Atom str; List []; _; value] :: _ - when Util.assoc_compare_opt Id.compare id arg_smt_names = Some (Some str) -> - (id, value_of_sexpr value ctyp) - | _ :: sexps -> find_arg id ctyp arg_smt_names sexps - | [] -> (id, V_unit) - -let build_counterexample args arg_ctyps arg_smt_names model = - List.map2 (fun id ctyp -> find_arg id ctyp arg_smt_names model) args arg_ctyps - -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) - -let check_counterexample ast env fname function_id args arg_ctyps arg_smt_names = - let open Printf in - print_endline ("Checking counterexample: " ^ fname); - let in_chan = ksprintf Unix.open_process_in "%s %s" (counterexample_command !opt_auto_solver) fname in - let lines = ref [] in - begin - try - while true do - lines := input_line in_chan :: !lines - done - with End_of_file -> () - end; - let solver_output = List.rev !lines |> String.concat "\n" in - begin - match solver_output |> parse_sexps with - | Atom "sat" :: (List (Atom "model" :: model) | List model) :: _ -> - let open Value in - let open Interpreter in - print_endline (sprintf "Solver found counterexample: %s" Util.("ok" |> green |> clear)); - let counterexample = build_counterexample args arg_ctyps arg_smt_names model in - List.iter (fun (id, v) -> print_endline (" " ^ string_of_id id ^ " -> " ^ string_of_value v)) counterexample; - let istate = initial_state ast env !primops in - let annot = (Parse_ast.Unknown, Type_check.mk_tannot env bool_typ) in - let call = - E_aux - ( E_app - ( function_id, - List.map - (fun (_, v) -> E_aux (E_internal_value v, (Parse_ast.Unknown, Type_check.empty_tannot))) - counterexample - ), - annot - ) - in - let result = run (Step (lazy "", istate, return call, [])) in - begin - match result with - | Some (V_bool false) | None -> - ksprintf print_endline "Replaying counterexample: %s" Util.("ok" |> green |> clear) - | _ -> () - end - | Atom "unsat" :: _ -> - print_endline "Solver could not find counterexample"; - print_endline "Solver output:"; - print_endline solver_output - | _ -> - print_endline "Unexpected solver output:"; - print_endline solver_output - end; - let status = Unix.close_process_in in_chan in - () diff --git a/src/sail_sv_backend/jib_sv.ml b/src/sail_sv_backend/jib_sv.ml index d74e2df90..e212169af 100644 --- a/src/sail_sv_backend/jib_sv.ml +++ b/src/sail_sv_backend/jib_sv.ml @@ -331,6 +331,7 @@ module Make (Config : CONFIG) = struct let max_unknown_bitvector_width = Config.max_unknown_bitvector_width let max_unknown_generic_vector_length = 32 let union_ctyp_classify = is_packed + let register_ref reg_name = Fn ("reg_ref", [String_lit reg_name]) end) (struct let print_bits l = function diff --git a/test/smt/lzcnt.unsat.sail b/test/smt/lzcnt.unsat.sail index b627c9e54..822b85863 100644 --- a/test/smt/lzcnt.unsat.sail +++ b/test/smt/lzcnt.unsat.sail @@ -2,7 +2,7 @@ default Order dec $include -val lzcnt = "count_leading_zeros" : forall 'w. bits('w) -> range(0, 'w) +val lzcnt = pure "count_leading_zeros" : forall 'w. bits('w) -> range(0, 'w) $property function prop() -> bool = { diff --git a/test/smt/revrev_endianness2.unsat.sail b/test/smt/revrev_endianness2.unsat.sail index 33ba93a22..2ab0e550b 100644 --- a/test/smt/revrev_endianness2.unsat.sail +++ b/test/smt/revrev_endianness2.unsat.sail @@ -1,8 +1,10 @@ default Order dec +$option -smt_bits_size 128 + $include -$property +$counterexample function prop forall 'n, 'n in {8, 16, 32, 64, 128}. (n: int('n), xs: bits('n)) -> bool = { if length(xs) == 8 then { reverse_endianness(reverse_endianness(xs)) == xs diff --git a/test/smt/revrev_endianness3.unsat.sail b/test/smt/revrev_endianness3.unsat.sail new file mode 100644 index 000000000..a75049596 --- /dev/null +++ b/test/smt/revrev_endianness3.unsat.sail @@ -0,0 +1,22 @@ +default Order dec + +$option -smt_bits_size 128 + +$include +$include + +$property +function prop forall 'n, 'n in {8, 16, 32, 64, 128}. (n: int('n), xs: bits(128)) -> bool = { + let xs = xs[n - 1 .. 0] in + if length(xs) == 8 then { + reverse_endianness(reverse_endianness(xs)) == xs + } else if length(xs) == 16 then { + reverse_endianness(reverse_endianness(xs)) == xs + } else if length(xs) == 32 then { + reverse_endianness(reverse_endianness(xs)) == xs + } else if length(xs) == 64 then { + reverse_endianness(reverse_endianness(xs)) == xs + } else { + reverse_endianness(reverse_endianness(xs)) == xs + } +} diff --git a/test/smt/run_tests.py b/test/smt/run_tests.py index 77f157967..5d035f402 100755 --- a/test/smt/run_tests.py +++ b/test/smt/run_tests.py @@ -20,7 +20,11 @@ 'assembly_mapping_sat': { 'z3', 'cvc4' }, # This test using unsupported CVC4 features 'arith_unsat': { 'z3', 'cvc4' }, 'arith_LFL_unsat' : { 'z3', 'cvc4' }, - 'revrev_endianness2_unsat' : { 'z3', 'cvc4' }, # There is some bug in this test + 'revrev_endianness2_unsat' : { 'z3', 'cvc4' }, # This test has a variable width bitvector as an argument, which lacks a well-formedness predicate + 'store_load_sat' : { 'z3', 'cvc4' }, + 'load_store_dep_sat' : { 'z3', 'cvc4' }, + 'store_load_scattered_sat' : { 'z3', 'cvc4' }, + 'mem_builtins_unsat' : { 'z3', 'cvc4' }, } print("Sail is {}".format(sail))