[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

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)
 
 

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

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

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);
+}

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, [<Offset trace>,Assignment,<Length trace>,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,<Offset trace>,Assignment,<Length trace>,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,<Length trace>,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,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: 3 Size: 1 by call to `two_symbolic_accesses` ]

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, [<LHS trace>,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, [<LHS trace>,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]

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) {