[Benchmark] Local data-flow benchmark

[ThomasHaas]

I just want to share a simple benchmark that benchmarks our handling of local data flow.

#include <assert.h>
#include <dat3m.h>

#define N 100

int main()
{
    int r1 = 0;
    for (int i = 0; i < N+1; i++) {
        if (__VERIFIER_nondet_bool()) { break; }
        r1 += i;
    }

    // Intermediate variable "phi = r1" should act like a phi-node. 
    // We need to make the assignment more complex/convoluted so that Dartagnan does not propagate it away.
    // int phi = (r1 + r1) / 2;

    int r2 = 0;
    for (int i = 0; i < N; i++) {
        if (__VERIFIER_nondet_bool()) { break; }
        r2 += r1;
        // r2 += phi;
    }

    assert(r2 <= N*(N*(N+1))/2);
}

Verifying this benchmark takes 25-40 seconds on my machine. With the intermediary phi assignment, it takes < 10 seconds.
I think this benchmark (or variants thereof) can also be used to test different data-flow encodings.
Maybe someone is interested in making Dartagnan faster using this benchmark :)
For example, we could automatically insert the phi node as mentioned here #576, or somehow make the data-flow encoding smarter to better reuse values.

[ThomasHaas]

I want to add another interesting variant of the benchmark.
If we replace the local int r1 by a global volatile int r1;, we get a version with a lot of memory accesses.
This by itself already makes the solving a lot slower.
If we reduce the size to N=10, the eager encoding solves it almost instantly (< 0.5s) but the lazy solver needs around 20 seconds. The discrepancy here is huge.
It might be worth investigating what eager constraints help here so much.

[hernanponcedeleon]

If we reduce the size to N=10, the eager encoding solves it almost instantly (< 0.5s) but the lazy solver needs around 20 seconds.

I cannot reproduce this in the current development branch

> cat test.c

#include <assert.h>
#include <dat3m.h>

#define N 10
volatile int r1 = 0;

int main()
{
    
    for (int i = 0; i < N+1; i++) {
        if (__VERIFIER_nondet_bool()) { break; }
        r1 += i;
    }

    // Intermediate variable "phi = r1" should act like a phi-node. 
    // We need to make the assignment more complex/convoluted so that Dartagnan does not propagate it away.
    // int phi = (r1 + r1) / 2;

    int r2 = 0;
    for (int i = 0; i < N; i++) {
        if (__VERIFIER_nondet_bool()) { break; }
        r2 += r1;
        // r2 += phi;
    }

    assert(r2 <= N*(N*(N+1))/2);
}

> java -jar dartagnan/target/dartagnan.jar cat/vmm.cat test.c --method=eager

Test: test.c
Result: PASS
Time: 0.925 secs

> java -jar dartagnan/target/dartagnan.jar cat/vmm.cat test.c --method=lazy

Test: test.c
Result: PASS
Time: 0.990 secs