From 5a4d4f08829f6c59c3ce20d4429bd977451ebe43 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Tue, 21 Aug 2018 07:59:06 -0700 Subject: [PATCH] [inferbo] Fail if trying to substitute non-symbolic conditions Reviewed By: ezgicicek Differential Revision: D9377804 fbshipit-source-id: 609fd1594 --- .../bufferOverrunProofObligations.ml | 87 ++++++++++--------- .../c/bufferoverrun/issue_kinds.c | 5 ++ .../codetoanalyze/c/bufferoverrun/issues.exp | 1 + 3 files changed, 52 insertions(+), 41 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index a14cbbaab..88343604c 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/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 - | `Equal | `LeftSmallerThanRight | `RightSubsumesLeft -> - {report_issue_type= Some IssueType.inferbo_alloc_is_negative; propagate= false} - | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.lb length) -> - {report_issue_type= Some IssueType.inferbo_alloc_may_be_negative; propagate= true} - | cmp_mone -> - match ItvPure.xcompare ~lhs:length ~rhs:itv_big with - | `Equal | `RightSmallerThanLeft | `RightSubsumesLeft -> - {report_issue_type= Some IssueType.inferbo_alloc_is_big; propagate= false} - | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.ub length) -> - {report_issue_type= Some IssueType.inferbo_alloc_may_be_big; propagate= true} - | cmp_big -> - let propagate = - match (cmp_mone, cmp_big) with - | (`NotComparable | `LeftSubsumesRight), _ | _, (`NotComparable | `LeftSubsumesRight) -> - true - | _ -> - false - in - {report_issue_type= None; propagate} + let is_symbolic = ItvPure.is_symbolic length in + match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.mone with + | `Equal | `LeftSmallerThanRight | `RightSubsumesLeft -> + {report_issue_type= Some IssueType.inferbo_alloc_is_negative; propagate= false} + | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.lb length) -> + { report_issue_type= Some IssueType.inferbo_alloc_may_be_negative + ; propagate= is_symbolic } + | cmp_mone -> + match ItvPure.xcompare ~lhs:length ~rhs:itv_big with + | `Equal | `RightSmallerThanLeft | `RightSubsumesLeft -> + {report_issue_type= Some IssueType.inferbo_alloc_is_big; propagate= false} + | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.ub length) -> + {report_issue_type= Some IssueType.inferbo_alloc_may_be_big; propagate= is_symbolic} + | cmp_big -> + let propagate = + match (cmp_mone, cmp_big) with + | (`NotComparable | `LeftSubsumesRight), _ + | _, (`NotComparable | `LeftSubsumesRight) -> + is_symbolic + | _ -> + 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 - | [] -> - Some cwt - | symbols -> - match Condition.subst bound_map rel_map caller_relation cwt.cond with - | None -> - None - | Some cond -> - let traces_caller = - List.fold symbols ~init:ValTraceSet.empty ~f:(fun val_traces symbol -> - match Itv.SymbolMap.find symbol trace_map with - | symbol_trace -> - ValTraceSet.join symbol_trace val_traces - | exception Caml.Not_found -> - val_traces ) - in - let trace = - ConditionTrace.make_call_and_subst ~traces_caller ~caller_pname ~callee_pname location - cwt.trace - in - Some {cond; trace} + let symbols = Condition.get_symbols cwt.cond in + if List.is_empty symbols then + L.(die InternalError) + "Trying to substitute a non-symbolic condition %a from %a at %a. Why was it propagated in \ + the first place?" + pp cwt Typ.Procname.pp callee_pname Location.pp location ; + match Condition.subst bound_map rel_map caller_relation cwt.cond with + | None -> + None + | Some cond -> + let traces_caller = + List.fold symbols ~init:ValTraceSet.empty ~f:(fun val_traces symbol -> + match Itv.SymbolMap.find symbol trace_map with + | symbol_trace -> + ValTraceSet.join symbol_trace val_traces + | exception Caml.Not_found -> + val_traces ) + in + let trace = + ConditionTrace.make_call_and_subst ~traces_caller ~caller_pname ~callee_pname location + cwt.trace + in + Some {cond; trace} let set_buffer_overrun_u5 {cond; trace} issue_type = diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c index 44da37b52..a1b7fbf42 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c +++ b/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); } diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index ca8f69886..65ee5b3da 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/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]