Data

Tools

Indexes

Applications

Experiments

Open Source Science

Recent Releases of vellvm

vellvm - v2.2.20250710

What's Changed

  • Preliminary support for the invoke/resume instructions https://github.com/vellvm/vellvm/commit/57767b950f943f55851e143af4c5876a510e1069
  • 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 https://github.com/vellvm/vellvm/issues/383
  • Parse landingpad by @Zdancewic in https://github.com/vellvm/vellvm/pull/384
  • Remove EOL from parser https://github.com/vellvm/vellvm/commit/40e120c10ae0cd837364ba4e534afdd2ca1b3008

Full Changelog: https://github.com/vellvm/vellvm/compare/v2.1.20250327...v2.2.20250710

- LLVM
Published by Chobbes 8 months ago

vellvm - 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 undef is now treated as UB (https://github.com/vellvm/vellvm/commit/53f8dba3d7d12caf8978351058878d3029a80aa0)

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: https://github.com/vellvm/vellvm/compare/v2.0.20250110...v2.1.20250327

- LLVM
Published by Chobbes 11 months ago

vellvm - 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 (9a268223, 1b3dc5a1)
  • 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 (dfbde64d)
  • Version bumps

Full Changelog: https://github.com/vellvm/vellvm/compare/v1.0.20240627...v2.0.20250110

- LLVM
Published by Chobbes about 1 year ago

vellvm - v1.0.20240627

Full Changelog: https://github.com/vellvm/vellvm/compare/v1.0.20240610...v1.0.20240627

Minor bug fixes to the print-ast functionality (https://github.com/vellvm/vellvm/issues/367)

- LLVM
Published by Chobbes over 1 year ago

vellvm - 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: https://github.com/vellvm/vellvm/compare/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 COQVERSION and OCAMLVERSION in the Makefile (used for make pin-coq for instance).
  • Adjustments to README for how to install dependencies with opam.

- LLVM
Published by Chobbes over 1 year ago

vellvm - 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

- LLVM
Published by Chobbes almost 2 years ago

vellvm - v1.0.20240416: initial opam release

This is the initial opam release of vellvm with the new memory model.

- LLVM
Published by Chobbes almost 2 years ago