jasmin-lang / jasmin

Language for high-assurance and high-speed cryptography
MIT License
271 stars 55 forks source link

stack alloc: relax the checker #841

Closed eponier closed 5 months ago

eponier commented 5 months ago

Before this patch, an assignment a = b, where a and b are two arrays, was allowed only if b was fully valid, and a was marked as fully valid too. After this patch, b does not need to be fully valid, and a is marked as having the same validity as b.

The motivation was to enable more freedom in the spilling of reg ptr. In particular, I needed the following pattern to be accepted.

reg ptr u64[N*K] r;
reg ptr u64[N] p;

for i = 0 to K {
  p = r[N*i:N];
  () = #spill (r); // f is using a lot of registers, so we have to spill as much as we can
  p = f (p);
  () = #unspill (r); // r is not fully valid due to the call, so this was rejected before
  r[N*i:N] = p;
}
eponier commented 5 months ago

I had a hard time trying to describe the change in the changelog, without entering the details of the checker. If you have a better formulation, then go ahead.

eponier commented 5 months ago

Also, I put the new tests in a x86-64 subfolder because there were tests on subarrays there, but what is tested is not x86-specific.