Remove dependence of C softfloat code on Sail model.
The flags and result for a softfloat operation are currently pushed to the Sail code from C like this:
// C
zfloat_result = res.v;
zfloat_fflags = (mach_bits)softfloat_exceptionFlags
// Sail
register float_result : bits(64)
register float_fflags : bits(64)
This changes it to pull the flags from the Sail side with a callback:
// C
mach_bits softfloat_float_flags(unit u)
{
return (mach_bits)softfloat_exceptionFlags;
}
// Sail
val extern_float_flags = {c: "softfloat_float_flags", ocaml: "Softfloat.float_flags", lem: "softfloat_float_flags"} : (unit) -> bits_LU
The float_result is changed to just be the return value of all of the functions.
The benefits are:
- It uses the official FFI system instead of hackily reaching into the generated C code.
- It removes the two-way dependence between the C softfloat code and the Sail model. The C softfloat code no longer has any references to the Sail model.
Tested with run_fp_tests.sh - all 82 tests pass.
Unit Test Results
712 tests ±0 396 :heavy_check_mark: - 316 0s :stopwatch: ±0s 6 suites ±0 0 :zzz: ± 0 1 files ±0 316 :x: +316
For more details on these failures, see this check.
Results for commit abf0427f. ± Comparison against base commit 69af65cf.
I'm just going to close this I think. Hopefully we can switch to pure Sail float code instead.