Signaling and quiet NaN are not handled correctly

[greitsch]

The following example produces the wrong result:

typedef union
{
  float value;
  unsigned int word;
} float_type;

int isinf_float(float x) {
 int ix;
 do { float_type gf_u; gf_u.value = (x); (ix) = gf_u.word; } while (0);
 ix &= 0x7fffffff;
 return ((ix)==0x7f800000L);
}

int main()
{
        float x = 0.0f;

        if (isinf_float(x)) {
                __VERIFIER_error();
        }

        return 0;
}

Ultimate output: error reachable Expected output: error unreachable (verified with GCC)

[greitsch]

Here is another example:

#include <math.h>

typedef union
{
  float value;
  unsigned int word;
} float_type;

int isnann(float x)
{
    int ix;
    do { float_type gf_u; gf_u.value = (x); (ix) = gf_u.word; } while (0);
    ix &= 0x7fffffff;
    return ((ix)>0x7f800000L);
}

int main()
{
    float x = NAN;

    if (!isnann(x))
    {
        __VERIFIER_error();
    }
}

Output: error reachable Expected: error unreachable (verified with GCC and CBMC)

[Heizmann]

Which setting did you use? I think the default setting of Ultimate is not sound for these kind of programs. Can you try one of the following preference files. examples/settings/automizer/MemoryModel/svcomp-Reach-64bit-Automizer_Bitvector4Byte.epf examples/settings/automizer/MemoryModel/svcomp-Reach-64bit-Automizer_Bitvector1Byte.epf

Important is that you use the "bitvector translation" and that you use the following setting. /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Memory\ Model=HoenickeLindenmann_1ByteResolution (Maybe HoenickeLindenmann_4ByteResolution also works).

[Breee]

We are using svcomp-Reach-64bit-Automizer_Bitvector.epf and the latest release of UAutomizer.

If I use the suggested settings: examples/settings/automizer/MemoryModel/svcomp-Reach-64bit-Automizer_Bitvector4Byte.epf examples/settings/automizer/MemoryModel/svcomp-Reach-64bit-Automizer_Bitvector1Byte.epf

UAutomizer will produce an exception:

ExceptionOrErrorResult: AssertionError: de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Sort RoundingMode not declared de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder: AssertionError: de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Sort RoundingMode not declared: de.uni_freiburg.informatik.ultimate.modelcheckerutils.boogie.TypeSortTranslator.constructSort(TypeSortTranslator.java:183)

However, after adding the setting: /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Memory\ Model=HoenickeLindenmann_1ByteResolution OR /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Memory\ Model=HoenickeLindenmann_4ByteResolution

to our current settings, svcomp-Reach-64bit-Automizer_Bitvector.epf, UAutomizer now returns that the first example is SAFE, but the second example is still UNSAFE.

[danieldietsch]

You do not need to modify the .epf file, you can just add --cacsl2boogietranslator.memory.model HoenickeLindenmann_1ByteResolution to the command line (see all options with --help --experimental) .

I tried it with the latest head and can confirm that 1Byte resolution fixes the first example, but not the second. The failure path is

We found a FailurePath:
[L19]               float x = NAN;
       VAL          [x=NaN]
[L21]  CALL, EXPR   isnann(x)
       VAL          [\old(x)=NaN]
[L11]               int ix;
       VAL          [\old(x)=NaN, x=NaN]
[L12]  FCALL        float_type gf_u;
       VAL          [\old(x)=NaN, gf_u={2:0}, x=NaN]
[L12]  FCALL        gf_u.value = (x)
       VAL          [\old(x)=NaN, gf_u={2:0}, x=NaN]
[L12]  EXPR, FCALL  gf_u.word
       VAL          [\old(x)=NaN, gf_u={2:0}, gf_u.word=-8388608, x=NaN]
[L12]               (ix) = gf_u.word
[L12]  COND FALSE   !(0)
       VAL          [\old(x)=NaN, ix=4286578688, x=NaN]
[L13]               ix &= 0x7fffffff
[L14]  RET          return ((ix)>0x7f800000L);
       VAL          [\old(x)=NaN, \result=0, ix=2139095040, x=NaN]
[L21]  EXPR         isnann(x)
       VAL          [isnann(x)=0, x=NaN]
[L21]  COND TRUE    !isnann(x)
[L23]               __VERIFIER_error()
       VAL          [x=NaN]

Note that gf_u.word is an unsigned int but the value we see in the CEX is gf_u.word=-8388608.

[Heizmann]

This might be a difficult problem within Ultimate. Ultimate translates the NaN macro into the constant ( NaN eb sb) of sort ( FloatingPoint eb sb)). This SMT constant can take the value of every value that is a NaN. However, the C11 standard says (in 7.12.5) that NaN can only be a quiet NaN and not a signaling NaN. SMT-LIB has no special constants or funtions for signaling vs. quiet NaN.

Could someone check more carefully what the a NaN and a signaling NaN is?

[Heizmann]

Possible solution (seems to me best at the moment)

• find out which bits distinguish quiet NaNs and signaling NaNs
• add axiom that transforms constant(s) (_ NaN eb sb) into bitvector and extracts these bits and enforces the corresponding values

Further comments.

• I can implement that if someone finds our which bits are important.
• It will only be completely sound and effective if someone implements the support for axioms/function symbols/constants in the model checker utils.
• This solution will increase costs for SMT solver calls. (probably unavoidable)

[danieldietsch]

"The bit pattern of the mantissa for a signalling NaN has the most significant digit set to zero and at least one of the remaining digits set to one."

I am unsure how to express this as an axiom in SMT. Perhaps something like

(declare-fun silentnan () (_ FloatingPoint 11 53))

(assert (!
  (forall ((y (_ BitVec 64)))
    (=> 
      (= silentnan ((_ to_fp 11 53) y ))
        (and 
          (= (_ bv0 1) ((_ extract 10 10) y))
          (not (= (_ bv0 53) ((_ extract 63 11) y)))
))) :named nanaxiom))

[Heizmann]

Unfortunately a very tricky problem.

Your axiom expresses exactly what we want (I did not check the indices). However, I presume that this is by far too expensive for SMT solvers.

1. Simple solution: use Z3's fp.to_ieee_bv function.

(declare-fun silentnan () (_ FloatingPoint 11 53))

(assert (!
    (and 
          (= (_ bv0 1) ((_ extract 10 10) (fp.to_ieee_bv silentnan)))
          (not (= (_ bv0 53) ((_ extract 63 11) (fp.to_ieee_bv silentnan))))
    )
 :named nanaxiom))

2. SMT-LIB compliant solution

   
   (declare-fun silentnanBitvector () (_ BitVec 64 ))
   (declare-fun silentnan () (_ FloatingPoint 11 53))

(assert (! (and (= silentnan ((_ tofp 11 53) silentnanBitvector )) (= ( bv0 1) (( extract 10 10) silentnanBitvector)) (not (= ( bv0 53) ((_ extract 63 11) silentnanBitvector))) ) :named nanaxiom))

Futher comments
1. We can ask the developers of other SMT solvers for similar extensions (similar to Z3's fp.to_ieee_bv)
2. If we implement that in Ultimate we should not use a new constant silentnan instead we should put a restriction on the NaN constant (and only the restriction that is yet missing!). Reasons
A. Easier to implement for us
B. Probably slightly simpler for SMT solver
C. Will less likely trigger unsoundness caused by our missing support for axioms, non-theory constants and functions.

[danieldietsch]

If I interpret the standard correctly, we cannot put a restriction on NaN because http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml states

All fp.to_* functions are unspecified for NaN and infinity input values.

and

This means for instance that the formula

(= (fp.toreal ( NaN 8 24)) (fp.to_real (fp c1 c2 c3)))

is satisfiable in this theory for all binary constants c1, c2, and c3 (of the proper sort).

If my interpretation is correct, we have to avoid the NaN constant and encode our own via its binary representation.

I found a discussion about including fp.to_ieee_bv in the floating point theory: http://www.cs.nyu.edu/pipermail/smt-lib/2017/001180.html -- it seems dead, but it also shows that we are not the only ones that would like to use the encoding you proposed in (1).

EDIT: Perhaps our local SMTLib grandmaster @jhoenicke has an idea how we can solve this problem?

[Heizmann]

I cannot follow your argumentation. I cannot see any SMT-LIB compliant fp.to_* function in the axioms that I proposed. But you are right, we should check if fp.to_ieee_bv is defined for the NaN constant.

[danieldietsch]

You are right, I got confused with to_ieee_bv and _to_fp.

Regarding fp.to_ieee_bv: it is defined but yields always the same representation, not all the possible ones.

There is also an open issue with this function in z3, so it might not be totally stable: https://github.com/Z3Prover/z3/issues/970

[Heizmann]

I just tried the current version of Automizer on both C programs above and got SAFE as result.

This might mean that there is now an additional bug that hides the fact that we do not support signaling NaNs.

[Breee]

This C program will produce the wrong result.

/* A union which permits us to convert between a double and two 32 bit  ints. */
typedef union {
  double value;
  struct {
    unsigned int lsw;
    unsigned int msw;
  } parts;
} ieee_double_shape_type;

double fabs_double(double x) {
  unsigned int high;
  do {
    ieee_double_shape_type gh_u;
    gh_u.value = (x);
    (high) = gh_u.parts.msw;
  } while (0);
  do {
    ieee_double_shape_type sh_u;
    sh_u.value = (x);
    sh_u.parts.msw = (high & 0x7fffffff);
    (x) = sh_u.value;
  } while (0);
  return x;
}

// nan check for doubles
int isnan_double(double x) {
  int hx, lx;
  do {
    ieee_double_shape_type ew_u;
    ew_u.value = (x);
    (hx) = ew_u.parts.msw;
    (lx) = ew_u.parts.lsw;
  } while (0);
  hx &= 0x7fffffff;
  hx |= (unsigned int)(lx | (-lx)) >> 31;
  hx = 0x7ff00000 - hx;
  return (int)(((unsigned int)(hx)) >> 31);
}
int main() {

  /* 
   * REQ-BL-1010
   * The fabs and procedure shall return NaN, if the argument x is NaN.
   */

  double x = 0.0 / 0.0; // NAN
  double res = fabs_double(x);

  // x is NAN, result shall be NAN
  if (!isnan_double(res)) {
    //@ assert \false ;
  }
  return 0;
}

Output: error reachable Expected: error unreachable (verified with GCC and CBMC)

We found a FailurePath: 
[L89]               double x = 0.0 / 0.0;
       VAL          [x=NaN]
[L90]  CALL, EXPR   fabs_double(x)
       VAL          [\old(x)=NaN]
[L53]               unsigned int high;
       VAL          [\old(x)=NaN, x=NaN]
[L55]  FCALL        ieee_double_shape_type gh_u;
       VAL          [\old(x)=NaN, gh_u={2:0}, x=NaN]
[L56]  FCALL        gh_u.value = (x)
       VAL          [\old(x)=NaN, gh_u={2:0}, x=NaN]
[L57]  EXPR, FCALL  gh_u.parts.msw
       VAL          [\old(x)=NaN, gh_u={2:0}, gh_u.parts.msw=2146435072, x=NaN]
[L57]               (high) = gh_u.parts.msw
[L58]  COND FALSE   !(0)
       VAL          [\old(x)=NaN, high=2146435072, x=NaN]
[L60]  FCALL        ieee_double_shape_type sh_u;
       VAL          [\old(x)=NaN, high=2146435072, sh_u={3:0}, x=NaN]
[L61]  FCALL        sh_u.value = (x)
       VAL          [\old(x)=NaN, high=2146435072, sh_u={3:0}, x=NaN]
[L62]  FCALL        sh_u.parts.msw = (high & 0x7fffffff)
       VAL          [\old(x)=NaN, high=2146435072, sh_u={3:0}, x=NaN]
[L63]  EXPR, FCALL  sh_u.value
       VAL          [\old(x)=NaN, high=2146435072, sh_u={3:0}, x=NaN]
[L63]               (x) = sh_u.value
[L64]  COND FALSE   !(0)
       VAL          [\old(x)=NaN, high=2146435072]
[L65]  RET          return x;
       VAL          [\old(x)=NaN, high=2146435072]
[L90]  EXPR         fabs_double(x)
       VAL          [x=NaN]
[L90]               double res = fabs_double(x);
[L93]  CALL, EXPR   isnan_double(res)
[L70]               int hx, lx;
[L72]  FCALL        ieee_double_shape_type ew_u;
       VAL          [ew_u={3:0}]
[L73]  FCALL        ew_u.value = (x)
       VAL          [ew_u={3:0}]
[L74]  EXPR, FCALL  ew_u.parts.msw
       VAL          [ew_u={3:0}, ew_u.parts.msw=2146435072]
[L74]               (hx) = ew_u.parts.msw
[L75]  EXPR, FCALL  ew_u.parts.lsw
       VAL          [ew_u={3:0}, ew_u.parts.lsw=0, hx=2146435072]
[L75]               (lx) = ew_u.parts.lsw
[L76]  COND FALSE   !(0)
       VAL          [hx=2146435072, lx=0]
[L77]               hx &= 0x7fffffff
[L78]               hx |= (unsigned int)(lx | (-lx)) >> 31
[L79]               hx = 0x7ff00000 - hx
[L80]  RET          return (int)(((unsigned int)(hx)) >> 31);
       VAL          [\result=0, hx=0, lx=0]
[L93]  EXPR         isnan_double(res)
       VAL          [isnan_double(res)=0, x=NaN]
[L93]  COND TRUE    !isnan_double(res)
[L94]               CodeAnnotStmt[Assertion]
       VAL          [x=NaN]

Ultimate call:

java -Xmx8G \
-jar plugins/org.eclipse.equinox.launcher_1.3.100.v20150511-1540.jar -data data/ \
-tc config/AutomizerReach.xml \
--cacsl2boogietranslator.memory.model HoenickeLindenmann_4ByteResolution \
-s config/svcomp-Reach-64bit-Automizer_Bitvector.epf \
-i <file>

[Heizmann]

I discussed the Issue with Cesare, Florian and Martin. If I understood them correctly, the situation is the following

• the SMT-LIB FloatingPoint theory supports the IEEE 754 standard, but does not aim to support additional restrictions resp. extensions
• IEEE 754 allows different NaN representation but does not mention "quit NaNs" and "signaling NaNs".
• IEEE 754 does not define a bit representation for storing floats
• The SMT way to work with architecture specific extensions of the encoding would be to store only bitvector representations and to write the result computation as follows 'myBvToFloatEncoding(output) = someFloatOperation(myBvToFloatEncoding(input))' and wrap the float operation if the architecture specific extension has also additional requirements
  1. This requires that the output has to be existentially quantified if the output is not stored in a variable but used in an expression.
  2. We already implemented this for storing floats in our memory array.

It seems to me that the newlib is not IEEE 754 compliant and I don't know how we should approach this. Options

1. Consequently focus (in some setting) on some x86 storage model
2. Model (in some setting) consequently according to the standard by wrapping every write/read by an uninterpreted function.
3. ???