[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
master
Jules Villard 4 years ago committed by Facebook GitHub Bot
parent 5a363c9b07
commit e549103d75

@ -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 =

@ -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=x1=y && true (no atoms), pruned=true (no atoms),
both=x=v6 && x = 0 y = 1 && 0=x1=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=v70=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=v70=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=v70=v83=v7=w12=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=v70=v83=v7=w12=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 )

@ -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]

@ -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,

@ -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<int>::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<int>::operator=`,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),return from call to `folly::Optional<int>::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<int>::operator=`,parameter `other` of folly::Optional<int>::operator=,passed as argument to `folly::Optional::assign(folly::Optional<Value> arg)` (modelled),return from call to `folly::Optional::assign(folly::Optional<Value> arg)` (modelled),return from call to `folly::Optional<int>::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<Value> arg)` (modelled),return from call to `folly::Optional::Optional(folly::Optional<Value> 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<Value> arg)` (modelled),return from call to `std::optional::operator=(std::optional<Value> 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<Value> arg)` (modelled),return from call to `std::optional::optional(std::optional<Value> 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<int>::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<int>::operator=`,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),return from call to `folly::Optional<int>::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]

@ -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<int> foo{5};
int x = foo.value_or(0);
if (x != 5) {
@ -295,7 +295,7 @@ void std_emplace(std::optional<State> 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<int> 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<int> foo{5};
int x = foo.value_or(0);
if (x != 5) {
@ -372,7 +372,7 @@ E getEnum() {
return E::OP2;
}
std::optional<std::string> cannot_be_empty_FP() {
std::optional<std::string> 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());
}

@ -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;
}
}

Loading…
Cancel
Save