Enum Property 

pub enum Property<'tcx> {
    Leaf(LeafProperty<'tcx>),
    Or(OrProperty<'tcx>),
}

A safety property: either a single predicate (Leaf) or a disjunction of alternative predicate groups (Or).

Conjunction (And) is deliberately not a variant: it is expressed by the surrounding collection — the caller’s requires list is already a conjunction, and each Or group is a conjunction of its members (DNF).

Splitting Leaf from Or makes the mutually-exclusive payloads (args vs. groups) explicit in the type, so a leaf can never carry alternatives and an Or can never carry arguments.

Variants

Leaf(LeafProperty<'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, ) -> PropertyArg<'tcx>

Resolve a single positional argument according to its declared role.

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 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 new_simple(kind: PropertyKind) -> Self

pub 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, ...), ...))

A disjunct is either a single property application P(...) or a parenthesised conjunction (P1(...), ..., Pn(...)). Two patterns are supported:

1. Null guard: exactly two disjuncts, one being Null(p) alone, the other a conjunction of properties over the same place p. The disjunction expands to the conjunct properties, each holding whenever p is non-null and vacuously for a null p.

2. General disjunction: each disjunct is standalone or a conjunction, e.g., any(Trait(T, Copy), Trait(T, TrivialClone)). Produces a single Property::Or whose groups encode the DNF structure: each inner Vec is one AND-group.

fn build_null_guard( tcx: TyCtxt<'tcx>, def_id: DefId, guard: &[(String, Vec<Expr>)], conjuncts: &[(String, Vec<Expr>)], ) -> Vec<Self>

Build the null-guard expansion: Null(p) OR (P1 & P2 & ...).

fn apply_null_guard(property: &mut Property<'tcx>, guard_key: &PlaceKey) -> bool

Recursively propagate a null-guard to a property and every member of its Or groups. Returns false if a place-bearing member constrains a place other than the guard.

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 new_with_args(kind: PropertyKind, args: Vec<PropertyArg<'tcx>>) -> Self

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

fn parse_target_args_with_for_each( tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr], ) -> (Vec<PropertyArg<'tcx>>, Option<ContractPlace<'tcx>>)

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

impl<'tcx> Property<'tcx>

pub 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_leaf(kind: PropertyKind, args: Vec<PropertyArg<'tcx>>) -> Self

Build a single predicate leaf.

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

Build a Property::Or disjunction from already-expanded DNF groups.

Each inner Vec is one AND-group (all its members must hold); at least one group must hold for the disjunction to be satisfied. This is the single place an Or property is constructed so that callers in the def, JSON (query), and any(...) (parser) layers share identical semantics.

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

The predicate kind of a leaf property (None for an Or, which has no single kind).

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

The positional arguments of a leaf property (Or has none).

pub fn groups(&self) -> &[Vec<Box<Property<'tcx>>>]

The alternative groups of an Or property (Leaf has none).

pub fn contract_kind(&self) -> ContractKind

pub fn null_guard(&self) -> Option<&PlaceKey>

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

pub fn origin_name(&self) -> Option<&str>

pub fn origin_args(&self) -> Option<&[String]>

The full call-site arguments of the compound def this property expanded from (None for plain primitives).

pub fn origin_meaning(&self) -> Option<&str>

The human-readable meaning of the compound def.

pub fn is_or(&self) -> bool

pub fn ty_arg(&self) -> Option<Ty<'tcx>>

The first Ty argument.

pub fn count_expr(&self) -> Option<&ContractExpr<'tcx>>

The first Expr argument, typically a count/length expression.

pub 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 (leaf or Or) with the display name, full call-site arguments, and meaning of the compound def it expanded from.

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

Attach a for_each container to a leaf property.

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) -> Property<'tcx>

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.