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

use std::fmt::Debug;
use std::hash::Hash;

use serde::{Deserialize, Serialize};

use crate::bitvector::{compute_u64_mask, util::compute_u64_sign_bit_mask};

pub trait BitvectorBound: Clone + Copy + PartialEq + Eq + Hash + Debug {
    fn width(&self) -> u32;
    fn mask(&self) -> u64;
    fn sign_bit_mask(&self) -> u64;

    fn allowed(&self, value: u64) -> bool {
        value <= self.mask()
    }
}

#[derive(Clone, Copy, PartialEq, Eq, Debug, Hash, Serialize, Deserialize)]
pub struct RBound {
    width: u32,
}

impl RBound {
    pub fn new(width: u32) -> Self {
        Self { width }
    }
}

impl BitvectorBound for RBound {
    fn width(&self) -> u32 {
        self.width
    }

    fn mask(&self) -> u64 {
        compute_u64_mask(self.width)
    }

    fn sign_bit_mask(&self) -> u64 {
        compute_u64_sign_bit_mask(self.width)
    }
}

#[derive(Clone, Copy, PartialEq, Eq, Debug, Hash, Serialize, Deserialize)]
pub struct CBound<const W: u32>;

impl<const W: u32> BitvectorBound for CBound<W> {
    fn width(&self) -> u32 {
        W
    }
    fn mask(&self) -> u64 {
        compute_u64_mask(W)
    }

    fn sign_bit_mask(&self) -> u64 {
        compute_u64_sign_bit_mask(W)
    }
}