From 77c56de7a9055130df52d16f71fe24ce38c2c85f Mon Sep 17 00:00:00 2001
From: Jia Chen <grievejia@fb.com>
Date: Fri, 30 Jun 2017 15:32:17 -0700
Subject: [PATCH] [infer][backend] Do not create abduced var for addresses of
 local variables that are marked as Aundef

Reviewed By: jeremydubreil

Differential Revision: D5343493

fbshipit-source-id: 12354e2
---
 infer/src/IR/Exp.re                              | 12 ++++++++++++
 infer/src/IR/Exp.rei                             |  6 +++++-
 infer/src/backend/symExec.ml                     |  2 +-
 infer/tests/codetoanalyze/c/biabduction/abduce.c | 15 +++++++++++++++
 4 files changed, 33 insertions(+), 2 deletions(-)
 create mode 100644 infer/tests/codetoanalyze/c/biabduction/abduce.c

diff --git a/infer/src/IR/Exp.re b/infer/src/IR/Exp.re
index a0db16c70..9ada3691a 100644
--- a/infer/src/IR/Exp.re
+++ b/infer/src/IR/Exp.re
@@ -143,6 +143,18 @@ let get_undefined footprint =>
   Var (Ident.create_fresh (if footprint {Ident.kfootprint} else {Ident.kprimed}));
 
 
+/** returns true if the expression represents a stack-directed address */
+let rec is_stack_addr e =>
+  switch (e: t) {
+  | Lvar pv => not (Pvar.is_global pv)
+  | UnOp _ e' _
+  | Cast _ e'
+  | Lfield e' _ _
+  | Lindex e' _ => is_stack_addr e'
+  | _ => false
+  };
+
+
 /** returns true if the express operates on address of local variable */
 let rec has_local_addr e =>
   switch (e: t) {
diff --git a/infer/src/IR/Exp.rei b/infer/src/IR/Exp.rei
index dde12d640..36715bc2c 100644
--- a/infer/src/IR/Exp.rei
+++ b/infer/src/IR/Exp.rei
@@ -106,7 +106,11 @@ let get_undefined: bool => t;
 let pointer_arith: t => bool;
 
 
-/** returns true if the express operates on address of local variable */
+/** returns true if the expression represents a stack-directed address */
+let is_stack_addr: t => bool;
+
+
+/** returns true if the expression operates on address of local variable */
 let has_local_addr: t => bool;
 
 
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index aad7c66b3..c4a4cd15b 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -946,7 +946,7 @@ let execute_load ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ loc
             | _ -> callee_opt in
           List.fold ~f:fold_undef_pname ~init:None (Attribute.get_for_exp tenv prop exp) in
         let prop' =
-          if Config.angelic_execution then
+          if Config.angelic_execution && not (Exp.is_stack_addr n_rhs_exp') then
             (* when we try to deref an undefined value, add it to the footprint *)
             match exp_get_undef_attr n_rhs_exp' with
             | Some (Apred (Aundef (callee_pname, ret_annots, callee_loc, _), _)) ->
diff --git a/infer/tests/codetoanalyze/c/biabduction/abduce.c b/infer/tests/codetoanalyze/c/biabduction/abduce.c
new file mode 100644
index 000000000..b8cbe98e4
--- /dev/null
+++ b/infer/tests/codetoanalyze/c/biabduction/abduce.c
@@ -0,0 +1,15 @@
+/*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+void external_func(int* const*);
+
+int const_local_no_abduce(int* p) {
+  external_func(&p);
+  return p ? *p : 0;
+  // We shouldn't get a stack address escape warning here
+}