search

OCamlPro / owi

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

symbolic instruction error: extend_i32/64 #228

Open epatrizio opened 6 months ago

epatrizio commented 6 months ago

symbolic_value: I32 and I64 modules

  (* FIXME: This is probably wrong? *)
  let extend_s n x = cvtop ty (ExtS (32 - n)) (make (Extract (x, n / 8, 0)))
  (* --- *)
  (* FIXME: This is probably wrong? *)
  let extend_s n x = cvtop ty (ExtS (64 - n)) (make (Extract (x, n / 8, 0)))
  let extend_i32_s x = cvtop ty (ExtS 32) x
  let extend_i32_u x = cvtop ty (ExtU 32) x
Failure("(i32.to_bool (i32.extend_i24_s (extract (i32 1725277188) 0 1)))")
zapashcanon commented 2 months ago

@filipeom, is this expected ?

filipeom commented 2 months ago

Yes, see https://github.com/OCamlPro/owi/issues/212#issuecomment-2245211214