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
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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137

use crate::ir::types::X86Regs;
use crate::lattices;
use lattices::davlattice::DAV;
use lattices::reachingdefslattice::LocIdx;
use lattices::{Lattice, VariableState};
use std::cmp::Ordering;

#[derive(Clone, PartialEq, Eq, PartialOrd, Debug)]
pub enum CallCheckValue {
    GuestTableBase,
    LucetTablesBase,
    TableSize,
    TypeOf(X86Regs), //regnum
    PtrOffset(DAV),
    TypedPtrOffset(u32),
    FnPtr(u32), //type
    CheckedVal,
    CheckFlag(u32, X86Regs),
    TypeCheckFlag(X86Regs, u32), //addr, regnum, typeidx
    Constant(u64),
}

use CallCheckValue::*;

#[derive(PartialEq, Eq, Clone, Debug)]
pub struct CallCheckValueLattice {
    pub v: Option<CallCheckValue>,
}

pub type CallCheckLattice = VariableState<CallCheckValueLattice>;

impl Default for CallCheckValueLattice {
    fn default() -> Self {
        CallCheckValueLattice { v: None }
    }
}

impl CallCheckValueLattice {
    pub fn new(v: CallCheckValue) -> Self {
        CallCheckValueLattice { v: Some(v) }
    }
}

impl Lattice for CallCheckValueLattice {
    fn meet(&self, other: &Self, loc_idx: &LocIdx) -> Self {
        if self.v.clone() == other.v {
            CallCheckValueLattice { v: self.v.clone() }
        } else {
            match (self.v.clone(), other.v.clone()) {
                (Some(PtrOffset(x)), Some(PtrOffset(y))) => CallCheckValueLattice {
                    v: Some(PtrOffset(x.meet(&y, loc_idx))),
                },
                (_, _) => CallCheckValueLattice { v: None },
            }
        }
    }
}

impl PartialOrd for CallCheckValueLattice {
    fn partial_cmp(&self, other: &CallCheckValueLattice) -> Option<Ordering> {
        match (self.v.clone(), other.v.clone()) {
            (None, None) => Some(Ordering::Equal),
            (None, _) => Some(Ordering::Less),
            (_, None) => Some(Ordering::Greater),
            (Some(x), Some(y)) => match (x.clone(), y.clone()) {
                (PtrOffset(x), PtrOffset(y)) => x.partial_cmp(&y),
                (_, _) => {
                    if x == y {
                        Some(Ordering::Equal)
                    } else {
                        None
                    }
                }
            },
        }
    }
}

#[test]
fn call_lattice_test() {
    let x1 = CallCheckValueLattice { v: None };
    let x2 = CallCheckValueLattice {
        v: Some(GuestTableBase),
    };
    let x3 = CallCheckValueLattice {
        v: Some(PtrOffset(DAV::Unknown)),
    };
    let x4 = CallCheckValueLattice {
        v: Some(PtrOffset(DAV::Unknown)),
    };
    let x5 = CallCheckValueLattice {
        v: Some(PtrOffset(DAV::Checked)),
    };

    assert_eq!(x1 == x2, false);
    assert_eq!(x2 == x3, false);
    assert_eq!(x3 == x4, true);
    assert_eq!(x4 == x5, false);

    assert_eq!(x1 != x2, true);
    assert_eq!(x2 != x3, true);
    assert_eq!(x3 != x4, false);
    assert_eq!(x4 != x5, true);

    assert_eq!(x1 > x2, false);
    assert_eq!(x2 > x3, false);
    assert_eq!(x3 > x4, false);
    assert_eq!(x4 > x5, false);

    assert_eq!(x1 < x2, true);
    assert_eq!(x2 < x3, false);
    assert_eq!(x3 < x4, false);
    assert_eq!(x4 < x5, true);

    assert_eq!(
        x1.meet(&x2, &LocIdx { addr: 0, idx: 0 }) == CallCheckValueLattice { v: None },
        true
    );
    assert_eq!(
        x2.meet(&x3, &LocIdx { addr: 0, idx: 0 }) == CallCheckValueLattice { v: None },
        true
    );
    assert_eq!(
        x3.meet(&x4, &LocIdx { addr: 0, idx: 0 })
            == CallCheckValueLattice {
                v: Some(PtrOffset(DAV::Unknown))
            },
        true
    );
    assert_eq!(
        x4.meet(&x5, &LocIdx { addr: 0, idx: 0 })
            == CallCheckValueLattice {
                v: Some(PtrOffset(DAV::Unknown))
            },
        true
    );
}