From 5d1a213f52cc09a7b8cd4b0e42aef76eddf14d27 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Sun, 23 Dec 2018 13:32:30 -0800 Subject: [PATCH] [Hil] Fix failure in exception node Reviewed By: jberdine Differential Revision: D13541755 fbshipit-source-id: a58458046 --- infer/src/absint/AbstractDomain.mli | 30 ++--- infer/src/checkers/Bindings.ml | 110 ++++++++++++------ .../codetoanalyze/java/quandary/Hil.java | 28 +++++ 3 files changed, 116 insertions(+), 52 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/quandary/Hil.java diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index bb41c6245..12c3899f9 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -146,29 +146,29 @@ end module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) : InvertedMapS with type key = Key.t and type value = ValueDomain.t -module FiniteMultiMap - (Key : PrettyPrintable.PrintableOrderedType) - (Value : PrettyPrintable.PrintableOrderedType) : sig - include WithBottom - - val add : Key.t -> Value.t -> t -> t - - val mem : Key.t -> t -> bool - - val remove : Key.t -> Value.t -> t -> t -end - (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *) include sig [@@@warning "-60"] - (** Boolean domain ordered by p || ~q. Useful when you want a boolean that's true only when it's - true in both conditional branches. *) - module BooleanAnd : S with type t = bool + module FiniteMultiMap + (Key : PrettyPrintable.PrintableOrderedType) + (Value : PrettyPrintable.PrintableOrderedType) : sig + include WithBottom + + val add : Key.t -> Value.t -> t -> t [@@warning "-32"] + + val mem : Key.t -> t -> bool [@@warning "-32"] + + val remove : Key.t -> Value.t -> t -> t [@@warning "-32"] + end end +(** Boolean domain ordered by p || ~q. Useful when you want a boolean that's true only when it's + true in both conditional branches. *) +module BooleanAnd : S with type t = bool + (** Boolean domain ordered by ~p || q. Useful when you want a boolean that's true only when it's true in one conditional branch. *) module BooleanOr : WithBottom with type t = bool diff --git a/infer/src/checkers/Bindings.ml b/infer/src/checkers/Bindings.ml index 636b63bb0..c37c182a3 100644 --- a/infer/src/checkers/Bindings.ml +++ b/infer/src/checkers/Bindings.ml @@ -8,57 +8,96 @@ open! IStd module F = Format module L = Logging -module Dead = AbstractDomain.InvertedSet (Var) -module Reverse = AbstractDomain.FiniteMultiMap (Var) (Var) + +module Reverse = struct + module Dead = AbstractDomain.BooleanAnd + module VarSet = AbstractDomain.FiniteSet (Var) + module DeadAndVarSet = AbstractDomain.Pair (Dead) (VarSet) + module M = AbstractDomain.Map (Var) (DeadAndVarSet) + + (* invariant: sets are not empty *) + type t = M.t + + let empty = M.empty + + let add k v rm = + M.update k + (function + | None -> Some (false, VarSet.singleton v) | Some (_, s) -> Some (false, VarSet.add v s)) + rm + + + let mem = M.mem + + let deadify k rm = + M.update k + (function (None | Some (true, _)) as vo -> vo | Some (false, s) -> Some (true, s)) + rm + + + let remove k v rm = + match M.find_opt k rm with + | None -> + (rm, false) + | Some (dead, s) -> + let s = VarSet.remove v s in + if VarSet.is_empty s then (M.remove k rm, dead) else (M.add k (dead, s) rm, false) + + + let pp = M.pp + + let join = M.join + + let widen = M.widen +end type t = { resolve: IdAccessPathMapDomain.t ; reverse: Reverse.t (** there is a [x -> y] mapping in reverse for each variable [y] appearing in [resolve x] *) - ; dead: Dead.t } + } -let empty = {resolve= IdAccessPathMapDomain.empty; reverse= Reverse.empty; dead= Dead.empty} +let empty = {resolve= IdAccessPathMapDomain.empty; reverse= Reverse.empty} -let add id ap {resolve; reverse; dead} = +let add id ap {resolve; reverse} = + if (Config.debug_exceptions || Config.write_html) && Reverse.mem id reverse then + (if Config.debug_exceptions then L.(die InternalError) else L.d_printfln ?color:None) + "Variable %a appearing on both sides of bindings" Var.pp id ; let resolve = IdAccessPathMapDomain.add id ap resolve in let reverse = HilExp.AccessExpression.fold_vars ap ~init:reverse ~f:(fun acc var_in_ap -> Reverse.add var_in_ap id acc ) in - let dead = Dead.remove id dead in - {resolve; reverse; dead} + {resolve; reverse} let exit_scope id bindings = - let {resolve; reverse; dead} = bindings in - match (Reverse.mem id reverse, IdAccessPathMapDomain.find_opt id resolve) with - | true, None -> - let dead = Dead.add id dead in - ({resolve; reverse; dead}, []) - | true, Some _ -> - L.(die InternalError) "Variable appearing on both sides of bindings" - | false, None -> - (bindings, [id]) - | false, Some ap -> + let {resolve; reverse} = bindings in + match IdAccessPathMapDomain.find_opt id resolve with + | None -> + if Reverse.mem id reverse then + let reverse = Reverse.deadify id reverse in + ({resolve; reverse}, []) + else (bindings, [id]) + | Some ap -> let resolve = IdAccessPathMapDomain.remove id resolve in - let reverse, vars, dead = - HilExp.AccessExpression.fold_vars ap ~init:(reverse, [], dead) - ~f:(fun (reverse, vars, dead) var_in_ap -> - let reverse = Reverse.remove var_in_ap id reverse in - if (not (Reverse.mem var_in_ap reverse)) && Dead.mem var_in_ap dead then - (reverse, var_in_ap :: vars, Dead.remove var_in_ap dead) - else (reverse, vars, dead) ) + let reverse, vars = + HilExp.AccessExpression.fold_vars ap ~init:(reverse, []) + ~f:(fun (reverse, vars) var_in_ap -> + let reverse, dead = Reverse.remove var_in_ap id reverse in + let vars = if dead then var_in_ap :: vars else vars in + (reverse, vars) ) in - ({resolve; reverse; dead}, vars) + ({resolve; reverse}, vars) let resolve {resolve} id = IdAccessPathMapDomain.find_opt id resolve let fold {resolve} ~init ~f = IdAccessPathMapDomain.fold f resolve init -let pp f {resolve; reverse; dead} = - F.fprintf f "{@[ resolve=@[%a@];@;reverse=@[%a@];@;dead=@[%a@];@]}" - IdAccessPathMapDomain.pp resolve Reverse.pp reverse Dead.pp dead +let pp f {resolve; reverse} = + F.fprintf f "{@[ resolve=@[%a@];@;reverse=@[%a@]@]}" IdAccessPathMapDomain.pp resolve + Reverse.pp reverse let ( <= ) ~lhs ~rhs = IdAccessPathMapDomain.( <= ) ~lhs:lhs.resolve ~rhs:rhs.resolve @@ -66,18 +105,15 @@ let ( <= ) ~lhs ~rhs = IdAccessPathMapDomain.( <= ) ~lhs:lhs.resolve ~rhs:rhs.re let join bindings1 bindings2 = if phys_equal bindings1 bindings2 then bindings1 else - let {resolve= resolve1; reverse= reverse1; dead= dead1} = bindings1 in - let {resolve= resolve2; reverse= reverse2; dead= dead2} = bindings2 in - { resolve= IdAccessPathMapDomain.join resolve1 resolve2 - ; reverse= Reverse.join reverse1 reverse2 - ; dead= Dead.join dead1 dead2 } + let {resolve= resolve1; reverse= reverse1} = bindings1 in + let {resolve= resolve2; reverse= reverse2} = bindings2 in + {resolve= IdAccessPathMapDomain.join resolve1 resolve2; reverse= Reverse.join reverse1 reverse2} let widen ~prev ~next ~num_iters = if phys_equal prev next then prev else - let {resolve= resolve1; reverse= reverse1; dead= dead1} = prev in - let {resolve= resolve2; reverse= reverse2; dead= dead2} = next in + let {resolve= resolve1; reverse= reverse1} = prev in + let {resolve= resolve2; reverse= reverse2} = next in { resolve= IdAccessPathMapDomain.widen ~prev:resolve1 ~next:resolve2 ~num_iters - ; reverse= Reverse.widen ~prev:reverse1 ~next:reverse2 ~num_iters - ; dead= Dead.widen ~prev:dead1 ~next:dead2 ~num_iters } + ; reverse= Reverse.widen ~prev:reverse1 ~next:reverse2 ~num_iters } diff --git a/infer/tests/codetoanalyze/java/quandary/Hil.java b/infer/tests/codetoanalyze/java/quandary/Hil.java new file mode 100644 index 000000000..63f2078c1 --- /dev/null +++ b/infer/tests/codetoanalyze/java/quandary/Hil.java @@ -0,0 +1,28 @@ +/* + * Copyright (c) 2018-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. + */ + +package codetoanalyze.java.quandary; + +import java.util.ArrayList; +import java.util.List; + +/** + * Repro of HIL bindings issue: In the exception node, the invariant that a bound variable cannot + * appear in the RHS of another binding is broken. + */ +class Hil { + public static void foo() { + List Y = new ArrayList<>(); + int dummy = 0; + for (Character x : "X".toCharArray()) { + dummy = 1; + } + for (Integer y : Y) { + dummy = 2; + } + } +}