Add location to all assertion strings #1461
Conversation
|
Draft because there are a few things I wasn't sure about (marked TODO in the code):
I tested it with the C backend and it seems to work anyway. |
Test Results 15 files 34 suites 0s ⏱️ For more details on these errors, see this check. Results for commit 36185fc. ♻️ This comment has been updated with latest results. |
|
I think probably we want to do this in |
Sail currently replaces empty assertion messages with their location, so `assert(false, "")` and `assert(false)` (which is equivalent to the former) will print their location, but `assert(false, "foo")` won't. This changes the behaviour so that instead all assertions print their location. The previous substitution was applied during type checking, but now it is done in the ANF step.
Timmmm
force-pushed
the
user/timh/assert_line
branch
from
7583800 to
36185fc
Compare
|
Like this? I haven't tested this version yet, and there are soooo many place I had to change that I didn't really understand so I'm way less sure about it! |
src/lib/anf.ml
Outdated
| let loc_string = Reporting.short_loc_to_string l in | ||
| let loc_aexp = mk_aexp (ae_lit (L_aux (L_string loc_string, l)) string_typ) in | ||
| let loc_aval, loc_wrap = to_aval loc_aexp in | ||
| (* TODO: What are these wrap functions? Do I need to use loc_wrap? *) |
There was a problem hiding this comment.
It's for the ANF transform. If you want to convert f(g(x)) into let y = g(x) in f(y), what to_aval(g(x)) will do is return a tuple containing y as a value and a function fun z -> let y = g(x) in z that 'wraps' an expression in the corresponding let-binding.
Here you can just make a literal value directly rather than a literal expression and converting it to a literal value.
|
Yes, it's a much bigger change to do it that way. I suppose we could just add the extra information in the C backend (and related ones) but I think it might be better to do it more generally? |
| | E_throw of 'a exp | ||
| | E_try of 'a exp * 'a pexp list | ||
| | E_assert of 'a exp * 'a exp | ||
| | E_assert of 'a exp * 'a exp * 'a exp |
There was a problem hiding this comment.
These files are generated, so we don't want to modify them by hand. They are generated by Rocq from the files in lib/rocq/theories.
I realise this does raise the difficulty of implementing this kind of change quite significantly.
|
What we could do is add it to the C backend like in your first commit, then generalise later. |
2 participants
Sail currently replaces empty assertion messages with their location, so
assert(false, "")andassert(false)(which is equivalent to the former) will print their location, butassert(false, "foo")won't.This changes the behaviour so that instead all assertions print their location.
The previous substitution was applied during type checking, but now it is done in the ANF step.
Fixes #1453