rapx/analysis/senryx/
symbolic_analysis.rs

1// use std::collections::HashMap;
2
3use rustc_middle::mir::{BinOp, UnOp};
4// use z3::ast::{Ast, BV, Bool};
5// use z3::{Config, Context, SatResult, Solver};
6
7// use crate::analysis::senryx::visitor::BodyVisitor;
8
9#[derive(Clone, Debug)]
10pub enum SymbolicDef {
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<usize>),
18    Ref(usize),
19}
20
21#[derive(Clone, Debug)]
22pub enum AnaOperand {
23    Local(usize),
24    Const(u128),
25}
26
27#[derive(Clone, Debug, Default)]
28pub struct ValueDomain {
29    pub def: Option<SymbolicDef>,
30    pub value_constraint: Option<u128>,
31    pub align: Option<(u64, u64)>,
32}
33
34// impl<'tcx> BodyVisitor<'tcx> {
35//     fn get_operand_bv(&'tcx self, ctx: &Context, op: &AnaOperand, z3_vars: &'tcx HashMap<usize, BV>) -> Option<BV> {
36//         match op {
37//             AnaOperand::Local(idx) => z3_vars.get(idx).cloned(),
38//             AnaOperand::Const(val) => Some(BV::from_u64(ctx, *val as u64, 64)),
39//         }
40//     }
41
42//     pub fn verify_with_z3<F>(&'tcx self, target_verifier: F) -> bool
43//     where
44//         F: FnOnce(&'tcx Context, &'tcx HashMap<usize, BV>) -> Bool<'tcx>
45//     {
46//         let cfg = Config::new();
47//         let ctx = Context::new(&cfg);
48//         let solver = Solver::new(&ctx);
49
50//         let mut z3_vars: HashMap<usize, BV> = HashMap::new();
51
52//         for local_index in self.value_domains.keys() {
53//             let name = format!("loc_{}", local_index);
54//             z3_vars.insert(*local_index, BV::new_const(&ctx, name, 64));
55//         }
56
57//         for (local_idx, domain) in &self.value_domains {
58//             let current_var = match z3_vars.get(local_idx) {
59//                 Some(v) => v,
60//                 None => continue,
61//             };
62
63//             if let Some(ref def) = domain.def {
64//                 match def {
65//                     SymbolicDef::Call(name, args) if name.contains("byte_add") && args.len() == 2 => {
66//                         if let (Some(lhs), Some(rhs)) = (z3_vars.get(&args[0]), z3_vars.get(&args[1])) {
67//                             solver.assert(&current_var._eq(&lhs.bvadd(rhs)));
68//                         }
69//                     },
70//                     SymbolicDef::Cast(src_idx, _) => {
71//                          if let Some(src_var) = z3_vars.get(src_idx) {
72//                             solver.assert(&current_var._eq(src_var));
73//                          }
74//                     },
75//                     SymbolicDef::Binary(op, lhs_idx, rhs_op) => {
76//                         if let (Some(lhs), Some(rhs)) = (z3_vars.get(lhs_idx), self.get_operand_bv(&ctx, rhs_op, &z3_vars)) {
77//                             let result_expr = match op {
78//                                 BinOp::Rem => lhs.bvurem(&rhs),
79//                                 BinOp::Eq => lhs._eq(&rhs).ite(&BV::from_u64(&ctx, 1, 64), &BV::from_u64(&ctx, 0, 64)),
80//                                 BinOp::Add => lhs.bvadd(&rhs),
81//                                 _ => continue,
82//                             };
83//                             solver.assert(&current_var._eq(&result_expr));
84//                         }
85//                     },
86//                     SymbolicDef::Use(src_idx) => {
87//                          if let Some(src_var) = z3_vars.get(src_idx) {
88//                             solver.assert(&current_var._eq(src_var));
89//                          }
90//                     }
91//                     _ => {}
92//                 }
93//             }
94//             if let Some(val) = domain.value_constraint {
95//                 let z3_val = BV::from_u64(&ctx, val as u64, 64);
96//                 solver.assert(&current_var._eq(&z3_val));
97//             }
98//         }
99
100//         let target_prop = target_verifier(&ctx, &z3_vars);
101//         solver.assert(&target_prop.not());
102
103//         match solver.check() {
104//             SatResult::Unsat => true,
105//             _ => false,
106//         }
107//     }
108
109//     pub fn verify_alignment(&self, local_idx: usize, required_align: u64) -> bool {
110//         self.verify_with_z3(|ctx, vars| {
111//             if let Some(var) = vars.get(&local_idx) {
112//                 let z3_align = BV::from_u64(ctx, required_align, 64);
113//                 let zero = BV::from_u64(ctx, 0, 64);
114//                 var.bvurem(&z3_align)._eq(&zero)
115//             } else {
116//                 Bool::from_bool(ctx, false)
117//             }
118//         })
119//     }
120// }
rapx/analysis/senryx/symbolic_analysis.rs

rapx/analysis/senryx/
symbolic_analysis.rs
