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 printf in 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 opam command 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 align in 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-tests flag to enable alive2 tests which check for poison (currently none).
  • Added -enable-srctgt-tests flag to enable the GenAlive2 random testing.
• Fix typos in intrinsic error messages ("intputs" -> "inputs").
• Add ushl_sat intrinsic, and update proofs.
• Add mmax_unsigned to VMemInt class.
• Make sure generated store instructions have void type in GenAlive2.
• Fix COQ_VERSION and OCAML_VERSION in the Makefile (used for make pin-coq for 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