Add remaining parsing for Bitvectors and Floating-point arithmetic

CHANGES.md

@@ -2,6 +2,8 @@
 
 ### Added
 
+- Use `Dolmen` to parse smt2 benchmarks
+- Add `Binder` expression to model: `Forall`, `Exists`, and `Let_in`
 - Provide hashconsed sets of expressions in `Expr.Set`
 
 ### Fixed

bench/benchpress.sexp

@@ -0,0 +1,43 @@
+(prover
+  (name smtml-z3)
+  (cmd "smtml run --mode incremental --solver z3 $file")
+  (sat "^sat")
+  (unsat "unsat")
+  (unknown "unknown"))
+
+(prover
+  (name smtml-bitwuzla)
+  (cmd "smtml run --mode incremental --solver bitwuzla $file")
+  (sat "^sat")
+  (unsat "unsat")
+  (unknown "unknown"))
+
+(prover
+  (name smtml-colibri2)
+  (cmd "smtml run --mode incremental --solver colibri2 $file")
+  (sat "^sat")
+  (unsat "unsat")
+  (unknown "unknown"))
+
+(dir
+  (path $cur_dir)
+  (pattern ".*.smt2")
+  (expect (run smtlib-read-status)))
+
+(task
+  (name local-test)
+  (synopsis "Run smtml on directories provided on the command line")
+  (action
+    (run_provers
+      (provers (smtml z3))
+      (timeout 30)
+      (dirs ()))))
+
+(task
+  (name collections-c)
+  (synopsis "Run smtml on collections-c benchmarks")
+  (action
+    (run_provers
+      (provers (z3 smtml-z3 smtml-bitwuzla smtml-colibri2))
+      (timeout 30)
+      (dirs ($cur_dir/data/collections-c)))))

bench/runner/benchpress.ml

@@ -0,0 +1,60 @@
+open Bos
+
+let ( let* ) v f = Result.bind v f
+
+let cfg = Fpath.v "./benchpress.sexp"
+
+let task task = Cmd.(v "benchpress" % "run" % "-c" % p cfg % "--task" % task)
+
+let list_files = Cmd.(v "benchpress" % "list-files")
+
+let show nc file =
+  Cmd.(v "benchpress" % "show" % "--detail" % file %% on nc (v "--no-color"))
+
+let string_of_run_out run_out =
+  let* output, (_, status) = OS.Cmd.out_string run_out in
+  match (status, output) with
+  | `Exited 0, output -> Ok output
+  | _ -> Error (`Msg "Cmd exited with non-zero code")
+
+let stdout_lines cmd =
+  let run_out = OS.Cmd.run_out cmd in
+  let* lines, (_, status) = OS.Cmd.out_lines run_out in
+  match (status, lines) with
+  | `Exited 0, lines -> Ok lines
+  | _ -> Error (`Msg "Cmd exited with non-zero code")
+
+let remove_ansi_escape_codes s =
+  let re = Str.regexp "\x1b\\[[0-9;]*m" in
+  Str.global_replace re "" s
+
+let notify_done url results =
+  let url = Webhook.url_of_string url in
+  let head = Git.get_head () in
+  let title = Fmt.str "Test results (commit hash=%s) :octopus:" head in
+  let body = Fmt.str "```%s```" (remove_ansi_escape_codes results) in
+  let body = Webhook.default_slack_mrkdwn title body in
+  Lwt_main.run @@ Webhook.post_and_forget url body
+
+let latest_results' nc =
+  let* lines = stdout_lines list_files in
+  match lines with
+  | [] -> Error (`Msg "Benchpress wasn't run yet")
+  | hd :: _ -> (
+    match String.split_on_char ' ' hd with
+    | [ file; _ ] -> Ok (OS.Cmd.run_out @@ show nc file)
+    | _ -> assert false )
+
+let latest_results nc =
+  let* run_out = latest_results' nc in
+  let _ = OS.Cmd.out_stdout run_out in
+  Ok ()
+
+let run hook t =
+  let* () = OS.Cmd.run @@ task t in
+  match hook with
+  | None -> Ok ()
+  | Some web_hook ->
+    let* run_out = latest_results' true in
+    let* output = string_of_run_out run_out in
+    Ok (notify_done web_hook output)

bench/runner/dune

@@ -0,0 +1,3 @@
+(executable
+ (name runner)
+ (libraries bos cohttp cohttp-lwt-unix cmdliner lwt yojson str))

bench/runner/git.ml

@@ -0,0 +1,14 @@
+(** Best effort to try and get commit hash of HEAD *)
+let get_head ?(length = 6) () =
+  let open Bos in
+  let short = Format.asprintf "--short=%d" length in
+  let cmd = Cmd.(v "git" % "rev-parse" % short % "HEAD") in
+  let output = OS.Cmd.run_out ~err:OS.Cmd.err_run_out cmd in
+  match OS.Cmd.out_string ~trim:true output with
+  | Ok (stdout, (_, `Exited 0)) -> stdout
+  | Error (`Msg err) ->
+    Format.eprintf "ERROR: %s@." err;
+    "unknown"
+  | Ok (stdout, (_, (`Exited _ | `Signaled _))) ->
+    Format.eprintf "%s@\nWARN: Unable to fetch git HEAD@." stdout;
+    "unknown"

bench/runner/runner.ml

@@ -0,0 +1,21 @@
+let cli =
+  let open Cmdliner in
+  let run =
+    let task = Arg.(required & opt (some string) None & info [ "task" ]) in
+    let hook = Arg.(value & opt (some string) None & info [ "web-hook" ]) in
+    let info = Cmd.info "run" in
+    Cmd.v info Term.(const Benchpress.run $ hook $ task)
+  in
+  let latest_results =
+    let nc = Arg.(value & flag & info [ "nc" ]) in
+    let info = Cmd.info "latest-results" in
+    Cmd.v info Term.(const Benchpress.latest_results $ nc)
+  in
+  let info = Cmd.info "runner" in
+  Cmd.group info [ run; latest_results ]
+
+let () =
+  match Cmdliner.Cmd.eval_value' cli with
+  | `Exit code -> exit code
+  | `Ok (Error (`Msg err)) -> failwith err
+  | `Ok (Ok ()) -> exit 0

bench/runner/webhook.ml

@@ -0,0 +1,41 @@
+open Cohttp
+open Cohttp_lwt_unix
+
+let headers =
+  let headers = Header.init () in
+  Header.add_list headers
+    [ ("Content-type", "application/json"); ("User-Agent", "Ecmabot/1.0") ]
+
+let default_slack_mrkdwn title body =
+  `Assoc
+    [ ( "blocks"
+      , `List
+          [ `Assoc
+              [ ("type", `String "header")
+              ; ( "text"
+                , `Assoc
+                    [ ("type", `String "plain_text")
+                    ; ("text", `String title)
+                    ; ("emoji", `Bool true)
+                    ] )
+              ]
+          ; `Assoc
+              [ ("type", `String "section")
+              ; ( "text"
+                , `Assoc [ ("type", `String "mrkdwn"); ("text", `String body) ]
+                )
+              ]
+          ] )
+    ]
+
+let url_of_string str = Uri.of_string str
+
+let post url body =
+  let body = Cohttp_lwt.Body.of_string (Yojson.to_string body) in
+  Client.post ~body ~headers url
+
+(** Sends POST and forgets about it *)
+let post_and_forget url body =
+  let open Lwt.Syntax in
+  let+ _ = post url body in
+  ()

bin/main.ml

@@ -19,46 +19,40 @@
 open Smtml
 open Solver_dispatcher
 
-let run debug solver prover_mode _print_statistics file =
+let get_solver debug solver prover_mode =
   let module Mappings =
     (val mappings_of_solver solver : Mappings_intf.S_with_fresh)
   in
   Mappings.set_debug debug;
-  let module Solver =
-    ( val match prover_mode with
-          | Options.Batch -> (module Solver.Batch (Mappings))
-          | Cached -> (module Solver.Cached (Mappings))
-          | Incremental -> (module Solver.Incremental (Mappings))
-        : Solver_intf.S )
-  in
+  match prover_mode with
+  | Options.Batch -> (module Solver.Batch (Mappings) : Solver_intf.S)
+  | Cached -> (module Solver.Cached (Mappings))
+  | Incremental -> (module Solver.Incremental (Mappings))
+
+let run debug solver prover_mode _print_statistics file =
+  let module Solver = (val get_solver debug solver prover_mode) in
   let module Interpret = Interpret.Make (Solver) in
   let ast = Compile.until_rewrite file in
-  let _ = Interpret.start ast in
+  let _ : Interpret.exec_state = Interpret.start ast in
   ()
 
 let test debug solver prover_mode print_statistics files =
-  let module Mappings =
-    (val mappings_of_solver solver : Mappings_intf.S_with_fresh)
-  in
-  Mappings.set_debug debug;
-  let module Solver =
-    ( val match prover_mode with
-          | Options.Batch -> (module Solver.Batch (Mappings))
-          | Cached -> (module Solver.Cached (Mappings))
-          | Incremental -> (module Solver.Incremental (Mappings))
-        : Solver_intf.S )
-  in
+  let module Solver = (val get_solver debug solver prover_mode) in
   let module Interpret = Interpret.Make (Solver) in
+  (* TODO: Add proper logs *)
+  let debug fmt k = if debug then k (Fmt.epr fmt) in
   let rec test_path state path =
     if Sys.is_directory (Fpath.to_string path) then test_dir state path
-    else
+    else begin
+      debug "File %a...@." (fun k -> k Fpath.pp path);
       let ast = Compile.until_rewrite path in
       Some (Interpret.start ?state ast)
+    end
   and test_dir state d =
     let result =
       Bos.OS.Dir.fold_contents
         (fun path state ->
-          if Fpath.has_ext ".smtml" path then test_path state path else state )
+          if Fpath.has_ext ".smt2" path then test_path state path else state )
         state d
     in
     match result with Error (`Msg e) -> failwith e | Ok state -> state
@@ -88,7 +82,10 @@ let to_smt2 debug solver filename =
   let assertions =
     List.filter_map (function Ast.Assert e -> Some e | _ -> None) ast
   in
-  Format.printf "%a@." (Mappings.pp_smt ?status:None) assertions
+  let name = Fpath.to_string @@ Fpath.base filename in
+  Format.printf "%a"
+    (Mappings.Smtlib.pp ~name ?logic:None ?status:None)
+    assertions
 
 let cli =
   Cmdliner.Cmd.group

dune-project

@@ -66,4 +66,16 @@
   (bisect_ppx
    (and
     :with-test
-    (>= "2.5.0")))))
+    (>= "2.5.0")))
+  (benchpress
+   (and
+    :with-test
+    (= "dev")))
+  (cohttp
+   :with-test)
+  (cohttp-lwt-unix
+   :with-test)
+  (lwt
+   :with-test)
+  (tls-lwt
+   :with-test)))

smtml.opam

@@ -24,6 +24,11 @@ depends: [
   "yojson" {>= "1.6.0"}
   "odoc" {with-doc}
   "bisect_ppx" {with-test & >= "2.5.0"}
+  "benchpress" {with-test & = "dev"}
+  "cohttp" {with-test}
+  "cohttp-lwt-unix" {with-test}
+  "lwt" {with-test}
+  "tls-lwt" {with-test}
 ]
 depopts: ["z3" "colibri2" "bitwuzla-cxx" "cvc5"]
 conflicts: [
@@ -49,4 +54,5 @@ available: arch != "arm32" & arch != "x86_32"
 pin-depends: [
   ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#6e302cc50d82b8fb04f1b37debf3bc4dafbd3e1b"]
   ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#6e302cc50d82b8fb04f1b37debf3bc4dafbd3e1b"]
+  ["benchpress.dev" "git+https://github.com/filipeom/benchpress.git#50355de32835b12f1b065a4700f493bc3d8c5342"]
 ]

smtml.opam.template

@@ -2,4 +2,5 @@ available: arch != "arm32" & arch != "x86_32"
 pin-depends: [
   ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#6e302cc50d82b8fb04f1b37debf3bc4dafbd3e1b"]
   ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#6e302cc50d82b8fb04f1b37debf3bc4dafbd3e1b"]
+  ["benchpress.dev" "git+https://github.com/filipeom/benchpress.git#50355de32835b12f1b065a4700f493bc3d8c5342"]
 ]

src/ast/ast.ml

@@ -49,15 +49,23 @@ let pp fmt (instr : t) =
     Fmt.pf fmt "(check-sat-assuming@ (%a))"
       (Fmt.list ~sep:Fmt.sp Expr.pp)
       assumptuions
-  | Push n -> Fmt.pf fmt "(push %d)" n
-  | Pop n -> Fmt.pf fmt "(pop %d)" n
   | Declare_const { id; sort } ->
     Fmt.pf fmt "(declare-const %a %a)" Symbol.pp id Symbol.pp sort
+  | Echo line -> Fmt.pf fmt "(echo %S)" line
+  | Exit -> Fmt.string fmt "(exit)"
+  | Get_assertions -> Fmt.string fmt "(get-assertions)"
+  | Get_assignment -> Fmt.string fmt "(get-assignment)"
+  | Get_info info -> Fmt.pf fmt "(get-info %a)" Fmt.string info
+  | Get_option opt -> Fmt.pf fmt "(get-option %a)" Fmt.string opt
   | Get_model -> Fmt.string fmt "(get-model)"
+  | Get_value htes ->
+    Fmt.pf fmt "(get-value %a)" (Fmt.parens (Fmt.list ~sep:Fmt.sp Expr.pp)) htes
+  | Pop n -> Fmt.pf fmt "(pop %d)" n
+  | Push n -> Fmt.pf fmt "(push %d)" n
+  | Reset -> Fmt.string fmt "(reset)"
+  | Reset_assertions -> Fmt.string fmt "(reset-assertions)"
+  | Set_info info -> Fmt.pf fmt "(set-info %a)" Expr.pp info
   | Set_logic logic -> Fmt.pf fmt "(set-logic %a)" Ty.pp_logic logic
-  | Exit -> Fmt.string fmt "(exit)"
-  | Get_assertions | Get_assignment | Reset | Reset_assertions | Echo _
-  | Get_info _ | Get_option _ | Get_value _ | Set_info _ | Set_option _ ->
-    Fmt.failwith "pp: TODO printing of unused cases"
+  | Set_option opt -> Fmt.pf fmt "(set-option %a)" Expr.pp opt
 
 let to_string (instr : t) : string = Fmt.str "%a" pp instr