[sledge] Add abstract domain interface

Reviewed By: mbouaziz

Differential Revision: D9846739

fbshipit-source-id: 56b4d63de

sledge/src/symbheap/domain.ml

@@ -0,0 +1,69 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * 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 = Sh.t
+
+let pp = Sh.pp
+
+let init globals =
+  Vector.fold globals ~init:Sh.emp ~f:(fun q -> function
+    | {Global.var; init= Some arr; siz} ->
+        let loc = Exp.var var in
+        let len = Exp.integer (Z.of_int siz) in
+        Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr})
+    | _ -> q )
+
+let bottom = Sh.false_ Var.Set.empty
+let join = Sh.or_
+let assume q b = Exec.assume b q
+let exec_inst = Exec.inst
+
+type from_call = Var.Subst.t [@@deriving compare, sexp]
+
+(** 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 the fresh vars. *)
+let call q actuals formals locals =
+  [%Trace.call fun {pf} ->
+    pf
+      "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ q: %a@]"
+      (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp)
+      (List.rev formals) Var.Set.pp locals Sh.pp q]
+  ;
+  let q', freshen_locals = Sh.freshen q ~wrt:locals in
+  let and_eq q formal actual =
+    let actual' = Exp.rename actual freshen_locals in
+    Sh.and_ (Exp.eq (Exp.var formal) actual') q
+  in
+  let and_eqs formals actuals q =
+    List.fold2_exn ~f:and_eq formals actuals ~init:q
+  in
+  (Sh.extend_us locals (and_eqs formals actuals q'), freshen_locals)
+  |>
+  [%Trace.retn fun {pf} (q', s) ->
+    pf "@[<hv>subst: %a@ q': %a@]" Var.Subst.pp s Sh.pp q']
+
+(** Leave scope of locals and express in terms of actuals instead of
+    formals: existentially quantify locals and formals, and apply inverse of
+    fresh variables for formals renaming to restore the shadowed variables. *)
+let retn locals freshen_locals q =
+  [%Trace.call fun {pf} ->
+    pf "@[<hv>locals: {@[%a@]}@ subst: %a@ q: %a@]" Var.Set.pp locals
+      Var.Subst.pp
+      (Var.Subst.invert freshen_locals)
+      Sh.pp q]
+  ;
+  Sh.rename (Var.Subst.invert freshen_locals) (Sh.exists locals q)
+  |>
+  [%Trace.retn fun {pf} -> pf "%a" Sh.pp]
+
+let resolve_callee lookup ptr _ =
+  match Var.of_exp ptr with
+  | Some callee_name -> lookup callee_name
+  | None -> []

sledge/src/symbheap/domain.mli

@@ -0,0 +1,25 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * 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 init : Global.t vector -> t
+val bottom : t
+val join : t -> t -> t
+val assume : t -> Exp.t -> t option
+val exec_inst : t -> Llair.inst -> (t, t * Llair.inst) result
+
+type from_call [@@deriving compare, sexp]
+
+val call : t -> Exp.t list -> Var.t list -> Var.Set.t -> t * from_call
+val retn : Var.Set.t -> from_call -> t -> t
+
+val resolve_callee :
+  (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list