You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: docs/interpreter-plan.md
+33-75Lines changed: 33 additions & 75 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -2,7 +2,7 @@
2
2
3
3
## 1. Motivation
4
4
5
-
The `vmentry_concolic.py` tool contains a ~400-line LLVM IR interpreter tightly coupled to a single value domain (`SymVal` with provenance tracking). The interpreter's opcode dispatch, register routing, pointer resolution, and block/terminator handling are generic — they depend on Striga's lifting conventions, not on the provenance domain. Extracting this interpreter into Striga as a reusable primitive enables multiple analysis backends (concrete emulation, taint tracking, symbolic execution, interval analysis, instruction counting) without reimplementing the same LLVM IR walking logic.
5
+
The `vmentry_concolic.py` tool contains a ~400-line LLVM IR interpreter tightly coupled to a single value domain (`SymVal` with provenance tracking). The interpreter's opcode dispatch, register routing, pointer resolution, and block/terminator handling are generic — they depend on Striga's lifting conventions, not on the provenance domain. Extracting this interpreter into Striga as a reusable primitive enables multiple analysis backends (concrete emulation, taint tracking, symbolic execution, interval analysis, and hook-based profiling) without reimplementing the same LLVM IR walking logic.
6
6
7
7
This document specifies the API shape, the required changes to `Semantics`, the interpreter core, the domain protocols, and concrete examples for each planned use case. Phases 1–3 are intended as the complete implementation specification for the first merge. Phase 4 domain examples are design sketches for follow-up work.
8
8
@@ -149,7 +149,7 @@ class AbstractValueDomain(ValueDomain[T], Protocol[T]):
149
149
"""Extended domain protocol for multi-path fixed-point analysis (future work).
150
150
151
151
Separated from ValueDomain so that single-trace domains (Concrete, Provenance,
152
-
Counting) do not need to stub out methods they will never use. The worklist
152
+
ProfilingHooks) do not need to stub out methods they will never use. The worklist
153
153
driver (section 11) requires this protocol; the single-trace Interpreter does not.
154
154
See section 11 for design context and planned use cases.
**Purpose.** Count operations by type to identify expensive handlers and measure optimization effectiveness.
1387
-
1388
-
**Domain.**
1386
+
**Purpose.** Count executed LLVM operations, stores, and boundary events to identify expensive handlers and measure optimization effectiveness. This is intentionally hook-based rather than a value domain: profiling is about instructions that executed, not about the expression tree that contributed to one result value.
19.Hook-based profiling helpers or examples, if useful.
1568
1527
1569
1528
---
1570
1529
@@ -1580,7 +1539,7 @@ This suite covers BinaryShield, VMProtect, Themida `example2-virt.bin`, `minivm-
1580
1539
1581
1540
Byte-identical `summary.md` comparisons are useful as an optional review aid, but they should not be the primary gate. Refactoring may legitimately improve expression rendering or seed ordering while preserving semantics.
1582
1541
1583
-
Broader interpreter correctness testing (lifting individual instructions, cross-validating against Unicorn, domain protocol compliance) is out of scope for the first implementation. The smoke suite plus `uv run ruff check .` and `uvx ty check` is the acceptance gate.
1542
+
Domain smoke tests should execute lifted instruction sequences, not just call domain helper methods directly. At minimum, cover register writes, memory round-trips, boundary hooks, and one expression-building case for SMT. Cross-validating broad instruction semantics against Unicorn remains out of scope for the first implementation. The smoke suite plus `uv run python tests/test_interpreter_domains.py`, `uv run ruff check .`, and `uvx ty check` is the acceptance gate.
@@ -1714,7 +1672,7 @@ Not all domains are useful in a multi-path setting:
1714
1672
| Taint (`Tainted`) | Yes | Join is label set union; concrete value is lost but taint propagation remains sound |
1715
1673
| Interval | Yes | Join is enclosing interval; this is the classical use case for abstract interpretation |
1716
1674
| SMT | Theoretically | Join is disjunction (`ite`); expressions grow exponentially without simplification |
1717
-
|Counting | No | Cost metrics are path-specific; joining counts from different paths is not meaningful|
1675
+
|Profiling hooks | No | Cost metrics are path-specific; aggregate in the driver instead of joining values|
1718
1676
1719
1677
The practical multi-path domains are intervals and taint. The SMT domain can work but needs aggressive expression simplification at join points to avoid blowup.
0 commit comments