[Bufferoverrun] More prune to make some nodes unreachable

Summary:
- Bottom-lift abstract memory domain to express unreachable node

- Two cases to make a node unreachable

  + constant: when an evaluation result of condition expression is
    bottom or false, e.g., "prune(0)".

  + alias: when the same structure e is compared to itself with "<",
    ">", and "!=", e.g., "prune(e < e)".

- Add test for the new prune (prune_constant.c, prune_alias.c)

- Debug the semantics of comparison

Reviewed By: mbouaziz

Differential Revision: D4938055

fbshipit-source-id: d0fadf0

infer/src/bufferoverrun/absLoc.ml

@@ -69,6 +69,7 @@ struct
       end)
 
   let bot = empty
+  let is_bot = is_empty
 
   let of_pvar pvar = singleton (Loc.of_pvar pvar)
   let of_id id = singleton (Loc.of_id id)

infer/src/bufferoverrun/arrayBlk.ml

@@ -133,6 +133,9 @@ include AbstractDomain.Map (PPMap) (ArrInfo)
 let bot : astate
   = empty
 
+let is_bot : astate -> bool
+  = is_empty
+
 let make : Allocsite.t -> Itv.t -> Itv.t -> Itv.t -> astate
   = fun a o sz st -> add a (ArrInfo.make (o, sz, st)) bot
 

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -428,7 +428,7 @@ let compute_post
   = fun { pdesc; tenv; extras = get_pdesc } ->
     let cfg = CFG.from_pdesc pdesc in
     let pdata = ProcData.make pdesc tenv get_pdesc in
-    let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.bot pdata in
+    let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata in
     let entry_mem =
       let entry_id = CFG.id (CFG.start_node cfg) in
       Analyzer.extract_post entry_id inv_map

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -288,6 +288,16 @@ struct
   let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t
     = fun f x y -> { bot with itv = f x.itv y.itv }
 
+  let has_pointer : t -> bool
+    = fun x ->
+      not (PowLoc.is_bot x.powloc && ArrayBlk.is_bot x.arrayblk)
+
+  let lift_cmp_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t
+    = fun f x y ->
+      if has_pointer x || has_pointer y then
+        {bot with itv = Itv.unknown_bool}
+      else lift_itv f x y
+
   let plus : t -> t -> t
     = fun x y ->
       { x with itv = Itv.plus x.itv y.itv; arrayblk = ArrayBlk.plus_offset x.arrayblk y.itv }
@@ -314,22 +324,22 @@ struct
     = lift_itv Itv.shiftrt
 
   let lt_sem : t -> t -> t
-    = lift_itv Itv.lt_sem
+    = lift_cmp_itv Itv.lt_sem
 
   let gt_sem : t -> t -> t
-    = lift_itv Itv.gt_sem
+    = lift_cmp_itv Itv.gt_sem
 
   let le_sem : t -> t -> t
-    = lift_itv Itv.le_sem
+    = lift_cmp_itv Itv.le_sem
 
   let ge_sem : t -> t -> t
-    = lift_itv Itv.ge_sem
+    = lift_cmp_itv Itv.ge_sem
 
   let eq_sem : t -> t -> t
-    = lift_itv Itv.eq_sem
+    = lift_cmp_itv Itv.eq_sem
 
   let ne_sem : t -> t -> t
-    = lift_itv Itv.ne_sem
+    = lift_cmp_itv Itv.ne_sem
 
   let land_sem : t -> t -> t
     = lift_itv Itv.land_sem
@@ -564,7 +574,7 @@ struct
     = fun k m -> try Some (M.find k m) with Not_found -> None
 end
 
-module Mem =
+module MemReach =
 struct
   type astate = { stack : Stack.astate; heap : Heap.astate; alias : Alias.astate }
   type t = astate
@@ -661,6 +671,97 @@ struct
       else weak_update_heap ploc v s
 end
 
+module Mem = struct
+  include AbstractDomain.BottomLifted (MemReach)
+
+  type t = astate
+
+  let bot : t = Bottom
+
+  let init : t = NonBottom (MemReach.bot)
+
+  let f_lift_default : 'a -> (MemReach.t -> 'a) -> t -> 'a =
+    fun default f m ->
+      match m with
+      | Bottom -> default
+      | NonBottom m' -> f m'
+
+  let f_lift : (MemReach.t -> MemReach.t) -> t -> t =
+    fun f ->
+      f_lift_default Bottom (fun m' -> NonBottom (f m'))
+
+  let pp_summary : F.formatter -> t -> unit
+    = fun fmt m ->
+      match m with
+      | Bottom -> F.fprintf fmt "unreachable"
+      | NonBottom m' -> MemReach.pp_summary fmt m'
+
+  let find_stack : Loc.t -> t -> Val.t
+    = fun k ->
+      f_lift_default Val.bot (MemReach.find_stack k)
+
+  let find_stack_set : PowLoc.t -> t -> Val.t
+    = fun k ->
+      f_lift_default Val.bot (MemReach.find_stack_set k)
+
+  let find_heap : Loc.t -> t -> Val.t
+    = fun k ->
+      f_lift_default Val.bot (MemReach.find_heap k)
+
+  let find_heap_set : PowLoc.t -> t -> Val.t
+    = fun k ->
+      f_lift_default Val.bot (MemReach.find_heap_set k)
+
+  let find_alias : Ident.t -> t -> Pvar.t option
+    = fun k ->
+      f_lift_default None (MemReach.find_alias k)
+
+  let load_alias : Ident.t -> Exp.t -> t -> t
+    = fun id e ->
+      f_lift (MemReach.load_alias id e)
+
+  let store_alias : Exp.t -> Exp.t -> t -> t
+    = fun e1 e2 ->
+      f_lift (MemReach.store_alias e1 e2)
+
+  let add_stack : Loc.t -> Val.t -> t -> t
+    = fun k v ->
+      f_lift (MemReach.add_stack k v)
+
+  let add_heap : Loc.t -> Val.t -> t -> t
+    = fun k v ->
+      f_lift (MemReach.add_heap k v)
+
+  let strong_update_stack : PowLoc.t -> Val.t -> t -> t
+    = fun p v ->
+      f_lift (MemReach.strong_update_stack p v)
+
+  let strong_update_heap : PowLoc.t -> Val.t -> t -> t
+    = fun p v ->
+      f_lift (MemReach.strong_update_heap p v)
+
+  let weak_update_stack : PowLoc.t -> Val.t -> t -> t
+    = fun p v ->
+      f_lift (MemReach.weak_update_stack p v)
+
+  let weak_update_heap : PowLoc.t -> Val.t -> t -> t
+    = fun p v ->
+      f_lift (MemReach.weak_update_heap p v)
+
+  let get_heap_symbols : t -> Itv.Symbol.t list
+    = f_lift_default [] MemReach.get_heap_symbols
+
+  let get_return : t -> Val.t
+    = f_lift_default Val.bot MemReach.get_return
+
+  let can_strong_update : PowLoc.t -> bool
+    = MemReach.can_strong_update
+
+  let update_mem : PowLoc.t -> Val.t -> t -> t
+    = fun ploc v ->
+      f_lift (MemReach.update_mem ploc v)
+end
+
 module Summary =
 struct
   type t = Mem.t * Mem.t * ConditionSet.t

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -53,33 +53,119 @@ struct
       | Typ.Tarray (typ, Some ilit) -> sizeof typ * IntLit.to_int ilit
       | _ -> 4
 
+  let rec must_alias : Exp.t -> Exp.t -> Mem.astate -> bool
+    = fun e1 e2 m ->
+      match e1, e2 with
+      | Exp.Var x1, Exp.Var x2 ->
+          (match Mem.find_alias x1 m, Mem.find_alias x2 m with
+           | Some x1', Some x2' -> Pvar.equal x1' x2'
+           | _, _ -> false)
+      | Exp.UnOp (uop1, e1', _), Exp.UnOp (uop2, e2', _) ->
+          Unop.equal uop1 uop2 && must_alias e1' e2' m
+      | Exp.BinOp (bop1, e11, e12), Exp.BinOp (bop2, e21, e22) ->
+          Binop.equal bop1 bop2
+          && must_alias e11 e21 m
+          && must_alias e12 e22 m
+      | Exp.Exn t1, Exp.Exn t2 -> must_alias t1 t2 m
+      | Exp.Const c1, Exp.Const c2 -> Const.equal c1 c2
+      | Exp.Cast (t1, e1'), Exp.Cast (t2, e2') ->
+          Typ.equal t1 t2 && must_alias e1' e2' m
+      | Exp.Lvar x1, Exp.Lvar x2 ->
+          Pvar.equal x1 x2
+      | Exp.Lfield (e1, fld1, _), Exp.Lfield (e2, fld2, _) ->
+          must_alias e1 e2 m && Fieldname.equal fld1 fld2
+      | Exp.Lindex (e11, e12), Exp.Lindex (e21, e22) ->
+          must_alias e11 e21 m && must_alias e12 e22 m
+      | Exp.Sizeof (t1, dynlen1, subt1), Exp.Sizeof (t2, dynlen2, subt2) ->
+          Typ.equal t1 t2
+          && must_alias_opt dynlen1 dynlen2 m
+          && Int.equal (Subtype.compare subt1 subt2) 0
+      | _, _ -> false
+
+  and must_alias_opt : Exp.dynamic_length -> Exp.dynamic_length -> Mem.astate -> bool
+    = fun dynlen1 dynlen2 m ->
+      match dynlen1, dynlen2 with
+      | Some e1, Some e2 -> must_alias e1 e2 m
+      | None, None -> true
+      | _, _ -> false
+
+  let comp_rev : Binop.t -> Binop.t
+    = function
+      | Binop.Lt -> Binop.Gt
+      | Binop.Gt -> Binop.Lt
+      | Binop.Le -> Binop.Ge
+      | Binop.Ge -> Binop.Le
+      | Binop.Eq -> Binop.Eq
+      | Binop.Ne -> Binop.Ne
+      | _ -> assert (false)
+
+  let comp_not : Binop.t -> Binop.t
+    = function
+      | Binop.Lt -> Binop.Ge
+      | Binop.Gt -> Binop.Le
+      | Binop.Le -> Binop.Gt
+      | Binop.Ge -> Binop.Lt
+      | Binop.Eq -> Binop.Ne
+      | Binop.Ne -> Binop.Eq
+      | _ -> assert (false)
+
+  let rec must_alias_cmp : Exp.t -> Mem.astate -> bool
+    = fun e m ->
+      match e with
+      | Exp.BinOp (Binop.Lt, e1, e2)
+      | Exp.BinOp (Binop.Gt, e1, e2)
+      | Exp.BinOp (Binop.Ne, e1, e2) -> must_alias e1 e2 m
+      | Exp.BinOp (Binop.LAnd, e1, e2) ->
+          must_alias_cmp e1 m || must_alias_cmp e2 m
+      | Exp.BinOp (Binop.LOr, e1, e2) ->
+          must_alias_cmp e1 m && must_alias_cmp e2 m
+      | Exp.UnOp (Unop.LNot, Exp.UnOp (Unop.LNot, e1, _), _) ->
+          must_alias_cmp e1 m
+      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Lt as c, e1, e2), _)
+      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Gt as c, e1, e2), _)
+      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Le as c, e1, e2), _)
+      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ge as c, e1, e2), _)
+      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq as c, e1, e2), _)
+      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ne as c, e1, e2), _) ->
+          must_alias_cmp (Exp.BinOp (comp_not c, e1, e2)) m
+      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) ->
+          let e1' = Exp.UnOp (Unop.LNot, e1, t) in
+          let e2' = Exp.UnOp (Unop.LNot, e2, t) in
+          must_alias_cmp (Exp.BinOp (Binop.LAnd, e1', e2')) m
+      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LAnd, e1, e2), t) ->
+          let e1' = Exp.UnOp (Unop.LNot, e1, t) in
+          let e2' = Exp.UnOp (Unop.LNot, e2, t) in
+          must_alias_cmp (Exp.BinOp (Binop.LOr, e1', e2')) m
+      | _ -> false
+
   let rec eval : Exp.t -> Mem.astate -> Location.t -> Val.t
     = fun exp mem loc ->
-      match exp with
-      | Exp.Var id -> Mem.find_stack (Var.of_id id |> Loc.of_var) mem
-      | Exp.Lvar pvar ->
-          let ploc = pvar |> Loc.of_pvar |> PowLoc.singleton in
-          let arr = Mem.find_stack_set ploc mem in
-          ploc |> Val.of_pow_loc |> Val.join arr
-      | Exp.UnOp (uop, e, _) -> eval_unop uop e mem loc
-      | Exp.BinOp (bop, e1, e2) -> eval_binop bop e1 e2 mem loc
-      | Exp.Const c -> eval_const c
-      | Exp.Cast (_, e) -> eval e mem loc
-      | Exp.Lfield (e, fn, _) ->
-          eval e mem loc
-          |> Val.get_all_locs
-          |> Fn.flip PowLoc.append_field fn
-          |> Val.of_pow_loc
-      | Exp.Lindex (e1, _) ->
-          let arr = eval e1 mem loc in (* must have array blk *)
-          (* let idx = eval e2 mem loc in *)
-          let ploc = arr |> Val.get_array_blk |> ArrayBlk.get_pow_loc in
-          (* if nested array, add the array blk *)
-          let arr = Mem.find_heap_set ploc mem in
-          Val.join (Val.of_pow_loc ploc) arr
-      | Exp.Sizeof (typ, _, _) -> Val.of_int (sizeof typ)
-      | Exp.Exn _
-      | Exp.Closure _ -> Val.bot
+      if must_alias_cmp exp mem then Val.of_int 0 else
+        match exp with
+        | Exp.Var id -> Mem.find_stack (Var.of_id id |> Loc.of_var) mem
+        | Exp.Lvar pvar ->
+            let ploc = pvar |> Loc.of_pvar |> PowLoc.singleton in
+            let arr = Mem.find_stack_set ploc mem in
+            ploc |> Val.of_pow_loc |> Val.join arr
+        | Exp.UnOp (uop, e, _) -> eval_unop uop e mem loc
+        | Exp.BinOp (bop, e1, e2) -> eval_binop bop e1 e2 mem loc
+        | Exp.Const c -> eval_const c
+        | Exp.Cast (_, e) -> eval e mem loc
+        | Exp.Lfield (e, fn, _) ->
+            eval e mem loc
+            |> Val.get_all_locs
+            |> Fn.flip PowLoc.append_field fn
+            |> Val.of_pow_loc
+        | Exp.Lindex (e1, _) ->
+            let arr = eval e1 mem loc in (* must have array blk *)
+            (* let idx = eval e2 mem loc in *)
+            let ploc = arr |> Val.get_array_blk |> ArrayBlk.get_pow_loc in
+            (* if nested array, add the array blk *)
+            let arr = Mem.find_heap_set ploc mem in
+            Val.join (Val.of_pow_loc ploc) arr
+        | Exp.Sizeof (typ, _, _) -> Val.of_int (sizeof typ)
+        | Exp.Exn _
+        | Exp.Closure _ -> Val.bot
 
   and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Location.t -> Val.t
     = fun unop e mem loc ->
@@ -197,26 +283,6 @@ struct
            | None -> mem)
       | _ -> mem
 
-  let comp_rev : Binop.t -> Binop.t
-    = function
-      | Binop.Lt -> Binop.Gt
-      | Binop.Gt -> Binop.Lt
-      | Binop.Le -> Binop.Ge
-      | Binop.Ge -> Binop.Le
-      | Binop.Eq -> Binop.Eq
-      | Binop.Ne -> Binop.Ne
-      | _ -> assert (false)
-
-  let comp_not : Binop.t -> Binop.t
-    = function
-      | Binop.Lt -> Binop.Ge
-      | Binop.Gt -> Binop.Le
-      | Binop.Le -> Binop.Gt
-      | Binop.Ge -> Binop.Lt
-      | Binop.Eq -> Binop.Ne
-      | Binop.Ne -> Binop.Eq
-      | _ -> assert (false)
-
   let prune_binop_right : Exp.t -> Location.t -> Mem.astate -> Mem.astate
     = fun e loc mem ->
       match e with
@@ -229,10 +295,22 @@ struct
           prune_binop_left (Exp.BinOp (comp_rev c, Exp.Var x, e')) loc mem
       | _ -> mem
 
+  let is_unreachable_constant : Exp.t -> Location.t -> Mem.astate -> bool
+    = fun e loc m ->
+      Val.(<=) ~lhs:(eval e m loc) ~rhs:(Val.of_int 0)
+
+  let prune_unreachable : Exp.t -> Location.t -> Mem.astate -> Mem.astate
+    = fun e loc mem ->
+      if is_unreachable_constant e loc mem then Mem.bot else mem
+
   let rec prune : Exp.t -> Location.t -> Mem.astate -> Mem.astate
     = fun e loc mem ->
       let mem =
-        mem |> prune_unop e |> prune_binop_left e loc |> prune_binop_right e loc
+        mem
+        |> prune_unreachable e loc
+        |> prune_unop e
+        |> prune_binop_left e loc
+        |> prune_binop_right e loc
       in
       match e with
       | Exp.BinOp (Binop.Ne, e, Exp.Const (Const.Cint i)) when IntLit.iszero i ->

infer/src/bufferoverrun/itv.ml

@@ -876,6 +876,9 @@ let pos : t
 let nat : t
   = NonBottom ItvPure.nat
 
+let unknown_bool : t
+  = NonBottom ItvPure.unknown_bool
+
 let make : Bound.t -> Bound.t -> t
   = fun l u -> if Bound.lt u l then Bottom else NonBottom (ItvPure.make l u)
 

infer/tests/codetoanalyze/c/bufferoverrun/Makefile

@@ -25,6 +25,8 @@ SOURCES = \
   nested_loop_with_label.c \
   break_continue_return.c \
   goto_loop.c \
-  inf_loop.c
+  inf_loop.c \
+  prune_constant.c \
+  prune_alias.c \
 
 include $(TESTS_DIR)/clang.make

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -7,5 +7,6 @@ codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN,
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offset : [10, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/goto_loop.c:24:3]
 codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset : [0, 10] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop.c:20:7]
 codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c:19:5]
+codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN, [Offset : [1, 1] Size : [1, 1] @ codetoanalyze/c/bufferoverrun/prune_alias.c:107:5]
 codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [Offset : [10, 10] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/trivial.c:15:3]
 codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/while_loop.c:16:10]

infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c

@@ -0,0 +1,109 @@
+/*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+void prune_alias_le_Ok(int x) {
+  int a[1];
+
+  if (x <= x) {
+    a[0] = 0;
+  } else {
+    a[1] = 0;
+  }
+}
+
+void prune_alias_ge_Ok(int x) {
+  int a[1];
+
+  if (x >= x) {
+    a[0] = 0;
+  } else {
+    a[1] = 0;
+  }
+}
+
+void prune_alias_eq_Ok(int x) {
+  int a[1];
+
+  if (x == x) {
+    a[0] = 0;
+  } else {
+    a[1] = 0;
+  }
+}
+
+void prune_alias_lt_Ok(int x) {
+  int a[1];
+
+  if (x < x) {
+    a[1] = 0;
+  }
+}
+
+void prune_alias_gt_Ok(int x) {
+  int a[1];
+
+  if (x > x) {
+    a[1] = 0;
+  }
+}
+
+void prune_alias_ne_Ok(int x) {
+  int a[1];
+
+  if (x != x) {
+    a[1] = 0;
+  }
+}
+
+void prune_alias_not_Ok(int x) {
+  int a[1];
+
+  if (!(x == x)) {
+    a[1] = 0;
+  }
+
+  if (!(x <= x)) {
+    a[1] = 0;
+  }
+
+  if (!(x >= x)) {
+    a[1] = 0;
+  }
+}
+
+void prune_alias_and_Ok(int x) {
+  int a[1];
+
+  if (x == x && x != x) {
+    a[1] = 0;
+  }
+}
+
+void prune_alias_or_Ok(int x, int y) {
+  int a[1];
+
+  if (x != x || y != y) {
+    a[1] = 0;
+  }
+}
+
+void prune_alias_exp_Ok(int x) {
+  int a[1];
+
+  if (x + 1 != x + 1) {
+    a[1] = 0;
+  }
+}
+
+void FP_prune_alias_exp_Ok(int x) {
+  int a[1];
+
+  if (x + 1 != 1 + x) {
+    a[1] = 0;
+  }
+}

infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c

@@ -0,0 +1,38 @@
+/*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+void prune_constant_true_Ok() {
+  int a[1];
+
+  if (1) {
+    a[0] = 0;
+  } else {
+    a[1] = 0;
+  }
+}
+
+void prune_constant_false_Ok() {
+  int a[1];
+
+  if (0) {
+    a[1] = 0;
+  } else {
+    a[0] = 0;
+  }
+}
+
+void prune_constant_value_Ok(int x) {
+  int a[1];
+  if (-1 < x && x < 1) {
+    if (x) {
+      a[1] = 0;
+    } else {
+      a[0] = 0;
+    }
+  }
+}