diff --git a/infer/src/istd/IContainer.ml b/infer/src/istd/IContainer.ml index 36675ab90..95d39f65a 100644 --- a/infer/src/istd/IContainer.ml +++ b/infer/src/istd/IContainer.ml @@ -68,6 +68,10 @@ let filter ~fold ~filter t ~init ~f = fold t ~init ~f:(fun acc item -> if filter item then f acc item else acc) +let fold_of_pervasives_set_fold fold collection ~init ~f = + fold (fun elt accum -> f accum elt) collection init + + let map ~f:g fold t ~init ~f = fold t ~init ~f:(fun acc item -> f acc (g item)) let fold_of_pervasives_map_fold fold collection ~init ~f = diff --git a/infer/src/istd/IContainer.mli b/infer/src/istd/IContainer.mli index 2144afb47..d313ab57d 100644 --- a/infer/src/istd/IContainer.mli +++ b/infer/src/istd/IContainer.mli @@ -45,6 +45,9 @@ val filter : val map : f:('a -> 'b) -> ('t, 'a, 'accum) Container.fold -> ('t, 'b, 'accum) Container.fold +val fold_of_pervasives_set_fold : + (('elt -> 'accum -> 'accum) -> 't -> 'accum -> 'accum) -> ('t, 'elt, 'accum) Container.fold + val fold_of_pervasives_map_fold : (('key -> 'value -> 'accum -> 'accum) -> 't -> 'accum -> 'accum) -> ('t, 'key * 'value, 'accum) Container.fold diff --git a/infer/src/istd/UnionFind.ml b/infer/src/istd/UnionFind.ml new file mode 100644 index 000000000..320ef548e --- /dev/null +++ b/infer/src/istd/UnionFind.ml @@ -0,0 +1,101 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +module type Element = sig + type t [@@deriving compare] + + val is_simpler_than : t -> t -> bool +end + +module Make (X : Element) = struct + module Set = Caml.Set.Make (X) + module Map = Caml.Map.Make (X) + + let equal_x = [%compare.equal: X.t] + + (** the union-find backing data structure: maps elements to their representatives *) + module UF : sig + (** to get a little bit of type safety *) + type repr = private X.t + + type t + + val empty : t + + val find_opt : t -> X.t -> repr option + + val find : t -> X.t -> repr + + val merge : t -> repr -> into:repr -> t + + module Map : Caml.Map.S with type key = repr + end = struct + type repr = X.t + + type t = X.t Map.t + + let empty = Map.empty + + let find_opt reprs x = + let rec find_opt_aux candidate_repr = + (* [x] is in the relation and now we are climbing up to the final representative *) + match Map.find_opt candidate_repr reprs with + | None -> + (* [candidate_repr] is the representative *) + candidate_repr + | Some candidate_repr' -> + (* keep climbing *) + find_opt_aux candidate_repr' + in + Map.find_opt x reprs |> Option.map ~f:find_opt_aux + + + let find reprs x = find_opt reprs x |> Option.value ~default:x + + let merge reprs x ~into:y = (* TODO: implement path compression *) Map.add x y reprs + + module Map = Map + end + + type repr = UF.repr + + module Classes = struct + let find classes (x : UF.repr) = UF.Map.find_opt x classes |> Option.value ~default:Set.empty + + let merge classes (x1 : UF.repr) ~into:(x2 : UF.repr) = + let class1 = find classes x1 in + let class2 = find classes x2 in + let new_class = Set.union class1 class2 |> Set.add (x1 :> X.t) in + UF.Map.remove x1 classes |> UF.Map.add x2 new_class + end + + type t = {reprs: UF.t; classes: Set.t UF.Map.t} + + let empty = {reprs= UF.empty; classes= UF.Map.empty} + + let find_opt uf x = UF.find_opt uf.reprs x + + let find uf x = UF.find uf.reprs x + + let union uf x1 x2 = + let repr1 = find uf x1 in + let repr2 = find uf x2 in + if equal_x (repr1 :> X.t) (repr2 :> X.t) then (* avoid creating loops in the relation *) uf + else + let from, into = + if X.is_simpler_than (repr1 :> X.t) (repr2 :> X.t) then (repr2, repr1) else (repr1, repr2) + in + let reprs = UF.merge uf.reprs from ~into in + let classes = Classes.merge uf.classes from ~into in + {reprs; classes} + + + let fold_congruences {classes} ~init ~f = + UF.Map.fold (fun repr xs acc -> f acc (repr, xs)) classes init +end diff --git a/infer/src/istd/UnionFind.mli b/infer/src/istd/UnionFind.mli new file mode 100644 index 000000000..792b54d91 --- /dev/null +++ b/infer/src/istd/UnionFind.mli @@ -0,0 +1,38 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +(** A union-find data structure. *) + +module type Element = sig + type t [@@deriving compare] + + val is_simpler_than : t -> t -> bool + (** will be used to choose a "simpler" representative for a given equivalence class when possible *) +end + +module Make (X : Element) : sig + type t + + type repr = private X.t + + module Set : Caml.Set.S with type elt = X.t + + val empty : t + + val union : t -> X.t -> X.t -> t + + val find_opt : t -> X.t -> repr option + + val find : t -> X.t -> repr + (** like [find_opt] but returns the element given if it wasn't found in the relation *) + + val fold_congruences : (t, repr * Set.t, 'acc) Container.fold + (** fold over the equivalence classes of the relation, singling out the representative for each + class *) +end diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml new file mode 100644 index 000000000..eceb0c1f9 --- /dev/null +++ b/infer/src/pulse/PulseFormula.ml @@ -0,0 +1,780 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +module F = Format +module L = Logging +module AbstractValue = PulseAbstractValue + +module Term = struct + type t = + | Const of Const.t + | Var of AbstractValue.t + | Add of t * t + | Minus of t + | LessThan of t * t + | LessEqual of t * t + | Equal of t * t + | NotEqual of t * t + | Mult of t * t + | Div of t * t + | And of t * t + | Or of t * t + | Not of t + | Mod of t * t + | BitAnd of t * t + | BitOr of t * t + | BitNot of t + | BitShiftLeft of t * t + | BitShiftRight of t * t + | BitXor of t * t + [@@deriving compare] + + let equal_syntax = [%compare.equal: t] + + let rec pp fmt = function + | Var v -> + AbstractValue.pp fmt v + | Const c -> + Const.pp Pp.text fmt c + | Minus t -> + F.fprintf fmt "-(%a)" pp t + | BitNot t -> + F.fprintf fmt "BitNot(%a)" pp t + | Not t -> + F.fprintf fmt "¬(%a)" pp t + | Add (t1, t2) -> + F.fprintf fmt "(%a)+(%a)" pp t1 pp t2 + | Mult (t1, t2) -> + F.fprintf fmt "(%a)×(%a)" pp t1 pp t2 + | Div (t1, t2) -> + F.fprintf fmt "(%a)÷(%a)" pp t1 pp t2 + | Mod (t1, t2) -> + F.fprintf fmt "(%a) mod (%a)" pp t1 pp t2 + | BitAnd (t1, t2) -> + F.fprintf fmt "(%a)&(%a)" pp t1 pp t2 + | BitOr (t1, t2) -> + F.fprintf fmt "(%a)|(%a)" pp t1 pp t2 + | BitShiftLeft (t1, t2) -> + F.fprintf fmt "(%a)<<(%a)" pp t1 pp t2 + | BitShiftRight (t1, t2) -> + F.fprintf fmt "(%a)>>(%a)" pp t1 pp t2 + | BitXor (t1, t2) -> + F.fprintf fmt "(%a) xor (%a)" pp t1 pp t2 + | And (t1, t2) -> + F.fprintf fmt "(%a)∧(%a)" pp t1 pp t2 + | Or (t1, t2) -> + F.fprintf fmt "(%a)∨(%a)" pp t1 pp t2 + | LessThan (t1, t2) -> + F.fprintf fmt "(%a)<(%a)" pp t1 pp t2 + | LessEqual (t1, t2) -> + F.fprintf fmt "(%a)≤(%a)" pp t1 pp t2 + | Equal (t1, t2) -> + F.fprintf fmt "(%a)=(%a)" pp t1 pp t2 + | NotEqual (t1, t2) -> + F.fprintf fmt "(%a)≠(%a)" pp t1 pp t2 + + + let of_absval v = Var v + + let of_intlit i = Const (Cint i) + + let one = of_intlit IntLit.one + + let zero = of_intlit IntLit.zero + + let of_unop (unop : Unop.t) t = + match unop with Neg -> Minus t | BNot -> BitNot t | LNot -> Not t + + + let of_binop (bop : Binop.t) t1 t2 = + match bop with + | PlusA _ | PlusPI -> + Add (t1, t2) + | MinusA _ | MinusPI | MinusPP -> + Add (t1, Minus t2) + | Mult _ -> + Mult (t1, t2) + | Div -> + Div (t1, t2) + | Mod -> + Mod (t1, t2) + | Shiftlt -> + BitShiftLeft (t1, t2) + | Shiftrt -> + BitShiftRight (t1, t2) + | Lt -> + LessThan (t1, t2) + | Gt -> + LessThan (t2, t1) + | Le -> + LessEqual (t1, t2) + | Ge -> + LessEqual (t2, t1) + | Eq -> + Equal (t1, t2) + | Ne -> + NotEqual (t1, t2) + | BAnd -> + BitAnd (t1, t2) + | BXor -> + BitXor (t1, t2) + | BOr -> + BitOr (t1, t2) + | LAnd -> + And (t1, t2) + | LOr -> + Or (t1, t2) + + + let is_zero = function Const c -> Const.iszero_int_float c | _ -> false + + let is_non_zero_const = function Const c -> not (Const.iszero_int_float c) | _ -> false + + (** Fold [f] on the strict sub-terms of [t], if any. Preserve physical equality if [f] does. *) + let fold_map_direct_subterms t ~init ~f = + match t with + | Var _ | Const _ -> + (init, t) + | Minus t_not | BitNot t_not | Not t_not -> + let acc, t_not' = f init t_not in + let t' = + if phys_equal t_not t_not' then t + else + match t with + | Minus _ -> + Minus t_not' + | BitNot _ -> + BitNot t_not' + | Not _ -> + Not t_not' + | Var _ + | Const _ + | Add _ + | Mult _ + | Div _ + | Mod _ + | BitAnd _ + | BitOr _ + | BitShiftLeft _ + | BitShiftRight _ + | BitXor _ + | And _ + | Or _ + | LessThan _ + | LessEqual _ + | Equal _ + | NotEqual _ -> + assert false + in + (acc, t') + | Add (t1, t2) + | Mult (t1, t2) + | Div (t1, t2) + | Mod (t1, t2) + | BitAnd (t1, t2) + | BitOr (t1, t2) + | BitShiftLeft (t1, t2) + | BitShiftRight (t1, t2) + | BitXor (t1, t2) + | And (t1, t2) + | Or (t1, t2) + | LessThan (t1, t2) + | LessEqual (t1, t2) + | Equal (t1, t2) + | NotEqual (t1, t2) -> + let acc, t1' = f init t1 in + let acc, t2' = f acc t2 in + let t' = + if phys_equal t1 t1' && phys_equal t2 t2' then t + else + match t with + | Add _ -> + Add (t1', t2') + | Mult _ -> + Mult (t1', t2') + | Div _ -> + Div (t1', t2') + | Mod _ -> + Mod (t1', t2') + | BitAnd _ -> + BitAnd (t1', t2') + | BitOr _ -> + BitOr (t1', t2') + | BitShiftLeft _ -> + BitShiftLeft (t1', t2') + | BitShiftRight _ -> + BitShiftRight (t1', t2') + | BitXor _ -> + BitXor (t1', t2') + | And _ -> + And (t1', t2') + | Or _ -> + Or (t1', t2') + | LessThan _ -> + LessThan (t1', t2') + | LessEqual _ -> + LessEqual (t1', t2') + | Equal _ -> + Equal (t1', t2') + | NotEqual _ -> + NotEqual (t1', t2') + | Var _ | Const _ | Minus _ | BitNot _ | Not _ -> + assert false + in + (acc, t') + + + let map_direct_subterms t ~f = + fold_map_direct_subterms t ~init:() ~f:(fun () t' -> ((), f t')) |> snd + + + let rec fold_map_variables t ~init ~f = + match t with + | Var v -> + let acc, v' = f init v in + let t' = if phys_equal v v' then t else Var v' in + (acc, t') + | _ -> + fold_map_direct_subterms t ~init ~f:(fun acc t' -> fold_map_variables t' ~init:acc ~f) +end + +(** Basically boolean terms, used to build formulas. *) +module Atom = struct + type t = + | LessEqual of Term.t * Term.t + | LessThan of Term.t * Term.t + | Equal of Term.t * Term.t + | NotEqual of Term.t * Term.t + [@@deriving compare] + + type atom = t + + let pp fmt = function + | LessEqual (t1, t2) -> + F.fprintf fmt "%a ≤ %a" Term.pp t1 Term.pp t2 + | LessThan (t1, t2) -> + F.fprintf fmt "%a < %a" Term.pp t1 Term.pp t2 + | Equal (t1, t2) -> + F.fprintf fmt "%a = %a" Term.pp t1 Term.pp t2 + | NotEqual (t1, t2) -> + F.fprintf fmt "%a ≠ %a" Term.pp t1 Term.pp t2 + + + let nnot = function + | LessEqual (t1, t2) -> + LessThan (t2, t1) + | LessThan (t1, t2) -> + LessEqual (t2, t1) + | Equal (t1, t2) -> + NotEqual (t1, t2) + | NotEqual (t1, t2) -> + Equal (t1, t2) + + + let get_terms atom = + let (LessEqual (t1, t2) | LessThan (t1, t2) | Equal (t1, t2) | NotEqual (t1, t2)) = atom in + (t1, t2) + + + (** preserve physical equality if [f] does *) + let fold_map_terms atom ~init ~f = + let t1, t2 = get_terms atom in + let acc, t1' = f init t1 in + let acc, t2' = f acc t2 in + let t' = + if phys_equal t1' t1 && phys_equal t2' t2 then atom + else + match atom with + | LessEqual _ -> + LessEqual (t1', t2') + | LessThan _ -> + LessThan (t1', t2') + | Equal _ -> + Equal (t1', t2') + | NotEqual _ -> + NotEqual (t1', t2') + in + (acc, t') + + + let map_terms atom ~f = fold_map_terms atom ~init:() ~f:(fun () t -> ((), f t)) |> snd + + let to_term : t -> Term.t = function + | LessEqual (t1, t2) -> + LessEqual (t1, t2) + | LessThan (t1, t2) -> + LessThan (t1, t2) + | Equal (t1, t2) -> + Equal (t1, t2) + | NotEqual (t1, t2) -> + NotEqual (t1, t2) + + + type eval_result = True | False | Atom of t + + let eval_result_of_bool b = if b then True else False + + let term_of_eval_result = function + | True -> + Term.one + | False -> + Term.zero + | Atom atom -> + to_term atom + + + (* other simplifications TODO: + - push Minus inwards + - (t1+i1)+((i2+t2)+i3) -> (t1+t2)+(i1+i2+i3): need to flatten trees of additions (and Minus) + - same for multiplications, possibly others too + *) + let rec eval_term t = + let open Term in + let t_norm_subterms = map_direct_subterms ~f:eval_term t in + match t_norm_subterms with + | Var _ | Const _ -> + t + | Minus (Minus t) -> + (* [--t = t] *) + t + | Minus (Const (Cint i)) -> + (* [-i = -1*i] *) + Const (Cint (IntLit.(mul minus_one) i)) + | BitNot (BitNot t) -> + (* [~~t = t] *) + t + | Not (Const c) when Const.iszero_int_float c -> + (* [!0 = 1] *) + one + | Not (Const c) when Const.isone_int_float c -> + (* [!1 = 0] *) + zero + | Add (Const (Cint i1), Const (Cint i2)) -> + (* constants *) + Const (Cint (IntLit.add i1 i2)) + | Add (Const c, t) when Const.iszero_int_float c -> + (* [0 + t = t] *) + t + | Add (t, Const c) when Const.iszero_int_float c -> + (* [t + 0 = t] *) + t + | Mult (Const c, t) when Const.isone_int_float c -> + (* [1 × t = t] *) + t + | Mult (t, Const c) when Const.isone_int_float c -> + (* [t × 1 = t] *) + t + | Mult (Const c, _) when Const.iszero_int_float c -> + (* [0 × t = 0] *) + zero + | Mult (_, Const c) when Const.iszero_int_float c -> + (* [t × 0 = 0] *) + zero + | Div (Const c, _) when Const.iszero_int_float c -> + (* [0 / t = 0] *) + zero + | Div (t, Const c) when Const.isone_int_float c -> + (* [t / 1 = t] *) + t + | Div (t, Const c) when Const.isminusone_int_float c -> + (* [t / (-1) = -t] *) + eval_term (Minus t) + | Div (Minus t1, Minus t2) -> + (* [(-t1) / (-t2) = t1 / t2] *) + eval_term (Div (t1, t2)) + | Mod (Const c, _) when Const.iszero_int_float c -> + (* [0 % t = 0] *) + zero + | Mod (_, Const (Cint i)) when IntLit.isone i -> + (* [t % 1 = 0] *) + zero + | Mod (t1, t2) when equal_syntax t1 t2 -> + (* [t % t = 0] *) + zero + | And (t1, t2) when is_zero t1 || is_zero t2 -> + (* [false ∧ t = t ∧ false = false] *) zero + | And (t1, t2) when is_non_zero_const t1 -> + (* [true ∧ t = t] *) t2 + | And (t1, t2) when is_non_zero_const t2 -> + (* [t ∧ true = t] *) t1 + | Or (t1, t2) when is_non_zero_const t1 || is_non_zero_const t2 -> + (* [true ∨ t = t ∨ true = true] *) one + | Or (t1, t2) when is_zero t1 -> + (* [false ∨ t = t] *) t2 + | Or (t1, t2) when is_zero t2 -> + (* [t ∨ false = t] *) t1 + (* terms that are atoms can be simplified in [eval_atom] *) + | LessEqual (t1, t2) -> + eval_atom (LessEqual (t1, t2) : atom) |> term_of_eval_result + | LessThan (t1, t2) -> + eval_atom (LessThan (t1, t2) : atom) |> term_of_eval_result + | Equal (t1, t2) -> + eval_atom (Equal (t1, t2) : atom) |> term_of_eval_result + | NotEqual (t1, t2) -> + eval_atom (NotEqual (t1, t2) : atom) |> term_of_eval_result + | _ -> + t_norm_subterms + + + (** This assumes that the terms in the atom have been normalized/evaluated already. + + TODO: probably a better way to implement this would be to rely entirely on + [eval_term (term_of_atom (atom))], possibly implementing it as something about observing the + sign/zero-ness of [t1 - t2]. *) + and eval_atom (atom : t) = + let t1, t2 = get_terms atom in + match (t1, t2) with + | Const (Cint i1), Const (Cint i2) -> ( + match atom with + | Equal _ -> + eval_result_of_bool (IntLit.eq i1 i2) + | NotEqual _ -> + eval_result_of_bool (IntLit.neq i1 i2) + | LessEqual _ -> + eval_result_of_bool (IntLit.leq i1 i2) + | LessThan _ -> + eval_result_of_bool (IntLit.lt i1 i2) ) + | _ -> + if Term.equal_syntax t1 t2 then + match atom with + | Equal _ -> + True + | NotEqual _ -> + False + | LessEqual _ -> + True + | LessThan _ -> + False + else Atom atom + + + let eval (atom : t) = map_terms atom ~f:eval_term |> eval_atom + + let fold_map_variables a ~init ~f = + fold_map_terms a ~init ~f:(fun acc t -> Term.fold_map_variables t ~init:acc ~f) + + + module Set = Caml.Set.Make (struct + type nonrec t = t [@@deriving compare] + end) +end + +module UnionFind = UnionFind.Make (struct + type t = Term.t [@@deriving compare] + + let is_simpler_than (t1 : Term.t) (t2 : Term.t) = + match (t1, t2) with + | Const _, _ -> + true + | _, Const _ -> + false + | Var _, _ -> + true + | _, Var _ -> + false + | _ -> + false +end) + +(** The main datatype is either in a normal form [True | False | NormalForm _], or in a + not-yet-normalized form [Atom _ | And _], or a mix of both. + + Note the absence of disjunction and negation: negations are interpreted eagerly and + under-approximately by only remembering the first produced disjunct, and disjunctions are kept + in {!Term.t} form. *) +type t = + | True + | False + | NormalForm of + { congruences: UnionFind.t + (** equality relation between terms represented by a union-find data structure with + canonical representatives for each class of congruent terms *) + ; facts: Atom.Set.t + (** atoms not of the form [Equal _], normalized with respect to the congruence relation + and the {!Atom.eval} function *) } + | And of t * t + | Atom of Atom.t + +let ffalse = False + +let is_literal_false = function False -> true | _ -> false + +let ttrue = True + +let rec pp fmt = function + | True -> + F.fprintf fmt "true" + | False -> + F.fprintf fmt "false" + | Atom atom -> + Atom.pp fmt atom + | NormalForm {congruences; facts} -> + let pp_collection ~fold ~sep ~pp_item fmt coll = + let pp_coll_aux is_first item = + F.fprintf fmt "@[%s%a@]" (if is_first then "" else sep) pp_item item ; + (* is_first not true anymore *) false + in + F.fprintf fmt "@[%t@]" (fun _fmt -> fold coll ~init:true ~f:pp_coll_aux |> ignore) + in + let pp_ts_or_repr repr fmt ts = + if UnionFind.Set.is_empty ts then Term.pp fmt repr + else + pp_collection ~sep:"=" + ~fold:(IContainer.fold_of_pervasives_set_fold UnionFind.Set.fold) + ~pp_item:Term.pp fmt ts + in + let pp_congruences fmt congruences = + pp_collection ~sep:"∧" ~fold:UnionFind.fold_congruences fmt congruences + ~pp_item:(fun fmt ((repr : UnionFind.repr), ts) -> + F.fprintf fmt "%a=%a" Term.pp (repr :> Term.t) (pp_ts_or_repr (repr :> Term.t)) ts ) + in + let pp_atoms fmt atoms = + pp_collection ~sep:"∧" + ~fold:(IContainer.fold_of_pervasives_set_fold Atom.Set.fold) + ~pp_item:(fun fmt atom -> F.fprintf fmt "{%a}" Atom.pp atom) + fmt atoms + in + F.fprintf fmt "[%a@;&&@ %a]" pp_congruences congruences pp_atoms facts + | And (phi1, phi2) -> + F.fprintf fmt "{%a}∧{%a}" pp phi1 pp phi2 + + +module NormalForm : sig + val of_formula : t -> t + (** This computes equivalence classes between terms induced by the given conjunctive formula, then + symbolically evaluates the resulting terms and atoms to form a [NormalForm _] term equivalent + to the input formula, or [True] or [False]. *) + + val to_formula : UnionFind.t -> Atom.Set.t -> t + (** transforms a congruence relation and set of atoms into a formula without [NormalForm _] + sub-formulas *) +end = struct + (* NOTE: throughout this module some cases that are never supposed to happen at the moment are + handled nonetheless to avoid hassle and surprises in the future. *) + + let to_formula uf facts = + let phi = Atom.Set.fold (fun atom phi -> And (Atom atom, phi)) facts True in + let phi = + UnionFind.fold_congruences uf ~init:phi ~f:(fun conjuncts (repr, terms) -> + L.d_printf "@\nEquivalence class of %a: " Term.pp (repr :> Term.t) ; + UnionFind.Set.fold + (fun t conjuncts -> + L.d_printf "%a," Term.pp t ; + if phys_equal t (repr :> Term.t) then conjuncts + else And (Atom (Equal ((repr :> Term.t), t)), conjuncts) ) + terms conjuncts ) + in + L.d_ln () ; + phi + + + (** used for quickly detecting contradictions *) + exception Contradiction + + (** normalize term by replacing every (sub-)term by its canonical representative *) + let rec apply_term uf t = + match (UnionFind.find_opt uf t :> Term.t option) with + | None -> + (* no representative found for [t], look for substitution opportunities in its sub-terms *) + Term.map_direct_subterms t ~f:(fun t' -> apply_term uf t') + | Some t_repr -> + t_repr + + + let apply_atom uf (atom : Atom.t) = + let atom' = Atom.map_terms atom ~f:(fun t -> apply_term uf t) in + match Atom.eval atom' with + | True -> + None + | False -> + (* early exit on contradictions *) + L.d_printfln "Contradiction detected! %a ~> %a is False" Atom.pp atom Atom.pp atom' ; + raise_notrace Contradiction + | Atom atom -> + Some atom + + + (** normalize atomes by replacing every (sub-)term by their canonical representative then + symbolically evaluating the result *) + let normalize_atoms uf ~add_to:facts0 atoms = + List.fold atoms ~init:facts0 ~f:(fun facts atom -> + match apply_atom uf atom with None -> facts | Some atom' -> Atom.Set.add atom' facts ) + + + (** Extract [NormalForm _] from the given formula and return the formula without that part + (replaced with [True]). If there are several [NormalForm _] sub-formulas, return only one of + them and leave the others in. *) + let split_normal_form phi = + let rec find_normal_form normal_form phi = + match phi with + | NormalForm _ when Option.is_some normal_form -> + (normal_form, phi) + | NormalForm {congruences; facts} -> + (Some (congruences, facts), ttrue) + | True | False | Atom _ -> + (normal_form, phi) + | And (phi1, phi2) -> + let normal_form, phi1' = find_normal_form normal_form phi1 in + let normal_form, phi2' = find_normal_form normal_form phi2 in + let phi' = + if phys_equal phi1' phi && phys_equal phi2' phi2 then phi else And (phi1', phi2') + in + (normal_form, phi') + in + find_normal_form None phi + + + (** split the given formula into [(uf, facts, atoms)] where [phi] is equivalent to + [uf ∧ facts ∧ atoms], [facts] are in normal form w.r.t. [uf], but [atoms] are not and need + to be normalized *) + let rec gather_congruences_and_facts ((uf, facts, atoms) as acc) phi = + match phi with + | True -> + acc + | False -> + raise Contradiction + | Atom (Equal (t1, t2)) -> + (* NOTE: this should also normalize sub-terms of [t1] and [t2] according to the equality + relation. We don't do that yet. *) + let uf = UnionFind.union uf t1 t2 in + (* change facts into atoms when the equality relation changes so they will be normalized + again later using the new equality relation *) + let atoms_with_facts = Atom.Set.fold (fun atom atoms -> atom :: atoms) facts atoms in + (uf, Atom.Set.empty, atoms_with_facts) + | Atom atom -> + (uf, facts, atom :: atoms) + | And (phi1, phi2) -> + let acc' = gather_congruences_and_facts acc phi1 in + gather_congruences_and_facts acc' phi2 + | NormalForm {congruences; facts} -> + gather_congruences_and_facts acc (to_formula congruences facts) + + + let of_formula phi = + (* start from a pre-existing normal form if any *) + let (uf, facts), phi = + match split_normal_form phi with + | Some uf_facts, phi -> + (uf_facts, phi) + | None, phi -> + ((UnionFind.empty, Atom.Set.empty), phi) + in + try + let uf, facts, new_facts = gather_congruences_and_facts (uf, facts, []) phi in + let facts = normalize_atoms uf ~add_to:facts new_facts in + NormalForm {congruences= uf; facts} + with Contradiction -> ffalse +end + +let mk_less_than t1 t2 = Atom (LessThan (t1, t2)) + +let mk_less_equal t1 t2 = Atom (LessEqual (t1, t2)) + +let mk_equal t1 t2 = Atom (Equal (t1, t2)) + +let mk_not_equal t1 t2 = Atom (NotEqual (t1, t2)) + +(** propagates literal [False] *) +let aand phi1 phi2 = + if is_literal_false phi1 || is_literal_false phi2 then ffalse else And (phi1, phi2) + + +let rec nnot phi = + match phi with + | True -> + False + | False -> + True + | Atom a -> + Atom (Atom.nnot a) + | NormalForm {congruences; facts} -> + NormalForm.to_formula congruences facts |> nnot + | And (phi1, _phi2) -> + (* HACK/TODO: this keeps only one disjunct of the negation, which is ok for + under-approximation even though it's quite incomplete (especially for [And (True, + phi)]!). We could work harder at disjunctions if that proves to be an issue. *) + nnot phi1 + + +(** Detects terms that look like formulas, but maybe the logic in here would be better in + [Atom.eval_term] to avoid duplicating reasoning steps. *) +let rec of_term (t : Term.t) = + match t with + | And (t1, t2) -> + aand (of_term t1) (of_term t2) + | LessThan (t1, t2) -> + mk_less_than t1 t2 + | LessEqual (t1, t2) -> + mk_less_equal t1 t2 + | Equal (t1, t2) -> + mk_equal t1 t2 + | NotEqual (t1, t2) -> + mk_not_equal t1 t2 + | Const (Cint i) -> + if IntLit.iszero i then ffalse else ttrue + | Const (Cfloat f) -> + if Float.equal f Float.zero then ffalse else ttrue + | Const (Cstr _ | Cfun _ | Cclass _) -> + ttrue + | Mult (t1, t2) -> + (* [t1 × t2 ≠ 0] iff [t1 ≠ 0] && [t2 ≠ 0] *) + aand (of_term t1) (of_term t2) + | Div (t1, t2) when Term.equal_syntax t1 t2 -> + (* [t ÷ t = 1] *) + ttrue + | Div (t1, t2) -> + (* [t1 ÷ t2 ≠ 0] iff [t1 ≠ 0 ∧ t1 ≥ t2] *) + aand (of_term t1) (mk_less_equal t2 t1) + | Not t -> + nnot (of_term t) + | Minus t -> + (* [-t ≠ 0] iff [t ≠ 0] *) + of_term t + | Add (t1, Minus t2) | Add (Minus t1, t2) -> + (* [t1 - t2 ≠ 0] iff [t1 ≠ t2] *) + mk_not_equal t1 t2 + | Or _ + | Add _ + | Var _ + | Mod _ + | BitAnd _ + | BitOr _ + | BitNot _ + | BitShiftLeft _ + | BitShiftRight _ + | BitXor _ -> + (* default case: we don't know how to change the term itself into a formula so we represent + the fact that [t] is "true" by [t ≠ 0] *) + Atom (NotEqual (t, Term.zero)) + + +let of_term_binop bop t1 t2 = + (* be brutal and convert to a term, then trust that [of_term] will restore the formula structure + as the conversion is lossless *) + Term.of_binop bop t1 t2 |> of_term + + +let normalize phi = NormalForm.of_formula phi + +let simplify ~keep:_ phi = (* TODO: actually remove variables not in [keep] *) normalize phi + +let rec fold_map_variables phi ~init ~f = + match phi with + | True | False -> + (init, phi) + | NormalForm {congruences; facts} -> + NormalForm.to_formula congruences facts |> fold_map_variables ~init ~f + | Atom atom -> + let acc, atom' = Atom.fold_map_variables atom ~init ~f in + let phi' = if phys_equal atom atom' then phi else Atom atom' in + (acc, phi') + | And (phi1, phi2) -> + let acc, phi1' = fold_map_variables phi1 ~init ~f in + let acc, phi2' = fold_map_variables phi2 ~init:acc ~f in + if phys_equal phi1' phi1 && phys_equal phi2' phi2 then (acc, phi) + else (acc, And (phi1', phi2')) diff --git a/infer/src/pulse/PulseFormula.mli b/infer/src/pulse/PulseFormula.mli new file mode 100644 index 000000000..f817fd037 --- /dev/null +++ b/infer/src/pulse/PulseFormula.mli @@ -0,0 +1,71 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +module F = Format +module AbstractValue = PulseAbstractValue + +(** {2 Arithmetic solver} + + Build formulas from SIL and tries to decide if they are (mostly un-)satisfiable. *) + +module Term : sig + (** Similar to {!Exp.t} but with no memory operations and with {!AbstractValue.t} instead of SIL + variables. The rich structure allows us to represent all of SIL but is not a promise that we + are able to meaningfully reason about all of it. *) + type t + + val zero : t + + val of_absval : AbstractValue.t -> t + + val of_intlit : IntLit.t -> t + + val of_binop : Binop.t -> t -> t -> t + + val of_unop : Unop.t -> t -> t +end + +type t + +val pp : F.formatter -> t -> unit + +(** {3 Build formulas from non-formulas} *) + +val ttrue : t + +val of_term_binop : Binop.t -> Term.t -> Term.t -> t + +val mk_equal : Term.t -> Term.t -> t + +val mk_less_equal : Term.t -> Term.t -> t + +val mk_less_than : Term.t -> Term.t -> t + +(** {3 Combine formulas} *) + +val aand : t -> t -> t + +val nnot : t -> t + +(** {3 Operations} *) + +val simplify : keep:AbstractValue.Set.t -> t -> t + +val fold_map_variables : t -> init:'a -> f:('a -> AbstractValue.t -> 'a * AbstractValue.t) -> 'a * t + +val is_literal_false : t -> bool +(** Call [is_literal_false (normalize phi)] to check satisfiability. *) + +val normalize : t -> t +(** Produces a semantically-equivalent formula¹ where all consequences of equalities have been + applied and some ad-hoc arithmetic and logical reasoning has been performed. In particular, the + canonical representation of a known-false formula is [ffalse], and [is_literal_false ffalse] is + [true]. Probably a good idea to not throw away the result of calling this if you are going to + re-use the formula. + + (¹) Except it might throw away disjuncts! *) diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index 644a1b507..32dcaee84 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/infer/src/pulse/PulsePathCondition.ml @@ -10,6 +10,7 @@ module F = Format module L = Logging module AbstractValue = PulseAbstractValue module CItv = PulseCItv +module Formula = PulseFormula module ValueHistory = PulseValueHistory module BoItvs = struct @@ -29,57 +30,58 @@ module CItvs = PrettyPrintable.MakePPMonoMap (AbstractValue) (CItv) facts deduced by one domain to inform another. *) type t = { satisfiable: bool - (** If [true] then [pudge] could still be unsatisfiable (asking that question is expensive). + (** If [true] then [formula] could still be unsatisfiable (asking that question is + expensive). If [false] then the other components of the record can be arbitrary. *) ; bo_itvs: BoItvs.t ; citvs: CItvs.t - ; pudge: Pudge.t } + ; formula: Formula.t } -let pp fmt {satisfiable; bo_itvs; citvs; pudge} = - F.fprintf fmt "@[sat:%b,@;bo: @[%a@],@;citv: @[%a@],@;pudge: @[%a@]@]" satisfiable BoItvs.pp - bo_itvs CItvs.pp citvs Pudge.pp pudge +let pp fmt {satisfiable; bo_itvs; citvs; formula} = + F.fprintf fmt "@[sat:%b,@;bo: @[%a@],@;citv: @[%a@],@;formula: @[%a@]@]" satisfiable BoItvs.pp + bo_itvs CItvs.pp citvs Formula.pp formula -let true_ = {satisfiable= true; bo_itvs= BoItvs.empty; citvs= CItvs.empty; pudge= Pudge.true_} +let true_ = {satisfiable= true; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue} -let false_ = {satisfiable= false; bo_itvs= BoItvs.empty; citvs= CItvs.empty; pudge= Pudge.true_} +let false_ = {satisfiable= false; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue} -let and_nonnegative v ({satisfiable; bo_itvs; citvs; pudge} as phi) = +let and_nonnegative v ({satisfiable; bo_itvs; citvs; formula} as phi) = if not satisfiable then phi else { satisfiable ; bo_itvs= BoItvs.add v Itv.ItvPure.nat bo_itvs ; citvs= CItvs.add v CItv.zero_inf citvs - ; pudge= Pudge.(and_formula (Formula.lt Term.zero (Term.of_absval v)) pudge) } + ; formula= Formula.(aand (mk_less_equal Term.zero (Term.of_absval v)) formula) } -let and_positive v ({satisfiable; bo_itvs; citvs; pudge} as phi) = +let and_positive v ({satisfiable; bo_itvs; citvs; formula} as phi) = if not satisfiable then phi else { satisfiable ; bo_itvs= BoItvs.add v Itv.ItvPure.pos bo_itvs ; citvs= CItvs.add v (CItv.ge_to IntLit.one) citvs - ; pudge= Pudge.(and_formula (Formula.lt Term.zero (Term.of_absval v)) pudge) } + ; formula= Formula.(aand (mk_less_than Term.zero (Term.of_absval v)) formula) } -let and_eq_int v i ({satisfiable; bo_itvs; citvs; pudge} as phi) = +let and_eq_int v i ({satisfiable; bo_itvs; citvs; formula} as phi) = if not satisfiable then phi else { satisfiable ; bo_itvs= BoItvs.add v (Itv.ItvPure.of_int_lit i) bo_itvs ; citvs= CItvs.add v (CItv.equal_to i) citvs - ; pudge= Pudge.(and_formula (Formula.eq (Term.of_absval v) (Term.of_intlit i)) pudge) } + ; formula= Formula.(aand (mk_equal (Term.of_absval v) (Term.of_intlit i)) formula) } -let simplify ~keep {satisfiable; bo_itvs; citvs; pudge} = +let simplify ~keep {satisfiable; bo_itvs; citvs; formula} = if not satisfiable then false_ else let is_in_keep v _ = AbstractValue.Set.mem v keep in { satisfiable ; bo_itvs= BoItvs.filter is_in_keep bo_itvs ; citvs= CItvs.filter is_in_keep citvs - ; pudge= Pudge.simplify ~keep pudge } + ; formula= Formula.simplify ~keep formula } let subst_find_or_new subst addr_callee = @@ -173,19 +175,14 @@ let and_citvs_callee subst citvs_caller citvs_callee = (subst, citvs') -let and_pudge_callee subst pudge_caller pudge_callee = +let and_formula_callee subst formula_caller formula_callee = (* need to translate callee variables to make sense for the caller, thereby possibly extending the current substitution *) - let subst, pudge_callee_translated = - Pudge.fold_map_variables pudge_callee ~init:subst ~f:(fun subst v_callee_arith -> - let v_callee = Pudge.Var.to_absval v_callee_arith in - let subst', v_caller = subst_find_or_new subst v_callee in - (subst', Pudge.Var.of_absval v_caller) ) + let subst, formula_callee_translated = + Formula.fold_map_variables formula_callee ~init:subst ~f:subst_find_or_new in - (* Don't trigger the computation of the underlying Sledge data structure by asking for - satisfiability here. Instead, pudge (un-)satisfiability is computed lazily when we discover - issues. *) - (subst, Pudge.and_ pudge_caller pudge_callee_translated) + L.d_printfln "translated callee formula: %a@\n" Formula.pp formula_callee_translated ; + (subst, Formula.aand formula_caller formula_callee_translated) let and_callee subst phi ~callee:phi_callee = @@ -201,8 +198,9 @@ let and_callee subst phi ~callee:phi_callee = L.d_printfln "contradiction found by concrete intervals" ; (subst, false_) | subst, citvs' -> - let subst, pudge' = and_pudge_callee subst phi.pudge phi_callee.pudge in - (subst, {satisfiable= true; bo_itvs= bo_itvs'; citvs= citvs'; pudge= pudge'}) ) + let subst, formula' = and_formula_callee subst phi.formula phi_callee.formula in + L.d_printfln "conjoined formula post call: %a@\n" Formula.pp formula' ; + (subst, {satisfiable= true; bo_itvs= bo_itvs'; citvs= citvs'; formula= formula'}) ) (** {2 Operations} *) @@ -241,28 +239,25 @@ let eval_bo_itv_binop binop_addr bop op_lhs op_rhs bo_itvs = BoItvs.add binop_addr bo_itv bo_itvs -let eval_pudge_binop binop_addr binop op_lhs op_rhs pudge = - let open Pudge in +let eval_formula_binop binop_addr binop op_lhs op_rhs formula = + let open Formula in let term_of_op = function | LiteralOperand i -> Term.of_intlit i | AbstractValueOperand v -> Term.of_absval v in - match Term.of_binop binop (term_of_op op_lhs) (term_of_op op_rhs) with - | None -> - pudge - | Some t_binop -> - and_formula (Formula.eq (Term.of_absval binop_addr) t_binop) pudge + let t_binop = Term.of_binop binop (term_of_op op_lhs) (term_of_op op_rhs) in + aand (mk_equal (Term.of_absval binop_addr) t_binop) formula -let eval_binop binop_addr binop op_lhs op_rhs ({satisfiable; bo_itvs; citvs; pudge} as phi) = +let eval_binop binop_addr binop op_lhs op_rhs ({satisfiable; bo_itvs; citvs; formula} as phi) = if not phi.satisfiable then phi else { satisfiable ; bo_itvs= eval_bo_itv_binop binop_addr binop op_lhs op_rhs bo_itvs ; citvs= eval_citv_binop binop_addr binop op_lhs op_rhs citvs - ; pudge= eval_pudge_binop binop_addr binop op_lhs op_rhs pudge } + ; formula= eval_formula_binop binop_addr binop op_lhs op_rhs formula } let eval_citv_unop unop_addr unop operand_addr citvs = @@ -282,22 +277,19 @@ let eval_bo_itv_unop unop_addr unop operand_addr bo_itvs = BoItvs.add unop_addr itv bo_itvs -let eval_pudge_unop unop_addr (unop : Unop.t) addr pudge = - let open Pudge in - match Term.of_unop unop (Term.of_absval addr) with - | None -> - pudge - | Some t_unop -> - and_formula (Formula.eq (Term.of_absval unop_addr) t_unop) pudge +let eval_formula_unop unop_addr (unop : Unop.t) addr formula = + let open Formula in + let t_unop = Term.of_unop unop (Term.of_absval addr) in + aand (mk_equal (Term.of_absval unop_addr) t_unop) formula -let eval_unop unop_addr unop addr ({satisfiable; bo_itvs; citvs; pudge} as phi) = +let eval_unop unop_addr unop addr ({satisfiable; bo_itvs; citvs; formula} as phi) = if not phi.satisfiable then phi else { satisfiable ; bo_itvs= eval_bo_itv_unop unop_addr unop addr bo_itvs ; citvs= eval_citv_unop unop_addr unop addr citvs - ; pudge= eval_pudge_unop unop_addr unop addr pudge } + ; formula= eval_formula_unop unop_addr unop addr formula } let prune_bo_with_bop ~negated v_opt arith bop arith' phi = @@ -316,12 +308,12 @@ let prune_bo_with_bop ~negated v_opt arith bop arith' phi = let eval_operand phi = function | LiteralOperand i -> - (None, Some (CItv.equal_to i), Itv.ItvPure.of_int_lit i, Pudge.Term.of_intlit i) + (None, Some (CItv.equal_to i), Itv.ItvPure.of_int_lit i, Formula.Term.of_intlit i) | AbstractValueOperand v -> ( Some v , CItvs.find_opt v phi.citvs , BoItvs.find_or_default v phi.bo_itvs - , Pudge.Term.of_absval v ) + , Formula.Term.of_absval v ) let record_citv_abduced addr_opt arith_opt citvs = @@ -334,21 +326,18 @@ let record_citv_abduced addr_opt arith_opt citvs = let bind_satisfiable phi ~f = if phi.satisfiable then f phi else phi -let prune_binop ~negated bop lhs_op rhs_op ({satisfiable; bo_itvs= _; citvs; pudge} as phi) = +let prune_binop ~negated bop lhs_op rhs_op ({satisfiable; bo_itvs= _; citvs; formula} as phi) = if not satisfiable then phi else - let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, pudge_lhs = eval_operand phi lhs_op in - let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, pudge_rhs = eval_operand phi rhs_op in + let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, t_lhs = eval_operand phi lhs_op in + let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, t_rhs = eval_operand phi rhs_op in let phi = - match Pudge.Formula.term_binop bop pudge_lhs pudge_rhs with - | None -> - phi - | Some f_positive -> - let pudge = - let f = if negated then Pudge.Formula.not_ f_positive else f_positive in - Pudge.and_formula f pudge - in - {phi with pudge} + let f_positive = Formula.of_term_binop bop t_lhs t_rhs in + let formula = + let f = if negated then Formula.nnot f_positive else f_positive in + Formula.aand f formula + in + {phi with formula} in match CItv.abduce_binop_is_true ~negated bop arith_lhs_opt arith_rhs_opt with | Unsatisfiable -> @@ -392,9 +381,9 @@ let is_known_zero phi v = || BoItvs.find_opt v phi.bo_itvs |> Option.value_map ~default:false ~f:Itv.ItvPure.is_zero -let is_unsat_cheap phi = not phi.satisfiable +let is_unsat_cheap phi = (not phi.satisfiable) || Formula.is_literal_false phi.formula let is_unsat_expensive phi = - (* note: contradictions are detected eagerly for all sub-domains except pudge, so just + (* note: contradictions are detected eagerly for all sub-domains except formula, so just evaluate that one *) - is_unsat_cheap phi || Pudge.is_unsat phi.pudge + is_unsat_cheap phi || Formula.normalize phi.formula |> Formula.is_literal_false diff --git a/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp b/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp index 782357e84..fc28c52e3 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp @@ -45,7 +45,7 @@ void diverge_if_alias_ok(int* x, int* y) { } } -void FP_diverge_before_null_deref_ok(int* x) { +void diverge_before_null_deref_ok(int* x) { diverge_if_alias_ok(x, x); int* p = nullptr; *p = 42; diff --git a/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp b/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp index 24fa95d6d..95e288ff1 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp @@ -36,7 +36,7 @@ bool equal(size_t x, size_t y) { return x == y; } -void FP_unreachable_interproc_compare_ok(int* x, size_t y) { +void unreachable_interproc_compare_ok(int* x, size_t y) { if (equal(y, 0)) { free(x); } diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index d2095e6c6..9fa12a20e 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,4 +1,3 @@ -codetoanalyze/cpp/pulse/aliasing.cpp, FP_diverge_before_null_deref_ok, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/aliasing.cpp, alias_null_deref_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/aliasing.cpp, call_ifnotthenderef_false_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `ifnotthenderef` here,parameter `x` of ifnotthenderef,invalid access occurs here] codetoanalyze/cpp/pulse/aliasing.cpp, call_ifthenderef_true_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `ifthenderef` here,parameter `x` of ifthenderef,invalid access occurs here] @@ -11,7 +10,6 @@ codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_b codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, reassign_lambda_capture_destroy_invoke_bad, 9, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here] -codetoanalyze/cpp/pulse/conditionals.cpp, FP_unreachable_interproc_compare_ok, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of FP_unreachable_interproc_compare_ok,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of FP_unreachable_interproc_compare_ok,invalid access occurs here] codetoanalyze/cpp/pulse/conditionals.cpp, add_test3_bad, 3, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of add_test3_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test3_bad,invalid access occurs here] codetoanalyze/cpp/pulse/conditionals.cpp, add_test5_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of add_test5_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test5_bad,invalid access occurs here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass::templated_wrapper_delete_ok` here,parameter `a` of deduplication::SomeTemplatedClass::templated_wrapper_delete_ok,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass::templated_wrapper_access_ok` here,parameter `a` of deduplication::SomeTemplatedClass::templated_wrapper_access_ok,invalid access occurs here]