Minor refactor of Matcher + Pstate and move Combinators around

Gillian-C2/lib/lifter/c2_lifter.ml

@@ -34,7 +34,7 @@ module Make
     (Gil :
       Gillian.Debugger.Lifter.Gil_fallback_lifter.Gil_lifter_with_state
         with type Lifter.memory = SMemory.t)
-    (Verification : Engine.Verifier.S with type annot = C2_annot.t) =
+    (Verification : Verify.Verifier.S with type annot = C2_annot.t) =
 struct
   open Exec_map
   module CmdReport = Verification.SAInterpreter.Logging.ConfigReport

GillianCore/biabduction/dune

@@ -0,0 +1,20 @@
+(library
+ (name biabduction)
+ (public_name gillian.biabduction)
+ (libraries engine monadic combinators utils gil_syntax incrementalAnalysis)
+ (preprocess
+  (pps ppx_deriving.std ppx_deriving_yojson))
+ (instrumentation
+  (backend landmarks --auto))
+ (flags
+  :standard
+  -open
+  Utils
+  -open
+  Gil_syntax
+  -open
+  Utils.Prelude
+  -open
+  IncrementalAnalysis
+  -open
+  Engine))

transformers/lib/states/ActionAdder.ml → GillianCore/combinators/ActionAdder.ml

@@ -1,5 +1,5 @@
 open Gil_syntax
-open Gillian.Monadic
+open Monadic
 
 module type ActionAddition = sig
   type t
@@ -17,7 +17,7 @@ module type ActionAddition = sig
   val get_fixes : err_t -> string Fix.t list
 
   val get_recovery_tactic :
-    t -> err_t -> Expr.t Gillian.General.Recovery_tactic.t
+    t -> err_t -> Expr.t Engine.General.Recovery_tactic.t
 end
 
 module Make (A : ActionAddition) (S : MyMonadicSMemory.S with type t = A.t) =

transformers/lib/states/Agreement.ml → GillianCore/combinators/Agreement.ml

@@ -1,9 +1,9 @@
-open Gillian.Utils
-open Gillian.Monadic
-open Gillian.Symbolic
+open Utils
+open Monadic
+open Engine.Symbolic
 open Gil_syntax
 module DR = Delayed_result
-module Recovery_tactic = Gillian.General.Recovery_tactic
+module Recovery_tactic = Engine.General.Recovery_tactic
 
 type t = Expr.t option [@@deriving yojson]
 type err_t = MissingState [@@deriving show, yojson]

transformers/lib/states/Exclusive.ml → GillianCore/combinators/Exclusive.ml

@@ -1,9 +1,9 @@
-open Gillian.Utils
-open Gillian.Monadic
-open Gillian.Symbolic
+open Utils
+open Monadic
+open Engine.Symbolic
 open Gil_syntax
 module DR = Delayed_result
-module Recovery_tactic = Gillian.General.Recovery_tactic
+module Recovery_tactic = Engine.General.Recovery_tactic
 
 type t = Expr.t option [@@deriving show, yojson]
 type err_t = MissingState [@@deriving show, yojson]

transformers/lib/states/Fix.ml → GillianCore/combinators/Fix.ml

@@ -1,10 +1,10 @@
-open Gillian.Gil_syntax
+open Gil_syntax
 
 type 'cp atom = 'cp * Expr.t list * Expr.t list [@@deriving yojson, show]
 type 'cp t = 'cp atom list [@@deriving yojson, show]
 
 let lvars (fix : 'cp t) =
-  let open Gillian.Utils.Containers in
+  let open Utils.Containers in
   List.fold_left
     (fun acc (_, ins, outs) ->
       let acc =
@@ -14,7 +14,7 @@ let lvars (fix : 'cp t) =
     SS.empty fix
 
 let alocs (fix : 'cp t) =
-  let open Gillian.Utils.Containers in
+  let open Utils.Containers in
   List.fold_left
     (fun acc (_, ins, outs) ->
       let acc =
@@ -23,8 +23,8 @@ let alocs (fix : 'cp t) =
       List.fold_left (fun acc e -> SS.union acc (Expr.alocs e)) acc outs)
     SS.empty fix
 
-let subst (subst : Gillian.Symbolic.Subst.t) (fix : 'a t) : 'a t =
-  let le_subst = Gillian.Symbolic.Subst.subst_in_expr subst ~partial:true in
+let subst (subst : Engine.Symbolic.Subst.t) (fix : 'a t) : 'a t =
+  let le_subst = Engine.Symbolic.Subst.subst_in_expr subst ~partial:true in
   let subst_atom (cp, ins, outs) =
     (cp, List.map le_subst ins, List.map le_subst outs)
   in

transformers/lib/states/Fractional.ml → GillianCore/combinators/Fractional.ml

@@ -1,9 +1,9 @@
-open Gillian.Utils
-open Gillian.Monadic
-open Gillian.Symbolic
+open Utils
+open Monadic
+open Engine.Symbolic
 open Gil_syntax
 module DR = Delayed_result
-module Recovery_tactic = Gillian.General.Recovery_tactic
+module Recovery_tactic = Engine.General.Recovery_tactic
 
 type err = MissingState | NotEnoughPermission [@@deriving show, yojson]
 

transformers/lib/states/Freeable.ml → GillianCore/combinators/Freeable.ml

@@ -1,6 +1,6 @@
-open Gillian.Utils
-open Gillian.Monadic
-open Gillian.Symbolic
+open Utils
+open Monadic
+open Engine.Symbolic
 module DR = Delayed_result
 
 type 'a freeable = None | Freed | SubState of 'a [@@deriving yojson, show]
@@ -168,7 +168,7 @@ module Make (S : MyMonadicSMemory.S) :
   let get_recovery_tactic s e =
     match (s, e) with
     | SubState s, SubError e -> S.get_recovery_tactic s e
-    | _ -> Gillian.General.Recovery_tactic.none (* TODO *)
+    | _ -> Engine.General.Recovery_tactic.none (* TODO *)
 
   let can_fix = function
     | SubError e -> S.can_fix e

transformers/lib/states/Injector.ml → GillianCore/combinators/Injector.ml

@@ -1,5 +1,5 @@
 open Gil_syntax
-open Gillian.Monadic
+open Monadic
 open Delayed.Syntax
 open Delayed_result.Syntax
 

transformers/lib/states/MList.ml → GillianCore/combinators/MList.ml

@@ -1,6 +1,6 @@
-open Gillian.Utils
-open Gillian.Monadic
-open Gillian.Symbolic
+open Utils
+open Monadic
+open Engine.Symbolic
 open Gil_syntax
 module DR = Delayed_result
 module ExpMap = MyUtils.ExpMap
@@ -222,12 +222,12 @@ module Make (S : MyMonadicSMemory.S) :
         let sub_recover =
           match ExpMap.find_opt idx (fst st) with
           | Some codom -> S.get_recovery_tactic codom e
-          | None -> Gillian.General.Recovery_tactic.none
+          | None -> Engine.General.Recovery_tactic.none
         in
-        Gillian.General.Recovery_tactic.merge
-          (Gillian.General.Recovery_tactic.try_unfold [ idx ])
+        Engine.General.Recovery_tactic.merge
+          (Engine.General.Recovery_tactic.try_unfold [ idx ])
           sub_recover
-    | _ -> Gillian.General.Recovery_tactic.none
+    | _ -> Engine.General.Recovery_tactic.none
 
   let can_fix = function
     | SubError (_, e) -> S.can_fix e

transformers/lib/states/MyMonadicSMemory.ml → GillianCore/combinators/MyMonadicSMemory.ml

@@ -1,9 +1,9 @@
-open Gillian.Monadic
-open Gillian.Symbolic
+open Monadic
+open Engine.Symbolic
 open Gil_syntax
-module Containers = Gillian.Utils.Containers
+module Containers = Utils.Containers
 module DR = Delayed_result
-module Recovery_tactic = Gillian.General.Recovery_tactic
+module Recovery_tactic = Engine.General.Recovery_tactic
 
 module type S = sig
   (* Type of states *)

transformers/lib/states/MyUtils.ml → GillianCore/combinators/MyUtils.ml

@@ -1,5 +1,5 @@
-open Gillian.Utils
-open Gillian.Monadic
+open Utils
+open Monadic
 open Gil_syntax
 
 module type IDs = sig
@@ -153,7 +153,7 @@ let get_loc =
           some ~learned:[ e == ALoc loc_name ] loc_name)
   | _ -> none ()
 
-module SMap = Gillian.Utils.Prelude.Map.Make (struct
+module SMap = Utils.Prelude.Map.Make (struct
   include String
 
   let of_yojson = function

transformers/lib/states/PMap.ml → GillianCore/combinators/PMap.ml

@@ -1,6 +1,6 @@
 open Gil_syntax
-open Gillian.Monadic
-module Subst = Gillian.Symbolic.Subst
+open Monadic
+module Subst = Engine.Symbolic.Subst
 module DR = Delayed_result
 module DO = Delayed_option
 
@@ -379,13 +379,13 @@ struct
         let sub_recover =
           match I.find_opt_unsafe (fst st) idx with
           | Some codom -> S.get_recovery_tactic codom e
-          | None -> Gillian.General.Recovery_tactic.none
+          | None -> Engine.General.Recovery_tactic.none
         in
-        Gillian.General.Recovery_tactic.merge sub_recover
-          (Gillian.General.Recovery_tactic.try_unfold [ idx ])
+        Engine.General.Recovery_tactic.merge sub_recover
+          (Engine.General.Recovery_tactic.try_unfold [ idx ])
     | NotAllocated idx | InvalidIndexValue idx ->
-        Gillian.General.Recovery_tactic.try_unfold [ idx ]
-    | _ -> Gillian.General.Recovery_tactic.none
+        Engine.General.Recovery_tactic.try_unfold [ idx ]
+    | _ -> Engine.General.Recovery_tactic.none
 
   let can_fix = function
     | SubError (_, _, e) -> S.can_fix e
@@ -545,12 +545,11 @@ struct
         let sub_recover =
           match I.find_opt_unsafe st idx with
           | Some codom -> S.get_recovery_tactic codom e
-          | None -> Gillian.General.Recovery_tactic.none
+          | None -> Engine.General.Recovery_tactic.none
         in
-        Gillian.General.Recovery_tactic.merge sub_recover
-          (Gillian.General.Recovery_tactic.try_unfold [ idx ])
-    | InvalidIndexValue idx ->
-        Gillian.General.Recovery_tactic.try_unfold [ idx ]
+        Engine.General.Recovery_tactic.merge sub_recover
+          (Engine.General.Recovery_tactic.try_unfold [ idx ])
+    | InvalidIndexValue idx -> Engine.General.Recovery_tactic.try_unfold [ idx ]
 
   let can_fix = function
     | SubError (_, _, e) -> S.can_fix e

transformers/lib/states/PMap.mli → GillianCore/combinators/PMap.mli

@@ -1,5 +1,5 @@
 open Gil_syntax
-open Gillian.Monadic
+open Monadic
 
 type index_mode = Static | Dynamic
 
@@ -19,7 +19,7 @@ module type PMapImpl = sig
   val fold : (Expr.t -> Entry.t -> 'a -> 'a) -> t -> 'a -> 'a
   val for_all : (Entry.t -> bool) -> t -> bool
   val compose : t -> t -> t Delayed.t
-  val substitution_in_place : Gillian.Symbolic.Subst.t -> t -> t Delayed.t
+  val substitution_in_place : Engine.Symbolic.Subst.t -> t -> t Delayed.t
 end
 
 module type OpenPMapType = sig

transformers/lib/states/Product.ml → GillianCore/combinators/Product.ml

@@ -1,5 +1,5 @@
-open Gillian.Monadic
-module Containers = Gillian.Utils.Containers
+open Monadic
+module Containers = Utils.Containers
 open MyUtils
 
 module Make (IDs : IDs) (S1 : MyMonadicSMemory.S) (S2 : MyMonadicSMemory.S) :

transformers/lib/states/Sum.ml → GillianCore/combinators/Sum.ml

@@ -1,5 +1,5 @@
-open Gillian.Utils
-open Gillian.Monadic
+open Utils
+open Monadic
 open MyUtils
 module DR = Delayed_result
 

transformers/lib/states/bi_abd.ml → GillianCore/combinators/bi_abd.ml

@@ -1,4 +1,4 @@
-open Gillian.Monadic
+open Monadic
 module DR = Delayed_result
 
 type ('a, 'pred) bi_state = { state : 'a; anti_frame : 'pred Fix.t }
@@ -75,11 +75,11 @@ module Make (Mem : MyMonadicSMemory.S) :
   (* Variables *)
 
   let lvars s =
-    let open Gillian.Utils.Containers in
+    let open Utils.Containers in
     Mem.lvars s.state |> SS.union (Fix.lvars s.anti_frame)
 
   let alocs s =
-    let open Gillian.Utils.Containers in
+    let open Utils.Containers in
     Mem.alocs s.state |> SS.union (Fix.alocs s.anti_frame)
 
   let substitution_in_place subst s =

transformers/lib/states/cmemory.ml → GillianCore/combinators/cmemory.ml

@@ -1,8 +1,8 @@
-open Gillian.Concrete
-module Expr = Gillian.Gil_syntax.Expr
+open Engine.Concrete
+module Expr = Gil_syntax.Expr
 
-module Make (InitData : Gillian.General.Init_data.S) :
-  Gillian.Concrete.Memory_S with type init_data = InitData.t = struct
+module Make (InitData : Engine.General.Init_data.S) :
+  Engine.Concrete.Memory_S with type init_data = InitData.t = struct
   type vt = Values.t
   type st = Subst.t
   type err_t = unit [@@deriving yojson, show]

GillianCore/combinators/cmemory.mli

@@ -0,0 +1,2 @@
+module Make (ID : Engine.General.Init_data.S) :
+  Engine.Concrete.Memory_S with type init_data = ID.t

GillianCore/combinators/dune

@@ -0,0 +1,14 @@
+(library
+ (name combinators)
+ (public_name gillian.combinators)
+ (libraries
+  engine
+  monadic
+  utils
+  gil_syntax
+  ppx_sat_runtime
+  ppx_deriving_yojson.runtime)
+ (preprocess
+  (pps ppx_deriving.show ppx_deriving_yojson gillian.ppx_sat))
+ (instrumentation
+  (backend landmarks --auto)))

GillianCore/command_line/dune

@@ -8,6 +8,8 @@
   utils
   usage_logs
   engine
+  verify
+  biabduction
   bulk
   logging
   debugger_lifter
@@ -27,6 +29,10 @@
   -open
   Engine
   -open
+  Verify
+  -open
+  Biabduction
+  -open
   Bulk
   -open
   IncrementalAnalysis))

GillianCore/debugging/debugger/dune

@@ -7,6 +7,7 @@
   str
   fmt.tty
   engine
+  verify
   sedap.types
   gil_syntax
   incrementalAnalysis
@@ -28,6 +29,8 @@
   -open
   Engine
   -open
+  Verify
+  -open
   Gil_syntax
   -open
   IncrementalAnalysis

GillianCore/debugging/lifter/dune

@@ -9,6 +9,7 @@
   sedap.types
   debugger_log
   debugger_utils
+  verify
   parserAndCompiler)
  (flags
   :standard
@@ -19,6 +20,8 @@
   -open
   Engine
   -open
+  Verify
+  -open
   Utils
   -open
   Utils.Prelude))