jasmin-lang / jasmin

Language for high-assurance and high-speed cryptography
MIT License
250 stars 53 forks source link

An example where stack alloc could be smarter #57

Open eponier opened 3 years ago

eponier commented 3 years ago

On the following example

fn f (reg ptr u64[2] r) -> reg u32 {
  reg u32 res;
  stack u64[2] a;
  stack u32[10] b;
  a[0]=0;
  b[1:2] = a[u32 0:2];
  res = b[1];
  return res;
}

jasmin returns an error about a bad alignment. This is because the stack alloc oracle (in OCaml) decides to align one slot to contain both a and b aligned on 64 bits and with b at the beginning of the slot. Due to the assignment b[1:2] = a[u32 0:2];, a is aligned on 32 bits but not 64, thus it cannot perform a[0]=0. The allocator could rather decide to add some padding, either before or inside the slot. In that second option, it could allocate a larger slot and put b 32 bits after the start of the slot. Then a would be aligned on 64 bits and the assignment a[0] = 0 would succeed.

This is really low-priority. This is an artificial example that I created to trigger the "bad alignment" error.

eponier commented 3 years ago

At least it's possible to circumvent that (but still not sure if there is a real use case and if it's worth thinking about that problem).

fn f (reg ptr u64[2] r) -> reg u32 {
  reg u32 res;
  stack u64[2] a;
  stack u32[10] b;
  stack u32[11] c; // larger slot
  a[0]=0;
  c[1:10] = b; // useless copy
  b = c[1:10]; // useless copy back
  b[1:2] = a[u32 0:2];
  res = b[1];
  return res;
}

The idea is to introduce an array just to create a larger slot. Then making useless copies to make the stack allocator understand how to use this larger slot.