rapx/analysis/senryx/
symbolic_analysis.rs

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

rapx/analysis/senryx/
symbolic_analysis.rs
