prusti_specs/specifications/
common.rs

1//! Data structures for storing information about specifications.
2//!
3//! Please see the `parser.rs` file for more information about
4//! specifications.
5
6use std::{
7    convert::TryFrom,
8    fmt::{Debug, Display},
9};
10use uuid::Uuid;
11
12#[derive(Clone, Copy, Debug, PartialEq, Eq)]
13/// A specification type.
14pub enum SpecType {
15    /// Precondition of a procedure.
16    Precondition,
17    /// Postcondition of a procedure.
18    Postcondition,
19    /// Loop invariant
20    Invariant,
21    /// Predicate
22    Predicate,
23    /// Struct invariant
24    StructInvariant,
25}
26
27#[derive(Debug)]
28/// A conversion from string into specification type error.
29pub enum TryFromStringError {
30    /// Reported when the string being converted is not one of the
31    /// following: `requires`, `ensures`, `invariant`.
32    UnknownSpecificationType,
33}
34
35impl<'a> TryFrom<&'a str> for SpecType {
36    type Error = TryFromStringError;
37
38    fn try_from(typ: &str) -> Result<SpecType, TryFromStringError> {
39        match typ {
40            "requires" => Ok(SpecType::Precondition),
41            "ensures" => Ok(SpecType::Postcondition),
42            "invariant" => Ok(SpecType::Invariant),
43            "predicate" => Ok(SpecType::Predicate),
44            _ => Err(TryFromStringError::UnknownSpecificationType),
45        }
46    }
47}
48
49#[derive(Debug, Default, PartialEq, Eq, Hash, Clone, Copy, PartialOrd, Ord)]
50/// A unique ID of the specification element such as entire precondition
51/// or postcondition.
52pub struct SpecificationId(Uuid);
53
54/// A reference to a procedure specification.
55#[derive(Debug, Clone, Copy)]
56pub enum SpecIdRef {
57    Precondition(SpecificationId),
58    Postcondition(SpecificationId),
59    Purity(SpecificationId),
60    Pledge {
61        lhs: Option<SpecificationId>,
62        rhs: SpecificationId,
63    },
64    Predicate(SpecificationId),
65    Terminates(SpecificationId),
66}
67
68impl Display for SpecificationId {
69    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
70        write!(
71            f,
72            "{}",
73            self.0.simple().encode_lower(&mut Uuid::encode_buffer()),
74        )
75    }
76}
77
78impl std::convert::TryFrom<String> for SpecificationId {
79    type Error = uuid::Error;
80    fn try_from(value: String) -> Result<Self, Self::Error> {
81        Uuid::parse_str(&value).map(Self)
82    }
83}
84
85impl SpecificationId {
86    pub fn dummy() -> Self {
87        Self(Uuid::nil())
88    }
89}
90
91pub(crate) struct SpecificationIdGenerator {}
92
93impl SpecificationIdGenerator {
94    pub(crate) fn new() -> Self {
95        Self {}
96    }
97    pub(crate) fn generate(&mut self) -> SpecificationId {
98        SpecificationId(Uuid::new_v4())
99    }
100}
101
102pub(crate) fn generate_struct_name(item: &syn::ItemImpl) -> String {
103    let uuid = Uuid::new_v4().simple();
104    let name_ty = generate_name_for_type(&item.self_ty).unwrap_or_default();
105    format!("PrustiStruct{name_ty}_{uuid}")
106}
107
108pub(crate) fn generate_struct_name_for_trait(item: &syn::ItemTrait) -> String {
109    let uuid = Uuid::new_v4().simple();
110    format!("PrustiTrait{}_{}", item.ident, uuid)
111}
112
113fn generate_name_for_type(ty: &syn::Type) -> Option<String> {
114    match ty {
115        syn::Type::Path(ty_path) => Some(String::from_iter(
116            ty_path
117                .path
118                .segments
119                .iter()
120                .map(|seg| seg.ident.to_string()),
121        )),
122        syn::Type::Slice(ty_slice) => {
123            let ty = &*ty_slice.elem;
124            Some(format!("Slice{}", generate_name_for_type(ty)?.as_str()))
125        }
126        _ => None,
127    }
128}
prusti_specs/specifications/common.rs

prusti_specs/specifications/
common.rs
