Module def 

User-defined contract def layer.

Users (downloading a prebuilt rapx binary) can define new named safety contracts as boolean combinations of the 21 primitive safety properties, and reference them from #[rapx::requires(MyTag(...))] — without recompiling rapx.

A def is a DNF macro over primitive property calls:

def MySafeRead(p: Target, T: Ty, n: Expr) =
    NonNull(p) && Align(p, T) && Allocated(p, T, n);

def StrOrBytes(s: Target, T: Ty, n: Expr) =
    ValidCStr(s, n) || (Allocated(s, T, n) && Init(s, T, n));

The DSL only composes existing primitives; it cannot invent new primitive semantics (those live in property_checker.rs). Expansion is a pure front-end that produces ordinary Property values consumed by the existing checker.

Structs

DefSpec

A parsed def declaration.

Subst 🔒

Substitute def formal parameters with the concrete call-site arguments inside a literal expression (e.g. turn size_of(T) * n into size_of(u32) * len, or p.unwrap_some() into head.unwrap_some()).

Enums

DefArg

A single argument in a def body: a reference to a formal parameter, or a literal (kept as source text, re-parsed as syn::Expr at expansion time).

DefBody

The body of a def, structured as DNF (Or of And of calls).

Functions

builtin_defs 🔒

Builtin defs shipped with rapx: the standard compound safety properties (std-contracts.rs) plus user extensions (user-contracts.rs).

builtin_defs_map 🔒

Builtin defs shipped with rapx: the standard compound safety properties (std-contracts.rs) plus user extensions (user-contracts.rs). Immutable and shared across every crate.

collect_def_refs 🔒

conv_def_and 🔒

conv_def_call 🔒

conv_def_leaf 🔒

conv_def_or 🔒

def_refs 🔒

Collect the tag names referenced by a DefBody, in left-to-right order.

def_ty_matches_arg_kind 🔒

Whether a def parameter annotation matches a primitive argument role.

expand_body 🔒

Expand a DefBody into the property list it denotes.

expand_def

Expand a named def against concrete argument expressions.

extract_contract_def_string 🔒

Extract the string literal from a #[rapx::def_contract("def ...")] attribute’s textual representation.

find_cycle_in 🔒

find_def

Look up a def by name, in the given crate’s namespace first, then the builtin namespace.

find_def_cycle

Return a cycle path (e.g. ["A", "B", "A"]) if expanding start can reach itself again through def-to-def references, None otherwise.

is_contract_def_attr 🔒

Whether an attribute path is rapx::def_contract (or the bare form with the tool prefix stripped).

parse_body 🔒

Parse the body into a DNF tree. || binds looser than &&.

parse_defs

Parse a source fragment containing block-shaped contract definitions (Name(params) { body }) into a list of DefSpecs.

parse_equation_params 🔒

parse_one_def_block 🔒

Parse a single leading Name(p: Ptr, T: Ty, ...) { body } block from s. Returns the DefSpec (without doc) and the number of bytes consumed through the closing }.

register_contract_defs

Scan the local crate for #[rapx::def_contract("...")] tool attributes (emitted by the rapx_macros::pred proc-macro) and register each embedded def string. Returns the number of defs registered.

register_defs_from_source

Parse def declarations from source and insert them into the given crate’s namespace. Returns the number of defs registered.

render_expr_src 🔒

Render a syn::Expr back to source-like text. proc_macro2 stringifies tokens space-separated (self . 0, size_of (T)), so collapse the spaces around punctuation for a readable form.

resolve_arg_string 🔒

Resolve a call-site argument expression to its display form, following the def parameter’s declared role so internal placeholders (e.g. Arg_0 from a JSON contract) render as the actual parameter name.

unknown_property 🔒

user_defs_map 🔒

Per-crate user defs, registered from #[rapx::def_contract] attributes.