Release 2023.06.0 of the Jasmin compiler
A new major version of the Jasmin compiler has just been released. It contains a few fixes and additions whose details can be found in the CHANGELOG. Below are a few highlights.
Local functions use CALL
and RET
instructions
Calls to local functions that expect a return address on the stack are now
compiled using the standard CALL
instruction rather than a direct jump.
Therefore, returns from such functions are compiled using the RET
instruction
rather than a computed jump.
Moreover, it is now the default that local functions expect their return address
on the stack. This is a breaking change: the old behavior (return address in a
register; call using a direct jump; return using a computed jump) is still
available using the #[returnaddress=reg]
annotation.
Enhancements to the automated safety checker
The Jasmin language is rather strict regarding memory alignment. The safety checker requires user code (as opposed to code introduced by the compiler) to comply with requirements that are stricter than what microprocessors actually enforce. There is now a command-line flag to weaken these checks.
While loops may now be annotated in two ways to fine-tune the safety analysis.
Loops tagged as #[bounded]
will be fully unrolled at analysis time: this may
improve the precision. This can prove particularly useful when loops initialize
arrays. Beware that the analyzer blindly follows this hint: if no constant upper
bound to the number of iteration can be found, analysis will loop forever.
The second annotation is #[no_termination_check]
: to be used when the
termination proof is out of reach of the automated tool.
Note that these annotations are ignored by the compiler and other tools.
Experimental support of the ARMv7 architecture
The compiler is now able to emit assembly from the ARMv7 instruction set, meaning that Jasmin programs can now be run, for instance, on Cortex-M4 microprocessors. This feature is still experimental: do not hesitate to contribute bug reports.
Changes to the semantics of shift and rotation operators
Shift and rotation operators used to truncate their second operand (the shift
amount) to the word size. This behavior matches the semantics of the x86
instructions but differs from the semantics of the arm
instructions.
In this version, this implicit truncation is no longer present. It is still
possible to explicitly ask for the old behavior (in particular this might be
required when compiling to x86
) and add a bitwise AND, e.g., x <<= c & 63
.
Beware of the relative priorities of the shift and AND operators: parentheses
are needed in instructions such as x = y << (c & 63)
.
Other noteworthy changes
The build system uses dune
instead of ocamlbuild
; this is only relevant when
manually building from sources (as opposed to installing using a package
manager).
The EasyCrypt library that supports verification of Jasmin programs is now distributed with the compiler.
The latex pretty-printer is now available as a separate jazz2tex
binary.