From 9888171d3df25d3d3a9df7a28a4be1cc58fdb7d0 Mon Sep 17 00:00:00 2001 From: zapashcanon Date: Sat, 3 Aug 2024 01:58:12 +0200 Subject: [PATCH] clean code and improve code coverage --- example/define_host_function/README.md | 12 +- example/define_host_function/extern.ml | 6 +- example/define_host_function/extern_mem.ml | 6 +- .../life_game/life_console.ml | 12 +- .../life_game/life_graphics.ml | 12 +- example/lib/README.md | 4 +- src/ast/text.ml | 4 +- src/bin/owi.ml | 3 +- src/cmd/cmd_c.ml | 10 +- src/cmd/cmd_c.mli | 2 +- src/cmd/cmd_conc.ml | 28 +-- src/cmd/cmd_fmt.ml | 12 +- src/cmd/cmd_fmt.mli | 2 - src/data_structures/indexed.ml | 6 - src/data_structures/indexed.mli | 4 - src/data_structures/stack.ml | 49 ++--- src/interpret/interpret.ml | 166 +++++++-------- src/script/script.ml | 2 +- src/symbolic/symbolic_memory.ml | 7 +- src/symbolic/symbolic_memory_make.ml | 5 +- src/text_to_binary/assigned.ml | 4 +- src/text_to_binary/rewrite.ml | 201 ++++++++---------- src/utils/result.ml | 2 - src/utils/result.mli | 2 - src/utils/syntax.ml | 16 -- src/utils/syntax.mli | 8 - test/c/concolic.c | 15 ++ test/c/concolic.t | 12 ++ test/c/dune | 1 + test/fmt/print_simplified.ml | 8 +- test/opt/debug.t | 25 +++ 31 files changed, 294 insertions(+), 352 deletions(-) create mode 100644 test/c/concolic.c create mode 100644 test/c/concolic.t create mode 100644 test/opt/debug.t diff --git a/example/define_host_function/README.md b/example/define_host_function/README.md index 04d603ad0..5545e78fb 100644 --- a/example/define_host_function/README.md +++ b/example/define_host_function/README.md @@ -79,7 +79,7 @@ let link_state = (* a pure wasm module refering to `sausage` *) let pure_wasm_module = match Parse.Text.Module.from_file (Fpath.v "extern.wat") with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok modul -> modul (* our pure wasm module, linked with `sausage` *) @@ -88,13 +88,13 @@ let module_to_run, link_state = Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None pure_wasm_module with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok v -> v (* let's run it ! it will print the values as defined in the print_i32 function *) let () = match Interpret.Concrete.modul link_state.envs module_to_run with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok () -> () ``` @@ -197,7 +197,7 @@ let link_state = (* 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 + | Error _ -> assert false | Ok modul -> modul (* our pure wasm module, linked with `chorizo` *) @@ -206,13 +206,13 @@ let module_to_run, link_state = Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None pure_wasm_module with - | Error e -> Result.failwith e + | Error _ -> assert false | 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 + | Error _ -> assert false | Ok () -> () ``` diff --git a/example/define_host_function/extern.ml b/example/define_host_function/extern.ml index 9c7b8c39f..8d4caccb0 100644 --- a/example/define_host_function/extern.ml +++ b/example/define_host_function/extern.ml @@ -33,7 +33,7 @@ let link_state = (* a pure wasm module refering to `sausage` *) let pure_wasm_module = match Parse.Text.Module.from_file (Fpath.v "extern.wat") with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok modul -> modul (* our pure wasm module, linked with `sausage` *) @@ -42,11 +42,11 @@ let module_to_run, link_state = Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None pure_wasm_module with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok v -> v (* let's run it ! it will print the values as defined in the print_i32 function *) let () = match Interpret.Concrete.modul link_state.envs module_to_run with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok () -> () diff --git a/example/define_host_function/extern_mem.ml b/example/define_host_function/extern_mem.ml index 06ae83ba3..911a777f4 100644 --- a/example/define_host_function/extern_mem.ml +++ b/example/define_host_function/extern_mem.ml @@ -32,7 +32,7 @@ let link_state = (* 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 + | Error _ -> assert false | Ok modul -> modul (* our pure wasm module, linked with `chorizo` *) @@ -41,11 +41,11 @@ let module_to_run, link_state = Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None pure_wasm_module with - | Error e -> Result.failwith e + | Error _ -> assert false | 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 + | Error _ -> assert false | Ok () -> () diff --git a/example/define_host_function/life_game/life_console.ml b/example/define_host_function/life_game/life_console.ml index 01ca64b58..ef59c52a0 100644 --- a/example/define_host_function/life_game/life_console.ml +++ b/example/define_host_function/life_game/life_console.ml @@ -58,7 +58,7 @@ let link_state = (* first pure wasm module refering to `life_ext` *) let pure_wasm_module_1 = match Parse.Text.Module.from_file (Fpath.v "life.wat") with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok modul -> modul (* our first pure wasm module, linked with `life_ext` *) @@ -67,19 +67,19 @@ let module_to_run, link_state = Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:(Some "life") pure_wasm_module_1 with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok (m, state) -> (m, state) (* let's run it ! First module to be interpreted *) let () = match Interpret.Concrete.modul link_state.envs module_to_run with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok () -> () (* second pure wasm module refering to `life_ext` *) let pure_wasm_module_2 = match Parse.Text.Module.from_file (Fpath.v "life_loop.wat") with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok modul -> modul (* our second pure wasm module, linked with `life_ext` and `life` interpreted before *) @@ -88,11 +88,11 @@ let module_to_run, link_state = Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None pure_wasm_module_2 with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok (m, state) -> (m, state) (* let's run it ! it will animate the game of life in console *) let () = match Interpret.Concrete.modul link_state.envs module_to_run with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok () -> () diff --git a/example/define_host_function/life_game/life_graphics.ml b/example/define_host_function/life_game/life_graphics.ml index a9551466c..dcfd61892 100644 --- a/example/define_host_function/life_game/life_graphics.ml +++ b/example/define_host_function/life_game/life_graphics.ml @@ -70,7 +70,7 @@ let link_state = (* first pure wasm module refering to `life_ext` *) let pure_wasm_module_1 = match Parse.Text.Module.from_file (Fpath.v "life.wat") with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok modul -> modul (* our first pure wasm module, linked with `life_ext` *) @@ -79,19 +79,19 @@ let module_to_run, link_state = Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:(Some "life") pure_wasm_module_1 with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok (m, state) -> (m, state) (* let's run it ! First module to be interpreted *) let () = match Interpret.Concrete.modul link_state.envs module_to_run with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok () -> () (* second pure wasm module refering to `life_ext` *) let pure_wasm_module_2 = match Parse.Text.Module.from_file (Fpath.v "life_loop.wat") with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok modul -> modul (* our second pure wasm module, linked with `life_ext` and `life` interpreted before *) @@ -100,11 +100,11 @@ let module_to_run, link_state = Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None pure_wasm_module_2 with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok (m, state) -> (m, state) (* let's run it ! it will animate the game of life in a graphics window *) let () = match Interpret.Concrete.modul link_state.envs module_to_run with - | Error e -> Result.failwith e + | Error _ -> assert false | Ok () -> () diff --git a/example/lib/README.md b/example/lib/README.md index 3452e9f18..77b6b7d79 100644 --- a/example/lib/README.md +++ b/example/lib/README.md @@ -18,7 +18,7 @@ val m : Text.modul = # let module_to_run, link_state = match Compile.Text.until_link Link.empty_state ~unsafe:false ~optimize:false ~name:None m with | Ok v -> v - | Error e -> Result.failwith e;; + | Error _ -> assert false;; val module_to_run : '_weak1 Link.module_to_run = ... val link_state : '_weak1 Link.state = @@ -27,7 +27,7 @@ val link_state : '_weak1 Link.state = Log.debug_on := true; match Interpret.Concrete.modul link_state.envs module_to_run with | Ok () -> () - | Error e -> Result.failwith e;; + | Error _ -> assert false;; interpreting ... stack : [ ] running instr: call 0 diff --git a/src/ast/text.ml b/src/ast/text.ml index 00425caeb..847d33d75 100644 --- a/src/ast/text.ml +++ b/src/ast/text.ml @@ -128,11 +128,11 @@ type result = let pp_result fmt = function | Result_const c -> pf fmt "(%a)" pp_result_const c - | Result_func_ref | Result_extern_ref -> Log.err "not yet implemented" + | Result_func_ref | Result_extern_ref -> assert false let pp_result_bis fmt = function | Result_const c -> pf fmt "%a" pp_result_const c - | Result_extern_ref | Result_func_ref -> Log.err "not yet implemented" + | Result_extern_ref | Result_func_ref -> assert false let pp_results fmt r = list ~sep:sp pp_result_bis fmt r diff --git a/src/bin/owi.ml b/src/bin/owi.ml index a05686f3b..61f64c6e1 100644 --- a/src/bin/owi.ml +++ b/src/bin/owi.ml @@ -119,7 +119,8 @@ let c_cmd = in let property = let doc = "property file" in - Arg.(value & opt (some string) None & info [ "property" ] ~doc) + Arg.( + value & opt (some existing_non_dir_file) None & info [ "property" ] ~doc ) in let includes = let doc = "headers path" in diff --git a/src/cmd/cmd_c.ml b/src/cmd/cmd_c.ml index 1805b7f8b..d025ab8a9 100644 --- a/src/cmd/cmd_c.ml +++ b/src/cmd/cmd_c.ml @@ -7,7 +7,7 @@ open Syntax type metadata = { arch : int - ; property : string option + ; property : Fpath.t option ; files : Fpath.t list } @@ -80,15 +80,14 @@ let metadata ~workspace arch property files : unit Result.t = let tag n = (("", n), []) in let el n d = `El (tag n, [ `Data d ]) in let* spec = - match property with None -> Ok "" | Some f -> OS.File.read @@ Fpath.v f + match property with None -> Ok "" | Some f -> OS.File.read f in let file = String.concat " " (List.map Fpath.to_string files) in let* hash = list_fold_left (fun context file -> - match Bos.OS.File.read file with - | Error (`Msg msg) -> Error (`Msg msg) - | Ok str -> Ok (Digestif.SHA256.feed_string context str) ) + let+ str = Bos.OS.File.read file in + Digestif.SHA256.feed_string context str ) Digestif.SHA256.empty files in let hash = Digestif.SHA256.to_hex (Digestif.SHA256.get hash) in @@ -121,7 +120,6 @@ let metadata ~workspace arch property files : unit Result.t = let cmd debug arch property _testcomp workspace workers opt_lvl includes files profiling unsafe optimize no_stop_at_failure no_values deterministic_result_order fail_mode concolic solver : unit Result.t = - if debug then Logs.set_level (Some Debug); let workspace = Fpath.v workspace in let includes = libc_location @ includes in let* (_exists : bool) = OS.Dir.create ~path:true workspace in diff --git a/src/cmd/cmd_c.mli b/src/cmd/cmd_c.mli index d87ca1344..1cef9feef 100644 --- a/src/cmd/cmd_c.mli +++ b/src/cmd/cmd_c.mli @@ -5,7 +5,7 @@ val cmd : bool -> int - -> string option + -> Fpath.t option -> bool -> string -> int diff --git a/src/cmd/cmd_conc.ml b/src/cmd/cmd_conc.ml index 64a721c4e..18858b0f7 100644 --- a/src/cmd/cmd_conc.ml +++ b/src/cmd/cmd_conc.ml @@ -274,13 +274,13 @@ let run_once tree link_state modules_to_run forced_values = Choice.run forced_values result in let () = List.iter2 Concolic.recover backups modules_to_run in - let end_of_trace = + let+ end_of_trace = match result with - | Ok (Ok ()) -> Normal - | Ok (Error e) -> Result.failwith e - | Error (Trap t) -> Trap t - | Error Assert_fail -> Assert_fail - | Error (Assume_fail _c) -> Assume_fail + | Ok (Ok ()) -> Ok Normal + | Ok (Error _ as e) -> e + | Error (Trap t) -> Ok (Trap t) + | Error Assert_fail -> Ok Assert_fail + | Error (Assume_fail _c) -> Ok Assume_fail in let trace = { assignments = symbols_value; remaining_pc = List.rev pc; end_of_trace } @@ -368,16 +368,16 @@ let launch solver tree link_state modules_to_run = end; Some m in - let rec loop count = - if count <= 0 then None + let rec loop count : _ Result.t = + if count <= 0 then Ok None else let model = find_model 20 in run_model model count - and run_model model count = - let r, thread = run_once tree link_state modules_to_run model in + and run_model model count : _ Result.t = + let* r, thread = run_once tree link_state modules_to_run model in match r with | Ok (Ok ()) -> loop (count - 1) - | Ok (Error e) -> Result.failwith e + | Ok (Error _ as e) -> e | Error (Assume_fail c) -> begin if debug then begin Fmt.pr "Assume_fail: %a@\n" Smtml.Expr.pp c; @@ -391,8 +391,8 @@ let launch solver tree link_state modules_to_run = loop (count - 1) | Some _model as model -> run_model model (count - 1) end - | Error (Trap trap) -> Some (`Trap trap, thread) - | Error Assert_fail -> Some (`Assert_fail, thread) + | Error (Trap trap) -> Ok (Some (`Trap trap, thread)) + | Error Assert_fail -> Ok (Some (`Assert_fail, thread)) in loop 10 @@ -413,7 +413,7 @@ let cmd profiling debug unsafe optimize _workers _no_stop_at_failure no_values simplify_then_link_files ~unsafe ~optimize files in let tree = fresh_tree [] in - let result = launch solver tree link_state modules_to_run in + let* result = launch solver tree link_state modules_to_run in let print_pc pc = Fmt.pr "PC:@\n"; diff --git a/src/cmd/cmd_fmt.ml b/src/cmd/cmd_fmt.ml index b380f8b58..9a846026a 100644 --- a/src/cmd/cmd_fmt.ml +++ b/src/cmd/cmd_fmt.ml @@ -16,14 +16,8 @@ let get_printer filename = | ext -> Error (`Unsupported_file_extension ext) let cmd_one inplace file = - match get_printer file with - | Error _e as e -> e - | Ok pp -> - if inplace then Bos.OS.File.writef file "%a@\n" pp () - else Ok (Fmt.pr "%a@\n" pp ()) + let* pp = get_printer file in + if inplace then Bos.OS.File.writef file "%a@\n" pp () + else Ok (Fmt.pr "%a@\n" pp ()) let cmd inplace files = list_iter (cmd_one inplace) files - -let format_file_to_string file = - let+ pp = get_printer file in - Fmt.str "%a@\n" pp () diff --git a/src/cmd/cmd_fmt.mli b/src/cmd/cmd_fmt.mli index 795b0b402..433a95470 100644 --- a/src/cmd/cmd_fmt.mli +++ b/src/cmd/cmd_fmt.mli @@ -3,5 +3,3 @@ (* Written by the Owi programmers *) val cmd : bool -> Fpath.t list -> unit Result.t - -val format_file_to_string : Fpath.t -> string Result.t diff --git a/src/data_structures/indexed.ml b/src/data_structures/indexed.ml index e894d2fa7..02b89f1b2 100644 --- a/src/data_structures/indexed.ml +++ b/src/data_structures/indexed.ml @@ -17,13 +17,7 @@ let return index value = { index; value } let has_index idx { index; _ } = idx = index -let get_at_exn i values = - let { value; _ } = List.find (has_index i) values in - value - let get_at i values = match List.find_opt (has_index i) values with | None -> None | Some { value; _ } -> Some value - -let pp f fmt v = f fmt v.value diff --git a/src/data_structures/indexed.mli b/src/data_structures/indexed.mli index 08d335838..14602cf80 100644 --- a/src/data_structures/indexed.mli +++ b/src/data_structures/indexed.mli @@ -14,8 +14,4 @@ val return : int -> 'a -> 'a t val get_at : int -> 'a t list -> 'a option -val get_at_exn : int -> 'a t list -> 'a - val has_index : int -> 'a t -> bool - -val pp : (Fmt.formatter -> 'a -> unit) -> Fmt.formatter -> 'a t -> unit diff --git a/src/data_structures/stack.ml b/src/data_structures/stack.ml index 02e56236d..33d835594 100644 --- a/src/data_structures/stack.ml +++ b/src/data_structures/stack.ml @@ -138,73 +138,51 @@ module Make (V : Value_intf.T) : let pop_i32 s = let hd, tl = pop s in - match hd with - | I32 n -> (n, tl) - | _ -> Log.err "invalid type (expected i32)" + match hd with I32 n -> (n, tl) | _ -> assert false let pop2_i32 s = let n2, s = pop s in let n1, tl = pop s in - match (n1, n2) with - | I32 n1, I32 n2 -> ((n1, n2), tl) - | _ -> Log.err "invalid type (expected i32)" + match (n1, n2) with I32 n1, I32 n2 -> ((n1, n2), tl) | _ -> assert false let pop_i64 s = let hd, tl = pop s in - match hd with - | I64 n -> (n, tl) - | _ -> Log.err "invalid type (expected i64)" + match hd with I64 n -> (n, tl) | _ -> assert false let pop2_i64 s = let n2, s = pop s in let n1, tl = pop s in - match (n1, n2) with - | I64 n1, I64 n2 -> ((n1, n2), tl) - | _ -> Log.err "invalid type (expected i64)" + match (n1, n2) with I64 n1, I64 n2 -> ((n1, n2), tl) | _ -> assert false let pop_f32 s = let hd, tl = pop s in - match hd with - | F32 f -> (f, tl) - | _ -> Log.err "invalid type (expected f32)" + match hd with F32 f -> (f, tl) | _ -> assert false let pop2_f32 s = let n2, s = pop s in let n1, tl = pop s in - match (n1, n2) with - | F32 n1, F32 n2 -> ((n1, n2), tl) - | _ -> Log.err "invalid type (expected f32)" + match (n1, n2) with F32 n1, F32 n2 -> ((n1, n2), tl) | _ -> assert false let pop_f64 s = let hd, tl = pop s in - match hd with - | F64 f -> (f, tl) - | _ -> Log.err "invalid type (expected f64)" + match hd with F64 f -> (f, tl) | _ -> assert false let pop2_f64 s = let n2, s = pop s in let n1, tl = pop s in - match (n1, n2) with - | F64 n1, F64 n2 -> ((n1, n2), tl) - | _ -> Log.err "invalid type (expected f64)" + match (n1, n2) with F64 n1, F64 n2 -> ((n1, n2), tl) | _ -> assert false let pop_ref s = let hd, tl = pop s in - match hd with - | Ref _ -> (hd, tl) - | _ -> Log.err "invalid type (expected ref)" + match hd with Ref _ -> (hd, tl) | _ -> assert false let pop_as_ref s = let hd, tl = pop s in - match hd with - | Ref hd -> (hd, tl) - | _ -> Log.err "invalid type (expected ref)" + match hd with Ref hd -> (hd, tl) | _ -> assert false let pop_bool s = let hd, tl = pop s in - match hd with - | I32 n -> (V.I32.to_bool n, tl) - | _ -> Log.err "invalid type (expected i32 (bool))" + match hd with I32 n -> (V.I32.to_bool n, tl) | _ -> assert false let pop_n s n = (List.filteri (fun i _hd -> i < n) s, List.filteri (fun i _hd -> i >= n) s) @@ -213,8 +191,5 @@ module Make (V : Value_intf.T) : let rec drop_n s n = if n = 0 then s - else - match s with - | [] -> Fmt.invalid_arg "drop_n" - | _ :: tl -> drop_n tl (n - 1) + else match s with [] -> assert false | _ :: tl -> drop_n tl (n - 1) end diff --git a/src/interpret/interpret.ml b/src/interpret/interpret.ml index 3c761c975..9edf91a48 100644 --- a/src/interpret/interpret.ml +++ b/src/interpret/interpret.ml @@ -1309,70 +1309,64 @@ module Make (P : Interpret_intf.P) : let* mem = Env.get_memory env mem_0 in let memory_length = Memory.size mem in let offset = const offset in - let> out_of_bounds = I32.(offset < const 0l) in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access - else - match nn with - | S32 -> - let n, stack = Stack.pop_i32 stack in - let pos, stack = Stack.pop_i32 stack in - let addr = I32.(pos + offset) in - let> out_of_bounds = - Bool.or_ I32.(lt_u memory_length (addr + const 4l)) - @@ I32.(pos < const 0l) - in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access - else begin - let* () = Memory.store_32 mem ~addr n in - st stack - end - | S64 -> - let n, stack = Stack.pop_i64 stack in - let pos, stack = Stack.pop_i32 stack in - let addr = I32.(pos + offset) in - let> out_of_bounds = - Bool.or_ I32.(lt_u memory_length (addr + const 8l)) - @@ I32.(pos < const 0l) - in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access - else begin - let* () = Memory.store_64 mem ~addr n in - st stack - end ) + match nn with + | S32 -> + let n, stack = Stack.pop_i32 stack in + let pos, stack = Stack.pop_i32 stack in + let addr = I32.(pos + offset) in + let> out_of_bounds = + Bool.or_ I32.(lt_u memory_length (addr + const 4l)) + @@ I32.(pos < const 0l) + in + if out_of_bounds then Choice.trap Out_of_bounds_memory_access + else begin + let* () = Memory.store_32 mem ~addr n in + st stack + end + | S64 -> + let n, stack = Stack.pop_i64 stack in + let pos, stack = Stack.pop_i32 stack in + let addr = I32.(pos + offset) in + let> out_of_bounds = + Bool.or_ I32.(lt_u memory_length (addr + const 8l)) + @@ I32.(pos < const 0l) + in + if out_of_bounds then Choice.trap Out_of_bounds_memory_access + else begin + let* () = Memory.store_64 mem ~addr n in + st stack + end ) | F_store (nn, { offset; _ }) -> ( let* mem = Env.get_memory env mem_0 in let memory_length = Memory.size mem in let offset = const offset in - let> out_of_bounds = I32.(offset < const 0l) in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access - else - match nn with - | S32 -> - let n, stack = Stack.pop_f32 stack in - let pos, stack = Stack.pop_i32 stack in - let addr = I32.(pos + offset) in - let> out_of_bounds = - Bool.or_ I32.(lt_u memory_length (addr + const 4l)) - @@ I32.(pos < const 0l) - in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access - else begin - let* () = Memory.store_32 mem ~addr (F32.to_bits n) in - st stack - end - | S64 -> - let n, stack = Stack.pop_f64 stack in - let pos, stack = Stack.pop_i32 stack in - let addr = I32.(pos + offset) in - let> out_of_bounds = - Bool.or_ I32.(lt_u memory_length (addr + const 8l)) - @@ I32.(pos < const 0l) - in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access - else begin - let* () = Memory.store_64 mem ~addr (F64.to_bits n) in - st stack - end ) + match nn with + | S32 -> + let n, stack = Stack.pop_f32 stack in + let pos, stack = Stack.pop_i32 stack in + let addr = I32.(pos + offset) in + let> out_of_bounds = + Bool.or_ I32.(lt_u memory_length (addr + const 4l)) + @@ I32.(pos < const 0l) + in + if out_of_bounds then Choice.trap Out_of_bounds_memory_access + else begin + let* () = Memory.store_32 mem ~addr (F32.to_bits n) in + st stack + end + | S64 -> + let n, stack = Stack.pop_f64 stack in + let pos, stack = Stack.pop_i32 stack in + let addr = I32.(pos + offset) in + let> out_of_bounds = + Bool.or_ I32.(lt_u memory_length (addr + const 8l)) + @@ I32.(pos < const 0l) + in + if out_of_bounds then Choice.trap Out_of_bounds_memory_access + else begin + let* () = Memory.store_64 mem ~addr (F64.to_bits n) in + st stack + end ) | I64_load32 (sx, { offset; _ }) -> let* mem = Env.get_memory env mem_0 in let offset = const offset in @@ -1402,31 +1396,26 @@ module Make (P : Interpret_intf.P) : | I_store16 (nn, { offset; _ }) -> let* mem = Env.get_memory env mem_0 in let offset = const offset in - let> out_of_bounds = I32.(offset < const 0l) in + let memory_length = Memory.size mem in + let n, stack = + match nn with + | S32 -> + let n, stack = Stack.pop_i32 stack in + (n, stack) + | S64 -> + let n, stack = Stack.pop_i64 stack in + (I64.to_int32 n, stack) + in + let pos, stack = Stack.pop_i32 stack in + let addr = I32.(pos + offset) in + let> out_of_bounds = + Bool.or_ I32.(pos < const 0l) I32.(lt_u memory_length (addr + const 2l)) + in if out_of_bounds then Choice.trap Out_of_bounds_memory_access - else - let memory_length = Memory.size mem in - let n, stack = - match nn with - | S32 -> - let n, stack = Stack.pop_i32 stack in - (n, stack) - | S64 -> - let n, stack = Stack.pop_i64 stack in - (I64.to_int32 n, stack) - in - let pos, stack = Stack.pop_i32 stack in - let addr = I32.(pos + offset) in - let> out_of_bounds = - Bool.or_ - I32.(pos < const 0l) - I32.(lt_u memory_length (addr + const 2l)) - in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access - else begin - let* () = Memory.store_16 mem ~addr n in - st stack - end + else begin + let* () = Memory.store_16 mem ~addr n in + st stack + end | I64_store32 { offset; _ } -> let* mem = Env.get_memory env mem_0 in let offset = const offset in @@ -1538,7 +1527,7 @@ module Make (P : Interpret_intf.P) : List.fold_left (fun u to_run -> let* () = u in - let+ end_stack, count = + let+ _end_stack, count = let env = Module_to_run.env modul in exec_expr envs env (State.Locals.of_list []) Stack.empty to_run None @@ -1546,12 +1535,7 @@ module Make (P : Interpret_intf.P) : Log.profile3 "Exec module %s@.%a@." (Option.value (Module_to_run.modul modul).id ~default:"anonymous" ) - State.print_count count; - match end_stack with - | [] -> () - | _ :: _ -> - Fmt.epr "non empty stack@\n%a@." Stack.pp end_stack; - assert false ) + State.print_count count ) (Choice.return ()) (Module_to_run.to_run modul) in diff --git a/src/script/script.ml b/src/script/script.ml index 7a0f7f009..3a4ec98f7 100644 --- a/src/script/script.ml +++ b/src/script/script.ml @@ -246,7 +246,7 @@ let run ~no_exhaustion ~optimize script = Compile.Text.until_link ~unsafe ~optimize ~name:None link_state m in let+ () = check_error_result expected got in - Log.err "TODO" + assert false | Assert (Assert_return (a, res)) -> Log.debug0 "*** assert_return@\n"; let* stack = action link_state a in diff --git a/src/symbolic/symbolic_memory.ml b/src/symbolic/symbolic_memory.ml index 56771af1f..2b9f9918f 100644 --- a/src/symbolic/symbolic_memory.ml +++ b/src/symbolic/symbolic_memory.ml @@ -23,10 +23,7 @@ let create size = ; chunks = Hashtbl.create 16 } -let i32 v = - match view v with - | Val (Num (I32 i)) -> i - | _ -> Log.err {|Unsupported symbolic value reasoning over "%a"|} Expr.pp v +let i32 v = match view v with Val (Num (I32 i)) -> i | _ -> assert false let grow m delta = let old_size = Value.I32.mul m.size page_size in @@ -190,7 +187,7 @@ let check_within_bounds m a = Ok ( Value.Bool.(or_ (const (Int32.lt ptr base)) upper_bound) , Value.const_i32 ptr ) ) - | _ -> Log.err {|Unable to calculate address of: "%a"|} Expr.pp a + | _ -> assert false let free m base = if not @@ Hashtbl.mem m.chunks base then diff --git a/src/symbolic/symbolic_memory_make.ml b/src/symbolic/symbolic_memory_make.ml index 88f9c2a4b..ae4d0fe1a 100644 --- a/src/symbolic/symbolic_memory_make.ml +++ b/src/symbolic/symbolic_memory_make.ml @@ -16,10 +16,7 @@ module Make (Backend : M) = struct { data = Backend.make (); size = Symbolic_value.const_i32 size } let i32 v = - match Smtml.Expr.view v with - | Val (Num (I32 i)) -> i - | _ -> - Log.err {|Unsupported symbolic value reasoning over "%a"|} Smtml.Expr.pp v + match Smtml.Expr.view v with Val (Num (I32 i)) -> i | _ -> assert false let grow m delta = let old_size = Symbolic_value.I32.mul m.size page_size in diff --git a/src/text_to_binary/assigned.ml b/src/text_to_binary/assigned.ml index 33e93e047..6672494db 100644 --- a/src/text_to_binary/assigned.ml +++ b/src/text_to_binary/assigned.ml @@ -70,8 +70,8 @@ let assign_heap_type (acc : type_acc) typ : type_acc Result.t = let func_types = match typ with | Def_func_t _ftype -> Indexed.return id typ :: func_types - | Def_array_t (_mut, _storage_type) -> func_types - | Def_struct_t _ -> func_types + | Def_array_t (_mut, _storage_type) -> assert false + | Def_struct_t _ -> assert false in { acc with func_types; last_assigned_int; all_types } diff --git a/src/text_to_binary/rewrite.ml b/src/text_to_binary/rewrite.ml index a2e419670..a04904d16 100644 --- a/src/text_to_binary/rewrite.ml +++ b/src/text_to_binary/rewrite.ml @@ -18,23 +18,21 @@ let typemap (types : binary str_type Named.t) = (fun idx typ acc -> TypeMap.add typ (Raw idx) acc) types TypeMap.empty -let find error (named : 'a Named.t) : _ -> binary indice Result.t = function - | Raw _i as indice -> Ok indice +let find (named : 'a Named.t) : _ -> binary indice = function + | Raw _i as indice -> indice | Text name -> ( match String_map.find_opt name named.named with - | None -> Error error - | Some i -> Ok (Raw i) ) + | None -> assert false + | Some i -> Raw i ) let get error (named : 'a Named.t) indice : 'a Indexed.t Result.t = - let* (Raw i) = find error named indice in + let (Raw i) = find named indice in (* TODO change Named.t structure to make that sensible *) match List.nth_opt named.values i with None -> Error error | Some v -> Ok v -let find_global (modul : Assigned.t) id : binary indice Result.t = - find (`Unknown_global id) modul.global id +let find_global (modul : Assigned.t) id : binary indice = find modul.global id -let find_memory (modul : Assigned.t) id : binary indice Result.t = - find (`Unknown_memory id) modul.mem id +let find_memory (modul : Assigned.t) id : binary indice = find modul.mem id let rewrite_expr (modul : Assigned.t) (locals : binary param list) (iexpr : text expr) : binary expr Result.t = @@ -91,32 +89,30 @@ let rewrite_expr (modul : Assigned.t) (locals : binary param list) in let* locals, _after_last_assigned_local = - List.fold_left - (fun acc ((name, _type) : binary param) -> - let* locals, next_free_int = acc in + list_fold_left + (fun (locals, next_free_int) ((name, _type) : binary param) -> match name with | None -> Ok (locals, next_free_int + 1) | Some name -> if String_map.mem name locals then Error (`Duplicate_local name) else Ok (String_map.add name next_free_int locals, next_free_int + 1) ) - (Ok (String_map.empty, 0)) - locals + (String_map.empty, 0) locals in let find_local = function - | Raw _i as id -> Ok id - | Text name as id -> ( + | Raw _i as id -> id + | Text name -> ( match String_map.find_opt name locals with - | None -> Error (`Unknown_local id) - | Some id -> Ok (Raw id) ) + | None -> assert false + | Some id -> Raw id ) in - let find_table id = find (`Unknown_table id) modul.table id in - let find_func id = find (`Unknown_func id) modul.func id in - let find_data id = find (`Unknown_data id) modul.data id in - let find_elem id = find (`Unknown_elem id) modul.elem id in - let find_type id = find (`Unknown_type id) modul.typ id in + let find_table id = find modul.table id in + let find_func id = find modul.func id in + let find_data id = find modul.data id in + let find_elem id = find modul.elem id in + let find_type id = find modul.typ id in let rec body (loop_count, block_ids) : text instr -> binary instr Result.t = function @@ -132,20 +128,20 @@ let rewrite_expr (modul : Assigned.t) (locals : binary param list) let+ id = block_id_to_raw (loop_count, block_ids) id in Br id | Call id -> - let+ id = find_func id in - Call id + let id = find_func id in + Ok (Call id) | Return_call id -> - let+ id = find_func id in - Return_call id + let id = find_func id in + Ok (Return_call id) | Local_set id -> - let+ id = find_local id in - Local_set id + let id = find_local id in + Ok (Local_set id) | Local_get id -> - let+ id = find_local id in - Local_get id + let id = find_local id in + Ok (Local_get id) | Local_tee id -> - let+ id = find_local id in - Local_tee id + let id = find_local id in + Ok (Local_tee id) | If_else (id, bt, e1, e2) -> let* bt = bt_to_raw bt in let block_ids = id :: block_ids in @@ -161,60 +157,60 @@ let rewrite_expr (modul : Assigned.t) (locals : binary param list) let+ e = expr e (loop_count, id :: block_ids) in Block (id, bt, e) | Call_indirect (tbl_i, bt) -> - let* tbl_i = find_table tbl_i in + let tbl_i = find_table tbl_i in let+ bt = bt_some_to_raw bt in Call_indirect (tbl_i, bt) | Return_call_indirect (tbl_i, bt) -> - let* tbl_i = find_table tbl_i in + let tbl_i = find_table tbl_i in let+ bt = bt_some_to_raw bt in Return_call_indirect (tbl_i, bt) | Call_ref t -> - let+ t = find_type t in - Call_ref t + let t = find_type t in + Ok (Call_ref t) | Return_call_ref bt -> let+ bt = bt_some_to_raw bt in Return_call_ref bt | Global_set id -> - let+ idx = find_global modul id in - Global_set idx + let idx = find_global modul id in + Ok (Global_set idx) | Global_get id -> - let+ idx = find_global modul id in - Global_get idx + let idx = find_global modul id in + Ok (Global_get idx) | Ref_func id -> - let+ id = find_func id in - Ref_func id + let id = find_func id in + Ok (Ref_func id) | Table_size id -> - let+ id = find_table id in - Table_size id + let id = find_table id in + Ok (Table_size id) | Table_get id -> - let+ id = find_table id in - Table_get id + let id = find_table id in + Ok (Table_get id) | Table_set id -> - let+ id = find_table id in - Table_set id + let id = find_table id in + Ok (Table_set id) | Table_grow id -> - let+ id = find_table id in - Table_grow id + let id = find_table id in + Ok (Table_grow id) | Table_init (i, i') -> - let* table = find_table i in - let+ elem = find_elem i' in - Table_init (table, elem) + let table = find_table i in + let elem = find_elem i' in + Ok (Table_init (table, elem)) | Table_fill id -> - let+ id = find_table id in - Table_fill id + let id = find_table id in + Ok (Table_fill id) | Table_copy (i, i') -> - let* table = find_table i in - let+ table' = find_table i' in - Table_copy (table, table') + let table = find_table i in + let table' = find_table i' in + Ok (Table_copy (table, table')) | Memory_init id -> - let+ id = find_data id in - Memory_init id + let id = find_data id in + Ok (Memory_init id) | Data_drop id -> - let+ id = find_data id in - Data_drop id + let id = find_data id in + Ok (Data_drop id) | Elem_drop id -> - let+ id = find_elem id in - Elem_drop id + let id = find_elem id in + Ok (Elem_drop id) | Select typ -> begin match typ with | None -> ok @@ Select None @@ -224,29 +220,29 @@ let rewrite_expr (modul : Assigned.t) (locals : binary param list) | Some [] | Some (_ :: _ :: _) -> Error `Invalid_result_arity end | Array_new_default id -> - let+ id = find_type id in - Array_new_default id + let id = find_type id in + Ok (Array_new_default id) | Array_set id -> - let+ id = find_type id in - Array_set id + let id = find_type id in + Ok (Array_set id) | Array_get id -> - let+ id = find_type id in - Array_set id + let id = find_type id in + Ok (Array_set id) | Ref_null heap_type -> let+ t = Binary_types.convert_heap_type None heap_type in Ref_null t | Br_on_cast (i, t1, t2) -> - let* i = find_type i in + let i = find_type i in let* t1 = Binary_types.convert_ref_type None t1 in let+ t2 = Binary_types.convert_ref_type None t2 in Br_on_cast (i, t1, t2) | Br_on_cast_fail (i, null, ht) -> - let* i = find_type i in + let i = find_type i in let+ ht = Binary_types.convert_heap_type None ht in Br_on_cast_fail (i, null, ht) | Struct_new_default i -> - let+ i = find_type i in - Struct_new_default i + let i = find_type i in + Ok (Struct_new_default i) | Ref_cast (null, ht) -> let+ ht = Binary_types.convert_heap_type None ht in Ref_cast (null, ht) @@ -286,12 +282,11 @@ let rewrite_block_type (typemap : binary indice TypeMap.t) (modul : Assigned.t) | _ -> assert false end | Bt_raw (_, func_type) -> - let* t = Binary_types.convert_func_type None func_type in - let+ idx = - try Ok (TypeMap.find (Def_func_t t) typemap) - with Not_found -> - Error - (`Msg (Fmt.str "Missing func type in index table %a" pp_func_type t)) + let+ t = Binary_types.convert_func_type None func_type in + let idx = + match TypeMap.find_opt (Def_func_t t) typemap with + | None -> assert false + | Some idx -> idx in Bt_raw (Some idx, t) @@ -309,11 +304,9 @@ let rewrite_elem (modul : Assigned.t) (elem : Text.elem) : Binary.elem Result.t match elem.mode with | Elem_declarative -> Ok Binary.Elem_declarative | Elem_passive -> Ok Elem_passive - | Elem_active (None, _expr) -> - (* TODO: does this really happen ? *) - Error (`Unknown_table (Raw 0)) + | Elem_active (None, _expr) -> assert false | Elem_active (Some id, expr) -> - let* (Raw indice) = find (`Unknown_table id) modul.table id in + let (Raw indice) = find modul.table id in let+ expr = rewrite_expr modul [] expr in Binary.Elem_active (Some indice, expr) in @@ -326,17 +319,15 @@ let rewrite_data (modul : Assigned.t) (data : Text.data) : Binary.data Result.t let+ mode = match data.mode with | Data_passive -> Ok Binary.Data_passive - | Data_active (None, _expr) -> - (* TODO: maybe we should change the type in assigned to avoid this case ? *) - assert false + | Data_active (None, _expr) -> assert false | Data_active (Some indice, expr) -> - let* (Raw indice) = find_memory modul indice in + let (Raw indice) = find_memory modul indice in let+ expr = rewrite_expr modul [] expr in Binary.Data_active (indice, expr) in { Binary.mode; id = data.id; init = data.init } -let rewrite_export err named (exports : Grouped.opt_export list) : +let rewrite_export named (exports : Grouped.opt_export list) : Binary.export list Result.t = list_map (fun { Grouped.name; id } -> @@ -344,26 +335,18 @@ let rewrite_export err named (exports : Grouped.opt_export list) : match id with | Curr id -> Ok id | Indice id -> - let+ (Raw id) = find (err id) named id in - id + let (Raw id) = find named id in + Ok id in { Binary.name; id } ) exports let rewrite_exports (modul : Assigned.t) (exports : Grouped.opt_exports) : Binary.exports Result.t = - let* global = - rewrite_export (fun id -> `Unknown_global id) modul.global exports.global - in - let* mem = - rewrite_export (fun id -> `Unknown_memory id) modul.mem exports.mem - in - let* table = - rewrite_export (fun id -> `Unknown_table id) modul.table exports.table - in - let+ func = - rewrite_export (fun id -> `Unknown_func id) modul.func exports.func - in + let* global = rewrite_export modul.global exports.global in + let* mem = rewrite_export modul.mem exports.mem in + let* table = rewrite_export modul.table exports.table in + let+ func = rewrite_export modul.func exports.func in { Binary.global; mem; table; func } let rewrite_func (typemap : binary indice TypeMap.t) (modul : Assigned.t) @@ -425,13 +408,13 @@ let modul (modul : Assigned.t) : Binary.modul Result.t = let runtime = rewrite_runtime (rewrite_func typemap modul) import in rewrite_named runtime modul.func in - let* types = rewrite_named (rewrite_types modul) modul.typ in - let+ start = + let+ types = rewrite_named (rewrite_types modul) modul.typ in + let start = match modul.start with - | None -> Ok None + | None -> None | Some id -> - let* (Raw id) = find (`Unknown_func id) func id in - Ok (Some id) + let (Raw id) = find func id in + Some id in let modul : Binary.modul = diff --git a/src/utils/result.ml b/src/utils/result.ml index 99d6d5c4f..9f6270ddb 100644 --- a/src/utils/result.ml +++ b/src/utils/result.ml @@ -124,5 +124,3 @@ let rec err_to_string = function | `Unknown_type id -> Fmt.str "unknown type %a" Types.pp_indice id | `Unsupported_file_extension ext -> Fmt.str "unsupported file_extension %S" ext - -let failwith e = Fmt.failwith "%s" (err_to_string e) diff --git a/src/utils/result.mli b/src/utils/result.mli index 56e93e634..8eacfbbc5 100644 --- a/src/utils/result.mli +++ b/src/utils/result.mli @@ -64,5 +64,3 @@ type err = type 'a t = ('a, err) Prelude.Result.t val err_to_string : err -> string - -val failwith : err -> 'a diff --git a/src/utils/syntax.ml b/src/utils/syntax.ml index 81d77970c..dcab8db4b 100644 --- a/src/utils/syntax.ml +++ b/src/utils/syntax.ml @@ -8,8 +8,6 @@ let ( let* ) o f = match o with Ok v -> f v | Error _ as e -> e let ( let+ ) o f = match o with Ok v -> Ok (f v) | Error _ as e -> e -let error v = Error v - let ok v = Ok v let list_iter f l = @@ -72,17 +70,3 @@ let array_map f a = raise Exit | Ok v -> v ) with Exit -> Option.get !err - -let array_fold_left f acc a = - let err = ref None in - let acc = ref acc in - try - for i = 0 to Array.length a - 1 do - match f !acc (Array.unsafe_get a i) with - | Error _e as e -> - err := Some e; - raise Exit - | Ok v -> acc := v - done; - Ok !acc - with Exit -> Option.get !err diff --git a/src/utils/syntax.mli b/src/utils/syntax.mli index b02f2b83a..bec07d026 100644 --- a/src/utils/syntax.mli +++ b/src/utils/syntax.mli @@ -10,8 +10,6 @@ val ( let* ) : val ( let+ ) : ('a, 'err) Prelude.Result.t -> ('a -> 'b) -> ('b, 'err) Prelude.Result.t -val error : string -> ('a, string) Prelude.Result.t - val ok : 'a -> ('a, 'err) Prelude.Result.t val list_iter : @@ -39,9 +37,3 @@ val array_map : ('a -> ('b, 'err) Prelude.Result.t) -> 'a array -> ('b array, 'err) Prelude.Result.t - -val array_fold_left : - ('a -> 'b -> ('a, 'err) Prelude.Result.t) - -> 'a - -> 'b array - -> ('a, 'err) Prelude.Result.t diff --git a/test/c/concolic.c b/test/c/concolic.c new file mode 100644 index 000000000..69933b218 --- /dev/null +++ b/test/c/concolic.c @@ -0,0 +1,15 @@ +#include + +int main(int argc, char **argv) { + static char array[5]; + char c = owi_i8(); + for (int i = 0; i < sizeof(array); i++) { + if (c == owi_i8()) { + return i; + } + } + + owi_assert(0); + + return 0; +} diff --git a/test/c/concolic.t b/test/c/concolic.t new file mode 100644 index 000000000..8fbbe20a2 --- /dev/null +++ b/test/c/concolic.t @@ -0,0 +1,12 @@ + $ owi c --concolic ./main.c --no-value + Assert failure + Model: + (model + (symbol_1 i32) + (symbol_2 i32) + (symbol_3 i32) + (symbol_4 i32) + (symbol_5 i32) + (symbol_6 i32)) + Reached problem! + [13] diff --git a/test/c/dune b/test/c/dune index 15998d46f..304cbc5ab 100644 --- a/test/c/dune +++ b/test/c/dune @@ -2,6 +2,7 @@ (deps %{bin:owi} (package owi) + concolic.c malloc_aligned.c main.c exit.c diff --git a/test/fmt/print_simplified.ml b/test/fmt/print_simplified.ml index a3b96500c..f23391c5f 100644 --- a/test/fmt/print_simplified.ml +++ b/test/fmt/print_simplified.ml @@ -9,23 +9,23 @@ let filename = Fpath.v Sys.argv.(1) let m = match Parse.Text.Module.from_file filename with | Ok m -> m - | Error e -> Result.failwith e + | Error _ -> assert false let m = match Compile.Text.until_binary ~unsafe:false m with | Ok m -> Binary_to_text.modul m - | Error e -> Result.failwith e + | Error _ -> assert false let s = Format.asprintf "%a@\n" Text.pp_modul m let m = match Parse.Text.Module.from_string s with | Ok m -> m - | Error e -> Result.failwith e + | Error _ -> assert false let m = match Compile.Text.until_binary ~unsafe:false m with | Ok m -> Binary_to_text.modul m - | Error e -> Result.failwith e + | Error _ -> assert false let () = Fmt.pr "%a@\n" Text.pp_modul m diff --git a/test/opt/debug.t b/test/opt/debug.t new file mode 100644 index 000000000..be822f59b --- /dev/null +++ b/test/opt/debug.t @@ -0,0 +1,25 @@ +test debug printing: + $ owi opt drop.wat --debug + parsing ... + checking ... + grouping ... + assigning ... + rewriting ... + typechecking ... + optimizing ... + (module + + (type (sub final (func))) + (global $g i32 i32.const 0) + (func $start + call 1 + call 2 + ) + (func $const + + ) + (func $local_global + + ) + (start 0) + )