machine-check-exec 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

use std::collections::BTreeSet;
use std::ops::ControlFlow;

use machine_check_common::check::Culprit;
use machine_check_common::ExecStats;
use mck::{abstr::BitvectorDomain, concr::FullMachine};

use crate::model_check::ThreeValuedChecker;
use crate::precision::Precision;
use crate::space::StateSpace;
use crate::{AbstrInput, AbstrPanicState, AbstrParam};

/// Work state, i.e. the meta-state of the whole verification.
pub struct WorkState<M: FullMachine> {
    /// Refinement precision for inputs (can make inputs more precise).
    pub input_precision: Precision<AbstrInput<M>>,
    /// Refinement precision for parameters (can make parameters more precise).
    pub param_precision: Precision<AbstrParam<M>>,
    /// Refinement precision for steps (can add step decay).
    pub step_precision: Precision<AbstrPanicState<M>>,
    /// Current state space.
    pub space: StateSpace<M>,
    /// Model checker.
    pub checker: ThreeValuedChecker,
    /// Culprit of verification returning unknown.
    pub culprit: Option<Culprit>,

    /// Number of refinements made until now.
    pub num_refinements: usize,
    /// Number of states generated until now.
    pub num_generated_states: usize,
    /// Number of transitions generated until now.
    pub num_generated_transitions: usize,
}

impl<M: FullMachine> WorkState<M> {
    pub fn new() -> Self {
        Self {
            input_precision: Precision::new(),
            param_precision: Precision::new(),
            step_precision: Precision::new(),
            space: StateSpace::new(),
            checker: ThreeValuedChecker::new(),
            culprit: None,
            num_refinements: 0,
            num_generated_states: 0,
            num_generated_transitions: 0,
        }
    }

    pub fn info(&mut self) -> ExecStats {
        ExecStats {
            num_refinements: self.num_refinements,
            num_generated_states: self.num_generated_states,
            num_final_states: self.space.num_nodes().saturating_sub(1),
            num_generated_transitions: self.num_generated_transitions,
            num_final_transitions: self.space.num_transitions(),
            inherent_panic_message: self.find_panic_string().map(String::from),
        }
    }

    pub fn find_panic_string(&mut self) -> Option<&'static str> {
        let panic_id = self.space.breadth_first_search(|_, state_data| {
            if let Some(panic_value) = state_data.panic.concrete_value() {
                if panic_value.is_nonzero() {
                    return ControlFlow::Break(panic_value.to_u64() as u32);
                }
            }
            ControlFlow::Continue(())
        });

        // TODO: panic_message approach does not work if there are multiple macro invocations
        panic_id.map(|panic_id: u32| M::panic_message(panic_id))
    }

    pub fn make_compact(&mut self) {
        // make sure that all state ids used outside the state space but in work state are retained
        // when making the state space compact
        let mut outside_used_ids = if let Some(culprit) = &self.culprit {
            BTreeSet::from_iter(culprit.path.iter().copied())
        } else {
            BTreeSet::new()
        };

        outside_used_ids.extend(self.input_precision.used_state_ids());
        outside_used_ids.extend(self.step_precision.used_state_ids());
        let removed_states = self.space.make_compact(outside_used_ids);
        self.checker.remove_states(&removed_states);
        log::trace!(
            "Compacted the state space by removing states {:?}",
            removed_states
        );
    }

    pub fn garbage_collect(&mut self) {
        if self.space.should_compact() {
            self.make_compact();
        }
    }
}