Skip to content

Fix unsound multiplication in Sign domain#361

Merged
lucaneg merged 1 commit intomasterfrom
fix-sign-multiplication-soundness
Apr 15, 2026
Merged

Fix unsound multiplication in Sign domain#361
lucaneg merged 1 commit intomasterfrom
fix-sign-multiplication-soundness

Conversation

@giacomozanatta
Copy link
Copy Markdown
Collaborator

@giacomozanatta giacomozanatta commented Apr 14, 2026

Description
When evaluating a binary expression with a MultiplicationOperator, if both operands are TOP, the implementation of the Sign Domain incorrectly returns +. However, since TOP represents any value (+, −, or 0), TOP × TOP should return TOP.
Similarly, if only one operand is TOP, the implementation retruns −, but TOP × + ≠ −.

Fixed bugs
No open issue related to this bug.

Implemented features
Added an isTop() guard: if either operand is TOP, the operation now returns TOP.

Further content
None.

@giacomozanatta giacomozanatta requested a review from lucaneg as a code owner April 14, 2026 07:51
@giacomozanatta giacomozanatta added the 🐛 type:bug Something isn't working label Apr 14, 2026
@lucaneg lucaneg added this to LiSA Apr 14, 2026
@lucaneg lucaneg added the 🏗 resolution:wip Incomplete work - do not review yet label Apr 14, 2026
@lucaneg lucaneg moved this to PR WIP in LiSA Apr 14, 2026
@lucaneg lucaneg added ⁉ priority:p2 Priority planning - level 2 🔍 scope:analysis Work regarding abstract domains or fixpoint algorithms and removed 🏗 resolution:wip Incomplete work - do not review yet labels Apr 15, 2026
@lucaneg lucaneg added this to the 1.0 milestone Apr 15, 2026
@lucaneg lucaneg moved this from PR WIP to PR Ready in LiSA Apr 15, 2026
@lucaneg lucaneg merged commit 16fe4e8 into master Apr 15, 2026
4 checks passed
@lucaneg lucaneg deleted the fix-sign-multiplication-soundness branch April 15, 2026 07:13
@github-project-automation github-project-automation Bot moved this from PR Ready to PR Merged in LiSA Apr 15, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

⁉ priority:p2 Priority planning - level 2 🔍 scope:analysis Work regarding abstract domains or fixpoint algorithms 🐛 type:bug Something isn't working

Projects

Status: PR Merged

Development

Successfully merging this pull request may close these issues.

2 participants