Enum WcetIntermediate 

pub enum WcetIntermediate {
    Declined {
        name: String,
        reason: WcetDecline,
        hint_rejections: Vec<WcetHintRejection>,
    },
    Composable {
        name: String,
        own_cycles: u64,
        instr_count: usize,
        call_sites: Vec<WcetCallSite>,
        loops: Vec<WcetLoopBound>,
        recursion_cert: Option<WcetRecursionCert>,
        hint_rejections: Vec<WcetHintRejection>,
    },
}

The per-function INTERMEDIATE result of the WCET pass BEFORE inter-procedural composition (#778 phase 3). The backend produces one of these per function; the module-level composer (crate::wcet consumers call synth_backend::wcet_compose) resolves each function’s direct call sites against the whole module and emits the final WcetFunction (a composed bound, or a propagated/recursion/indirect decline).

Splitting the pass in two keeps composition a PURE function over already-decided per-function facts: own_cycles already prices every non-call instruction (including each BL’s branch overhead) at its proven execution count, so the composed total is own_cycles + Σ_site multiplier_site × callee_total — the per-site multiplier makes a call inside a proven loop sound by construction.

Variants

Declined

The function declines for a reason INDEPENDENT of composition (an unproven loop, an internal looped expansion, an unsupported core, an unresolved label branch, an indirect call, or an unmodeled op). Carried straight through to a WcetFunction::Declined; composition never rescues these.

Fields

name: String

reason: WcetDecline

hint_rejections: Vec<WcetHintRejection>

Composable

The function’s own body is bounded; its final bound depends only on resolving the recorded direct call sites against the module’s other functions.

Fields

name: String

own_cycles: u64

The summed worst-case cost of every instruction in the final stream (each priced at its documented worst case × its proven execution-count multiplier), INCLUDING each direct BL’s branch overhead. The callee bodies are added by the composer via call_sites.

instr_count: usize

Number of ARM instructions summed (diagnostic, carried to the bound).

call_sites: Vec<WcetCallSite>

The direct call sites to resolve at compose time.

loops: Vec<WcetLoopBound>

Proven loops inside this function (carried to the bound unchanged).

recursion_cert: Option<WcetRecursionCert>

(#778 phase 4 / #49) A proven self-recursion certificate, when this function is a bounded single-self-call chain with a verified depth hint. The composer folds the self-edge as (max_depth+1) × frame_cost instead of declining Recursion. None for a non-recursive function or an unverifiable/unhinted recursion (which still declines).

hint_rejections: Vec<WcetHintRejection>

Hints rejected while analyzing this function (carried to the bound).

Implementations

impl WcetIntermediate

pub fn name(&self) -> &str

The compiled function name this intermediate is for.

Trait Implementations

impl Clone for WcetIntermediate

fn clone(&self) -> WcetIntermediate

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for WcetIntermediate

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

Formats the value using the given formatter.

impl Eq for WcetIntermediate

impl PartialEq for WcetIntermediate

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for WcetIntermediate