Coverage for src/alprina_cli/agents/web3_auditor/symbolic_executor.py: 0%

1""" 

2Symbolic Execution Engine for Solidity Smart Contracts 

3 

4WEEK 3 DAY 1: Symbolic Execution 

5================================= 

6 

7Implements symbolic execution to detect vulnerabilities through path analysis 

8and constraint solving. Uses Z3 theorem prover for constraint satisfaction. 

9 

10Author: Alprina Development Team 

11Date: 2025-11-12 

12 

13References: 

14- OYENTE: Symbolic execution for Ethereum (2016) 

15- Mythril: Constraint-based vulnerability detection 

16- Manticore: Dynamic symbolic execution 

17""" 

18 

19import re 

20from typing import List, Dict, Any, Optional, Set, Tuple 

21from dataclasses import dataclass, field 

22from enum import Enum 

23import z3 

24 

25try: 

26 from .solidity_analyzer import SolidityVulnerability, VulnerabilityType 

27except ImportError: 

28 # For standalone testing 

29 import sys 

30 from pathlib import Path 

31 sys.path.insert(0, str(Path(__file__).parent)) 

32 from solidity_analyzer import SolidityVulnerability, VulnerabilityType 

33 

34 

35class SymbolicType(Enum): 

36 """Types in symbolic execution""" 

37 UINT256 = "uint256" 

38 INT256 = "int256" 

39 ADDRESS = "address" 

40 BOOL = "bool" 

41 BYTES32 = "bytes32" 

42 UNKNOWN = "unknown" 

43 

44 

45@dataclass 

46class SymbolicVariable: 

47 """Represents a symbolic variable during execution""" 

48 name: str 

49 sym_type: SymbolicType 

50 z3_var: z3.ExprRef 

51 is_tainted: bool = False # From user input 

52 source_line: Optional[int] = None 

53 

54 

55@dataclass 

56class PathConstraint: 

57 """Represents a constraint along an execution path""" 

58 condition: str 

59 z3_constraint: z3.BoolRef 

60 line_number: int 

61 is_true_branch: bool # True if we took the "true" branch 

62 

63 

64@dataclass 

65class SymbolicState: 

66 """State during symbolic execution""" 

67 variables: Dict[str, SymbolicVariable] = field(default_factory=dict) 

68 constraints: List[PathConstraint] = field(default_factory=list) 

69 storage: Dict[str, SymbolicVariable] = field(default_factory=dict) 

70 memory: Dict[str, SymbolicVariable] = field(default_factory=dict) 

71 execution_path: List[int] = field(default_factory=list) # Line numbers 

72 

73 def copy(self) -> 'SymbolicState': 

74 """Create a copy of this state for branch exploration""" 

75 import copy 

76 return copy.deepcopy(self) 

77 

78 

79@dataclass 

80class SymbolicVulnerability: 

81 """Vulnerability found via symbolic execution""" 

82 vulnerability_type: str 

83 severity: str 

84 title: str 

85 description: str 

86 line_number: int 

87 function_name: str 

88 proof: Optional[str] = None # Z3 model showing exploit 

89 path_constraints: List[str] = field(default_factory=list) 

90 confidence: int = 95 

91 

92 

93class SymbolicExecutor: 

94 """ 

95 Symbolic execution engine for Solidity contracts 

96 

97 Capabilities: 

98 - Integer overflow/underflow detection via constraint solving 

99 - Unreachable code detection 

100 - Taint analysis for user inputs 

101 - Path feasibility analysis 

102 - Division by zero detection 

103 

104 Week 3 Day 1 Implementation: 

105 - Basic symbolic execution framework 

106 - Integer overflow detection with Z3 

107 - Simple path exploration 

108 """ 

109 

110 def __init__(self): 

111 self.solver = z3.Solver() 

112 self.vulnerabilities: List[SymbolicVulnerability] = [] 

113 

114 # Z3 constants for Solidity types 

115 self.MAX_UINT256 = 2**256 - 1 

116 self.MIN_INT256 = -(2**255) 

117 self.MAX_INT256 = 2**255 - 1 

118 

119 def analyze_contract(self, contract_code: str, file_path: str) -> List[SolidityVulnerability]: 

120 """ 

121 Analyze contract using symbolic execution 

122 

123 Returns standard SolidityVulnerability objects for integration 

124 with existing Week 2 economic impact calculator 

125 """ 

126 self.vulnerabilities = [] 

127 

128 # Extract functions from contract 

129 functions = self._extract_functions(contract_code) 

130 

131 for func in functions: 

132 # Symbolically execute each function 

133 self._execute_function(func, file_path) 

134 

135 # Convert to standard format 

136 return self._convert_to_standard_format(file_path) 

137 

138 def _extract_functions(self, contract_code: str) -> List[Dict[str, Any]]: 

139 """Extract function definitions from contract""" 

140 functions = [] 

141 lines = contract_code.split('\n') 

142 

143 i = 0 

144 while i < len(lines): 

145 line = lines[i].strip() 

146 

147 # Match function definition 

148 func_match = re.match( 

149 r'function\s+(\w+)\s*\([^)]*\)\s*(public|external|internal|private)?', 

150 line 

151 ) 

152 

153 if func_match: 

154 func_name = func_match.group(1) 

155 visibility = func_match.group(2) or 'internal' 

156 

157 # Extract function body 

158 start_line = i 

159 brace_count = 0 

160 body_lines = [] 

161 

162 # Find opening brace 

163 while i < len(lines) and '{' not in lines[i]: 

164 i += 1 

165 

166 if i < len(lines): 

167 brace_count = lines[i].count('{') - lines[i].count('}') 

168 body_lines.append(lines[i]) 

169 i += 1 

170 

171 # Extract until closing brace 

172 while i < len(lines) and brace_count > 0: 

173 line = lines[i] 

174 brace_count += line.count('{') - line.count('}') 

175 body_lines.append(line) 

176 i += 1 

177 

178 functions.append({ 

179 'name': func_name, 

180 'visibility': visibility, 

181 'start_line': start_line + 1, 

182 'body': '\n'.join(body_lines), 

183 'body_lines': body_lines 

184 }) 

185 

186 i += 1 

187 

188 return functions 

189 

190 def _execute_function(self, func: Dict[str, Any], file_path: str): 

191 """ 

192 Symbolically execute a function 

193 

194 Explores all execution paths and detects vulnerabilities 

195 """ 

196 func_name = func['name'] 

197 start_line = func['start_line'] 

198 body_lines = func['body_lines'] 

199 

200 # Initialize symbolic state 

201 initial_state = SymbolicState() 

202 

203 # Create symbolic parameters (tainted input) 

204 params = self._extract_parameters(func['body']) 

205 for param_name, param_type in params.items(): 

206 sym_var = self._create_symbolic_variable(param_name, param_type, is_tainted=True) 

207 initial_state.variables[param_name] = sym_var 

208 

209 # Execute symbolically 

210 self._explore_paths(body_lines, initial_state, func_name, start_line, file_path) 

211 

212 def _extract_parameters(self, func_def: str) -> Dict[str, SymbolicType]: 

213 """Extract function parameters and their types""" 

214 params = {} 

215 

216 # Match parameter list 

217 param_match = re.search(r'\(([^)]*)\)', func_def) 

218 if not param_match: 

219 return params 

220 

221 param_list = param_match.group(1) 

222 if not param_list.strip(): 

223 return params 

224 

225 # Parse each parameter 

226 for param in param_list.split(','): 

227 param = param.strip() 

228 if not param: 

229 continue 

230 

231 parts = param.split() 

232 if len(parts) >= 2: 

233 param_type_str = parts[0] 

234 param_name = parts[1] 

235 

236 # Map to symbolic type 

237 param_type = self._map_to_symbolic_type(param_type_str) 

238 params[param_name] = param_type 

239 

240 return params 

241 

242 def _map_to_symbolic_type(self, type_str: str) -> SymbolicType: 

243 """Map Solidity type string to SymbolicType""" 

244 if 'uint' in type_str: 

245 return SymbolicType.UINT256 

246 elif type_str.startswith('int'): 

247 return SymbolicType.INT256 

248 elif type_str == 'address': 

249 return SymbolicType.ADDRESS 

250 elif type_str == 'bool': 

251 return SymbolicType.BOOL 

252 elif 'bytes' in type_str: 

253 return SymbolicType.BYTES32 

254 else: 

255 return SymbolicType.UNKNOWN 

256 

257 def _create_symbolic_variable( 

258 self, 

259 name: str, 

260 sym_type: SymbolicType, 

261 is_tainted: bool = False 

262 ) -> SymbolicVariable: 

263 """Create a symbolic variable with Z3 representation""" 

264 

265 if sym_type == SymbolicType.UINT256: 

266 z3_var = z3.BitVec(name, 256) 

267 elif sym_type == SymbolicType.INT256: 

268 z3_var = z3.BitVec(name, 256) 

269 elif sym_type == SymbolicType.BOOL: 

270 z3_var = z3.Bool(name) 

271 elif sym_type == SymbolicType.ADDRESS: 

272 z3_var = z3.BitVec(name, 160) # Addresses are 160 bits 

273 else: 

274 z3_var = z3.BitVec(name, 256) # Default to 256-bit 

275 

276 return SymbolicVariable( 

277 name=name, 

278 sym_type=sym_type, 

279 z3_var=z3_var, 

280 is_tainted=is_tainted 

281 ) 

282 

283 def _explore_paths( 

284 self, 

285 body_lines: List[str], 

286 state: SymbolicState, 

287 func_name: str, 

288 start_line: int, 

289 file_path: str 

290 ): 

291 """ 

292 Explore execution paths in function body 

293 

294 Day 2 Enhancement: Path condition extraction and branch analysis 

295 - Extract conditions from if/require/assert statements 

296 - Track path constraints for each branch 

297 - Detect unreachable code using constraint solving 

298 """ 

299 

300 i = 0 

301 while i < len(body_lines): 

302 line = body_lines[i] 

303 line_number = start_line + i 

304 line_stripped = line.strip() 

305 

306 if not line_stripped or line_stripped.startswith('//'): 

307 i += 1 

308 continue 

309 

310 # Track execution path 

311 state.execution_path.append(line_number) 

312 

313 # DAY 2: Extract and analyze conditional branches 

314 if self._is_conditional(line_stripped): 

315 self._analyze_conditional_branch( 

316 body_lines, i, state, func_name, start_line, file_path 

317 ) 

318 

319 # DAY 2: Detect require/assert statements 

320 if 'require(' in line_stripped or 'assert(' in line_stripped: 

321 self._analyze_requirement(line_stripped, line_number, state, func_name) 

322 

323 # Day 1: Arithmetic operations 

324 self._analyze_arithmetic(line_stripped, line_number, state, func_name, file_path) 

325 

326 # Day 1: Divisions 

327 self._analyze_division(line_stripped, line_number, state, func_name, file_path) 

328 

329 # Day 1: Tainted data flow 

330 self._analyze_taint_flow(line_stripped, line_number, state, func_name, file_path) 

331 

332 # DAY 2: Check for unreachable code 

333 if len(state.constraints) > 0: 

334 self._check_path_feasibility(state, line_number, func_name, file_path) 

335 

336 i += 1 

337 

338 def _is_conditional(self, line: str) -> bool: 

339 """Check if line contains a conditional statement""" 

340 return ( 

341 line.strip().startswith('if ') or 

342 line.strip().startswith('if(') or 

343 'else if' in line or 

344 'else {' in line 

345 ) 

346 

347 def _analyze_conditional_branch( 

348 self, 

349 body_lines: List[str], 

350 line_index: int, 

351 state: SymbolicState, 

352 func_name: str, 

353 start_line: int, 

354 file_path: str 

355 ): 

356 """ 

357 Analyze conditional branches (if/else) 

358 

359 DAY 2: Path Condition Extraction 

360 - Extract condition from if statement 

361 - Create Z3 constraint for condition 

362 - Explore both true and false branches 

363 - Detect unreachable branches 

364 """ 

365 line = body_lines[line_index] 

366 line_number = start_line + line_index 

367 

368 # Extract condition from if statement 

369 if_match = re.search(r'if\s*\(([^)]+)\)', line) 

370 if not if_match: 

371 return 

372 

373 condition_str = if_match.group(1).strip() 

374 

375 # Parse condition into Z3 constraint 

376 z3_constraint = self._parse_condition_to_z3(condition_str, state) 

377 

378 if z3_constraint is None: 

379 # Can't parse condition, skip advanced analysis 

380 return 

381 

382 # Create path constraint for true branch 

383 true_constraint = PathConstraint( 

384 condition=condition_str, 

385 z3_constraint=z3_constraint, 

386 line_number=line_number, 

387 is_true_branch=True 

388 ) 

389 

390 # Create path constraint for false branch 

391 false_constraint = PathConstraint( 

392 condition=f"!({condition_str})", 

393 z3_constraint=z3.Not(z3_constraint), 

394 line_number=line_number, 

395 is_true_branch=False 

396 ) 

397 

398 # Check if true branch is feasible 

399 true_state = state.copy() 

400 true_state.constraints.append(true_constraint) 

401 

402 if self._is_path_feasible(true_state): 

403 # True branch is reachable 

404 pass 

405 else: 

406 # True branch is unreachable! 

407 self.vulnerabilities.append(SymbolicVulnerability( 

408 vulnerability_type="unreachable_code", 

409 severity="low", 

410 title=f"Unreachable Code in {func_name}", 

411 description=( 

412 f"The condition `{condition_str}` at line {line_number} " 

413 f"can never be true given the current path constraints. " 

414 f"The code inside this if-block is unreachable." 

415 ), 

416 line_number=line_number, 

417 function_name=func_name, 

418 proof=f"Z3 proved condition is always false: {condition_str}", 

419 confidence=95 

420 )) 

421 

422 # Check if false branch is feasible (for else clauses) 

423 false_state = state.copy() 

424 false_state.constraints.append(false_constraint) 

425 

426 if not self._is_path_feasible(false_state): 

427 # Condition is always true (else is unreachable) 

428 self.vulnerabilities.append(SymbolicVulnerability( 

429 vulnerability_type="unreachable_code", 

430 severity="info", 

431 title=f"Condition Always True in {func_name}", 

432 description=( 

433 f"The condition `{condition_str}` at line {line_number} " 

434 f"is always true. Consider simplifying the code." 

435 ), 

436 line_number=line_number, 

437 function_name=func_name, 

438 proof=f"Z3 proved condition is always true: {condition_str}", 

439 confidence=90 

440 )) 

441 

442 def _parse_condition_to_z3(self, condition: str, state: SymbolicState) -> Optional[z3.BoolRef]: 

443 """ 

444 Parse a Solidity condition into a Z3 constraint 

445 

446 DAY 2: Enhanced condition parsing 

447 Supports: 

448 - Comparisons: ==, !=, <, >, <=, >= 

449 - Boolean operators: &&, ||, ! 

450 - Basic arithmetic 

451 """ 

452 

453 # Simple comparison operators 

454 for op, z3_op in [ 

455 ('==', lambda a, b: a == b), 

456 ('!=', lambda a, b: a != b), 

457 ('>=', lambda a, b: z3.UGE(a, b)), # Unsigned greater or equal 

458 ('<=', lambda a, b: z3.ULE(a, b)), 

459 ('>', lambda a, b: z3.UGT(a, b)), 

460 ('<', lambda a, b: z3.ULT(a, b)), 

461 ]: 

462 if op in condition: 

463 parts = condition.split(op) 

464 if len(parts) == 2: 

465 left = parts[0].strip() 

466 right = parts[1].strip() 

467 

468 # Try to create Z3 expressions 

469 left_z3 = self._parse_expression_to_z3(left, state) 

470 right_z3 = self._parse_expression_to_z3(right, state) 

471 

472 if left_z3 is not None and right_z3 is not None: 

473 return z3_op(left_z3, right_z3) 

474 

475 # Boolean conditions 

476 if condition in state.variables: 

477 var = state.variables[condition] 

478 if var.sym_type == SymbolicType.BOOL: 

479 return var.z3_var 

480 

481 # Negation 

482 if condition.startswith('!'): 

483 inner = condition[1:].strip() 

484 inner_z3 = self._parse_condition_to_z3(inner, state) 

485 if inner_z3 is not None: 

486 return z3.Not(inner_z3) 

487 

488 # Can't parse 

489 return None 

490 

491 def _parse_expression_to_z3(self, expr: str, state: SymbolicState) -> Optional[z3.ExprRef]: 

492 """Parse a Solidity expression into Z3""" 

493 

494 # Integer literal 

495 if expr.isdigit(): 

496 return z3.BitVecVal(int(expr), 256) 

497 

498 # Variable reference 

499 if expr in state.variables: 

500 return state.variables[expr].z3_var 

501 

502 # msg.sender, msg.value, etc. 

503 if expr.startswith('msg.'): 

504 # Create symbolic variable for msg properties 

505 var_name = expr.replace('.', '_') 

506 if var_name not in state.variables: 

507 z3_var = z3.BitVec(var_name, 256) 

508 state.variables[var_name] = SymbolicVariable( 

509 name=var_name, 

510 sym_type=SymbolicType.UINT256, 

511 z3_var=z3_var, 

512 is_tainted=True 

513 ) 

514 return state.variables[var_name].z3_var 

515 

516 # Can't parse 

517 return None 

518 

519 def _is_path_feasible(self, state: SymbolicState) -> bool: 

520 """ 

521 Check if execution path is feasible using Z3 

522 

523 DAY 2: Constraint solving for path feasibility 

524 Returns True if there exists a satisfying assignment 

525 """ 

526 if len(state.constraints) == 0: 

527 return True 

528 

529 solver = z3.Solver() 

530 

531 # Add all path constraints 

532 for constraint in state.constraints: 

533 solver.add(constraint.z3_constraint) 

534 

535 # Check satisfiability 

536 result = solver.check() 

537 return result == z3.sat 

538 

539 def _check_path_feasibility( 

540 self, 

541 state: SymbolicState, 

542 line_number: int, 

543 func_name: str, 

544 file_path: str 

545 ): 

546 """ 

547 Check if current path is feasible 

548 

549 If not, report unreachable code 

550 """ 

551 if not self._is_path_feasible(state): 

552 # This path is unreachable! 

553 constraint_desc = ", ".join([c.condition for c in state.constraints[-3:]]) 

554 

555 self.vulnerabilities.append(SymbolicVulnerability( 

556 vulnerability_type="unreachable_code", 

557 severity="info", 

558 title=f"Unreachable Code Detected in {func_name}", 

559 description=( 

560 f"Code at line {line_number} is unreachable due to " 

561 f"contradicting path constraints: {constraint_desc}" 

562 ), 

563 line_number=line_number, 

564 function_name=func_name, 

565 proof=f"Path constraints are unsatisfiable", 

566 confidence=90 

567 )) 

568 

569 def _analyze_requirement( 

570 self, 

571 line: str, 

572 line_number: int, 

573 state: SymbolicState, 

574 func_name: str 

575 ): 

576 """ 

577 Analyze require/assert statements 

578 

579 DAY 2: Extract constraints from require/assert 

580 These become path constraints for subsequent code 

581 """ 

582 

583 # Extract condition from require/assert 

584 req_match = re.search(r'(require|assert)\s*\(([^)]+)\)', line) 

585 if not req_match: 

586 return 

587 

588 condition_str = req_match.group(2).strip() 

589 

590 # Remove error message if present 

591 if ',' in condition_str: 

592 condition_str = condition_str.split(',')[0].strip() 

593 

594 # Parse to Z3 

595 z3_constraint = self._parse_condition_to_z3(condition_str, state) 

596 

597 if z3_constraint is not None: 

598 # Add as path constraint 

599 constraint = PathConstraint( 

600 condition=condition_str, 

601 z3_constraint=z3_constraint, 

602 line_number=line_number, 

603 is_true_branch=True 

604 ) 

605 state.constraints.append(constraint) 

606 

607 # Check if this requirement is always true 

608 solver = z3.Solver() 

609 solver.add(z3.Not(z3_constraint)) # Can it be false? 

610 

611 if solver.check() == z3.unsat: 

612 # Requirement is always satisfied (redundant) 

613 self.vulnerabilities.append(SymbolicVulnerability( 

614 vulnerability_type="redundant_check", 

615 severity="info", 

616 title=f"Redundant Check in {func_name}", 

617 description=( 

618 f"The requirement `{condition_str}` at line {line_number} " 

619 f"is always true and can be removed." 

620 ), 

621 line_number=line_number, 

622 function_name=func_name, 

623 proof=f"Z3 proved condition is always satisfied", 

624 confidence=85 

625 )) 

626 

627 def _analyze_arithmetic( 

628 self, 

629 line: str, 

630 line_number: int, 

631 state: SymbolicState, 

632 func_name: str, 

633 file_path: str 

634 ): 

635 """ 

636 Analyze arithmetic operations for overflow/underflow 

637 

638 Detects patterns like: 

639 - balance += amount 

640 - total = a + b 

641 - result = value - 1 

642 """ 

643 

644 # Pattern: variable += expr 

645 add_assign_match = re.search(r'(\w+)\s*\+=\s*(.+?)[;\s]', line) 

646 if add_assign_match: 

647 var_name = add_assign_match.group(1) 

648 expr = add_assign_match.group(2).strip() 

649 

650 # Check if unchecked block 

651 is_unchecked = 'unchecked' in line or any('unchecked' in bl for bl in state.execution_path[-5:] if isinstance(bl, str)) 

652 

653 if not is_unchecked: 

654 # Check for potential overflow 

655 self._check_overflow_addition(var_name, expr, line_number, state, func_name, file_path) 

656 

657 # Pattern: variable = a + b 

658 add_match = re.search(r'(\w+)\s*=\s*(.+?)\s*\+\s*(.+?)[;\s]', line) 

659 if add_match: 

660 result_var = add_match.group(1) 

661 left_operand = add_match.group(2).strip() 

662 right_operand = add_match.group(3).strip() 

663 

664 is_unchecked = 'unchecked' in line 

665 if not is_unchecked: 

666 self._check_overflow_addition_expr( 

667 result_var, left_operand, right_operand, 

668 line_number, state, func_name, file_path 

669 ) 

670 

671 # Pattern: variable -= expr (underflow) 

672 sub_assign_match = re.search(r'(\w+)\s*-=\s*(.+?)[;\s]', line) 

673 if sub_assign_match: 

674 var_name = sub_assign_match.group(1) 

675 expr = sub_assign_match.group(2).strip() 

676 

677 is_unchecked = 'unchecked' in line 

678 if not is_unchecked: 

679 self._check_underflow_subtraction(var_name, expr, line_number, state, func_name, file_path) 

680 

681 def _check_overflow_addition( 

682 self, 

683 var_name: str, 

684 expr: str, 

685 line_number: int, 

686 state: SymbolicState, 

687 func_name: str, 

688 file_path: str 

689 ): 

690 """ 

691 Check if addition can overflow using Z3 

692 

693 Creates constraint: var + expr > MAX_UINT256 

694 If satisfiable, overflow is possible 

695 """ 

696 

697 # Create Z3 variables 

698 var_z3 = z3.BitVec(f"{var_name}_before", 256) 

699 expr_z3 = z3.BitVec(f"{expr}_value", 256) 

700 result_z3 = var_z3 + expr_z3 

701 

702 # Check if overflow possible: result < var (unsigned overflow wraps) 

703 overflow_constraint = z3.ULT(result_z3, var_z3) 

704 

705 # Try to find a model where overflow occurs 

706 solver = z3.Solver() 

707 solver.add(overflow_constraint) 

708 

709 if solver.check() == z3.sat: 

710 model = solver.model() 

711 

712 # Extract example values 

713 var_value = model.eval(var_z3, model_completion=True) 

714 expr_value = model.eval(expr_z3, model_completion=True) 

715 

716 proof = f"Overflow possible: {var_name} = {var_value}, {expr} = {expr_value}" 

717 

718 self.vulnerabilities.append(SymbolicVulnerability( 

719 vulnerability_type="integer_overflow", 

720 severity="high", 

721 title=f"Integer Overflow in {func_name}", 

722 description=( 

723 f"Arithmetic operation `{var_name} += {expr}` at line {line_number} " 

724 f"can overflow. This can lead to incorrect balances or unauthorized access." 

725 ), 

726 line_number=line_number, 

727 function_name=func_name, 

728 proof=proof, 

729 confidence=90 

730 )) 

731 

732 def _check_overflow_addition_expr( 

733 self, 

734 result_var: str, 

735 left: str, 

736 right: str, 

737 line_number: int, 

738 state: SymbolicState, 

739 func_name: str, 

740 file_path: str 

741 ): 

742 """Check if a + b can overflow""" 

743 

744 left_z3 = z3.BitVec(f"{left}_value", 256) 

745 right_z3 = z3.BitVec(f"{right}_value", 256) 

746 result_z3 = left_z3 + right_z3 

747 

748 # Overflow check: result < left OR result < right 

749 overflow_constraint = z3.Or( 

750 z3.ULT(result_z3, left_z3), 

751 z3.ULT(result_z3, right_z3) 

752 ) 

753 

754 solver = z3.Solver() 

755 solver.add(overflow_constraint) 

756 

757 if solver.check() == z3.sat: 

758 model = solver.model() 

759 left_value = model.eval(left_z3, model_completion=True) 

760 right_value = model.eval(right_z3, model_completion=True) 

761 

762 proof = f"Overflow: {left} = {left_value}, {right} = {right_value}" 

763 

764 self.vulnerabilities.append(SymbolicVulnerability( 

765 vulnerability_type="integer_overflow", 

766 severity="medium", 

767 title=f"Potential Integer Overflow in {func_name}", 

768 description=( 

769 f"Addition `{result_var} = {left} + {right}` at line {line_number} " 

770 f"can overflow without `unchecked` block or overflow protection." 

771 ), 

772 line_number=line_number, 

773 function_name=func_name, 

774 proof=proof, 

775 confidence=85 

776 )) 

777 

778 def _check_underflow_subtraction( 

779 self, 

780 var_name: str, 

781 expr: str, 

782 line_number: int, 

783 state: SymbolicState, 

784 func_name: str, 

785 file_path: str 

786 ): 

787 """Check if subtraction can underflow""" 

788 

789 var_z3 = z3.BitVec(f"{var_name}_before", 256) 

790 expr_z3 = z3.BitVec(f"{expr}_value", 256) 

791 

792 # Underflow: var < expr (for unsigned) 

793 underflow_constraint = z3.ULT(var_z3, expr_z3) 

794 

795 solver = z3.Solver() 

796 solver.add(underflow_constraint) 

797 

798 if solver.check() == z3.sat: 

799 model = solver.model() 

800 var_value = model.eval(var_z3, model_completion=True) 

801 expr_value = model.eval(expr_z3, model_completion=True) 

802 

803 proof = f"Underflow: {var_name} = {var_value}, {expr} = {expr_value}" 

804 

805 self.vulnerabilities.append(SymbolicVulnerability( 

806 vulnerability_type="integer_underflow", 

807 severity="high", 

808 title=f"Integer Underflow in {func_name}", 

809 description=( 

810 f"Subtraction `{var_name} -= {expr}` at line {line_number} " 

811 f"can underflow, wrapping to MAX_UINT256." 

812 ), 

813 line_number=line_number, 

814 function_name=func_name, 

815 proof=proof, 

816 confidence=90 

817 )) 

818 

819 def _analyze_division( 

820 self, 

821 line: str, 

822 line_number: int, 

823 state: SymbolicState, 

824 func_name: str, 

825 file_path: str 

826 ): 

827 """Detect potential division by zero""" 

828 

829 # Pattern: variable = a / b 

830 div_match = re.search(r'(\w+)\s*=\s*(.+?)\s*/\s*(.+?)[;\s]', line) 

831 if not div_match: 

832 return 

833 

834 result_var = div_match.group(1) 

835 numerator = div_match.group(2).strip() 

836 denominator = div_match.group(3).strip() 

837 

838 # Check if denominator can be zero 

839 if denominator.isdigit() and int(denominator) != 0: 

840 # Constant non-zero, safe 

841 return 

842 

843 # Check if there's a require statement protecting against zero 

844 # This is a simplified check 

845 if f"require({denominator} > 0" in line or f"require({denominator} != 0" in line: 

846 return 

847 

848 # Potential division by zero 

849 self.vulnerabilities.append(SymbolicVulnerability( 

850 vulnerability_type="division_by_zero", 

851 severity="medium", 

852 title=f"Potential Division by Zero in {func_name}", 

853 description=( 

854 f"Division operation `{result_var} = {numerator} / {denominator}` at line {line_number} " 

855 f"does not check if denominator is zero. This will cause transaction revert." 

856 ), 

857 line_number=line_number, 

858 function_name=func_name, 

859 proof=f"Denominator '{denominator}' not validated before division", 

860 confidence=75 

861 )) 

862 

863 def _analyze_taint_flow( 

864 self, 

865 line: str, 

866 line_number: int, 

867 state: SymbolicState, 

868 func_name: str,