search

OCamlPro / owi

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

Incomplete simplification in smtml #212

Open epatrizio opened 8 months ago

epatrizio commented 8 months ago

Context : Symbolic fuzzing #189 Similar errors occur during fuzzing : 

Failure("(i64.eq (i64.extend_i48_s (extract (i64 -5690315267789494568) 0 2)) (i64 0))")

Failure("(i32.eq (i32.extend_i16_s (extract (i32 916602011) 0 2)) (i32 0))")

Failure("(i32.to_bool (i32.extend_i16_s (extract (i32 1815251545) 0 2)))")

Failure("(bool.or ([i32.lt](http://i32.lt/) (i32 0) (i32.add (i32.extend_i16_s (extract (i32 0) 0 2)) (i32 925874591))) (bool.or ([i32.lt](http://i32.lt/) (i32.extend_i16_s (extract (i32 0) 0 2)) (i32 0)) (bool.or ([i32.lt](http://i32.lt/) (i32.add (i32.extend_i16_s (extract (i32 0) 0 2)) (i32 925874591)) (i32 0)) ([i32.lt](http://i32.lt/) (i32.add (i32.extend_i16_s (extract (i32 0) 0 2)) (i32 925874590)) (i32 0)))))")
zapashcanon commented 4 months ago

@filipeom, is this expected ?

filipeom commented 4 months ago

Yes, since we're not concretely simplifying extract. I will address this once I change the representation of bitvectors in smtml.