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

[inferbo] Declare unsigned typed parameters

Browse Source 
Reviewed By: mbouaziz

Differential Revision: D5272681

fbshipit-source-id: 7edf251
master
Sungkeun Cho 8 years ago committed by Facebook Github Bot
parent 1f721d0824
commit 52c0caafaf
7 changed files with 27 additions and 16 deletions
Show Stats Download Patch File Download Diff File

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

@ -174,7 +174,10 @@ struct
in
let field = Loc.append_field loc fn in
match typ.Typ.desc with
| Typ.Tint _
| Typ.Tint ikind ->
let unsigned = Typ.ikind_is_unsigned ikind in
let v = Dom.Val.make_sym ~unsigned pname sym_num in
(Dom.Mem.add_heap field v mem, sym_num + 2)
| Typ.Tfloat _ ->
let v = Dom.Val.make_sym pname sym_num in
(Dom.Mem.add_heap field v mem, sym_num + 2)
@ -205,8 +208,9 @@ struct
let pname = Procdesc.get_proc_name pdesc in
let add_formal (mem, inst_num, sym_num) (pvar, typ) =
match typ.Typ.desc with
| Typ.Tint _ ->
let v = Dom.Val.make_sym pname sym_num in
| Typ.Tint ikind ->
let unsigned = Typ.ikind_is_unsigned ikind in
let v = Dom.Val.make_sym ~unsigned pname sym_num in
let mem = Dom.Mem.add_heap (Loc.of_pvar pvar) v mem in
(mem, inst_num + 1, sym_num + 2)
| Typ.Tptr (typ, _) ->

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

@ -274,8 +274,9 @@ struct
let modify_itv : Itv.t -> t -> t
= fun i x -> { x with itv = i }
let make_sym : Typ.Procname.t -> int -> t
= fun pname i -> { bot with itv = Itv.make_sym pname i }
let make_sym : ?unsigned:bool -> Typ.Procname.t -> int -> t
= fun ?(unsigned=false) pname i ->
{ bot with itv = Itv.make_sym ~unsigned pname i }
let unknown_bit : t -> t
= fun x -> { x with itv = Itv.top }

2
infer/src/bufferoverrun/bufferOverrunSemantics.ml
Unescape View File

@ -405,6 +405,8 @@ struct
if Int.equal coeff 1
then Itv.SubstMap.add symbol actual map
else assert false
| Itv.Bound.MinMax (Itv.Bound.Max, 0, symbol) ->
Itv.SubstMap.add symbol actual map
| _ -> assert false
in
List.fold ~f:add_pair ~init:Itv.SubstMap.empty pairs

15
infer/src/bufferoverrun/itv.ml
Unescape View File

@ -553,9 +553,14 @@ struct
let upper = Bound.of_sym (SymLinear.get_new pname) in
(lower, upper)
let make_sym : Typ.Procname.t -> int -> t
= fun pname i ->
let lower = Bound.of_sym (SymLinear.make pname i) in
let make_sym : unsigned:bool -> Typ.Procname.t -> int -> t
= fun ~unsigned pname i ->
let lower =
if unsigned then
Bound.MinMax (Bound.Max, 0, Symbol.make pname i)
else
Bound.of_sym (SymLinear.make pname i)
in
let upper = Bound.of_sym (SymLinear.make pname (i+1)) in
(lower, upper)
@ -963,8 +968,8 @@ let minus : t -> t -> t
let get_new_sym : Typ.Procname.t -> t
= fun pname -> NonBottom (ItvPure.get_new_sym pname)
let make_sym : Typ.Procname.t -> int -> t
= fun pname i -> NonBottom (ItvPure.make_sym pname i)
let make_sym : ?unsigned:bool -> Typ.Procname.t -> int -> t
= fun ?(unsigned=false) pname i -> NonBottom (ItvPure.make_sym ~unsigned pname i)
let neg : t -> t
= lift1 ItvPure.neg

2
infer/tests/codetoanalyze/c/bufferoverrun/arith.c
Unescape View File

@ -39,7 +39,7 @@ void modulo_signed_Good2(int i) {
}
}
void modulo_unsigned_Good_FP(unsigned int i) {
void modulo_unsigned_Good(unsigned int i) {
char arr[5];
arr[i % 5] = 123;
}

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

@ -1,6 +1,5 @@
codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN, [Offset: [-4, 4] Size: [5, 5]]
codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN, [Offset: [-4, 4] Size: [5, 5]]
codetoanalyze/c/bufferoverrun/arith.c, modulo_unsigned_Good_FP, 2, BUFFER_OVERRUN, [Offset: [-4, 4] Size: [5, 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, 4, CONDITION_ALWAYS_TRUE, []
codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, []

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

@ -1,13 +1,13 @@
codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<LMB<TFM>*,std::allocator<LMB<TFM>*>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<LMB<TFM>*,std::allocator<LMB<TFM>*>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `ral()` ]
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/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Offset: [0, +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: [max(0, s$6), s$7] Size: [max(0, 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/vector.cpp, constructor_Good_FP, 2, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<Int_no_copy,std::allocator<Int_no_copy>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_at()` ]
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:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [Offset: [max(0, s$14), s$15] Size: [max(0, s$14), s$15] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Good_FP, 3, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]

Write Preview
Loading…
Cancel
Save