SMT backend `return` bug?

[PRugg-Cap]

I've been using the SMT backend with z3 and I noticed something seems to be going wrong with return. I would expect the following functions to all give counterexamples, but fun_a generates (assert false) (after some declarations) in smt2 which of course is unsat, so would as I understand it imply the function always returns true:

$include <generic_equality.sail>

$property
function fun_a(x : range(0, 100)) -> bool = {
  if x == 0 then return true;
  if x == 100 then return true;
  false
} // unsat, but I have checked that fun_a(7) evaluates to false.

$property
function fun_b(x : range(0, 100)) -> bool = {
  if x == 0 then return true;
  false
} // sat

$property
function fun_c(x: range(0, 100)) -> bool = {
 if x == 0 | x == 100 then return true;
 false
} // sat

Using sail 0.17.1, sail -smt.

Please let me know if I'm misunderstanding something major!

[Alasdair]

I think this is a bug. We probably need to rewrite the functions internally to have a single return point.

[PRugg-Cap]

Weirdly it's happy if the false at the end is changed to return false, which suggests there might be an easier fix, e.g. just treating the fall through case more like a return?

[Alasdair]

I'm not 100% on the cause yet, but in the intermediate representation it uses there isn't really a distinction between the final expression being returned and an explicit return. I suspect the issue is to do with the shape of the SSA graph and changing the return is probably subtly changing how it's generated.

[Alasdair]

Changing the false at the end to return false changes the last bit of IR from

  return = false
end_function_1:
  end return
end_block_exception_6:
  arbitrary %bool

to

  return = false
  goto cleanup_2
  //unreachable after return
  goto end_cleanup_3
cleanup_2:
  goto end_function_1
end_cleanup_3:
end_function_1:
  end return
end_block_exception_8:
  arbitrary %bool

which is just a bunch of redundant jumps that should be simplified away, so something weird is happening...

[Alasdair]

Yes, it seems like that small change causes the shape of the control-flow graph to differ in an interesting way

[Alasdair]

The problem was the pruning I was doing to limit the size of path conditions was overly agressive and didn't work for certain graph shapes that could be produced by unstructured control flow (i.e. not if or match). I have a patch, but the problem is it massively increases the size of the generated SMT for some existing problems to the point where checking them becomes infeasible.

[PRugg-Cap]

Hmm, okay, thanks for looking into it!

[Alasdair]

I will probably end up merging it because it does fix a soundness bug, there might be some cleverer path-condition simplification I can do that would mitigate the performance issues.

[Alasdair]

Should be fixed now. I merged in my new SMT backend that fixes this and a few other issues. The behavior may have changed slightly in other places, so please report any issues you run into.