Parameterize Thread on Symbolic Memory and Choice Monad on Thread

CHANGES.md

@@ -1,5 +1,6 @@
 ## unreleased
 
+- parameterize the `Thread` module on the symbolic memory and the `Choice_monad` module on a Thread
 - adds a `owi_char` function to create char symbolic value
 - adds a `Mem` argument to external function to allow direct manipulation of the memory.
 - support other solvers through the `--solver` option (Z3, Colibri2, Bitwuzla and CVC5)

src/cmd/cmd_sym.ml

@@ -4,7 +4,7 @@
 
 open Syntax
 module Expr = Smtml.Expr
-module Choice = Symbolic.P.Choice
+module Choice = Symbolic_choice_with_memory
 
 let ( let*/ ) (t : 'a Result.t) (f : 'a -> 'b Result.t Choice.t) :
   'b Result.t Choice.t =
@@ -46,14 +46,15 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
   let* _created_dir = Bos.OS.Dir.create ~path:true ~mode:0o755 workspace in
   let pc = Choice.return (Ok ()) in
   let result = List.fold_left (run_file ~unsafe ~optimize) pc files in
-  let thread : Thread.t = Thread.create () in
+  let thread = Thread_with_memory.init () in
   let res_queue = Wq.init () in
-  let callback = function
-    | Symbolic_choice.EVal (Ok ()), _ -> ()
+  let callback v =
+    match v with
+    | Symbolic_choice_intf.EVal (Ok ()), _ -> ()
     | v -> Wq.push v res_queue
   in
   let join_handles =
-    Symbolic_choice.run ~workers solver result thread ~callback
+    Symbolic_choice_with_memory.run ~workers solver result thread ~callback
       ~callback_init:(fun () -> Wq.make_pledge res_queue)
       ~callback_end:(fun () -> Wq.end_pledge res_queue)
   in
@@ -74,7 +75,7 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
     | Seq.Nil -> Ok count_acc
     | Seq.Cons ((result, _thread), tl) ->
       let* model =
-        let open Symbolic_choice in
+        let open Symbolic_choice_intf in
         match result with
         | EAssert (assertion, model) ->
           print_bug (`EAssert (assertion, model));
@@ -100,7 +101,7 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
     if deterministic_result_order then
       results
       |> Seq.map (function (_, thread) as x ->
-           (x, List.rev @@ Thread.breadcrumbs thread) )
+           (x, List.rev @@ Thread_with_memory.breadcrumbs thread) )
       |> List.of_seq
       |> List.sort (fun (_, bc1) (_, bc2) ->
              List.compare Prelude.Int32.compare bc1 bc2 )

src/dune

@@ -61,7 +61,10 @@
   solver
   symbolic
   symbolic_choice
+  symbolic_choice_intf
   symbolic_choice_minimalist
+  symbolic_choice_with_memory
+  symbolic_choice_without_memory
   symbolic_global
   symbolic_memory
   symbolic_table
@@ -75,6 +78,9 @@
   text_lexer
   text_parser
   thread
+  thread_intf
+  thread_with_memory
+  thread_without_memory
   tracing
   trap
   typecheck

src/intf/choice_intf.ml

@@ -40,4 +40,6 @@ module type Complete = sig
   val thread : thread t
 
   val add_pc : V.vbool -> unit t
+
+  val lift_mem : 'a Symbolic_choice_without_memory.t -> 'a t
 end

src/intf/symbolic_choice_intf.ml

@@ -0,0 +1,81 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+type 'a eval =
+  | EVal of 'a
+  | ETrap of Trap.t * Smtml.Model.t
+  | EAssert of Smtml.Expr.t * Smtml.Model.t
+
+module type S = sig
+  module V : Func_intf.Value_types
+
+  type thread
+
+  type 'a t
+
+  val return : 'a -> 'a t
+
+  val bind : 'a t -> ('a -> 'b t) -> 'b t
+
+  val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+
+  val map : 'a t -> ('a -> 'b) -> 'b t
+
+  val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+
+  val trap : Trap.t -> 'a t
+
+  val select : V.vbool -> bool t
+
+  val select_i32 : V.int32 -> Int32.t t
+
+  val assertion : V.vbool -> unit t
+
+  val with_thread : (thread -> 'a) -> 'a t
+
+  val with_new_symbol : Smtml.Ty.t -> (Smtml.Symbol.t -> 'b) -> 'b t
+
+  val solver : Solver.t t
+
+  val thread : thread t
+
+  val add_pc : V.vbool -> unit t
+
+  type 'a run_result = ('a eval * thread) Seq.t
+
+  val run :
+       workers:int
+    -> Smtml.Solver_dispatcher.solver_type
+    -> 'a t
+    -> thread
+    -> callback:('a eval * thread -> unit)
+    -> callback_init:(unit -> unit)
+    -> callback_end:(unit -> unit)
+    -> unit Domain.t array
+end
+
+module type Intf = sig
+  module type S = S
+
+  module CoreImpl : sig
+    (* The core implementation of the monad. It is isolated in a module to *)
+    (* restict its exposed interface and maintain its invariant. *)
+
+    module State : sig
+      type ('a, 's) t
+
+      val project_state :
+           ('st1 -> 'st2 * 'backup)
+        -> ('backup -> 'st2 -> 'st1)
+        -> ('a, 'st2) t
+        -> ('a, 'st1) t
+    end
+  end
+
+  module Make (Thread : Thread.S) :
+    S
+      with type 'a t = ('a eval, Thread.t) CoreImpl.State.t
+       and type thread := Thread.t
+       and module V := Symbolic_value
+end

src/intf/thread_intf.ml

@@ -0,0 +1,62 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+module type M = sig
+  type collection
+
+  val init : unit -> collection
+
+  val clone : collection -> collection
+end
+
+module type S = sig
+  type t
+
+  module Memory : M
+
+  val init : unit -> t
+
+  val create :
+       int
+    -> Smtml.Symbol.t list
+    -> Symbolic_value.vbool list
+    -> Memory.collection
+    -> Symbolic_table.collection
+    -> Symbolic_global.collection
+    -> int32 list
+    -> t
+
+  val pc : t -> Symbolic_value.vbool list
+
+  val memories : t -> Memory.collection
+
+  val tables : t -> Symbolic_table.collection
+
+  val globals : t -> Symbolic_global.collection
+
+  val breadcrumbs : t -> int32 list
+
+  val symbols_set : t -> Smtml.Symbol.t list
+
+  val symbols : t -> int
+
+  val clone : t -> t
+
+  val add_pc : t -> Symbolic_value.vbool -> t
+
+  val add_breadcrumb : t -> int32 -> t
+
+  val add_symbol : t -> Smtml.Symbol.t -> t
+
+  val incr_symbols : t -> t
+end
+
+module type Intf = sig
+  module type M = M
+
+  module type S = S
+
+  module Make (Symbolic_memory : M) :
+    S with type Memory.collection = Symbolic_memory.collection
+end

src/symbolic/symbolic.ml

@@ -2,20 +2,8 @@
 (* 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)
+    (Thread : Thread.S with type Memory.collection = Symbolic_memory.collection)
     (Choice : Choice_intf.Complete
                 with module V := Symbolic_value
                  and type thread := Thread.t) =
@@ -180,8 +168,10 @@ struct
   end
 end
 
-module P = MakeP [@inlined hint] (Thread) (Symbolic_choice)
-module M = MakeP [@inlined hint] (Thread) (Symbolic_choice_minimalist)
+module P =
+  MakeP [@inlined hint] (Thread_with_memory) (Symbolic_choice_with_memory)
+module M =
+  MakeP [@inlined hint] (Thread_with_memory) (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 }