Skip to main content

qcode/value/function/
footprint.rs

1//! The precise memory **footprint** lattice value: the persistable half of a
2//! function's memory effect channel.
3//!
4//! These types are produced by `qcode_analysis`'s RAM effect channel
5//! (`calls::argpromote::ram_summary`) and consumed by anything that needs to
6//! know *which addresses* a function may touch rather than merely which spaces.
7//! They live in core — not in the analysis crate that derives them — because
8//! they are persisted on [`MemoryChannelState`](super::MemoryChannelState),
9//! and core cannot depend upward on `qcode_analysis`.
10//!
11//! Ordering is deliberate: the sets are [`BTreeSet`]s, not `FxHashSet`s, so the
12//! serialized form and every iteration over a footprint are deterministic. A
13//! footprint is compared across analysis runs (the effect delta, and the
14//! sliced-vs-full differential harness), and a hash-ordered set would make two
15//! equal footprints render differently.
16
17use std::collections::BTreeSet;
18
19/// What an effect entry's offsets are relative to.
20#[derive(
21    Clone, Copy, Debug, PartialEq, Eq, Hash, PartialOrd, Ord, serde::Serialize, serde::Deserialize,
22)]
23pub enum RamBase {
24    /// The pointer passed at this positional argument index of the summary
25    /// owner's `pure_reg` interface (`param[i] ↔ Call.args[i]` lockstep).
26    Param(u32),
27    /// A slot in the summary owner's **own frame**: a constant offset (`< 0`)
28    /// from its incoming `@SP`. Minted only by the effect channel's `transfer`
29    /// (a callee effect rebased through an own-frame-local argument), always a
30    /// *write*, and dropped again when transferred one level further up — the
31    /// frame dies at return, so the effect is contained.
32    Frame(i64),
33    /// An absolute (literal) address in real ram.
34    Global(u64),
35    /// A **function-private space** landing: a callee effect rebased through a
36    /// call argument that is a pointer into the summary owner's own private
37    /// (shadow/temp) space. Outward-invisible: a private-space object can
38    /// neither be observed nor aliased by any caller, so like a `Frame` write it
39    /// is dropped from the outward footprint.
40    Private,
41}
42
43/// One scalar memory location: `size` bytes at `base + offset`.
44#[derive(
45    Clone, Copy, Debug, PartialEq, Eq, Hash, PartialOrd, Ord, serde::Serialize, serde::Deserialize,
46)]
47pub struct RamField {
48    pub base: RamBase,
49    pub offset: i64,
50    pub size: usize,
51}
52
53/// One bounded dynamic-index effect: the half-open byte span
54/// `[base + lo, base + hi)`.
55#[derive(
56    Clone, Copy, Debug, PartialEq, Eq, Hash, PartialOrd, Ord, serde::Serialize, serde::Deserialize,
57)]
58pub struct RamRegion {
59    pub base: RamBase,
60    pub lo: i64,
61    pub hi: i64,
62}
63
64/// One **whole-object** location: the entire (extent-unknown) object addressed
65/// by `base`. Minted **only**
66/// from an external prototype's pointer parameters; bodied-function scans never
67/// mint object entries (their footprint is exhaustively classified into
68/// fields/regions). `write == true` models a read+write (possibly in-out)
69/// access — the object is both potentially read and clobbered.
70#[derive(
71    Clone, Copy, Debug, PartialEq, Eq, Hash, PartialOrd, Ord, serde::Serialize, serde::Deserialize,
72)]
73pub struct RamObject {
74    pub base: RamBase,
75}
76
77/// One direction of the exhaustively classified memory footprint.
78///
79/// The sets are ordered ([`BTreeSet`]) rather than hashed: this value is
80/// persisted and compared across runs, so its iteration and wire order must not
81/// depend on hash seeding or insertion order.
82#[derive(
83    Clone, Debug, Default, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize,
84)]
85pub struct RamLocations {
86    #[serde(default)]
87    pub fields: BTreeSet<RamField>,
88    #[serde(default)]
89    pub regions: BTreeSet<RamRegion>,
90    #[serde(default)]
91    pub objects: BTreeSet<RamObject>,
92}
93
94impl RamLocations {
95    /// Total number of entries across all three components.
96    pub fn len(&self) -> usize {
97        self.fields.len() + self.regions.len() + self.objects.len()
98    }
99
100    /// Whether the footprint holds no entries at all.
101    pub fn is_empty(&self) -> bool {
102        self.len() == 0
103    }
104
105    /// Whether nothing in this footprint is observable by any caller: empty, or
106    /// `Frame`/`Private`-contained (writes into the owner's own frame, dead at
107    /// return, or into a function-private space). This is the argpromote
108    /// blocking-call gate's admission predicate.
109    pub fn bases_invisible(&self) -> bool {
110        self.fields
111            .iter()
112            .all(|f| matches!(f.base, RamBase::Frame(_) | RamBase::Private))
113            && self
114                .regions
115                .iter()
116                .all(|r| matches!(r.base, RamBase::Frame(_) | RamBase::Private))
117            && self
118                .objects
119                .iter()
120                .all(|o| matches!(o.base, RamBase::Frame(_) | RamBase::Private))
121    }
122}
123
124/// The precise half of a memory summary. Analysis first computes these sets;
125/// materialization may attach SSA values to the same location keys, but must
126/// never add or remove keys.
127#[derive(
128    Clone, Debug, Default, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize,
129)]
130pub struct Footprint {
131    #[serde(default)]
132    pub reads: RamLocations,
133    #[serde(default)]
134    pub writes: RamLocations,
135}
136
137impl Footprint {
138    pub fn len(&self) -> usize {
139        self.reads.len() + self.writes.len()
140    }
141
142    pub fn is_empty(&self) -> bool {
143        self.reads.is_empty() && self.writes.is_empty()
144    }
145
146    pub fn invisible(&self) -> bool {
147        // Reading the owner's fresh frame is not a valid outward effect.
148        self.reads
149            .fields
150            .iter()
151            .all(|f| matches!(f.base, RamBase::Private))
152            && self
153                .reads
154                .regions
155                .iter()
156                .all(|r| matches!(r.base, RamBase::Private))
157            && self
158                .reads
159                .objects
160                .iter()
161                .all(|o| matches!(o.base, RamBase::Private))
162            && self.writes.bases_invisible()
163    }
164}