From f12f7b7c2aea9ed587762b3e2d4297a0b32e949f Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Mon, 15 Jul 2024 16:08:48 +0200 Subject: [PATCH] Add mlis for Symbolic_choice_with(out)_memory modules --- src/cmd/cmd_sym.ml | 1 - src/intf/thread_intf.ml | 9 ---- src/symbolic/symbolic.ml | 2 +- src/symbolic/symbolic_choice.ml | 11 ++--- src/symbolic/symbolic_choice_with_memory.ml | 4 ++ ...ce.mli => symbolic_choice_with_memory.mli} | 7 ++-- .../symbolic_choice_without_memory.ml | 4 ++ .../symbolic_choice_without_memory.mli | 42 +++++++++++++++++++ src/symbolic/thread_with_memory.mli | 2 +- src/symbolic/thread_without_memory.mli | 2 +- 10 files changed, 62 insertions(+), 22 deletions(-) rename src/symbolic/{.symbolic_choice.mli => symbolic_choice_with_memory.mli} (78%) create mode 100644 src/symbolic/symbolic_choice_without_memory.mli diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml index 33e6a9ed9..d9d15cc89 100644 --- a/src/cmd/cmd_sym.ml +++ b/src/cmd/cmd_sym.ml @@ -109,7 +109,6 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values else results in let* count = print_and_count_failures 0 results in - Format.pp_std "completed paths: %d@." !path_counter; if count > 0 then Error (`Found_bug count) else begin Fmt.pr "All OK"; diff --git a/src/intf/thread_intf.ml b/src/intf/thread_intf.ml index 904380f66..476de531f 100644 --- a/src/intf/thread_intf.ml +++ b/src/intf/thread_intf.ml @@ -52,20 +52,11 @@ module type S = sig val incr_symbols : t -> t end -module type S_with_memory = - S with type Memory.collection = Symbolic_memory.collection - -module type S_without_memory = S with type Memory.collection = bool - module type Intf = sig module type M = M module type S = S - module type S_with_memory = S_with_memory - - module type S_without_memory = S_without_memory - module Make (Symbolic_memory : M) : S with type Memory.collection = Symbolic_memory.collection end diff --git a/src/symbolic/symbolic.ml b/src/symbolic/symbolic.ml index c3030e558..c33009e98 100644 --- a/src/symbolic/symbolic.ml +++ b/src/symbolic/symbolic.ml @@ -3,7 +3,7 @@ (* Written by the Owi programmers *) module MakeP - (Thread : Thread.S_with_memory) + (Thread : Thread.S with type Memory.collection = Symbolic_memory.collection) (Choice : Choice_intf.Complete with module V := Symbolic_value and type thread := Thread.t) = diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml index 5dd8249b8..366b3a77f 100644 --- a/src/symbolic/symbolic_choice.ml +++ b/src/symbolic/symbolic_choice.ml @@ -225,10 +225,10 @@ module CoreImpl = struct other = St (fun st -> - let ( let* ) = M.( let* ) in + let ( let+ ) = M.( let+ ) in let proj, backup = project_and_backup st in - let* res, new_state = run other proj in - M.return (res, restore backup new_state) ) + let+ res, new_state = run other proj in + (res, restore backup new_state) ) end module Eval = struct @@ -274,7 +274,9 @@ module CoreImpl = struct end (* *) - module Make (Thread : Thread.S) = struct + module Make (Thread : Thread.S) : + S with type thread := Thread.t and type 'a t = ('a, Thread.t) Eval.t = + struct include Eval type 'a t = ('a, Thread.t) Eval.t @@ -343,7 +345,6 @@ end We can now use CoreImpl only through its exposed signature which maintains all invariants. *) -(* module CoreImpl' : S = CoreImpl *) module Make (Thread : Thread.S) = struct include CoreImpl.Make (Thread) diff --git a/src/symbolic/symbolic_choice_with_memory.ml b/src/symbolic/symbolic_choice_with_memory.ml index a15689a8a..d143f5d0b 100644 --- a/src/symbolic/symbolic_choice_with_memory.ml +++ b/src/symbolic/symbolic_choice_with_memory.ml @@ -1,3 +1,7 @@ +(* SPDX-License-Identifier: AGPL-3.0-or-later *) +(* Copyright © 2021-2024 OCamlPro *) +(* Written by the Owi programmers *) + include Symbolic_choice.Make (Thread_with_memory) let lift_mem (mem_op : 'a Symbolic_choice_without_memory.t) : 'a t = diff --git a/src/symbolic/.symbolic_choice.mli b/src/symbolic/symbolic_choice_with_memory.mli similarity index 78% rename from src/symbolic/.symbolic_choice.mli rename to src/symbolic/symbolic_choice_with_memory.mli index c52a97c0d..602df230b 100644 --- a/src/symbolic/.symbolic_choice.mli +++ b/src/symbolic/symbolic_choice_with_memory.mli @@ -9,8 +9,7 @@ type 'a eval = private include Choice_intf.Complete - with type thread := Thread.t - and type 'a run_result = ('a eval * Thread.t) Seq.t + with type thread := Thread_with_memory.t and module V := Symbolic_value val with_new_symbol : Smtml.Ty.t -> (Smtml.Symbol.t -> 'b) -> 'b t @@ -19,8 +18,8 @@ val run : workers:int -> Smtml.Solver_dispatcher.solver_type -> 'a t - -> Thread.t - -> callback:('a eval * Thread.t -> unit) + -> Thread_with_memory.t + -> callback:('a eval * Thread_with_memory.t -> unit) -> callback_init:(unit -> unit) -> callback_end:(unit -> unit) -> unit Domain.t array diff --git a/src/symbolic/symbolic_choice_without_memory.ml b/src/symbolic/symbolic_choice_without_memory.ml index 4351d9b18..5041426ce 100644 --- a/src/symbolic/symbolic_choice_without_memory.ml +++ b/src/symbolic/symbolic_choice_without_memory.ml @@ -1 +1,5 @@ +(* SPDX-License-Identifier: AGPL-3.0-or-later *) +(* Copyright © 2021-2024 OCamlPro *) +(* Written by the Owi programmers *) + include Symbolic_choice.Make (Thread_without_memory) diff --git a/src/symbolic/symbolic_choice_without_memory.mli b/src/symbolic/symbolic_choice_without_memory.mli new file mode 100644 index 000000000..e44339c9b --- /dev/null +++ b/src/symbolic/symbolic_choice_without_memory.mli @@ -0,0 +1,42 @@ +(* SPDX-License-Identifier: AGPL-3.0-or-later *) +(* 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 diff --git a/src/symbolic/thread_with_memory.mli b/src/symbolic/thread_with_memory.mli index 683d4debb..0e93de7a9 100644 --- a/src/symbolic/thread_with_memory.mli +++ b/src/symbolic/thread_with_memory.mli @@ -3,7 +3,7 @@ (* Written by the Owi programmers *) (** @inline *) -include Thread.S_with_memory +include Thread.S with type Memory.collection = Symbolic_memory.collection val project : t -> Thread_without_memory.t * Memory.collection diff --git a/src/symbolic/thread_without_memory.mli b/src/symbolic/thread_without_memory.mli index db2d1f1f3..f385f9e7e 100644 --- a/src/symbolic/thread_without_memory.mli +++ b/src/symbolic/thread_without_memory.mli @@ -3,4 +3,4 @@ (* Written by the Owi programmers *) (** @inline *) -include Thread.S_without_memory +include Thread.S with type Memory.collection = bool