Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make solver output failsafe #462

Merged
merged 1 commit into from
Mar 1, 2024
Merged

Make solver output failsafe #462

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 9 additions & 6 deletions src/sail_smt_backend/smtlib.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -690,7 +690,7 @@ let rec run frame =

let check_counterexample ast env fname function_id args arg_ctyps arg_smt_names =
let open Printf in
prerr_endline ("Checking counterexample: " ^ fname);
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
Expand All @@ -700,15 +700,15 @@ let check_counterexample ast env fname function_id args arg_ctyps arg_smt_names
done
with End_of_file -> ()
end;
let solver_output = List.rev !lines |> String.concat "\n" |> parse_sexps in
let solver_output = List.rev !lines |> String.concat "\n" in
begin
match solver_output with
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) -> prerr_endline (" " ^ string_of_id id ^ " -> " ^ string_of_value v)) counterexample;
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 =
Expand All @@ -729,10 +729,13 @@ let check_counterexample ast env fname function_id args arg_ctyps arg_smt_names
ksprintf print_endline "Replaying counterexample: %s" Util.("ok" |> green |> clear)
| _ -> ()
end
| _ ->
| Atom "unsat" :: _ ->
print_endline "Solver could not find counterexample";
print_endline "Solver output:";
List.iter print_endline !lines
print_endline solver_output
| _ ->
print_endline "Unexpected solver output:";
print_endline solver_output
end;
let status = Unix.close_process_in in_chan in
()
Loading