From 52c0caafaff36ba5508b685db012e79477a4b2fa Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 19 Jun 2017 19:59:33 -0700 Subject: [PATCH] [inferbo] Declare unsigned typed parameters Reviewed By: mbouaziz Differential Revision: D5272681 fbshipit-source-id: 7edf251 --- infer/src/bufferoverrun/bufferOverrunChecker.ml | 10 +++++++--- infer/src/bufferoverrun/bufferOverrunDomain.ml | 5 +++-- infer/src/bufferoverrun/bufferOverrunSemantics.ml | 2 ++ infer/src/bufferoverrun/itv.ml | 15 ++++++++++----- infer/tests/codetoanalyze/c/bufferoverrun/arith.c | 2 +- .../codetoanalyze/c/bufferoverrun/issues.exp | 1 - .../codetoanalyze/cpp/bufferoverrun/issues.exp | 8 ++++---- 7 files changed, 27 insertions(+), 16 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 28f052c9d..48650078a 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -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, _) -> diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index fe77fd588..9ed813e80 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -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 } diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index ff0bcbe83..075448a3a 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -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 diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 715d83955..2754383ae 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index f69042a29..0b38ac5a1 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -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; } diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 522e4c97e..a5aca49c7 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -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, [] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 2769c99f8..b1df493ee 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -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_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*,std::allocator*>>_operator[]()` ] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_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*,std::allocator*>>_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>_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>_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>_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>_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>_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>_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>_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>_operator[]()` ]