From 2f681d28026d92c1256d2019be643fb87dc1a392 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed Date: Wed, 21 Jul 2021 19:04:09 +0000 Subject: [PATCH 1/5] Differentiate between check, codegen, and verification errors. --- src/test/cbmc/BinOp_Offset/main_fail.rs | 3 + .../cbmc/Count/Unstable/Ctlz/bounds_fail.rs | 1 + .../cbmc/Count/Unstable/Cttz/bounds_fail.rs | 1 + src/test/cbmc/DynTrait/boxed_trait_fail.rs | 2 + .../cbmc/DynTrait/different_crates_fail.rs | 2 + src/test/cbmc/DynTrait/nested_boxes_fail.rs | 2 + src/test/cbmc/FatPointers/boxmuttrait_fail.rs | 2 + src/test/cbmc/FatPointers/boxslice2_fail.rs | 2 + src/test/cbmc/FatPointers/boxtrait_fail.rs | 2 + src/test/cbmc/FatPointers/trait1_fail.rs | 2 + src/test/cbmc/FatPointers/trait2_fail.rs | 2 + src/test/cbmc/FatPointers/trait3_fail.rs | 2 + src/test/cbmc/Intrinsics/abort_fail.rs | 3 + .../cbmc/PointerOffset/Unstable/main_fail.rs | 3 + src/test/cbmc/SIMD/Compare/main_fail.rs | 3 + src/test/cbmc/SizeAndAlignOfDst/main_fail.rs | 2 + src/test/cbmc/Slice/pathbuf_fail.rs | 3 + src/test/cbmc/Slice/slice_from_raw_fail.rs | 3 + ...Binary_search_fail.rs => Binary_search.rs} | 3 +- src/test/smack/basic/add_fail.rs | 1 + src/test/smack/basic/arith_assume_fail.rs | 1 + src/test/smack/basic/div_fail.rs | 1 + src/test/smack/basic/mod_fail.rs | 1 + src/test/smack/basic/mul_fail.rs | 1 + src/test/smack/basic/sub_fail.rs | 1 + src/test/smack/functions/closure_fail.rs | 1 + src/test/smack/functions/double_fail.rs | 1 + .../smack/generics/generic_function_fail1.rs | 1 + .../smack/generics/generic_function_fail2.rs | 1 + .../smack/generics/generic_function_fail3.rs | 1 + .../smack/generics/generic_function_fail4.rs | 1 + .../smack/generics/generic_function_fail5.rs | 1 + src/test/smack/loops/gauss_sum_nondet.rs | 1 - src/test/smack/loops/gauss_sum_nondet_fail.rs | 2 +- src/test/smack/loops/iterator_fail.rs | 2 +- src/test/smack/overflow/add_overflow_fail.rs | 1 + src/test/smack/overflow/mul_overflow_fail.rs | 1 + src/test/smack/overflow/sub_overflow_fail.rs | 1 + src/test/smack/recursion/fac_fail.rs | 1 + src/test/smack/recursion/fib_fail.rs | 1 + src/test/smack/structures/option_fail.rs | 1 + src/test/smack/structures/point_fail.rs | 1 + src/test/smack/vector/vec1_fail1.rs | 1 + src/test/smack/vector/vec1_fail2.rs | 1 + src/test/smack/vector/vec1_fail3.rs | 1 + src/test/smack/vector/vec_resize_fail.rs | 1 + src/tools/compiletest/src/common.rs | 8 ++ src/tools/compiletest/src/header.rs | 35 ++++++- src/tools/compiletest/src/runtest.rs | 94 ++++++++++++++++--- 49 files changed, 192 insertions(+), 17 deletions(-) rename src/test/prusti/{Binary_search_fail.rs => Binary_search.rs} (96%) diff --git a/src/test/cbmc/BinOp_Offset/main_fail.rs b/src/test/cbmc/BinOp_Offset/main_fail.rs index 57014c62b0b1..1f58e72af644 100644 --- a/src/test/cbmc/BinOp_Offset/main_fail.rs +++ b/src/test/cbmc/BinOp_Offset/main_fail.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// rmc-verify-fail + include!("../../rmc-prelude.rs"); pub fn test_offset_in_double_array() { diff --git a/src/test/cbmc/Count/Unstable/Ctlz/bounds_fail.rs b/src/test/cbmc/Count/Unstable/Ctlz/bounds_fail.rs index deb91a6646e7..b9b665e86490 100644 --- a/src/test/cbmc/Count/Unstable/Ctlz/bounds_fail.rs +++ b/src/test/cbmc/Count/Unstable/Ctlz/bounds_fail.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail // cbmc-flags: --bounds-check #![feature(core_intrinsics)] diff --git a/src/test/cbmc/Count/Unstable/Cttz/bounds_fail.rs b/src/test/cbmc/Count/Unstable/Cttz/bounds_fail.rs index 5fa791853c05..c310fc11e177 100644 --- a/src/test/cbmc/Count/Unstable/Cttz/bounds_fail.rs +++ b/src/test/cbmc/Count/Unstable/Cttz/bounds_fail.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail // cbmc-flags: --bounds-check #![feature(core_intrinsics)] diff --git a/src/test/cbmc/DynTrait/boxed_trait_fail.rs b/src/test/cbmc/DynTrait/boxed_trait_fail.rs index b1d9de112430..ecf9a5f24f14 100644 --- a/src/test/cbmc/DynTrait/boxed_trait_fail.rs +++ b/src/test/cbmc/DynTrait/boxed_trait_fail.rs @@ -1,6 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail + // Dynamic traits should work when used through a box // _fail test; all assertions inverted. trait Shape { diff --git a/src/test/cbmc/DynTrait/different_crates_fail.rs b/src/test/cbmc/DynTrait/different_crates_fail.rs index 2a8211b4da97..a9ded2ff5881 100644 --- a/src/test/cbmc/DynTrait/different_crates_fail.rs +++ b/src/test/cbmc/DynTrait/different_crates_fail.rs @@ -1,6 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail + // This test uses a trait defined in a different crate (the standard library) // and a test defined in the local crate. The goal is to test vtable resolution // of duplicate names across different crates. diff --git a/src/test/cbmc/DynTrait/nested_boxes_fail.rs b/src/test/cbmc/DynTrait/nested_boxes_fail.rs index d3001ddb8053..29ff259e743b 100644 --- a/src/test/cbmc/DynTrait/nested_boxes_fail.rs +++ b/src/test/cbmc/DynTrait/nested_boxes_fail.rs @@ -1,6 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail + // This test checks the size and align fields for 3-deep nested trait pointers. The // outter 2 dynamic trait objects have fat pointers as their backing data. // In this failing tests, assertions are inverted to use !=. diff --git a/src/test/cbmc/FatPointers/boxmuttrait_fail.rs b/src/test/cbmc/FatPointers/boxmuttrait_fail.rs index 51a621cc56c4..3408abd6bdd9 100644 --- a/src/test/cbmc/FatPointers/boxmuttrait_fail.rs +++ b/src/test/cbmc/FatPointers/boxmuttrait_fail.rs @@ -1,6 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail + use std::io::{sink, Write}; fn main() { diff --git a/src/test/cbmc/FatPointers/boxslice2_fail.rs b/src/test/cbmc/FatPointers/boxslice2_fail.rs index 7e809e1606e9..14a216ca23b2 100644 --- a/src/test/cbmc/FatPointers/boxslice2_fail.rs +++ b/src/test/cbmc/FatPointers/boxslice2_fail.rs @@ -1,6 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail + // Casts boxed array to boxed slice (example taken from rust documentation) use std::str; diff --git a/src/test/cbmc/FatPointers/boxtrait_fail.rs b/src/test/cbmc/FatPointers/boxtrait_fail.rs index de5947149011..8951aa5ef626 100644 --- a/src/test/cbmc/FatPointers/boxtrait_fail.rs +++ b/src/test/cbmc/FatPointers/boxtrait_fail.rs @@ -1,6 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail + // This is handled by the box to box case of unsized pointers pub trait Trait { diff --git a/src/test/cbmc/FatPointers/trait1_fail.rs b/src/test/cbmc/FatPointers/trait1_fail.rs index 05fd76a2df04..c28c632e091c 100644 --- a/src/test/cbmc/FatPointers/trait1_fail.rs +++ b/src/test/cbmc/FatPointers/trait1_fail.rs @@ -1,6 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail + // Cast a concrete ref to a trait ref. pub trait Subscriber { diff --git a/src/test/cbmc/FatPointers/trait2_fail.rs b/src/test/cbmc/FatPointers/trait2_fail.rs index d7f535bc0890..aa8705f54feb 100644 --- a/src/test/cbmc/FatPointers/trait2_fail.rs +++ b/src/test/cbmc/FatPointers/trait2_fail.rs @@ -1,6 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail + // Cast a concrete ref to a trait raw pointer. pub trait Subscriber { diff --git a/src/test/cbmc/FatPointers/trait3_fail.rs b/src/test/cbmc/FatPointers/trait3_fail.rs index 04898500e7d8..620d2b4290ba 100644 --- a/src/test/cbmc/FatPointers/trait3_fail.rs +++ b/src/test/cbmc/FatPointers/trait3_fail.rs @@ -1,6 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail + // Cast a concrete ref to // concrete raw pointer // trait ref diff --git a/src/test/cbmc/Intrinsics/abort_fail.rs b/src/test/cbmc/Intrinsics/abort_fail.rs index c45a069b7a5f..153bc3321189 100644 --- a/src/test/cbmc/Intrinsics/abort_fail.rs +++ b/src/test/cbmc/Intrinsics/abort_fail.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// rmc-verify-fail + #![feature(core_intrinsics)] use std::intrinsics; fn main() { diff --git a/src/test/cbmc/PointerOffset/Unstable/main_fail.rs b/src/test/cbmc/PointerOffset/Unstable/main_fail.rs index 1579b97c1e75..672bc26cc242 100644 --- a/src/test/cbmc/PointerOffset/Unstable/main_fail.rs +++ b/src/test/cbmc/PointerOffset/Unstable/main_fail.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// rmc-verify-fail + #![feature(core_intrinsics)] use std::intrinsics::ptr_offset_from; diff --git a/src/test/cbmc/SIMD/Compare/main_fail.rs b/src/test/cbmc/SIMD/Compare/main_fail.rs index 2e45f0b6f327..02db2149b7ee 100644 --- a/src/test/cbmc/SIMD/Compare/main_fail.rs +++ b/src/test/cbmc/SIMD/Compare/main_fail.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// rmc-verify-fail + #![feature(repr_simd, platform_intrinsics)] #[repr(simd)] diff --git a/src/test/cbmc/SizeAndAlignOfDst/main_fail.rs b/src/test/cbmc/SizeAndAlignOfDst/main_fail.rs index 700a5477f3b7..1b8098dec498 100644 --- a/src/test/cbmc/SizeAndAlignOfDst/main_fail.rs +++ b/src/test/cbmc/SizeAndAlignOfDst/main_fail.rs @@ -6,6 +6,8 @@ // This test still fails with a final coercion error for // DummySubscriber to dyn Subscriber. +// rmc-verify-fail + use std::sync::Arc; use std::sync::Mutex; diff --git a/src/test/cbmc/Slice/pathbuf_fail.rs b/src/test/cbmc/Slice/pathbuf_fail.rs index 76dc80fd2a9a..a6c1ba2113ac 100644 --- a/src/test/cbmc/Slice/pathbuf_fail.rs +++ b/src/test/cbmc/Slice/pathbuf_fail.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// rmc-verify-fail + use std::fs; use std::path::PathBuf; pub fn main() { diff --git a/src/test/cbmc/Slice/slice_from_raw_fail.rs b/src/test/cbmc/Slice/slice_from_raw_fail.rs index 4d180f461ef6..7b1e3335cfb1 100644 --- a/src/test/cbmc/Slice/slice_from_raw_fail.rs +++ b/src/test/cbmc/Slice/slice_from_raw_fail.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// rmc-verify-fail + use std::slice; include!("../../rmc-prelude.rs"); diff --git a/src/test/prusti/Binary_search_fail.rs b/src/test/prusti/Binary_search.rs similarity index 96% rename from src/test/prusti/Binary_search_fail.rs rename to src/test/prusti/Binary_search.rs index 40223377b0ac..a8cd21d14ef7 100644 --- a/src/test/prusti/Binary_search_fail.rs +++ b/src/test/prusti/Binary_search.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail // cbmc-flags: --unwind 4 use std::cmp::Ordering::*; @@ -43,7 +44,7 @@ fn binary_search(arr: &[T], elem: &T) -> Option { None } -include!("../../rmc-prelude.rs"); +include!("../rmc-prelude.rs"); fn get() -> [i32; 11] { [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11] diff --git a/src/test/smack/basic/add_fail.rs b/src/test/smack/basic/add_fail.rs index a826ffbb3506..dab1e8ad1ae7 100644 --- a/src/test/smack/basic/add_fail.rs +++ b/src/test/smack/basic/add_fail.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // @expect error +// rmc-verify-fail pub fn main() { let a = 2; diff --git a/src/test/smack/basic/arith_assume_fail.rs b/src/test/smack/basic/arith_assume_fail.rs index 7277374fd299..b279588af7de 100644 --- a/src/test/smack/basic/arith_assume_fail.rs +++ b/src/test/smack/basic/arith_assume_fail.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // @expect error +// rmc-verify-fail include!("../../rmc-prelude.rs"); diff --git a/src/test/smack/basic/div_fail.rs b/src/test/smack/basic/div_fail.rs index 7a389fc0d288..4dfd34404679 100644 --- a/src/test/smack/basic/div_fail.rs +++ b/src/test/smack/basic/div_fail.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // @expect error +// rmc-verify-fail pub fn main() { let a = 2; diff --git a/src/test/smack/basic/mod_fail.rs b/src/test/smack/basic/mod_fail.rs index 6b09f95769d2..e586bc34092d 100644 --- a/src/test/smack/basic/mod_fail.rs +++ b/src/test/smack/basic/mod_fail.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // @expect error +// rmc-verify-fail pub fn main() { let a = 2; diff --git a/src/test/smack/basic/mul_fail.rs b/src/test/smack/basic/mul_fail.rs index fb1e73e40daf..1b9cbcc10ce0 100644 --- a/src/test/smack/basic/mul_fail.rs +++ b/src/test/smack/basic/mul_fail.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // @expect error +// rmc-verify-fail pub fn main() { let a = 2; diff --git a/src/test/smack/basic/sub_fail.rs b/src/test/smack/basic/sub_fail.rs index be2b46a4d82e..aa79dadd0209 100644 --- a/src/test/smack/basic/sub_fail.rs +++ b/src/test/smack/basic/sub_fail.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // @expect error +// rmc-verify-fail pub fn main() { let a = 2; diff --git a/src/test/smack/functions/closure_fail.rs b/src/test/smack/functions/closure_fail.rs index 975be573a716..e858e3c87858 100644 --- a/src/test/smack/functions/closure_fail.rs +++ b/src/test/smack/functions/closure_fail.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // @flag --no-memory-splitting // @expect verified +// rmc-verify-fail fn call_with_one(mut some_closure: F) -> () where diff --git a/src/test/smack/functions/double_fail.rs b/src/test/smack/functions/double_fail.rs index df39e066f7f7..3e3d9597d007 100644 --- a/src/test/smack/functions/double_fail.rs +++ b/src/test/smack/functions/double_fail.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // @expect error +// rmc-verify-fail fn double(a: u32) -> u32 { a * 2 diff --git a/src/test/smack/generics/generic_function_fail1.rs b/src/test/smack/generics/generic_function_fail1.rs index cc1c80489620..d97897373533 100644 --- a/src/test/smack/generics/generic_function_fail1.rs +++ b/src/test/smack/generics/generic_function_fail1.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // @expect error +// rmc-verify-fail struct Point { pub x: T, diff --git a/src/test/smack/generics/generic_function_fail2.rs b/src/test/smack/generics/generic_function_fail2.rs index b4d1cdee484d..a45f5d17a328 100644 --- a/src/test/smack/generics/generic_function_fail2.rs +++ b/src/test/smack/generics/generic_function_fail2.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // @expect error +// rmc-verify-fail struct Point { pub x: T, diff --git a/src/test/smack/generics/generic_function_fail3.rs b/src/test/smack/generics/generic_function_fail3.rs index 7156b3fd35f4..c2f7f742be1c 100644 --- a/src/test/smack/generics/generic_function_fail3.rs +++ b/src/test/smack/generics/generic_function_fail3.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // @expect error +// rmc-verify-fail struct Point { pub x: T, diff --git a/src/test/smack/generics/generic_function_fail4.rs b/src/test/smack/generics/generic_function_fail4.rs index ae3dfeb72cd6..52f4f5d3b4fd 100644 --- a/src/test/smack/generics/generic_function_fail4.rs +++ b/src/test/smack/generics/generic_function_fail4.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // @expect verified +// rmc-verify-fail struct Point { pub x: T, diff --git a/src/test/smack/generics/generic_function_fail5.rs b/src/test/smack/generics/generic_function_fail5.rs index 2cac16cda9af..1f9369510df5 100644 --- a/src/test/smack/generics/generic_function_fail5.rs +++ b/src/test/smack/generics/generic_function_fail5.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // @expect verified +// rmc-verify-fail struct Point { pub x: T, diff --git a/src/test/smack/loops/gauss_sum_nondet.rs b/src/test/smack/loops/gauss_sum_nondet.rs index 33c70312017f..6f57722d8ea0 100644 --- a/src/test/smack/loops/gauss_sum_nondet.rs +++ b/src/test/smack/loops/gauss_sum_nondet.rs @@ -2,7 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // @flag --no-memory-splitting --unroll=4 // @expect verified - // cbmc-flags: --unwind 5 include!("../../rmc-prelude.rs"); diff --git a/src/test/smack/loops/gauss_sum_nondet_fail.rs b/src/test/smack/loops/gauss_sum_nondet_fail.rs index d29f31dc2d50..43045d2f1566 100644 --- a/src/test/smack/loops/gauss_sum_nondet_fail.rs +++ b/src/test/smack/loops/gauss_sum_nondet_fail.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // @flag --no-memory-splitting --unroll=10 // @expect error - +// rmc-verify-fail // cbmc-flags: --unwind 5 include!("../../rmc-prelude.rs"); diff --git a/src/test/smack/loops/iterator_fail.rs b/src/test/smack/loops/iterator_fail.rs index 72fca0cf5134..4a5b537d8582 100644 --- a/src/test/smack/loops/iterator_fail.rs +++ b/src/test/smack/loops/iterator_fail.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // @flag --no-memory-splitting --unroll=10 // @expect error - +// rmc-verify-fail // cbmc-flags: --unwind 5 fn fac(n: u64) -> u64 { diff --git a/src/test/smack/overflow/add_overflow_fail.rs b/src/test/smack/overflow/add_overflow_fail.rs index 3ba735e6c281..e9f8d3f5774c 100644 --- a/src/test/smack/overflow/add_overflow_fail.rs +++ b/src/test/smack/overflow/add_overflow_fail.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // @flag --integer-overflow // @expect overflow +// rmc-verify-fail pub fn get128() -> u8 { 128 diff --git a/src/test/smack/overflow/mul_overflow_fail.rs b/src/test/smack/overflow/mul_overflow_fail.rs index 7fc95268c842..a89509d7e611 100644 --- a/src/test/smack/overflow/mul_overflow_fail.rs +++ b/src/test/smack/overflow/mul_overflow_fail.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // @flag --integer-overflow // @expect overflow +// rmc-verify-fail fn get128() -> u8 { 128 diff --git a/src/test/smack/overflow/sub_overflow_fail.rs b/src/test/smack/overflow/sub_overflow_fail.rs index 557968972608..fce508a36ab6 100644 --- a/src/test/smack/overflow/sub_overflow_fail.rs +++ b/src/test/smack/overflow/sub_overflow_fail.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // @flag --integer-overflow // @expect overflow +// rmc-verify-fail fn get128() -> u8 { 128 diff --git a/src/test/smack/recursion/fac_fail.rs b/src/test/smack/recursion/fac_fail.rs index 8da67d48ed9e..47ab6439cfbc 100644 --- a/src/test/smack/recursion/fac_fail.rs +++ b/src/test/smack/recursion/fac_fail.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // @flag --unroll=10 // @expect error +// rmc-verify-fail fn fac(n: u64, acc: u64) -> u64 { match n { diff --git a/src/test/smack/recursion/fib_fail.rs b/src/test/smack/recursion/fib_fail.rs index 14cba9bb9ee4..537203831b4a 100644 --- a/src/test/smack/recursion/fib_fail.rs +++ b/src/test/smack/recursion/fib_fail.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // @flag --unroll=10 // @expect error +// rmc-verify-fail fn fib(x: u64) -> u64 { match x { diff --git a/src/test/smack/structures/option_fail.rs b/src/test/smack/structures/option_fail.rs index 5e2bfe77348f..70a835f62f07 100644 --- a/src/test/smack/structures/option_fail.rs +++ b/src/test/smack/structures/option_fail.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // @expect reachable +// rmc-verify-fail fn safe_div(x: u32, y: u32) -> Option { if y != 0 { Some(x / y) } else { None } diff --git a/src/test/smack/structures/point_fail.rs b/src/test/smack/structures/point_fail.rs index 4361f98bcbb7..8d6895a9b0c7 100644 --- a/src/test/smack/structures/point_fail.rs +++ b/src/test/smack/structures/point_fail.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // @expect error +// rmc-verify-fail use std::ops::{Add, AddAssign}; diff --git a/src/test/smack/vector/vec1_fail1.rs b/src/test/smack/vector/vec1_fail1.rs index bf164d34d4ca..858c17a1a08c 100644 --- a/src/test/smack/vector/vec1_fail1.rs +++ b/src/test/smack/vector/vec1_fail1.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // @flag --no-memory-splitting // @expect error +// rmc-verify-fail pub fn main() { let mut v: Vec = Vec::new(); diff --git a/src/test/smack/vector/vec1_fail2.rs b/src/test/smack/vector/vec1_fail2.rs index dd7b910164d4..4c5d8ce96614 100644 --- a/src/test/smack/vector/vec1_fail2.rs +++ b/src/test/smack/vector/vec1_fail2.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // @flag --no-memory-splitting // @expect error +// rmc-verify-fail pub fn main() { let mut v: Vec = Vec::new(); diff --git a/src/test/smack/vector/vec1_fail3.rs b/src/test/smack/vector/vec1_fail3.rs index 7843d004179d..0ce12dcfcae4 100644 --- a/src/test/smack/vector/vec1_fail3.rs +++ b/src/test/smack/vector/vec1_fail3.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // @flag --no-memory-splitting // @expect error +// rmc-verify-fail pub fn main() { let mut v: Vec = Vec::new(); diff --git a/src/test/smack/vector/vec_resize_fail.rs b/src/test/smack/vector/vec_resize_fail.rs index 07377c1a5973..ca7ae526ee66 100644 --- a/src/test/smack/vector/vec_resize_fail.rs +++ b/src/test/smack/vector/vec_resize_fail.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // @flag --no-memory-splitting --unroll=3 // @expect error +// rmc-verify-fail pub fn main() { let mut v1: Vec = vec![0]; diff --git a/src/tools/compiletest/src/common.rs b/src/tools/compiletest/src/common.rs index 0108b66f05b8..f38ebd4fc36b 100644 --- a/src/tools/compiletest/src/common.rs +++ b/src/tools/compiletest/src/common.rs @@ -118,6 +118,14 @@ impl fmt::Display for PassMode { } } +/// Stage where an RMC test should fail. +#[derive(Copy, Clone, Debug, PartialEq, PartialOrd)] +pub enum RMCFailMode { + Check, + Codegen, + Verify, +} + #[derive(Copy, Clone, Debug, PartialEq, PartialOrd)] pub enum FailMode { Check, diff --git a/src/tools/compiletest/src/header.rs b/src/tools/compiletest/src/header.rs index 40c13a7b4144..073577110d68 100644 --- a/src/tools/compiletest/src/header.rs +++ b/src/tools/compiletest/src/header.rs @@ -7,7 +7,9 @@ use std::path::{Path, PathBuf}; use tracing::*; -use crate::common::{CompareMode, Config, Debugger, FailMode, Mode, PanicStrategy, PassMode}; +use crate::common::{ + CompareMode, Config, Debugger, FailMode, Mode, PanicStrategy, PassMode, RMCFailMode, +}; use crate::util; use crate::{extract_cdb_version, extract_gdb_version}; @@ -121,6 +123,8 @@ pub struct TestProps { pass_mode: Option, // Ignore `--pass` overrides from the command line for this test. ignore_pass: bool, + // How far this RMC test should proceed to start failing. + pub rmc_fail_mode: Option, // How far this test should proceed to start failing. pub fail_mode: Option, // rustdoc will test the output of the `--test` option @@ -170,6 +174,7 @@ impl TestProps { forbid_output: vec![], incremental_dir: None, pass_mode: None, + rmc_fail_mode: None, fail_mode: None, ignore_pass: false, check_test_line_numbers_match: false, @@ -331,6 +336,7 @@ impl TestProps { } self.update_pass_mode(ln, cfg, config); + self.update_rmc_fail_mode(ln, config); self.update_fail_mode(ln, config); if !self.ignore_pass { @@ -383,6 +389,33 @@ impl TestProps { } } + /// Checks if `ln` specifies which stage the test should fail on and updates + /// RMC fail mode accordingly. + fn update_rmc_fail_mode(&mut self, ln: &str, config: &Config) { + let check_rmc = |mode: &str| { + if config.mode != Mode::RMC { + panic!("`rmc-{}-fail` header is only supported in RMC tests", mode); + } + }; + let rmc_fail_mode = if config.parse_name_directive(ln, "rmc-check-fail") { + check_rmc("check"); + Some(RMCFailMode::Check) + } else if config.parse_name_directive(ln, "rmc-codegen-fail") { + check_rmc("codegen"); + Some(RMCFailMode::Codegen) + } else if config.parse_name_directive(ln, "rmc-verify-fail") { + check_rmc("verify"); + Some(RMCFailMode::Verify) + } else { + None + }; + match (self.rmc_fail_mode, rmc_fail_mode) { + (None, Some(_)) => self.rmc_fail_mode = rmc_fail_mode, + (Some(_), Some(_)) => panic!("multiple `rmc-*-fail` headers in a single test"), + (_, None) => {} + } + } + fn update_fail_mode(&mut self, ln: &str, config: &Config) { let check_ui = |mode: &str| { if config.mode != Mode::Ui { diff --git a/src/tools/compiletest/src/runtest.rs b/src/tools/compiletest/src/runtest.rs index 9635f0929cbe..e63a44146fd7 100644 --- a/src/tools/compiletest/src/runtest.rs +++ b/src/tools/compiletest/src/runtest.rs @@ -1,6 +1,8 @@ // ignore-tidy-filelength -use crate::common::{expected_output_path, UI_EXTENSIONS, UI_FIXED, UI_STDERR, UI_STDOUT}; +use crate::common::{ + expected_output_path, RMCFailMode, UI_EXTENSIONS, UI_FIXED, UI_STDERR, UI_STDOUT, +}; use crate::common::{output_base_dir, output_base_name, output_testname_unique}; use crate::common::{ Assembly, CargoRMC, Expected, Incremental, JsDocTest, MirOpt, RunMake, RustdocJson, Ui, RMC, @@ -400,7 +402,6 @@ impl<'test> TestCx<'test> { panic!("revision name must begin with rpass, rfail, or cfail"); } } - RMC => !self.testpaths.file.to_str().unwrap().contains("fail"), mode => panic!("unimplemented for mode {:?}", mode), } } @@ -2392,20 +2393,68 @@ impl<'test> TestCx<'test> { } /// Adds rmc scripts directory to the `PATH` environment variable. - fn add_rmc_dir_to_path(&self, rmc: &mut Command) { + fn add_rmc_dir_to_path(&self, command: &mut Command) { // If the PATH enviornment variable is already defined, if let Some((key, val)) = env::vars().find(|(key, _)| key == "PATH") { // Add the RMC scripts directory to the PATH. - rmc.env(key, format!("{}:{}", self.config.rmc_dir_path.to_str().unwrap(), val)); + command.env(key, format!("{}:{}", self.config.rmc_dir_path.to_str().unwrap(), val)); } else { // Otherwise, insert PATH as a new enviornment variable and set its value to the RMC scripts directory. - rmc.env(String::from("PATH"), String::from(self.config.rmc_dir_path.to_str().unwrap())); + command.env( + String::from("PATH"), + String::from(self.config.rmc_dir_path.to_str().unwrap()), + ); + } + } + + /// Runs `rustc` on the test file specified by `self.testpaths.file`. An + /// error message is printed to stdout if the check result is not expected. + fn check(&self) { + let mut rustc = Command::new("rmc-rustc"); + rustc.args(["-Z", "no-codegen"]).arg(&self.testpaths.file); + self.add_rmc_dir_to_path(&mut rustc); + let proc_res = self.compose_and_run_compiler(rustc, None); + if self.props.rmc_fail_mode == Some(RMCFailMode::Check) { + if proc_res.status.success() { + self.fatal_proc_rec("test failed: expected check failure, got success", &proc_res); + } + } else { + if !proc_res.status.success() { + self.fatal_proc_rec("test failed: expected check success, got failure", &proc_res); + } + } + } + + /// Runs `rustc` on the test file specified by `self.testpaths.file`. An + /// error message is printed to stdout if the codgen result is not expected. + fn codgen(&self) { + let mut rustc = Command::new("rmc-rustc"); + rustc + .args(["-Z", "codegen-backend=gotoc", "--cfg=rmc", "--out-dir"]) + .arg(self.output_base_dir()) + .arg(&self.testpaths.file); + self.add_rmc_dir_to_path(&mut rustc); + let proc_res = self.compose_and_run_compiler(rustc, None); + if self.props.rmc_fail_mode == Some(RMCFailMode::Codegen) { + if proc_res.status.success() { + self.fatal_proc_rec( + "test failed: expected codegen failure, got success", + &proc_res, + ); + } + } else { + if !proc_res.status.success() { + self.fatal_proc_rec( + "test failed: expected codegen success, got failure", + &proc_res, + ); + } } } /// Runs RMC on the test file specified by `self.testpaths.file`. An error - /// message is printed to stdout if verification result is not expected. - fn run_rmc_test(&self) { + /// message is printed to stdout if the verification result is not expected. + fn verify(&self) { // Other modes call self.compile_test(...). However, we cannot call it here for two reasons: // 1. It calls rustc instead of RMC // 2. It may pass some options that do not make sense for RMC @@ -2443,18 +2492,39 @@ impl<'test> TestCx<'test> { ) } // Print an error if the verification result is not expected. - if self.should_compile_successfully(self.pass_mode()) { - if !proc_res.status.success() { - self.fatal_proc_rec("test failed: expected success, got failure", &proc_res); + if self.props.rmc_fail_mode == Some(RMCFailMode::Verify) { + if proc_res.status.success() { + self.fatal_proc_rec( + "test failed: expected verification failure, got success", + &proc_res, + ); } } else { - if proc_res.status.success() { - self.fatal_proc_rec("test failed: expected failure, got success", &proc_res); + if !proc_res.status.success() { + self.fatal_proc_rec( + "test failed: expected verification success, got failure", + &proc_res, + ); } } } } + /// Checks, codgens, and verifies the test file specified by + /// `self.testpaths.file`. An error message is printed to stdout if a result + /// is not expected. + fn run_rmc_test(&self) { + self.check(); + if self.props.rmc_fail_mode == Some(RMCFailMode::Check) { + return; + } + self.codgen(); + if self.props.rmc_fail_mode == Some(RMCFailMode::Codegen) { + return; + } + self.verify(); + } + /// If the test file contains expected failures in some locations, ensure /// that verification does not succeed in those locations. fn verify_expect_fail(str: &str) -> Vec { From 921ba68132482d373b7b98def9fad2bb7e95c5e0 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed Date: Thu, 22 Jul 2021 12:35:02 +0000 Subject: [PATCH 2/5] Fix typo. --- src/tools/compiletest/src/runtest.rs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/tools/compiletest/src/runtest.rs b/src/tools/compiletest/src/runtest.rs index e63a44146fd7..a21eec8db9b8 100644 --- a/src/tools/compiletest/src/runtest.rs +++ b/src/tools/compiletest/src/runtest.rs @@ -2426,8 +2426,9 @@ impl<'test> TestCx<'test> { } /// Runs `rustc` on the test file specified by `self.testpaths.file`. An - /// error message is printed to stdout if the codgen result is not expected. - fn codgen(&self) { + /// error message is printed to stdout if the codegen result is not + /// expected. + fn codegen(&self) { let mut rustc = Command::new("rmc-rustc"); rustc .args(["-Z", "codegen-backend=gotoc", "--cfg=rmc", "--out-dir"]) @@ -2518,7 +2519,7 @@ impl<'test> TestCx<'test> { if self.props.rmc_fail_mode == Some(RMCFailMode::Check) { return; } - self.codgen(); + self.codegen(); if self.props.rmc_fail_mode == Some(RMCFailMode::Codegen) { return; } From 82006a4bc4a690cfe39769b8b573e1549a4d3b17 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed Date: Thu, 22 Jul 2021 14:30:00 +0000 Subject: [PATCH 3/5] Rename tests. --- .../{fixme_main_fail.rs => fixme_main.rs} | 2 ++ .../{fixme_main_fail.rs => fixme_main.rs} | 2 ++ src/test/cbmc/BinOp_Offset/main_fail.rs | 1 - .../{fixme_main_fail.rs => fixme_main.rs} | 2 ++ .../{fixme_main_fail.rs => fixme_main.rs} | 2 ++ .../Ctlz/{bounds_fail.rs => bounds.rs} | 1 - .../Cttz/{bounds_fail.rs => bounds.rs} | 1 - .../cbmc/DynTrait/boxed_closure_fail_fixme.rs | 3 ++- src/test/cbmc/DynTrait/boxed_trait_fail.rs | 1 - .../cbmc/DynTrait/different_crates_fail.rs | 1 - src/test/cbmc/DynTrait/nested_boxes_fail.rs | 1 - src/test/cbmc/FatPointers/boxmuttrait_fail.rs | 1 - src/test/cbmc/FatPointers/boxslice1.rs | 2 +- .../{boxslice2_fail.rs => boxslice2.rs} | 1 - src/test/cbmc/FatPointers/boxtrait_fail.rs | 1 - src/test/cbmc/FatPointers/trait1_fail.rs | 1 - src/test/cbmc/FatPointers/trait2_fail.rs | 1 - src/test/cbmc/FatPointers/trait3_fail.rs | 1 - .../Intrinsics/{abort_fail.rs => abort.rs} | 1 - .../cbmc/PointerOffset/Unstable/main_fail.rs | 1 - ...xme_from_raw_fail.rs => fixme_from_raw.rs} | 1 + .../{fixme_main_fail.rs => fixme_main.rs} | 2 ++ .../SIMD/Compare/{main_fail.rs => main.rs} | 1 - src/test/cbmc/SIMD/mem/volatile.rs | 21 +++++++++++++++++++ src/test/cbmc/Serde/{main_fail.rs => main.rs} | 2 ++ src/test/cbmc/SizeAndAlignOfDst/main_fail.rs | 1 - ...drop_in_place_fail.rs => drop_in_place.rs} | 2 ++ .../Slice/{pathbuf_fail.rs => pathbuf.rs} | 1 - ...ice_from_raw_fail.rs => slice_from_raw.rs} | 1 - src/test/prusti/Binary_search.rs | 1 - src/test/smack/basic/{add_fail.rs => add.rs} | 0 ...{arith_assume_fail.rs => arith_assume3.rs} | 0 src/test/smack/basic/{div_fail.rs => div.rs} | 0 src/test/smack/basic/{mod_fail.rs => mod.rs} | 0 src/test/smack/basic/{mul_fail.rs => mul.rs} | 0 src/test/smack/basic/{sub_fail.rs => sub.rs} | 0 ...function_fail1.rs => generic_function1.rs} | 0 ...function_fail2.rs => generic_function2.rs} | 0 ...function_fail3.rs => generic_function3.rs} | 0 ...function_fail4.rs => generic_function4.rs} | 0 ...function_fail5.rs => generic_function5.rs} | 0 .../{add_overflow_fail.rs => add_overflow.rs} | 0 .../{mul_overflow_fail.rs => mul_overflow.rs} | 0 .../{sub_overflow_fail.rs => sub_overflow.rs} | 0 .../smack/vector/{vec1_fail1.rs => vec11.rs} | 0 .../smack/vector/{vec1_fail2.rs => vec12.rs} | 0 .../smack/vector/{vec1_fail3.rs => vec13.rs} | 0 src/tools/compiletest/src/runtest.rs | 2 +- 48 files changed, 40 insertions(+), 22 deletions(-) rename src/test/cbmc/Assert/UninitValid/{fixme_main_fail.rs => fixme_main.rs} (97%) rename src/test/cbmc/Assert/ZeroValid/{fixme_main_fail.rs => fixme_main.rs} (96%) rename src/test/cbmc/BitManipulation/Stable/{fixme_main_fail.rs => fixme_main.rs} (97%) rename src/test/cbmc/BitManipulation/Unstable/{fixme_main_fail.rs => fixme_main.rs} (97%) rename src/test/cbmc/Count/Unstable/Ctlz/{bounds_fail.rs => bounds.rs} (99%) rename src/test/cbmc/Count/Unstable/Cttz/{bounds_fail.rs => bounds.rs} (99%) rename src/test/cbmc/FatPointers/{boxslice2_fail.rs => boxslice2.rs} (99%) rename src/test/cbmc/Intrinsics/{abort_fail.rs => abort.rs} (99%) rename src/test/cbmc/Pointers_Basic/{fixme_from_raw_fail.rs => fixme_from_raw.rs} (95%) rename src/test/cbmc/Pointers_OutOfScopeFail/{fixme_main_fail.rs => fixme_main.rs} (96%) rename src/test/cbmc/SIMD/Compare/{main_fail.rs => main.rs} (99%) create mode 100644 src/test/cbmc/SIMD/mem/volatile.rs rename src/test/cbmc/Serde/{main_fail.rs => main.rs} (96%) rename src/test/cbmc/Slice/{drop_in_place_fail.rs => drop_in_place.rs} (95%) rename src/test/cbmc/Slice/{pathbuf_fail.rs => pathbuf.rs} (99%) rename src/test/cbmc/Slice/{slice_from_raw_fail.rs => slice_from_raw.rs} (99%) rename src/test/smack/basic/{add_fail.rs => add.rs} (100%) rename src/test/smack/basic/{arith_assume_fail.rs => arith_assume3.rs} (100%) rename src/test/smack/basic/{div_fail.rs => div.rs} (100%) rename src/test/smack/basic/{mod_fail.rs => mod.rs} (100%) rename src/test/smack/basic/{mul_fail.rs => mul.rs} (100%) rename src/test/smack/basic/{sub_fail.rs => sub.rs} (100%) rename src/test/smack/generics/{generic_function_fail1.rs => generic_function1.rs} (100%) rename src/test/smack/generics/{generic_function_fail2.rs => generic_function2.rs} (100%) rename src/test/smack/generics/{generic_function_fail3.rs => generic_function3.rs} (100%) rename src/test/smack/generics/{generic_function_fail4.rs => generic_function4.rs} (100%) rename src/test/smack/generics/{generic_function_fail5.rs => generic_function5.rs} (100%) rename src/test/smack/overflow/{add_overflow_fail.rs => add_overflow.rs} (100%) rename src/test/smack/overflow/{mul_overflow_fail.rs => mul_overflow.rs} (100%) rename src/test/smack/overflow/{sub_overflow_fail.rs => sub_overflow.rs} (100%) rename src/test/smack/vector/{vec1_fail1.rs => vec11.rs} (100%) rename src/test/smack/vector/{vec1_fail2.rs => vec12.rs} (100%) rename src/test/smack/vector/{vec1_fail3.rs => vec13.rs} (100%) diff --git a/src/test/cbmc/Assert/UninitValid/fixme_main_fail.rs b/src/test/cbmc/Assert/UninitValid/fixme_main.rs similarity index 97% rename from src/test/cbmc/Assert/UninitValid/fixme_main_fail.rs rename to src/test/cbmc/Assert/UninitValid/fixme_main.rs index 38541c2d355b..06c24dee9d53 100644 --- a/src/test/cbmc/Assert/UninitValid/fixme_main_fail.rs +++ b/src/test/cbmc/Assert/UninitValid/fixme_main.rs @@ -1,5 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail + use std::mem::{self, MaybeUninit}; fn main() { diff --git a/src/test/cbmc/Assert/ZeroValid/fixme_main_fail.rs b/src/test/cbmc/Assert/ZeroValid/fixme_main.rs similarity index 96% rename from src/test/cbmc/Assert/ZeroValid/fixme_main_fail.rs rename to src/test/cbmc/Assert/ZeroValid/fixme_main.rs index 435cfd18f1a7..805173c08f7d 100644 --- a/src/test/cbmc/Assert/ZeroValid/fixme_main_fail.rs +++ b/src/test/cbmc/Assert/ZeroValid/fixme_main.rs @@ -1,5 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail + // The function zeroed() calls assert_zero_valid to mark that it is only defined to assign an // all-zero bit pattern to a type T if this is a valid value. So the following is undefined. diff --git a/src/test/cbmc/BinOp_Offset/main_fail.rs b/src/test/cbmc/BinOp_Offset/main_fail.rs index 1f58e72af644..49d4c3ea20aa 100644 --- a/src/test/cbmc/BinOp_Offset/main_fail.rs +++ b/src/test/cbmc/BinOp_Offset/main_fail.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail include!("../../rmc-prelude.rs"); diff --git a/src/test/cbmc/BitManipulation/Stable/fixme_main_fail.rs b/src/test/cbmc/BitManipulation/Stable/fixme_main.rs similarity index 97% rename from src/test/cbmc/BitManipulation/Stable/fixme_main_fail.rs rename to src/test/cbmc/BitManipulation/Stable/fixme_main.rs index c1a9bee0a280..928572cc1c2c 100644 --- a/src/test/cbmc/BitManipulation/Stable/fixme_main_fail.rs +++ b/src/test/cbmc/BitManipulation/Stable/fixme_main.rs @@ -1,5 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail + fn main() { // Intrinsics implemented as integer primitives // https://doc.rust-lang.org/core/intrinsics/fn.cttz.html diff --git a/src/test/cbmc/BitManipulation/Unstable/fixme_main_fail.rs b/src/test/cbmc/BitManipulation/Unstable/fixme_main.rs similarity index 97% rename from src/test/cbmc/BitManipulation/Unstable/fixme_main_fail.rs rename to src/test/cbmc/BitManipulation/Unstable/fixme_main.rs index 75e6331cea21..b892b70121e0 100644 --- a/src/test/cbmc/BitManipulation/Unstable/fixme_main_fail.rs +++ b/src/test/cbmc/BitManipulation/Unstable/fixme_main.rs @@ -1,5 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail + #![feature(core_intrinsics)] use std::intrinsics::{ctlz, cttz, cttz_nonzero}; diff --git a/src/test/cbmc/Count/Unstable/Ctlz/bounds_fail.rs b/src/test/cbmc/Count/Unstable/Ctlz/bounds.rs similarity index 99% rename from src/test/cbmc/Count/Unstable/Ctlz/bounds_fail.rs rename to src/test/cbmc/Count/Unstable/Ctlz/bounds.rs index b9b665e86490..7db52aa63ab6 100644 --- a/src/test/cbmc/Count/Unstable/Ctlz/bounds_fail.rs +++ b/src/test/cbmc/Count/Unstable/Ctlz/bounds.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail // cbmc-flags: --bounds-check diff --git a/src/test/cbmc/Count/Unstable/Cttz/bounds_fail.rs b/src/test/cbmc/Count/Unstable/Cttz/bounds.rs similarity index 99% rename from src/test/cbmc/Count/Unstable/Cttz/bounds_fail.rs rename to src/test/cbmc/Count/Unstable/Cttz/bounds.rs index c310fc11e177..0327087efa1a 100644 --- a/src/test/cbmc/Count/Unstable/Cttz/bounds_fail.rs +++ b/src/test/cbmc/Count/Unstable/Cttz/bounds.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail // cbmc-flags: --bounds-check diff --git a/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs b/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs index c3a7f2cf90ef..54d8523b6945 100644 --- a/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs +++ b/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs @@ -1,10 +1,11 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail // Check that we can codegen a boxed dyn closure and fail an inner assertion // This current verifies "successfully" because the closure is not actually -// called in the resulting CotoC code. +// called in the resulting GotoC code. // https://github.com/model-checking/rmc/issues/240 include!("../../rmc-prelude.rs"); diff --git a/src/test/cbmc/DynTrait/boxed_trait_fail.rs b/src/test/cbmc/DynTrait/boxed_trait_fail.rs index ecf9a5f24f14..9e690ef063eb 100644 --- a/src/test/cbmc/DynTrait/boxed_trait_fail.rs +++ b/src/test/cbmc/DynTrait/boxed_trait_fail.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail // Dynamic traits should work when used through a box diff --git a/src/test/cbmc/DynTrait/different_crates_fail.rs b/src/test/cbmc/DynTrait/different_crates_fail.rs index a9ded2ff5881..3b7c47fe2338 100644 --- a/src/test/cbmc/DynTrait/different_crates_fail.rs +++ b/src/test/cbmc/DynTrait/different_crates_fail.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail // This test uses a trait defined in a different crate (the standard library) diff --git a/src/test/cbmc/DynTrait/nested_boxes_fail.rs b/src/test/cbmc/DynTrait/nested_boxes_fail.rs index 29ff259e743b..fd6a6332a35f 100644 --- a/src/test/cbmc/DynTrait/nested_boxes_fail.rs +++ b/src/test/cbmc/DynTrait/nested_boxes_fail.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail // This test checks the size and align fields for 3-deep nested trait pointers. The diff --git a/src/test/cbmc/FatPointers/boxmuttrait_fail.rs b/src/test/cbmc/FatPointers/boxmuttrait_fail.rs index 3408abd6bdd9..63233d093455 100644 --- a/src/test/cbmc/FatPointers/boxmuttrait_fail.rs +++ b/src/test/cbmc/FatPointers/boxmuttrait_fail.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail use std::io::{sink, Write}; diff --git a/src/test/cbmc/FatPointers/boxslice1.rs b/src/test/cbmc/FatPointers/boxslice1.rs index eaca29c49e01..91e29de5ceaf 100644 --- a/src/test/cbmc/FatPointers/boxslice1.rs +++ b/src/test/cbmc/FatPointers/boxslice1.rs @@ -11,5 +11,5 @@ fn main() { // This transformer produces a Box<[u8]> let _sparkle_heart_str = str::from_utf8(&sparkle_heart_vec); - // see boxslice2_fail.rs for an attempt to test sparkle_heart_str + // see boxslice2.rs for an attempt to test sparkle_heart_str } diff --git a/src/test/cbmc/FatPointers/boxslice2_fail.rs b/src/test/cbmc/FatPointers/boxslice2.rs similarity index 99% rename from src/test/cbmc/FatPointers/boxslice2_fail.rs rename to src/test/cbmc/FatPointers/boxslice2.rs index 14a216ca23b2..c5c103e36213 100644 --- a/src/test/cbmc/FatPointers/boxslice2_fail.rs +++ b/src/test/cbmc/FatPointers/boxslice2.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail // Casts boxed array to boxed slice (example taken from rust documentation) diff --git a/src/test/cbmc/FatPointers/boxtrait_fail.rs b/src/test/cbmc/FatPointers/boxtrait_fail.rs index 8951aa5ef626..05d650bb8bc3 100644 --- a/src/test/cbmc/FatPointers/boxtrait_fail.rs +++ b/src/test/cbmc/FatPointers/boxtrait_fail.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail // This is handled by the box to box case of unsized pointers diff --git a/src/test/cbmc/FatPointers/trait1_fail.rs b/src/test/cbmc/FatPointers/trait1_fail.rs index c28c632e091c..1cb23c38f0c4 100644 --- a/src/test/cbmc/FatPointers/trait1_fail.rs +++ b/src/test/cbmc/FatPointers/trait1_fail.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail // Cast a concrete ref to a trait ref. diff --git a/src/test/cbmc/FatPointers/trait2_fail.rs b/src/test/cbmc/FatPointers/trait2_fail.rs index aa8705f54feb..50de1a127e0a 100644 --- a/src/test/cbmc/FatPointers/trait2_fail.rs +++ b/src/test/cbmc/FatPointers/trait2_fail.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail // Cast a concrete ref to a trait raw pointer. diff --git a/src/test/cbmc/FatPointers/trait3_fail.rs b/src/test/cbmc/FatPointers/trait3_fail.rs index 620d2b4290ba..5a1fca792443 100644 --- a/src/test/cbmc/FatPointers/trait3_fail.rs +++ b/src/test/cbmc/FatPointers/trait3_fail.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail // Cast a concrete ref to diff --git a/src/test/cbmc/Intrinsics/abort_fail.rs b/src/test/cbmc/Intrinsics/abort.rs similarity index 99% rename from src/test/cbmc/Intrinsics/abort_fail.rs rename to src/test/cbmc/Intrinsics/abort.rs index 153bc3321189..fc445524774d 100644 --- a/src/test/cbmc/Intrinsics/abort_fail.rs +++ b/src/test/cbmc/Intrinsics/abort.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail #![feature(core_intrinsics)] diff --git a/src/test/cbmc/PointerOffset/Unstable/main_fail.rs b/src/test/cbmc/PointerOffset/Unstable/main_fail.rs index 672bc26cc242..a7ced6f3510b 100644 --- a/src/test/cbmc/PointerOffset/Unstable/main_fail.rs +++ b/src/test/cbmc/PointerOffset/Unstable/main_fail.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail #![feature(core_intrinsics)] diff --git a/src/test/cbmc/Pointers_Basic/fixme_from_raw_fail.rs b/src/test/cbmc/Pointers_Basic/fixme_from_raw.rs similarity index 95% rename from src/test/cbmc/Pointers_Basic/fixme_from_raw_fail.rs rename to src/test/cbmc/Pointers_Basic/fixme_from_raw.rs index b3a25e21e58f..ea8d8c3271ca 100644 --- a/src/test/cbmc/Pointers_Basic/fixme_from_raw_fail.rs +++ b/src/test/cbmc/Pointers_Basic/fixme_from_raw.rs @@ -1,5 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail fn main() { let address = 0x01234usize; diff --git a/src/test/cbmc/Pointers_OutOfScopeFail/fixme_main_fail.rs b/src/test/cbmc/Pointers_OutOfScopeFail/fixme_main.rs similarity index 96% rename from src/test/cbmc/Pointers_OutOfScopeFail/fixme_main_fail.rs rename to src/test/cbmc/Pointers_OutOfScopeFail/fixme_main.rs index 43c97aef82bd..744213ee8767 100644 --- a/src/test/cbmc/Pointers_OutOfScopeFail/fixme_main_fail.rs +++ b/src/test/cbmc/Pointers_OutOfScopeFail/fixme_main.rs @@ -1,5 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-verify-fail + fn main() { // declare pointer to integer let p_subscoped: *const u32; diff --git a/src/test/cbmc/SIMD/Compare/main_fail.rs b/src/test/cbmc/SIMD/Compare/main.rs similarity index 99% rename from src/test/cbmc/SIMD/Compare/main_fail.rs rename to src/test/cbmc/SIMD/Compare/main.rs index 02db2149b7ee..adfd84cc1376 100644 --- a/src/test/cbmc/SIMD/Compare/main_fail.rs +++ b/src/test/cbmc/SIMD/Compare/main.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail #![feature(repr_simd, platform_intrinsics)] diff --git a/src/test/cbmc/SIMD/mem/volatile.rs b/src/test/cbmc/SIMD/mem/volatile.rs new file mode 100644 index 000000000000..31f019a03b37 --- /dev/null +++ b/src/test/cbmc/SIMD/mem/volatile.rs @@ -0,0 +1,21 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-codegen-fail + +#![feature(core_intrinsics)] + +use std::intrinsics::*; + +pub fn main() { + let mut a: Box = Box::new(0); + unsafe { + let x = volatile_load(&*a); + assert!(x == *a); + volatile_store(&mut *a, 1); + assert!(*a == 1); + unaligned_volatile_store(&mut *a, 2); + assert!(*a == 2); + volatile_set_memory(&mut *a, 3, 1); + assert!(*a == 3); + } +} diff --git a/src/test/cbmc/Serde/main_fail.rs b/src/test/cbmc/Serde/main.rs similarity index 96% rename from src/test/cbmc/Serde/main_fail.rs rename to src/test/cbmc/Serde/main.rs index 688f430ae39d..acd38b53b2e7 100644 --- a/src/test/cbmc/Serde/main_fail.rs +++ b/src/test/cbmc/Serde/main.rs @@ -1,5 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-check-fail + // We currently assert(false) for reify function pointer. // So this codegens but fails model checking. diff --git a/src/test/cbmc/SizeAndAlignOfDst/main_fail.rs b/src/test/cbmc/SizeAndAlignOfDst/main_fail.rs index 1b8098dec498..2fffc98fc27f 100644 --- a/src/test/cbmc/SizeAndAlignOfDst/main_fail.rs +++ b/src/test/cbmc/SizeAndAlignOfDst/main_fail.rs @@ -5,7 +5,6 @@ // Arc>. // This test still fails with a final coercion error for // DummySubscriber to dyn Subscriber. - // rmc-verify-fail use std::sync::Arc; diff --git a/src/test/cbmc/Slice/drop_in_place_fail.rs b/src/test/cbmc/Slice/drop_in_place.rs similarity index 95% rename from src/test/cbmc/Slice/drop_in_place_fail.rs rename to src/test/cbmc/Slice/drop_in_place.rs index 6157653dcd6f..d02a9c473b0f 100644 --- a/src/test/cbmc/Slice/drop_in_place_fail.rs +++ b/src/test/cbmc/Slice/drop_in_place.rs @@ -1,5 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +// rmc-check-fail + #[allow(unconditional_recursion)] pub unsafe fn drop_in_place(to_drop: *mut T) { // Code here does not matter - this is replaced by the diff --git a/src/test/cbmc/Slice/pathbuf_fail.rs b/src/test/cbmc/Slice/pathbuf.rs similarity index 99% rename from src/test/cbmc/Slice/pathbuf_fail.rs rename to src/test/cbmc/Slice/pathbuf.rs index a6c1ba2113ac..d7c886914369 100644 --- a/src/test/cbmc/Slice/pathbuf_fail.rs +++ b/src/test/cbmc/Slice/pathbuf.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail use std::fs; diff --git a/src/test/cbmc/Slice/slice_from_raw_fail.rs b/src/test/cbmc/Slice/slice_from_raw.rs similarity index 99% rename from src/test/cbmc/Slice/slice_from_raw_fail.rs rename to src/test/cbmc/Slice/slice_from_raw.rs index 7b1e3335cfb1..49cf8257c204 100644 --- a/src/test/cbmc/Slice/slice_from_raw_fail.rs +++ b/src/test/cbmc/Slice/slice_from_raw.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail use std::slice; diff --git a/src/test/prusti/Binary_search.rs b/src/test/prusti/Binary_search.rs index a8cd21d14ef7..f6c3c2ef49f3 100644 --- a/src/test/prusti/Binary_search.rs +++ b/src/test/prusti/Binary_search.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT - // rmc-verify-fail // cbmc-flags: --unwind 4 diff --git a/src/test/smack/basic/add_fail.rs b/src/test/smack/basic/add.rs similarity index 100% rename from src/test/smack/basic/add_fail.rs rename to src/test/smack/basic/add.rs diff --git a/src/test/smack/basic/arith_assume_fail.rs b/src/test/smack/basic/arith_assume3.rs similarity index 100% rename from src/test/smack/basic/arith_assume_fail.rs rename to src/test/smack/basic/arith_assume3.rs diff --git a/src/test/smack/basic/div_fail.rs b/src/test/smack/basic/div.rs similarity index 100% rename from src/test/smack/basic/div_fail.rs rename to src/test/smack/basic/div.rs diff --git a/src/test/smack/basic/mod_fail.rs b/src/test/smack/basic/mod.rs similarity index 100% rename from src/test/smack/basic/mod_fail.rs rename to src/test/smack/basic/mod.rs diff --git a/src/test/smack/basic/mul_fail.rs b/src/test/smack/basic/mul.rs similarity index 100% rename from src/test/smack/basic/mul_fail.rs rename to src/test/smack/basic/mul.rs diff --git a/src/test/smack/basic/sub_fail.rs b/src/test/smack/basic/sub.rs similarity index 100% rename from src/test/smack/basic/sub_fail.rs rename to src/test/smack/basic/sub.rs diff --git a/src/test/smack/generics/generic_function_fail1.rs b/src/test/smack/generics/generic_function1.rs similarity index 100% rename from src/test/smack/generics/generic_function_fail1.rs rename to src/test/smack/generics/generic_function1.rs diff --git a/src/test/smack/generics/generic_function_fail2.rs b/src/test/smack/generics/generic_function2.rs similarity index 100% rename from src/test/smack/generics/generic_function_fail2.rs rename to src/test/smack/generics/generic_function2.rs diff --git a/src/test/smack/generics/generic_function_fail3.rs b/src/test/smack/generics/generic_function3.rs similarity index 100% rename from src/test/smack/generics/generic_function_fail3.rs rename to src/test/smack/generics/generic_function3.rs diff --git a/src/test/smack/generics/generic_function_fail4.rs b/src/test/smack/generics/generic_function4.rs similarity index 100% rename from src/test/smack/generics/generic_function_fail4.rs rename to src/test/smack/generics/generic_function4.rs diff --git a/src/test/smack/generics/generic_function_fail5.rs b/src/test/smack/generics/generic_function5.rs similarity index 100% rename from src/test/smack/generics/generic_function_fail5.rs rename to src/test/smack/generics/generic_function5.rs diff --git a/src/test/smack/overflow/add_overflow_fail.rs b/src/test/smack/overflow/add_overflow.rs similarity index 100% rename from src/test/smack/overflow/add_overflow_fail.rs rename to src/test/smack/overflow/add_overflow.rs diff --git a/src/test/smack/overflow/mul_overflow_fail.rs b/src/test/smack/overflow/mul_overflow.rs similarity index 100% rename from src/test/smack/overflow/mul_overflow_fail.rs rename to src/test/smack/overflow/mul_overflow.rs diff --git a/src/test/smack/overflow/sub_overflow_fail.rs b/src/test/smack/overflow/sub_overflow.rs similarity index 100% rename from src/test/smack/overflow/sub_overflow_fail.rs rename to src/test/smack/overflow/sub_overflow.rs diff --git a/src/test/smack/vector/vec1_fail1.rs b/src/test/smack/vector/vec11.rs similarity index 100% rename from src/test/smack/vector/vec1_fail1.rs rename to src/test/smack/vector/vec11.rs diff --git a/src/test/smack/vector/vec1_fail2.rs b/src/test/smack/vector/vec12.rs similarity index 100% rename from src/test/smack/vector/vec1_fail2.rs rename to src/test/smack/vector/vec12.rs diff --git a/src/test/smack/vector/vec1_fail3.rs b/src/test/smack/vector/vec13.rs similarity index 100% rename from src/test/smack/vector/vec1_fail3.rs rename to src/test/smack/vector/vec13.rs diff --git a/src/tools/compiletest/src/runtest.rs b/src/tools/compiletest/src/runtest.rs index a21eec8db9b8..9ca7241ddeb3 100644 --- a/src/tools/compiletest/src/runtest.rs +++ b/src/tools/compiletest/src/runtest.rs @@ -2511,7 +2511,7 @@ impl<'test> TestCx<'test> { } } - /// Checks, codgens, and verifies the test file specified by + /// Checks, codegens, and verifies the test file specified by /// `self.testpaths.file`. An error message is printed to stdout if a result /// is not expected. fn run_rmc_test(&self) { From 0db2018ed96194f358a141f2ec1608c70afecd9c Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed Date: Thu, 22 Jul 2021 16:33:51 +0000 Subject: [PATCH 4/5] Address concerns. --- .../core_intrinsics.rs} | 0 src/tools/compiletest/src/common.rs | 11 ++++- src/tools/compiletest/src/header.rs | 47 ++++++++++++------- src/tools/compiletest/src/runtest.rs | 16 +++---- src/tools/dashboard/src/main.rs | 13 +++++ 5 files changed, 59 insertions(+), 28 deletions(-) rename src/test/cbmc/{SIMD/mem/volatile.rs => VolatileIntrinsics/core_intrinsics.rs} (100%) diff --git a/src/test/cbmc/SIMD/mem/volatile.rs b/src/test/cbmc/VolatileIntrinsics/core_intrinsics.rs similarity index 100% rename from src/test/cbmc/SIMD/mem/volatile.rs rename to src/test/cbmc/VolatileIntrinsics/core_intrinsics.rs diff --git a/src/tools/compiletest/src/common.rs b/src/tools/compiletest/src/common.rs index f38ebd4fc36b..09a2380924aa 100644 --- a/src/tools/compiletest/src/common.rs +++ b/src/tools/compiletest/src/common.rs @@ -118,11 +118,18 @@ impl fmt::Display for PassMode { } } -/// Stage where an RMC test should fail. +/// Step at which RMC test should fail. #[derive(Copy, Clone, Debug, PartialEq, PartialOrd)] -pub enum RMCFailMode { +pub enum RMCFailStep { + /// RMC panics before the codegen step. This step runs the same checks on + /// the test code as `cargo check` including syntax, type, name resolution, + /// and barrow checks. Check, + /// RMC panics at the codegen step because the test code uses unimplemented + /// and/or unsupported features. Codegen, + /// RMC panics after the codegen step because of verification failures or + /// other CBMC errors. Verify, } diff --git a/src/tools/compiletest/src/header.rs b/src/tools/compiletest/src/header.rs index 073577110d68..63800b808956 100644 --- a/src/tools/compiletest/src/header.rs +++ b/src/tools/compiletest/src/header.rs @@ -8,7 +8,7 @@ use std::path::{Path, PathBuf}; use tracing::*; use crate::common::{ - CompareMode, Config, Debugger, FailMode, Mode, PanicStrategy, PassMode, RMCFailMode, + CompareMode, Config, Debugger, FailMode, Mode, PanicStrategy, PassMode, RMCFailStep, }; use crate::util; use crate::{extract_cdb_version, extract_gdb_version}; @@ -123,8 +123,8 @@ pub struct TestProps { pass_mode: Option, // Ignore `--pass` overrides from the command line for this test. ignore_pass: bool, - // How far this RMC test should proceed to start failing. - pub rmc_fail_mode: Option, + // At which step is the RMC test expected to fail. + pub rmc_panic_step: Option, // How far this test should proceed to start failing. pub fail_mode: Option, // rustdoc will test the output of the `--test` option @@ -174,7 +174,7 @@ impl TestProps { forbid_output: vec![], incremental_dir: None, pass_mode: None, - rmc_fail_mode: None, + rmc_panic_step: None, fail_mode: None, ignore_pass: false, check_test_line_numbers_match: false, @@ -397,20 +397,9 @@ impl TestProps { panic!("`rmc-{}-fail` header is only supported in RMC tests", mode); } }; - let rmc_fail_mode = if config.parse_name_directive(ln, "rmc-check-fail") { - check_rmc("check"); - Some(RMCFailMode::Check) - } else if config.parse_name_directive(ln, "rmc-codegen-fail") { - check_rmc("codegen"); - Some(RMCFailMode::Codegen) - } else if config.parse_name_directive(ln, "rmc-verify-fail") { - check_rmc("verify"); - Some(RMCFailMode::Verify) - } else { - None - }; - match (self.rmc_fail_mode, rmc_fail_mode) { - (None, Some(_)) => self.rmc_fail_mode = rmc_fail_mode, + let rmc_fail_step = config.parse_rmc_step_fail_directive(ln); + match (self.rmc_panic_step, rmc_fail_step) { + (None, Some(_)) => self.rmc_panic_step = rmc_fail_step, (Some(_), Some(_)) => panic!("multiple `rmc-*-fail` headers in a single test"), (_, None) => {} } @@ -559,6 +548,28 @@ impl Config { self.parse_name_value_directive(line, "compile-flags") } + /// Parses strings of the form `rmc-*-fail` and returns the step at which + /// RMC is expected to panic. + fn parse_rmc_step_fail_directive(&self, line: &str) -> Option { + let check_rmc = |mode: &str| { + if self.mode != Mode::RMC { + panic!("`rmc-{}-fail` header is only supported in RMC tests", mode); + } + }; + if self.parse_name_directive(line, "rmc-check-fail") { + check_rmc("check"); + Some(RMCFailStep::Check) + } else if self.parse_name_directive(line, "rmc-codegen-fail") { + check_rmc("codegen"); + Some(RMCFailStep::Codegen) + } else if self.parse_name_directive(line, "rmc-verify-fail") { + check_rmc("verify"); + Some(RMCFailStep::Verify) + } else { + None + } + } + /// Parses strings of the form `// rmc-flags: ...` and returns the options listed after `rmc-flags:` fn parse_rmc_flags(&self, line: &str) -> Option { self.parse_name_value_directive(line, "rmc-flags") diff --git a/src/tools/compiletest/src/runtest.rs b/src/tools/compiletest/src/runtest.rs index 9ca7241ddeb3..417310e9a59b 100644 --- a/src/tools/compiletest/src/runtest.rs +++ b/src/tools/compiletest/src/runtest.rs @@ -1,7 +1,7 @@ // ignore-tidy-filelength use crate::common::{ - expected_output_path, RMCFailMode, UI_EXTENSIONS, UI_FIXED, UI_STDERR, UI_STDOUT, + expected_output_path, RMCFailStep, UI_EXTENSIONS, UI_FIXED, UI_STDERR, UI_STDOUT, }; use crate::common::{output_base_dir, output_base_name, output_testname_unique}; use crate::common::{ @@ -2407,14 +2407,14 @@ impl<'test> TestCx<'test> { } } - /// Runs `rustc` on the test file specified by `self.testpaths.file`. An + /// Runs `rmc-rustc` on the test file specified by `self.testpaths.file`. An /// error message is printed to stdout if the check result is not expected. fn check(&self) { let mut rustc = Command::new("rmc-rustc"); rustc.args(["-Z", "no-codegen"]).arg(&self.testpaths.file); self.add_rmc_dir_to_path(&mut rustc); let proc_res = self.compose_and_run_compiler(rustc, None); - if self.props.rmc_fail_mode == Some(RMCFailMode::Check) { + if self.props.rmc_panic_step == Some(RMCFailStep::Check) { if proc_res.status.success() { self.fatal_proc_rec("test failed: expected check failure, got success", &proc_res); } @@ -2425,7 +2425,7 @@ impl<'test> TestCx<'test> { } } - /// Runs `rustc` on the test file specified by `self.testpaths.file`. An + /// Runs `rmc-rustc` on the test file specified by `self.testpaths.file`. An /// error message is printed to stdout if the codegen result is not /// expected. fn codegen(&self) { @@ -2436,7 +2436,7 @@ impl<'test> TestCx<'test> { .arg(&self.testpaths.file); self.add_rmc_dir_to_path(&mut rustc); let proc_res = self.compose_and_run_compiler(rustc, None); - if self.props.rmc_fail_mode == Some(RMCFailMode::Codegen) { + if self.props.rmc_panic_step == Some(RMCFailStep::Codegen) { if proc_res.status.success() { self.fatal_proc_rec( "test failed: expected codegen failure, got success", @@ -2493,7 +2493,7 @@ impl<'test> TestCx<'test> { ) } // Print an error if the verification result is not expected. - if self.props.rmc_fail_mode == Some(RMCFailMode::Verify) { + if self.props.rmc_panic_step == Some(RMCFailStep::Verify) { if proc_res.status.success() { self.fatal_proc_rec( "test failed: expected verification failure, got success", @@ -2516,11 +2516,11 @@ impl<'test> TestCx<'test> { /// is not expected. fn run_rmc_test(&self) { self.check(); - if self.props.rmc_fail_mode == Some(RMCFailMode::Check) { + if self.props.rmc_panic_step == Some(RMCFailStep::Check) { return; } self.codegen(); - if self.props.rmc_fail_mode == Some(RMCFailMode::Codegen) { + if self.props.rmc_panic_step == Some(RMCFailStep::Codegen) { return; } self.verify(); diff --git a/src/tools/dashboard/src/main.rs b/src/tools/dashboard/src/main.rs index a8d8243d03e9..2d22e021a48d 100644 --- a/src/tools/dashboard/src/main.rs +++ b/src/tools/dashboard/src/main.rs @@ -4,6 +4,19 @@ mod dashboard; mod reference; +use std::intrinsics::*; + fn main() { reference::display_reference_dashboard(); + let mut a: Box = Box::new(0); + unsafe { + let x = volatile_load(&*a); + assert!(x == *a); + volatile_store(&mut *a, 1); + assert!(*a == 1); + unaligned_volatile_store(&mut *a, 2); + assert!(*a == 2); + volatile_set_memory(&mut *a, 3, 1); + assert!(*a == 3); + } } From 0a656d3897bcdf037bbaab6f2b9641f68058363f Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed Date: Thu, 22 Jul 2021 17:45:37 +0000 Subject: [PATCH 5/5] Remove unnecessary code and fix typos. --- src/tools/compiletest/src/common.rs | 6 +++--- src/tools/compiletest/src/header.rs | 5 ----- src/tools/dashboard/src/main.rs | 13 ------------- 3 files changed, 3 insertions(+), 21 deletions(-) diff --git a/src/tools/compiletest/src/common.rs b/src/tools/compiletest/src/common.rs index 09a2380924aa..240f4cf30694 100644 --- a/src/tools/compiletest/src/common.rs +++ b/src/tools/compiletest/src/common.rs @@ -121,9 +121,9 @@ impl fmt::Display for PassMode { /// Step at which RMC test should fail. #[derive(Copy, Clone, Debug, PartialEq, PartialOrd)] pub enum RMCFailStep { - /// RMC panics before the codegen step. This step runs the same checks on - /// the test code as `cargo check` including syntax, type, name resolution, - /// and barrow checks. + /// RMC panics before the codegen step (up to MIR generation). This step + /// runs the same checks on the test code as `cargo check` including syntax, + /// type, name resolution, and borrow checks. Check, /// RMC panics at the codegen step because the test code uses unimplemented /// and/or unsupported features. diff --git a/src/tools/compiletest/src/header.rs b/src/tools/compiletest/src/header.rs index 63800b808956..4704a240c97b 100644 --- a/src/tools/compiletest/src/header.rs +++ b/src/tools/compiletest/src/header.rs @@ -392,11 +392,6 @@ impl TestProps { /// Checks if `ln` specifies which stage the test should fail on and updates /// RMC fail mode accordingly. fn update_rmc_fail_mode(&mut self, ln: &str, config: &Config) { - let check_rmc = |mode: &str| { - if config.mode != Mode::RMC { - panic!("`rmc-{}-fail` header is only supported in RMC tests", mode); - } - }; let rmc_fail_step = config.parse_rmc_step_fail_directive(ln); match (self.rmc_panic_step, rmc_fail_step) { (None, Some(_)) => self.rmc_panic_step = rmc_fail_step, diff --git a/src/tools/dashboard/src/main.rs b/src/tools/dashboard/src/main.rs index 2d22e021a48d..a8d8243d03e9 100644 --- a/src/tools/dashboard/src/main.rs +++ b/src/tools/dashboard/src/main.rs @@ -4,19 +4,6 @@ mod dashboard; mod reference; -use std::intrinsics::*; - fn main() { reference::display_reference_dashboard(); - let mut a: Box = Box::new(0); - unsafe { - let x = volatile_load(&*a); - assert!(x == *a); - volatile_store(&mut *a, 1); - assert!(*a == 1); - unaligned_volatile_store(&mut *a, 2); - assert!(*a == 2); - volatile_set_memory(&mut *a, 3, 1); - assert!(*a == 3); - } }