From 86861498a5ad7cc7b2efcf636a6f1a59838bb1ca Mon Sep 17 00:00:00 2001 From: Radu Grigore Date: Sat, 9 Mar 2019 13:54:35 -0800 Subject: [PATCH] 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 | 66 +++++++++++++++---- infer/src/biabduction/Prop.ml | 25 ++++--- infer/tests/codetoanalyze/cpp/errors/Makefile | 1 + .../biabduction/process_splitting_assert.cpp | 43 ++++++++++++ .../tests/codetoanalyze/cpp/errors/issues.exp | 1 + .../codetoanalyze/objc/errors/issues.exp | 2 +- 6 files changed, 115 insertions(+), 23 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/errors/biabduction/process_splitting_assert.cpp diff --git a/infer/src/biabduction/Dom.ml b/infer/src/biabduction/Dom.ml index ed25eeea2..f2a12d772 100644 --- a/infer/src/biabduction/Dom.ml +++ b/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 compare (i, _) (i', _) = Ident.compare i i' in - List.sort ~compare sub_list - in - let rec find_duplicates = function - | (i, _) :: ((i', _) :: _ as t) -> - Ident.equal i i' || find_duplicates t - | _ -> - false + let uniq_sub_list = + let compare (i, _) (j, _) = Ident.compare i j in + List.dedup_and_sort ~compare sub_list in - if find_duplicates sub_list_sorted then ( L.d_strln "failure reason 12" ; raise Sil.JoinFail ) - else Sil.subst_of_list sub_list_sorted + Sil.subst_of_list uniq_sub_list 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} *) diff --git a/infer/src/biabduction/Prop.ml b/infer/src/biabduction/Prop.ml index a3b4796d8..4282897ae 100644 --- a/infer/src/biabduction/Prop.ml +++ b/infer/src/biabduction/Prop.ml @@ -1721,16 +1721,25 @@ 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'' = - match a' with - | Aeq (Exp.Var i, e) when not (Exp.ident_mem e i) -> - let mysub = Sil.subst_of_list [(i, e)] in - let sigma_fp' = sigma_normalize tenv mysub p'.sigma_fp in - let pi_fp' = a' :: pi_normalize tenv mysub sigma_fp' p'.pi_fp in - footprint_normalize tenv (set p' ~pi_fp:pi_fp' ~sigma_fp:sigma_fp') - | _ -> - footprint_normalize tenv (set p' ~pi_fp:(a' :: p'.pi_fp)) + 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 + let sigma_fp' = sigma_normalize tenv mysub p'.sigma_fp in + let pi_fp' = a' :: pi_normalize tenv mysub sigma_fp' p'.pi_fp in + footprint_normalize tenv (set p' ~pi_fp:pi_fp' ~sigma_fp:sigma_fp') + | _ -> + 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'' diff --git a/infer/tests/codetoanalyze/cpp/errors/Makefile b/infer/tests/codetoanalyze/cpp/errors/Makefile index d1aa4c172..3a986d81e 100644 --- a/infer/tests/codetoanalyze/cpp/errors/Makefile +++ b/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 \ diff --git a/infer/tests/codetoanalyze/cpp/errors/biabduction/process_splitting_assert.cpp b/infer/tests/codetoanalyze/cpp/errors/biabduction/process_splitting_assert.cpp new file mode 100644 index 000000000..e6d6797fa --- /dev/null +++ b/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 +#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'; + } +} diff --git a/infer/tests/codetoanalyze/cpp/errors/issues.exp b/infer/tests/codetoanalyze/cpp/errors/issues.exp index 1bc68d49c..76a632e9d 100644 --- a/infer/tests/codetoanalyze/cpp/errors/issues.exp +++ b/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>___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_Pointer,start of procedure Pointer,return from a call to unique_ptr_with_deleter::Pointer_Pointer] INFER_MODEL/cpp/include/infer_model/unique_ptr.h, std::unique_ptr>___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_Pointer,start of procedure Pointer,return from a call to unique_ptr_with_deleter::Pointer_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()] diff --git a/infer/tests/codetoanalyze/objc/errors/issues.exp b/infer/tests/codetoanalyze/objc/errors/issues.exp index 6cad5c9e3..d438cb5f9 100644 --- a/infer/tests/codetoanalyze/objc/errors/issues.exp +++ b/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]