wat2wasm, additional tests

example/c/README.md

@@ -35,7 +35,7 @@ $ owi c ./poly.c -w1
 ...
 Model:
   (model
-    (symbol_0 (i32 2)))
+    (symbol_0 (i32 4)))
 Reached problem!
 [13]
 ```
@@ -333,9 +333,8 @@ OPTIONS
            skip typechecking pass
 
        -w VAL, --workers=VAL (absent=n)
-           number of workers for symbolic execution. Defaults to a
-           machine-specific value given by the OCaml
-           Domain.recommended_domain_count function.
+           number of workers for symbolic execution. Defaults to the number
+           of physical cores.
 
 COMMON OPTIONS
        --help[=FMT] (default=auto)

example/conc/README.md

@@ -72,9 +72,8 @@ OPTIONS
            skip typechecking pass
 
        -w VAL, --workers=VAL (absent=n)
-           number of workers for symbolic execution. Defaults to a
-           machine-specific value given by the OCaml
-           Domain.recommended_domain_count function.
+           number of workers for symbolic execution. Defaults to the number
+           of physical cores.
 
        --workspace=VAL (absent=owi-out)
            path to the workspace directory

example/sym/README.md

@@ -76,9 +76,8 @@ OPTIONS
            skip typechecking pass
 
        -w VAL, --workers=VAL (absent=n)
-           number of workers for symbolic execution. Defaults to a
-           machine-specific value given by the OCaml
-           Domain.recommended_domain_count function.
+           number of workers for symbolic execution. Defaults to the number
+           of physical cores.
 
        --workspace=VAL (absent=owi-out)
            path to the workspace directory

src/ast/binary_encoder.ml

@@ -112,8 +112,11 @@ let write_block_type buf (typ : binary block_type option) =
   | None | Some (Bt_raw (None, ([], []))) -> Buffer.add_char buf '\x40'
   | Some (Bt_raw (None, ([], [ vt ]))) -> write_valtype buf vt
   | Some (Bt_raw (None, (pt, _))) ->
-    write_paramtype buf pt (*TODO: bug? yes, modul.types *)
-  | _ -> assert false (* TODO: types link *)
+    write_paramtype buf pt
+    (* TODO: memo
+       will this pattern matching be enough with the use of the new modul.types field?
+    *)
+  | _ -> assert false (* TODO: same, new pattern matching cases ? *)
 
 let write_global_type buf ((mut, vt) : _ global_type) =
   write_valtype buf vt;
@@ -155,6 +158,13 @@ let write_table_import buf
   write_reftype buf heaptype;
   write_limits buf limits
 
+let write_func_import buf
+  ({ Imported.modul; name; desc = _; _ } : _ block_type Imported.t) =
+  write_string buf modul;
+  write_string buf name;
+  Buffer.add_char buf '\x00'
+(* TODO: How to get typeidx ? *)
+
 let write_fc buf i =
   Buffer.add_char buf '\xFC';
   write_u32_of_int buf i
@@ -194,6 +204,8 @@ let rec write_instr buf instr =
   | Call_indirect (idx, bt) ->
     add_char '\x11';
     write_block_type buf (Some bt);
+    (* TODO: get typeidx instead of block_type ?
+       (see call_indirect.wat test) *)
     write_indice buf idx
   | Drop -> add_char '\x1A'
   | Select None -> add_char '\x1B'
@@ -635,13 +647,7 @@ let encode_imports buf (funcs, tables, memories, globals) =
     List.length funcs + List.length tables + List.length memories
     + List.length globals
   in
-  List.iteri
-    (fun i { Imported.modul; name; _ } ->
-      write_string imp_buf modul;
-      write_string imp_buf name;
-      Buffer.add_char imp_buf '\x00';
-      write_u32_of_int imp_buf i (* TODO ? *) )
-    funcs;
+  List.iter (write_func_import imp_buf) funcs;
   List.iter (write_table_import imp_buf) tables;
   List.iter (write_memory_import imp_buf) memories;
   List.iter (write_global_import imp_buf) globals;

test/wat2wasm/call_indirect.t

@@ -0,0 +1,51 @@
+  $ owi wat2wasm call_indirect.wat
+  $ owi run call_indirect.wasm --debug
+  typechecking ...
+  linking      ...
+  interpreting ...
+  stack        : [  ]
+  running instr: i32.const 0
+  stack        : [ i32.const 0 ]
+  running instr: i32.const 0
+  stack        : [ i32.const 0 ; i32.const 0 ]
+  running instr: i32.const 1
+  stack        : [ i32.const 1 ; i32.const 0 ; i32.const 0 ]
+  running instr: table.init 0 0
+  stack        : [  ]
+  running instr: elem.drop 0
+  stack        : [  ]
+  stack        : [  ]
+  running instr: call 1
+  calling func : func anonymous
+  stack        : [  ]
+  running instr: i64.const 1
+  stack        : [ i64.const 1 ]
+  running instr: i32.const 0
+  stack        : [ i32.const 0 ; i64.const 1 ]
+  running instr: call_indirect 126 
+  owi: internal error, uncaught exception:
+       Not_found
+
+  [125]
+  $ owi wasm2wat call_indirect.wasm
+  (module
+
+    (type (sub final  (func (param i64) (result i64))))
+
+    (type (sub final  (func)))
+    (table 1 10 (ref null func))
+    (func (param i64) (result i64)
+      local.get 0
+      i64.const -1
+      i64.add
+    )
+    (func
+      i64.const 1
+      i32.const 0
+      call_indirect 126 
+      unreachable
+      drop
+    )
+    (elem (table 0) (offset i32.const 0) (ref null func) (item ref.func 0))
+    (start 1)
+  )

test/wat2wasm/call_indirect.wat

@@ -0,0 +1,21 @@
+(module
+  (type $sig (func (param i64) (result i64)))
+
+  (table $t0 1 10 funcref)
+  (elem (i32.const 0) $fct)
+
+  (func $fct (type $sig)
+    local.get 0
+    i64.const -1
+    i64.add
+  )
+
+  (func $start
+    i64.const 1
+    i32.const 0
+    call_indirect (type $sig)
+    drop
+  )
+
+  (start $start)
+)

test/wat2wasm/concolic.t

@@ -0,0 +1,7 @@
+  $ owi wat2wasm symbolic.wat
+  $ owi sym symbolic.wasm
+  integer representation too long
+  [26]
+  $ owi wasm2wat symbolic.wasm
+  integer representation too long
+  [26]

test/wat2wasm/concolic.wat

@@ -0,0 +1,11 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+
+  (func $start (local $x i32)
+    (local.set $x (call $i32_symbol))
+    (if (i32.lt_s (i32.const 5) (local.get $x)) (then
+      unreachable
+    )))
+
+  (start $start)
+)

test/wat2wasm/dune

@@ -1,2 +1,12 @@
 (cram
- (deps %{bin:owi} bad.ext func.wat globals.wat loop.wat mem.wat rec.wat))
+ (deps
+  %{bin:owi}
+  bad.ext
+  call_indirect.wat
+  concolic.wat
+  func.wat
+  globals.wat
+  loop.wat
+  mem.wat
+  rec.wat
+  symbolic.wat))

test/wat2wasm/loop.wat

@@ -3,17 +3,21 @@
     (local $cloop i32)
     i32.const 0
     local.set $cloop
+    ;; f32.const 42
     (loop $l (result i64) ;; TODO: add (param f32)
       local.get $cloop
       i32.const 1
       i32.add
       local.tee $cloop
       local.get $nloop
       i32.ne
-      (if
-        (then br $l)
+      (if 
+        (then
+          ;; f32.const 42
+          br $l)
         (else nop))
       ;; br_if $l
+      ;; drop
       i64.const 42
     )
   )

test/wat2wasm/symbolic.t

@@ -0,0 +1,7 @@
+  $ owi wat2wasm concolic.wat
+  $ owi conc concolic.wasm
+  integer representation too long
+  [26]
+  $ owi wasm2wat concolic.wasm
+  integer representation too long
+  [26]

test/wat2wasm/symbolic.wat

@@ -0,0 +1,11 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+
+  (func $start (local $x i32)
+    (local.set $x (call $i32_symbol))
+    (if (i32.lt_s (i32.const 5) (local.get $x)) (then
+      unreachable
+    )))
+
+  (start $start)
+)