From dd2e7b47821fc6b82bf756d65b21cffe710e958b Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 9 Jul 2020 07:43:26 -0700 Subject: [PATCH] [sledge] Refactor: Add Fol module to be used for external interface of solver Reviewed By: ngorogiannis Differential Revision: D22170509 fbshipit-source-id: f4ed2bfee --- sledge/src/domain_sh.ml | 2 +- sledge/src/exec.ml | 2 +- sledge/src/exec.mli | 2 +- sledge/src/fol.ml | 10 ++++++++++ sledge/src/fol.mli | 10 ++++++++++ sledge/src/sh.ml | 2 +- sledge/src/sh.mli | 2 +- sledge/src/sh_test.ml | 2 +- sledge/src/solver.ml | 2 +- sledge/src/solver.mli | 2 +- sledge/src/solver_test.ml | 2 +- 11 files changed, 29 insertions(+), 9 deletions(-) create mode 100644 sledge/src/fol.ml create mode 100644 sledge/src/fol.mli diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index 0cf0574c4..9199a2457 100644 --- a/sledge/src/domain_sh.ml +++ b/sledge/src/domain_sh.ml @@ -7,7 +7,7 @@ (** Abstract domain *) -open Ses +open Fol type t = Sh.t [@@deriving equal, sexp] diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml index 3c87e65ce..f98a95bd0 100644 --- a/sledge/src/exec.ml +++ b/sledge/src/exec.ml @@ -7,7 +7,7 @@ (** Symbolic Execution *) -open Ses +open Fol [@@@warning "+9"] diff --git a/sledge/src/exec.mli b/sledge/src/exec.mli index 5f70d5514..4fef881c4 100644 --- a/sledge/src/exec.mli +++ b/sledge/src/exec.mli @@ -7,7 +7,7 @@ (** Symbolic Execution *) -open Ses +open Fol val assume : Sh.t -> Term.t -> Sh.t option val kill : Sh.t -> Var.t -> Sh.t diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml new file mode 100644 index 000000000..815af7adf --- /dev/null +++ b/sledge/src/fol.ml @@ -0,0 +1,10 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +module Var = Ses.Var +module Term = Ses.Term +module Equality = Ses.Equality diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli new file mode 100644 index 000000000..815af7adf --- /dev/null +++ b/sledge/src/fol.mli @@ -0,0 +1,10 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +module Var = Ses.Var +module Term = Ses.Term +module Equality = Ses.Equality diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index 376dd244f..9db819adf 100644 --- a/sledge/src/sh.ml +++ b/sledge/src/sh.ml @@ -7,7 +7,7 @@ (** Symbolic Heap Formulas *) -open Ses +open Fol [@@@warning "+9"] diff --git a/sledge/src/sh.mli b/sledge/src/sh.mli index 50d8fd946..8595ec8d0 100644 --- a/sledge/src/sh.mli +++ b/sledge/src/sh.mli @@ -7,7 +7,7 @@ (** Symbolic Heap Formulas *) -open Ses +open Fol (** Segment of memory starting at [loc] containing [seq] (a byte-array) of size [siz], contained in an enclosing allocation-block starting at [bas] diff --git a/sledge/src/sh_test.ml b/sledge/src/sh_test.ml index a13068de9..8e4185e17 100644 --- a/sledge/src/sh_test.ml +++ b/sledge/src/sh_test.ml @@ -5,7 +5,7 @@ * LICENSE file in the root directory of this source tree. *) -open Ses +open Fol let%test_module _ = ( module struct diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml index f12a70735..fd7fb2ba9 100644 --- a/sledge/src/solver.ml +++ b/sledge/src/solver.ml @@ -7,7 +7,7 @@ (** Frame Inference Solver over Symbolic Heaps *) -open Ses +open Fol module Goal : sig (** Excision judgment diff --git a/sledge/src/solver.mli b/sledge/src/solver.mli index c4e1600de..ae6ae86ca 100644 --- a/sledge/src/solver.mli +++ b/sledge/src/solver.mli @@ -7,7 +7,7 @@ (** Frame Inference Solver over Symbolic Heaps *) -open Ses +open Fol 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 diff --git a/sledge/src/solver_test.ml b/sledge/src/solver_test.ml index 85306c4fd..db520f393 100644 --- a/sledge/src/solver_test.ml +++ b/sledge/src/solver_test.ml @@ -5,7 +5,7 @@ * LICENSE file in the root directory of this source tree. *) -open Ses +open Fol let%test_module _ = ( module struct