Add YAML-driven property-based testing for FAIR conversion#4
Open
ericbodden wants to merge 29 commits intodevelopfrom
Open
Add YAML-driven property-based testing for FAIR conversion#4ericbodden wants to merge 29 commits intodevelopfrom
ericbodden wants to merge 29 commits intodevelopfrom
Conversation
Implement a hybrid approach for eliminating infeasible branches: 1. Conversion-time predicate narrowing: New predicate() DSL construct in InvokeExprHandler lets analyses declare that a method return value constrains abstract state (e.g., isOpen()=true => state OPEN). The converter emits SetValueOp narrowing statements in branch targets. 2. Interpretation-time assume evaluation: New AssumeHandler<T> interface lets analyses evaluate FAIRAssumeStmt conditions against known abstract values. StmtResult.Unreachable propagates through FixpointEngine and BodyIterationStrategy to skip infeasible blocks. Gatekeeper in DslStmtSemantics.translateIf() ensures assumes are only generated when the analysis can evaluate them (has an AssumeHandler). Updates to example analyses: - Typestate: predicate rule for isOpen() with whenTrue(OPEN) - ConstProp: withComparisons() for all 6 relational operators + FlatIntAssumeHandler for dead branch detection Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Drop FAIRConstantStmt case (removed upstream) and keep AssumeHandler-based executeAssume() from the branch elimination feature. Removed merge artifact files (BACKUP/BASE/LOCAL/REMOTE). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Update all 16 test Java files to use standard void main(String[] args) signature and remove return statements. Update Controller.kt to look up main with VoidType instead of IntType. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Replace manual stmt-by-stmt iteration with SootUp JimplePrinter and a TrackingStmtPrinter that records display-line positions via IdentityHashMap. The Jimple panel now shows full formatted output with labels, gotos, locals, and braces while preserving the four-panel interlinked highlighting via stmtIdx to displayLine mapping. Also fixes VoidType bug in ConvertEndpoint (main methods are void). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Rewrite FAIRBody.toString() and viz FAIR rendering to show block structure: labels on branch targets, goto pseudo-instructions at block ends, and two blank lines between FAIR instruction groups from different Jimple statements. Labels use 1-based numbering and empty pass-through blocks are resolved to avoid duplicate labels. In the viz, goto lines render in italics and labels/blanks are non-clickable. A new 'kind' field on FairLineInfo distinguishes stmt/label/goto/blank lines. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Introduces a declarative property spec (fair-properties.yaml) with 13 semantic invariants — 9 statement-level def/use contracts and 4 CFG flow-level properties — verified across all 16 test Java classes (286 dynamic tests). Properties are loaded by a JUnit 5 @testfactory runner that cross-products every property × every method. A shared SootUp view avoids OOM from repeated JRT class loading. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Previously the entire .claude/ directory was gitignored. Per recommended practice, commit shared configuration (skills, rules, agents) and only exclude settings.local.json which contains personal overrides. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Two visualization improvements: 1. Jimple panel now has a Simplified toggle (on by default) that rewrites verbose invoke syntax to Java-like calls: - virtualinvoke r0.<Foo: int bar(int)>(x) becomes r0.bar(x) - staticinvoke <Foo: int bar(int)>(x) becomes Foo.bar(x) - specialinvoke r0.<Foo: void <init>()>() becomes new Foo() Toggling off shows the raw Jimple. Simplification is done client-side so no re-fetch is needed. 2. Method dropdown now lists methods in Java source file order, sorted by the earliest Java line number found in each method's Jimple body. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
ifeq jumps when condition == 0 (false), so trueTarget is the false-path of the predicate and falseTarget is the true-path. Swap narrowingTrue/ narrowingFalse placement so SET_VALUE narrowing lands in the same block as the guarded statements (e.g. division in unreachableCodeTypeState). Add two new YAML-driven semantic properties: - narrowing-paired-with-assume: SET_VALUE blocks must contain an assume - assume-matches-edge: sibling TRUE/FALSE assumes must use complementary comparison operators Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
ericbodden
force-pushed
the
property-based-testing
branch
from
2c5294d to
1efa5a3
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
src/test/resources/fair-properties.yamldefines 15 semantic invariants for the Jimple→FAIR conversion — 9 statement-level def/use contracts (apply, copy, replace, set-constant, ret, assume) and 6 CFG/flow-level properties (assume-at-head, branch-conditions, symmetric-edges, entry-no-predecessors, narrowing-paired-with-assume, assume-matches-edge).@TestFactorycross-products every property × every method across all 16 test Java classes, generating 340 dynamic tests./generate-property-checksreads the YAML spec and generates Kotlin implementations inSemanticPropertyChecks.kt, so adding a new property is: write YAML → run skill → review generated code..gitignoreto track.claude/skills/per recommended practice.SET_VALUE) was placed on the wrong branch.ifeqalways jumps when the condition is zero (false), sotrueTargetis the false-path of the predicate. SwappednarrowingTrue/narrowingFalseplacement so narrowing lands in the same block as the guarded statements.New files
src/test/resources/fair-properties.yamlsrc/test/kotlin/properties/FAIRProperty.ktsrc/test/kotlin/properties/SemanticPropertyChecks.ktsrc/test/kotlin/properties/FAIRPropertyTest.kt.claude/skills/generate-property-checks/SKILL.mdBug fix: predicate narrowing on wrong branch
In
TypestateExampleForBranchElimination.unreachableCodeTypeStateWithDivisionByZero(), the predicate narrowingapply SET_VALUE(IS_OPEN)was ending up on a different branch from the if-body statements. Root cause: JVMifeqjumps when the condition == 0 (false), sogetTargetStmts()returns the block where the predicate returned false, but the converter was placingnarrowingTruethere. Fixed by swappingnarrowingTrue/narrowingFalsein the branch prepend logic.New semantic properties
narrowing-paired-with-assumeSET_VALUEapply must also contain aFAIRAssumeStmtassume-matches-edgeTest plan
./gradlew test— 340 tests pass (up from 286)SET_VALUE(IS_OPEN)and guarded statements now share the same block🤖 Generated with Claude Code