Support some of std::vec::Vec methods

Author: coord-e

src/refine/template.rs

@@ -141,6 +141,13 @@ impl<'tcx> TypeBuilder<'tcx> {
             mir_ty::TyKind::Adt(def, params) if def.is_box() => {
                 rty::PointerType::own(self.build(params.type_at(0))).into()
             }
+            // TODO: Declare this in std.rs
+            mir_ty::TyKind::Adt(def, params)
+                if self.tcx.is_diagnostic_item(rustc_span::sym::Vec, def.did()) =>
+            {
+                let content = rty::ArrayType::new(rty::Type::Int, self.build(params.type_at(0)));
+                rty::TupleType::new(vec![content.into(), rty::Type::Int.into()]).into()
+            }
             mir_ty::TyKind::Adt(def, params) => {
                 if def.is_enum() {
                     let sym = refine::datatype_symbol(self.tcx, def.did());
@@ -269,6 +276,15 @@ where
             mir_ty::TyKind::Adt(def, params) if def.is_box() => {
                 rty::PointerType::own(self.build(params.type_at(0))).into()
             }
+            mir_ty::TyKind::Adt(def, params)
+                if self
+                    .inner
+                    .tcx
+                    .is_diagnostic_item(rustc_span::sym::Vec, def.did()) =>
+            {
+                let content = rty::ArrayType::new(rty::Type::Int, self.build(params.type_at(0)));
+                rty::TupleType::new(vec![content.into(), rty::Type::Int.into()]).into()
+            }
             mir_ty::TyKind::Adt(def, params) => {
                 if def.is_enum() {
                     let sym = refine::datatype_symbol(self.inner.tcx, def.did());

std.rs

@@ -201,3 +201,88 @@ fn _extern_spec_i32_is_positive(x: i32) -> bool {
 fn _extern_spec_i32_is_negative(x: i32) -> bool {
     i32::is_negative(x)
 }
+
+#[thrust::extern_spec_fn]
+#[thrust::requires(true)]
+#[thrust::ensures(result.1 == 0)]
+fn _extern_spec_vec_new<T>() -> Vec<T> {
+    Vec::<T>::new()
+}
+
+#[thrust::extern_spec_fn]
+#[thrust::requires(true)]
+#[thrust::ensures(^vec == ((*vec).0.store((*vec).1, elem), (*vec).1 + 1))]
+fn _extern_spec_vec_push<T>(vec: &mut Vec<T>, elem: T) {
+    Vec::push(vec, elem)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust::requires(true)]
+#[thrust::ensures(result == (*vec).1)]
+fn _extern_spec_vec_len<T>(vec: &Vec<T>) -> usize {
+    Vec::len(vec)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust::requires(index < (*vec).1)]
+#[thrust::ensures(*result == (*vec).0.select(index))]
+fn _extern_spec_vec_index<T>(vec: &Vec<T>, index: usize) -> &T {
+    <Vec<T> as std::ops::Index<usize>>::index(vec, index)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust::requires(index < (*vec).1)]
+#[thrust::ensures(
+    *result == (*vec).0.select(index) &&
+    ^result == (^vec).0.select(index) &&
+    ^vec == ((*vec).0.store(index, ^result), (*vec).1)
+)]
+fn _extern_spec_vec_index_mut<T>(vec: &mut Vec<T>, index: usize) -> &mut T {
+    <Vec<T> as std::ops::IndexMut<usize>>::index_mut(vec, index)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust::requires(true)]
+#[thrust::ensures((^vec).1 == 0)]
+fn _extern_spec_vec_clear<T>(vec: &mut Vec<T>) {
+    Vec::clear(vec)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust::requires(true)]
+#[thrust::ensures(
+    (
+        (*vec).1 > 0 &&
+        (^vec).1 == (*vec).1 - 1 &&
+        result == std::option::Option::<T0>::Some((*vec).0.select((*vec).1 - 1))
+    ) || (
+        (*vec).1 == 0 &&
+        (^vec).1 == 0 &&
+        result == std::option::Option::<T0>::None()
+    )
+)]
+fn _extern_spec_vec_pop<T>(vec: &mut Vec<T>) -> Option<T> {
+    Vec::pop(vec)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust::requires(true)]
+#[thrust::ensures(result == ((*vec).1 == 0))]
+fn _extern_spec_vec_is_empty<T>(vec: &Vec<T>) -> bool {
+    Vec::is_empty(vec)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust::requires(true)]
+#[thrust::ensures(
+    (
+        (*vec).1 > len &&
+        ^vec == ((*vec).0, len)
+    ) || (
+        (*vec).1 <= len &&
+        ^vec == *vec
+    )
+)]
+fn _extern_spec_vec_truncate<T>(vec: &mut Vec<T>, len: usize) {
+    Vec::truncate(vec, len)
+}

tests/ui/fail/vec_1.rs

@@ -0,0 +1,8 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let mut v = Vec::new();
+    v.push(0);
+    assert!(v.len() == 0);
+}

tests/ui/fail/vec_2.rs

@@ -0,0 +1,10 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let mut v = Vec::new();
+    v.push(0);
+    v[0] += 1;
+    assert!(v.pop().unwrap() == 1);
+    assert!(v.pop().unwrap() == 1);
+}

tests/ui/fail/vec_3.rs

@@ -0,0 +1,14 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let mut v = Vec::new();
+    v.push(0);
+    v.push(1);
+    v.push(2);
+    assert!(v.len() == 2);
+    v.truncate(1);
+    assert!(v[1] == 0);
+    v.clear();
+    assert!(v.len() == 1);
+}

tests/ui/pass/vec_1.rs

@@ -0,0 +1,9 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let mut v = Vec::new();
+    v.push(0);
+    assert!(v.len() == 1);
+    assert!(v[0] == 0);
+}

tests/ui/pass/vec_2.rs

@@ -0,0 +1,11 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let mut v = Vec::new();
+    v.push(0);
+    v[0] += 1;
+    v.push(1);
+    assert!(v.pop().unwrap() == 1);
+    assert!(v.pop().unwrap() == 1);
+}

tests/ui/pass/vec_3.rs

@@ -0,0 +1,14 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let mut v = Vec::new();
+    v.push(0);
+    v.push(1);
+    v.push(2);
+    assert!(v.len() == 3);
+    v.truncate(1);
+    assert!(v[0] == 0);
+    v.clear();
+    assert!(v.len() == 0);
+}