From f0baed30f0cdbe60736da19783399c89140d6a47 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Thu, 28 Sep 2023 17:38:05 +0200 Subject: [PATCH] Adding tests for push/pop --- tests/dune.inc | 26 ++++++ .../testfile-push-pop1.err.dolmen.expected | 4 + .../smtlib/testfile-push-pop1.err.dolmen.smt2 | 22 +++++ tools/gentest.ml | 92 +++++++++++++------ 4 files changed, 115 insertions(+), 29 deletions(-) create mode 100644 tests/smtlib/testfile-push-pop1.err.dolmen.expected create mode 100644 tests/smtlib/testfile-push-pop1.err.dolmen.smt2 diff --git a/tests/dune.inc b/tests/dune.inc index 8cd156411..9f565477d 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -203125,6 +203125,32 @@ ; Auto-generated part end ; File auto-generated by gentests +; Auto-generated part begin +(subdir smtlib + (rule + (target testfile-push-pop1.err.dolmen_dolmen.output) + (deps (:input testfile-push-pop1.err.dolmen.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 1 123 124 125 142) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-push-pop1.err.dolmen_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-push-pop1.err.dolmen.expected testfile-push-pop1.err.dolmen_dolmen.output)))) +; Auto-generated part end +; File auto-generated by gentests + ; Auto-generated part begin (subdir sum (rule diff --git a/tests/smtlib/testfile-push-pop1.err.dolmen.expected b/tests/smtlib/testfile-push-pop1.err.dolmen.expected new file mode 100644 index 000000000..2321d46f4 --- /dev/null +++ b/tests/smtlib/testfile-push-pop1.err.dolmen.expected @@ -0,0 +1,4 @@ + +unknown + +unknown diff --git a/tests/smtlib/testfile-push-pop1.err.dolmen.smt2 b/tests/smtlib/testfile-push-pop1.err.dolmen.smt2 new file mode 100644 index 000000000..3573ba7c2 --- /dev/null +++ b/tests/smtlib/testfile-push-pop1.err.dolmen.smt2 @@ -0,0 +1,22 @@ +(set-logic ALL) + +; Pushing an empty assertion stack +(push 1) +(check-sat) + +(declare-const x Int) +; Pushing twice the assertion stack with 'x' +(push 2) + +; Pushing once the assertion stack with 'y' +(declare-const y Int) +(push 1) + +(assert (= x y)) +(check-sat) + +; Popping three times -> y disappears +(pop 3) + +(assert (= x y)) +; Raises an error \ No newline at end of file diff --git a/tools/gentest.ml b/tools/gentest.ml index 92181b68a..46ddaf9de 100644 --- a/tools/gentest.ml +++ b/tools/gentest.ml @@ -107,14 +107,24 @@ end = struct end module Test : sig + + type params = { + exclude: string list; + filters: string list option; + compare_should_succeed: bool; + ae_should_succeed: bool; + } + type t = private { cmd: Cmd.t; pb_file: string; - should_succeed: bool + params: params } (** Type of a test. *) - val make: cmd: Cmd.t -> pb_file: string -> should_succeed: bool -> t + val base_params : params + + val make: cmd: Cmd.t -> pb_file: string -> params:params -> t (** Set up the test. *) val pp_expected_output: t printer @@ -123,13 +133,28 @@ module Test : sig val pp_stanza: t printer (** Pretty print the dune test. *) end = struct + + type params = { + exclude: string list; + filters: string list option; + compare_should_succeed: bool; + ae_should_succeed: bool; + } + type t = { cmd: Cmd.t; pb_file: string; - should_succeed: bool + params: params; } - let make ~cmd ~pb_file ~should_succeed = {cmd; pb_file; should_succeed} + let base_params = { + exclude = []; + filters = None; + compare_should_succeed = true; + ae_should_succeed = true; + } + + let make ~cmd ~pb_file ~params = {cmd; pb_file; params} let pp_output fmt tst = let filename = Filename.chop_extension tst.pb_file in @@ -142,7 +167,7 @@ end = struct let pp_stanza fmt tst = let pp_diff_command fmt tst = - if tst.should_succeed then + if tst.params.compare_should_succeed then Format.fprintf fmt "@[(diff %a %a)@]" pp_expected_output tst pp_output tst @@ -152,6 +177,11 @@ end = struct pp_expected_output tst pp_output tst in + let accepted_ae_exit_code = + if tst.params.ae_should_succeed then + "0" + else "(or 1 123 124 125 142)" + in Format.fprintf fmt "\ @[\ (rule@,\ @@ -162,7 +192,7 @@ end = struct @[(chdir %%{workspace_root}@,\ @[(with-stdout-to %%{target}@,\ @[(ignore-stderr@,\ -@[(with-accepted-exit-codes 0@,\ +@[(with-accepted-exit-codes %s@,\ @[(run @[%a@])))))))@]@]@]@]@]@]@]@ \ @[(rule@,\ @[(deps %a)@,\ @@ -171,6 +201,7 @@ end = struct @[(action@ %a))@]@]@]@]@]" pp_output tst tst.pb_file + accepted_ae_exit_code Cmd.pp tst.cmd pp_output tst (Cmd.group tst.cmd) @@ -198,40 +229,43 @@ end = struct tests: Test.t list; } - let filter ?(exclude = []) filters cmd = - not (List.exists (String.equal (Cmd.name cmd)) exclude) && - match filters with + let filter (params : Test.params) cmd = + not (List.exists (String.equal (Cmd.name cmd)) params.exclude) && + match params.filters with | Some filters -> List.exists (String.equal (Cmd.name cmd)) filters | None -> true let make ~root ~path ~cmds ~pb_files = let tests = List.fold_left (fun acc1 pb_file -> - let exclude, filters, should_succeed = + let params = List.fold_left ( - fun (exclude, filters_opt, should_succeed) -> + fun (acc : Test.params) -> function | "fail" -> - exclude, - filters_opt, - false - | "dolmen" -> - "legacy" :: exclude, - Some ["dolmen"], - should_succeed - | "models" -> - "legacy" :: "fpa" :: exclude, - Some ["tableaux"], - should_succeed + {acc with compare_should_succeed = false} + | "err" -> + {acc with ae_should_succeed = false} + | "dolmen" -> { + acc with + exclude = "legacy" :: acc.exclude; + filters = Some ["dolmen"] + } + | "models" -> { + acc with + exclude = + "legacy" :: "fpa" :: acc.exclude; + filters = Some ["tableaux"] + } | "fpa" -> - exclude, - Some ["fpa"], - should_succeed - | _ -> (exclude, filters_opt, should_succeed) - ) ([], None, true) (String.split_on_char '.' pb_file) + {acc with filters = Some ["fpa"]} + | _ -> acc + ) + Test.base_params + (String.split_on_char '.' pb_file) in List.fold_left (fun acc2 cmd -> - if filter ~exclude filters cmd then - Test.make ~cmd ~pb_file ~should_succeed :: acc2 + if filter params cmd then + Test.make ~cmd ~pb_file ~params :: acc2 else acc2 ) acc1 cmds) [] pb_files