machine_check_common/iir/
description.rs

1use std::fmt::Debug;
2
3use mck::refin::{Boolean, RArray, RBitvector, RefinementDomain, RefinementValue};
4
5use indexmap::IndexMap;
6use serde::{Deserialize, Serialize};
7
8use crate::iir::{
9    context::IContext,
10    func::{IFn, IFnDeclaration},
11    path::IIdent,
12    ty::IElementaryType,
13};
14
15#[derive(Clone, Debug, Serialize, Deserialize)]
16pub struct IMachine {
17    pub machine: IStructId,
18    pub init: IFnId,
19    pub next: IFnId,
20
21    pub input: IStructId,
22    pub param: IStructId,
23    pub state: IStructId,
24
25    pub description: IDescription,
26}
27
28#[derive(Clone, Debug, Serialize, Deserialize)]
29pub struct IDescription {
30    pub structs: IndexMap<IIdent, IStruct>,
31}
32
33#[derive(Clone, Copy, Hash, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
34pub struct IStructId(pub usize);
35
36#[derive(Clone, Debug, Serialize, Deserialize)]
37pub struct IStructDeclaration {
38    pub fields: IndexMap<IIdent, IElementaryType>,
39    pub fns: IndexMap<(ITrait, IIdent), IFnDeclaration>,
40}
41
42#[derive(Clone, Debug, Serialize, Deserialize)]
43pub struct IStruct {
44    pub fields: IndexMap<IIdent, IElementaryType>,
45    pub fns: IndexMap<(ITrait, IIdent), IFn>,
46}
47
48#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
49pub enum ITrait {
50    Inherent,
51    Machine,
52}
53
54#[derive(Clone, Debug, Serialize, Deserialize, Default)]
55pub struct IImpl {
56    fns: IndexMap<IIdent, IFn>,
57}
58
59impl IMachine {
60    pub fn machine(&self) -> &IStruct {
61        self.description.struct_with_id(self.machine)
62    }
63
64    pub fn input(&self) -> &IStruct {
65        self.description.struct_with_id(self.input)
66    }
67
68    pub fn param(&self) -> &IStruct {
69        self.description.struct_with_id(self.param)
70    }
71
72    pub fn state(&self) -> &IStruct {
73        self.description.struct_with_id(self.state)
74    }
75
76    pub fn init(&self) -> &IFn {
77        self.description.fn_with_id(self.init)
78    }
79    pub fn next(&self) -> &IFn {
80        self.description.fn_with_id(self.next)
81    }
82}
83
84impl IDescription {
85    pub fn context(&self) -> IContext {
86        IContext {
87            structs: Some(&self.structs),
88        }
89    }
90
91    pub fn struct_with_id(&self, id: IStructId) -> &IStruct {
92        self.structs
93            .get_index(id.0)
94            .expect("Struct with given id should exist")
95            .1
96    }
97
98    pub fn fn_with_id(&self, id: IFnId) -> &IFn {
99        self.struct_with_id(id.struct_id)
100            .fns
101            .get_index(id.fn_index)
102            .expect("Call with given id should exist")
103            .1
104    }
105}
106
107impl IStruct {
108    pub fn clean_refin(&self, description: &IDescription) -> RefinementValue {
109        let mut result = Vec::new();
110        for field_ty in self.fields.values() {
111            let field_result = match field_ty {
112                IElementaryType::Bitvector(width) => {
113                    RefinementValue::Bitvector(RBitvector::new_unmarked(*width))
114                }
115                IElementaryType::Array(array) => RefinementValue::Array(RArray::new_unmarked(
116                    array.index_width,
117                    array.element_width,
118                )),
119                IElementaryType::Boolean => RefinementValue::Boolean(Boolean::new_unmarked()),
120                IElementaryType::Struct(struct_id) => {
121                    let iir_struct = description.struct_with_id(*struct_id);
122                    iir_struct.clean_refin(description)
123                }
124            };
125            result.push(field_result)
126        }
127
128        RefinementValue::Struct(result)
129    }
130
131    pub fn dirty_refin(&self, description: &IDescription) -> RefinementValue {
132        let mut result = Vec::new();
133        for field_ty in self.fields.values() {
134            let field_result = match field_ty {
135                IElementaryType::Bitvector(width) => {
136                    RefinementValue::Bitvector(RBitvector::new_marked_unimportant(*width))
137                }
138                IElementaryType::Array(array) => RefinementValue::Array(
139                    RArray::new_marked_unimportant(array.index_width, array.element_width),
140                ),
141                IElementaryType::Boolean => {
142                    RefinementValue::Boolean(Boolean::new_marked_unimportant())
143                }
144                IElementaryType::Struct(struct_id) => {
145                    let iir_struct = description.struct_with_id(*struct_id);
146                    iir_struct.dirty_refin(description)
147                }
148            };
149            result.push(field_result)
150        }
151
152        RefinementValue::Struct(result)
153    }
154
155    pub fn into_declaration(self) -> IStructDeclaration {
156        let fns = self
157            .fns
158            .into_iter()
159            .map(|func| (func.0, func.1.into_declaration()))
160            .collect();
161
162        IStructDeclaration {
163            fields: self.fields,
164            fns,
165        }
166    }
167}
168
169impl Debug for IStructId {
170    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
171        write!(f, "${}", self.0)
172    }
173}
174
175#[derive(Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
176pub struct IFnId {
177    pub struct_id: IStructId,
178    pub fn_index: usize,
179}
180
181impl Debug for IFnId {
182    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
183        write!(f, "{:?}::{}", self.struct_id, self.fn_index)
184    }
185}
machine_check_common/iir/description.rs

machine_check_common/iir/
description.rs
