wip

src/cmd/cmd_sym.ml

@@ -17,8 +17,12 @@ let link_state =
        Link.extern_module' Link.empty_state ~name:"symbolic" ~func_typ
          Symbolic_wasm_ffi.symbolic_extern_module
      in
-     Link.extern_module' link_state ~name:"summaries" ~func_typ
-       Symbolic_wasm_ffi.summaries_extern_module )
+     let link_state =
+       Link.extern_module' link_state ~name:"summaries" ~func_typ
+         Symbolic_wasm_ffi.summaries_extern_module
+     in
+     Link.extern_module' link_state ~name:"debug" ~func_typ
+       Symbolic_wasm_ffi.debug_extern_module )
 
 let run_binary_modul ~unsafe ~optimize (pc : unit Result.t Choice.t)
   (m : Binary.modul) =
@@ -81,9 +85,9 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
       Format.pp_std "Assert failure: %a@\n" Expr.pp assertion;
       Format.pp_std "Model:@\n  @[<v>%a@]@." (Smtml.Model.pp ~no_values) model
   in
-  let rec print_and_count_failures count_acc results =
+  let rec print_and_count_failures (failures_acc, paths_acc) results =
     match results () with
-    | Seq.Nil -> Ok count_acc
+    | Seq.Nil -> Ok (failures_acc, paths_acc)
     | Seq.Cons ((result, _thread), tl) ->
       let* model =
         let open Symbolic_choice in
@@ -98,7 +102,8 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
           failwith "unreachable: callback should have filtered eval ok out."
         | EVal (Error e) -> Error e
       in
-      let count_acc = succ count_acc in
+      let paths_acc = succ paths_acc in
+      let failures_acc = succ failures_acc in
       let* () =
         if not no_values then
           let testcase =
@@ -107,8 +112,9 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
           Cmd_utils.write_testcase ~dir:workspace testcase
         else Ok ()
       in
-      if no_stop_at_failure then print_and_count_failures count_acc tl
-      else Ok count_acc
+      if no_stop_at_failure then
+        print_and_count_failures (failures_acc, paths_acc) tl
+      else Ok (failures_acc, paths_acc)
   in
   let results =
     if deterministic_result_order then
@@ -121,8 +127,9 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
       |> List.to_seq |> Seq.map fst
     else results
   in
-  let* count = print_and_count_failures 0 results in
-  if count > 0 then Error (`Found_bug count)
+  let* failures, paths = print_and_count_failures (0, 0) results in
+  Format.pp_std "Completed paths: %d@." paths;
+  if failures > 0 then Error (`Found_bug failures)
   else begin
     Format.pp_std "All OK";
     Ok ()

src/concolic/concolic_wasm_ffi.ml

@@ -184,3 +184,7 @@ let summaries_extern_module =
     ]
   in
   { Link.functions }
+
+let debug_extern_module =
+  let functions = [] in
+  { Link.functions }

src/intf/wasm_ffi_intf.ml

@@ -46,4 +46,6 @@ module type S = sig
   val symbolic_extern_module : extern_func Link.extern_module
 
   val summaries_extern_module : extern_func Link.extern_module
+
+  val debug_extern_module : extern_func Link.extern_module
 end

src/symbolic/symbolic.ml

@@ -57,58 +57,25 @@ struct
   module Memory = struct
     include Symbolic_memory
 
-    let concretise (a : Smtml.Expr.t) : Smtml.Expr.t Choice.t =
-      let open Choice in
-      let open Smtml in
-      match Expr.view a with
-      (* Avoid unecessary re-hashconsing and allocation when the value
-         is already concrete. *)
-      | Val _ | Ptr { offset = { node = Val _; _ }; _ } -> return a
-      | Ptr { base; offset } ->
-        let+ offset = select_i32 offset in
-        Expr.ptr base (Symbolic_value.const_i32 offset)
-      | _ ->
-        let+ v = select_i32 a in
-        Symbolic_value.const_i32 v
-
-    let check_within_bounds m a =
-      match check_within_bounds m a with
-      | Error t -> Choice.trap t
-      | Ok (cond, ptr) ->
-        let open Choice in
-        let* out_of_bounds = select cond in
-        if out_of_bounds then trap Trap.Memory_heap_buffer_overflow
-        else return ptr
-
-    let with_concrete (m : t) a f : 'a Choice.t =
-      let open Choice in
-      let* addr = concretise a in
-      let+ ptr = check_within_bounds m addr in
-      f m ptr
-
-    let load_8_s m a = with_concrete m a load_8_s
+    let load_8_s m a = Choice.return @@ load_8_s m a
 
-    let load_8_u m a = with_concrete m a load_8_u
+    let load_8_u m a = Choice.return @@ load_8_u m a
 
-    let load_16_s m a = with_concrete m a load_16_s
+    let load_16_s m a = Choice.return @@ load_16_s m a
 
-    let load_16_u m a = with_concrete m a load_16_u
+    let load_16_u m a = Choice.return @@ load_16_u m a
 
-    let load_32 m a = with_concrete m a load_32
+    let load_32 m a = Choice.return @@ load_32 m a
 
-    let load_64 m a = with_concrete m a load_64
+    let load_64 m a = Choice.return @@ load_64 m a
 
-    let store_8 m ~addr v =
-      with_concrete m addr (fun m addr -> store_8 m ~addr v)
+    let store_8 m ~addr v = Choice.return @@ store_8 m ~addr v
 
-    let store_16 m ~addr v =
-      with_concrete m addr (fun m addr -> store_16 m ~addr v)
+    let store_16 m ~addr v = Choice.return @@ store_16 m ~addr v
 
-    let store_32 m ~addr v =
-      with_concrete m addr (fun m addr -> store_32 m ~addr v)
+    let store_32 m ~addr v = Choice.return @@ store_32 m ~addr v
 
-    let store_64 m ~addr v =
-      with_concrete m addr (fun m addr -> store_64 m ~addr v)
+    let store_64 m ~addr v = Choice.return @@ store_64 m ~addr v
   end
 
   module Data = struct

src/symbolic/symbolic.old.ml

@@ -0,0 +1,189 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+module type Thread = sig
+  type t
+
+  val memories : t -> Symbolic_memory.collection
+
+  val tables : t -> Symbolic_table.collection
+
+  val globals : t -> Symbolic_global.collection
+
+  val pc : t -> Symbolic_value.vbool list
+end
+
+module MakeP
+    (Thread : Thread)
+    (Choice : Choice_intf.Complete
+                with module V := Symbolic_value
+                 and type thread := Thread.t) =
+struct
+  module Value = Symbolic_value
+  module Choice = Choice
+  module Extern_func = Concrete_value.Make_extern_func (Value) (Choice)
+  module Global = Symbolic_global
+  module Table = Symbolic_table
+
+  type thread = Thread.t
+
+  let select (c : Value.vbool) ~(if_true : Value.t) ~(if_false : Value.t) :
+    Value.t Choice.t =
+    match (if_true, if_false) with
+    | I32 if_true, I32 if_false ->
+      Choice.return (Value.I32 (Value.Bool.select_expr c ~if_true ~if_false))
+    | I64 if_true, I64 if_false ->
+      Choice.return (Value.I64 (Value.Bool.select_expr c ~if_true ~if_false))
+    | F32 if_true, F32 if_false ->
+      Choice.return (Value.F32 (Value.Bool.select_expr c ~if_true ~if_false))
+    | F64 if_true, F64 if_false ->
+      Choice.return (Value.F64 (Value.Bool.select_expr c ~if_true ~if_false))
+    | Ref _, Ref _ ->
+      let open Choice in
+      let+ b = select c in
+      if b then if_true else if_false
+    | _, _ -> assert false
+
+  module Elem = struct
+    type t = Link_env.elem
+
+    let get (elem : t) i : Value.ref_value =
+      match elem.value.(i) with Funcref f -> Funcref f | _ -> assert false
+
+    let size (elem : t) = Array.length elem.value
+  end
+
+  module Memory = struct
+    include Symbolic_memory
+
+    let concretise (a : Smtml.Expr.t) : Smtml.Expr.t Choice.t =
+      let open Choice in
+      let open Smtml in
+      match Expr.view a with
+      (* Avoid unecessary re-hashconsing and allocation when the value
+         is already concrete. *)
+      | Val _ | Ptr { offset = { node = Val _; _ }; _ } -> return a
+      | Ptr { base; offset } ->
+        let+ offset = select_i32 offset in
+        Expr.ptr base (Symbolic_value.const_i32 offset)
+      | _ ->
+        let+ v = select_i32 a in
+        Symbolic_value.const_i32 v
+
+    let check_within_bounds m a =
+      match is_out_of_bounds m a with
+      | Error t -> Choice.trap t
+      | Ok (cond, ptr) ->
+        let open Choice in
+        let* out_of_bounds = select cond in
+        if out_of_bounds then trap Trap.Memory_heap_buffer_overflow
+        else return ptr
+
+    let with_concrete (m : t) a f : 'a Choice.t =
+      let open Choice in
+      let* addr = concretise a in
+      let+ ptr = check_within_bounds m addr in
+      f m ptr
+
+    let load_8_s m a = with_concrete m a load_8_s
+
+    let load_8_u m a = with_concrete m a load_8_u
+
+    let load_16_s m a = with_concrete m a load_16_s
+
+    let load_16_u m a = with_concrete m a load_16_u
+
+    let load_32 m a = with_concrete m a load_32
+
+    let load_64 m a = with_concrete m a load_64
+
+    let store_8 m ~addr v =
+      with_concrete m addr (fun m addr -> store_8 m ~addr v)
+
+    let store_16 m ~addr v =
+      with_concrete m addr (fun m addr -> store_16 m ~addr v)
+
+    let store_32 m ~addr v =
+      with_concrete m addr (fun m addr -> store_32 m ~addr v)
+
+    let store_64 m ~addr v =
+      with_concrete m addr (fun m addr -> store_64 m ~addr v)
+  end
+
+  module Data = struct
+    type t = Link_env.data
+
+    let value data = data.Link_env.value
+  end
+
+  module Env = struct
+    type t = Extern_func.extern_func Link_env.t
+
+    type t' = Env_id.t
+
+    let get_memory env id =
+      let orig_mem = Link_env.get_memory env id in
+      let f (t : thread) =
+        let memories = Thread.memories t in
+        Symbolic_memory.get_memory (Link_env.id env) orig_mem memories id
+      in
+      Choice.with_thread f
+
+    let get_func = Link_env.get_func
+
+    let get_extern_func = Link_env.get_extern_func
+
+    let get_table (env : t) i : Table.t Choice.t =
+      let orig_table = Link_env.get_table env i in
+      let f (t : thread) =
+        let tables = Thread.tables t in
+        Symbolic_table.get_table (Link_env.id env) orig_table tables i
+      in
+      Choice.with_thread f
+
+    let get_elem env i = Link_env.get_elem env i
+
+    let get_data env n =
+      let data = Link_env.get_data env n in
+      Choice.return data
+
+    let get_global (env : t) i : Global.t Choice.t =
+      let orig_global = Link_env.get_global env i in
+      let f (t : thread) =
+        let globals = Thread.globals t in
+        Symbolic_global.get_global (Link_env.id env) orig_global globals i
+      in
+      Choice.with_thread f
+
+    let drop_elem _ =
+      (* TODO *)
+      ()
+
+    let drop_data = Link_env.drop_data
+  end
+
+  module Module_to_run = struct
+    (** runnable module *)
+    type t =
+      { modul : Binary.modul
+      ; env : Env.t
+      ; to_run : Types.binary Types.expr list
+      }
+
+    let env (t : t) = t.env
+
+    let modul (t : t) = t.modul
+
+    let to_run (t : t) = t.to_run
+  end
+end
+
+module P = MakeP [@inlined hint] (Thread) (Symbolic_choice)
+module M = MakeP [@inlined hint] (Thread) (Symbolic_choice_minimalist)
+
+let convert_module_to_run (m : 'f Link.module_to_run) =
+  P.Module_to_run.{ modul = m.modul; env = m.env; to_run = m.to_run }
+
+let convert_module_to_run_minimalist (m : 'f Link.module_to_run) =
+  M.Module_to_run.{ modul = m.modul; env = m.env; to_run = m.to_run }