Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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: 1. It uses the official FFI system instead of hackily reaching into the generated C code. 2. 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.
- Loading branch information