From 320c82d9ad92adab67f462ae80bf3dd38c847556 Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Wed, 21 Jul 2021 03:28:38 -0700
Subject: [PATCH] [pulse] Evaluate (e+0) as e

Summary: Pulse evaluated (e1+e2) as a new value that is a sum of evaluation results of e1 and e2.  However, when e2 is known as zero, we can have a simpler evaluation result without introducing the new value. This diff returns the evaluation result of e1 when e2 is known as zero.

Reviewed By: ngorogiannis

Differential Revision: D29736444

fbshipit-source-id: d5ce5a60e
---
 infer/src/pulse/PulseOperations.ml         | 25 ++++++++++++++--------
 infer/tests/codetoanalyze/c/pulse/uninit.c | 14 ++++++++++++
 2 files changed, 30 insertions(+), 9 deletions(-)

diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml
index 205c33e3e..7aed9e313 100644
--- a/infer/src/pulse/PulseOperations.ml
+++ b/infer/src/pulse/PulseOperations.ml
@@ -257,16 +257,23 @@ let eval path mode location exp0 astate =
         let unop_addr = AbstractValue.mk_fresh () in
         let+ astate = PulseArithmetic.eval_unop unop_addr unop addr astate in
         (astate, (unop_addr, hist))
-    | BinOp (bop, e_lhs, e_rhs) ->
+    | BinOp (bop, e_lhs, e_rhs) -> (
         let* astate, (addr_lhs, hist_lhs) = eval path Read e_lhs astate in
-        (* NOTE: keeping track of only [hist_lhs] into the binop is not the best *)
-        let* astate, (addr_rhs, _hist_rhs) = eval path Read e_rhs astate in
-        let binop_addr = AbstractValue.mk_fresh () in
-        let+ astate =
-          PulseArithmetic.eval_binop binop_addr bop (AbstractValueOperand addr_lhs)
-            (AbstractValueOperand addr_rhs) astate
-        in
-        (astate, (binop_addr, hist_lhs))
+        let* astate, (addr_rhs, hist_rhs) = eval path Read e_rhs astate in
+        match bop with
+        | (PlusA _ | PlusPI | MinusA _ | MinusPI) when PulseArithmetic.is_known_zero astate addr_rhs
+          ->
+            Ok (astate, (addr_lhs, hist_lhs))
+        | PlusA _ when PulseArithmetic.is_known_zero astate addr_lhs ->
+            Ok (astate, (addr_rhs, hist_rhs))
+        | _ ->
+            let binop_addr = AbstractValue.mk_fresh () in
+            let+ astate =
+              PulseArithmetic.eval_binop binop_addr bop (AbstractValueOperand addr_lhs)
+                (AbstractValueOperand addr_rhs) astate
+            in
+            (* NOTE: keeping track of only [hist_lhs] into the binop is not the best *)
+            (astate, (binop_addr, hist_lhs)) )
     | Const _ | Sizeof _ | Exn _ ->
         Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) []))
   in
diff --git a/infer/tests/codetoanalyze/c/pulse/uninit.c b/infer/tests/codetoanalyze/c/pulse/uninit.c
index 182870d47..f8356f6fc 100644
--- a/infer/tests/codetoanalyze/c/pulse/uninit.c
+++ b/infer/tests/codetoanalyze/c/pulse/uninit.c
@@ -159,3 +159,17 @@ void nested_struct_bad() {
   x.g1.f2 = 42;
   read_g1_f1(&x);
 }
+
+void init_ptr_zero(int* ptr, int i) {
+  if (i != 0) {
+    *ptr = 42;
+  } else {
+    *(ptr + i) = 42;
+  }
+}
+
+void call_init_ptr_zero_good() {
+  int x;
+  init_ptr_zero(&x, 0);
+  int y = x;
+}