pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[pulse] check that new arithmetic facts are consistent with the heap

Browse Source 
Summary:
Communicate new facts from the arithmetic domain to the memory domain to
detect contradictions between the two.

Reviewed By: jberdine

Differential Revision: D24832079

fbshipit-source-id: 2caf8e9af
master
Jules Villard 4 years ago committed by Facebook GitHub Bot
parent 47e9f8ffec
commit 578583f2ab
11 changed files with 277 additions and 157 deletions
Show Stats Download Patch File Download Diff File

38
infer/src/pulse/PulseAbductiveDomain.ml
Unescape View File

@ -431,11 +431,47 @@ let invalidate_locals pdesc astate : t =
type summary = t [@@deriving yojson_of] type summary = t [@@deriving yojson_of]
let is_allocated {post; pre} v =
let is_heap_allocated base_mem v =
BaseMemory.find_opt v base_mem.heap
|> Option.exists ~f:(fun edges -> not (BaseMemory.Edges.is_empty edges))
in
let is_pvar = function Var.ProgramVar _ -> true | Var.LogicalVar _ -> false in
let is_stack_allocated base_mem v =
BaseStack.exists
(fun var (address, _) -> is_pvar var && AbstractValue.equal address v)
base_mem.stack
in
(* OPTIM: the post stack contains at least the pre stack so no need to check both *)
is_heap_allocated (post :> BaseDomain.t) v
|| is_heap_allocated (pre :> BaseDomain.t) v
|| is_stack_allocated (post :> BaseDomain.t) v
let incorporate_new_eqs astate (phi, new_eqs) =
List.fold_until new_eqs ~init:phi ~finish:Fn.id ~f:(fun phi (new_eq : PulseFormula.new_eq) ->
match new_eq with
| EqZero v when is_allocated astate v ->
L.d_printfln "CONTRADICTION: %a = 0 but is allocated" AbstractValue.pp v ;
Stop PathCondition.false_
| Equal (v1, v2)
when (not (AbstractValue.equal v1 v2)) && is_allocated astate v1 && is_allocated astate v2
->
L.d_printfln "CONTRADICTION: %a = %a but both are separately allocated" AbstractValue.pp
v1 AbstractValue.pp v2 ;
Stop PathCondition.false_
| _ ->
Continue phi )
let summary_of_post pdesc astate = let summary_of_post pdesc astate =
let astate = filter_for_summary astate in let astate = filter_for_summary astate in
let astate, live_addresses, _ = discard_unreachable astate in let astate, live_addresses, _ = discard_unreachable astate in
let astate = let astate =
{astate with path_condition= PathCondition.simplify ~keep:live_addresses astate.path_condition} { astate with
path_condition=
PathCondition.simplify ~keep:live_addresses astate.path_condition
|> incorporate_new_eqs astate }
in in
invalidate_locals pdesc astate invalidate_locals pdesc astate

6
infer/src/pulse/PulseAbductiveDomain.mli
Unescape View File

@ -172,3 +172,9 @@ val set_post_edges : AbstractValue.t -> BaseMemory.Edges.t -> t -> t
val set_post_cell : AbstractValue.t * ValueHistory.t -> BaseDomain.cell -> Location.t -> t -> t val set_post_cell : AbstractValue.t * ValueHistory.t -> BaseDomain.cell -> Location.t -> t -> t
(** directly set the edges and attributes for the given address, bypassing abduction altogether *) (** directly set the edges and attributes for the given address, bypassing abduction altogether *)
val incorporate_new_eqs : t -> PathCondition.t * PathCondition.new_eqs -> PathCondition.t
(** Check that the new equalities discovered are compatible with the current pre and post heaps,
e.g. [x = 0] is not compatible with [x] being allocated, and [x = y] is not compatible with [x]
and [y] being allocated separately. In those cases, the resulting path condition is
{!PathCondition.false_}. *)

10
infer/src/pulse/PulseArithmetic.ml
Unescape View File

@ -10,7 +10,9 @@ open PulseBasicInterface
module AbductiveDomain = PulseAbductiveDomain module AbductiveDomain = PulseAbductiveDomain
let map_path_condition ~f astate = let map_path_condition ~f astate =
AbductiveDomain.set_path_condition (f astate.AbductiveDomain.path_condition) astate AbductiveDomain.set_path_condition
(f astate.AbductiveDomain.path_condition |> AbductiveDomain.incorporate_new_eqs astate)
astate
let and_nonnegative v astate = let and_nonnegative v astate =
@ -41,6 +43,7 @@ let eval_unop unop_addr unop addr astate =
let prune_binop ~negated bop lhs_op rhs_op astate = let prune_binop ~negated bop lhs_op rhs_op astate =
let phi' = let phi' =
PathCondition.prune_binop ~negated bop lhs_op rhs_op astate.AbductiveDomain.path_condition PathCondition.prune_binop ~negated bop lhs_op rhs_op astate.AbductiveDomain.path_condition
|> AbductiveDomain.incorporate_new_eqs astate
in in
AbductiveDomain.set_path_condition phi' astate AbductiveDomain.set_path_condition phi' astate
@ -50,7 +53,10 @@ let is_known_zero astate v = PathCondition.is_known_zero astate.AbductiveDomain.
let is_unsat_cheap astate = PathCondition.is_unsat_cheap astate.AbductiveDomain.path_condition let is_unsat_cheap astate = PathCondition.is_unsat_cheap astate.AbductiveDomain.path_condition
let is_unsat_expensive astate = let is_unsat_expensive astate =
let phi', is_unsat = PathCondition.is_unsat_expensive astate.AbductiveDomain.path_condition in let phi', is_unsat, new_eqs =
PathCondition.is_unsat_expensive astate.AbductiveDomain.path_condition
in
let phi' = AbductiveDomain.incorporate_new_eqs astate (phi', new_eqs) in
(AbductiveDomain.set_path_condition phi' astate, is_unsat) (AbductiveDomain.set_path_condition phi' astate, is_unsat)

177
infer/src/pulse/PulseFormula.ml
Unescape View File

@ -980,6 +980,10 @@ module VarUF =
end) end)
(Var.Set) (Var.Set)
type new_eq = EqZero of Var.t | Equal of Var.t * Var.t
type new_eqs = new_eq list
module Formula = struct module Formula = struct
(* redefined for yojson output *) (* redefined for yojson output *)
type var_eqs = VarUF.t type var_eqs = VarUF.t
@ -1021,15 +1025,15 @@ module Formula = struct
(** module that breaks invariants more often that the rest, with an interface that is safer to use *) (** module that breaks invariants more often that the rest, with an interface that is safer to use *)
module Normalizer : sig module Normalizer : sig
val and_var_linarith : Var.t -> LinArith.t -> t -> t normalized val and_var_linarith : Var.t -> LinArith.t -> t * new_eqs -> (t * new_eqs) normalized
val and_var_var : Var.t -> Var.t -> t -> t normalized val and_var_var : Var.t -> Var.t -> t * new_eqs -> (t * new_eqs) normalized
val and_atom : Atom.t -> t -> t normalized val and_atom : Atom.t -> t * new_eqs -> (t * new_eqs) normalized
val normalize_atom : t -> Atom.t -> Atom.t option normalized val normalize_atom : t -> Atom.t -> Atom.t option normalized
val normalize : t -> t normalized val normalize : t -> (t * new_eqs) normalized
val implies_atom : t -> Atom.t -> bool val implies_atom : t -> Atom.t -> bool
end = struct end = struct
@ -1075,44 +1079,53 @@ module Formula = struct
LinSubst l' ) LinSubst l' )
let rec solve_normalized_eq ~fuel l1 l2 phi = 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 ->
EqZero v :: new_eqs
| _ ->
new_eqs
let rec solve_normalized_eq ~fuel new_eqs l1 l2 phi =
LinArith.solve_eq l1 l2 LinArith.solve_eq l1 l2
>>= function >>= function
| None -> | None ->
Sat phi Sat (phi, [])
| Some (v, l) -> ( | Some (v, l) -> (
match LinArith.get_as_var l with match LinArith.get_as_var l with
| Some v' -> | Some v' ->
merge_vars ~fuel (v :> Var.t) v' phi merge_vars ~fuel new_eqs (v :> Var.t) v' phi
| None -> ( | None -> (
match Var.Map.find_opt (v :> Var.t) phi.linear_eqs with match Var.Map.find_opt (v :> Var.t) phi.linear_eqs with
| None -> | None ->
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 (* 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] *) [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} Sat ({phi with linear_eqs= Var.Map.add (v :> Var.t) l phi.linear_eqs}, new_eqs)
| Some l' -> | Some l' ->
(* This is the only step that consumes fuel: discovering an equality [l = l']: because we (* This is the only step that consumes fuel: discovering an equality [l = l']: because we
do not record these anywhere (except when there consequence can be recorded as [y = do not record these anywhere (except when their consequence can be recorded as [y =
l''] or [y = y'], we could potentially discover the same equality over and over and l''] or [y = y'], we could potentially discover the same equality over and over and
diverge otherwise. Or could we? *) diverge otherwise. Or could we? *)
(* [l'] is possibly not normalized w.r.t. the current [phi] so take this opportunity to (* [l'] is possibly not normalized w.r.t. the current [phi] so take this opportunity to
normalize it *) normalize it *)
if fuel > 0 then ( if fuel > 0 then (
L.d_printfln "Consuming fuel solving linear equality (from %d)" fuel ; L.d_printfln "Consuming fuel solving linear equality (from %d)" fuel ;
solve_normalized_eq ~fuel:(fuel - 1) l (apply phi l') phi ) solve_normalized_eq ~fuel:(fuel - 1) new_eqs l (apply phi l') phi )
else ( else (
(* [fuel = 0]: give up simplifying further for fear of diverging *) (* [fuel = 0]: give up simplifying further for fear of diverging *)
L.d_printfln "Ran out of fuel solving linear equality" ; L.d_printfln "Ran out of fuel solving linear equality" ;
Sat phi ) ) ) Sat (phi, new_eqs) ) ) )
and merge_vars ~fuel v1 v2 phi = and merge_vars ~fuel new_eqs v1 v2 phi =
let var_eqs, subst_opt = VarUF.union phi.var_eqs v1 v2 in let var_eqs, subst_opt = VarUF.union phi.var_eqs v1 v2 in
let phi = {phi with var_eqs} in let phi = {phi with var_eqs} in
match subst_opt with match subst_opt with
| None -> | None ->
(* we already knew the equality *) (* we already knew the equality *)
Sat phi Sat (phi, new_eqs)
| Some (v_old, v_new) -> ( | Some (v_old, v_new) -> (
(* new equality [v_old = v_new]: we need to update a potential [v_old = l] to be [v_new = (* new equality [v_old = v_new]: we need to update a potential [v_old = l] to be [v_new =
l], and if [v_new = l'] was known we need to also explore the consequences of [l = l'] *) l], and if [v_new = l'] was known we need to also explore the consequences of [l = l'] *)
@ -1123,6 +1136,7 @@ module Formula = struct
normalization steps: when the stronger invariant holds we can normalize in one step (in normalization steps: when the stronger invariant holds we can normalize in one step (in
[normalize_linear_eqs]). *) [normalize_linear_eqs]). *)
let v_new = (v_new :> Var.t) in let v_new = (v_new :> Var.t) in
let new_eqs = Equal (v_old, v_new) :: new_eqs in
let phi, l_new = let phi, l_new =
match Var.Map.find_opt v_new phi.linear_eqs with match Var.Map.find_opt v_new phi.linear_eqs with
| None -> | None ->
@ -1146,46 +1160,47 @@ module Formula = struct
in in
match (l_old, l_new) with match (l_old, l_new) with
| None, None | None, Some _ -> | None, None | None, Some _ ->
Sat phi Sat (phi, new_eqs)
| Some l, None -> | Some l, None ->
Sat {phi with linear_eqs= Var.Map.add v_new l phi.linear_eqs} let new_eqs = add_lin_eq_to_new_eqs v_new l new_eqs in
Sat ({phi with linear_eqs= Var.Map.add v_new l phi.linear_eqs}, new_eqs)
| Some l1, Some l2 -> | Some l1, Some l2 ->
(* no need to consume fuel here as we can only go through this branch finitely many (* no need to consume fuel here as we can only go through this branch finitely many
times because there are finitely many variables in a given formula *) times because there are finitely many variables in a given formula *)
(* TODO: we may want to keep the "simpler" representative for [v_new] between [l1] and [l2] *) (* TODO: we may want to keep the "simpler" representative for [v_new] between [l1] and [l2] *)
solve_normalized_eq ~fuel l1 l2 phi ) solve_normalized_eq ~fuel new_eqs l1 l2 phi )
(** an arbitrary value *) (** an arbitrary value *)
let base_fuel = 5 let base_fuel = 5
let solve_eq t1 t2 phi = solve_normalized_eq ~fuel:base_fuel (apply phi t1) (apply phi t2) phi let solve_eq new_eqs t1 t2 phi =
solve_normalized_eq ~fuel:base_fuel new_eqs (apply phi t1) (apply phi t2) phi
let and_var_linarith v l phi = solve_eq l (LinArith.of_var v) phi
let and_var_var v1 v2 phi = merge_vars ~fuel:base_fuel v1 v2 phi let and_var_linarith v l (phi, new_eqs) = solve_eq new_eqs l (LinArith.of_var v) phi
let rec normalize_linear_eqs ~fuel phi0 = let rec normalize_linear_eqs ~fuel (phi0, new_eqs) =
let* changed, phi' = let* changed, phi_new_eqs' =
(* reconstruct the relation from scratch *) (* reconstruct the relation from scratch *)
Var.Map.fold Var.Map.fold
(fun v l acc -> (fun v l acc ->
let* changed, phi = acc in let* changed, phi_new_eqs = acc in
let l' = apply phi0 l in let l' = apply phi0 l in
let+ phi' = and_var_linarith v l' phi in let+ phi_new_eqs' = and_var_linarith v l' phi_new_eqs in
(changed || not (phys_equal l l'), phi') ) (changed || not (phys_equal l l'), phi_new_eqs') )
phi0.linear_eqs phi0.linear_eqs
(Sat (false, {phi0 with linear_eqs= Var.Map.empty})) (Sat (false, ({phi0 with linear_eqs= Var.Map.empty}, new_eqs)))
in in
if changed then if changed then
if fuel > 0 then ( if fuel > 0 then (
(* do another pass if we can afford it *) (* do another pass if we can afford it *)
L.d_printfln "consuming fuel normalizing linear equalities (from %d)" fuel ; L.d_printfln "consuming fuel normalizing linear equalities (from %d)" fuel ;
normalize_linear_eqs ~fuel:(fuel - 1) phi' ) normalize_linear_eqs ~fuel:(fuel - 1) phi_new_eqs' )
else ( else (
L.d_printfln "ran out of fuel normalizing linear equalities" ; L.d_printfln "ran out of fuel normalizing linear equalities" ;
Sat phi' ) Sat phi_new_eqs' )
else Sat phi0 else Sat (phi0, new_eqs)
let normalize_atom phi (atom : Atom.t) = let normalize_atom phi (atom : Atom.t) =
@ -1204,54 +1219,60 @@ module Formula = struct
(** return [(new_linear_equalities, phi ∧ atom)], where [new_linear_equalities] is [true] if (** return [(new_linear_equalities, phi ∧ atom)], where [new_linear_equalities] is [true] if
[phi.linear_eqs] was changed as a result *) [phi.linear_eqs] was changed as a result *)
let and_atom atom phi = let and_atom atom (phi, new_eqs) =
normalize_atom phi atom normalize_atom phi atom
>>= function >>= function
| None -> | None ->
Sat (false, phi) Sat (false, (phi, new_eqs))
| Some (Atom.Equal (Linear l, Const c)) | Some (Atom.Equal (Const c, Linear l)) -> | 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 (* 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 they end up only on one side, hence only this match case is needed to detect linear
equalities *) equalities *)
let+ phi' = solve_eq l (LinArith.of_q c) phi in let+ phi', new_eqs = solve_eq new_eqs l (LinArith.of_q c) phi in
(true, phi') (true, (phi', new_eqs))
| Some atom' -> | Some atom' ->
Sat (false, {phi with atoms= Atom.Set.add atom' phi.atoms}) Sat (false, ({phi with atoms= Atom.Set.add atom' phi.atoms}, new_eqs))
let normalize_atoms phi = let normalize_atoms (phi, new_eqs) =
let atoms0 = phi.atoms in let atoms0 = phi.atoms in
let init = Sat (false, {phi with atoms= Atom.Set.empty}) in let init = Sat (false, ({phi with atoms= Atom.Set.empty}, new_eqs)) in
IContainer.fold_of_pervasives_set_fold Atom.Set.fold atoms0 ~init ~f:(fun acc atom -> IContainer.fold_of_pervasives_set_fold Atom.Set.fold atoms0 ~init ~f:(fun acc atom ->
let* changed, phi = acc in let* changed, phi_new_eqs = acc in
let+ changed', phi = and_atom atom phi in let+ changed', phi_new_eqs = and_atom atom phi_new_eqs in
(changed || changed', phi) ) (changed || changed', phi_new_eqs) )
(* interface *)
let normalize phi = let normalize phi0 =
(* NOTE: we may consume a quadratic amount of [fuel] here since the fuel here is not consumed by (* NOTE: we may consume a quadratic amount of [fuel] here since the fuel here is not consumed by
[normalize_linear_eqs] (i.e. [normalize_linear_eqs] does not return the remaining [normalize_linear_eqs] (i.e. [normalize_linear_eqs] does not return the remaining
fuel). That's ok because there's not much fuel to begin with, and as long as we're making fuel). That's ok because there's not much fuel to begin with, and as long as we're making
progress it's probably worth it anyway. *) progress it's probably worth it anyway. *)
let rec normalize_with_fuel ~fuel phi = let rec normalize_with_fuel ~fuel phi_new_eqs =
if fuel <= 0 then ( if fuel <= 0 then (
L.d_printfln "ran out of fuel when normalizing" ; L.d_printfln "ran out of fuel when normalizing" ;
Sat phi ) Sat phi_new_eqs )
else else
let* new_linear_eqs, phi = normalize_linear_eqs ~fuel phi >>= normalize_atoms in let* new_linear_eqs, phi_new_eqs' =
normalize_linear_eqs ~fuel phi_new_eqs >>= normalize_atoms
in
if new_linear_eqs then ( if new_linear_eqs then (
L.d_printfln "new linear equalities, consuming fuel (from %d)" fuel ; L.d_printfln "new linear equalities, consuming fuel (from %d)" fuel ;
normalize_with_fuel ~fuel:(fuel - 1) phi ) normalize_with_fuel ~fuel:(fuel - 1) phi_new_eqs' )
else Sat phi else Sat phi_new_eqs'
in in
normalize_with_fuel ~fuel:base_fuel phi normalize_with_fuel ~fuel:base_fuel (phi0, [])
let and_atom atom phi_new_eqs = and_atom atom phi_new_eqs >>| snd
let and_atom atom phi = and_atom atom phi >>| snd let and_var_var v1 v2 (phi, new_eqs) = merge_vars ~fuel:base_fuel new_eqs v1 v2 phi
let implies_atom phi atom = let implies_atom phi atom =
(* [φ ⊢ a] iff [φ ∧ ¬a] is inconsistent *) (* [φ ⊢ a] iff [φ ∧ ¬a] is inconsistent *)
match and_atom (Atom.nnot atom) phi with Sat _ -> false | Unsat -> true match and_atom (Atom.nnot atom) (phi, []) with Sat _ -> false | Unsat -> true
end end
end end
@ -1276,9 +1297,9 @@ let pp = pp_with_pp_var Var.pp
let and_known_atom atom phi = let and_known_atom atom phi =
let open SatUnsatMonad in let open SatUnsatMonad in
let* known = Formula.Normalizer.and_atom atom phi.known in let* known, _ = Formula.Normalizer.and_atom atom (phi.known, []) in
let+ both = Formula.Normalizer.and_atom atom phi.both in let+ both, new_eqs = Formula.Normalizer.and_atom atom (phi.both, []) in
{phi with known; both} ({phi with known; both}, new_eqs)
let and_mk_atom mk_atom op1 op2 phi = let and_mk_atom mk_atom op1 op2 phi =
@ -1306,7 +1327,7 @@ let prune_binop ~negated (bop : Binop.t) x y phi =
let ty = Term.of_operand y in let ty = Term.of_operand y in
let t = Term.of_binop bop tx ty in let t = Term.of_binop bop tx ty in
let atom = if negated then Atom.Equal (t, Term.zero) else Atom.NotEqual (t, Term.zero) in let atom = if negated then Atom.Equal (t, Term.zero) else Atom.NotEqual (t, Term.zero) in
let* both = Formula.Normalizer.and_atom atom phi.both in let* both, new_eqs = Formula.Normalizer.and_atom atom (phi.both, []) in
let+ pruned = let+ pruned =
(* Use [both] to normalize [atom] here to take previous [prune]s into account. This shouldn't (* Use [both] to normalize [atom] here to take previous [prune]s into account. This shouldn't
change whether [known |- pruned] overall, which is what we'll want to ultimately check in change whether [known |- pruned] overall, which is what we'll want to ultimately check in
@ -1314,13 +1335,13 @@ let prune_binop ~negated (bop : Binop.t) x y phi =
Formula.Normalizer.normalize_atom phi.both atom Formula.Normalizer.normalize_atom phi.both atom
>>| Option.fold ~init:phi.pruned ~f:(fun pruned atom -> Atom.Set.add atom pruned) >>| Option.fold ~init:phi.pruned ~f:(fun pruned atom -> Atom.Set.add atom pruned)
in in
{phi with pruned; both} ({phi with pruned; both}, new_eqs)
let normalize phi = let normalize phi =
let open SatUnsatMonad in let open SatUnsatMonad in
let* both = Formula.Normalizer.normalize phi.both in let* both, new_eqs = Formula.Normalizer.normalize phi.both in
let* known = Formula.Normalizer.normalize phi.known in let* known, _ = Formula.Normalizer.normalize phi.known in
let+ pruned = let+ pruned =
Atom.Set.fold Atom.Set.fold
(fun atom pruned_sat -> (fun atom pruned_sat ->
@ -1334,7 +1355,7 @@ let normalize phi =
Sat (Atom.Set.add atom pruned) ) Sat (Atom.Set.add atom pruned) )
phi.pruned (Sat Atom.Set.empty) phi.pruned (Sat Atom.Set.empty)
in in
{both; known; pruned} ({both; known; pruned}, new_eqs)
(** translate each variable in [phi_foreign] according to [f] then incorporate each fact into [phi0] *) (** translate each variable in [phi_foreign] according to [f] then incorporate each fact into [phi0] *)
@ -1348,42 +1369,42 @@ let and_fold_subst_variables phi0 ~up_to_f:phi_foreign ~init ~f:f_var =
let sat_value_exn (norm : 'a normalized) = let sat_value_exn (norm : 'a normalized) =
match norm with Unsat -> raise Contradiction | Sat x -> x match norm with Unsat -> raise Contradiction | Sat x -> x
in in
let and_var_eqs var_eqs_foreign acc_phi = let and_var_eqs var_eqs_foreign acc_phi_new_eqs =
VarUF.fold_congruences var_eqs_foreign ~init:acc_phi VarUF.fold_congruences var_eqs_foreign ~init:acc_phi_new_eqs
~f:(fun (acc_f, phi) (repr_foreign, vs_foreign) -> ~f:(fun (acc_f, phi_new_eqs) (repr_foreign, vs_foreign) ->
let acc_f, repr = f_var acc_f (repr_foreign :> Var.t) in let acc_f, repr = f_var acc_f (repr_foreign :> Var.t) in
IContainer.fold_of_pervasives_set_fold Var.Set.fold vs_foreign ~init:(acc_f, phi) IContainer.fold_of_pervasives_set_fold Var.Set.fold vs_foreign ~init:(acc_f, phi_new_eqs)
~f:(fun (acc_f, phi) v_foreign -> ~f:(fun (acc_f, phi_new_eqs) v_foreign ->
let acc_f, v = f_var acc_f v_foreign in let acc_f, v = f_var acc_f v_foreign in
let phi = Formula.Normalizer.and_var_var repr v phi |> sat_value_exn in let phi_new_eqs = Formula.Normalizer.and_var_var repr v phi_new_eqs |> sat_value_exn in
(acc_f, phi) ) ) (acc_f, phi_new_eqs) ) )
in in
let and_linear_eqs linear_eqs_foreign acc_phi = let and_linear_eqs linear_eqs_foreign acc_phi_new_eqs =
IContainer.fold_of_pervasives_map_fold Var.Map.fold linear_eqs_foreign ~init:acc_phi IContainer.fold_of_pervasives_map_fold Var.Map.fold linear_eqs_foreign ~init:acc_phi_new_eqs
~f:(fun (acc_f, phi) (v_foreign, l_foreign) -> ~f:(fun (acc_f, phi_new_eqs) (v_foreign, l_foreign) ->
let acc_f, v = f_var acc_f v_foreign in let acc_f, v = f_var acc_f v_foreign in
let acc_f, l = LinArith.fold_subst_variables l_foreign ~init:acc_f ~f:f_subst in let acc_f, l = LinArith.fold_subst_variables l_foreign ~init:acc_f ~f:f_subst in
let phi = Formula.Normalizer.and_var_linarith v l phi |> sat_value_exn in let phi_new_eqs = Formula.Normalizer.and_var_linarith v l phi_new_eqs |> sat_value_exn in
(acc_f, phi) ) (acc_f, phi_new_eqs) )
in in
let and_atoms atoms_foreign acc_phi = let and_atoms atoms_foreign acc_phi_new_eqs =
IContainer.fold_of_pervasives_set_fold Atom.Set.fold atoms_foreign ~init:acc_phi IContainer.fold_of_pervasives_set_fold Atom.Set.fold atoms_foreign ~init:acc_phi_new_eqs
~f:(fun (acc_f, phi) atom_foreign -> ~f:(fun (acc_f, phi_new_eqs) atom_foreign ->
let acc_f, atom = Atom.fold_subst_variables atom_foreign ~init:acc_f ~f:f_subst in let acc_f, atom = Atom.fold_subst_variables atom_foreign ~init:acc_f ~f:f_subst in
let phi = Formula.Normalizer.and_atom atom phi |> sat_value_exn in let phi_new_eqs = Formula.Normalizer.and_atom atom phi_new_eqs |> sat_value_exn in
(acc_f, phi) ) (acc_f, phi_new_eqs) )
in in
let and_ phi_foreign acc phi = let and_ phi_foreign acc phi =
try try
Sat Sat
( and_var_eqs phi_foreign.Formula.var_eqs (acc, phi) ( and_var_eqs phi_foreign.Formula.var_eqs (acc, (phi, []))
|> and_linear_eqs phi_foreign.Formula.linear_eqs |> and_linear_eqs phi_foreign.Formula.linear_eqs
|> and_atoms phi_foreign.Formula.atoms ) |> and_atoms phi_foreign.Formula.atoms )
with Contradiction -> Unsat with Contradiction -> Unsat
in in
let open SatUnsatMonad in let open SatUnsatMonad in
let* acc, both = and_ phi_foreign.both init phi0.both in let* acc, (both, new_eqs) = and_ phi_foreign.both init phi0.both in
let* acc, known = and_ phi_foreign.known acc phi0.known in let* acc, (known, _) = and_ phi_foreign.known acc phi0.known in
let and_pruned pruned_foreign acc_pruned = let and_pruned pruned_foreign acc_pruned =
IContainer.fold_of_pervasives_set_fold Atom.Set.fold pruned_foreign ~init:acc_pruned IContainer.fold_of_pervasives_set_fold Atom.Set.fold pruned_foreign ~init:acc_pruned
~f:(fun (acc_f, pruned) atom_foreign -> ~f:(fun (acc_f, pruned) atom_foreign ->
@ -1397,7 +1418,7 @@ let and_fold_subst_variables phi0 ~up_to_f:phi_foreign ~init ~f:f_var =
let+ acc, pruned = let+ acc, pruned =
try Sat (and_pruned phi_foreign.pruned (acc, phi0.pruned)) with Contradiction -> Unsat try Sat (and_pruned phi_foreign.pruned (acc, phi0.pruned)) with Contradiction -> Unsat
in in
(acc, {known; pruned; both}) (acc, {known; pruned; both}, new_eqs)
(** Intermediate step of [simplify]: build an (undirected) graph between variables where an edge (** Intermediate step of [simplify]: build an (undirected) graph between variables where an edge
@ -1480,7 +1501,7 @@ let get_reachable_from graph vs =
let simplify ~keep phi = let simplify ~keep phi =
let open SatUnsatMonad in let open SatUnsatMonad in
let+ phi = normalize phi in let+ phi, new_eqs = normalize 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 atoms when they contain only variables that do not appear in atoms mentioning (* Get rid of atoms when they contain only variables that do not appear in atoms mentioning
variables in [keep], or variables appearing in atoms together with variables in [keep], and variables in [keep], or variables appearing in atoms together with variables in [keep], and
@ -1510,7 +1531,7 @@ let simplify ~keep phi =
let known = simplify_phi phi.known in let known = simplify_phi phi.known in
let both = simplify_phi phi.both in let both = simplify_phi phi.both in
let pruned = Atom.Set.filter filter_atom phi.pruned in let pruned = Atom.Set.filter filter_atom phi.pruned in
{known; pruned; both} ({known; pruned; both}, new_eqs)
let is_known_zero phi v = let is_known_zero phi v =

28
infer/src/pulse/PulseFormula.mli
Unescape View File

@ -30,29 +30,39 @@ type operand = LiteralOperand of IntLit.t | AbstractValueOperand of Var.t
(** {3 Build formulas} *) (** {3 Build formulas} *)
(** some operations will return a set of new facts discovered that are relevant to communicate to
the memory domain *)
type new_eq = EqZero of Var.t | Equal of Var.t * Var.t
type new_eqs = new_eq list
val ttrue : t val ttrue : t
val and_equal : operand -> operand -> t -> t normalized val and_equal : operand -> operand -> t -> (t * new_eqs) normalized
val and_less_equal : operand -> operand -> t -> t normalized val and_less_equal : operand -> operand -> t -> (t * new_eqs) normalized
val and_less_than : operand -> operand -> t -> t normalized val and_less_than : operand -> operand -> t -> (t * new_eqs) normalized
val and_equal_unop : Var.t -> Unop.t -> operand -> t -> t normalized val and_equal_unop : Var.t -> Unop.t -> operand -> t -> (t * new_eqs) normalized
val and_equal_binop : Var.t -> Binop.t -> operand -> operand -> t -> t normalized val and_equal_binop : Var.t -> Binop.t -> operand -> operand -> t -> (t * new_eqs) normalized
val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> t normalized val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> (t * new_eqs) normalized
(** {3 Operations} *) (** {3 Operations} *)
val normalize : t -> t normalized val normalize : t -> (t * new_eqs) normalized
(** think a bit harder about the formula *) (** think a bit harder about the formula *)
val simplify : keep:Var.Set.t -> t -> t normalized val simplify : keep:Var.Set.t -> t -> (t * new_eqs) normalized
val and_fold_subst_variables : val and_fold_subst_variables :
t -> up_to_f:t -> init:'acc -> f:('acc -> Var.t -> 'acc * Var.t) -> ('acc * t) normalized t
-> up_to_f:t
-> init:'acc
-> f:('acc -> Var.t -> 'acc * Var.t)
-> ('acc * t * new_eqs) normalized
val is_known_zero : t -> Var.t -> bool val is_known_zero : t -> Var.t -> bool

5
infer/src/pulse/PulseInterproc.ml
Unescape View File

@ -221,10 +221,13 @@ let conjoin_callee_arith pre_post call_state =
pre_post.AbductiveDomain.path_condition pre_post.AbductiveDomain.path_condition
(AddressMap.pp ~pp_value:(fun fmt (addr, _) -> AbstractValue.pp fmt addr)) (AddressMap.pp ~pp_value:(fun fmt (addr, _) -> AbstractValue.pp fmt addr))
call_state.subst ; call_state.subst ;
let subst, path_condition = let subst, path_condition, new_eqs =
PathCondition.and_callee call_state.subst call_state.astate.path_condition PathCondition.and_callee call_state.subst call_state.astate.path_condition
~callee:pre_post.AbductiveDomain.path_condition ~callee:pre_post.AbductiveDomain.path_condition
in in
let path_condition =
AbductiveDomain.incorporate_new_eqs call_state.astate (path_condition, new_eqs)
in
if PathCondition.is_unsat_cheap path_condition then raise (Contradiction PathCondition) if PathCondition.is_unsat_cheap path_condition then raise (Contradiction PathCondition)
else else
let astate = AbductiveDomain.set_path_condition path_condition call_state.astate in let astate = AbductiveDomain.set_path_condition path_condition call_state.astate in

107
infer/src/pulse/PulsePathCondition.ml
Unescape View File

@ -45,53 +45,61 @@ let true_ = {is_unsat= false; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula
let false_ = {is_unsat= true; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue} let false_ = {is_unsat= true; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue}
let map_sat phi f = if phi.is_unsat then phi else f phi type new_eqs = PulseFormula.new_eqs
let map_sat phi f = if phi.is_unsat then (phi, []) else f phi
let ( let+ ) phi f = map_sat phi f let ( let+ ) phi f = map_sat phi f
let map_formula_sat (x : 'a Formula.normalized) f = match x with Unsat -> false_ | Sat x' -> f x' let map_formula_sat (x : 'a Formula.normalized) f =
match x with Unsat -> (false_, []) | Sat x' -> f x'
let ( let+| ) x f = map_formula_sat x f let ( let+| ) x f = map_formula_sat x f
let and_nonnegative v phi = let and_nonnegative v phi =
let+ {is_unsat; bo_itvs; citvs; formula} = phi in let+ {is_unsat; bo_itvs; citvs; formula} = phi in
let+| formula = let+| formula, new_eqs =
Formula.and_less_equal (LiteralOperand IntLit.zero) (AbstractValueOperand v) formula Formula.and_less_equal (LiteralOperand IntLit.zero) (AbstractValueOperand v) formula
in in
{ is_unsat ( { is_unsat
; bo_itvs= BoItvs.add v Itv.ItvPure.nat bo_itvs ; bo_itvs= BoItvs.add v Itv.ItvPure.nat bo_itvs
; citvs= CItvs.add v CItv.zero_inf citvs ; citvs= CItvs.add v CItv.zero_inf citvs
; formula } ; formula }
, new_eqs )
let and_positive v phi = let and_positive v phi =
let+ {is_unsat; bo_itvs; citvs; formula} = phi in let+ {is_unsat; bo_itvs; citvs; formula} = phi in
let+| formula = let+| formula, new_eqs =
Formula.and_less_than (LiteralOperand IntLit.zero) (AbstractValueOperand v) formula Formula.and_less_than (LiteralOperand IntLit.zero) (AbstractValueOperand v) formula
in in
{ is_unsat ( { is_unsat
; bo_itvs= BoItvs.add v Itv.ItvPure.pos bo_itvs ; bo_itvs= BoItvs.add v Itv.ItvPure.pos bo_itvs
; citvs= CItvs.add v (CItv.ge_to IntLit.one) citvs ; citvs= CItvs.add v (CItv.ge_to IntLit.one) citvs
; formula } ; formula }
, new_eqs )
let and_eq_int v i phi = let and_eq_int v i phi =
let+ {is_unsat; bo_itvs; citvs; formula} = phi in let+ {is_unsat; bo_itvs; citvs; formula} = phi in
let+| formula = Formula.and_equal (AbstractValueOperand v) (LiteralOperand i) formula in let+| formula, new_eqs = Formula.and_equal (AbstractValueOperand v) (LiteralOperand i) formula in
{ is_unsat ( { is_unsat
; bo_itvs= BoItvs.add v (Itv.ItvPure.of_int_lit i) bo_itvs ; bo_itvs= BoItvs.add v (Itv.ItvPure.of_int_lit i) bo_itvs
; citvs= CItvs.add v (CItv.equal_to i) citvs ; citvs= CItvs.add v (CItv.equal_to i) citvs
; formula } ; formula }
, new_eqs )
let simplify ~keep phi = let simplify ~keep phi =
let+ {is_unsat; bo_itvs; citvs; formula} = phi in let+ {is_unsat; bo_itvs; citvs; formula} = phi in
let+| formula = Formula.simplify ~keep formula in let+| formula, new_eqs = Formula.simplify ~keep formula in
let is_in_keep v _ = AbstractValue.Set.mem v keep in let is_in_keep v _ = AbstractValue.Set.mem v keep in
{ is_unsat ( { is_unsat
; bo_itvs= BoItvs.filter is_in_keep bo_itvs ; bo_itvs= BoItvs.filter is_in_keep bo_itvs
; citvs= CItvs.filter is_in_keep citvs ; citvs= CItvs.filter is_in_keep citvs
; formula } ; formula }
, new_eqs )
let subst_find_or_new subst addr_callee = let subst_find_or_new subst addr_callee =
@ -193,26 +201,27 @@ let and_formula_callee subst formula_caller ~callee:formula_callee =
let and_callee subst phi ~callee:phi_callee = let and_callee subst phi ~callee:phi_callee =
if phi.is_unsat || phi_callee.is_unsat then (subst, false_) if phi.is_unsat || phi_callee.is_unsat then (subst, false_, [])
else else
match and_bo_itvs_callee subst phi.bo_itvs phi_callee.bo_itvs with match and_bo_itvs_callee subst phi.bo_itvs phi_callee.bo_itvs with
| exception Contradiction -> | exception Contradiction ->
L.d_printfln "contradiction found by inferbo intervals" ; L.d_printfln "contradiction found by inferbo intervals" ;
(subst, false_) (subst, false_, [])
| subst, bo_itvs' -> ( | subst, bo_itvs' -> (
match and_citvs_callee subst phi.citvs phi_callee.citvs with match and_citvs_callee subst phi.citvs phi_callee.citvs with
| exception Contradiction -> | exception Contradiction ->
L.d_printfln "contradiction found by concrete intervals" ; L.d_printfln "contradiction found by concrete intervals" ;
(subst, false_) (subst, false_, [])
| subst, citvs' -> ( | subst, citvs' -> (
match and_formula_callee subst phi.formula ~callee:phi_callee.formula with match and_formula_callee subst phi.formula ~callee:phi_callee.formula with
| Unsat -> | Unsat ->
L.d_printfln "contradiction found by formulas" ; L.d_printfln "contradiction found by formulas" ;
(subst, false_) (subst, false_, [])
| Sat (subst, formula') -> | Sat (subst, formula', new_eqs) ->
(* TODO: normalize here? *) (* TODO: normalize here? *)
L.d_printfln "conjoined formula post call: %a@\n" Formula.pp formula' ; L.d_printfln "conjoined formula post call: %a@\n" Formula.pp formula' ;
(subst, {is_unsat= false; bo_itvs= bo_itvs'; citvs= citvs'; formula= formula'}) ) ) (subst, {is_unsat= false; bo_itvs= bo_itvs'; citvs= citvs'; formula= formula'}, new_eqs)
) )
(** {2 Operations} *) (** {2 Operations} *)
@ -255,11 +264,12 @@ let eval_bo_itv_binop binop_addr bop op_lhs op_rhs bo_itvs =
let eval_binop binop_addr binop op_lhs op_rhs phi = let eval_binop binop_addr binop op_lhs op_rhs phi =
let+ {is_unsat; bo_itvs; citvs; formula} = phi in let+ {is_unsat; bo_itvs; citvs; formula} = phi in
let+| formula = Formula.and_equal_binop binop_addr binop op_lhs op_rhs formula in let+| formula, new_eqs = Formula.and_equal_binop binop_addr binop op_lhs op_rhs formula in
{ is_unsat ( { is_unsat
; bo_itvs= eval_bo_itv_binop binop_addr binop op_lhs op_rhs bo_itvs ; bo_itvs= eval_bo_itv_binop binop_addr binop op_lhs op_rhs bo_itvs
; citvs= eval_citv_binop binop_addr binop op_lhs op_rhs citvs ; citvs= eval_citv_binop binop_addr binop op_lhs op_rhs citvs
; formula } ; formula }
, new_eqs )
let eval_citv_unop unop_addr unop operand_addr citvs = let eval_citv_unop unop_addr unop operand_addr citvs =
@ -281,11 +291,14 @@ let eval_bo_itv_unop unop_addr unop operand_addr bo_itvs =
let eval_unop unop_addr unop addr phi = let eval_unop unop_addr unop addr phi =
let+ {is_unsat; bo_itvs; citvs; formula} = phi in let+ {is_unsat; bo_itvs; citvs; formula} = phi in
let+| formula = Formula.and_equal_unop unop_addr unop (AbstractValueOperand addr) formula in let+| formula, new_eqs =
{ is_unsat Formula.and_equal_unop unop_addr unop (AbstractValueOperand addr) formula
; bo_itvs= eval_bo_itv_unop unop_addr unop addr bo_itvs in
; citvs= eval_citv_unop unop_addr unop addr citvs ( { is_unsat
; formula } ; bo_itvs= eval_bo_itv_unop unop_addr unop addr bo_itvs
; citvs= eval_citv_unop unop_addr unop addr citvs
; formula }
, new_eqs )
let prune_bo_with_bop ~negated v_opt arith bop arith' phi = let prune_bo_with_bop ~negated v_opt arith bop arith' phi =
@ -318,14 +331,14 @@ let record_citv_abduced addr_opt arith_opt citvs =
let prune_binop ~negated bop lhs_op rhs_op ({is_unsat; bo_itvs= _; citvs; formula} as phi) = let prune_binop ~negated bop lhs_op rhs_op ({is_unsat; bo_itvs= _; citvs; formula} as phi) =
if is_unsat then phi if is_unsat then (phi, [])
else else
let value_lhs_opt, arith_lhs_opt, bo_itv_lhs = eval_operand phi lhs_op in let value_lhs_opt, arith_lhs_opt, bo_itv_lhs = eval_operand phi lhs_op in
let value_rhs_opt, arith_rhs_opt, bo_itv_rhs = eval_operand phi rhs_op in let value_rhs_opt, arith_rhs_opt, bo_itv_rhs = eval_operand phi rhs_op in
match CItv.abduce_binop_is_true ~negated bop arith_lhs_opt arith_rhs_opt with match CItv.abduce_binop_is_true ~negated bop arith_lhs_opt arith_rhs_opt with
| Unsatisfiable -> | Unsatisfiable ->
L.d_printfln "contradiction detected by concrete intervals" ; L.d_printfln "contradiction detected by concrete intervals" ;
false_ (false_, [])
| Satisfiable (abduced_lhs, abduced_rhs) -> ( | Satisfiable (abduced_lhs, abduced_rhs) -> (
let phi = let phi =
let citvs = let citvs =
@ -355,9 +368,9 @@ let prune_binop ~negated bop lhs_op rhs_op ({is_unsat; bo_itvs= _; citvs; formul
match Formula.prune_binop ~negated bop lhs_op rhs_op formula with match Formula.prune_binop ~negated bop lhs_op rhs_op formula with
| Unsat -> | Unsat ->
L.d_printfln "contradiction detected by formulas" ; L.d_printfln "contradiction detected by formulas" ;
false_ (false_, [])
| Sat formula -> | Sat (formula, new_eqs) ->
{phi with is_unsat; formula} ) ({phi with is_unsat; formula}, new_eqs) )
(** {2 Queries} *) (** {2 Queries} *)
@ -373,13 +386,13 @@ let is_unsat_cheap phi = phi.is_unsat
let is_unsat_expensive phi = let is_unsat_expensive phi =
(* note: contradictions are detected eagerly for all sub-domains except formula, so just (* note: contradictions are detected eagerly for all sub-domains except formula, so just
evaluate that one *) evaluate that one *)
if is_unsat_cheap phi then (phi, true) if is_unsat_cheap phi then (phi, true, [])
else else
match Formula.normalize phi.formula with match Formula.normalize phi.formula with
| Unsat -> | Unsat ->
(false_, true) (false_, true, [])
| Sat formula -> | Sat (formula, new_eqs) ->
({phi with formula}, false) ({phi with formula}, false, new_eqs)
let as_int phi v = let as_int phi v =

22
infer/src/pulse/PulsePathCondition.mli
Unescape View File

@ -14,20 +14,24 @@ type t [@@deriving yojson_of]
val true_ : t val true_ : t
val false_ : t
val pp : F.formatter -> t -> unit val pp : F.formatter -> t -> unit
type new_eqs = PulseFormula.new_eqs
(** {2 Building arithmetic constraints} *) (** {2 Building arithmetic constraints} *)
val and_nonnegative : AbstractValue.t -> t -> t val and_nonnegative : AbstractValue.t -> t -> t * new_eqs
(** [and_nonnegative v phi] is [phi ∧ v≥0] *) (** [and_nonnegative v phi] is [phi ∧ v≥0] *)
val and_positive : AbstractValue.t -> t -> t val and_positive : AbstractValue.t -> t -> t * new_eqs
(** [and_positive v phi] is [phi ∧ v>0] *) (** [and_positive v phi] is [phi ∧ v>0] *)
val and_eq_int : AbstractValue.t -> IntLit.t -> t -> t val and_eq_int : AbstractValue.t -> IntLit.t -> t -> t * new_eqs
(** [and_eq_int v i phi] is [phi ∧ v=i] *) (** [and_eq_int v i phi] is [phi ∧ v=i] *)
val simplify : keep:AbstractValue.Set.t -> t -> t val simplify : keep:AbstractValue.Set.t -> t -> t * new_eqs
(** [simplify ~keep phi] attempts to get rid of as many variables in [fv phi] but not in [keep] as (** [simplify ~keep phi] attempts to get rid of as many variables in [fv phi] but not in [keep] as
possible *) possible *)
@ -35,17 +39,17 @@ val and_callee :
(AbstractValue.t * ValueHistory.t) AbstractValue.Map.t (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t
-> t -> t
-> callee:t -> callee:t
-> (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t * t -> (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t * t * new_eqs
(** {2 Operations} *) (** {2 Operations} *)
type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t
val eval_binop : AbstractValue.t -> Binop.t -> operand -> operand -> t -> t val eval_binop : AbstractValue.t -> Binop.t -> operand -> operand -> t -> t * new_eqs
val eval_unop : AbstractValue.t -> Unop.t -> AbstractValue.t -> t -> t val eval_unop : AbstractValue.t -> Unop.t -> AbstractValue.t -> t -> t * new_eqs
val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> t val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> t * new_eqs
(** {2 Queries} *) (** {2 Queries} *)
@ -55,7 +59,7 @@ val is_known_zero : t -> AbstractValue.t -> bool
val is_unsat_cheap : t -> bool val is_unsat_cheap : t -> bool
(** whether the state contains a contradiction, call this as often as you want *) (** whether the state contains a contradiction, call this as often as you want *)
val is_unsat_expensive : t -> t * bool val is_unsat_expensive : t -> t * bool * new_eqs
(** whether the state contains a contradiction, only call this when you absolutely have to *) (** whether the state contains a contradiction, only call this when you absolutely have to *)
val as_int : t -> AbstractValue.t -> int option val as_int : t -> AbstractValue.t -> int option

8
infer/src/pulse/unit/PulseFormulaTest.ml
Unescape View File

@ -40,7 +40,7 @@ let of_binop bop f1 f2 phi =
let* phi, op1 = f1 phi in let* phi, op1 = f1 phi in
let* phi, op2 = f2 phi in let* phi, op2 = f2 phi in
let v = Var.mk_fresh () in let v = Var.mk_fresh () in
let+ phi = and_equal_binop v bop op1 op2 phi in let+ phi, _new_eqs = and_equal_binop v bop op1 op2 phi in
(phi, AbstractValueOperand v) (phi, AbstractValueOperand v)
@ -59,13 +59,13 @@ let ( mod ) f1 f2 phi = of_binop Mod f1 f2 phi
let ( = ) f1 f2 phi = let ( = ) f1 f2 phi =
let* phi, op1 = f1 phi in let* phi, op1 = f1 phi in
let* phi, op2 = f2 phi in let* phi, op2 = f2 phi in
and_equal op1 op2 phi and_equal op1 op2 phi >>| fst
let ( < ) f1 f2 phi = let ( < ) f1 f2 phi =
let* phi, op1 = f1 phi in let* phi, op1 = f1 phi in
let* phi, op2 = f2 phi in let* phi, op2 = f2 phi in
and_less_than op1 op2 phi and_less_than op1 op2 phi >>| fst
let ( && ) f1 f2 phi = f1 phi >>= f2 let ( && ) f1 f2 phi = f1 phi >>= f2
@ -119,7 +119,7 @@ let normalized_pp fmt = function
let test ~f phi = let test ~f phi =
AbstractValue.State.set init_vars_state ; AbstractValue.State.set init_vars_state ;
phi ttrue >>= f |> F.printf "%a" normalized_pp phi ttrue >>= f >>| fst |> F.printf "%a" normalized_pp
let normalize phi = test ~f:normalize phi let normalize phi = test ~f:normalize phi

32
infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp
Unescape View File

@ -28,11 +28,7 @@ void call_ifnotthenderef_false_null_bad() { ifnotthenderef(false, nullptr); }
// should be FN given the current "all allocated addresses are assumed // should be FN given the current "all allocated addresses are assumed
// disjoint unless specified otherwise" but we detect the bug because // disjoint unless specified otherwise" but we detect the bug because
// we don't propagate pure equalities that we discover to the heap part // we don't propagate pure equalities that we discover to the heap part
// void FN_alias_null_deref_latent(int* x, int* y) {
// Well, at the moment it *is* FN but because we mark the issue
// "latent" because the "if" test is not conclusively true. This is
// also ok.
void alias_null_deref_latent(int* x, int* y) {
*x = 32; *x = 32;
*y = 52; *y = 52;
if (x == y) { if (x == y) {
@ -54,3 +50,29 @@ void diverge_before_null_deref_ok(int* x) {
int* p = nullptr; int* p = nullptr;
*p = 42; *p = 42;
} }
// this test makes more sense in an inter-procedural setting
void stack_addresses_are_not_null_ok() {
int x;
if (&x == nullptr) {
int* p = nullptr;
*p = 42;
}
}
void stack_addresses_are_distinct_ok() {
int x;
int y;
if (&x == &y) {
int* p = nullptr;
*p = 42;
}
}
void null_test_after_deref_ok(int* x) {
*x = 42;
if (x == nullptr) {
int* p = nullptr;
*p = 42;
}
}

1
infer/tests/codetoanalyze/cpp/pulse/issues.exp
Unescape View File

@ -1,4 +1,3 @@
codetoanalyze/cpp/pulse/aliasing.cpp, alias_null_deref_latent, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/aliasing.cpp, call_ifnotthenderef_false_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `ifnotthenderef` here,parameter `x` of ifnotthenderef,invalid access occurs here] codetoanalyze/cpp/pulse/aliasing.cpp, call_ifnotthenderef_false_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `ifnotthenderef` here,parameter `x` of ifnotthenderef,invalid access occurs here]
codetoanalyze/cpp/pulse/aliasing.cpp, call_ifthenderef_true_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `ifthenderef` here,parameter `x` of ifthenderef,invalid access occurs here] codetoanalyze/cpp/pulse/aliasing.cpp, call_ifthenderef_true_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `ifthenderef` here,parameter `x` of ifthenderef,invalid access occurs here]
codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `setLanguage` here,variable `C++ temporary` accessed here,passed as argument to `Range::Range`,parameter `str` of Range::Range,return from call to `Range::Range`,passed as argument to `std::basic_string::~basic_string()` (modelled),return from call to `std::basic_string::~basic_string()` (modelled),was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `setLanguage`,variable `C++ temporary` accessed here,passed as argument to `Range::Range`,parameter `str` of Range::Range,passed as argument to `std::basic_string::data()` (modelled),return from call to `std::basic_string::data()` (modelled),assigned,return from call to `Range::Range`,return from call to `setLanguage`,when calling `Range::operator[]` here,parameter `this` of Range::operator[],invalid access occurs here] codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `setLanguage` here,variable `C++ temporary` accessed here,passed as argument to `Range::Range`,parameter `str` of Range::Range,return from call to `Range::Range`,passed as argument to `std::basic_string::~basic_string()` (modelled),return from call to `std::basic_string::~basic_string()` (modelled),was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `setLanguage`,variable `C++ temporary` accessed here,passed as argument to `Range::Range`,parameter `str` of Range::Range,passed as argument to `std::basic_string::data()` (modelled),return from call to `std::basic_string::data()` (modelled),assigned,return from call to `Range::Range`,return from call to `setLanguage`,when calling `Range::operator[]` here,parameter `this` of Range::operator[],invalid access occurs here]

Write Preview
Loading…
Cancel
Save