Skip to content

fix: resolve CSE and simplify_locals Z3 verification failures #42

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
avrabe wants to merge 13 commits into
base: main
Choose a base branch
from
Open

fix: resolve CSE and simplify_locals Z3 verification failures #42

avrabe wants to merge 13 commits into from

Conversation

@avrabe
Copy link
Contributor

@avrabe avrabe commented Dec 31, 2025

Summary

  • Fixed 3 critical bugs caught by Z3 translation validation
  • All 25/25 fixtures now pass with Z3 verification (was 16/24)

Bugs Fixed

1. CSE LocalTee index out of bounds (verify.rs)

  • Z3 shared inputs were sized from original function
  • CSE adds new locals, causing index overflow
  • Fix: extend locals dynamically like globals

2. Unsafe LocalGet CSE (lib.rs)

  • CSE cached local.get values that could change via local.set
  • Fix: only CSE constants, not LocalGet

3. SimplifyLocals equivalence bug (lib.rs)

  • Equivalence tracking unsound with control flow
  • dst=src remained valid after dst modified in branch
  • Fix: skip equivalence substitution with control flow

Test plan

  • All 25 fixtures pass with Z3 verification
  • Unit tests pass
  • CI known failures list cleared

avrabe added 13 commits December 31, 2025 16:20
@avrabe
fix: resolve CSE and simplify_locals Z3 verification failures
93da24f 
- CSE: extend locals dynamically in verify.rs for optimizer-added locals
- CSE: only cache constants, not LocalGet (values can change)
- simplify_locals: skip equivalence substitution with control flow
- Result: 25/25 fixtures pass with Z3 verification (was 16/24)
@avrabe
ci: run validate-shared tests in release mode
a153a7d
@avrabe
feat: implement single-use temp folding (#37)
9122348 
Convert local.set; local.get patterns to local.tee for efficiency.
Updates tests to count both LocalSet and LocalTee as stores.
@avrabe
feat: implement dead store elimination and single-use temp folding
73a817d 
- Replace local.set with drop when local is never read (#36)
- Eliminate local.tee when local has no local.get reads
- Convert local.set $x; local.get $x -> local.tee $x (#37)
- Update RSE tests to reflect optimization cascades
@avrabe
fix: enable CSE phase4 test (was fixed by LocalTee bug fix)
1259cf7
@avrabe
feat: enable CSE phase4 test and add global.get to LICM
d470d9b 
- Remove ignore from test_cse_phase4_duplicate_constants (now passes)
- Add find_modified_globals() for LICM global tracking
- Add GlobalGet to is_loop_invariant check
- Add tests for global.get hoisting in loops
@avrabe
feat: add non-consecutive LICM for invariant value producers
dc12025 
Phase 2 LICM now hoists single invariant instructions from anywhere
in loop bodies, not just from the start:
- global.get when global not modified in loop
- local.get when local not modified in loop
- constants (i32/i64/f32/f64)

Each hoisted value is stored to a new local before the loop,
and replaced with local.get inside the loop.
@avrabe
feat: add expression tree hoisting to LICM
dba5210 
Enhances LICM Phase 2 to hoist entire invariant expression
trees, not just single instructions. Uses stack simulation
to identify complete expressions that are loop-invariant.
@avrabe
feat: add verification coverage tracking for TCL-3 metrics
eb484b9 
Adds VerificationCoverage struct and VerificationResult enum to
track what percentage of functions are Z3-verified vs skipped.
Includes compute_verification_coverage() for module-level metrics.
@avrabe
feat(verify): add Z3 Array theory for memory model verification
c12fa9b 
Implement precise memory verification using Z3 Array theory instead of
imprecise symbolic values:

- Add Array[BitVec32 -> BitVec8] for byte-addressable memory
- Implement I32Load/I32Store with little-endian byte encoding
- Implement I64Load/I64Store with little-endian byte encoding
- Remove I32Load, I64Load, I32Store, I64Store from skip list
- Update contains_memory_instructions to only flag unverifiable ops
- Add test_memory_load_store_verification test

Also fixes pre-existing clippy warnings in lib.rs.
@avrabe
feat(verify): enable bounded loop verification for simple loops
8cbb3d9 
Implement selective loop verification that allows simple loops to be
verified using bounded unrolling while still skipping complex loops:

- Rename contains_loops to contains_complex_loops
- Add is_complex_loop() to identify loops that are too complex:
  - Nested loops (loops within loops)
  - Loops with unverifiable instructions
  - Loops with > 50 instructions
- Add contains_any_loop() for nested loop detection
- Add count_instructions() for loop body size checking
- Add test_simple_loop_verification test

Simple loops without nesting, unverifiable ops, or excessive size are
now verified using MAX_LOOP_UNROLL=3 bounded unrolling instead of being
skipped entirely.
@avrabe
docs(readme): add verification coverage output example
c26962d 
Show the coverage tracking output in README example. Details about
what's verified vs skipped are in FORMAL_VERIFICATION_GUIDE.md,
keeping the README evergreen.
@avrabe
fix(ci): free disk space before coverage job
01aee1a 
- Remove dotnet/android/ghc to free ~10GB disk space
- Exclude verification feature from coverage (tested separately in z3-verification)
- Z3 compilation + LLVM instrumentation together exhaust runner disk
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@avrabe