Skip to content

Fix unreach-call verdict in weaver buffer benchmarks

Zhihang Sun requested to merge Misasasa/sv-benchmarks:weaver-buffer into main

After discussing with weaver's developers @schuessf @klumppdo , we find the three "buffer benchmarks" in weaver have wrong verdicts, including popl20-bad-buffer-mult-alt.wvr.c, popl20-more-buffer-mult.wvr.c, and popl20-more-buffer-series.wvr.c.

For example, bad-buffer-mult-alt has

    __VERIFIER_atomic_begin();
    assume_abort_if_not(q1_back >= 0 && q1_back < n1 && q1[q1_back] == C);
    q1_back++;
    __VERIFIER_atomic_end();
    __VERIFIER_atomic_begin();
    i++;
    __VERIFIER_atomic_end();

while bad-buffer-mult-alt2 replaces it with

    __VERIFIER_atomic_begin();
    assume_abort_if_not(q1_back >= 0 && q1_back < n1 && q1[q1_back] == C);
    q1_back++;
    i++;
    __VERIFIER_atomic_end();

both of which won't cause property violations.

Additionally, we find that another order

    __VERIFIER_atomic_begin();
    assume_abort_if_not(q1_back >= 0 && q1_back < n1 && q1[q1_back] == C);
    i++;
    __VERIFIER_atomic_end();
    __VERIFIER_atomic_begin();
    q1_back++;
    __VERIFIER_atomic_end();

may cause property violations. We implement this order into a new variant, called bad-buffer-mult-alt3.

Merge request reports