[infer][backend] Invalidate by-ref parameters for logical variables as well as program variables when calling undefined functions

Reviewed By: jeremydubreil

Differential Revision: D5363552

fbshipit-source-id: e76db48

infer/src/IR/Pvar.re

@@ -27,6 +27,7 @@ type pvar_kind =
   | Callee_var Typ.Procname.t /** local variable belonging to a callee */
   | Abduced_retvar Typ.Procname.t Location.t /** synthetic variable to represent return value */
   | Abduced_ref_param Typ.Procname.t t Location.t
+  | Abduced_ref_param_val Typ.Procname.t Ident.t Location.t
   /** synthetic variable to represent param passed by reference */
   | Global_var (translation_unit, bool, bool, bool)
   /** global variable: translation unit + is it compile constant? + is it POD? + is it a static
@@ -70,6 +71,12 @@ let rec _pp f pv => {
     } else {
       F.fprintf f "%a$%a%a|abducedRefParam" Typ.Procname.pp n Location.pp l Mangled.pp name
     }
+  | Abduced_ref_param_val n id l =>
+    if !Config.pp_simple {
+      F.fprintf f "%a|%a|abducedRefParamVal" (Ident.pp Pp.text) id Mangled.pp name
+    } else {
+      F.fprintf f "%a$%a%a|abducedRefParamVal" Typ.Procname.pp n Location.pp l Mangled.pp name
+    }
   | Global_var (translation_unit, is_const, is_pod, _) =>
     F.fprintf
       f
@@ -120,6 +127,14 @@ let pp_latex f pv => {
       (Mangled.to_string name)
       (Latex.pp_string Latex.Roman)
       "abducedRefParam"
+  | Abduced_ref_param_val _ =>
+    F.fprintf
+      f
+      "%a_{%a}"
+      (Latex.pp_string Latex.Roman)
+      (Mangled.to_string name)
+      (Latex.pp_string Latex.Roman)
+      "abducedRefParamVal"
   | Global_var _ => Latex.pp_string Latex.Boldface f (Mangled.to_string name)
   | Seed_var =>
     F.fprintf
@@ -194,7 +209,8 @@ let get_simplified_name pv => {
 let is_abduced pv =>
   switch pv.pv_kind {
   | Abduced_retvar _
-  | Abduced_ref_param _ => true
+  | Abduced_ref_param _
+  | Abduced_ref_param_val _ => true
   | _ => false
   };
 
@@ -291,6 +307,7 @@ let to_callee pname pvar =>
   | Callee_var _
   | Abduced_retvar _
   | Abduced_ref_param _
+  | Abduced_ref_param_val _
   | Seed_var =>
     L.d_str "Cannot convert pvar to callee: ";
     d pvar;
@@ -353,6 +370,11 @@ let mk_abduced_ref_param (proc_name: Typ.Procname.t) (pv: t) (loc: Location.t) :
   {pv_hash: name_hash name, pv_name: name, pv_kind: Abduced_ref_param proc_name pv loc}
 };
 
+let mk_abduced_ref_param_val (proc_name: Typ.Procname.t) (id: Ident.t) (loc: Location.t) :t => {
+  let name = Mangled.from_string ("$REF_PARAM_VAL_" ^ Typ.Procname.to_unique_id proc_name);
+  {pv_hash: name_hash name, pv_name: name, pv_kind: Abduced_ref_param_val proc_name id loc}
+};
+
 let get_translation_unit pvar =>
   switch pvar.pv_kind {
   | Global_var (tu, _, _, _) => tu

infer/src/IR/Pvar.rei

@@ -105,6 +105,10 @@ let mk: Mangled.t => Typ.Procname.t => t;
 let mk_abduced_ref_param: Typ.Procname.t => t => Location.t => t;
 
 
+/** create an abduced variable for a parameter passed by reference */
+let mk_abduced_ref_param_val: Typ.Procname.t => Ident.t => Location.t => t;
+
+
 /** create an abduced return variable for a call to [proc_name] at [loc] */
 let mk_abduced_ret: Typ.Procname.t => Location.t => t;
 

infer/src/backend/symExec.ml

@@ -1290,66 +1290,68 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
         prop.Prop.sigma in
     Prop.normalize tenv (Prop.set prop ~sigma:sigma') in
   let add_actual_by_ref_to_footprint prop (actual, actual_typ, _) =
-    match actual with
-    | Exp.Lvar actual_pv ->
-        (* introduce a fresh program variable to allow abduction on the return value *)
-        let abduced_ref_pv =
-          Pvar.mk_abduced_ref_param callee_pname actual_pv callee_loc in
-        let already_has_abduced_retval p =
-          List.exists
-            ~f:(fun hpred -> match hpred with
-                | Sil.Hpointsto (Exp.Lvar pv, _, _) -> Pvar.equal pv abduced_ref_pv
-                | _ -> false)
-            p.Prop.sigma_fp in
-        (* prevent introducing multiple abduced retvals for a single call site in a loop *)
-        if already_has_abduced_retval prop then prop
-        else
-        if !Config.footprint then
-          let prop', abduced_strexp =
-            match actual_typ.Typ.desc with
-            | Typ.Tptr ({desc=Tstruct _} as typ, _) ->
-                (* for struct types passed by reference, do abduction on the fields of the
-                   struct *)
-                add_struct_value_to_footprint tenv abduced_ref_pv typ prop
-            | Typ.Tptr (typ, _) ->
-                (* for pointer types passed by reference, do abduction directly on the pointer *)
-                let (prop', fresh_fp_var) =
-                  add_to_footprint tenv abduced_ref_pv typ prop in
-                prop', Sil.Eexp (fresh_fp_var, Sil.Inone)
-            | _ ->
-                failwith
-                  ("No need for abduction on non-pointer type " ^
-                   (Typ.to_string actual_typ)) in
-          (* replace [actual] |-> _ with [actual] |-> [fresh_fp_var] *)
-          let filtered_sigma =
-            List.map
-              ~f:(function
-                  | Sil.Hpointsto (lhs, _, typ_exp) when Exp.equal lhs actual ->
-                      Sil.Hpointsto (lhs, abduced_strexp, typ_exp)
-                  | hpred -> hpred)
-              prop'.Prop.sigma in
-          Prop.normalize tenv (Prop.set prop' ~sigma:filtered_sigma)
-        else
-          (* bind actual passed by ref to the abduced value pointed to by the synthetic pvar *)
-          let prop' =
-            let filtered_sigma =
-              List.filter
-                ~f:(function
-                    | Sil.Hpointsto (lhs, _, _) when Exp.equal lhs actual ->
-                        false
-                    | _ -> true)
-                prop.Prop.sigma in
-            Prop.normalize tenv (Prop.set prop ~sigma:filtered_sigma) in
-          List.fold
-            ~f:(fun p hpred ->
-                match hpred with
-                | Sil.Hpointsto (Exp.Lvar pv, rhs, texp) when Pvar.equal pv abduced_ref_pv ->
-                    let new_hpred = Sil.Hpointsto (actual, rhs, texp) in
-                    Prop.normalize tenv (Prop.set p ~sigma:(new_hpred :: prop'.Prop.sigma))
-                | _ -> p)
-            ~init:prop'
-            prop'.Prop.sigma
-    | _ -> assert false in
+    let abduced = match actual with
+      | Exp.Lvar actual_pv ->
+          Pvar.mk_abduced_ref_param callee_pname actual_pv callee_loc
+      | Exp.Var actual_id ->
+          Pvar.mk_abduced_ref_param_val callee_pname actual_id callee_loc
+      | _ -> assert false
+    in
+    let already_has_abduced_retval p =
+      List.exists
+        ~f:(fun hpred -> match hpred with
+            | Sil.Hpointsto (Exp.Lvar pv, _, _) -> Pvar.equal pv abduced
+            | _ -> false)
+        p.Prop.sigma_fp in
+    (* prevent introducing multiple abduced retvals for a single call site in a loop *)
+    if already_has_abduced_retval prop then prop
+    else
+    if !Config.footprint then
+      let prop', abduced_strexp =
+        match actual_typ.Typ.desc with
+        | Typ.Tptr ({desc=Tstruct _} as typ, _) ->
+            (* for struct types passed by reference, do abduction on the fields of the
+               struct *)
+            add_struct_value_to_footprint tenv abduced typ prop
+        | Typ.Tptr (typ, _) ->
+            (* for pointer types passed by reference, do abduction directly on the pointer *)
+            let (prop', fresh_fp_var) =
+              add_to_footprint tenv abduced typ prop in
+            prop', Sil.Eexp (fresh_fp_var, Sil.Inone)
+        | _ ->
+            failwith
+              ("No need for abduction on non-pointer type " ^
+               (Typ.to_string actual_typ)) in
+      (* replace [actual] |-> _ with [actual] |-> [fresh_fp_var] *)
+      let filtered_sigma =
+        List.map
+          ~f:(function
+              | Sil.Hpointsto (lhs, _, typ_exp) when Exp.equal lhs actual ->
+                  Sil.Hpointsto (lhs, abduced_strexp, typ_exp)
+              | hpred -> hpred)
+          prop'.Prop.sigma in
+      Prop.normalize tenv (Prop.set prop' ~sigma:filtered_sigma)
+    else
+      (* bind actual passed by ref to the abduced value pointed to by the synthetic pvar *)
+      let prop' =
+        let filtered_sigma =
+          List.filter
+            ~f:(function
+                | Sil.Hpointsto (lhs, _, _) when Exp.equal lhs actual ->
+                    false
+                | _ -> true)
+            prop.Prop.sigma in
+        Prop.normalize tenv (Prop.set prop ~sigma:filtered_sigma) in
+      List.fold
+        ~f:(fun p hpred ->
+            match hpred with
+            | Sil.Hpointsto (Exp.Lvar pv, rhs, texp) when Pvar.equal pv abduced ->
+                let new_hpred = Sil.Hpointsto (actual, rhs, texp) in
+                Prop.normalize tenv (Prop.set p ~sigma:(new_hpred :: prop'.Prop.sigma))
+            | _ -> p)
+        ~init:prop'
+        prop'.Prop.sigma
+  in
   (* non-angelic mode; havoc each var passed by reference by assigning it to a fresh id *)
   let havoc_actual_by_ref prop (actual, actual_typ, _) =
     let actual_pt_havocd_var =
@@ -1435,10 +1437,29 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots
             actuals
           |> fst
     else prop in
+  let should_abduce_param_value pname =
+    let open Typ.Procname in
+    match pname with
+    | Java _ ->
+        (* FIXME (T19882766): we need to disable this for Java because it breaks too many tests *)
+        false
+    | ObjC_Cpp _ ->
+        (* FIXME: we need to work around a frontend hack for std::shared_ptr
+         * to silent some of the uninitialization warnings *)
+        if String.is_suffix ~suffix:"_std__shared_ptr"
+            (Typ.Procname.to_string callee_pname) then
+          false
+        else
+          true
+    | _ -> true
+  in
   let actuals_by_ref =
     List.filter_mapi
       ~f:(fun i actual -> match actual with
           | (Exp.Lvar _ as e, ({Typ.desc=Tptr _} as t)) -> Some (e, t, i)
+          | (Exp.Var _ as e, ({Typ.desc=Tptr _} as t))
+            when should_abduce_param_value callee_pname ->
+              Some (e, t, i)
           | _ -> None)
       args in
   let has_nullable_annot = Annotations.ia_is_nullable ret_annots in

infer/tests/codetoanalyze/cpp/errors/issues.exp

@@ -52,6 +52,8 @@ codetoanalyze/cpp/errors/numeric/min_max.cpp, max_int_div0, 0, DIVIDE_BY_ZERO, [
 codetoanalyze/cpp/errors/numeric/min_max.cpp, min_X_div0, 2, DIVIDE_BY_ZERO, [start of procedure min_X_div0(),start of procedure X,return from a call to X_X,start of procedure X,return from a call to X_X]
 codetoanalyze/cpp/errors/numeric/min_max.cpp, min_int_div0, 0, DIVIDE_BY_ZERO, [start of procedure min_int_div0()]
 codetoanalyze/cpp/errors/overwrite_attribute/main.cpp, testSetIntValue, 3, DIVIDE_BY_ZERO, [start of procedure testSetIntValue(),start of procedure setIntValue(),return from a call to setIntValue]
+codetoanalyze/cpp/errors/pointers/unintialized.cpp, known_ctor_dangling_bad, 2, DANGLING_POINTER_DEREFERENCE, [start of procedure known_ctor_dangling_bad(),start of procedure TestDangling,return from a call to TestDangling_TestDangling]
+codetoanalyze/cpp/errors/pointers/unintialized.cpp, known_ctor_dangling_bad, 2, UNINITIALIZED_VALUE, [start of procedure known_ctor_dangling_bad(),start of procedure TestDangling,return from a call to TestDangling_TestDangling]
 codetoanalyze/cpp/errors/pointers/unintialized.cpp, uninitialized_dangling_bad, 2, DANGLING_POINTER_DEREFERENCE, [start of procedure uninitialized_dangling_bad()]
 codetoanalyze/cpp/errors/pointers/unintialized.cpp, uninitialized_dangling_bad, 2, UNINITIALIZED_VALUE, [start of procedure uninitialized_dangling_bad()]
 codetoanalyze/cpp/errors/resource_leaks/raii.cpp, resource_leak, 7, RESOURCE_LEAK, [start of procedure resource_leak(),Condition is false]

infer/tests/codetoanalyze/cpp/errors/pointers/unintialized.cpp

@@ -15,3 +15,28 @@ void uninitialized_dangling_bad() {
   int* p;
   delete p;
 }
+
+struct TestDangling {
+  int* p;
+  // Field p is deliberately left uninitialized
+  TestDangling() {}
+  // This constructor is deliberately left unimplemented
+  // to make sure Infer treats undefined function conservatively
+  TestDangling(int);
+};
+
+int known_ctor_dangling_bad() {
+  auto t0 = new TestDangling();
+  int ret = *(t0->p); // should report a dangling pointer dereference here as p
+                      // is dangling
+  delete t0;
+  return ret;
+}
+
+int unknown_ctor_assume_no_dangling_ok() {
+  auto t1 = new TestDangling(0);
+  int ret =
+      *(t1->p); // TestDangling(0) is not known so p may have been initialized
+  delete t1;
+  return ret;
+}

infer/tests/codetoanalyze/objc/errors/issues.exp

@@ -13,7 +13,6 @@ codetoanalyze/objc/errors/npe/null_returned_by_method.m, NullReturnedByMethodA_t
 codetoanalyze/objc/errors/procdescs/main.c, ProcdescMain, 2, MEMORY_LEAK, [start of procedure ProcdescMain(),Skipped call: function or method not found]
 codetoanalyze/objc/errors/procdescs/main.c, ProcdescMain, 3, MEMORY_LEAK, [start of procedure ProcdescMain(),Skipped call: function or method not found]
 codetoanalyze/objc/errors/procdescs/main.c, call_nslog, 1, MEMORY_LEAK, [start of procedure call_nslog()]
-codetoanalyze/objc/errors/procdescs/main.c, call_nslog, 2, MEMORY_LEAK, [start of procedure call_nslog(),Skipped call: function or method not found]
 codetoanalyze/objc/errors/procdescs/main.c, call_nslog, 3, MEMORY_LEAK, [start of procedure call_nslog(),Skipped call: function or method not found]
 codetoanalyze/objc/errors/property/main.c, property_main, 2, MEMORY_LEAK, [start of procedure property_main(),Skipped call: function or method not found]
 codetoanalyze/objc/errors/property/main.c, property_main, 3, MEMORY_LEAK, [start of procedure property_main(),Skipped call: function or method not found]