Checksafety: soundly handle ArrayInit #343
Conversation
vbgl
force-pushed
the
checksafety-array-init
branch
from
e9826d2 to
0b76d20
Compare
|
Hmm, I guessed wrong the PR number… |
vbgl
force-pushed
the
checksafety-array-init
branch
from
0b76d20 to
aac0c93
Compare
There was a problem hiding this comment.
Hi Vincent,
I am not able to understand this path. It is not du to the patch itself, but to my general understanding of this code.
If I understand well, for array_init we should forget what we known about the array (or the cell of the array). In a sense we should recover the state that we have for local variables just after entering in a function. Are we sure that your patch ensure that ?
vbgl
force-pushed
the
checksafety-array-init
branch
from
aac0c93 to
bc2ffc3
Compare
vbgl
force-pushed
the
checksafety-array-init
branch
from
bc2ffc3 to
d2e32a2
Compare
|
Well spotted. I’ve thus added a negative test case. CI: https://gitlab.com/jasmin-lang/jasmin/-/pipelines/778487126 |
|
If you want to exercise the code a bit more, you can use |
|
Well, this exercises the second case of assign_slice, but this is not the main point of this PR. Exercising the other interesting cases seems impossible to me. |
|
Then I’d recommend to merge this as-is. |
Currently, the safety checker crashes when it encounters an explicit
ArrayInit“instruction”.Note that some of the added code is not tested as I don’t know how to exercise it…