Clarify and redesign dataflow analysis magic numbers for memory keys and worklist iteration limits

[snowykr]

Summary

The dataflow analysis currently relies on several magic numbers in snx/dataflow.py:

1. A hard-coded base value 1000 to distinguish static memory locations from stack slots in _get_stack_slot_key.
2. Two hard-coded iteration limits (* 10 and 20) to bound the worklist dataflow fixpoint iteration.

These values are not documented, are not tied to the architecture's defined constraints, and may hide real design issues in the dataflow domain (especially around sp_offset growth and memory modeling).

---

Details

1. Magic number 1000 in _get_stack_slot_key

def _get_stack_slot_key(self, addr_op: AddressOperand, state: AbstractState) -> int | None:
    if addr_op.base.index == 3:
        return state.sp_offset + addr_op.offset
    elif addr_op.base.index == 0:
        return 1000 + addr_op.offset
    return None

• $3-based addresses are treated as stack slots:
  key_stack = state.sp_offset + offset
• $0-based addresses are treated as static memory:
  key_static = 1000 + offset

The intent seems to be to store both stack and static memory locations in a single map (stack_slots: dict[int, ValueState]) by partitioning the key space.

However:

• The constant 1000 is not documented anywhere (code, comments, or README).
• sp_offset is an unbounded integer that can grow arbitrarily large via repeated LDA $3, k($3) instructions. There is no invariant guaranteeing that sp_offset + offset will never overlap with 1000 + offset' for some offsets.
• As a result, stack and static memory keys can, in principle, collide, and nothing in the current implementation prevents that.

This is more than a style issue: it is an ad-hoc encoding of two different memory domains into a single integer domain without a sound separation.

2. Magic numbers 10 and 20 in the worklist iteration

worklist = [entry_pc]
visited_count: dict[int, int] = {}
max_iterations = len(self._ir_program.instructions) * 10

while worklist and max_iterations > 0:
    max_iterations -= 1
    pc = worklist.pop(0)

    if pc not in self._inst_by_pc:
        continue

    visited_count[pc] = visited_count.get(pc, 0) + 1
    if visited_count[pc] > 20:
        continue

    inst = self._inst_by_pc[pc]
    in_state = self._states.get(pc, AbstractState())
    out_state, successors = self._transfer(inst, in_state)
    ...

The dataflow lattice is:

• Finite for ValueState (UNINIT, DATA, RETURN_ADDR, UNKNOWN).
• Unbounded for sp_offset: int, which is updated on LDA $3, k($3) and merged via max(self.sp_offset, other.sp_offset).

Because sp_offset can strictly increase along cycles, the fixpoint iteration may never stabilize in theory. The current implementation addresses this by:

• A global iteration cap: len(instructions) * 10.
• A per-PC visit cap: at most 20 visits per PC.

Effects:

• The analysis can terminate before reaching a true fixpoint.
• Some PCs may never be analyzed, or may end up with under-propagated (over-approximate) states.
• This may lead to:
  • True reachable PCs being flagged as unreachable_pcs.
  • Extra D001/D002-style diagnostics for memory reads that would be initialized if the analysis ran to a proper fixpoint.
  • Potentially, missed diagnostics in more subtle cases.

Again, these constants are not documented and are not obviously derived from any property of the CFG or the abstract domain; they act as an implicit "timeout" for the analysis.

---

Why this matters

• The current magic numbers encode important semantic distinctions (stack vs static memory, termination of the analysis) in a way that is not explicit or robust.
• They make the behavior of the analysis dependent on arbitrary thresholds rather than on well-defined abstract domains and proven convergence.
• This can lead to:
  • Non-obvious false positives/false negatives in diagnostics.
  • Fragile behavior when the architecture or simulator configuration changes (e.g., larger memory, different stack discipline).

---

Proposed direction

This issue suggests two levels of improvement:

Short-term (low-risk cleanups)

1. Introduce named constants and document their purpose

   • Example:

     _STATIC_MEMORY_KEY_BASE = 1000
     _MAX_ITERATIONS_MULTIPLIER = 10
     _MAX_VISITS_PER_PC = 20

   • Use these in _get_stack_slot_key and in the worklist loop.
   • Add concise comments explaining:
     • Why static memory keys are offset from stack keys.
     • That the iteration limits are currently a heuristic to avoid potential non-termination.

2. Expose iteration limits as configuration

   • Allow DataflowAnalyzer (and/or analyze_dataflow) to receive optional parameters for these limits, so tests/benchmarks can tune them or set them higher/lower if needed.

3. Track when limits are hit

   • Internally record whether the global iteration cap or per-PC visit cap was reached.
   • (Optionally) surface this in DataflowResult (e.g., as flags or a list of PCs) to make it visible when the analysis exited early.

Longer-term (design-level improvements)

1. Use an explicit memory slot domain instead of integer key hacks

   • Replace int keys with something like:

     @dataclass(frozen=True, slots=True)
     class MemorySlot:
         kind: Literal["stack", "static"]
         index: int

     or a simple tagged tuple.
   • Store stack_slots: dict[MemorySlot, ValueState].
   • Have _get_stack_slot_key (renamed to something like _get_memory_slot) return distinct slots for stack vs static memory without relying on numeric separation.

2. Make sp_offset a finite abstract domain

   • Instead of using unbounded integers, introduce a bounded or categorized abstraction for the stack pointer offset (e.g., exact small offsets vs. a saturated "too deep" / "unknown" category).
   • Ensure that the combined abstract state lattice is finite and that join operations are monotone, so that fixpoint iteration is guaranteed to terminate without arbitrary iteration caps.

3. Revisit the worklist fixpoint strategy

   • Once the domain is finite, the main loop can be driven by "no state changed" rather than by iteration counts.
   • Any remaining iteration caps can then be kept as a last-resort safeguard rather than a primary correctness mechanism.

---

Additional context

• Runtime semantics (SNXSimulator) treat memory as a single 128-word array with no explicit distinction between stack and static regions.
• The dataflow analysis introduces a conceptual separation (stack via $3, static via $0) purely for tracking initialization and return-address correctness, but currently encodes this via ad-hoc integer ranges.
• The README documents $0–$3 and basic instruction semantics but does not yet describe the dataflow memory model or its limitations.