[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

@@ -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" () )
   |>

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

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

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)]

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

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

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]
   ;

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

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 _ =

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

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

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 )

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