Cases where unwrap does not ensure the invariant of the object?

Editor
Jan 5, 2010 at 2:56 PM

Hi all,

I am running into a bit of a problem here: in some cases, unwrapping a wrapped structure does not entail that structure's invariants in the resulting state. The code I am working on involves huge numbers of invariants, and I have failed so far to reproduce the problem with a smaller version, so I am not attaching any code, but it would probably help to know if there are cases where such a situation (invariant not holding immediately after unwrap) is possible.

Cheers,
Francois

Coordinator
Jan 12, 2010 at 7:50 AM

Asserting quantified formulae may sometimes not work "out-of-box" due to trigger / Z3 behavior -- are quantifiers involved in your example?

Best, Mark

Editor
Jan 18, 2010 at 7:37 AM

I indeed have a lot of quantifiers (including a few forall/exists alternations, which is probably the worst thing I could do, from what I understand), and it looks like it is indeed a triggering issue. Thanks for pointing me there, I tend to forget that Z3 is not perfect, and to have way too much confidence in it.

Francois

Editor
Jan 25, 2010 at 11:25 AM

Hi again, list.

I finally took the time to look into this matter a bit more, and identified the faulty invariants. Since I cannot get rid of some of them, I investigated further and realised that it might not something I can fix with source-level triggers. The following code is an example of one of the invariants that goes wrong, and more specifically, when it goes wrong:

 

#include <vcc.h>
struct preds1
{
int dummy;
spec(bool P1[mathint];)
spec(bool P2[mathint][mathint];)
spec(bool P3[mathint];)
invariant(forall(mathint a; P1[a] && forall(mathint b; P2[a][b]) ==> P3[a]))
};
void testInvInv1(spec(struct preds1 ^P))
requires(inv(P))
{
assert(inv(P));
}
void testInvInd1(spec(struct preds1 ^P))
requires(inv(P))
{
assert(forall(mathint a; P->P1[a] && forall(mathint b; P->P2[a][b]) ==> P->P3[a]));
}
void testWrappedInv1(spec(struct preds1 ^P))
requires(wrapped(P))
writes(P)
{
assert(inv(P));
speconly(unwrap(P);)
assert(inv(P));
}
void testWrappedInd1(spec(struct preds1 ^P))
requires(wrapped(P))
writes(P)
{
assert(inv(P));
speconly(unwrap(P);)
assert(forall(mathint a; P->P1[a] && forall(mathint b; P->P2[a][b]) ==> P->P3[a]));
}

 

 

#include <vcc.h>

struct preds
{
	int dummy;

	spec(bool P1[mathint];)
	spec(bool P2[mathint][mathint];)
	spec(bool P3[mathint];)

	invariant(forall(mathint a; P1[a] && forall(mathint b; P2[a][b]) ==> P3[a]))
};

void testInv(spec(struct preds ^P))
requires(inv(P))
{
	assert(inv(P)); // (1) Succeeds
}

void testWrapped(spec(struct preds ^P))
requires(wrapped(P))
writes(P)
{
	assert(inv(P)); // (2) Succeeds

	speconly(unwrap(P);)
	assert(inv(P)); // (3) Fails
}

The problem seems to come from the unwrapping, that may indeed cause triggering issues in Z3, but is there anything I can do on the code above itself to make it go through? (without changing the shape of the invariant: I may not be able to do so in all instances of P1, P2 and P3.)

 

 

 

Editor
Jan 28, 2010 at 3:47 PM

Here is an extra example, with a call to wrap() failing because of the invariant "not holding" when it is asserted both using inv(P) and the actual formula. I guess my question is: what, in the encoding of wrap() and unwrap() (or static_wrap and static_unwrap, since they are the corresponding boogie calls), prevents the triggers that applied previously from being applied?

 

#include <vcc.h>

struct preds
{
	int dummy;

	spec(bool P1[mathint];)
	spec(bool P2[mathint][mathint];)
	spec(bool P3[mathint];)

	invariant(forall(mathint a; P1[a] && forall(mathint b; P2[a][b]) ==> P3[a]))
};

void test(spec(struct preds ^P))
requires(inv(P))
requires(!closed(P))
writes(P)
{
	assert(inv(P));
	assert(forall(mathint a; P->P1[a] && forall(mathint b; P->P2[a][b]) ==> P->P3[a]));
	speconly(wrap(P);)
}

 

Coordinator
Mar 24, 2011 at 7:25 AM

Hi Francois,

  this last example can be made working like this:

#include <vcc.h>

spec(ispure bool match_mathint(mathint x) returns(true);)

struct preds
{
  int dummy;

  spec(bool P1[mathint];)
  spec(bool P2[mathint][mathint];)
  spec(bool P3[mathint];)

  invariant(forall(mathint a; P1[a] && forall(mathint b; {sk_hack(match_mathint(b))} {match_mathint(b)} P2[a][b]) ==> P3[a]))
};

void test(spec(struct preds ^P))
  requires(inv(P))
  requires(!closed(P))
  writes(P)
{
  assert(inv(P));
  assert(forall(mathint a; P->P1[a] && forall(mathint b; {sk_hack(match_mathint(b))} {match_mathint(b)} P->P2[a][b]) ==> P->P3[a]));
  wrap(P);
}

  Hope that helps,

  Mark