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

[inferbo] Prepare for several kinds of safety conditions

Browse Source 
Reviewed By: jvillard

Differential Revision: D6373063

fbshipit-source-id: ef7cd35
master
Mehdi Bouaziz 7 years ago committed by Facebook Github Bot
parent cb363d8dcb
commit d12371c6c3
2 changed files with 66 additions and 35 deletions
Show Stats Download Patch File Download Diff File

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

@ -541,35 +541,30 @@ module Report = struct
let report_error : Procdesc.t -> PO.ConditionSet.t -> unit =
fun pdesc conds ->
fun pdesc cond_set ->
let pname = Procdesc.get_proc_name pdesc in
let report1 cond trace =
let alarm = PO.Condition.check cond in
match alarm with
| None ->
()
| Some issue_type ->
let caller_pname, location =
match PO.ConditionTrace.get_cond_trace trace with
| PO.ConditionTrace.Inter (caller_pname, _, location) ->
(caller_pname, location)
| PO.ConditionTrace.Intra pname ->
(pname, PO.ConditionTrace.get_location trace)
in
if Typ.Procname.equal pname caller_pname then
let description = PO.description cond trace in
let error_desc = Localise.desc_buffer_overrun description in
let exn = Exceptions.Checkers (issue_type.IssueType.unique_id, error_desc) in
let trace =
match TraceSet.choose_shortest trace.PO.ConditionTrace.val_traces with
| trace ->
make_err_trace trace description
| exception _ ->
[Errlog.make_trace_element 0 location description []]
in
Reporting.log_error_deprecated pname ~loc:location ~ltr:trace exn
let report cond trace issue_type =
let caller_pname, location =
match PO.ConditionTrace.get_cond_trace trace with
| PO.ConditionTrace.Inter (caller_pname, _, location) ->
(caller_pname, location)
| PO.ConditionTrace.Intra pname ->
(pname, PO.ConditionTrace.get_location trace)
in
if Typ.Procname.equal pname caller_pname then
let description = PO.description cond trace in
let error_desc = Localise.desc_buffer_overrun description in
let exn = Exceptions.Checkers (issue_type.IssueType.unique_id, error_desc) in
let trace =
match TraceSet.choose_shortest trace.PO.ConditionTrace.val_traces with
| trace ->
make_err_trace trace description
| exception _ ->
[Errlog.make_trace_element 0 location description []]
in
Reporting.log_error_deprecated pname ~loc:location ~ltr:trace exn
in
PO.ConditionSet.iter conds ~f:report1
PO.ConditionSet.check_all ~report cond_set
end

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

@ -15,7 +15,7 @@ module ItvPure = Itv.ItvPure
module MF = MarkupFormatter
module ValTraceSet = BufferOverrunTrace.Set
module Condition = struct
module ArrayAccessCondition = struct
type t = {idx: ItvPure.astate; size: ItvPure.astate} [@@deriving compare]
let get_symbols c = ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size
@ -149,8 +149,8 @@ module Condition = struct
else Some IssueType.buffer_overrun_l3
let subst : t -> Itv.Bound.t bottom_lifted Itv.SubstMap.t -> t option =
fun c bound_map ->
let subst : Itv.Bound.t bottom_lifted Itv.SubstMap.t -> t -> t option =
fun bound_map c ->
match (ItvPure.subst c.idx bound_map, ItvPure.subst c.size bound_map) with
| NonBottom idx, NonBottom size ->
Some {idx; size}
@ -159,6 +159,35 @@ module Condition = struct
end
module Condition = struct
type t = ArrayAccess of ArrayAccessCondition.t [@@deriving compare]
let make_array_access = Option.map ~f:(fun c -> ArrayAccess c)
let get_symbols = function ArrayAccess c -> ArrayAccessCondition.get_symbols c
let subst bound_map = function
| ArrayAccess c ->
ArrayAccessCondition.subst bound_map c |> make_array_access
let have_similar_bounds c1 c2 =
match (c1, c2) with ArrayAccess c1, ArrayAccess c2 ->
ArrayAccessCondition.have_similar_bounds c1 c2
let xcompare ~lhs ~rhs =
match (lhs, rhs) with ArrayAccess lhs, ArrayAccess rhs ->
ArrayAccessCondition.xcompare ~lhs ~rhs
let pp fmt = function ArrayAccess c -> ArrayAccessCondition.pp fmt c
let pp_description fmt = function ArrayAccess c -> ArrayAccessCondition.pp_description fmt c
let check = function ArrayAccess c -> ArrayAccessCondition.check c
end
module ConditionTrace = struct
type cond_trace =
| Intra of Typ.Procname.t
@ -238,14 +267,14 @@ module ConditionSet = struct
let try_merge ~existing ~new_ =
(* we don't want to remove issues that would end up in a higher bucket,
e.g. [a, b] < [c, d] is subsumed by [a, +oo] < [c, d] but the latter is less precise *)
if Condition.have_similar_bounds existing.cond new_.cond then
match Condition.xcompare ~lhs:existing.cond ~rhs:new_.cond with
| `Equal ->
(* keep the first one in the code *)
if compare_by_location existing new_ <= 0 then `DoNotAddAndStop
else `RemoveExistingAndContinue
(* we don't want to remove issues that would end up in a higher bucket,
e.g. [a, b] < [c, d] is subsumed by [a, +oo] < [c, d] but the latter is less precise *)
| `LeftSubsumesRight ->
`DoNotAddAndStop
| `RightSubsumesLeft ->
@ -274,7 +303,7 @@ module ConditionSet = struct
let join condset1 condset2 = List.fold_left ~f:add_one condset1 ~init:condset2
let add_bo_safety pname location id ~idx ~size val_traces condset =
match Condition.make ~idx ~size with
match ArrayAccessCondition.make ~idx ~size |> Condition.make_array_access with
| None ->
condset
| Some cond ->
@ -293,7 +322,7 @@ module ConditionSet = struct
| [] ->
add_one condset cwt
| symbols ->
match Condition.subst cwt.cond bound_map with
match Condition.subst bound_map cwt.cond with
| None ->
condset
| Some cond ->
@ -315,7 +344,14 @@ module ConditionSet = struct
List.fold condset ~f:subst_add_cwt ~init:[]
let iter ~f condset = List.iter condset ~f:(fun cwt -> f cwt.cond cwt.trace)
let check_all ~report condset =
List.iter condset ~f:(fun cwt ->
match Condition.check cwt.cond with
| None ->
()
| Some issue_type ->
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

Write Preview
Loading…
Cancel
Save