SV-COMP: unreach-call failure in float-newlib/double_req_bl_0682a.c

[RyanGlScott]

crux-llvm incorrectly reports that reach_error() is reachable when simulating SV-COMP's float-newlib/double_req_bl_0682a.c program. float-newlib/double_req_bl_0682a.c is quite a large program, so I've attempted to minimize it with C-Reduce:

#include <stdint.h>
#include <stdlib.h>

static double const pi = 3.1415926535897931160E+00;

typedef union {
  double a;
  struct {
    uint32_t b;
    uint32_t c;
  } d;
} e;

double z(double h, double i) {
  uint32_t f;
  e g;
  g.a = i;
  f = ((g.d.c >> 31) & 1) | ((g.d.c >> 30) & 2);
  switch (f) {
  case 0:
  case 1:
    return 0.0;
  case 2:
    return 1.0e300;
  case 3:
    return -pi;
  }
}

int main() {
  double x = -1.0 / 0.0; // -INF
  double y = -0x2.8p-1044;
  double res = z(y, x);

  if (res != -pi) {
    abort();
  }

  return 0;
}

If I compile this with clang test.c -O1 -o test && ./test, it will return 0. If I run it through crux-llvm, however, it fails to verify:

$ crux-llvm --solver=z3 -O1 test.c
Resolving dependencies...
Up to date
[Crux] Using pointer width: 64 for file crux-build/crux~test.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] *** debug executable: results/test/debug-36
[Crux] *** break on line: 36
[Crux] Found counterexample for verification goal
[Crux]   test.c:36:5: error: in main
[Crux]   Call to abort
[Crux] Goal status:
[Crux]   Total: 1
[Crux]   Proved: 0
[Crux]   Disproved: 1
[Crux]   Incomplete: 0
[Crux]   Unknown: 0
[Crux] Overall status: Invalid.

[RyanGlScott]

Minimizing this further is tricky, since optimizations can sometimes mask the issue. I've managed to trim it down to this file, which exhibits the same problem when run with -O0:

#include <stdlib.h>

static double const pi = 3.1415926535897931160E+00;

double const arr[4] = { 0.0, 0.0, 1.0e300, -pi};

int main() {
  if (arr[3] != -pi) {
    abort();
  }
  return 0;
}

$ crux-llvm test2.c --solver=z3 -O0
Up to date
[Crux] Using pointer width: 64 for file crux-build/crux~test2.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] *** debug executable: results/test2/debug-9
[Crux] *** break on line: 9
[Crux] Found counterexample for verification goal
[Crux]   test2.c:9:5: error: in main
[Crux]   Call to abort
[Crux] Goal status:
[Crux]   Total: 1
[Crux]   Proved: 0
[Crux]   Disproved: 1
[Crux]   Incomplete: 0
[Crux]   Unknown: 0
[Crux] Overall status: Invalid.

Or, if you prefer bitcode instead, this works with all optimization levels:

@switch.table.z = dso_local constant [4 x double] [double 0.000000e+00, double 0.000000e+00, double 1.000000e+300, double 0xC00921FB54442D18], align 16

define i32 @main() {
entry:
  %negpi = getelementptr inbounds [4 x double], [4 x double]* @switch.table.z, i64 0, i64 3
  %negpi.load = load double, double* %negpi, align 8
  %cmp = fcmp une double %negpi.load, 0xC00921FB54442D18
  br i1 %cmp, label %if.then, label %if.end

if.then:                                          ; preds = %entry
  call void @abort()
  unreachable

if.end:                                           ; preds = %entry
  ret i32 0
}

; Function Attrs: noreturn nounwind
declare dso_local void @abort() local_unnamed_addr

$ crux-llvm test4.ll --solver=z3
Up to date
[Crux] Using pointer width: 64 for file crux-build/crux~test4.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] *** debug executable: results/test4/debug-unknown
[Crux] *** break on line: unknown
[Crux] Found counterexample for verification goal
[Crux]   internal: error: in main
[Crux]   Call to abort
[Crux] Goal status:
[Crux]   Total: 1
[Crux]   Proved: 0
[Crux]   Disproved: 1
[Crux]   Incomplete: 0
[Crux]   Unknown: 0
[Crux] Overall status: Invalid.

[RyanGlScott]

What's interesting is if I change the type of the array from having double elements to int64_t elements, then it works. This leads me to suspect that the culprit is the valueLoad function:

crucible/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Common.hs

Lines 522 to 525 in 7942801

	Bitvector lw -> loadBitvector lo lw so v
	Float -> BVToFloat $ valueLoad 0 (bitvectorType 4) so v
	Double -> BVToDouble $ valueLoad 0 (bitvectorType 8) so v
	X86_FP80 -> BVToX86_FP80 $ valueLoad 0 (bitvectorType 10) so v

The three floating-point cases all hardcode the load address 0. This seems wrong, especially since the Bitvector case uses load address lo.

[robdockins]

Good catch @RyanGlScott