[pulse] record aliasing information in the arithmetic

Summary:
Until then we mostly ignored aliasing constraints added by callees,
except some of the cases where the aliasing was incompatible with the
current heap. But, we should add `v_caller = v_caller'` any time both
of these (caller) variables are equal to the same callee variable.

These situations are hard to create at the moment since all values in
the pre-condition heap are created distinct and never change. The next
diff introduces canonicalisation of states and merges equal variables,
thus needs this change.

Reviewed By: skcho

Differential Revision: D25092213

fbshipit-source-id: 9fa7b8b53

infer/src/pulse/PulseInterproc.ml

@@ -92,20 +92,42 @@ let fold_globals_of_stack call_loc stack call_state ~f =
           Ok call_state )
 
 
+let and_aliasing_arith ~addr_callee ~addr_caller0 call_state =
+  match AddressMap.find_opt addr_callee call_state.subst with
+  | Some (addr_caller', _) when not (AbstractValue.equal addr_caller' addr_caller0) ->
+      (* NOTE: discarding new equalities here instead of passing them to
+         {!AbductiveDomain.incorporate_new_eqs} because it would be too slow to do each time we
+         visit a new address. We should re-normalize at the end of the call instead (TODO). *)
+      let path_condition, _new_eqs =
+        PathCondition.and_eq_vars addr_caller0 addr_caller'
+          call_state.astate.AbductiveDomain.path_condition
+      in
+      if PathCondition.is_unsat_cheap path_condition then raise (Contradiction PathCondition)
+      else
+        {call_state with astate= AbductiveDomain.set_path_condition path_condition call_state.astate}
+  | _ ->
+      call_state
+
+
 let visit call_state ~pre ~addr_callee ~addr_hist_caller =
   let addr_caller = fst addr_hist_caller in
-  ( match AddressMap.find_opt addr_caller call_state.rev_subst with
-  | Some addr_callee' when not (AbstractValue.equal addr_callee addr_callee') ->
-      (* [addr_caller] corresponds to several values in the callee, see if that's a problem for
-         applying the pre-condition, i.e. if both values are addresses in the callee's heap, which
-         means they must be disjoint. If so, raise a contradiction, but if not then continue as it
-         just means that the callee doesn't care about the value of these variables. *)
-      if
-        BaseMemory.mem addr_callee pre.BaseDomain.heap
-        && BaseMemory.mem addr_callee' pre.BaseDomain.heap
-      then raise (Contradiction (Aliasing {addr_caller; addr_callee; addr_callee'; call_state}))
-  | _ ->
-      () ) ;
+  let call_state =
+    match AddressMap.find_opt addr_caller call_state.rev_subst with
+    | Some addr_callee' when not (AbstractValue.equal addr_callee addr_callee') ->
+        if
+          (* [addr_caller] corresponds to several values in the callee, see if that's a problem for
+             applying the pre-condition, i.e. if both values are addresses in the callee's heap,
+             which means they must be disjoint. If so, raise a contradiction, but if not then
+             continue as it just means that the callee doesn't care about the value of these
+             variables, but record that they are equal. *)
+          BaseMemory.mem addr_callee pre.BaseDomain.heap
+          && BaseMemory.mem addr_callee' pre.BaseDomain.heap
+        then raise (Contradiction (Aliasing {addr_caller; addr_callee; addr_callee'; call_state}))
+        else and_aliasing_arith ~addr_callee:addr_callee' ~addr_caller0:addr_caller call_state
+    | _ ->
+        call_state
+  in
+  let call_state = and_aliasing_arith ~addr_callee ~addr_caller0:addr_caller call_state in
   if AddressSet.mem addr_callee call_state.visited then (`AlreadyVisited, call_state)
   else
     ( `NotAlreadyVisited

infer/src/pulse/PulsePathCondition.ml

@@ -91,6 +91,15 @@ let and_eq_int v i phi =
   , new_eqs )
 
 
+let and_eq_vars v1 v2 phi =
+  let+ {is_unsat; bo_itvs; citvs; formula} = phi in
+  let+| formula, new_eqs =
+    Formula.and_equal (AbstractValueOperand v1) (AbstractValueOperand v2) formula
+  in
+  (* TODO: add to non-formula domains? *)
+  ({is_unsat; bo_itvs; citvs; formula}, new_eqs)
+
+
 let simplify ~keep phi =
   let+ {is_unsat; bo_itvs; citvs; formula} = phi in
   let+| formula, new_eqs = Formula.simplify ~keep formula in

infer/src/pulse/PulsePathCondition.mli

@@ -31,6 +31,8 @@ val and_positive : AbstractValue.t -> t -> t * new_eqs
 val and_eq_int : AbstractValue.t -> IntLit.t -> t -> t * new_eqs
 (** [and_eq_int v i phi] is [phi ∧ v=i] *)
 
+val and_eq_vars : AbstractValue.t -> AbstractValue.t -> t -> t * new_eqs
+
 val simplify : keep:AbstractValue.Set.t -> t -> t * new_eqs
 (** [simplify ~keep phi] attempts to get rid of as many variables in [fv phi] but not in [keep] as
     possible *)