Skip to content

Commit

Permalink
Simplify results handling in main thread.
Browse files Browse the repository at this point in the history
Since 853bd37, all results processed in
the main thread are errors.
  • Loading branch information
krtab committed Jun 26, 2024
1 parent 853bd37 commit f0bf04d
Show file tree
Hide file tree
Showing 4 changed files with 14 additions and 18 deletions.
2 changes: 1 addition & 1 deletion src/cmd/cmd_conc.ml
Original file line number Diff line number Diff line change
Expand Up @@ -437,7 +437,7 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
let testcase =
List.sort compare (Smtml.Model.get_bindings model) |> List.map snd
in
Cmd_utils.write_testcase ~dir:workspace ~err:true testcase
Cmd_utils.write_testcase ~dir:workspace testcase
else Ok ()
in

Expand Down
19 changes: 8 additions & 11 deletions src/cmd/cmd_sym.ml
Original file line number Diff line number Diff line change
Expand Up @@ -85,32 +85,29 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
match results () with
| Seq.Nil -> Ok count_acc
| Seq.Cons ((result, _thread), tl) ->
let* is_err, model =
let* model =
let open Symbolic_choice in
match result with
| EAssert (assertion, model) ->
print_bug (`EAssert (assertion, model));
Ok (true, Some model)
Ok model
| ETrap (tr, model) ->
print_bug (`ETrap (tr, model));
Ok (true, Some model)
| EVal (Ok ()) -> Ok (false, None)
Ok model
| EVal (Ok ()) ->
failwith "unreachable: callback should have filtered eval ok out."
| EVal (Error e) -> Error e
in
let count_acc = if is_err then succ count_acc else count_acc in
let count_acc = succ count_acc in
let* () =
if not no_values then
let model =
match model with None -> Hashtbl.create 16 | Some m -> m
in
let testcase =
List.sort compare (Smtml.Model.get_bindings model) |> List.map snd
in
Cmd_utils.write_testcase ~dir:workspace ~err:is_err testcase
Cmd_utils.write_testcase ~dir:workspace testcase
else Ok ()
in
if (not is_err) || no_stop_at_failure then
print_and_count_failures count_acc tl
if no_stop_at_failure then print_and_count_failures count_acc tl
else Ok count_acc
in
let results =
Expand Down
8 changes: 4 additions & 4 deletions src/cmd/cmd_utils.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,10 @@

open Syntax

let out_testcase ~dst ~err testcase =
let out_testcase ~dst testcase =
let o = Xmlm.make_output ~nl:true ~indent:(Some 2) dst in
let tag ?(atts = []) name = (("", name), atts) in
let atts = if err then Some [ (("", "coversError"), "true") ] else None in
let atts = Some [ (("", "coversError"), "true") ] in

This comment has been minimized.

Copy link
@zapashcanon

zapashcanon Jun 26, 2024

Member

I believe you can replace let tag ?(atts = []) by let tag atts and remove the option here now @krtab.

let to_string v = Format.asprintf "%a" Smtml.Value.pp_num v in
let input v = `El (tag "input", [ `Data (to_string v) ]) in
let testcase = `El (tag ?atts "testcase", List.map input testcase) in
Expand All @@ -19,13 +19,13 @@ let out_testcase ~dst ~err testcase =

let write_testcase =
let cnt = ref 0 in
fun ~dir ~err testcase ->
fun ~dir testcase ->
incr cnt;
let name = Format.ksprintf Fpath.v "testcase-%d.xml" !cnt in
let path = Fpath.append dir name in
let* res =
Bos.OS.File.with_oc path
(fun chan () -> Ok (out_testcase ~dst:(`Channel chan) ~err testcase))
(fun chan () -> Ok (out_testcase ~dst:(`Channel chan) testcase))
()
in
res
Expand Down
3 changes: 1 addition & 2 deletions src/cmd/cmd_utils.mli
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,7 @@
(* Copyright © 2021-2024 OCamlPro *)
(* Written by the Owi programmers *)

val write_testcase :
dir:Fpath.t -> err:bool -> Smtml.Value.t list -> unit Result.t
val write_testcase : dir:Fpath.t -> Smtml.Value.t list -> unit Result.t

val add_main_as_start :
Binary.modul -> (Binary.modul, [> `Msg of string ]) result

0 comments on commit f0bf04d

Please sign in to comment.