"cannot put a reg ptr argument into the local stack": no location

[eponier]

trafficstars

With the following code

fn f (reg ptr u64[3] r) -> reg u64 {
  reg u64 res;
  stack u64[3] s;
  s = r;
  res = s[0];
  return res;
}

we get the error cannot put a reg ptr argument into the local stack but with no location, so it can be difficult to know what is the source of the error.

This is not trivial to solve since the code that emits this error does not have the locations at hand.

[eponier]

@vbgl do you have an idea to improve the current situation?

[vbgl]

Could this kind of error be caught earlier? Say by some type-checking pass?

Otherwise, you have the name of the function and the name of the argument. This can be use to slightly improve the message.

[eponier]

This may be possible to reject this kind of assignment by type-checking, but this is not trivial, since stack array = reg ptr array is allowed in general. One would have to check that the reg ptr is an argument to reject this instruction. And we may have to do something also for sub-arrays...

For the moment, it is certainly easier to make the smallest move and just print the function and the name of the argument.

Another solution could be to remove the OCaml check and fail due to the Coq checker. The error message would be less precise (we would get that the regions associated to the variables are not equal), but we would get the line of the instruction.

[vbgl]

Also, it seems hard to blame a particular instruction: there might be a long sequence of assignments and array slicing (or even a DAG) inducing the aliasing constraint between a local stack variable and a function parameter, without any instruction involving both of them, right?

[eponier]

I don't understand the code enough to answer properly, but this is plausible. Ok, I'll go with the lightest solution.

[vbgl]

Here is an example. Which line would you like to blame?

fn f(reg ptr u64[1] arg) -> reg u64 {
  stack u64[1] s;
  reg ptr u64[1] x y;
  reg u64 z;
  s[0] = 42;
  x = s[0:1];
  y = arg;
  x[0:1] = y[0:1];
  z = s[0];
  z += x[0];
  return z;
}

[eponier]

I'd say line x[0:1] = y[0:1] (and this is the line reported by the Coq verifier if I disable the check in the OCaml code).

[eponier]

But once again, the error reported by the OCaml code is probably clearer for the user than the generic "regions are distinct" error reported by the Coq code.

[eponier]

Actually, I see two more solutions:

• the OCaml code prints a warning and the Coq code triggers the error, thus we have both pieces of information
• in Coq we can check whether the region of the right hand-side comes from a parameter and prints a more precise error message in this case, but that would mean pass the list of parameters as an additional argument to a lot of functions, I am not sure it is worth the trouble.

[vbgl]

I’m not convinced that the location reported by the Coq checker is “the right one”. IMHO, pointing to a particular instruction might be misleading.

[eponier]

PR https://github.com/jasmin-lang/jasmin/pull/60 adds the function name and location. I leave this PR open, because we may want an even clearer message.