Represent ambivalent floats as bitvectors

[enkejill]

We want to rewrite the current translation of C floating point types to Boogie to fix various issues, in particular the support of different kinds of NaNs.

Our solution is -- at a very high level -- to wrap all FP operations with our own bitvector encoding, which should be changeable (see also @Heizmann's comment on #228).

The following parts are needed.

• [x] Represent floating point types as bitvectors instead of floats (i.e., change the representation in PostProcessor)
• [x] Create wrapper function similar to:

  procedure write~intFLOATTYPE4(#value : C_FLOAT, #ptr : $Pointer$, #sizeOfWrittenType : C_INT) returns ();
  ensures (exists #valueAsBitvector : bv32 :: #memory_int == old(#memory_int)[#ptr := #valueAsBitvector] && ~fp~FLOAT(#valueAsBitvector[32:31], #valueAsBitvector[31:23], #valueAsBitvector[23:0]) == #value);
  modifies #memory_int;

• [x] Add wrapper function as procedure in PostProcessor.postProcess()
• [x] Convert float function input/output from/to bitvec
• [ ] Adjust rounding mode handling accordingly.
• [x] Custom implementation of copysign
• [ ] Research which other functions that will need a custom implementation according to standard. (functions that can return specific NaNs, i.e. sNaN, qNaN or specific +NaN / -NaN)

This feature is related to #228, #268, #381, #398, #412, and #423 .

It might also be relevant for #233 and #54

[Heizmann]

Let us assume we have a floating point operation fp.op that occurs in z := fp.op(x,y)

An obvious(?) translation would be

havoc z;
assume to_fp_unsigned(z) ==  fp.op(to_fp_unsigned(x),to_fp_unsigned((y))

Unfortunately, this will in general lead to quantified formulas but I cannot see a better solution. However, the following could be an optimization.

if (fp.isNan(fp.op(to_fp_unsigned(x),to_fp_unsigned((y))) {
    havoc z;
    assume to_fp_unsigned(z) == fp.op(to_fp_unsigned(x),to_fp_unsigned((y))
} else {
    z := fp.to_ubv(fp.op(to_fp_unsigned(x),to_fp_unsigned((y))) )
}

[danieldietsch]

We could also do it the other way around, i.e., checking if one of the Ops is NaN and thus would need non-determinism before doing the operation. We will first implement the "easiest" solution that always uses quantifiers.

[danieldietsch]

Simple wrapper function:

procedure float_to_bv32(#value : C_FLOAT) returns (bvvalue : bv32);
ensures ~fp~FLOAT(#bvvalue[32:31], #bvvalue[31:23], #bvvalue[23:0]) == #value;

[enkejill]

SMTLIBException in RCFGBuilder:

noopscript.java line 468 => checks sorts and returns null if it can't build a function

sorts are set here: statements2transformula.java line 546 getboogievar() line 555 lookup

the lookup seems to only consider the procedure itself, without the parameters specific to the call

[Heizmann]

Is this a bug report for me? I think I did not understand the problem. But I can say the following.

The return sort must be non-null if and only if we have an explicitly instantiated polymorphic FunctionSymbol, i.e., a function of the form (as ). Since these classes belong to SMTInterpol I cannot add this documentation to the code.

[danieldietsch]

No, this is not a bug report for you ;) -- we still have to investigate what the real issue is.

Perhaps @enkejill can explain what our current difficulty is: namely, that because we did never introduce a Boogie type that is equivalent to the FloatingPoint sort of SMT, we abuse the Boogie type system.