machine_check_exec/
framework.rs

1use std::collections::BTreeMap;
2use std::ops::ControlFlow;
3
4use log::log_enabled;
5use log::trace;
6use machine_check_common::check::Conclusion;
7use machine_check_common::check::KnownConclusion;
8use machine_check_common::check::Property;
9use machine_check_common::property::Subproperty;
10use machine_check_common::ExecError;
11use machine_check_common::ExecStats;
12use machine_check_common::NodeId;
13use machine_check_common::ParamValuation;
14use machine_check_common::StateId;
15use mck::concr::FullMachine;
16use work_state::WorkState;
17
18use crate::space::StateSpace;
19use crate::Strategy;
20use crate::{RefinInput, RefinPanicState, RefinParam};
21use mck::refin::Refine;
22
23mod refine;
24mod regenerate;
25mod work_state;
26
27/// Three-valued abstraction refinement framework.
28pub struct Framework<M: FullMachine> {
29    /// Abstract system.
30    abstract_system: M::Abstr,
31
32    /// Default input precision.
33    default_input_precision: RefinInput<M>,
34
35    /// Default parameter precision.
36    default_param_precision: RefinParam<M>,
37
38    /// Default step precision.
39    default_step_precision: RefinPanicState<M>,
40
41    /// Work state containing the structures that change during verification.
42    work_state: WorkState<M>,
43}
44
45impl<M: FullMachine> Framework<M> {
46    /// Constructs the framework with a given system and strategy.
47    pub fn new(abstract_system: M::Abstr, strategy: Strategy) -> Self {
48        // default the input and param precision to clean (inputs will be refined)
49        let (default_input_precision, default_param_precision) = if strategy.naive_inputs {
50            (Refine::dirty(), Refine::dirty())
51        } else {
52            (Refine::clean(), Refine::clean())
53        };
54
55        // default the step precision to dirty (steps will remain non-decayed)
56        let default_step_precision = if strategy.use_decay {
57            Refine::clean()
58        } else {
59            Refine::dirty()
60        };
61
62        // return the framework with empty state space, before any construction
63        Framework {
64            abstract_system,
65            default_input_precision,
66            default_step_precision,
67            default_param_precision,
68            work_state: WorkState::new(),
69        }
70    }
71
72    pub fn verify(&mut self, property: &Property) -> Result<KnownConclusion, ExecError> {
73        // loop verification steps until some conclusion is reached
74        let result = loop {
75            match self.step_verification(property) {
76                ControlFlow::Continue(()) => {}
77                ControlFlow::Break(result) => break result,
78            }
79        };
80
81        // make compact after verification for nice state space information
82        self.work_state.make_compact();
83
84        if log_enabled!(log::Level::Trace) {
85            trace!("Verification final space: {:#?}", self.work_state.space);
86        }
87        result
88    }
89
90    pub fn step_verification(
91        &mut self,
92        property: &Property,
93    ) -> ControlFlow<Result<KnownConclusion, ExecError>> {
94        // if the space is invalid (just after construction), regenerate it
95        if !self.work_state.space.is_valid() {
96            self.regenerate(NodeId::ROOT);
97        } else if let Some(culprit) = self.work_state.culprit.take() {
98            // we have a culprit, refine on it
99            if let Err(err) = self.refine(&culprit) {
100                // the refinement is incomplete
101                return ControlFlow::Break(Err(err));
102            }
103            // run garbage collection
104            self.work_state.garbage_collect();
105        }
106
107        if log_enabled!(log::Level::Trace) {
108            trace!("Model-checking state space: {:#?}", self.work_state.space);
109        }
110
111        // perform model-checking
112        match self
113            .work_state
114            .checker
115            .check_property(&self.work_state.space, property)
116        {
117            Ok(Conclusion::Known(conclusion)) => {
118                // conclude the result
119                ControlFlow::Break(Ok(conclusion))
120            }
121            Ok(Conclusion::Unknown(culprit)) => {
122                // we have a new culprit, continue the control flow
123                self.work_state.culprit = Some(culprit);
124                ControlFlow::Continue(())
125            }
126            Ok(Conclusion::NotCheckable) => {
127                // should never happen, the state space should be valid
128                panic!("The state space should be valid after stepping verification");
129            }
130            Err(err) => {
131                // propagate the error
132                ControlFlow::Break(Err(err))
133            }
134        }
135    }
136
137    pub fn check_subproperty_with_labelling(
138        &mut self,
139        property: &Subproperty,
140    ) -> Result<(Conclusion, BTreeMap<StateId, ParamValuation>), ExecError> {
141        self.work_state
142            .checker
143            .check_subproperty_with_labelling(&self.work_state.space, property)
144    }
145
146    pub fn find_panic_string(&mut self) -> Option<&'static str> {
147        self.work_state.find_panic_string()
148    }
149
150    pub fn reset(&mut self) {
151        // reset the work state
152        self.work_state = WorkState::new()
153    }
154
155    pub fn info(&mut self) -> ExecStats {
156        self.work_state.info()
157    }
158
159    pub fn space(&self) -> &StateSpace<M> {
160        &self.work_state.space
161    }
162
163    pub fn make_compact(&mut self) {
164        self.work_state.make_compact();
165    }
166}
machine_check_exec/framework.rs

machine_check_exec/
framework.rs
