How to handle function with floating point arguments?

[TerryGuo]

Hi there,

I am new to SAW and formal verification, but the tutorial is great, especially the part related to prove ffs_ref/ffs_imp/ffs_musl are equivalent. However for my case, the input argument is float, for example I want to prove below two C functions are equivalent:

float triple_f_a(float a) {
   return a + a + a;
}

float triple_f_b(float a) {
  return a * 3;
}

with below SAW script

triple_f_a <- llvm_extract a "triple_f_a"
triple_f_b <- llvm_extract a "triple_f_b"

When run this SAW script file, I got error:

Extracting implementation term: triple_f_a
Stack trace:
"llvm_extract"(...)
Crucible extraction currently only supports Crucible base types FloatRepr SingleFloatRepr

Sorry for my little knowldge on SAW. Any help or guide are welcomed.

[RyanGlScott]

Unfortunately, SAW is not currently capable of proving properties involving float-point types. See #1237.

[sauclovian-g]

That error message is all wet, though. We can at least improve that...

[TerryGuo]

Thanks for your helping. I will seek other tools to verify floating point type.