Jean-Christophe Léchenet

Sort out the interaction between scopes of variables

1

I create this issue to have something written down. In pretyping, we have 3 kinds of variables : param, global and local, and it seems to me that the interactions...

Mutable arguments that are not meant to be returned

5

Apparently before PR https://github.com/jasmin-lang/jasmin/pull/82, some people were relying on a pattern involving inline functions and `reg ptr` arguments used as a scratchpad. Here is a small example. ``` inline fn...

Test the extraction to EasyCrypt

1

We were reported a few bugs (https://github.com/jasmin-lang/jasmin/issues/128, https://github.com/jasmin-lang/jasmin/issues/130, https://github.com/jasmin-lang/jasmin/issues/135) of the extraction to EasyCrypt recently, it would be good to have tests for it, because it seems we have none...

Benjamin tried to extract `examples/test_set0.jazz` and to parse the output with EasyCrypt and it appeared that `MOV` was not known as an operator.

Errors from array expansion are not clear

1

In particular, the one reading `cannot expand variable ? (defined at line ?) (the default scale must be used)`. Probably adding the involved `wsize` and/or rephrasing could help.

In the following code ``` fn f (reg const ptr u64[2] a) -> reg u64 { reg u64 res; reg mut ptr u64[2] b; b = a; b[0] = 1;...

EasyCrypt in Jasmin's CI

2

- what version of EasyCrypt shoud we use? - what do we want to test?

Errors with array copies

1

If we copy a stack array into a reg array, we can easily get errors. It is enough to have the size of the target array (in bytes) not a...

Long term work

"type mismatch" after reg alloc

2

I don't know if my program makes any sense, but compiling it gives an internal compilation error produced by the allocation checker after reg alloc. ``` export fn main ()...