machine_check_common/iir/
func.rs

1use std::{collections::BTreeMap, fmt::Debug};
2
3use mck::{abstr::AbstractValue, refin::RefinementValue};
4use serde::{Deserialize, Serialize};
5
6use crate::iir::{
7    context::{IContext, IFnContext},
8    path::IIdent,
9    stmt::IStmt,
10    ty::IElementaryType,
11    variable::{IVarId, IVarInfo},
12    IAbstr, IRefin,
13};
14
15#[derive(Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
16pub struct IBlock {
17    pub stmts: Vec<IStmt>,
18}
19
20#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
21pub struct IFnOutput {
22    pub normal: IVarId,
23    pub panic: IVarId,
24}
25
26#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
27pub struct ISignature {
28    pub ident: IIdent,
29    pub inputs: Vec<IVarId>,
30    pub output: IFnOutput,
31}
32
33#[derive(Clone, Debug, PartialEq, Eq, Hash)]
34pub struct IGlobal {
35    pub ident: IIdent,
36    pub ty: IElementaryType,
37}
38
39#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
40pub struct IFnDeclaration {
41    pub signature: ISignature,
42    pub variables: BTreeMap<IVarId, IVarInfo>,
43}
44
45#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
46pub struct IFn {
47    pub signature: ISignature,
48    pub variables: BTreeMap<IVarId, IVarInfo>,
49    pub block: IBlock,
50}
51
52impl IFn {
53    pub fn globals_to_input_values(
54        &self,
55        globals: &BTreeMap<String, AbstractValue>,
56    ) -> Vec<AbstractValue> {
57        let mut input_values = Vec::new();
58
59        for input_id in &self.signature.inputs {
60            let input_info = self
61                .variables
62                .get(input_id)
63                .expect("Input should be in local variables");
64            let abstract_value = globals
65                .get(input_info.ident.name())
66                .expect("Input should be in global forward");
67            input_values.push(abstract_value.clone());
68        }
69
70        input_values
71    }
72
73    pub fn call(
74        &self,
75        context: &IContext,
76        input_values: Vec<AbstractValue>,
77    ) -> (AbstractValue, AbstractValue) {
78        let abstr = self.forward_interpret(context, input_values);
79        self.forward_result(&abstr)
80    }
81
82    pub fn forward_interpret(
83        &self,
84        context: &IContext,
85        input_values: Vec<AbstractValue>,
86    ) -> IAbstr {
87        let mut abstr = IAbstr::new();
88
89        assert_eq!(self.signature.inputs.len(), input_values.len());
90
91        for (input_var_id, input_value) in self
92            .signature
93            .inputs
94            .iter()
95            .cloned()
96            .zip(input_values.into_iter())
97        {
98            abstr.insert_value(input_var_id, input_value);
99        }
100
101        let fn_context = IFnContext {
102            func: self,
103            context,
104        };
105
106        self.block.forward_interpret(&fn_context, &mut abstr);
107
108        abstr
109    }
110
111    pub fn forward_result(&self, abstr: &IAbstr) -> (AbstractValue, AbstractValue) {
112        let normal_result = abstr.value(self.signature.output.normal).clone();
113        let panic_result = abstr.value(self.signature.output.panic).clone();
114        (normal_result, panic_result)
115    }
116
117    pub fn backward_interpret(
118        &self,
119        context: &IContext,
120        abstr: &IAbstr,
121        later_normal: RefinementValue,
122        later_panic: RefinementValue,
123    ) -> IRefin {
124        let mut refin = IRefin::new();
125
126        refin.insert_value(self.signature.output.normal, later_normal);
127        refin.insert_value(self.signature.output.panic, later_panic);
128
129        let fn_context = IFnContext {
130            func: self,
131            context,
132        };
133
134        self.block
135            .backward_interpret(&fn_context, abstr, &mut refin);
136
137        refin
138    }
139
140    pub fn backward_earlier(&self, abstr: &IAbstr, refin: &IRefin) -> Vec<RefinementValue> {
141        let mut result = Vec::new();
142        for input_var_id in &self.signature.inputs {
143            result.push(
144                refin
145                    .value_opt(*input_var_id)
146                    .cloned()
147                    .unwrap_or_else(|| RefinementValue::unmarked_for(abstr.value(*input_var_id))),
148            );
149        }
150        result
151    }
152
153    pub fn into_declaration(self) -> IFnDeclaration {
154        IFnDeclaration {
155            signature: self.signature,
156            variables: self.variables,
157        }
158    }
159}
160
161impl IBlock {
162    pub fn forward_interpret(&self, context: &IFnContext, abstr: &mut IAbstr) {
163        for stmt in &self.stmts {
164            stmt.forward_interpret(context, abstr);
165        }
166    }
167
168    pub fn backward_interpret(&self, context: &IFnContext, abstr: &IAbstr, refin: &mut IRefin) {
169        // go in reverse
170        for stmt in self.stmts.iter().rev() {
171            stmt.backward_interpret(context, abstr, refin);
172        }
173    }
174}
175
176impl Debug for IBlock {
177    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
178        let mut franz = f.debug_set();
179
180        for stmt in &self.stmts {
181            franz.entry(stmt);
182        }
183
184        franz.finish()
185    }
186}
machine_check_common/iir/func.rs

machine_check_common/iir/
func.rs
