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

[Inferbo] remove redundant alarm message

Browse Source 
Summary:
This diff removes redundant alarm message of intra-procedural
alarms from Inferbo.

Reviewed By: mbouaziz

Differential Revision: D5154319

fbshipit-source-id: bc1c827
master
Kihong Heo 8 years ago committed by Facebook Github Bot
parent cc6b0f1e0b
commit 485814a75a
5 changed files with 153 additions and 146 deletions
Show Stats Download Patch File Download Diff File

9
infer/src/IR/Location.re
Unescape View File

@ -31,6 +31,7 @@ let none file => {line: (-1), col: (-1), file};
let dummy = none (SourceFile.invalid __FILE__);
/** Pretty print a location */
let pp f (loc: t) => F.fprintf f "[line %d]" loc.line;
@ -42,3 +43,11 @@ let to_string loc => {
s
}
};
/** Pretty print a file-position of a location */
let pp_file_pos f (loc: t) => {
let fname = SourceFile.to_string loc.file;
let pos = to_string loc;
F.fprintf f "%s:%s" fname pos
};

4
infer/src/IR/Location.rei
Unescape View File

@ -38,3 +38,7 @@ let pp: Format.formatter => t => unit;
/** String representation of a location. */
let to_string: t => string;
/** Pretty print a file-position of a location */
let pp_file_pos: Format.formatter => t => unit;

250
infer/src/bufferoverrun/bufferOverrunDomain.ml
Unescape View File

@ -21,6 +21,10 @@ let always_strong_update = true (* unsound but ok for bug catching *)
module Condition =
struct
type trace = Intra of Typ.Procname.t
| Inter of Typ.Procname.t * Typ.Procname.t * Location.t
[@@deriving compare]
type t = {
proc_name : Typ.Procname.t;
loc : Location.t;
@ -30,134 +34,124 @@ struct
size : Itv.astate;
}
[@@deriving compare]
and trace = Intra of Typ.Procname.t
| Inter of Typ.Procname.t * Typ.Procname.t * Location.t
[@@deriving compare]
and astate = t
let set_size_pos : t -> t
= fun c ->
if Itv.Bound.lt (Itv.lb c.size) Itv.Bound.zero
then { c with size = Itv.make Itv.Bound.zero (Itv.ub c.size) }
else c
let string_of_location : Location.t -> string
= fun loc ->
let fname = SourceFile.to_string loc.Location.file in
let pos = Location.to_string loc in
F.fprintf F.str_formatter "%s:%s" fname pos;
F.flush_str_formatter ()
let pp_location : F.formatter -> t -> unit
= fun fmt c ->
F.fprintf fmt "%s" (string_of_location c.loc)
let pp : F.formatter -> t -> unit
= fun fmt c ->
let c = set_size_pos c in
if Config.bo_debug <= 1 then
F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c
else
match c.trace with
Inter (_, pname, loc) ->
let pname = Typ.Procname.to_string pname in
F.fprintf fmt "%a < %a at %a by call %s() at %s"
Itv.pp c.idx Itv.pp c.size pp_location c pname (string_of_location loc)
| Intra _ -> F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c
let get_location : t -> Location.t
= fun c -> c.loc
let get_trace : t -> trace
= fun c -> c.trace
let get_proc_name : t -> Typ.Procname.t
= fun c -> c.proc_name
let make : Typ.Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t
= fun proc_name loc id ~idx ~size ->
{ proc_name; idx; size; loc; id ; trace = Intra proc_name }
let filter1 : t -> bool
= fun c ->
Itv.eq c.idx Itv.top || Itv.eq c.size Itv.top
|| Itv.Bound.eq (Itv.lb c.idx) Itv.Bound.MInf
|| Itv.Bound.eq (Itv.lb c.size) Itv.Bound.MInf
|| (Itv.eq c.idx Itv.nat && Itv.eq c.size Itv.nat)
let filter2 : t -> bool
= fun c ->
(* basically, alarms involving infinity are filtered *)
(not (Itv.is_finite c.idx) || not (Itv.is_finite c.size))
&& (* except the following cases *)
not ((Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb < 0 *)
Itv.Bound.lt (Itv.lb c.idx) Itv.Bound.zero)
||
(Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb > size lb *)
(Itv.Bound.gt (Itv.lb c.idx) (Itv.lb c.size)))
||
(Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb > size ub *)
(Itv.Bound.gt (Itv.lb c.idx) (Itv.ub c.size)))
||
(Itv.Bound.is_not_infty (Itv.ub c.idx) && (* idx non-infty ub > size lb *)
(Itv.Bound.gt (Itv.ub c.idx) (Itv.lb c.size)))
||
(Itv.Bound.is_not_infty (Itv.ub c.idx) && (* idx non-infty ub > size ub *)
(Itv.Bound.gt (Itv.ub c.idx) (Itv.ub c.size))))
(* check buffer overrun and return its confidence *)
let check : t -> string option
= fun c ->
(* idx = [il, iu], size = [sl, su], we want to check that 0 <= idx < size *)
let c' = set_size_pos c in (* if sl < 0, use sl' = 0 *)
let not_overrun = Itv.lt_sem c'.idx c'.size in
let not_underrun = Itv.le_sem Itv.zero c'.idx in
(* il >= 0 and iu < sl, definitely not an error *)
if Itv.eq not_overrun Itv.one && Itv.eq not_underrun Itv.one then
None
(* iu < 0 or il >= su, definitely an error *)
else if Itv.eq not_overrun Itv.zero || Itv.eq not_underrun Itv.zero then
Some Localise.BucketLevel.b1
(* su <= iu < +oo, most probably an error *)
else if Itv.Bound.is_not_infty (Itv.ub c.idx)
&& Itv.Bound.le (Itv.ub c.size) (Itv.ub c.idx) then
Some Localise.BucketLevel.b2
(* symbolic il >= sl, probably an error *)
else if Itv.Bound.is_symbolic (Itv.lb c.idx)
&& Itv.Bound.le (Itv.lb c'.size) (Itv.lb c.idx) then
Some Localise.BucketLevel.b3
(* other symbolic bounds are probably too noisy *)
else if Config.bo_debug <= 3 && (Itv.is_symbolic c.idx || Itv.is_symbolic c.size) then
None
else if filter1 c then
Some Localise.BucketLevel.b5
else if filter2 c then
Some Localise.BucketLevel.b3
else
Some Localise.BucketLevel.b2
let invalid : t -> bool
= fun x -> Itv.invalid x.idx || Itv.invalid x.size
let to_string : t -> string
= fun c ->
let c = set_size_pos c in
"Offset: " ^ Itv.to_string c.idx ^ " Size: " ^ Itv.to_string c.size
^ " @ " ^ string_of_location c.loc
^ (match c.trace with
Inter (_, pname, _) ->
" by call "
^ MF.monospaced_to_string (Typ.Procname.to_string pname ^ "()") ^ " "
| Intra _ -> "")
let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> t
= fun c subst_map caller_pname callee_pname loc ->
if Itv.is_symbolic c.idx || Itv.is_symbolic c.size then
{ c with idx = Itv.subst c.idx subst_map;
size = Itv.subst c.size subst_map;
trace = Inter (caller_pname, callee_pname, loc) }
else c
type astate = t
let set_size_pos : t -> t
= fun c ->
if Itv.Bound.lt (Itv.lb c.size) Itv.Bound.zero
then { c with size = Itv.make Itv.Bound.zero (Itv.ub c.size) }
else c
let pp_location : F.formatter -> t -> unit
= fun fmt c ->
Location.pp_file_pos fmt c.loc
let pp : F.formatter -> t -> unit
= fun fmt c ->
let c = set_size_pos c in
if Config.bo_debug <= 1 then
F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c
else
match c.trace with
Inter (_, pname, loc) ->
let pname = Typ.Procname.to_string pname in
F.fprintf fmt "%a < %a at %a by call %s() at %a"
Itv.pp c.idx Itv.pp c.size pp_location c pname Location.pp_file_pos loc
| Intra _ -> F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c
let get_location : t -> Location.t
= fun c -> c.loc
let get_trace : t -> trace
= fun c -> c.trace
let get_proc_name : t -> Typ.Procname.t
= fun c -> c.proc_name
let make : Typ.Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t
= fun proc_name loc id ~idx ~size ->
{ proc_name; idx; size; loc; id ; trace = Intra proc_name }
let filter1 : t -> bool
= fun c ->
Itv.eq c.idx Itv.top || Itv.eq c.size Itv.top
|| Itv.Bound.eq (Itv.lb c.idx) Itv.Bound.MInf
|| Itv.Bound.eq (Itv.lb c.size) Itv.Bound.MInf
|| (Itv.eq c.idx Itv.nat && Itv.eq c.size Itv.nat)
let filter2 : t -> bool
= fun c ->
(* basically, alarms involving infinity are filtered *)
(not (Itv.is_finite c.idx) || not (Itv.is_finite c.size))
&& (* except the following cases *)
not ((Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb < 0 *)
Itv.Bound.lt (Itv.lb c.idx) Itv.Bound.zero)
||
(Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb > size lb *)
(Itv.Bound.gt (Itv.lb c.idx) (Itv.lb c.size)))
||
(Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb > size ub *)
(Itv.Bound.gt (Itv.lb c.idx) (Itv.ub c.size)))
||
(Itv.Bound.is_not_infty (Itv.ub c.idx) && (* idx non-infty ub > size lb *)
(Itv.Bound.gt (Itv.ub c.idx) (Itv.lb c.size)))
||
(Itv.Bound.is_not_infty (Itv.ub c.idx) && (* idx non-infty ub > size ub *)
(Itv.Bound.gt (Itv.ub c.idx) (Itv.ub c.size))))
(* check buffer overrun and return its confidence *)
let check : t -> string option
= fun c ->
(* idx = [il, iu], size = [sl, su], we want to check that 0 <= idx < size *)
let c' = set_size_pos c in (* if sl < 0, use sl' = 0 *)
let not_overrun = Itv.lt_sem c'.idx c'.size in
let not_underrun = Itv.le_sem Itv.zero c'.idx in
(* il >= 0 and iu < sl, definitely not an error *)
if Itv.eq not_overrun Itv.one && Itv.eq not_underrun Itv.one then
None
(* iu < 0 or il >= su, definitely an error *)
else if Itv.eq not_overrun Itv.zero || Itv.eq not_underrun Itv.zero then
Some Localise.BucketLevel.b1
(* su <= iu < +oo, most probably an error *)
else if Itv.Bound.is_not_infty (Itv.ub c.idx)
&& Itv.Bound.le (Itv.ub c.size) (Itv.ub c.idx) then
Some Localise.BucketLevel.b2
(* symbolic il >= sl, probably an error *)
else if Itv.Bound.is_symbolic (Itv.lb c.idx)
&& Itv.Bound.le (Itv.lb c'.size) (Itv.lb c.idx) then
Some Localise.BucketLevel.b3
(* other symbolic bounds are probably too noisy *)
else if Config.bo_debug <= 3 && (Itv.is_symbolic c.idx || Itv.is_symbolic c.size) then
None
else if filter1 c then
Some Localise.BucketLevel.b5
else if filter2 c then
Some Localise.BucketLevel.b3
else
Some Localise.BucketLevel.b2
let invalid : t -> bool
= fun x -> Itv.invalid x.idx || Itv.invalid x.size
let to_string : t -> string
= fun c ->
let c = set_size_pos c in
"Offset: " ^ Itv.to_string c.idx ^ " Size: " ^ Itv.to_string c.size
^ (match c.trace with
| Inter (_, pname, _) ->
let loc = pp_location F.str_formatter c; F.flush_str_formatter () in
" @ " ^ loc ^ " by call "
^ MF.monospaced_to_string (Typ.Procname.to_string pname ^ "()") ^ " "
| Intra _ -> "")
let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> t
= fun c subst_map caller_pname callee_pname loc ->
if Itv.is_symbolic c.idx || Itv.is_symbolic c.size then
{ c with idx = Itv.subst c.idx subst_map;
size = Itv.subst c.size subst_map;
trace = Inter (caller_pname, callee_pname, loc) }
else c
end
module ConditionSet =

32
infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
Unescape View File

@ -1,20 +1,20 @@
codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN, [Offset: [3xs$0 + 1, 3xs$1 + 1] Size: [3xs$0 + 1, 3xs$1 + 1] @ codetoanalyze/c/bufferoverrun/array_dynlength.c:13:3]
codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/break_continue_return.c:29:5]
codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN, [Offset: [3xs$0 + 1, 3xs$1 + 1] Size: [3xs$0 + 1, 3xs$1 + 1]]
codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10]]
codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ]
codetoanalyze/c/bufferoverrun/do_while.c, do_while, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ]
codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN, [Offset: [0, 9] Size: [5, 10] @ codetoanalyze/c/bufferoverrun/for_loop.c:38:5]
codetoanalyze/c/bufferoverrun/function_call.c, call_by_ptr_good_FP, 4, BUFFER_OVERRUN, [Offset: [99, 99] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:36:3]
codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN, [Offset: [0, 9] Size: [5, 10]]
codetoanalyze/c/bufferoverrun/function_call.c, call_by_ptr_good_FP, 4, BUFFER_OVERRUN, [Offset: [99, 99] Size: [10, 10]]
codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [20, 20] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:18:3 by call `arr_access()` ]
codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [100, 100] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:17:3 by call `arr_access()` ]
codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/global.c:14:5]
codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offset: [10, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/goto_loop.c:24:3]
codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN, [Offset: [0, 255] Size: [255, 255] @ codetoanalyze/c/bufferoverrun/models.c:29:5]
codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN, [Offset: [-1, 255] Size: [10000, 10000] @ codetoanalyze/c/bufferoverrun/models.c:22:3]
codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop.c:20:7]
codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c:19:5]
codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/pointer_arith.c:14:5]
codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/prune_alias.c:107:5]
codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, 0] @ codetoanalyze/c/bufferoverrun/sizeof.c:16:5]
codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, 0] @ codetoanalyze/c/bufferoverrun/sizeof.c:32:5]
codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/trivial.c:15:3]
codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/while_loop.c:16:10]
codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]]
codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offset: [10, +oo] Size: [10, 10]]
codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN, [Offset: [0, 255] Size: [255, 255]]
codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN, [Offset: [-1, 255] Size: [10000, 10000]]
codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10]]
codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10]]
codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]]
codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [1, 1]]
codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, 0]]
codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, 0]]
codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]]
codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10]]

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

@ -1,5 +1,5 @@
codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_good_FP, 4, BUFFER_OVERRUN, [Offset: [99, 99] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/function_call.cpp:18:3]
codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_good_FP, 4, BUFFER_OVERRUN, [Offset: [99, 99] Size: [10, 10]]
codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ]
codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN, [Offset: [s$6, s$7] Size: [s$6, s$7] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ]
codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/trivial.cpp:15:3]
codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [Offset: [s$14, s$15] Size: [s$14, s$15] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:91:24 by call `std::vector<int,std::allocator<int>>_operator[]()` ]

Write Preview
Loading…
Cancel
Save