Module InferModules__Prop
Functions for Propositions (i.e., Symbolic Heaps)
type pi
= InferIR.Sil.atom list
type sigma
= InferIR.Sil.hpred list
type 'a t
= private
{
sigma : sigma;
spatial part
sub : InferIR.Sil.subst;
substitution
pi : pi;
pure part
sigma_fp : sigma;
abduced spatial part
pi_fp : pi;
abduced pure part
}
the kind 'a should range over
normal
andexposed
type struct_init_mode
=
|
No_init
|
Fld_init
type to describe different strategies for initializing fields of a structure.
No_init
does not initialize any fields of the struct.Fld_init
initializes the fields of the struct with fresh variables (C) or default values (Java).
Basic Functions for propositions
val d_sub : InferIR.Sil.subst -> unit
Dump a substitution.
val pp_pi : InferStdlib.Pp.env -> Stdlib.Format.formatter -> pi -> unit
Pretty print a pi.
val d_pi : pi -> unit
Dump a pi.
val d_sigma : sigma -> unit
Dump a sigma.
val sigma_get_stack_nonstack : bool -> sigma -> sigma * sigma
Split sigma into stack and nonstack parts. The boolean indicates whether the stack should only include local variales.
val prop_update_obj_sub : InferStdlib.Pp.env -> 'a t -> InferStdlib.Pp.env
Update the object substitution given the stack variables in the prop
val pp_prop : InferStdlib.Pp.env -> Stdlib.Format.formatter -> 'a t -> unit
Pretty print a proposition.
val prop_pred_env : 'a t -> InferIR.Sil.Predicates.env
Create a predicate environment for a prop
val d_prop : 'a t -> unit
Dump a proposition.
val d_proplist_with_typ : 'a t list -> unit
val max_stamp : ?f:(InferIR.Ident.t -> bool) -> normal t -> int
val pi_free_vars : pi -> InferIR.Ident.t InferStdlib.IStd.Sequence.t
val sigma_free_vars : sigma -> InferIR.Ident.t InferStdlib.IStd.Sequence.t
val free_vars : normal t -> InferIR.Ident.t InferStdlib.IStd.Sequence.t
val gen_free_vars : normal t -> (unit, InferIR.Ident.t) InferStdlib.IStd.Sequence.Generator.t
val sorted_gen_free_vars : sorted t -> (unit, InferIR.Ident.t) InferStdlib.IStd.Sequence.Generator.t
val non_pure_free_vars : normal t -> InferIR.Ident.t InferStdlib.IStd.Sequence.t
val dfs_sort : InferIR.Tenv.t -> normal t -> sorted t
val pi_sub : InferIR.Sil.subst -> InferIR.Sil.atom list -> InferIR.Sil.atom list
Apply substitution for pi
val sigma_sub : InferIR.Sil.subst -> InferIR.Sil.hpred list -> InferIR.Sil.hpred list
Apply subsitution for sigma
val prop_sub : InferIR.Sil.subst -> 'a t -> exposed t
Apply subsitution to prop. Result is not normalized.
val prop_expmap : (InferIR.Exp.t -> InferIR.Exp.t) -> 'a t -> exposed t
Apply the substitution to all the expressions in the prop.
val sigma_replace_exp : InferIR.Tenv.t -> (InferIR.Exp.t * InferIR.Exp.t) list -> InferIR.Sil.hpred list -> InferIR.Sil.hpred list
Relaces all expressions in the
hpred list
using the first argument. Assume that the first parameter defines a partial function. No expressions inside hpara are replaced.
Normalization
val mk_inequality : InferIR.Tenv.t -> InferIR.Exp.t -> InferIR.Sil.atom
Turn an inequality expression into an atom
val atom_is_inequality : InferIR.Sil.atom -> bool
Return
true
if the atom is an inequality
val atom_exp_le_const : InferIR.Sil.atom -> (InferIR.Exp.t * InferIR.IntLit.t) option
If the atom is
e<=n
returne,n
val atom_const_lt_exp : InferIR.Sil.atom -> (InferIR.IntLit.t * InferIR.Exp.t) option
If the atom is
n<e
returnn,e
val exp_normalize_prop : ?destructive:bool -> InferIR.Tenv.t -> 'a t -> InferIR.Exp.t -> InferIR.Exp.t
Normalize
exp
using the pure part ofprop
. Later, we should change this such that the normalization exposes offsets ofexp
as much as possible.If
destructive
is true then normalize more aggressively, which may lose some useful structure or types.
val exp_normalize_noabs : InferIR.Tenv.t -> InferIR.Sil.subst -> InferIR.Exp.t -> InferIR.Exp.t
Normalize the expression without abstracting complex subexpressions
val exp_collapse_consecutive_indices_prop : InferIR.Typ.t -> InferIR.Exp.t -> InferIR.Exp.t
Collapse consecutive indices that should be added. For instance, this function reduces
x[1][1]
tox[2]
. Thetyp
argument is used to ensure the soundness of this collapsing.
val lexp_normalize_prop : InferIR.Tenv.t -> 'a t -> InferIR.Exp.t -> InferIR.Exp.t
Normalize
exp
used for the address of a heap cell. This normalization does not combine two offsets insideexp
.
val atom_normalize_prop : InferIR.Tenv.t -> 'a t -> InferIR.Sil.atom -> InferIR.Sil.atom
val sigma_normalize_prop : InferIR.Tenv.t -> 'a t -> InferIR.Sil.hpred list -> InferIR.Sil.hpred list
val normalize : InferIR.Tenv.t -> exposed t -> normal t
normalize a prop
Compaction
val prop_compact : InferIR.Sil.sharing_env -> normal t -> normal t
Return a compact representation of the prop
Queries about propositions
val prop_is_emp : 'a t -> bool
Check if the sigma part of the proposition is emp
Functions for changing and generating propositions
val mk_neq : InferIR.Tenv.t -> InferIR.Exp.t -> InferIR.Exp.t -> InferIR.Sil.atom
Construct a disequality.
val mk_eq : InferIR.Tenv.t -> InferIR.Exp.t -> InferIR.Exp.t -> InferIR.Sil.atom
Construct an equality.
val mk_pred : InferIR.Tenv.t -> InferIR.PredSymb.t -> InferIR.Exp.t list -> InferIR.Sil.atom
Construct a positive pred.
val mk_npred : InferIR.Tenv.t -> InferIR.PredSymb.t -> InferIR.Exp.t list -> InferIR.Sil.atom
Construct a negative pred.
val create_strexp_of_type : InferIR.Tenv.t -> struct_init_mode -> InferIR.Typ.t -> InferIR.Exp.t option -> InferIR.Sil.inst -> InferIR.Sil.strexp
create a strexp of the given type, populating the structures if
expand_structs
is true
val mk_ptsto : InferIR.Tenv.t -> InferIR.Exp.t -> InferIR.Sil.strexp -> InferIR.Exp.t -> InferIR.Sil.hpred
Construct a pointsto.
val mk_ptsto_exp : InferIR.Tenv.t -> struct_init_mode -> (InferIR.Exp.t * InferIR.Exp.t * InferIR.Exp.t option) -> InferIR.Sil.inst -> InferIR.Sil.hpred
Construct a points-to predicate for an expression using either the provided expression
name
as base for fresh identifiers.
val mk_ptsto_lvar : InferIR.Tenv.t -> struct_init_mode -> InferIR.Sil.inst -> (InferIR.Pvar.t * InferIR.Exp.t * InferIR.Exp.t option) -> InferIR.Sil.hpred
Construct a points-to predicate for a single program variable. If
expand_structs
is true, initialize the fields of structs with fresh variables.
val mk_lseg : InferIR.Tenv.t -> InferIR.Sil.lseg_kind -> InferIR.Sil.hpara -> InferIR.Exp.t -> InferIR.Exp.t -> InferIR.Exp.t list -> InferIR.Sil.hpred
Construct a lseg predicate
val mk_dllseg : InferIR.Tenv.t -> InferIR.Sil.lseg_kind -> InferIR.Sil.hpara_dll -> InferIR.Exp.t -> InferIR.Exp.t -> InferIR.Exp.t -> InferIR.Exp.t -> InferIR.Exp.t list -> InferIR.Sil.hpred
Construct a dllseg predicate
val prop_reset_inst : (InferIR.Sil.inst -> InferIR.Sil.inst) -> 'a t -> exposed t
Reset every inst in the prop using the given map
val prop_hpred_star : 'a t -> InferIR.Sil.hpred -> exposed t
Conjoin a heap predicate by separating conjunction.
val prop_sigma_star : 'a t -> InferIR.Sil.hpred list -> exposed t
Conjoin a list of heap predicates by separating conjunction
val prop_atom_and : InferIR.Tenv.t -> ?footprint:bool -> normal t -> InferIR.Sil.atom -> normal t
Conjoin a pure atomic predicate by normal conjunction.
val conjoin_eq : InferIR.Tenv.t -> ?footprint:bool -> InferIR.Exp.t -> InferIR.Exp.t -> normal t -> normal t
Conjoin
exp1
=exp2
with a symbolic heapprop
.
val conjoin_neq : InferIR.Tenv.t -> ?footprint:bool -> InferIR.Exp.t -> InferIR.Exp.t -> normal t -> normal t
Conjoin
exp1
!=exp2
with a symbolic heapprop
.
val get_pure : 'a t -> InferIR.Sil.atom list
Return the pure part of
prop
.
val prop_rename_primed_footprint_vars : InferIR.Tenv.t -> normal t -> normal t
Canonicalize the names of primed variables.
val prop_expand : InferIR.Tenv.t -> normal t -> normal t list
Expand PE listsegs if the flag is on.
Functions for existentially quantifying and unquantifying variables
val exist_quantify : InferIR.Tenv.t -> ?ids_queue:unit InferIR.Ident.HashQueue.t -> InferIR.Ident.t list -> normal t -> normal t
Existentially quantify the
ids
inprop
.
val prop_normal_vars_to_primed_vars : InferIR.Tenv.t -> normal t -> normal t
convert the footprint vars to primed vars.
val prop_primed_vars_to_normal_vars : InferIR.Tenv.t -> normal t -> normal t
convert the primed vars to normal vars.
Prop iterators
val prop_iter_create : normal t -> unit prop_iter option
Create an iterator, return None if sigma part is empty.
val prop_iter_to_prop : InferIR.Tenv.t -> 'a prop_iter -> normal t
Return the prop associated to the iterator.
val prop_iter_add_atom : bool -> 'a prop_iter -> InferIR.Sil.atom -> 'a prop_iter
Add an atom to the pi part of prop iter. The first parameter records whether it is done during footprint or during re - execution.
val prop_iter_remove_curr_then_to_prop : InferIR.Tenv.t -> 'a prop_iter -> normal t
Remove the current element from the iterator, and return the prop associated to the resulting iterator.
val prop_iter_current : InferIR.Tenv.t -> 'a prop_iter -> InferIR.Sil.hpred * 'a
Return the current hpred and state.
val prop_iter_update_current : 'a prop_iter -> InferIR.Sil.hpred -> 'a prop_iter
Update the current element of the iterator.
val prop_iter_prev_then_insert : 'a prop_iter -> InferIR.Sil.hpred -> 'a prop_iter
Insert before the current element of the iterator.
val prop_iter_max_stamp : ?f:(InferIR.Ident.t -> bool) -> 'a prop_iter -> int
Find the maximum stamp of a free variable of a certain kind.
val prop_iter_get_footprint_sigma : 'a prop_iter -> InferIR.Sil.hpred list
Extract the sigma part of the footprint
val prop_iter_replace_footprint_sigma : 'a prop_iter -> InferIR.Sil.hpred list -> 'a prop_iter
Replace the sigma part of the footprint
val prop_iter_find : unit prop_iter -> (InferIR.Sil.hpred -> 'a option) -> 'a prop_iter option
Scan sigma to find an
hpred
satisfying the filter function.
val prop_iter_update_current_by_list : 'a prop_iter -> InferIR.Sil.hpred list -> unit prop_iter
Update the current element of the iterator by a nonempty list of elements.
val prop_iter_make_id_primed : InferIR.Tenv.t -> InferIR.Ident.t -> 'a prop_iter -> 'a prop_iter
Rename
ident
initer
by a fresh primed identifier
Internal modules
module Metrics : sig ... end
module CategorizePreconditions : sig ... end