ocamlpro / owi Goto Github PK
View Code? Open in Web Editor NEWWebAssembly Swissknife & cross-language bugfinder
Home Page: https://ocamlpro.github.io/owi/
License: GNU Affero General Public License v3.0
WebAssembly Swissknife & cross-language bugfinder
Home Page: https://ocamlpro.github.io/owi/
License: GNU Affero General Public License v3.0
we should be able to parse and print the binary format
(module $m
(func $f0 (result f32)
f32.const 0
f64.const 0
i32.const 0
(if
(then
)
)
f32.demote_f64
drop
)
)
Owi launches this error : type mismatch (pop) requires [f64] but stack has [f32 f64]
while everything is ok with the official interpreter
it would make sense only when --script
is used, and would ignore all exhaustion tests from Wasm scripts, it's useful when debugging
The intrinsics library does not work on Windows. Actually, it seems that the few functions we're using could work. We could either:
to make sure we don't forget those
also add a function that do not perform the actual check and link it to a --unsafe
flag when we know the module are correct to save time
The following wasm is analyzed unsoundly by owi_sym. The assert should fail because of overflow but it does with an irrelevant model.
Model:
(model
(symbol_1 i32 (i32 1))
)
(module
(type (;0;) (func (result i32)))
(type (;1;) (func (param i32)))
(type (;2;) (func (param i32) (result i32)))
(type (;3;) (func))
(import "symbolic" "i32_symbol" (func $i32_symbol (type 0)))
(import "symbolic" "assert" (func $owi_assert (type 1)))
(func $__WASP_symb_int (type 2) (param i32) (result i32)
call $i32_symbol)
(func $__WASP_assert (type 1) (param i32)
local.get 0
call $owi_assert)
(func $_start (type 3)
call $__original_main
drop
return)
(func $__original_main (type 0) (result i32)
(local i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32 i32)
global.get $__stack_pointer
local.set 0
i32.const 16
local.set 1
local.get 0
local.get 1
i32.sub
local.set 2
local.get 2
global.set $__stack_pointer
i32.const 0
local.set 3
local.get 2
local.get 3
i32.store offset=12
i32.const 1024
local.set 4
local.get 4
call $__WASP_symb_int
local.set 5
local.get 2
local.get 5
i32.store offset=8
local.get 2
i32.load offset=8
local.set 6
i32.const 0
local.set 7
local.get 6
local.set 8
local.get 7
local.set 9
local.get 8
local.get 9
i32.gt_s
local.set 10
i32.const 1
local.set 11
local.get 10
local.get 11
i32.and
local.set 12
block ;; label = @1
local.get 12
i32.eqz
br_if 0 (;@1;)
local.get 2
i32.load offset=8
local.set 13
i32.const 1
local.set 14
local.get 13
local.get 14
i32.add
local.set 15
local.get 2
local.get 15
i32.store offset=4
local.get 2
i32.load offset=4
local.set 16
i32.const 0
local.set 17
local.get 16
local.set 18
local.get 17
local.set 19
local.get 18
local.get 19
i32.gt_s
local.set 20
i32.const 1
local.set 21
local.get 20
local.get 21
i32.and
local.set 22
local.get 22
call $__WASP_assert
end
i32.const 0
local.set 23
i32.const 16
local.set 24
local.get 2
local.get 24
i32.add
local.set 25
local.get 25
global.set $__stack_pointer
local.get 23
return)
(table (;0;) 1 1 funcref)
(memory (;0;) 129)
(global $__stack_pointer (mut i32) (i32.const 8389648))
(export "memory" (memory 0))
(export "_start" (func $_start))
(data $.rodata (i32.const 1024) "a\00"))
derived using waspc with all optimization deactivated from the following C file (example01)
#include <wasp.h>
int main() {
int a = __WASP_symb_int("a");
int b;
if (a > 0) {
b = a + 1;
__WASP_assert(b > 0);
}
return 0;
}
(module $m
(start 0)
(func $start
;; 1. OK Owi / KO! Official interpreter
i32.const 1
i64.const 2
;; 2. KO! Owi / OK Official interpreter
;; i64.const 2
;; i32.const 1
(if (param i64) (param i32)
(then
drop
drop
)
(else
drop
drop
)
)
)
)
This module seems to be correct in Owi but this error is launched with official wasm interpreter :
type mismatch: instruction requires [i64 i32 i32] but stack has [i32 i64 i32]
The behavior is reversed in case 2 (see comment 2).
(module
(func $f
(loop
br 0
br 1
br 2
(loop
br 0
br 1
br 2
br 3
br 4
)
)
))
$ owi f.wast
owi: internal error, uncaught exception:
Failure("nth")
see the exception proposal
SIMD proposal is now part of Wasm
We're using Bytes
for the memory, this works for 64 bits architectures. For 32 bits architectures, it limits the memory to 16Mo. We should write a library providing the Bytes
interface with an implementation that uses something like Bigarray
on 32 bits architecture and keeps Bytes
on 64 bits architecture.
For instance:
(module
(func (export "f")
unreachable)
)
After parsing, is desugared to:
(module
(func
unreachable)
(export "f" (func))
)
But it should be:
(module
(func
unreachable)
(export "f" (func 0))
)
Unfortunately, we add this back only after the group/rewrite/assign operation, which removes names (and we want to keep them for owi fmt
).
We should probably add a first pass that handle this.
on the line of what was tried in 8255e93
which would have the empty type in wasm side
this requires to update the GADTs definition in value.ml
memory.fill of negative values throws errors :
out of bounds memory access
(first and third i32.const ...
)
internal error, uncaught exception: Invalid_argument("Char.chr")
(second i32.const ...
)
These errors should be catch ?
(module $m
(memory $m 1)
(start 0)
(func $start
i32.const -1
i32.const -1
i32.const -1
memory.fill
)
)
and fail at runtime saying the user should reinstall with z3 available
The declaration of a non-mutable global variable should be
(module $m
[...]
(global $g i32 i32.const 0)
[...]
)
instead of
(module $m
[...]
(global $g (i32) i32.const 0)
[...]
)
we should at least split the script and module parts, see the doc in menhir https://cambium.inria.fr/~fpottier/menhir/manual.html#sec28
should keep comments at some point
(module $m
(memory $m0 6)
(func $start
(block $b0 (result i32)
i32.const 42
br $b0
i32.eqz
memory.size
(if
(then
i64.const 0
drop
)
)
memory.grow
drop
drop
i32.const 0
)
drop
)
)
That would be as owi fmt
but printing the simplified module.
MData { id = Some "id"; init = "str data init"; mode = Data_passive}
printing should be
(data $id "str data init")
instead of
(data "str data init")
(module $m
(rec
(type $t [...]))
[...]
)
Recursive types are not yet implemented in the reference interpreter : syntax error: unknown operator rec
.
But when there's only one type, rec
isn't useful in the pretty printer.
GC proposal is now stabilized
Simplification of OfBool (ToBool x)
into x
is not correct. It doesn't erase the top bits
Lines 128 to 131 in 4445d60
Format.fprintf fmt {|(data %a %a %S)|} id_opt d.id data_mode d.mode d.init
(types.ml - line 950)
Using %S
tag to display the init string of the data instruction could produce errors.
For example, %S
escapes special characters : check Issue #36
(module
(func
(block $b4 (result i32) (result f64)
i32.const 0
f64.const 0
i32.const 0
br_if $b4
br $b4
i32.const 0
f64.const 0
)
drop
drop
)
)
found by fuzzing
"There should be a model. There is not" -- Pierre C.
(module
(type (;0;) (func (result i32)))
(type (;1;) (func (param i32)))
(import "symbolic" "i32_symbol" (func $i32_symbol (type 0)))
(import "symbolic" "assert" (func $owi_assert (type 1)))
(func $_start
(local $x i32)
call $i32_symbol
local.set $x
( call $owi_assert (local.get $x) )
return)
(export "_start" (func $_start))
)
CHECK:
(bool.not (i32.to_bool symbol_1))
/CHECK KO
PATH CONDITION:
Assert failure: (i32.to_bool symbol_1)
Model:
(model
)
Reached problem!
Solver time 0.000606s
calls 1
mean time 0.606000ms
(module $m
(start 0)
(func $start
call $f
)
(func $f (local i32) (local i32) (local i32) (local i32)
i32.const 0
local.set 3
)
)
This module is correct, but its interpretation after optimization launches this error :
owi: internal error, uncaught exception: Invalid_argument("index out of bounds")
Owi stack trace (debug mode) displays : local.set 1
instead of local.set 0
Only locale id:3
is used, so it must become id:0
after optimization.
cc @chambart
Add the line number to complete "running instr:" label
(data ...)
initialization instruction (in active mode) should be
(module $m
(data $d0 (memory $m0) (offset i32.const 42) "string init")
(memory $m0 1)
[...]
)
instead of
(module $m
(data $d0 ($m0 i32.const 42) "string init")
(memory $m0 1)
[...]
)
cc @Swrup as it should be quite similar to fmt
There is a proper internship offed (in french).
A minimal version of owi opt
has been implemented in #23.
Some easy ideas to start with:
Stack-based optimisations:
Representations for optimisation:
Have a look at existing Wasm optimizers:
let memarg [...] =
[...]
Format.fprintf fmt "offset=%d align=%d" offset align
(types.ml - line 532)
align
should be interpreted as a power of 2 (2^align)
This program is not correctly typed but when it is executed with Owi, the error is detected during the interpretation.
Typechecker should intercept it before ?
(module
(start 0)
(func
i32.const -1
i64.const 0
i32.const 1
(if (param i32) (param i64)
(then
f32.reinterpret_i32
drop
drop
)
(else
drop
drop
)
)
)
)
(module $m
(data $d0 (memory $m0) (offset i32.const 0) "%]\"\148\020\182x\132\185F\235I\133o\190_Ar\150M\186\182\175>\132\1686\"\029C(\129\006\166\b<\138\160\176\0028U\218\217v+\012\159V,\127\177U\2510\192\253V\182;\148\018\191\248")
(memory $m0 1)
(start 0)
(func $start
)
)
Memory initialization string from (data ...) instruction is not correct.
The official wasm interpreter launches this error message : syntax error: illegal escape
Owi launches this error message : Lexing error int_of_string
Is it possible to improve the Owi error message?
memory.grow of a negative value throws an error :
owi: internal error, uncaught exception: Invalid_argument("Bytes.create")
This error should be catch ?
(module
(memory 0)
(func $start
i32.const -1
memory.grow
drop
)
(start $start)
)
was started in c38c8ac
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.