From 2e4fbb7fe56c57b5ca875daee5e9798a492ceea6 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 30 Oct 2019 07:57:58 -0700 Subject: [PATCH] [pulse] intervals! Summary: This adds a more interesting value domain to pulse: concrete intervals. There are still two main limitations: 1. arithmetic operations are all over-approximated: any assignment involving arithmetic operations is replaced by non-determinism 2. abstract values that are discovered to be equal are not merged into one Reviewed By: skcho Differential Revision: D18058972 fbshipit-source-id: 0492a590f --- infer/src/IR/IntLit.ml | 2 + infer/src/IR/IntLit.mli | 2 + infer/src/pulse/PulseAbductiveDomain.ml | 29 +- infer/src/pulse/PulseArithmetic.ml | 404 ++++++++++++++++-- infer/src/pulse/PulseArithmetic.mli | 30 +- infer/src/pulse/PulseAttribute.ml | 2 +- infer/src/pulse/PulseOperations.ml | 21 +- .../codetoanalyze/cpp/pulse/conditionals.cpp | 4 +- .../codetoanalyze/cpp/pulse/fbstring.cpp | 19 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 3 - .../tests/codetoanalyze/cpp/pulse/values.cpp | 2 +- 11 files changed, 431 insertions(+), 87 deletions(-) diff --git a/infer/src/IR/IntLit.ml b/infer/src/IR/IntLit.ml index 7bff07bc8..8335ea0f4 100644 --- a/infer/src/IR/IntLit.ml +++ b/infer/src/IR/IntLit.ml @@ -148,6 +148,8 @@ let shift_right intlit1 {i= i2} = lift1 (fun i -> Z.shift_right i i2) intlit1 +let max i1 i2 = if geq i1 i2 then i1 else i2 + let min i1 i2 = if leq i1 i2 then i1 else i2 let pp f intlit = if isnull intlit then F.pp_print_string f "null" else Z.pp_print f intlit.i diff --git a/infer/src/IR/IntLit.mli b/infer/src/IR/IntLit.mli index b239d775d..5c18e69b2 100644 --- a/infer/src/IR/IntLit.mli +++ b/infer/src/IR/IntLit.mli @@ -89,6 +89,8 @@ val shift_right : t -> t -> t val sub : t -> t -> t +val max : t -> t -> t + val min : t -> t -> t val to_int : t -> int option diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index f77991195..1ccf1f480 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -447,26 +447,25 @@ module PrePost = struct match Attributes.get_arithmetic attrs_pre with | None -> call_state - | Some _ as arith_callee -> + | Some _ as arith_callee -> ( let addr_caller = fst addr_hist_caller in let astate = call_state.astate in let arith_caller = Memory.get_arithmetic addr_caller astate in (* TODO: we don't use [abduced_callee] but we could probably use it to refine the attributes for that address in the post since abstract values are immutable *) - let satisfiable, abduce_caller, _abduce_callee = - Arithmetic.abduce_binop_is_true ~negated:false Eq arith_caller arith_callee - in - if not satisfiable then - raise - (CannotApplyPre - (Arithmetic {addr_caller; addr_callee= addr_pre; arith_caller; arith_callee})) ; - let new_astate = - Option.fold abduce_caller ~init:astate ~f:(fun astate abduce_caller -> - let attribute = Attribute.Arithmetic abduce_caller in - Memory.abduce_attribute addr_caller attribute astate - |> Memory.add_attribute addr_caller attribute ) - in - {call_state with astate= new_astate} + match Arithmetic.abduce_binop_is_true ~negated:false Eq arith_caller arith_callee with + | Unsatisfiable -> + raise + (CannotApplyPre + (Arithmetic {addr_caller; addr_callee= addr_pre; arith_caller; arith_callee})) + | Satisfiable (abduce_caller, _abduce_callee) -> + let new_astate = + Option.fold abduce_caller ~init:astate ~f:(fun astate abduce_caller -> + let attribute = Attribute.Arithmetic abduce_caller in + Memory.abduce_attribute addr_caller attribute astate + |> Memory.add_attribute addr_caller attribute ) + in + {call_state with astate= new_astate} ) (** Materialize the (abstract memory) subgraph of [pre] reachable from [addr_pre] in diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml index a343a52a0..590fe74f9 100644 --- a/infer/src/pulse/PulseArithmetic.ml +++ b/infer/src/pulse/PulseArithmetic.ml @@ -7,62 +7,392 @@ open! IStd module F = Format -type t = EqualTo of Const.t [@@deriving compare] +module Bound = struct + type t = Int of IntLit.t | MinusInfinity | PlusInfinity [@@deriving compare] -let pp fmt = function EqualTo c -> F.fprintf fmt "=%a" (Const.pp Pp.text) c + let pp fmt = function + | Int i -> + IntLit.pp fmt i + | MinusInfinity -> + F.pp_print_string fmt "-∞" + | PlusInfinity -> + F.pp_print_string fmt "+∞" -(** booleans with \top *) -module TBool = struct - type t = True | False | Top + + let equal b1 b2 = + match (b1, b2) with + | MinusInfinity, MinusInfinity | PlusInfinity, PlusInfinity -> + true + | Int i1, Int i2 -> + IntLit.eq i1 i2 + | _ -> + false + + + let le b1 b2 = + match (b1, b2) with + | MinusInfinity, _ | _, PlusInfinity -> + true + | (Int _ | PlusInfinity), MinusInfinity | PlusInfinity, Int _ -> + false + | Int i1, Int i2 -> + IntLit.leq i1 i2 + + + let lt b1 b2 = + match (b1, b2) with + | MinusInfinity, _ | _, PlusInfinity -> + true + | (Int _ | PlusInfinity), MinusInfinity | PlusInfinity, Int _ -> + false + | Int i1, Int i2 -> + IntLit.lt i1 i2 + + + let ge b1 b2 = + match (b1, b2) with + | _, MinusInfinity | PlusInfinity, _ -> + true + | MinusInfinity, (Int _ | PlusInfinity) | Int _, PlusInfinity -> + false + | Int i1, Int i2 -> + IntLit.geq i1 i2 + + + let gt b1 b2 = + match (b1, b2) with + | _, MinusInfinity | PlusInfinity, _ -> + true + | MinusInfinity, (Int _ | PlusInfinity) | Int _, PlusInfinity -> + false + | Int i1, Int i2 -> + IntLit.gt i1 i2 + + + let min b1 b2 = if le b1 b2 then b1 else b2 + + let max b1 b2 = if le b1 b2 then b2 else b1 + + let add_int b i = + match b with MinusInfinity | PlusInfinity -> b | Int i' -> Int (IntLit.add i' i) + + + let is_interval b1 b2 = + match (b1, b2) with + | MinusInfinity, MinusInfinity | PlusInfinity, PlusInfinity -> + false + | _ -> + le b1 b2 end -let flip_abduced (tbool, c1, c2) = (tbool, c2, c1) +module Unsafe : sig + type t = private + | Between of Bound.t * Bound.t (** we write [b1,b2] for these *) + | Outside of IntLit.t * IntLit.t (** we write i1][i2 for these *) + [@@deriving compare] + + val between : Bound.t -> Bound.t -> t + + val outside : IntLit.t -> IntLit.t -> t + + val equal_to : IntLit.t -> t + + val not_equal_to : IntLit.t -> t +end = struct + type t = Between of Bound.t * Bound.t | Outside of IntLit.t * IntLit.t [@@deriving compare] + + let between b1 b2 = + assert (Bound.is_interval b1 b2) ; + Between (b1, b2) + + + let outside i1 i2 = + assert (IntLit.leq i1 i2) ; + Outside (i1, i2) + + + let equal_to i = + let b = Bound.Int i in + Between (b, b) + + + let not_equal_to i = Outside (i, i) +end + +include Unsafe + +let pp fmt = function + | Between (MinusInfinity, PlusInfinity) -> + F.fprintf fmt "∈ℕ" + | Between (lower, PlusInfinity) -> + F.fprintf fmt "≥%a" Bound.pp lower + | Between (MinusInfinity, upper) -> + F.fprintf fmt "≤%a" Bound.pp upper + | Between (lower, upper) when Bound.equal lower upper -> + F.fprintf fmt "=%a" Bound.pp lower + | Between (lower, upper) -> + F.fprintf fmt "∈[%a,%a]" Bound.pp lower Bound.pp upper + | Outside (l, u) when IntLit.eq l u -> + F.fprintf fmt "≠%a" IntLit.pp l + | Outside (l, u) -> + F.fprintf fmt "∉[%a,%a]" IntLit.pp l IntLit.pp u + + +let has_empty_intersection a1 a2 = + match (a1, a2) with + | Outside _, Outside _ -> + false + | Between (lower1, upper1), Between (lower2, upper2) -> + Bound.lt upper1 lower2 || Bound.lt upper2 lower1 + | Between (lower1, upper1), Outside (l2, u2) | Outside (l2, u2), Between (lower1, upper1) -> + (* is [l1, u1] inside [l2, u2]? *) + Bound.le (Int l2) lower1 && Bound.ge (Int u2) upper1 + -let rec abduce_eq a1 a2 = +let add_int a i = + match a with + | Between (lower, upper) -> + between (Bound.add_int lower i) (Bound.add_int upper i) + | Outside (l, u) -> + outside (IntLit.add i l) (IntLit.add i u) + + +let to_singleton = function Between (Int l1, Int l2) when IntLit.eq l1 l2 -> Some l1 | _ -> None + +(** [remove_element e a] compute [a - {e}] if representable and if it is not [a] *) +let remove_element e = function + | Between (lower, upper) when Bound.equal lower upper -> + (* empty sets are not allowed to be represented *) None + | Between (Int l, upper) when IntLit.eq l e -> + Some (between (Int (IntLit.(add one) l)) upper) + | Between (lower, Int u) when IntLit.eq u e -> + Some (between lower (Int (IntLit.(add minus_one) u))) + | Between (MinusInfinity, PlusInfinity) -> + Some (not_equal_to e) + | Between _ -> + None + | Outside (l, u) -> + let l_minus_one = IntLit.(add minus_one) l in + if IntLit.eq e l_minus_one then Some (outside l_minus_one u) + else + (* can't have [l-1 = u+1] because [l≤u] *) + let u_plus_one = IntLit.(add one) u in + if IntLit.eq e u_plus_one then Some (outside l u_plus_one) else None + + +type abduction_result = Unsatisfiable | Satisfiable of t option * t option + +let flip_abduced = function + | Unsatisfiable -> + Unsatisfiable + | Satisfiable (lhs, rhs) -> + Satisfiable (rhs, lhs) + + +let rec abduce_eq (a1 : t) (a2 : t) = match (a1, a2) with - | Some (EqualTo c1), Some (EqualTo c2) when Const.equal c1 c2 -> - (TBool.True, None, None) - | Some (EqualTo _c1), Some (EqualTo _c2) (* c1≠c2 *) -> - (TBool.False, None, None) - | None, Some _ -> + | Between (lower1, upper1), Between (lower2, upper2) -> + (* ∃x. l1≤x≤u1 ∧ l2≤x≤u2 *) + (* ⇔ ∃x. max(l1,l2)≤x≤min(u1,u2) *) + let lower = Bound.max lower1 lower2 in + let upper = Bound.min upper1 upper2 in + if Bound.lt upper lower then Unsatisfiable + else + let tighter = Some (between lower upper) in + Satisfiable (tighter, tighter) + | Outside (l1, u1), Outside (l2, u2) -> + (* ∃x. (xu1) ∧ (xu2) ∧ li<=ui*) + (* all the possible cases: + x: --------[ ]--------- + y: -----[ ]-------- + + x: ---[ ]------ + y: -----[ ]-------- + + x: ---[ ]---------- + y: -----[ ]-------- + + x: ---------[ ]---- + y: -----[ ]-------- + + -> SAT, can tighten both to min(l1,l2)][max(u1,u2) + + x: ---------------[ ]-- + y: -----[ ]-------- + or symmetrically x<->y => cannot express the 3 intervals that would be needed so return SAT + (TODO: we might want to keep only one of these, which would be a kind of recency model of + disequalities: remember the last known disequality) + *) + if IntLit.leq l1 u2 && IntLit.leq l2 u1 then + let l = IntLit.min l1 l2 in + let u = IntLit.max u1 u2 in + let tighter = Some (outside l u) in + Satisfiable (tighter, tighter) + else Satisfiable (None, None) + | Outside _, Between _ -> abduce_eq a2 a1 |> flip_abduced - | Some (EqualTo _c), None -> - (TBool.True, None, a1) - | None, None -> - (TBool.Top, None, None) + | Between (lower1, upper1), Outside (l2, u2) -> + (* ∃x. l1≤x≤u1 ∧ (xu2) *) + (* all the possible cases: + + x: [-------] + y: --[ ]--- + + case 1 above: SAT, cannot say more unless a1 is [-∞,+∞] (then we can abduce that a1 is + the same as a2) + + x: [--] + y: ------[ ]-- + case 2 above: UNSAT -let abduce_ne a1 a2 = + x: [---] + y: ------[ ]-- + + case 3 above: SAT: x = x\cap y for both + + x: [----] + y: ------[ ]-- + + case 4 above: SAT: x\cap y for both + *) + if Bound.lt lower1 (Int l2) && Bound.gt upper1 (Int u2) then + (* case 1 *) + match a1 with + | Between (MinusInfinity, PlusInfinity) -> + Satisfiable (Some a2, None) + | _ -> + Satisfiable (None, None) + else if Bound.ge lower1 (Int l2) && Bound.le upper1 (Int u2) then (* case 2 *) + Unsatisfiable + else if + (* l1≥l2 or u1≤u2 but not both, i.e. x is on only one side of y and their intersection is + one interval *) + Bound.lt lower1 (Int l2) + then + (* case 3 & 4: x left of y *) + let lower = lower1 in + let upper = Bound.min upper1 (Int (IntLit.(add minus_one) l2)) in + let tighter = Some (between lower upper) in + Satisfiable (tighter, tighter) + else + (* l1≥l2 ∧ u1>u2*) + (* case 3 & 4: x right of y *) + let lower = Bound.max lower1 (Int (IntLit.(add one) u2)) in + let upper = upper1 in + let tighter = Some (between lower upper) in + Satisfiable (tighter, tighter) + + +let abduce_ne (a1 : t) (a2 : t) = + if has_empty_intersection a1 a2 then Satisfiable (None, None) + else + match (to_singleton a1, to_singleton a2) with + | Some _, Some _ -> + (* non-empty intersection between 2 singletons => they are the same singleton and hence the + same integer and have the same value, so cannot be disequal *) + Unsatisfiable + | None, None -> + (* non-empty intersection and each predicate can be satisfied by ≥2 elements => we cannot + know if they are disequal or not *) + Satisfiable (None, None) + | Some e1, None -> ( + match remove_element e1 a2 with + | Some _ as abduced2 -> + Satisfiable (None, abduced2) + | None -> + Satisfiable (None, None) ) + | None, Some e2 -> ( + match remove_element e2 a1 with + | Some _ as abduced1 -> + Satisfiable (abduced1, None) + | None -> + Satisfiable (None, None) ) + + +let abduce_le (a1 : t) (a2 : t) = match (a1, a2) with - | Some (EqualTo c1), Some (EqualTo c2) when Const.equal c1 c2 -> - (TBool.False, None, None) - | Some (EqualTo _c1), Some (EqualTo _c2) (* c1≠c2 *) -> - (TBool.True, None, None) - | None, Some _ | Some _, None -> - (* cannot express ≠c so go to Top *) - (TBool.Top, None, None) - | None, None -> - (TBool.Top, None, None) + | Between (lower1, upper1), Between (lower2, upper2) -> + (* ∃x≤y. l1≤x≤u1 ∧ l2≤y≤u2 *) + (* ⇔ ∃x,y. x≤y ∧ l1≤x≤min(u1,u2) ∧ max(l1,l2)≤y≤u2 *) + let min_u1u2 = Bound.min upper1 upper2 in + let max_l1l2 = Bound.max lower1 lower2 in + if Bound.lt min_u1u2 lower1 || Bound.lt upper2 max_l1l2 then + (* any of these contradict the formula above *) + Unsatisfiable + else Satisfiable (Some (between lower1 min_u1u2), Some (between max_l1l2 upper2)) + | Outside _, Outside _ -> + Satisfiable (None, None) + | Between (lower1, _upper1), Outside (l2, u2) -> + (* ∃x≤y. l1≤x≤u1 ∧ yu2 *) + (* two cases: + 1. l1 + (* similarly, two cases: + 1. u1≥u2: can refine to x≤min(l1+1, u2) + x: -----[ ]--------------------- + y: ..-] + or y: ...-----] + 2. u1l2 *) + let upper = Bound.min (Int (IntLit.(add one) l1)) upper2 in + Satisfiable (Some (between MinusInfinity upper), None) + else (* case 2: l1≤l2 *) + Satisfiable (None, None) -let abduce_binop_constraints ~negated (bop : Binop.t) a1 a2 = +let abduce_lt (a1 : t) (a2 : t) = + match abduce_le (add_int a1 IntLit.one) a2 with + | Satisfiable (Some abduced1, abduced2_opt) -> + Satisfiable (Some (add_int abduced1 IntLit.minus_one), abduced2_opt) + | result -> + result + + +let abduce_binop_constraints ~negated (bop : Binop.t) (a1 : t) (a2 : t) = let open Binop in match (bop, negated) with | Eq, false | Ne, true -> abduce_eq a1 a2 | Eq, true | Ne, false -> abduce_ne a1 a2 + | Le, false | Gt, true -> + abduce_le a1 a2 + | Ge, false | Lt, true -> + abduce_le a2 a1 |> flip_abduced + | Lt, false | Ge, true -> + abduce_lt a1 a2 + | Gt, false | Le, true -> + abduce_lt a2 a1 |> flip_abduced | _ -> - (TBool.Top, None, None) - - -let abduce_binop_is_true_aux ~negated bop a1_opt a2_opt = - Logging.d_printfln "abduce_binop_is_true ~negated:%b %s (%a) (%a)" negated - (Binop.str Pp.text bop) (Pp.option pp) a1_opt (Pp.option pp) a2_opt ; - abduce_binop_constraints ~negated bop a1_opt a2_opt + Satisfiable (None, None) let abduce_binop_is_true ~negated bop v1 v2 = - let result, abduced1, abduced2 = abduce_binop_is_true_aux ~negated bop v1 v2 in - let can_go_through = match result with Top | True -> true | False -> false in - (can_go_through, abduced1, abduced2) + Logging.d_printfln "abduce_binop_is_true ~negated:%b %s (%a) (%a)" negated + (Binop.str Pp.text bop) (Pp.option pp) v1 (Pp.option pp) v2 ; + match (v1, v2) with + | None, None -> + (* two existential variables: no way to express in the non-relational domain *) + Satisfiable (None, None) + | _ -> + let unknown = between MinusInfinity PlusInfinity in + let a1 = Option.value v1 ~default:unknown in + let a2 = Option.value v2 ~default:unknown in + abduce_binop_constraints ~negated bop a1 a2 diff --git a/infer/src/pulse/PulseArithmetic.mli b/infer/src/pulse/PulseArithmetic.mli index 90333e89d..b50b7f667 100644 --- a/infer/src/pulse/PulseArithmetic.mli +++ b/infer/src/pulse/PulseArithmetic.mli @@ -7,19 +7,31 @@ open! IStd module F = Format -type t = EqualTo of Const.t [@@deriving compare] +module Bound : sig + type t = Int of IntLit.t | MinusInfinity | PlusInfinity +end + +type t = private Between of Bound.t * Bound.t | Outside of IntLit.t * IntLit.t +[@@deriving compare] + +val equal_to : IntLit.t -> t val pp : F.formatter -> t -> unit -val abduce_binop_is_true : - negated:bool -> Binop.t -> t option -> t option -> bool * t option * t option -(** given [arith_lhs_opt bop arith_rhs_opt], return a triple - [(satisfiable,abduced_lhs_opt,abduced_rhs_opt)] such that (taking lhs=true if lhs_opt is [None], - same for rhs): +type abduction_result = + | Unsatisfiable (** the assertion is never true given the parameters *) + | Satisfiable of t option * t option + (** the assertion is satisfiable and when it is true then the lhs and rhs can be optionally + refined to the given new intervals *) + +val abduce_binop_is_true : negated:bool -> Binop.t -> t option -> t option -> abduction_result +(** given [arith_lhs_opt bop arith_rhs_opt] and if not [negated], return either - - [satisfiable] iff lhs bop rhs ≠ ∅ + - [Unsatisfiable] iff lhs bop rhs = ∅ - - [abduced_lhs_opt=Some alhs] if [satisfiable] and (lhs bop rhs ≠ ∅ => alhs⇔lhs) (and similarly for rhs) + - [Satisfiable (abduced_lhs_opt,abduced_rhs_opt)] iff lhs bop rhs ≠ ∅, such that (taking lhs=true + if lhs_opt is [None], same for rhs) [abduced_lhs_opt=Some alhs] if (lhs bop rhs ≠ ∅ => alhs⇔lhs) + (and similarly for rhs) - - likewise if [negated] with (lhs bop rhs = ∅) in the two points above + If [negated] then imagine a similar explanation replacing "= ∅" with "≠ ∅" and vice-versa. *) diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 1badf4cfe..d29107857 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -60,7 +60,7 @@ module Attribute = struct let std_vector_reserve_rank = Variants.to_rank StdVectorReserve - let const_rank = Variants.to_rank (Arithmetic (Arithmetic.EqualTo (Cint IntLit.zero))) + let const_rank = Variants.to_rank (Arithmetic (Arithmetic.equal_to IntLit.zero)) let pp f attribute = let pp_string_if_debug string fmt () = diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 086cc0c6b..c0e142362 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -131,12 +131,12 @@ let eval location exp0 astate = Closures.record location name (List.rev rev_captured) astate | Cast (_, exp') -> eval exp' astate - | Const c -> + | Const (Cint i) -> (* TODO: make identical const the same address *) let addr = AbstractValue.mk_fresh () in - let astate = Memory.add_attribute addr (Arithmetic (Arithmetic.EqualTo c)) astate in + let astate = Memory.add_attribute addr (Arithmetic (Arithmetic.equal_to i)) astate in Ok (astate, (addr, [])) - | Sizeof _ | UnOp _ | BinOp _ | Exn _ -> + | Const _ | Sizeof _ | UnOp _ | BinOp _ | Exn _ -> Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) [])) in eval exp0 astate @@ -144,8 +144,8 @@ let eval location exp0 astate = let eval_arith location exp astate = match (exp : Exp.t) with - | Const c -> - Ok (astate, None, Some (Arithmetic.EqualTo c)) + | Const (Cint i) -> + Ok (astate, None, Some (Arithmetic.equal_to i)) | exp -> ( eval location exp astate >>| fun (astate, (addr, _)) -> @@ -167,14 +167,17 @@ let record_abduced addr_opt arith_opt astate = let rec eval_cond ~negated location exp astate = match (exp : Exp.t) with - | BinOp (bop, e1, e2) -> + | BinOp (bop, e1, e2) -> ( eval_arith location e1 astate >>= fun (astate, addr1, eval1) -> eval_arith location e2 astate >>| fun (astate, addr2, eval2) -> - let result, abduced1, abduced2 = Arithmetic.abduce_binop_is_true ~negated bop eval1 eval2 in - let astate = record_abduced addr1 abduced1 astate |> record_abduced addr2 abduced2 in - (astate, result) + match Arithmetic.abduce_binop_is_true ~negated bop eval1 eval2 with + | Unsatisfiable -> + (astate, false) + | Satisfiable (abduced1, abduced2) -> + let astate = record_abduced addr1 abduced1 astate |> record_abduced addr2 abduced2 in + (astate, true) ) | UnOp (LNot, exp', _) -> eval_cond ~negated:(not negated) location exp' astate | exp -> diff --git a/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp b/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp index c3799ff23..b3ddd0d41 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp @@ -15,8 +15,7 @@ void unreachable_eq_then_ne_ok(int* x, int y) { } } -// pulse only tracks equality for now, not disequality -void FP_unreachable_ne_then_eq_ok(int* x, int y) { +void unreachable_ne_then_eq_ok(int* x, int y) { if (y != 0) { free(x); } @@ -32,6 +31,7 @@ bool equal_explicit(size_t x, size_t y) { return false; } +// need relational domain to give this a good spec bool equal(size_t x, size_t y) { return x == y; } diff --git a/infer/tests/codetoanalyze/cpp/pulse/fbstring.cpp b/infer/tests/codetoanalyze/cpp/pulse/fbstring.cpp index 93d5ddde6..dc8f0cc38 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/fbstring.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/fbstring.cpp @@ -30,7 +30,7 @@ struct LikeFBString { int category_; char* buffer_; size_t size_; - unsigned int refcount; + unsigned int* refcount_; LikeFBString() {} @@ -64,18 +64,20 @@ struct LikeFBString { } void copyLarge(const LikeFBString& src) { - refcount++; buffer_ = src.buffer_; size_ = src.size_; + refcount_ = src.refcount_; + *refcount_ = *refcount_ + 1; } int category() const { return category_; } - void incr_ref_count() { refcount++; } - void decr_ref_count() { - refcount--; - if (refcount == 0) { + if (*refcount_ <= 0) { + exit(1); + } + *refcount_ = *refcount_ - 1; + if (*refcount_ == 0) { free(buffer_); } } @@ -89,10 +91,7 @@ void copy_fbstring(LikeFBString& s) { LikeFBString t = s; } -void FP_pass_to_copy_ok() { - // Currently pulse follows impossible control flow and thinks the - // underlying buffer of s is freed twice: once per copy. That is - // caused by manual ref-counting in the case of large strings. +void pass_to_copy_ok() { LikeFBString s; copy_fbstring(s); } diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 37ffe22a0..da9c130d1 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -6,12 +6,10 @@ codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6 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, FP_unreachable_ne_then_eq_ok, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of FP_unreachable_ne_then_eq_ok,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of FP_unreachable_ne_then_eq_ok,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] 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] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<_Bool>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,when calling `deduplication::templated_delete_function<_Bool>` here,parameter `a` of deduplication::templated_delete_function<_Bool>,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function<_Bool>` here,parameter `a` of deduplication::templated_access_function<_Bool>,invalid access occurs here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,when calling `deduplication::templated_delete_function` here,parameter `a` of deduplication::templated_delete_function,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function` here,parameter `a` of deduplication::templated_access_function,invalid access occurs here] -codetoanalyze/cpp/pulse/fbstring.cpp, FP_pass_to_copy_ok, 6, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,when calling `copy_fbstring` here,parameter `s` of copy_fbstring,passed as argument to `LikeFBString::LikeFBString`,parameter `src` of LikeFBString::LikeFBString,passed as argument to `LikeFBString::copyLarge`,parameter `src` of LikeFBString::copyLarge,assigned,return from call to `LikeFBString::copyLarge`,return from call to `LikeFBString::LikeFBString`,when calling `LikeFBString::~LikeFBString` here,parameter `this` of LikeFBString::~LikeFBString,when calling `LikeFBString::__infer_inner_destructor_~LikeFBString` here,parameter `this` of LikeFBString::__infer_inner_destructor_~LikeFBString,when calling `LikeFBString::decr_ref_count` here,parameter `this` of LikeFBString::decr_ref_count,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `LikeFBString::~LikeFBString` here,parameter `this` of LikeFBString::~LikeFBString,when calling `LikeFBString::__infer_inner_destructor_~LikeFBString` here,parameter `this` of LikeFBString::__infer_inner_destructor_~LikeFBString,when calling `LikeFBString::decr_ref_count` here,parameter `this` of LikeFBString::decr_ref_count,invalid access occurs here] codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp, UsingDelayedDestruction::double_delete_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `this` of UsingDelayedDestruction::double_delete_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `this` of UsingDelayedDestruction::double_delete_bad,invalid access occurs here] codetoanalyze/cpp/pulse/frontend.cpp, deref_null_namespace_alias_ptr_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `some::thing::bad_ptr` here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `some::thing::bad_ptr`,return from call to `some::thing::bad_ptr`,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/interprocedural.cpp, access_to_invalidated_alias2_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of access_to_invalidated_alias2_bad,assigned,when calling `invalidate_and_set_to_null` here,parameter `x_ptr` of invalidate_and_set_to_null,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of access_to_invalidated_alias2_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here] @@ -52,7 +50,6 @@ codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `p` declared here,when calling `invalidate_local_ok` here,variable `t` declared here,is the address of a stack variable `t` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `p` declared here,passed as argument to `invalidate_local_ok`,variable `t` declared here,assigned,return from call to `invalidate_local_ok`,invalid access occurs here] codetoanalyze/cpp/pulse/values.cpp, FP_infeasible_tricky_ok, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of FP_infeasible_tricky_ok,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of FP_infeasible_tricky_ok,invalid access occurs here] -codetoanalyze/cpp/pulse/values.cpp, FP_no_free_if_ok, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of FP_no_free_if_ok,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of FP_no_free_if_ok,invalid access occurs here] codetoanalyze/cpp/pulse/values.cpp, error_under_true_conditionals_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,invalid access occurs here] codetoanalyze/cpp/pulse/values.cpp, free_if_deref_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of free_if_deref_bad,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of free_if_deref_bad,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/values.cpp b/infer/tests/codetoanalyze/cpp/pulse/values.cpp index f5e3d7bd4..b9215fb4b 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/values.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/values.cpp @@ -48,7 +48,7 @@ void free_if(int* x, int b) { } } -void FP_no_free_if_ok(int* x) { +void no_free_if_ok(int* x) { free_if(x, 0); *x = 42; }