Skip to content
Open

V2 #121

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 9 additions & 3 deletions interpreter/binary/decode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -95,7 +95,11 @@ let rec vsN n s =
else Int64.(logor x (shift_left (vsN (n - 7) s) 7))

let vu1 s = Int64.to_int (vuN 1 s)
let vu32 s = Int64.to_int32 (vuN 32 s)
let vu32 s =
let res = Int64.to_int32 (vuN 32 s) in
(* prerr_endline ("Got int " ^ Int32.to_string res); *)
res

let vs7 s = Int64.to_int (vsN 7 s)
let vs32 s = Int64.to_int32 (vsN 32 s)
let vs64 s = vsN 64 s
Expand All @@ -116,8 +120,10 @@ let vec f s = let n = len32 s in list f n s

let name s =
let pos = pos s in
try Utf8.decode (string s) with Utf8.Utf8 ->
error s pos "invalid UTF-8 encoding"
let str = string s in
(* prerr_endline ("??? " ^ str) ; *)
try Utf8.decode str with Utf8.Utf8 ->
( prerr_endline ("??? " ^ str) ; error s pos "invalid UTF-8 encoding" )

let sized f s =
let size = len32 s in
Expand Down
3 changes: 3 additions & 0 deletions interpreter/main/flags.ml
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@ let debug_error = ref false

let disable_float = ref false

let br_mode = ref false

let trace_from = ref (-1)

let insert_error = ref (-1)
Expand Down Expand Up @@ -70,6 +72,7 @@ let input_all_file_proofs = ref false
let input_proof = ref false
let input_out = ref false
let output_proof = ref false
let output_io_proof = ref false

let sbrk_offset = ref 0l

17 changes: 16 additions & 1 deletion interpreter/main/main.ml
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,8 @@ let add_arg source = args := !args @ [source]

let quote s = "\"" ^ String.escaped s ^ "\""

let inter_mode = ref false

let merge_mode = ref false
let float_mode = ref false
let float_error_mode = ref false
Expand All @@ -52,6 +54,7 @@ let underscore_mode = ref false
let counter_mode = ref false
let test_counter_mode = ref false
let handle_nan_mode = ref false
let dyncall_mode = ref false

let critical_mode = ref false
let buildstack_mode = ref false
Expand Down Expand Up @@ -81,6 +84,7 @@ let argspec = Arg.align
"-t", Arg.Set Flags.trace, " trace execution";
"-v", Arg.Unit banner, " show version";

"-inter", Arg.Set inter_mode, " start execution at an intermediate state";
"-critical", Arg.Set critical_mode, " find the critical path to step";
"-limit-stack", Arg.Set check_stack_mode, " check sizes of stack frames";
"-build-stack", Arg.Set buildstack_mode, " build the stack for critical path";
Expand All @@ -106,6 +110,7 @@ let argspec = Arg.align
"-counter", Arg.Set counter_mode, " add a counter variable to the file";
"-test-counter", Arg.Set test_counter_mode, " add a counter variable to the file (new test version)";
"-handle-nan", Arg.Set handle_nan_mode, " canonize floating point values to remove non-determinism";
"-dyncall", Arg.Set dyncall_mode, " simplify dynamic calls";
"-add-globals", Arg.String (fun s -> globals_file := Some s), " add globals to the module";
"-init-code", Arg.String (fun s -> add_arg ("(input " ^ quote s ^ ")") ; init_code := Some s), " output initial code for a wasm file";
"-imports", Arg.Set print_imports, " print imports from the wasm file";
Expand Down Expand Up @@ -152,6 +157,7 @@ let argspec = Arg.align
"-input", Arg.Set Flags.input_proof, " output information about input";
"-input2", Arg.Set Flags.input_out, " output information about input";
"-output", Arg.Set Flags.output_proof, " output information about output";
"-output-io", Arg.Set Flags.output_io_proof, " output information about output";
"-sbrk-offset", Arg.Int (fun n -> Flags.sbrk_offset := Int32.of_int n), " memory offset used by sbrk";
"-output-step", Arg.Int (fun x -> Flags.output_file_at := x), " for which step the file will be output";
"-output-file", Arg.Int (fun x -> Flags.output_file_number := x), " which file will be output at the given step";
Expand Down Expand Up @@ -200,6 +206,9 @@ let () =
Run.create_sexpr_file "critical.wast" () (fun () -> m);
Run.create_binary_file "critical.wasm" () (fun () -> m)
| _ -> () );
( match !inter_mode, !lst with
| true, m :: _ -> Loadstate.run m
| _ -> () );
( match !secret_stack_mode, !lst with
| true, m :: _ ->
let m = Secretstack.process m in
Expand All @@ -224,6 +233,12 @@ let () =
Run.create_sexpr_file "intfloat.wast" () (fun () -> m);
Run.create_binary_file "intfloat.wasm" () (fun () -> m)
| _ -> () );
( match !dyncall_mode, !lst with
| true, a :: _ ->
let m = Dyncall.process a in
Run.create_sexpr_file "dyncall.wast" () (fun () -> m);
Run.create_binary_file "dyncall.wasm" () (fun () -> m)
| _ -> () );
( match !float_error_mode, !lst with
| true, a :: _ ->
let m = Floaterror.process a in
Expand Down Expand Up @@ -294,7 +309,7 @@ let () =
| true, m :: _ ->
let open Source in
let open Ast in
let lst = Merkle.func_imports m in
let lst = Sourceutil.func_imports m in
let import_name n = "[\"" ^ Utf8.encode n.it.module_name ^ "\",\"" ^ Utf8.encode n.it.item_name ^ "\"]" in
Printf.printf "[%s]\n" (String.concat ", " (List.map import_name lst))
| _ -> () );
Expand Down
95 changes: 44 additions & 51 deletions interpreter/merkle/addglobals.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ open Merge
open Ast
open Types
open Source
open Merkle
open Sourceutil

(* remap function calls *)
let rec remap_func' map gmap gmap2 ftmap = function
Expand Down Expand Up @@ -57,11 +57,11 @@ let add_import taken special imports map map2 num imp =
let loc = Int32.of_int (List.length !imports) in
Hashtbl.add map (Int32.of_int num) loc;
imports := imp :: !imports;
Run.trace ("Got import " ^ name);
trace ("Got import " ^ name);
Hashtbl.add taken name loc
end else begin
let loc = Hashtbl.find taken name in
Run.trace ("Dropping import " ^ name);
trace ("Dropping import " ^ name);
Hashtbl.add map (Int32.of_int num) loc
end;
if Hashtbl.mem special name then begin
Expand All @@ -70,54 +70,41 @@ let add_import taken special imports map map2 num imp =

let int_global i = GetGlobal {it=Int32.of_int i; at=no_region}

let int_const y = Const (elem (Values.I32 (Int32.of_int y)))
let int64_const y = Const (elem (Values.I64 y))
let f64_const y = Const (elem (Values.F64 y))

let int_binary i =
let res = Bytes.create 4 in
Bytes.set res 0 (Char.chr (i land 0xff));
Bytes.set res 1 (Char.chr ((i lsr 8) land 0xff));
Bytes.set res 2 (Char.chr ((i lsr 16) land 0xff));
Bytes.set res 3 (Char.chr ((i lsr 24) land 0xff));
Bytes.to_string res

let generate_data (addr, i) : string segment =
elem {
offset=elem [elem (int_const (addr*4))];
index=elem 0l;
init=int_binary i;
}

(* need to add a TOTAL_MEMORY global *)

let add_i32_global m name tmem =
let open Types in
let idx = Int32.of_int (List.length (global_imports m) + List.length m.it.globals) in
do_it m (fun m -> {m with
globals=m.globals@[elem {value=elem [elem (int_const tmem)]; gtype=GlobalType (I32Type, Immutable)}];
exports=m.exports@[elem {name=Utf8.decode name; edesc=elem (GlobalExport (elem idx))}]})

let add_i64_global m name tmem =
let open Types in
let idx = Int32.of_int (List.length (global_imports m) + List.length m.it.globals) in
do_it m (fun m -> {m with
globals=m.globals@[elem {value=elem [elem (int64_const tmem)]; gtype=GlobalType (I64Type, Immutable)}];
exports=m.exports@[elem {name=Utf8.decode name; edesc=elem (GlobalExport (elem idx))}]})

let add_f64_global m name tmem =
let open Types in
let idx = Int32.of_int (List.length (global_imports m) + List.length m.it.globals) in
do_it m (fun m -> {m with
globals=m.globals@[elem {value=elem [elem (f64_const tmem)]; gtype=GlobalType (F64Type, Immutable)}];
exports=m.exports@[elem {name=Utf8.decode name; edesc=elem (GlobalExport (elem idx))}]})

let has_import m name =
List.exists (fun im -> Utf8.encode im.it.item_name = name) m.it.imports
let add_setters m =
let asmjs = find_global_index m (Utf8.decode "ASMJS") in
do_it m (fun m ->
(* add function types *)
let ftypes = m.types @ [
it (FuncType ([I32Type], []));
] in
let ftypes_len = List.length m.types in
let set_type = it (Int32.of_int (ftypes_len)) in
let make_func num =
elem {
ftype = set_type;
locals = [];
body = List.map it [GetLocal (it 0l); SetGlobal (it num)];
} in
(* add exports *)
let fnum = List.length (func_imports (it m)) + List.length m.funcs in
let added = [
it {name=Utf8.decode "setHelperStack"; edesc=it (FuncExport (it (Int32.of_int fnum)))};
it {name=Utf8.decode "setHelperStackLimit"; edesc=it (FuncExport (it (Int32.of_int (fnum+1))))};
] in
let stack_ptr = asmjs - 16 in (* this is the difficult place *)
let stack_max = stack_ptr + 1 in
let set1 = make_func (Int32.of_int stack_ptr) in
let set2 = make_func (Int32.of_int stack_max) in
{m with funcs=m.funcs @ [set1; set2];
types=ftypes;
exports=m.exports @ added; })

let add_globals m fn =
let globals, mem, tmem = load_file fn in
let m = if !Flags.asmjs then add_i32_global m "ASMJS" 0 else m in
let m =
if !Flags.asmjs then add_setters (add_i32_global m "ASMJS" 1) else m in
let m = add_i32_global m "TOTAL_MEMORY" tmem in
(* let m = add_i32_global m "GAS" 0 in *)
let m = add_i32_global m "GAS_LIMIT" (!Flags.gas_limit) in
Expand All @@ -141,7 +128,7 @@ let add_globals m fn =
let name = "_env_" ^ x in
let inst = Const (elem (Values.I32 (Int32.of_int y))) in
Hashtbl.add special_globals name inst;
Run.trace ("Blah " ^ name ^ " fddd " ^ string_of_int (555+i));
trace ("Blah " ^ name ^ " fddd " ^ string_of_int (555+i));
Hashtbl.add taken_globals name (Int32.add 555l (Int32.of_int i)) in
List.iteri reserve_export globals;
List.iteri (fun n x -> add_import taken_globals special_globals g_imports gmap1 gmap2 n x) (global_imports m);
Expand All @@ -153,28 +140,34 @@ let add_globals m fn =
let offset_ga = num_g - num_ga in

List.iteri (fun i _ ->
Run.trace ("global " ^ string_of_int (i+num_ga) ^ " -> " ^ string_of_int (i + num_ga + offset_ga));
trace ("global " ^ string_of_int (i+num_ga) ^ " -> " ^ string_of_int (i + num_ga + offset_ga));
Hashtbl.add gmap1 (Int32.of_int (i + num_ga)) (Int32.of_int (i + num_ga + offset_ga))) m.it.globals;

List.iter (fun (x,y) -> Run.trace ("Global " ^ x ^ " = " ^ string_of_int y)) globals;
List.iter (fun (x,y) -> trace ("Global " ^ x ^ " = " ^ string_of_int y)) globals;
(* initialize these globals differently *)
(* when initializing globals, cannot access previous globals *)
(* remap exports *)
let exports_a = List.map (remap_export (fun x -> x) (Hashtbl.find gmap1) ftmap1 "") m.it.exports in
(* funcs will have to be remapped *)
let funcs_a = List.map (remap (fun x -> x) (Hashtbl.find gmap1) (Hashtbl.find gmap2) ftmap1) m.it.funcs in
(* table elements have to be remapped *)
Run.trace ("Remapping globals");
trace ("Remapping globals");
let new_data = List.map generate_data mem in
let mem_size = Int32.of_int (Byteutil.pow2 (!Flags.memory_size - 13)) in
let mem = {
idesc=elem (MemoryImport (MemoryType {min=mem_size; max=Some mem_size}));
module_name=Utf8.decode "env";
item_name=Utf8.decode "memory";
} in
let table = if other_imports_nomem m = [] then [] else [
elem {idesc=elem (TableImport (TableType ({min=100000l; max=None}, AnyFuncType)));
module_name=Utf8.decode "env";
item_name=Utf8.decode "table";
}
] in
{m with it={(m.it) with funcs = funcs_a; data=m.it.data@new_data;
globals = List.map (remap_global (fun x -> x) (Hashtbl.find gmap1) (Hashtbl.find gmap2) ftmap1) m.it.globals;
imports = List.rev !g_imports @ func_imports m @ other_imports_nomem m @ [elem mem];
imports = List.rev !g_imports @ func_imports m @ table @ [elem mem];
exports = exports_a;
elems = List.map (remap_elem_segments (fun x -> x) (Hashtbl.find gmap1) (Hashtbl.find gmap2) ftmap1) m.it.elems;
}}
Expand Down
Loading