Fix overflow in versions of nla-digbench/geo1-u.c
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