SMT: Allow custom queries

As an example:

$counterexample :query exist match_failure
function prop(xs: bits(4)) -> unit = {
  match xs {
    _ : bits(3) @ 0b0 => ()
  }
}

Will return

Solver found counterexample: ok
  xs -> 0x1

as we are asking for an input such that a match failure occurs,
meanwhile

$counterexample :query ~(exist match_failure)
function prop(xs: bits(4)) -> unit = {
  match xs {
    _ : bits(3) @ 0b0 => ()
  }
}

will return 0x0 as we are asking for an input such that no match
failure occurs. Note that we can now support properties for
non-boolean functions by not including the return event in the query.

4 files changed, 145 insertions, 38 deletions

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 9303051d..719f0b53 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -54,6 +54,7 @@ open Ast_util
 open Jib
 open Jib_util
 open Smtlib
+open Property
 
 module IntSet = Set.Make(struct type t = int let compare = compare end)
 module IntMap = Map.Make(struct type t = int let compare = compare end)
@@ -66,37 +67,6 @@ let opt_ignore_overflow = ref false
 
 let opt_auto = ref false
 
-type event = Overflow | Assertion | Assumption | Match | Return
-
-type query =
-   | Q_all of event   (* All events of type are true *)
-   | Q_exist of event (* Some event of type is true *)
-   | Q_not of query
-   | Q_and of query list
-   | Q_or of query list
-
-let default_query =
-  Q_or [Q_and [Q_all Assertion; Q_all Return; Q_not (Q_exist Match)]; Q_exist Overflow; Q_not (Q_all Assumption)]
-
-module Event = struct
-  type t = event
-  let compare e1 e2 =
-    match e1, e2 with
-    | Overflow, Overflow -> 0
-    | Assertion, Assertion -> 0
-    | Assumption, Assumption -> 0
-    | Match, Match -> 0
-    | Return, Return -> 0
-    | Overflow, _ -> 1
-    | _, Overflow -> -1
-    | Assertion, _ -> 1
-    | _, Assertion -> -1
-    | Assumption, _ -> 1
-    | _, Assumption -> -1
-    | Match, _ -> 1
-    | _, Match -> -1
-end
-
 module EventMap = Map.Make(Event)
 
 (* Note that we have to use x : ty ref rather than mutable x : ty, to
@@ -1585,6 +1555,8 @@ let smt_cdef props lets name_file ctx all_cdefs = function
      | intervening_lets, Some (None, args, instrs) ->
         let prop_type, prop_args, pragma_l, vs = Bindings.find function_id props in
 
+        let pragma = parse_pragma pragma_l prop_args in
+
         let stack = Stack.create () in
 
         let ctx = { ctx with events = ref EventMap.empty; pragma_l = pragma_l; arg_stack = Stack.create () } in
@@ -1604,8 +1576,8 @@ let smt_cdef props lets name_file ctx all_cdefs = function
           |> remove_pointless_goto
         in
 
-        let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Jib_util.pp_instr instrs) in
-        prerr_endline str;
+        (* let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Jib_util.pp_instr instrs) in
+        prerr_endline str; *)
 
         let open Jib_ssa in
         let start, cfg = ssa instrs in
@@ -1634,7 +1606,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function
             end
           ) visit_order;
 
-        let query = smt_query ctx default_query in
+        let query = smt_query ctx pragma.query in
         push_smt_defs stack [Assert (Fn ("not", [query]))];
 
         let fname = name_file (string_of_id function_id) in
diff --git a/src/property.ml b/src/property.ml
index 56bdbe2e..84e9d734 100644
--- a/src/property.ml
+++ b/src/property.ml
@@ -50,6 +50,7 @@
 
 open Ast
 open Ast_util
+open Smtlib
 
 let find_properties (Defs defs) =
   let rec find_prop acc = function
@@ -120,3 +121,103 @@ let add_property_guards props (Defs defs) =
 
 let rewrite defs =
   add_property_guards (find_properties defs) defs
+
+type event = Overflow | Assertion | Assumption | Match | Return
+
+type query =
+   | Q_all of event   (* All events of type are true *)
+   | Q_exist of event (* Some event of type is true *)
+   | Q_not of query
+   | Q_and of query list
+   | Q_or of query list
+
+let default_query =
+  Q_or [Q_and [Q_all Assertion; Q_all Return; Q_not (Q_exist Match)]; Q_exist Overflow; Q_not (Q_all Assumption)]
+
+module Event = struct
+  type t = event
+  let compare e1 e2 =
+    match e1, e2 with
+    | Overflow, Overflow -> 0
+    | Assertion, Assertion -> 0
+    | Assumption, Assumption -> 0
+    | Match, Match -> 0
+    | Return, Return -> 0
+    | Overflow, _ -> 1
+    | _, Overflow -> -1
+    | Assertion, _ -> 1
+    | _, Assertion -> -1
+    | Assumption, _ -> 1
+    | _, Assumption -> -1
+    | Match, _ -> 1
+    | _, Match -> -1
+end
+
+let string_of_event = function
+  | Overflow -> "overflow"
+  | Assertion -> "assertion"
+  | Assumption -> "assumption"
+  | Match -> "match_failure"
+  | Return -> "return"
+
+let rec string_of_query = function
+  | Q_all ev -> "A " ^ string_of_event ev
+  | Q_exist ev -> "E " ^ string_of_event ev
+  | Q_not q -> "~(" ^ string_of_query q ^ ")"
+  | Q_and qs -> "(" ^ Util.string_of_list " & " string_of_query qs ^ ")"
+  | Q_or qs -> "(" ^ Util.string_of_list " | " string_of_query qs ^ ")"
+
+let parse_query =
+  let amp = token (function Str.Delim "&" -> Some () | _ -> None) in
+  let bar = token (function Str.Delim "|" -> Some () | _ -> None) in
+  let lparen = token (function Str.Delim "(" -> Some () | _ -> None) in
+  let rparen = token (function Str.Delim ")" -> Some () | _ -> None) in
+  let quant = token (function Str.Text ("A" | "all") -> Some (fun x -> Q_all x)
+                            | Str.Text ("E" | "exist") -> Some (fun x -> Q_exist x)
+                            | _ -> None) in
+  let event = token (function Str.Text "overflow" -> Some Overflow
+                            | Str.Text "assertion" -> Some Assertion
+                            | Str.Text "assumption" -> Some Assumption
+                            | Str.Text "match_failure" -> Some Match
+                            | Str.Text "return"-> Some Return
+                            | _ -> None) in
+  let tilde = token (function Str.Delim "~" -> Some () | _ -> None) in
+
+  let rec exp0 () =
+    pchoose (exp1 () >>= fun x -> bar >>= fun _ -> exp0 () >>= fun y -> preturn (Q_or [x; y]))
+            (exp1 ())
+  and exp1 () =
+    pchoose (exp2 () >>= fun x -> amp >>= fun _ -> exp1 () >>= fun y -> preturn (Q_and [x; y]))
+            (exp2 ())
+  and exp2 () =
+    pchoose (tilde >>= fun _ -> exp3 () >>= fun x -> preturn (Q_not x))
+            (exp3 ())
+  and exp3 () =
+    pchoose (lparen >>= fun _ -> exp0 () >>= fun x -> rparen >>= fun _ -> preturn x)
+            (quant >>= fun f -> event >>= fun ev -> preturn (f ev))
+  in
+  parse (exp0 ()) "[ \n\t]+\\|(\\|)\\|&\\||\\|~"
+
+type pragma = {
+    query : query
+  }
+
+let default_pragma = {
+    query = default_query
+  }
+
+let parse_pragma l input =
+  let key = Str.regexp ":[a-z]+" in
+  let tokens = Str.full_split key input in
+  let rec process_toks pragma = function
+    | Str.Delim ":query" :: Str.Text query :: rest ->
+       begin match parse_query query with
+       | Some q -> process_toks { query = q } rest
+       | None ->
+          raise (Reporting.err_general l ("Could not parse query " ^ String.trim query))
+       end
+    | [] -> pragma
+    | _ ->
+       raise (Reporting.err_general l "Could not parse pragma")
+  in
+  process_toks default_pragma tokens
diff --git a/src/property.mli b/src/property.mli
index fa24377a..3789fa63 100644
--- a/src/property.mli
+++ b/src/property.mli
@@ -87,3 +87,24 @@ val find_properties : 'a defs -> (string * string * l * 'a val_spec) Bindings.t
    constraints of the function are ignored.
 *)
 val rewrite : tannot defs -> tannot defs
+
+type event = Overflow | Assertion | Assumption | Match | Return
+
+module Event : sig
+  type t = event
+  val compare : event -> event -> int
+end
+
+type query =
+   | Q_all of event
+   | Q_exist of event
+   | Q_not of query
+   | Q_and of query list
+   | Q_or of query list
+
+type pragma = {
+    query : query
+  }
+
+val parse_pragma : Parse_ast.l -> string -> pragma
+
diff --git a/src/smtlib.ml b/src/smtlib.ml
index fe7aee5e..d17cb4d9 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -322,12 +322,25 @@ let rec sexp toks =
   in
   parse toks
 
+let parse p delim_regexp input =
+  let delim = Str.regexp delim_regexp 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 p tokens with
+  | Ok (result, []) -> Some result
+  | Ok (result, _) -> None
+  | Fail -> None
+
 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
+    | Str.Delim d when String.trim d = "" -> false
+    | _ -> true
   in
   let tokens = List.filter non_whitespace tokens in
   match plist sexp tokens with
@@ -347,7 +360,7 @@ let value_of_sexpr sexpr =
      | _ -> failwith "Cannot parse sexpr as ctyp"
      end
   | _ -> assert false
-          
+
 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) ->
@@ -365,7 +378,7 @@ let rec run frame =
      run (Interpreter.eval_frame frame)
   | Interpreter.Break frame ->
      run (Interpreter.eval_frame frame)
-  
+
 let check_counterexample ast env fname args arg_ctyps arg_smt_names =
   let open Printf in
   prerr_endline ("Checking counterexample: " ^ fname);