-
Notifications
You must be signed in to change notification settings - Fork 17
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Dealing with the linear memory in external functions
- Loading branch information
1 parent
fa6d84f
commit ed313a4
Showing
4 changed files
with
200 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,51 @@ | ||
open Owi | ||
|
||
(* an extern module that will be linked with a wasm module *) | ||
let extern_module : Concrete_value.Func.extern_func Link.extern_module = | ||
(* some custom functions *) | ||
let memset m start byte length = | ||
let rec loop offset = | ||
if Int32.le offset length then begin | ||
Concrete_memory.store_8 m ~addr:(Int32.add start offset) byte; | ||
loop (Int32.add offset 1l) | ||
end | ||
in | ||
loop 0l | ||
in | ||
let print_x64 (i : int64) = Printf.printf "0x%LX\n%!" i in | ||
(* we need to describe their types *) | ||
let functions = | ||
[ ( "print_x64" | ||
, Concrete_value.Func.Extern_func (Func (Arg (I64, Res), R0), print_x64) | ||
) | ||
; ( "memset" | ||
, Concrete_value.Func.Extern_func | ||
(Func (Mem (Arg (I32, Arg (I32, Arg (I32, Res)))), R0), memset) ) | ||
] | ||
in | ||
{ functions } | ||
|
||
(* a link state that contains our custom module, available under the name `chorizo` *) | ||
let link_state = | ||
Link.extern_module Link.empty_state ~name:"chorizo" extern_module | ||
|
||
(* a pure wasm module refering to `$extern_mem` *) | ||
let pure_wasm_module = | ||
match Parse.Text.Module.from_file (Fpath.v "extern_mem.wat") with | ||
| Error e -> Result.failwith e | ||
| Ok modul -> modul | ||
|
||
(* our pure wasm module, linked with `chorizo` *) | ||
let module_to_run, link_state = | ||
match | ||
Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None | ||
pure_wasm_module | ||
with | ||
| Error e -> Result.failwith e | ||
| Ok v -> v | ||
|
||
(* let's run it ! it will print the values as defined in the print_i64 function *) | ||
let () = | ||
match Interpret.Concrete.modul link_state.envs module_to_run with | ||
| Error e -> Result.failwith e | ||
| Ok () -> () |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,19 @@ | ||
(module $extern_mem | ||
|
||
(import "chorizo" "memset" (func $memset (param i32 i32 i32))) | ||
|
||
(import "chorizo" "print_x64" (func $print_x64 (param i64))) | ||
|
||
(memory 1) | ||
|
||
(func $start | ||
|
||
;; memset 0 0xAA 8 | ||
(call $memset (i32.const 0) (i32.const 0xAA) (i32.const 8)) | ||
|
||
;; print_x64 (load 0) | ||
(call $print_x64 (i64.load (i32.const 0))) | ||
) | ||
|
||
(start $start) | ||
) |