Skip to content

Commit

Permalink
Fix more SMT tests with new SMT/SV backend
Browse files Browse the repository at this point in the history 
Currently the only failing tests are those involving memory ops,
which we no longer support here.
  • Loading branch information
@Alasdair
Alasdair committed May 2, 2024
1 parent af4c4ba commit e4a1fb3
Show file tree
Hide file tree
Showing 12 changed files with 576 additions and 1,045 deletions.
324 changes: 168 additions & 156 deletions src/lib/smt_exp.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -324,165 +325,176 @@ 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"

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
Loading

0 comments on commit e4a1fb3

Please sign in to comment.