Skip to content

Fix overflow in versions of nla-digbench/geo1-u.c

Martin Spiessl requested to merge masp/sv-benchmarks:geo1-u-fix-overflow into main

This fixes an overflow for geo1-u.c. This nla-digbench task in the meanwhile got various variants (nla-digbench-scaling and recursified) which are also addressed, namely:

./nla-digbench-scaling/geo1-u_unwindbound1.c
./nla-digbench-scaling/geo1-u_unwindbound100.c
./nla-digbench-scaling/geo1-u_unwindbound2.c
./nla-digbench-scaling/geo1-u_unwindbound20.c
./nla-digbench-scaling/geo1-u_unwindbound5.c
./nla-digbench-scaling/geo1-u_unwindbound50.c
./nla-digbench-scaling/geo1-u_unwindbound10.c
./nla-digbench/geo1-u.c
./recursified_nla-digbench/recursified_geo1-u.c

We fix the overflow in the original tasks and generate a variant that keeps the overflow, changes the overflow-verdict to false and strips all other properties (unreach-call in this case) as is standard procedure.

The overflow can be reproduced for example for nla-digbench/geo1-u.c with the following concrete values for the two nondet calls:

z = 3102212096U;
k = 4;

Then GCC's overflow sanitizer easily finds it:

$ gcc -O0 -fsanitize=signed-integer-overflow test/programs/benchmarks/nla-digbench/geo1-u.c
$ ./a.out 
test/programs/benchmarks/nla-digbench/geo1-u.c:40:11: runtime error: signed integer overflow: 3102212096 * 3102212096 cannot be represented in type 'long long int'
test/programs/benchmarks/nla-digbench/geo1-u.c:33:28: runtime error: signed integer overflow: 3102212097 * 3102212096 cannot be represented in type 'long long int'
test/programs/benchmarks/nla-digbench/geo1-u.c:39:15: runtime error: signed integer overflow: 3102212097 * 3102212096 cannot be represented in type 'long long int'
test/programs/benchmarks/nla-digbench/geo1-u.c:33:31: runtime error: signed integer overflow: 1120923795195428864 - -8823024182038626303 cannot be represented in type 'long long int'
test/programs/benchmarks/nla-digbench/geo1-u.c:44:7: runtime error: signed integer overflow: 1120

changes were done using the following bash script:

for file in $(ls nla-digbench-scaling/geo1-u_unwindbound*.c nla-digbench/geo1-u.c recursified_nla-digbench/recursified_geo1-u.c); do
        DIR=$(dirname $file)
        base=$(basename $file .c)
        for ext in yml c; do
                filename=$base.$ext
                newname="${filename/geo1-u/geo1-u2}"
                cp $DIR/$filename $DIR/$newname
                git add $DIR/$newname
        done
        ymlfile="${base}.yml"
        newyml="${ymlfile/geo1-u/geo1-u2}"
        newprogram="${base/geo1-u/geo1-u2}"
        sed -i "s|$base.c|$newprogram.c|g" $DIR/$newyml
        if [ "$newyml" = "recursified_geo1-u2.yml" ]; then
          sed -i '/- expected_verdict: false/,+1 d' $DIR/$newyml #for recursive task only
          sed -i '/- expected_verdict: true/,+1 s/true/false/' $DIR/$newyml #for recursive task only
        else
          sed -i '/property_file: \.\.\/properties\/unreach-call\.prp/,+1 d' $DIR/$newyml
          sed -i '/property_file: \.\.\/properties\/no-overflow\.prp/,+1 s/expected_verdict: true/expected_verdict: false/' $DIR/$newyml
        fi
        git add $DIR/$newyml
        sed -i "s|\(long long x, y, c;\)|unsigned \1|g" $file
        sed -i "s|\(long long \*c, \)\(long long \*y, unsigned int \*z, \)\(long long \*x\)|unsigned \1unsigned \2unsigned \3|g" $file
        sed -i "s|\(long long [xyc];\)|unsigned \1|g" $file
        git add $file
done

Merge request reports