Change Default UI to New Display and Add UI Test Suite (rust-lang#828)

* Change expected files and add flags to explicitly demand old output

* Fix issues with dry run and change default output to regular style

* Add UI test suite

docs/src/tutorial/arbitrary-variables/Cargo.toml

@@ -11,4 +11,4 @@ vector-map = "1.0.1"
 [workspace]
 
 [workspace.metadata.kani]
-flags = { default-checks = false, unwind = "2" }
+flags = { default-checks = false, unwind = "2", output-format = "old" }

docs/src/tutorial/kani-first-steps/Cargo.toml

@@ -11,3 +11,6 @@ edition = "2018"
 proptest = "1.0.0"
 
 [workspace]
+
+[workspace.metadata.kani]
+flags = { output-format = "old" }

docs/src/tutorial/kinds-of-failure/Cargo.toml

@@ -11,3 +11,6 @@ edition = "2018"
 proptest = "1.0.0"
 
 [workspace]
+
+[workspace.metadata.kani]
+flags = { output-format = "old" }

docs/src/tutorial/loops-unwinding/Cargo.toml

@@ -10,4 +10,4 @@ edition = "2018"
 [workspace]
 
 [package.metadata.kani]
-flags = { unwind = "11" }
+flags = { unwind = "11", output-format = "old" }

scripts/cbmc_json_parser.py

@@ -26,7 +26,7 @@
 
 # Enum to store the style of output that is given by the argument flags
 output_style_switcher = {
-    'default': 'old',
+    'default': 'regular',
     'regular': 'regular',
     'terse': 'terse',
     'old': 'old'

scripts/kani-regression.sh

@@ -47,6 +47,7 @@ TESTS=(
     "cargo-kani cargo-kani"
     "kani-docs cargo-kani"
     "kani-fixme kani-fixme"
+    "ui expected"
 )
 
 # Extract testing suite information and run compiletest

scripts/kani.py

@@ -191,7 +191,7 @@ def run_cmd(
     # Write to stdout if specified, or if failure, or verbose or debug
     if (output_to == "stdout" or process.returncode != EXIT_CODE_SUCCESS or verbose or debug) and not quiet:
         # By Default, the flag passed is the old output style
-        if (output_style != kani_flags.OutputStyle.OLD):
+        if (output_style != kani_flags.OutputStyle.OLD and not dry_run):
             try:
                 cbmc_json_parser.transform_cbmc_output(stdout, output_style)
             except BaseException:

scripts/kani_flags.py

@@ -137,7 +137,7 @@ class OutputStyle(str, Enum):
     Allows user to pass flags and for kani to change the UI based on the
     flag that is passed. Ex - kani test.rs --output-format new
     """
-    DEFAULT = 'old'
+    DEFAULT = 'regular'
     REGULAR = 'regular'
     TERSE = 'terse'
     OLD = 'old'
@@ -242,7 +242,7 @@ def add_output_flags(make_group, add_flag, config):
     add_flag(
         group,
         "--output-format",
-        default=OutputStyle.OLD,
+        default=OutputStyle.DEFAULT,
         type=OutputStyle,
         action=EnumAction,
         help="Select the format for output")

tests/cargo-kani/dependencies/Cargo.toml

@@ -10,3 +10,6 @@ edition = "2021"
 [dependencies]
 memchr = { version = "2", default-features = false }
 rand = "0.8.4"
+
+[kani.flags]
+output-format = "old"

tests/cargo-kani/simple-config-toml/Cargo.toml

@@ -18,4 +18,5 @@ gen-c = true
 [kani.flags]
 visualize = false
 mangler = "v0"
+output-format = "old"
 cbmc-args = []

tests/cargo-kani/simple-extern/Cargo.toml

@@ -11,3 +11,6 @@ edition = "2018"
 
 [kani.flags.linking]
 c-lib = ["src/helper.c"]
+
+[kani.flags]
+output-format = "old"

tests/cargo-kani/simple-lib/Cargo.toml

@@ -8,3 +8,6 @@ edition = "2018"
 [dependencies]
 
 [workspace]
+
+[kani.flags]
+output-format = "old"

tests/cargo-kani/simple-main/Cargo.toml

@@ -8,3 +8,6 @@ edition = "2018"
 [dependencies]
 
 [workspace]
+
+[kani.flags]
+output-format = "old"

tests/cargo-kani/simple-proof-annotation/Cargo.toml

@@ -7,3 +7,6 @@ version = "0.1.0"
 edition = "2021"
 
 [dependencies]
+
+[kani.flags]
+output-format = "old"

tests/expected/abort/expected

@@ -1,3 +1,2 @@
-line 12 a panicking function std::process::abort is invoked: FAILURE
-line 16 a panicking function std::process::abort is invoked: SUCCESS
-
+line 14 a panicking function std::process::abort is invoked: FAILURE
+line 18 a panicking function std::process::abort is invoked: SUCCESS

tests/expected/abort/main.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --output-format old
 //
 // Test that the abort() function is respected and nothing beyond it will execute.
 

tests/expected/allocation/expected

@@ -1,2 +1,2 @@
-line 8 assertion failed: foo() == None: SUCCESS
-line 11 assertion failed: foo() == y: SUCCESS
+line 10 assertion failed: foo() == None: SUCCESS
+line 13 assertion failed: foo() == y: SUCCESS

tests/expected/allocation/main.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --output-format old
 fn foo() -> Option<i32> {
     None
 }

tests/expected/array/expected

@@ -3,7 +3,7 @@ array 'y'.0 upper bound in y.0[var_12]: SUCCESS
 array 'y'.0 upper bound in y.0[var_16]: FAILURE
 array 'x'.0 upper bound in x.0[var_3]: SUCCESS
 array 'x'.0 upper bound in x.0[var_5]: SUCCESS
-line 12 assertion failed: y[0] == 1: SUCCESS
-line 13 assertion failed: y[1] == 2: SUCCESS
-line 14 index out of bounds: the length is move _17 but the index is _16: FAILURE
-line 14 assertion failed: y[z] == 3: FAILURE
+line 14 assertion failed: y[0] == 1: SUCCESS
+line 15 assertion failed: y[1] == 2: SUCCESS
+line 16 index out of bounds: the length is move _17 but the index is _16: FAILURE
+line 16 assertion failed: y[z] == 3: FAILURE

tests/expected/array/main.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --output-format old
 // cbmc-flags: --bounds-check
 fn foo(x: [i32; 5]) -> [i32; 2] {
     [x[0], x[1]]

tests/expected/assert-eq/expected

@@ -1,3 +1,3 @@
-line 15 assertion failed: x + 1 == y: SUCCESS
-line 16 assertion failed: x == y: FAILURE
-line 17 assertion failed: x != y: SUCCESS
+line 17 assertion failed: x + 1 == y: SUCCESS
+line 18 assertion failed: x == y: FAILURE
+line 19 assertion failed: x != y: SUCCESS

tests/expected/assert-eq/main.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --output-format old
 /// This test touches a surprising amount of MIR, thanks to the `assert_eq!`, which translates into something like
 /// if(x != y) { String msg = format_error_message(<x as debug>::fmt(x), <y as debug>::fmt(y)); panic!(msg)} else {}
 /// This leads us to the land of foreign types, ReifyFnPointer, and transmute.

tests/expected/assert-location/assert-false/expected

@@ -1,3 +1,3 @@
-line 12 assertion failed: false: FAILURE
-line 17 "{}", s: FAILURE
-line 21 "Fail with custom static message": FAILURE
+line 13 assertion failed: false: FAILURE
+line 18 "{}", s: FAILURE
+line 22 "Fail with custom static message": FAILURE

tests/expected/assert-location/assert-false/main.rs

@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 // Check the location of the assert statement when using assert!(false);
+// kani-flags: --output-format old
 
 fn any_bool() -> bool {
     kani::nondet()

tests/expected/assert-location/debug-assert/expected

@@ -1,2 +1,2 @@
-line 6 This should fail and stop the execution: FAILURE
-line 7 "This should be unreachable": SUCCESS
+line 7 This should fail and stop the execution: FAILURE
+line 8 "This should be unreachable": SUCCESS

tests/expected/assert-location/debug-assert/main.rs

@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+// kani-flags: --output-format old
 pub fn main() {
     for i in 0..4 {
         debug_assert!(i > 0, "This should fail and stop the execution");

tests/expected/binop/expected

@@ -1,42 +1,42 @@
-line 4 attempt to compute `move _8 + move _9`, which would overflow: SUCCESS
-line 4 assertion failed: a + b == correct: SUCCESS
-line 5 attempt to compute `move _15 + move _16`, which would overflow: SUCCESS
-line 5 assertion failed: a + b == wrong: FAILURE
-line 9 attempt to compute `move _8 - move _9`, which would overflow: SUCCESS
-line 9 assertion failed: a - b == correct: SUCCESS
-line 10 attempt to compute `move _15 - move _16`, which would overflow: SUCCESS
-line 10 assertion failed: a - b == wrong: FAILURE
-line 14 attempt to compute `move _8 * move _9`, which would overflow: SUCCESS
-line 14 assertion failed: a * b == correct: SUCCESS
-line 15 attempt to compute `move _15 * move _16`, which would overflow: SUCCESS
-line 15 assertion failed: a * b == wrong: FAILURE
-line 19 attempt to divide `_8` by zero: SUCCESS
-line 19 attempt to compute `_8 / _9`, which would overflow: SUCCESS
-line 19 assertion failed: a / b == correct: SUCCESS
-line 20 attempt to divide `_18` by zero: SUCCESS
-line 20 attempt to compute `_18 / _19`, which would overflow: SUCCESS
-line 20 assertion failed: a / b == wrong: FAILURE
-line 24 attempt to calculate the remainder of `_8` with a divisor of zero: SUCCESS
-line 24 attempt to compute the remainder of `_8 % _9`, which would overflow: SUCCESS
-line 24 assertion failed: a % b == correct: SUCCESS
-line 25 attempt to calculate the remainder of `_18` with a divisor of zero: SUCCESS
-line 25 attempt to compute the remainder of `_18 % _19`, which would overflow: SUCCESS
-line 25 assertion failed: a % b == wrong: FAILURE
-line 29 attempt to shift left by `move _9`, which would overflow: SUCCESS
-line 29 assertion failed: a << b == correct: SUCCESS
-line 30 attempt to shift left by `move _16`, which would overflow: SUCCESS
-line 30 assertion failed: a << b == wrong: FAILURE
-line 34 attempt to shift right by `move _9`, which would overflow: SUCCESS
-line 34 assertion failed: a >> b == correct: SUCCESS
-line 35 attempt to shift right by `move _16`, which would overflow: SUCCESS
-line 35 assertion failed: a >> b == wrong: FAILURE
-line 39 attempt to shift right by `move _9`, which would overflow: SUCCESS
-line 39 assertion failed: a >> b == correct: SUCCESS
-line 40 attempt to shift right by `move _16`, which would overflow: SUCCESS
-line 40 assertion failed: a >> b == wrong: FAILURE
-line 44 assertion failed: a & b == correct: SUCCESS
-line 45 assertion failed: a & b == wrong: FAILURE
-line 49 assertion failed: a | b == correct: SUCCESS
-line 50 assertion failed: a | b == wrong: FAILURE
-line 54 assertion failed: a ^ b == correct: SUCCESS
-line 55 assertion failed: a ^ b == wrong: FAILURE
+line 6 attempt to compute `move _8 + move _9`, which would overflow: SUCCESS
+line 6 assertion failed: a + b == correct: SUCCESS
+line 7 attempt to compute `move _15 + move _16`, which would overflow: SUCCESS
+line 7 assertion failed: a + b == wrong: FAILURE
+line 11 attempt to compute `move _8 - move _9`, which would overflow: SUCCESS
+line 11 assertion failed: a - b == correct: SUCCESS
+line 12 attempt to compute `move _15 - move _16`, which would overflow: SUCCESS
+line 12 assertion failed: a - b == wrong: FAILURE
+line 16 attempt to compute `move _8 * move _9`, which would overflow: SUCCESS
+line 16 assertion failed: a * b == correct: SUCCESS
+line 17 attempt to compute `move _15 * move _16`, which would overflow: SUCCESS
+line 17 assertion failed: a * b == wrong: FAILURE
+line 21 attempt to divide `_8` by zero: SUCCESS
+line 21 attempt to compute `_8 / _9`, which would overflow: SUCCESS
+line 21 assertion failed: a / b == correct: SUCCESS
+line 22 attempt to divide `_18` by zero: SUCCESS
+line 22 attempt to compute `_18 / _19`, which would overflow: SUCCESS
+line 22 assertion failed: a / b == wrong: FAILURE
+line 26 attempt to calculate the remainder of `_8` with a divisor of zero: SUCCESS
+line 26 attempt to compute the remainder of `_8 % _9`, which would overflow: SUCCESS
+line 26 assertion failed: a % b == correct: SUCCESS
+line 27 attempt to calculate the remainder of `_18` with a divisor of zero: SUCCESS
+line 27 attempt to compute the remainder of `_18 % _19`, which would overflow: SUCCESS
+line 27 assertion failed: a % b == wrong: FAILURE
+line 31 attempt to shift left by `move _9`, which would overflow: SUCCESS
+line 31 assertion failed: a << b == correct: SUCCESS
+line 32 attempt to shift left by `move _16`, which would overflow: SUCCESS
+line 32 assertion failed: a << b == wrong: FAILURE
+line 36 attempt to shift right by `move _9`, which would overflow: SUCCESS
+line 36 assertion failed: a >> b == correct: SUCCESS
+line 37 attempt to shift right by `move _16`, which would overflow: SUCCESS
+line 37 assertion failed: a >> b == wrong: FAILURE
+line 41 attempt to shift right by `move _9`, which would overflow: SUCCESS
+line 41 assertion failed: a >> b == correct: SUCCESS
+line 42 attempt to shift right by `move _16`, which would overflow: SUCCESS
+line 42 assertion failed: a >> b == wrong: FAILURE
+line 46 assertion failed: a & b == correct: SUCCESS
+line 47 assertion failed: a & b == wrong: FAILURE
+line 51 assertion failed: a | b == correct: SUCCESS
+line 52 assertion failed: a | b == wrong: FAILURE
+line 56 assertion failed: a ^ b == correct: SUCCESS
+line 57 assertion failed: a ^ b == wrong: FAILURE

tests/expected/binop/main.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --output-format old
 fn iadd_test(a: i32, b: i32, correct: i32, wrong: i32) {
     assert!(a + b == correct);
     assert!(a + b == wrong);

tests/expected/closure/expected

@@ -1,6 +1,6 @@
-line 18 attempt to compute `move _8 + move _9`, which would overflow: SUCCESS
-line 18 attempt to compute `move _5 + move _6`, which would overflow: SUCCESS
-line 18 attempt to compute `(*((*_1).0: &mut i32)) + move _4`, which would overflow: SUCCESS
-line 23 attempt to compute `move _18 + const 12_i32`, which would overflow: SUCCESS
-line 23 assertion failed: original_num + 12 == num: SUCCESS
-line 23 arithmetic overflow on signed + in var_18 + 12: SUCCESS
+line 20 attempt to compute `move _8 + move _9`, which would overflow: SUCCESS
+line 20 attempt to compute `move _5 + move _6`, which would overflow: SUCCESS
+line 20 attempt to compute `(*((*_1).0: &mut i32)) + move _4`, which would overflow: SUCCESS
+line 25 attempt to compute `move _18 + const 12_i32`, which would overflow: SUCCESS
+line 25 assertion failed: original_num + 12 == num: SUCCESS
+line 25 arithmetic overflow on signed + in var_18 + 12: SUCCESS

tests/expected/closure/main.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --output-format old
 // cbmc-flags: --signed-overflow-check
 fn call_with_one<F>(mut some_closure: F) -> ()
 where

tests/expected/closure2/expected

@@ -1,4 +1,4 @@
-line 5 attempt to compute `move _3 + move _4`, which would overflow: SUCCESS
 line 7 attempt to compute `move _3 + move _4`, which would overflow: SUCCESS
-line 8 assertion failed: z == 102: SUCCESS
-line 9 assertion failed: g(z) == 206: SUCCESS
+line 9 attempt to compute `move _3 + move _4`, which would overflow: SUCCESS
+line 10 assertion failed: z == 102: SUCCESS
+line 11 assertion failed: g(z) == 206: SUCCESS

tests/expected/closure2/main.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --output-format old
 fn main() {
     let x = 2;
     let f = |y| x + y;

tests/expected/closure3/expected

@@ -1,3 +1,3 @@
-line 14 attempt to compute `move _3 + move _4`, which would overflow: SUCCESS
-line 15 attempt to compute `move _11 + const 10_i64`, which would overflow: SUCCESS
-line 15 assertion failed: num + 10 == y: SUCCESS
+line 16 attempt to compute `move _3 + move _4`, which would overflow: SUCCESS
+line 17 attempt to compute `move _11 + const 10_i64`, which would overflow: SUCCESS
+line 17 assertion failed: num + 10 == y: SUCCESS

tests/expected/closure3/main.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --output-format old
 fn call_with_one<F, T>(f: F) -> T
 where
     F: FnOnce(i64) -> T,

tests/expected/comp/expected

@@ -1,11 +1,11 @@
-line 5 attempt to compute `move _6 + move _7`, which would overflow: SUCCESS
-line 5 attempt to compute `move _10 + move _11`, which would overflow: SUCCESS
-line 5 assertion failed: a + b == b + a: SUCCESS
-line 6 attempt to compute `move _16 + move _17`, which would overflow: SUCCESS
-line 6 attempt to compute `move _21 + move _22`, which would overflow: SUCCESS
-line 6 attempt to compute `move _20 + const 1_i32`, which would overflow: SUCCESS
-line 6 assertion failed: a + b != a + b + 1: SUCCESS
-line 11 attempt to compute `move _6 + move _7`, which would overflow: SUCCESS
-line 11 assertion failed: a + b > a: SUCCESS
-line 12 attempt to compute `move _13 - move _14`, which would overflow: SUCCESS
-line 12 assertion failed: a - b < a: SUCCESS
+line 7 attempt to compute `move _6 + move _7`, which would overflow: SUCCESS
+line 7 attempt to compute `move _10 + move _11`, which would overflow: SUCCESS
+line 7 assertion failed: a + b == b + a: SUCCESS
+line 8 attempt to compute `move _16 + move _17`, which would overflow: SUCCESS
+line 8 attempt to compute `move _21 + move _22`, which would overflow: SUCCESS
+line 8 attempt to compute `move _20 + const 1_i32`, which would overflow: SUCCESS
+line 8 assertion failed: a + b != a + b + 1: SUCCESS
+line 13 attempt to compute `move _6 + move _7`, which would overflow: SUCCESS
+line 13 assertion failed: a + b > a: SUCCESS
+line 14 attempt to compute `move _13 - move _14`, which would overflow: SUCCESS
+line 14 assertion failed: a - b < a: SUCCESS

tests/expected/comp/main.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --output-format old
 #[allow(dead_code)]
 fn eq1(a: i32, b: i32) {
     assert!(a + b == b + a);

tests/expected/copy/main.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --output-format old
 use std::ptr;
 
 fn main() {

tests/expected/dry-run-flag-conflict-auto-unwind/main.rs

@@ -1,6 +1,8 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+// kani-flags: --output-format old
+
 // kani-flags: --dry-run --auto-unwind
 // cbmc-flags: --unwind 2