Enforce formatting of RMC tests.

rustfmt.toml

@@ -13,7 +13,15 @@ ignore = [
 
     # tests for now are not formatted, as they are sometimes pretty-printing constrained
     # (and generally rustfmt can move around comments in UI-testing incompatible ways)
-    "src/test",
+    "src/test/*",
+    "!src/test/cargo-rmc",
+    "!src/test/cbmc",
+    "!src/test/expected",
+    "!src/test/firecracker",
+    "!src/test/prusti",
+    "!src/test/rmc-prelude.rs",
+    "!src/test/serial",
+    "!src/test/smack",
 
     # do not format submodules
     "library/backtrace",

src/bootstrap/format.rs

@@ -58,9 +58,9 @@ pub fn format(build: &Build, check: bool, paths: &[PathBuf]) {
     }
     let rustfmt_config = t!(std::fs::read_to_string(&rustfmt_config));
     let rustfmt_config: RustfmtConfig = t!(toml::from_str(&rustfmt_config));
-    let mut ignore_fmt = ignore::overrides::OverrideBuilder::new(&build.src);
+    let mut ignore_fmt = ignore::gitignore::GitignoreBuilder::new(&build.src);
     for ignore in rustfmt_config.ignore {
-        ignore_fmt.add(&format!("!{}", ignore)).expect(&ignore);
+        ignore_fmt.add_line(None, &ignore).expect(&ignore);
     }
     let git_available = match Command::new("git")
         .arg("--version")
@@ -129,7 +129,9 @@ pub fn format(build: &Build, check: bool, paths: &[PathBuf]) {
         None => WalkBuilder::new(src.clone()),
     }
     .types(matcher)
-    .overrides(ignore_fmt)
+    .filter_entry(move |e| {
+        !ignore_fmt.matched(e.path(), e.file_type().unwrap().is_dir()).is_ignore()
+    })
     .build_parallel();
 
     // there is a lot of blocking involved in spawning a child process and reading files to format.

src/test/cbmc/DynTrait/different_crates.rs

@@ -13,7 +13,7 @@ impl std::iter::Iterator for Counter {
     type Item = usize;
 
     fn next(&mut self) -> Option<Self::Item> {
-        // Increment our count. 
+        // Increment our count.
         self.count += 1;
         Some(self.count)
     }
@@ -30,24 +30,24 @@ impl Iterator for Counter {
     }
 }
 
-trait Combined : Iterator + std::iter::Iterator<Item = usize> {}
+trait Combined: Iterator + std::iter::Iterator<Item = usize> {}
 
 impl Combined for Counter {}
 
-fn std_count(c : &mut dyn std::iter::Iterator<Item = usize>) -> usize {
+fn std_count(c: &mut dyn std::iter::Iterator<Item = usize>) -> usize {
     c.next().unwrap()
 }
 
-fn weird_count(c : &mut dyn Iterator) -> usize {
+fn weird_count(c: &mut dyn Iterator) -> usize {
     c.next().unwrap()
 }
 
 fn main() {
-    let counter : &mut Counter = &mut Counter { count: 0 };
+    let counter: &mut Counter = &mut Counter { count: 0 };
     assert!(std_count(counter as &mut dyn std::iter::Iterator<Item = usize>) == 1);
     assert!(weird_count(counter as &mut dyn Iterator) == 42);
-    
+
     let counter_combined = counter as &mut dyn Combined;
     assert!(std::iter::Iterator::next(counter_combined).unwrap() == 2);
     assert!(Iterator::next(counter_combined).unwrap() == 42);
-}
+}

src/test/cbmc/DynTrait/different_crates_fail.rs

@@ -13,7 +13,7 @@ impl std::iter::Iterator for Counter {
     type Item = usize;
 
     fn next(&mut self) -> Option<Self::Item> {
-        // Increment our count. 
+        // Increment our count.
         self.count += 1;
         Some(self.count)
     }
@@ -30,24 +30,24 @@ impl Iterator for Counter {
     }
 }
 
-trait Combined : Iterator + std::iter::Iterator<Item = usize> {}
+trait Combined: Iterator + std::iter::Iterator<Item = usize> {}
 
 impl Combined for Counter {}
 
-fn std_count(c : &mut dyn std::iter::Iterator<Item = usize>) -> usize {
+fn std_count(c: &mut dyn std::iter::Iterator<Item = usize>) -> usize {
     c.next().unwrap()
 }
 
-fn weird_count(c : &mut dyn Iterator) -> usize {
+fn weird_count(c: &mut dyn Iterator) -> usize {
     c.next().unwrap()
 }
 
 fn main() {
-    let counter : &mut Counter = &mut Counter { count: 0 };
+    let counter: &mut Counter = &mut Counter { count: 0 };
     assert!(std_count(counter as &mut dyn std::iter::Iterator<Item = usize>) == 0); // Should be 1
     assert!(weird_count(counter as &mut dyn Iterator) == 0); // Should be 42
-    
+
     let counter_combined = counter as &mut dyn Combined;
     assert!(std::iter::Iterator::next(counter_combined).unwrap() == 0); // Should be 2
     assert!(Iterator::next(counter_combined).unwrap() == 0); // Should be 42
-}
+}

src/test/cbmc/DynTrait/nested_boxes.rs

@@ -1,7 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// This test checks the size and align fields for 3-deep nested trait pointers. The 
+// 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.
 
 #![feature(core_intrinsics)]
@@ -20,33 +20,33 @@ struct Foo {
 }
 
 fn main() {
-    let dyn_trait1 : Box<dyn Send> = Box::new(Foo{ _a : 1, _b : 2});
-    let dyn_trait2 : Box<dyn Send> = Box::new(dyn_trait1);
-    let dyn_trait3 : Box<dyn Send> = Box::new(dyn_trait2);
+    let dyn_trait1: Box<dyn Send> = Box::new(Foo { _a: 1, _b: 2 });
+    let dyn_trait2: Box<dyn Send> = Box::new(dyn_trait1);
+    let dyn_trait3: Box<dyn Send> = Box::new(dyn_trait2);
 
     // Do some unsafe magic to check that we generate the right three vtables
     unsafe {
         let trait_object3: TraitObject = transmute(dyn_trait3);
-        
+
         // Outermost trait object
         // The size is 16, because the data is another fat pointer
         let vtable3: *mut usize = trait_object3.vtable as *mut usize;
         assert!(size_from_vtable(vtable3) == 16);
         assert!(align_from_vtable(vtable3) == 8);
-        
+
         // Inspect the data pointer from dyn_trait3
         let data_ptr3 = trait_object3.data as *mut usize;
-        
+
         // The second half of this fat pointer is another vtable, for dyn_trait2
         let vtable2 = *(data_ptr3.offset(1) as *mut *mut usize);
 
         // The size is 16, because the data is another fat pointer
         assert!(size_from_vtable(vtable2) == 16);
         assert!(align_from_vtable(vtable2) == 8);
-        
+
         // Inspect the data pointer from dyn_trait2
         let data_ptr2 = *(data_ptr3 as *mut *mut usize);
-        
+
         // The second half of this fat pointer is another vtable, for dyn_trait1
         let vtable1 = *(data_ptr2.offset(1) as *mut *mut usize);
 

src/test/cbmc/DynTrait/nested_boxes_fail.rs

@@ -1,7 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// This test checks the size and align fields for 3-deep nested trait pointers. The 
+// 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 !=.
 
@@ -22,33 +22,33 @@ struct Foo {
 }
 
 fn main() {
-    let dyn_trait1 : Box<dyn Send> = Box::new(Foo{ _a : 1, _b : 2});
-    let dyn_trait2 : Box<dyn Send> = Box::new(dyn_trait1);
-    let dyn_trait3 : Box<dyn Send> = Box::new(dyn_trait2);
+    let dyn_trait1: Box<dyn Send> = Box::new(Foo { _a: 1, _b: 2 });
+    let dyn_trait2: Box<dyn Send> = Box::new(dyn_trait1);
+    let dyn_trait3: Box<dyn Send> = Box::new(dyn_trait2);
 
     // Do some unsafe magic to check that we generate the right three vtables
     unsafe {
         let trait_object3: TraitObject = transmute(dyn_trait3);
-        
+
         // Outermost trait object
         // The size is 16, because the data is another fat pointer
         let vtable3: *mut usize = trait_object3.vtable as *mut usize;
         assert!(size_from_vtable(vtable3) != 16);
         assert!(align_from_vtable(vtable3) != 8);
-        
+
         // Inspect the data pointer from dyn_trait3
         let data_ptr3 = trait_object3.data as *mut usize;
-        
+
         // The second half of this fat pointer is another vtable, for dyn_trait2
         let vtable2 = *(data_ptr3.offset(1) as *mut *mut usize);
 
         // The size is 16, because the data is another fat pointer
         assert!(size_from_vtable(vtable2) != 16);
         assert!(align_from_vtable(vtable2) != 8);
-        
+
         // Inspect the data pointer from dyn_trait2
         let data_ptr2 = *(data_ptr3 as *mut *mut usize);
-        
+
         // The second half of this fat pointer is another vtable, for dyn_trait1
         let vtable1 = *(data_ptr2.offset(1) as *mut *mut usize);
 

src/test/cbmc/DynTrait/std_lib_add_duplicate.rs

@@ -1,12 +1,12 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-trait WeirdAdd  {
+trait WeirdAdd {
     fn add(&self, rhs: i32) -> i32;
 }
 
 impl WeirdAdd for i32 {
     fn add(&self, other: i32) -> i32 {
-        self/2 + other/2
+        self / 2 + other / 2
     }
 }
 

src/test/cbmc/DynTrait/vtable_duplicate_field_override.rs

@@ -9,7 +9,7 @@ trait B {
 }
 
 trait T: A + B {
-    fn foo(&self) -> i32;   
+    fn foo(&self) -> i32;
 }
 
 struct S {

src/test/cbmc/DynTrait/vtable_size_align_drop.rs

@@ -46,11 +46,7 @@ impl Animal for Cow {
 
 // Returns some struct that implements Animal, but we don't know which one at compile time.
 fn random_animal(random_number: i64) -> Box<dyn Animal> {
-    if random_number < 5 {
-        Box::new(Sheep { sheep_num: 7 })
-    } else {
-        Box::new(Cow { cow_num: 9 })
-    }
+    if random_number < 5 { Box::new(Sheep { sheep_num: 7 }) } else { Box::new(Cow { cow_num: 9 }) }
 }
 
 fn main() {

src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs

@@ -49,11 +49,7 @@ impl Animal for Cow {
 
 // Returns some struct that implements Animal, but we don't know which one at compile time.
 fn random_animal(random_number: i64) -> Box<dyn Animal> {
-    if random_number < 5 {
-        Box::new(Sheep { sheep_num: 7 })
-    } else {
-        Box::new(Cow { cow_num: 9 })
-    }
+    if random_number < 5 { Box::new(Sheep { sheep_num: 7 }) } else { Box::new(Cow { cow_num: 9 }) }
 }
 
 fn main() {

src/test/cbmc/FatPointers/boxmuttrait.rs

@@ -4,9 +4,9 @@
 #![feature(raw)]
 #![allow(deprecated)]
 
+use std::io::{sink, Write};
 use std::mem::transmute;
 use std::raw::TraitObject;
-use std::io::{sink, Write};
 
 include!("../Helpers/vtable_utils_ignore.rs");
 
@@ -19,21 +19,20 @@ fn main() {
     let num_bytes = log2.write(&buffer).unwrap();
     assert!(num_bytes == 5);
 
-
     // Do some unsafe magic to check that we generate the right two vtables
     unsafe {
         let dest_trait_object: TraitObject = transmute(&*dest);
-        
+
         // The vtable has [&drop, size, align, ....]
         let dest_vtable_ptr = dest_trait_object.vtable as *mut usize;
-        
+
         // The size is 16, because the data is another fat pointer
         assert!(size_from_vtable(dest_vtable_ptr) == 16);
         assert!(align_from_vtable(dest_vtable_ptr) == 8);
-        
+
         // Inspect the data pointer from dest
         let dest_data_ptr = dest_trait_object.data as *mut usize;
-        
+
         // // The second half of this fat pointer is another vtable, for log
         let second_vtable_ptr = dest_data_ptr.offset(1) as *mut *mut usize;
         let second_vtable = *second_vtable_ptr;

src/test/cbmc/Helpers/vtable_utils_ignore.rs

@@ -1,25 +1,19 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Because each regression test does not share a crate, we just use 
+// Because each regression test does not share a crate, we just use
 // an import! to share this code across test directories.
-fn drop_from_vtrable(vtable_ptr : *mut usize) -> *mut () {
+fn drop_from_vtrable(vtable_ptr: *mut usize) -> *mut () {
     // 1st pointer-sized position
-    unsafe {
-        *vtable_ptr as *mut ()
-    }
+    unsafe { *vtable_ptr as *mut () }
 }
 
-fn size_from_vtable(vtable_ptr : *mut usize) -> usize {
+fn size_from_vtable(vtable_ptr: *mut usize) -> usize {
     // 2nd usize-sized position
-    unsafe {
-        *(vtable_ptr.offset(1))
-    }
+    unsafe { *(vtable_ptr.offset(1)) }
 }
 
-fn align_from_vtable(vtable_ptr : *mut usize) -> usize {
+fn align_from_vtable(vtable_ptr: *mut usize) -> usize {
     // 3rd usize-sized position
-    unsafe {
-        *(vtable_ptr.offset(2))
-    }
+    unsafe { *(vtable_ptr.offset(2)) }
 }

src/test/expected/assert-eq/main.rs

@@ -5,14 +5,14 @@
 /// This leads us to the land of foreign types, ReifyFnPointer, and transmute.
 /// The "C" output from RMC is about 1KLOC, vs 80LOC for the same version with straight `assert!`.
 ///     https://github.com/model-checking/rmc/issues/14
-/// The assertion message printed to the user on success is uninformative: 
+/// The assertion message printed to the user on success is uninformative:
 ///     "library/std/src/macros.rs line 17 a panicking function core::panicking::panic_fmt is invoked: SUCCESS"
 ///     https://github.com/model-checking/rmc/issues/13
 
 fn main() {
     let x = 1;
     let y = 2;
-    assert_eq!(x+1, y);
-    assert_eq!(x,y);//Expected failure
+    assert_eq!(x + 1, y);
+    assert_eq!(x, y); //Expected failure
     assert_ne!(x, y);
 }

src/test/expected/binop/main.rs

@@ -71,4 +71,4 @@ fn main() {
     iband_test(3, 10, 2, 3);
     ibor_test(0, 2389034, 2389034, 0);
     ibxor_test(0, 2389034, 2389034, 0);
-}
+}

src/test/expected/closure/main.rs

@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // cbmc-flags: --signed-overflow-check
 fn call_with_one<F>(mut some_closure: F) -> ()
-    where
-        F: FnMut(i64, i64) -> (),
+where
+    F: FnMut(i64, i64) -> (),
 {
     some_closure(1, 1);
 }

src/test/expected/closure3/main.rs

@@ -1,8 +1,8 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 fn call_with_one<F, T>(f: F) -> T
-    where
-        F: FnOnce(i64) -> T,
+where
+    F: FnOnce(i64) -> T,
 {
     f(10)
 }

src/test/expected/comp/main.rs

@@ -21,4 +21,4 @@ fn main() {
         eq1(a, b);
         eq2(a, b);
     }
-}
+}