Vincent Laporte

Remove deprecated legacy interface to the CT checker

2

Let’s make some room for a better interface.

Compiling the following program crashes at asm-generation time: ~~~ export fn bad_inc(reg u64 p) { [p + 8] = [p] + 1; } ~~~ Stack-allocation is not aware of x86...

The Jasmin compiler use `rectypes` in the type of expressions: this might not be needed.

The following program is well-typed, yet, it is rejected by the pre-typing phase (since version 2022.04). ~~~ fn id(reg u64 x) -> reg u64 { return x; } inline fn...

Unused stack variable “may not be initialized”

1

Compilation of the program below fails with: > variable allocation: variable “s.159” (declared at "bug_680.jazz", line 3 (12-13)) may not be initialized ~~~ export fn adc_stack(reg u64 x) { stack...

Compilation of the following program crashes with: > "bug_681.jazz", line 6 (2-8): compilation error in function load_small: asmgen: invalid rexpr for oprd (32)[RSP + ((64u) 0)] invalid Load size It...

~~~ export fn add_stack(reg u64 x) { stack u64 s; s = 0; ?{}, _ = #ADD(s, x); } ~~~ The `Regalloc.fill_in_missing_names` function creates a variable of kind `reg` for...

Release with ARM support

1

This gathers things to happen before a release of Jasmin with ARM support can happen. ### Required - [ ] Extraction to EasyCrypt (#366) - Started: #417 - Continued: #460...

The safety checker is not ready to handle programs using SLH primitives, e.g., ~~~ export fn main() { reg u64 ms; stack u8[8] s; reg ptr u8[8] p; p =...