delcypher / fp-benchmarks-imperial Goto Github PK

The interval_klee_bug.x86_64.bc benchmark declares several counter example locations in its spec. However when I run our tool on it some of those are not covered. Our exploration is not exhaustive unfortunately so unlike #13 I'm less certain if those asserts are reachable.

WARNING:MainThread: MATCH SPEC for task no_assert_fail but with warnings:
/home/user/build_O2/benchmarks/c/imperial/synthetic/interval_klee_bug.x86_64.bc (/home/imperial/experiments/imperial/tool_exchange/0/wd/workdir-60/klee-wd)
Observed counter examples do not cover all listed for this task in spec. The following locations were not covered:
{'interval.c': {104}}

We observe failures on line 99. @afd are you sure line 104 is reachable? Could you look into this?

WARNING:MainThread: MATCH SPEC for task no_invalid_deref but with warnings:
/home/user/build_O2/benchmarks/c/imperial/synthetic/sum_is_commutative_klee_float_bug.x86_64.bc (/home/dsl11/dev/klee-afr/experiments/first/wd/workdir-83/klee-wd)
Observed counter examples not listed in spec
  Test 000006 in /home/user/fp-bench/benchmarks/c/imperial/synthetic/sum_is_commutative/sum_is_commutative.c:40

@afd This is your benchmark. Could you added the out of bound memory access to the list of counter examples for no_invalid_deref verification task.

We should add a license

Our tool is reporting bugs in this benchmark but the

/home/user/build_O2/benchmarks/c/imperial/gsl/benchmarks/blas_klee_bug.x86_64.bc (/home/dsl11/dev/klee-afr/experiments/first/wd/workdir-43/klee-wd)
Observed counter examples not listed in spec
  Test 000001 in /home/user/fp-bench/benchmarks/c/imperial/gsl/benchmarks/blas/blas-sym.c:50
  Test 000002 in /home/user/fp-bench/benchmarks/c/imperial/gsl/benchmarks/blas/blas-sym.c:49

but the spec doesn't list them as an expected counter examples.

They should be added.

@ccadar I think you're the author of this benchmark. Could you add them?

Several benchmarks

• synthetic/fadd_to_exact_zero/fadd_to_exact_zero.c
• synthetic/fsub_to_exact_zero/fsub_to_exact_zero.c
• synthetic/interval/interval.c
• synthetic/rounding_sqrt/rounding_sqrt.c

maybe parts of gsl too (I'm not sure).

access the floating point environment without setting the pragma. This is undefined behaviour and should be fixed.

#pragma STDC FENV_ACCESS ON

Indeed Clang 3.9 at -O3 mis-compiles the interval benchmark.

See https://bugs.llvm.org//show_bug.cgi?id=8100

Note Clang doesn't support this pragma currently.

GCC also miscompiles this benchmark at -O3.

This one is a bit more interesting than the last few: With N set to 5, this variant actually runs without failure. The comment in line 55 of sum_is_not_associative.c states that failure is expected with N=400.

The vectors_klee_bug.x86_64 benchmark declares several counter example locations in its spec. However when I run our tool on it some of those are not covered and our exploration appears to be exhaustive. Later on this results in a warning when analysing our results.

WARNING:MainThread: MATCH SPEC for task no_assert_fail but with warnings:
/home/user/build_O2/benchmarks/c/imperial/gsl/benchmarks/vectors_klee_bug.x86_64.bc (/home/imperial/experiments/imperial/tool_exchange/0/wd/workdir-57/klee-wd)
Observed counter examples do not cover all listed for this task in spec. The following locations were not covered:
{'vector_example.c': {57, 58}}

I suspect those locations (i.e. lines 57 and 58 in vector_example.c) are not reachable? @ccadar could you look into this and fix if appropriate.

The statistics_klee_bug.x86_64.bcbenchmark declares several counter example locations in its spec. However when I run our tool on it some of those are not covered. Our exploration is not exhaustive unfortunately so unlike #13 I'm less certain if those asserts are reachable.

When later analysing a run of our tool I get the following warning.

WARNING:MainThread: MATCH SPEC for task no_assert_fail but with warnings:
/home/user/build_O2/benchmarks/c/imperial/gsl/benchmarks/statistics_klee_bug.x86_64.bc (/home/imperial/experiments/imperial/tool_exchange/0/wd/workdir-55/klee-wd)
Observed counter examples do not cover all listed for this task in spec. The following locations were not covered:
{'stat.c': {45, 48, 49, 50, 51, 52}}

We observe assertion failures on lines 44, 46 and 47.

I worry that some of the counter examples given are actually not reachable. @ccadar could you look into this?

This benchmark is supposed to be correct according to the spec.yml file but our tool found a bug in it (during testing we probably didn't let our tool run long enough to find the bug).

WARNING:MainThread: MISMATCH SPEC for task no_assert_fail:
/home/user/build_O2/benchmarks/c/imperial/gsl/benchmarks/blas_klee_correct.x86_64.bc (/home/dsl11/dev/klee-afr/experiments/first/wd/workdir-44/klee-wd)

WARNING:MainThread:   Test 000001 in /home/user/fp-bench/benchmarks/c/imperial/gsl/benchmarks/blas/blas-sym.c:46

The particular failure is

KLEE: ERROR: /home/user/fp-bench/benchmarks/c/imperial/gsl/benchmarks/blas/blas-sym.c:46: ASSERTION FAIL: c[0] == a[0]*b[0] + a[1]*b[2] + a[2]*b[4]

Examining the ktest file reveals that the problematic value is a nan which the test does not guard against.
We should probably add a klee_assume(!isnan(a[0])) or something?

@ccadar This is your benchmark. Any thoughts on it?

synthetic/sqrt/sqrt.c has a termination bug which has some similarities similar to the bug I tried to fix in #12

Calling naive_sqrt(float x) with x being 2.0f causes the function to enter what appears to be an infinite loop.

@afd could you take a look at this?

This (rounding_sqrt_non_klee ) benchmark is in the issta_2017 category. It shouldn't be.

This variant expects an assertion failure on line 79, but the corresponding assertion is on line 81.

We found some minor issues with non_klee variants while running on an unfiltered list. None of these are in the issta category, but they might as well be fixed.

This variant is named no_bug but its spec has no_assert_fail set to false.

Both of these variants expect assertions on line 113, but the corresponding assertion is on line 120.