[Uninit][9/13] Check rhs using prestate

Reviewed By: da319

Differential Revision: D10250227

fbshipit-source-id: c72e08924

infer/src/checkers/uninit.ml

@@ -184,6 +184,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   let exec_instr (astate : Domain.astate) {ProcData.pdesc; extras= {formals; summary}; tenv} _
       (instr : HilInstr.t) =
+    let check_access_expr ~loc rhs_access_expr =
+      if should_report_var pdesc tenv astate.maybe_uninit_vars rhs_access_expr then
+        report_intra rhs_access_expr loc summary
+    in
+    let check_hil_expr ~loc = function
+      | HilExp.AccessExpression access_expr ->
+          check_access_expr ~loc access_expr
+      | _ ->
+          ()
+    in
     let update_prepost access_expr rhs =
       let lhs_base = AccessExpression.get_base access_expr in
       if
@@ -198,6 +208,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     in
     match instr with
     | Assign (lhs_access_expr, rhs_expr, loc) ->
+        (* check on lhs_typ to avoid false positive when assigning a pointer to another *)
+        ( match AccessExpression.get_typ lhs_access_expr tenv with
+        | Some lhs_typ when not (Typ.is_reference lhs_typ) ->
+            check_hil_expr ~loc rhs_expr
+        | _ ->
+            () ) ;
         let maybe_uninit_vars' = MaybeUninitVars.remove lhs_access_expr astate.maybe_uninit_vars in
         let maybe_uninit_vars =
           if AccessExpression.is_base lhs_access_expr then
@@ -208,22 +224,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           else maybe_uninit_vars'
         in
         let prepost = update_prepost lhs_access_expr rhs_expr in
-        (* check on lhs_typ to avoid false positive when assigning a pointer to another *)
-        let is_lhs_not_a_pointer =
-          match AccessExpression.get_typ lhs_access_expr tenv with
-          | None ->
-              false
-          | Some lhs_ap_typ ->
-              not (Typ.is_reference lhs_ap_typ)
-        in
-        ( match rhs_expr with
-        | AccessExpression rhs_access_expr ->
-            if
-              should_report_var pdesc tenv maybe_uninit_vars rhs_access_expr
-              && is_lhs_not_a_pointer
-            then report_intra rhs_access_expr loc summary
-        | _ ->
-            () ) ;
         {astate with maybe_uninit_vars; prepost}
     | Call (_, Direct callee_pname, _, _, _)
       when Typ.Procname.equal callee_pname BuiltinDecl.objc_cpp_throw ->
@@ -299,13 +299,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             () ) ;
         {astate with maybe_uninit_vars}
     | Assume (expr, _, _, loc) ->
-        ( match expr with
+        check_hil_expr expr ~loc ; astate
-        | AccessExpression rhs_access_expr ->
-            if should_report_var pdesc tenv astate.maybe_uninit_vars rhs_access_expr then
-              report_intra rhs_access_expr loc summary
-        | _ ->
-            () ) ;
-        astate
 
 
   let pp_session_name node fmt = F.fprintf fmt "uninit %a" CFG.Node.pp_id (CFG.Node.id node)

infer/tests/codetoanalyze/c/uninit/arrays.c

@@ -0,0 +1,63 @@
+/*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+int array_good1_FP() {
+  int a[10];
+  for (int i = 0; i < 10; i++) {
+    a[i] = 0;
+  }
+  return a[2];
+}
+
+int array_bad() {
+  int a[10];
+  for (int i = 0; i < 5; i++) {
+    a[i] = 0;
+  }
+  return a[9];
+}
+
+int nondet();
+
+int array_good2_FP() {
+  int* a[10];
+  int i = 0;
+  while (i < 10) {
+    if (nondet()) {
+      a[i] = 0;
+      i++;
+    }
+  }
+  return a[2];
+}
+
+int array_good3_FP(int m) {
+  int* a[1000];
+  int i = 0;
+  while (i < 1000 && i < m) {
+    if (nondet()) {
+      a[i] = 0;
+      m--;
+    }
+  }
+  return i > 0 ? a[i - 1] : 42;
+}
+
+void mayinit_vpp(const void**);
+void use_vp(void*);
+
+void* call_to_mayinit_and_return_good_FP() {
+  void* obj[10];
+  mayinit_vpp((const void**)obj);
+  return obj[0];
+}
+
+void call_to_mayinit_and_call_use_good() {
+  void* obj[10];
+  mayinit_vpp((const void**)obj);
+  use_vp(obj[0]);
+}

infer/tests/codetoanalyze/c/uninit/issues.exp

@@ -1 +1,7 @@
+codetoanalyze/c/uninit/arrays.c, array_bad, 5, UNINITIALIZED_VALUE, no_bucket, ERROR, []
+codetoanalyze/c/uninit/arrays.c, array_good1_FP, 5, UNINITIALIZED_VALUE, no_bucket, ERROR, []
+codetoanalyze/c/uninit/arrays.c, array_good2_FP, 9, UNINITIALIZED_VALUE, no_bucket, ERROR, []
+codetoanalyze/c/uninit/arrays.c, array_good3_FP, 9, UNINITIALIZED_VALUE, no_bucket, ERROR, []
+codetoanalyze/c/uninit/arrays.c, call_to_mayinit_and_return_good_FP, 3, UNINITIALIZED_VALUE, no_bucket, ERROR, []
 codetoanalyze/c/uninit/uninit.c, dereference_bad, 2, UNINITIALIZED_VALUE, no_bucket, ERROR, []
+codetoanalyze/c/uninit/uninit.c, self_assign_bad, 2, UNINITIALIZED_VALUE, no_bucket, ERROR, []

infer/tests/codetoanalyze/c/uninit/uninit.c

@@ -21,7 +21,14 @@ int dereference_bad() {
   return *p;
 }
 
-void FN_self_assign() {
+void self_assign_bad() {
   int x;
   x = x;
 }
+
+void use_and_mayinit(int, int*);
+
+void call_to_use_and_mayinit_bad_FN() {
+  int x;
+  use_and_mayinit(x, &x);
+}