Open tautschnig opened 4 months ago
As a further example (and in an attempt to see what answers to the above questions would actually work out), consider the following program:
__CPROVER_bool nondet_bool();
int main()
{
int *p = (int *)0;
while(nondet_bool())
{
int x;
if(p != 0)
*p = 1; // should be disallowed
p = &x;
*p = 42; // should be permitted
if(nondet_bool())
break;
}
if(p != 0)
{
int t = *p; // should be disallowed
}
}
With this example, I do believe it is necessary to create fresh objects (for symbolic execution: fresh indices alone would not suffice) for each loop iteration.
My mental model of the execution of a GOTO program is that there is an environment map of variable names -> value. DECL
adds an entry to this map, with it's initial value being non-deterministic. DEAD
removes the entry from the map entirely. Before any ASSIGN
we much check that there is an entry in the map for the value. Any evaluation including the RHS of ASSIGN
, ASSERT
, ASSUME
and FUNCTION_CALL
must check that the variable is present before getting the value. The tricky case is what happens when you dereference a pointer and one of it's possible values is no longer in the environment map, for example:
int x;
int p = &x;
while (nondet()) {
int y;
if (nondet()) {
p = &y;
}
}
*p = 0;
The most liberal interpretation is to return non-det / top on read for any missing values and ignore writes to dead things. However this might be too generous and it might be better to give an error.
To use this informal semantics to try to answer your questions...
When is a fresh instance of some named symbol created, when is that not the case?
DECL
creates new instances. The only complication is recursion. This is a bit fiddly because you sort of want the environment map to be stack allocated, but what happens if you reference something before you DECL, does that reference the caller's version? Also, what happens if you fail to DEAD a local variable.
Does a declaration merely set an instance of an object to a non-deterministic value?
No, it adds it to the environment, making it valid to reference it.
Does a (re-)declaration reset the value of __CPROVER_dead_object, or does this need to be left to an explicit GOTO program instruction?
Awkward. Ideally I would want __CPROVER_dead_object
to be modelling and thus independent of the semantics.
Does a DEAD statement equally set an instance of an object to a non-deterministic value?
No, it means that it is no longer valid to even speak its name!
Does a DEAD statement alone non-deterministically update the value stored in __CPROVER_dead_object, or should that be done via a GOTO program statement?
Again, I would want this to be independent of the semantics, if possible.
Is a repeated DEAD statement (for the same symbol) harmful?
I think it shouldn't happen. It can be safely ignored if the implementation is preferring robustness.
Maybe we really do need to do the long-proposed formalisation of the GOTO language...
Consider the GOTO program produced from the following C input (this is about GOTO program semantics, not butchering C semantics), which fails to verify for any unwinding value greater or equal to 2:
Running CBMC yields:
While this verification result is consistent for C programs, it should be possible to create a GOTO program in some different way such that
main::1::1::1::x
is not marked "DEAD" when executingbreak
: GOTO programs don't have a concept of code blocks restricting scope other than as mandated by declarations and DEAD statements. With such a change, the verification failure still persists, but is now surprising for the GOTO program (as shown below for reference, minus instruction 17) will not have killedmain::1::1::1::x
when assigning toescaped
. (The reason is that goto-symex does not make any attempt to merge L1 instances of the same symbol at phi nodes.) Before trying to hack a fix into goto-symex, I'd like to seek consensus on the following questions:__CPROVER_dead_object
, or does this need to be left to an explicit GOTO program instruction?__CPROVER_dead_object
, or should that be done via a GOTO program statement?GOTO program for reference: