Slightly more precise pi_partial_meet

Summary:
To meet the pure parts of formulas, the process was to (a) call Rename.extend
with variables occuring in similar places and (b) extract substitutions out of
those. Two matching primed vars would both be replaced by some fresh primed var.
However, equivalence classes of primed variables would *not* be replaced by
one fresh (primed) variable. Now, that should work.

Reviewed By: mbouaziz

Differential Revision: D14150192

fbshipit-source-id: 90ca9216c

infer/src/biabduction/Dom.ml

@@ -48,7 +48,7 @@ let sigma_get_start_lexps_sort sigma =
 
 (** {2 Utility functions for side} *)
 
-type side = Lhs | Rhs
+type side = Lhs | Rhs [@@deriving compare]
 
 let select side e1 e2 = match side with Lhs -> e1 | Rhs -> e2
 
@@ -523,6 +523,8 @@ module Rename : sig
 
   val to_subst_proj : side -> unit Ident.HashQueue.t -> Sil.subst
 
+  val get_unify_eqs : unit -> (Exp.t * Exp.t) list
+
   val to_subst_emb : side -> Sil.subst
   (*
   val get : Exp.t -> Exp.t -> Exp.t option
@@ -656,6 +658,47 @@ end = struct
     else Sil.subst_of_list sub_list_side
 
 
+  module SideExpPairHash = Hashtbl.Make (struct
+    type t = side * Exp.t [@@deriving compare]
+
+    let hash = Hashtbl.hash
+
+    let equal = [%compare.equal: t]
+  end)
+
+  (* Each triple (L,R,U) in !tbl gives rise to an edge (Lhs,L)--(Rhs,R)
+  labeled by U. For each connected component, return equalities that constrain
+  all its Us to be equal. *)
+  let get_unify_eqs () : (Exp.t * Exp.t) list =
+    let find_classes () =
+      let module UF = Union_find in
+      let uf = Memo.general UF.create in
+      let handle_triple (le, re, _) = UF.union (uf (Lhs, le)) (uf (Rhs, re)) in
+      List.iter ~f:handle_triple !tbl ;
+      let get x = UF.get (uf x) in
+      get
+    in
+    let pick_rep get =
+      let module H = SideExpPairHash in
+      let rep_cache = H.create (2 * List.length !tbl) in
+      let handle_triple (le, re, ue) =
+        H.replace rep_cache (get (Lhs, le)) ue ;
+        H.replace rep_cache (get (Rhs, re)) ue
+      in
+      List.iter ~f:handle_triple !tbl ;
+      let rep x =
+        try H.find rep_cache (get x) with Caml.Not_found ->
+          L.die L.InternalError "Dom.Rename.get_unify_eqs broken"
+      in
+      rep
+    in
+    let make_eqs rep =
+      let f (le, _, ue) = (ue, rep (Lhs, le)) in
+      List.rev_map ~f !tbl
+    in
+    () |> find_classes |> pick_rep |> make_eqs
+
+
   let to_subst_emb (side : side) =
     let renaming_restricted =
       let pick_id_case (e1, e2, _) =
@@ -669,18 +712,11 @@ end = struct
       in
       List.map ~f:project renaming_restricted
     in
-    let sub_list_sorted =
+    let uniq_sub_list =
-      let compare (i, _) (i', _) = Ident.compare i i' in
+      let compare (i, _) (j, _) = Ident.compare i j in
-      List.sort ~compare sub_list
+      List.dedup_and_sort ~compare sub_list
-    in
-    let rec find_duplicates = function
-      | (i, _) :: ((i', _) :: _ as t) ->
-          Ident.equal i i' || find_duplicates t
-      | _ ->
-          false
     in
-    if find_duplicates sub_list_sorted then ( L.d_strln "failure reason 12" ; raise Sil.JoinFail )
+    Sil.subst_of_list uniq_sub_list
-    else Sil.subst_of_list sub_list_sorted
 
 
   let get_others' f_lookup side e =
@@ -1791,14 +1827,16 @@ let pi_partial_meet tenv (p : Prop.normal Prop.t) (ep1 : 'a Prop.t) (ep2 : 'b Pr
   in
   let f1 p' atom = Prop.prop_atom_and tenv p' (handle_atom sub1 dom1 atom) in
   let f2 p' atom = Prop.prop_atom_and tenv p' (handle_atom sub2 dom2 atom) in
+  let f3 p' (a, b) = Prop.conjoin_eq tenv a b p' in
   let pi1 = ep1.Prop.pi in
   let pi2 = ep2.Prop.pi in
   let p_pi1 = List.fold ~f:f1 ~init:p pi1 in
   let p_pi2 = List.fold ~f:f2 ~init:p_pi1 pi2 in
-  if Prover.check_inconsistency_base tenv p_pi2 then (
+  let p_pi3 = List.fold ~f:f3 ~init:p_pi2 (Rename.get_unify_eqs ()) in
+  if Prover.check_inconsistency_base tenv p_pi3 then (
     L.d_strln "check_inconsistency_base failed" ;
     raise Sil.JoinFail )
-  else p_pi2
+  else p_pi3
 
 
 (** {2 Join and Meet for Prop} *)

infer/src/biabduction/Prop.ml

@@ -1721,7 +1721,12 @@ module Normalize = struct
       in
       if not footprint then p'
       else
+        let predicate_warning =
+          not (Sil.atom_free_vars a' |> Sequence.for_all ~f:Ident.is_footprint)
+        in
         let p'' =
+          if predicate_warning then footprint_normalize tenv p'
+          else
             match a' with
             | Aeq (Exp.Var i, e) when not (Exp.ident_mem e i) ->
                 let mysub = Sil.subst_of_list [(i, e)] in
@@ -1731,6 +1736,10 @@ module Normalize = struct
             | _ ->
                 footprint_normalize tenv (set p' ~pi_fp:(a' :: p'.pi_fp))
         in
+        if predicate_warning then (
+          L.d_warning "dropping non-footprint " ;
+          Sil.d_atom a' ;
+          L.d_ln () ) ;
         unsafe_cast_to_normal p''
 
 

infer/tests/codetoanalyze/cpp/errors/Makefile

@@ -12,6 +12,7 @@ INFER_OPTIONS = --biabduction-only --ml-buckets cpp --debug-exceptions --project
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES = \
+  $(wildcard biabduction/*.cpp) \
   $(wildcard c_tests/*.cpp) \
   include_header/header.h \
   include_header/include_templ.cpp \

infer/tests/codetoanalyze/cpp/errors/biabduction/process_splitting_assert.cpp

@@ -0,0 +1,43 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <memory.h>
+#define size_t int
+#define off_t int
+
+struct foo { // globals are treated differntly
+
+  char * memory_;
+  size_t memory_size_;
+
+  bool ReadBytes(void *buffer, size_t size, off_t offset) {
+    if (memory_) {
+      if (offset < 0) {
+        return false;
+      }
+      if (offset + size >= memory_size_) {
+          return false;
+      }
+      memcpy(buffer, memory_ + offset, size);
+      return true;
+    } else {
+      return false;
+    }
+  }
+
+  void FindHeader(off_t &offset) {
+    int magic;
+    ReadBytes(&magic, sizeof(magic), 0);
+    ReadBytes(&magic, sizeof(magic), 0);
+  }
+
+};
+
+void fail(char * x) {
+  if (x == 0) {
+    *x = 'a';
+  }
+}

infer/tests/codetoanalyze/cpp/errors/issues.exp

@@ -1,6 +1,7 @@
 INFER_MODEL/cpp/include/infer_model/unique_ptr.h, std::operator!=<65d659492edc5cb5>, 1, Abduction_case_not_implemented, no_bucket, ERROR, [start of procedure std::operator!=<65d659492edc5cb5>()]
 INFER_MODEL/cpp/include/infer_model/unique_ptr.h, std::unique_ptr<int,unique_ptr_with_deleter::Deleter<int>>___infer_inner_destructor_~unique_ptr, 0, Missing_fld, no_bucket, ERROR, [start of procedure __infer_inner_destructor_~unique_ptr,start of procedure Pointer,return from a call to unique_ptr_with_deleter::Pointer<int>_Pointer,start of procedure Pointer,return from a call to unique_ptr_with_deleter::Pointer<int>_Pointer]
 INFER_MODEL/cpp/include/infer_model/unique_ptr.h, std::unique_ptr<int[_*4],unique_ptr_with_deleter::Deleter<int[_*4]>>___infer_inner_destructor_~unique_ptr, 0, Missing_fld, no_bucket, ERROR, [start of procedure __infer_inner_destructor_~unique_ptr,start of procedure Pointer,return from a call to unique_ptr_with_deleter::Pointer<int[_*4]>_Pointer,start of procedure Pointer,return from a call to unique_ptr_with_deleter::Pointer<int[_*4]>_Pointer]
+codetoanalyze/cpp/errors/biabduction/process_splitting_assert.cpp, fail, 2, NULL_DEREFERENCE, B5, ERROR, [start of procedure fail(),Taking true branch]
 codetoanalyze/cpp/errors/c_tests/c_bugs.cpp, crash_fgetc, 4, NULL_DEREFERENCE, B1, ERROR, [start of procedure crash_fgetc()]
 codetoanalyze/cpp/errors/c_tests/c_bugs.cpp, crash_getc, 4, NULL_DEREFERENCE, B1, ERROR, [start of procedure crash_getc()]
 codetoanalyze/cpp/errors/c_tests/c_bugs.cpp, malloc_fail_gets_reported, 2, NULL_DEREFERENCE, B1, ERROR, [start of procedure malloc_fail_gets_reported()]

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

@@ -20,7 +20,7 @@ codetoanalyze/objc/shared/block/BlockVar.m, BlockVar_navigateToURLInBackground,
 codetoanalyze/objc/shared/block/block.m, main1, 30, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure main1(),start of procedure block,start of procedure block,return from a call to objc_blockobjc_blockmain1_2_3,return from a call to objc_blockmain1_2,start of procedure block,return from a call to objc_blockmain1_1]
 codetoanalyze/objc/shared/block/block_no_args.m, My_manager_m, 10, NULL_DEREFERENCE, B1, ERROR, [start of procedure m,start of procedure block,return from a call to objc_blockMy_manager_m_1,Taking true branch]
 codetoanalyze/objc/shared/category_procdesc/main.c, CategoryProcdescMain, 5, MEMORY_LEAK, no_bucket, ERROR, [start of procedure CategoryProcdescMain(),Skipping performDaysWork: method has no implementation,return from a call to CategoryProcdescMain]
-codetoanalyze/objc/shared/field_superclass/SuperExample.m, ASuper_init, 2, NULL_DEREFERENCE, B2, ERROR, [start of procedure init,start of procedure init,return from a call to BSuper_init]
+codetoanalyze/objc/shared/field_superclass/SuperExample.m, ASuper_init, 2, NULL_DEREFERENCE, B2, ERROR, [start of procedure init]
 codetoanalyze/objc/errors/blocks_in_heap/BlockInHeap.m, block_in_heap_executed_after_bi_abduction_ok_test, 3, NULL_DEREFERENCE, B1, ERROR, [start of procedure block_in_heap_executed_after_bi_abduction_ok_test(),start of procedure block_in_heap_executed_after_bi_abduction_ok_no_retain_cycle(),start of procedure assign_block_to_ivar,Executing synthesized setter setHandler:,return from a call to BlockInHeap_assign_block_to_ivar,Executing synthesized getter handler,start of procedure block,return from a call to objc_blockBlockInHeap_assign_block_to_ivar_1,return from a call to block_in_heap_executed_after_bi_abduction_ok_no_retain_cycle,Taking true branch]
 codetoanalyze/objc/errors/field_superclass/SubtypingExample.m, Employee_initWithName:andAge:andEducation:, 3, NULL_TEST_AFTER_DEREFERENCE, no_bucket, WARNING, [start of procedure initWithName:andAge:andEducation:,start of procedure initWithName:andAge:,return from a call to Person_initWithName:andAge:,Taking false branch]
 codetoanalyze/objc/errors/field_superclass/SubtypingExample.m, Employee_initWithName:andAge:andEducation:, 6, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure initWithName:andAge:andEducation:,start of procedure initWithName:andAge:,return from a call to Person_initWithName:andAge:,Taking true branch]