wrong type for `Bool.ite`

[redianthus]

Hi @filipeom,

I've had a crash in smtml with the following PC coming from owi:

(let-const symbol_0 f64)
(assert (f64.le_s (f64.abs symbol_0) (f64 0x4202a05f20000000)))
(assert (f64.lt_s
          (f64 0x4066800000000000)
          (bool.ite
            (f64.lt_s symbol_0 (f64 0x0000000000000000))
              (f64.neg symbol_0)
              symbol_0)))

The crash is the following: File "src/smtml/mappings.ml", line 419, characters 15-21: Assertion failed.

I think I found the reason why it crashes: the bool.ite has type bool because the Bool.ite is written as follow in smtml:

let ite c r1 r2 = triop Ty_bool Ite c r1 r2

Which seems to be wrong, as it should have the type of r1 (or r2 as they should be equal).

WDYT?

To reproduce, you can use:

owi c testcomp/sv-benchmarks/c/float-benchs/sin_interpolated_index-1.c -vv

[redianthus]

I have a similar one with other files that are not involving ite:

$ owi c testcomp/sv-benchmarks/c/nla-digbench-scaling/freire2_valuebound10.c -vv
...
owi: [DEBUG] path condition smt query:
              (let-const symbol_0 f64)
              (assert (f64.le_s (f64 0x0000000000000000) symbol_0))
              (assert (f64.le_s symbol_0 (f64 0x4024000000000000)))
              (check-sat)
owi: internal error, uncaught exception:
     File "src/smtml/mappings.ml", line 419, characters 15-21: Assertion failed
$ owi c testcomp/sv-benchmarks/c/nla-digbench-scaling/freire2_valuebound100.c -vv
...
owi: [DEBUG] path condition smt query:
              (let-const symbol_0 f64)
              (assert (f64.le_s (f64 0x0000000000000000) symbol_0))
              (assert (f64.le_s symbol_0 (f64 0x4059000000000000)))
              (check-sat)
owi: internal error, uncaught exception:
     File "src/smtml/mappings.ml", line 419, characters 15-21: Assertion failed
$ owi c testcomp/sv-benchmarks/c/nla-digbench-scaling/freire2_valuebound2.c -vv
...
owi: [DEBUG] path condition smt query:
              (let-const symbol_0 f64)
              (assert (f64.le_s (f64 0x0000000000000000) symbol_0))
              (assert (f64.le_s symbol_0 (f64 0x4000000000000000)))
              (check-sat)
owi: internal error, uncaught exception:
     File "src/smtml/mappings.ml", line 419, characters 15-21: Assertion failed

[redianthus]

OK, so after investigating a little bit with @hra687261 we believe there are two issues:

1. ite should indeed have the type of its branches rather than bool
2. In expr.raw something is wrong:

  let ( = ) e1 e2 = relop Ty_bool Eq e1 e2

  let ( != ) e1 e2 = relop Ty_bool Ne e1 e2

  let ( > ) e1 e2 = relop T.ty Gt e1 e2

  let ( >= ) e1 e2 = relop T.ty Ge e1 e2

  let ( < ) e1 e2 = relop T.ty Lt e1 e2

  let ( <= ) e1 e2 = relop T.ty Le e1 e2

It should be Ty_bool everywhere. Which also probably mean that this parameter is not needed.

[hra687261]

It should be Ty_bool everywhere. Which also probably mean that this parameter is not needed.

(Yes, either that or if the ty in relop ty ... is the type parameter of the relop and not the type of the returned expression, then = and != should take a type parameter which is the type of e1 and e2)

[filipeom]

Sorry, I was a bit busy preparing for my trip in the past days. Are you using Expr_raw in owi?

I ran this locally and got this:

owi: [DEBUG] path condition smt query:
              (let-const symbol_0 f64)
              (assert (f64.le_s (f64 0x0000000000000000) symbol_0))
              (assert (f64.le_s symbol_0 (f64 0x4024000000000000)))
              (check-sat)
owi: [INFO] stack         : [ (i32.of_bool
                               (bool.ne
                                (i32.add 1
                                 (i32.trunc_sat_f64_s
                                  (f64.add (f64.mul symbol_0 4.)
                                   (f64.mul symbol_0 -4.)))) 1)) ]
owi: [INFO] running instr : br_if 2
owi: [DEBUG] path condition smt query:
              (let-const symbol_0 f64)
              (assert (f64.le_s (f64 0x0000000000000000) symbol_0))
              (assert (f64.le_s symbol_0 (f64 0x4024000000000000)))
              (check-sat)
owi: internal error, uncaught exception:
     File "src/smtml/mappings.ml", line 419, characters 15-21: Assertion failed
     Raised at Stdlib__Domain.join in file "domain.ml", line 299, characters 16-24
     Called from Stdlib__Array.iter in file "array.ml", line 113, characters 31-48
     Called from Owi__Ws.read_as_seq.(fun) in file "src/exploration/ws.ml", line 19, characters 4-16
     Called from Owi__Symbolic_driver.print_and_count_failures.aux in file "src/symbolic/symbolic_driver.ml", line 17, characters 10-20
     Called from Owi__Symbolic_driver.handle_result in file "src/symbolic/symbolic_driver.ml", lines 96-98, characters 4-65
     Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
     Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44

Seems that the assertion failure is actually triggered by this line of code:

smtml/src/smtml/mappings.ml

Line 419 in 99674a6

| _ -> assert false

Which would make sense. If we look at the top of the stack before it blows up we see that the following expression:

owi: [INFO] stack         : [ (i32.of_bool
                               (bool.ne
                                (i32.add 1
                                 (i32.trunc_sat_f64_s
                                  (f64.add (f64.mul symbol_0 4.)
                                   (f64.mul symbol_0 -4.)))) 1)) ]

Is using Trunc_sat_f64_s, which is not being handled by the function linked above. Can you try #474 to see if it fixes the issue?