impala icon indicating copy to clipboard operation
impala copied to clipboard

pe_assert

Open michael-kenzel opened this issue 6 years ago • 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…

michael-kenzel avatar Jan 28 '20 15:01 michael-kenzel

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

richardmembarth avatar Jan 29 '20 14:01 richardmembarth

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…

michael-kenzel avatar Jan 29 '20 14:01 michael-kenzel

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

madmann91 avatar Jan 29 '20 15:01 madmann91

@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.

michael-kenzel avatar Jan 29 '20 15:01 michael-kenzel

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).

stlemme avatar Jan 29 '20 22:01 stlemme

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);
}

madmann91 avatar Jan 31 '20 23:01 madmann91

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.

leissa avatar Jan 31 '20 23:01 leissa