mirsa-analysis 0.3.0

Analysis orchestration for mirsa
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

use mirsa_domains::allocation::AllocationState;
use mirsa_domains::allocation::state::is_allocation_pointer;
use mirsa_relations::symbolic::{SymbolicExpr, SymbolicFact, SymbolicState};
use rustc_middle::mir::{BinOp, LocalDecls, Operand};
use rustc_middle::ty::{TyCtxt, TyKind};

pub fn reduce_fact<'tcx>(
    tcx: TyCtxt<'tcx>,
    local_decls: &LocalDecls<'tcx>,
    state: &mut AllocationState<'tcx>,
    symbolic: &SymbolicState<'tcx>,
    fact: &SymbolicFact<'tcx>,
) -> bool {
    let (operand, truth) = match fact {
        SymbolicFact::EqConst { expr, value } => {
            let Some(value) = boolean_value(expr, *value, local_decls, tcx) else {
                return true;
            };
            (expr, value)
        }
        SymbolicFact::NeConst { expr, value } => {
            let Some(value) = boolean_value(expr, *value, local_decls, tcx) else {
                return true;
            };
            (expr, !value)
        }
    };
    let (Operand::Copy(place) | Operand::Move(place)) = operand else {
        return true;
    };
    let Some(SymbolicExpr::Cmp { op, left, right }) = symbolic.expr_for_place(*place) else {
        return true;
    };
    let equality_holds = matches!((op, truth), (BinOp::Eq, true) | (BinOp::Ne, false));
    if !equality_holds
        || !is_allocation_pointer(tcx, left.ty(local_decls, tcx))
        || !is_allocation_pointer(tcx, right.ty(local_decls, tcx))
    {
        return true;
    }
    let (Operand::Copy(left) | Operand::Move(left)) = left else {
        return true;
    };
    let (Operand::Copy(right) | Operand::Move(right)) = right else {
        return true;
    };
    state.constrain_equal_paths(symbolic, *left, *right)
}

fn boolean_value<'tcx>(
    operand: &Operand<'tcx>,
    value: u128,
    local_decls: &LocalDecls<'tcx>,
    tcx: TyCtxt<'tcx>,
) -> Option<bool> {
    if !matches!(operand.ty(local_decls, tcx).kind(), TyKind::Bool) {
        return None;
    }
    match value {
        0 => Some(false),
        1 => Some(true),
        _ => None,
    }
}