Add float_compose to complement float_decompose

[Timmmm]

This can be useful for example to make a generic canonical_NaN() function.

[Timmmm]

See riscv/sail-riscv#594 (comment) for motivation.

[github-actions]

Test Results

   12 files  ±0     24 suites  ±0   0s ⏱️ ±0s
  740 tests ±0    740 ✅ ±0  0 💤 ±0  0 ❌ ±0 
2 468 runs  ±0  2 467 ✅ ±0  1 💤 ±0  0 ❌ ±0 

Results for commit f4e59fe. ± Comparison against base commit c2fe0d4.

♻️ This comment has been updated with latest results.

[jordancarlin]

Would probably be good to get this merged as more and more of the float library code comes together.

[Timmmm]

Rebased. I did also try adding an SMT test:

default Order dec

$include <prelude.sail>
$include <float/common.sail>

$counterexample
function float_compose_round_trip forall 'n, 'n in { 16, 32, 64, 128 }. (x : bits('n)) -> bool =
  float_compose(float_decompose(x)) == x

I don't think forall works with SMT though - it gave

-----------------
Testing SMT: cvc4
-----------------
Failed: timeout 30s cvc4 --lang=smt2.6 float_compose_prop.smt2 1> float_compose.out
stdout:

stderr:

0 passes and 1 failures
---------------
Testing SMT: z3
---------------
Failed: timeout 30s z3 float_compose_prop.smt2 1> float_compose.out
stdout:

stderr:
(error "failed to open file 'float_compose_prop.smt2'")

I also tried with just one bit size:

$counterexample
function float_compose_round_trip(x : bits(32)) -> bool =
  float_compose(float_decompose(x)) == x

But unfortunately it runs into an unimplemented case:

Todo:
append : (%bv1, %bv) -> %bv32

After implementing that (#860), it seems to still have issues.

❯ sail --smt --smt-auto --smt-auto-solver z3 float_compose.unsat.sail 
Checking counterexample: prop.smt2
Solver found counterexample: ok
  gs#2 -> 0x80000000
Failed to replay counterexample: error
  Function returned true

❯ sail --smt --smt-auto float_compose.unsat.sail
Checking counterexample: prop.smt2
prop.smt2:2.2: No set-logic command was given before this point.
prop.smt2:2.2: cvc5 will make all theories available.
prop.smt2:2.2: Consider setting a stricter logic for (likely) better performance.
prop.smt2:2.2: To suppress this warning in the future use (set-logic ALL).
Solver found counterexample: ok
  gs#2 -> 0x80000000
Failed to replay counterexample: error
  Function returned true

Maybe my implementation of append is wrong...

[Timmmm]

Oh actually the issue with the forall version is I didn't name the function prop. With that change it gives some more fun errors:

❯ sail --smt --smt-auto float_compose.unsat.sail
Checking counterexample: prop.smt2
prop.smt2:2.2: No set-logic command was given before this point.
prop.smt2:2.2: cvc5 will make all theories available.
prop.smt2:2.2: Consider setting a stricter logic for (likely) better performance.
prop.smt2:2.2: To suppress this warning in the future use (set-logic ALL).
Unexpected solver output:
(error "Parse Error: prop.smt2:17.74: high extract index is bigger than the size of the bit-vector")

❯ sail --smt --smt-auto --smt-auto-solver z3 float_compose.unsat.sail 
Checking counterexample: prop.smt2
Unexpected solver output:
(error "line 17 column 73: invalid extract application")
(error "line 18 column 274: invalid extract application")
(error "line 23 column 44: unknown constant zz44/2")
(error "line 26 column 49: unknown constant zz44/2")
(error "line 27 column 44: unknown constant zz47/2")
(error "line 28 column 49: unknown constant zz46/2")
(error "line 29 column 205: unknown constant zz43/2")
sat
(
  (define-fun zz41/2 () Bits
    zz40/1)
  (define-fun zz48/1 () Bits
    (Bits #x3f #x0000000000000000))
  (define-fun zz49/2 () (_ BitVec 64)
    (concat #x00000000000000 (len zz40/1)))
  (define-fun zz40/1 () Bits
    (Bits #x3f #x0000000000000000))
  (define-fun zz47/1 () Bits
    (Bits #x3f #x0000000000000000))
  (define-fun zz46/1 () Bits
    (Bits #x3f #x0000000000000000))
  (define-fun zz43/1 () Bits
    (Bits #x3f #x0000000000000000))
  (define-fun zz41/1 () Bits
    (Bits #x3f #x0000000000000000))
  (define-fun zz42/1 () Bits
    (Bits #x3f #x0000000000000000))
  (define-fun zz42/2 () Bits
    zz40/1)
)

Slightly worrying that z3 has what appear to be fatal errors but then it just carries on anyway!