diff --git a/infer/src/IR/Ident.ml b/infer/src/IR/Ident.ml index 1375b76bb..9ddf4e7b2 100644 --- a/infer/src/IR/Ident.ml +++ b/infer/src/IR/Ident.ml @@ -256,3 +256,9 @@ let hashqueue_of_sequence ?init s = let set_of_sequence ?(init = Set.empty) s = Sequence.fold s ~init ~f:(fun ids id -> Set.add id ids) + +let counts_of_sequence seq = + let h = Hash.create (Sequence.length seq) in + let get id = Option.value (Hash.find_opt h id) ~default:0 in + let bump id = Hash.replace h id (1 + get id) in + Sequence.iter ~f:bump seq ; get diff --git a/infer/src/IR/Ident.mli b/infer/src/IR/Ident.mli index 814caf2ee..6e2131f88 100644 --- a/infer/src/IR/Ident.mli +++ b/infer/src/IR/Ident.mli @@ -139,3 +139,5 @@ val to_string : t -> string val hashqueue_of_sequence : ?init:unit HashQueue.t -> t Sequence.t -> unit HashQueue.t val set_of_sequence : ?init:Set.t -> t Sequence.t -> Set.t + +val counts_of_sequence : t Sequence.t -> t -> int diff --git a/infer/src/biabduction/Abs.ml b/infer/src/biabduction/Abs.ml index 152765992..d84dfe00e 100644 --- a/infer/src/biabduction/Abs.ml +++ b/infer/src/biabduction/Abs.ml @@ -1152,6 +1152,92 @@ let check_junk pname tenv prop = else Prop.normalize tenv (Prop.set prop ~sigma:sigma_new ~sigma_fp:sigma_fp_new) +(** Removes (pure) atoms (such as v=E) containing a variable v that (a) has no other occurrence and + (b) [count v] is 0. The default count is the constant 0. One should use the argument count if + the proposition being simplified should make sense in a larger scope, which is not seen; + [count v] should give the number of occurrences of v in the context. *) +let remove_pure_garbage tenv ?(count = fun _ -> 0) prop = + if Prop.has_footprint prop then L.d_warning "Abs.remove_pure_garbage ignores footprint" ; + (* Normalization may change counts of occurrences. Which free variables we drop depends on counts. + Dropping variables involves exposing the Prop.t, so we must necessarily re-normalize. Since we change + counts again, other variables may become dropable. We start with normalization, which empirically leads + to more dropping. *) + let changed = ref false in + let rec go prop = + let propcount = prop |> Prop.free_vars |> Ident.counts_of_sequence in + let prop = Prop.set prop ~pi:(Prop.get_pure prop) ~sub:Sil.sub_empty in + let drop id = Int.equal 1 (count id + propcount id) in + let keep atom = not (Sequence.exists ~f:drop (Sil.atom_free_vars atom)) in + let pi = List.filter ~f:keep prop.Prop.pi in + let dropped = List.length pi < List.length prop.Prop.pi in + changed := !changed || dropped ; + let prop = Prop.set ~pi prop in + let prop = Prop.normalize tenv prop in + if dropped then go prop else prop + in + (go prop, !changed) + + +(* During re-execution, free variables in Prop.t have the whole spec as their scope. Thus, most +functions in Prop abstain from dropping free variables. Here, however, we can do it. Let's call an +atom an orphan when it contains a variable v that does not occur anywhere else in the spec. Orphans +can be dropped. Alpha-renaming can create orphans. Thus, we will perform a best-effort fixpoint +computation (rename, drop)*, stopping when the last drop is a no-op. *) +let abstract_spec pname tenv spec = + let open BiabductionSummary in + let rename spec = spec_normalize tenv spec in + let drop spec = + let changed = ref false in + let precount = spec.pre |> Jprop.to_prop |> Prop.free_vars |> Ident.counts_of_sequence in + let update_post (p, path) = + let p, dropped = remove_pure_garbage tenv p ~count:precount in + changed := !changed || dropped ; + (p, path) + in + let posts = List.map ~f:update_post spec.posts in + let spec = {spec with posts} in + (spec, !changed) + in + let rec loop spec = + let s1 = rename spec in + let s2, changed = drop (expose s1) in + if changed then loop s2 else s1 + in + let collapse_posts spec = + let spec = expose spec in + let implies (prop1, _path1) (prop2, _path2) = + (* TODO(rgrigore): [Prover.check_implication] gives up immediately if the consequence contains + a disequality. As a workaround, here we drop pure facts from the consequent that are known to + be true. *) + let module AtomSet = Caml.Set.Make (struct + type t = Sil.atom + + let compare = Sil.compare_atom + end) in + let pre_pure = + let pre = Jprop.to_prop spec.pre in + AtomSet.of_list (Prop.get_pure pre) + in + let prop1_pure = AtomSet.of_list (Prop.get_pure prop1) in + let known = AtomSet.union pre_pure prop1_pure in + let toprove = AtomSet.of_list prop2.Prop.pi in + let toprove = AtomSet.diff toprove known in + let prop2 = Prop.set prop2 ~pi:(AtomSet.elements toprove) in + Prover.check_implication pname tenv prop1 prop2 + in + let rec filter kept x unseen = + (* INV: if a is kept and b is kept or unseen then (not (implies a b)). + We keep x unless that would break the invariant. *) + let others = List.rev_append kept unseen in + let kept = if List.exists ~f:(implies x) others then kept else x :: kept in + match unseen with [] -> kept | y :: unseen -> filter kept y unseen + in + let posts = match spec.posts with [] | [_] -> spec.posts | p :: posts -> filter [] p posts in + {spec with posts} + in + rename (collapse_posts (loop spec)) + + (** Check whether the prop contains junk. If it does, and [Config.allowleak] is true, remove the junk, otherwise raise a Leak exception. *) let abstract_junk pname tenv prop = diff --git a/infer/src/biabduction/Abs.mli b/infer/src/biabduction/Abs.mli index e52e3a64f..a80de2c2b 100644 --- a/infer/src/biabduction/Abs.mli +++ b/infer/src/biabduction/Abs.mli @@ -16,6 +16,11 @@ type rules val abstract : Typ.Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t (** Abstract a proposition. *) +val abstract_spec : + Typ.Procname.t -> Tenv.t -> Prop.normal BiabductionSummary.spec -> BiabductionSummary.NormSpec.t +(** Normalizes names and applies simplifications, soem of which require looking at both pre and + post. *) + val abstract_junk : Typ.Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t (** Check whether the prop contains junk. If it does, and [Config.allowleak] is true, remove the junk, otherwise raise a Leak exception. *) diff --git a/infer/src/biabduction/BiabductionSummary.ml b/infer/src/biabduction/BiabductionSummary.ml index 76b11c2e4..d31feaf09 100644 --- a/infer/src/biabduction/BiabductionSummary.ml +++ b/infer/src/biabduction/BiabductionSummary.ml @@ -126,6 +126,13 @@ module Jprop = struct do_filter [] jpl + let shallow_map ~f = function + | Prop (n, p) -> + Prop (n, f p) + | Joined (n, p, jp1, jp2) -> + Joined (n, f p, jp1, jp2) + + let rec map (f : 'a Prop.t -> 'b Prop.t) = function | Prop (n, p) -> Prop (n, f p) @@ -168,17 +175,17 @@ module NormSpec : sig val normalize : Tenv.t -> Prop.normal spec -> t - val tospecs : t list -> Prop.normal spec list - val compact : Sil.sharing_env -> t -> t (** Return a compact representation of the spec *) + val tospec : t -> Prop.normal spec + val erase_join_info_pre : Tenv.t -> t -> t (** Erase join info from pre of spec *) end = struct type t = Prop.normal spec - let tospecs specs = specs + let tospec spec = spec let gen_free_vars tenv (spec : Prop.normal spec) = let open Sequence.Generator in @@ -197,7 +204,6 @@ end = struct ; visited= spec.visited } - (** Convert spec into normal form w.r.t. variable renaming *) let normalize tenv (spec : Prop.normal spec) : Prop.normal spec = let idlist = free_vars tenv spec |> Ident.hashqueue_of_sequence |> Ident.HashQueue.keys in let count = ref 0 in @@ -225,11 +231,13 @@ end = struct normalize tenv spec' end -(** Convert spec into normal form w.r.t. variable renaming *) +(** Convert spec into normal form *) let spec_normalize = NormSpec.normalize +let expose = NormSpec.tospec + (** Cast a list of normalized specs to a list of specs *) -let normalized_specs_to_specs = NormSpec.tospecs +let normalized_specs_to_specs = List.map ~f:NormSpec.tospec type phase = FOOTPRINT | RE_EXECUTION [@@deriving compare] @@ -279,11 +287,14 @@ let pp_specs pe fmt specs = F.fprintf fmt "%a
@\n" (pp_spec0 pe (Some (cnt + 1, total))) spec ) -let get_specs_from_preposts preposts = Option.value_map ~f:NormSpec.tospecs ~default:[] preposts +let get_specs_from_preposts preposts = + Option.value_map ~f:(List.map ~f:NormSpec.tospec) ~default:[] preposts + type t = {preposts: NormSpec.t list; phase: phase} let opt_get_phase = function None -> FOOTPRINT | Some {phase} -> phase let pp pe fmt {preposts; phase} = - F.fprintf fmt "phase= %s@\n%a" (string_of_phase phase) (pp_specs pe) (NormSpec.tospecs preposts) + F.fprintf fmt "phase= %s@\n%a" (string_of_phase phase) (pp_specs pe) + (List.map ~f:NormSpec.tospec preposts) diff --git a/infer/src/biabduction/BiabductionSummary.mli b/infer/src/biabduction/BiabductionSummary.mli index 3cb12d033..ab6a5ab1c 100644 --- a/infer/src/biabduction/BiabductionSummary.mli +++ b/infer/src/biabduction/BiabductionSummary.mli @@ -37,6 +37,9 @@ module Jprop : sig val map : ('a Prop.t -> 'b Prop.t) -> 'a t -> 'b t (** map the function to each prop in the jprop, pointwise *) + val shallow_map : f:('a Prop.t -> 'a Prop.t) -> 'a t -> 'a t + (** map f over the top-level prop *) + val to_prop : 'a t -> 'a Prop.t (** Extract the toplevel jprop of a prop *) end @@ -62,13 +65,15 @@ module NormSpec : sig (** Erase join info from pre of spec *) end +val expose : NormSpec.t -> Prop.normal spec + val normalized_specs_to_specs : NormSpec.t list -> Prop.normal spec list (** Cast a list of normalized specs to a list of specs *) val pp_spec : Format.formatter -> _ spec -> unit val spec_normalize : Tenv.t -> Prop.normal spec -> NormSpec.t -(** Convert spec into normal form w.r.t. variable renaming *) +(** Convert spec into normal form. *) type phase = FOOTPRINT | RE_EXECUTION diff --git a/infer/src/biabduction/Prop.ml b/infer/src/biabduction/Prop.ml index a49c99d88..fafa56fa5 100644 --- a/infer/src/biabduction/Prop.ml +++ b/infer/src/biabduction/Prop.ml @@ -47,6 +47,8 @@ module Core : sig ; pi_fp: pi (** abduced pure part *) } [@@deriving compare] + val has_footprint : 'a t -> bool + val prop_emp : normal t (** Proposition [true /\ emp]. *) @@ -72,6 +74,8 @@ end = struct ; pi_fp: pi (** abduced pure part *) } [@@deriving compare] + let has_footprint {sigma_fp; pi_fp} = not (List.is_empty sigma_fp && List.is_empty pi_fp) + (** Proposition [true /\ emp]. *) let prop_emp : normal t = {sub= Sil.sub_empty; pi= []; sigma= []; pi_fp= []; sigma_fp= []} diff --git a/infer/src/biabduction/Prop.mli b/infer/src/biabduction/Prop.mli index 08b19aa1e..0d42691b4 100644 --- a/infer/src/biabduction/Prop.mli +++ b/infer/src/biabduction/Prop.mli @@ -43,6 +43,9 @@ type struct_init_mode = No_init | Fld_init (** {2 Basic Functions for propositions} *) +val has_footprint : 'a t -> bool +(** sigma_fp is nonempty or pi_fp is nonempty *) + val compare_prop : 'a t -> 'a t -> int (** Compare propositions *) diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 058530c88..e7a850162 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -789,14 +789,7 @@ let execute_filter_prop summary exe_env tenv proc_cfg (plist, visited) in let pre = - let p = - PropUtil.remove_locals_ret tenv pdesc (BiabductionSummary.Jprop.to_prop precondition) - in - match precondition with - | BiabductionSummary.Jprop.Prop (n, _) -> - BiabductionSummary.Jprop.Prop (n, p) - | BiabductionSummary.Jprop.Joined (n, _, jp1, jp2) -> - BiabductionSummary.Jprop.Joined (n, p, jp1, jp2) + BiabductionSummary.Jprop.shallow_map ~f:(PropUtil.remove_locals_ret tenv pdesc) precondition in let spec = BiabductionSummary.{pre; posts; visited} in L.d_decrease_indent () ; do_after_node init_node ; Some spec @@ -867,7 +860,7 @@ let perform_analysis_phase exe_env tenv (summary : Summary.t) (proc_cfg : ProcCf (Localise.verbatim_desc "Leak_while_collecting_specs_after_footprint") in Reporting.log_issue_deprecated_using_state Exceptions.Error pname exn ; - (* retuning no specs *) [] + (* returning no specs *) [] in (specs, BiabductionSummary.FOOTPRINT) in @@ -1050,8 +1043,9 @@ let update_specs tenv prev_summary phase (new_specs : BiabductionSummary.NormSpe in let res = ref [] in let convert pre (post_set, visited) = + let pname = Summary.get_proc_name prev_summary in res := - BiabductionSummary.spec_normalize tenv + Abs.abstract_spec pname tenv BiabductionSummary.{pre; posts= Paths.PathSet.elements post_set; visited} :: !res in diff --git a/infer/tests/build_systems/ant/issues.exp b/infer/tests/build_systems/ant/issues.exp index c57c39ec4..dbdf58777 100644 --- a/infer/tests/build_systems/ant/issues.exp +++ b/infer/tests/build_systems/ant/issues.exp @@ -114,7 +114,7 @@ codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.Nu codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefNullableRet(boolean):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure derefNullableRet(...),start of procedure nullableRet(...),Taking true branch,return from a call to Object NullPointerExceptions.nullableRet(boolean)] codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefUndefNullableRet():void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure derefUndefNullableRet(),Skipping undefNullableRet(): unknown method,Definition of undefNullableRet()] codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefUndefNullableRetWrapper():void, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure derefUndefNullableRetWrapper(),start of procedure undefNullableWrapper(),Skipping undefNullableRet(): unknown method,Definition of undefNullableRet(),return from a call to Object NullPointerExceptions.undefNullableWrapper()] -codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterLoopOnList(codetoanalyze.java.infer.NullPointerExceptions$L):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking true branch,Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)] +codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterLoopOnList(codetoanalyze.java.infer.NullPointerExceptions$L):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking true branch,Taking true branch,Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)] codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock1(java.util.concurrent.locks.Lock):void, 4, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure dereferenceAfterUnlock1(...),Skipping toString(): unknown method] codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock2(java.util.concurrent.locks.Lock):void, 6, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure dereferenceAfterUnlock2(...),Skipping toString(): unknown method] codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.hashmapNPE(java.util.HashMap,java.lang.Object):java.lang.String, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hashmapNPE(...)] diff --git a/infer/tests/codetoanalyze/java/infer/issues.exp b/infer/tests/codetoanalyze/java/infer/issues.exp index 2584bc84c..aa07a7124 100644 --- a/infer/tests/codetoanalyze/java/infer/issues.exp +++ b/infer/tests/codetoanalyze/java/infer/issues.exp @@ -119,7 +119,7 @@ codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.Nu codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefNullableRet(boolean):void, 2, NULL_DEREFERENCE, B2, ERROR, [start of procedure derefNullableRet(...),start of procedure nullableRet(...),Taking true branch,return from a call to Object NullPointerExceptions.nullableRet(boolean)] codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefUndefNullableRet():void, 2, NULL_DEREFERENCE, B1, ERROR, [start of procedure derefUndefNullableRet(),Skipping undefNullableRet(): unknown method,Definition of undefNullableRet()] codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefUndefNullableRetWrapper():void, 1, NULL_DEREFERENCE, B1, ERROR, [start of procedure derefUndefNullableRetWrapper(),start of procedure undefNullableWrapper(),Skipping undefNullableRet(): unknown method,Definition of undefNullableRet(),return from a call to Object NullPointerExceptions.undefNullableWrapper()] -codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterLoopOnList(codetoanalyze.java.infer.NullPointerExceptions$L):void, 2, NULL_DEREFERENCE, B2, ERROR, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking true branch,Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)] +codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterLoopOnList(codetoanalyze.java.infer.NullPointerExceptions$L):void, 2, NULL_DEREFERENCE, B2, ERROR, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking true branch,Taking true branch,Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)] codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock1(java.util.concurrent.locks.Lock):void, 4, NULL_DEREFERENCE, B1, ERROR, [start of procedure dereferenceAfterUnlock1(...),Skipping toString(): unknown method] codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock2(java.util.concurrent.locks.Lock):void, 6, NULL_DEREFERENCE, B1, ERROR, [start of procedure dereferenceAfterUnlock2(...),Skipping toString(): unknown method] codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.hashmapNPE(java.util.HashMap,java.lang.Object):java.lang.String, 1, NULL_DEREFERENCE, B2, ERROR, [start of procedure hashmapNPE(...)]