1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
//! Symbolic execution and constraint solving using Z3.
//!
//! This module provides symbolic execution capabilities for SSA analysis,
//! powered by the Z3 SMT solver. It enables:
//!
//! - Building symbolic expressions from SSA operations
//! - Solving constraints to find values that satisfy conditions
//! - Enumerating all solutions within a range
//! - Control flow unflattening by inverting state encodings
//!
//! # Architecture
//!
//! The module uses [`SymbolicExpr`] as an intermediate representation that
//! maps directly to SSA operations. When solving is needed, expressions are
//! translated to Z3's AST and solved using Z3's powerful SMT solver.
//!
//! ```text
//! SSA Operations → SymbolicExpr (our IR) → Z3 AST → Z3 Solver → Solutions
//! ```
//!
//! # Module Structure
//!
//! The target-agnostic IR + evaluator now live in `analyssa::analysis::symbolic`:
//!
//! - [`SymbolicOp`] - Symbolic operation kinds (add, xor, comparison, etc.) — `analyssa::analysis::symbolic::ops`
//! - [`SymbolicExpr`] - Symbolic expression tree — `analyssa::analysis::symbolic::expr`
//! - [`SymbolicEvaluator`] - Builds expressions from SSA operations — `analyssa::analysis::symbolic::evaluator`
//!
//! The Z3 binding stays in dotscope under the `z3` Cargo feature (analyssa
//! intentionally avoids the Z3 dependency):
//!
//! - [`Z3Solver`] - Z3-based constraint solver (this crate, gated on `z3`)
//!
//! # Use Cases
//!
//! ## Control Flow Unflattening
//!
//! The primary use case is inverting state encodings used by control flow
//! flattening obfuscators like ConfuserEx. These obfuscators use a pattern:
//!
//! ```text
//! switch_idx = f(state) // e.g., (state XOR C1) % N
//! switch (switch_idx) {
//! case 0: ...; state = g0(state); break;
//! case 1: ...; state = g1(state); break;
//! ...
//! }
//! ```
//!
//! Given `f(state)` as a symbolic expression and a target case index, we use
//! Z3 to solve for all state values that reach that case:
//!
//! ```text
//! solve: f(state) == target_case
//! ```
//!
//! ## Constraint Satisfaction
//!
//! More generally, the module can solve arbitrary constraints involving
//! bitvector arithmetic (32-bit):
//!
//! - Arithmetic: add, sub, mul, div, rem
//! - Bitwise: and, or, xor, not, shl, shr
//! - Comparisons: eq, ne, lt, gt, le, ge (signed and unsigned)
//!
//! # Example
//!
//! ```rust,ignore
//! use dotscope::analysis::{SymbolicExpr, SymbolicOp, Z3Solver};
//!
//! // Build expression: (state XOR 0x12345678) % 13
//! let state = SymbolicExpr::named("state");
//! let xored = SymbolicExpr::binary(SymbolicOp::Xor, state, SymbolicExpr::constant(0x12345678));
//! let result = SymbolicExpr::binary(SymbolicOp::RemU, xored, SymbolicExpr::constant(13));
//!
//! // Use Z3 to find all states that produce case index 5
//! let solver = Z3Solver::new();
//! let solutions = solver.solve_for_value(&result, "state", 5, 100);
//!
//! // Build mapping: case_index -> [state values that reach it]
//! let mapping = solver.build_case_mapping(&result, "state", 13, 10);
//! ```
//!
//! # Performance Considerations
//!
//! Z3 context creation has some overhead. For repeated solving, create a single
//! [`Z3Solver`] and reuse it. The solver uses 32-bit bitvectors (`BV(32)`) for
//! all computations, matching CIL's `int32` semantics.
// `SymbolicEvaluator`, `SymbolicExpr`, `SymbolicOp` live in
// `analyssa::analysis::symbolic`. The Z3 binding stays here behind the `z3`
// feature flag — Z3 is a dotscope-side dependency that analyssa intentionally
// doesn't take.
pub use ;
pub use Z3Solver;