rapx/check/senryx/
symbolic_analysis.rs

1//! Symbolic value domain and Z3 proof adapter for Senryx.
2//!
3//! The path visitor records lightweight symbolic definitions for MIR locals.
4//! Property checkers translate those definitions plus path constraints into Z3
5//! bit-vector formulas and prove obligations by checking that the negation is
6//! unsatisfiable.
7
8use rustc_middle::mir::{BinOp, UnOp};
9use std::collections::HashMap;
10
11use z3::ast::{Ast, BV, Bool};
12use z3::{Config, Context, SatResult, Solver};
13
14use crate::check::senryx::visitor::PlaceTy;
15
16/// Symbolic definition tracked for one MIR local.
17#[derive(Clone, Debug, PartialEq, Eq)]
18pub enum SymbolicDef<'tcx> {
19    Param(usize),
20    Constant(u128),
21    Use(usize),
22    Cast(usize, String),
23    Binary(BinOp, usize, AnaOperand),
24    UnOp(UnOp),
25    Call(String, Vec<AnaOperand>),
26    Ref(usize),
27    /// Pointer offset operation
28    PtrOffset(BinOp, usize, AnaOperand, PlaceTy<'tcx>),
29}
30
31/// Operand used inside symbolic definitions.
32#[derive(Clone, Debug, PartialEq, Eq)]
33pub enum AnaOperand {
34    Local(usize),
35    Const(u128),
36}
37
38/// Current symbolic value information for one MIR local.
39#[derive(Clone, Debug, Default)]
40pub struct ValueDomain<'tcx> {
41    pub def: Option<SymbolicDef<'tcx>>,
42    pub value_constraint: Option<u128>,
43}
44
45impl<'tcx> ValueDomain<'tcx> {
46    /// Return a concrete value when the domain has one.
47    pub fn get_constant(&self) -> Option<u128> {
48        if let Some(SymbolicDef::Constant(c)) = self.def {
49            Some(c)
50        } else {
51            self.value_constraint
52        }
53    }
54}
55
56/// Verifies a target property using Z3 SMT solver given variable domains and path constraints.
57/// Returns true if the property holds (UNSAT for negation), false otherwise.
58pub fn verify_with_z3<'tcx, F>(
59    values: HashMap<usize, ValueDomain<'tcx>>,
60    path_constraints: Vec<SymbolicDef<'tcx>>,
61    target_verifier: F,
62) -> bool
63where
64    F: for<'ctx> FnOnce(&'ctx Context, &HashMap<usize, BV<'ctx>>) -> Bool<'ctx>,
65{
66    let cfg = Config::new();
67    let ctx = Context::new(&cfg);
68    let solver = Solver::new(&ctx);
69
70    let mut z3_vars: HashMap<usize, BV> = HashMap::new();
71
72    // Debug Header
73    rap_debug!("\n=== Z3 Constraint Generation Start ===");
74
75    // Create symbolic bitvector variables for all locals
76    for local_index in values.keys() {
77        let name = format!("loc_{}", local_index);
78        z3_vars.insert(*local_index, BV::new_const(&ctx, name, 64));
79    }
80
81    // Encode variable definitions (assignments, operations) as solver constraints
82    for (local_idx, domain) in &values {
83        let current_var = match z3_vars.get(local_idx) {
84            Some(v) => v,
85            None => continue,
86        };
87
88        if let Some(ref def) = domain.def {
89            match def {
90                SymbolicDef::Cast(src_idx, _ty) => {
91                    if let Some(src_var) = z3_vars.get(src_idx) {
92                        rap_debug!("  [Def] _{} == _{} (Cast)", local_idx, src_idx);
93                        solver.assert(&current_var._eq(src_var));
94                    }
95                }
96                SymbolicDef::Binary(op, lhs_idx, rhs_op) => {
97                    if let (Some(lhs), Some(rhs)) =
98                        (z3_vars.get(lhs_idx), get_operand_bv(&ctx, rhs_op, &z3_vars))
99                    {
100                        let op_str = binop_to_str(op);
101                        let rhs_str = operand_to_str(rhs_op);
102                        rap_debug!(
103                            "  [Def] _{} == _{} {} {}",
104                            local_idx,
105                            lhs_idx,
106                            op_str,
107                            rhs_str
108                        );
109
110                        let result_expr = match op {
111                            BinOp::Rem => lhs.bvurem(&rhs),
112                            BinOp::Eq => lhs
113                                ._eq(&rhs)
114                                .ite(&BV::from_u64(&ctx, 1, 64), &BV::from_u64(&ctx, 0, 64)),
115                            BinOp::Ne => lhs
116                                ._eq(&rhs)
117                                .not()
118                                .ite(&BV::from_u64(&ctx, 1, 64), &BV::from_u64(&ctx, 0, 64)),
119                            BinOp::Add => lhs.bvadd(&rhs),
120                            BinOp::Sub => lhs.bvsub(&rhs),
121                            BinOp::Mul => lhs.bvmul(&rhs),
122                            BinOp::Div => lhs.bvudiv(&rhs),
123                            BinOp::BitAnd => lhs.bvand(&rhs),
124                            BinOp::BitOr => lhs.bvor(&rhs),
125                            BinOp::BitXor => lhs.bvxor(&rhs),
126                            BinOp::Shl => lhs.bvshl(&rhs),
127                            BinOp::Shr => lhs.bvlshr(&rhs),
128                            BinOp::Le => lhs
129                                .bvule(&rhs)
130                                .ite(&BV::from_u64(&ctx, 1, 64), &BV::from_u64(&ctx, 0, 64)),
131                            BinOp::Lt => lhs
132                                .bvult(&rhs)
133                                .ite(&BV::from_u64(&ctx, 1, 64), &BV::from_u64(&ctx, 0, 64)),
134                            BinOp::Gt => lhs
135                                .bvugt(&rhs)
136                                .ite(&BV::from_u64(&ctx, 1, 64), &BV::from_u64(&ctx, 0, 64)),
137                            BinOp::Ge => lhs
138                                .bvuge(&rhs)
139                                .ite(&BV::from_u64(&ctx, 1, 64), &BV::from_u64(&ctx, 0, 64)),
140                            _ => {
141                                rap_debug!("    [Warning] Z3: Unsupported Binary Op: {:?}", op);
142                                continue;
143                            }
144                        };
145                        solver.assert(&current_var._eq(&result_expr));
146                    }
147                }
148                SymbolicDef::Use(src_idx) => {
149                    if let Some(src_var) = z3_vars.get(src_idx) {
150                        rap_debug!("  [Def] _{} == _{}", local_idx, src_idx);
151                        solver.assert(&current_var._eq(src_var));
152                    }
153                }
154                SymbolicDef::PtrOffset(op, base, idx, stride) => {
155                    // Try to translate PtrOffset if stride is concrete
156                    if let PlaceTy::Ty(_, size) = stride {
157                        if let (Some(base_var), Some(idx_var)) =
158                            (z3_vars.get(base), get_operand_bv(&ctx, idx, &z3_vars))
159                        {
160                            let stride_bv = BV::from_u64(&ctx, *size as u64, 64);
161                            let byte_offset = idx_var.bvmul(&stride_bv);
162
163                            let op_str = match op {
164                                BinOp::Add | BinOp::Offset => "+",
165                                BinOp::Sub => "-",
166                                _ => "?",
167                            };
168                            let idx_str = operand_to_str(idx);
169
170                            rap_debug!(
171                                "  [Def] _{} == _{} {} ({} * {} bytes)",
172                                local_idx,
173                                base,
174                                op_str,
175                                idx_str,
176                                size
177                            );
178
179                            let res = match op {
180                                BinOp::Add => base_var.bvadd(&byte_offset),
181                                BinOp::Sub => base_var.bvsub(&byte_offset),
182                                _ => base_var.bvadd(&byte_offset),
183                            };
184                            solver.assert(&current_var._eq(&res));
185                        }
186                    } else {
187                        rap_debug!(
188                            "  [Def] _{} := PtrOffset(...) (Skipped: Generic/Unknown Stride)",
189                            local_idx
190                        );
191                    }
192                }
193                _ => {}
194            }
195        }
196        if let Some(val) = domain.value_constraint {
197            rap_debug!("  [Val] _{} == {}", local_idx, val);
198            let z3_val = BV::from_u64(&ctx, val as u64, 64);
199            solver.assert(&current_var._eq(&z3_val));
200        }
201    }
202
203    // Apply path constraints (e.g., branch conditions)
204    for constraint in path_constraints {
205        match constraint {
206            SymbolicDef::Binary(op, lhs_idx, rhs_op) => {
207                if let (Some(lhs), Some(rhs)) = (
208                    z3_vars.get(&lhs_idx),
209                    get_operand_bv(&ctx, &rhs_op, &z3_vars),
210                ) {
211                    let op_str = binop_to_str(&op);
212                    let rhs_str = operand_to_str(&rhs_op);
213                    rap_debug!("  [Path] _{} {} {}", lhs_idx, op_str, rhs_str);
214
215                    match op {
216                        BinOp::Eq => solver.assert(&lhs._eq(&rhs)),
217                        BinOp::Ne => solver.assert(&lhs._eq(&rhs).not()),
218                        BinOp::Lt => solver.assert(&lhs.bvult(&rhs)),
219                        BinOp::Le => solver.assert(&lhs.bvule(&rhs)),
220                        BinOp::Gt => solver.assert(&rhs.bvult(&lhs)),
221                        BinOp::Ge => solver.assert(&rhs.bvule(&lhs)),
222                        _ => {}
223                    }
224                }
225            }
226            _ => {}
227        }
228    }
229
230    // Assert negation of the target property
231    rap_debug!("  [Target] Asserting negation of target property...");
232    let target_prop = target_verifier(&ctx, &z3_vars);
233    solver.assert(&target_prop.not());
234
235    // Check satisfiability
236    let result = solver.check();
237
238    rap_debug!("=== Z3 Verify Finished ===");
239    debug_z3_solver_state(&solver, result, &z3_vars);
240
241    // UNSAT means no counter-example exists -> property holds
242    match result {
243        SatResult::Unsat => true,
244        _ => false,
245    }
246}
247
248// Helper function to handle Z3 solver debug outputs
249fn debug_z3_solver_state<'ctx>(
250    solver: &Solver<'ctx>,
251    result: SatResult,
252    z3_vars: &HashMap<usize, BV<'ctx>>,
253) {
254    match result {
255        SatResult::Unsat => {
256            rap_debug!("[Z3 Result] UNSAT (Verification Passed)");
257        }
258        SatResult::Sat => {
259            rap_debug!("[Z3 Result] SAT (Verification Failed) - Counter-example found:");
260
261            if let Some(model) = solver.get_model() {
262                // Extract and log specific values for variables in the model
263                let mut sorted_vars: Vec<_> = z3_vars.iter().collect();
264                sorted_vars.sort_by_key(|k| k.0);
265
266                rap_debug!("  --- Counter-example Values ---");
267                for (idx, bv) in sorted_vars {
268                    if let Some(interp) = model.eval(bv, true) {
269                        let val_str = interp
270                            .as_u64()
271                            .map(|v| v.to_string())
272                            .unwrap_or_else(|| interp.to_string());
273                        rap_debug!("  _{}: {}", idx, val_str);
274                    }
275                }
276                rap_debug!("  ------------------------------");
277            }
278        }
279        SatResult::Unknown => {
280            let reason = solver
281                .get_reason_unknown()
282                .unwrap_or_else(|| "Unknown".to_string());
283            rap_debug!("[Z3 Result] UNKNOWN. Reason: {}", reason);
284        }
285    }
286}
287
288fn get_operand_bv<'a>(
289    ctx: &'a Context,
290    op: &'a AnaOperand,
291    z3_vars: &'a HashMap<usize, BV>,
292) -> Option<BV<'a>> {
293    match op {
294        AnaOperand::Local(idx) => z3_vars.get(idx).cloned(),
295        AnaOperand::Const(val) => Some(BV::from_u64(ctx, *val as u64, 64)),
296    }
297}
298
299// Helper to format operands for debug
300fn operand_to_str(op: &AnaOperand) -> String {
301    match op {
302        AnaOperand::Local(id) => format!("_{}", id),
303        AnaOperand::Const(val) => format!("{}", val),
304    }
305}
306
307// Helper to format BinOp to string
308fn binop_to_str(op: &BinOp) -> &'static str {
309    match op {
310        BinOp::Add => "+",
311        BinOp::Sub => "-",
312        BinOp::Mul => "*",
313        BinOp::Div => "/",
314        BinOp::Rem => "%",
315        BinOp::BitXor => "^",
316        BinOp::BitAnd => "&",
317        BinOp::BitOr => "|",
318        BinOp::Shl => "<<",
319        BinOp::Shr => ">>",
320        BinOp::Eq => "==",
321        BinOp::Ne => "!=",
322        BinOp::Lt => "<",
323        BinOp::Le => "<=",
324        BinOp::Gt => ">",
325        BinOp::Ge => ">=",
326        BinOp::Offset => "offset",
327        _ => "?",
328    }
329}
rapx/check/senryx/symbolic_analysis.rs

rapx/check/senryx/
symbolic_analysis.rs
