mck 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

use std::num::NonZero;

use crate::{
    abstr::{three_valued::RThreeValuedBitvector, BitvectorDomain},
    backward::HwArith,
    bitvector::refin::three_valued::{
        support::{runtime_default_bi_mark, runtime_default_uni_mark},
        RMarkBitvector,
    },
    misc::BitvectorBound,
    refin::RefinementDomain,
};

impl HwArith for RThreeValuedBitvector {
    type Mark = RMarkBitvector;
    type DivRemResult = (RMarkBitvector, RMarkBitvector);

    fn arith_neg(normal_input: (Self,), mark_later: Self::Mark) -> (Self::Mark,) {
        runtime_default_uni_mark(normal_input, mark_later)
    }

    fn add(normal_input: (Self, Self), mark_later: Self::Mark) -> (Self::Mark, Self::Mark) {
        runtime_default_bi_mark(normal_input, mark_later)
    }

    fn sub(normal_input: (Self, Self), mark_later: Self::Mark) -> (Self::Mark, Self::Mark) {
        runtime_default_bi_mark(normal_input, mark_later)
    }

    fn mul(normal_input: (Self, Self), mark_later: Self::Mark) -> (Self::Mark, Self::Mark) {
        runtime_default_bi_mark(normal_input, mark_later)
    }

    fn udiv(
        normal_input: (Self, Self),
        mark_later: (RMarkBitvector, RMarkBitvector),
    ) -> (Self::Mark, Self::Mark) {
        runtime_divrem_mark(normal_input, mark_later)
    }

    fn sdiv(
        normal_input: (Self, Self),
        mark_later: (RMarkBitvector, RMarkBitvector),
    ) -> (Self::Mark, Self::Mark) {
        runtime_divrem_mark(normal_input, mark_later)
    }

    fn urem(
        normal_input: (Self, Self),
        mark_later: (RMarkBitvector, RMarkBitvector),
    ) -> (Self::Mark, Self::Mark) {
        runtime_divrem_mark(normal_input, mark_later)
    }

    fn srem(
        normal_input: (Self, Self),
        mark_later: (RMarkBitvector, RMarkBitvector),
    ) -> (Self::Mark, Self::Mark) {
        runtime_divrem_mark(normal_input, mark_later)
    }
}

fn runtime_divrem_mark(
    normal_input: (RThreeValuedBitvector, RThreeValuedBitvector),
    mark_later: (RMarkBitvector, RMarkBitvector),
) -> (RMarkBitvector, RMarkBitvector) {
    assert_eq!(normal_input.0.bound(), normal_input.1.bound());
    let width = normal_input.0.bound().width();

    // first is result, second is panic
    let mark_later_result = mark_later.0;
    let mark_later_panic = mark_later.1;

    // prefer marking panic
    if mark_later_panic.importance() > 0 {
        // this only depends on the divisor, mark just the divisor
        let importance = if let Some(mark_later) = mark_later_result.inner {
            mark_later.importance
        } else {
            NonZero::<u8>::MIN
        };
        return (
            RMarkBitvector::new_unmarked(width),
            RMarkBitvector::new_marked(importance, width).limit(&normal_input.1),
        );
    }

    // no panic marking, mark normally
    runtime_default_bi_mark(normal_input, mark_later_result)
}