rapx 0.7.63

A static analysis platform for Rust program analysis and verification
// RAPx contract DSL grammar.
//
// This is the single source of truth for the contract-DSL expression surface.
// The generated parser feeds two entry points (`expr` and `def_body`): contract
// expressions/predicates, and `pred!`/`def_property` bodies. The attribute
// wrapper (`#[rapx::requires(...)]`), tag names, and the `any(...)` combinator
// are handled by `syn` in `attr.rs` / `builder.rs`, since attribute token
// streams are Rust syntax.
//
// `size_of::<T>()` / `align_of::<T>()` (turbofish, optionally with a
// `std::mem::` / `core::mem::` path prefix) are also supported; `size_of(T)`
// remains the preferred shorthand.

// ── Tokens / trivia ────────────────────────────────────────────────────────

WHITESPACE = _{ " " | "\t" | "\r" | "\n" }

int   = @{ ASCII_DIGIT+ }
ident = @{ (ASCII_ALPHA | "_") ~ (ASCII_ALPHANUMERIC | "_")* }

relop  = { "==" | "!=" | "<=" | ">=" | "<" | ">" }
addop  = { "+" | "-" }
mulop  = { "*" | "/" | "%" }
bor    = { "|" }
bxor   = { "^" }
band   = { "&" }
unop   = { "!" | "-" }

// ── Tag call ────────────────────────────────────────────────────────────────

tag_call = { ident ~ "(" ~ arg_list? ~ ")" }

arg_list = { arg ~ ("," ~ arg)* }

// ── Arguments ────────────────────────────────────────────────────────────────

arg = { expr }

// ── Expression layer ────────────────────────────────────────────────────────

expr_input  = { SOI ~ expr ~ EOI }
expr        = { if_expr | not_is_empty | cmp }
if_expr     = { "if" ~ cond ~ "{" ~ expr ~ "}" ~ "else" ~ "{" ~ expr ~ "}" }
cond        = { not_is_empty | cmp }
not_is_empty = { "!" ~ base ~ "." ~ "is_empty" ~ "(" ~ ")" }
cmp         = { bit_or ~ (relop ~ bit_or)? }
bit_or      = { bit_xor ~ (bor ~ bit_xor)* }
bit_xor     = { bit_and ~ (bxor ~ bit_and)* }
bit_and     = { additive ~ (band ~ additive)* }
additive    = { multiplicative ~ (addop ~ multiplicative)* }
multiplicative = { unary ~ (mulop ~ unary)* }
unary       = { unop ~ unary | primary }
primary     = { int | call | size_of_call | const_path | place | "(" ~ expr ~ ")" }

// ── Builtin functions ───────────────────────────────────────────────────────

call    = { builtin ~ "(" ~ arg_list? ~ ")" }
builtin = { "size_of" | "align_of" | "len" | "min" | "max" }

// size_of::<T>() / align_of::<T>() with optional `std::mem::` / `core::mem::`
// path prefix (turbofish form).
size_of_call = { ("std" ~ "::" ~ "mem" ~ "::" | "core" ~ "::" ~ "mem" ~ "::")? ~ ("size_of" | "align_of") ~ "::" ~ "<" ~ ident ~ ">" ~ "(" ~ ")" }

// ── Places and projections ──────────────────────────────────────────────────

place      = { base ~ projection* }
base       = { "self" | "return" | "Arg_" ~ int | ident }
projection = { "." ~ member }
member     = { ident ~ "()"? | int }

// ── Type-level constants (T::MAX, isize::MAX, ...) ──────────────────────────

const_path = { ident ~ "::" ~ ("MAX" | "MIN" | "BITS") }

// ── `pred!` body ────────────────────────────────────────────────────────

def_body = { SOI ~ or_expr ~ EOI }
or_expr  = { and_expr ~ ("||" ~ and_expr)* }
and_expr = { def_leaf ~ ("&&" ~ def_leaf)* }
def_leaf = { tag_call | "(" ~ or_expr ~ ")" }