AnyDSL/impala

pe_assert

michael-kenzel opened this issue · 7 comments

It would be really great to have some sort of static_assert during partial evaluation, e.g.,

pe_assert ( <expression> [, <message>] )

to make compilation fail with a meaningful error message in cases where domain-specific sanity checks can tell us at compile time that the generated code will be meaningless…

Is the behaviour exactly identical to pe_info(), expect for the fact that it should make compilation fail?

Well, the intended behavior would be that pe_assert(expression, "message") would be ignored if expression evaluates to true and, if expression evaluates to false, make compilation fail, producing a diagnostic at the corresponding source location that includes the provided error message (if any). So not exactly like pe_info, but there are similarities…

What is the behaviour if the condition is not provably false nor provably true during PE?

@madmann91 Good question…I guess that should just be a hard error as asserting that a condition be true during PE would obviously require that the condition is actually one that can be checked during PE? Thinking about it, that would probably also make this a good debugging tool as it would allow one to make sure that certain things are actually getting PE'ed the way one expected them to be; and catch if they don't…

So then to rephrase:

pe_assert(expression, "message")

should be ignored if expression is provably true during PE and, otherwise, result in compilation failure, producing a diagnostic for the corresponding source location that includes the provided message.

What is the behaviour if the condition is not provably false nor provably true during PE?

We could simply emit a runtime assert() evaluating the expression instead with the same diagnostic for the corresponding source location (e.g. when compiling in debug mode).

The problem with that is that it will be very common to have the condition be neither provably true nor provably false during partial evaluation. With the current partial evaluator, it could be that the call to pe_assert ends up being dead code (never executed), but the compiler might not be able to see that before the last optimizations happen (say, after 3 rounds of inlining). It could also be that the partial evaluator is just not 'clever' enough to prove that the condition is true (or false). An example where this would happen is this:

fn do_stuff(c: bool) -> () {
  let mut x = 33;
  let mut y = 5;
  if c {
    y = 3;
  }
  // The condition cannot be evaluated at partial evaluation time
  // because the partial evaluator is not able to see the value of
  // x after the branch (that's a limitation of the current impl.)
  pe_assert(x == 33);
}

Optimizing this is btw not super trivial. You'll need to integrate

  1. SSA construction and
  2. copy propagation

with the partial evaluator to make things like this work reliably. I'm currently working on this in the t2 branch.