From b4683d965d071dbf4d6cd0866d32c14ba05f5c40 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 20 Nov 2018 23:25:03 -0800 Subject: [PATCH] [inferbo] Resize array on casting Summary: It modifies sizes and offsets of array values on pointer castings. Currently, it supports only simple castings of pointer-to-integers. Reviewed By: mbouaziz Differential Revision: D12920589 fbshipit-source-id: a5ba831b8 --- infer/src/bufferoverrun/arrayBlk.ml | 14 ++++++++++++++ infer/src/bufferoverrun/bounds.ml | 9 ++++----- infer/src/bufferoverrun/bounds.mli | 2 ++ .../src/bufferoverrun/bufferOverrunDomain.ml | 7 +++++++ .../bufferoverrun/bufferOverrunSemantics.ml | 19 +++++++++++++++---- infer/src/bufferoverrun/itv.ml | 18 ++++++++++++++++-- infer/src/bufferoverrun/itv.mli | 8 ++++++++ .../c/bufferoverrun/array_multidim.c | 18 +++++++++++++++++- .../codetoanalyze/c/bufferoverrun/cast.c | 7 ++++++- .../codetoanalyze/c/bufferoverrun/issues.exp | 8 ++++---- .../codetoanalyze/c/bufferoverrun/sizeof.c | 2 +- .../cpp/bufferoverrun/relation.cpp | 2 +- 12 files changed, 95 insertions(+), 19 deletions(-) diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index f25c8c8ce..fb347a6d4 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -93,6 +93,16 @@ module ArrInfo = struct let set_size : Itv.t -> t -> t = fun size arr -> {arr with size} + + (* Set new stride only when the previous stride is a constant interval. *) + let set_stride : Z.t -> t -> t = + fun new_stride ({offset; size; stride} as arr) -> + Option.value_map (Itv.is_const stride) ~default:arr ~f:(fun stride -> + assert ((not Z.(equal stride zero)) && not Z.(equal new_stride zero)) ; + if Z.equal new_stride stride then arr + else + let set itv = Itv.div_const (Itv.mult_const itv stride) new_stride in + {offset= set offset; size= set size; stride= Itv.of_big_int new_stride} ) end include AbstractDomain.Map (Allocsite) (ArrInfo) @@ -111,6 +121,8 @@ let offsetof : astate -> Itv.t = fun a -> fold (fun _ arr -> Itv.join arr.ArrInf let sizeof : astate -> Itv.t = fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.size) a Itv.bot +let strideof : astate -> Itv.t = fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.stride) a Itv.bot + let sizeof_byte : astate -> Itv.t = fun a -> fold (fun _ arr -> Itv.join (Itv.mult arr.ArrInfo.size arr.ArrInfo.stride)) a Itv.bot @@ -170,3 +182,5 @@ let prune_eq : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_ let prune_ne : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_ne a1 a2 let set_size : Itv.t -> astate -> astate = fun size a -> map (ArrInfo.set_size size) a + +let set_stride : Z.t -> astate -> astate = fun stride a -> map (ArrInfo.set_stride stride) a diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index c4481eab1..0d03366f1 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -430,11 +430,10 @@ module Bound = struct let xcompare = PartialOrder.of_le ~le - let is_const : t -> bool = function - | Linear (_, se) when SymLinear.is_zero se -> - true - | _ -> - false + let is_const : t -> bool = function Linear (_, se) -> SymLinear.is_zero se | _ -> false + + let eq_const : Z.t -> t -> bool = + fun z -> function Linear (z', se) -> SymLinear.is_zero se && Z.(equal z' z) | _ -> false let neg : t -> t = function diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index ce0c137d6..c164b4437 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -91,6 +91,8 @@ module Bound : sig val is_const : t -> Z.t sexp_option + val eq_const : Z.t -> t -> bool + val plus_l : t -> t -> t val plus_u : t -> t -> t diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 6f8530138..ceb9e2387 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -319,6 +319,13 @@ module Val = struct fun size v -> {v with arrayblk= ArrayBlk.set_size size v.arrayblk} + let set_array_stride : Z.t -> t -> t = + fun new_stride v -> + let stride = ArrayBlk.strideof (get_array_blk v) in + if Itv.eq_const new_stride stride then v + else {v with arrayblk= ArrayBlk.set_stride new_stride v.arrayblk} + + module Itv = struct let m1_255 = of_itv Itv.m1_255 diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 0b644c72c..4b4f80168 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -131,6 +131,15 @@ let rec must_alias_cmp : Exp.t -> Mem.astate -> bool = false +let set_array_stride integer_type_widths typ v = + match typ with + | Typ.({desc= Tptr ({desc= Tint ikind}, Pk_pointer)}) -> + let width = Typ.width_of_ikind integer_type_widths ikind in + Val.set_array_stride (Z.of_int (width / 8)) v + | _ -> + v + + let rec eval : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Val.t = fun integer_type_widths exp mem -> if must_alias_cmp exp mem then Val.of_int 0 @@ -147,8 +156,9 @@ let rec eval : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Val.t = eval_binop integer_type_widths bop e1 e2 mem | Exp.Const c -> eval_const c - | Exp.Cast (_, e) -> - eval integer_type_widths e mem + | Exp.Cast (t, e) -> + let v = eval integer_type_widths e mem in + set_array_stride integer_type_widths t v | Exp.Lfield (e, fn, _) -> eval integer_type_widths e mem |> Val.get_all_locs |> PowLoc.append_field ~fn |> Val.of_pow_loc @@ -263,8 +273,9 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Val.t = Mem.find_set (PowLoc.singleton (Loc.of_pvar pvar)) mem | Exp.BinOp (bop, e1, e2) -> eval_binop integer_type_widths bop e1 e2 mem - | Exp.Cast (_, e) -> - eval_arr integer_type_widths e mem + | Exp.Cast (t, e) -> + let v = eval_arr integer_type_widths e mem in + set_array_stride integer_type_widths t v | Exp.Lfield (e, fn, _) -> let locs = eval integer_type_widths e mem |> Val.get_all_locs |> PowLoc.append_field ~fn in Mem.find_set locs mem diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 9a220eb53..fff073b96 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -574,12 +574,14 @@ module ItvPure = struct let is_const : t -> Z.t option = fun (l, u) -> match (Bound.is_const l, Bound.is_const u) with - | Some n, Some m when Z.equal n m -> - Some n + | (Some n as z), Some m when Z.equal n m -> + z | _, _ -> None + let eq_const : Z.t -> t -> bool = fun z (l, u) -> Bound.eq_const z l && Bound.eq_const z u + let is_zero : t -> bool = fun (l, u) -> Bound.is_zero l && Bound.is_zero u let is_one : t -> bool = fun (l, u) -> Bound.eq l Bound.one && Bound.eq u Bound.one @@ -940,6 +942,10 @@ let bind1 : (ItvPure.t -> t) -> t -> t = bind1_gen ~bot:Bottom let bind1b : (ItvPure.t -> Boolean.t) -> t -> Boolean.t = bind1_gen ~bot:Boolean.Bottom +let bind1bool : (ItvPure.t -> bool) -> t -> bool = bind1_gen ~bot:false + +let bind1zo : (ItvPure.t -> Z.t option) -> t -> Z.t option = bind1_gen ~bot:None + let lift2 : (ItvPure.t -> ItvPure.t -> ItvPure.t) -> t -> t -> t = fun f x y -> match (x, y) with @@ -972,14 +978,22 @@ let make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t NonBottom (ItvPure.make_sym ~unsigned pname symbol_table path new_sym_num) +let is_const : astate -> Z.t option = bind1zo ItvPure.is_const + +let eq_const : Z.t -> astate -> bool = fun z -> bind1bool (ItvPure.eq_const z) + let neg : t -> t = lift1 ItvPure.neg let lnot : t -> Boolean.t = bind1b ItvPure.lnot let mult : t -> t -> t = lift2 ItvPure.mult +let mult_const : t -> Z.t -> t = fun x z -> lift1 (fun x -> ItvPure.mult_const z x) x + let div : t -> t -> t = lift2 ItvPure.div +let div_const : t -> Z.t -> t = fun x z -> lift1 (fun x -> ItvPure.div_const x z) x + let mod_sem : t -> t -> t = lift2 ItvPure.mod_sem let shiftlt : t -> t -> t = lift2 ItvPure.shiftlt diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 432820359..4e5cca5a7 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -172,6 +172,10 @@ val of_int_lit : IntLit.t -> t val of_int64 : Int64.t -> t +val is_const : t -> Z.t option + +val eq_const : Z.t -> t -> bool + val make_sym : ?unsigned:bool -> Typ.Procname.t -> Symb.SymbolTable.t -> Symb.SymbolPath.t -> Counter.t -> t @@ -199,10 +203,14 @@ val range : t -> ItvRange.t val div : t -> t -> t +val div_const : t -> Z.t -> t + val minus : t -> t -> t val mult : t -> t -> t +val mult_const : t -> Z.t -> t + val plus : t -> t -> t val shiftlt : t -> t -> t diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/array_multidim.c b/infer/tests/codetoanalyze/c/bufferoverrun/array_multidim.c index a3736562a..631dc866b 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/array_multidim.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/array_multidim.c @@ -33,7 +33,7 @@ void multidim_arr3_Good() { }; } -void multidim_arr4_Good_FP() { +void multidim_arr4_Good() { int a[3][2]; int* p = a; *(p + 5) = 0; @@ -56,3 +56,19 @@ void multidim_arr5_Bad() { a[0][0] = 0; a[0][10] = 0; } + +void multidim_arr6_Good() { + int a[3][2]; + int b[10]; + int* p = a; + *p = 5; + b[a[0][0]] = 1; +} + +void multidim_arr6_Bad_FN() { + int a[3][2]; + int b[5]; + int* p = a; + *p = 5; + b[a[0][0]] = 1; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/cast.c b/infer/tests/codetoanalyze/c/bufferoverrun/cast.c index 21dec68dd..fcd247515 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/cast.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/cast.c @@ -17,11 +17,16 @@ void cast_Bad_FN() { *(int32_t*)arr = 123; } -void cast2_Good_FP() { +void cast2_Good() { int32_t arr[4]; *(((char*)arr) + 4) = 123; } +void cast2_Bad() { + int32_t arr[4]; + *(((char*)arr) + 20) = 123; +} + void cast_unsigned_to_signed_Good() { char arr[10]; uint32_t x = 15; diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index bf8c7daf0..97bf94ce9 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -38,8 +38,7 @@ codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_O codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Parameter: x[*].f,Assignment,Assignment,Assignment,ArrayAccess: Offset: -1 Size: 2] codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 2 Size: 2] codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 3 Size: 3] -codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 6 Size: 3] -codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 5 Size: 3] +codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 6 Size: 6] codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr5_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/big_array.c, use_big_array_bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Assignment,Return,Assignment,ArrayAccess: Offset: 999999999 Size: 26460] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] @@ -47,7 +46,7 @@ codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/calloc.c, calloc_bad1, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: -1 Size: 10] codetoanalyze/c/bufferoverrun/calloc.c, calloc_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 Size: 10] -codetoanalyze/c/bufferoverrun/cast.c, cast2_Good_FP, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 4 Size: 4] +codetoanalyze/c/bufferoverrun/cast.c, cast2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 20 Size: 16] codetoanalyze/c/bufferoverrun/cast.c, cast_float_to_int_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/cast.c, cast_float_to_int_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] @@ -191,9 +190,10 @@ codetoanalyze/c/bufferoverrun/relation.c, FP_array_access2_Ok, 4, BUFFER_OVERRUN codetoanalyze/c/bufferoverrun/relation.c, FP_array_access3_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 3 Size: 1] codetoanalyze/c/bufferoverrun/relation.c, FP_array_access4_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 3 Size: 1] codetoanalyze/c/bufferoverrun/relation.c, FP_call_array_access_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: -1 Size: 1 by call to `array_access_Ok` ] -codetoanalyze/c/bufferoverrun/sizeof.c, FN_static_stride_bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 1 Size: 0] +codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 1 Size: 0] codetoanalyze/c/bufferoverrun/trivial.c, malloc_zero_Bad, 2, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Alloc: Length: 0] codetoanalyze/c/bufferoverrun/trivial.c, trivial_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_once_intentional_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c b/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c index 3760c0e8a..f2ac30f58 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c @@ -20,7 +20,7 @@ struct some_struct { int x1; }; -void FN_static_stride_bad() { +void static_stride_bad() { struct some_struct a[10]; char *x, *y; x = (char*)&(a[5]); diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/relation.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/relation.cpp index 8980f4ff2..6a51f4eec 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/relation.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/relation.cpp @@ -116,6 +116,6 @@ size_t id(size_t s) { void FP_call_id_Ok() { size_t s1 = 5; size_t s2 = id(1 + s1); - char* arr = (char*)malloc(s2 * sizeof(char*)); + char* arr = (char*)malloc(s2 * sizeof(char)); arr[s1] = 0; }