rapx/verify/property_checker/
string.rs

1//! Checker for `ValidString`: UTF-8 validity of tracked byte buffers.
2
3use crate::helpers::mir_scan::Checkpoint;
4use crate::verify::contract::Property;
5use crate::verify::report::CheckResult;
6use crate::verify::vm::state::VmState;
7use z3::{SatResult, Solver};
8
9use super::PropertyChecker;
10
11impl PropertyChecker {
12    /// Shared UTF-8 byte check: prove the tracked buffer bytes of `alloc_id` are
13    /// *not* valid UTF-8 (i.e. disprove the DFA), reporting `Failed` when the
14    /// solver proves they cannot be valid.
15    fn check_utf8_alloc<'z3, 'tcx>(
16        &self,
17        vm_state: &VmState<'z3, 'tcx>,
18        solver: &Solver<'z3>,
19        alloc_id: crate::verify::vm::state::AllocId,
20    ) -> CheckResult {
21        if vm_state.alloc(alloc_id).facts.dead {
22            return CheckResult::Failed;
23        }
24        if vm_state.is_utf8_trusted(alloc_id) {
25            return CheckResult::ProvedByRule;
26        }
27        let Some(valid) = vm_state.utf8_validity(alloc_id) else {
28            return CheckResult::ProvedByRule; // no byte-level info → trust
29        };
30
31        solver.push();
32        solver.assert(&valid);
33        let r = solver.check();
34        solver.pop(1);
35        match r {
36            SatResult::Unsat => CheckResult::Failed,
37            _ => CheckResult::ProvedByRule,
38        }
39    }
40
41    pub(super) fn check_valid_string<'z3, 'tcx>(
42        &self,
43        vm_state: &VmState<'z3, 'tcx>,
44        solver: &Solver<'z3>,
45        checkpoint: &Checkpoint<'tcx>,
46        property: &Property<'tcx>,
47    ) -> CheckResult {
48        // Empty byte range: trivially valid UTF-8.
49        if let Some(count) = property
50            .args()
51            .get(2)
52            .and_then(|a| self.resolve_arg_term(vm_state, checkpoint, a))
53        {
54            if count.as_u64() == Some(0) {
55                return CheckResult::ProvedByRule;
56            }
57        }
58
59        let Some(value) = self.target_value(vm_state, checkpoint, property) else {
60            return CheckResult::ProvedByRule;
61        };
62        if let Some(alloc_id) = value.provenance_alloc_id() {
63            return self.check_utf8_alloc(vm_state, solver, alloc_id);
64        }
65
66        // A one-argument `ValidString(iter)` targets an `Iterator<Item = u8>`:
67        // trace the (possibly `Cloned`/`Rev`-wrapped) iterator to the backing
68        // byte buffer of its innermost `Iter`/`IterMut` and UTF-8-check that.
69        if let Some(local) = vm_state.find_local_by_address(&value.z3_term) {
70            if let Some((alloc_id, _end_offset)) = vm_state.iter_utf8_buffer(local) {
71                return self.check_utf8_alloc(vm_state, solver, alloc_id);
72            }
73        }
74        CheckResult::ProvedByRule
75    }
76}
rapx/verify/property_checker/string.rs

rapx/verify/property_checker/
string.rs
