From 1bde1ef0f0cae50769897733331e8a8c2eff7f43 Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Wed, 11 Dec 2019 04:40:49 -0800
Subject: [PATCH] [pulse] use inferbo's prune in `PRUNE` nodes

Summary:
After passing a `PRUNE` instruction we can refine the current inferbo
intervals for the values involved.

Reviewed By: ezgicicek

Differential Revision: D18889103

fbshipit-source-id: b521046aa
---
 infer/src/IR/Binop.ml              | 46 ++++++++++++++++++++++++++++++
 infer/src/IR/Binop.mli             |  7 +++++
 infer/src/bufferoverrun/itv.mli    |  2 ++
 infer/src/pulse/PulseOperations.ml | 26 ++++++++++++++++-
 4 files changed, 80 insertions(+), 1 deletion(-)

diff --git a/infer/src/IR/Binop.ml b/infer/src/IR/Binop.ml
index da7d65fdf..f55f99c70 100644
--- a/infer/src/IR/Binop.ml
+++ b/infer/src/IR/Binop.ml
@@ -49,6 +49,52 @@ let injective = function PlusA _ | PlusPI | MinusA _ | MinusPI | MinusPP -> true
     "don't know". *)
 let is_zero_runit = function PlusA _ | PlusPI | MinusA _ | MinusPI | MinusPP -> true | _ -> false
 
+let symmetric = function
+  | (PlusA _ | PlusPI | Mult _ | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr) as symmetric_op ->
+      Some symmetric_op
+  | MinusA _ | MinusPP | MinusPI | Div | Mod | Shiftlt | Shiftrt ->
+      None
+  | Lt ->
+      Some Gt
+  | Gt ->
+      Some Lt
+  | Le ->
+      Some Ge
+  | Ge ->
+      Some Le
+
+
+let negate = function
+  | Eq ->
+      Some Ne
+  | Ne ->
+      Some Eq
+  | Lt ->
+      Some Ge
+  | Gt ->
+      Some Le
+  | Le ->
+      Some Gt
+  | Ge ->
+      Some Lt
+  | LAnd
+  | LOr
+  | PlusA _
+  | PlusPI
+  | Mult _
+  | BAnd
+  | BXor
+  | BOr
+  | MinusA _
+  | MinusPP
+  | MinusPI
+  | Div
+  | Mod
+  | Shiftlt
+  | Shiftrt ->
+      None
+
+
 let to_string = function
   | PlusA _ ->
       "+"
diff --git a/infer/src/IR/Binop.mli b/infer/src/IR/Binop.mli
index deea20e45..6a029bdad 100644
--- a/infer/src/IR/Binop.mli
+++ b/infer/src/IR/Binop.mli
@@ -47,3 +47,10 @@ val is_zero_runit : t -> bool
 (** This function returns true if 0 is the right unit of [binop]. The return value false means
     "don't know". *)
 
+val symmetric : t -> t option
+(** [symmetric bop] returns' [Some bop'] if [x bop y] if and only if [y bop' x] for all x, y, or
+    [None] if no such [bop'] exists *)
+
+val negate : t -> t option
+(** [negate bop] returns' [Some bop'] if [not (x bop y)] if and only if [x bop' y] for all x, y, or
+    [None] if no such [bop'] exists *)
diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli
index bf1fd05f7..0ad2da821 100644
--- a/infer/src/bufferoverrun/itv.mli
+++ b/infer/src/bufferoverrun/itv.mli
@@ -112,6 +112,8 @@ module ItvPure : sig
   val arith_unop : Unop.t -> t -> t option
 
   val to_boolean : t -> Boolean.t
+
+  val prune_binop : Binop.t -> t -> t -> t bottom_lifted
 end
 
 include module type of AbstractDomain.BottomLifted (ItvPure)
diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml
index 59d091b8a..47457a7a8 100644
--- a/infer/src/pulse/PulseOperations.ml
+++ b/infer/src/pulse/PulseOperations.ml
@@ -268,6 +268,24 @@ let record_abduced event location addr_opt orig_arith_hist_opt arith_opt astate
 
 
 let prune ~is_then_branch if_kind location ~condition astate =
+  let prune_with_bop ~negated v_opt arith bop arith' astate =
+    match
+      Option.both v_opt (if negated then Binop.negate bop else Some bop)
+      |> Option.map ~f:(fun (v, positive_bop) ->
+             (v, Itv.ItvPure.prune_binop positive_bop arith arith') )
+    with
+    | None ->
+        (astate, true)
+    | Some (_, Bottom) ->
+        (astate, false)
+    | Some (v, NonBottom arith_pruned) ->
+        let attr_arith = Attribute.BoItv arith_pruned in
+        let astate =
+          Memory.abduce_attribute v attr_arith astate |> Memory.add_attribute v attr_arith
+        in
+        (astate, true)
+  in
+  let bind_satisfiable ~satisfiable astate ~f = if satisfiable then f astate else (astate, false) in
   let rec prune_aux ~negated exp astate =
     match (exp : Exp.t) with
     | BinOp (bop, exp_lhs, exp_rhs) -> (
@@ -298,7 +316,13 @@ let prune ~is_then_branch if_kind location ~condition astate =
               | Bottom ->
                   false
             in
-            (astate, satisfiable) )
+            let astate, satisfiable =
+              bind_satisfiable ~satisfiable astate ~f:(fun astate ->
+                  prune_with_bop ~negated value_lhs_opt bo_itv_lhs bop bo_itv_rhs astate )
+            in
+            Option.value_map (Binop.symmetric bop) ~default:(astate, satisfiable) ~f:(fun bop' ->
+                bind_satisfiable ~satisfiable astate ~f:(fun astate ->
+                    prune_with_bop ~negated value_rhs_opt bo_itv_rhs bop' bo_itv_lhs astate ) ) )
     | UnOp (LNot, exp', _) ->
         prune_aux ~negated:(not negated) exp' astate
     | exp ->