LM is a typed assembler. It takes “Zero Cost Abstraction” to the logical conclusion of permitting any and all binary code to be generated. The language itself is functional, however the generated code need not be. It is intended to provide a backend for the LSTS compiler and proof assistant.
One Code, Many Representations
One of the concepts introduced in LM is code equivalence and metric driven instruction selection. Take for example the code:
x = 0;
This code may be naively represented with a simple mov
instruction. We will say that x
is stored in a register to make the code simpler.
mov $0, %r8
A slightly better instruction selection may take advantage of the fact that the constant 0
is assigned to x
.
xor %r8, %r8
When declaring code we can define instruction selection in a fairly straightforward manner using types.
mov := λ(: src Imm64)(: tgt Register64). asm!( 'mov \s src , \s tgt \n );
mov := λ(: src Imm64/0)(: tgt Register64). asm!( 'xor \s tgt , \s tgt \n );
Here the second representation is said to be preferred. It is a very simple optimization, however the code is hopefully a bit cleaner than typical compiler guts.
Compiler Benchmarks
The compiler compiles itself in 0m0.078s
. The memory pressure is a little higher than it needs to be, but there are some simple optimizations to make it much more efficient.
Future Work
Notably something that is missing from the compiler is blame tracking. The error messages are currently inadequate or entirely non-existent. It is maybe a little early to call this version anywhere near complete. However it is stable enough to compile itself and assemble a decently large class of useful programs.