rapx/analysis/senryx/contracts/
contract.rs

1use super::abstract_state::*;
2use crate::analysis::senryx::contracts::state_lattice::Lattice;
3
4#[derive(Debug, PartialEq, Clone)]
5pub enum Contract<'tcx> {
6    ValueCheck { op: Op, value: Value },
7    StateCheck { op: Op, state: StateType<'tcx> },
8}
9
10pub fn check_contract<'tcx>(
11    contract: &Contract<'tcx>,
12    abstate_item: &AbstractStateItem<'tcx>,
13) -> bool {
14    match contract {
15        Contract::ValueCheck { op, value } => {
16            return handle_value_op(&abstate_item.value, op, value);
17        }
18        Contract::StateCheck { op: _, state } => {
19            for ab_state in &abstate_item.state {
20                if check_is_same_state_type(ab_state, &state) && !ab_state.check() {
21                    return false;
22                }
23                // if check_is_same_state_type(ab_state, &state)
24                //     && handle_state_op(ab_state, op, state)
25                // {
26                //     return true;
27                // }
28            }
29            return true;
30        }
31    }
32}
33
34pub fn check_is_same_state_type(left: &StateType, right: &StateType) -> bool {
35    match (left, right) {
36        (StateType::AllocatedState(_), StateType::AllocatedState(_)) => {
37            return true;
38        }
39        (StateType::AlignState(_), StateType::AlignState(_)) => {
40            return true;
41        }
42        _ => false,
43    }
44}
45
46pub fn handle_value_op<T: std::cmp::PartialEq + std::cmp::PartialOrd>(
47    left: &(T, T),
48    op: &Op,
49    right: &T,
50) -> bool {
51    match op {
52        Op::EQ => {
53            return left.0 == *right;
54        }
55        Op::NE => {
56            return left.0 != *right;
57        }
58        Op::LT => {
59            return left.1 < *right;
60        }
61        Op::GT => {
62            return left.0 > *right;
63        }
64        Op::LE => {
65            return left.1 <= *right;
66        }
67        Op::GE => {
68            return left.0 >= *right;
69        }
70    }
71}
72
73pub fn handle_state_op<'tcx>(left: &StateType<'tcx>, op: &Op, right: &StateType<'tcx>) -> bool {
74    match op {
75        Op::LT => left.less_than(right.clone()),
76        Op::LE => left.less_than(right.clone()) || left.equal(right.clone()),
77        Op::GT => right.less_than(left.clone()),
78        Op::GE => right.less_than(left.clone()) || right.equal(left.clone()),
79        Op::EQ => left.equal(right.clone()),
80        Op::NE => !left.equal(right.clone()),
81    }
82}
rapx/analysis/senryx/contracts/contract.rs

rapx/analysis/senryx/contracts/
contract.rs
