A new major version of the Jasmin compiler has just been released. Some noteworthy changes are listed below. More details can be found in the CHANGELOG.

New target: ARMv8-A

The Jasmin compiler is now able to emit assembly for 64-bit ARM processors. As this feature is rather new, it is expected to have limitations and issues. Please do report them so that they can be fixed.

Semantics of the Jasmin language now defined using “interaction trees”

This is a rather technical change: users might not notice it. Just note that the compiler correctness theorem now also applies to non-terminating programs. Therefore, the safety checker no longer needs to ensure termination.

Changes regarding extraction to EasyCrypt

There is now finer control over the extraction of global variables and literal values.

Moreover, in addition to bug fixes & updates, the description of x86 instructions is now only exposed in JModel_x86 (as opposed to the more general JWord module).

Preliminary support for safety assertions

Jasmin source programs can be decorated with safety assertions: as assert(message, condition) instructions within function bodies or as pre- and post-conditions annotating function definitions.

Compiler interface

A few legacy command-line options to the compiler have been removed: -lea, -nolea, -set0, -noset0, and -noinsertarraycopy.

There is a new jasmin-checksafety interface to the safety checker.

Polishing of the semantics

The formal description of a few machine instructions have been made more accurate. In particular the DIT/DOIT information (about execution time being independent of the values of the operands) is more precise. Alignment requirements of some instructions have also been corrected.