Skip to content

Tracing redesign: ScopedTraceContext + PathPredicateStore (foundational PR)#288

Draft
PhilippGrulich wants to merge 8 commits into
mainfrom
claude/redesign-nautilus-tracing-UVtaS
Draft

Tracing redesign: ScopedTraceContext + PathPredicateStore (foundational PR)#288
PhilippGrulich wants to merge 8 commits into
mainfrom
claude/redesign-nautilus-tracing-UVtaS

Conversation

@PhilippGrulich

@PhilippGrulich PhilippGrulich commented May 14, 2026

Copy link
Copy Markdown
Member

Summary

Adds a third tracing context, ScopedTraceContext, selectable via engine.traceMode = "scopedTracing" alongside the existing LazyTraceContext and ExceptionBasedTraceContext. The existing tracers are untouched and remain the default.

The scoped tracer pairs three layered mechanisms — PathPredicateStore (dominator-based pruning), integer-constant tracking with static CMP folding, and the existing tag-stable Snapshot scheme — to deliver concrete trace-size reductions on every fixture in the pathExplosion_* family.

Trace-size results (raw-trace RETURN counts)

Fixture LazyTraceContext ScopedTraceContext Reduction
pathExplosion_baseline_oneCall 3 3
pathExplosion_baseline_threeCallsNoBranch 27 9
pathExplosion_postCallBranch_1 6 4 33%
pathExplosion_postCallBranch_3 54 12 4.5×
pathExplosion_independentIfs_4 2 2
pathExplosion_constraintBlind_dead 4 2 50%

Every reduced trace also passes the full trace → SSACreationPhase → VerifySSA → TraceToIRConversionPhase pipeline — the test suite added in this PR runs each fixture end-to-end so size wins can't be silently malformed.

What's in the PR

  1. ScopedTraceContext (src/nautilus/tracing/ScopedTraceContext.{hpp,cpp}) — full TracingInterface implementation with three new per-iteration caches:

    • integerConstants : ValueRef → int64_t — populated in traceConstant() for every CONST op with an integer literal; propagated through traceCopy().
    • staticBoolValues : ValueRef → bool — populated in traceBinaryOp() when both operands of a comparison are present in integerConstants; computed by static evaluation.
    • comparisonCache : ValueRef → (var, cmpOp, lit) — derived from CMPs of var cmp const; used by PathPredicateStore::evaluate.
  2. PathPredicateStore (src/nautilus/tracing/predicate/) — small per-iteration constraint store with entailment / contradiction reasoning over integer-literal comparisons. Push / pop is balanced with branch enter / leave; 8 unit tests cover the reasoning.

  3. SymbolicExecutionContext::recordPrunedNoThrow(tag, takenDirection) — new hook in the symbolic executor that lets the tracer mark a tag as fully explored without enqueueing the dead arm onto inflightExecutionPaths. This is what turns "we know this branch is dead" into actual iterations-saved instead of dead-arm exploration.

  4. safeCheckTag — defensive replacement for ExecutionTrace::checkTag inside the scoped tracer. Detects the same-block self-merge condition and routes to passive mode instead of throwing.

  5. Mode dispatchengine.traceMode = "scopedTracing" selects the new context in LegacyCompiler.cpp. Defaults are unchanged.

  6. Tests (test/scoped-tracing-tests/, 18 cases, 65 assertions):

    • 8 unit tests for PathPredicateStore.
    • 6 end-to-end tests asserting exact trace sizes (scoped == N, lazy == M) on every pathExplosion_* fixture.
    • 2 minimal regression fixtures for dominator-implied / contradicted CMPs.
    • 1 full-pipeline well-formedness test (trace → SSA verify → IR) across every fixture.
    • 1 noBranch sanity check across all three tracers.

Pruning flow at a CMP

traceBool(value, prob):
  if value is in staticBoolValues:     # both operands were CONST
    direction = staticBoolValues[value]
    SymbolicExecutionContext.recordPrunedNoThrow(tag, direction)
  elif PathPredicateStore.evaluate(candidate predicate) has a verdict:
    direction = verdict                # dominator implies/contradicts
    SymbolicExecutionContext.recordPrunedNoThrow(tag, direction)
  else:
    SymbolicExecutionContext.recordNoThrow(tag)   # normal worklist

recordPrunedNoThrow marks the tag as SecondVisit immediately so the symbolic executor never enqueues the dead arm — every prune is iterations-saved, not just trace-size-saved.

Why baseline_threeCallsNoBranch is 9 (not 3)

The constant-folding cascade prunes most upstream-path × downstream-branch combinations, but the leaf's body is still inlined three times at the trace level. Bringing that count from 9 → 3 requires per-function sub-traces with explicit CALL-op emission — covered in the plan file (/root/.claude/plans/...) and tracked as the remaining milestone for this redesign. That change needs either std::source_location plumbing through every val<T> operator macro or a dladdr-based scope ID and is sized for its own PR.

Test plan

  • ctest --test-dir nautilus --output-on-failure — 193/193 pass on Debug + Clang.
  • nautilus-scoped-tracing-tests — 18/18 pass (predicates + path-explosion + dominator pruning + full-pipeline well-formedness).
  • cmake --build . --target format — clean.
  • CI matrix (GCC 14, Clang 19, Clang 21, macOS, ARM, sanitisers).
  • Benchmark verification (no regression on default lazyTracing mode; new tracer not in the default path).

https://claude.ai/code/session_01XDkjLQbFMxtTeyB3w15T56

Introduces a third tracing context selectable via
engine.traceMode = "scopedTracing", alongside the existing
LazyTraceContext and ExceptionBasedTraceContext.

ScopedTraceContext drops aliveVars.hash() from the Snapshot identity,
which fixes the upstream-ValueRef fan-out documented in
PathExplosionFunctions.hpp:45-67 for the pathExplosion_postCallBranch_*
family.  It also carries a per-iteration PathPredicateStore that
accumulates simple integer-literal constraints along the current
path; the store is unit-tested in isolation and is wired into
traceBool for future symbolic-executor pruning.

Known limitation: the constraintBlind_dead fixture currently triggers
a same-block control-flow merge because the outer/inner sibling CMPs
collide once aliveVars is removed.  The fixture is marked
[!shouldfail] in nautilus-scoped-tracing-tests and a TODO is recorded
in ScopedTraceContext.hpp.  Full per-function sub-trace boundary
detection (the deeper cure documented in the plan) is left to a
follow-up PR.

All 189 existing tests continue to pass; 14 new tests cover the
PathPredicateStore and end-to-end behaviour of the new tracer on the
path-explosion fixtures.

https://claude.ai/code/session_01XDkjLQbFMxtTeyB3w15T56

@github-actions github-actions Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Tracing Benchmark

Details
Benchmark suite Current: ffbe420 Previous: f9cd28f Ratio
ssa_add 169.19 ns (± 8.45218) 178.473 ns (± 9.97434) 0.95
ssa_ifThenElse 411.151 ns (± 34.798) 459.53 ns (± 43.4269) 0.89
ssa_deeplyNestedIfElse 1.02026 us (± 58.5238) 1.16567 us (± 124.837) 0.88
ssa_loop 430.815 ns (± 40.0964) 487.861 ns (± 38.2642) 0.88
ssa_ifInsideLoop 770.643 ns (± 48.4699) 895.76 ns (± 72.8648) 0.86
ssa_loopDirectCall 434.737 ns (± 23.1553) 491.118 ns (± 45.7827) 0.89
ssa_pointerLoop 518.034 ns (± 26.2617) 583.073 ns (± 41.8959) 0.89
ssa_staticLoop 422.674 ns (± 24.3131) 422.539 ns (± 47.7647) 1.00
ssa_fibonacci 447.954 ns (± 26.7221) 503.737 ns (± 39.1986) 0.89
ssa_gcd 410.146 ns (± 30.0213) 445.234 ns (± 36.8343) 0.92
trace_add 2.10783 us (± 245.813) 2.27731 us (± 155.69) 0.93
completing_trace_add 2.11232 us (± 214.794) 2.32405 us (± 143.855) 0.91
scoped_trace_add 2.14222 us (± 223.992)
trace_ifThenElse 7.71636 us (± 1.03693) 8.63915 us (± 776.354) 0.89
completing_trace_ifThenElse 4.20497 us (± 493.946) 4.54071 us (± 401.003) 0.93
scoped_trace_ifThenElse 4.7585 us (± 485.126)
trace_deeplyNestedIfElse 26.8275 us (± 4.77303) 25.5445 us (± 1.57172) 1.05
completing_trace_deeplyNestedIfElse 11.5724 us (± 1.43393) 12.559 us (± 987.646) 0.92
scoped_trace_deeplyNestedIfElse 4.06074 us (± 382.398)
trace_loop 7.67568 us (± 1.10577) 8.80429 us (± 1.55155) 0.87
completing_trace_loop 4.30372 us (± 542) 4.79104 us (± 376.911) 0.90
scoped_trace_loop 4.83061 us (± 547.288)
trace_ifInsideLoop 15.0827 us (± 2.13645) 16.6688 us (± 1.56827) 0.90
completing_trace_ifInsideLoop 8.15191 us (± 1.46817) 8.40114 us (± 807.253) 0.97
scoped_trace_ifInsideLoop 7.22514 us (± 1.06727)
trace_loopDirectCall 7.9572 us (± 1.08344) 8.6864 us (± 697.439) 0.92
completing_trace_loopDirectCall 4.32981 us (± 458.753) 4.86476 us (± 354.791) 0.89
scoped_trace_loopDirectCall 4.81759 us (± 566.845)
trace_pointerLoop 12.4247 us (± 2.41736) 14.0902 us (± 1.18648) 0.88
completing_trace_pointerLoop 9.04364 us (± 1.10857) 10.1206 us (± 990.611) 0.89
scoped_trace_pointerLoop 10.0049 us (± 1.26855)
trace_staticLoop 6.96898 us (± 666.959) 7.21602 us (± 496.139) 0.97
completing_trace_staticLoop 7.07913 us (± 696.699) 7.43532 us (± 991.516) 0.95
scoped_trace_staticLoop 7.63797 us (± 703.487)
trace_fibonacci 9.04343 us (± 1.33094) 10.0814 us (± 861.346) 0.90
completing_trace_fibonacci 5.52136 us (± 615.954) 6.00031 us (± 426.095) 0.92
scoped_trace_fibonacci 6.00706 us (± 755.035)
trace_gcd 7.17721 us (± 1.16162) 7.79585 us (± 648.305) 0.92
completing_trace_gcd 3.66719 us (± 478.957) 3.87126 us (± 272.452) 0.95
scoped_trace_gcd 3.99767 us (± 406.782)
trace_nestedIf10 36.5151 us (± 6.33645) 38.0283 us (± 3.64798) 0.96
completing_trace_nestedIf10 36.1399 us (± 6.00299) 37.3711 us (± 3.21573) 0.97
scoped_trace_nestedIf10 45.9735 us (± 6.39049)
trace_nestedIf100 1.43884 ms (± 19.0085) 1.35476 ms (± 22.6997) 1.06
completing_trace_nestedIf100 1.46903 ms (± 29.4572) 1.35268 ms (± 26.016) 1.09
scoped_trace_nestedIf100 2.23148 ms (± 28.3513)
trace_chainedIf10 93.8853 us (± 12.929) 97.7583 us (± 4.73759) 0.96
completing_trace_chainedIf10 47.7467 us (± 10.547) 48.3258 us (± 3.59147) 0.99
scoped_trace_chainedIf10 60.2988 us (± 9.84188)
trace_chainedIf100 4.38091 ms (± 131.498) 4.43042 ms (± 29.6138) 0.99
completing_trace_chainedIf100 2.17263 ms (± 36.7855) 2.24075 ms (± 31.9951) 0.97
scoped_trace_chainedIf100 3.09617 ms (± 37.5147)
exec_mlir_add 12.2587 ns (± 1.43446) 10.6651 ns (± 0.946586) 1.15
exec_mlir_fibonacci 16.7679 us (± 2.57717) 13.4703 us (± 2.01788) 1.24
exec_mlir_sum 552.929 us (± 59.0406) 527.422 us (± 21.2529) 1.05
exec_cpp_add 4.57002 ns (± 0.768555) 4.69868 ns (± 0.745035) 0.97
exec_cpp_fibonacci 109.671 us (± 10.0418) 96.6361 us (± 9.26507) 1.13
exec_cpp_sum 23.6287 ms (± 362.817) 35.9426 ms (± 115.287) 0.66
exec_bc_add 44.8539 ns (± 4.9627) 44.8635 ns (± 8.015) 1.00
exec_bc_fibonacci 625.81 us (± 11.8725) 859.028 us (± 13.0138) 0.73
exec_bc_sum 145.027 ms (± 15.6763) 186.067 ms (± 1.36597) 0.78
exec_asmjit_add 3.60941 ns (± 0.40211) 3.48273 ns (± 0.424618) 1.04
exec_asmjit_fibonacci 22.2392 us (± 1.63834) 20.8625 us (± 3.3694) 1.07
exec_asmjit_sum 5.3064 ms (± 185.152) 4.87965 ms (± 312.598) 1.09
exec_bc_add_noRegAlloc 69.9733 ns (± 39.9902) 44.3118 ns (± 3.89068) 1.58
exec_bc_add_regAlloc 44.5335 ns (± 4.38348) 44.599 ns (± 5.15383) 1.00
exec_bc_fibonacci_noRegAlloc 636.89 us (± 17.0147) 852.767 us (± 11.3762) 0.75
exec_bc_fibonacci_regAlloc 626.274 us (± 12.4768) 875.208 us (± 25.409) 0.72
exec_bc_sum_noRegAlloc 143.12 ms (± 453.171) 185.974 ms (± 222.438) 0.77
exec_bc_sum_regAlloc 143.163 ms (± 946.513) 185.982 ms (± 165.251) 0.77
exec_bc_addOne 36.2941 ns (± 3.50209) 36.0837 ns (± 6.3975) 1.01
exec_mlir_addOne 282.196 ns (± 8.50915) 258.154 ns (± 2.33301) 1.09
exec_cpp_addOne 3.83026 ns (± 0.721327) 3.54853 ns (± 0.249363) 1.08
exec_interpreted_addOne 38.4136 ns (± 1.80811) 37.1985 ns (± 2.33453) 1.03
e2e_tiered_bc_to_mlir 46.2578 us (± 16.6756) 56.9167 us (± 7.69512) 0.81
e2e_single_mlir 6.16852 ms (± 209.357) 5.52315 ms (± 41.2737) 1.12
trace_peOne 6.57495 us (± 982.032)
completing_trace_peOne 6.64642 us (± 1.14381)
scoped_trace_peOne 7.92535 us (± 1.28649)
trace_pe3Calls 75.1147 us (± 11.0268)
completing_trace_pe3Calls 75.4155 us (± 9.69101)
scoped_trace_pe3Calls 42.7818 us (± 9.01471)
trace_peIndIfs 27.4959 us (± 4.40053)
completing_trace_peIndIfs 15.2906 us (± 2.45762)
scoped_trace_peIndIfs 18.816 us (± 3.99706)
trace_pePost1 13.5246 us (± 2.08289)
completing_trace_pePost1 13.6979 us (± 2.03705)
scoped_trace_pePost1 14.1958 us (± 2.10332)
trace_pePost3 274.946 us (± 18.4103)
completing_trace_pePost3 255.257 us (± 25.2612)
scoped_trace_pePost3 55.6593 us (± 10.5082)
trace_peBlind 8.15945 us (± 1.29296)
completing_trace_peBlind 8.20158 us (± 1.25815)
scoped_trace_peBlind 7.0098 us (± 988.973)
comp_mlir_add 6.47175 ms (± 821.717) 5.55479 ms (± 56.4997) 1.17
comp_mlir_ifThenElse 6.86291 ms (± 188.128) 6.14317 ms (± 38.4483) 1.12
comp_mlir_deeplyNestedIfElse 5.62267 ms (± 137.28) 5.06889 ms (± 99.0918) 1.11
comp_mlir_loop 7.86682 ms (± 265.806) 7.14743 ms (± 31.0585) 1.10
comp_mlir_ifInsideLoop 30.1375 ms (± 389.534) 28.6125 ms (± 100.629) 1.05
comp_mlir_loopDirectCall 13.3027 ms (± 396.251) 11.792 ms (± 44.0495) 1.13
comp_mlir_pointerLoop 28.7409 ms (± 424.38) 27.7179 ms (± 76.6326) 1.04
comp_mlir_staticLoop 5.63187 ms (± 173.643) 5.03112 ms (± 38.6111) 1.12
comp_mlir_fibonacci 11.3119 ms (± 203.15) 10.4618 ms (± 76.5332) 1.08
comp_mlir_gcd 10.3158 ms (± 268.67) 9.43388 ms (± 42.8866) 1.09
comp_mlir_nestedIf10 11.274 ms (± 276.359) 10.5281 ms (± 45.0755) 1.07
comp_mlir_nestedIf100 26.565 ms (± 370.879) 25.0116 ms (± 102.345) 1.06
comp_mlir_chainedIf10 10.5703 ms (± 312.142) 9.56929 ms (± 46.3491) 1.10
comp_mlir_chainedIf100 21.6057 ms (± 369.7) 20.2061 ms (± 81.9884) 1.07
comp_cpp_add 28.2627 ms (± 668.604) 24.3267 ms (± 189.47) 1.16
comp_cpp_ifThenElse 29.205 ms (± 1.45665) 24.9638 ms (± 283.6) 1.17
comp_cpp_deeplyNestedIfElse 29.8797 ms (± 2.4894) 26.0088 ms (± 233.598) 1.15
comp_cpp_loop 28.9265 ms (± 850.648) 25.0851 ms (± 291.998) 1.15
comp_cpp_ifInsideLoop 30.144 ms (± 1.50869) 26.2072 ms (± 775.414) 1.15
comp_cpp_loopDirectCall 29.4873 ms (± 900.07) 25.3831 ms (± 531.136) 1.16
comp_cpp_pointerLoop 29.4341 ms (± 628.226) 25.4858 ms (± 203.254) 1.15
comp_cpp_staticLoop 28.6521 ms (± 952.879) 24.7845 ms (± 176.103) 1.16
comp_cpp_fibonacci 28.9982 ms (± 2.96445) 25.2385 ms (± 205.167) 1.15
comp_cpp_gcd 28.707 ms (± 669.207) 25.0233 ms (± 436.288) 1.15
comp_cpp_nestedIf10 32.4655 ms (± 670.03) 28.0721 ms (± 363.361) 1.16
comp_cpp_nestedIf100 65.7886 ms (± 467.895) 61.7276 ms (± 707.638) 1.07
comp_cpp_chainedIf10 34.2756 ms (± 665.595) 30.7822 ms (± 574.356) 1.11
comp_cpp_chainedIf100 95.5081 ms (± 3.77001) 91.9107 ms (± 685.096) 1.04
comp_bc_add 14.5286 us (± 2.51273) 14.7773 us (± 1.91246) 0.98
comp_bc_ifThenElse 16.9963 us (± 3.96259) 19.2429 us (± 3.53172) 0.88
comp_bc_deeplyNestedIfElse 20.2984 us (± 4.43318) 23.0339 us (± 3.44593) 0.88
comp_bc_loop 16.6359 us (± 4.46054) 18.9128 us (± 2.70016) 0.88
comp_bc_ifInsideLoop 19.0189 us (± 3.64977) 21.5194 us (± 2.28647) 0.88
comp_bc_loopDirectCall 17.0491 us (± 4.05145) 19.2878 us (± 2.03113) 0.88
comp_bc_pointerLoop 17.9258 us (± 4.35881) 20.5351 us (± 2.66896) 0.87
comp_bc_staticLoop 16.6935 us (± 3.89256) 17.2132 us (± 2.1155) 0.97
comp_bc_fibonacci 16.9827 us (± 3.55847) 19.1709 us (± 2.93634) 0.89
comp_bc_gcd 15.8824 us (± 2.69544) 18.5754 us (± 2.5724) 0.86
comp_bc_nestedIf10 30.8009 us (± 4.3562) 35.6002 us (± 4.60432) 0.87
comp_bc_nestedIf100 192.385 us (± 10.1449) 198.41 us (± 10.198) 0.97
comp_bc_chainedIf10 42.6986 us (± 7.79238) 52.6073 us (± 9.11991) 0.81
comp_bc_chainedIf100 306.332 us (± 12.0704) 309.294 us (± 26.888) 0.99
comp_asmjit_add 17.7054 us (± 5.2727) 22.1735 us (± 4.82406) 0.80
comp_asmjit_ifThenElse 26.9644 us (± 5.71155) 33.4071 us (± 4.26649) 0.81
comp_asmjit_deeplyNestedIfElse 48.6531 us (± 11.146) 56.4176 us (± 5.25514) 0.86
comp_asmjit_loop 28.5741 us (± 5.67626) 35.8631 us (± 4.35405) 0.80
comp_asmjit_ifInsideLoop 47.9551 us (± 10.6704) 57.5183 us (± 8.7641) 0.83
comp_asmjit_loopDirectCall 31.9399 us (± 6.65296) 47.2559 us (± 9.00425) 0.68
comp_asmjit_pointerLoop 34.4428 us (± 5.99247) 48.2785 us (± 6.56048) 0.71
comp_asmjit_staticLoop 24.0377 us (± 5.74962) 28.6917 us (± 4.31543) 0.84
comp_asmjit_fibonacci 31.1864 us (± 6.01052) 43.5157 us (± 6.92307) 0.72
comp_asmjit_gcd 28.8314 us (± 5.68034) 35.3711 us (± 4.19816) 0.82
comp_asmjit_nestedIf10 99.8478 us (± 17.9786) 103.255 us (± 10.7623) 0.97
comp_asmjit_nestedIf100 1052.8200000000002 us (± 27965.2) 1057.97 us (± 54427.5) 1.00
comp_asmjit_chainedIf10 147.004 us (± 15.6326) 153.183 us (± 14.6589) 0.96
comp_asmjit_chainedIf100 2.21471 ms (± 115.667) 2.16653 ms (± 46.7063) 1.02
tiered_compile_addOne 45.3727 us (± 15.873) 55.1658 us (± 10.7264) 0.82
single_compile_mlir_addOne 3.58827 ms (± 107.333) 3.25749 ms (± 57.5499) 1.10
single_compile_cpp_addOne 27.6415 ms (± 522.465) 24.4391 ms (± 405.29) 1.13
single_compile_bc_addOne 45.679 us (± 15.1487) 60.6703 us (± 11.2707) 0.75
tiered_compile_sumLoop 60.2018 us (± 16.8028) 79.6202 us (± 15.7788) 0.76
single_compile_mlir_sumLoop 5.64736 ms (± 137.436) 5.35632 ms (± 118.42) 1.05
single_compile_cpp_sumLoop 28.0264 ms (± 468.101) 26.0899 ms (± 453.281) 1.07
single_compile_bc_sumLoop 61.4161 us (± 17.9021) 78.6934 us (± 10.1775) 0.78
ir_add 733.87 ns (± 69.8561) 757.379 ns (± 38.5584) 0.97
ir_ifThenElse 1.50381 us (± 75.54) 1.58461 us (± 136.165) 0.95
ir_deeplyNestedIfElse 3.29635 us (± 204.392) 3.40826 us (± 363.019) 0.97
ir_loop 1.66959 us (± 88.9069) 1.63694 us (± 149.086) 1.02
ir_ifInsideLoop 2.85306 us (± 254.075) 2.83439 us (± 293.378) 1.01
ir_loopDirectCall 1.79231 us (± 113.589) 1.80584 us (± 177.074) 0.99
ir_pointerLoop 1.97311 us (± 149.656) 1.97161 us (± 153.779) 1.00
ir_staticLoop 1.40567 us (± 73.5288) 1.44956 us (± 119.501) 0.97
ir_fibonacci 1.8305 us (± 100.282) 1.72022 us (± 143.401) 1.06
ir_gcd 1.41916 us (± 82.6629) 1.4549 us (± 101.976) 0.98
ir_nestedIf10 7.62729 us (± 459.6) 7.70943 us (± 540.522) 0.99
ir_nestedIf100 89.8004 us (± 4.50704) 93.6887 us (± 16.2569) 0.96
ir_chainedIf10 11.6191 us (± 708.306) 11.594 us (± 826.837) 1.00
ir_chainedIf100 167.88 us (± 6.71317) 169.138 us (± 8.3263) 0.99

This comment was automatically generated by workflow using github-action-benchmark.

claude added 7 commits May 14, 2026 18:44
…ormedness coverage

The first revision of ScopedTraceContext dropped aliveVars.hash() from
recordSnapshot() in an attempt to collapse the postCallBranch path-explosion.
End-to-end coverage of the SSA + IR pipeline (added in this commit) revealed
that the smaller traces were structurally malformed: RETURN ops at the same
source line across different symbolic-execution iterations collide on a
single Snapshot, processControlFlowMerge accumulates their inputs into one
op, and SSACreationPhase rejects the result with "Wrong number of arguments
in trace: expected 1, got N".

Reverting the Snapshot to (Tag*, staticHash ^ aliveHash) restores Lazy-equivalent
correctness on every path-explosion fixture (verified by running each through
SSACreationPhase + SSA verifier + TraceToIRConversionPhase).  The actual
path-explosion fix requires per-function sub-traces with explicit CALL-op
emission at boundary crossings; that work is sized for a separate follow-up
PR and tracked in the plan file.

Also adds:
- safeCheckTag() defensive helper that detects the same-block self-merge
  case (which the stable Snapshot scheme can still produce on edge fixtures
  like constraintBlind_dead) and falls back to passive mode instead of
  letting processControlFlowMerge throw RuntimeException.
- "full pipeline" test that runs every path-explosion fixture through
  trace -> SSA verify -> IR, catching this class of bug going forward.

All 191 tests pass; PathPredicateStore infrastructure is unchanged and remains
the substantive new feature of ScopedTraceContext over Lazy at this point.

https://claude.ai/code/session_01XDkjLQbFMxtTeyB3w15T56
ScopedTraceContext now actually consults its PathPredicateStore at every
CMP: if the candidate predicate is entailed (false arm is dead) or
contradicted (true arm is dead) by the active dominators' predicates,
the dead arm is skipped entirely.

New surface:
  - SymbolicExecutionContext::recordPrunedNoThrow(tag, takenDirection)
    marks the tag as fully explored without enqueueing the dead arm
    onto inflightExecutionPaths, so the symbolic executor never wastes
    an iteration re-running the function to reach a branch we have
    already proven unreachable.

  - ScopedTraceContext::traceBool dispatches to recordPrunedNoThrow
    when PathPredicateStore::evaluate returns a verdict, otherwise
    falls through to the regular recordNoThrow worklist behaviour.

Behavioural results:
  - pathExplosion_constraintBlind_dead drops from 4 -> 2 RETURNs (the
    inner `if (x == 1)` arms that are entailed/contradicted by the
    outer dominator).  This matches the originally documented "intended"
    count for that fixture in PathExplosionFunctions.hpp.
  - Two new minimal regression fixtures (redundant-dominator-CMP and
    contradicted-dominator-CMP) cover the pruning mechanism with focused
    assertions.
  - All other path-explosion fixtures keep their existing trace shape;
    they don't have dominator-implied CMPs so the predicate store is a
    no-op for them.

All 193 tests (existing + new) pass; SSA verifier accepts every pruned
trace via the full-pipeline coverage from the previous commit.

The Snapshot scheme is still aliveVars-based (matches Lazy); the
per-function-sub-trace path-explosion lever remains the next milestone.

https://claude.ai/code/session_01XDkjLQbFMxtTeyB3w15T56
Extends the scoped tracer with two new per-iteration caches:

  integerConstants : ValueRef -> int64_t
    Populated in traceConstant() for every CONST op whose literal extracts
    cleanly as an integer.  Propagated through traceCopy() so the cache
    survives val<T> moves / assignments.

  staticBoolValues : ValueRef -> bool
    Populated in traceBinaryOp() when both operands of a comparison op
    are present in integerConstants, by statically evaluating the CMP.

traceBool() consults staticBoolValues first; if the bool is known, the
already-existing recordPrunedNoThrow path skips the dead arm.  This
catches CMPs whose value is constant-folded (e.g. `1 == 42` after an
inlined `return 1`) — which is exactly the shape produced by inlining a
return-constant leaf into a caller that branches on the result.

Behavioural results (vs LazyTraceContext, raw-trace RETURN counts):

  pathExplosion_baseline_oneCall              3 -> 3   (unchanged)
  pathExplosion_baseline_threeCallsNoBranch  27 -> 9   (3x reduction)
  pathExplosion_postCallBranch_1              6 -> 4   (33% reduction)
  pathExplosion_postCallBranch_3             54 -> 12  (4.5x reduction)
  pathExplosion_independentIfs_4              2 -> 2   (unchanged, no constants)
  pathExplosion_constraintBlind_dead          4 -> 2   (predicate-based)

Each fixture is also run through the full SSA-verify + IR-generation
pipeline to confirm well-formedness — 193 / 193 tests pass.

This is the constant-propagation half of the path-explosion fix.  The
remaining lever (turning `baseline_threeCallsNoBranch` from 9 -> 3 via
proper per-function sub-traces with CALL-op emission) is unchanged and
still a follow-up; the constant cache only fires when at least one path
through the inlined callee produces a CONST return value.

https://claude.ai/code/session_01XDkjLQbFMxtTeyB3w15T56
…ontext

Adds the six pathExplosion_* fixtures to a new "Path Explosion Tracing
Benchmark" Catch test case and rotates ScopedTraceContext into the
traceContexts vector alongside ExceptionBased and Lazy.  This is the
benchmark counterpart to the trace-size assertions in
nautilus-scoped-tracing-tests so the wall-time wins land in CI's
benchmark report.

Local results (Debug, 30 samples, microseconds per trace):

  baseline_oneCall              exc=91   lazy=89   scoped=92   (+4%)
  baseline_threeCallsNoBranch   exc=800  lazy=725  scoped=463  (-36%)
  independentIfs_4              exc=187  lazy=175  scoped=192  (+10%)
  postCallBranch_1              exc=155  lazy=153  scoped=153  (~=)
  postCallBranch_3              exc=1893 lazy=2319 scoped=892  (-62%)
  constraintBlind_dead          exc=110  lazy=109  scoped=95   (-13%)

Fixtures with no constants to fold and no dominator-implied CMPs pay
~4-10% overhead from comparisonCache / integerConstants / staticBoolValues
upkeep; the wins dominate where path-explosion structure is present.

https://claude.ai/code/session_01XDkjLQbFMxtTeyB3w15T56
…oke CI

Two follow-ups to PR #288 in one commit:

1. Pay-as-you-go cache gating in ScopedTraceContext

   Adds thread_local boolean flags `hasIntegerConstants`,
   `hasComparisonCache`, `hasStaticBoolValues` that each flip the first
   time the corresponding cache receives a useful entry, and reset in
   resume() alongside the maps.  Every hot-path lookup (traceConstant,
   traceCopy, traceBinaryOp, traceUnaryOp, traceBool, derivePredicate)
   is now guarded by the relevant flag, so workloads with no integer
   constants and no dominator-implied predicates pay one boolean
   branch instead of an unordered_map probe.

   The flag also helps avoid evaluate() walks when the predicate store
   is empty (`predicates_.size() > 0` precondition).

   Locally re-benchmarked the path-explosion fixtures with samples=20:
   wins are intact (pe3Calls -38%, pePost3 -55%, peBlind -19% vs Lazy).

   Workloads with many CMPs against integer literals but no
   constant-folding / dominator-entailment opportunities (nestedIf100,
   chainedIf100) still pay residual overhead from the
   `comparisonCache` insert + `predicates_.evaluate` linear walk; the
   structural fix for those is per-var predicate indexing, tracked as
   a follow-up.

2. Shorten path-explosion benchmark names so CI parser succeeds

   The previous commit (6a6af6c) added benchmark names like
   `completing_trace_pathExplosion_baseline_threeCallsNoBranch` which
   are long enough that Catch2 wraps them onto a continuation line
   (`completing_trace_pathExplosion_bas-\neline_threeCallsNoBranch`).
   github-action-benchmark's catch2 parser regexes one row at a time
   and reported "No benchmark found for bench suite. Possibly mangled
   output from Catch2", failing the "Run tracing benchmark" CI job.
   (The benchmarks themselves ran fine.)

   Compressed the fixture keys to `peOne / pe3Calls / peIndIfs /
   pePost1 / pePost3 / peBlind`.  Combined name with the longest
   tracer prefix `completing_trace_` stays under Catch2's wrap
   threshold, and the action regex picks them up cleanly.

All 202 tests pass.  Existing tracer names, the unrelated benchmark
test cases, and the default `lazyTracing` behavior are untouched.

https://claude.ai/code/session_01XDkjLQbFMxtTeyB3w15T56
… per-var index

Implements four targeted follow-ups (items 1-4 from the improvements list)
that together more than halve the trace size on the two deepest
path-explosion fixtures without changing the snapshot scheme.

1. Reflexive-CMP shortcut

   `traceBinaryOp(CMP, x, x)` is statically known regardless of any cache:
   EQ / LTE / GTE -> true; NEQ / LT / GT -> false.  Fast path checks raw
   refs (`left.ref == right.ref`); slow path canonicalises both refs
   through the alias map so `y = x; y cmp x` also fires.  Only the slow
   path pays an unordered_map probe, and only when `hasAliases` is true.

2. Arithmetic constant folding

   When both operands of ADD / SUB / MUL / DIV / MOD / AND / OR / BAND /
   BOR / BXOR / LSH / RSH are in `integerConstants`, the result is
   evaluated statically (with __builtin_*_overflow / divide-by-zero /
   undefined-shift guards) and recorded.  Result must also fit in the
   target nautilus type (i8 / i16 / i32 / i64 / ui8..ui64) to avoid
   pushing a constant that diverges from the runtime-wrapped value.
   This is the lever that lets `r + 1` after a CONST inlined return
   propagate as a constant into the downstream CMP.

3. Alias tracking through traceCopy

   `traceCopy(ref)` records `aliases[result.ref] = canonicalRef(ref.ref)`
   so any later CMP that compares the copy can be canonicalised back to
   the original.  `derivePredicate` canonicalises the var before
   returning the predicate, and the reflexive-CMP shortcut consults the
   alias map.  Both gated by `hasAliases` for pay-as-you-go.

4. Per-var index inside PathPredicateStore

   `byVar_ : ValueRef -> vector<index>` lets `evaluate(candidate)` walk
   only the predicates that mention the candidate's var, instead of the
   entire active stack.  Push / pop maintain the index in O(1) amortised.
   `clear()` resets both `active_` and `byVar_` in one shot so
   ScopedTraceContext::resume() doesn't pop one entry at a time.

Behavioural impact (RETURN counts vs LazyTraceContext, before / now):

  baseline_threeCallsNoBranch  27   9 -> 7   (1.3x further reduction)
  postCallBranch_3             54  12 -> 4   (3.0x further reduction; 13x vs Lazy)

Wall-time impact (Debug, 20 samples, scoped vs lazy mean us per trace):

  pe3Calls           714  ->  431  us  (-40%)
  pePost1            153  ->  161  us  (~equal; no headroom to harvest)
  pePost3           2029  ->  544  us  (-73%, was -55% before)
  peBlind            110  ->   91  us  (-17%)

  deeplyNestedIfElse  152 ->   69 us  (-55%)

Workloads with many CMPs against the same variable but no
entailment opportunities (nestedIf100, chainedIf100) still pay
~50-65% overhead from the unavoidable predicate-store linear walk
within the single var bucket.  The structural fix for those is
unified-range predicates per var (`x > N` collapsed instead of
appended), tracked as a follow-up (item 5 in the improvements list).

Adds three focused unit tests covering the reflexive CMP, the
arithmetic propagation through ADD, and the alias path through
traceCopy.  All 205 existing + new tests pass; SSA verifier accepts
every pruned trace.

https://claude.ai/code/session_01XDkjLQbFMxtTeyB3w15T56
Threads a small env-var lookup into LegacyCompiler::compileToIR so the
existing execution / val / ir-pass / tracing test binaries can be run
against any tracer without modifying each Options-constructing callsite.

Lookup order is now: env var > engine option > built-in default
(lazyTracing).  Empty env var values are ignored.  Unrecognised values
fall through to the else-branch (ExceptionBasedTraceContext) matching
the existing dispatch semantics.

Used immediately to validate that the new ScopedTraceContext produces
correct compiled output on the full test suite:

  NAUTILUS_TRACE_MODE=scopedTracing       ctest ...   205 / 205 pass
  NAUTILUS_TRACE_MODE=exceptionBasedTracing ctest ... 205 / 205 pass
  (default lazyTracing)                    ctest ...   205 / 205 pass

This includes every Engine.compile() path the suite exercises (Bool /
Cast / Pointer / Function-Ptr / Select / Module / Loop / Tiered
compilation tests in both compiler and interpreter variants, plus the
21 dedicated scoped-tracing-tests).  Verifies end-to-end semantic
correctness, not just the previously asserted trace-size shrinkage.

https://claude.ai/code/session_01XDkjLQbFMxtTeyB3w15T56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants