Prop (infer.InferModules.Prop)

type normal

kind for normal props, i.e. normalized

type exposed

kind for exposed props

type sorted

kind for sorted props

type pi = InferIR.Sil.atom list

type sigma = InferIR.Sil.hpred list

type 'a t = private {

`sigma : sigma;`	(** spatial part *)
`sub : InferIR.Sil.exp_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 and exposed

include sig ... end

val compare : ('a ‑> 'a ‑> int) ‑> 'a t ‑> 'a t ‑> int

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 compare_prop : 'a t ‑> 'a t ‑> int

Compare propositions

val equal_sigma : sigma ‑> sigma ‑> bool

Check the equality of two sigma's

val pp_sub : InferStdlib.Pp.env ‑> Format.formatter ‑> InferIR.Sil.subst ‑> unit

Pretty print a substitution.

val d_sub : InferIR.Sil.subst ‑> unit

Dump a substitution.

val pp_pi : InferStdlib.Pp.env ‑> Format.formatter ‑> pi ‑> unit

Pretty print a pi.

val d_pi : pi ‑> unit

Dump a pi.

val pp_sigma : InferStdlib.Pp.env ‑> Format.formatter ‑> sigma ‑> unit

Pretty print a sigma.

val d_sigma : sigma ‑> unit

Dump a sigma.

val d_pi_sigma : pi ‑> sigma ‑> unit

Dump a pi and 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 ‑> Format.formatter ‑> 'a t ‑> unit

Pretty print a proposition.

val pp_prop_with_typ : InferStdlib.Pp.env ‑> Format.formatter ‑> normal t ‑> unit

Pretty print a proposition with type information

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 pp_proplist_with_typ : InferStdlib.Pp.env ‑> Format.formatter ‑> normal t list ‑> unit

Pretty print a list propositions with type information

val d_proplist_with_typ : 'a t list ‑> unit

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 footprint_free_vars : normal t ‑> InferIR.Ident.t InferStdlib.IStd.Sequence.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 return e,n

val atom_const_lt_exp : InferIR.Sil.atom ‑> (InferIR.IntLit.t * InferIR.Exp.t) option

If the atom is n<e return n,e

val exp_normalize_prop : ?⁠destructive:bool ‑> InferIR.Tenv.t ‑> 'a t ‑> InferIR.Exp.t ‑> InferIR.Exp.t

Normalize exp using the pure part of prop. Later, we should change this such that the normalization exposes offsets of exp 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 x11 to x2. The typ 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 inside exp.

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

val expose : normal t ‑> exposed t

expose a prop, no-op used to instantiate the sub-type relation

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_emp : normal t

Proposition true /\ emp.

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 heap prop.

val conjoin_neq : InferIR.Tenv.t ‑> ?⁠footprint:bool ‑> InferIR.Exp.t ‑> InferIR.Exp.t ‑> normal t ‑> normal t

Conjoin exp1!=exp2 with a symbolic heap prop.

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 extract_footprint : 'a t ‑> exposed t

Extract the footprint and return it as a prop

val extract_spec : normal t ‑> normal t * normal t

Extract the (footprint,current) pair

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 in prop.

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.

val from_pi : pi ‑> exposed t

Build an exposed prop from pi

val from_sigma : sigma ‑> exposed t

Build an exposed prop from sigma

val set : ?⁠sub:InferIR.Sil.exp_subst ‑> ?⁠pi:pi ‑> ?⁠sigma:sigma ‑> ?⁠pi_fp:pi ‑> ?⁠sigma_fp:sigma ‑> 'a t ‑> exposed t

Set individual fields of the prop.

Prop iterators

type 'a prop_iter

Iterator over the sigma part. Each iterator has a current hpred.

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_next : 'a prop_iter ‑> unit prop_iter option

Return the next iterator.

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_footprint_free_vars : 'a prop_iter ‑> InferIR.Ident.t InferStdlib.IStd.Sequence.t

Find fav of the footprint part of the iterator

val prop_iter_free_vars : 'a prop_iter ‑> InferIR.Ident.t InferStdlib.IStd.Sequence.t

Find fav of the iterator

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_set_state : 'a prop_iter ‑> 'b ‑> 'b prop_iter

Set the state of an iterator

val prop_iter_make_id_primed : InferIR.Tenv.t ‑> InferIR.Ident.t ‑> 'a prop_iter ‑> 'a prop_iter

Rename ident in iter by a fresh primed identifier

Module InferModules.Prop