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

[inferbo] Use std::vector model for std::string

Browse Source 
Summary:
This diff uses the models of vector for modelling string in Cpp.

Depends on D16963153

Reviewed By: ezgicicek

Differential Revision: D16963166

fbshipit-source-id: 5effe2d72
master
Sungkeun Cho 5 years ago committed by Facebook Github Bot
parent 9e5115a9e0
commit 59f06568cf
3 changed files with 81 additions and 83 deletions
Show Stats Download Patch File Download Diff File

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

@ -770,9 +770,9 @@ end
inside the if branch.
"AliasTarget.Empty relation": For pruning vector.length with vector::empty() results, we adopt a
specific relation between %r and v, where %r=v.empty(). So, if %r!=0, v's array length
([v.length]) is pruned by v.length=0. On the other hand, if %r==0, v's array length is pruned by
v.length>=1.
specific relation between %r and v->elements, where %r=v.empty(). So, if %r!=0, v's array length
([v->elements->length]) is pruned by 0. On the other hand, if %r==0, v's array length is pruned
by >=1.
"AliasTarget.Nullity relation": For pruning vector.length with vector::empty() results, we adopt
a specific relation between %r and i, where %r=v.empty() and i=v.length. So, if %r!=0, i is

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

@ -497,6 +497,14 @@ module CFArray = struct
let at (array_exp, _) (index_exp, _) = at ?size:None array_exp index_exp
let length e =
let exec {integer_type_widths} ~ret:(ret_id, _) mem =
let v = Sem.eval_arr integer_type_widths e mem in
let length = Dom.Val.of_itv (ArrayBlk.sizeof (Dom.Val.get_array_blk v)) in
Dom.Mem.add_stack (Loc.of_id ret_id) length mem
in
{exec; check= no_check}
end
module Split = struct
@ -577,13 +585,6 @@ 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 StdVector = struct
let append_field loc ~vec_typ ~elt_typ =
Loc.append_field loc ~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ)
@ -668,7 +669,10 @@ module StdVector = struct
let exec model_env ~ret:(id, _) mem =
let deref_of_vec = deref_of model_env elt_typ vec_arg mem in
let array_v = Dom.Mem.find_set deref_of_vec mem in
let mem = array_empty_exec id array_v mem in
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
let mem = model_by_value empty id mem in
match PowLoc.is_singleton_or_more deref_of_vec with
| IContainer.Singleton loc ->
Dom.Mem.load_empty_alias id loc mem
@ -710,76 +714,58 @@ module StdVector = struct
end
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 =
let {exec= malloc_exec; check= malloc_check} = malloc ~can_be_zero:true len in
let exec model_env ~ret:((ret_id, _) as ret) mem =
let mem = malloc_exec model_env ~ret mem in
let v = Dom.Mem.find (Loc.of_id ret_id) mem in
let mem = Dom.Mem.update_mem (Sem.eval_locs tgt mem) v mem in
let contents =
let src_locs = Sem.eval_locs src mem in
Dom.Mem.find_set src_locs mem
let constructor_from_char_ptr_common char_typ (tgt_exp, tgt_typ) src ~len_opt =
let exec ({pname; node_hash; integer_type_widths} as model_env) ~ret mem =
let mem =
Option.value_map len_opt ~default:mem ~f:(fun len ->
let {exec= malloc_exec} = malloc ~can_be_zero:true len in
malloc_exec model_env ~ret mem )
in
let tgt_locs = Sem.eval_locs tgt_exp mem in
let tgt_deref =
let allocsite =
Allocsite.make pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None
~represents_multiple_values:false
in
PowLoc.singleton (Loc.of_allocsite allocsite)
in
Dom.Mem.update_mem (Dom.Val.get_all_locs v) contents mem
let mem =
Dom.Mem.update_mem tgt_locs (Dom.Val.of_pow_loc ~traces:Trace.Set.bottom tgt_deref) mem
in
let elem_locs = StdVector.append_fields ~vec_typ:tgt_typ ~elt_typ:char_typ tgt_deref in
match src with
| Exp.Const (Const.Cstr s) ->
BoUtils.Exec.decl_string model_env ~do_alloc:true elem_locs s mem
| _ ->
let v = Sem.eval integer_type_widths src mem in
Dom.Mem.update_mem elem_locs v mem
in
let check ({location; integer_type_widths} as model_env) mem cond_set =
let cond_set = malloc_check model_env mem cond_set in
BoUtils.Check.lindex integer_type_widths ~array_exp:src ~index_exp:len ~last_included:true
mem location cond_set
Option.value_map len_opt ~default:cond_set ~f:(fun len ->
let {check= malloc_check} = malloc ~can_be_zero:true len in
let cond_set = malloc_check model_env mem cond_set in
BoUtils.Check.lindex integer_type_widths ~array_exp:src ~index_exp:len
~last_included:true mem location cond_set )
in
{exec; check}
(* The (5) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
let constructor_from_char_ptr_without_len tgt src =
let exec ({integer_type_widths} as model_env) ~ret:_ mem =
match src with
| Exp.Const (Const.Cstr s) ->
let locs = Sem.eval_locs tgt mem in
BoUtils.Exec.decl_string model_env ~do_alloc:true locs s mem
| _ ->
let tgt_locs = Sem.eval_locs tgt mem in
let v = Sem.eval integer_type_widths src mem in
Dom.Mem.update_mem tgt_locs v mem
in
{exec; check= no_check}
(* The (4) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
let constructor_from_char_ptr char_typ (tgt_exp, tgt_typ) src len =
constructor_from_char_ptr_common char_typ (tgt_exp, tgt_typ) src ~len_opt:(Some len)
(* The (7) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
let copy_constructor tgt src =
let exec _ ~ret:_ mem =
let tgt_locs = Sem.eval_locs tgt mem in
let v = Dom.Mem.find_set (Sem.eval_locs src mem) mem in
Dom.Mem.update_mem tgt_locs v mem
in
{exec; check= no_check}
(* The (5) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
let constructor_from_char_ptr_without_len char_typ (tgt_exp, tgt_typ) src =
constructor_from_char_ptr_common char_typ (tgt_exp, tgt_typ) src ~len_opt:None
let empty e =
let exec {integer_type_widths} ~ret:(ret_id, _) mem =
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
| Some (l, None) ->
Dom.Mem.load_empty_alias ret_id l mem
| _ ->
mem )
| _ ->
mem
in
{exec; check= no_check}
(* The (7) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
let copy_constructor = StdVector.constructor_copy
let empty = StdVector.empty
let length e =
let exec {integer_type_widths} ~ret:(ret_id, _) mem =
let v = Sem.eval_arr integer_type_widths e mem in
let length = Dom.Val.of_itv (ArrayBlk.sizeof (Dom.Val.get_array_blk v)) in
Dom.Mem.add_stack (Loc.of_id ret_id) length mem
in
{exec; check= no_check}
let length = StdVector.size
end
(** Java's integers are modeled with an indirection to a memory
@ -1039,9 +1025,9 @@ module Call = struct
; -"__exit" <>--> bottom
; -"CFArrayCreate" <>$ any_arg $+ capt_exp $+ capt_exp $+...$--> CFArray.create_array
; -"CFArrayCreateCopy" <>$ any_arg $+ capt_exp $!--> create_copy_array
; -"MCFArrayGetCount" <>$ capt_exp $!--> StdBasicString.length
; -"CFDictionaryGetCount" <>$ capt_exp $!--> StdBasicString.length
; -"CFArrayGetCount" <>$ capt_exp $!--> StdBasicString.length
; -"MCFArrayGetCount" <>$ capt_exp $!--> CFArray.length
; -"CFDictionaryGetCount" <>$ capt_exp $!--> CFArray.length
; -"CFArrayGetCount" <>$ capt_exp $!--> CFArray.length
; -"CFArrayGetValueAtIndex" <>$ capt_arg $+ capt_arg $!--> CFArray.at
; -"exit" <>--> bottom
; -"__cast" <>$ capt_exp $+ capt_exp $+...$--> cast
@ -1102,17 +1088,29 @@ module Call = struct
; std_array2 >:: "at" $ capt_arg $+ capt_arg $!--> StdArray.at
; std_array2 >:: "operator[]" $ capt_arg $+ capt_arg $!--> StdArray.at
; -"std" &:: "array" &::.*--> no_model
; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp
; -"std" &:: "basic_string"
< capt_typ `T
&+...>:: "basic_string" $ capt_arg
$+ capt_exp_of_typ (-"std" &:: "basic_string")
$--> StdBasicString.copy_constructor
; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp $+ capt_exp_of_prim_typ char_ptr
; -"std" &:: "basic_string"
< capt_typ `T
&+...>:: "basic_string" $ capt_arg $+ capt_exp_of_prim_typ char_ptr
$--> StdBasicString.constructor_from_char_ptr_without_len
; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp $+ capt_exp_of_prim_typ char_ptr
; -"std" &:: "basic_string"
< capt_typ `T
&+...>:: "basic_string" $ capt_arg $+ capt_exp_of_prim_typ char_ptr
$+ capt_exp_of_prim_typ (Typ.mk (Typ.Tint Typ.size_t))
$--> StdBasicString.constructor_from_char_ptr
; -"std" &:: "basic_string" &:: "empty" $ capt_exp $--> StdBasicString.empty
; -"std" &:: "basic_string" &:: "length" $ capt_exp $--> StdBasicString.length
; -"std" &:: "basic_string" &:: "size" $ capt_exp $--> StdBasicString.length
; -"std" &:: "basic_string"
< capt_typ `T
&+...>:: "empty" $ capt_arg $--> StdBasicString.empty
; -"std" &:: "basic_string"
< capt_typ `T
&+...>:: "length" $ capt_arg $--> StdBasicString.length
; -"std" &:: "basic_string"
< capt_typ `T
&+...>:: "size" $ capt_arg $--> StdBasicString.length
; -"std" &:: "basic_string" &:: "compare" &--> by_value Dom.Val.Itv.top
; +PatternMatch.implements_lang "String"
&:: "equals"

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

@ -85,8 +85,8 @@ codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INTEGER_OVERFLOW
codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_contents_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, call_length4_1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Array declaration,Array access: Offset: 11 Size: 10 by call to `length4` ]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, call_length4_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Length trace>,Array declaration,Array access: Offset: 11 Size: 10 by call to `length4` ]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, call_length4_1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `*c`,<Length trace>,Array declaration,Array access: Offset: 11 Size: 10 by call to `length4` ]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, call_length4_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `*c`,<Length trace>,Array declaration,Array access: Offset: 11 Size: 10 by call to `length4` ]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, compare_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, compare_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, empty_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
@ -96,10 +96,10 @@ codetoanalyze/cpp/bufferoverrun/std_string.cpp, equal_Bad, 5, BUFFER_OVERRUN_L1,
codetoanalyze/cpp/bufferoverrun/std_string.cpp, equal_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char1_Bad, 3, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: snprintf,Assignment,<Length trace>,Array declaration,Array access: Offset: [-1, +oo] Size: 1024]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char2_Bad, 6, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: vsnprintf,Assignment,<Length trace>,Array declaration,Array access: Offset: [-1, +oo] Size: 1024]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, length2_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 11 Size: 10]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, length3_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 11 Size: 10]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, length_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 11 Size: 10]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, size_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 11 Size: 10]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, length2_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: 11 Size: 10]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, length3_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: 11 Size: 10]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, length_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: 11 Size: 10]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, size_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: 11 Size: 10]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string1_Bad, 3, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: snprintf,Assignment,<Length trace>,Array declaration,Array access: Offset added: [0, +oo] Size: 1024]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string1_Good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string2_Bad, 6, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: vsnprintf,Assignment,<Length trace>,Array declaration,Array access: Offset added: [0, +oo] Size: 1024]

Write Preview
Loading…
Cancel
Save