From 966424f5ba2b0133a42584cbb68f032f3b9306de Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 29 Feb 2024 12:45:06 +0000 Subject: [PATCH] Parse structs in SMT counterexamples --- src/sail_smt_backend/jib_smt.ml | 10 ++++++++-- src/sail_smt_backend/sail_plugin_smt.ml | 2 +- src/sail_smt_backend/smtlib.ml | 14 ++++++++++++-- 3 files changed, 21 insertions(+), 5 deletions(-) diff --git a/src/sail_smt_backend/jib_smt.ml b/src/sail_smt_backend/jib_smt.ml index bacbaf8d0..3b7dce0e9 100644 --- a/src/sail_smt_backend/jib_smt.ml +++ b/src/sail_smt_backend/jib_smt.ml @@ -2257,8 +2257,14 @@ let smt_cdef props lets name_file ctx all_cdefs smt_includes = function let header = smt_header ctx all_cdefs in - if !(ctx.use_string) || !(ctx.use_real) then output_string out_chan "(set-logic ALL)\n" - else output_string out_chan "(set-logic QF_AUFBVFPDT)\n"; + (* If the solver is Z3, don't output a logic as Z3 will infer it. *) + begin + match !opt_auto_solver with + | Z3 -> () + | _ -> + if !(ctx.use_string) || !(ctx.use_real) then output_string out_chan "(set-logic ALL)\n" + else output_string out_chan "(set-logic QF_AUFBVFPDT)\n" + end; List.iter (fun def -> diff --git a/src/sail_smt_backend/sail_plugin_smt.ml b/src/sail_smt_backend/sail_plugin_smt.ml index 472972d39..200e9f3c3 100644 --- a/src/sail_smt_backend/sail_plugin_smt.ml +++ b/src/sail_smt_backend/sail_plugin_smt.ml @@ -75,7 +75,7 @@ let set_auto_solver arg = let smt_options = [ - ("-smt_auto", Arg.Tuple [Arg.Set Jib_smt.opt_auto], " generate SMT and automatically call the smt solver"); + ("-smt_auto", Arg.Tuple [Arg.Set Jib_smt.opt_auto], " automatically call the smt solver on generated SMT"); ( "-smt_auto_solver", Arg.String set_auto_solver, " set the solver to use for counterexample checks (default cvc5)" diff --git a/src/sail_smt_backend/smtlib.ml b/src/sail_smt_backend/smtlib.ml index 279cf4765..4c6c86362 100644 --- a/src/sail_smt_backend/smtlib.ml +++ b/src/sail_smt_backend/smtlib.ml @@ -624,7 +624,7 @@ let parse_sexps input = let tokens = List.filter non_whitespace tokens in match plist sexp tokens with Ok (result, _) -> result | Fail -> failwith "Parse failure" -let value_of_sexpr sexpr = +let rec value_of_sexpr sexpr = let open Jib in let open Value in function @@ -639,7 +639,17 @@ let value_of_sexpr sexpr = | Atom v when String.length v > 2 && String.sub v 0 2 = "#x" -> let v = String.sub v 2 (String.length v - 2) in mk_vector (Sail_lib.get_slice_int' (n, Big_int.of_string ("0x" ^ v), 0)) - | _ -> failwith ("Cannot parse sexpr as ctyp: " ^ string_of_sexpr sexpr) + | _ -> 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 | cty -> failwith ("Unsupported type in sexpr: " ^ Jib_util.string_of_ctyp cty)