Make wasp usable and benchmarkable again

.github/workflows/build.yml

@@ -0,0 +1,34 @@
+name: Build
+
+on:
+  push:
+    branches: main
+  pull_request:
+    branches: main
+
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+    runs-on: ubuntu-latest
+    env:
+      # allow opam depext to yes package manager prompts
+      OPAMCONFIRMLEVEL: unsafe-yes
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Setup OCaml 4.14
+        uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: 4.14
+          dune-cache: true
+
+      - name: Install dependencies
+        run: opam install -y . --deps-only --with-test
+
+      - name: Build
+        run: opam exec -- dune build @install
+
+      - name: Test
+        run: opam exec -- dune runtest

.gitignore

@@ -27,9 +27,5 @@ result
 .DS_Store
 nix/profiles/
 
-# dkml desktop CI
-/msys64
-/.ci
-
-**/wasp-out/
+wasp-out/*
 bin/libc.wasm

.ocamlformat

@@ -1,4 +1,4 @@
-version=0.25.1
+version=0.26.2
 assignment-operator=end-line
 break-cases=fit
 break-fun-decl=wrap
@@ -25,7 +25,7 @@ let-binding-spacing=compact
 let-module=compact
 margin=80
 max-indent=2
-module-item-spacing=compact
+module-item-spacing=sparse
 ocaml-version=4.14.0
 ocp-indent-compat=false
 parens-ite=false

bin/dune

@@ -0,0 +1,6 @@
+(executable
+ (package wasp)
+ (name main)
+ (public_name wasp)
+ (modules main options)
+ (libraries prelude interpreter wasp))

bin/main.ml

@@ -0,0 +1,30 @@
+open Prelude
+module Flags = Interpreter.Flags
+
+let run_concolic filename unchecked trace timeout workspace no_simplify policy
+  queries log =
+  let open Wasp.Std.Let_syntax.Result in
+  Flags.unchecked := unchecked;
+  Flags.trace := trace;
+  Flags.timeout := timeout;
+  Flags.output := workspace;
+  Flags.simplify := no_simplify;
+  (* Flags.policy := *)
+  Flags.queries := queries;
+  Flags.log := log;
+  let+ data = Bos.OS.File.read filename in
+  if not (Wasp.Run.run_string_concolic data policy) then 1 else 0
+
+let cli =
+  let info = Cmdliner.Cmd.info "wasp" ~version:"%%VERSION%%" in
+  Cmdliner.Cmd.group info [ Options.cmd_concolic run_concolic ]
+
+let () =
+  match Cmdliner.Cmd.eval_value' cli with
+  | `Ok result -> (
+    match result with
+    | Ok n -> exit n
+    | Error (`Msg msg) ->
+      Fmt.epr "unexpected error: %s@." msg;
+      exit 2 )
+  | `Exit n -> exit n

bin/options.ml

@@ -0,0 +1,53 @@
+open Cmdliner
+
+let path = ((fun s -> `Ok (Fpath.v s)), Fpath.pp)
+
+let file0 =
+  let doc = "$(docv) to analyse" in
+  Arg.(required & pos 0 (some path) None & info [] ~doc ~docv:"FILE")
+
+let unchecked =
+  let doc = "Unchecked, do not perform validation" in
+  Arg.(value & flag & info [ "u"; "unchecked" ] ~doc)
+
+let trace =
+  let doc = "Trace execution" in
+  Arg.(value & flag & info [ "t"; "trace" ] ~doc)
+
+let timeout =
+  let doc = "Time limit" in
+  Arg.(value & opt int ~-1 & info [ "timeout" ] ~doc)
+
+let workspace =
+  let doc = "Directory to output report and testsuite (default=wasp-out)" in
+  Arg.(value & opt string "wasp-out" & info [ "workspace" ] ~doc)
+
+let no_simplify =
+  let doc = "Don't perform algebraic simplifications of symbolic expressions" in
+  Arg.(value & flag & info [ "no-simplify" ] ~doc)
+
+let policy_conv =
+  Arg.enum
+    [ ("random", Concolic.Eval.Random)
+    ; ("depth", Concolic.Eval.Depth)
+    ; ("breadth", Concolic.Eval.Breadth)
+    ]
+
+let policy =
+  let doc = "Search policy random|depth|breadth (default=random)" in
+  Arg.(value & opt policy_conv Concolic.Eval.Random & info [ "policy" ] ~doc)
+
+let queries =
+  let doc = "Output solver queries in .smt2 format" in
+  Arg.(value & flag & info [ "queries" ] ~doc)
+
+let log =
+  let doc = "Logs paths and memory" in
+  Arg.(value & flag & info [ "log" ] ~doc)
+
+let cmd_concolic run =
+  let info = Cmd.info "concolic" in
+  Cmd.v info
+    Term.(
+      const run $ file0 $ unchecked $ trace $ timeout $ workspace $ no_simplify
+      $ policy $ queries $ log )

bin/wasp_se.ml

@@ -0,0 +1,83 @@
+open Interpreter
+
+let name = "WebAssembly Static Executor"
+
+let version = "v0.1"
+
+let configure () =
+  Import.register (Utf8.decode "spectest") Spectest.lookup;
+  Import.register (Utf8.decode "env") Env.lookup
+
+let banner () = print_endline (name ^ " " ^ version)
+
+let usage = "Usage: " ^ name ^ " [option] [file ...]"
+
+let args = ref []
+
+let add_arg source = args := !args @ [ source ]
+
+let quote s = "\"" ^ String.escaped s ^ "\""
+
+let argspec =
+  Arg.align
+    [ ( "-"
+      , Arg.Set Flags.interactive
+      , " run interactively (default if no files given)" )
+    ; ("-e", Arg.String add_arg, " evaluate string")
+    ; ( "-i"
+      , Arg.String (fun file -> add_arg ("(input " ^ quote file ^ ")"))
+      , " read script from file" )
+    ; ( "-o"
+      , Arg.String (fun file -> add_arg ("(output " ^ quote file ^ ")"))
+      , " write module to file" )
+    ; ("-s", Arg.Set Flags.print_sig, " show module signatures")
+    ; ("-u", Arg.Set Flags.unchecked, " unchecked, do not perform validation")
+    ; ("-h", Arg.Clear Flags.harness, " exclude harness for JS conversion")
+    ; ("-d", Arg.Set Flags.dry, " dry, do not run program")
+    ; ("-t", Arg.Set Flags.trace, " trace execution")
+    ; ( "-v"
+      , Arg.Unit
+          (fun () ->
+            banner ();
+            exit 0 )
+      , " show version" )
+    ; ("--timeout", Arg.Set_int Flags.timeout, " time limit (default=900s)")
+    ; ( "--workspace"
+      , Arg.Set_string Flags.output
+      , " directory to output report and test-suite (default=output)" )
+    ; ( "--policy"
+      , Arg.Set_string Flags.policy
+      , " search policy random|depth|breadth|breadth-l|half-breadth (default: \
+         random)" )
+    ; ( "--encoding"
+      , Arg.Set_string Flags.encoding
+      , " encoding policy incremental|batch (default: incremental)" )
+    ; ( "--memory"
+      , Arg.Set_string Flags.memory
+      , " memory backend map|lazy|tree (default: map)" )
+    ; ( "--queries"
+      , Arg.Set Flags.queries
+      , " output solver queries in .smt2 format" )
+    ; ( "--allocs"
+      , Arg.Int (fun i -> Flags.fixed_numbers := i :: !Flags.fixed_numbers)
+      , " add allocation size to be tested on symbolic allocations" )
+    ; ("--log", Arg.Set Flags.log, " logs paths and memory")
+    ]
+
+let () =
+  Printexc.record_backtrace true;
+  try
+    configure ();
+    Arg.parse argspec (fun file -> add_arg ("(input " ^ quote file ^ ")")) usage;
+    List.iter (fun arg -> if not (Wasp.Run.run_string_se arg) then exit 1) !args;
+    if !args = [] then Flags.interactive := true;
+    if !Flags.interactive then (
+      Flags.print_sig := true;
+      banner ();
+      Wasp.Run.run_stdin () )
+  with exn ->
+    flush_all ();
+    prerr_endline
+      (Sys.argv.(0) ^ ": uncaught exception " ^ Printexc.to_string exn);
+    Printexc.print_backtrace stderr;
+    exit 2

dune-project

@@ -17,10 +17,14 @@
  (name wasp)
  (synopsis "WebAssembly Symbolic Processor (WASP)")
  (description "WASP is a symbolic execution engine for testing and validating Wasm modules.")
- (depends base batteries ocamlformat))
-
-(package
- (name waspc)
- (synopsis "")
- (description "")
- (depends ocaml dune re2 bos pyml cmdliner))
+ (depends
+   batteries
+   bos
+   cmdliner
+   dune
+   ocaml
+   (ocamlformat :with-dev-setup)
+   pyml
+   re2
+   (smtml (>= "0.2.4"))
+   z3))