ocamlpro / owi Goto Github PK

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:

• ask upstream to make it available on Windows and warn that some functions may fail at runtime
• vendor the few functions we need
• write a compatibility library that uses a pure OCaml implementation on Windows

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).

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.

Reported by @Swrup when working on #83.

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
  )
)

cc @chambart

I found 0fd850c and I'm wondering if it's something we want to merge or what ?

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

• Depth-First Search (DFS): Traverses states in depth-first order.
• Breadth-First Search (BFS): Traverses states in breadth-first order.
• Random State Search: Randomly selects a state to explore. See how it is implemented in KLEE.
• Random Path Selection: Described in KLEE OSDI’08 paper.
• Non Uniform Random Search (NURS): Selects a state randomly according to a given distribution. The distribution can be based on the minimum distance to an uncovered instruction (MD2U), the query cost, etc. See how it is implemented in KLEE.
• Guiding Symbolic Execution with A* (see pre-publication).
• Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding;
• FeatMaker: Automated Feature Engineering for Search Strategy of Symbolic Execution.

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

try to bring back boolify which was removed in 35c3527 cc @chambart

Simplification of OfBool (ToBool x) into x is not correct. It doesn't erase the top bits

https://github.com/WebAssembly/extended-const

cc @Swrup

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

https://github.com/WebAssembly/multi-memory

cc @Swrup

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:

• remove unused functions;
• remove unused globals;
• remove unused parameters (a little bit harder as it requires to update call sites);
• remove pure functions with empty return type.

Stack-based optimisations:

• Local optimization in a compiler for a stack-based Lisp machine;
• Optimisation Techniques for Stack Based Architectures;
• Stack-based typed assembly language.

Representations for optimisation:

• That’s a Tough Call : Studying the Challenges of
  Call Graph Construction for WebAssembly;
• Improving the Precision of Call Graph Construction for Webassembly with Symbolic Execution and Slicing;
• Global value numbers and redundant computations;
• An efficient method of computing static single assignment form;
• Combining analyses, combining optimizations;
• Compiling with Continuations, Continued.

Have a look at existing Wasm optimizers:

• binaryen;
• Low-Level Code Synthesis Using Constraint Programming;
• Ahead-of-time compilation in a language-independent environment.

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)

As expected, performances suffered a bit from #1. @chambart had some idea on how to make them great again.

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