Move attribute processing functions to kani_middle. (rust-lang#1838)

Co-authored-by: Celina G. Val <[email protected]>

Author: aaronbembenek-aws

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -4,11 +4,11 @@
 //! This file contains functions related to codegenning MIR functions into gotoc
 
 use crate::codegen_cprover_gotoc::GotocCtx;
+use crate::kani_middle::attributes::{extract_integer_argument, partition_kanitool_attributes};
 use cbmc::goto_program::{Expr, Stmt, Symbol};
 use cbmc::InternString;
 use kani_metadata::HarnessMetadata;
-use rustc_ast::ast;
-use rustc_ast::{Attribute, LitKind};
+use rustc_ast::Attribute;
 use rustc_hir::def::DefKind;
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir::{HasLocalDecls, Local};
@@ -436,59 +436,3 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 }
-
-/// If the attribute is named `kanitool::name`, this extracts `name`
-fn kanitool_attr_name(attr: &ast::Attribute) -> Option<String> {
-    match &attr.kind {
-        ast::AttrKind::Normal(normal) => {
-            let segments = &normal.item.path.segments;
-            if (!segments.is_empty()) && segments[0].ident.as_str() == "kanitool" {
-                Some(segments[1].ident.as_str().to_string())
-            } else {
-                None
-            }
-        }
-        _ => None,
-    }
-}
-
-/// Partition all the attributes into two buckets, proof_attributes and other_attributes
-fn partition_kanitool_attributes(
-    all_attributes: &[Attribute],
-) -> (Vec<&Attribute>, Vec<(String, &Attribute)>) {
-    let mut proof_attributes = vec![];
-    let mut other_attributes = vec![];
-
-    for attr in all_attributes {
-        // Get the string the appears after "kanitool::" in each attribute string.
-        // Ex - "proof" | "unwind" etc.
-        if let Some(attribute_string) = kanitool_attr_name(attr).as_deref() {
-            if attribute_string == "proof" {
-                proof_attributes.push(attr);
-            } else {
-                other_attributes.push((attribute_string.to_string(), attr));
-            }
-        }
-    }
-
-    (proof_attributes, other_attributes)
-}
-
-/// Extracts the integer value argument from the attribute provided
-/// For example, `unwind(8)` return `Some(8)`
-fn extract_integer_argument(attr: &Attribute) -> Option<u128> {
-    // Vector of meta items , that contain the arguments given the attribute
-    let attr_args = attr.meta_item_list()?;
-    // Only extracts one integer value as argument
-    if attr_args.len() == 1 {
-        let x = attr_args[0].literal()?;
-        match x.kind {
-            LitKind::Int(y, ..) => Some(y),
-            _ => None,
-        }
-    }
-    // Return none if there are no attributes or if there's too many attributes
-    else {
-        None
-    }
-}

kani-compiler/src/kani_middle/attributes.rs

@@ -0,0 +1,61 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! This module contains code for processing Rust attributes (like `kani::proof`).
+
+use rustc_ast::{AttrKind, Attribute, LitKind};
+
+/// Partition all the attributes into two buckets, proof_attributes and other_attributes
+pub fn partition_kanitool_attributes(
+    all_attributes: &[Attribute],
+) -> (Vec<&Attribute>, Vec<(String, &Attribute)>) {
+    let mut proof_attributes = vec![];
+    let mut other_attributes = vec![];
+
+    for attr in all_attributes {
+        // Get the string the appears after "kanitool::" in each attribute string.
+        // Ex - "proof" | "unwind" etc.
+        if let Some(attribute_string) = kanitool_attr_name(attr).as_deref() {
+            if attribute_string == "proof" {
+                proof_attributes.push(attr);
+            } else {
+                other_attributes.push((attribute_string.to_string(), attr));
+            }
+        }
+    }
+
+    (proof_attributes, other_attributes)
+}
+
+/// Extracts the integer value argument from the attribute provided
+/// For example, `unwind(8)` return `Some(8)`
+pub fn extract_integer_argument(attr: &Attribute) -> Option<u128> {
+    // Vector of meta items , that contain the arguments given the attribute
+    let attr_args = attr.meta_item_list()?;
+    // Only extracts one integer value as argument
+    if attr_args.len() == 1 {
+        let x = attr_args[0].literal()?;
+        match x.kind {
+            LitKind::Int(y, ..) => Some(y),
+            _ => None,
+        }
+    }
+    // Return none if there are no attributes or if there's too many attributes
+    else {
+        None
+    }
+}
+
+/// If the attribute is named `kanitool::name`, this extracts `name`
+fn kanitool_attr_name(attr: &Attribute) -> Option<String> {
+    match &attr.kind {
+        AttrKind::Normal(normal) => {
+            let segments = &normal.item.path.segments;
+            if (!segments.is_empty()) && segments[0].ident.as_str() == "kanitool" {
+                Some(segments[1].ident.as_str().to_string())
+            } else {
+                None
+            }
+        }
+        _ => None,
+    }
+}

kani-compiler/src/kani_middle/mod.rs

@@ -2,4 +2,5 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! This module contains code that are backend agnostic. For example, MIR analysis
 //! and transformations.
+pub mod attributes;
 pub mod reachability;