Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 33 additions & 0 deletions docs/god-object-inventory.md
Original file line number Diff line number Diff line change
Expand Up @@ -365,6 +365,39 @@ Flash 1,856,146 -> 1,856,406 (+260)
src.ino 7,483 -> 6,598 lines arduino-cli SUCCESS 58 tests pass
```

## 12. Band 3c — weather and geocache; the proof now checks the moved code itself

**What moved** — the two data domains that consume the sensors:

| unit | owns | functions |
|---|---|---|
| `weather` | `weatherHistory`, `weatherHistoryCount`, `weatherHistoryHead`, `lastWeatherLog`, `weatherTrend`, `weatherLogFileCount`, `weatherLogEntryCount`, `lastFramFlush`; private `lastWeatherLogCheck`; `WeatherReading`, `WeatherTrend`; the three `WEATHER_*` defines | `getCurrentTimestamp`, `getWeatherFilename`, `addToWeatherHistory`, `getWeatherReading`, `logWeatherToFRAM`, `logWeatherReading`, `loadWeatherHistory`, `calculateWeatherTrend`, `getTrendArrow`, `calculateForecast`, `updateWeatherLogStats`, **`framFlushToSD`** |
| `geocache` | `cacheList`, `cacheListCount`, the seven `gcFilter*`/`gcSortMode` settings, `gcCachedDist`, `gcFilteredIndices`, `gcFilteredCount`, `gcLastSortTime`, `listHighlightIndex`; `GeocacheEntry`; `MAX_CACHES` and the four file/size defines | `saveCacheFoundStatus`, `loadCacheFoundStatus`, `decodeROT13`, `extractXMLField`, `extractXMLFloat`, `parseGPXFromString`, `gcUpdateDistances`, `gcApplyFilters`, `loadGeocachesFromSD` |

Four cut-set variables left (`cacheList`, `cacheListCount`, `listHighlightIndex`, `weatherTrend`); `src.ino` 6,598 → 5,808 lines. `framFlushToSD`, held back by 3a, went to `weather` as #272 proposed: it flushes the battery ring and the weather ring, and after 3b both are expressible through `battery.h` and `fram.h`, so `weather` — the higher of the two domains — is the one place it reaches nothing it should not. `lastFramFlush` went with it, published for `loop`. `selectedCacheIndex` and `listScrollOffset` stayed: list-UI state touched only by screen callbacks and buttons, band 4's.

**The proof got stronger.** Until this band the verifier attributed a moved function's size change with the single word "moved" — the bulk of every band's code was the least-checked part of it. It now compares every moved function's reference set before and after: a reference may disappear from the intra-object graph only because its target now lives in a different object, and nothing may appear. All 21 functions of this band pass with every reference kept; three that grew (`loadGeocachesFromSD` +30, `loadCacheFoundStatus` +16, `decodeROT13` +2) are the compiler's inlining and relaxation choices in a smaller unit, with identical references.

**Harness, this band:** default arguments are stripped from a moved definition, since the header's prototype carries them (`parseGPXFromString(…, bool append = false)`); runs of more than two blank lines, which removals leave behind, are collapsed. Eight empty section banners and orphaned comments left by bands 1–3b were removed by hand.

**Measured** — `scripts/verify_extraction.py`, PASS:

```
symbols 589 before -> 589 after, union of 14 objects (no new initialiser: both units hold PODs only)
46 relocated: weather 22, geocache 24
2 linkage changes b -> B, declared: weatherLogFileCount, weatherLogEntryCount
removed none, added none
deltas 18 symbols, net +43: 4 call a moved function, 3 touch published state, 3 moved
functions (references identical), 8 identical references
unexplained: none
moved 21 functions checked by reference set: every reference kept
sections .flash.text +116: our input sections +115 (.text +59, literal pools +56), +1 alignment
.flash.rodata +68: input +188 (string literals now split across two more objects), merged
.dram0.bss +0
Flash 1,856,406 -> 1,856,590 (+184) RAM 103,248 unchanged
src.ino 6,598 -> 5,808 lines arduino-cli SUCCESS 58 tests pass
```

---

## Appendix — the full tables
Expand Down
16 changes: 15 additions & 1 deletion scripts/extract_unit.py
Original file line number Diff line number Diff line change
Expand Up @@ -338,7 +338,14 @@ def inc_line(inc: str) -> str:
cpp.extend(lines[i + 1:var_ends[n] + 1])
for c, d, b, e, n, st in moves:
cpp.append(nl)
cpp.extend(lines[c:e + 1])
for i in range(c, e + 1):
l = lines[i]
if d <= i <= b and not st:
# a default argument may appear once: the header's prototype
# carries it, so the definition must not (parseGPXFromString)
head, sep, tail = l.partition("{")
l = re.sub(r"\s*=\s*[^,)]+(?=\s*[,)])", "", head) + sep + tail
cpp.append(l)

# ---- manifest -------------------------------------------------------------
print(f"unit {unit}: {'header only' if a.header_only else f'{len(moves)} functions'}")
Expand Down Expand Up @@ -402,6 +409,13 @@ def is_comment(i: int) -> bool:
remove.add(k)
k -= 1
out = [l for i, l in enumerate(lines) if i not in remove]
# removals leave runs of blank lines; never more than two in a row
collapsed, blanks = [], 0
for l in out:
blanks = blanks + 1 if l.strip() == "" else 0
if blanks <= 2:
collapsed.append(l)
out = collapsed
inc_idx2 = max(i for i, l in enumerate(out[:200]) if l.startswith("#include"))
out.insert(inc_idx2 + 1, f'#include "{unit}.h"' + nl)

Expand Down
43 changes: 41 additions & 2 deletions scripts/verify_extraction.py
Original file line number Diff line number Diff line change
Expand Up @@ -214,15 +214,38 @@ def refset(g):
return ({norm(c) for c in g["calls"]},
{norm(v) for v in g["vars_ext"] + g["vars_static"]})

after_tag = {dm(s): v[2] for s, v in after.items()} # demangled name -> object it lives in now

def moved_residue(s: str, tag: str):
"""For a function now in object `tag`: references it lost that are NOT
explained by the target living in another object now, plus any gained."""
bg, ag = bgraph.get(s), agraph.get(s)
if bg is None or ag is None:
return None
bc, bv = refset(bg)
ac, av = refset(ag)
lost = (bc - ac) | (bv - av)
gained = (ac - bc) | (av - bv)
cross = {r for r in lost if after_tag.get(r, tag) != tag}
return (lost - cross) | gained, len(cross)

deltas = [(s, before[s], after[s]) for s in set(before) & set(after) if before[s][1] != after[s][1]]
print(f"\n2. size deltas: {len(deltas)} symbols, net {sum(y[1] - x[1] for _, x, y in deltas):+d} bytes")
attributed = collections.Counter()
for s, x, y in sorted(deltas, key=lambda t: (t[2][1] - t[1][1], dm(t[0]))):
k = dm(s)
d = y[1] - x[1]
if base(k) in moved or y[2] != "src":
attributed["moved function itself"] += 1
print(f" {d:+5d} {k[:46]:<46} moved function; relaxation in the new TU")
r = moved_residue(s, y[2])
if r is None:
attributed["moved, not authored"] += 1
print(f" {d:+5d} {k[:46]:<46} moved with its unit; not an authored function")
elif r[0]:
print(f" {d:+5d} {k[:46]:<46} UNEXPLAINED in moved function: {sorted(r[0])}")
ok = False
else:
attributed["moved function itself"] += 1
print(f" {d:+5d} {k[:46]:<46} moved; same references, {r[1]} now cross-TU")
continue
bg, ag = bgraph.get(s), agraph.get(s)
if bg is None or ag is None:
Expand Down Expand Up @@ -257,6 +280,22 @@ def refset(g):
print(f" {d:+5d} {k[:46]:<46} {why}")
print(" attribution:", dict(attributed))

# ---- 2b. every moved function keeps its reference set ------------------
checked, cross_total = 0, 0
for s, (cls, _, tag) in after.items():
if tag == "src" or cls not in "Tt":
continue
r = moved_residue(s, tag)
if r is None:
continue
checked += 1
cross_total += r[1]
if r[0]:
print(f" UNEXPLAINED in moved {dm(s)[:50]}: {sorted(r[0])}")
ok = False
print(f"\n2b. moved functions checked by reference set: {checked}, "
f"{cross_total} references now cross-TU, every other reference kept")

# ---- 3. output sections -------------------------------------------------
if a.before_elf and a.after_elf:
sb, sa = sections(pathlib.Path(a.before_elf)), sections(pathlib.Path(a.after_elf))
Expand Down
Loading