[sledge] Build: Move sledge equality solver to separate lib

Reviewed By: ngorogiannis

Differential Revision: D22170508

fbshipit-source-id: 1e9cf4a79

infer/src/pulse/PulseDummySledge.ml

@@ -37,14 +37,14 @@ module Term = struct
 end
 
 (* same type as {!PulsePathCondition.t} to be nice to summary serialization *)
-type t = {eqs: Sledge.Equality.t lazy_t; non_eqs: Sledge.Term.t lazy_t}
+type t = {eqs: Ses.Equality.t lazy_t; non_eqs: Ses.Term.t lazy_t}
 
 (* still print to make sure the formula never changes in debug *)
 let pp fmt {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} =
-  F.fprintf fmt "%a∧%a" Sledge.Equality.pp eqs Sledge.Term.pp non_eqs
+  F.fprintf fmt "%a∧%a" Ses.Equality.pp eqs Ses.Term.pp non_eqs
 
 
-let true_ = {eqs= Lazy.from_val Sledge.Equality.true_; non_eqs= Lazy.from_val Sledge.Term.true_}
+let true_ = {eqs= Lazy.from_val Ses.Equality.true_; non_eqs= Lazy.from_val Ses.Term.true_}
 
 let and_eq () () phi = phi
 

infer/src/pulse/PulseSledge.ml

@@ -13,7 +13,7 @@ module AbstractValue = PulseAbstractValue
 [@@@warning "+9"]
 
 module Var = struct
-  module Var = Sledge.Var
+  module Var = Ses.Var
 
   let of_absval (v : AbstractValue.t) = Var.identified ~name:"v" ~id:(v :> int)
 
@@ -26,7 +26,7 @@ module Var = struct
 end
 
 module Term = struct
-  module Term = Sledge.Term
+  module Term = Ses.Term
 
   let of_intlit i = Term.integer (IntLit.to_big_int i)
 
@@ -75,7 +75,7 @@ module Term = struct
 end
 
 module Equality = struct
-  include Sledge.Equality
+  include Ses.Equality
 
   let assert_no_new_vars api new_vars =
     if not (Var.Set.is_empty new_vars) then
@@ -83,25 +83,25 @@ module Equality = struct
 
 
   let and_eq t1 t2 r =
-    let new_vars, r' = Sledge.Equality.and_eq Var.Set.empty t1 t2 r in
+    let new_vars, r' = Ses.Equality.and_eq Var.Set.empty t1 t2 r in
     assert_no_new_vars "Equality.and_eq" new_vars ;
     r'
 
 
   let and_term t r =
-    let new_vars, r' = Sledge.Equality.and_term Var.Set.empty t r in
+    let new_vars, r' = Ses.Equality.and_term Var.Set.empty t r in
     assert_no_new_vars "Equality.and_term" new_vars ;
     r'
 
 
   let and_ r1 r2 =
-    let new_vars, r' = Sledge.Equality.and_ Var.Set.empty r1 r2 in
+    let new_vars, r' = Ses.Equality.and_ Var.Set.empty r1 r2 in
     assert_no_new_vars "Equality.and_" new_vars ;
     r'
 
 
   let apply_subst subst r =
-    let new_vars, r' = Sledge.Equality.apply_subst Var.Set.empty subst r in
+    let new_vars, r' = Ses.Equality.apply_subst Var.Set.empty subst r in
     assert_no_new_vars "Equality.apply_subst" new_vars ;
     r'
 end

sledge/bin/domain_itv.ml

@@ -7,6 +7,7 @@
 
 (** Interval abstract domain *)
 
+open Ses
 open Apron
 
 let equal_apron_typ =

sledge/dune

@@ -45,12 +45,24 @@
    (pps ppx_sledge ppx_trace))
   (inline_tests)))
 
+(subdir
+ src/ses
+ (library
+  (name ses)
+  (public_name sledge.ses)
+  (libraries nonstdlib llair)
+  (flags
+   (:standard -open NS))
+  (preprocess
+   (pps ppx_sledge ppx_trace))
+  (inline_tests)))
+
 (subdir
  src
  (library
   (name sledge)
   (public_name sledge)
-  (libraries nonstdlib llair)
+  (libraries nonstdlib llair ses)
   (flags
    (:standard -open NS))
   (preprocess

sledge/src/domain_sh.ml

@@ -7,6 +7,8 @@
 
 (** Abstract domain *)
 
+open Ses
+
 type t = Sh.t [@@deriving equal, sexp]
 
 let pp fs q = Format.fprintf fs "@[{ %a@ }@]" Sh.pp q

sledge/src/exec.ml

@@ -7,6 +7,8 @@
 
 (** Symbolic Execution *)
 
+open Ses
+
 [@@@warning "+9"]
 
 module Fresh : sig

sledge/src/exec.mli

@@ -7,6 +7,8 @@
 
 (** Symbolic Execution *)
 
+open Ses
+
 val assume : Sh.t -> Term.t -> Sh.t option
 val kill : Sh.t -> Var.t -> Sh.t
 val move : Sh.t -> (Var.t * Term.t) iarray -> Sh.t

sledge/src/sh.ml

@@ -7,6 +7,8 @@
 
 (** Symbolic Heap Formulas *)
 
+open Ses
+
 [@@@warning "+9"]
 
 type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t}

sledge/src/sh.mli

@@ -7,6 +7,8 @@
 
 (** Symbolic Heap Formulas *)
 
+open Ses
+
 (** Segment of memory starting at [loc] containing [seq] (a byte-array) of
     size [siz], contained in an enclosing allocation-block starting at [bas]
     of length [len]. *)

sledge/src/sh_test.ml

@@ -5,6 +5,8 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
+open Ses
+
 let%test_module _ =
   ( module struct
     open Sh

sledge/src/solver.ml

@@ -7,6 +7,8 @@
 
 (** Frame Inference Solver over Symbolic Heaps *)
 
+open Ses
+
 module Goal : sig
   (** Excision judgment
 

sledge/src/solver.mli

@@ -7,6 +7,8 @@
 
 (** Frame Inference Solver over Symbolic Heaps *)
 
+open Ses
+
 val infer_frame : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option
 (** If [infer_frame p xs q] is [Some r], then [p ⊢ ∃xs. q * r]. The
     vocabulary of [r] is the vocabulary of [q] union [xs]. A goal is for [r]

sledge/src/solver_test.ml

@@ -5,6 +5,8 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
+open Ses
+
 let%test_module _ =
   ( module struct
     let () =