From 581487ec612942c0c5cb56a38aa5d8a173d71866 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 4 Dec 2020 07:29:50 -0800 Subject: [PATCH] [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 | 46 +++++++++++++++++++------- infer/src/pulse/PulsePathCondition.ml | 9 +++++ infer/src/pulse/PulsePathCondition.mli | 2 ++ 3 files changed, 45 insertions(+), 12 deletions(-) diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 44c4688d5..4cdd1cfce 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/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 diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index fecf0cd67..56ee70da2 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/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 diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli index 00c79175b..2159375df 100644 --- a/infer/src/pulse/PulsePathCondition.mli +++ b/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 *)