310 lines
19 KiB
Python
310 lines
19 KiB
Python
#!/usr/bin/env python3
|
||
"""Build the FC11 card source from the shared FreeRTOS C card vocabulary."""
|
||
|
||
import hashlib
|
||
import json
|
||
import subprocess
|
||
import uuid
|
||
from pathlib import Path
|
||
|
||
|
||
ROOT = Path(__file__).resolve().parents[1]
|
||
BASE = ROOT.parent / "lab-rv32i-freertos-c-notifications" / "json" / "card_source.json"
|
||
|
||
|
||
def sha256(path: Path) -> str:
|
||
return hashlib.sha256(path.read_bytes()).hexdigest()
|
||
|
||
|
||
def code_step(step_id, number, label, code_ref, evidence, strategy="code.storage"):
|
||
return {
|
||
"id": step_id, "number": number, "label": label, "mode": "CODE",
|
||
"strategy_ref": strategy, "svg_label": f"{number:02d}",
|
||
"code_ref": code_ref, "description": label, "evidence": evidence,
|
||
}
|
||
|
||
|
||
def run_step(step_id, number, label, event, code_ref, evidence, strategy="run.heap"):
|
||
snapshot = {
|
||
1: "h0", 2: "h1", 3: "h2", 4: "dynamic-run",
|
||
5: "static-run", 6: "dynamic-callback", 7: "static-callback",
|
||
8: "pass",
|
||
}[event]
|
||
return {
|
||
"id": step_id, "number": number, "label": label, "mode": "RUN",
|
||
"event_id": f"E{event:02d}", "strategy_ref": strategy,
|
||
"svg_label": f"{number:02d}", "code_ref": code_ref,
|
||
"snapshot_ref": f"task01.{snapshot}", "description": label,
|
||
"evidence": evidence,
|
||
}
|
||
|
||
|
||
def section(aid, label, title, content, asset, orientation, steps):
|
||
width, height = (940, 560) if orientation == "landscape" else (660, 760)
|
||
return {
|
||
"title": f"{aid} — {label.title()}",
|
||
"order": int(aid[1:]) * 10,
|
||
"content_kind": "prose",
|
||
"asset_page_mode": "one-per-page",
|
||
"page_orientation": orientation,
|
||
"content_tex": content,
|
||
"assets": [{
|
||
"path": f"assets/{asset}.png",
|
||
"html_path": f"assets/{asset}.svg",
|
||
"source_path": f"assets/{asset}.puml",
|
||
"caption": f"{aid} {label} — {title}.",
|
||
"label": f"fig:{asset}",
|
||
"alt": title,
|
||
"kind": "diagram",
|
||
"width": 1.0,
|
||
"page_grid": {
|
||
"columns": 1, "rows": 1, "page_width": width,
|
||
"page_height": height, "overview": True,
|
||
"step_tiles": {s["id"]: 1 for s in steps},
|
||
},
|
||
"interactive": {
|
||
"kind": "uml-class",
|
||
"storage_key": f"fc11-{asset}",
|
||
"title": f"{aid} · {title}",
|
||
"task": {"id": "task01", "label": "Task01 · two storage policies"},
|
||
"block": {"id": aid.lower(), "label": f"{aid} {label}", "description": content},
|
||
"phases": [{"id": label.lower(), "label": title.upper(), "steps": steps}],
|
||
},
|
||
}],
|
||
}
|
||
|
||
|
||
data = json.loads(BASE.read_text())
|
||
card_uuid = str(uuid.uuid5(uuid.NAMESPACE_URL, "stem:freertos-c:fc11:static-allocation"))
|
||
task_uuid = str(uuid.uuid5(uuid.NAMESPACE_URL, "stem:freertos-c:fc11:task01"))
|
||
issued = "2026-07-19T00:00:00+02:00"
|
||
repo_url = "http://77.90.8.171:3001/edu-inf/lab-rv32i-freertos-c-static-allocation"
|
||
html_url = f"https://{card_uuid}/{task_uuid}"
|
||
|
||
data["card"].update({
|
||
"id": "mpabi-freertos-c-11-static-allocation",
|
||
"number": "11", "count": "15", "slug": "static-allocation",
|
||
"title": "Static and dynamic allocation",
|
||
"topic": "task, queue and timer with two storage policies",
|
||
"level": "Rok 2 · L11 · RV32I/Hazard3", "revision_date": issued,
|
||
"version": "v00.01", "uuid": card_uuid,
|
||
})
|
||
data["title_block"].update({
|
||
"title": "Static and dynamic allocation", "url": html_url,
|
||
"repository_url": repo_url, "url_host_uuid": card_uuid,
|
||
"doc_uuid": task_uuid, "issued_on": issued, "series": "FREERTOS-C-11",
|
||
})
|
||
data["front_page_scope"] = {
|
||
"title": "Cel karty",
|
||
"content_tex": "Uczeń rozdziela semantykę obiektu FreeRTOS od polityki przechowywania i dowodzi jej przez adresy oraz cztery pomiary wolnego heap.",
|
||
"scope_title": "Zakres karty",
|
||
"scope_content_tex": "Dynamiczny i statyczny task, queue oraz timer wykonują ten sam eksperyment. H1 jest mniejsze od H0, H2 równa się H1, a H3 równa się H2. Pamięć Idle i timer-service dostarcza aplikacja.",
|
||
"scope_table": {"headers": ["Lekcja", "Task", "Idea", "Priorytet", "Status", "Version"], "rows": [{
|
||
"chapter": "FC11", "task": "Task01", "idea_tex": "behavior parity plus storage provenance",
|
||
"priority": "główny", "status": "ready", "version": "v00.01", "key": True,
|
||
}]},
|
||
}
|
||
data["viewpoints"] = [
|
||
{"id": "A1", "label": "CONTEXT", "subtitle": "ownership boundaries", "status": "enabled", "target_label": "fig:a1-context"},
|
||
{"id": "A2", "label": "STRUCTURE", "subtitle": "dynamic/static object pairs", "status": "enabled", "target_label": "fig:a2-structure"},
|
||
{"id": "A3", "label": "DISPATCH", "subtitle": "same kernel dispatch", "status": "unavailable", "reason": "Storage policy does not change callback dispatch."},
|
||
{"id": "A4", "label": "APPLICATION", "subtitle": "behavior parity", "status": "enabled", "target_label": "fig:a4-application"},
|
||
{"id": "A5", "label": "FLOW", "subtitle": "H0/H1/H2/H3", "status": "enabled", "target_label": "fig:a5-flow"},
|
||
{"id": "A6", "label": "STATE", "subtitle": "covered by flow", "status": "unavailable", "reason": "No new lifecycle state machine; the card compares storage."},
|
||
{"id": "A7", "label": "RUNTIME", "subtitle": "address provenance", "status": "enabled", "target_label": "fig:a7-runtime"},
|
||
{"id": "A8", "label": "PATTERNS", "subtitle": "policy comparison", "status": "unavailable", "reason": "No wrapper pattern is introduced in this C card."},
|
||
]
|
||
data["debug_strategies"] = {
|
||
"code.storage": {
|
||
"id": "code.storage", "kind": "code", "action": "open",
|
||
"expected_observations": ["persistent Static* buffers", "application static Idle/timer task memory"],
|
||
"assertions": ["no local-lifetime storage", "both allocation modes enabled"],
|
||
"evidence_fields": ["symbol", "section", "code_ref"], "prerequisites": ["FC11 source"],
|
||
"layout": ["buffers", "create APIs", "FreeRTOSConfig"],
|
||
"commands": ["rg -n 'x.*CreateStatic|vApplicationGet.*TaskMemory|Static(Task|Queue|Timer)_t' include src"],
|
||
},
|
||
"run.heap": {
|
||
"id": "run.heap", "kind": "run", "action": "replay",
|
||
"expected_observations": ["H1 < H0", "H2 == H1", "H3 == H2"],
|
||
"assertions": ["objects alive at H3", "no exact delta assumption"],
|
||
"evidence_fields": ["H0", "H1", "H2", "H3", "timestamp"],
|
||
"prerequisites": ["clean Hazard3 RAM"], "layout": ["heap values", "event order"],
|
||
"commands": ["print g_fc11.heap_h0", "print g_fc11.heap_h1", "print g_fc11.heap_h2", "print g_fc11.heap_h3"],
|
||
},
|
||
"run.parity": {
|
||
"id": "run.parity", "kind": "run", "action": "replay",
|
||
"expected_observations": ["both receive 0xCAFE", "both timers callback once"],
|
||
"assertions": ["distinct stacks", "PASS and deterministic digest"],
|
||
"evidence_fields": ["received", "timer calls", "SP", "digest"],
|
||
"prerequisites": ["scheduler running"], "layout": ["two branches", "verifier"],
|
||
"commands": ["print/x g_fc11.dynamic_received", "print/x g_fc11.static_received", "print g_fc11_pass"],
|
||
},
|
||
}
|
||
|
||
a1 = [
|
||
code_step("application", 1, "application owns experiment", "src/tasks/task01_static_allocation.c:20", "global experiment"),
|
||
code_step("dynamic", 2, "dynamic APIs request storage", "src/tasks/task01_static_allocation.c:218", "xTaskCreate/xQueueCreate/xTimerCreate"),
|
||
code_step("static", 3, "static APIs receive storage", "src/tasks/task01_static_allocation.c:239", "named buffers"),
|
||
code_step("kernel", 4, "kernel owns object semantics", "vendor/FreeRTOS-Kernel/tasks.c:1", "same scheduler"),
|
||
code_step("ram", 5, "both policies coexist in RAM", "src/tasks/task01_static_allocation.c:26", "ucHeap plus static buffers"),
|
||
]
|
||
a2 = [
|
||
run_step("dynamic-task", 1, "dynamic task handle is in heap", 2, "src/tasks/task01_static_allocation.c:218", "heap address"),
|
||
run_step("static-task", 2, "static task uses TCB and stack buffers", 3, "src/tasks/task01_static_allocation.c:239", "outside heap"),
|
||
run_step("dynamic-queue", 3, "dynamic queue object is in heap", 2, "src/tasks/task01_static_allocation.c:228", "heap address"),
|
||
run_step("static-queue", 4, "static queue uses supplied storage", 3, "src/tasks/task01_static_allocation.c:247", "outside heap"),
|
||
run_step("dynamic-timer", 5, "dynamic timer object is in heap", 2, "src/tasks/task01_static_allocation.c:229", "heap address"),
|
||
run_step("static-timer", 6, "static timer uses StaticTimer_t", 3, "src/tasks/task01_static_allocation.c:250", "outside heap"),
|
||
code_step("services", 7, "Idle and timer-service storage is static", "src/tasks/task01_static_allocation.c:45", "two application callbacks"),
|
||
]
|
||
a4 = [
|
||
run_step("dynamic-worker", 1, "dynamic branch receives message", 4, "src/tasks/task01_static_allocation.c:121", "0xCAFE", "run.parity"),
|
||
run_step("static-worker", 2, "static branch receives message", 5, "src/tasks/task01_static_allocation.c:139", "0xCAFE", "run.parity"),
|
||
run_step("daemon", 3, "daemon executes both callbacks", 7, "src/tasks/task01_static_allocation.c:99", "1 + 1", "run.parity"),
|
||
run_step("verifier", 4, "verifier checks behavior parity", 8, "src/tasks/task01_static_allocation.c:157", "PASS", "run.parity"),
|
||
]
|
||
a5 = [
|
||
run_step("h0", 1, "H0 baseline", 1, "src/tasks/task01_static_allocation.c:214", "baseline"),
|
||
run_step("h1", 2, "dynamic objects make H1 smaller", 2, "src/tasks/task01_static_allocation.c:236", "H1 < H0"),
|
||
run_step("h2", 3, "static objects leave heap unchanged", 3, "src/tasks/task01_static_allocation.c:263", "H2 = H1"),
|
||
run_step("dynamic-run", 4, "dynamic worker runs", 4, "src/tasks/task01_static_allocation.c:121", "message" , "run.parity"),
|
||
run_step("static-run", 5, "static worker runs", 5, "src/tasks/task01_static_allocation.c:139", "message", "run.parity"),
|
||
run_step("dynamic-callback", 6, "dynamic timer callback", 6, "src/tasks/task01_static_allocation.c:99", "count 1", "run.parity"),
|
||
run_step("static-callback", 7, "static timer callback", 7, "src/tasks/task01_static_allocation.c:99", "count 1", "run.parity"),
|
||
run_step("pass", 8, "H3 unchanged and verifier passes", 8, "src/tasks/task01_static_allocation.c:157", "H3 = H2", "run.parity"),
|
||
]
|
||
a7 = [
|
||
run_step("heap-arena", 1, "dynamic handles lie in ucHeap", 8, "src/tasks/task01_static_allocation.c:174", "three true predicates"),
|
||
run_step("named-buffers", 2, "static handles lie outside ucHeap", 8, "src/tasks/task01_static_allocation.c:177", "three false predicates"),
|
||
code_step("service-buffers", 3, "kernel-service buffers are named", "src/tasks/task01_static_allocation.c:34", "Idle and daemon buffers"),
|
||
run_step("heap-relation", 4, "four checkpoints satisfy relation", 8, "include/task01_static_allocation_model.h:34", "H1<H0; H2=H1; H3=H2"),
|
||
run_step("evidence", 5, "commit-last evidence is deterministic", 8, "src/tasks/task01_static_allocation.c:72", "cdf44a0a", "run.parity"),
|
||
]
|
||
data["sections"] = [
|
||
section("A1", "CONTEXT", "ownership boundaries", "Application, kernel and RAM responsibilities are explicit.", "a1-context", "portrait", a1),
|
||
section("A2", "STRUCTURE", "object pairs", "Task, queue and timer are compared pairwise.", "a2-structure", "landscape", a2),
|
||
section("A4", "APPLICATION", "behavior parity", "Storage differs while application behavior remains equal.", "a4-application", "portrait", a4),
|
||
section("A5", "FLOW", "four heap checkpoints", "H0/H1/H2/H3 bracket creation and scheduler startup.", "a5-flow", "landscape", a5),
|
||
section("A7", "RUNTIME", "address provenance", "Debugger evidence connects handles to heap or named buffers.", "a7-runtime", "portrait", a7),
|
||
{"title": "Task01 — two storage policies", "order": 90, "content_kind": "tasks", "task_refs": ["task01"]},
|
||
]
|
||
data["tasks_order"] = ["task01"]
|
||
data["tasks"] = {"task01": {
|
||
"title": "Same behavior, two storage policies", "uuid": task_uuid,
|
||
"prompt_tex": "Przejdź po A1, A2, A4, A5 i A7. Odtwórz E01–E08 oraz udowodnij relacje H1<H0, H2=H1 i H3=H2.",
|
||
"criterion": "PASS; address provenance; message and callback parity; deterministic digest.",
|
||
"conclusion_tex": "Statyczne API zmienia własność pamięci, ale nie semantykę taska, kolejki ani timera.",
|
||
"flow": [
|
||
{"kind": "block", "id": "predict", "title": "A — przewidywanie", "content_tex": "Przewidź cztery pomiary heap.", "steps": [
|
||
{"id": "relation", "title": "Zapisz relacje H0–H3.", "content_tex": "Nie zakładaj dokładnej liczby bajtów."},
|
||
{"id": "ownership", "title": "Wskaż właściciela pamięci.", "content_tex": "Rozdziel ucHeap i named buffers."},
|
||
]},
|
||
{"kind": "block", "id": "replay", "title": "B — replay Hazard3", "content_tex": "Wykonaj E01–E08 z clean RAM.", "steps": [
|
||
{"id": "heap", "title": "Zbadaj H0/H1/H2/H3.", "content_tex": "Zapisz wartości i relacje."},
|
||
{"id": "parity", "title": "Zbadaj obie gałęzie.", "content_tex": "Porównaj message, timer callback i stack."},
|
||
{"id": "pass", "title": "Zbadaj E08.", "content_tex": "Zapisz PASS, digest i timestamp."},
|
||
]},
|
||
{"kind": "exercise", "id": "choose-policy", "title": "Ćwiczenie — wybór polityki", "prompt_tex": "Dla taska okresowego, kolejki telemetrycznej i timera bezpieczeństwa wybierz dynamiczne albo statyczne tworzenie. Uzasadnij lifetime i ownership.", "evidence_tex": "Tabela obiekt→API→storage→lifetime oraz ślad H0–H3.", "criterion": "Każdy bufor ma trwałość co najmniej tak długą jak obiekt kernelowy.", "based_on": ["predict", "replay"]},
|
||
],
|
||
"educational_requirement_refs": ["FC11.WE01"], "learning_effect_refs": ["FC11.EN01", "FC11.EK01"], "assessment_criterion_ref": "FC11.KW01",
|
||
}}
|
||
|
||
elf = ROOT / "build/task01_static_allocation/prog.elf"
|
||
image = ROOT / "build/task01_static_allocation/prog.bin"
|
||
blob = subprocess.check_output(["git", "hash-object", "src/tasks/task01_static_allocation.c"], cwd=ROOT, text=True).strip()
|
||
items = {}
|
||
checks = {
|
||
1: ("h0", ["g_fc11_event_count", 1]),
|
||
2: ("h1", ["g_fc11.heap_h1 < g_fc11.heap_h0", 1]),
|
||
3: ("h2", ["g_fc11.heap_h2 == g_fc11.heap_h1", 1]),
|
||
4: ("dynamic-run", ["g_fc11.dynamic_received", 0xCAFE]),
|
||
5: ("static-run", ["g_fc11.static_received", 0xCAFE]),
|
||
6: ("dynamic-callback", ["g_fc11.dynamic_timer_calls", 1]),
|
||
7: ("static-callback", ["g_fc11.static_timer_calls", 1]),
|
||
8: ("pass", ["g_fc11_pass", 1]),
|
||
}
|
||
for event, (name, check) in checks.items():
|
||
items[f"task01.{name}"] = {
|
||
"event_id": f"E{event:02d}",
|
||
"stop": {"symbol": "fc11_checkpoint_committed", "offset": 0, "condition": f"$a0 == {event}"},
|
||
"verify": {"expressions": [{"expr": check[0], "equals": check[1]}]},
|
||
}
|
||
data["debug_checkpoints"] = {
|
||
"schema": "stem-debug-checkpoints.v1", "semantics": "deterministic-replay",
|
||
"artifact": {"source": "src/tasks/task01_static_allocation.c", "source_git_blob": blob,
|
||
"elf": "build/task01_static_allocation/prog.elf", "hazard3_elf_sha256": sha256(elf),
|
||
"hazard3_image": "build/task01_static_allocation/prog.bin", "hazard3_image_sha256": sha256(image)},
|
||
"targets": {"hazard3-sim": {"adapter": "hazard3-reset-load-replay.v1", "baseline": "restart-backend", "clean_ram": True}},
|
||
"items": items,
|
||
}
|
||
data["educational_requirements"] = {"FC11.WE01": {
|
||
"text": "Porównanie dynamicznej i statycznej polityki pamięci obiektów FreeRTOS.", "label": "storage policy and behavior parity",
|
||
"learning_effects": ["FC11.EN01", "FC11.EK01"], "learning_tree": {
|
||
"schema": "we-learning-tree.v1", "policy": "Każda aktywna kotwica wskazuje kod lub checkpoint.",
|
||
"ogolne": [{"effect_ref": "FC11.EN01", "display": "EN LOCAL RTOS.11", "source": "LOCAL", "official": "RTOS", "local": "11", "kind": "EN", "tree_id": "FC11.WE01.OG.LOCAL.RTOS.11", "text": "Uczeń rozdziela semantykę obiektu i politykę przechowywania.", "kw": [{"criterion_ref": "FC11.KW01", "display": "KW LOCAL RTOS.11", "source": "LOCAL", "kind": "KW", "official": "RTOS", "local": "11", "text": "Łączy kod, diagram i dowód runtime."}]}],
|
||
"zawodowe": [{"effect_ref": "FC11.EK01", "display": "EK LOCAL RTOS.11", "source": "LOCAL", "official": "RTOS", "local": "11", "kind": "EK", "tree_id": "FC11.WE01.TECH.LOCAL.RTOS.11", "text": "Uczeń odtwarza E01–E08 i dowodzi H1<H0, H2=H1, H3=H2.", "kw": [{"criterion_ref": "FC11.KW01", "display": "KW LOCAL RTOS.11", "source": "LOCAL", "kind": "KW", "official": "RTOS", "local": "11", "text": "Łączy kod, diagram i dowód runtime."}]}],
|
||
},
|
||
}}
|
||
data["learning_effects"] = {
|
||
"FC11.EN01": {"bloom_level": "Analiza", "label": "Storage ownership", "text": "Uczeń rozdziela semantykę obiektu i politykę przechowywania.", "assessment_criteria": ["FC11.KW01"]},
|
||
"FC11.EK01": {"bloom_level": "Zastosowanie", "label": "Heap replay", "text": "Uczeń odtwarza E01–E08 i dowodzi H1<H0, H2=H1, H3=H2.", "assessment_criteria": ["FC11.KW01"]},
|
||
}
|
||
data["assessment_criteria"] = {"FC11.KW01": {"text": "PASS; address provenance; message and callback parity; deterministic digest.", "learning_effects": ["FC11.EN01", "FC11.EK01"]}}
|
||
|
||
spec_sections = []
|
||
for expanded in data["sections"]:
|
||
if expanded.get("content_kind") == "tasks":
|
||
continue
|
||
aid = expanded["title"].split()[0]
|
||
asset = expanded["assets"][0]
|
||
interactive = asset["interactive"]
|
||
stem = Path(asset["path"]).stem
|
||
spec_asset = {
|
||
"stem": stem,
|
||
"title": interactive["title"],
|
||
"caption": asset["caption"],
|
||
"label": asset["label"],
|
||
"alt": asset["alt"],
|
||
"phases": interactive["phases"],
|
||
}
|
||
if aid == "A5":
|
||
spec_asset["diagram_kind"] = "sequence"
|
||
spec_sections.append({
|
||
"id": aid,
|
||
"label": interactive["block"]["label"].split(maxsplit=1)[1],
|
||
"title": expanded["title"].split("—", 1)[1].strip(),
|
||
"order": expanded["order"],
|
||
"orientation": expanded["page_orientation"],
|
||
"description": interactive["block"]["description"],
|
||
"content_tex": expanded["content_tex"],
|
||
"assets": [spec_asset],
|
||
})
|
||
|
||
task = data["tasks"]["task01"]
|
||
spec = {
|
||
"card": {key: data["card"][key] for key in ("number", "slug", "title", "topic", "status", "version")},
|
||
"front": {"goal": data["front_page_scope"]["content_tex"], "scope": data["front_page_scope"]["scope_content_tex"]},
|
||
"viewpoints": [{key: value[key] for key in ("id", "label", "status", "subtitle", "reason") if key in value} for value in data["viewpoints"]],
|
||
"artifact": {"source": "src/tasks/task01_static_allocation.c", "elf": "build/task01_static_allocation/prog.elf", "image": "build/task01_static_allocation/prog.bin"},
|
||
"strategies": list(data["debug_strategies"].values()),
|
||
"checkpoints": data["debug_checkpoints"]["items"],
|
||
"sections": spec_sections,
|
||
"learning": {
|
||
"model_label": data["learning_effects"]["FC11.EN01"]["label"],
|
||
"model": data["learning_effects"]["FC11.EN01"]["text"],
|
||
"replay_label": data["learning_effects"]["FC11.EK01"]["label"],
|
||
"replay": data["learning_effects"]["FC11.EK01"]["text"],
|
||
"criterion": data["assessment_criteria"]["FC11.KW01"]["text"],
|
||
"requirement": data["educational_requirements"]["FC11.WE01"]["text"],
|
||
},
|
||
"task": {
|
||
"short_label": "two storage policies",
|
||
"title": task["title"], "prompt_tex": task["prompt_tex"],
|
||
"conclusion_tex": task["conclusion_tex"], "flow": task["flow"],
|
||
},
|
||
}
|
||
|
||
out = ROOT / "json/card_spec.json"
|
||
out.write_text(json.dumps(spec, ensure_ascii=False, indent=2) + "\n")
|
||
print(out)
|