unwinding assertion bug?
Ariel Godio
if (current != NULL){
current = current->next;
}
I tried to simplify the code, to post it here (and discard some possible sources of problems):
#include <stdlib.h>
struct node
{
int value;
struct node *next;
};
struct list
{
int size;
struct node *head;
};
void removeLast(struct list * l)
{
int index = l->size - 1;
struct node **current;
for(current = &(l->head); index && *current; index--)
current = &(*current)->next;
*current = (*current)->next;
l->size--;
}
int main () {
//build a 2-nodes list
struct node *n0 = malloc(sizeof(struct node));
struct node *n1 = malloc(sizeof(struct node));
struct list *l = malloc(sizeof(struct list));
l->size = 2;
l->head = n0;
n0->next=n1;
n1->next=NULL;
//remove last node from list
//this passes
// struct node **current = &(l->head);
// current = &(*current)->next;
// *current = (*current)->next;
// l->size--;
//this doesn't
removeLast(l);
__CPROVER_assert(n0->next == NULL , "not NULL");
}
run whit: cbmc file.c --unwind 4 --pointer-check --unwinding-assertions
(I know I don't need such an unwind, 2 should be enough)
Essentially, it creates a 2-nodes list, removes the last node and checks the size of the list. I don't care about the memory leak this remove produces because the original code uses the node.
removeLast(l), was originally designed to remove any node of the list, given an index to remove, that's why it uses ** pointers, the code would be simpler if I just wanted to remove the last node.
I provide 2 ways of removing the last node, calling removeLast(l) and calling the code that removeLast(l) will finally call. The former makes the verification fail on the last assert, but running with unwind 2 or 3 passes, and with unwind 1 fails the unwinding assertion.
The latter passes for every unwind grater than 1, just as expected. (comment removeLast and uncomment the code under //this passes to check)
many methods rely on this type of check: if(somePointer != NULL)... I thinks this is the reason why I get lots of pointer errors.
_________________________________________________________
I noticed that any of the following changes, fixes the problem (this probably helps finding an explanation):
swapping the fields of the struct node:
struct node
{
struct node *next;
int value;
};
using the constant 1 in removeLast, instead of l->size -1, which is the same for a 2-nodes list
int index = 1;
_________________________________________________________
I hope this helps, thanks in advance!
Ariel Godio
Any idea?
Thanks!
Martin Nyx Brain
> Hello!
>
> AFAIK choosing a bigger-than-you-need unwind, should not change the
> verification result, besides producing a bigger formula.
the assertions that have been checked but increasing the unwinding limit
can:
1. reach new parts of the code (and thus new assertions).
2. reach previously checked assertions but with new possibilities.
The first can cause the final yes/no result to change, the second can
cause the per-assertion results to change.
> I run CBMC 5.7 (MAC) on a program that manipulates an array of singly
> linked lists, without success.
> All the traces make no sense (for me), for example arguing a dereference
> failure in some code like this:
>
>
> current = current->next;
>
> }
There have always been issues around non-deterministic pointers. We
have tended to assume that they can be invalid or NULL. They can only
be valid if the user has explicitly constructed things that they could
point to. We are working on changing this and automatically
constructing things for them to point to but this is not in a released
version yet.
> I tried to simplify the code, to post it here (and discard some possible
> sources of problems):
>
>
> #include <stdlib.h>
>
>
> struct node
>
> {
>
> int value;
>
> struct node *next;
>
> };
>
>
> struct list
>
> {
>
> int size;
>
> struct node *head;
>
> };
>
>
> void removeLast(struct list * l)
>
> {
>
> int index = l->size - 1;
>
> struct node **current;
>
> current = &(*current)->next;
>
> *current = (*current)->next;
>
> l->size--;
>
> }
>
>
> int main () {
>
>
> struct node *n0 = malloc(*sizeof*(struct node));
>
> struct node *n1 = malloc(*sizeof*(struct node));
>
>
> struct list *l = malloc(*sizeof*(struct list));
> l->size = 2;
>
> l->head = n0;
>
>
> n0->next=n1;
>
> n1->next=NULL;
>
>
>
>
> *//this passes*
>
> *// struct node **current = &(l->head);*
>
> *// current = &(*current)->next;*
>
> *// *current = (*current)->next;*
>
> *// l->size--;*
>
>
> *//this doesn't*
> removeLast(l);
>
>
> __CPROVER_assert(n0->next == NULL , "not NULL");
>
> }
>
>
> run whit: cbmc file.c --unwind 4 --pointer-check --unwinding-assertions
>
> (I know I don't need such an unwind, 2 should be enough)
should be 2?
> Essentially, it creates a 2-nodes list, removes the last node and checks
> the size of the list. I don't care about the memory leak this remove
> produces because the original code uses the node.
>
> removeLast(l), was originally designed to remove any node of the list,
> given an index to remove, that's why it uses ** pointers, the code would be
> simpler if I just wanted to remove the last node.
>
>
> I provide 2 ways of removing the last node, calling removeLast(l) and
> calling the code that removeLast(l) will finally call. The former makes the
> verification fail on the last assert, but running with unwind 2 or 3
> passes, and with unwind 1 fails the unwinding assertion.
>
>
> The latter passes for every unwind grater than 1, just as expected.
>
>
> many methods rely on this type of check: *if*(somePointer != NULL)... I
>
> _________________________________________________________
>
>
> I noticed that any of the following changes, fixes the problem (this
> probably helps finding an explanation):
>
>
> swapping the fields of the struct node:
>
>
> struct node
>
> {
>
> struct node *next;
>
> int value;
>
> };
>
>
> using the constant 1 in removeLast, instead of l->size -1, which is the
> same for a 2-nodes list
>
>
> int index = 1;
>
>
> _________________________________________________________
>
>
> I hope this helps, thanks in advance!
then submit this an issue to our issue tracker:
http://github.com/diffblue/cbmc/
Cheers,
- Martin
Ariel Godio
El miércoles, 14 de junio de 2017, 10:26:33 (UTC-3), martin...@cs.ox.ac.uk escribió:
On Thu, 2017-06-01 at 05:52 -0700, Ariel Godio wrote:
> Hello!
>
> AFAIK choosing a bigger-than-you-need unwind, should not change the
> verification result, besides producing a bigger formula.
Ummm... sort of... It should not affect the truth of the invocations of
the assertions that have been checked but increasing the unwinding limit
can:
1. reach new parts of the code (and thus new assertions).
2. reach previously checked assertions but with new possibilities.
The first can cause the final yes/no result to change, the second can
cause the per-assertion results to change.
Thanks!
Michael Tautschnig
Resurrecting this thread as it took a while to find time to play with this.
On Wed, Jun 14, 2017 at 14:26:25 +0100, Martin Brain wrote:
> On Thu, 2017-06-01 at 05:52 -0700, Ariel Godio wrote:
> > Hello!
> >
> > AFAIK choosing a bigger-than-you-need unwind, should not change the
> > verification result, besides producing a bigger formula.
>
> Ummm... sort of... It should not affect the truth of the invocations of
> the assertions that have been checked but increasing the unwinding limit
> can:
>
> 1. reach new parts of the code (and thus new assertions).
> 2. reach previously checked assertions but with new possibilities.
>
> The first can cause the final yes/no result to change, the second can
> cause the per-assertion results to change.
>
> > I run CBMC 5.7 (MAC) on a program that manipulates an array of singly
> > linked lists, without success.
> > All the traces make no sense (for me), for example arguing a dereference
> > failure in some code like this:
> >
> > *if* (current != NULL){
> >
> > current = current->next;
> >
> > }
>
> There have always been issues around non-deterministic pointers. We
> have tended to assume that they can be invalid or NULL. They can only
> be valid if the user has explicitly constructed things that they could
> point to. We are working on changing this and automatically
> constructing things for them to point to but this is not in a released
> version yet.
>
An issue I had faced in preparation of SV-COMP'17 was non-deterministic pointers
being chosen as pointing to objects that would only become live in later
unwindings. These problems are addressed by
https://github.com/diffblue/cbmc/pull/982, and I have thus tried the example of
this thread on that branch. Indeed the problem appears to be resolved, i.e., I
no longer get spurious counterexamples with larger unwindings. Specifically, the
commit "Use a known constant offset when dereferencing" fully resolves the
problem.
I am going to add the example posted in this thread as a regression test.
Best,
Michael
Ariel Godio
Michael Tautschnig
On Mon, Feb 05, 2018 at 14:20:43 -0800, Ariel Godio wrote:
> Hello again
>
> I've been working on other projects.
>
> I found the regression test you added on cbmc/regression/cbmc/Malloc24 and
> still fails with
>
> CBMC version 5.8 64-bit x86_64 macos and
> CBMC version 5.8 64-bit x86_64 linux
>
> btw, the code you added on "Use a known constant offset when dereferencing"
> is still there.
>
> Maybe a change in the middle reinserted the bug.
>
As unfortunately CBMC still doesn't print the exact git commit as part of its
version string: are you using CBMC 5.8 as released in August 2017? If so, that
would not be expected to fix the problem as the changes have only been merged in
November 2017.
Please let us know!
Best,
Michael