From ad08184d3b27eff0b67133801625b524471821f3 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 14 Feb 2019 18:34:08 -0800 Subject: [PATCH] [inferbo] Keep alias of simple plus/minus arithmetic Summary: It keeps alias of simple plus/minus arithmetic in order to pruning the value of "++i" expression. Reviewed By: mbouaziz Differential Revision: D14080230 fbshipit-source-id: d3af32a32 --- .../src/bufferoverrun/bufferOverrunDomain.ml | 34 +++++++++++++++---- .../src/bufferoverrun/bufferOverrunModels.ml | 13 ++++--- .../bufferoverrun/bufferOverrunSemantics.ml | 32 ++++++++++++----- .../codetoanalyze/c/bufferoverrun/do_while.c | 18 ++++++++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 1 + .../codetoanalyze/c/performance/issues.exp | 6 ++-- .../c/performance/switch_continue.c | 2 +- 7 files changed, 83 insertions(+), 23 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index b605a8527..27c2e654b 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -141,6 +141,8 @@ module Val = struct let of_big_int n = of_itv (Itv.of_big_int n) + let of_int_lit n = of_itv (Itv.of_int_lit n) + let of_loc ?(traces = TraceSet.empty) x = {bot with powloc= PowLoc.singleton x; traces} let of_pow_loc ~traces powloc = {bot with powloc; traces} @@ -592,7 +594,12 @@ module MemPure = struct end module AliasTarget = struct - type t = Simple of Loc.t | Empty of Loc.t | Fgets of Loc.t | Nullity of Loc.t + type t = + | Simple of Loc.t + | SimplePlusA of Loc.t * IntLit.t + | Empty of Loc.t + | Fgets of Loc.t + | Nullity of Loc.t [@@deriving compare] let equal = [%compare.equal: t] @@ -600,6 +607,9 @@ module AliasTarget = struct let pp fmt = function | Simple l -> Loc.pp fmt l + | SimplePlusA (l, i) -> + if IntLit.isnegative i then F.fprintf fmt "%a-%a" Loc.pp l IntLit.pp (IntLit.neg i) + else F.fprintf fmt "%a+%a" Loc.pp l IntLit.pp i | Empty l -> F.fprintf fmt "empty(%a)" Loc.pp l | Fgets l -> @@ -612,12 +622,17 @@ module AliasTarget = struct let nullity l = Nullity l - let use l = function Simple l' | Empty l' | Fgets l' | Nullity l' -> Loc.equal l l' + let use l = function + | Simple l' | SimplePlusA (l', _) | Empty l' | Fgets l' | Nullity l' -> + Loc.equal l l' + let loc_map x ~f = match x with | Simple l -> Option.map (f l) ~f:(fun l -> Simple l) + | SimplePlusA (l, i) -> + Option.map (f l) ~f:(fun l -> SimplePlusA (l, i)) | Empty l -> Option.map (f l) ~f:(fun l -> Empty l) | Fgets l -> @@ -722,6 +737,11 @@ module Alias = struct | Exp.Var l when Loc.is_return loc -> let update_ret retl = {a with ret= AliasRet.v retl} in Option.value_map (find l a) ~default:a ~f:update_ret + | Exp.BinOp (Binop.PlusA _, Exp.Var id, Exp.Const (Const.Cint i)) + | Exp.BinOp (Binop.PlusA _, Exp.Const (Const.Cint i), Exp.Var id) -> + lift_map (AliasMap.load id (AliasTarget.SimplePlusA (loc, IntLit.neg i))) a + | Exp.BinOp (Binop.MinusA _, Exp.Var id, Exp.Const (Const.Cint i)) -> + lift_map (AliasMap.load id (AliasTarget.SimplePlusA (loc, i))) a | _ -> a @@ -1139,11 +1159,13 @@ module MemReach = struct let find_alias : Ident.t -> _ t0 -> AliasTarget.t option = fun k m -> Alias.find k m.alias - let find_simple_alias : Ident.t -> _ t0 -> Loc.t option = + let find_simple_alias : Ident.t -> _ t0 -> (Loc.t * IntLit.t option) option = fun k m -> match Alias.find k m.alias with | Some (AliasTarget.Simple l) -> - Some l + Some (l, None) + | Some (AliasTarget.SimplePlusA (l, i)) -> + Some (l, Some i) | Some (AliasTarget.Empty _ | AliasTarget.Fgets _ | AliasTarget.Nullity _) | None -> None @@ -1259,7 +1281,7 @@ module MemReach = struct | LatestPrune.V (x, prunes, _), Exp.Var r | LatestPrune.V (x, _, prunes), Exp.UnOp (Unop.LNot, Exp.Var r, _) -> ( match find_simple_alias r m with - | Some (Loc.Var (Var.ProgramVar y)) when Pvar.equal x y -> + | Some (Loc.Var (Var.ProgramVar y), None) when Pvar.equal x y -> PrunePairs.fold apply1 prunes m | _ -> m ) @@ -1400,7 +1422,7 @@ module Mem = struct fun k -> f_lift_default ~default:None (MemReach.find_alias k) - let find_simple_alias : Ident.t -> _ t0 -> Loc.t option = + let find_simple_alias : Ident.t -> _ t0 -> (Loc.t * IntLit.t option) option = fun k -> f_lift_default ~default:None (MemReach.find_simple_alias k) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 357ab0d00..a694973fd 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -97,7 +97,9 @@ let malloc size_exp = let typ, stride, length0, dyn_length = get_malloc_info size_exp in let length = Sem.eval integer_type_widths length0 mem in let traces = Trace.(Set.add_elem location ArrayDeclaration) (Dom.Val.get_traces length) in - let path = Option.bind (Dom.Mem.find_simple_alias id mem) ~f:Loc.get_path in + let path = + match Dom.Mem.find_simple_alias id mem with Some (l, None) -> Loc.get_path l | _ -> None + in let offset, size = (Itv.zero, Dom.Val.get_itv length) in let allocsite = let represents_multiple_values = not (Itv.is_one size) in @@ -553,9 +555,12 @@ module StdBasicString = struct 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 match e with - | Exp.Var id -> - Option.value_map (Dom.Mem.find_simple_alias id mem) ~default:mem ~f:(fun l -> - Dom.Mem.load_empty_alias ret_id l mem ) + | 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 diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index cfaad3ecf..860bcd912 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -308,7 +308,12 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t = match Mem.find_alias id mem with | Some (AliasTarget.Simple loc) -> Mem.find loc mem - | Some (AliasTarget.Empty _ | AliasTarget.Fgets _ | AliasTarget.Nullity _) | None -> + | Some + ( AliasTarget.SimplePlusA _ + | AliasTarget.Empty _ + | AliasTarget.Fgets _ + | AliasTarget.Nullity _ ) + | None -> Val.bot ) | Exp.Lvar pvar -> Mem.find (Loc.of_pvar pvar) mem @@ -475,7 +480,7 @@ module Prune = struct let v = Mem.find lv mem in let v' = Val.prune_eq_zero v in update_mem_in_prune lv v' astate - | None -> + | Some (AliasTarget.SimplePlusA _) | None -> astate ) | Exp.UnOp (Unop.LNot, Exp.Var x, _) -> ( match Mem.find_alias x mem with @@ -492,7 +497,7 @@ module Prune = struct let itv_v = Itv.prune_comp Binop.Ge (Val.get_itv v) Itv.one in let v' = Val.modify_itv itv_v v in update_mem_in_prune lv v' astate - | Some (AliasTarget.Fgets _) | None -> + | Some (AliasTarget.SimplePlusA _ | AliasTarget.Fgets _) | None -> astate ) | _ -> astate @@ -508,9 +513,12 @@ module Prune = struct | Exp.BinOp ((Binop.Le as comp), Exp.Var x, e') | Exp.BinOp ((Binop.Ge as comp), Exp.Var x, e') -> ( match Mem.find_simple_alias x mem with - | Some lv -> + | Some (lv, opt_i) -> let lhs = Mem.find lv mem in - let rhs = eval integer_type_widths e' mem in + let rhs = + let v' = eval integer_type_widths e' mem in + Option.value_map opt_i ~default:v' ~f:(fun i -> Val.minus_a v' (Val.of_int_lit i)) + in let v = Val.prune_comp comp lhs rhs in let pruning_exp = PruningExp.make comp ~lhs ~rhs in update_mem_in_prune lv v ~pruning_exp astate @@ -518,9 +526,12 @@ module Prune = struct astate ) | Exp.BinOp (Binop.Eq, Exp.Var x, e') -> ( match Mem.find_simple_alias x mem with - | Some lv -> + | Some (lv, opt_i) -> let lhs = Mem.find lv mem in - let rhs = eval integer_type_widths e' mem in + let rhs = + let v' = eval integer_type_widths e' mem in + Option.value_map opt_i ~default:v' ~f:(fun i -> Val.minus_a v' (Val.of_int_lit i)) + in let v = Val.prune_eq lhs rhs in let pruning_exp = PruningExp.make Binop.Eq ~lhs ~rhs in update_mem_in_prune lv v ~pruning_exp astate @@ -528,9 +539,12 @@ module Prune = struct astate ) | Exp.BinOp (Binop.Ne, Exp.Var x, e') -> ( match Mem.find_simple_alias x mem with - | Some lv -> + | Some (lv, opt_i) -> let lhs = Mem.find lv mem in - let rhs = eval integer_type_widths e' mem in + let rhs = + let v' = eval integer_type_widths e' mem in + Option.value_map opt_i ~default:v' ~f:(fun i -> Val.minus_a v' (Val.of_int_lit i)) + in let v = Val.prune_ne lhs rhs in let pruning_exp = PruningExp.make Binop.Ne ~lhs ~rhs in update_mem_in_prune lv v ~pruning_exp astate diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/do_while.c b/infer/tests/codetoanalyze/c/bufferoverrun/do_while.c index fe1b5e0e7..d229a0671 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/do_while.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/do_while.c @@ -26,3 +26,21 @@ void do_while_Bad() { char* a = malloc(10); do_while_sub(a, 11); /* BUG */ } + +void do_while_2_Good() { + int count = 10; + int a[count]; + int i = 0; + do { + a[i] = 0; + } while (++i < count); +} + +void do_while_2_Bad() { + int count = 10; + int a[count]; + int i = 0; + do { + a[i] = 0; + } while (i++ < count); +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index a76ecb190..13d861e7a 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -91,6 +91,7 @@ codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Bad, 5, BUFFER_OVE codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/do_while.c, do_while_2_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Assignment,Array declaration,Array access: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/do_while.c, do_while_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Assignment,Call,,Assignment,,Parameter `*a`,Array access: Offset: [0, 10] Size: 10 by call to `do_while_sub` ] codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `*arr`,Array access: Offset: 1 Size: 1 by call to `two_accesses` ] codetoanalyze/c/bufferoverrun/duplicates.c, tsa_one_alarm_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `n`,,Array declaration,Array access: Offset: 3 Size: 1 by call to `two_symbolic_accesses` ] diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index 9172da0af..85cd46e6e 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -62,8 +62,8 @@ codetoanalyze/c/performance/loops.c, loop_use_global_vars, 1, EXPENSIVE_EXECUTIO codetoanalyze/c/performance/purity.c, loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7006, degree = 0] codetoanalyze/c/performance/switch_continue.c, test_switch, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/performance/switch_continue.c, test_switch, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0] -codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] -codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] -codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] +codetoanalyze/c/performance/switch_continue.c, unroll_loop, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] +codetoanalyze/c/performance/switch_continue.c, unroll_loop, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] +codetoanalyze/c/performance/switch_continue.c, unroll_loop, 14, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 25 + 12 ⋅ (n - 1), degree = 1] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1] diff --git a/infer/tests/codetoanalyze/c/performance/switch_continue.c b/infer/tests/codetoanalyze/c/performance/switch_continue.c index ab013ca19..3a0d2e6e1 100644 --- a/infer/tests/codetoanalyze/c/performance/switch_continue.c +++ b/infer/tests/codetoanalyze/c/performance/switch_continue.c @@ -26,7 +26,7 @@ int test_switch() { return 0; } -int unroll_loop_FP(int n) { +int unroll_loop(int n) { int ret = 0; int loop = n + 3 / 4; switch (n % 8) {