hax_rust_engine/
attributes.rs

1//! Work with hax attributes.
2
3use std::collections::HashMap;
4
5use hax_lib_macros_types::{AssociationRole, AttrPayload, ItemUid};
6
7use crate::ast::diagnostics::{Context, DiagnosticInfo, DiagnosticInfoKind};
8
9use super::ast::*;
10use visitors::AstVisitorMut;
11
12/// A graph of items connected via the hax attribute [`AttrPayload::AssociatedItem`] and UUIDs.
13#[derive(Clone)]
14pub struct LinkedItemGraph {
15    items: HashMap<ItemUid, Item>,
16    context: Context,
17}
18
19impl Default for LinkedItemGraph {
20    fn default() -> Self {
21        Self {
22            items: Default::default(),
23            context: Context::Unknown,
24        }
25    }
26}
27
28/// Get an iterator over hax attributes contained in the given attributes.
29pub fn hax_attributes(attrs: &Attributes) -> impl Iterator<Item = &AttrPayload> {
30    attrs.iter().flat_map(|attr| match &attr.kind {
31        AttributeKind::Hax(attr_payload) => Some(attr_payload),
32        _ => None,
33    })
34}
35
36fn uuid(context: Context, item: &Item) -> Option<ItemUid> {
37    let mut uuids = hax_attributes(&item.meta.attributes).flat_map(|attr| match attr {
38        AttrPayload::Uid(item_uid) => Some(item_uid),
39        _ => None,
40    });
41    let uuid = uuids.next()?;
42    if let Some(other) = uuids.next() {
43        emit_assertion_failure(
44            context,
45            item.span(),
46            format!(
47                "Found more than one UUID hax attribute on this item. The two first UUIDs are {uuid} and {other}."
48            ),
49        );
50        None
51    } else {
52        Some(uuid.clone())
53    }
54}
55
56fn emit_assertion_failure(context: Context, span: span::Span, message: impl Into<String>) {
57    DiagnosticInfo {
58        context,
59        span,
60        kind: DiagnosticInfoKind::AssertionFailure {
61            details: message.into(),
62        },
63    }
64    .emit();
65}
66
67impl std::fmt::Debug for LinkedItemGraph {
68    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
69        f.debug_struct("LinkedItemGraph")
70            .field(
71                "items",
72                &self
73                    .items
74                    .iter()
75                    .map(|(id, item)| (id.to_string(), item.ident.to_debug_string()))
76                    .collect::<Vec<_>>(),
77            )
78            .field("context", &self.context)
79            .finish()
80    }
81}
82
83impl LinkedItemGraph {
84    /// Clone items marked with UUIDs attributes to build a graph of linked items.
85    /// This graph clones the items that represent linked items: e.g. pre and post conditions.
86    pub fn new(items: &[Item], context: Context) -> Self {
87        Self {
88            items: HashMap::from_iter(
89                items
90                    .iter()
91                    .filter_map(|item| Some((uuid(context.clone(), item)?, item.clone()))),
92            ),
93            context,
94        }
95    }
96
97    fn emit_assertion_failure(&self, span: span::Span, message: impl Into<String>) {
98        emit_assertion_failure(self.context.clone(), span, message)
99    }
100
101    fn emit_unimplemented(&self, span: span::Span, issue_id: u32, message: impl Into<String>) {
102        DiagnosticInfo {
103            context: self.context.clone(),
104            span,
105            kind: DiagnosticInfoKind::Unimplemented {
106                issue_id: Some(issue_id),
107                details: Some(message.into()),
108            },
109        }
110        .emit();
111    }
112
113    /// Given a graph and an item `item`, returns an iterator of the various items that are linked with `item`.
114    pub fn linked_items_iter(
115        &self,
116        item: &impl HasMetadata,
117    ) -> impl Iterator<Item = (AssociationRole, Result<&Item, DiagnosticInfo>)> {
118        let item_attributes = &item.metadata().attributes;
119        hax_attributes(item_attributes).flat_map(move |attr| match attr {
120            AttrPayload::AssociatedItem { role, item: target } => {
121                let target = self.items.get(target).map(Ok).unwrap_or_else(|| {
122                    Err(DiagnosticInfo {
123                        context: self.context.clone(),
124                        span: item.span(),
125                        kind: DiagnosticInfoKind::AssertionFailure {
126                            details: format!("An item linked via hax attributes could not be found. The UUID is {target:?}. The graph is {:#?}.", self),
127                        },
128                    })
129                });
130                Some((*role, target))
131            }
132            _ => None,
133        })
134    }
135
136    /// Returns the items linked to a given item.
137    pub fn linked_items(
138        &self,
139        item: &impl HasMetadata,
140    ) -> HashMap<AssociationRole, Vec<Result<&Item, DiagnosticInfo>>> {
141        let mut map: HashMap<AssociationRole, Vec<_>> = HashMap::new();
142        for (role, item) in self.linked_items_iter(item) {
143            map.entry(role).or_default().push(item);
144        }
145        map
146    }
147
148    /// Returns the precondition, postcondition and decreases clause, if any, for a given item.
149    /// When operating on a linked function, `self_id` is the local identifier of `self`.
150    pub fn fn_like_linked_expressions(
151        &self,
152        item: &impl HasMetadata,
153        self_id: Option<identifiers::LocalId>,
154    ) -> FnLikeAssocatedExpressions {
155        let assoc_items = self.linked_items(item);
156        let get = |role| {
157            assoc_items
158                .get(&role)
159                .iter()
160                .flat_map(|vec| vec.iter())
161                .flat_map(|item| match item {
162                    Ok(item) => Some(item),
163                    Err(err) => {
164                        err.emit();
165                        None
166                    }
167                })
168                .map(|item| extract_expr(&self.context, item, self_id.clone()))
169                .collect::<Vec<_>>()
170        };
171        let precondition = {
172            let mut preconditions = get(AssociationRole::Requires).into_iter();
173            preconditions.next().map(|(e, _)| {
174                for extra in preconditions {
175                    self.emit_unimplemented(extra.0.span(), 1270, "multiple pre-conditions");
176                }
177                e
178            })
179        };
180        let decreases = {
181            let mut decreases = get(AssociationRole::Decreases).into_iter();
182            decreases.next().map(|(e, _)| {
183                for extra in decreases {
184                    self.emit_unimplemented(extra.0.span(), 1270, "multiple decreases");
185                }
186                e
187            })
188        };
189        let postcondition = {
190            let mut postconditions = get(AssociationRole::Ensures).into_iter();
191            postconditions.next().and_then(|(e, params)| {
192                for extra in postconditions {
193                    self.emit_unimplemented(extra.0.span(), 1270, "multiple post-conditions");
194                }
195                if let Some(last_param) = params.last() {
196                    Some(Postcondition {
197                        result_binder: last_param.pat.clone(),
198                        body: e.clone(),
199                    })
200                } else {
201                    self.emit_assertion_failure(
202                        e.span(),
203                        "hax ensures attribute: could not find output binder",
204                    );
205                    None
206                }
207            })
208        };
209        FnLikeAssocatedExpressions {
210            decreases,
211            precondition,
212            postcondition,
213        }
214    }
215}
216
217fn extract_expr<'a>(
218    context: &Context,
219    item: &'a Item,
220    self_id: Option<identifiers::LocalId>,
221) -> (Expr, Vec<&'a Param>) {
222    let ItemKind::Fn { body, params, .. } = item.kind() else {
223        return (
224            ExprKind::Error(ErrorNode::assertion_failure(
225                item.clone(),
226                context.clone(),
227                "Expected an function",
228            ))
229            .into_expr(item.span(), Ty::prop(), vec![]),
230            vec![],
231        );
232    };
233    let mut body = body.clone();
234    if let Some(self_id) = self_id
235        && let [maybe_self, ..] = params.as_slice()
236        && let PatKind::Binding {
237            var, sub_pat: None, ..
238        } = &*maybe_self.pat.kind
239    {
240        // Here, we expect `self_id` is `self`, thus we cannot have any shadowing.
241        utils::mappers::SubstLocalIds::one(var.clone(), self_id.clone()).visit(&mut body)
242    }
243    (body, params.iter().collect())
244}
245
246/// A postcondition.
247///
248/// ## Example
249/// The expression `result != x` in the following is a postcondition.
250/// Note that `result` is an extra binder that represent the result of `f`, whose type is `u8` in this case: the return type of `f`.
251///
252/// ```rust
253/// #[hax_lib::ensures(|result| result != x)]
254/// fn f(x: u8) -> u8 { x.wrapping_add(1) }
255/// ```
256pub struct Postcondition {
257    /// In the example, this is `|result|`.
258    pub result_binder: Pat,
259    /// The formula of the postcondition, `result != x` in the example.
260    pub body: Expr,
261}
262
263/// The various linked expressions one can usually find on a (linked or not) function.
264pub struct FnLikeAssocatedExpressions {
265    /// A decreases clause, see [`hax_lib::decreases`]
266    pub decreases: Option<Expr>,
267    /// A decreases clause, see [`hax_lib::decreases`]
268    pub precondition: Option<Expr>,
269    /// A decreases clause, see [`hax_lib::decreases`]
270    pub postcondition: Option<Postcondition>,
271}
hax_rust_engine/attributes.rs

hax_rust_engine/
attributes.rs
