[pulse] Normalize return values of binop/unop

Summary:
In D29736444 (320c82d9ad), we added an ad-hoc simplification of formula. This diff reverts the diff and addresses the issue in the normalization logic.

Problem:

Before the D29736444 (320c82d9ad) diff, given `p1=p2+0;`, Pulse could not reason correctly that the pointers `p1` and `p2` are alias.  While we tried to solve the issue by an ad-hoc simplification (addressing it as `p1=p2;`), the real bug was in the normalization logic.

https://www.internalfb.com/code/infer/[62c8b92c390587538b9e16032b72af56efe2b527]/infer/src/pulse/PulseOperations.ml?lines=270-276

Here, it makes a new value of `binop_addr` and returns it as a result of a binary operation. However, inside `PulseArithmetic.eval_binop`, if it finds an alias between `binop_addr` and another one `alias_addr`, it replaces all `binop_addr` in `astate` into the `alias_addr`.  Thus, the last line returns `binop_addr` as a result, but there is no usage of which inside `astate`.

As a solution, we replaced `binop_addr` too, when needed.

Reviewed By: da319

Differential Revision: D29878980

fbshipit-source-id: 96a35bf16

infer/src/pulse/PulseAbductiveDomain.ml

@@ -1052,6 +1052,15 @@ let incorporate_new_eqs new_eqs astate =
         Error (`PotentialInvalidAccess (astate, address, must_be_valid))
 
 
+let incorporate_new_eqs_on_val new_eqs v =
+  List.find_map new_eqs ~f:(function
+    | PulseFormula.Equal (v1, v2) when AbstractValue.equal v1 v ->
+        Some v2
+    | _ ->
+        None )
+  |> Option.value ~default:v
+
+
 module Topl = struct
   let small_step loc event astate =
     {astate with topl= PulseTopl.small_step loc astate.path_condition event astate.topl}

infer/src/pulse/PulseAbductiveDomain.mli

@@ -216,6 +216,9 @@ val incorporate_new_eqs :
     and [y] being allocated separately. In those cases, the resulting path condition is
     {!PathCondition.false_}. *)
 
+val incorporate_new_eqs_on_val : PathCondition.new_eqs -> AbstractValue.t -> AbstractValue.t
+(** Similar to [incorporate_new_eqs], but apply to an abstract value. *)
+
 val initialize : AbstractValue.t -> t -> t
 (** Remove "Uninitialized" attribute of the given address *)
 

infer/src/pulse/PulseArithmetic.ml

@@ -10,11 +10,21 @@ open PulseBasicInterface
 module AbductiveDomain = PulseAbductiveDomain
 module AccessResult = PulseAccessResult
 
-let map_path_condition ~f astate =
+let map_path_condition_common ~f astate =
   let phi, new_eqs = f astate.AbductiveDomain.path_condition in
-  AbductiveDomain.set_path_condition phi astate
-  |> AbductiveDomain.incorporate_new_eqs new_eqs
-  |> AccessResult.of_abductive_result
+  let astate = AbductiveDomain.set_path_condition phi astate in
+  let result =
+    AbductiveDomain.incorporate_new_eqs new_eqs astate |> AccessResult.of_abductive_result
+  in
+  (result, new_eqs)
+
+
+let map_path_condition ~f astate = map_path_condition_common ~f astate |> fst
+
+let map_path_condition_with_ret ~f astate ret =
+  let result, new_eqs = map_path_condition_common ~f astate in
+  Result.map result ~f:(fun result ->
+      (result, AbductiveDomain.incorporate_new_eqs_on_val new_eqs ret) )
 
 
 let and_nonnegative v astate =
@@ -39,17 +49,17 @@ let and_equal op1 op2 astate =
 
 
 let eval_binop binop_addr binop op_lhs op_rhs astate =
-  map_path_condition astate ~f:(fun phi ->
+  map_path_condition_with_ret astate binop_addr ~f:(fun phi ->
       PathCondition.eval_binop binop_addr binop op_lhs op_rhs phi )
 
 
 let eval_unop unop_addr unop addr astate =
-  map_path_condition astate ~f:(fun phi -> PathCondition.eval_unop unop_addr unop addr phi)
+  map_path_condition_with_ret astate unop_addr ~f:(fun phi ->
+      PathCondition.eval_unop unop_addr unop addr phi )
 
 
 let prune_binop ~negated bop lhs_op rhs_op astate =
-  map_path_condition astate ~f:(fun phi ->
-      PathCondition.prune_binop ~negated bop lhs_op rhs_op phi )
+  map_path_condition astate ~f:(fun phi -> PathCondition.prune_binop ~negated bop lhs_op rhs_op phi)
 
 
 let prune_eq_zero v astate =

infer/src/pulse/PulseArithmetic.mli

@@ -32,14 +32,14 @@ val eval_binop :
   -> operand
   -> operand
   -> AbductiveDomain.t
-  -> AbductiveDomain.t AccessResult.t
+  -> (AbductiveDomain.t * AbstractValue.t) AccessResult.t
 
 val eval_unop :
      AbstractValue.t
   -> Unop.t
   -> AbstractValue.t
   -> AbductiveDomain.t
-  -> AbductiveDomain.t AccessResult.t
+  -> (AbductiveDomain.t * AbstractValue.t) AccessResult.t
 
 val prune_binop :
      negated:bool

infer/src/pulse/PulseModels.ml

@@ -480,7 +480,7 @@ module StdAtomicInteger = struct
   let arith_bop path prepost location event ret_id bop this operand astate =
     let* astate, int_addr, (old_int, hist) = load_backing_int path location this astate in
     let bop_addr = AbstractValue.mk_fresh () in
-    let* astate =
+    let* astate, bop_addr =
       PulseArithmetic.eval_binop bop_addr bop (AbstractValueOperand old_int) operand astate
     in
     let+ astate =
@@ -1438,7 +1438,7 @@ module JavaInteger = struct
     let<*> astate, _int_addr1, (int1, hist) = load_backing_int path location this astate in
     let<*> astate, _int_addr2, (int2, _) = load_backing_int path location arg astate in
     let binop_addr = AbstractValue.mk_fresh () in
-    let<+> astate =
+    let<+> astate, binop_addr =
       PulseArithmetic.eval_binop binop_addr Binop.Eq (AbstractValueOperand int1)
         (AbstractValueOperand int2) astate
     in

infer/src/pulse/PulseOperations.ml

@@ -255,25 +255,18 @@ let eval path mode location exp0 astate =
     | UnOp (unop, exp, _typ) ->
         let* astate, (addr, hist) = eval path Read exp astate in
         let unop_addr = AbstractValue.mk_fresh () in
-        let+ astate = PulseArithmetic.eval_unop unop_addr unop addr astate in
+        let+ astate, unop_addr = 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
-        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)) )
+        (* 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, binop_addr =
+          PulseArithmetic.eval_binop binop_addr bop (AbstractValueOperand addr_lhs)
+            (AbstractValueOperand addr_rhs) astate
+        in
+        (astate, (binop_addr, hist_lhs))
     | Const _ | Sizeof _ | Exn _ ->
         Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) []))
   in