Skip to content

Explainability#353

Merged
lucaneg merged 32 commits intomasterfrom
explainability
Jan 21, 2026
Merged

Explainability#353
lucaneg merged 32 commits intomasterfrom
explainability

Conversation

@lucaneg
Copy link
Member

@lucaneg lucaneg commented Dec 22, 2025

Adding features to increase the understandability of the results.

  • fixpoint with history, implemented as an abstract state
  • event queue to use as comunication channel between the fixpoint and some listeners
  • listeners for producing traces of fixpoints
  • listeners for producing notices on call resolutions
  • listeners for producing notices on unexpected bottom states

Implemented features
Closes #334

@lucaneg lucaneg added this to the 0.2 milestone Dec 22, 2025
@lucaneg lucaneg self-assigned this Dec 22, 2025
Copilot AI review requested due to automatic review settings December 22, 2025 09:16
@lucaneg lucaneg added 🎆 type:feature New feature or request ‼ priority:p1 Priority planning - level 1 🏨 scope:infrastructure Work regarding the general infrastructure and functioning of LiSA labels Dec 22, 2025
@lucaneg lucaneg added this to LiSA Dec 22, 2025
@lucaneg lucaneg moved this to PR WIP in LiSA Dec 22, 2025
@lucaneg lucaneg added the 🏗 resolution:wip Incomplete work - do not review yet label Dec 22, 2025
Copy link

Copilot AI left a comment

Choose a reason for hiding this comment

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

Pull request overview

This PR adds "explainability" features to increase the understandability of analysis results. The main contribution is a fixpoint history tracking mechanism implemented as an abstract state. This allows users to see how abstract values evolve during fixpoint iterations.

Key changes include:

  • Introduction of upchain and downchain operations to distinguish fixpoint traversal from general lattice operations (lub/glb)
  • Implementation of HistoryState and HistoryDomain classes that wrap existing lattices to track fixpoint iteration history
  • Refactoring all fixpoint implementations to use the new operations

Reviewed changes

Copilot reviewed 51 out of 53 changed files in this pull request and generated 1 comment.

Show a summary per file
File Description
Lattice.java Adds upchain and downchain interface methods with comprehensive documentation
BaseLattice.java Provides default implementations that delegate to lubAux/glbAux
HistoryState.java New class implementing history tracking with recursive stack structure
HistoryDomain.java New domain wrapper that delegates operations while preserving history
CompoundState.java Implements new operations by delegating to composed states
Various fixpoint classes Replace lub/glb calls with upchain/downchain in join operations
Test files Add tests for history tracking, rename test method, update test infrastructure
IMP test cases Formatting fixes (whitespace) and new JSON output files for history tests

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

@lucaneg lucaneg requested a review from Copilot January 16, 2026 17:35
Copy link

Copilot AI left a comment

Choose a reason for hiding this comment

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

Pull request overview

Copilot reviewed 296 out of 491 changed files in this pull request and generated no new comments.


💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

@lucaneg lucaneg requested a review from Copilot January 19, 2026 08:10
Copy link

Copilot AI left a comment

Choose a reason for hiding this comment

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

Pull request overview

Copilot reviewed 296 out of 491 changed files in this pull request and generated no new comments.


💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

@lucaneg lucaneg requested a review from Copilot January 20, 2026 22:22
Copy link

Copilot AI left a comment

Choose a reason for hiding this comment

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

Pull request overview

Copilot reviewed 157 out of 551 changed files in this pull request and generated no new comments.


💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

@lucaneg lucaneg removed the 🏗 resolution:wip Incomplete work - do not review yet label Jan 21, 2026
@lucaneg lucaneg moved this from PR WIP to PR Ready in LiSA Jan 21, 2026
@lucaneg lucaneg merged commit b7ac18a into master Jan 21, 2026
3 checks passed
@lucaneg lucaneg deleted the explainability branch January 21, 2026 06:00
@github-project-automation github-project-automation bot moved this from PR Ready to PR Merged in LiSA Jan 21, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

‼ priority:p1 Priority planning - level 1 🏨 scope:infrastructure Work regarding the general infrastructure and functioning of LiSA 🎆 type:feature New feature or request

Projects

Status: PR Merged

Development

Successfully merging this pull request may close these issues.

[FEATURE REQUEST] Explainability

2 participants