This project is read-only.

Arrays of mathint cause a FailureException

Oct 10, 2009 at 10:14 AM

Hi all,

When trying to verify the following code, I get a "OOPS: assertion failed" message.

#include <vcc2.h>

struct sample
{
    int dummy;
    
    spec(mathint ghost[42];)
};

VCC runs fine when the same declaration is inside a function (as in the code below).

#include <vcc2.h>

void sample()
{
    int dummy;    
    spec(mathint ghost[42];)
}

Is there any particular reason why the first declaration should fail? In any case, I am also pretty sure that the uncaught exception is a bug.

Cheers,
Francois

Oct 10, 2009 at 10:51 AM

Hi Francois,

yes, the OOPS looks like a bug. As a work-around, you can use a map instead of an array, by declaring ghost as mathint ghost[unsigned].

BTW, when the local array ghost[42] is assigned to, VCC gives a warning about not being able to determine the number of elements in the array. I'm don't know about the significance of the warning, though. Using a map in the function as well makes the warning go away. Here's a full example with the suite output in the comment at the end (VCC can check that via vcc /s):

#include <vcc2.h>

struct sample {
    int dummy;
    spec(mathint ghost[unsigned];)
};

void use_sample() {
    struct sample s;
    speconly(s.ghost[42] = 1;)
}

void sample()
{
    int dummy;    
    spec(mathint ghost[42];)
    speconly(ghost[0] = 1;)
}

void bar()
{
    int dummy;    
    spec(mathint ghost[unsigned];)
    speconly(ghost[0] = 1;)
}
/*`
testcase(17,51) : warning VC9102: don't know how to determine number of elements in array: @ptr_addition(ghost, checked*(0, 0))
testcase(17,45) : warning VC9300: [possible unsoundness]: assignment to physical location from specification code
Verification of sample succeeded.
Verification of use_sample succeeded.
Verification of bar succeeded.
`*/

Oct 10, 2009 at 12:22 PM

Thank you for your reply, Mark.

I was already using the map-based work-around. However, I ran into some Z3 timeouts that I thought were not deserved, and thought that maybe the use of maps was to blame for it. Is there any reason for maps to slow down any verification? The other, very probable, possibility, is that my code is simply bad :)

Oct 10, 2009 at 12:53 PM

Hi Francois,

  I haven't noticed particular examples, where maps are slow. In principle, the encoding for map types should be simpler than for arrays, so, I would actually expect them to be faster (I have no data to back that up, though). Sometimes, I have noticed triggering problems with maps (i.e., more explicit assertions than initially expected where required to make proofs run through); these should not however be related to the timeouts you observed. There are less of these with current VCC versions.

  If you can construct a small example that exhibits the performance problem, that would be great for the experts to look at. If you have lots of universally quantified assertions / invariants, some carefully chosen explicit triggers can make a big difference.

  Some other advice concerning time-outs is to always try a couple of random seeds (/z:/rs:0, /z:rs:0, etc.). You are probably aware of that already. Sometimes, the problems is more of an "instability" rather than Z3 being totally unable to prove something.

  Hope that helps,

  Mark

Oct 10, 2009 at 1:04 PM

As I suspected, and as you replied, it was not the maps. Thanks again for the quick answer.

Oct 10, 2009 at 1:07 PM
This discussion has been copied to a work item. Click here to go to the work item and continue the discussion.
Oct 12, 2009 at 7:09 AM

Mark has already covered most of the important things. Just to sum things up: maps are typically easier on the prover than arrays - maps are values, arrays are objects. Similarly, records are easier on the prover than structs - same reason.

As a rule of thumb: for verification purposes, you should always prefer maps over arrays and records over structs, unless you actually require them to be objects because they need to have invariants or need to be owned.

Oct 14, 2009 at 9:07 AM

A fix for this has been checked in and will be release in the next drop.