[pulse] normalise caller addresses on the fly when applying summaries

Summary:
Exploring the precondition, and especially the formula of a summary can make us
learn new variable equalities that invalidate what was stored in (the range of)
the "callee abstract val -> caller abstract val" map. We didn't tackle this in
the earlier changes for on-the-fly canonicalisation, time to do so! This also
lets us ingest the entire callee formula in one go and avoids eager
normalisation of the substitution map.

Fixes facebook#1785

Reviewed By: skcho

Differential Revision: D50931121

fbshipit-source-id: 9c761e9f39720c022ef02e758dbc439cac211d5b

infer/src/pulse/PulseAccessResult.mli

@@ -23,6 +23,8 @@ type error =
           times. For convenience this is part of the [error] datatype but the invariant that an
           [error] within a [WithSummary (error, summary)] cannot itself be a [WithSummary _]. *)
 
+val astate_of_error : error -> AbductiveDomain.t
+
 type 'a t = ('a, error) PulseResult.t
 
 val with_summary : ('a, error * AbductiveDomain.Summary.t) PulseResult.t -> 'a t

infer/src/pulse/PulseFormula.ml

@@ -3963,13 +3963,15 @@ let subst_find_or_new subst addr_callee =
       (subst, fst addr_hist_caller)
 
 
-let and_callee_pre subst formula ~callee:formula_callee =
-  and_conditions_fold_subst_variables formula ~up_to_f:formula_callee ~f:subst_find_or_new
-    ~init:subst
-
-
-let and_callee_post subst formula_caller ~callee:formula_callee =
-  and_fold_subst_variables formula_caller ~up_to_f:formula_callee ~f:subst_find_or_new ~init:subst
+let and_callee_formula subst formula ~callee:formula_callee =
+  let* subst, formula, new_eqs =
+    and_conditions_fold_subst_variables formula ~up_to_f:formula_callee ~f:subst_find_or_new
+      ~init:subst
+  in
+  let+ subst, formula, new_eqs' =
+    and_fold_subst_variables ~up_to_f:formula_callee ~f:subst_find_or_new ~init:subst formula
+  in
+  (subst, formula, RevList.append new_eqs' new_eqs)
 
 
 let fold_variables {conditions; phi} ~init ~f =

infer/src/pulse/PulseFormula.mli

@@ -117,13 +117,7 @@ val is_manifest : is_allocated:(Var.t -> bool) -> t -> bool
 val get_var_repr : t -> Var.t -> Var.t
 (** get the canonical representative for the variable according to the equality relation *)
 
-val and_callee_pre :
-     (Var.t * ValueHistory.t) Var.Map.t
-  -> t
-  -> callee:t
-  -> ((Var.t * ValueHistory.t) Var.Map.t * t * new_eqs) SatUnsat.t
-
-val and_callee_post :
+val and_callee_formula :
      (Var.t * ValueHistory.t) Var.Map.t
   -> t
   -> callee:t

infer/tests/codetoanalyze/c/pulse/issues.exp

@@ -75,8 +75,6 @@ codetoanalyze/c/pulse/memory_leak.c, user_malloc_leak_bad, 0, MEMORY_LEAK_C, no_
 codetoanalyze/c/pulse/memory_leak.c, test_config_options_no_free_bad, 2, MEMORY_LEAK_C, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `my_realloc (custom realloc)` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, alloc_ref_counted_bad, 6, MEMORY_LEAK_C, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, return_malloc_deref_bad, 4, MEMORY_LEAK_C, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
-codetoanalyze/c/pulse/memory_leak.c, FP_alloc_then_free_all_in_array_ok, 3, MEMORY_LEAK_C, no_bucket, ERROR, [allocation part of the trace starts here,when calling `allocate_all_in_array` here,allocated by `malloc` here,memory becomes unreachable here]
-codetoanalyze/c/pulse/memory_leak.c, FP_alloc_then_free_42_in_array_ok, 3, MEMORY_LEAK_C, no_bucket, ERROR, [allocation part of the trace starts here,when calling `allocate_42_in_array` here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/nullptr.c, malloc_no_check_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc (null case)` (modelled),is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, create_null_path2_latent_FN, 8, NULLPTR_DEREFERENCE_LATENT, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,assigned,is assigned to the null pointer,null pointer dereference part of the trace starts here,parameter `p` of create_null_path2_latent_FN,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_unconditionally_latent_FN, 7, NULLPTR_DEREFERENCE_LATENT, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,in call to `malloc (null case)` (modelled),is assigned to the null pointer,null pointer dereference part of the trace starts here,parameter `p` of malloc_then_call_create_null_path_then_deref_unconditionally_latent_FN,invalid access occurs here]

infer/tests/codetoanalyze/c/pulse/memory_leak.c

@@ -227,7 +227,7 @@ void free_all_in_array(int* array[]) {
   }
 }
 
-void FP_alloc_then_free_all_in_array_ok() {
+void alloc_then_free_all_in_array_ok() {
   int* array[2];
   allocate_all_in_array(array);
   free_all_in_array(array);
@@ -241,7 +241,7 @@ void free_42_in_array(int* array[]) {
   free(array[42]);
 }
 
-void FP_alloc_then_free_42_in_array_ok() {
+void alloc_then_free_42_in_array_ok() {
   int* array[64];
   allocate_42_in_array(array);
   free_42_in_array(array);

infer/tests/codetoanalyze/objc/pulse/issues.exp

@@ -263,6 +263,7 @@ codetoanalyze/objc/pulse/taint/testNSArray.m, testNSArray_cell_ReplaceObjectAtIn
 codetoanalyze/objc/pulse/taint/testNSArray.m, testNSArray_cell_SetObjectAtIndexedSubscript_bad, 4, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `create_tainted` with kind `SimpleSource`,value passed as argument `#0` to `testNSArray_sink` with kind `SimpleSink`], source: create_tainted, sink: testNSArray_sink, tainted expression: value
 codetoanalyze/objc/pulse/taint/testNSArray.m, testNSArray_cell_ArrayWithArrayBad, 5, TAINT_ERROR, no_bucket, ERROR, [in call to `init_NSMutableArray_with_tainted_and_untainted`,source of the taint here: value returned from `create_tainted` with kind `SimpleSource`,return from call to `init_NSMutableArray_with_tainted_and_untainted`,value passed as argument `#0` to `testNSArray_sink` with kind `SimpleSink`], source: create_tainted, sink: testNSArray_sink, tainted expression: value
 codetoanalyze/objc/pulse/taint/testNSArray.m, testNSArray_cell_sinkInCalleeBad, 2, TAINT_ERROR, no_bucket, ERROR, [in call to `init_NSMutableArray_with_tainted_and_untainted`,source of the taint here: value returned from `create_tainted` with kind `SimpleSource`,return from call to `init_NSMutableArray_with_tainted_and_untainted`,when calling `sinkObjectAt0` here,value passed as argument `#0` to `testNSArray_sink` with kind `SimpleSink`], source: create_tainted, sink: testNSArray_sink, tainted expression: UNKNOWN
+codetoanalyze/objc/pulse/taint/testNSArray.m, testNSArray_cell_sinkInCalleeBad, 2, TAINT_ERROR, no_bucket, ERROR, [in call to `init_NSMutableArray_with_tainted_and_untainted`,source of the taint here: value returned from `create_tainted` with kind `SimpleSource`,return from call to `init_NSMutableArray_with_tainted_and_untainted`,when calling `sinkObjectAt0` here,value passed as argument `#0` to `testNSArray_sink` with kind `SimpleSink`], source: create_tainted, sink: testNSArray_sink, tainted expression: mArr->__infer_backing_array[_]
 codetoanalyze/objc/pulse/taint/testNSDictionary.m, testNSDictionary_DictionaryWithObjectsForKeysBad, 4, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `create_tainted` with kind `SimpleSource`,in call to `NSDictionary.dictionaryWithObjects:forKeys:`,value passed as argument `#0` to `testNSDictionary_sink` with kind `SimpleSink`], source: create_tainted, sink: testNSDictionary_sink, tainted expression: propagated
 codetoanalyze/objc/pulse/taint/testNSDictionary.m, testNSDictionary_DictionaryWithObjectsForKeysCountBad, 6, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `create_tainted_id` with kind `SimpleSource`,in call to `NSDictionary.dictionaryWithObjects:forKeys:count:`,value passed as argument `#0` to `testNSDictionary_sink` with kind `SimpleSink`], source: create_tainted_id, sink: testNSDictionary_sink, tainted expression: propagated
 codetoanalyze/objc/pulse/taint/testNSDictionary.m, testNSDictionary_InitWithObjectsForKeysBad, 4, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `create_tainted` with kind `SimpleSource`,in call to `NSDictionary.initWithObjects:forKeys:`,value passed as argument `#0` to `testNSDictionary_sink` with kind `SimpleSink`], source: create_tainted, sink: testNSDictionary_sink, tainted expression: propagated