rapx/verify/smt_check/
alive.rs

1//! Lifetime anchoring checks for the `Alive` safety property.
2//!
3//! `Alive` is different from numeric SPs: `from_raw_parts(_mut)` does not only
4//! require a valid address at the callsite, it also asks the returned view's
5//! lifetime to be anchored to a source that really owns or borrows the memory.
6//! This first checker intentionally focuses on common safe-wrapper shapes:
7//!
8//! - elided returns tied to `&self` / `&mut self`;
9//! - explicit returns tied to a real host parameter used to produce the pointer;
10//! - obvious lifetime widening, unrelated host, and `'static` escapes.
11
12use std::collections::HashSet;
13
14use rustc_hir::def_id::DefId;
15use rustc_middle::{
16    mir::{Local, Operand, Rvalue, StatementKind, TerminatorKind},
17    ty::{self, TyCtxt},
18};
19
20use crate::{
21    helpers::name::parse_signature,
22    verify::{
23        call_summary::CallEffect,
24        contract::Property,
25        def_use::PlaceKey,
26        helpers::Checkpoint,
27        report::CheckResult,
28        verifier::{AbstractValue, CallSummary, ForwardVisitResult, StateFact},
29    },
30};
31
32use super::common::{SmtCheckResult, SmtChecker};
33
34#[derive(Clone, Copy, Debug, Eq, PartialEq)]
35enum AliveProducer {
36    SharedSlice,
37    UniqueSlice,
38}
39
40#[derive(Clone, Debug, Eq, PartialEq)]
41enum ReturnLifetime {
42    Elided,
43    Named(String),
44    Static,
45    Unknown,
46}
47
48#[derive(Clone, Debug)]
49struct SignatureInfo {
50    text: String,
51    return_lifetime: ReturnLifetime,
52    has_ref_self: bool,
53    has_mut_self: bool,
54    consumes_self: bool,
55}
56
57/// Checks whether an `Alive` obligation has a lifetime anchor for the returned view.
58pub(crate) fn check<'tcx>(
59    checker: &SmtChecker<'tcx>,
60    checkpoint: &Checkpoint<'tcx>,
61    property: &Property<'tcx>,
62    forward: &ForwardVisitResult<'tcx>,
63) -> SmtCheckResult {
64    let Some(destination) = call_destination(checker.tcx, checkpoint) else {
65        return SmtCheckResult::unknown("Alive producer destination could not be resolved");
66    };
67    let Some(producer) =
68        alive_producer_from_destination(checker.tcx, checkpoint.caller, destination)
69    else {
70        return SmtCheckResult::unknown(
71            "Alive lowering currently supports borrowed view producers",
72        );
73    };
74    if !destination_flows_to_return(checker.tcx, checkpoint.caller, destination) {
75        return SmtCheckResult::proved(
76            "Alive view is local; no escaped returned lifetime must be anchored",
77        );
78    }
79
80    let Some(signature) = SignatureInfo::from_def_id(checker.tcx, checkpoint.caller) else {
81        return SmtCheckResult::unknown("Alive caller signature could not be recovered");
82    };
83    let target = checker
84        .property_target(checkpoint, property)
85        .or_else(|| checker.callsite_arg_place(checkpoint, 0));
86    let pointer_origin_param = target.as_ref().and_then(|place| {
87        pointer_origin_param_local(checker.tcx, checkpoint.caller, place, forward)
88    });
89
90    match &signature.return_lifetime {
91        ReturnLifetime::Elided => check_elided_return(producer, &signature),
92        ReturnLifetime::Static => failed("Alive failed: returned slice is widened to 'static"),
93        ReturnLifetime::Named(lifetime) => check_named_return(
94            checker.tcx,
95            checkpoint.caller,
96            producer,
97            &signature,
98            lifetime,
99            pointer_origin_param,
100        ),
101        ReturnLifetime::Unknown => {
102            SmtCheckResult::unknown("Alive return lifetime shape is not supported yet")
103        }
104    }
105}
106
107/// Checks whether an elided return lifetime can be tied to the receiver borrow.
108fn check_elided_return(producer: AliveProducer, signature: &SignatureInfo) -> SmtCheckResult {
109    if signature.has_mut_self && producer == AliveProducer::UniqueSlice {
110        return SmtCheckResult::proved(
111            "Alive proved: returned mutable slice is tied to the current &mut self borrow",
112        );
113    }
114    if signature.has_ref_self && producer == AliveProducer::SharedSlice {
115        return SmtCheckResult::proved(
116            "Alive proved: returned shared slice is tied to the current &self borrow",
117        );
118    }
119    if signature.has_ref_self && producer == AliveProducer::UniqueSlice {
120        return failed("Alive failed: mutable slice is tied only to a shared self borrow");
121    }
122    SmtCheckResult::unknown("Alive elided lifetime is not tied to a supported receiver")
123}
124
125/// Checks whether an explicit return lifetime is tied to the pointer source.
126fn check_named_return<'tcx>(
127    tcx: TyCtxt<'tcx>,
128    caller: DefId,
129    producer: AliveProducer,
130    signature: &SignatureInfo,
131    lifetime: &str,
132    pointer_origin_param: Option<usize>,
133) -> SmtCheckResult {
134    let source_params = params_with_lifetime(tcx, caller, signature, lifetime);
135
136    if let Some(origin) = pointer_origin_param {
137        if source_params.contains(&origin) {
138            return SmtCheckResult::proved(format!(
139                "Alive proved: returned lifetime '{lifetime} is tied to the source parameter that produced the pointer"
140            ));
141        }
142        if !source_params.is_empty() {
143            return failed(format!(
144                "Alive failed: returned lifetime '{lifetime} is tied to a host parameter, but the pointer comes from another source"
145            ));
146        }
147    }
148
149    if producer == AliveProducer::UniqueSlice
150        && signature.has_ref_self
151        && !signature.consumes_self
152        && source_params.is_empty()
153    {
154        return failed(format!(
155            "Alive failed: returned mutable slice uses lifetime '{lifetime}, but that lifetime is not tied to this &mut self borrow"
156        ));
157    }
158
159    if source_params.is_empty() {
160        return failed(format!(
161            "Alive failed: returned lifetime '{lifetime} has no proven source parameter"
162        ));
163    }
164
165    SmtCheckResult::unknown(format!(
166        "Alive could not prove that the pointer is produced from lifetime '{lifetime}"
167    ))
168}
169
170/// Builds a failed SMT check result with a single diagnostic note.
171fn failed(note: impl Into<String>) -> SmtCheckResult {
172    SmtCheckResult {
173        result: CheckResult::Failed,
174        query: None,
175        notes: vec![note.into()],
176    }
177}
178
179/// Classifies the borrowed view returned by the Alive-producing call destination.
180fn alive_producer_from_destination<'tcx>(
181    tcx: TyCtxt<'tcx>,
182    caller: DefId,
183    destination: Local,
184) -> Option<AliveProducer> {
185    let body = tcx.optimized_mir(caller);
186    let ty = body.local_decls[destination].ty;
187    match ty.kind() {
188        ty::Ref(_, _, ty::Mutability::Mut) => Some(AliveProducer::UniqueSlice),
189        ty::Ref(_, _, ty::Mutability::Not) => Some(AliveProducer::SharedSlice),
190        _ => None,
191    }
192}
193
194impl SignatureInfo {
195    /// Recovers the caller signature metadata needed for lifetime anchoring.
196    fn from_def_id(tcx: TyCtxt<'_>, def_id: DefId) -> Option<Self> {
197        let text = function_signature_text(tcx, def_id)?;
198        let params = params_segment(&text).unwrap_or_default();
199        Some(Self {
200            return_lifetime: return_lifetime(&text),
201            has_mut_self: params.contains("&mut self")
202                || params.contains("&'") && params.contains("mut self"),
203            has_ref_self: params.contains("&self")
204                || params.contains("&mut self")
205                || params.contains("&'") && params.contains("self"),
206            consumes_self: params
207                .split(',')
208                .next()
209                .is_some_and(|first| first.trim() == "self"),
210            text,
211        })
212    }
213}
214
215/// Extracts a compact source-level function signature from the HIR span.
216fn function_signature_text(tcx: TyCtxt<'_>, def_id: DefId) -> Option<String> {
217    let local = def_id.as_local()?;
218    let hir_id = tcx.local_def_id_to_hir_id(local);
219    let span = tcx.hir_span(hir_id);
220    let snippet = tcx.sess.source_map().span_to_snippet(span).ok()?;
221    let start = snippet.find("fn ")?;
222    let rest = &snippet[start..];
223    let end = rest.find('{').unwrap_or(rest.len());
224    Some(rest[..end].split_whitespace().collect::<Vec<_>>().join(" "))
225}
226
227/// Extracts the comma-separated parameter segment from a compact signature.
228fn params_segment(signature: &str) -> Option<String> {
229    let start = signature.find('(')?;
230    let end = signature[start + 1..].find(')')? + start + 1;
231    Some(signature[start + 1..end].to_string())
232}
233
234/// Parses the return lifetime shape from a compact signature.
235fn return_lifetime(signature: &str) -> ReturnLifetime {
236    let Some((_, ret)) = signature.split_once("->") else {
237        return ReturnLifetime::Unknown;
238    };
239    let ret = ret
240        .split("where")
241        .next()
242        .unwrap_or(ret)
243        .trim()
244        .trim_end_matches(';')
245        .trim()
246        .replace("& '", "&'");
247    if ret.starts_with("&'static") {
248        return ReturnLifetime::Static;
249    }
250    if let Some(rest) = ret.strip_prefix("&'") {
251        let lifetime = rest
252            .chars()
253            .take_while(|ch| ch.is_ascii_alphanumeric() || *ch == '_')
254            .collect::<String>();
255        if !lifetime.is_empty() {
256            return ReturnLifetime::Named(lifetime);
257        }
258    }
259    if ret.starts_with('&') {
260        return ReturnLifetime::Elided;
261    }
262    ReturnLifetime::Unknown
263}
264
265/// Finds MIR argument locals whose source signature type carries the target lifetime.
266fn params_with_lifetime(
267    tcx: TyCtxt<'_>,
268    caller: DefId,
269    signature: &SignatureInfo,
270    lifetime: &str,
271) -> HashSet<usize> {
272    let (names, _) = parse_signature(tcx, caller);
273    names
274        .iter()
275        .enumerate()
276        .filter_map(|(index, name)| {
277            if name.is_empty() {
278                return None;
279            }
280            let pattern = format!("{name}: &'{lifetime}");
281            let text = signature.text.replace("& '", "&'");
282            text.contains(&pattern).then_some(index + 1)
283        })
284        .collect()
285}
286
287/// Returns the destination local of the Alive-producing callsite.
288fn call_destination<'tcx>(tcx: TyCtxt<'tcx>, checkpoint: &Checkpoint<'tcx>) -> Option<Local> {
289    let body = tcx.optimized_mir(checkpoint.caller);
290    let terminator = body.basic_blocks[checkpoint.block].terminator();
291    let TerminatorKind::Call { destination, .. } = &terminator.kind else {
292        return None;
293    };
294    Some(destination.local)
295}
296
297/// Checks whether the call destination may escape through the function return.
298fn destination_flows_to_return<'tcx>(tcx: TyCtxt<'tcx>, caller: DefId, destination: Local) -> bool {
299    if destination.as_usize() == 0 {
300        return true;
301    }
302    let body = tcx.optimized_mir(caller);
303    if body.local_decls[Local::from_usize(0)].ty == body.local_decls[destination].ty {
304        return true;
305    }
306    for block in body.basic_blocks.iter() {
307        for statement in &block.statements {
308            let StatementKind::Assign(assign) = &statement.kind else {
309                continue;
310            };
311            let (target, rvalue) = &**assign;
312            if target.local.as_usize() != 0 {
313                continue;
314            }
315            if rvalue_source_local(rvalue) == Some(destination) {
316                return true;
317            }
318        }
319    }
320    false
321}
322
323/// Extracts the source local from simple copy, move, cast, or deref-copy rvalues.
324fn rvalue_source_local<'tcx>(rvalue: &Rvalue<'tcx>) -> Option<Local> {
325    match rvalue {
326        Rvalue::Use(Operand::Copy(place), ..)
327        | Rvalue::Use(Operand::Move(place), ..)
328        | Rvalue::Cast(_, Operand::Copy(place), _)
329        | Rvalue::Cast(_, Operand::Move(place), _)
330        | Rvalue::CopyForDeref(place) => Some(place.local),
331        _ => None,
332    }
333}
334
335/// Finds the caller argument local that originally produced a pointer place.
336fn pointer_origin_param_local<'tcx>(
337    tcx: TyCtxt<'tcx>,
338    caller: DefId,
339    place: &PlaceKey,
340    forward: &ForwardVisitResult<'tcx>,
341) -> Option<usize> {
342    let mut seen = HashSet::new();
343    pointer_origin_param_local_inner(tcx, caller, place, forward, &mut seen)
344}
345
346/// Recursively follows local values and call summaries to recover pointer provenance.
347fn pointer_origin_param_local_inner<'tcx>(
348    tcx: TyCtxt<'tcx>,
349    caller: DefId,
350    place: &PlaceKey,
351    forward: &ForwardVisitResult<'tcx>,
352    seen: &mut HashSet<PlaceKey>,
353) -> Option<usize> {
354    if !seen.insert(place.clone()) {
355        return None;
356    }
357    if let Some(local) = place.local() {
358        let body = tcx.optimized_mir(caller);
359        if (1..=body.arg_count).contains(&local.as_usize()) {
360            return Some(local.as_usize());
361        }
362
363        if let Some(call) = call_result_for_local(forward, local) {
364            return call_pointer_origin_param(tcx, caller, call, forward, seen);
365        }
366
367        if let Some(value) = forward.values.get(&local) {
368            return value_pointer_origin_param(tcx, caller, value, forward, seen);
369        }
370    }
371    None
372}
373
374/// Finds the retained call summary that produced a given local.
375fn call_result_for_local<'a, 'tcx>(
376    forward: &'a ForwardVisitResult<'tcx>,
377    local: Local,
378) -> Option<&'a CallSummary<'tcx>> {
379    forward.facts.iter().find_map(|fact| {
380        let StateFact::Call(call) = fact else {
381            return None;
382        };
383        (call.destination == local).then_some(call)
384    })
385}
386
387/// Recovers pointer provenance from interprocedural call effects.
388fn call_pointer_origin_param<'tcx>(
389    tcx: TyCtxt<'tcx>,
390    caller: DefId,
391    call: &CallSummary<'tcx>,
392    forward: &ForwardVisitResult<'tcx>,
393    seen: &mut HashSet<PlaceKey>,
394) -> Option<usize> {
395    for effect in &call.effects {
396        match effect {
397            CallEffect::ReturnPointerFromArg { arg } | CallEffect::ReturnAliasArg { arg } => {
398                let value = call.args.get(*arg)?;
399                return value_pointer_origin_param(tcx, caller, value, forward, seen);
400            }
401            CallEffect::ReturnPointerAdd { base_arg, .. }
402            | CallEffect::ReturnPointerSub { base_arg, .. } => {
403                let value = call.args.get(*base_arg)?;
404                return value_pointer_origin_param(tcx, caller, value, forward, seen);
405            }
406            _ => {}
407        }
408    }
409    None
410}
411
412/// Recovers pointer provenance from an abstract value.
413fn value_pointer_origin_param<'tcx>(
414    tcx: TyCtxt<'tcx>,
415    caller: DefId,
416    value: &AbstractValue<'tcx>,
417    forward: &ForwardVisitResult<'tcx>,
418    seen: &mut HashSet<PlaceKey>,
419) -> Option<usize> {
420    match value {
421        AbstractValue::Place(place) | AbstractValue::Ref(place) | AbstractValue::RawPtr(place) => {
422            pointer_origin_param_local_inner(tcx, caller, place, forward, seen)
423        }
424        AbstractValue::Cast(inner, _) => {
425            value_pointer_origin_param(tcx, caller, inner, forward, seen)
426        }
427        AbstractValue::CallResult(call) => {
428            call_pointer_origin_param(tcx, caller, call, forward, seen)
429        }
430        _ => None,
431    }
432}
rapx/verify/smt_check/alive.rs

rapx/verify/smt_check/
alive.rs
