From e549103d75bf5d2e0fe32da0150be4979bc83dde Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 1 Apr 2021 10:24:57 -0700 Subject: [PATCH] [pulse] use term_eqs Summary: Whenever an equality "t = v" (t an arbitrary term, v a variable) is added (or "v = t"), remember the "t -> v" mapping after canonicalising t and v. Use this to detect when two variables are equal to the same term: `t = v` and `t = v'` now yields `v = v'` to be added to the equality relation of variables. This increases the precision of the arithmetic engine. Interestingly, the impact on most code I've tried is: 1. mostly same perfs as before, if a bit slower (could be within noise) 2. slightly more (latent) bugs reported in absolute numbers I would have expected it to be more expensive and yield fewer bugs (as fewer false positives), but there could be second-order effects at play here where we get more coverage. We definitely get more latent issues due to dereferencing pointers after testing nullness, as can be seen in the unit tests as well, which may alone explain (2). There's some complexity when adding term equalities where the term is linear, as we also need to add it to `linear_eqs` but `term_eqs` and `linear_eqs` are interested in slightly different normal forms. Reviewed By: skcho Differential Revision: D27331336 fbshipit-source-id: 7314e127a --- infer/src/pulse/PulseFormula.ml | 222 +++++++++++++++--- infer/src/pulse/unit/PulseFormulaTest.ml | 75 +++--- infer/tests/codetoanalyze/c/pulse/issues.exp | 1 + infer/tests/codetoanalyze/c/pulse/nullptr.c | 5 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 11 +- .../codetoanalyze/cpp/pulse/optional.cpp | 14 +- .../tests/codetoanalyze/cpp/pulse/values.cpp | 12 +- 7 files changed, 249 insertions(+), 91 deletions(-) diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index 7e8c6a498..350881517 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -448,10 +448,20 @@ module Term = struct fold_map_direct_subterms t ~init:() ~f:(fun () t' -> ((), f t')) |> snd - let rec map_subterms t ~f = - let t' = map_direct_subterms t ~f:(fun t' -> map_subterms t' ~f) in - f t' + let rec fold_map_subterms t ~init ~f = + let acc, t' = + fold_map_direct_subterms t ~init ~f:(fun acc t' -> fold_map_subterms t' ~init:acc ~f) + in + f acc t' + + + let fold_subterms t ~init ~f = fold_map_subterms t ~init ~f:(fun acc t' -> (f acc t', t')) |> fst + let map_subterms t ~f = fold_map_subterms t ~init:() ~f:(fun () t' -> ((), f t')) |> snd + + let iter_subterms t ~f = Container.iter ~fold:fold_subterms t ~f + + let exists_subterm t ~f = Container.exists ~iter:iter_subterms t ~f let rec fold_subst_variables t ~init ~f = match t with @@ -1075,7 +1085,9 @@ module Formula = struct { var_eqs: var_eqs (** equality relation between variables *) ; linear_eqs: linear_eqs (** equalities of the form [x = l] where [l] is from linear arithmetic *) - ; term_eqs: Term.VarMap.t_ (** equalities of the form [t = x] *) + ; term_eqs: Term.VarMap.t_ + (** equalities of the form [t = x], used to detect when two abstract values are equal to + the same term (hence equal) *) ; atoms: Atom.Set.t (** "everything else"; not always normalized w.r.t. the components above *) } [@@deriving compare, equal, yojson_of] @@ -1107,6 +1119,8 @@ module Formula = struct module Normalizer : sig val and_var_linarith : Var.t -> LinArith.t -> t * new_eqs -> (t * new_eqs) SatUnsat.t + val and_var_term : Var.t -> Term.t -> t * new_eqs -> (t * new_eqs) SatUnsat.t + val and_var_var : Var.t -> Var.t -> t * new_eqs -> (t * new_eqs) SatUnsat.t val and_atom : Atom.t -> t * new_eqs -> (t * new_eqs) SatUnsat.t @@ -1151,7 +1165,7 @@ module Formula = struct (** substitute vars in [l] *once* with their linear form to discover more simplification opportunities *) - let apply phi l = + let normalize_linear phi l = LinArith.subst_variables l ~f:(fun v -> let repr = (get_repr phi v :> Var.t) in match Var.Map.find_opt repr phi.linear_eqs with @@ -1161,6 +1175,22 @@ module Formula = struct LinSubst l' ) + let normalize_var_const phi t = + Term.subst_variables t ~f:(fun v -> + let v_canon = (get_repr phi v :> Var.t) in + match Var.Map.find_opt v_canon phi.linear_eqs with + | None -> + VarSubst v_canon + | Some l -> ( + match LinArith.get_as_const l with + | None -> + (* OPTIM: don't make the term bigger *) VarSubst v_canon + | Some q -> + (* replace vars by constants when available to possibly trigger further + simplifications in atoms. This is not actually needed for [term_eqs]. *) + QSubst q ) ) + + let add_lin_eq_to_new_eqs v l new_eqs = match LinArith.get_as_const l with | Some q when Q.is_zero q -> @@ -1169,6 +1199,9 @@ module Formula = struct new_eqs + (** add [l1 = l2] to [phi.linear_eqs] and resolves consequences of that new fact + + [l1] and [l2] should have already been through {!normalize_linear} (w.r.t. [phi]) *) let rec solve_normalized_lin_eq ~fuel new_eqs l1 l2 phi = LinArith.solve_eq l1 l2 >>= function @@ -1181,10 +1214,14 @@ module Formula = struct | None -> ( match Var.Map.find_opt (v :> Var.t) phi.linear_eqs with | None -> + (* add to the [term_eqs] relation only when we also add to [linear_eqs] *) + let+ phi, new_eqs = + solve_normalized_term_eq_no_lin ~fuel new_eqs (Term.Linear l) (v :> Var.t) phi + in let new_eqs = add_lin_eq_to_new_eqs v l new_eqs in (* this can break the (as a result non-)invariant that variables in the domain of [linear_eqs] do not appear in the range of [linear_eqs] *) - Sat ({phi with linear_eqs= Var.Map.add (v :> Var.t) l phi.linear_eqs}, new_eqs) + ({phi with linear_eqs= Var.Map.add (v :> Var.t) l phi.linear_eqs}, new_eqs) | Some l' -> (* This is the only step that consumes fuel: discovering an equality [l = l']: because we do not record these anywhere (except when their consequence can be recorded as [y = @@ -1192,7 +1229,7 @@ module Formula = struct diverge otherwise. Or could we? *) (* [l'] is possibly not normalized w.r.t. the current [phi] so take this opportunity to normalize it, and replace [v]'s current binding *) - let l'' = apply phi l' in + let l'' = normalize_linear phi l' in let phi = if phys_equal l' l'' then phi else {phi with linear_eqs= Var.Map.add (v :> Var.t) l'' phi.linear_eqs} @@ -1206,6 +1243,72 @@ module Formula = struct Sat (phi, new_eqs) ) ) ) + (** add [t = v] to [phi.term_eqs] and resolves consequences of that new fact; don't use directly + as it doesn't do any checks on what else should be done about [t = v] *) + and solve_normalized_term_eq_no_lin_ ~fuel new_eqs t v phi = + match Term.VarMap.find_opt t phi.term_eqs with + | None -> + (* [t] isn't known already: add it *) + Sat ({phi with term_eqs= Term.VarMap.add t v phi.term_eqs}, new_eqs) + | Some v' -> + (* [t = v'] already in the map, need to explore consequences of [v = v']*) + merge_vars ~fuel new_eqs v v' phi + + + (** add [t = v] to [phi.term_eqs] and resolves consequences of that new fact; assumes that + linear facts have been or will be added to [phi.linear_eqs] separately + + [t] should have already been through {!normalize_var_const} and [v] should be a + representative from {!get_repr} (w.r.t. [phi]) *) + and solve_normalized_term_eq_no_lin ~fuel new_eqs (t : Term.t) v phi = + match t with + | Linear l when LinArith.get_as_var l |> Option.is_some -> + (* [v1=v2] is already taken care of by [var_eqs] *) + Sat (phi, new_eqs) + | _ -> + let t = + match t with + | Linear l -> ( + match LinArith.get_as_const l with Some c -> Term.Const c | None -> t ) + | _ -> + t + in + solve_normalized_term_eq_no_lin_ ~fuel new_eqs t v phi + + + (** same as {!solve_normalized_eq_no_lin} but also adds linear to [phi.linear_eqs] *) + and solve_normalized_term_eq ~fuel new_eqs (t : Term.t) v phi = + match t with + | Linear l when LinArith.get_as_var l |> Option.is_some -> + (* [v1=v2] is already taken care of by [var_eqs] *) + Sat (phi, new_eqs) + | Linear l -> ( + (* [l = v]: need to first solve it to get [l' = v'] such that [v' < vars(l')], and [l'] is + normalized wrt [phi.linear_eqs] (to get a canonical form), add this to [term_eqs], then + in order to know which equality should be added to [linear_eqs] we still need to + substitute [v'] with [linear_eqs] and solve again *) + LinArith.solve_eq (normalize_linear phi l) (LinArith.of_var v) + >>= function + | None -> + (* [v = v], we can drop this tautology *) + Sat (phi, new_eqs) + | Some (v', l') -> + (* [l'] could contain [v], which hasn't been through [linear_eqs], so normalize again *) + let l' = normalize_linear phi l' in + let* phi, new_eqs = + solve_normalized_term_eq_no_lin_ ~fuel new_eqs (Term.Linear l') v' phi + in + solve_normalized_lin_eq ~fuel new_eqs l' + (normalize_linear phi (LinArith.of_var v')) + phi ) + | Const c -> + (* same as above but constants ([c]) are always normalized so it's simpler *) + let* phi, new_eqs = solve_normalized_term_eq_no_lin_ ~fuel new_eqs t v phi in + solve_normalized_lin_eq ~fuel new_eqs (LinArith.of_q c) (LinArith.of_var v) phi + | _ -> + solve_normalized_term_eq_no_lin ~fuel new_eqs t v phi + + and merge_vars ~fuel new_eqs v1 v2 phi = let var_eqs, subst_opt = VarUF.union phi.var_eqs v1 v2 in let phi = {phi with var_eqs} in @@ -1262,7 +1365,8 @@ module Formula = struct let base_fuel = 10 let solve_lin_eq new_eqs t1 t2 phi = - solve_normalized_lin_eq ~fuel:base_fuel new_eqs (apply phi t1) (apply phi t2) phi + solve_normalized_lin_eq ~fuel:base_fuel new_eqs (normalize_linear phi t1) + (normalize_linear phi t2) phi let and_var_linarith v l (phi, new_eqs) = solve_lin_eq new_eqs l (LinArith.of_var v) phi @@ -1271,7 +1375,7 @@ module Formula = struct Var.Map.fold (fun v l acc -> let* changed, ((_, new_eqs) as phi_new_eqs) = acc in - let l' = apply phi0 l in + let l' = normalize_linear phi0 l in let+ phi', new_eqs' = and_var_linarith v l' phi_new_eqs in let changed', new_eqs' = if phys_equal l l' then (changed, new_eqs) else (true, new_eqs') @@ -1282,19 +1386,33 @@ module Formula = struct let normalize_atom phi (atom : Atom.t) = - let normalize_term phi t = - Term.subst_variables t ~f:(fun v -> - let v_canon = (get_repr phi v :> Var.t) in - match Var.Map.find_opt v_canon phi.linear_eqs with - | None -> - VarSubst v_canon - | Some l -> ( - match LinArith.get_as_const l with None -> LinSubst l | Some q -> QSubst q ) ) - in - let atom' = Atom.map_terms atom ~f:(fun t -> normalize_term phi t) in + let atom' = Atom.map_terms atom ~f:(fun t -> normalize_var_const phi t) in Atom.eval atom' |> sat_of_eval_result + let and_var_term ~fuel v t (phi, new_eqs) = + let t' : Term.t = normalize_var_const phi t |> Atom.eval_term in + let v' = (get_repr phi v :> Var.t) in + (* check if unsat given what we know of [v'] and [t'], in other words be at least as + complete as general atoms *) + let* _ = Atom.eval (Equal (t', normalize_var_const phi (Var v'))) |> sat_of_eval_result in + solve_normalized_term_eq ~fuel new_eqs t' v' phi + + + let normalize_term_eqs (phi0, new_eqs0) = + Term.VarMap.fold + (fun t v acc_sat_unsat -> + let* new_lin, ((_phi, new_eqs) as phi_new_eqs) = acc_sat_unsat in + let+ phi', new_eqs' = and_var_term ~fuel:base_fuel v t phi_new_eqs in + let new_lin, new_eqs' = + if phys_equal phi'.linear_eqs phi0.linear_eqs then (new_lin, new_eqs) + else (true, new_eqs') + in + (new_lin, (phi', new_eqs')) ) + phi0.term_eqs + (Sat (false, ({phi0 with term_eqs= Term.VarMap.empty}, new_eqs0))) + + (** return [(new_linear_equalities, phi ∧ atom)], where [new_linear_equalities] is [true] if [phi.linear_eqs] was changed as a result *) let and_atom atom (phi, new_eqs) = @@ -1302,12 +1420,19 @@ module Formula = struct >>= function | None -> Sat (false, (phi, new_eqs)) + | Some (Atom.Equal (Linear _, Linear _)) -> + assert false | Some (Atom.Equal (Linear l, Const c)) | Some (Atom.Equal (Const c, Linear l)) -> (* NOTE: {!normalize_atom} calls {!Atom.eval}, which normalizes linear equalities so they end up only on one side, hence only this match case is needed to detect linear equalities *) let+ phi', new_eqs = solve_lin_eq new_eqs l (LinArith.of_q c) phi in (true, (phi', new_eqs)) + | Some (Atom.Equal (Linear l, t) | Atom.Equal (t, Linear l)) + when Option.is_some (LinArith.get_as_var l) -> + let v = Option.value_exn (LinArith.get_as_var l) in + let+ phi_new_eqs' = solve_normalized_term_eq ~fuel:base_fuel new_eqs t v phi in + (false, phi_new_eqs') | Some atom' -> Sat (false, ({phi with atoms= Atom.Set.add atom' phi.atoms}, new_eqs)) @@ -1321,22 +1446,23 @@ module Formula = struct (changed || changed', phi_new_eqs) ) - let rec normalize_with_fuel ~fuel ((phi0, new_eqs0) as phi_new_eqs0) = + let rec normalize_with_fuel ~fuel phi_new_eqs0 = if fuel < 0 then ( L.d_printfln "ran out of fuel when normalizing" ; Sat phi_new_eqs0 ) else - (* reconstruct the linear relation from scratch *) let* new_linear_eqs, phi_new_eqs' = - let* new_linear_eqs_from_linear, phi_new_eqs = normalize_linear_eqs (phi0, new_eqs0) in + let* new_linear_eqs_from_linear, phi_new_eqs = normalize_linear_eqs phi_new_eqs0 in if new_linear_eqs_from_linear && fuel > 0 then (* do another round of linear normalization early if we will renormalize again anyway; - no need to first normalize atoms w.r.t. a linear relation that's going to change and - trigger a recompute of these anyway *) + no need to first normalize term_eqs and atoms w.r.t. a linear relation that's going + to change and trigger a recompute of these anyway *) Sat (true, phi_new_eqs) else + let* new_linear_eqs_from_terms, phi_new_eqs = normalize_term_eqs phi_new_eqs in let+ new_linear_eqs_from_atoms, phi_new_eqs = normalize_atoms phi_new_eqs in - (new_linear_eqs_from_linear || new_linear_eqs_from_atoms, phi_new_eqs) + ( new_linear_eqs_from_linear || new_linear_eqs_from_terms || new_linear_eqs_from_atoms + , phi_new_eqs ) in if new_linear_eqs then ( L.d_printfln "new linear equalities, consuming fuel (from %d)" fuel ; @@ -1350,6 +1476,8 @@ module Formula = struct let and_atom atom phi_new_eqs = and_atom atom phi_new_eqs >>| snd + let and_var_term v t phi_new_eqs = and_var_term ~fuel:base_fuel v t phi_new_eqs + let and_var_var v1 v2 (phi, new_eqs) = merge_vars ~fuel:base_fuel new_eqs v1 v2 phi let implies_atom phi atom = @@ -1455,6 +1583,21 @@ module DynamicTypes = struct t in let changed = ref false in + let term_eqs = + if + Term.VarMap.exists + (fun t _ -> Term.exists_subterm t ~f:(function IsInstanceOf _ -> true | _ -> false)) + phi.both.term_eqs + then + (* slow path: reconstruct everything *) + Term.VarMap.fold + (fun t v term_eqs' -> + let t' = Term.map_subterms t ~f:simplify_is_instance_of in + changed := !changed || not (phys_equal t t') ; + Term.VarMap.add t' v term_eqs' ) + phi.both.term_eqs Term.VarMap.empty + else (* fast path: nothing to do *) phi.both.term_eqs + in let atoms = Atom.Set.map (fun atom -> @@ -1464,7 +1607,7 @@ module DynamicTypes = struct t' ) ) phi.both.atoms in - if !changed then {phi with both= {phi.both with atoms}} else phi + if !changed then {phi with both= {phi.both with atoms; term_eqs}} else phi end let normalize tenv ~get_dynamic_type phi = @@ -1517,6 +1660,14 @@ let and_fold_subst_variables phi0 ~up_to_f:phi_foreign ~init ~f:f_var = let phi_new_eqs = Formula.Normalizer.and_var_linarith v l phi_new_eqs |> sat_value_exn in (acc_f, phi_new_eqs) ) in + let and_term_eqs term_eqs_foreign acc_phi_new_eqs = + IContainer.fold_of_pervasives_map_fold Term.VarMap.fold term_eqs_foreign ~init:acc_phi_new_eqs + ~f:(fun (acc_f, phi_new_eqs) (t_foreign, v_foreign) -> + let acc_f, t = Term.fold_subst_variables t_foreign ~init:acc_f ~f:f_subst in + let acc_f, v = f_var acc_f v_foreign in + let phi_new_eqs = Formula.Normalizer.and_var_term v t phi_new_eqs |> sat_value_exn in + (acc_f, phi_new_eqs) ) + in let and_atoms atoms_foreign acc_phi_new_eqs = IContainer.fold_of_pervasives_set_fold Atom.Set.fold atoms_foreign ~init:acc_phi_new_eqs ~f:(fun (acc_f, phi_new_eqs) atom_foreign -> @@ -1529,6 +1680,7 @@ let and_fold_subst_variables phi0 ~up_to_f:phi_foreign ~init ~f:f_var = Sat ( and_var_eqs phi_foreign.Formula.var_eqs (acc, (phi, [])) |> and_linear_eqs phi_foreign.Formula.linear_eqs + |> and_term_eqs phi_foreign.Formula.term_eqs |> and_atoms phi_foreign.Formula.atoms ) with Contradiction -> Unsat in @@ -1637,15 +1789,18 @@ module DeadVariables = struct |> Seq.fold_left (fun vs v -> Var.Set.add v vs) (Var.Set.singleton v) |> add_all ) phi.Formula.linear_eqs ; + (* helper function: compute [vs U vars(t)] *) + let union_vars_of_term t vs = + Term.fold_variables t ~init:vs ~f:(fun vs v -> Var.Set.add v vs) + in (* add edges between all pairs of variables appearing in [t1] or [t2] (yes this is quadratic in the number of variables of these terms) *) let add_from_terms t1 t2 = - (* compute [vs U vars(t)] *) - let union_vars_of_term t vs = - Term.fold_variables t ~init:vs ~f:(fun vs v -> Var.Set.add v vs) - in union_vars_of_term t1 Var.Set.empty |> union_vars_of_term t2 |> add_all in + Term.VarMap.iter + (fun t v -> union_vars_of_term t (Var.Set.singleton v) |> add_all) + phi.Formula.term_eqs ; Atom.Set.iter (fun atom -> let t1, t2 = Atom.get_terms atom in @@ -1693,7 +1848,7 @@ module DeadVariables = struct result. *) let var_graph = build_var_graph phi.both in let vars_to_keep = get_reachable_from var_graph keep in - L.d_printfln "Reachable vars: {%a}" Var.Set.pp vars_to_keep ; + L.d_printfln "Reachable vars: %a" Var.Set.pp vars_to_keep ; (* discard atoms which have variables *not* in [vars_to_keep], which in particular is enough to guarantee that *none* of their variables are in [vars_to_keep] thanks to transitive closure on the graph above *) @@ -1720,12 +1875,13 @@ end let simplify tenv ~get_dynamic_type ~keep phi = let open SatUnsat.Import in let* phi, new_eqs = normalize tenv ~get_dynamic_type phi in - L.d_printfln_escaped "Simplifying %a wrt {%a}" pp phi Var.Set.pp keep ; + L.d_printfln_escaped "@[Simplifying %a@,wrt %a@]" pp phi Var.Set.pp keep ; (* get rid of as many variables as possible *) let+ phi = QuantifierElimination.eliminate_vars ~keep phi in (* TODO: doing [QuantifierElimination.eliminate_vars; DeadVariables.eliminate] a few times may eliminate even more variables *) - (DeadVariables.eliminate ~keep phi, new_eqs) + let phi = DeadVariables.eliminate ~keep phi in + (phi, new_eqs) let is_known_zero phi v = diff --git a/infer/src/pulse/unit/PulseFormulaTest.ml b/infer/src/pulse/unit/PulseFormulaTest.ml index b4bd92247..5618ceaa2 100644 --- a/infer/src/pulse/unit/PulseFormulaTest.ml +++ b/infer/src/pulse/unit/PulseFormulaTest.ml @@ -176,9 +176,8 @@ let%test_module "normalization" = normalize (of_binop Eq x y = i 0 && x = i 0 && y = i 1) ; [%expect {| - known=true (no var=var) && x = 0 ∧ y = 1 ∧ v6 = 0 && true (no term_eqs) && true (no atoms), - pruned=true (no atoms), - both=true (no var=var) && x = 0 ∧ y = 1 ∧ v6 = 0 && true (no term_eqs) && true (no atoms)|}] + known=x=v6 && x = 0 ∧ y = 1 && 0=x∧1=y && true (no atoms), pruned=true (no atoms), + both=x=v6 && x = 0 ∧ y = 1 && 0=x∧1=y && true (no atoms)|}] let%expect_test _ = normalize (x = i 0 && x < i 0) ; @@ -196,36 +195,36 @@ let%test_module "normalization" = && x = -v6 + v8 -1 ∧ v7 = v8 -1 ∧ v10 = 0 && - true (no term_eqs) + 0=v10∧[-v6 + v8 -1]=x∧[v8 -1]=v7∧[z]×[v8]=v9∧[v]×[y]=v6∧[v9]÷[w]=v10 && - {0 = [v9]÷[w]}∧{[v6] = [v]×[y]}∧{[v9] = [z]×[v8]}, + true (no atoms), pruned=true (no atoms), both=true (no var=var) && x = -v6 + v8 -1 ∧ v7 = v8 -1 ∧ v10 = 0 && - true (no term_eqs) + 0=v10∧[-v6 + v8 -1]=x∧[v8 -1]=v7∧[z]×[v8]=v9∧[v]×[y]=v6∧[v9]÷[w]=v10 && - {0 = [v9]÷[w]}∧{[v6] = [v]×[y]}∧{[v9] = [z]×[v8]} |}] + true (no atoms) |}] (* check that this becomes all linear equalities *) let%expect_test _ = normalize (i 12 * (x + (i 3 * y) + i 1) / i 7 = i 0) ; [%expect {| - known=true (no var=var) + known=v8=v9=v10 && - x = -v6 -1 ∧ y = 1/3·v6 ∧ v7 = -1 ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0 + x = -v6 -1 ∧ y = 1/3·v6 ∧ v7 = -1 ∧ v8 = 0 && - true (no term_eqs) + -1=v7∧0=v8∧[-v6 -1]=x∧[1/3·v6]=y && true (no atoms), pruned=true (no atoms), - both=true (no var=var) + both=v8=v9=v10 && - x = -v6 -1 ∧ y = 1/3·v6 ∧ v7 = -1 ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0 + x = -v6 -1 ∧ y = 1/3·v6 ∧ v7 = -1 ∧ v8 = 0 && - true (no term_eqs) + -1=v7∧0=v8∧[-v6 -1]=x∧[1/3·v6]=y && true (no atoms)|}] @@ -234,21 +233,19 @@ let%test_module "normalization" = normalize (z * (x + (v * y) + i 1) / w = i 0 && z = i 12 && v = i 3 && w = i 7) ; [%expect {| - known=true (no var=var) + known=v8=v9=v10 && - x = -v6 -1 ∧ y = 1/3·v6 ∧ z = 12 ∧ w = 7 ∧ v = 3 ∧ v7 = -1 - ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0 + x = -v6 -1 ∧ y = 1/3·v6 ∧ z = 12 ∧ w = 7 ∧ v = 3 ∧ v7 = -1 ∧ v8 = 0 && - true (no term_eqs) + -1=v7∧0=v8∧3=v∧7=w∧12=z∧[-v6 -1]=x∧[1/3·v6]=y && true (no atoms), pruned=true (no atoms), - both=true (no var=var) + both=v8=v9=v10 && - x = -v6 -1 ∧ y = 1/3·v6 ∧ z = 12 ∧ w = 7 ∧ v = 3 ∧ v7 = -1 - ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0 + x = -v6 -1 ∧ y = 1/3·v6 ∧ z = 12 ∧ w = 7 ∧ v = 3 ∧ v7 = -1 ∧ v8 = 0 && - true (no term_eqs) + -1=v7∧0=v8∧3=v∧7=w∧12=z∧[-v6 -1]=x∧[1/3·v6]=y && true (no atoms)|}] end ) @@ -266,31 +263,31 @@ let%test_module "variable elimination" = simplify ~keep:[x_var] (x = i 0 && y = i 1 && z = i 2 && w = i 3) ; [%expect {| - known=true (no var=var) && x = 0 && true (no term_eqs) && true (no atoms), pruned=true (no atoms), - both=true (no var=var) && x = 0 && true (no term_eqs) && true (no atoms)|}] + known=true (no var=var) && x = 0 && 0=x && true (no atoms), pruned=true (no atoms), + both=true (no var=var) && x = 0 && 0=x && true (no atoms)|}] let%expect_test _ = simplify ~keep:[x_var] (x = y + i 1 && x = i 0) ; [%expect {| - known=true (no var=var) && x = 0 && true (no term_eqs) && true (no atoms), pruned=true (no atoms), - both=true (no var=var) && x = 0 && true (no term_eqs) && true (no atoms)|}] + known=true (no var=var) && x = 0 && 0=x && true (no atoms), pruned=true (no atoms), + both=true (no var=var) && x = 0 && 0=x && true (no atoms)|}] let%expect_test _ = simplify ~keep:[y_var] (x = y + i 1 && x = i 0) ; [%expect {| - known=true (no var=var) && y = -1 && true (no term_eqs) && true (no atoms), pruned=true (no atoms), - both=true (no var=var) && y = -1 && true (no term_eqs) && true (no atoms)|}] + known=true (no var=var) && y = -1 && -1=y && true (no atoms), pruned=true (no atoms), + both=true (no var=var) && y = -1 && -1=y && true (no atoms)|}] (* should keep most of this or realize that [w = z] hence this boils down to [z+1 = 0] *) let%expect_test _ = simplify ~keep:[y_var; z_var] (x = y + z && w = x - y && v = w + i 1 && v = i 0) ; [%expect {| - known=true (no var=var) && x = y -1 ∧ z = -1 && true (no term_eqs) && true (no atoms), + known=true (no var=var) && x = y -1 ∧ z = -1 && -1=z∧[y -1]=x && true (no atoms), pruned=true (no atoms), - both=true (no var=var) && x = y -1 ∧ z = -1 && true (no term_eqs) && true (no atoms)|}] + both=true (no var=var) && x = y -1 ∧ z = -1 && -1=z∧[y -1]=x && true (no atoms)|}] let%expect_test _ = simplify ~keep:[x_var; y_var] (x = y + z && w + x + y = i 0 && v = w + i 1) ; @@ -300,7 +297,7 @@ let%test_module "variable elimination" = && x = -v + v7 +1 ∧ y = -v7 ∧ z = -v + 2·v7 +1 ∧ w = v -1 && - true (no term_eqs) + [v -1]=w∧[-v7]=y∧[-v + v7 +1]=x∧[-v + 2·v7 +1]=z && true (no atoms), pruned=true (no atoms), @@ -308,7 +305,7 @@ let%test_module "variable elimination" = && x = -v + v7 +1 ∧ y = -v7 ∧ z = -v + 2·v7 +1 ∧ w = v -1 && - true (no term_eqs) + [v -1]=w∧[-v7]=y∧[-v + v7 +1]=x∧[-v + 2·v7 +1]=z && true (no atoms)|}] @@ -316,8 +313,8 @@ let%test_module "variable elimination" = simplify ~keep:[x_var; y_var] (x = y + i 4 && x = w && y = z) ; [%expect {| - known=true (no var=var) && x = y +4 && true (no term_eqs) && true (no atoms), - pruned=true (no atoms), both=true (no var=var) && x = y +4 && true (no term_eqs) && true (no atoms)|}] + known=true (no var=var) && x = y +4 && [y +4]=x && true (no atoms), pruned=true (no atoms), + both=true (no var=var) && x = y +4 && [y +4]=x && true (no atoms)|}] end ) let%test_module "non-linear simplifications" = @@ -326,15 +323,15 @@ let%test_module "non-linear simplifications" = simplify ~keep:[w_var] (((i 0 / (x * z)) & v) * v mod y = w) ; [%expect {| - known=true (no var=var) && w = 0 && true (no term_eqs) && true (no atoms), pruned=true (no atoms), - both=true (no var=var) && w = 0 && true (no term_eqs) && true (no atoms)|}] + known=true (no var=var) && w = 0 && 0=w && true (no atoms), pruned=true (no atoms), + both=true (no var=var) && w = 0 && 0=w && true (no atoms)|}] let%expect_test "constant propagation: bitshift" = simplify ~keep:[x_var] (of_binop Shiftlt (of_binop Shiftrt (i 0b111) (i 2)) (i 2) = x) ; [%expect {| - known=true (no var=var) && x = 4 && true (no term_eqs) && true (no atoms), pruned=true (no atoms), - both=true (no var=var) && x = 4 && true (no term_eqs) && true (no atoms)|}] + known=true (no var=var) && x = 4 && 4=x && true (no atoms), pruned=true (no atoms), + both=true (no var=var) && x = 4 && 4=x && true (no atoms)|}] let%expect_test "non-linear becomes linear" = normalize (w = (i 2 * z) - i 3 && z = x * y && y = i 2) ; @@ -344,7 +341,7 @@ let%test_module "non-linear simplifications" = && x = 1/4·v6 ∧ y = 2 ∧ z = 1/2·v6 ∧ w = v6 -3 && - true (no term_eqs) + 2=y∧[v6 -3]=w∧[1/4·v6]=x∧[1/2·v6]=z && true (no atoms), pruned=true (no atoms), @@ -352,7 +349,7 @@ let%test_module "non-linear simplifications" = && x = 1/4·v6 ∧ y = 2 ∧ z = 1/2·v6 ∧ w = v6 -3 && - true (no term_eqs) + 2=y∧[v6 -3]=w∧[1/4·v6]=x∧[1/2·v6]=z && true (no atoms)|}] end ) diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index 0752afb80..3323f2c02 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -8,6 +8,7 @@ codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, MEMORY_LE codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/c/pulse/nullptr.c, FN_bug_after_malloc_result_test_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, malloc_no_check_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,null pointer dereference part of the trace starts here,allocated by call to `malloc` (modelled),assigned,invalid access occurs here] +codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_unconditionally_latent, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,null pointer dereference part of the trace starts here,parameter `p` of malloc_then_call_create_null_path_then_deref_unconditionally_latent,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/c/pulse/uninit.c, call_to_use_and_mayinit_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here] codetoanalyze/c/pulse/uninit.c, dereference_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `p` declared here,read to uninitialized value occurs here] diff --git a/infer/tests/codetoanalyze/c/pulse/nullptr.c b/infer/tests/codetoanalyze/c/pulse/nullptr.c index 953471b6a..7fed5bf07 100644 --- a/infer/tests/codetoanalyze/c/pulse/nullptr.c +++ b/infer/tests/codetoanalyze/c/pulse/nullptr.c @@ -37,7 +37,8 @@ void create_null_path2_ok(int* p) { } // combine several of the difficulties above -void malloc_then_call_create_null_path_then_deref_unconditionally_ok(int* p) { +void malloc_then_call_create_null_path_then_deref_unconditionally_latent( + int* p) { int* x = (int*)malloc(sizeof(int)); if (p) { *p = 32; @@ -59,7 +60,7 @@ void nullptr_deref_young_bad(int* x) { // due to the recency model of memory accesses, vec[0] can get forgotten // by the time we have processed the last element of the // initialization so we don't report here -void nullptr_deref_old_bad_FP(int* x) { +void FN_nullptr_deref_old_bad(int* x) { int* vec[65] = {NULL, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 877ef6390..6d0c9b1a6 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -5,6 +5,7 @@ codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_str codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_latent, 6, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_latent, 6, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_latent, 5, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,invalid access occurs here] +codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_latent, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_latent, 8, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()` here,parameter `s` of call_lambda_bad::lambda_closures.cpp:163:12::operator(),invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, call_lambda_std_fun_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `call_lambda_std_fun_bad::lambda_closures.cpp:171:7::operator()` here,parameter `s` of call_lambda_std_fun_bad::lambda_closures.cpp:171:7::operator(),invalid access occurs here] @@ -50,7 +51,7 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_read_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_read_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] codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_delete` here,parameter `x` of wraps_delete,when calling `wraps_delete_inner` here,parameter `x` of wraps_delete_inner,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_write_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] codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `may_return_invalid_ptr_ok` here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `may_return_invalid_ptr_ok`,return from call to `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,parameter `y` of call_store,when calling `store` here,parameter `y` of store,invalid access occurs here] -codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,when calling `set_first_non_null_ok` here,parameter `y` of set_first_non_null_ok,invalid access occurs here] +codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,parameter `x` of set_x_then_crash_double_latent,when calling `set_first_non_null_ok` here,parameter `y` of set_first_non_null_ok,invalid access occurs here] codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 1, USE_AFTER_DELETE, no_bucket, ERROR, [calling context starts here,in call to `invalidate_node_alias_latent`,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here] @@ -64,23 +65,18 @@ codetoanalyze/cpp/pulse/nullptr.cpp, std_true_type_deref_bad, 3, NULLPTR_DEREFER codetoanalyze/cpp/pulse/nullptr.cpp, test_after_dereference2_latent, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,is the null pointer,null pointer dereference part of the trace starts here,parameter `x` of test_after_dereference2_latent,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, assign2_bad, 4, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `folly::Optional::operator=` here,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::operator=`,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::operator=`,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, assign_bad, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),passed as argument to `folly::Optional::operator=`,parameter `other` of folly::Optional::operator=,passed as argument to `folly::Optional::assign(folly::Optional arg)` (modelled),return from call to `folly::Optional::assign(folly::Optional arg)` (modelled),return from call to `folly::Optional::operator=`,invalid access occurs here] -codetoanalyze/cpp/pulse/optional.cpp, cannot_be_empty_FP, 2, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getOptionalValue` here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `getOptionalValue`,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),return from call to `getOptionalValue`,invalid access occurs here] -codetoanalyze/cpp/pulse/optional.cpp, get_pointer_no_check_none_check_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,passed as argument to `folly::Optional::get_pointer()` (modelled),return from call to `folly::Optional::get_pointer()` (modelled),is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `folly::Optional::get_pointer()` (modelled),return from call to `folly::Optional::get_pointer()` (modelled),assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/optional.cpp, get_pointer_no_check_none_check_bad, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::get_pointer()` (modelled),return from call to `folly::Optional::get_pointer()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, inside_try_catch_FP, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `might_return_none` here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `might_return_none`,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),return from call to `might_return_none`,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, none_copy_bad, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),passed as argument to `folly::Optional::Optional(folly::Optional arg)` (modelled),return from call to `folly::Optional::Optional(folly::Optional arg)` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, none_no_check_bad, 2, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, not_none_check_value_ok_FP, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, operator_arrow_bad, 0, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),when calling `emplace` here,parameter `state` of emplace,passed as argument to `folly::Optional::operator->()` (modelled),return from call to `folly::Optional::operator->()` (modelled),invalid access occurs here] -codetoanalyze/cpp/pulse/optional.cpp, smart_pointer_FP, 2, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Node::getShared` here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `Node::getShared`,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),return from call to `Node::getShared`,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, std_assign2_bad, 4, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `std::optional::operator=(None)` (modelled),return from call to `std::optional::operator=(None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `std::optional::operator=(None)` (modelled),return from call to `std::optional::operator=(None)` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, std_assign_bad, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),passed as argument to `std::optional::operator=(std::optional arg)` (modelled),return from call to `std::optional::operator=(std::optional arg)` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, std_none_copy_bad, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),passed as argument to `std::optional::optional(std::optional arg)` (modelled),return from call to `std::optional::optional(std::optional arg)` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, std_none_no_check_bad, 2, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, std_not_none_check_value_ok_FP, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),invalid access occurs here] -codetoanalyze/cpp/pulse/optional.cpp, std_operator_arrow_bad, 0, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),when calling `std_emplace` here,parameter `state` of std_emplace,passed as argument to `std::optional::operator->()` (modelled),return from call to `std::optional::operator->()` (modelled),invalid access occurs here] -codetoanalyze/cpp/pulse/optional.cpp, std_value_or_check_value_ok_FP, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, test_trace_ref, 4, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `folly::Optional::operator=` here,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::operator=`,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::operator=`,invalid access occurs here] -codetoanalyze/cpp/pulse/optional.cpp, value_or_check_value_ok_FP, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/path.cpp, faulty_call_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `only_bad_on_42_latent`,source of the null value part of the trace starts here,when calling `may_return_null` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `may_return_null`,return from call to `may_return_null`,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/path.cpp, only_bad_on_42_latent, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,when calling `may_return_null` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `may_return_null`,return from call to `may_return_null`,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getwrapperHeap` here,passed as argument to `WrapsB::WrapsB`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `WrapsB::WrapsB`,when calling `WrapsB::~WrapsB` here,parameter `this` of WrapsB::~WrapsB,when calling `WrapsB::__infer_inner_destructor_~WrapsB` here,parameter `this` of WrapsB::__infer_inner_destructor_~WrapsB,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `getwrapperHeap`,passed as argument to `WrapsB::WrapsB`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `WrapsB::WrapsB`,passed as argument to `ReferenceWrapperHeap::ReferenceWrapperHeap`,parameter `a` of ReferenceWrapperHeap::ReferenceWrapperHeap,passed as argument to `WrapsB::getb`,return from call to `WrapsB::getb`,assigned,return from call to `ReferenceWrapperHeap::ReferenceWrapperHeap`,return from call to `getwrapperHeap`,invalid access occurs here] @@ -133,7 +129,6 @@ codetoanalyze/cpp/pulse/use_after_free.cpp, trigger_assumed_aliasing3_bad, 0, US codetoanalyze/cpp/pulse/use_after_free.cpp, trigger_assumed_aliasing_bad, 0, USE_AFTER_FREE, no_bucket, ERROR, [calling context starts here,in call to `assumed_aliasing_latent`,invalidation part of the trace starts here,parameter `x` of assumed_aliasing_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `y` of assumed_aliasing_latent,invalid access occurs here] 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_int_over_cap_ok, 13, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/values.cpp, FP_ints_are_not_rationals_ok, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,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] diff --git a/infer/tests/codetoanalyze/cpp/pulse/optional.cpp b/infer/tests/codetoanalyze/cpp/pulse/optional.cpp index 956d526d9..fd64fb62a 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/optional.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/optional.cpp @@ -184,9 +184,9 @@ int value_or_check_empty_ok() { return -1; } -// missing a more precise model for -// constructing an optional from a value -int value_or_check_value_ok_FP() { +// missing a more precise model for constructing an optional from a +// value, which could cause an FP but doesn't at the moment +int value_or_check_value_ok() { folly::Optional foo{5}; int x = foo.value_or(0); if (x != 5) { @@ -295,7 +295,7 @@ void std_emplace(std::optional state) { auto pos = state->vec.begin(); } -void std_operator_arrow_bad() { std_emplace(std::nullopt); } +void FN_std_operator_arrow_bad() { std_emplace(std::nullopt); } int std_value_or_check_empty_ok() { std::optional foo{std::nullopt}; @@ -305,7 +305,7 @@ int std_value_or_check_empty_ok() { return -1; } -int std_value_or_check_value_ok_FP() { +int std_value_or_check_value_ok() { std::optional foo{5}; int x = foo.value_or(0); if (x != 5) { @@ -372,7 +372,7 @@ E getEnum() { return E::OP2; } -std::optional cannot_be_empty_FP() { +std::optional cannot_be_empty() { if (getEnum() == E::OP1) { return getOptionalValue().value(); } @@ -399,7 +399,7 @@ struct Node { } }; -int smart_pointer_FP(const Node& node) { +int smart_pointer(const Node& node) { if (node.getShared().has_value()) { return *(node.getShared().value()); } diff --git a/infer/tests/codetoanalyze/cpp/pulse/values.cpp b/infer/tests/codetoanalyze/cpp/pulse/values.cpp index 5d428749a..68bba2b8d 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/values.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/values.cpp @@ -116,8 +116,9 @@ void function_empty_range_interproc_ok() { find_first_non_space(x); } -// arithmetic on integers does not wrap around but ignores too-large values -void FP_int_over_cap_ok() { +// arithmetic on integers does not wrap around but ignores too-large +// values. However, somehow the FP is gone for other reasons. +void int_over_cap_ok() { unsigned long one = 1; // 2^(63+63+3) + 2*2^(63+3) + 1*8 = 2^129 + 2^67 + 8 = 8 mod 2^64 // this is convoluted to escape various simplifications from Z that would @@ -169,3 +170,10 @@ void shift_by_too_much_ok(int x) { *p = 42; } } + +void interproc_mult_ok(int v, int w) { + if (mult(32, 52) != 1664 || mult(10, v) != 10 * v || mult(v, w) != v * w) { + int* p = nullptr; + *p = 42; + } +}