[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

@@ -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) {

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;
 
 

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, _), _)) ->

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
+}