Enum Property 

pub(crate) enum Property<'tcx> {
    Atom(AtomProperty<'tcx>),
    And(AndProperty<'tcx>),
    Or(OrProperty<'tcx>),
}

A safety property: a boolean formula over atomic predicates.

The formula is a tree of three node kinds — Atom (a single predicate), And (conjunction: all members hold), and Or (disjunction: at least one member holds). Box breaks the recursion; the top level of a contract is simply a Vec<Property> (an implicit conjunction of requirements).

Variants

Atom(AtomProperty<'tcx>)

And(AndProperty<'tcx>)

Or(OrProperty<'tcx>)

Implementations

impl<'tcx> Property<'tcx>

fn parse_from_spec( tcx: TyCtxt<'tcx>, def_id: DefId, spec: &PropertySpec, exprs: &[Expr], ) -> Self

Parse a property from the declaration table, dispatching on the tag’s assembly strategy.

fn resolve_arg( tcx: TyCtxt<'tcx>, def_id: DefId, tag: &str, arg_kind: ArgKind, expr: &Expr, ) -> Option<PropertyArg<'tcx>>

Resolve a single positional argument according to its declared role.

Returns None when a Ty argument cannot be resolved, so the caller degrades the whole property to Unknown instead of silently substituting the never type (which would make Align/Typed trivially provable).

fn build_uniform( tcx: TyCtxt<'tcx>, def_id: DefId, spec: &PropertySpec, exprs: &[Expr], ) -> Self

Positional resolution over one of the spec’s accepted forms.

pub(crate) fn new( tcx: TyCtxt<'tcx>, def_id: DefId, name: &str, exprs: &[Expr], ) -> Self

fn build_size(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self

fn build_allocated(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self

fn build_inbound(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self

fn build_nonoverlap(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self

fn build_validnum(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self

fn build_targets( spec: &PropertySpec, tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr], ) -> Self

fn build_pinned(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Self

fn build_split_transmute( tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr], ) -> Self

fn build_contain_no_type( tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr], ) -> Self

fn new_simple(kind: PropertyKind) -> Self

pub(crate) fn parse_list( tcx: TyCtxt<'tcx>, def_id: DefId, name: &str, exprs: &[Expr], ) -> Vec<Self>

Parse one annotation entry into the properties it denotes.

Plain entries (Align(p, T), Owning(p), …) yield one property. The any(...) combinator may expand to several: see Self::parse_any.

fn parse_any(tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr]) -> Vec<Self>

Parse the disjunctive combinator any(D1, D2, ...) written in DNF: any means logical OR between disjuncts, and commas inside a parenthesised disjunct mean logical AND:

any(Null(p), (P1(p, ...), P2(p, ...), ...))
any(Trait(T, Copy), Trait(T, TrivialClone), ...)

A disjunct is either a single property application P(...) or a parenthesised conjunction (P1(...), ..., Pn(...)). Any number (≥ 2) of disjuncts is accepted; each is expanded into its constituent properties, producing a single Property::Or whose disjuncts are atoms or And nodes.

fn disjunct_parts(expr: &Expr) -> Option<Vec<(String, Vec<Expr>)>>

Split one disjunct into its conjunct calls: a (P1, P2, ...) tuple, a parenthesised single property (P), or a bare property application.

fn call_parts(expr: &Expr) -> Option<(String, Vec<Expr>)>

Split a Name(arg, ...) call expression into its name and arguments.

fn check_arg_length(expr_len: usize, required_len: usize, sp: &str) -> bool

impl<'tcx> Property<'tcx>

pub(crate) fn display_for_report( &self, tcx: TyCtxt<'tcx>, struct_def_id: Option<DefId>, fn_def_id: Option<DefId>, ) -> String

impl<'tcx> Property<'tcx>

pub(crate) fn new_atom(kind: PropertyKind, args: Vec<PropertyArg<'tcx>>) -> Self

Build a single atomic predicate.

pub(crate) fn new_and(conjuncts: Vec<Property<'tcx>>) -> Self

Build a conjunction (And) of already-expanded conjuncts.

pub(crate) fn new_or(disjuncts: Vec<Property<'tcx>>) -> Self

Build a disjunction (Or) of already-expanded disjuncts.

pub(crate) fn conjunction(conjuncts: Vec<Property<'tcx>>) -> Self

Normalize a list of conjuncts into a single Property: a singleton is returned as-is, otherwise the list is wrapped in an And node.

pub(crate) fn kind(&self) -> Option<PropertyKind>

The predicate kind of an atom (None for And/Or, which have no single kind).

pub(crate) fn args(&self) -> &[PropertyArg<'tcx>]

The positional arguments of an atom (And/Or have none).

pub(crate) fn target_place(&self) -> Option<&ContractPlace<'tcx>>

The ContractPlace this atom’s first argument refers to, when the first argument is a place (or an index access over one, e.g. slice[i]).

pub(crate) fn conjuncts(&self) -> &[Box<Property<'tcx>>]

The conjuncts of an And property (Atom/Or have none).

pub(crate) fn disjuncts(&self) -> &[Box<Property<'tcx>>]

The disjuncts of an Or property (Atom/And have none).

pub(crate) fn contract_kind(&self) -> ContractKind

pub(crate) fn for_each(&self) -> Option<&ContractPlace<'tcx>>

pub(crate) fn origin(&self) -> Option<&ContractOrigin>

Display metadata when this property was expanded from a compound property.

pub(crate) fn is_or(&self) -> bool

pub(crate) fn is_and(&self) -> bool

pub(crate) fn apply_kind(&mut self, kind: Option<&str>)

Apply contract kind metadata from a JSON entry or attribute.

pub(crate) fn set_origin( &mut self, name: String, args: Vec<String>, meaning: Option<String>, )

Tag a property (atom, And, or Or) with the display name, full call-site arguments, and meaning of the compound property it expanded from.

pub(crate) fn clear_origin(&mut self)

Remove the compound-origin display metadata from this property.

pub(crate) fn set_for_each(&mut self, place: Option<ContractPlace<'tcx>>)

Attach a for_each container to an atom.

pub(crate) fn set_contract_kind(&mut self, k: ContractKind)

Override the contract kind (e.g. Alias → Hazard).

Trait Implementations

impl<'tcx> Clone for Property<'tcx>

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'tcx> Debug for Property<'tcx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.