Custom state on analysis init + custom call return logic#346
Merged
Conversation
There was a problem hiding this comment.
Pull request overview
This PR adds support for custom call return logic and custom initial states in the analysis framework. It introduces the onCallReturn method to both SemanticDomain and SemanticComponent interfaces, allowing domains to restore or modify state when execution returns from a callee. Additionally, it updates makeLattice to define the initial analysis state.
Key changes:
- Added
onCallReturnmethod to enable custom state restoration after function calls - Enhanced
makeLatticedocumentation to clarify it returns the initial analysis state - Refactored initial state setup from
LiSARunnerintoAnalysis.makeLatticefor better encapsulation
Reviewed changes
Copilot reviewed 11 out of 11 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| SemanticDomain.java | Added abstract onCallReturn method and updated makeLattice documentation |
| SemanticComponent.java | Added default onCallReturn method implementation and updated makeLattice documentation |
| Analysis.java | Implemented onCallReturn and enhanced makeLattice to properly initialize analysis state |
| LiSARunner.java | Simplified to use analysis.makeLattice() directly, removing local state initialization |
| ContextBasedAnalysis.java | Integrated onCallReturn call after unscoping to restore caller state |
| TestAbstractDomain.java | Added trivial onCallReturn implementation for test domain |
| TracePartitioning.java | Added onCallReturn implementation with TODO for trace matching, updated makeLattice to return top |
| NonInterference.java | Implemented onCallReturn to restore non-interference guards from caller |
| SimpleAbstractDomain.java | Delegated onCallReturn to component domains and updated makeLattice to return top |
| Reachability.java | Implemented onCallReturn to restore reachability status and updated makeLattice to start as reachable |
| DomainWithReplacement.java | Fixed documentation comment from SemanticDomain to SemanticComponent |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/Reachability.java
Show resolved
Hide resolved
lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/informationFlow/NonInterference.java
Show resolved
Hide resolved
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
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.
Description
SemanticDomain#makeLatticecan now create arbitrary lattice elements that are kept as starting states for the analysis.SemanticDomainnow also has aonCallReturnthat allows custom modifications to the state returned by calls.Fixed bugs
Closes #256