rapx/verify/property_checker/
string.rs

1#[cfg(not(rapx_has_skip_norm_wip))]
2use crate::compat::SkipNormWip;
3use z3::{SatResult, Solver, ast::Int};
4use crate::verify::contract::Property;
5use crate::verify::report::CheckResult;
6use crate::helpers::mir_scan::Checkpoint;
7use crate::verify::vm::state::VmState;
8
9use super::PropertyChecker;
10
11impl PropertyChecker {
12    pub(super) fn check_valid_string<'ctx, 'tcx>(
13        &self,
14        vm_state: &VmState<'ctx, 'tcx>,
15        solver: &Solver<'ctx>,
16        checkpoint: &Checkpoint<'tcx>,
17        property: &Property<'tcx>,
18    ) -> CheckResult {
19        // Empty byte range: trivially valid UTF-8.
20        if let Some(count) = property
21            .args()
22            .get(2)
23            .and_then(|a| self.resolve_arg_term(vm_state, checkpoint, a))
24        {
25            if count.as_u64() == Some(0) {
26                return CheckResult::Proved;
27            }
28        }
29
30        let Some(value) = self.target_value(vm_state, checkpoint, property) else {
31            return CheckResult::Proved;
32        };
33        let Some(alloc_id) = value.provenance_alloc_id() else {
34            return CheckResult::Proved;
35        };
36
37        // A dead allocation cannot back a live string (use-after-free).
38        if vm_state.alloc(alloc_id).dead {
39            return CheckResult::Failed;
40        }
41
42        // Byte-level check: prove the tracked buffer bytes are *not* valid UTF-8.
43        let byte_pairs = vm_state.alloc_byte_values(alloc_id);
44        if byte_pairs.is_empty() {
45            return CheckResult::Proved; // no byte-level info → trust
46        }
47        let bytes: Vec<Int<'ctx>> = byte_pairs.iter().map(|(_, t)| (*t).clone()).collect();
48        let valid = super::utf8_validity(vm_state.ctx, &bytes);
49
50        solver.push();
51        solver.assert(&valid);
52        let r = solver.check();
53        solver.pop(1);
54        match r {
55            SatResult::Unsat => CheckResult::Failed,
56            _ => CheckResult::Proved,
57        }
58    }
59}
rapx/verify/property_checker/string.rs

rapx/verify/property_checker/
string.rs
