Vecdeque CVE demo (rust-lang#971)

* Add harness to VecDeque CVE

Author: celinval

tests/cargo-kani/vecdeque-cve/Cargo.toml

@@ -0,0 +1,15 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "vecdeque-cve"
+version = "0.1.0"
+edition = "2018"
+description = "Reproduces CVE-2018-1000657"
+
+[lib]
+path = "src/harness.rs"
+
+[dependencies]
+
+[package.metadata.kani.flags]
+cbmc-args = ["--no-built-in-assertions"]

tests/cargo-kani/vecdeque-cve/reserve_available_capacity_is_no_op.expected

@@ -0,0 +1,17 @@
+fixed::VecDeque::<T, A>::handle_capacity_increase.assertion.14\
+Status: UNREACHABLE\
+Description: "assertion failed: self.head < self.tail"
+
+fixed::VecDeque::<T, A>::handle_capacity_increase.assertion.16\
+Status: UNREACHABLE\
+Description: "assertion failed: self.head < self.cap()"
+
+fixed::VecDeque::<T, A>::handle_capacity_increase.assertion.18\
+Status: UNREACHABLE\
+Description: "assertion failed: self.tail < self.cap()"
+
+fixed::VecDeque::<T, A>::handle_capacity_increase.assertion.20\
+Status: UNREACHABLE\
+Description: "assertion failed: self.cap().count_ones() == 1"
+
+VERIFICATION:- SUCCESSFUL

tests/cargo-kani/vecdeque-cve/reserve_available_capacity_should_fail.expected

@@ -0,0 +1,6 @@
+cve::VecDeque::<T, A>::handle_capacity_increase.assertion\
+- Status: FAILURE\
+- Description: "assertion failed: self.head < self.cap()"
+Location: src/cve.rs
+
+Failed Checks: assertion failed: self.head < self.cap()

tests/cargo-kani/vecdeque-cve/reserve_more_capacity_still_works.expected

@@ -0,0 +1,17 @@
+cve::VecDeque::<T, A>::handle_capacity_increase.assertion\
+Status: SUCCESS\
+Description: "assertion failed: self.head < self.cap()"\
+Location: src/cve.rs
+
+cve::VecDeque::<T, A>::handle_capacity_increase.assertion\
+Status: SUCCESS\
+Description: "assertion failed: self.tail < self.cap()"\
+Location: src/cve.rs
+
+cve::VecDeque::<T, A>::handle_capacity_increase.assertion\
+Status: SUCCESS\
+Description: "assertion failed: self.cap().count_ones() == 1"\
+Location: src/cve.rs
+
+VERIFICATION:- SUCCESSFUL
+

tests/cargo-kani/vecdeque-cve/reserve_more_capacity_works.expected

@@ -0,0 +1,17 @@
+fixed::VecDeque::<T, A>::handle_capacity_increase.assertion\
+Status: SUCCESS\
+Description: "assertion failed: self.head < self.cap()"\
+Location: src/fixed.rs
+
+fixed::VecDeque::<T, A>::handle_capacity_increase.assertion\
+Status: SUCCESS\
+Description: "assertion failed: self.tail < self.cap()"\
+Location: src/fixed.rs
+
+fixed::VecDeque::<T, A>::handle_capacity_increase.assertion\
+Status: SUCCESS\
+Description: "assertion failed: self.cap().count_ones() == 1"\
+Location: src/fixed.rs
+
+VERIFICATION:- SUCCESSFUL
+