Allow wasp to run the same benchmarks as owi

bin/main.ml

@@ -1,5 +1,10 @@
 open Prelude
+module Import = Interpreter.Import
 module Flags = Interpreter.Flags
+module Utf8 = Interpreter.Utf8
+
+let configure () =
+  Import.register (Utf8.decode "symbolic") Concolic.Host.lookup
 
 let run_concolic filename unchecked trace timeout workspace no_simplify policy
   queries log =
@@ -13,6 +18,7 @@ let run_concolic filename unchecked trace timeout workspace no_simplify policy
   (* Flags.policy := *)
   Flags.queries := queries;
   Flags.log := log;
+  configure ();
   let testsuite = Fpath.(v workspace / "test_suite") in
   let* _ = Bos.OS.Dir.create ~path:true testsuite in
   let+ data = Bos.OS.File.read filename in

src/concolic/eval.ml

@@ -17,6 +17,7 @@ module Globals = Common.Globals
 module Instance = Interpreter.Instance
 module Source = Interpreter.Source
 module Trap = Common.Trap
+module Types = Interpreter.Types
 
 let memory_error at = function
   | Heap.InvalidAddress a ->
@@ -835,7 +836,12 @@ module ConcolicStepper (C : Checkpoint_intf.S with type config = config) :
           let code' = ([], [ Plain (Block (out, f.it.body)) @@ f.at ]) in
           let frame' = { inst = !inst'; locals = List.map ref locals'' } in
           (vs', [ Frame (List.length out, frame', code') @@ e.at ], mem, pc, bp)
-        | Interpreter.Func.HostFunc (_, _) -> failwith "HostFunc error" )
+        | HostFunc (FuncType ([], [ Types.I32Type ]), _) ->
+          let x = Store.next store "symbol" in
+          let ty = Ty.Ty_bitv 32 in
+          let v = Store.get store x ty false in
+          ((v, Expr.symbol (Symbol.make ty x)) :: vs', [], mem, pc, bp)
+        | HostFunc (_, _) -> failwith "Unknown host func" )
     in
     step_cnt := !step_cnt + 1;
     { c with code = (vs', es' @ List.tl es); mem = mem'; pc = pc'; bp = bp' }
@@ -951,7 +957,7 @@ module Guided_search (L : Common.WorkList) (S : Stepper) = struct
   let rec eval_loop (c : config) wls : config =
     match c.code with
     | _, [] -> c
-    | _, { it = Trapping msg; at } :: _ -> Trap.error at msg
+    | _, { it = Trapping _; _ } :: _ -> c
     | vs, { it = Interrupt Limit; _ } :: _ -> { c with code = (vs, []) }
     | _, { it = Interrupt _; _ } :: _ -> c
     | _, { it = Restart _; _ } :: _ ->
@@ -1006,6 +1012,14 @@ module Guided_search (L : Common.WorkList) (S : Stepper) = struct
         let tree', _ = Execution_tree.move_true !(c.tree) in
         c.tree := tree';
         concolic_loop (update c (vs, es) pc (Store.get_key_types store))
+      | _, { it = Trapping msg; at } :: _ -> (
+        Fmt.epr "%s: %s@." (Source.string_of_region at) msg;
+        match find_sat_path (pc_wl, cp_wl) with
+        | None -> None
+        | Some (_, None) -> concolic_loop (reset c glob0 code0 mem0)
+        | Some (pc', Some cp) ->
+          let _, c' = clone !cp in
+          concolic_loop (update c' c'.code c'.pc (Expr.get_symbols [ pc' ])) )
       | _ -> (
         Common.write_test_case testsuite (Store.to_json store);
         match find_sat_path (pc_wl, cp_wl) with
@@ -1254,7 +1268,7 @@ let add_import m ext im inst =
   | ExternMemory mem -> { inst with memories = mem :: inst.memories }
   | ExternGlobal glob -> { inst with globals = glob :: inst.globals }
 
-let init m exts =
+let init m exts testsuite policy =
   let open Ast in
   let open Interpreter in
   let open Source in
@@ -1295,6 +1309,6 @@ let init m exts =
   List.iter (fun f -> f ()) init_elems;
   List.iter (fun f -> f ()) init_datas;
   Option.iter
-    (fun x -> ignore (main "" Random (func inst x) [] inst memory))
+    (fun x -> ignore (main testsuite policy (func inst x) [] inst memory))
     start;
   (memory, inst)

src/concolic/host.ml

@@ -0,0 +1,11 @@
+open Prelude
+open Interpreter
+open Instance
+open Types
+
+let i32_symbol _env = assert false
+
+let lookup name t =
+  match (Interpreter.Utf8.encode name, t) with
+  | "i32_symbol", ExternFuncType t -> ExternFunc (Func.alloc_host t i32_symbol)
+  | _ -> Fmt.failwith "Not found"

src/run.ml

@@ -394,7 +394,7 @@ let assert_message at name msg re =
     print_endline ("Expect: \"" ^ re ^ "\"");
     Assert.error at ("wrong " ^ name ^ " error") )
 
-let run_assertion ass invoke =
+let run_assertion ass invoke testsuite policy =
   match ass.it with
   | AssertMalformed (def, re) -> (
     trace "Asserting malformed...";
@@ -417,7 +417,7 @@ let run_assertion ass invoke =
     if not !Flags.unchecked then Valid.check_module m;
     match
       let imports = Import.link m in
-      ignore (Concolic.Eval.init m imports)
+      ignore (Concolic.Eval.init m imports testsuite policy)
     with
     | exception (Import.Unknown (_, msg) | Common.Link (_, msg)) ->
       assert_message ass.at "linking" msg re
@@ -428,7 +428,7 @@ let run_assertion ass invoke =
     if not !Flags.unchecked then Valid.check_module m;
     match
       let imports = Import.link m in
-      ignore (Concolic.Eval.init m imports)
+      ignore (Concolic.Eval.init m imports testsuite policy)
     with
     | exception Common.Trap (_, msg) ->
       assert_message ass.at "instantiation" msg re
@@ -450,7 +450,7 @@ let run_assertion ass invoke =
       assert_message ass.at "exhaustion" msg re
     | _ -> Assert.error ass.at "expected exhaustion error" )
 
-let rec run_command cmd invoke =
+let rec run_command testsuite policy cmd invoke =
   match cmd.it with
   | Module (x_opt, def) ->
     quote := cmd :: !quote;
@@ -466,7 +466,7 @@ let rec run_command cmd invoke =
     if not !Flags.dry then (
       trace "Initializing...";
       let imports = Import.link m in
-      let memory, inst = Concolic.Eval.init m imports in
+      let memory, inst = Concolic.Eval.init m imports testsuite policy in
       bind memories x_opt memory;
       bind instances x_opt inst )
   | Register (name, x_opt) ->
@@ -483,17 +483,17 @@ let rec run_command cmd invoke =
       if vs <> [] then print_values vs
   | Assertion ass ->
     quote := cmd :: !quote;
-    if not !Flags.dry then run_assertion ass invoke
-  | Meta cmd -> run_meta cmd invoke
+    if not !Flags.dry then run_assertion ass invoke testsuite policy
+  | Meta cmd -> run_meta testsuite policy cmd invoke
 
-and run_meta cmd invoke =
+and run_meta testsuite policy cmd invoke =
   match cmd.it with
   | Script (x_opt, script) ->
-    run_quote_script script invoke;
+    run_quote_script testsuite policy script invoke;
     bind scripts x_opt (lookup_script None cmd.at)
   | Input (x_opt, file) ->
     ( try
-        if not (input_file file (fun s -> run_quote_script s invoke)) then
+        if not (input_file file (fun s -> run_quote_script testsuite policy s invoke)) then
           Abort.error cmd.at "aborting"
       with Sys_error msg -> IO.error cmd.at msg );
     bind scripts x_opt (lookup_script None cmd.at);
@@ -511,13 +511,13 @@ and run_meta cmd invoke =
     try output_stdout (fun () -> lookup_module x_opt cmd.at)
     with Sys_error msg -> IO.error cmd.at msg )
 
-and run_script script invoke =
-  List.iter (fun cmd -> run_command cmd invoke) script
+and run_script testsuite policy script invoke =
+  List.iter (fun cmd -> run_command testsuite policy cmd invoke) script
 
-and run_quote_script script invoke =
+and run_quote_script testsuite policy script invoke =
   let save_quote = !quote in
   quote := [];
-  ( try run_script script invoke
+  ( try run_script testsuite policy script invoke
     with exn ->
       quote := save_quote;
       raise exn );
@@ -547,7 +547,7 @@ let run_file _file =
 
 let run_string_concolic ~testsuite ~data policy =
   with_string data (fun script ->
-      run_script script (invoke_concolic testsuite policy) )
+      run_script testsuite policy script (invoke_concolic testsuite policy) )
 
 (* let run_string_se string = *)
 (*   input_string string ~callback:(fun s -> run_script s invoke_se) *)