Releases: vellvm/vellvm
v2.2.20250710
What's Changed
- Preliminary support for the invoke/resume instructions 57767b9
- These changes introduce a new LLVMExcE event type. There are also preliminary changes to the Stack events for handling exceptions, which are currently unused.
- Make sdiv poison, -1 be poison #383
- Parse landingpad by @Zdancewic in #384
- Remove EOL from parser 40e120c
Full Changelog: v2.1.20250327...v2.2.20250710
Contributors
Assets 3
v2.1.20250327
This release updates Vellvm to Rocq 9.0, as well as a few small changes. This release also changes the opam package to rocq-vellvm
Semantic Changes:
- Branching on
undefis now treated as UB (53f8dba)
General Updates:
- Grand renaming of coq -> rocq
- Update imports to use Stdlib everywhere
- Remove usage of deprecated lemmas
- Fix various miscellaneous warnings from Rocq
- Version bumps for ExtLib and Paco
- Updated READMEs
Notably Rocq 9.0 also seems to have substantially improved the compilation time for Vellvm :)
Full Changelog: v2.0.20250110...v2.1.20250327
v2.0.20250110
This is a major release for Vellvm with some significant changes to the LLVM AST, padding, and support for some new features.
Features:
- Support for opaque pointer types: https://llvm.org/docs/OpaquePointers.html
- Support for command-line arguments (argc / argv) when interpreting LLVM IR programs
- Support for variable argument functions (https://llvm.org/docs/LangRef.html#va-arg-instruction)
- Support for
printfin LLVM IR programs - Rudimentary linker support (#369)
- Appropriate padding calculations for 64-bit LLVM (and fix sizeof to account for this)
- Support for arbitrary bitwidth integers in LLVM IR (
i8s,i12s, etc... Any bitwidth is supported) - GEP now supports signed indices
- Support for coq 8.20
Misc fixes:
- Fix lexer bugs (9a26822, 1b3dc5a)
- Update the
make opamcommand in the Makefile to use the dependencies in the.opam file - README fixes (adding ICFP24 paper, authors, etc)
- Various fixes to QC generators
- Performance improvements, particularly around string operations (dfbde64)
- Version bumps
Full Changelog: v1.0.20240627...v2.0.20250110
v1.0.20240627
Full Changelog: v1.0.20240610...v1.0.20240627
Minor bug fixes to the print-ast functionality (#367)
v1.0.20240610
This release is a revision with a few bug fixes to the pretty printer, adjustments to the test suite, and the introduction of the ushl_sat intrinsic.
Full Changelog: v1.0.20240416...v1.0.20240610
- Fix bug with
alignin the LLVM IR pretty printer. - Fix pretty printing in call instructions where the function is an expression.
- Adjust test suite
- Fix bug in assertion style tests where doubles were converted into floats.
- Cleaned out some alive2 test cases that don't make sense in vellvm.
- Fix some nan assertion tests that were ported from the test-suite incorrectly.
- Added
-enable-poison-testsflag to enable alive2 tests which check for poison (currently none). - Added
-enable-srctgt-testsflag to enable the GenAlive2 random testing.
- Fix typos in intrinsic error messages ("intputs" -> "inputs").
- Add
ushl_satintrinsic, and update proofs. - Add mmax_unsigned to VMemInt class.
- Make sure generated
storeinstructions havevoidtype in GenAlive2. - Fix COQ_VERSION and OCAML_VERSION in the Makefile (used for make
pin-coqfor instance). - Adjustments to README for how to install dependencies with opam.
v1.0.20240416: initial opam release
This is the initial opam release of vellvm with the new memory model.
ICFP 2021 Artifact
This is a release marking the artifact submission for the paper "Modular, compositional, and executable formal semantics for LLVM IR" at ICFP 2021
https://dl.acm.org/doi/10.1145/3473572
This artifact can also be accessed from: https://zenodo.org/record/4777196