__CPROVER_floatbv binary assignment

[Chester Wong]

Hi,

I am trying to test the floating point with its binary value, for example I want a floating point number that has an IEEE754 format of 0x777FFEBC, may I know is there a proper way to assign it to the __CPROVER_floatbv type?

I tried to use the union and the pointer to do the casting between uint and float, but it is not working when I try to generate the smt.

```

#define FLOAT32 __CPROVER_floatbv[32][23]

typedef union cfloat_uint32 {

    FLOAT32 f;

    uint32_t v;

} cfloat_uint32;

uint32_t totest(uint32_t a, uint32_t b) {

    cfloat_uint32 c_fa, c_fb;

    c_fa.v = a; c_fb.v = b;

    cfloat_uint32 c_result;

    c_result.f = c_fa.f + c_fb.f;

    assert(0 == c_result.v);

    return 0;

}

```

The "--function totest --no-simplify --unwind 65 --smt2 --outfile out.smt" option gives the error:

```

Invariant check failed

File: ../src/solvers/smt2/smt2_conv.cpp:939 function: type2id

Condition: false

Reason: Unreachable

Backtrace:

cbmc(print_backtrace(std::ostream&)+0x50) [0x7f581b350de0]

cbmc(get_backtrace[abi:cxx11]()+0x169) [0x7f581b351389]

cbmc(std::enable_if<std::is_base_of<invariant_failedt, invariant_failedt>::value, void>::type invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&>(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)+0x48) [0x7f581ac397d8]

cbmc(smt2_convt::type2id[abi:cxx11](typet const&) const+0x6f5) [0x7f581b1a3095]

cbmc(smt2_convt::floatbv_suffix[abi:cxx11](exprt const&) const+0x60) [0x7f581b1a3300]

cbmc(smt2_convt::find_symbols(exprt const&)+0x1f7) [0x7f581b1ba867]

cbmc(smt2_convt::find_symbols(exprt const&)+0x83) [0x7f581b1ba6f3]

cbmc(smt2_convt::find_symbols(exprt const&)+0x83) [0x7f581b1ba6f3]

cbmc(smt2_convt::find_symbols(exprt const&)+0x83) [0x7f581b1ba6f3]

cbmc(smt2_convt::find_symbols(exprt const&)+0x83) [0x7f581b1ba6f3]

cbmc(smt2_convt::prepare_for_convert_expr(exprt const&)+0x48) [0x7f581b1bc2a8]

cbmc(smt2_convt::set_to(exprt const&, bool)+0x36c) [0x7f581b1bdd2c]

cbmc(symex_target_equationt::convert_assignments(decision_proceduret&)+0xd1) [0x7f581ae5c211]

cbmc(symex_target_equationt::convert_without_assertions(decision_proceduret&)+0x7a) [0x7f581ae64a9a]

cbmc(symex_target_equationt::convert(decision_proceduret&)+0x42) [0x7f581ae655e2]

cbmc(convert_symex_target_equation(symex_target_equationt&, decision_proceduret&, message_handlert&)+0x334) [0x7f581ac55164]

cbmc(prepare_property_decider(std::unordered_map<dstringt, property_infot, std::hash<dstringt>, std::equal_to<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&, symex_target_equationt&, goto_symex_property_decidert&, ui_message_handlert&)+0x3c5) [0x7f581ac555e5]

cbmc(multi_path_symex_checkert::operator()(std::unordered_map<dstringt, property_infot, std::hash<dstringt>, std::equal_to<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&)+0x155) [0x7f581ac65555]

cbmc(stop_on_fail_verifiert<multi_path_symex_checkert>::operator()()+0x35) [0x7f581ac42625]

cbmc(cbmc_parse_optionst::doit()+0xcfb) [0x7f581ac40ecb]

cbmc(parse_options_baset::main()+0x8f) [0x7f581ac3799f]

cbmc(main+0x39) [0x7f581ac26fc9]

/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f581a4370b3]

cbmc(_start+0x2e) [0x7f581ac391ee]

```

It seems not to be a right way to assign the floating point with union casting. May I know is there any other way to do this?

Thank you very much. 

[Martin Nyx Brain]

On Mon, 2021-08-02 at 10:33 -0700, Chester Wong wrote:
> Hi,
>
> I am trying to test the floating point with its binary value, for
> example I
> want a floating point number that has an IEEE754 format of
> 0x777FFEBC, may
> I know is there a proper way to assign it to the __CPROVER_floatbv
> type?

If you want IEEE754 single precision, you don't need to use
__CPROVER_floatbv, just float will work. Then you can use the hex
format and do:

float f = 0x1.fffd78p+111f;

> I tried to use the union and the pointer to do the casting between
> uint and
> float, but it is not working when I try to generate the smt.

<snip>

> The "--function totest --no-simplify --unwind 65 --smt2 --outfile
> out.smt"
> option gives the error:
> ```
> Invariant check failed
> File: ../src/solvers/smt2/smt2_conv.cpp:939 function: type2id
> Condition: false
> Reason: Unreachable
> Backtrace:

<snip>

This is an error; invariants should not be triggered by user inputs.
Please report this on the github error tracker.

Cheers,
- Martin

[Chester Wong]

Thank you very much for your reply!

> If you want IEEE754 single precision, you don't need to use
> __CPROVER_floatbv, just float will work. Then you can use the hex
> format and do:
> 
> float f = 0x1.fffd78p+111f;

But this is the case that I know the value beforehand right? What if I want to convert the arbitrary unsigned number to the float (like what I did with the union casting)?

Thank you very much.

 

[Martin Nyx Brain]

union whatever {
int32_t binary;
float f;
}

should work, as should the more fragile:

*((int32_t *)&f)

Try them with the SAT backend first. Type unsafe access is less well
supported in SMT due to a number of technical challenges.

Cheers,
- Martin