Bring back concolic options

.gitignore

@@ -27,5 +27,5 @@ result
 .DS_Store
 nix/profiles/
 
-**/wasp-out/
+wasp-out/*
 bin/libc.wasm

bin/dune

@@ -3,4 +3,4 @@
  (name main)
  (public_name wasp)
  (modules main options)
- (libraries cmdliner interpreter wasp))
+ (libraries prelude interpreter wasp))

bin/main.ml

@@ -1,8 +1,30 @@
-let main filename = Format.printf "%a@." Fpath.pp filename
+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 open Cmdliner in
-  let info = Cmd.info "wasp" ~version:"%%VERSION%%" in
-  Cmd.v info Term.(const main $ Options.file0)
+  let info = Cmdliner.Cmd.info "wasp" ~version:"%%VERSION%%" in
+  Cmdliner.Cmd.group info [ Options.cmd_concolic run_concolic ]
 
-let () = exit (Cmdliner.Cmd.eval cli)
+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

@@ -3,5 +3,51 @@ open Cmdliner
 let path = ((fun s -> `Ok (Fpath.v s)), Fpath.pp)
 
 let file0 =
-  let doc = "input file to analyse" in
+  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 )

src/concolic/eval.ml

@@ -233,7 +233,15 @@ let mk_relop ?(reduce : bool = true) (e : Expr.t) (ty : Ty.t) =
     | Ty_fp 64 -> Expr.relop (Ty_fp 64) Ne e (Expr.value zero)
     | _ -> assert false )
 
-let add_constraint ?neg:_ _ _ = assert false
+let add_constraint ?(neg : bool = false) e pc =
+  let cond =
+    let c = to_relop (Expr.simplify e) in
+    if neg then Option.map (fun e -> Expr.Bool.not e) c else c
+  in
+  match (cond, Expr.view pc) with
+  | None, _ -> pc
+  | Some cond, Val True -> cond
+  | Some cond, _ -> Expr.binop Ty_bool And cond pc
 
 let branch_on_cond bval c pc tree =
   let tree', to_branch =

src/concolic/store.ml

@@ -186,10 +186,11 @@ let rec eval (env : t) (e : Expr.t) : Value.t =
       in
       Hashtbl.replace env.map x v;
       Num v )
-  | Extract (e, _, _) ->
-    let _v = int64_of_value (eval env e) in
-    (* Num (I64 (Expr.nland64 (Int64.shift_right v (l * 8)) (h - l))) *)
-    assert false
+  | Extract (e', h, l) when h - l = 1 ->
+    let v = int64_of_value (eval env e') in
+    Num (I64 Int64.(logand (shift_right v (8 * l)) 0xffL))
+  | Extract (_, _, _) ->
+      assert false
   | Concat (e1, e2) -> (
     let v1 = int64_of_value (eval env e1) in
     let v2 = int64_of_value (eval env e2) in

src/run.ml

@@ -524,7 +524,7 @@ and run_quote_script script invoke =
   bind scripts None (List.rev !quote);
   quote := !quote @ save_quote
 
-let invoke_concolic f vs inst =
+let invoke_concolic _policy f vs inst =
   Concolic.Eval.main f
     (List.map
        (fun v ->
@@ -545,8 +545,8 @@ let run_file _file =
   (* input_file file run_script *)
   assert false
 
-let run_string_concolic string =
-  input_string string ~callback:(fun s -> run_script s invoke_concolic)
+let run_string_concolic string policy =
+  input_string string ~callback:(fun s -> run_script s (invoke_concolic policy))
 
 (* let run_string_se string = *)
 (*   input_string string ~callback:(fun s -> run_script s invoke_se) *)

src/run.mli

@@ -8,7 +8,7 @@ exception IO of Source.region * string
 
 val trace : string -> unit
 
-val run_string_concolic : string -> bool
+val run_string_concolic : string -> Concolic.Eval.policy -> bool
 
 val run_file : string -> bool
 

src/std.ml

@@ -0,0 +1,6 @@
+module Let_syntax = struct
+  module Result = struct
+    let ( let* ) = Result.bind
+    let ( let+ ) v f = Result.map f v
+  end
+end

tests/failing/dune

@@ -0,0 +1,4 @@
+(cram
+ (deps
+  %{bin:wasp}
+  test1.wast))

tests/failing/test_failing.t

@@ -0,0 +1,2 @@
+Run tests with assertion failures in concolic:
+  $ wasp concolic test1.wast

tests/passing/dune

@@ -0,0 +1,4 @@
+(cram
+ (deps
+  %{bin:wasp}
+  test1.wast))

tests/passing/test_passing.t

@@ -0,0 +1,2 @@
+Run tests without issues in concolic:
+  $ wasp concolic test1.wast