From 0ab1223d3d725518474478a4c92ba43232b00286 Mon Sep 17 00:00:00 2001
From: Timotej Kapus <kapust@fb.com>
Date: Thu, 27 Jun 2019 09:30:08 -0700
Subject: [PATCH] [sledge] Function summarization: solver can show pre

Summary:
This diff is preparation for function summarization and focuses on
function calls and function summary precondition computation.

It introduces `-function-summaries` flag behind most of functionality is
hidden, when enabled on each call

* A function summary is computed by quantifying all the non-formal/global variables
  and removing all the segments that are not reachable from them
* `pre` and `foot` are computed from function summary and the calling context
  by replacing formals with actuals again.
* A solver is asked if `pre` entails `foot` and a frame is printed if it
  does

Currently this only works for formulas without disjunctions, so when
function summaries are enabled, that state is first moved to dnf and then
the call is done for each disjunct.

Reviewed By: ngorogiannis

Differential Revision: D15898928

fbshipit-source-id: 49d32504c
---
 sledge/src/control.ml                |  40 +++++---
 sledge/src/control.mli               |   3 +-
 sledge/src/sledge.ml                 |   6 +-
 sledge/src/sledge_buck.ml            |   4 +-
 sledge/src/symbheap/domain.ml        |  28 +++--
 sledge/src/symbheap/domain.mli       |  12 ++-
 sledge/src/symbheap/equality.ml      |  17 ++--
 sledge/src/symbheap/equality.mli     |   7 +-
 sledge/src/symbheap/equality_test.ml |  12 +++
 sledge/src/symbheap/sh.ml            |   3 +
 sledge/src/symbheap/sh.mli           |   3 +
 sledge/src/symbheap/state_domain.ml  | 147 +++++++++++++++++++++++++--
 sledge/src/symbheap/state_domain.mli |   9 +-
 13 files changed, 246 insertions(+), 45 deletions(-)

diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 43356788a..aa7b7a9d2 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -9,7 +9,7 @@
 
     The analysis' semantics of control flow. *)
 
-type exec_opts = {bound: int; skip_throw: bool}
+type exec_opts = {bound: int; skip_throw: bool; function_summaries: bool}
 
 module Stack : sig
   type t
@@ -254,19 +254,27 @@ let exec_jump ?temps stk state block ({dst; args} as jmp : Llair.jump) =
   exec_goto stk state block jmp
 
 let exec_call ~opts stk state block ({dst; args; retreating} : Llair.jump)
-    (return : Llair.jump) throw =
+    (return : Llair.jump) throw globals =
   [%Trace.call fun {pf} ->
     pf "%a from %a" Var.pp dst.parent.name.var Var.pp
       return.dst.parent.name.var]
   ;
-  let locals = dst.parent.locals in
-  let state, from_call = Domain.call args dst.params locals state in
-  ( match
-      Stack.push_call ~bound:opts.bound dst ~retreating ~return from_call
-        ?throw stk
-    with
-  | Some stk -> Work.add stk ~prev:block ~retreating state dst
-  | None -> Work.skip )
+  let dnf_states =
+    if opts.function_summaries then Domain.dnf state else [state]
+  in
+  List.fold ~init:Work.skip dnf_states ~f:(fun acc state ->
+      let locals = dst.parent.locals in
+      let state, from_call =
+        Domain.call ~summaries:opts.function_summaries args dst.params
+          locals globals state
+      in
+      Work.seq acc
+        ( match
+            Stack.push_call ~bound:opts.bound dst ~retreating ~return
+              from_call ?throw stk
+          with
+        | Some stk -> Work.add stk ~prev:block ~retreating state dst
+        | None -> Work.skip ) )
   |>
   [%Trace.retn fun {pf} _ -> pf ""]
 
@@ -395,7 +403,7 @@ let exec_term :
             | None ->
                 exec_call ~opts stk state block
                   {dst= callee.entry; args; retreating}
-                  return throw )
+                  return throw pgm.globals )
             |> Work.seq x ) )
   | Return {exp} -> exec_return stk state block exp
   | Throw {exc} ->
@@ -423,8 +431,8 @@ let exec_block :
       Report.invalid_access_inst state inst ;
       Work.skip
 
-let harness : Llair.t -> (int -> Work.t) option =
- fun pgm ->
+let harness : opts:exec_opts -> Llair.t -> (int -> Work.t) option =
+ fun ~opts pgm ->
   let entry_points = Config.find_list "entry-points" in
   List.find_map entry_points ~f:(fun name ->
       Llair.Func.find pgm.functions (Var.program name) )
@@ -432,7 +440,9 @@ let harness : Llair.t -> (int -> Work.t) option =
   | Some {locals; entry= {params= []} as block} ->
       Some
         (Work.init
-           (fst (Domain.call [] [] locals (Domain.init pgm.globals)))
+           (fst
+              (Domain.call ~summaries:opts.function_summaries [] [] locals
+                 pgm.globals (Domain.init pgm.globals)))
            block)
   | _ -> None
 
@@ -440,7 +450,7 @@ let exec_pgm : exec_opts -> Llair.t -> unit =
  fun opts pgm ->
   [%Trace.call fun {pf} -> pf "@]@,@["]
   ;
-  ( match harness pgm with
+  ( match harness ~opts pgm with
   | Some work -> Work.run ~f:(exec_block ~opts pgm) (work opts.bound)
   | None -> fail "no applicable harness" () )
   |>
diff --git a/sledge/src/control.mli b/sledge/src/control.mli
index 6edfc0b6f..95f3febf3 100644
--- a/sledge/src/control.mli
+++ b/sledge/src/control.mli
@@ -9,6 +9,7 @@
 
 type exec_opts =
   { bound: int  (** Loop/recursion unrolling bound *)
-  ; skip_throw: bool  (** Treat throw as unreachable *) }
+  ; skip_throw: bool  (** Treat throw as unreachable *)
+  ; function_summaries: bool  (** Use function summarisation *) }
 
 val exec_pgm : exec_opts -> Llair.t -> unit
diff --git a/sledge/src/sledge.ml b/sledge/src/sledge.ml
index a85d1df78..c76149707 100644
--- a/sledge/src/sledge.ml
+++ b/sledge/src/sledge.ml
@@ -66,8 +66,12 @@ let analyze =
   and skip_throw =
     flag "skip-throw" no_arg
       ~doc:"do not explore past throwing an exception"
+  and function_summaries =
+    flag "function-summaries" no_arg
+      ~doc:"Use function summaries (in development)"
   in
-  fun program () -> Control.exec_pgm {bound; skip_throw} (program ())
+  fun program () ->
+    Control.exec_pgm {bound; skip_throw; function_summaries} (program ())
 
 let analyze_cmd =
   let summary = "analyze LLAIR code" in
diff --git a/sledge/src/sledge_buck.ml b/sledge/src/sledge_buck.ml
index c19c08850..3ec2cff86 100644
--- a/sledge/src/sledge_buck.ml
+++ b/sledge/src/sledge_buck.ml
@@ -231,8 +231,8 @@ let main ~(command : unit Command.basic_command) ~analyze =
      //fully/qualified/build:target. The mechanism used to integrate with \
      buck uses the arguments passed to the linker, so the target must \
      specify a binary that will be linked, not for instance a library \
-     archive. Sledge passes the --config sledge.build=True flag to buck, which can \
-     be used to configure buck targets for sledge."
+     archive. Sledge passes the --config sledge.build=True flag to buck, \
+     which can be used to configure buck targets for sledge."
   in
   Command.group ~summary ~readme ~preserve_subcommand_order:()
     [("analyze", analyze_cmd); ("bitcode", bitcode_cmd); ("link", link_cmd)]
diff --git a/sledge/src/symbheap/domain.ml b/sledge/src/symbheap/domain.ml
index 20b1b10f2..1a53105e9 100644
--- a/sledge/src/symbheap/domain.ml
+++ b/sledge/src/symbheap/domain.ml
@@ -45,18 +45,27 @@ type from_call =
 [@@deriving sexp_of]
 
 let jump actuals formals ?temps (entry, current) =
-  let current, _ =
-    State_domain.call actuals formals Var.Set.empty ?temps current
-  in
+  let current, _ = State_domain.jump actuals formals ?temps current in
   (entry, current)
 
-let call actuals formals locals (_, current) =
-  [%Trace.call fun {pf} -> pf ""]
+let call ~summaries actuals formals locals globals_vec (_, 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 current, state_from_call =
-    State_domain.call actuals formals locals current
+  let caller_current, state_from_call =
+    State_domain.call ~summaries actuals formals locals globals current
   in
-  ((current, current), {state_from_call; caller_entry= current})
+  ( (caller_current, caller_current)
+  , {state_from_call; caller_entry= current} ))
   |>
   [%Trace.retn fun {pf} (reln, _) -> pf "@,%a" pp reln]
 
@@ -74,5 +83,8 @@ let retn formals {caller_entry; 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
diff --git a/sledge/src/symbheap/domain.mli b/sledge/src/symbheap/domain.mli
index bc4cf0e99..e7c48a83a 100644
--- a/sledge/src/symbheap/domain.mli
+++ b/sledge/src/symbheap/domain.mli
@@ -22,9 +22,19 @@ val exec_intrinsic :
 type from_call [@@deriving sexp_of]
 
 val jump : Exp.t list -> Var.t list -> ?temps:Var.Set.t -> t -> t
-val call : Exp.t list -> Var.t list -> Var.Set.t -> t -> t * from_call
+
+val call :
+     summaries:bool
+  -> Exp.t list
+  -> 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 -> from_call -> t -> t
+val dnf : t -> t list
 
 val resolve_callee :
   (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list
diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index 2ea07fbb9..6a00729fe 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -22,6 +22,11 @@ type t =
             'rep(resentative)' of [a] *) }
 [@@deriving compare, equal, sexp]
 
+let classes r =
+  Map.fold r.rep ~init:empty_map ~f:(fun ~key ~data cls ->
+      if Exp.equal key data then cls
+      else Map.add_multi cls ~key:data ~data:key )
+
 (** Pretty-printing *)
 
 let pp fs {sat; rep} =
@@ -37,16 +42,12 @@ let pp fs {sat; rep} =
     (Map.to_alist rep)
 
 let pp_classes fs r =
-  let cls =
-    Map.fold r.rep ~init:empty_map ~f:(fun ~key ~data cls ->
-        if Exp.equal key data then cls
-        else Map.add_multi cls ~key:data ~data:key )
-  in
   List.pp "@ @<2>∧ "
     (fun fs (key, data) ->
       Format.fprintf fs "@[%a@ = %a@]" Exp.pp key (List.pp "@ = " Exp.pp)
         (List.sort ~compare:Exp.compare data) )
-    fs (Map.to_alist cls)
+    fs
+    (Map.to_alist (classes r))
 
 let pp_diff fs (r, s) =
   let pp_sdiff_map pp_elt_diff equal nam fs x y =
@@ -220,6 +221,10 @@ let entails r s =
 
 let normalize = canon
 
+let class_of r e =
+  let e' = normalize r e in
+  e' :: Map.find_multi (classes r) e'
+
 let difference r a b =
   [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Exp.pp a Exp.pp b pp r]
   ;
diff --git a/sledge/src/symbheap/equality.mli b/sledge/src/symbheap/equality.mli
index 11e4d2072..cf80ea97b 100644
--- a/sledge/src/symbheap/equality.mli
+++ b/sledge/src/symbheap/equality.mli
@@ -45,11 +45,14 @@ val entails_eq : t -> Exp.t -> Exp.t -> bool
 val entails : t -> t -> bool
 (** Test if one relation entails another. *)
 
+val class_of : t -> Exp.t -> Exp.t list
+(** Equivalence class of [e]: all the expressions in [f] in the relation
+    such that [e = f] is implied by the relation. *)
+
 val normalize : t -> Exp.t -> Exp.t
 (** Normalize an exp [e] to [e'] such that [e = e'] is implied by the
     relation, where [e'] and its sub-exps are expressed in terms of the
-    relation's canonical representatives of each equivalence-modulo-offset
-    class. *)
+    relation's canonical representatives of each equivalence class. *)
 
 val difference : t -> Exp.t -> Exp.t -> Z.t option
 (** The difference as an offset. [difference r a b = Some k] if [r] implies
diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml
index cfa406116..e63fb626f 100644
--- a/sledge/src/symbheap/equality_test.ml
+++ b/sledge/src/symbheap/equality_test.ml
@@ -211,6 +211,18 @@ let%test_module _ =
 
       %v_3 = %w_4 = %x_5 = %y_6 = %z_7 |}]
 
+    let%expect_test _ =
+      printf (List.pp " , " Exp.pp) (Equality.class_of r7 t) ;
+      printf (List.pp " , " Exp.pp) (Equality.class_of r7 x) ;
+      printf (List.pp " , " Exp.pp) (Equality.class_of r7 z) ;
+      [%expect
+        {|
+        %t_1
+
+        %v_3 , %x_5
+
+        %w_4 , %z_7 , %y_6 |}]
+
     let r7' = and_eq x z r7
 
     let%expect_test _ =
diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml
index 7b1931bbb..3fae3dd4f 100644
--- a/sledge/src/symbheap/sh.ml
+++ b/sledge/src/symbheap/sh.ml
@@ -404,6 +404,9 @@ let with_pure pure q = {q with pure} |> check invariant
 let rem_seg seg q =
   {q with heap= List.remove_exn q.heap seg} |> check invariant
 
+let filter_heap ~f q =
+  {q with heap= List.filter q.heap ~f} |> check invariant
+
 (** Query *)
 
 let is_emp = function
diff --git a/sledge/src/symbheap/sh.mli b/sledge/src/symbheap/sh.mli
index da8b6ef9c..4a64cdcae 100644
--- a/sledge/src/symbheap/sh.mli
+++ b/sledge/src/symbheap/sh.mli
@@ -76,6 +76,9 @@ val rem_seg : seg -> t -> t
     (physically equal to) one of the elements of [q.heap]. Raises if [s] is
     not an element of [q.heap]. *)
 
+val filter_heap : f:(seg -> bool) -> t -> t
+(** [filter_heap q f] Remove all segments in [q] for which [f] returns false *)
+
 (** Quantification and Vocabulary *)
 
 val exists : Var.Set.t -> t -> t
diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml
index b609f8415..24c386048 100644
--- a/sledge/src/symbheap/state_domain.ml
+++ b/sledge/src/symbheap/state_domain.ml
@@ -26,6 +26,41 @@ let exec_assume = Exec.assume
 let exec_return = Exec.return
 let exec_inst = Exec.inst
 let exec_intrinsic = Exec.intrinsic
+let dnf = Sh.dnf
+
+let exp_eq_class_has_only_vars_in fvs cong exp =
+  [%Trace.call fun {pf} ->
+    pf "@[<v> fvs: @[%a@] @,cong: @[%a@] @,exp: @[%a@]@]" Var.Set.pp fvs
+      Equality.pp cong Exp.pp exp]
+  ;
+  let exp_has_only_vars_in fvs exp = Set.is_subset (Exp.fv exp) ~of_:fvs in
+  let exp_eq_class = Equality.class_of cong exp in
+  List.exists ~f:(exp_has_only_vars_in fvs) exp_eq_class
+  |>
+  [%Trace.retn fun {pf} -> pf "%b"]
+
+let garbage_collect (q : t) ~wrt =
+  [%Trace.call fun {pf} -> pf "%a" pp q]
+  ;
+  (* only support DNF for now *)
+  assert (List.is_empty q.djns) ;
+  let rec all_reachable_vars previous current (q : t) =
+    if previous == current then current
+    else
+      let new_set =
+        List.fold ~init:current q.heap ~f:(fun current seg ->
+            if exp_eq_class_has_only_vars_in current q.cong seg.loc then
+              List.fold (Equality.class_of q.cong seg.arr) ~init:current
+                ~f:(fun c e -> Set.union c (Exp.fv e))
+            else current )
+      in
+      all_reachable_vars current new_set q
+  in
+  let r_vars = all_reachable_vars Var.Set.empty wrt q in
+  Sh.filter_heap q ~f:(fun seg ->
+      exp_eq_class_has_only_vars_in r_vars q.cong seg.loc )
+  |>
+  [%Trace.retn fun {pf} -> pf "%a" pp]
 
 type from_call = Var.Subst.t [@@deriving compare, equal, sexp]
 
@@ -33,12 +68,36 @@ type from_call = Var.Subst.t [@@deriving compare, equal, sexp]
     of locals: rename formals to fresh vars in formula and actuals, add
     equations between each formal and actual, and quantify the temps and
     fresh vars. *)
-let call actuals formals locals ?temps q =
+let jump actuals formals ?temps q =
+  [%Trace.call fun {pf} ->
+    pf "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ q: %a@]"
+      (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp)
+      (List.rev formals) Sh.pp q]
+  ;
+  let q', freshen_locals = Sh.freshen q ~wrt:(Var.Set.of_list formals) 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
+  ( Option.fold ~f:(Fn.flip Sh.exists) temps
+      ~init:(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']
+
+(** 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 formals locals globals q =
   [%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]
+      (List.rev formals) Var.Set.pp locals pp q]
   ;
   let wrt = Set.add_list formals locals in
   let q', freshen_locals = Sh.freshen q ~wrt in
@@ -49,13 +108,39 @@ let call actuals formals locals ?temps q =
   let and_eqs formals actuals q =
     List.fold2_exn ~f:and_eq formals actuals ~init:q
   in
-  ( Sh.extend_us locals
-      (Option.fold ~f:(Fn.flip Sh.exists) temps
-         ~init:(and_eqs formals actuals q'))
-  , freshen_locals )
+  let q'', state_from_call =
+    (Sh.extend_us locals (and_eqs formals actuals q'), freshen_locals)
+  in
+  if summaries then (
+    let formals_set = Var.Set.of_list formals in
+    let non_function_specific_vars =
+      Set.diff (Sh.fv q'') (Set.union formals_set globals)
+    in
+    let function_summary_pre = Sh.exists non_function_specific_vars q'' in
+    let function_summary_pre =
+      garbage_collect function_summary_pre ~wrt:function_summary_pre.us
+    in
+    [%Trace.info "function summary pre %a" pp function_summary_pre] ;
+    let and_eq q formal actual =
+      Sh.and_ (Exp.eq (Exp.var formal) actual) q
+    in
+    (* Replace formals with actuals in the function summary *)
+    let foot =
+      Sh.exists formals_set
+        (List.fold2_exn ~f:and_eq formals actuals ~init:function_summary_pre)
+    in
+    (* Replace formals with actuals in the callsite precondition *)
+    let pre =
+      Sh.exists formals_set
+        (List.fold2_exn ~f:and_eq formals actuals ~init:q'')
+    in
+    let xs, foot = Sh.bind_exists ~wrt:pre.us foot in
+    let frame = Solver.infer_frame pre xs foot in
+    [%Trace.info "Maybe frame %a" (Option.pp "%a" pp) frame] ) ;
+  (q'', state_from_call)
   |>
   [%Trace.retn fun {pf} (q', s) ->
-    pf "@[<hv>subst: %a@ q': %a@]" Var.Subst.pp s Sh.pp q']
+    pf "@[<hv>subst: %a@ q': %a@]" Var.Subst.pp s pp q']
 
 (** Leave scope of locals: existentially quantify locals. *)
 let post locals q =
@@ -86,3 +171,51 @@ let resolve_callee lookup ptr _ =
   match Var.of_exp ptr with
   | Some callee_name -> lookup callee_name
   | None -> []
+
+let%test_module _ =
+  ( module struct
+    let pp = Format.printf "@.%a@." Sh.pp
+    let wrt = Var.Set.empty
+    let main_, wrt = Var.fresh "main" ~wrt
+    let a_, wrt = Var.fresh "a" ~wrt
+    let n_, wrt = Var.fresh "n" ~wrt
+    let b_, wrt = Var.fresh "b" ~wrt
+    let end_, _ = Var.fresh "end" ~wrt
+    let a = Exp.var a_
+    let main = Exp.var main_
+    let b = Exp.var b_
+    let n = Exp.var n_
+    let endV = Exp.var end_
+    let seg_main = Sh.seg {loc= main; bas= b; len= n; siz= n; arr= a}
+    let seg_a = Sh.seg {loc= a; bas= b; len= n; siz= n; arr= endV}
+    let seg_cycle = Sh.seg {loc= a; bas= b; len= n; siz= n; arr= main}
+
+    let%expect_test _ =
+      pp (garbage_collect seg_main ~wrt:(Var.Set.of_list [])) ;
+      [%expect {| emp |}]
+
+    let%expect_test _ =
+      pp
+        (garbage_collect (Sh.star seg_a seg_main)
+           ~wrt:(Var.Set.of_list [a_])) ;
+      [%expect {| %a_2 -[ %b_4, %n_3 )-> ⟨%n_3,%end_5⟩ |}]
+
+    let%expect_test _ =
+      pp
+        (garbage_collect (Sh.star seg_a seg_main)
+           ~wrt:(Var.Set.of_list [main_])) ;
+      [%expect
+        {|
+          %main_1 -[ %b_4, %n_3 )-> ⟨%n_3,%a_2⟩
+        * %a_2 -[ %b_4, %n_3 )-> ⟨%n_3,%end_5⟩ |}]
+
+    let%expect_test _ =
+      pp
+        (garbage_collect
+           (Sh.star seg_cycle seg_main)
+           ~wrt:(Var.Set.of_list [a_])) ;
+      [%expect
+        {|
+          %main_1 -[ %b_4, %n_3 )-> ⟨%n_3,%a_2⟩
+        * %a_2 -[ %b_4, %n_3 )-> ⟨%n_3,%main_1⟩ |}]
+  end )
diff --git a/sledge/src/symbheap/state_domain.mli b/sledge/src/symbheap/state_domain.mli
index 194e8b4a3..b283530e7 100644
--- a/sledge/src/symbheap/state_domain.mli
+++ b/sledge/src/symbheap/state_domain.mli
@@ -21,16 +21,21 @@ val exec_intrinsic :
 
 type from_call [@@deriving compare, equal, sexp]
 
+val jump :
+  Exp.t list -> Var.t list -> ?temps:Var.Set.t -> t -> t * from_call
+
 val call :
-     Exp.t list
+     summaries:bool
+  -> Exp.t list
   -> Var.t list
   -> Var.Set.t
-  -> ?temps:Var.Set.t
+  -> Var.Set.t
   -> t
   -> t * from_call
 
 val post : Var.Set.t -> t -> t
 val retn : Var.t list -> from_call -> t -> t
+val dnf : t -> t list
 
 val resolve_callee :
   (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list