rapx/check/senryx/verification/
align.rs

1//! Alignment contract checker for Senryx.
2//!
3//! This file owns all APIs related to `Align(ptr, T)` and path-sensitive
4//! alignment refinement. The checker can currently prove these alignment cases:
5//!
6//! 1. **Caller-provided contract facts**: the checked graph node already has a
7//!    contract fact such as `Align(ptr, T)`.
8//! 2. **Direct pointer/object compatibility**: the pointer's operational trace
9//!    state (OTS) is known aligned and the modeled pointee object has an ABI
10//!    alignment that is at least as strong as the contract-required type.
11//! 3. **Pointer arithmetic preservation**: the pointer was produced by a
12//!    recognized offset operation (`ptr.add`, `ptr.sub`, `ptr.offset`,
13//!    byte-level variants, or MIR `Offset`) and the Z3 model proves that every
14//!    modeled offset keeps the resulting address aligned for the required type.
15//! 4. **Runtime alignment guards**: branch refinement from calls such as
16//!    `ptr.is_aligned()` marks the checked pointer, and its traced source when
17//!    available, as aligned or unaligned on the corresponding path.
18//!
19//! The algorithm checks cheap local facts first: contract facts, then graph/OTS
20//! facts. It falls back to Z3 only when the graph records symbolic pointer
21//! arithmetic. Generic types are handled by enumerating the finite layout set
22//! discovered by `GenericChecker`; if that set is empty, the checker uses a
23//! conservative alignment/stride candidate set.
24
25use crate::{
26    analysis::utils::fn_info::{get_pointee, is_ptr, is_ref},
27    check::senryx::{
28        contract::{AlignState, PropertyContract},
29        symbolic_analysis::{AnaOperand, SymbolicDef, verify_with_z3},
30        visitor::{BodyVisitor, PlaceTy},
31    },
32    rap_debug,
33};
34use rustc_middle::{mir::BinOp, ty::Ty};
35use z3::ast::{Ast, BV};
36
37impl<'tcx> BodyVisitor<'tcx> {
38    /// Prove that `arg` satisfies the contract `Align(arg, contract_required_ty)`.
39    ///
40    /// The proof order is contract facts, then symbolic offset proof, then direct
41    /// graph/OTS alignment. The offset proof is tried before the direct check
42    /// because derived pointers normally carry their key alignment evidence in
43    /// `offset_from` rather than in the immediate pointee type alone.
44    pub fn check_align(&self, arg: usize, contract_required_ty: Ty<'tcx>) -> bool {
45        let required_ty_layout = self.visit_ty_and_get_layout(contract_required_ty);
46        if self.check_align_from_facts(arg, &required_ty_layout) {
47            return true;
48        }
49
50        if let Some((op, base_local, offset_op, stride_layout)) = self.get_ptr_offset_info(arg) {
51            return self.check_offset_align_with_z3(
52                op,
53                base_local,
54                offset_op,
55                stride_layout,
56                contract_required_ty,
57            );
58        }
59
60        self.check_align_directly(arg, required_ty_layout)
61    }
62
63    /// Check alignment facts that came directly from caller annotations.
64    fn check_align_from_facts(&self, arg: usize, required_layout: &PlaceTy<'tcx>) -> bool {
65        if let Some(var) = self.chains.get_var_node(arg) {
66            for fact in &var.facts.contracts {
67                if let PropertyContract::Align(fact_ty) = fact {
68                    let fact_layout = self.visit_ty_and_get_layout(*fact_ty);
69                    if Self::two_types_cast_check(fact_layout, required_layout.clone()) {
70                        return true;
71                    }
72                }
73            }
74        }
75        false
76    }
77
78    /// Check alignment from the current graph state and pointed object type.
79    fn check_align_directly(&self, pointer_id: usize, required_ty: PlaceTy<'tcx>) -> bool {
80        if let Some(pointee) = self.chains.get_obj_ty_through_chain(pointer_id) {
81            let pointee_ty = self.visit_ty_and_get_layout(pointee);
82            let pointer = self.chains.get_var_node(pointer_id).unwrap();
83
84            if let AlignState::Aligned(_) = pointer.ots.align {
85                return Self::two_types_cast_check(pointee_ty, required_ty);
86            }
87        }
88        false
89    }
90
91    /// Use Z3 to prove that pointer arithmetic preserves required alignment.
92    ///
93    /// The formula models `result = base +/- index * stride` and proves that
94    /// whenever the base address is aligned for each possible base alignment,
95    /// the result address is aligned for every required alignment.
96    fn check_offset_align_with_z3(
97        &self,
98        op: BinOp,
99        base_local: usize,
100        offset_op: AnaOperand,
101        stride_layout: PlaceTy<'tcx>,
102        contract_required_ty: Ty<'tcx>,
103    ) -> bool {
104        let req_layout = self.visit_ty_and_get_layout(contract_required_ty);
105        let mut req_aligns = req_layout.possible_aligns();
106
107        if let PlaceTy::GenericTy(..) = req_layout {
108            if req_aligns.is_empty() {
109                req_aligns.extend([1, 2, 4, 8, 16, 32, 64]);
110            }
111        }
112
113        if req_aligns.len() == 1 && req_aligns.contains(&1) {
114            return true;
115        }
116
117        let base_node = if let Some(node) = self.chains.get_var_node(base_local) {
118            node
119        } else {
120            return false;
121        };
122
123        let base_pointee_ty = if let Some(ty) = base_node.ty {
124            get_pointee(ty)
125        } else {
126            return false;
127        };
128
129        let base_layout = self.visit_ty_and_get_layout(base_pointee_ty);
130        let mut base_aligns = base_layout.possible_aligns();
131
132        if let PlaceTy::GenericTy(..) = base_layout {
133            if base_aligns.is_empty() {
134                base_aligns.extend([1, 2, 4, 8, 16, 32, 64]);
135            }
136        }
137
138        rap_debug!(
139            "Z3 Align Check: base_{} {:?} (aligns {:?}) {:?} offset (stride {:?}) => req_aligns {:?}",
140            base_local,
141            op,
142            base_aligns,
143            op,
144            stride_layout,
145            req_aligns
146        );
147
148        verify_with_z3(
149            self.value_domains.clone(),
150            self.path_constraints.clone(),
151            |ctx, vars| {
152                let bv_zero = BV::from_u64(ctx, 0, 64);
153
154                let bv_base = if let Some(b) = vars.get(&base_local) {
155                    b.clone()
156                } else {
157                    return z3::ast::Bool::from_bool(ctx, false);
158                };
159
160                let bv_index = match &offset_op {
161                    AnaOperand::Local(idx) => {
162                        if let Some(v) = vars.get(idx) {
163                            v.clone()
164                        } else {
165                            BV::from_u64(ctx, 0, 64)
166                        }
167                    }
168                    AnaOperand::Const(val) => BV::from_u64(ctx, *val as u64, 64),
169                };
170
171                let possible_strides: Vec<u64> = match &stride_layout {
172                    PlaceTy::Ty(_, size) => vec![*size as u64],
173                    PlaceTy::GenericTy(_, _, layout_set) => {
174                        if layout_set.is_empty() {
175                            vec![1, 2, 4, 8, 16, 32, 64]
176                        } else {
177                            layout_set.iter().map(|(_, size)| *size as u64).collect()
178                        }
179                    }
180                    PlaceTy::Unknown => vec![1],
181                };
182
183                let mut constraints = Vec::new();
184                let is_same_generic = match (&req_layout, &base_layout) {
185                    (PlaceTy::GenericTy(n1, _, _), PlaceTy::GenericTy(n2, _, _)) => n1 == n2,
186                    _ => false,
187                };
188
189                for stride in possible_strides {
190                    let bv_stride = BV::from_u64(ctx, stride, 64);
191                    let bv_byte_offset = bv_index.bvmul(&bv_stride);
192                    let result_ptr = match op {
193                        BinOp::Add => bv_base.bvadd(&bv_byte_offset),
194                        BinOp::Sub => bv_base.bvsub(&bv_byte_offset),
195                        _ => bv_base.bvadd(&bv_byte_offset),
196                    };
197
198                    if is_same_generic {
199                        for align in &req_aligns {
200                            let bv_align = BV::from_u64(ctx, *align as u64, 64);
201                            let base_is_aligned = bv_base.bvurem(&bv_align)._eq(&bv_zero);
202                            let result_aligned = result_ptr.bvurem(&bv_align)._eq(&bv_zero);
203                            constraints.push(base_is_aligned.implies(&result_aligned));
204                        }
205                    } else {
206                        for b_align in &base_aligns {
207                            for r_align in &req_aligns {
208                                let bv_base_align = BV::from_u64(ctx, *b_align as u64, 64);
209                                let bv_req_align = BV::from_u64(ctx, *r_align as u64, 64);
210                                let base_is_aligned = bv_base.bvurem(&bv_base_align)._eq(&bv_zero);
211                                let result_aligned = result_ptr.bvurem(&bv_req_align)._eq(&bv_zero);
212                                constraints.push(base_is_aligned.implies(&result_aligned));
213                            }
214                        }
215                    }
216                }
217
218                if constraints.is_empty() {
219                    return z3::ast::Bool::from_bool(ctx, false);
220                }
221
222                let constraints_refs: Vec<&z3::ast::Bool> = constraints.iter().collect();
223                z3::ast::Bool::and(ctx, &constraints_refs)
224            },
225        )
226    }
227
228    /// Return the pointer-offset summary attached to a graph node, if present.
229    fn get_ptr_offset_info(&self, arg: usize) -> Option<(BinOp, usize, AnaOperand, PlaceTy<'tcx>)> {
230        if let Some(domain) = self.chains.get_var_node(arg) {
231            if let Some(SymbolicDef::PtrOffset(op, base, off, place_ty)) = &domain.offset_from {
232                return Some((*op, *base, off.clone(), place_ty.clone()));
233            }
234        }
235        None
236    }
237
238    /// Refine the alignment state after a branch such as `ptr.is_aligned()`.
239    ///
240    /// `is_aligned == true` records an `Aligned(pointee_ty)` fact; `false`
241    /// records `Unaligned(pointee_ty)`. The visitor calls this on both the
242    /// condition operand and, when traceable, the source pointer.
243    pub fn update_align_state(&mut self, ptr_local: usize, is_aligned: bool) {
244        let ptr_ty_opt = self.chains.get_var_node(ptr_local).and_then(|n| n.ty);
245
246        if let Some(ptr_ty) = ptr_ty_opt {
247            if is_ptr(ptr_ty) || is_ref(ptr_ty) {
248                let pointee_ty = get_pointee(ptr_ty);
249
250                if let Some(ptr_node) = self.chains.get_var_node_mut(ptr_local) {
251                    if is_aligned {
252                        ptr_node.ots.align = AlignState::Aligned(pointee_ty);
253                        rap_debug!(
254                            "Refine State: _{} (source) marked as Aligned({:?}) via condition (True).",
255                            ptr_local,
256                            pointee_ty
257                        );
258                    } else {
259                        ptr_node.ots.align = AlignState::Unaligned(pointee_ty);
260                        rap_debug!(
261                            "Refine State: _{} (source) marked as Unaligned({:?}) via condition (False).",
262                            ptr_local,
263                            pointee_ty
264                        );
265                    }
266                }
267            }
268        }
269    }
270
271    /// Check a previously computed alignment state without re-running offset proof.
272    pub fn check_align_by_pre_computed_state(
273        &self,
274        arg: usize,
275        contract_required_ty: Ty<'tcx>,
276    ) -> bool {
277        if let Some(var) = self.chains.get_var_node(arg) {
278            if let AlignState::Aligned(state_ty) = var.ots.align {
279                let state_layout = self.visit_ty_and_get_layout(state_ty);
280                let req_layout = self.visit_ty_and_get_layout(contract_required_ty);
281
282                rap_debug!(
283                    "Check Align: arg_{} StateTy: {:?} vs ReqTy: {:?}",
284                    arg,
285                    state_layout,
286                    req_layout
287                );
288
289                return Self::two_types_cast_check(state_layout, req_layout);
290            } else {
291                rap_debug!("Check Align: arg_{} is Unaligned or Unknown", arg);
292            }
293        } else {
294            rap_debug!("Check Align: arg_{} node not found", arg);
295        }
296        false
297    }
298
299    /// Return true when every possible source alignment implies the destination alignment.
300    fn two_types_cast_check(src: PlaceTy<'tcx>, dest: PlaceTy<'tcx>) -> bool {
301        let src_aligns = src.possible_aligns();
302        let dest_aligns = dest.possible_aligns();
303        if dest_aligns.len() == 0 && src != dest {
304            return false;
305        }
306
307        for &d_align in &dest_aligns {
308            if d_align != 1 && src_aligns.len() == 0 {
309                return false;
310            }
311            for &s_align in &src_aligns {
312                if s_align < d_align {
313                    return false;
314                }
315            }
316        }
317        true
318    }
319
320    /// Try to strengthen a base pointer's alignment with numeric constraints.
321    fn _try_refine_alignment(&self, base_local: usize, current_align: u64) -> u64 {
322        for candidate in [64, 32, 16, 8, 4] {
323            if candidate <= current_align {
324                break;
325            }
326
327            let is_proven = verify_with_z3(
328                self.value_domains.clone(),
329                self.path_constraints.clone(),
330                |ctx, vars| {
331                    if let Some(bv_base) = vars.get(&base_local) {
332                        let bv_cand = BV::from_u64(ctx, candidate, 64);
333                        let bv_zero = BV::from_u64(ctx, 0, 64);
334                        bv_base.bvurem(&bv_cand)._eq(&bv_zero)
335                    } else {
336                        z3::ast::Bool::from_bool(ctx, false)
337                    }
338                },
339            );
340
341            if is_proven {
342                rap_debug!(
343                    "Refine Align: Successfully refined base_{} to align {}",
344                    base_local,
345                    candidate
346                );
347                return candidate;
348            }
349        }
350        current_align
351    }
352
353    /// Prove that a symbolic offset is a multiple of `align`.
354    fn _check_offset_is_aligned(&self, offset: &AnaOperand, align: u64) -> bool {
355        verify_with_z3(
356            self.value_domains.clone(),
357            self.path_constraints.clone(),
358            |ctx, vars| {
359                let bv_align = BV::from_u64(ctx, align, 64);
360                let bv_zero = BV::from_u64(ctx, 0, 64);
361
362                let bv_offset = match offset {
363                    AnaOperand::Local(idx) => {
364                        if let Some(v) = vars.get(idx) {
365                            v.clone()
366                        } else {
367                            BV::from_u64(ctx, 0, 64)
368                        }
369                    }
370                    AnaOperand::Const(val) => BV::from_u64(ctx, *val as u64, 64),
371                };
372
373                bv_offset.bvurem(&bv_align)._eq(&bv_zero)
374            },
375        )
376    }
377
378    /// Prove that an accumulated symbolic offset plus one current operand is aligned.
379    fn _check_cumulative_offset_aligned(
380        &self,
381        acc_def: &SymbolicDef<'tcx>,
382        curr_op: &AnaOperand,
383        align: u64,
384    ) -> bool {
385        verify_with_z3(
386            self.value_domains.clone(),
387            self.path_constraints.clone(),
388            |ctx, vars| {
389                let bv_align = BV::from_u64(ctx, align, 64);
390                let bv_zero = BV::from_u64(ctx, 0, 64);
391                let bv_acc = self.symbolic_def_to_bv(ctx, vars, acc_def);
392                let bv_curr = match curr_op {
393                    AnaOperand::Local(idx) => {
394                        if let Some(v) = vars.get(idx) {
395                            v.clone()
396                        } else {
397                            BV::from_u64(ctx, 0, 64)
398                        }
399                    }
400                    AnaOperand::Const(val) => BV::from_u64(ctx, *val as u64, 64),
401                };
402                let total = bv_acc.bvadd(&bv_curr);
403                total.bvurem(&bv_align)._eq(&bv_zero)
404            },
405        )
406    }
407
408    /// Convert a local symbolic definition to a Z3 bit-vector expression.
409    fn symbolic_def_to_bv<'a>(
410        &self,
411        ctx: &'a z3::Context,
412        vars: &std::collections::HashMap<usize, BV<'a>>,
413        def: &SymbolicDef<'tcx>,
414    ) -> BV<'a> {
415        match def {
416            SymbolicDef::Constant(c) => BV::from_u64(ctx, *c as u64, 64),
417            SymbolicDef::Use(l) => vars.get(l).cloned().unwrap_or(BV::from_u64(ctx, 0, 64)),
418            SymbolicDef::Binary(op, lhs, rhs) => {
419                let lhs_bv = vars.get(lhs).cloned().unwrap_or(BV::from_u64(ctx, 0, 64));
420                let rhs_bv = match rhs {
421                    AnaOperand::Local(l) => {
422                        vars.get(l).cloned().unwrap_or(BV::from_u64(ctx, 0, 64))
423                    }
424                    AnaOperand::Const(c) => BV::from_u64(ctx, *c as u64, 64),
425                };
426                match op {
427                    BinOp::Add => lhs_bv.bvadd(&rhs_bv),
428                    _ => BV::from_u64(ctx, 0, 64),
429                }
430            }
431            _ => BV::from_u64(ctx, 0, 64),
432        }
433    }
434}
rapx/check/senryx/verification/align.rs

rapx/check/senryx/verification/
align.rs
