CSE: Compositional Symbolic Execution for TOSEM paper revision

[Stevengre]

Goal

Implement publication-quality Compositional Symbolic Execution (CSE) for KMIR to produce experimental results for the TOSEM paper revision. CSE summarizes callee functions as K rewrite rules and reuses them across caller proofs.

Architecture

Summary = K rewrite rule matching #execTerminatorCall by function name:

rule <k> #execTerminatorCall(_, FUNC, ARGS, DEST, TARGET, _, _) ~> _CONT
      => #setLocalValue(DEST, RET_VALUE) ~> #continueAt(TARGET)
     </k>
  requires getFunctionName(FUNC) ==String "callee_name"
   andBool PATH_CONSTRAINTS

Requires slotStore (PR #1059) — References use global slot handles, enabling caller-independent summaries.

Acceptance Criteria

#	Criterion	Status
H1	CSE reuse PASSES when baseline PASSES	✅ verified
H2	reuse_splits == baseline_splits	✅ verified
H3	reuse_stuck == 0	✅ verified
H4	reuse_ndbranch == 0	✅ verified
H5	Summary = compiled K rules via add-module	✅ working
H6	Callee proofs complete before export	⚠️ needs enforcement

Current Status (branch: feature/cse-slotstore)

Working: CSE pipeline fires summary rules, 58% depth reduction, proof passes.

Needs work:

• Path constraints and slotStore effects in summary rules
• Argument binding for value-dependent returns
• Callee completeness gate (stuck → no export)
• Full 41-test p-token evaluation with speedup
• Paper artifacts (LaTeX table, CSV)

Spec

See docs/cse-spec.md on branch feature/cse-slotstore.