rapx 0.7.63

A static analysis platform for Rust program analysis and verification
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
138
139
140
141
142
143
144
145

//! Direct MIR dispatch for symbolic execution rules.

use rustc_middle::mir::{
    BasicBlock, Local, NonDivergingIntrinsic, Place, Rvalue, Statement, StatementKind, Terminator,
    TerminatorKind,
};

use super::super::state::{VmState, VmValue};
use super::{rvalue, statement, terminator};
use crate::verify::mir_support;

pub(super) fn exec_statement<'z3, 'tcx>(state: &mut VmState<'z3, 'tcx>, stmt: &Statement<'tcx>) {
    let name = match &stmt.kind {
        StatementKind::Assign(assign) => {
            let (place, value) = &**assign;
            statement::exec_assign(state, place, value);
            "Assign"
        }
        StatementKind::StorageLive(local) => {
            statement::exec_storage_live(state, *local);
            "StorageLive"
        }
        StatementKind::StorageDead(local) => {
            statement::exec_storage_dead(state, *local);
            "StorageDead"
        }
        StatementKind::Intrinsic(intrinsic)
            if let NonDivergingIntrinsic::Assume(operand) = &**intrinsic =>
        {
            statement::exec_assume(state, operand);
            "Assume"
        }
        StatementKind::Intrinsic(intrinsic)
            if let NonDivergingIntrinsic::CopyNonOverlapping(copy) = &**intrinsic =>
        {
            statement::exec_copy_nonoverlapping(state, copy);
            "CopyNonOverlapping"
        }
        kind if mir_support::ignored_statement(kind) => "Ignored",
        _ => {
            state.unsupported_mir = true;
            "Unsupported"
        }
    };
    log::trace!("vm statement rule: {name}");
}

pub(super) fn exec_terminator<'z3, 'tcx>(
    state: &mut VmState<'z3, 'tcx>,
    term: &Terminator<'tcx>,
    successor: Option<BasicBlock>,
) {
    let name = match &term.kind {
        TerminatorKind::Call {
            func,
            args,
            destination,
            ..
        } => {
            let caller_id = state.current_frame.current_def_id;
            state.exec_call(func, args, destination.local, caller_id);
            "Call"
        }
        TerminatorKind::TailCall { func, args, .. } => {
            let caller_id = state.current_frame.current_def_id;
            state.exec_call(func, args, Local::from_usize(0), caller_id);
            "TailCall"
        }
        TerminatorKind::SwitchInt { discr, targets } => {
            terminator::exec_switch_int(state, discr, targets, successor);
            "SwitchInt"
        }
        TerminatorKind::Assert { cond, expected, .. } => {
            terminator::exec_assert(state, cond, *expected);
            "Assert"
        }
        TerminatorKind::Drop { place, .. } => {
            terminator::exec_drop(state, place);
            "Drop"
        }
        kind if mir_support::ignored_terminator(kind) => "Ignored",
        _ => {
            state.unsupported_mir = true;
            "Unsupported"
        }
    };
    log::trace!("vm terminator rule: {name}");
}

pub(super) fn eval_rvalue<'z3, 'tcx>(
    state: &mut VmState<'z3, 'tcx>,
    place: &Place<'tcx>,
    rv: &Rvalue<'tcx>,
) -> VmValue<'z3, 'tcx> {
    #[allow(unreachable_patterns)]
    let (name, value) = match rv {
        Rvalue::Use(operand, ..) => ("Use", rvalue::eval_use(state, place, operand)),
        Rvalue::Ref(_, _, source) => ("Ref", rvalue::eval_ref(state, place, source)),
        Rvalue::RawPtr(_, source) => ("RawPtr", rvalue::eval_raw_ptr(state, place, source)),
        Rvalue::BinaryOp(op, pair) => ("BinaryOp", rvalue::eval_binary_op(state, place, *op, pair)),
        Rvalue::UnaryOp(op, operand) => {
            ("UnaryOp", rvalue::eval_unary_op(state, place, *op, operand))
        }
        Rvalue::Cast(_, operand, ty) => ("Cast", rvalue::eval_cast(state, operand, *ty)),
        Rvalue::Aggregate(kind, operands) => (
            "Aggregate",
            rvalue::eval_aggregate(state, place, kind, operands),
        ),
        Rvalue::Discriminant(source) => (
            "Discriminant",
            rvalue::eval_discriminant(state, place, source),
        ),
        #[cfg(not(rapx_ge_99))]
        Rvalue::ShallowInitBox(operand, _) => (
            "ShallowInitBox",
            rvalue::eval_shallow_init_box(state, place, operand),
        ),
        Rvalue::CopyForDeref(source) => (
            "CopyForDeref",
            rvalue::eval_copy_for_deref(state, place, source),
        ),
        Rvalue::Repeat(operand, _) => ("Repeat", rvalue::eval_repeat(state, place, operand)),
        Rvalue::ThreadLocalRef(def_id) => (
            "ThreadLocalRef",
            rvalue::eval_thread_local_ref(state, place, *def_id),
        ),
        #[cfg(not(rapx_ge_95))]
        Rvalue::NullaryOp(op) => ("NullaryOp", rvalue::eval_nullary_op(state, place, op)),
        Rvalue::WrapUnsafeBinder(operand, _) => (
            "WrapUnsafeBinder",
            rvalue::eval_wrap_unsafe_binder(state, place, operand),
        ),
        #[cfg(rapx_rvalue_has_reborrow)]
        Rvalue::Reborrow(_, _, source) => ("Reborrow", rvalue::eval_reborrow(state, place, source)),
        _ => {
            state.unsupported_mir = true;
            (
                "Unsupported",
                rvalue::eval_fresh_value(state, place, "unsupported_rvalue"),
            )
        }
    };
    log::trace!("vm rvalue rule: {name}");
    value
}