Skip to content

Conversation

@RyanGlScott
Copy link
Collaborator

Towards GaloisInc/llvm-pretty-bc-parser#306.


Marked as a draft for now, as I do not intend to merge this until after the next llvm-pretty Hackage release.

RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Oct 29, 2025
LLVM 18 adds an `nneg` flag to `zext` instructions, which enforces that the
argument must be non-negative. Per the LLVM Language Reference
(https://releases.llvm.org/18.1.0/docs/LangRef.html#id245), if `nneg` is set
and the argument is negative, then `zext` should return a poisoned value. See
also GaloisInc/llvm-pretty-bc-parser#306.

This makes the necessary changes to `crucible-llvm` to implement these
semantics.

This bumps the following submodules:

* GaloisInc/llvm-pretty#169
* GaloisInc/llvm-pretty-bc-parser#317
RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Oct 29, 2025
LLVM 19 adds an `nneg` flag to `uitofp` instructions, which enforces that the
argument must be non-negative. Per the LLVM Language Reference
(https://releases.llvm.org/19.1.0/docs/LangRef.html#id277), if `nneg` is set
and the argument is negative, then `uitofp` should return a poisoned value. See
also GaloisInc/llvm-pretty-bc-parser#306.

This makes the necessary changes to `crucible-llvm` to implement these
semantics.

This bumps the following submodules:

* GaloisInc/llvm-pretty#169
* GaloisInc/llvm-pretty-bc-parser#317
RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Oct 29, 2025
LLVM 20 adds `nuw` and `nsw` flags to `trunc` instructions, which enforces that
unsigned and signed overflow should not occur, respectively. Per the LLVM
Language Reference (https://releases.llvm.org/20.1.0/docs/LangRef.html#id243),
if overflow does occur, then `trunc` should return a poisoned value. See also
GaloisInc/llvm-pretty-bc-parser#306.

This makes the necessary changes to `crucible-llvm` to implement these
semantics.

This bumps the following submodules:

* GaloisInc/llvm-pretty#169
* GaloisInc/llvm-pretty-bc-parser#317
RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Oct 31, 2025
LLVM 18 adds an `nneg` flag to `zext` instructions, which enforces that the
argument must be non-negative. Per the LLVM Language Reference
(https://releases.llvm.org/18.1.0/docs/LangRef.html#id245), if `nneg` is set
and the argument is negative, then `zext` should return a poisoned value. See
also GaloisInc/llvm-pretty-bc-parser#306.

This makes the necessary changes to `crucible-llvm` to implement these
semantics.

This bumps the following submodules:

* GaloisInc/llvm-pretty#169
* GaloisInc/llvm-pretty-bc-parser#317
RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Oct 31, 2025
LLVM 19 adds an `nneg` flag to `uitofp` instructions, which enforces that the
argument must be non-negative. Per the LLVM Language Reference
(https://releases.llvm.org/19.1.0/docs/LangRef.html#id277), if `nneg` is set
and the argument is negative, then `uitofp` should return a poisoned value. See
also GaloisInc/llvm-pretty-bc-parser#306.

This makes the necessary changes to `crucible-llvm` to implement these
semantics.

This bumps the following submodules:

* GaloisInc/llvm-pretty#169
* GaloisInc/llvm-pretty-bc-parser#317
RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Oct 31, 2025
LLVM 20 adds `nuw` and `nsw` flags to `trunc` instructions, which enforces that
unsigned and signed overflow should not occur, respectively. Per the LLVM
Language Reference (https://releases.llvm.org/20.1.0/docs/LangRef.html#id243),
if overflow does occur, then `trunc` should return a poisoned value. See also
GaloisInc/llvm-pretty-bc-parser#306.

This makes the necessary changes to `crucible-llvm` to implement these
semantics.

This bumps the following submodules:

* GaloisInc/llvm-pretty#169
* GaloisInc/llvm-pretty-bc-parser#317
RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Oct 31, 2025
LLVM 18 adds an `nneg` flag to `zext` instructions, which enforces that the
argument must be non-negative. Per the LLVM Language Reference
(https://releases.llvm.org/18.1.0/docs/LangRef.html#id245), if `nneg` is set
and the argument is negative, then `zext` should return a poisoned value. See
also GaloisInc/llvm-pretty-bc-parser#306.

This makes the necessary changes to `crucible-llvm` to implement these
semantics.

This bumps the following submodules:

* GaloisInc/llvm-pretty#169
* GaloisInc/llvm-pretty-bc-parser#317
RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Oct 31, 2025
LLVM 19 adds an `nneg` flag to `uitofp` instructions, which enforces that the
argument must be non-negative. Per the LLVM Language Reference
(https://releases.llvm.org/19.1.0/docs/LangRef.html#id277), if `nneg` is set
and the argument is negative, then `uitofp` should return a poisoned value. See
also GaloisInc/llvm-pretty-bc-parser#306.

This makes the necessary changes to `crucible-llvm` to implement these
semantics.

This bumps the following submodules:

* GaloisInc/llvm-pretty#169
* GaloisInc/llvm-pretty-bc-parser#317
RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Oct 31, 2025
LLVM 20 adds `nuw` and `nsw` flags to `trunc` instructions, which enforces that
unsigned and signed overflow should not occur, respectively. Per the LLVM
Language Reference (https://releases.llvm.org/20.1.0/docs/LangRef.html#id243),
if overflow does occur, then `trunc` should return a poisoned value. See also
GaloisInc/llvm-pretty-bc-parser#306.

This makes the necessary changes to `crucible-llvm` to implement these
semantics.

This bumps the following submodules:

* GaloisInc/llvm-pretty#169
* GaloisInc/llvm-pretty-bc-parser#317
RyanGlScott added a commit to GaloisInc/saw-script that referenced this pull request Oct 31, 2025
This bumps the `llvm-pretty`, `llvm-pretty-bc-parser`, and `crucible`
submodules in order to bring in several downstream changes that, in total,
allow SAW to support LLVM versions up to 20. These include:

* `llvm-pretty`:
  GaloisInc/llvm-pretty#168,
  GaloisInc/llvm-pretty#169, and
  GaloisInc/llvm-pretty#170

* `llvm-pretty-bc-parser`:
  GaloisInc/llvm-pretty-bc-parser#316,
  GaloisInc/llvm-pretty-bc-parser#317, and
  GaloisInc/llvm-pretty-bc-parser#318

* `crucible`:
  GaloisInc/crucible#1600,
  GaloisInc/crucible#1602,
  GaloisInc/crucible#1603, and
  GaloisInc/crucible#1606

The only code changes that had to be made in SAW itself involve the LLVM
backend's skeleton-related commands, which look up debug metadata to figure out
which variables are declared. For the time being, I have opted not to make
these commands look into LLVM's new debug records to find equivalent
information, although it probably should. (TODO RGS: Open an issue about this.)
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.

4 participants