PK domain is sometimes less precise than int?

[chkl]

Hi everyone,

I found a few interesting cases in which crab using the pk domain is less precise than when using the int domain. One example:

extern void __VERIFIER_error() __attribute__((__noreturn__));
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {   
    ERROR:
        __VERIFIER_error();
    }   
}
int main() {
    int i, j, k;
    i = 0;
    j = 0;
    while (i <= 100) {
        __VERIFIER_assert(i + 1 != 0); 
        i = i + 1;
        /* this part is relevant to the reachability of the assertion */
        while (j < 20) {
            j = i + j;
        }   
    }   
    return 0;
}

I invoked crab with the following parameters:
./crabllvm.py -m 32 --crab-inter --crab-check=assert --crab-dom=int
For which the output ends in

************** ANALYSIS RESULTS ****************
1  Number of total safe checks
0  Number of total error checks
0  Number of total warning checks

Now, if switch to the pk domain (--crab-dom=pk), the output changes to

************** ANALYSIS RESULTS ****************
0  Number of total safe checks
0  Number of total error checks
1  Number of total warning checks

Is there are a particular reason for this or this is a bug?

Thank you very much,
Chris

[caballa]

AFIK, this is not a bug. In fact, this kind of loss of precision is well known for the pk domain. Although in theory pk is strictly more precise than intervals, in practice some abstract operations (mainly widening) can cause the opposite.
I recommend you to read this great paper Stratified Static Analysis Based on Variable Dependencies by David Monniaux and Le Guen. They actually have a similar program like yours: a program with a nested loop where the convergence of the innermost loop is the cause to lose the lower bound of "i" which is the counter used by the outermost loop. Very roughly, the solution they proposed, which unfortunately is not implemented in crab, is to perform several static analysis runs on multiple slices of the original program where each slice contains only a subset of the original variables. In that way, they limit the negative side-effects of performing widening on the whole program.

[caballa]

I just found a more recent paper Experimental Evaluation of Numerical Domains
for Inferring Ranges by Amato and Rubino discussing the same issue.

[chkl]

Thank you very much for the explanation and the paper recommendations.

[chkl]

I have a follow-up question on that: What about the octagon domain? The two papers you mentioned afaik don't report any imprecision with the octagon domain. I am asking because I found an example where octagon is less precise than integers (https://gist.github.com/chkl/2fc864b6f0782f49cc10c62df3fbc499, It's an ugly example using auto-generated code, I tried to slice away the irrelevant parts)

[caballa]

One common reason is disequalities (i.e., !=). The octagon domain usually ignores disequalities while intervals handle some. For instance, if you have the interval x = [0,10] and then the constraint x != 10 then intervals will be able to say that x = [0,9]. However, octagons probably will still say 0 <= x <= 10.