[inferbo] Fail if trying to substitute non-symbolic conditions

Reviewed By: ezgicicek

Differential Revision: D9377804

fbshipit-source-id: 609fd1594

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -68,26 +68,29 @@ module AllocSizeCondition = struct
     | `LeftSmallerThanRight ->
         {report_issue_type= Some IssueType.inferbo_alloc_is_negative; propagate= false}
     | _ ->
-      match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.mone with
+        let is_symbolic = ItvPure.is_symbolic length in
-      | `Equal | `LeftSmallerThanRight | `RightSubsumesLeft ->
+        match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.mone with
-          {report_issue_type= Some IssueType.inferbo_alloc_is_negative; propagate= false}
+        | `Equal | `LeftSmallerThanRight | `RightSubsumesLeft ->
-      | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.lb length) ->
+            {report_issue_type= Some IssueType.inferbo_alloc_is_negative; propagate= false}
-          {report_issue_type= Some IssueType.inferbo_alloc_may_be_negative; propagate= true}
+        | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.lb length) ->
-      | cmp_mone ->
+            { report_issue_type= Some IssueType.inferbo_alloc_may_be_negative
-        match ItvPure.xcompare ~lhs:length ~rhs:itv_big with
+            ; propagate= is_symbolic }
-        | `Equal | `RightSmallerThanLeft | `RightSubsumesLeft ->
+        | cmp_mone ->
-            {report_issue_type= Some IssueType.inferbo_alloc_is_big; propagate= false}
+          match ItvPure.xcompare ~lhs:length ~rhs:itv_big with
-        | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.ub length) ->
+          | `Equal | `RightSmallerThanLeft | `RightSubsumesLeft ->
-            {report_issue_type= Some IssueType.inferbo_alloc_may_be_big; propagate= true}
+              {report_issue_type= Some IssueType.inferbo_alloc_is_big; propagate= false}
-        | cmp_big ->
+          | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.ub length) ->
-            let propagate =
+              {report_issue_type= Some IssueType.inferbo_alloc_may_be_big; propagate= is_symbolic}
-              match (cmp_mone, cmp_big) with
+          | cmp_big ->
-              | (`NotComparable | `LeftSubsumesRight), _ | _, (`NotComparable | `LeftSubsumesRight) ->
+              let propagate =
-                  true
+                match (cmp_mone, cmp_big) with
-              | _ ->
+                | (`NotComparable | `LeftSubsumesRight), _
-                  false
+                | _, (`NotComparable | `LeftSubsumesRight) ->
-            in
+                    is_symbolic
-            {report_issue_type= None; propagate}
+                | _ ->
+                    false
+              in
+              {report_issue_type= None; propagate}
 
 
   let subst bound_map length =
@@ -432,27 +435,29 @@ module ConditionWithTrace = struct
 
 
   let subst (bound_map, trace_map) rel_map caller_relation caller_pname callee_pname location cwt =
-    match Condition.get_symbols cwt.cond with
+    let symbols = Condition.get_symbols cwt.cond in
-    | [] ->
+    if List.is_empty symbols then
-        Some cwt
+      L.(die InternalError)
-    | symbols ->
+        "Trying to substitute a non-symbolic condition %a from %a at %a. Why was it propagated in \
-      match Condition.subst bound_map rel_map caller_relation cwt.cond with
+         the first place?"
-      | None ->
+        pp cwt Typ.Procname.pp callee_pname Location.pp location ;
-          None
+    match Condition.subst bound_map rel_map caller_relation cwt.cond with
-      | Some cond ->
+    | None ->
-          let traces_caller =
+        None
-            List.fold symbols ~init:ValTraceSet.empty ~f:(fun val_traces symbol ->
+    | Some cond ->
-                match Itv.SymbolMap.find symbol trace_map with
+        let traces_caller =
-                | symbol_trace ->
+          List.fold symbols ~init:ValTraceSet.empty ~f:(fun val_traces symbol ->
-                    ValTraceSet.join symbol_trace val_traces
+              match Itv.SymbolMap.find symbol trace_map with
-                | exception Caml.Not_found ->
+              | symbol_trace ->
-                    val_traces )
+                  ValTraceSet.join symbol_trace val_traces
-          in
+              | exception Caml.Not_found ->
-          let trace =
+                  val_traces )
-            ConditionTrace.make_call_and_subst ~traces_caller ~caller_pname ~callee_pname location
+        in
-              cwt.trace
+        let trace =
-          in
+          ConditionTrace.make_call_and_subst ~traces_caller ~caller_pname ~callee_pname location
-          Some {cond; trace}
+            cwt.trace
+        in
+        Some {cond; trace}
 
 
   let set_buffer_overrun_u5 {cond; trace} issue_type =

infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c

@@ -134,6 +134,8 @@ int s2_symbolic_widened_Good_FP(int n) {
   }
 }
 
+int l1_call_to_s2_symbolic_widened_Bad() { s2_symbolic_widened_Bad(1); }
+
 void may_underrun_symbolic_Nowarn_Good(int n) {
   int a[n];
   a[n - 1] = 0;
@@ -161,6 +163,9 @@ void alloc_is_big_Bad() { malloc(2 * 1000 * 1000 * 1000); }
 
 void alloc_may_be_big_Bad() { malloc(zero_or_ten(1) * 100 * 1000 * 1000 + 1); }
 
+// Non-symbolic, should not be propagated
+void call_to_alloc_may_be_big_Good() { alloc_may_be_big_Bad(); }
+
 void alloc_may_be_big_Good_FP() {
   malloc(zero_or_ten(1) * 100 * 1000 * 1000 + 1);
 }

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

@@ -35,6 +35,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Good_FP, 1, INFERB
 codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Bad, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [-5, 5]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Good_FP, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [-5, 5]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Bad, 1, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Call,Parameter: n,Alloc: Length: [100000000, +oo] by call to `alloc_may_be_big2_Silenced` ]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: [1, +oo] Size: 1 by call to `s2_symbolic_widened_Bad` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [max(10, i.lb), i.ub] Size: 10]