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

[inferbo] Add vector model: empty

Browse Source 
Summary:
It adds a model of vector::empty.

Depends on D16687269

Reviewed By: ezgicicek

Differential Revision: D16687280

fbshipit-source-id: 997a5faeb
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent c05062556f
commit 58b403c8ff
3 changed files with 31 additions and 16 deletions
Show Stats Download Patch File Download Diff File

29
infer/src/bufferoverrun/bufferOverrunModels.ml
Unescape View File

@ -567,6 +567,13 @@ module StdArray = struct
{exec; check= no_check}
end
let array_empty_exec ret_id array_v mem =
let traces = Dom.Val.get_traces array_v in
let size = ArrayBlk.sizeof (Dom.Val.get_array_blk array_v) in
let empty = Dom.Val.of_itv ~traces (Itv.of_bool (Itv.le_sem size Itv.zero)) in
model_by_value empty ret_id mem
module StdBasicString = struct
(* The (4) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
let constructor_from_char_ptr tgt src len =
@ -616,11 +623,8 @@ module StdBasicString = struct
let empty e =
let exec {integer_type_widths} ~ret:(ret_id, _) mem =
let v = Sem.eval integer_type_widths e mem in
let traces = Dom.Val.get_traces v in
let size = ArrayBlk.sizeof (Dom.Val.get_array_blk v) in
let empty = Dom.Val.of_itv ~traces (Itv.of_bool (Itv.le_sem size Itv.zero)) in
let mem = Dom.Mem.add_stack (Loc.of_id ret_id) empty mem in
let array_v = Sem.eval integer_type_widths e mem in
let mem = array_empty_exec ret_id array_v mem in
match e with
| Exp.Var id -> (
match Dom.Mem.find_simple_alias id mem with
@ -734,6 +738,20 @@ module StdVector = struct
Dom.Val.set_array_length location ~length:new_size v )
let empty vec_exp =
let exec _ ~ret:(id, _) mem =
let deref_of_vec = deref_of vec_exp mem in
let array_v = Dom.Mem.find_set deref_of_vec mem in
let mem = array_empty_exec id array_v mem in
match PowLoc.is_singleton_or_more deref_of_vec with
| IContainer.Singleton loc ->
Dom.Mem.load_empty_alias id loc mem
| IContainer.(Empty | More) ->
mem
in
{exec; check= no_check}
let push_back vec_exp elt_exp =
let exec model_env ~ret:_ mem =
let mem =
@ -1120,6 +1138,7 @@ module Call = struct
$+? any_arg $--> StdVector.constructor_copy
; -"std" &:: "vector" < any_typ &+ any_typ >:: "operator[]" $ capt_exp $+ capt_exp
$--> StdVector.at
; -"std" &:: "vector" < any_typ &+ any_typ >:: "empty" $ capt_exp $--> StdVector.empty
; -"std" &:: "vector" < any_typ &+ any_typ >:: "push_back" $ capt_exp $+ capt_exp
$--> StdVector.push_back
; -"std" &:: "vector" < any_typ &+ any_typ >:: "reserve" $ any_arg $+ any_arg $--> no_model

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

@ -107,12 +107,7 @@ codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string2_Good, 6, CONDITION_AL
codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc::symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `this->h[*]`,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/this.cpp, CThis::access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `this->n`,<Length trace>,Parameter `this->n`,Array declaration,Array access: Offset: this->n + 1 Size: this->n + 1]
codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access2_Good, 2, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Array declaration,Assignment,Call,Parameter `*v->vector_elem`,Allocation: Length: 0 by call to `safe_access2` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access4_Good, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*v->vector_elem`,Array access: Offset: 0 Size: 0 by call to `safe_access4` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access5_Good, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*v->vector_elem`,Array access: Offset: 0 Size: 0 by call to `safe_access5` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_data_Good, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: std::vector<int,std::allocator<int>>::data,Assignment,Array access: Offset: [-oo, +oo] (⇐ [-oo, +oo] + 4) Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access3_Good, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access6, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Offset trace>,Unknown value from: std::vector<int,std::allocator<int>>::empty,<Length trace>,Array declaration,Assignment,Array access: Offset: [-oo, +oo] Size: 2]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 6 Size: 5]
codetoanalyze/cpp/bufferoverrun/vector.cpp, constructor_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 3 Size: 1]
codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: std::vector<int,std::allocator<int>>::data,Assignment,Array access: Offset: [-oo, +oo] (⇐ [-oo, +oo] + [-oo, +oo]) Size: [0, +oo]]
@ -121,5 +116,6 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN
codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Array declaration,Call,Parameter `*init`,Assignment,Call,Parameter `*__param_0->a`,Assignment,Call,<Length trace>,Parameter `count`,Call,Parameter `idx`,Assignment,Array access: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/cpp/bufferoverrun/vector.cpp, simple_size_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Array declaration,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 3 Size: 3]
codetoanalyze/cpp/bufferoverrun/void_ptr.cpp, FP_call_casting_void_ptr_Ok, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*p`,Assignment,Array access: Offset: 14 Size: 2 by call to `casting_void_ptr` ]

12
infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp
Unescape View File

@ -80,12 +80,12 @@ void safe_access2(std::vector<int> v) {
}
}
void FP_call_safe_access2_Good() {
void call_safe_access2_Good() {
std::vector<int> v;
safe_access2(v);
}
void FP_safe_access3_Good() {
void safe_access3_Good() {
std::vector<int> v;
if (!v.empty()) {
v[0] = 1;
@ -98,7 +98,7 @@ void safe_access4(std::vector<int> v) {
}
}
void FP_call_safe_access4_Good() {
void call_safe_access4_Good() {
std::vector<int> v;
safe_access4(v);
}
@ -110,19 +110,19 @@ void safe_access5(std::vector<int> v) {
}
}
void FP_call_safe_access5_Good() {
void call_safe_access5_Good() {
std::vector<int> v;
safe_access5(v);
}
void FP_safe_access6(std::vector<int> v) {
void safe_access6(std::vector<int> v) {
std::vector<int> v2(2);
v2[v.empty()];
}
void call_safe_access6_Good() {
std::vector<int> v;
FP_safe_access6(v);
safe_access6(v);
}
void FP_data_Good() {

Write Preview
Loading…
Cancel
Save