Enum WcetFunction 

pub enum WcetFunction {
    Bounded {
        name: String,
        cycles: u64,
        instr_count: usize,
        loops: Vec<WcetLoopBound>,
        recursion: Option<WcetRecursionBound>,
        hint_rejections: Vec<WcetHintRejection>,
        hint_key: Option<WcetHintKey>,
    },
    Declined {
        name: String,
        reason: WcetDecline,
        note: String,
        op: Option<String>,
        offset: Option<u64>,
        hint_rejections: Vec<WcetHintRejection>,
        hint_key: Option<WcetHintKey>,
    },
}

The per-function result: either a sound cycle bound or a loud decline.

Variants

Bounded

A sound upper bound on this function’s execution in cycles.

Fields

name: String

Function name (WASM export or generated).

cycles: u64

The sound worst-case cycle bound. For a loop-free function this is the SUM of each instruction’s documented worst-case cycles (each executes at most once). For a function whose loops ALL have proven trip counts (#778 phase 2) each instruction’s cost is multiplied by its proven worst-case execution count. Always ≥ any real execution under the stated precondition.

instr_count: usize

Number of ARM instructions summed (diagnostic).

loops: Vec<WcetLoopBound>

Proven loops (empty for a loop-free function), ascending head offset.

recursion: Option<WcetRecursionBound>

(#778 phase 4 / #49) Present iff this bound was composed via a verified self-recursion certificate; states the derived depth + frame count.

hint_rejections: Vec<WcetHintRejection>

Hints that were rejected (the static proof stands independently).

hint_key: Option<WcetHintKey>

(#1063) The key --wcet-hints matches this function on, plus its build-locality — filled by the module driver, absent on sidecars predating the field (additive).

Declined

No bound emitted — a loud decline with a machine-readable reason. A decline is emitted (rather than the function omitted) so the map is COMPLETE: a consumer sees every function is either bounded or explicitly unbounded, never silently missing.

Fields

name: String

Function name.

reason: WcetDecline

Machine-readable reason.

note: String

Human-readable note (reason.note()).

op: Option<String>

(#921) The op that caused the decline, as its ArmOp variant name (I64Add, MveDivF32, …). Emitted for unmodeled-op, where the reason alone left a consumer nothing to act on but a hand-bisect.

ADDITIVE and optional: absent for every other reason, and absent when it cannot be determined, so existing consumers are unaffected.

offset: Option<u64>

(#921) Byte offset of that op within the function, from the REAL encoder — the same source of truth WcetLoopBound::head_offset uses, so the two are cross-referenceable in one disassembly.

None when any preceding op is one the encoder refuses: an offset that cannot be computed is OMITTED, never approximated, because a wrong offset sends a consumer to the wrong instruction.

hint_rejections: Vec<WcetHintRejection>

Hints that were offered for this function and rejected.

hint_key: Option<WcetHintKey>

(#1063) The key --wcet-hints matches this function on, plus its build-locality — filled by the module driver, absent on sidecars predating the field (additive).

Implementations

impl WcetFunction

pub fn declined(name: impl Into<String>, reason: WcetDecline) -> Self

Construct a decline, filling in the note from the reason.

pub fn declined_at( name: impl Into<String>, reason: WcetDecline, op: impl Into<String>, offset: Option<u64>, ) -> Self

(#921) Construct a decline that NAMES the offending op and its byte offset. Used for unmodeled-op, whose reason string alone left a consumer with nothing to act on but a hand-bisect of the whole object.

offset is None when the byte position could not be computed from the real encoder; the op name is still emitted, because “which instruction” is the actionable half even without “where”.

pub fn declined_with_rejections( name: impl Into<String>, reason: WcetDecline, hint_rejections: Vec<WcetHintRejection>, ) -> Self

Construct a decline carrying rejected-hint records.

pub fn name(&self) -> &str

The function name this entry is keyed by in the sidecar.

pub fn set_identity(&mut self, display_name: &str, key: &WcetHintKey)

(#1063) Rewrite this entry to its durable identity: the display name plus the hint-key contract the driver assigned. Called by the module driver after composition (composition works in compile names, func_<idx> for internal functions).

Trait Implementations

impl Clone for WcetFunction

fn clone(&self) -> WcetFunction

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for WcetFunction

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for WcetFunction

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for WcetFunction

impl PartialEq for WcetFunction

fn eq(&self, other: &WcetFunction) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl Serialize for WcetFunction

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for WcetFunction