[sledge] Extract relational logic from Sh_domain, create "domain" module

Summary:
Generalize the lifting from State_domain (i.e. symbolic heaps) to Sh_domain (i.e. relations over symbolic heaps).
Also, extract abstract-domain-related code into its own module/directory.

Reviewed By: jberdine

Differential Revision: D17319007

fbshipit-source-id: cefbd1393

sledge/.gitignore

@@ -8,6 +8,7 @@
 /src/llair/dune
 /src/symbheap/dune
 /src/trace/dune
+/src/domain/dune
 /src/version.ml
 /test/*/*.bc
 /test/*/*.bc.err

sledge/src/domain/domain_sig.ml

@@ -7,7 +7,7 @@
 
 (** Abstract Domain *)
 module type Dom = sig
-  type t
+  type t [@@deriving equal, sexp_of]
 
   val pp : t pp
   val report_fmt_thunk : t -> Formatter.t -> unit

sledge/src/domain/dune.in

@@ -0,0 +1,20 @@
+(* -*- tuareg -*- *)
+(*
+ * 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.
+ *)
+
+let deps = ["import"; "llair_"]
+
+;;
+Jbuild_plugin.V1.send
+@@ Format.sprintf {|
+(library
+ (name domain)
+ %s
+ (libraries %s))
+|}
+     (flags `lib deps)
+     (libraries deps)

sledge/src/domain/relation.ml

@@ -0,0 +1,128 @@
+(*
+ * 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.
+ *)
+
+(** Relational abstract domain, elements of which are interpreted as Hoare
+    triples over a base state domain *)
+
+module type State_domain_sig = sig
+  include Domain_sig.Dom
+
+  val create_summary :
+       locals:Var.Set.t
+    -> formals:Var.Set.t
+    -> entry:t
+    -> current:t
+    -> summary * t
+end
+
+module Make (State_domain : State_domain_sig) = struct
+  type t = State_domain.t * State_domain.t [@@deriving sexp_of, equal]
+
+  let embed b = (b, b)
+
+  let pp fs (entry, curr) =
+    Format.fprintf fs "@[<v 1> entry: %a@;current:%a@]" State_domain.pp
+      entry State_domain.pp curr
+
+  let report_fmt_thunk (_, curr) fs = State_domain.pp fs curr
+  let init globals = embed (State_domain.init globals)
+
+  let join (entry_a, current_a) (entry_b, current_b) =
+    assert (State_domain.equal entry_b entry_a) ;
+    (entry_a, State_domain.join current_a current_b)
+
+  let is_false (_, curr) = State_domain.is_false curr
+
+  let exec_assume (entry, current) cnd =
+    match State_domain.exec_assume current cnd with
+    | Some current -> Some (entry, current)
+    | None -> None
+
+  let exec_kill (entry, current) reg =
+    (entry, State_domain.exec_kill current reg)
+
+  let exec_move (entry, current) formal actual =
+    (entry, State_domain.exec_move current formal actual)
+
+  let exec_inst (entry, current) inst =
+    match State_domain.exec_inst current inst with
+    | Ok current -> Ok (entry, current)
+    | Error e -> Error e
+
+  let exec_intrinsic ~skip_throw (entry, current) areturn intrinsic actuals
+      =
+    match
+      State_domain.exec_intrinsic ~skip_throw current areturn intrinsic
+        actuals
+    with
+    | None -> None
+    | Some (Ok current) -> Some (Ok (entry, current))
+    | Some (Error e) -> Some (Error e)
+
+  type from_call =
+    {state_from_call: State_domain.from_call; caller_entry: State_domain.t}
+  [@@deriving sexp_of]
+
+  let call ~summaries actuals areturn formals locals globals_vec
+      (entry, current) =
+    let globals =
+      Var.Set.of_vector
+        (Vector.map globals_vec ~f:(fun (g : Global.t) -> g.var))
+    in
+    ([%Trace.call fun {pf} ->
+       pf
+         "@[<v>@[actuals: (@[%a@])@ formals: (@[%a@])@]@ locals: {@[%a@]}@ \
+          globals: {@[%a@]}@ current: %a@]"
+         (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp)
+         (List.rev formals) Var.Set.pp locals Var.Set.pp globals
+         State_domain.pp current]
+    ;
+    let caller_current, state_from_call =
+      State_domain.call ~summaries actuals areturn formals locals
+        globals_vec current
+    in
+    ( (caller_current, caller_current)
+    , {state_from_call; caller_entry= entry} ))
+    |>
+    [%Trace.retn fun {pf} (reln, _) -> pf "@,%a" pp reln]
+
+  let post locals {state_from_call; caller_entry} (_, current) =
+    [%Trace.call fun {pf} -> pf "locals: %a" Var.Set.pp locals]
+    ;
+    (caller_entry, State_domain.post locals state_from_call current)
+    |>
+    [%Trace.retn fun {pf} -> pf "@,%a" pp]
+
+  let retn formals freturn {caller_entry; state_from_call} (_, current) =
+    [%Trace.call fun {pf} -> pf "@,%a" State_domain.pp current]
+    ;
+    (caller_entry, State_domain.retn formals freturn state_from_call current)
+    |>
+    [%Trace.retn fun {pf} -> pf "@,%a" pp]
+
+  let dnf (entry, current) =
+    List.map ~f:(fun c -> (entry, c)) (State_domain.dnf current)
+
+  let resolve_callee f e (_, current) =
+    State_domain.resolve_callee f e current
+
+  type summary = State_domain.summary
+
+  let pp_summary = State_domain.pp_summary
+
+  let create_summary ~locals ~formals (entry, current) =
+    let fs, current =
+      State_domain.create_summary ~locals ~formals ~entry ~current
+    in
+    (fs, (entry, current))
+
+  let apply_summary rel summ =
+    let entry, current = rel in
+    Option.map
+      ~f:(fun c -> (entry, c))
+      (State_domain.apply_summary current summ)
+end

sledge/src/domain/relation.mli

@@ -0,0 +1,22 @@
+(*
+ * 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.
+ *)
+
+(** Relational abstract domain, elements of which are interpreted as Hoare
+    triples over a base domain *)
+
+module type State_domain_sig = sig
+  include Domain_sig.Dom
+
+  val create_summary :
+       locals:Var.Set.t
+    -> formals:Var.Set.t
+    -> entry:t
+    -> current:t
+    -> summary * t
+end
+
+module Make (State_domain : State_domain_sig) : Domain_sig.Dom

sledge/src/domain/unit.ml

@@ -7,7 +7,7 @@
 
 (** "Unit" abstract domain *)
 
-type t = unit
+type t = unit [@@deriving equal, sexp_of]
 
 let pp fs () = Format.pp_print_string fs "()"
 let report_fmt_thunk () fs = pp fs ()

sledge/src/dune.in

@@ -6,7 +6,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-let deps = ["import"; "llair_"; "symbheap"; "config"]
+let deps = ["import"; "llair_"; "symbheap"; "config"; "domain"]
 
 ;;
 Jbuild_plugin.V1.send

sledge/src/sledge.ml

@@ -13,8 +13,8 @@ open Command.Let_syntax
 
 type 'a param = 'a Command.Param.t
 
-module Sh_executor = Control.Make (Sh_domain)
+module Sh_executor = Control.Make (Domain.Relation.Make (State_domain))
-module Unit_executor = Control.Make (Unit_domain)
+module Unit_executor = Control.Make (Domain.Unit)
 
 (* reverse application in the Command.Param applicative *)
 let ( |*> ) : 'a param -> ('a -> 'b) param -> 'b param =

sledge/src/symbheap/dune.in

@@ -6,7 +6,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-let deps = ["import"; "llair_"]
+let deps = ["import"; "llair_"; "domain"]
 
 ;;
 Jbuild_plugin.V1.send

sledge/src/symbheap/sh_domain.ml

@@ -1,111 +0,0 @@
-(*
- * 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.
- *)
-
-(** Abstract domain *)
-
-type t = State_domain.t * State_domain.t
-
-let embed q = (q, q)
-
-let pp fs (entry, current) =
-  Format.fprintf fs "@[<v 1> entry: %a@;current: %a@]" State_domain.pp entry
-    State_domain.pp current
-
-let report_fmt_thunk (_, curr) fs = State_domain.pp fs curr
-let init globals = embed (State_domain.init globals)
-
-let join (entry_a, current_a) (entry_b, current_b) =
-  assert (State_domain.equal entry_b entry_a) ;
-  (entry_a, State_domain.join current_a current_b)
-
-let is_false (_, curr) = State_domain.is_false curr
-
-let exec_assume (entry, current) cnd =
-  match State_domain.exec_assume current cnd with
-  | Some current -> Some (entry, current)
-  | None -> None
-
-let exec_kill (entry, current) reg =
-  (entry, State_domain.exec_kill current reg)
-
-let exec_move (entry, current) formal actual =
-  (entry, State_domain.exec_move current formal actual)
-
-let exec_inst (entry, current) inst =
-  match State_domain.exec_inst current inst with
-  | Ok current -> Ok (entry, current)
-  | Error e -> Error e
-
-let exec_intrinsic ~skip_throw (entry, current) areturn intrinsic actuals =
-  match
-    State_domain.exec_intrinsic ~skip_throw current areturn intrinsic
-      actuals
-  with
-  | None -> None
-  | Some (Ok current) -> Some (Ok (entry, current))
-  | Some (Error e) -> Some (Error e)
-
-type from_call =
-  {state_from_call: State_domain.from_call; caller_entry: State_domain.t}
-[@@deriving sexp_of]
-
-let call ~summaries actuals areturn formals locals globals_vec
-    (entry, current) =
-  let globals =
-    Var.Set.of_vector
-      (Vector.map globals_vec ~f:(fun (g : Global.t) -> g.var))
-  in
-  ([%Trace.call fun {pf} ->
-     pf
-       "@[<v>@[actuals: (@[%a@])@ formals: (@[%a@])@]@ locals: {@[%a@]}@ \
-        globals: {@[%a@]}@ current: %a@]"
-       (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp)
-       (List.rev formals) Var.Set.pp locals Var.Set.pp globals
-       State_domain.pp current]
-  ;
-  let caller_current, state_from_call =
-    State_domain.call ~summaries actuals areturn formals locals globals
-      current
-  in
-  ((caller_current, caller_current), {state_from_call; caller_entry= entry}))
-  |>
-  [%Trace.retn fun {pf} (reln, _) -> pf "@,%a" pp reln]
-
-let post locals {caller_entry} (_, current) =
-  [%Trace.call fun {pf} -> pf "locals: %a" Var.Set.pp locals]
-  ;
-  (caller_entry, State_domain.post locals current)
-  |>
-  [%Trace.retn fun {pf} -> pf "@,%a" pp]
-
-let retn formals freturn {caller_entry; state_from_call} (_, current) =
-  [%Trace.call fun {pf} -> pf "@,%a" State_domain.pp current]
-  ;
-  (caller_entry, State_domain.retn formals freturn state_from_call current)
-  |>
-  [%Trace.retn fun {pf} -> pf "@,%a" pp]
-
-let dnf (entry, current) =
-  List.map ~f:(fun c -> (entry, c)) (State_domain.dnf current)
-
-let resolve_callee f e (_, current) =
-  State_domain.resolve_callee f e current
-
-type summary = State_domain.summary
-
-let pp_summary = State_domain.pp_summary
-
-let create_summary ~locals ~formals (entry, current) =
-  let fs, current =
-    State_domain.create_summary ~locals ~formals ~entry ~current
-  in
-  (fs, (entry, current))
-
-let apply_summary (entry, current) fs =
-  Option.map
-    ~f:(fun c -> (entry, c))
-    (State_domain.apply_summary fs current)

sledge/src/symbheap/sh_domain.mli

@@ -1,57 +0,0 @@
-(*
- * 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.
- *)
-
-(** Abstract domain *)
-
-type t
-
-val pp : t pp
-val report_fmt_thunk : t -> Formatter.t -> unit
-val init : Global.t vector -> t
-val join : t -> t -> t
-val is_false : t -> bool
-val exec_assume : t -> Exp.t -> t option
-val exec_kill : t -> Var.t -> t
-val exec_move : t -> Var.t -> Exp.t -> t
-val exec_inst : t -> Llair.inst -> (t, unit) result
-
-val exec_intrinsic :
-     skip_throw:bool
-  -> t
-  -> Var.t option
-  -> Var.t
-  -> Exp.t list
-  -> (t, unit) result option
-
-type from_call [@@deriving sexp_of]
-type summary
-
-val pp_summary : summary pp
-
-(* formals should include all the parameters of the summary. That is both
-   formals and globals.*)
-val create_summary :
-  locals:Var.Set.t -> formals:Var.Set.t -> t -> summary * t
-
-val apply_summary : t -> summary -> t option
-
-val call :
-     summaries:bool
-  -> Exp.t list
-  -> Var.t option
-  -> Var.t list
-  -> Var.Set.t
-  -> Global.t vector
-  -> t
-  -> t * from_call
-
-val post : Var.Set.t -> from_call -> t -> t
-val retn : Var.t list -> Var.t option -> from_call -> t -> t
-val dnf : t -> t list
-
-val resolve_callee :
-  (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list

sledge/src/symbheap/state_domain.ml

@@ -15,6 +15,7 @@ let pp_simp fs q =
   Sh.pp fs !q'
 
 let pp = pp_simp
+let report_fmt_thunk = Fn.flip pp
 
 let init globals =
   Vector.fold globals ~init:Sh.emp ~f:(fun q -> function
@@ -73,7 +74,7 @@ type from_call = {areturn: Var.t option; subst: Var.Subst.t; frame: Sh.t}
 (** Express formula in terms of formals instead of actuals, and enter scope
     of locals: rename formals to fresh vars in formula and actuals, add
     equations between each formal and actual, and quantify fresh vars. *)
-let call ~summaries actuals areturn formals locals globals q =
+let call ~summaries actuals areturn formals locals globals_vec q =
   [%Trace.call fun {pf} ->
     pf
       "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ q: %a@]"
@@ -95,9 +96,13 @@ let call ~summaries actuals areturn formals locals globals q =
     let q'' = Sh.extend_us locals q'' in
     (q'', {areturn; subst= freshen_locals; frame= Sh.emp})
   else
-    let formals_set = Var.Set.of_list formals in
     (* Add the formals here to do garbage collection and then get rid of
        them *)
+    let formals_set = Var.Set.of_list formals
+    and globals =
+      Var.Set.of_vector
+        (Vector.map globals_vec ~f:(fun (g : Global.t) -> g.var))
+    in
     let function_summary_pre =
       garbage_collect q'' ~wrt:(Set.union formals_set globals)
     in
@@ -118,7 +123,7 @@ let call ~summaries actuals areturn formals locals globals q =
       q']
 
 (** Leave scope of locals: existentially quantify locals. *)
-let post locals q =
+let post locals _ q =
   [%Trace.call fun {pf} ->
     pf "@[<hv>locals: {@[%a@]}@ q: %a@]" Var.Set.pp locals Sh.pp q]
   ;
@@ -186,7 +191,7 @@ let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
   |>
   [%Trace.retn fun {pf} (fs, _) -> pf "@,%a" pp_summary fs]
 
-let apply_summary ({xs; foot; post} as fs) q =
+let apply_summary q ({xs; foot; post} as fs) =
   [%Trace.call fun {pf} -> pf "fs: %a@ q: %a" pp_summary fs pp q]
   ;
   let xs_in_q = Set.inter xs q.Sh.us in

sledge/src/symbheap/state_domain.mli

@@ -7,41 +7,7 @@
 
 (** Abstract domain *)
 
-type t [@@deriving equal, sexp_of]
+include Domain_sig.Dom
-
-val pp : t pp
-val init : Global.t vector -> t
-val join : t -> t -> t
-val is_false : t -> bool
-val exec_assume : t -> Exp.t -> t option
-val exec_kill : t -> Var.t -> t
-val exec_move : t -> Var.t -> Exp.t -> t
-val exec_inst : t -> Llair.inst -> (t, unit) result
-
-val exec_intrinsic :
-     skip_throw:bool
-  -> t
-  -> Var.t option
-  -> Var.t
-  -> Exp.t list
-  -> (t, unit) result option
-
-type from_call [@@deriving compare, equal, sexp]
-
-val call :
-     summaries:bool
-  -> Exp.t list
-  -> Var.t option
-  -> Var.t list
-  -> Var.Set.t
-  -> Var.Set.t
-  -> t
-  -> t * from_call
-
-type summary = {xs: Var.Set.t; foot: t; post: t}
-
-val pp_summary : summary pp
-val apply_summary : summary -> t -> t option
 
 (* formals should include all the parameters of the summary. That is both
    formals and globals.*)
@@ -51,10 +17,3 @@ val create_summary :
   -> entry:t
   -> current:t
   -> summary * t
-
-val post : Var.Set.t -> t -> t
-val retn : Var.t list -> Var.t option -> from_call -> t -> t
-val dnf : t -> t list
-
-val resolve_callee :
-  (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list