Add option to enable layout randomization (rust-lang#1623)

giltho · web-flow · commit 1eb9643d8e98 · 2022-09-27T11:34:17.000-05:00
diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs
@@ -191,6 +191,13 @@ pub struct KaniArgs {
     /// Disable CBMC's slice formula which prevents values from being assigned to redundant variables in traces.
     #[structopt(long, hidden_short_help(true), requires("enable-unstable"))]
     pub no_slice_formula: bool,
+
+    /// Randomize the layout of structures. This option can help catching code that relies on
+    /// a specific layout chosen by the compiler that is not guaranteed to be stable in the future.
+    /// If a value is given, it will be used as the seed for randomization
+    /// See the `-Z randomize-layout` and `-Z layout-seed` arguments of the rust compiler.
+    #[structopt(long)]
+    pub randomize_layout: Option<Option<u64>>,
     /*
     The below is a "TODO list" of things not yet implemented from the kani_flags.py script.
 
@@ -351,6 +358,22 @@ impl KaniArgs {
             self.cbmc_args.iter().any(|s| s.to_str().unwrap().starts_with("--unwind"));
         let natives_unwind = self.default_unwind.is_some() || self.unwind.is_some();
 
+        if self.randomize_layout.is_some() && self.concrete_playback.is_some() {
+            let random_seed = if let Some(seed) = self.randomize_layout.unwrap() {
+                format!(" -Z layout-seed={}", seed)
+            } else {
+                String::new()
+            };
+
+            // `tracing` is not a dependency of `kani-driver`, so we println! here instead.
+            println!(
+                "Using concrete playback with --randomize-layout.\n\
+                The produced tests will have to be played with the same rustc arguments:\n\
+                -Z randomize-layout{}",
+                random_seed
+            );
+        }
+
         // TODO: these conflicting flags reflect what's necessary to pass current tests unmodified.
         // We should consider improving the error messages slightly in a later pull request.
         if natives_unwind && extra_unwind {
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
@@ -148,6 +148,15 @@ impl KaniSession {
             flags.push(abs_type.into());
         }
 
+        if let Some(seed_opt) = self.args.randomize_layout {
+            flags.push("-Z".into());
+            flags.push("randomize-layout".into());
+            if let Some(seed) = seed_opt {
+                flags.push("-Z".into());
+                flags.push(format!("layout-seed={}", seed).into());
+            }
+        }
+
         flags.push("-C".into());
         flags.push("symbol-mangling-version=v0".into());
 
diff --git a/kani-driver/src/concrete_playback.rs b/kani-driver/src/concrete_playback.rs
@@ -43,7 +43,11 @@ impl KaniSession {
                     harness.pretty_name
                 ),
                 Some(concrete_vals) => {
-                    let concrete_playback = format_unit_test(&harness.mangled_name, &concrete_vals);
+                    let concrete_playback = format_unit_test(
+                        &harness.mangled_name,
+                        &concrete_vals,
+                        self.args.randomize_layout,
+                    );
                     match playback_mode {
                         ConcretePlaybackMode::Print => {
                             println!(
@@ -222,7 +226,14 @@ impl KaniSession {
 }
 
 /// Generate a unit test from a list of concrete values.
-fn format_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> UnitTest {
+/// `randomize_layout_seed` is `None` when layout is not randomized,
+/// `Some(None)` when layout is randomized without seed, and
+/// `Some(Some(seed))` when layout is randomized with the seed `seed`.
+fn format_unit_test(
+    harness_name: &str,
+    concrete_vals: &[ConcreteVal],
+    randomize_layout_seed: Option<Option<u64>>,
+) -> UnitTest {
     /*
     Given a number of byte vectors, format them as:
     // interp_concrete_val_1
@@ -249,10 +260,23 @@ fn format_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> UnitTe
     let hash = hasher.finish();
 
     let concrete_playback_func_name = format!("kani_concrete_playback_{harness_name}_{hash}");
+
+    let randomize_layout_message = match randomize_layout_seed {
+        None => String::new(),
+        Some(None) => {
+            "// This test has to be run with rustc option: -Z randomize-layout\n    ".to_string()
+        }
+        Some(Some(seed)) => format!(
+            "// This test has to be run with rust options: -Z randomize-layout -Z layout-seed={}\n    ",
+            seed,
+        ),
+    };
+
     #[rustfmt::skip]
     let concrete_playback = format!(
 "#[test]
 fn {concrete_playback_func_name}() {{
+    {randomize_layout_message}\
     let concrete_vals: Vec<Vec<u8>> = vec![
 {vecs_as_str}
     ];
diff --git a/tests/kani/LayoutRandomization/should_fail.rs b/tests/kani/LayoutRandomization/should_fail.rs
@@ -0,0 +1,72 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test only succeeds on the layout of a structure being
+// decided in a deterministic way.
+// With randomization, there is a very very high probability that it fails (1 - (1/2^100))
+
+// kani-flags: --randomize-layout=0
+// kani-verify-fail
+
+macro_rules! make_structs {
+    ($i:ident) => {
+        struct $i {
+            a: u32,
+            b: u16,
+        }
+    };
+
+    ($i:ident, $($rest:ident),+) => {
+        make_structs!($i);
+        make_structs!($($rest),+);
+    };
+  }
+
+// We only need Foo1 to be clone
+impl Clone for Foo1 {
+    fn clone(&self) -> Self {
+        Self { a: self.a, b: self.b }
+    }
+}
+
+macro_rules! check_against {
+    ($to_check:ident, $current_against:ty) => {
+        {
+            let other: $current_against = unsafe {std::mem::transmute($to_check.clone())};
+            assert_eq!($to_check.a, other.a);
+            assert_eq!($to_check.b, other.b);
+        }
+    };
+    ($to_check:ident, $current_against:ty, $($rest:ty),+) => {
+        check_against!($to_check, $current_against);
+        check_against!($to_check, $($rest),+);
+    };
+  }
+
+make_structs!(
+    Foo1, Foo2, Foo3, Foo4, Foo5, Foo6, Foo7, Foo8, Foo9, Foo10, Foo11, Foo12, Foo13, Foo14, Foo15,
+    Foo16, Foo17, Foo18, Foo19, Foo20, Foo21, Foo22, Foo23, Foo24, Foo25, Foo26, Foo27, Foo28,
+    Foo29, Foo30, Foo31, Foo32, Foo33, Foo34, Foo35, Foo36, Foo37, Foo38, Foo39, Foo40, Foo41,
+    Foo42, Foo43, Foo44, Foo45, Foo46, Foo47, Foo48, Foo49, Foo50, Foo51, Foo52, Foo53, Foo54,
+    Foo55, Foo56, Foo57, Foo58, Foo59, Foo60, Foo61, Foo62, Foo63, Foo64, Foo65, Foo66, Foo67,
+    Foo68, Foo69, Foo70, Foo71, Foo72, Foo73, Foo74, Foo75, Foo76, Foo77, Foo78, Foo79, Foo80,
+    Foo81, Foo82, Foo83, Foo84, Foo85, Foo86, Foo87, Foo88, Foo89, Foo90, Foo91, Foo92, Foo93,
+    Foo94, Foo95, Foo96, Foo97, Foo98, Foo99, Foo100
+);
+
+#[kani::proof]
+fn main() {
+    let a: u32 = kani::any();
+    let b: u16 = kani::any();
+    let base = Foo1 { a, b };
+    check_against!(
+        base, Foo2, Foo3, Foo4, Foo5, Foo6, Foo7, Foo8, Foo9, Foo10, Foo11, Foo12, Foo13, Foo14,
+        Foo15, Foo16, Foo17, Foo18, Foo19, Foo20, Foo21, Foo22, Foo23, Foo24, Foo25, Foo26, Foo27,
+        Foo28, Foo29, Foo30, Foo31, Foo32, Foo33, Foo34, Foo35, Foo36, Foo37, Foo38, Foo39, Foo40,
+        Foo41, Foo42, Foo43, Foo44, Foo45, Foo46, Foo47, Foo48, Foo49, Foo50, Foo51, Foo52, Foo53,
+        Foo54, Foo55, Foo56, Foo57, Foo58, Foo59, Foo60, Foo61, Foo62, Foo63, Foo64, Foo65, Foo66,
+        Foo67, Foo68, Foo69, Foo70, Foo71, Foo72, Foo73, Foo74, Foo75, Foo76, Foo77, Foo78, Foo79,
+        Foo80, Foo81, Foo82, Foo83, Foo84, Foo85, Foo86, Foo87, Foo88, Foo89, Foo90, Foo91, Foo92,
+        Foo93, Foo94, Foo95, Foo96, Foo97, Foo98, Foo99, Foo100
+    );
+}
diff --git a/tests/kani/LayoutRandomization/should_succeed.rs b/tests/kani/LayoutRandomization/should_succeed.rs
@@ -0,0 +1,70 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that `--randomize-layout` doesn't affect repr(C) and Kani is still bit-precise
+
+// kani-flags: --randomize-layout=0
+
+macro_rules! make_structs {
+  ($i:ident) => {
+      #[repr(C)]
+      struct $i {
+          a: u32,
+          b: u16,
+      }
+  };
+
+  ($i:ident, $($rest:ident),+) => {
+      make_structs!($i);
+      make_structs!($($rest),+);
+  };
+}
+
+// We only need Foo1 to be clone
+impl Clone for Foo1 {
+    fn clone(&self) -> Self {
+        Self { a: self.a, b: self.b }
+    }
+}
+
+macro_rules! check_against {
+  ($to_check:ident, $current_against:ty) => {
+      {
+          let other: $current_against = unsafe {std::mem::transmute($to_check.clone())};
+          assert_eq!($to_check.a, other.a);
+          assert_eq!($to_check.b, other.b);
+      }
+  };
+  ($to_check:ident, $current_against:ty, $($rest:ty),+) => {
+      check_against!($to_check, $current_against);
+      check_against!($to_check, $($rest),+);
+  };
+}
+
+make_structs!(
+    Foo1, Foo2, Foo3, Foo4, Foo5, Foo6, Foo7, Foo8, Foo9, Foo10, Foo11, Foo12, Foo13, Foo14, Foo15,
+    Foo16, Foo17, Foo18, Foo19, Foo20, Foo21, Foo22, Foo23, Foo24, Foo25, Foo26, Foo27, Foo28,
+    Foo29, Foo30, Foo31, Foo32, Foo33, Foo34, Foo35, Foo36, Foo37, Foo38, Foo39, Foo40, Foo41,
+    Foo42, Foo43, Foo44, Foo45, Foo46, Foo47, Foo48, Foo49, Foo50, Foo51, Foo52, Foo53, Foo54,
+    Foo55, Foo56, Foo57, Foo58, Foo59, Foo60, Foo61, Foo62, Foo63, Foo64, Foo65, Foo66, Foo67,
+    Foo68, Foo69, Foo70, Foo71, Foo72, Foo73, Foo74, Foo75, Foo76, Foo77, Foo78, Foo79, Foo80,
+    Foo81, Foo82, Foo83, Foo84, Foo85, Foo86, Foo87, Foo88, Foo89, Foo90, Foo91, Foo92, Foo93,
+    Foo94, Foo95, Foo96, Foo97, Foo98, Foo99, Foo100
+);
+
+#[kani::proof]
+fn main() {
+    let a: u32 = kani::any();
+    let b: u16 = kani::any();
+    let base = Foo1 { a, b };
+    check_against!(
+        base, Foo2, Foo3, Foo4, Foo5, Foo6, Foo7, Foo8, Foo9, Foo10, Foo11, Foo12, Foo13, Foo14,
+        Foo15, Foo16, Foo17, Foo18, Foo19, Foo20, Foo21, Foo22, Foo23, Foo24, Foo25, Foo26, Foo27,
+        Foo28, Foo29, Foo30, Foo31, Foo32, Foo33, Foo34, Foo35, Foo36, Foo37, Foo38, Foo39, Foo40,
+        Foo41, Foo42, Foo43, Foo44, Foo45, Foo46, Foo47, Foo48, Foo49, Foo50, Foo51, Foo52, Foo53,
+        Foo54, Foo55, Foo56, Foo57, Foo58, Foo59, Foo60, Foo61, Foo62, Foo63, Foo64, Foo65, Foo66,
+        Foo67, Foo68, Foo69, Foo70, Foo71, Foo72, Foo73, Foo74, Foo75, Foo76, Foo77, Foo78, Foo79,
+        Foo80, Foo81, Foo82, Foo83, Foo84, Foo85, Foo86, Foo87, Foo88, Foo89, Foo90, Foo91, Foo92,
+        Foo93, Foo94, Foo95, Foo96, Foo97, Foo98, Foo99, Foo100
+    );
+}
