rapx/analysis/senryx/
visitor_check.rs

1use std::collections::HashSet;
2
3use super::{
4    contracts::abstract_state::AlignState,
5    matcher::{UnsafeApi, get_arg_place},
6    visitor::{BodyVisitor, CheckResult, PlaceTy},
7};
8use crate::{
9    analysis::{
10        core::{
11            alias_analysis::AAResult,
12            dataflow::{DataFlowAnalysis, default::DataFlowAnalyzer},
13        },
14        senryx::{
15            contracts::property::{CisRange, CisRangeItem, PropertyContract},
16            symbolic_analysis::{AnaOperand, SymbolicDef, verify_with_z3},
17        },
18        utils::fn_info::{
19            display_hashmap, generate_contract_from_annotation_without_field_types,
20            generate_contract_from_std_annotation_json, get_cleaned_def_path_name, get_pointee,
21            is_ptr, is_ref, is_strict_ty_convert, reflect_generic,
22        },
23    },
24    rap_debug, rap_error, rap_info, rap_warn,
25};
26use rustc_data_structures::fx::FxHashMap;
27use rustc_hir::def_id::DefId;
28use rustc_middle::mir::BinOp;
29use rustc_middle::mir::Operand;
30use rustc_middle::mir::Place;
31use rustc_middle::ty::Ty;
32use rustc_span::Span;
33use rustc_span::source_map::Spanned;
34use z3::ast::Ast;
35use z3::ast::BV;
36
37impl<'tcx> BodyVisitor<'tcx> {
38    /// Entry point for handling standard library unsafe API calls and verifying their contracts.
39    pub fn handle_std_unsafe_call(
40        &mut self,
41        _dst_place: &Place<'_>,
42        def_id: &DefId,
43        args: &[Spanned<Operand>],
44        _path_index: usize,
45        _fn_map: &FxHashMap<DefId, AAResult>,
46        fn_span: Span,
47        fn_result: UnsafeApi,
48        generic_mapping: FxHashMap<String, Ty<'tcx>>,
49    ) {
50        let func_name = get_cleaned_def_path_name(self.tcx, *def_id);
51
52        // If the target API has contract annotation in signature,
53        // this fn-call could be replaced with 'generate_contract_from_annotation_without_field_types(self.tcx, *def_id);'
54        let args_with_contracts = generate_contract_from_std_annotation_json(self.tcx, *def_id);
55
56        for (idx, (base, fields, contract)) in args_with_contracts.iter().enumerate() {
57            rap_debug!("Find contract for {:?}, {base}: {:?}", def_id, contract);
58            let arg_tuple = get_arg_place(&args[*base].node);
59            // if this arg is a constant
60            if arg_tuple.0 {
61                continue; //TODO: check the constant value
62            } else {
63                let arg_place = self.chains.find_var_id_with_fields_seq(arg_tuple.1, fields);
64                self.check_contract(
65                    arg_place,
66                    args,
67                    contract.clone(),
68                    &generic_mapping,
69                    func_name.clone(),
70                    fn_span,
71                    idx,
72                );
73            }
74        }
75    }
76
77    /// Dispatcher function that validates a specific contract type.
78    pub fn check_contract(
79        &mut self,
80        arg: usize,
81        args: &[Spanned<Operand>],
82        contract: PropertyContract<'tcx>,
83        generic_mapping: &FxHashMap<String, Ty<'tcx>>,
84        func_name: String,
85        fn_span: Span,
86        idx: usize,
87    ) -> bool {
88        rap_debug!("Check contract {:?} for {:?}.", contract, func_name);
89        let (sp_name, check_result) = match contract {
90            PropertyContract::Align(ty) => {
91                let contract_required_ty = reflect_generic(generic_mapping, &func_name, ty);
92                let check_result = self.check_align(arg, contract_required_ty);
93                ("Align", check_result)
94            }
95            PropertyContract::InBound(ty, contract_len) => {
96                let contract_required_ty = reflect_generic(generic_mapping, &func_name, ty);
97                let check_result = self.check_inbound(arg, contract_len, contract_required_ty);
98                ("Inbound", check_result)
99            }
100            PropertyContract::NonNull => {
101                let check_result = self.check_non_null(arg);
102                ("NonNull", check_result)
103            }
104            PropertyContract::Typed(ty) => {
105                let check_result = self.check_typed(arg);
106                ("Typed", check_result)
107            }
108            PropertyContract::ValidPtr(ty, contract_len) => {
109                let contract_required_ty = reflect_generic(generic_mapping, &func_name, ty);
110                let check_result = self.check_valid_ptr(arg, contract_len, contract_required_ty);
111                ("ValidPtr", check_result)
112            }
113            _ => ("Unknown", false),
114        };
115
116        self.insert_checking_result(sp_name, check_result, func_name, fn_span, idx);
117        true
118    }
119
120    // ---------------------- Sp checking functions --------------------------
121
122    /// Taint Analysis: Check if the base pointer comes from a determined/aligned source.
123    /// Sources considered determined/aligned:
124    /// 1. References (Stack allocation) -> `&x`
125    /// 2. AddressOf (Stack allocation) -> `&raw x`
126    /// 3. Known aligned API calls -> `as_ptr`, `as_mut_ptr`, `alloc`
127    fn is_base_determined(&self, base_local: usize) -> bool {
128        if let Some(domain) = self.value_domains.get(&base_local) {
129            if let Some(def) = &domain.def {
130                match def {
131                    SymbolicDef::Ref(_) => return true, // &T is aligned
132                    SymbolicDef::Use(src) => return self.is_base_determined(*src), // Trace back
133                    SymbolicDef::Cast(src, _) => return self.is_base_determined(*src), // Trace back
134                    SymbolicDef::Call(func_name, _) => {
135                        // Whitelist aligned allocation/access APIs
136                        if func_name.contains("as_ptr")
137                            || func_name.contains("as_mut_ptr")
138                            || func_name.contains("alloc")
139                        {
140                            return true;
141                        }
142                    }
143                    _ => {}
144                }
145            }
146        }
147        // Check VariableNode properties if SymbolicDef didn't give strict answer
148        let points_to = self.chains.get_point_to_id(base_local);
149
150        // If it points to a known Allocated object (not Unknown/Param), it's likely determined locally
151        if points_to != base_local {
152            if let Some(target_node) = self.chains.get_var_node(points_to) {
153                // Check if target is a local stack variable (id < local_len)
154                if self.chains.is_local(target_node.id) {
155                    return true;
156                }
157            }
158        }
159
160        false
161    }
162
163    //  ------- End: Align checking functions -------
164
165    pub fn check_non_zst(&self, arg: usize) -> bool {
166        let obj_ty = self.chains.get_obj_ty_through_chain(arg);
167        if obj_ty.is_none() {
168            self.show_error_info(arg);
169        }
170        let ori_ty = self.visit_ty_and_get_layout(obj_ty.unwrap());
171        match ori_ty {
172            PlaceTy::Ty(_align, size) => size == 0,
173            PlaceTy::GenericTy(_, _, tys) => {
174                if tys.is_empty() {
175                    return false;
176                }
177                for (_, size) in tys {
178                    if size != 0 {
179                        return false;
180                    }
181                }
182                true
183            }
184            _ => false,
185        }
186    }
187
188    // checking the value ptr points to is valid for its type
189    pub fn check_typed(&self, arg: usize) -> bool {
190        let obj_ty = self.chains.get_obj_ty_through_chain(arg).unwrap();
191        let var = self.chains.get_var_node(arg);
192        let var_ty = var.unwrap().ty.unwrap();
193        if obj_ty != var_ty && is_strict_ty_convert(self.tcx, obj_ty, var_ty) {
194            return false;
195        }
196        self.check_init(arg)
197    }
198
199    pub fn check_non_null(&self, arg: usize) -> bool {
200        let point_to_id = self.chains.get_point_to_id(arg);
201        let var_ty = self.chains.get_var_node(point_to_id);
202        if var_ty.is_none() {
203            self.show_error_info(arg);
204        }
205        var_ty.unwrap().ots.nonnull
206    }
207
208    // check each field's init state in the tree.
209    // check arg itself when it doesn't have fields.
210    pub fn check_init(&self, arg: usize) -> bool {
211        let point_to_id = self.chains.get_point_to_id(arg);
212        let var = self.chains.get_var_node(point_to_id);
213        if var.unwrap().field.is_empty() {
214            let mut init_flag = true;
215            for field in &var.unwrap().field {
216                init_flag &= self.check_init(*field.1);
217            }
218            init_flag
219        } else {
220            var.unwrap().ots.init
221        }
222    }
223
224    pub fn check_allocator_consistency(&self, _func_name: String, _arg: usize) -> bool {
225        true
226    }
227
228    pub fn check_allocated(&self, _arg: usize) -> bool {
229        true
230    }
231
232    pub fn check_inbound(
233        &self,
234        arg: usize,
235        length_arg: CisRangeItem,
236        contract_ty: Ty<'tcx>,
237    ) -> bool {
238        false
239    }
240
241    pub fn check_valid_string(&self, _arg: usize) -> bool {
242        true
243    }
244
245    pub fn check_valid_cstr(&self, _arg: usize) -> bool {
246        true
247    }
248
249    pub fn check_valid_num(&self, _arg: usize) -> bool {
250        true
251    }
252
253    pub fn check_alias(&self, _arg: usize) -> bool {
254        true
255    }
256
257    // --------------------- Checking Compound SPs ---------------------
258
259    pub fn check_valid_ptr(
260        &self,
261        arg: usize,
262        length_arg: CisRangeItem,
263        contract_ty: Ty<'tcx>,
264    ) -> bool {
265        !self.check_non_zst(arg)
266            || (self.check_non_zst(arg) && self.check_deref(arg, length_arg, contract_ty))
267    }
268
269    pub fn check_deref(&self, arg: usize, length_arg: CisRangeItem, contract_ty: Ty<'tcx>) -> bool {
270        self.check_allocated(arg) && self.check_inbound(arg, length_arg, contract_ty)
271    }
272
273    pub fn check_ref_to_ptr(
274        &self,
275        arg: usize,
276        length_arg: CisRangeItem,
277        contract_ty: Ty<'tcx>,
278    ) -> bool {
279        self.check_deref(arg, length_arg, contract_ty)
280            && self.check_init(arg)
281            && self.check_align(arg, contract_ty)
282            && self.check_alias(arg)
283    }
284
285    // -------------------------- helper functions: insert checking results --------------------------
286
287    // Insert result general API
288    pub fn insert_checking_result(
289        &mut self,
290        sp: &str,
291        is_passed: bool,
292        func_name: String,
293        fn_span: Span,
294        idx: usize,
295    ) {
296        if sp == "Unknown" {
297            return;
298        }
299        if is_passed {
300            self.insert_successful_check_result(func_name.clone(), fn_span, idx + 1, sp);
301        } else {
302            self.insert_failed_check_result(func_name.clone(), fn_span, idx + 1, sp);
303        }
304    }
305
306    // Insert falied SP result
307    pub fn insert_failed_check_result(
308        &mut self,
309        func_name: String,
310        fn_span: Span,
311        idx: usize,
312        sp: &str,
313    ) {
314        if let Some(existing) = self
315            .check_results
316            .iter_mut()
317            .find(|result| result.func_name == func_name && result.func_span == fn_span)
318        {
319            if let Some(passed_set) = existing.passed_contracts.get_mut(&idx) {
320                passed_set.remove(sp);
321                if passed_set.is_empty() {
322                    existing.passed_contracts.remove(&idx);
323                }
324            }
325            existing
326                .failed_contracts
327                .entry(idx)
328                .and_modify(|set| {
329                    set.insert(sp.to_string());
330                })
331                .or_insert_with(|| {
332                    let mut new_set = HashSet::new();
333                    new_set.insert(sp.to_string());
334                    new_set
335                });
336        } else {
337            let mut new_result = CheckResult::new(&func_name, fn_span);
338            new_result
339                .failed_contracts
340                .insert(idx, HashSet::from([sp.to_string()]));
341            self.check_results.push(new_result);
342        }
343    }
344
345    // Insert successful SP result
346    pub fn insert_successful_check_result(
347        &mut self,
348        func_name: String,
349        fn_span: Span,
350        idx: usize,
351        sp: &str,
352    ) {
353        if let Some(existing) = self
354            .check_results
355            .iter_mut()
356            .find(|result| result.func_name == func_name && result.func_span == fn_span)
357        {
358            if let Some(failed_set) = existing.failed_contracts.get_mut(&idx) {
359                if failed_set.contains(sp) {
360                    return;
361                }
362            }
363
364            existing
365                .passed_contracts
366                .entry(idx)
367                .and_modify(|set| {
368                    set.insert(sp.to_string());
369                })
370                .or_insert_with(|| HashSet::from([sp.to_string()]));
371        } else {
372            let mut new_result = CheckResult::new(&func_name, fn_span);
373            new_result
374                .passed_contracts
375                .insert(idx, HashSet::from([sp.to_string()]));
376            self.check_results.push(new_result);
377        }
378    }
379
380    pub fn show_error_info(&self, arg: usize) {
381        rap_warn!(
382            "In func {:?}, visitor checker error! Can't get {arg} in chain!",
383            get_cleaned_def_path_name(self.tcx, self.def_id)
384        );
385        display_hashmap(&self.chains.variables, 1);
386    }
387}
388
389/// Impl block for Align check
390/// Align checking functions
391impl<'tcx> BodyVisitor<'tcx> {
392    // Main API for align check
393    pub fn check_align(&self, arg: usize, contract_required_ty: Ty<'tcx>) -> bool {
394        let required_ty_layout = self.visit_ty_and_get_layout(contract_required_ty);
395        if self.check_align_from_cis(arg, &required_ty_layout) {
396            return true;
397        }
398        // check offset
399        if let Some((op, base_local, offset_op, stride_layout)) = self.get_ptr_offset_info(arg) {
400            return self.check_offset_align_with_z3(
401                op,
402                base_local,
403                offset_op,
404                stride_layout,
405                contract_required_ty,
406            );
407        }
408
409        // If no offset or cannot derive, try direct type casting check
410        self.check_align_directly(arg, required_ty_layout)
411    }
412
413    /// First check for Align.
414    /// If this var has contextual invariant state (cis), like:
415    ///      #[rapx::proof::Align::(x, usize)]
416    ///      pub fn test(x: *const usize) { ... }
417    /// CIS will record 'x: Align(usize)' information for align check
418    fn check_align_from_cis(&self, arg: usize, required_layout: &PlaceTy<'tcx>) -> bool {
419        if let Some(var) = self.chains.get_var_node(arg) {
420            for cis in &var.cis.contracts {
421                if let PropertyContract::Align(cis_ty) = cis {
422                    let cis_layout = self.visit_ty_and_get_layout(*cis_ty);
423                    if Self::two_types_cast_check(cis_layout, required_layout.clone()) {
424                        return true;
425                    }
426                }
427            }
428        }
429        false
430    }
431
432    /// Second check for Align.
433    /// If no offset, check the type of ptr an its pointed object's type directly
434    fn check_align_directly(&self, pointer_id: usize, required_ty: PlaceTy<'tcx>) -> bool {
435        if let Some(pointee) = self.chains.get_obj_ty_through_chain(pointer_id) {
436            let pointee_ty = self.visit_ty_and_get_layout(pointee);
437            let pointer = self.chains.get_var_node(pointer_id).unwrap();
438
439            // If the pointer has an explicitly recorded aligned state
440            if let AlignState::Aligned(_) = pointer.ots.align {
441                return Self::two_types_cast_check(pointee_ty, required_ty);
442            }
443        }
444        false
445    }
446
447    /// Third check for Align.
448    /// If ptr has Offset, use Z3 to solve constraints.
449    /// Assuming `offset_op` is the accumulated offset from `base_local`.
450    fn check_offset_align_with_z3(
451        &self,
452        op: BinOp,
453        base_local: usize,
454        offset_op: AnaOperand,
455        stride_layout: PlaceTy<'tcx>,
456        contract_required_ty: Ty<'tcx>,
457    ) -> bool {
458        // 1. get target type (Req) layout and alignment requirements
459        let req_layout = self.visit_ty_and_get_layout(contract_required_ty);
460        let mut req_aligns = req_layout.possible_aligns();
461
462        // handle generic types: if target is generic and has no alignment constraints, check all common alignments (1~64)
463        if let PlaceTy::GenericTy(..) = req_layout {
464            if req_aligns.is_empty() {
465                req_aligns.extend([1, 2, 4, 8, 16, 32, 64]);
466            }
467        }
468
469        // opt: if only alignment 1 is required, it's always safe
470        if req_aligns.len() == 1 && req_aligns.contains(&1) {
471            return true;
472        }
473
474        // 2. get base node
475        let base_node = if let Some(node) = self.chains.get_var_node(base_local) {
476            node
477        } else {
478            return false;
479        };
480
481        // if base type is unknown, cannot assume base is aligned
482        let base_pointee_ty = if let Some(ty) = base_node.ty {
483            // Note: here we need the pointee type, not the pointer type itself
484            crate::analysis::utils::fn_info::get_pointee(ty)
485        } else {
486            return false;
487        };
488
489        let base_layout = self.visit_ty_and_get_layout(base_pointee_ty);
490        let mut base_aligns = base_layout.possible_aligns();
491
492        // handle generic types: Base is also generic, extend its possible alignments
493        if let PlaceTy::GenericTy(..) = base_layout {
494            if base_aligns.is_empty() {
495                base_aligns.extend([1, 2, 4, 8, 16, 32, 64]);
496            }
497        }
498
499        rap_debug!(
500            "Z3 Align Check: base_{} {:?} (aligns {:?}) {:?} offset (stride {:?}) => req_aligns {:?}",
501            base_local,
502            op,
503            base_aligns,
504            op,
505            stride_layout,
506            req_aligns
507        );
508
509        verify_with_z3(
510            self.value_domains.clone(),
511            self.path_constraints.clone(),
512            |ctx, vars| {
513                let bv_zero = BV::from_u64(ctx, 0, 64);
514
515                // Model Base address
516                let bv_base = if let Some(b) = vars.get(&base_local) {
517                    b.clone()
518                } else {
519                    // if base address is not available, return false
520                    return z3::ast::Bool::from_bool(ctx, false);
521                };
522
523                // Model Index
524                let bv_index = match &offset_op {
525                    AnaOperand::Local(idx) => {
526                        if let Some(v) = vars.get(idx) {
527                            v.clone()
528                        } else {
529                            BV::from_u64(ctx, 0, 64)
530                        }
531                    }
532                    AnaOperand::Const(val) => BV::from_u64(ctx, *val as u64, 64),
533                };
534
535                // Model Stride
536                let possible_strides: Vec<u64> = match &stride_layout {
537                    PlaceTy::Ty(_, size) => vec![*size as u64],
538                    PlaceTy::GenericTy(_, _, layout_set) => {
539                        if layout_set.is_empty() {
540                            // Generic type with no size constraints, check all common strides
541                            vec![1, 2, 4, 8, 16, 32, 64]
542                        } else {
543                            layout_set.iter().map(|(_, size)| *size as u64).collect()
544                        }
545                    }
546                    PlaceTy::Unknown => vec![1],
547                };
548
549                let mut constraints = Vec::new();
550
551                // Coupling check: are Req and Base the same generic parameter?
552                let is_same_generic = match (&req_layout, &base_layout) {
553                    (PlaceTy::GenericTy(n1, _, _), PlaceTy::GenericTy(n2, _, _)) => n1 == n2,
554                    _ => false,
555                };
556
557                // check all Strides
558                for stride in possible_strides {
559                    let bv_stride = BV::from_u64(ctx, stride, 64);
560                    let bv_byte_offset = bv_index.bvmul(&bv_stride);
561
562                    // Model Result Pointer
563                    let result_ptr = match op {
564                        BinOp::Add => bv_base.bvadd(&bv_byte_offset),
565                        BinOp::Sub => bv_base.bvsub(&bv_byte_offset),
566                        _ => bv_base.bvadd(&bv_byte_offset), // default Add
567                    };
568
569                    if is_same_generic {
570                        // Same generic type: if Base satisfies alignment A, result must also satisfy A
571                        for align in &req_aligns {
572                            let bv_align = BV::from_u64(ctx, *align as u64, 64);
573
574                            // Precondition
575                            let base_is_aligned = bv_base.bvurem(&bv_align)._eq(&bv_zero);
576                            // Postcondition
577                            let result_aligned = result_ptr.bvurem(&bv_align)._eq(&bv_zero);
578
579                            constraints.push(base_is_aligned.implies(&result_aligned));
580                        }
581                    } else {
582                        // Different types: Base satisfies its own alignment => Result satisfies target alignment
583                        for b_align in &base_aligns {
584                            for r_align in &req_aligns {
585                                let bv_base_align = BV::from_u64(ctx, *b_align as u64, 64);
586                                let bv_req_align = BV::from_u64(ctx, *r_align as u64, 64);
587
588                                let base_is_aligned = bv_base.bvurem(&bv_base_align)._eq(&bv_zero);
589                                let result_aligned = result_ptr.bvurem(&bv_req_align)._eq(&bv_zero);
590
591                                constraints.push(base_is_aligned.implies(&result_aligned));
592                            }
593                        }
594                    }
595                }
596
597                if constraints.is_empty() {
598                    // No constraints generated, return false
599                    return z3::ast::Bool::from_bool(ctx, false);
600                }
601
602                // Must satisfy all generated constraints (AND)
603                let constraints_refs: Vec<&z3::ast::Bool> = constraints.iter().collect();
604                z3::ast::Bool::and(ctx, &constraints_refs)
605            },
606        )
607    }
608
609    // If the arg has offset from its pointed object, this function will return:
610    fn get_ptr_offset_info(&self, arg: usize) -> Option<(BinOp, usize, AnaOperand, PlaceTy<'tcx>)> {
611        if let Some(domain) = self.chains.get_var_node(arg) {
612            if let Some(def) = &domain.offset_from {
613                match def {
614                    SymbolicDef::PtrOffset(op, base, off, place_ty) => {
615                        return Some((*op, *base, off.clone(), place_ty.clone()));
616                    }
617                    _ => {}
618                }
619            }
620        }
621        None
622    }
623
624    /// Updates the alignment state of the given local variable.
625    /// is_aligned = true  -> Aligned
626    /// is_aligned = false -> Unaligned
627    pub fn update_align_state(&mut self, ptr_local: usize, is_aligned: bool) {
628        // Get type info
629        let ptr_ty_opt = self.chains.get_var_node(ptr_local).and_then(|n| n.ty);
630
631        if let Some(ptr_ty) = ptr_ty_opt {
632            if is_ptr(ptr_ty) || is_ref(ptr_ty) {
633                let pointee_ty = get_pointee(ptr_ty);
634
635                if let Some(ptr_node) = self.chains.get_var_node_mut(ptr_local) {
636                    if is_aligned {
637                        ptr_node.ots.align = AlignState::Aligned(pointee_ty);
638                        rap_debug!(
639                            "Refine State: _{} (source) marked as Aligned({:?}) via condition (True).",
640                            ptr_local,
641                            pointee_ty
642                        );
643                    } else {
644                        ptr_node.ots.align = AlignState::Unaligned(pointee_ty);
645
646                        rap_debug!(
647                            "Refine State: _{} (source) marked as Unaligned({:?}) via condition (False).",
648                            ptr_local,
649                            pointee_ty
650                        );
651                    }
652                }
653            }
654        }
655    }
656
657    /// Checks if the argument satisfies the alignment requirements of the contract.
658    /// Retrieves the pre-computed state from the graph and compares types.
659    pub fn check_align_by_pre_computed_state(
660        &self,
661        arg: usize,
662        contract_required_ty: Ty<'tcx>,
663    ) -> bool {
664        // 1. Retrieve the variable node from the graph
665        if let Some(var) = self.chains.get_var_node(arg) {
666            // 2. Check if the state is marked as 'Aligned'
667            if let AlignState::Aligned(state_ty) = var.ots.align {
668                // 3. Compare the state's recorded type with the contract's required type
669                // We assume the pointer is aligned for `state_ty`. We must ensure
670                // `state_ty` alignment implies `contract_required_ty` alignment.
671                let state_layout = self.visit_ty_and_get_layout(state_ty);
672                let req_layout = self.visit_ty_and_get_layout(contract_required_ty);
673
674                rap_debug!(
675                    "Check Align: arg_{} StateTy: {:?} vs ReqTy: {:?}",
676                    arg,
677                    state_layout,
678                    req_layout
679                );
680
681                // True if Src alignment requirements >= Dest alignment requirements
682                return Self::two_types_cast_check(state_layout, req_layout);
683            } else {
684                rap_debug!("Check Align: arg_{} is Unaligned or Unknown", arg);
685            }
686        } else {
687            rap_debug!("Check Align: arg_{} node not found", arg);
688        }
689        false
690    }
691
692    // Helper function: check whether type cast is aligned.
693    fn two_types_cast_check(src: PlaceTy<'tcx>, dest: PlaceTy<'tcx>) -> bool {
694        let src_aligns = src.possible_aligns();
695        let dest_aligns = dest.possible_aligns();
696        if dest_aligns.len() == 0 && src != dest {
697            // dst ty could be arbitrary type && src and dst are different types
698            return false;
699        }
700
701        for &d_align in &dest_aligns {
702            if d_align != 1 && src_aligns.len() == 0 {
703                // src ty could be arbitrary type
704                return false;
705            }
706            for &s_align in &src_aligns {
707                if s_align < d_align {
708                    return false;
709                }
710            }
711        }
712        true
713    }
714
715    /// Attempts to prove a stricter alignment for the base pointer using Z3 and path constraints.
716    fn try_refine_alignment(&self, base_local: usize, current_align: u64) -> u64 {
717        // Check alignments in descending order: 64, 32, 16, 8, 4
718        for candidate in [64, 32, 16, 8, 4] {
719            if candidate <= current_align {
720                break;
721            }
722
723            let is_proven = verify_with_z3(
724                self.value_domains.clone(),
725                self.path_constraints.clone(),
726                |ctx, vars| {
727                    if let Some(bv_base) = vars.get(&base_local) {
728                        let bv_cand = BV::from_u64(ctx, candidate, 64);
729                        let bv_zero = BV::from_u64(ctx, 0, 64);
730                        // Prove: base % candidate == 0
731                        bv_base.bvurem(&bv_cand)._eq(&bv_zero)
732                    } else {
733                        z3::ast::Bool::from_bool(ctx, false)
734                    }
735                },
736            );
737
738            if is_proven {
739                rap_debug!(
740                    "Refine Align: Successfully refined base_{} to align {}",
741                    base_local,
742                    candidate
743                );
744                return candidate;
745            }
746        }
747        current_align
748    }
749
750    /// Checks if the offset is a multiple of the required alignment using Z3.
751    fn check_offset_is_aligned(&self, _base_local: usize, offset: &AnaOperand, align: u64) -> bool {
752        verify_with_z3(
753            self.value_domains.clone(),
754            self.path_constraints.clone(),
755            |ctx, vars| {
756                let bv_align = BV::from_u64(ctx, align, 64);
757                let bv_zero = BV::from_u64(ctx, 0, 64);
758
759                let bv_offset = match offset {
760                    AnaOperand::Local(idx) => {
761                        if let Some(v) = vars.get(idx) {
762                            v.clone()
763                        } else {
764                            BV::from_u64(ctx, 0, 64)
765                        }
766                    }
767                    AnaOperand::Const(val) => BV::from_u64(ctx, *val as u64, 64),
768                };
769
770                // Prove: offset % align == 0
771                bv_offset.bvurem(&bv_align)._eq(&bv_zero)
772            },
773        )
774    }
775
776    /// Checks if (AccumulatedDef + CurrentOp) % Align == 0 using Z3.
777    fn check_cumulative_offset_aligned(
778        &self,
779        _base_local: usize,
780        acc_def: &SymbolicDef,
781        curr_op: &AnaOperand,
782        align: u64,
783    ) -> bool {
784        verify_with_z3(
785            self.value_domains.clone(),
786            self.path_constraints.clone(),
787            |ctx, vars| {
788                let bv_align = BV::from_u64(ctx, align, 64);
789                let bv_zero = BV::from_u64(ctx, 0, 64);
790                let bv_acc = self.symbolic_def_to_bv(ctx, vars, acc_def);
791                let bv_curr = match curr_op {
792                    AnaOperand::Local(idx) => {
793                        if let Some(v) = vars.get(idx) {
794                            v.clone()
795                        } else {
796                            BV::from_u64(ctx, 0, 64)
797                        }
798                    }
799                    AnaOperand::Const(val) => BV::from_u64(ctx, *val as u64, 64),
800                };
801                let total = bv_acc.bvadd(&bv_curr);
802                // Prove: (acc + curr) % align == 0
803                total.bvurem(&bv_align)._eq(&bv_zero)
804            },
805        )
806    }
807
808    // Helper: Converts Operand to SymbolicDef
809    fn operand_to_symbolic_def(&self, op: AnaOperand) -> SymbolicDef<'tcx> {
810        match op {
811            AnaOperand::Local(l) => SymbolicDef::Use(l),
812            AnaOperand::Const(c) => SymbolicDef::Constant(c),
813        }
814    }
815
816    // Helper: Combines two offsets into a SymbolicDef (Simplified)
817    fn combine_offsets(&self, def: SymbolicDef<'tcx>, op: AnaOperand) -> SymbolicDef<'tcx> {
818        match (def, op) {
819            (SymbolicDef::Constant(c1), AnaOperand::Const(c2)) => SymbolicDef::Constant(c1 + c2),
820            (SymbolicDef::Use(l), o) => SymbolicDef::Binary(BinOp::Add, l, o),
821            (d, _) => d,
822        }
823    }
824
825    // Helper: Converts SymbolicDef to Z3 BitVector
826    fn symbolic_def_to_bv<'a>(
827        &self,
828        ctx: &'a z3::Context,
829        vars: &std::collections::HashMap<usize, BV<'a>>,
830        def: &SymbolicDef,
831    ) -> BV<'a> {
832        match def {
833            SymbolicDef::Constant(c) => BV::from_u64(ctx, *c as u64, 64),
834            SymbolicDef::Use(l) => vars.get(l).cloned().unwrap_or(BV::from_u64(ctx, 0, 64)),
835            SymbolicDef::Binary(op, lhs, rhs) => {
836                let lhs_bv = vars.get(lhs).cloned().unwrap_or(BV::from_u64(ctx, 0, 64));
837                let rhs_bv = match rhs {
838                    AnaOperand::Local(l) => {
839                        vars.get(l).cloned().unwrap_or(BV::from_u64(ctx, 0, 64))
840                    }
841                    AnaOperand::Const(c) => BV::from_u64(ctx, *c as u64, 64),
842                };
843                match op {
844                    BinOp::Add => lhs_bv.bvadd(&rhs_bv),
845                    _ => BV::from_u64(ctx, 0, 64),
846                }
847            }
848            _ => BV::from_u64(ctx, 0, 64),
849        }
850    }
851}
rapx/analysis/senryx/visitor_check.rs

rapx/analysis/senryx/
visitor_check.rs
