From 37f148c7da5868877e210cd95104e1e493510b84 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Sat, 10 Aug 2024 11:22:56 +0200 Subject: [PATCH] Trim explored paths and enable collections-c for owi conc --- example/conc/README.md | 2 +- src/cmd/cmd_conc.ml | 408 +++++++++--------- src/cmd/cmd_sym.ml | 8 +- src/concolic/concolic_choice.ml | 27 +- src/concolic/concolic_value.ml | 4 +- src/concolic/concolic_wasm_ffi.ml | 6 +- src/symbolic/symbolic_memory.ml | 7 +- src/symbolic/symbolic_value.ml | 1 + test/c/collections-c/array_tests.t | 51 --- test/c/collections-c/deque_tests.t | 69 --- test/c/collections-c/dune | 3 +- test/c/collections-c/list_tests.t | 75 ---- test/c/collections-c/queue_tests.t | 9 - test/c/collections-c/ring_buffer_tests.t | 7 - test/c/collections-c/run-subdir.sh | 35 ++ test/c/collections-c/slist_tests.t | 75 ---- test/c/collections-c/stack_tests.t | 5 - test/c/collections-c/tests_array.t | 123 ++++++ .../{buggy_tests.t => tests_buggy.t} | 6 +- test/c/collections-c/tests_deque.t | 172 ++++++++ test/c/collections-c/tests_list.t | 187 ++++++++ .../{pqueue_tests.t => tests_pqueue.t} | 15 +- test/c/collections-c/tests_queue.t | 22 + test/c/collections-c/tests_ring_buffer.t | 17 + test/c/collections-c/tests_slist.t | 187 ++++++++ test/c/collections-c/tests_stack.t | 12 + test/c/collections-c/tests_treeset.t | 32 ++ test/c/collections-c/tests_treetable.t | 67 +++ test/c/collections-c/treeset_tests.t | 13 - test/c/collections-c/treetable_tests.t | 27 -- test/conc/global_sharing.t | 2 +- test/wat2wasm/cmd_conc.t | 2 +- 32 files changed, 1114 insertions(+), 562 deletions(-) delete mode 100644 test/c/collections-c/array_tests.t delete mode 100644 test/c/collections-c/deque_tests.t delete mode 100644 test/c/collections-c/list_tests.t delete mode 100644 test/c/collections-c/queue_tests.t delete mode 100644 test/c/collections-c/ring_buffer_tests.t create mode 100755 test/c/collections-c/run-subdir.sh delete mode 100644 test/c/collections-c/slist_tests.t delete mode 100644 test/c/collections-c/stack_tests.t create mode 100644 test/c/collections-c/tests_array.t rename test/c/collections-c/{buggy_tests.t => tests_buggy.t} (75%) create mode 100644 test/c/collections-c/tests_deque.t create mode 100644 test/c/collections-c/tests_list.t rename test/c/collections-c/{pqueue_tests.t => tests_pqueue.t} (54%) create mode 100644 test/c/collections-c/tests_queue.t create mode 100644 test/c/collections-c/tests_ring_buffer.t create mode 100644 test/c/collections-c/tests_slist.t create mode 100644 test/c/collections-c/tests_stack.t create mode 100644 test/c/collections-c/tests_treeset.t create mode 100644 test/c/collections-c/tests_treetable.t delete mode 100644 test/c/collections-c/treeset_tests.t delete mode 100644 test/c/collections-c/treetable_tests.t diff --git a/example/conc/README.md b/example/conc/README.md index 25f8db645..4fa958b67 100644 --- a/example/conc/README.md +++ b/example/conc/README.md @@ -28,7 +28,7 @@ $ owi conc ./mini.wat Trap: unreachable Model: (model - (symbol_1 (i32 6))) + (symbol_1 (i32.const 6))) Reached problem! [13] ``` diff --git a/src/cmd/cmd_conc.ml b/src/cmd/cmd_conc.ml index 18858b0f7..6fa18d69f 100644 --- a/src/cmd/cmd_conc.ml +++ b/src/cmd/cmd_conc.ml @@ -8,7 +8,8 @@ module Choice = Concolic.P.Choice (* let () = Random.self_init () *) let () = Random.init 42 -let debug = false +(* TODO: add a flag for this *) +let print_paths = false let ( let** ) (t : 'a Result.t Choice.t) (f : 'a -> 'b Result.t Choice.t) : 'b Result.t Choice.t = @@ -62,12 +63,6 @@ let run_modules_to_run (link_state : _ Link.state) modules_to_run = (Interpret.Concolic.modul link_state.envs) to_run ) (Choice.return (Ok ())) modules_to_run -let get_model ~symbols solver pc = - let pc = Concolic_choice.pc_to_exprs pc in - Solver.model ~symbols ~pc solver - -type assignments = (Smtml.Symbol.t * Concrete_value.t) list - type end_of_trace = | Assume_fail | Assert_fail @@ -75,7 +70,7 @@ type end_of_trace = | Normal type trace = - { assignments : assignments + { assignments : Concolic_choice.assignments ; remaining_pc : Concolic_choice.pc_elt list ; end_of_trace : end_of_trace } @@ -106,6 +101,11 @@ end type unexplored = Unexplored.t +type assert_status = + | Unknown + | Valid + | Invalid of Concolic_choice.assignments + type node = | Select of { cond : Smtml.Expr.t @@ -123,35 +123,34 @@ type node = | Assert of { cond : Smtml.Expr.t ; cont : eval_tree - ; mutable disproved : assignments option + ; mutable status : assert_status } | Unreachable - | Not_explored + | Not_explored (** A node was discovered but has not yet been explored *) + | Being_explored + (** A node that has been seen in `find_node_to_run` and is being explored *) + | Explored (** A fully explored path *) and eval_tree = { mutable node : node ; mutable unexplored : unexplored - ; pc : Concolic_choice.pc - ; mutable ends : (end_of_trace * assignments) list + ; pc : Choice.pc + ; mutable ends : (end_of_trace * Concolic_choice.assignments) list } -let rec rec_count_unexplored tree = - match tree.node with - | Select { if_true; if_false; _ } -> - Unexplored.add - (rec_count_unexplored if_true) - (rec_count_unexplored if_false) - | Select_i32 { branches; _ } -> - IMap.fold - (fun _ branch -> Unexplored.add (rec_count_unexplored branch)) - branches Unexplored.zero - | Assume { cont; _ } | Assert { cont; _ } -> rec_count_unexplored cont - | Unreachable -> Unexplored.zero - | Not_explored -> Unexplored.one +let pp_node fmt = function + | Select _ -> Fmt.string fmt "Select" + | Select_i32 _ -> Fmt.string fmt "Select_i32" + | Assume _ -> Fmt.string fmt "Assume" + | Assert _ -> Fmt.string fmt "Assert" + | Unreachable -> Fmt.string fmt "Unreachable" + | Not_explored -> Fmt.string fmt "Not_explored" + | Being_explored -> Fmt.string fmt "Being_explored" + | Explored -> Fmt.string fmt "Explored" -let _ = rec_count_unexplored +let _ = pp_node -let count_unexplored tree = +let count_unexplored (tree : eval_tree) : Unexplored.t = match tree.node with | Select { if_true; if_false; _ } -> Unexplored.add if_true.unexplored if_false.unexplored @@ -160,19 +159,19 @@ let count_unexplored tree = (fun _ branch -> Unexplored.add branch.unexplored) branches Unexplored.zero | Assume { cont; _ } | Assert { cont; _ } -> cont.unexplored - | Unreachable -> Unexplored.zero + | Unreachable | Being_explored | Explored -> Unexplored.zero | Not_explored -> Unexplored.one let update_unexplored tree = tree.unexplored <- count_unexplored tree -let update_node tree node = +let update_node (tree : eval_tree) (node : node) : unit = tree.node <- node; update_unexplored tree -let fresh_tree pc = +let fresh_tree (pc : Choice.pc) : eval_tree = { node = Not_explored; unexplored = Unexplored.one; pc; ends = [] } -let new_node pc (head : Concolic_choice.pc_elt) : node = +let new_node (pc : Choice.pc) (head : Choice.pc_elt) : node = match head with | Select (cond, _) -> Select @@ -183,37 +182,42 @@ let new_node pc (head : Concolic_choice.pc_elt) : node = | Select_i32 (value, _) -> Select_i32 { value; branches = IMap.empty } | Assume cond -> Assume { cond; cont = fresh_tree (Assume cond :: pc) } | Assert cond -> - Assert { cond; cont = fresh_tree (Assert cond :: pc); disproved = None } + Assert { cond; cont = fresh_tree (Assert cond :: pc); status = Unknown } -let try_initialize pc node head = +let try_initialize (pc : Choice.pc) (node : eval_tree) (head : Choice.pc_elt) = match node.node with - | Not_explored -> update_node node (new_node pc head) + | Not_explored | Being_explored -> update_node node (new_node pc head) | _ -> () let check = true -let rec add_trace pc node (trace : trace) to_update : eval_tree list = +let set_on_unexplored tree transition = + match tree.node with + | Not_explored | Being_explored -> tree.node <- transition + | _ -> assert false (* Sanity Check *) + +let rec add_trace (pc : Choice.pc) (node : eval_tree) (trace : trace) + (to_update : eval_tree list) : eval_tree list = match trace.remaining_pc with | [] -> begin node.ends <- (trace.end_of_trace, trace.assignments) :: node.ends; - let () = - match trace.end_of_trace with - | Trap Unreachable -> begin - match node.node with - | Not_explored -> node.node <- Unreachable - | Unreachable -> () - | _ -> assert false - end - | _ -> () - in + ( match trace.end_of_trace with + | Normal -> set_on_unexplored node Explored + | Assume_fail -> + (* TODO: do something in this case? Otherwise, it might remain in Being_explored in unsat paths? *) + () + | Trap Unreachable -> set_on_unexplored node Unreachable + | Trap _ | Assert_fail -> + (* TODO: Mark this as explored to avoid possibly empty pcs? *) + () ); node :: to_update end | head_of_trace :: tail_of_trace -> ( try_initialize pc node head_of_trace; let pc = head_of_trace :: pc in match (node.node, head_of_trace) with - | Not_explored, _ -> assert false - | Unreachable, _ -> assert false + | (Unreachable | Not_explored | Being_explored | Explored), _ -> + assert false | Select { cond; if_true; if_false }, Select (cond', v) -> if check then assert (Smtml.Expr.equal cond cond'); let branch = if v then if_true else if_false in @@ -242,13 +246,11 @@ let rec add_trace pc node (trace : trace) to_update : eval_tree list = { trace with remaining_pc = tail_of_trace } (node :: to_update) | _, Assume _ | Assume _, _ -> assert false - | Assert ({ cond; cont; disproved = _ } as assert_), Assert cond' -> + | Assert ({ cond; cont; status = _ } as assert_), Assert cond' -> if check then assert (Smtml.Expr.equal cond cond'); - begin - match (tail_of_trace, trace.end_of_trace) with - | [], Assert_fail -> assert_.disproved <- Some trace.assignments - | _ -> () - end; + ( match (tail_of_trace, trace.end_of_trace) with + | [], Assert_fail -> assert_.status <- Invalid trace.assignments + | _ -> () ); add_trace pc cont { trace with remaining_pc = tail_of_trace } (node :: to_update) ) @@ -257,20 +259,17 @@ let add_trace tree trace = let to_update = add_trace [] tree trace [] in List.iter update_unexplored to_update -let run_once tree link_state modules_to_run forced_values = +let run_once link_state modules_to_run (forced_values : Smtml.Model.t) = let backups = List.map Concolic.backup modules_to_run in let result = run_modules_to_run link_state modules_to_run in - let ( ( result - , Choice. - { pc - ; symbols = _ - ; symbols_value - ; shared = _ - ; preallocated_values = _ - } ) as r ) = - let forced_values = - match forced_values with None -> Hashtbl.create 0 | Some v -> v - in + let ( result + , Choice. + { pc + ; symbols = _ + ; symbols_value + ; shared = _ + ; preallocated_values = _ + } ) = Choice.run forced_values result in let () = List.iter2 Concolic.recover backups modules_to_run in @@ -285,116 +284,131 @@ let run_once tree link_state modules_to_run forced_values = let trace = { assignments = symbols_value; remaining_pc = List.rev pc; end_of_trace } in - if debug then begin - Fmt.pr "Add trace:@\n"; - Fmt.pr "%a@\n" Concolic_choice.pp_pc trace.remaining_pc - end; - add_trace tree trace; - r + (result, trace) (* Very naive ! *) -let rec find_node_to_run tree = - match tree.node with - | Not_explored -> - if debug then begin - Fmt.pr "Try unexplored@.%a@.@." Concolic_choice.pp_pc tree.pc - end; - Some tree.pc - | Select { cond = _; if_true; if_false } -> - let b = - if Unexplored.none if_true.unexplored then false - else if Unexplored.none if_false.unexplored then true - else Random.bool () - in - if debug then begin - Fmt.pr "Select bool %b@." b - end; - let tree = if b then if_true else if_false in - find_node_to_run tree - | Select_i32 { value = _; branches } -> - (* TODO: better ! *) - let branches = IMap.bindings branches in - let branches = - List.filter (fun (_i, v) -> not (Unexplored.none v.unexplored)) branches - in - let n = List.length branches in - if n = 0 then None - else begin - let i = Random.int n in - let i, branch = List.nth branches i in - if debug then begin - Fmt.pr "Select_i32 %li@." i - end; - find_node_to_run branch - end - | Assume { cond = _; cont } -> find_node_to_run cont - | Assert { cond; cont = _; disproved = None } -> - let pc : Concolic_choice.pc = Select (cond, false) :: tree.pc in - Fmt.pr "Try Assert@.%a@.@." Concolic_choice.pp_pc pc; - Some pc - | Assert { cond = _; cont; disproved = Some _ } -> find_node_to_run cont - | Unreachable -> - Fmt.pr "Unreachable (Retry)@.%a@." Concolic_choice.pp_pc tree.pc; - None +let find_node_to_run tree = + let ( let* ) = Option.bind in + let rec loop tree to_update = + match tree.node with + | Not_explored -> + Log.debug2 "Try unexplored@.%a@." Concolic_choice.pp_pc tree.pc; + Some (tree.pc, tree :: to_update) + | Select { cond = _; if_true; if_false } -> + let* b = + match + ( Unexplored.none if_true.unexplored + , Unexplored.none if_false.unexplored ) + with + | true, false -> Some false (* Unexplored paths in `else` branch *) + | false, true -> Some true (* Unexplored paths in `then` branch *) + | false, false -> Some (Random.bool ()) (* Unexplored in both *) + | true, true -> None (* No unexplored remain *) + in + Log.debug1 "Select bool %b@." b; + loop (if b then if_true else if_false) (tree :: to_update) + | Select_i32 { value = _; branches } -> + (* TODO: better ! *) + let branches = IMap.bindings branches in + let branches = + List.filter (fun (_i, v) -> not (Unexplored.none v.unexplored)) branches + in + let n = List.length branches in + if n = 0 then None + else begin + let i = Random.int n in + let i, branch = List.nth branches i in + Log.debug1 "Select_i32 %li@." i; + loop branch (tree :: to_update) + end + | Assume { cond = _; cont } -> loop cont (tree :: to_update) + | Assert { cond; cont = _; status = Unknown } -> + let pc : Concolic_choice.pc = Select (cond, false) :: tree.pc in + Log.debug2 "Try Assert@.%a@.@." Concolic_choice.pp_pc pc; + Some (pc, tree :: to_update) + | Assert { cond = _; cont; status = _ } -> loop cont (tree :: to_update) + | Unreachable -> + Log.debug2 "Unreachable (Retry)@.%a@." Concolic_choice.pp_pc tree.pc; + None + | Being_explored | Explored -> None + in + loop tree [] let pc_model solver pc = let pc = Concolic_choice.pc_to_exprs pc in match Solver.check solver pc with | `Unsat | `Unknown -> None | `Sat -> - let symbols = None in - let model = Solver.model ~symbols ~pc solver in - Some model - -let find_model_to_run solver tree = - match find_node_to_run tree with - | None -> None - | Some pc -> pc_model solver pc - -let launch solver tree link_state modules_to_run = - let rec find_model n = - if n = 0 then begin - Fmt.pr "Failed to find something to run@\n"; - None - end - else - match find_model_to_run solver tree with - | None -> find_model (n - 1) - | Some m -> - if debug then begin - Fmt.pr "Found something to run %a@\n" - (Smtml.Model.pp ~no_values:false) - m - end; - Some m - in - 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 : _ 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 _ as e) -> e - | Error (Assume_fail c) -> begin - if debug then begin - Fmt.pr "Assume_fail: %a@\n" Smtml.Expr.pp c; - Fmt.pr "Assignments:@\n%a@\n" Concolic_choice.pp_assignments - thread.symbols_value; - Fmt.pr "Retry !@\n" - end; - match pc_model solver thread.pc with + let symbols = Some (Smtml.Expr.get_symbols pc) in + Some (Solver.model ~symbols ~pc solver) + +let rec find_model_to_run solver tree = + let ( let* ) = Option.bind in + let* pc, to_update = find_node_to_run tree in + let node = List.hd to_update in + let model = + match pc with + | [] -> assert false + | pc -> ( + match pc_model solver pc with | None -> - Fmt.epr "Can't satisfy assume !@\n"; - loop (count - 1) - | Some _model as model -> run_model model (count - 1) - end - | Error (Trap trap) -> Ok (Some (`Trap trap, thread)) - | Error Assert_fail -> Ok (Some (`Assert_fail, thread)) + ( match node.node with + | Not_explored -> node.node <- Unreachable + | Assert assert_ -> assert_.status <- Valid + | _ -> assert false (* Sanity check *) ); + find_model_to_run solver tree + | Some model -> + ( match node.node with + | Not_explored -> node.node <- Being_explored + | Assert assert_ -> assert_.status <- Invalid [] (* TODO: assignments *) + | _ -> assert false (* Sanity check *) ); + Some model ) in - loop 10 + (* Have to update tree because of the paths trimmed above *) + List.iter update_unexplored to_update; + model + +let count_path = ref 0 + +let run solver tree link_state modules_to_run = + (* Initial model is empty (no symbolic variables yet) *) + let initial_model = Hashtbl.create 0 in + let rec loop model = + incr count_path; + let* result, trace = run_once link_state modules_to_run model in + add_trace tree trace; + let* error = + match result with + | Ok (Ok ()) -> Ok None + | Ok (Error _ as e) -> e + | Error (Assume_fail c) -> ( + decr count_path; + (* Current path condition led to assume failure, try to satisfy *) + Log.debug2 "Assume_fail: %a@." Smtml.Expr.pp c; + Log.debug2 "Pc:@.%a" Concolic_choice.pp_pc trace.remaining_pc; + Log.debug2 "Assignments:@.%a@." + (Concolic_choice.pp_assignments ~no_values:false) + trace.assignments; + Log.debug0 "Retry !@."; + match pc_model solver (Assume c :: trace.remaining_pc) with + | Some model -> loop model + | None -> Ok None ) + | Error (Trap trap) -> + (* TODO: Check if we want to report this *) + Ok (Some (`Trap trap, trace)) + | Error Assert_fail -> + (* TODO: Check if we want to report this *) + Ok (Some (`Assert_fail, trace)) + in + match error with + | Some _ -> Ok error + | None -> ( + (* No error, we can go again if we still have stuff to explore *) + match find_model_to_run solver tree with + | None -> Ok None + | Some model -> loop model ) + in + loop initial_model (* NB: This function propagates potential errors (Result.err) occurring during evaluation (OS, syntax error, etc.), except for Trap and Assert, @@ -404,7 +418,6 @@ let cmd profiling debug unsafe optimize _workers _no_stop_at_failure no_values _deterministic_result_order _fail_mode (workspace : Fpath.t) solver files = if profiling then Log.profiling_on := true; if debug then Log.debug_on := true; - (* deterministic_result_order implies no_stop_at_failure *) (* let no_stop_at_failure = deterministic_result_order || no_stop_at_failure in *) let* _created_dir = Bos.OS.Dir.create ~path:true ~mode:0o755 workspace in @@ -413,50 +426,41 @@ 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 print_pc pc = - Fmt.pr "PC:@\n"; - Fmt.pr "%a@\n" Concolic_choice.pp_pc pc - in - let print_values symbols_value = - Fmt.pr "Assignments:@\n"; - List.iter - (fun (s, v) -> Fmt.pr " %a: %a" Smtml.Symbol.pp s Concrete_value.pp v) - symbols_value; - Fmt.pr "@\n" - in - - let testcase model = + let* result = run solver tree link_state modules_to_run in + let testcase assignments = if not no_values then - let testcase = Smtml.Model.get_bindings model |> List.map snd in + let testcase : Smtml.Value.t list = + List.map + (fun (_, v) -> + match v with + | Concrete_value.I32 x -> Smtml.Value.Num (I32 x) + | I64 x -> Num (I64 x) + | F32 x -> Num (F32 (Float32.to_bits x)) + | F64 x -> Num (F64 (Float64.to_bits x)) + | Ref _ -> assert false ) + assignments + in Cmd_utils.write_testcase ~dir:workspace testcase else Ok () in - + if print_paths then Fmt.pr "Completed paths: %d@." !count_path; match result with | None -> - Fmt.pr "OK@\n"; + Fmt.pr "All OK@."; Ok () - | Some (`Trap trap, thread) -> + | Some (`Trap trap, { assignments; _ }) -> + let assignments = List.rev assignments in Fmt.pr "Trap: %s@\n" (Trap.to_string trap); - if debug then begin - print_pc thread.pc; - print_values thread.symbols_value - end; - let symbols = None in - let model = get_model ~symbols solver thread.pc in - Fmt.pr "Model:@\n @[%a@]@." (Smtml.Model.pp ~no_values) model; - let* () = testcase model in + Fmt.pr "Model:@\n @[%a@]@." + (Concolic_choice.pp_assignments ~no_values) + assignments; + let* () = testcase assignments in Error (`Found_bug 1) - | Some (`Assert_fail, thread) -> + | Some (`Assert_fail, { assignments; _ }) -> + let assignments = List.rev assignments in Fmt.pr "Assert failure@\n"; - if debug then begin - print_pc thread.pc; - print_values thread.symbols_value - end; - let symbols = None in - let model = get_model ~symbols solver thread.pc in - Fmt.pr "Model:@\n @[%a@]@." (Smtml.Model.pp ~no_values) model; - let* () = testcase model in + Fmt.pr "Model:@\n @[%a@]@." + (Concolic_choice.pp_assignments ~no_values) + assignments; + let* () = testcase assignments in Error (`Found_bug 1) diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml index 00b869aca..8c1af29cb 100644 --- a/src/cmd/cmd_sym.ml +++ b/src/cmd/cmd_sym.ml @@ -12,6 +12,9 @@ type fail_mode = | `Both ] +(* TODO: add a flag for this *) +let print_paths = false + let ( let*/ ) (t : 'a Result.t) (f : 'a -> 'b Result.t Choice.t) : 'b Result.t Choice.t = match t with Error e -> Choice.return (Error e) | Ok x -> f x @@ -54,8 +57,10 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values let result = List.fold_left (run_file ~unsafe ~optimize) pc files in let thread = Thread_with_memory.init () in let res_queue = Wq.make () in + let path_count = ref 0 in let callback v = let open Symbolic_choice_intf in + incr path_count; match (fail_mode, v) with | _, (EVal (Ok ()), _) -> () | _, (EVal (Error e), thread) -> Wq.push (`Error e, thread) res_queue @@ -115,8 +120,9 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values else results in let* count = print_and_count_failures 0 results in + if print_paths then Fmt.pr "Completed paths: %d@." !path_count; if count > 0 then Error (`Found_bug count) else begin - Fmt.pr "All OK"; + Fmt.pr "All OK@."; Ok () end diff --git a/src/concolic/concolic_choice.ml b/src/concolic/concolic_choice.ml index 126e40c28..a57afbc2f 100644 --- a/src/concolic/concolic_choice.ml +++ b/src/concolic/concolic_choice.ml @@ -14,6 +14,10 @@ type pc_elt = | Assume of Symbolic_value.vbool | Assert of Symbolic_value.vbool +type pc = pc_elt list + +type assignments = (Smtml.Symbol.t * Concrete_value.t) list + let pp_pc_elt fmt = function | Select (c, v) -> Fmt.pf fmt "Select(%a, %b)" Smtml.Expr.pp c v | Select_i32 (c, v) -> Fmt.pf fmt "Select_i32(%a, %li)" Smtml.Expr.pp c v @@ -22,11 +26,16 @@ let pp_pc_elt fmt = function let pp_pc fmt pc = List.iter (fun e -> Fmt.pf fmt " %a@\n" pp_pc_elt e) pc -let pp_assignments fmt assignments = - List.iter - (fun (sym, v) -> - Fmt.pf fmt " %a : %a@\n" Smtml.Symbol.pp sym Concrete_value.pp v ) - assignments +let pp_assignments ~no_values fmt assignments = + let open Smtml in + let pp_v = + if not no_values then + Fmt.parens (Fmt.pair ~sep:Fmt.sp Symbol.pp (Fmt.parens Concrete_value.pp)) + else fun fmt (x, _) -> + let ty = Symbol.type_of x in + Fmt.parens (Fmt.pair ~sep:Fmt.sp Smtml.Symbol.pp Smtml.Ty.pp) fmt (x, ty) + in + Fmt.pf fmt "(model@\n %a)" (Fmt.vbox (Fmt.list pp_v)) assignments let pc_elt_to_expr = function | Select (c, v) -> Some (if v then c else Smtml.Expr.Bool.not c) @@ -36,8 +45,6 @@ let pc_elt_to_expr = function let pc_to_exprs pc = List.filter_map pc_elt_to_expr pc -type pc = pc_elt list - type shared_thread_info = { memories : Symbolic_memory.collection ; tables : Symbolic_table.collection @@ -47,7 +54,7 @@ type shared_thread_info = type thread = { pc : pc ; symbols : int - ; symbols_value : (Smtml.Symbol.t * Concrete_value.t) list + ; symbols_value : assignments ; preallocated_values : (Smtml.Symbol.t, Smtml.Value.t) Hashtbl.t ; shared : shared_thread_info } @@ -84,7 +91,7 @@ let ( let+ ) = map let abort = M (fun st -> - (Ok (), { st with pc = Assert (Symbolic_value.Bool.const false) :: st.pc }) + (Ok (), { st with pc = Assume (Symbolic_value.Bool.const false) :: st.pc }) ) let add_pc (c : Concolic_value.V.vbool) = @@ -94,7 +101,7 @@ let add_pc_to_thread (st : thread) c = { st with pc = c :: st.pc } let no_choice e = let v = Smtml.Expr.simplify e in - match Smtml.Expr.view v with Val _ -> true | _ -> false + not (Smtml.Expr.is_symbolic v) let select (vb : Concolic_value.V.vbool) = let r = vb.concrete in diff --git a/src/concolic/concolic_value.ml b/src/concolic/concolic_value.ml index db607edbf..fc848f586 100644 --- a/src/concolic/concolic_value.ml +++ b/src/concolic/concolic_value.ml @@ -141,9 +141,7 @@ module T_pair (C : Value_intf.T) (S : Value_intf.T) = struct match (C.Ref.get_func ref.concrete, S.Ref.get_func ref.symbolic) with | Null, Null -> Null | Type_mismatch, Type_mismatch -> Type_mismatch - | Ref_value c, Ref_value s -> - assert (equal_func_intf c s); - Ref_value c + | Ref_value c, Ref_value _s -> Ref_value c | _ -> assert false let get_externref ref ty_id : _ Value_intf.get_ref = diff --git a/src/concolic/concolic_wasm_ffi.ml b/src/concolic/concolic_wasm_ffi.ml index abc4ed679..4a7f16ab7 100644 --- a/src/concolic/concolic_wasm_ffi.ml +++ b/src/concolic/concolic_wasm_ffi.ml @@ -110,14 +110,16 @@ module M : match view v.symbolic with | Val (Num (I32 v)) -> Choice.return v | _ -> - Log.debug2 {|alloc: cannot allocate base pointer "%a"|} Expr.pp v.symbolic; + Log.debug2 {|alloc: cannot allocate base pointer "%a"@.|} Expr.pp + v.symbolic; Choice.bind (abort ()) (fun () -> assert false) let ptr (v : Value.int32) : int32 Choice.t = match view v.symbolic with | Ptr { base; _ } -> Choice.return base | _ -> - Log.debug2 {|free: cannot fetch pointer base of "%a"|} Expr.pp v.symbolic; + Log.debug2 {|free: cannot fetch pointer base of "%a"@.|} Expr.pp + v.symbolic; Choice.bind (abort ()) (fun () -> assert false) let exit (_p : Value.int32) : unit Choice.t = abort () diff --git a/src/symbolic/symbolic_memory.ml b/src/symbolic/symbolic_memory.ml index 2b9f9918f..69519e55e 100644 --- a/src/symbolic/symbolic_memory.ml +++ b/src/symbolic/symbolic_memory.ml @@ -149,9 +149,10 @@ let extract v pos = | Val (Num (I64 i)) -> let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in value (Num (I8 i')) - | Cvtop (_, Zero_extend 24, ({ node = Symbol _; _ } as sym)) - | Cvtop (_, Sign_extend 24, ({ node = Symbol _; _ } as sym)) - when Smtml.Ty.equal (Ty_bitv 8) (ty sym) -> + | Cvtop + ( _ + , (Zero_extend 24 | Sign_extend 24) + , ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym) ) -> sym | _ -> make (Extract (v, pos + 1, pos)) diff --git a/src/symbolic/symbolic_value.ml b/src/symbolic/symbolic_value.ml index c3ee37722..d8861ce0c 100644 --- a/src/symbolic/symbolic_value.ml +++ b/src/symbolic/symbolic_value.ml @@ -200,6 +200,7 @@ module I32 = struct let to_bool (e : vbool) = match view e with | Val (Num (I32 i)) -> Bool.const @@ Int32.ne i 0l + | Ptr _ -> Bool.const true | Cvtop (_, OfBool, cond) -> cond | _ -> make (Cvtop (ty, ToBool, e)) diff --git a/test/c/collections-c/array_tests.t b/test/c/collections-c/array_tests.t deleted file mode 100644 index cb098ee86..000000000 --- a/test/c/collections-c/array_tests.t +++ /dev/null @@ -1,51 +0,0 @@ -Array tests: - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_add.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_addAt2.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_contains.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_deepCopy.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_getAt.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_indexOf.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_iterAdd.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_iterRemove.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_iterReplace.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_reduce.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_remove.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_removeAll.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_removeAt.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_replaceAt.c - Assert failure: (bool.ne symbol_3 symbol_2) - Model: - (model - (symbol_0 (i32 0)) - (symbol_1 (i32 0)) - (symbol_2 (i32 0)) - (symbol_3 (i32 0))) - Reached problem! - [13] - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_reverse.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_shallowCopy.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_subarray.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_zipIterAdd.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_zipIterNext.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_zipIterRemove.c - All OK - $ owi c -I files/normal/include files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/array/array_test_zipIterReplace.c - All OK diff --git a/test/c/collections-c/deque_tests.t b/test/c/collections-c/deque_tests.t deleted file mode 100644 index d34de03ca..000000000 --- a/test/c/collections-c/deque_tests.t +++ /dev/null @@ -1,69 +0,0 @@ -Deque tests: - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_bufferExpansion.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_contains.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_trimCapacity.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_copyShallow.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_addLast.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_removeFirst.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_filter2.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_filter1.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_getFirst.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_getAt.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_addFirst.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_size.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_filter3.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_zipIterRemove.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_filterMut1.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_addAt4.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_reverse.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_getLast.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_filterMut2.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_iterRemove.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_addAt1.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_iterNext.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_removeAll.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_zipIterAdd.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_iterAdd.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_removeLast.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_zipIterNext.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_addAt2.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_capacity.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_copyDeep.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_addAt3.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_zipIterReplace.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_addAt5.c - All OK - $ owi c -I files/normal/include files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/deque/deque_test_filterMut3.c - All OK diff --git a/test/c/collections-c/dune b/test/c/collections-c/dune index 7e35cc7bd..8339d15fb 100644 --- a/test/c/collections-c/dune +++ b/test/c/collections-c/dune @@ -2,4 +2,5 @@ (deps %{bin:owi} (package owi) - (source_tree files))) + (source_tree files) + run-subdir.sh)) diff --git a/test/c/collections-c/list_tests.t b/test/c/collections-c/list_tests.t deleted file mode 100644 index 8741b3d9b..000000000 --- a/test/c/collections-c/list_tests.t +++ /dev/null @@ -1,75 +0,0 @@ -List tests: - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_zipIterAdd.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_add.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_indexOf.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_removeAll.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_copyShallow.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_zipIterNext.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_removeLast.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_addFirst.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_splice.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_new.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_copyDeep.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_mutFilter2.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_spliceAt.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_filter2.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_addLast.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_iterDescAdd.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_iterDescRemove.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_replaceAt.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_getLast.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_zipIterReplace.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_filter1.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_removeFirst.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_sort.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_zipIterRemove.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_addAt.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_sublist.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_iterAdd.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_iterRemove.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_mutFilter1.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_addAll.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_getAt.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_remove.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_contains.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_removeAt.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_addAllAt.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_toArray.c - All OK - $ owi c -I files/normal/include files/normal/src/list.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/list/list_test_reverse.c - All OK diff --git a/test/c/collections-c/queue_tests.t b/test/c/collections-c/queue_tests.t deleted file mode 100644 index 86be9dc58..000000000 --- a/test/c/collections-c/queue_tests.t +++ /dev/null @@ -1,9 +0,0 @@ -Queue tests: - $ owi c -I files/normal/include files/normal/src/queue.c files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/queue/queue_test_enqueue.c - All OK - $ owi c -I files/normal/include files/normal/src/queue.c files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/queue/queue_test_poll.c - All OK - $ owi c -I files/normal/include files/normal/src/queue.c files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/queue/queue_test_iter.c - All OK - $ owi c -I files/normal/include files/normal/src/queue.c files/normal/src/deque.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/queue/queue_test_zipIterNext.c - All OK diff --git a/test/c/collections-c/ring_buffer_tests.t b/test/c/collections-c/ring_buffer_tests.t deleted file mode 100644 index e490736a7..000000000 --- a/test/c/collections-c/ring_buffer_tests.t +++ /dev/null @@ -1,7 +0,0 @@ -Ring-buffer tests: - $ owi c -I files/normal/include files/normal/src/ring_buffer.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/ring_buffer/ring_buffer_test_enqueue.c - All OK - $ owi c -I files/normal/include files/normal/src/ring_buffer.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/ring_buffer/ring_buffer_test_dequeue.c - All OK - $ owi c -I files/normal/include files/normal/src/ring_buffer.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/ring_buffer/ring_buffer_test_capacity.c - All OK diff --git a/test/c/collections-c/run-subdir.sh b/test/c/collections-c/run-subdir.sh new file mode 100755 index 000000000..0608b601c --- /dev/null +++ b/test/c/collections-c/run-subdir.sh @@ -0,0 +1,35 @@ +#!/bin/sh + +DIR=$1 +shift + +OPT=$@ + +SRC=$(ls files/normal/src/*.c) + +run_once() { + mode=$1 + test=$2 + + owi c \ + $OPT \ + $mode \ + -I ./files/normal/include \ + $SRC \ + $test + + return_code=$? + [ $return_code -ne 0 ] && printf "\n[$return_code]\n" +} + +for test in $(ls files/normal/testsuite/$DIR/*.c); do + printf "Testing \"$test\":\n" + + printf "Using owi sym:\n" + run_once "" "$test" + + printf "Using owi conc:\n" + run_once "--concolic" "$test" +done + +exit 0 diff --git a/test/c/collections-c/slist_tests.t b/test/c/collections-c/slist_tests.t deleted file mode 100644 index 128019ea1..000000000 --- a/test/c/collections-c/slist_tests.t +++ /dev/null @@ -1,75 +0,0 @@ -Slist tests: - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_addAll.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_filterMut3.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_removeAll.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_toArray.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_removeAt.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_copyDeep.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_get.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_remove.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_addFirst.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_addAt.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_contains.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_spliceAt.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_iterAdd.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_zipIterNext.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_getFirst.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_removeLast.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_removeFirst.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_new.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_add.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_addLast.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_zipIterAdd.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_filter3.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_copyShallow.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_indexOf.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_getLast.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_sublist.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_filter2.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_filter1.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_zipIterReplace.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_splice.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_zipIterRemove.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_filterMut2.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_reverse.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_addAllAt.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_replaceAt.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_filterMut1.c - All OK - $ owi c -I files/normal/include files/normal/src/slist.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/slist/slist_test_iterRemove.c - All OK diff --git a/test/c/collections-c/stack_tests.t b/test/c/collections-c/stack_tests.t deleted file mode 100644 index defe9c1c1..000000000 --- a/test/c/collections-c/stack_tests.t +++ /dev/null @@ -1,5 +0,0 @@ -Stack tests: - $ owi c -I files/normal/include files/normal/src/stack.c files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/stack/stack_test_pop.c - All OK - $ owi c -I files/normal/include files/normal/src/stack.c files/normal/src/array.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/stack/stack_test_push.c - All OK diff --git a/test/c/collections-c/tests_array.t b/test/c/collections-c/tests_array.t new file mode 100644 index 000000000..084fb0fbc --- /dev/null +++ b/test/c/collections-c/tests_array.t @@ -0,0 +1,123 @@ +Array tests: + $ ./run-subdir.sh array + Testing "files/normal/testsuite/array/array_test_add.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_addAt2.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_contains.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_deepCopy.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_getAt.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_indexOf.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_iterAdd.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_iterRemove.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_iterReplace.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_reduce.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_remove.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_removeAll.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_removeAt.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_replaceAt.c": + Using owi sym: + Assert failure: (bool.ne symbol_3 symbol_2) + Model: + (model + (symbol_0 (i32 0)) + (symbol_1 (i32 0)) + (symbol_2 (i32 0)) + (symbol_3 (i32 0))) + Reached problem! + [13] + Using owi conc: + Assert failure + Model: + (model + (symbol_1 (i32.const 1048068351)) + (symbol_2 (i32.const 12775386)) + (symbol_3 (i32.const 0)) + (symbol_4 (i32.const 0))) + Reached problem! + [13] + Testing "files/normal/testsuite/array/array_test_reverse.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_shallowCopy.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_subarray.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_zipIterAdd.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_zipIterNext.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_zipIterRemove.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/array/array_test_zipIterReplace.c": + Using owi sym: + All OK + Using owi conc: + All OK diff --git a/test/c/collections-c/buggy_tests.t b/test/c/collections-c/tests_buggy.t similarity index 75% rename from test/c/collections-c/buggy_tests.t rename to test/c/collections-c/tests_buggy.t index e7461e39d..dab6207d6 100644 --- a/test/c/collections-c/buggy_tests.t +++ b/test/c/collections-c/tests_buggy.t @@ -1,12 +1,14 @@ Bug-triggering tests: - $ owi c -I files/bugs/include files/bugs/src/array.c files/bugs/src/common.c files/bugs/src/utils.c files/bugs/testsuite/array_test_remove.c + $ owi c -I files/bugs/include files/bugs/src/array.c files/bugs/src/common.c \ + > files/bugs/src/utils.c files/bugs/testsuite/array_test_remove.c Trap: memory heap buffer overflow Model: (model (symbol_0 (i32 8))) Reached problem! [13] - $ owi c -I files/bugs/include files/bugs/src/list.c files/bugs/src/common.c files/bugs/src/utils.c files/bugs/testsuite/list_test_zipIterAdd.c --no-value + $ owi c -I files/bugs/include files/bugs/src/list.c files/bugs/src/common.c \ + > files/bugs/src/utils.c files/bugs/testsuite/list_test_zipIterAdd.c --no-value Assert failure: false Model: (model diff --git a/test/c/collections-c/tests_deque.t b/test/c/collections-c/tests_deque.t new file mode 100644 index 000000000..119bfabc5 --- /dev/null +++ b/test/c/collections-c/tests_deque.t @@ -0,0 +1,172 @@ +Deque tests: + $ ./run-subdir.sh deque + Testing "files/normal/testsuite/deque/deque_test_addAt1.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_addAt2.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_addAt3.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_addAt4.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_addAt5.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_addFirst.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_addLast.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_bufferExpansion.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_capacity.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_contains.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_copyDeep.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_copyShallow.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_filter1.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_filter2.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_filter3.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_filterMut1.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_filterMut2.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_filterMut3.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_getAt.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_getFirst.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_getLast.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_iterAdd.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_iterNext.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_iterRemove.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_removeAll.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_removeFirst.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_removeLast.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_reverse.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_size.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_trimCapacity.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_zipIterAdd.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_zipIterNext.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_zipIterRemove.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/deque/deque_test_zipIterReplace.c": + Using owi sym: + All OK + Using owi conc: + All OK diff --git a/test/c/collections-c/tests_list.t b/test/c/collections-c/tests_list.t new file mode 100644 index 000000000..14a9cb334 --- /dev/null +++ b/test/c/collections-c/tests_list.t @@ -0,0 +1,187 @@ +List tests: + $ ./run-subdir.sh list + Testing "files/normal/testsuite/list/list_test_add.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_addAll.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_addAllAt.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_addAt.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_addFirst.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_addLast.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_contains.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_copyDeep.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_copyShallow.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_filter1.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_filter2.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_getAt.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_getLast.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_indexOf.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_iterAdd.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_iterDescAdd.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_iterDescRemove.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_iterRemove.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_mutFilter1.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_mutFilter2.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_new.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_remove.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_removeAll.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_removeAt.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_removeFirst.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_removeLast.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_replaceAt.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_reverse.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_sort.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_splice.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_spliceAt.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_sublist.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_toArray.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_zipIterAdd.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_zipIterNext.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_zipIterRemove.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/list/list_test_zipIterReplace.c": + Using owi sym: + All OK + Using owi conc: + All OK diff --git a/test/c/collections-c/pqueue_tests.t b/test/c/collections-c/tests_pqueue.t similarity index 54% rename from test/c/collections-c/pqueue_tests.t rename to test/c/collections-c/tests_pqueue.t index 3e1ffb119..cf1ce580c 100644 --- a/test/c/collections-c/pqueue_tests.t +++ b/test/c/collections-c/tests_pqueue.t @@ -1,5 +1,7 @@ Pqueue tests: - $ owi c -O0 -I files/normal/include files/normal/src/pqueue.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/pqueue/pqueue_test_enqueue.c --no-value + $ ./run-subdir.sh pqueue -O0 --no-value + Testing "files/normal/testsuite/pqueue/pqueue_test_enqueue.c": + Using owi sym: Trap: memory heap buffer overflow Model: (model @@ -9,9 +11,12 @@ Pqueue tests: (symbol_3 i32) (symbol_4 i32) (symbol_5 i32)) - Reached problem!Segmentation fault - [139] - $ owi c -O0 -I files/normal/include files/normal/src/pqueue.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/pqueue/pqueue_test_pop.c --no-value + Reached problem! + [13] + Using owi conc: + All OK + Testing "files/normal/testsuite/pqueue/pqueue_test_pop.c": + Using owi sym: Trap: memory heap buffer overflow Model: (model @@ -26,3 +31,5 @@ Pqueue tests: (symbol_8 i32)) Reached problem! [13] + Using owi conc: + All OK diff --git a/test/c/collections-c/tests_queue.t b/test/c/collections-c/tests_queue.t new file mode 100644 index 000000000..a81f77dcb --- /dev/null +++ b/test/c/collections-c/tests_queue.t @@ -0,0 +1,22 @@ +Queue tests: + $ ./run-subdir.sh queue + Testing "files/normal/testsuite/queue/queue_test_enqueue.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/queue/queue_test_iter.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/queue/queue_test_poll.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/queue/queue_test_zipIterNext.c": + Using owi sym: + All OK + Using owi conc: + All OK diff --git a/test/c/collections-c/tests_ring_buffer.t b/test/c/collections-c/tests_ring_buffer.t new file mode 100644 index 000000000..8fae9f005 --- /dev/null +++ b/test/c/collections-c/tests_ring_buffer.t @@ -0,0 +1,17 @@ +Ring-buffer tests: + $ ./run-subdir.sh ring_buffer + Testing "files/normal/testsuite/ring_buffer/ring_buffer_test_capacity.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/ring_buffer/ring_buffer_test_dequeue.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/ring_buffer/ring_buffer_test_enqueue.c": + Using owi sym: + All OK + Using owi conc: + All OK diff --git a/test/c/collections-c/tests_slist.t b/test/c/collections-c/tests_slist.t new file mode 100644 index 000000000..efc4af0a6 --- /dev/null +++ b/test/c/collections-c/tests_slist.t @@ -0,0 +1,187 @@ +Slist tests: + $ ./run-subdir.sh slist + Testing "files/normal/testsuite/slist/slist_test_add.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_addAll.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_addAllAt.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_addAt.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_addFirst.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_addLast.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_contains.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_copyDeep.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_copyShallow.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_filter1.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_filter2.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_filter3.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_filterMut1.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_filterMut2.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_filterMut3.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_get.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_getFirst.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_getLast.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_indexOf.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_iterAdd.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_iterRemove.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_new.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_remove.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_removeAll.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_removeAt.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_removeFirst.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_removeLast.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_replaceAt.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_reverse.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_splice.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_spliceAt.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_sublist.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_toArray.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_zipIterAdd.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_zipIterNext.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_zipIterRemove.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/slist/slist_test_zipIterReplace.c": + Using owi sym: + All OK + Using owi conc: + All OK diff --git a/test/c/collections-c/tests_stack.t b/test/c/collections-c/tests_stack.t new file mode 100644 index 000000000..7e5afc1a0 --- /dev/null +++ b/test/c/collections-c/tests_stack.t @@ -0,0 +1,12 @@ +Stack tests: + $ ./run-subdir.sh stack + Testing "files/normal/testsuite/stack/stack_test_pop.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/stack/stack_test_push.c": + Using owi sym: + All OK + Using owi conc: + All OK diff --git a/test/c/collections-c/tests_treeset.t b/test/c/collections-c/tests_treeset.t new file mode 100644 index 000000000..ca20e8680 --- /dev/null +++ b/test/c/collections-c/tests_treeset.t @@ -0,0 +1,32 @@ +Treeset tests: + $ ./run-subdir.sh treeset + Testing "files/normal/testsuite/treeset/treeset_test_add.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/treeset/treeset_test_iterNext.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/treeset/treeset_test_iterRemove.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/treeset/treeset_test_remove.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/treeset/treeset_test_removeAll.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/treeset/treeset_test_size.c": + Using owi sym: + All OK + Using owi conc: + All OK diff --git a/test/c/collections-c/tests_treetable.t b/test/c/collections-c/tests_treetable.t new file mode 100644 index 000000000..83b701ff1 --- /dev/null +++ b/test/c/collections-c/tests_treetable.t @@ -0,0 +1,67 @@ +Treetable tests: + $ ./run-subdir.sh treetable + Testing "files/normal/testsuite/treetable/treetable_test_add.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/treetable/treetable_test_get.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/treetable/treetable_test_getFirst.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/treetable/treetable_test_getGreaterThan.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/treetable/treetable_test_getLast.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/treetable/treetable_test_getLessThan.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/treetable/treetable_test_iterNext.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/treetable/treetable_test_iterRemove.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/treetable/treetable_test_remove.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/treetable/treetable_test_removeAll.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/treetable/treetable_test_removeFirst.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/treetable/treetable_test_removeLast.c": + Using owi sym: + All OK + Using owi conc: + All OK + Testing "files/normal/testsuite/treetable/treetable_test_size.c": + Using owi sym: + All OK + Using owi conc: + All OK diff --git a/test/c/collections-c/treeset_tests.t b/test/c/collections-c/treeset_tests.t deleted file mode 100644 index 7b7d22398..000000000 --- a/test/c/collections-c/treeset_tests.t +++ /dev/null @@ -1,13 +0,0 @@ -Treeset tests: - $ owi c -I files/normal/include files/normal/src/treeset.c files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treeset/treeset_test_remove.c - All OK - $ owi c -I files/normal/include files/normal/src/treeset.c files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treeset/treeset_test_iterNext.c - All OK - $ owi c -I files/normal/include files/normal/src/treeset.c files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treeset/treeset_test_removeAll.c - All OK - $ owi c -I files/normal/include files/normal/src/treeset.c files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treeset/treeset_test_iterRemove.c - All OK - $ owi c -I files/normal/include files/normal/src/treeset.c files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treeset/treeset_test_add.c - All OK - $ owi c -I files/normal/include files/normal/src/treeset.c files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treeset/treeset_test_size.c - All OK diff --git a/test/c/collections-c/treetable_tests.t b/test/c/collections-c/treetable_tests.t deleted file mode 100644 index 65001a6de..000000000 --- a/test/c/collections-c/treetable_tests.t +++ /dev/null @@ -1,27 +0,0 @@ -Treetable tests: - $ owi c -I files/normal/include files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treetable/treetable_test_getFirst.c - All OK - $ owi c -I files/normal/include files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treetable/treetable_test_remove.c - All OK - $ owi c -I files/normal/include files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treetable/treetable_test_iterNext.c - All OK - $ owi c -I files/normal/include files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treetable/treetable_test_removeFirst.c - All OK - $ owi c -I files/normal/include files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treetable/treetable_test_getGreaterThan.c - All OK - $ owi c -I files/normal/include files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treetable/treetable_test_getLessThan.c - All OK - $ owi c -I files/normal/include files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treetable/treetable_test_size.c - All OK - $ owi c -I files/normal/include files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treetable/treetable_test_removeAll.c - All OK - $ owi c -I files/normal/include files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treetable/treetable_test_iterRemove.c - All OK - $ owi c -I files/normal/include files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treetable/treetable_test_add.c - All OK - $ owi c -I files/normal/include files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treetable/treetable_test_get.c - All OK - $ owi c -I files/normal/include files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treetable/treetable_test_removeLast.c - All OK - $ owi c -I files/normal/include files/normal/src/treetable.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/treetable/treetable_test_getLast.c - All OK diff --git a/test/conc/global_sharing.t b/test/conc/global_sharing.t index f02f7ad9d..a34575016 100644 --- a/test/conc/global_sharing.t +++ b/test/conc/global_sharing.t @@ -1,2 +1,2 @@ $ owi conc global_sharing.wat - OK + All OK diff --git a/test/wat2wasm/cmd_conc.t b/test/wat2wasm/cmd_conc.t index b454b6c09..88d880fd4 100644 --- a/test/wat2wasm/cmd_conc.t +++ b/test/wat2wasm/cmd_conc.t @@ -3,7 +3,7 @@ Trap: unreachable Model: (model - (symbol_1 (i32 6))) + (symbol_1 (i32.const 6))) Reached problem! [13] $ owi wasm2wat symbolic.wasm