[sledge] Add: SMT-LIB frontend to SLEdge's internal first-order theory solver

Summary:
The SLEdge internal first-order theory solver targets the "word
problem", where a query has the form `C ⊢ L` where `C` is a
conjunction of literals and `L` is a single literal. This can be
abused to implement a naive SMT solver using an expansion to
disjunctive-normal form and checking `C ⊢ false` for each branch `C`
of the DNF. This is not useful as an SMT solver, but can be used for
testing.

Reviewed By: ngorogiannis

Differential Revision: D23459524

fbshipit-source-id: 5483e5a84

sledge/bin/sledge_cli.ml

@@ -45,19 +45,26 @@ let command ~summary ?readme param =
       Trace.flush () ;
       Format.printf "@\nRESULT: Success: Invalid Accesses: %i@."
         (Report.invalid_access_count ())
-    with exn ->
+    with
-      let bt = Printexc.get_raw_backtrace () in
+    | Smtlib.Unsound ->
-      Trace.flush () ;
+        Trace.flush () ;
-      ( match exn with
+        Format.printf "@\nRESULT: Unsound@."
-      | Frontend.Invalid_llvm msg ->
+    | Smtlib.Incomplete ->
-          Format.printf "@\nRESULT: Invalid input: %s@." msg
+        Trace.flush () ;
-      | Unimplemented msg ->
+        Format.printf "@\nRESULT: Incomplete@."
-          Format.printf "@\nRESULT: Unimplemented: %s@." msg
+    | exn ->
-      | Failure msg -> Format.printf "@\nRESULT: Internal error: %s@." msg
+        let bt = Printexc.get_raw_backtrace () in
-      | _ ->
+        Trace.flush () ;
-          Format.printf "@\nRESULT: Unknown error: %s@."
+        ( match exn with
-            (Printexc.to_string exn) ) ;
+        | Frontend.Invalid_llvm msg ->
-      Printexc.raise_with_backtrace exn bt
+            Format.printf "@\nRESULT: Invalid input: %s@." msg
+        | Unimplemented msg ->
+            Format.printf "@\nRESULT: Unimplemented: %s@." msg
+        | Failure msg -> Format.printf "@\nRESULT: Internal error: %s@." msg
+        | _ ->
+            Format.printf "@\nRESULT: Unknown error: %s@."
+              (Printexc.to_string exn) ) ;
+        Printexc.raise_with_backtrace exn bt
   in
   Command.basic ~summary ?readme (trace *> param >>| wrap)
 
@@ -230,6 +237,17 @@ let disassemble_cmd =
   in
   command ~summary ~readme param
 
+let smt_cmd =
+  let summary = "process SMT-LIB benchmarks" in
+  let readme () =
+    "The <input> file is interpreted as an SMT-LIB 2 benchmark."
+  in
+  let param =
+    let%map_open input = anon ("<input>" %: string) in
+    fun () -> Smtlib.process input
+  in
+  command ~summary ~readme param
+
 let summary = "SLEdge static analyzer"
 
 let readme () =
@@ -245,4 +263,5 @@ Command.run ~version:Version.version ~build_info:Version.build_info
      [ ("buck", Sledge_buck.main ~command ~analyze:(translate >*> analyze))
      ; ("llvm", llvm_grp)
      ; ("analyze", analyze_cmd)
-     ; ("disassemble", disassemble_cmd) ])
+     ; ("disassemble", disassemble_cmd)
+     ; ("smt", smt_cmd) ])

sledge/bin/smtlib.ml

@@ -0,0 +1,186 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Process SMT-LIB benchmarks using SLEdge's first-order theory solver. *)
+
+module Smt = Smtlib_utils.V_2_6
+open Fol
+module VarEnv = Map.Make (String)
+
+type var_env = Term.t VarEnv.t
+type frame = {mutable asserts: Smt.Ast.term list; mutable var_env: var_env}
+
+let init_stack = [{asserts= []; var_env= VarEnv.empty}]
+let stack = ref init_stack
+let top () = List.hd_exn !stack
+
+let push () =
+  let {asserts; var_env} = top () in
+  stack := {asserts; var_env} :: !stack
+
+let pop () =
+  match !stack with
+  | [] -> assert false
+  | [_] -> ()
+  | _ :: tl -> stack := tl
+
+let reset () = stack := init_stack
+
+let id =
+  let count = ref (-1) in
+  fun () ->
+    incr count ;
+    !count
+
+let decl_var name =
+  let v = Term.var (Var.identified ~name ~id:(id ())) in
+  let top = top () in
+  top.var_env <- VarEnv.add_exn ~key:name ~data:v top.var_env
+
+let assert_term term =
+  let top = top () in
+  top.asserts <- term :: top.asserts
+
+let rec x_let init nes =
+  List.fold nes ~init ~f:(fun n (name, term) ->
+      VarEnv.add_exn ~key:name ~data:(x_trm init term) n )
+
+and x_trm : var_env -> Smt.Ast.term -> Term.t =
+ fun n term ->
+  match term with
+  | Const s -> (
+    try VarEnv.find_exn n s
+    with _ -> (
+      try Term.rational (Q.of_string s)
+      with _ -> (
+        try Term.rational (Q.of_float (Float.of_string s))
+        with _ -> fail "not a rational: %a" Smt.Ast.pp_term term () ) ) )
+  | Arith (Add, e :: es) ->
+      List.fold ~f:(fun s e -> Term.add s (x_trm n e)) ~init:(x_trm n e) es
+  | Arith (Minus, e :: es) ->
+      List.fold ~f:(fun s e -> Term.sub s (x_trm n e)) ~init:(x_trm n e) es
+  | Arith (Mult, es) -> (
+    match List.map ~f:(x_trm n) es with
+    | e :: es ->
+        List.fold es ~init:e ~f:(fun p e ->
+            match Term.const_of e with
+            | Some q -> Term.mulq q p
+            | None -> (
+              match Term.const_of p with
+              | Some q -> Term.mulq q e
+              | None -> fail "nonlinear: %a" Smt.Ast.pp_term term () ) )
+    | [] -> fail "malformed: %a" Smt.Ast.pp_term term () )
+  | Arith (Div, es) -> (
+    match List.map ~f:(x_trm n) es with
+    | e :: es ->
+        List.fold es ~init:e ~f:(fun p e ->
+            match Term.const_of e with
+            | Some q -> Term.mulq (Q.inv q) p
+            | None -> fail "nonlinear: %a" Smt.Ast.pp_term term () )
+    | [] -> fail "malformed: %a" Smt.Ast.pp_term term () )
+  | If (c, t, e) ->
+      Term.ite ~cnd:(x_fml n c) ~thn:(x_trm n t) ~els:(x_trm n e)
+  | App _ -> todo "%a" Smt.Ast.pp_term term ()
+  | Let (nes, e) -> x_trm (x_let n nes) e
+  | Attr (e, _) -> x_trm n e
+  | Fun _ | HO_app _ -> fail "higher-order: %a" Smt.Ast.pp_term term ()
+  | Match _ -> fail "datatype: %a" Smt.Ast.pp_term term ()
+  | Cast _ -> fail "cast: %a" Smt.Ast.pp_term term ()
+  | Arith ((Add | Minus), _) -> fail "malformed: %a" Smt.Ast.pp_term term ()
+  | True | False
+   |Arith ((Leq | Lt | Geq | Gt), _)
+   |Is_a _ | Eq _ | Imply _ | And _ | Or _ | Not _ | Distinct _ | Forall _
+   |Exists _ ->
+      Formula.inject (x_fml n term)
+
+and x_fml : var_env -> Smt.Ast.term -> Formula.t =
+ fun n term ->
+  match term with
+  | True -> Formula.tt
+  | False -> Formula.ff
+  | If (cnd, pos, neg) ->
+      Formula.cond ~cnd:(x_fml n cnd) ~pos:(x_fml n pos) ~neg:(x_fml n neg)
+  | App _ -> todo "%a" Smt.Ast.pp_term term ()
+  | Let (nes, b) -> x_fml (x_let n nes) b
+  | Eq (d, e) -> Formula.eq (x_trm n d) (x_trm n e)
+  | Imply (a, b) -> x_fml n (Or [Not a; b])
+  | And bs -> Formula.andN (List.map ~f:(x_fml n) bs)
+  | Or bs -> Formula.orN (List.map ~f:(x_fml n) bs)
+  | Distinct es ->
+      es
+      |> List.map ~f:(x_trm n)
+      |> Iter.diagonal_l
+      |> Iter.map ~f:(fun (d, e) -> Formula.dq d e)
+      |> Iter.to_list
+      |> Formula.andN
+  | Not b -> Formula.not_ (x_fml n b)
+  | Attr (b, _) -> x_fml n b
+  | Cast _ -> fail "cast: %a" Smt.Ast.pp_term term ()
+  | Arith ((Leq | Lt | Geq | Gt), _) ->
+      fail "inequality: %a" Smt.Ast.pp_term term ()
+  | Fun _ | HO_app _ -> fail "higher-order: %a" Smt.Ast.pp_term term ()
+  | Match _ | Is_a _ -> fail "datatype: %a" Smt.Ast.pp_term term ()
+  | Forall _ | Exists _ -> fail "quantifier: %a" Smt.Ast.pp_term term ()
+  | Const _ | Arith ((Add | Minus | Mult | Div), _) ->
+      Formula.dq0 (x_trm n term)
+
+let x_context {asserts; var_env} =
+  Context.dnf (Formula.andN (List.map ~f:(x_fml var_env) asserts))
+
+let check_unsat (_, asserts, ctx) =
+  [%Trace.call fun {pf} ->
+    pf "%a@ %a@ %a" Formula.pp asserts Context.pp ctx Context.pp_raw ctx]
+  ;
+  ( Context.is_unsat ctx
+  || Formula.equal Formula.ff
+       (Formula.map_terms ~f:(Context.normalize ctx) asserts) )
+  |>
+  [%Trace.retn fun {pf} -> pf "%b"]
+
+exception Unsound
+exception Incomplete
+
+let expect_unsat = ref false
+
+let check_sat () =
+  let unsat = Iter.for_all ~f:check_unsat (x_context (top ())) in
+  if (not unsat) && !expect_unsat then raise Incomplete
+  else if unsat && not !expect_unsat then raise Unsound
+
+let process_stmt (stmt : Smt.Ast.statement) =
+  match stmt.stmt with
+  | Stmt_set_logic _ -> ()
+  | Stmt_set_info (":status", "unsat") -> expect_unsat := true
+  | Stmt_set_info (":status", _) -> expect_unsat := false
+  | Stmt_set_info _ | Stmt_set_option _ | Stmt_decl_sort _ -> ()
+  | Stmt_decl {fun_name; fun_args= []} -> decl_var fun_name
+  | Stmt_decl _ -> todo "%a" Smt.Ast.pp_stmt stmt ()
+  | Stmt_fun_def {fr_decl= {fun_name; fun_args= []}; fr_body} ->
+      assert_term (Eq (Const fun_name, fr_body))
+  | Stmt_fun_def _ | Stmt_fun_rec _ | Stmt_funs_rec _ ->
+      fail "function definition: %a" Smt.Ast.pp_stmt stmt ()
+  | Stmt_data _ -> fail "datatype definition" ()
+  | Stmt_assert term -> assert_term term
+  | Stmt_get_assertions | Stmt_get_assignment | Stmt_get_info _
+   |Stmt_get_model | Stmt_get_option _ | Stmt_get_proof
+   |Stmt_get_unsat_assumptions | Stmt_get_unsat_core | Stmt_get_value _ ->
+      ()
+  | Stmt_check_sat -> check_sat ()
+  | Stmt_check_sat_assuming _ -> fail "check-sat-assuming" ()
+  | Stmt_pop n ->
+      for _ = 1 to n do
+        pop ()
+      done
+  | Stmt_push n ->
+      for _ = 1 to n do
+        push ()
+      done
+  | Stmt_reset | Stmt_reset_assertions -> reset ()
+  | Stmt_exit -> ()
+
+let process filename =
+  List.iter ~f:process_stmt (Smt.parse_file_exn filename)

sledge/bin/smtlib.mli

@@ -0,0 +1,13 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Process SMT-LIB benchmarks using SLEdge's first-order theory solver. *)
+
+exception Unsound
+exception Incomplete
+
+val process : string -> unit

sledge/dune

@@ -109,7 +109,8 @@
   (package sledge)
   (libraries apron apron.boxMPQ ctypes ctypes.foreign dune-build-info llvm
     llvm.irreader llvm.analysis llvm.scalar_opts llvm.target llvm.ipo
-    llvm.linker shexp.process yojson trace nonstdlib sledge model)
+    llvm.linker shexp.process yojson trace nonstdlib sledge model
+    smtlib-utils)
   (flags
    (:standard -w -58 -open NS -open Sledge -open Model))
   (preprocess

sledge/sledge-help.txt

@@ -15,6 +15,7 @@ The [-trace <spec>] argument of each subcommand enables debug tracing according
   . translate  translate LLVM bitcode to LLAIR
   analyze      analyze LLAIR code
   disassemble  print LLAIR code in textual form
+  smt          process SMT-LIB benchmarks
   version      print version information
   help         explain a given subcommand (perhaps recursively)
 
@@ -224,6 +225,23 @@ The <input> file must be LLAIR code, as produced by `sledge llvm translate`.
                               (alias: -?)
 
 
+====== sledge smt ======
+
+process SMT-LIB benchmarks
+
+  sledge smt <input>
+
+The <input> file is interpreted as an SMT-LIB 2 benchmark.
+
+=== flags ===
+
+  [-colors]         enable printing in colors
+  [-margin <cols>]  wrap debug tracing at <cols> columns
+  [-trace <spec>]   enable debug tracing
+  [-help]           print this help text and exit
+                    (alias: -?)
+
+
 ====== sledge version ======
 
 print version information

sledge/sledge.opam

@@ -23,6 +23,7 @@ depends: [
   "ppx_compare"
   "ppx_hash"
   "shexp"
+  "smtlib-utils"
   "yojson"
   "zarith"
 ]