Skip to content

Added translation for LLVM FNeg instruction. #291

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Apr 24, 2025

Conversation

PhilipBotha
Copy link
Contributor

@PhilipBotha PhilipBotha commented Oct 12, 2024

Added translation for LLVM FNeg instruction. No hint.
Implementation is a modification of the patch by @phoon0416. Using multiplcation by -1.0 instead of subtracting from -0.0.
Added two tests, one for float and one for double that should successfully be analysed with ikos with the FNeg addition without throwing an unsupported LLVM instruction exception.

From the LLVM Language reference manual

The value produced is a copy of the operand with its sign bit flipped. The value is otherwise completely identical; in particular, if the input is a NaN, then the quiet/signaling bit and payload are perfectly preserved.

Using compiler explorer to test:
Using (-0.0) - NaN does not flip the bit. Same with -1.0 * NaN. -NaN does flip the bit.

The code in this PR does not quite adhere to the LLVM requirements of FNeg, but should cover most use cases.

@PhilipBotha
Copy link
Contributor Author

Outstanding with this PR is the location and running of the two test cases for verifying that the ikos can now handle LLVM FNeg instructions.

@PhilipBotha PhilipBotha marked this pull request as draft October 12, 2024 12:26
@ivanperez-keera
Copy link
Collaborator

This PR seems ready to be merged, and based on this comment, it's all working well.

@PhilipBotha , if you are ready, can you please 1) mark it as ready for review and 2) if you haven't already, can you please sign one of the two CLAs (whichever applies to your situation): https://github.com/NASA-SW-VnV/ikos/tree/master/doc/contribute and send it to [email protected], CC-ing [email protected].

@ivanperez-keera ivanperez-keera marked this pull request as ready for review April 24, 2025 06:39
IKOS does not understand the LLVM unary instruction fneg, which returns the
negation of its operand. This makes common C programs fail to be processed by
IKOS, which stops with a message like:

```
ikos-analyzer: <some_source.pp.bc>: error: unsupported llvm instruction fneg [2]
ikos: error: a run-time error occurred
```

This commit adds to IKOS' frontend the translation of the fneg instruction.  It
also adds two tests that use fneg, one with float and one with double, which
should be analyzable with IKOS.
@ivanperez-keera ivanperez-keera merged commit ac7f7c1 into NASA-SW-VnV:master Apr 24, 2025
1 of 2 checks passed
@ivanperez-keera
Copy link
Collaborator

@PhilipBotha Thank you for your contribution. Your form was received and processed, and this PR merged.

Future contributions will not require sending another form, so they should be easier and quicker to process.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants