veriwasm 0.1.4

A safety verifier for native-compiled WebAssembly code
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

use crate::lattices;
use lattices::reachingdefslattice::{LocIdx, ReachingDefnLattice};
use lattices::Lattice;
use std::cmp::Ordering;

// Dependent Abstract Value
#[derive(Clone, PartialEq, Eq, Debug)]
pub enum DAV {
    Unknown,
    Unchecked(ReachingDefnLattice),
    Checked,
}

impl PartialOrd for DAV {
    fn partial_cmp(&self, other: &DAV) -> Option<Ordering> {
        match (self, other) {
            (DAV::Unknown, DAV::Unknown) => Some(Ordering::Equal),
            (DAV::Unknown, _) => Some(Ordering::Less),
            (DAV::Unchecked(x), DAV::Unchecked(y)) => {
                if x == y {
                    Some(Ordering::Equal)
                } else {
                    None
                }
            }
            (DAV::Unchecked(_), DAV::Checked) => Some(Ordering::Less),
            (DAV::Checked, DAV::Checked) => Some(Ordering::Equal),
            (DAV::Checked, DAV::Unchecked(_)) => Some(Ordering::Greater),
            (DAV::Unchecked(_), DAV::Unknown) => Some(Ordering::Greater),
            (DAV::Checked, DAV::Unknown) => Some(Ordering::Greater),
        }
    }
}

impl Lattice for DAV {
    fn meet(&self, other: &Self, _loc_idx: &LocIdx) -> Self {
        match (self, other) {
            (DAV::Unknown, _) => DAV::Unknown,
            (_, DAV::Unknown) => DAV::Unknown,
            (DAV::Unchecked(x), DAV::Unchecked(y)) => {
                if x == y {
                    self.clone()
                } else {
                    DAV::Unknown
                }
            }
            (DAV::Checked, DAV::Checked) => self.clone(),
            (DAV::Unchecked(_), DAV::Checked) => self.clone(),
            (DAV::Checked, DAV::Unchecked(_)) => other.clone(),
        }
    }
}

//What is a default index? This might be wrong.
//Perhaps default is what index should be at start of function.
impl Default for DAV {
    fn default() -> Self {
        DAV::Unknown
    }
}