From 8a20a3987003edf84f1d2928cc8a6772ff4eb963 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Wed, 31 Jul 2024 11:41:46 +0200 Subject: [PATCH] Reintroduce `symbolic_choice.mli` Creates `symbolic_choice_intf.ml` to define the symbolic choice monad's interface and `eval` type definition for easier reuse. --- src/cmd/cmd_sym.ml | 4 +- src/dune | 1 + src/intf/symbolic_choice_intf.ml | 81 +++++++++++ src/symbolic/symbolic_choice.ml | 130 ++++++++---------- src/symbolic/symbolic_choice.mli | 6 + src/symbolic/symbolic_choice_with_memory.mli | 25 +--- .../symbolic_choice_without_memory.mli | 46 ++----- 7 files changed, 163 insertions(+), 130 deletions(-) create mode 100644 src/intf/symbolic_choice_intf.ml create mode 100644 src/symbolic/symbolic_choice.mli diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml index d9d15cc89..f61287521 100644 --- a/src/cmd/cmd_sym.ml +++ b/src/cmd/cmd_sym.ml @@ -50,7 +50,7 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values let res_queue = Wq.init () in let callback v = match v with - | Symbolic_choice_with_memory.EVal (Ok ()), _ -> () + | Symbolic_choice_intf.EVal (Ok ()), _ -> () | v -> Wq.push v res_queue in let join_handles = @@ -75,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_with_memory in + let open Symbolic_choice_intf in match result with | EAssert (assertion, model) -> print_bug (`EAssert (assertion, model)); diff --git a/src/dune b/src/dune index a1f301801..d95dc021c 100644 --- a/src/dune +++ b/src/dune @@ -61,6 +61,7 @@ solver symbolic symbolic_choice + symbolic_choice_intf symbolic_choice_minimalist symbolic_choice_with_memory symbolic_choice_without_memory diff --git a/src/intf/symbolic_choice_intf.ml b/src/intf/symbolic_choice_intf.ml new file mode 100644 index 000000000..1c39b7ab0 --- /dev/null +++ b/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 diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml index 366b3a77f..322d883c0 100644 --- a/src/symbolic/symbolic_choice.ml +++ b/src/symbolic/symbolic_choice.ml @@ -2,68 +2,7 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -module type S = sig - (* - The core implementation of the monad. It is isolated in a module to restict its exposed interface - and maintain its invariant. In particular, choose must guarantee that the Thread.t is cloned in each branch. - Using functions defined here should be foolproof. - *) - - 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 assertion_fail : Smtml.Expr.t -> Smtml.Model.t -> 'a t - - val stop : 'a t - - val trap : Trap.t -> 'a t - - val thread : thread t - - val yield : unit t - - val solver : Solver.t t - - val with_thread : (thread -> 'a) -> 'a t - - val set_thread : thread -> unit t - - val modify_thread : (thread -> thread) -> unit t - - (* - Indicates a possible choice between two values. Thread duplication - is already handled by choose and should not be done before by the caller. - *) - val choose : 'a t -> 'a t -> 'a t - - type 'a eval = - | EVal of 'a - | ETrap of Trap.t * Smtml.Model.t - | EAssert of Smtml.Expr.t * Smtml.Model.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 +include Symbolic_choice_intf (* Multicore is based on several layers of monad transformers defined here @@ -238,11 +177,6 @@ module CoreImpl = struct *) module M = State - type 'a eval = - | EVal of 'a - | ETrap of Trap.t * Smtml.Model.t - | EAssert of Smtml.Expr.t * Smtml.Model.t - type ('a, 's) t = ('a eval, 's) M.t let return x : _ t = M.return (EVal x) @@ -273,10 +207,63 @@ module CoreImpl = struct let ( let+ ) = map end - (* *) - module Make (Thread : Thread.S) : - S with type thread := Thread.t and type 'a t = ('a, Thread.t) Eval.t = - struct + module Make (Thread : Thread.S) : sig + (* + The core implementation of the monad. It is isolated in a module to restict its exposed interface + and maintain its invariant. In particular, choose must guarantee that the Thread.t is cloned in each branch. + Using functions defined here should be foolproof. + *) + + type thread := Thread.t + + type 'a t = ('a, Thread.t) Eval.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 assertion_fail : Smtml.Expr.t -> Smtml.Model.t -> 'a t + + val stop : 'a t + + val trap : Trap.t -> 'a t + + val thread : thread t + + val yield : unit t + + val solver : Solver.t t + + val with_thread : (thread -> 'a) -> 'a t + + val set_thread : thread -> unit t + + val modify_thread : (thread -> thread) -> unit t + + (* + Indicates a possible choice between two values. Thread duplication + is already handled by choose and should not be done before by the caller. + *) + val choose : 'a t -> 'a t -> 'a 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 = struct include Eval type 'a t = ('a, Thread.t) Eval.t @@ -345,7 +332,6 @@ end We can now use CoreImpl only through its exposed signature which maintains all invariants. *) - module Make (Thread : Thread.S) = struct include CoreImpl.Make (Thread) diff --git a/src/symbolic/symbolic_choice.mli b/src/symbolic/symbolic_choice.mli new file mode 100644 index 000000000..248f3fa72 --- /dev/null +++ b/src/symbolic/symbolic_choice.mli @@ -0,0 +1,6 @@ +(* SPDX-License-Identifier: AGPL-3.0-or-later *) +(* Copyright © 2021-2024 OCamlPro *) +(* Written by the Owi programmers *) + +(** @inline *) +include Symbolic_choice_intf.Intf diff --git a/src/symbolic/symbolic_choice_with_memory.mli b/src/symbolic/symbolic_choice_with_memory.mli index 602df230b..dfdf98570 100644 --- a/src/symbolic/symbolic_choice_with_memory.mli +++ b/src/symbolic/symbolic_choice_with_memory.mli @@ -2,24 +2,13 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -type 'a eval = private - | EVal of 'a - | ETrap of Trap.t * Smtml.Model.t - | EAssert of Smtml.Expr.t * Smtml.Model.t - include - Choice_intf.Complete - with type thread := Thread_with_memory.t + Symbolic_choice_intf.S + with type 'a t = + ( 'a Symbolic_choice_intf.eval + , Thread_with_memory.t ) + Symbolic_choice.CoreImpl.State.t + and type thread := Thread_with_memory.t and module V := Symbolic_value -val with_new_symbol : Smtml.Ty.t -> (Smtml.Symbol.t -> 'b) -> 'b t - -val run : - workers:int - -> Smtml.Solver_dispatcher.solver_type - -> 'a t - -> Thread_with_memory.t - -> callback:('a eval * Thread_with_memory.t -> unit) - -> callback_init:(unit -> unit) - -> callback_end:(unit -> unit) - -> unit Domain.t array +val lift_mem : 'a Symbolic_choice_without_memory.t -> 'a t diff --git a/src/symbolic/symbolic_choice_without_memory.mli b/src/symbolic/symbolic_choice_without_memory.mli index e44339c9b..422b6cd55 100644 --- a/src/symbolic/symbolic_choice_without_memory.mli +++ b/src/symbolic/symbolic_choice_without_memory.mli @@ -2,41 +2,11 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -type 'a eval = private - | EVal of 'a - | ETrap of Trap.t * Smtml.Model.t - | EAssert of Smtml.Expr.t * Smtml.Model.t - -type 'a t = ('a, Thread_without_memory.t) Symbolic_choice.CoreImpl.Eval.t - -type thread := Thread_without_memory.t - -module V := Symbolic_value - -type 'a run_result - -val return : 'a -> 'a t - -val bind : 'a t -> ('a -> 'b t) -> 'b t - -val map : 'a t -> ('a -> 'b) -> 'b t - -val select : V.vbool -> bool t - -val select_i32 : V.int32 -> Int32.t t - -val trap : Trap.t -> 'a t - -val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t - -val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t - -val assertion : V.vbool -> unit t - -val with_thread : (thread -> 'b) -> 'b t - -val solver : Solver.t t - -val thread : thread t - -val add_pc : V.vbool -> unit t +include + Symbolic_choice_intf.S + with type 'a t = + ( 'a Symbolic_choice_intf.eval + , Thread_without_memory.t ) + Symbolic_choice.CoreImpl.State.t + and type thread := Thread_without_memory.t + and module V := Symbolic_value