OCamlPro / owi

WebAssembly Swissknife & cross-language bugfinder
https://ocamlpro.github.io/owi/
GNU Affero General Public License v3.0
135 stars 17 forks source link

symbolic instruction Encoding error: trunc_f32/64 #217

Open epatrizio opened 8 months ago

epatrizio commented 8 months ago

symbolic_value: I32 and I64 modules

let trunc_f32_s x = cvtop ty TruncSF32 x
let trunc_f32_u x = cvtop ty TruncUF32 x
let trunc_f64_s x = cvtop ty TruncSF64 x
let trunc_f64_u x = cvtop ty TruncUF64 x
Encoding.Eval_numeric.IntegerOverflow
  Raised at Encoding__Eval_numeric.I64CvtOp.trunc_f32_u in file "lib/eval_numeric.ml", line 359, characters 8-29
  Called from Encoding__Eval_numeric.I64CvtOp.cvtop in file "lib/eval_numeric.ml", line 387, characters 23-57
  Called from Owi__Symbolic_value.cvtop in file "src/symbolic_value.ml", line 41, characters 28-61
zapashcanon commented 3 months ago

@filipeom, is this expected ?

zapashcanon commented 2 months ago

@filipeom (I guess you missed this one the last time as there was a bunch of different pings haha)

filipeom commented 2 months ago

Yes, this is the expected the result. The issue here is probably because Owi raises a Types.Trap "integer overflow" whereas smtml raises a IntegerOverflow exception. So they are not being handled correctly by the interpreter.

I can try to re-raise the correct Trap to fix these

zapashcanon commented 2 months ago

Oh, so it should be easy to fix then.

I can try to re-raise the correct Trap to fix these

What do you mean by this?

filipeom commented 2 months ago

I was thinking of doing something similar to this:

Because the primitives for concrete interpreter trunc_f{32|64}_{s|u} raise the trap: https://github.com/OCamlPro/owi/blob/aef0bd62b3dd028023a63547928f686c3438c3e5/src/primitives/convert.ml#L22

And, in smtml we raise:

https://github.com/formalsec/smtml/blob/a21054602aa9900a2f07d489dba9a313df833b8a/src/eval.ml#L767

I could just change the symbolic trunc_f{32|64}_{s|u} to do:

let trunc_f32_s x = 
  try cvtop ty TruncSF32 x with 
  | IntegerOverflow -> Types.Trap "integer overflow" 

To make the behaviour the same as the concrete interpreter

zapashcanon commented 2 months ago

But you don't have access to this exception, right?