Add unit tests for all types of volume objects (#342)

Signed-off-by: ZichengMa <[email protected]>

src/kubernetes_api_objects/volume.rs

@@ -315,6 +315,16 @@ impl ConfigMapProjection {
         }
     }
 
+    #[verifier(external_body)]
+    pub fn clone(&self) -> (config_map_projection: ConfigMapProjection)
+        ensures
+            config_map_projection@ == self@,
+    {
+        ConfigMapProjection {
+            inner: self.inner.clone(),
+        }
+    }
+
     #[verifier(external_body)]
     pub fn set_name(&mut self, name: String)
         ensures
@@ -357,6 +367,16 @@ impl SecretProjection {
         }
     }
 
+    #[verifier(external_body)]
+    pub fn clone(&self) -> (secret_projection: SecretProjection)
+        ensures
+            secret_projection@ == self@,
+    {
+        SecretProjection {
+            inner: self.inner.clone(),
+        }
+    }
+
     #[verifier(external_body)]
     pub fn set_name(&mut self, name: String)
         ensures
@@ -513,6 +533,16 @@ impl ObjectFieldSelector {
         }
     }
 
+    #[verifier(external_body)]
+    pub fn clone(&self) -> (object_field_selector: ObjectFieldSelector)
+        ensures
+            object_field_selector@ == self@,
+    {
+        ObjectFieldSelector {
+            inner: self.inner.clone(),
+        }
+    }
+
     pub fn new_with(api_version: String, field_path: String) -> (object_field_selector: ObjectFieldSelector)
         ensures
             object_field_selector@ == ObjectFieldSelectorView::default().set_api_version(api_version@).set_field_path(field_path@),

src/unit_tests/kubernetes_api_objects/configmap_projection.rs

@@ -0,0 +1,73 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+use crate::kubernetes_api_objects::container::*;
+use crate::kubernetes_api_objects::object_meta::*;
+use crate::kubernetes_api_objects::pod::*;
+use crate::kubernetes_api_objects::resource::*;
+use crate::kubernetes_api_objects::volume::*;
+use crate::vstd_ext::string_map::*;
+use vstd::prelude::*;
+use vstd::string::*;
+
+verus! {
+// Tests for configmap projecion
+#[test]
+#[verifier(external)]
+pub fn test_default() {
+    let config_map_projection = ConfigMapProjection::default();
+    assert_eq!(config_map_projection.into_kube(), deps_hack::k8s_openapi::api::core::v1::ConfigMapProjection::default());
+}
+
+#[test]
+#[verifier(external)]
+pub fn test_set_name() {
+    let mut config_map_projection = ConfigMapProjection::default();
+    config_map_projection.set_name(new_strlit("name").to_string());
+    assert_eq!("name".to_string(), config_map_projection.into_kube().name.unwrap());
+}
+
+#[test]
+#[verifier(external)]
+pub fn test_set_items() {
+    let mut config_map_projection = ConfigMapProjection::default();
+    let key_to_paths_gen = || {
+        let mut key_to_path_1 = KeyToPath::default();
+        let mut key_to_path_2 = KeyToPath::default();
+        let mut key_to_paths = Vec::new();
+        key_to_path_1.set_key(new_strlit("key1").to_string());
+        key_to_path_1.set_path(new_strlit("path1").to_string());
+        key_to_path_2.set_key(new_strlit("key2").to_string());
+        key_to_path_2.set_path(new_strlit("path2").to_string());
+        key_to_paths.push(key_to_path_1);
+        key_to_paths.push(key_to_path_2);
+        key_to_paths
+    };
+    config_map_projection.set_items(key_to_paths_gen());
+    assert_eq!(
+        key_to_paths_gen()
+            .into_iter()
+            .map(|s: KeyToPath| s.into_kube())
+            .collect::<Vec<_>>(),
+        config_map_projection.into_kube().items.unwrap()
+    );
+}
+
+#[test]
+#[verifier(external)]
+pub fn test_clone() {
+    let mut config_map_projection = ConfigMapProjection::default();
+    config_map_projection.set_name(new_strlit("name").to_string());
+    let mut key_to_path_1 = KeyToPath::default();
+    let mut key_to_path_2 = KeyToPath::default();
+    let mut key_to_paths = Vec::new();
+    key_to_path_1.set_key(new_strlit("key1").to_string());
+    key_to_path_1.set_path(new_strlit("path1").to_string());
+    key_to_path_2.set_key(new_strlit("key2").to_string());
+    key_to_path_2.set_path(new_strlit("path2").to_string());
+    key_to_paths.push(key_to_path_1);
+    key_to_paths.push(key_to_path_2);
+    config_map_projection.set_items(key_to_paths);
+    let config_map_projection_clone = config_map_projection.clone();
+    assert_eq!(config_map_projection.into_kube(), config_map_projection_clone.into_kube());
+}
+}

src/unit_tests/kubernetes_api_objects/configmap_volume_source.rs

@@ -0,0 +1,28 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+use crate::kubernetes_api_objects::container::*;
+use crate::kubernetes_api_objects::object_meta::*;
+use crate::kubernetes_api_objects::pod::*;
+use crate::kubernetes_api_objects::resource::*;
+use crate::kubernetes_api_objects::volume::*;
+use crate::vstd_ext::string_map::*;
+use vstd::prelude::*;
+use vstd::string::*;
+
+verus! {
+// Tests for config map volume source
+#[test]
+#[verifier(external)]
+pub fn test_default() {
+    let config_map_volume_source = ConfigMapVolumeSource::default();
+    assert_eq!(config_map_volume_source.into_kube(), deps_hack::k8s_openapi::api::core::v1::ConfigMapVolumeSource::default());
+}
+
+#[test]
+#[verifier(external)]
+pub fn test_set_name() {
+    let mut config_map_volume_source = ConfigMapVolumeSource::default();
+    config_map_volume_source.set_name(new_strlit("name").to_string());
+    assert_eq!("name".to_string(), config_map_volume_source.into_kube().name.unwrap());
+}
+}

src/unit_tests/kubernetes_api_objects/downwardapi_volume_file.rs

@@ -0,0 +1,33 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+use crate::kubernetes_api_objects::container::*;
+use crate::kubernetes_api_objects::object_meta::*;
+use crate::kubernetes_api_objects::pod::*;
+use crate::kubernetes_api_objects::resource::*;
+use crate::kubernetes_api_objects::volume::*;
+use crate::vstd_ext::string_map::*;
+use vstd::prelude::*;
+use vstd::string::*;
+
+verus! {
+// Tests for downwardAPI volume file
+#[test]
+#[verifier(external)]
+pub fn test_default() {
+    let downward_api_volume_file = DownwardAPIVolumeFile::default();
+    assert_eq!(downward_api_volume_file.into_kube(), deps_hack::k8s_openapi::api::core::v1::DownwardAPIVolumeFile::default());
+}
+
+#[test]
+#[verifier(external)]
+pub fn test_set_field_ref() {
+    let mut downward_api_volume_file = DownwardAPIVolumeFile::default();
+    let mut object_field_selector = ObjectFieldSelector::default();
+    object_field_selector.set_field_path(new_strlit("field_path").to_string());
+    downward_api_volume_file.set_field_ref(object_field_selector.clone());
+    assert_eq!(
+        object_field_selector.into_kube(),
+        downward_api_volume_file.into_kube().field_ref.unwrap()
+    );
+}
+}

src/unit_tests/kubernetes_api_objects/downwardapi_volume_source.rs

@@ -0,0 +1,44 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+use crate::kubernetes_api_objects::container::*;
+use crate::kubernetes_api_objects::object_meta::*;
+use crate::kubernetes_api_objects::pod::*;
+use crate::kubernetes_api_objects::resource::*;
+use crate::kubernetes_api_objects::volume::*;
+use crate::vstd_ext::string_map::*;
+use vstd::prelude::*;
+use vstd::string::*;
+
+verus! {
+// Tests for downwardAPI volume source
+#[test]
+#[verifier(external)]
+pub fn test_default() {
+    let downward_api_volume_source = DownwardAPIVolumeSource::default();
+    assert_eq!(downward_api_volume_source.into_kube(), deps_hack::k8s_openapi::api::core::v1::DownwardAPIVolumeSource::default());
+}
+
+#[test]
+#[verifier(external)]
+pub fn test_set_items() {
+    let mut downward_api_volume_source = DownwardAPIVolumeSource::default();
+    let downward_api_volume_file_gen = || {
+        let mut downward_api_volume_file_1 = DownwardAPIVolumeFile::default();
+        let mut downward_api_volume_file_2 = DownwardAPIVolumeFile::default();
+        let mut downward_api_volume_files = Vec::new();
+        downward_api_volume_file_1.set_path(new_strlit("path1").to_string());
+        downward_api_volume_file_2.set_path(new_strlit("path2").to_string());
+        downward_api_volume_files.push(downward_api_volume_file_1);
+        downward_api_volume_files.push(downward_api_volume_file_2);
+        downward_api_volume_files
+    };
+    downward_api_volume_source.set_items(downward_api_volume_file_gen());
+    assert_eq!(
+        downward_api_volume_file_gen()
+            .into_iter()
+            .map(|s: DownwardAPIVolumeFile| s.into_kube())
+            .collect::<Vec<_>>(),
+        downward_api_volume_source.into_kube().items.unwrap()
+    );
+}
+}

src/unit_tests/kubernetes_api_objects/hostpath_volume_source.rs

@@ -0,0 +1,28 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+use crate::kubernetes_api_objects::container::*;
+use crate::kubernetes_api_objects::object_meta::*;
+use crate::kubernetes_api_objects::pod::*;
+use crate::kubernetes_api_objects::resource::*;
+use crate::kubernetes_api_objects::volume::*;
+use crate::vstd_ext::string_map::*;
+use vstd::prelude::*;
+use vstd::string::*;
+
+verus! {
+// Tests for host path volume source
+#[test]
+#[verifier(external)]
+pub fn test_default() {
+    let host_path_volume_source = HostPathVolumeSource::default();
+    assert_eq!(host_path_volume_source.into_kube(), deps_hack::k8s_openapi::api::core::v1::HostPathVolumeSource::default());
+}
+
+#[test]
+#[verifier(external)]
+pub fn test_set_path() {
+    let mut host_path_volume_source = HostPathVolumeSource::default();
+    host_path_volume_source.set_path(new_strlit("path").to_string());
+    assert_eq!("path".to_string(), host_path_volume_source.into_kube().path);
+}
+}

src/unit_tests/kubernetes_api_objects/key_to_path.rs

@@ -0,0 +1,36 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+use crate::kubernetes_api_objects::container::*;
+use crate::kubernetes_api_objects::object_meta::*;
+use crate::kubernetes_api_objects::pod::*;
+use crate::kubernetes_api_objects::resource::*;
+use crate::kubernetes_api_objects::volume::*;
+use crate::vstd_ext::string_map::*;
+use vstd::prelude::*;
+use vstd::string::*;
+
+verus! {
+// Tests for key to path
+#[test]
+#[verifier(external)]
+pub fn test_default() {
+    let key_to_path = KeyToPath::default();
+    assert_eq!(key_to_path.into_kube(), deps_hack::k8s_openapi::api::core::v1::KeyToPath::default());
+}
+
+#[test]
+#[verifier(external)]
+pub fn test_set_key() {
+    let mut key_to_path = KeyToPath::default();
+    key_to_path.set_key(new_strlit("key").to_string());
+    assert_eq!("key".to_string(), key_to_path.into_kube().key);
+}
+
+#[test]
+#[verifier(external)]
+pub fn test_set_path() {
+    let mut key_to_path = KeyToPath::default();
+    key_to_path.set_path(new_strlit("path").to_string());
+    assert_eq!("path".to_string(), key_to_path.into_kube().path);
+}
+}

src/unit_tests/kubernetes_api_objects/mod.rs

@@ -1,10 +1,16 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
 pub mod config_map;
+pub mod configmap_projection;
+pub mod configmap_volume_source;
 pub mod container;
+pub mod downwardapi_volume_file;
+pub mod downwardapi_volume_source;
+pub mod empty_dir_volume_source;
 pub mod env_var;
 pub mod env_var_source;
 pub mod execaction;
+pub mod hostpath_volume_source;
 pub mod lifecycle;
 pub mod lifecycle_handler;
 pub mod object_field_selector;
@@ -13,6 +19,12 @@ pub mod pod;
 pub mod pod_spec;
 pub mod pod_template_spec;
 pub mod probe;
+pub mod projected_volume_source;
 pub mod resource_requirements;
+pub mod secret_projection;
+pub mod secret_volume_source;
 pub mod tcp_socket_action;
+pub mod volume;
 pub mod volume_mount;
+pub mod volume_projection;
+pub mod key_to_path;

src/unit_tests/kubernetes_api_objects/projected_volume_source.rs

@@ -0,0 +1,44 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+use crate::kubernetes_api_objects::container::*;
+use crate::kubernetes_api_objects::object_meta::*;
+use crate::kubernetes_api_objects::pod::*;
+use crate::kubernetes_api_objects::resource::*;
+use crate::kubernetes_api_objects::volume::*;
+use crate::vstd_ext::string_map::*;
+use vstd::prelude::*;
+use vstd::string::*;
+
+verus! {
+// Tests for projected volume source
+#[test]
+#[verifier(external)]
+pub fn test_default() {
+    let projected_volume_source = ProjectedVolumeSource::default();
+    assert_eq!(projected_volume_source.into_kube(), deps_hack::k8s_openapi::api::core::v1::ProjectedVolumeSource::default());
+}
+
+#[test]
+#[verifier(external)]
+pub fn test_set_resources() {
+    let mut projected_volume_source = ProjectedVolumeSource::default();
+    let volume_projections_gen = || {
+        let mut volume_projection_1 = VolumeProjection::default();
+        let mut volume_projection_2 = VolumeProjection::default();
+        let mut volume_projections = Vec::new();
+        volume_projection_1.set_config_map(ConfigMapProjection::default());
+        volume_projection_2.set_secret(SecretProjection::default());
+        volume_projections.push(volume_projection_1);
+        volume_projections.push(volume_projection_2);
+        volume_projections
+    };
+    projected_volume_source.set_sources(volume_projections_gen());
+    assert_eq!(
+        volume_projections_gen()
+            .into_iter()
+            .map(|s: VolumeProjection| s.into_kube())
+            .collect::<Vec<_>>(),
+        projected_volume_source.into_kube().sources.unwrap()
+    );
+}
+}