machine-check-machine 0.7.1

Utility crate for the formal verification tool machine-check
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77

use syn::{Path, PathArguments};

use crate::{
    into_wir::Error,
    wir::{WIdent, WPath, WPathSegment, WSpan},
};

pub fn fold_path(path: Path, self_ty: Option<&WPath>) -> Result<WPath, Error> {
    let path_span = WSpan::from_syn(&path);

    let mut segments = Vec::new();

    for segment in path.segments {
        let PathArguments::None = segment.arguments else {
            return Err(Error::unsupported_syn_construct(
                "Generics here",
                &segment.arguments,
            ));
        };
        segments.push(WPathSegment {
            ident: WIdent::from_syn_ident(segment.ident),
        });
    }

    // for now, disallow paths that can break out (super / crate / $crate)
    for segment in segments.iter() {
        if segment.ident.name() == "super"
            || segment.ident.name() == "crate"
            || segment.ident.name() == "$crate"
        {
            return Err(Error::unsupported_construct(
                "Path segment super / crate / $crate",
                WSpan::from_span(segment.ident.span()),
            ));
        }
    }

    // disallow global paths to any other crates than machine_check and std
    let mut leading_colon = path.leading_colon.map(|leading| WSpan::from_syn(&leading));

    if leading_colon.is_some() {
        let crate_segment = segments
            .first()
            .expect("Global path should have at least one segment");
        let crate_ident = &crate_segment.ident;
        if crate_ident.name() != "machine_check" && crate_ident.name() != "std" {
            return Err(Error::unsupported_construct(
                "Absolute paths not starting with 'machine_check' or 'std'",
                path_span,
            ));
        }
    } else {
        // replace leading Self if possible
        if let Some(self_ty) = self_ty {
            if !segments.is_empty() && segments[0].ident.name() == "Self" {
                // set replaced segments spans to the original Self span
                let first_segment_span = segments[0].ident.span();
                let mut self_replacement = self_ty.clone();
                for self_ty_segment in &mut self_replacement.segments {
                    self_ty_segment.ident.set_span(first_segment_span);
                }
                // remove Self and concat
                let mut segments_iter = segments.drain(..);
                let _ = segments_iter.next();
                self_replacement.segments.extend(segments_iter);
                segments = self_replacement.segments;
                // put leading colon according to self type
                leading_colon = self_ty.leading_colon;
            }
        }
    }

    Ok(WPath {
        leading_colon,
        segments,
    })
}