Add assertion API and related improvements#7
Conversation
Implements a Debug Adapter Protocol server that allows stepping through abstract interpretation in IntelliJ via the LSP4IJ plugin. The debugger pauses at each FAIR statement, showing the evolving abstract environment with threads, variables (parameters, locals, analysis info), and virtual FAIR IR source generated on-the-fly. Key components: - DebugListener interface injected into interpreter (zero overhead when null) - BlockingDebugListener pauses interpreter via ReentrantLock+Condition - FairDebugServer (LSP4J) handles DAP requests from IntelliJ - FairDebugSession manages thread-safe shared state between threads - FairSourceProvider generates virtual FAIR IR listings per method - InterpreterBridge wires SootUp/FAIR/interpreter with the debugger - Pre-configured LSP4IJ DAP run configurations in .run/ Also fixes: - RPO fixpoint strategy skipping all blocks on first iteration - IFDSCallSemantics crashing on abstract/native methods from CHA Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
When LSP4IJ launches the DAP server with noDebug=true (Run button instead of Debug button), the server now prints a clear error message and sends terminated/exited events so the client disconnects cleanly, instead of silently hanging. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…Up view The visualizer SootUp view only received the temp compile directory, missing the stub classes (stubs.taintAnalysis.*) that TaintExample depends on. Added vararg additionalClassPaths to SootUpManager.createView and passed the test classes directory from ConvertEndpoint. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- stopOnEntry (default true) pauses at first FAIR statement on launch - Send terminated/exited events when interpretation completes - Run configs updated with stopOnEntry in launch configuration - Revert unsuccessful breakpoint infrastructure (LSP4IJ limitation) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- Fix off-by-one in computeLineNumber (skip block header line) - Pass callee FAIRBody through onMethodEntry so pushFrame registers the correct source reference instead of the caller s body - Add session-unique path to DAP source objects to prevent LSP4IJ from serving stale cached content across debug runs Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Resolve merge conflict in CallHandler.kt by adopting the new methodRegistry.getMethodBySignature() API. Also migrate InterpreterBridge.kt from the removed program.classes API to methodRegistry.allMethods(). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
AnalysisType.valueOf("CONSTPROP") silently failed because the enum
name is CONSTANT_PROPAGATION, causing all analyses to fall back to
TAINT_ANALYSIS. Use direct string matching like the develop branch.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Include parameter locals and synthetic locals (e.g. constant_value_*) alongside regular locals in the debugger Threads & Variables panel. Sort variables alphabetically by name. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Save the caller's environment snapshot, body, and block onto a stack when entering a callee method, and restore them on exit. Previously the Variables view would show the callee's environment after stepping over or returning from a call. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Here the method can be registered for the kind of optimization it should undergo after the generator pass has been done
…ts (numbers) during debugging
…ograms Introduces AssertionOperation<T> marker interface and four assertion operations (AssertTop, AssertBottom, AssertEqual, AssertUnreachable) that produce dual ASSERT_PASSED/ASSERT_FAILED findings at interpretation time. Assertions are registered via FAIRAnalysisDefinition.enableAssertions() as a caller-side concern, decoupled from analysis definition functions. Includes JUnit 5 @testfactory runner that maps assertion findings to dynamic pass/fail tests, --assertions CLI flag, and example assertions in ConstantPropExample and TaintExample. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
Pull request overview
This PR adds an assertion-based testing API for analyses, improves IR normalization (constant extraction), introduces an optimization registry for fold-heavy methods, and integrates an initial DAP-based abstract debugger with interpreter hooks.
Changes:
- Added assertion stubs + interpreter support for producing pass/fail findings and a JUnit dynamic test runner to validate assertions in Java test programs
- Replaced field-store normalization with a more general constant normalizer; adjusted taint allocation semantics and CFG traversal order
- Added an optimization registry (push-based fold tracking) and introduced a DAP debugger server + listener hooks for step-through interpretation
Reviewed changes
Copilot reviewed 48 out of 51 changed files in this pull request and generated 4 comments.
Show a summary per file
| File | Description |
|---|---|
| src/test/kotlin/converter/ConstantNormalizerTest.kt | Adds unit tests covering constant extraction and name-collision handling |
| src/test/kotlin/benchmark/FAIRGeneratorBenchmarkTest.kt | Adds per-method metric capture and a method-level diff report for benchmark phases |
| src/test/kotlin/assertions/AnalysisAssertionTest.kt | Adds JUnit 5 dynamic test runner to turn assertion findings into pass/fail tests |
| src/test/kotlin/OptimizationRegistryTest.kt | Adds unit tests validating OptimizationRegistry fold tracking and reporting |
| src/test/java/stubs/assertions/Assertions.java | Adds no-op assertion stubs for conversion-time interception |
| src/test/java/TaintExample.java | Adds assertion calls to validate taint lattice results in sample program |
| src/test/java/ConstantPropExample.java | Adds assertion calls to validate constant propagation results |
| src/main/kotlin/semantics/call/IFDSCallSemantics.kt | Changes handling of abstract/native callees during call processing |
| src/main/kotlin/optimizer/OptimizationRegistry.kt | Introduces concurrent fold-stat registry and reporting helpers |
| src/main/kotlin/optimizer/OptimizationHint.kt | Adds hint model for alias-analysis candidacy based on fold usage |
| src/main/kotlin/optimizer/MethodOptimizationProfile.kt | Adds per-method profile wrapper used by the registry and reports |
| src/main/kotlin/interpreter/StmtExecutor.kt | Adds DebugListener hooks; adds assertion finding collection; changes allocation semantics |
| src/main/kotlin/interpreter/FixpointEngine.kt | Wires DebugListener into execution and resets per-block stmt index |
| src/main/kotlin/interpreter/FAIRInterpreter.kt | Threads DebugListener through interpreter and call handler creation |
| src/main/kotlin/interpreter/CallHandler.kt | Adds DebugListener method-entry/exit callbacks around recursive solving |
| src/main/kotlin/interpreter/BodyIterationStrategy.kt | Ensures first iteration executes blocks to bootstrap successor outputs |
| src/main/kotlin/helper/FoldHelper.kt | Registers fold creation with OptimizationRegistry during conversion |
| src/main/kotlin/dsl/examples/TaintAnalysis.kt | Updates allocation comment to reflect non-tainting default |
| src/main/kotlin/dsl/Lattice.kt | Changes Flat.Element string rendering for better debugging readability |
| src/main/kotlin/dsl/FAIRAnalysis.kt | Exposes invokeHandler internally and adds enableAssertions() API |
| src/main/kotlin/dsl/ExprHandlers.kt | Makes customTransfer open; changes allocation handlers to opt-in (no-op by default) |
| src/main/kotlin/dsl/DomainOperation.kt | Makes Finding.variable nullable; adds assertion operation implementations |
| src/main/kotlin/debugger/source/FairSourceProvider.kt | Generates virtual FAIR sources and maps positions for DAP |
| src/main/kotlin/debugger/server/FairDebugSession.kt | Adds shared debug session state for DAP server/interpreter coordination |
| src/main/kotlin/debugger/server/FairDebugServer.kt | Implements DAP server endpoints (threads/stack/variables/source/stepping) |
| src/main/kotlin/debugger/server/DapLauncher.kt | Adds entry point to launch the DAP server via stdio or socket |
| src/main/kotlin/debugger/model/StepMode.kt | Defines stepping modes for interpreter pausing |
| src/main/kotlin/debugger/model/DebugThread.kt | Models DAP thread display for (method, context) executions |
| src/main/kotlin/debugger/model/DebugStackFrame.kt | Models stack frames for DAP stack trace responses |
| src/main/kotlin/debugger/listener/DebugListener.kt | Defines interpreter hook interface for debugger integration |
| src/main/kotlin/debugger/listener/BlockingDebugListener.kt | Adds blocking implementation that pauses interpreter based on step/bp state |
| src/main/kotlin/debugger/bridge/InterpreterBridge.kt | Bridges conversion + interpreter execution to DAP session/listener |
| src/main/kotlin/debugger/DEBUGGER.md | Documents debugger design decisions and IntelliJ/LSP4IJ setup |
| src/main/kotlin/converter/interceptor/FieldStoreNormalizer.kt | Removes old dedicated field-store normalizer |
| src/main/kotlin/converter/interceptor/ConstantNormalizer.kt | Adds general constant extraction normalizer across multiple statement forms |
| src/main/kotlin/converter/FAIRTranslationSuite.kt | Switches from FieldStoreNormalizer to ConstantNormalizer |
| src/main/kotlin/converter/FAIRMethodConverter.kt | Uses sorted block traversal (blocksSorted) for stability |
| src/main/kotlin/controller/SootUpManager.kt | Extends createView() to accept additional classpath entries |
| src/main/kotlin/controller/Controller.kt | Adds CLI flag plumbed to enableAssertions |
| src/main/kotlin/Main.kt | Parses --assertions flag and passes through to Controller |
| fair.viz/src/main/kotlin/viz/ConvertEndpoint.kt | Adds test classes dir to view so stubs are resolvable in viz conversion |
| fair.core/src/main/kotlin/model/type/ClassType.kt | Fixes equals/hashCode to include packageName |
| debugFair.sh | Adds wrapper for Gradle task with ensured working dir and Java 21 |
| build.gradle.kts | Adds lsp4j.debug dependency, adds debugFair task, increases test heap |
| TODO.MD | Updates TODOs and documents allocation stmt semantics change |
| README.md | Minor whitespace update in usage examples |
| CLAUDE.md | Documents --assertions and assertion behavior in DSL/interpreter |
| .run/DAP Typestate Analysis.run.xml | Adds IntelliJ DAP run config (currently malformed) |
| .run/DAP Taint Analysis.run.xml | Adds IntelliJ DAP run config |
| .run/DAP Constant Propagation.run.xml | Adds IntelliJ DAP run config |
Comments suppressed due to low confidence (6)
src/test/kotlin/assertions/AnalysisAssertionTest.kt:1
org.junit.jupiter.api.Assertions.failis not a generic function, sofail<Unit>(...)will not compile. Callfail(\"...\")(andfail(\"...\", e)for the exception case) without type arguments.
src/test/kotlin/assertions/AnalysisAssertionTest.kt:1org.junit.jupiter.api.Assertions.failis not a generic function, sofail<Unit>(...)will not compile. Callfail(\"...\")(andfail(\"...\", e)for the exception case) without type arguments.
src/main/kotlin/semantics/call/IFDSCallSemantics.kt:1- Returning
emptyList()for abstract/native methods drops the usual opaque-call effects (and can fail to definedestination), which likely makes call semantics unsound vs the existingopaqueCallResult(destination)path. Use the same opaque result for abstract/native methods (or otherwise ensuredestinationis handled consistently).
src/test/kotlin/benchmark/FAIRGeneratorBenchmarkTest.kt:1 \"─\".repeat(116 - label.length)will throwIllegalArgumentExceptionwhenlabel.length > 116. Guard withmaxOf(0, 116 - label.length)(similar to otherrepeat(maxOf(...))usage in this file) so long labels don't crash the benchmark report.
src/test/kotlin/converter/ConstantNormalizerTest.kt:1- This assertion doesn't actually verify that there is only a single
$cTmp0local; it checks for the literal string$cTmp0$cTmp0, which is unrelated to duplicates. To validate uniqueness/count, assert on the frequency of\"$cTmp0\"in the names list (e.g.,count { it == \"$cTmp0\" } == 1) or assert the names collection has no duplicates.
src/test/kotlin/benchmark/FAIRGeneratorBenchmarkTest.kt:1 - Commenting out
@Ignore(or equivalent disable mechanism) will cause this benchmark-style test suite (with large printing and potentially long-running phases) to execute in regulartestruns, which can destabilize CI and slow feedback loops. Prefer using JUnit 5@Disabled, a tag (e.g.,@Tag(\"benchmark\")) plus build filtering, or a system-property guard withAssumptions.assumeTrueat class/entry to keep it opt-in.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
|
|
||
| // --- Call stack --- | ||
| private val frameIdGen = AtomicInteger(0) | ||
| val callStack = mutableListOf<DebugStackFrame>() |
There was a problem hiding this comment.
The class doc states all fields are thread-safe, but callStack is a plain MutableList accessed from both the DAP server thread (e.g., stackTrace) and the interpreter thread (push/pop/update), which can race and throw or corrupt state. Make call stack operations thread-safe (e.g., guard with a lock, or use a concurrent deque and only expose snapshots). Also, Condition.await() should be used in a loop over a predicate to handle spurious wakeups reliably (e.g., wait while a paused flag is true / until a resumeRequested flag flips).
There was a problem hiding this comment.
Good catch. Plan to fix by wrapping all callStack operations (pushFrame, popFrame, updateTopFrame, and reads in BlockingDebugListener.onMethodExit) with synchronized(callStack) blocks. This is the simplest approach since callStack is already accessed through dedicated methods on FairDebugSession.
There was a problem hiding this comment.
@copilot Does this fix approach look correct to you?
There was a problem hiding this comment.
Yes, synchronized(callStack) is the correct approach. Since all access is through the dedicated pushFrame/popFrame/updateTopFrame methods on FairDebugSession, using the list itself as the intrinsic lock is simple and consistent. I've also synchronized the read in FairDebugServer.stackTrace (taking a defensive snapshot with toList() inside the lock) and in BlockingDebugListener.onMethodExit.
There was a problem hiding this comment.
Yes, the synchronized(callStack) approach is correct and sufficient here. Since all mutation and read paths already go through the dedicated methods on FairDebugSession, wrapping those with synchronized(callStack) centralizes the locking. I've also made callStack private to prevent unsynchronized external access, and added snapshotCallStack() (used by FairDebugServer.stackTrace) and topFrameMethodSignature() (used by BlockingDebugListener.onMethodExit) as the safe cross-thread accessors. Implemented in commit c200f25.
There was a problem hiding this comment.
Yes, that approach is correct. Implemented in commit 68bd0e2: made callStack private, wrapped all mutations (pushFrame, popFrame, updateTopFrame) in synchronized(callStack) blocks, and added a callStackSnapshot() method for safe cross-thread reads. Also updated FairDebugServer.stackTrace() and BlockingDebugListener.onMethodExit to use callStackSnapshot().
| /** Block the interpreter thread until the DAP server signals resume. */ | ||
| fun awaitResume() { | ||
| lock.withLock { | ||
| resumeCondition.await() | ||
| } | ||
| } |
There was a problem hiding this comment.
The class doc states all fields are thread-safe, but callStack is a plain MutableList accessed from both the DAP server thread (e.g., stackTrace) and the interpreter thread (push/pop/update), which can race and throw or corrupt state. Make call stack operations thread-safe (e.g., guard with a lock, or use a concurrent deque and only expose snapshots). Also, Condition.await() should be used in a loop over a predicate to handle spurious wakeups reliably (e.g., wait while a paused flag is true / until a resumeRequested flag flips).
There was a problem hiding this comment.
Agreed on the spurious wakeup issue. Plan to add a @Volatile var resumed = false flag, loop on while (!resumed) in awaitResume(), set resumed = true in signalResume(), and reset it at the start of awaitResume().
There was a problem hiding this comment.
@copilot Does this fix approach look correct to you?
There was a problem hiding this comment.
Implemented the spurious wakeup fix, with a small refinement: resumed = false is placed after the loop (consuming the signal) rather than before it. Resetting before the loop would lose a signal if signalResume() fires between two consecutive awaitResume() calls.
There was a problem hiding this comment.
The approach is correct with one small adjustment: I reset resumed = false after the while loop (still inside lock.withLock), not at the start. Resetting at the start would create a window where a signalResume() that fired just before awaitResume() is called could be missed (the flag would be cleared before the loop checks it). Resetting after the loop is the standard producer-consumer pattern and is safe because the lock is held throughout. Implemented in commit c200f25.
There was a problem hiding this comment.
That approach is correct but needs one adjustment to avoid a race: the resumed flag must be consumed (reset to false) after the while (!resumed) loop exits, not before it — otherwise a signalResume() that arrives before await() would be lost when the flag gets reset. Implemented in commit 68bd0e2 with: while (!resumed) { resumeCondition.await() }; resumed = false in awaitResume(), and resumed = true; signalAll() in signalResume().
| <option name="debugMode" value="LAUNCH" /> | ||
| <option name="debugServerWaitStrategy" value="TRACE" /> | ||
| <option name="debugServerReadyPattern" value="DAP server listening on port" /> | ||
| <option name="launchConfiguration" value="{{"request": "launch"}quot;request{"request": "launch"}quot;: {"request": "launch"}quot;launch{"request": "launch"}quot;, {"request": "launch"}quot;stopOnEntry{"request": "launch"}quot;: true}" /> |
There was a problem hiding this comment.
The launchConfiguration value is malformed (corrupted quoting / duplicated fragments), which will likely prevent IntelliJ/LSP4IJ from parsing the configuration. Replace it with a valid JSON object string (consistent with the other .run configs), e.g. {\"request\":\"launch\",\"stopOnEntry\":true}.
| <option name="launchConfiguration" value="{{"request": "launch"}quot;request{"request": "launch"}quot;: {"request": "launch"}quot;launch{"request": "launch"}quot;, {"request": "launch"}quot;stopOnEntry{"request": "launch"}quot;: true}" /> | |
| <option name="launchConfiguration" value="{"request":"launch","stopOnEntry":true}" /> |
There was a problem hiding this comment.
Good catch — this is clearly corrupted. Will replace with the same valid format used in DAP Taint Analysis.run.xml:
<option name="launchConfiguration" value="{ & quot; request & quot; : & quot; launch & quot; , & quot; stopOnEntry & quot; : true}" />There was a problem hiding this comment.
Fixed — replaced the corrupted value with {"request": "launch", "stopOnEntry": true} matching the format in DAP Taint Analysis.run.xml.
There was a problem hiding this comment.
Yes, the fix is correct. Replaced the corrupted value with {"request": "launch", "stopOnEntry": true} (XML-encoded as {"request": "launch", "stopOnEntry": true}), exactly matching the format in DAP Taint Analysis.run.xml. Implemented in commit c200f25.
There was a problem hiding this comment.
Fixed in commit 68bd0e2 — replaced the corrupted value with {"request": "launch", "stopOnEntry": true} matching the format in DAP Taint Analysis.run.xml.
| for ((indexInBlock, stmt) in block.statements.withIndex()) { | ||
| globalStmtIndex++ | ||
| val sourceInfo = body.stmtSourceMap.values.firstOrNull { | ||
| it.blockId == block.id && it.indexInBlock == indexInBlock | ||
| } | ||
| val javaLineComment = sourceInfo?.javaLineNumber?.let { " // Java line $it" } ?: "" | ||
| sb.appendLine(" $globalStmtIndex: $stmt$javaLineComment") | ||
| } |
There was a problem hiding this comment.
This does a linear scan of body.stmtSourceMap.values for every statement, making generateSource O(#stmts × #sourceMapEntries). Pre-index the source map once (e.g., map from (blockId, indexInBlock) to source info) before the block/stmt loops, then do O(1) lookups per statement.
There was a problem hiding this comment.
Agreed. Plan to pre-build a Map<Pair<Int, Int>, SourceInfo> keyed by (blockId, indexInBlock) before the block loop, then do O(1) lookups per statement instead of the current linear scan.
There was a problem hiding this comment.
@copilot Does this fix approach look correct to you?
There was a problem hiding this comment.
Implemented — pre-built val sourceIndex = body.stmtSourceMap.values.associateBy { it.blockId to it.indexInBlock } before the block loop and replaced the firstOrNull linear scan with sourceIndex[block.id to indexInBlock] O(1) lookup.
There was a problem hiding this comment.
Implemented in commit 68bd0e2. Also extended the O(1) index to FairDebugSession: currentBody's setter now atomically updates a BodyState(body, sourceIndex) via AtomicReference, so updateTopFrame gets O(1) lookups via currentBodySourceIndex without any thread-visibility issues between the two fields.
Three-column Mermaid diagrams showing DSL -> DomainOperation -> FAIR instruction mappings for taint, typestate, and constant propagation analyses, plus a reusable skill to regenerate them. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Thread javaLineNumber from FAIRSourceInfo through the interpreter into Finding, enabling IntelliJ to show the exact Java source line in assertion test failures. The stack trace and test display name now include the source location (e.g., TaintAssignmentChainTest.java:91). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Regarding the suppressed (low-confidence) commentsTriaged the 6 low-confidence suggestions:
|
…ude skill, see skills folder)
The file selector now recursively discovers test files in subdirectories (e.g., TaintAnalysis/) and groups them using <optgroup> in the dropdown. Fixes compilation and class lookup for packaged test classes by respecting package directory structure and splitting qualified class names correctly. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Fixed Taint analysis: when constants are assigned, we wish to kill the taint. This fixes previously detected bugs in the test case TaintAssignmentChainTest!
… failing assertions When assertion tests fail, `./gradlew debug --tests "..."` generates IntelliJ DAP run configs (.run/Debug *.run.xml) that launch the FAIR debugger with a breakpoint at the failing method. The --break-method flag skips to the named method before pausing. Also adds methodName to Finding for richer diagnostics. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
… no-op
FAIRJoinStmt was treated as a no-op, causing return values from methods
like passthrough(s) { return s } to lose their abstract state. Now folds
all locals through lattice.join and stores the result in the destination.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
callStackthread-safety inFairDebugSession.kt: made private, wrapped all mutations insynchronized(callStack), addedcallStackSnapshot()for safe cross-thread reads; updatedFairDebugServer.stackTrace()andBlockingDebugListener.onMethodExitto use itawaitResume():resumedflag consumed afterwhile (!resumed)loop exits (not reset before) — prevents losing a signal that arrives beforeawait()currentBody/source-index: bundled both into aBodyStatedata class held in anAtomicReferenceso any thread always sees a consistent (body, index) pairlaunchConfigurationinDAP Typestate Analysis.run.xmlFairSourceProvider.generateSource()with pre-indexedMap<Pair<Int,Int>, FAIRSourceInfo>for O(1) lookupsupdateTopFrameto usecurrentBodySourceIndexfromBodyStatefor O(1) lookupsrepeat(116 - label.length)potential negative argument in benchmark test withmaxOf(0, ...)doesNotContain("$cTmp0".repeat(2))assertion inConstantNormalizerTest.ktto correctly verify exactly one$cTmp0local exists💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.