From a8ad84b9d3c14734387dc8715818eaae0b42c8f2 Mon Sep 17 00:00:00 2001
From: Jia Chen <grievejia@fb.com>
Date: Mon, 26 Jun 2017 18:48:17 -0700
Subject: [PATCH] Prevent addresses of local vars from appearing in function
 summary

Reviewed By: jeremydubreil

Differential Revision: D5316446

fbshipit-source-id: 70355f4
---
 infer/src/IR/Exp.re             | 13 +++++++++++++
 infer/src/IR/Exp.rei            |  4 ++++
 infer/src/IR/Sil.re             |  8 ++++++++
 infer/src/IR/Sil.rei            |  2 ++
 infer/src/backend/Attribute.ml  | 13 ++++++++++++-
 infer/src/backend/tabulation.ml |  4 +++-
 6 files changed, 42 insertions(+), 2 deletions(-)

diff --git a/infer/src/IR/Exp.re b/infer/src/IR/Exp.re
index dca08e891..c41327d38 100644
--- a/infer/src/IR/Exp.re
+++ b/infer/src/IR/Exp.re
@@ -143,6 +143,19 @@ let get_undefined footprint =>
   Var (Ident.create_fresh (if footprint {Ident.kfootprint} else {Ident.kprimed}));
 
 
+/** returns true if the express operates on address of local variable */
+let rec has_local_addr e =>
+  switch (e: t) {
+  | Lvar pv => Pvar.is_local pv
+  | UnOp _ e' _
+  | Cast _ e'
+  | Lfield e' _ _ => has_local_addr e'
+  | BinOp _ e0 e1
+  | Lindex e0 e1 => has_local_addr e0 || has_local_addr e1
+  | _ => false
+  };
+
+
 /** Create integer constant */
 let int i => Const (Cint i);
 
diff --git a/infer/src/IR/Exp.rei b/infer/src/IR/Exp.rei
index 19ca72db2..7e0da90e4 100644
--- a/infer/src/IR/Exp.rei
+++ b/infer/src/IR/Exp.rei
@@ -106,6 +106,10 @@ let get_undefined: bool => t;
 let pointer_arith: t => bool;
 
 
+/** returns true if the express operates on address of local variable */
+let has_local_addr: t => bool;
+
+
 /** Integer constant 0 */
 let zero: t;
 
diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re
index 3d9d5bfc2..4f4874d2a 100644
--- a/infer/src/IR/Sil.re
+++ b/infer/src/IR/Sil.re
@@ -96,6 +96,14 @@ type atom =
 
 let equal_atom = [%compare.equal : atom];
 
+let atom_has_local_addr a =>
+  switch a {
+  | Aeq e0 e1
+  | Aneq e0 e1 => Exp.has_local_addr e0 || Exp.has_local_addr e1
+  | Apred _
+  | Anpred _ => false
+  };
+
 
 /** kind of lseg or dllseg predicates */
 type lseg_kind =
diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei
index eb39bfc9f..c3ecc8390 100644
--- a/infer/src/IR/Sil.rei
+++ b/infer/src/IR/Sil.rei
@@ -93,6 +93,8 @@ type atom =
 
 let equal_atom: atom => atom => bool;
 
+let atom_has_local_addr: atom => bool;
+
 
 /** kind of lseg or dllseg predicates */
 type lseg_kind =
diff --git a/infer/src/backend/Attribute.ml b/infer/src/backend/Attribute.ml
index 3d25e21cf..b604a26c1 100644
--- a/infer/src/backend/Attribute.ml
+++ b/infer/src/backend/Attribute.ml
@@ -294,7 +294,18 @@ let deallocate_stack_vars tenv (p: 'a Prop.t) pvars =
           end in
     List.iter ~f:do_var !fresh_address_vars;
     !res in
-  !stack_vars_address_in_post, List.fold ~f:(Prop.prop_atom_and tenv) ~init:p'' pi
+  (* Filter out local addresses in p'' *)
+  let filtered_pi, changed = List.fold_right p''.pi ~init:([], false)
+      ~f:(fun a (filtered, changed) ->
+          if Sil.atom_has_local_addr a then
+            filtered, true
+          else
+            a :: filtered, changed
+        ) in
+  (* Avoid normalization when p'' does not change *)
+  let p''' = if changed then Prop.normalize tenv (Prop.set p'' ~pi:filtered_pi)
+    else p'' in
+  !stack_vars_address_in_post, List.fold ~f:(Prop.prop_atom_and tenv) ~init:p''' pi
 
 (** Input of this method is an exp in a prop. Output is a formal variable or path from a
     formal variable that is equal to the expression,
diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml
index 7c10428d3..a8b515adc 100644
--- a/infer/src/backend/tabulation.ml
+++ b/infer/src/backend/tabulation.ml
@@ -1134,7 +1134,9 @@ let prop_pure_to_footprint tenv (p: 'a Prop.t) : Prop.normal Prop.t =
   if List.is_empty new_footprint_atoms
   then p
   else (* add pure fact to footprint *)
-    Prop.normalize tenv (Prop.set p ~pi_fp:(p.Prop.pi_fp @ new_footprint_atoms))
+    let filtered_pi_fp = List.filter (p.Prop.pi_fp @ new_footprint_atoms) ~f:(fun a ->
+        not (Sil.atom_has_local_addr a)) in
+    Prop.normalize tenv (Prop.set p ~pi_fp:filtered_pi_fp)
 
 (** post-process the raw result of a function call *)
 let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc results =