cargo kani --tests fails on crates with integration tests

[zhassan-aws]

Steps to reproduce:

1. cargo new foo
2. cd foo
3. Append the following to src/main.rs:

#[cfg(test)]
mod tests {
    #[test]
    #[kani::proof]
    fn check() {
        assert!(1 + 1 == 2);
    }
}

4. Run cargo kani --tests. Verification is successful:

SUMMARY: 
 ** 0 of 1 failed

VERIFICATION:- SUCCESSFUL

5. Under the package root directory, create a tests directory, and place a my_test.rs file inside with the following:

#[test]
fn main() {
    assert!(2 + 2 == 4);
}

6. Run cargo clean
7. Run cargo kani --tests again

This fails with the following:

$ cargo kani --tests
   Compiling foo v0.1.0 (/home/ubuntu/examples/integ_tests/foo)
    Finished test [unoptimized + debuginfo] target(s) in 0.26s
  Executable unittests src/main.rs (target/x86_64-unknown-linux-gnu/debug/deps/foo-61c8a3392540768f)
  Executable tests/my_test.rs (target/x86_64-unknown-linux-gnu/debug/deps/my_test-3ee8fa6d631c7ebc)
/home/ubuntu/git/kani/library/std/src/lib.rs: In function 'main':
/home/ubuntu/git/kani/library/std/src/lib.rs:41:9: error: 
reason for conflict at #this: number of members is different (2/0)

struct _15120766920117065333 {
  struct _15678888388531287603 ** data;
  unsigned long int len;
}
struct Unit {
}
error: conflicting types for variable 'main::1::var_1'
old definition in module '' file /home/ubuntu/examples/integ_tests/foo/src/main.rs line 1 column 1 function main
struct _15120766920117065333 {
  struct _15678888388531287603 ** data;
  unsigned long int len;
}
new definition in module '' file /home/ubuntu/git/kani/library/std/src/lib.rs line 41 column 9 function main
struct Unit {
}
         kani::assert($cond, concat!("assertion failed: ", stringify!($cond)));
/home/ubuntu/examples/integ_tests/foo/tests/my_test.rs: In function 'main':
/home/ubuntu/examples/integ_tests/foo/tests/my_test.rs:3:13: error: error: conflicting types for variable 'main::1::var_2'
old definition in module '' file /home/ubuntu/examples/integ_tests/foo/src/main.rs line 1 column 1 function main
struct [_13271361662039110976; 0] {
  struct _15678888388531287603 *[0] 0;
} *
new definition in module '' file /home/ubuntu/examples/integ_tests/foo/tests/my_test.rs line 3 column 13 function main
_Bool
     assert!(2 + 2 == 4);
typechecking main failed
Error: goto-cc exited with status exit status: 1

with Kani version: 43cb18c5d21

[zhassan-aws]

Same issue is reproducible with lib crates.

[zhassan-aws]

We can use cargo test's --lib option to avoid running integration tests, e.g.:

$ git diff
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index f8624297f97..d7010adf323 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -48,6 +48,7 @@ pub fn cargo_build(&self) -> Result<CargoOutputs> {
         if self.args.tests {
             args.push("test".into());
             args.push("--no-run".into());
+            args.push("--lib".into());
         } else {
             args.push("build".into());
         }

However, this results in an error for binary crates:

error: no library targets found in package `foo`

[tedinski]

Is this just about main in integration tests? Isn't that a strange thing to do? Did we actually run into code somewhere that does that?

[zhassan-aws]

It is used in s2n-quic, e.g.:

https://github.com/aws/s2n-quic/blob/main/quic/s2n-quic-core/tests/varint/fuzz_target.rs

[tedinski]

Writing down thoughts so they don't get lost.

Two potential issues here

1. #661 This could be causing issues because main might otherwise be given a fully-qualified name that doesn't clash.
2. #1598 This could be causing issues because perhaps there really is a main regardless, and now we're colliding multiple binaries symbols together into one binary.

[zhassan-aws]

This was fixed by the MIR linker. Closing.