SMT: Add parser for generated models

Simple parser-combinator style parser for generated models. It's
actually quite tricky to reconstruct the models because we can have:

let x = something

$counterexample
function prop(x: bits(32)) -> bool = ...

where the function argument becomes zx/1 rather than zx/0, which is what
we'd expect for the argument of a property. Might need to do something
smarter with encoding locations into smt names to figure out what SMT
variables correspond to which souce variables exactly. The above
also previously generated incorrect SMT, which has now been fixed.

4 files changed, 156 insertions, 32 deletions

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 60b7202b..04546e3e 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -61,6 +61,8 @@ let zencode_name id = string_of_name ~deref_current_exception:false ~zencode:tru
 
 let opt_ignore_overflow = ref false
 
+let opt_auto = ref false
+
 type ctx = {
     (* Arbitrary-precision bitvectors are represented as a (BitVec lbits_index, BitVec (2 ^ lbits_index)) pair. *)
     lbits_index : int;
@@ -498,7 +500,7 @@ let builtin_sign_extend ctx vbits vlen ret_ctyp =
      let top_bit_one = Fn ("=", [Extract (n - 1, n - 1, bv); Bin "1"]) in
      Ite (top_bit_one, Fn ("concat", [bvones (m - n); bv]), Fn ("concat", [bvzero (m - n); bv]))
 
-  | _ -> failwith "Cannot compile zero_extend"
+  | _ -> builtin_type_error "sign_extend" [vbits; vlen] (Some ret_ctyp)
 
 let builtin_shift shiftop ctx vbits vshift ret_ctyp =
   match cval_ctyp vbits with
@@ -512,7 +514,7 @@ let builtin_shift shiftop ctx vbits vshift ret_ctyp =
      let shift = bvzeint ctx (lbits_size ctx) vshift in
      Fn ("Bits", [Fn ("len", [bv]); Fn (shiftop, [Fn ("contents", [bv]); shift])])
 
-  | _ -> failwith ("Cannot compile shift: " ^ shiftop)
+  | _ -> builtin_type_error shiftop [vbits; vshift] (Some ret_ctyp)
 
 let builtin_not_bits ctx v ret_ctyp =
   match cval_ctyp v, ret_ctyp with
@@ -529,35 +531,23 @@ let builtin_not_bits ctx v ret_ctyp =
 
   | _, _ -> builtin_type_error "not_bits" [v] (Some ret_ctyp)
 
-let builtin_or_bits ctx v1 v2 ret_ctyp =
+let builtin_bitwise fn ctx v1 v2 ret_ctyp =
   match cval_ctyp v1, cval_ctyp v2 with
   | CT_fbits (n, _), CT_fbits (m, _) ->
      assert (n = m);
      let smt1 = smt_cval ctx v1 in
      let smt2 = smt_cval ctx v2 in
-     bvor smt1 smt2
+     Fn (fn, [smt1; smt2])
 
   | CT_lbits _, CT_lbits _ ->
      let smt1 = smt_cval ctx v1 in
      let smt2 = smt_cval ctx v2 in
-     Fn ("Bits", [Fn ("len", [smt1]); bvor (Fn ("contents", [smt1])) (Fn ("contents", [smt2]))])
-
-  | _ -> failwith "Cannot compile or_bits"
-
-let builtin_and_bits ctx v1 v2 ret_ctyp =
-  match cval_ctyp v1, cval_ctyp v2 with
-  | CT_fbits (n, _), CT_fbits (m, _) ->
-     assert (n = m);
-     let smt1 = smt_cval ctx v1 in
-     let smt2 = smt_cval ctx v2 in
-     bvand smt1 smt2
+     Fn ("Bits", [Fn ("len", [smt1]); Fn (fn, [Fn ("contents", [smt1]); Fn ("contents", [smt2])])])
 
-  | CT_lbits _, CT_lbits _ ->
-     let smt1 = smt_cval ctx v1 in
-     let smt2 = smt_cval ctx v2 in
-     Fn ("Bits", [Fn ("len", [smt1]); bvand (Fn ("contents", [smt1])) (Fn ("contents", [smt2]))])
+  | _ -> builtin_type_error fn [v1; v2] (Some ret_ctyp)
 
-  | _ -> failwith "Cannot compile or_bits"
+let builtin_and_bits = builtin_bitwise "bvand"
+let builtin_or_bits = builtin_bitwise "bvor"
 
 let builtin_append ctx v1 v2 ret_ctyp =
   match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
@@ -663,7 +653,7 @@ let builtin_unsigned ctx v ret_ctyp =
        let smt = smt_cval ctx v in
        Fn ("concat", [bvzero (ctx.lint_size - n); smt])
 
-  | ctyp, _ -> failwith (Printf.sprintf "Cannot compile unsigned : %s -> %s" (string_of_ctyp ctyp) (string_of_ctyp ret_ctyp))
+  | ctyp, _ -> builtin_type_error "unsigned" [v] (Some ret_ctyp)
 
 let builtin_signed ctx v ret_ctyp =
   match cval_ctyp v, ret_ctyp with
@@ -1016,10 +1006,7 @@ let rec ctyp_of_typ ctx typ =
   | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" ->
      CT_list (ctyp_of_typ ctx typ)
 
-  (* When converting a sail bitvector type into C, we have three options in order of efficiency:
-     - If the length is obviously static and smaller than 64, use the fixed bits type (aka uint64_t), fbits.
-     - If the length is less than 64, then use a small bits type, sbits.
-     - If the length may be larger than 64, use a large bits type lbits. *)
+  (* Note that we have to use lbits for zero-length bitvectors because they are not allowed by SMTLIB *)
   | Typ_app (id, [A_aux (A_nexp n, _);
                   A_aux (A_order ord, _);
                   A_aux (A_typ (Typ_aux (Typ_id vtyp_id, _)), _)])
@@ -1477,14 +1464,12 @@ let smt_cdef props lets name_file ctx all_cdefs = function
         let stack = Stack.create () in
 
         smt_header ctx stack all_cdefs;
-        let smt_args =
-          List.map2 (fun id ctyp -> declare_const ctx (Name (id, 0)) ctyp) args arg_ctyps
+        let arg_decls =
+          List.map2 (fun id ctyp -> idecl ctyp (name id)) args arg_ctyps
         in
-        push_smt_defs stack smt_args;
-
         let instrs =
           let open Jib_optimize in
-          (lets @ intervening_lets @ instrs)
+          (lets @ intervening_lets @ arg_decls @ instrs)
           |> inline all_cdefs (fun _ -> true)
           |> List.map (map_instr (expand_reg_deref ctx))
           |> flatten_instrs
@@ -1516,7 +1501,8 @@ let smt_cdef props lets name_file ctx all_cdefs = function
             end
           ) visit_order;
 
-        let out_chan = open_out (name_file (string_of_id function_id)) in
+        let fname = name_file (string_of_id function_id) in
+        let out_chan = open_out fname in
         if prop_type = "counterexample" then
           output_string out_chan "(set-option :produce-models true)\n";
         output_string out_chan "(set-logic QF_AUFBVDT)\n";
@@ -1529,7 +1515,11 @@ let smt_cdef props lets name_file ctx all_cdefs = function
 
         output_string out_chan "(check-sat)\n";
         if prop_type = "counterexample" then
-          output_string out_chan "(get-model)\n"
+          output_string out_chan "(get-model)\n";
+
+        close_out out_chan;
+        if prop_type = "counterexample" then
+          check_counterexample fname args
 
      | _ -> failwith "Bad function body"
      end
diff --git a/src/sail.ml b/src/sail.ml
index d9f4c55a..4be5279d 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -127,6 +127,9 @@ let options = Arg.align ([
   ( "-smt",
     set_target "smt",
     " print SMT translated version of input");
+  ( "-smt_auto",
+    Arg.Tuple [set_target "smt"; Arg.Set Jib_smt.opt_auto],
+    " generate SMT and automatically call the solver (implies -smt)");
   ( "-smt_ignore_overflow",
     Arg.Set Jib_smt.opt_ignore_overflow,
     " ignore integer overflow in generated SMT");
diff --git a/src/smtlib.ml b/src/smtlib.ml
index 7d6bb564..2b874a03 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -48,6 +48,9 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
+open Ast
+open Ast_util
+
 type smt_typ =
   | Bitvec of int
   | Bool
@@ -244,3 +247,121 @@ 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
+
+type 'a parse_result =
+  | Ok of 'a * Str.split_result list
+  | Fail
+
+type 'a parser = Str.split_result list -> 'a parse_result
+
+let (>>=) (m : 'a parser) (f : 'a -> 'b parser) (toks : Str.split_result list) =
+  match m toks with
+  | Ok (r, toks) -> f r toks
+  | Fail -> Fail
+
+let pmap f m toks =
+  match m toks with
+  | Ok (r, toks) -> Ok (f r, toks)
+  | Fail -> Fail
+
+let token f = function
+  | tok :: toks ->
+     begin match f tok with
+     | Some x -> Ok (x, toks)
+     | None -> Fail
+     end
+  | [] -> Fail
+
+let preturn x toks = Ok (x, toks)
+
+let rec plist m toks =
+  match m toks with
+  | Ok (x, toks) ->
+     begin match plist m toks with
+     | Ok (xs, toks) -> Ok (x :: xs, toks)
+     | Fail -> Fail
+     end
+  | Fail -> Ok ([], toks)
+
+let pchoose m n toks =
+  match m toks with
+  | Fail -> n toks
+  | Ok (x, toks) -> Ok (x, toks)
+
+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 "(" | Str.Delim ")" | Str.Text _ -> true
+    | Str.Delim _ -> false
+  in
+  let tokens = List.filter non_whitespace tokens in
+  match plist sexp tokens with
+  | Ok (result, _) -> result
+  | Fail -> failwith "Parse failure"
+
+let rec find_arg id = function
+  | List [Atom "define-fun"; Atom str; List []; _; value] :: _ when (Ast_util.string_of_id id ^ "/0") = str ->
+     Some (id, value)
+  | _ :: sexps -> find_arg id sexps
+  | [] -> None
+
+let build_counterexample args sexps =
+  Util.map_filter (fun id -> find_arg id sexps) args
+  |> List.fold_left (fun m (k, v) -> Bindings.add k v m) Bindings.empty
+
+let check_counterexample fname args =
+  let open Printf in
+  prerr_endline ("Checking counterexample: " ^ fname ^ Util.string_of_list ", " Ast_util.string_of_id args);
+  let in_chan = ksprintf Unix.open_process_in "cvc4 --lang=smt2.6 %s" 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" |> parse_sexps in
+  begin match solver_output with
+  | Atom "sat" :: List (Atom "model" :: model) :: _ ->
+     prerr_endline (sprintf "Solver found counterexample: %s" Util.("success" |> green |> clear));
+     let counterexample = build_counterexample args model in
+     if not (Bindings.cardinal counterexample = List.length args) then
+       ksprintf prerr_endline "Could not find all arguments in model %s" Util.("failure" |> red |> clear);
+  | _ ->
+     prerr_endline "failure"
+  end;
+  let status = Unix.close_process_in in_chan in
+  ()
diff --git a/test/smt/tl_let_shadow.sat.sail b/test/smt/tl_let_shadow.sat.sail
new file mode 100644
index 00000000..b8830a09
--- /dev/null
+++ b/test/smt/tl_let_shadow.sat.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+let xs = 0xFFFF_FFFF
+
+$counterexample
+function prop(xs: bits(32)) -> bool = {
+  xs == 0xFFFF_FFFF
+}
\ No newline at end of file