From 66365c2d547e74deca8bbb0353694b6387fd9bd5 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 9 Dec 2020 11:21:44 -0800 Subject: [PATCH] [pulse] add comment for [subst_find_or_new] Summary: I wrote an entire diff trying to fix the "bug" that this wasn't needed so I think this warrants a comment ;) Reviewed By: ezgicicek Differential Revision: D25423958 fbshipit-source-id: 414038e40 --- infer/src/pulse/PulseInterproc.ml | 23 ++++++++++++++--------- 1 file changed, 14 insertions(+), 9 deletions(-) diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 223fa84f3..be57aebdd 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -137,6 +137,20 @@ let visit call_state ~pre ~addr_callee ~addr_hist_caller = ; rev_subst= AddressMap.add addr_caller addr_callee call_state.rev_subst } ) +(** HACK: we don't need to update the [rev_subst] of a call state when generating a fresh value for + the caller because there's no chance that value appears anywhere else in the caller state, hence + we cannot possibly get clashes about that caller value, which is the only thing [rev_subst] is + used for. This is why this function is allowed to take only [subst] as argument and not a full + call state. *) +let subst_find_or_new subst addr_callee ~default_hist_caller = + match AddressMap.find_opt addr_callee subst with + | None -> + let addr_hist_fresh = (AbstractValue.mk_fresh (), default_hist_caller) in + (AddressMap.add addr_callee addr_hist_fresh subst, addr_hist_fresh) + | Some addr_hist_caller -> + (subst, addr_hist_caller) + + (* {3 reading the pre from the current state} *) let add_call_to_trace proc_name call_location caller_history in_call = @@ -222,15 +236,6 @@ let add_call_to_attributes proc_name call_location caller_history attrs = add_call_to_trace proc_name call_location caller_history trace ) ) -let subst_find_or_new subst addr_callee ~default_hist_caller = - match AddressMap.find_opt addr_callee subst with - | None -> - let addr_hist_fresh = (AbstractValue.mk_fresh (), default_hist_caller) in - (AddressMap.add addr_callee addr_hist_fresh subst, addr_hist_fresh) - | Some addr_hist_caller -> - (subst, addr_hist_caller) - - let conjoin_callee_arith pre_post call_state = L.d_printfln "applying callee path condition: (%a)[%a]" PathCondition.pp pre_post.AbductiveDomain.path_condition