symbolic sqrt is slow

[epatrizio]

f32.sqrt and f64.sqrt instructions do not end. So, in symbolic tests, these instructions have been commented out.

https://github.com/OCamlPro/owi/blob/2ef083c191e8fa1da71ceb6b46f5d2dc19334841/test/sym/unop_f32.wat#L37

https://github.com/OCamlPro/owi/blob/2ef083c191e8fa1da71ceb6b46f5d2dc19334841/test/sym/unop_f64.wat#L37

[zapashcanon]

Small reproduction case:

(module
  (import "symbolic" "f32_symbol" (func $f32_symbol (result f32)))

  (func $start

    (f32.eq (f32.sqrt (call $f32_symbol)) (f32.const 0))
    (if (then unreachable))

  )

  (start $start)
)

Actually, this is hanging because encoding is raising Encoding.Solver.Unknown and we do not properly handle this in Symbolic_choice.

So two questions:

• @filipeom, is it expected that Z3 can not handle sqrt ? After a quick search online, I believe we would have to use the non-linear solver or something like this ?
• @chambart, @krtab, could you have a look at how we could fix this in Symbolic_choice ? This is hopefully similar to ed033dfb7d665b941b19be3345834543a8c01231.

Also, on a related note, @filipeom, do you think we should change the type of Encoding.Solver.check (to a bool option for instance) to avoid using exceptions ?

[filipeom]

* @filipeom, is it expected that Z3 can not handle `sqrt` ? After a quick search online, I believe we would have to use the non-linear solver or something like this ?

Z3 should be able to handle the sqrt (but really slooowly, see https://github.com/formalsec/encoding/commit/92ae62526cfb1fc9bb7b872622271fad61493971)

Also, on a related note, @filipeom, do you think we should change the type of Encoding.Solver.check (to a bool option for instance) to avoid using exceptions ?

Yes, I agree this should be done :smiley: Either an option or a ADT like type satisfiabilty to be more expressive

Edit: I ran the example to reproduce and it gave-me this:

$ time owi sym test.wast
Trap: unreachable
Model:
  (model
    (symbol_0 (f32 -0.)))
Reached problem!
owi sym test.wast  17.68s user 0.10s system 99% cpu 17.809 total

[filipeom]

Also, using assert:

    (call $assert
      (f32.ne
        (f32.sqrt (local.get $f))
        (f32.const 0.0)))

Instead of:

    (f32.eq (f32.sqrt (call $f32_symbol)) (f32.const 0))
    (if (then unreachable))

Dropped execution time to ~10s. While, adding an assume, made it instantaneous. But not very interesting:

(module
  (import "symbolic" "f32_symbol" (func $f32_symbol (result f32)))
  (import "symbolic" "assume" (func $assume (param i32)))
  (import "symbolic" "assert" (func $assert (param i32)))
  (func $start
    (local $f f32)
    (local.set $f (call $f32_symbol))
    (call $assume
      (f32.eq
        (local.get $f)
        (f32.const 4.0)))
    (call $assert
      (f32.ne
        (f32.sqrt (local.get $f))
        (f32.const 2.0)))
  )

  (start $start)
)

[krtab]

I cannot reproduce this either, neither on main nor on #170

[zapashcanon]

I can reproduce on main...

Not that it is looping indefinitely, but that it is very slow and we should try to fix it.

[zapashcanon]

I asked @silene (thanks again! :)) and this is because float arithmetic is implemented through bit-blasting. It is very slow because it requires generating a huge amount of variables. You can confirm this by:

• using float64 which will be even worse;
• printing the Z3 statistics (see #184) to see the number.

For some reason, it seems that using other numbers (e.g. 12 instead of 0, is a little bit faster).

If we still want to check this in our tests (and I'd like to), we should find numbers for which it is fast (and maybe combine this with the assert + f32.ne that @filipeom mentionned, if it makes things faster for some reason).

[epatrizio]

For information, in the PR #194 mentioned above, float operations div and mul have been deactivated (they are very time-consuming - ~ 25 sec !) It's the same for float copysign, but it's less important.