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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107

mod item_impl;
mod item_struct;

use syn::{GenericArgument, Item, Path};

use crate::{
    util::{create_angle_bracketed_path_arguments, create_type_path},
    wir::{
        IntoSyn, WDescription, WElementaryType, WExpr, WExprCall, WGeneralType, WIdent,
        WItemImplTrait, WPanicResult, WPanicResultType, WPath, WSsaLocal, WStmt, WType, YConverted,
        YStage, ZAssignTypes, ZIfPolarity,
    },
};

use self::{
    item_impl::{preprocess_item_impl, process_item_impl},
    item_struct::process_item_struct,
};

#[derive(Clone, Debug, Hash)]
pub struct YAbstr;

#[derive(Clone, Debug, Hash)]
pub struct ZAbstrIfPolarity(pub bool);

impl IntoSyn<Path> for ZAbstrIfPolarity {
    fn into_syn(self) -> Path {
        if self.0 {
            syn_path::path!(::mck::forward::Test::can_be_true)
        } else {
            syn_path::path!(::mck::forward::Test::can_be_false)
        }
    }
}

impl ZIfPolarity for ZAbstrIfPolarity {}

#[derive(Clone, Debug, Hash)]
pub struct ZAbstr;

impl ZAssignTypes for ZAbstr {
    type Stmt = WStmt<ZAbstr>;
    type FundamentalType = WElementaryType;
    type AssignLeft = WIdent;
    type AssignRight = WExpr<WExprCall>;
    type IfPolarity = ZAbstrIfPolarity;
}

impl YStage for YAbstr {
    type AssignTypes = ZAbstr;
    type InputType = WType<WElementaryType>;
    type OutputType = WPanicResultType<WElementaryType>;
    type FnResult = WPanicResult;
    type Local = WSsaLocal<WGeneralType<WElementaryType>>;
    type ItemImplTrait = WAbstrItemImplTrait;
}

#[derive(Clone, Debug, Hash)]
pub struct WAbstrItemImplTrait {
    pub machine_type: WPath,
    pub trait_: WItemImplTrait,
}

impl IntoSyn<Path> for WAbstrItemImplTrait {
    fn into_syn(self) -> Path {
        let mut trait_path = self.trait_.into_syn();
        trait_path.segments.last_mut().unwrap().arguments = create_angle_bracketed_path_arguments(
            false,
            vec![GenericArgument::Type(create_type_path(
                self.machine_type.clone().into(),
            ))],
            self.machine_type.span(),
        );
        trait_path
    }
}

pub(crate) fn create_abstract_description(
    description: WDescription<YConverted>,
) -> (WDescription<YAbstr>, Vec<Item>) {
    let mut machine_types = Vec::new();
    for item_impl in description.impls.iter() {
        if let Some(ty) = preprocess_item_impl(item_impl) {
            machine_types.push(ty);
        }
    }

    let mut misc_items = Vec::new();

    let mut abstract_description = WDescription::<YAbstr> {
        structs: Vec::new(),
        impls: Vec::new(),
    };

    for item_struct in description.structs {
        let (item_struct, other_impls) = process_item_struct(item_struct);
        abstract_description.structs.push(item_struct);
        misc_items.extend(other_impls.into_iter().map(Item::Impl));
    }

    for item_impl in description.impls {
        let item_impls = process_item_impl(item_impl, &machine_types);
        abstract_description.impls.extend(item_impls);
    }

    (abstract_description, misc_items)
}