Is this a bug?

[chkl]

Hello, I stumbled upon the following phenomenon: Consider this file interesting-simplified.c:

> cat interesting-simplified.c 
extern void __VERIFIER_error() __attribute__((__noreturn__));
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
}
int main()
{
    int i = 0;
    while (i < 100000)
    {
        i = i + 1;
    }
    __VERIFIER_assert(i != 11);
    return 0;
}

Running > CORRAL="mono /tmp/corral/bin/Release/corral.exe" smack -x=svcomp --clang-options=-m32 interesting-simplified.c results in the output:

SMACK program verifier version 1.9.0
SMACK found no errors with unroll bound 1.

Now, when I just change the assertion from i != 11 to i != 10, the output changes to:

SMACK program verifier version 1.9.0
/usr/local/share/smack/lib/smack.c(47,1): This assertion can fail
Execution trace:
    /usr/local/share/smack/lib/smack.c(1782,3): Trace: Thread=1  (CALL $initialize, CALL __SMACK_static_init, RETURN from __SMACK_static_init , CALL __SMACK_init_func_memory_model)
    /usr/local/share/smack/lib/smack.c(1782,3): Trace: Thread=1  ()
    /usr/local/share/smack/lib/smack.c(1787,1): Trace: Thread=1  ()
    /database/random5_budgets/interesting-simplified-xfPVOF.c(13,5): Trace: Thread=1  (RETURN from __SMACK_init_func_memory_model , RETURN from $initialize )
    /database/random5_budgets/interesting-simplified-xfPVOF.c(13,5): Trace: Thread=1  ()
    /database/random5_budgets/interesting-simplified-xfPVOF.c(13,5): Trace: Thread=1  (smack:entry:main = -4134)
    /database/random5_budgets/interesting-simplified-xfPVOF.c(13,5): Trace: Thread=1  ()
    /database/random5_budgets/interesting-simplified-xfPVOF.c(17,5): Trace: Thread=1  ()
    /database/random5_budgets/interesting-simplified-xfPVOF.c(17,5): Trace: Thread=1  (CALL __VERIFIER_assert)
    /database/random5_budgets/interesting-simplified-xfPVOF.c(4,10): Trace: Thread=1  ()
    /database/random5_budgets/interesting-simplified-xfPVOF.c(4,9): Trace: Thread=1  ()
    /database/random5_budgets/interesting-simplified-xfPVOF.c(5,5): Trace: Thread=1  ()
    /database/random5_budgets/interesting-simplified-xfPVOF.c(7,9): Trace: Thread=1  ()
    /database/random5_budgets/interesting-simplified-xfPVOF.c(7,9): Trace: Thread=1  (CALL __VERIFIER_error)
    /usr/local/share/smack/lib/smack.c(47,3): Trace: Thread=1  ()
    /usr/local/share/smack/lib/smack.c(47,3): Trace: Thread=1  (ASSERTION FAILS assert false;
    /database/random5_budgets/interesting-simplified-xfPVOF.c(7,9): Trace: Thread=1  (RETURN from __VERIFIER_error )
    /database/random5_budgets/interesting-simplified-xfPVOF.c(17,5): Trace: Thread=1  (RETURN from __VERIFIER_assert )
    /database/random5_budgets/interesting-simplified-xfPVOF.c(17,5): Trace: Thread=1  (Done)

SMACK found an error.

To my limited understanding, smack uses bounded model checking so I would understand if in both cases it didn't reach the 100000th loop unrolling. What I don't understand is that the result depends on whether the assertion contains a 10 or an 11.

[zvonimir]

There are two related things happening here.

1. We have this hacky heuristic in SMACK that searches for large constants in SVCOMP benchmarks and replaces them with small numbers to reduce size of benchmarks. In this case, 100000 will be replaced with 10. So while (i < 100000) basically becomes while (i < 10).
2. On top of that, LLVM does constant propagation, which greatly simplifies this code and gets rid of the loop completely. LLVM knows that i is 10 after the loop terminates, and that is how the assertion is evaluated without SMACK having to unwind the loop (since the loop is not there any more). These two things taken together result in the behavior you observed. What you discovered is a drawback of our simple size-reduction heuristics. I hope this makes sense.

[chkl]

Thank you very much for clarifying this. I've found another "interesting" case since then. How does Smack handle (potentially) infinite loops? Consider this file:

extern void __VERIFIER_error() __attribute__((__noreturn__));
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
    return;
}

int main()
{
    int x = 0;
    while (1)
    {
        __VERIFIER_assert(x != 2);
        x++;
    }
    return 0;
}

Smack couldn't find an error for me in this one.

[zvonimir]

When I run SMACK with --unroll=3 it finds this bug. How did you run it?

[chkl]

I called smack using

 > CORRAL="mono /tmp/corral/bin/Release/corral.exe" smack -x=svcomp --clang-options=-m32 interesting.c

You are right, adding --unroll=3 makes smack find the error. Sorry for the confusion.

[chkl]

I am sorry to bother. Coming back to my original post: Is there a way to disable the "hacky heuristic"?

[zvonimir]

Let me implement a switch that turns it off. I'll let you know once that is done. This is also related to issue #159.

[chkl]

That'd be great. Thank you very much.