From b25d0fa63eddeeeb4c991c99325f9f342a9af33c 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 | 31 +++++++++++++++++++++++-- 3 files changed, 38 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..aebd360e0 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,34 @@ 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 + | 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_ctor (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 | cty -> failwith ("Unsupported type in sexpr: " ^ Jib_util.string_of_ctyp cty)