pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[Inferbo] Do not propagate all safety conditions

Browse Source 
Reviewed By: skcho

Differential Revision: D7289292

fbshipit-source-id: 999b14a
master
Mehdi Bouaziz 7 years ago committed by Facebook Github Bot
parent 0ba528c3fa
commit e9a3913fdb
3 changed files with 45 additions and 31 deletions
Show Stats Download Patch File Download Diff File

5
infer/src/bufferoverrun/bufferOverrunChecker.ml
Unescape View File

@ -536,7 +536,7 @@ module Report = struct
List.fold_right ~f ~init:([], 0) trace.trace |> fst |> List.rev List.fold_right ~f ~init:([], 0) trace.trace |> fst |> List.rev
let report_errors : Specs.summary -> Procdesc.t -> PO.ConditionSet.t -> unit = let report_errors : Specs.summary -> Procdesc.t -> PO.ConditionSet.t -> PO.ConditionSet.t =
fun summary pdesc cond_set -> fun summary pdesc cond_set ->
let pname = Procdesc.get_proc_name pdesc in let pname = Procdesc.get_proc_name pdesc in
let report cond trace issue_type = let report cond trace issue_type =
@ -575,8 +575,7 @@ let compute_post
let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata in let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata in
let entry_mem = extract_post inv_map (CFG.start_node cfg) in let entry_mem = extract_post inv_map (CFG.start_node cfg) in
let exit_mem = extract_post inv_map (CFG.exit_node cfg) in let exit_mem = extract_post inv_map (CFG.exit_node cfg) in
let cond_set = Report.check_proc summary pdata inv_map in let cond_set = Report.check_proc summary pdata inv_map |> Report.report_errors summary pdesc in
Report.report_errors summary pdesc cond_set ;
match (entry_mem, exit_mem) with match (entry_mem, exit_mem) with
| Some entry_mem, Some exit_mem -> | Some entry_mem, Some exit_mem ->
Some (entry_mem, exit_mem, cond_set) Some (entry_mem, exit_mem, cond_set)

68
infer/src/bufferoverrun/bufferOverrunProofObligations.ml
Unescape View File

@ -15,6 +15,8 @@ module ItvPure = Itv.ItvPure
module MF = MarkupFormatter module MF = MarkupFormatter
module ValTraceSet = BufferOverrunTrace.Set module ValTraceSet = BufferOverrunTrace.Set
type checked_condition = {report_issue_type: IssueType.t option; propagate: bool}
module AllocSizeCondition = struct module AllocSizeCondition = struct
type t = ItvPure.astate type t = ItvPure.astate
@ -62,23 +64,30 @@ module AllocSizeCondition = struct
let check length = let check length =
match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.zero with match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.zero with
| `Equal | `RightSubsumesLeft -> | `Equal | `RightSubsumesLeft ->
Some IssueType.inferbo_alloc_is_zero {report_issue_type= Some IssueType.inferbo_alloc_is_zero; propagate= false}
| `LeftSmallerThanRight -> | `LeftSmallerThanRight ->
Some IssueType.inferbo_alloc_is_negative {report_issue_type= Some IssueType.inferbo_alloc_is_negative; propagate= false}
| _ -> | _ ->
match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.mone with match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.mone with
| `Equal | `LeftSmallerThanRight | `RightSubsumesLeft -> | `Equal | `LeftSmallerThanRight | `RightSubsumesLeft ->
Some IssueType.inferbo_alloc_is_negative {report_issue_type= Some IssueType.inferbo_alloc_is_negative; propagate= false}
| `LeftSubsumesRight when Itv.Bound.is_not_infty (ItvPure.lb length) -> | `LeftSubsumesRight when Itv.Bound.is_not_infty (ItvPure.lb length) ->
Some IssueType.inferbo_alloc_may_be_negative {report_issue_type= Some IssueType.inferbo_alloc_may_be_negative; propagate= true}
| _ -> | cmp_mone ->
match ItvPure.xcompare ~lhs:length ~rhs:itv_big with match ItvPure.xcompare ~lhs:length ~rhs:itv_big with
| `Equal | `RightSmallerThanLeft | `RightSubsumesLeft -> | `Equal | `RightSmallerThanLeft | `RightSubsumesLeft ->
Some IssueType.inferbo_alloc_is_big {report_issue_type= Some IssueType.inferbo_alloc_is_big; propagate= false}
| `LeftSubsumesRight when Itv.Bound.is_not_infty (ItvPure.ub length) -> | `LeftSubsumesRight when Itv.Bound.is_not_infty (ItvPure.ub length) ->
Some IssueType.inferbo_alloc_may_be_big {report_issue_type= Some IssueType.inferbo_alloc_may_be_big; propagate= true}
| _ -> | cmp_big ->
None let propagate =
match (cmp_mone, cmp_big) with
| `NotComparable, _ | _, `NotComparable ->
true
| _ ->
false
in
{report_issue_type= None; propagate}
let subst bound_map length = let subst bound_map length =
@ -194,7 +203,7 @@ module ArrayAccessCondition = struct
(* check buffer overrun and return its confidence *) (* check buffer overrun and return its confidence *)
let check : t -> IssueType.t option = let check : t -> checked_condition =
fun c -> fun c ->
(* idx = [il, iu], size = [sl, su], we want to check that 0 <= idx < size *) (* idx = [il, iu], size = [sl, su], we want to check that 0 <= idx < size *)
let c' = set_size_pos c in let c' = set_size_pos c in
@ -202,21 +211,28 @@ module ArrayAccessCondition = struct
let not_overrun = ItvPure.lt_sem c'.idx c'.size in let not_overrun = ItvPure.lt_sem c'.idx c'.size in
let not_underrun = ItvPure.le_sem ItvPure.zero c'.idx in let not_underrun = ItvPure.le_sem ItvPure.zero c'.idx in
(* il >= 0 and iu < sl, definitely not an error *) (* il >= 0 and iu < sl, definitely not an error *)
if ItvPure.is_one not_overrun && ItvPure.is_one not_underrun then None if ItvPure.is_one not_overrun && ItvPure.is_one not_underrun then
(* iu < 0 or il >= su, definitely an error *) {report_issue_type= None; propagate= false} (* iu < 0 or il >= su, definitely an error *)
else if ItvPure.is_zero not_overrun || ItvPure.is_zero not_underrun then else if ItvPure.is_zero not_overrun || ItvPure.is_zero not_underrun then
Some IssueType.buffer_overrun_l1 (* su <= iu < +oo, most probably an error *) {report_issue_type= Some IssueType.buffer_overrun_l1; propagate= false}
(* su <= iu < +oo, most probably an error *)
else if Itv.Bound.is_not_infty (ItvPure.ub c.idx) else if Itv.Bound.is_not_infty (ItvPure.ub c.idx)
&& Itv.Bound.le (ItvPure.ub c.size) (ItvPure.ub c.idx) && Itv.Bound.le (ItvPure.ub c.size) (ItvPure.ub c.idx)
then Some IssueType.buffer_overrun_l2 (* symbolic il >= sl, probably an error *) then {report_issue_type= Some IssueType.buffer_overrun_l2; propagate= false}
(* symbolic il >= sl, probably an error *)
else if Itv.Bound.is_symbolic (ItvPure.lb c.idx) else if Itv.Bound.is_symbolic (ItvPure.lb c.idx)
&& Itv.Bound.le (ItvPure.lb c'.size) (ItvPure.lb c.idx) && Itv.Bound.le (ItvPure.lb c'.size) (ItvPure.lb c.idx)
then Some IssueType.buffer_overrun_s2 (* other symbolic bounds are probably too noisy *) then {report_issue_type= Some IssueType.buffer_overrun_s2; propagate= true}
else if Config.bo_debug <= 3 && (ItvPure.is_symbolic c.idx || ItvPure.is_symbolic c.size) then else
None (* other symbolic bounds are probably too noisy *)
else if filter1 c then Some IssueType.buffer_overrun_l5 let is_symbolic = ItvPure.is_symbolic c.idx || ItvPure.is_symbolic c.size in
else if filter2 c then Some IssueType.buffer_overrun_l4 let report_issue_type =
else Some IssueType.buffer_overrun_l3 if Config.bo_debug <= 3 && is_symbolic then None
else if filter1 c then Some IssueType.buffer_overrun_l5
else if filter2 c then Some IssueType.buffer_overrun_l4
else Some IssueType.buffer_overrun_l3
in
{report_issue_type; propagate= is_symbolic}
let subst : Itv.Bound.t bottom_lifted Itv.SubstMap.t -> t -> t option = let subst : Itv.Bound.t bottom_lifted Itv.SubstMap.t -> t -> t option =
@ -461,13 +477,11 @@ module ConditionSet = struct
let check_all ~report condset = let check_all ~report condset =
List.iter condset ~f:(fun cwt -> List.filter condset ~f:(fun cwt ->
match Condition.check cwt.cond with let {report_issue_type; propagate} = Condition.check cwt.cond in
| None -> report_issue_type |> Option.map ~f:(set_buffer_overrun_u5 cwt)
() |> Option.iter ~f:(report cwt.cond cwt.trace) ;
| Some issue_type -> propagate )
let issue_type = set_buffer_overrun_u5 cwt issue_type in
report cwt.cond cwt.trace issue_type )
let pp_cwt fmt cwt = F.fprintf fmt "%a %a" Condition.pp cwt.cond ConditionTrace.pp cwt.trace let pp_cwt fmt cwt = F.fprintf fmt "%a %a" Condition.pp cwt.cond ConditionTrace.pp cwt.trace

3
infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
Unescape View File

@ -34,8 +34,8 @@ codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRU
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN_L5, ERROR, [Call,Call,Assignment,Return,Assignment,Return,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN_L5, ERROR, [Call,Call,Assignment,Return,Assignment,Return,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, BUFFER_OVERRUN_S2, ERROR, [Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, BUFFER_OVERRUN_S2, ERROR, [Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_u_FP, 5, BUFFER_OVERRUN_S2, ERROR, [Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$8), -1+max(1, s$9)] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_u_FP, 5, BUFFER_OVERRUN_S2, ERROR, [Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$8), -1+max(1, s$9)] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, ERROR, [Call,Call,Call,Assignment,Call,Call,Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, ERROR, [Call,Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, ERROR, [Call,Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN_L1, ERROR, [Call,Parameter: newsize,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: i,ArrayAccess: Offset: [42, 42] Size: [42, 42] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call to `my_vector_oob_Bad()` ]
codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, ERROR, [Call,Call,ArrayDeclaration,Assignment,Parameter: i,ArrayAccess: Offset: [u$4, u$5] Size: [u$4, u$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call to `int_vector_access_at()` ] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, ERROR, [Call,Call,ArrayDeclaration,Assignment,Parameter: i,ArrayAccess: Offset: [u$4, u$5] Size: [u$4, u$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call to `int_vector_access_at()` ]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]] codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]] codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]]
@ -50,4 +50,5 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN
codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, 0] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/vector.cpp:206:3 by call to `access_minus_one()` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, 0] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/vector.cpp:206:3 by call to `access_minus_one()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [Call,Call,Assignment,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [1, 1] Size: [1, 1]] codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [Call,Call,Assignment,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [1, 1] Size: [1, 1]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, 0] Size: [0, 0]] codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, 0] Size: [0, 0]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, ERROR, [Call,Call,Assignment,Call,Call,Call]
codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, WARNING, [] codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, WARNING, []

Write Preview
Loading…
Cancel
Save