diff --git a/examples/reachability/README.md b/examples/reachability/README.md new file mode 100644 index 0000000000..dbebe444c4 --- /dev/null +++ b/examples/reachability/README.md @@ -0,0 +1,258 @@ +# USVM Reachability Analysis - Target File Formats + +This document describes the supported target file formats for the USVM TypeScript Reachability Analysis tool. + +## Supported Formats + +The tool automatically detects and supports three different JSON formats for specifying targets: + +### 1. Linear Trace Format - `{ "targets": [...] }` + +A single linear trace containing a sequence of target points. In a linear trace: +- **Only the first target** should be marked as `"initial"` (entry point) +- **Only the last target** should be marked as `"final"` (end point) +- **All intermediate targets** don't need a type field (defaults to `"intermediate"`) + +**Example: `targets.json`** +```json +{ + "targets": [ + { + "type": "initial", + "location": { + "fileName": "ProcessManager.ts", + "className": "Process", + "methodName": "start", + "stmtType": "IfStmt", + "block": 0, + "index": 0 + } + }, + { + "location": { + "fileName": "ProcessManager.ts", + "className": "Process", + "methodName": "start", + "stmtType": "AssignStmt", + "block": 1, + "index": 3 + } + }, + { + "location": { + "fileName": "ProcessManager.ts", + "className": "Process", + "methodName": "terminate", + "stmtType": "CallStmt", + "block": 0, + "index": 0 + } + }, + { + "type": "final", + "location": { + "fileName": "ProcessManager.ts", + "className": "Process", + "methodName": "terminate", + "stmtType": "ReturnStmt", + "block": 2, + "index": 7 + } + } + ] +} +``` + +### 2. Tree Trace Format - `{ "target": {...}, "children": [...] }` + +A single tree-like trace with hierarchical target structure. + +**Example: `targets-tree.json`** +```json +{ + "target": { + "type": "initial", + "location": { + "fileName": "ProcessManager.ts", + "className": "ProcessManager", + "methodName": "createProcess", + "stmtType": "IfStmt", + "block": 0, + "index": 0 + } + }, + "children": [ + { + "target": { + "location": { + "fileName": "ProcessManager.ts", + "className": "ProcessManager", + "methodName": "createProcess", + "stmtType": "AssignStmt", + "block": 1, + "index": 3 + } + }, + "children": [ + { + "target": { + "type": "final", + "location": { + "fileName": "ProcessManager.ts", + "className": "ProcessManager", + "methodName": "createProcess", + "stmtType": "ReturnStmt", + "block": 2, + "index": 7 + } + } + } + ] + } + ] +} +``` + +### 3. Trace List Format - `[ {...} ]` + +An array of traces that can contain both linear and tree traces. + +**Example: `targets-mixed.json`** +```json +[ + { + "targets": [ + { + "type": "initial", + "location": { + "fileName": "UserService.ts", + "className": "UserService", + "methodName": "authenticate", + "stmtType": "IfStmt", + "block": 0, + "index": 0 + } + }, + { + "location": { + "fileName": "UserService.ts", + "className": "UserService", + "methodName": "validate", + "stmtType": "CallStmt", + "block": 0, + "index": 0 + } + }, + { + "type": "final", + "location": { + "fileName": "UserService.ts", + "className": "UserService", + "methodName": "validate", + "stmtType": "ReturnStmt", + "block": 3, + "index": 8 + } + } + ] + }, + { + "target": { + "type": "initial", + "location": { + "fileName": "DatabaseManager.ts", + "className": "DatabaseManager", + "methodName": "connect", + "stmtType": "IfStmt", + "block": 0, + "index": 0 + } + }, + "children": [ + { + "target": { + "type": "final", + "location": { + "fileName": "DatabaseManager.ts", + "className": "DatabaseManager", + "methodName": "establishConnection", + "stmtType": "ReturnStmt", + "block": 0, + "index": 2 + } + } + } + ] + } +] +``` + +## Target Types + +Each target can have one of three types: + +- **`initial`**: Entry point of a trace (only first target in linear traces) +- **`intermediate`**: Intermediate point in execution (default - can be omitted) +- **`final`**: End point of a trace (only last target in linear traces) + +## Location Structure + +Each target must specify a location with the following fields: + +- **`fileName`**: The TypeScript source file name +- **`className`**: The class containing the method +- **`methodName`**: The method name +- **`stmtType`**: IR statement type (e.g., "IfStmt", "AssignStmt", "CallStmt", "ReturnStmt") +- **`block`**: Control flow block number +- **`index`**: Statement index within the block + +## Common Statement Types + +The `stmtType` field should contain the IR name of the statement at the specified coordinates: + +- **`IfStmt`**: Conditional if statement +- **`AssignStmt`**: Assignment statement +- **`CallStmt`**: Method/function call statement +- **`ReturnStmt`**: Return statement +- **`WhileStmt`**: While loop statement +- **`ForStmt`**: For loop statement +- **`ThrowStmt`**: Throw/exception statement + +## Linear Trace Rules + +For linear traces (both standalone and within trace lists): + +1. **Single Initial Point**: Only the very first target should have `"type": "initial"` +2. **Single Final Point**: Only the very last target should have `"type": "final"` +3. **Omit Intermediate Types**: All targets between first and last can omit the `"type"` field entirely (defaults to `"intermediate"`) +4. **Sequential Execution**: Targets represent a single execution path through the code + +## Automatic Format Detection + +The tool automatically detects which format is being used based on the JSON structure: + +- If the JSON is an array at the top level -> Trace List Format +- If the JSON object contains a `"targets"` field -> Linear Trace Format +- If the JSON object contains a `"target"` field -> Tree Trace Format + +No manual format specification is required! + +## Usage Examples + +```bash +# Using linear trace format +./reachability -p ./my-project -t targets.json + +# Using hierarchical (tree-like) format +./reachability -p ./my-project -t targets-tree.json + +# Using mixed array format +./reachability -p ./my-project -t targets-mixed.json + +# Auto-generate targets (no file needed) +./reachability -p ./my-project +``` + +## Legacy Format Support + +The tool maintains backward compatibility with legacy target file formats using regex-based parsing as a fallback option. diff --git a/examples/reachability/reachability-cli.sh b/examples/reachability/reachability-cli.sh new file mode 100755 index 0000000000..058796660c --- /dev/null +++ b/examples/reachability/reachability-cli.sh @@ -0,0 +1,238 @@ +#!/bin/bash + +# TypeScript Reachability Analysis CLI Wrapper +# This script makes it easy to run reachability analysis on TypeScript projects + +set -e + +SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +USVM_ROOT="$(cd "$SCRIPT_DIR/../.." && pwd)" + +# Default values +PROJECT_PATH="" +TARGETS_FILE="" +OUTPUT_DIR="./reachability-results" +MODE="PUBLIC_METHODS" +SOLVER="YICES" +TIMEOUT=300 +STEPS=3500 +VERBOSE=false +INCLUDE_STATEMENTS=false +METHOD_FILTER="" +EXECUTION_MODE="shadow" # Options: shadow, dist + +# Colors for output +RED='\033[0;31m' +GREEN='\033[0;32m' +BLUE='\033[0;34m' +YELLOW='\033[1;33m' +NC='\033[0m' # No Color + +usage() { + echo -e "${BLUE}šŸŽÆ TypeScript Reachability Analysis Tool${NC}" + echo "" + echo "Usage: $0 -p PROJECT_PATH [OPTIONS]" + echo "" + echo "Required:" + echo " -p, --project PATH TypeScript project directory" + echo "" + echo "Optional:" + echo " -t, --targets FILE JSON file with target definitions" + echo " -o, --output DIR Output directory (default: ./reachability-results)" + echo " -m, --mode MODE Analysis mode: ALL_METHODS, PUBLIC_METHODS, ENTRY_POINTS" + echo " --method PATTERN Filter methods by name pattern" + echo " --solver SOLVER SMT solver: YICES, Z3, CVC5 (default: YICES)" + echo " --timeout SECONDS Analysis timeout (default: 300)" + echo " --steps LIMIT Max steps limit (default: 3500)" + echo " --exec-mode MODE Execution mode: shadow, dist (default: shadow)" + echo " -v, --verbose Enable verbose output" + echo " --include-statements Include statement details in output" + echo " -h, --help Show this help message" + echo "" + echo "Execution modes:" + echo " shadow: Uses shadow JAR: java -cp usvm-ts-all.jar ..." + echo " dist: Uses Gradle distribution binary: /path/to/bin/usvm-ts ..." + echo "" + echo "Examples:" + echo " # Analyze all public methods in a TypeScript project (using shadow JAR)" + echo " $0 -p ./my-typescript-project" + echo "" + echo " # Use Gradle distribution binary instead" + echo " $0 -p ./my-typescript-project --exec-mode dist" + echo "" + echo " # Use custom targets and verbose output with distribution binary" + echo " $0 -p ./my-project -t ./targets.json -v --exec-mode dist" + echo "" + echo " # Analyze specific methods with detailed output" + echo " $0 -p ./project --method ProcessManager --include-statements" +} + +# Parse command line arguments +while [[ $# -gt 0 ]]; do + case $1 in + -p|--project) + PROJECT_PATH="$2" + shift 2 + ;; + -t|--targets) + TARGETS_FILE="$2" + shift 2 + ;; + -o|--output) + OUTPUT_DIR="$2" + shift 2 + ;; + -m|--mode) + MODE="$2" + shift 2 + ;; + --method) + METHOD_FILTER="$2" + shift 2 + ;; + --solver) + SOLVER="$2" + shift 2 + ;; + --timeout) + TIMEOUT="$2" + shift 2 + ;; + --steps) + STEPS="$2" + shift 2 + ;; + --exec-mode) + case "$2" in + shadow|dist) + EXECUTION_MODE="$2" + ;; + *) + echo -e "${RED}āŒ Error: Invalid execution mode '$2'. Valid options: shadow, dist${NC}" + exit 1 + ;; + esac + shift 2 + ;; + -v|--verbose) + VERBOSE=true + shift + ;; + --include-statements) + INCLUDE_STATEMENTS=true + shift + ;; + -h|--help) + usage + exit 0 + ;; + *) + echo -e "${RED}āŒ Unknown option: $1${NC}" + usage + exit 1 + ;; + esac +done + +# Validate required arguments +if [[ -z "$PROJECT_PATH" ]]; then + echo -e "${RED}āŒ Error: Project path is required${NC}" + usage + exit 1 +fi + +if [[ ! -d "$PROJECT_PATH" ]]; then + echo -e "${RED}āŒ Error: Project path does not exist: $PROJECT_PATH${NC}" + exit 1 +fi + +# Display configuration +echo -e "${BLUE}šŸš€ Starting TypeScript Reachability Analysis${NC}" +echo "šŸ“ Project: $PROJECT_PATH" +echo "šŸ“„ Output: $OUTPUT_DIR" +echo "šŸ” Mode: $MODE" +echo "āš™ļø Solver: $SOLVER" +echo "šŸ“¦ Execution mode: $EXECUTION_MODE" + +# Build command arguments +CMD_ARGS=() +CMD_ARGS+=("--project" "$PROJECT_PATH") +CMD_ARGS+=("--output" "$OUTPUT_DIR") +CMD_ARGS+=("--mode" "$MODE") +CMD_ARGS+=("--solver" "$SOLVER") +CMD_ARGS+=("--timeout" "$TIMEOUT") +CMD_ARGS+=("--steps" "$STEPS") + +if [[ -n "$TARGETS_FILE" ]]; then + if [[ ! -f "$TARGETS_FILE" ]]; then + echo -e "${RED}āŒ Error: Targets file does not exist: $TARGETS_FILE${NC}" + exit 1 + fi + CMD_ARGS+=("--targets" "$TARGETS_FILE") + echo "šŸ“‹ Targets: $TARGETS_FILE" +fi + +if [[ -n "$METHOD_FILTER" ]]; then + CMD_ARGS+=("--method" "$METHOD_FILTER") + echo "šŸŽÆ Method filter: $METHOD_FILTER" +fi + +if [[ "$VERBOSE" == true ]]; then + CMD_ARGS+=("--verbose") + echo "šŸ“ Verbose mode enabled" +fi + +if [[ "$INCLUDE_STATEMENTS" == true ]]; then + CMD_ARGS+=("--include-statements") + echo "šŸ“ Including statement details" +fi + +echo "" +echo -e "${YELLOW}āš” Running analysis...${NC}" + +# Execute based on chosen mode +if [[ "$EXECUTION_MODE" == "dist" ]]; then + echo "šŸ“¦ Using Gradle distribution binary" + + # Path to the Gradle distribution binary + DIST_BIN_PATH="$USVM_ROOT/usvm-ts/build/install/usvm-ts/bin/usvm-ts-reachability" + + # Check if distribution exists, if not try to build it + if [[ ! -f "$DIST_BIN_PATH" ]]; then + echo -e "${YELLOW}āš ļø Distribution binary not found, attempting to build...${NC}" + cd "$USVM_ROOT" + if ! ./gradlew :usvm-ts:installDist; then + echo -e "${RED}āŒ Error: Failed to build distribution${NC}" + exit 1 + fi + fi + + # Execute using distribution binary + "$DIST_BIN_PATH" "${CMD_ARGS[@]}" + +else + echo "šŸ“¦ Using Shadow JAR" + + # Path to the compiled shadow JAR + JAR_PATH="$USVM_ROOT/usvm-ts/build/libs/usvm-ts-all.jar" + + # Check if JAR exists, if not try to build it + if [[ ! -f "$JAR_PATH" ]]; then + echo -e "${YELLOW}āš ļø JAR not found, attempting to build...${NC}" + cd "$USVM_ROOT" + if ! ./gradlew :usvm-ts:shadowJar; then + echo -e "${RED}āŒ Error: Failed to build JAR${NC}" + exit 1 + fi + fi + + # Execute using shadow JAR + java -Dfile.encoding=UTF-8 \ + -Dsun.stdout.encoding=UTF-8 \ + -cp "$JAR_PATH" \ + org.usvm.api.reachability.cli.ReachabilityKt \ + "${CMD_ARGS[@]}" +fi + +echo "" +echo -e "${GREEN}āœ… Analysis complete! Check the results in: $OUTPUT_DIR${NC}" diff --git a/examples/reachability/sample-project/FileSystem.ts b/examples/reachability/sample-project/FileSystem.ts new file mode 100644 index 0000000000..4cd3f8bbc3 --- /dev/null +++ b/examples/reachability/sample-project/FileSystem.ts @@ -0,0 +1,317 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +// File System Simulator - Sample TypeScript project for reachability analysis +// This project simulates basic file system operations without floating-point arithmetic + +export class FileSystemNode { + public name: string; + public isDirectory: boolean; + public parent: FileSystemNode | null; + public children: FileSystemNode[]; + public content: string; + public permissions: number; // Using integer permissions (e.g., 755, 644) + public size: number; + + constructor(name: string, isDirectory: boolean = false, parent: FileSystemNode | null = null) { + this.name = name; + this.isDirectory = isDirectory; + this.parent = parent; + this.children = []; + this.content = ""; + this.permissions = isDirectory ? 755 : 644; + this.size = 0; + } + + public addChild(child: FileSystemNode): boolean { + if (!this.isDirectory) { + throw new Error("Cannot add child to a file"); + } + + // Check if child already exists + for (let i = 0; i < this.children.length; i++) { + if (this.children[i].name === child.name) { + return false; // Child already exists + } + } + + child.parent = this; + this.children.push(child); + return true; + } + + public removeChild(name: string): boolean { + if (!this.isDirectory) { + return false; + } + + for (let i = 0; i < this.children.length; i++) { + if (this.children[i].name === name) { + this.children.splice(i, 1); + return true; + } + } + return false; + } + + public findChild(name: string): FileSystemNode | null { + if (!this.isDirectory) { + return null; + } + + for (let i = 0; i < this.children.length; i++) { + if (this.children[i].name === name) { + return this.children[i]; + } + } + return null; + } + + public getPath(): string { + if (this.parent === null) { + return "/"; + } + + let path = ""; + let current: FileSystemNode | null = this; + + while (current !== null && current.parent !== null) { + path = "/" + current.name + path; + current = current.parent; + } + + return path === "" ? "/" : path; + } + + public calculateSize(): number { + if (!this.isDirectory) { + return this.content.length; + } + + let totalSize = 0; + for (let i = 0; i < this.children.length; i++) { + totalSize += this.children[i].calculateSize(); + } + this.size = totalSize; + return totalSize; + } +} + +export class FileSystem { + private root: FileSystemNode; + private currentDirectory: FileSystemNode; + + constructor() { + this.root = new FileSystemNode("", true); + this.currentDirectory = this.root; + } + + public createFile(path: string, content: string = ""): boolean { + const pathParts = this.parsePath(path); + if (pathParts.length === 0) { + return false; + } + + const fileName = pathParts[pathParts.length - 1]; + const dirPath = pathParts.slice(0, -1); + const parentDir = this.navigateToPath(dirPath); + + if (parentDir === null || !parentDir.isDirectory) { + return false; + } + + const newFile = new FileSystemNode(fileName, false, parentDir); + newFile.content = content; + newFile.size = content.length; + + return parentDir.addChild(newFile); + } + + public createDirectory(path: string): boolean { + const pathParts = this.parsePath(path); + if (pathParts.length === 0) { + return false; + } + + const dirName = pathParts[pathParts.length - 1]; + const parentPath = pathParts.slice(0, -1); + const parentDir = this.navigateToPath(parentPath); + + if (parentDir === null || !parentDir.isDirectory) { + return false; + } + + const newDir = new FileSystemNode(dirName, true, parentDir); + return parentDir.addChild(newDir); + } + + public deleteFile(path: string): boolean { + const pathParts = this.parsePath(path); + if (pathParts.length === 0) { + return false; + } + + const fileName = pathParts[pathParts.length - 1]; + const dirPath = pathParts.slice(0, -1); + const parentDir = this.navigateToPath(dirPath); + + if (parentDir === null) { + return false; + } + + const fileToDelete = parentDir.findChild(fileName); + if (fileToDelete === null || fileToDelete.isDirectory) { + return false; + } + + return parentDir.removeChild(fileName); + } + + public readFile(path: string): string | null { + const node = this.findNode(path); + if (node === null || node.isDirectory) { + return null; + } + return node.content; + } + + public writeFile(path: string, content: string): boolean { + const node = this.findNode(path); + if (node === null || node.isDirectory) { + return false; + } + + node.content = content; + node.size = content.length; + return true; + } + + public listDirectory(path: string = ""): string[] { + const node = path === "" ? this.currentDirectory : this.findNode(path); + if (node === null || !node.isDirectory) { + return []; + } + + const result: string[] = []; + for (let i = 0; i < node.children.length; i++) { + const child = node.children[i]; + const prefix = child.isDirectory ? "d " : "f "; + result.push(prefix + child.name); + } + return result; + } + + public changeDirectory(path: string): boolean { + const node = this.findNode(path); + if (node === null || !node.isDirectory) { + return false; + } + + this.currentDirectory = node; + return true; + } + + public getCurrentPath(): string { + return this.currentDirectory.getPath(); + } + + public copyFile(sourcePath: string, destPath: string): boolean { + const sourceNode = this.findNode(sourcePath); + if (sourceNode === null || sourceNode.isDirectory) { + return false; + } + + return this.createFile(destPath, sourceNode.content); + } + + public moveFile(sourcePath: string, destPath: string): boolean { + const sourceNode = this.findNode(sourcePath); + if (sourceNode === null || sourceNode.isDirectory) { + return false; + } + + const content = sourceNode.content; + if (!this.deleteFile(sourcePath)) { + return false; + } + + if (!this.createFile(destPath, content)) { + // Restore the original file if destination creation fails + this.createFile(sourcePath, content); + return false; + } + + return true; + } + + public findFiles(pattern: string, startPath: string = ""): string[] { + const startNode = startPath === "" ? this.root : this.findNode(startPath); + if (startNode === null) { + return []; + } + + const results: string[] = []; + this.searchRecursive(startNode, pattern, results); + return results; + } + + private searchRecursive(node: FileSystemNode, pattern: string, results: string[]): void { + if (!node.isDirectory && node.name.indexOf(pattern) >= 0) { + results.push(node.getPath()); + } + + if (node.isDirectory) { + for (let i = 0; i < node.children.length; i++) { + this.searchRecursive(node.children[i], pattern, results); + } + } + } + + private parsePath(path: string): string[] { + if (path === "" || path === "/") { + return []; + } + + // Remove leading slash and split + const cleaned = path.startsWith("/") ? path.substring(1) : path; + return cleaned.split("/").filter(part => part.length > 0); + } + + private navigateToPath(pathParts: string[]): FileSystemNode | null { + let current = this.root; + + for (let i = 0; i < pathParts.length; i++) { + const part = pathParts[i]; + if (part === "..") { + if (current.parent !== null) { + current = current.parent; + } + } else if (part !== ".") { + const child = current.findChild(part); + if (child === null || !child.isDirectory) { + return null; + } + current = child; + } + } + + return current; + } + + private findNode(path: string): FileSystemNode | null { + const pathParts = this.parsePath(path); + if (pathParts.length === 0) { + return this.root; + } + + const fileName = pathParts[pathParts.length - 1]; + const dirPath = pathParts.slice(0, -1); + const parentDir = this.navigateToPath(dirPath); + + if (parentDir === null) { + return null; + } + + return parentDir.findChild(fileName); + } +} diff --git a/examples/reachability/sample-project/MemoryManager.ts b/examples/reachability/sample-project/MemoryManager.ts new file mode 100644 index 0000000000..766b258f9f --- /dev/null +++ b/examples/reachability/sample-project/MemoryManager.ts @@ -0,0 +1,291 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +// Memory Manager - Sample TypeScript project for reachability analysis +// This project simulates memory management operations using only SMT-solver friendly constructs: +// - Integer operations (no floating-point, no modulo) +// - Array operations (length, indexing) +// - Object field access and updates +// - Conditional logic and control flow + +export enum MemoryBlockState { + FREE = 0, + ALLOCATED = 1, + RESERVED = 2 +} + +export class MemoryBlock { + public startAddress: number; + public size: number; + public state: MemoryBlockState; + public ownerId: number; // Process ID that owns this block + + constructor(startAddress: number, size: number) { + this.startAddress = startAddress; + this.size = size; + this.state = MemoryBlockState.FREE; + this.ownerId = 0; + } + + public allocate(ownerId: number): boolean { + if (this.state === MemoryBlockState.FREE) { + this.state = MemoryBlockState.ALLOCATED; + this.ownerId = ownerId; + return true; + } + return false; + } + + public free(): boolean { + if (this.state === MemoryBlockState.ALLOCATED) { + this.state = MemoryBlockState.FREE; + this.ownerId = 0; + return true; + } + return false; + } + + public reserve(): boolean { + if (this.state === MemoryBlockState.FREE) { + this.state = MemoryBlockState.RESERVED; + return true; + } + return false; + } + + public getEndAddress(): number { + return this.startAddress + this.size - 1; + } +} + +export class MemoryManager { + private blocks: MemoryBlock[]; + private totalMemory: number; + private allocatedMemory: number; + private reservedMemory: number; + + constructor(totalMemory: number) { + this.totalMemory = totalMemory; + this.blocks = []; + this.allocatedMemory = 0; + this.reservedMemory = 0; + + // Initialize with one large free block + this.blocks.push(new MemoryBlock(0, totalMemory)); + } + + public allocateMemory(size: number, ownerId: number): number { + if (size <= 0) { + return -1; // Invalid size + } + + // Find suitable free block using first-fit algorithm + for (let i = 0; i < this.blocks.length; i++) { + const block = this.blocks[i]; + if (block.state === MemoryBlockState.FREE && block.size >= size) { + return this.splitAndAllocate(i, size, ownerId); + } + } + + return -1; // No suitable block found + } + + private splitAndAllocate(blockIndex: number, size: number, ownerId: number): number { + const block = this.blocks[blockIndex]; + const startAddress = block.startAddress; + + if (block.size === size) { + // Perfect fit - just allocate the whole block + block.allocate(ownerId); + this.allocatedMemory += size; + } else { + // Split the block + const remainingSize = block.size - size; + + // Resize current block to allocated size + block.size = size; + block.allocate(ownerId); + this.allocatedMemory += size; + + // Create new free block for remaining space + const newBlock = new MemoryBlock(startAddress + size, remainingSize); + this.insertBlock(blockIndex + 1, newBlock); + } + + return startAddress; + } + + private insertBlock(index: number, newBlock: MemoryBlock): void { + // Shift elements to make room + this.blocks.push(new MemoryBlock(0, 0)); // Add space at end + for (let i = this.blocks.length - 1; i > index; i--) { + this.blocks[i] = this.blocks[i - 1]; + } + this.blocks[index] = newBlock; + } + + public freeMemory(startAddress: number): boolean { + // Find block by start address + for (let i = 0; i < this.blocks.length; i++) { + const block = this.blocks[i]; + if (block.startAddress === startAddress && + block.state === MemoryBlockState.ALLOCATED) { + + this.allocatedMemory -= block.size; + block.free(); + + // Try to merge with adjacent free blocks + this.mergeAdjacentBlocks(i); + return true; + } + } + return false; + } + + private mergeAdjacentBlocks(blockIndex: number): void { + const block = this.blocks[blockIndex]; + + // Merge with next block if it's free + if (blockIndex + 1 < this.blocks.length) { + const nextBlock = this.blocks[blockIndex + 1]; + if (nextBlock.state === MemoryBlockState.FREE && + block.getEndAddress() + 1 === nextBlock.startAddress) { + + block.size += nextBlock.size; + this.removeBlock(blockIndex + 1); + } + } + + // Merge with previous block if it's free + if (blockIndex > 0) { + const prevBlock = this.blocks[blockIndex - 1]; + if (prevBlock.state === MemoryBlockState.FREE && + prevBlock.getEndAddress() + 1 === block.startAddress) { + + prevBlock.size += block.size; + this.removeBlock(blockIndex); + } + } + } + + private removeBlock(index: number): void { + // Shift elements to remove the block + for (let i = index; i < this.blocks.length - 1; i++) { + this.blocks[i] = this.blocks[i + 1]; + } + this.blocks.pop(); + } + + public getMemoryUsage(ownerId: number): number { + let usage = 0; + for (let i = 0; i < this.blocks.length; i++) { + const block = this.blocks[i]; + if (block.state === MemoryBlockState.ALLOCATED && block.ownerId === ownerId) { + usage += block.size; + } + } + return usage; + } + + public getFreeMemory(): number { + return this.totalMemory - this.allocatedMemory - this.reservedMemory; + } + + public getAllocatedMemory(): number { + return this.allocatedMemory; + } + + public getFragmentation(): number { + // Count number of free blocks (simple fragmentation metric) + let freeBlockCount = 0; + for (let i = 0; i < this.blocks.length; i++) { + if (this.blocks[i].state === MemoryBlockState.FREE) { + freeBlockCount += 1; + } + } + return freeBlockCount; + } + + public getLargestFreeBlock(): number { + let largest = 0; + for (let i = 0; i < this.blocks.length; i++) { + const block = this.blocks[i]; + if (block.state === MemoryBlockState.FREE && block.size > largest) { + largest = block.size; + } + } + return largest; + } + + public compactMemory(): number { + // Simple compaction - move all allocated blocks to beginning + let compactedBlocks: MemoryBlock[] = []; + let currentAddress = 0; + let totalFreed = 0; + + // Collect allocated blocks and move them to beginning + for (let i = 0; i < this.blocks.length; i++) { + const block = this.blocks[i]; + if (block.state === MemoryBlockState.ALLOCATED) { + const newBlock = new MemoryBlock(currentAddress, block.size); + newBlock.allocate(block.ownerId); + compactedBlocks.push(newBlock); + currentAddress += block.size; + } else if (block.state === MemoryBlockState.FREE) { + totalFreed += block.size; + } + } + + // Add one large free block at the end + if (totalFreed > 0) { + compactedBlocks.push(new MemoryBlock(currentAddress, totalFreed)); + } + + this.blocks = compactedBlocks; + return totalFreed; + } + + public defragmentMemory(): boolean { + let mergedAny = false; + let i = 0; + + while (i < this.blocks.length - 1) { + const current = this.blocks[i]; + const next = this.blocks[i + 1]; + + if (current.state === MemoryBlockState.FREE && + next.state === MemoryBlockState.FREE && + current.getEndAddress() + 1 === next.startAddress) { + + // Merge the blocks + current.size += next.size; + this.removeBlock(i + 1); + mergedAny = true; + } else { + i += 1; + } + } + + return mergedAny; + } + + public freeAllMemoryForOwner(ownerId: number): number { + let freedMemory = 0; + + for (let i = 0; i < this.blocks.length; i++) { + const block = this.blocks[i]; + if (block.state === MemoryBlockState.ALLOCATED && block.ownerId === ownerId) { + freedMemory += block.size; + this.allocatedMemory -= block.size; + block.free(); + } + } + + // Perform defragmentation after freeing + if (freedMemory > 0) { + this.defragmentMemory(); + } + + return freedMemory; + } +} diff --git a/examples/reachability/sample-project/ProcessManager.ts b/examples/reachability/sample-project/ProcessManager.ts new file mode 100644 index 0000000000..bf82dae18a --- /dev/null +++ b/examples/reachability/sample-project/ProcessManager.ts @@ -0,0 +1,327 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +// Process Manager - Sample TypeScript project for reachability analysis +// This project simulates basic process management operations using only SMT-solver friendly constructs: +// - Integer operations (no floating-point) +// - Array operations (length, indexing) +// - Object field access and updates +// - Conditional logic and control flow +// - Function calls without complex inheritance + +export enum ProcessState { + CREATED = 0, + READY = 1, + RUNNING = 2, + BLOCKED = 3, + TERMINATED = 4 +} + +export enum ProcessPriority { + LOW = 1, + NORMAL = 2, + HIGH = 3, + CRITICAL = 4 +} + +export class Process { + public pid: number; + public parentPid: number; + public state: ProcessState; + public priority: ProcessPriority; + public memoryUsage: number; // in KB, integer only + public cpuTime: number; // in milliseconds, integer only + public children: number[]; // Array of child PIDs + public isSystemProcess: boolean; + + constructor(pid: number, parentPid: number = 0) { + this.pid = pid; + this.parentPid = parentPid; + this.state = ProcessState.CREATED; + this.priority = ProcessPriority.NORMAL; + this.memoryUsage = 1024; // Default 1MB + this.cpuTime = 0; + this.children = []; + this.isSystemProcess = parentPid === 0; + } + + public start(): boolean { + if (this.state === ProcessState.CREATED || this.state === ProcessState.READY) { + this.state = ProcessState.RUNNING; + return true; + } + return false; + } + + public pause(): boolean { + if (this.state === ProcessState.RUNNING) { + this.state = ProcessState.READY; + return true; + } + return false; + } + + public block(): boolean { + if (this.state === ProcessState.RUNNING) { + this.state = ProcessState.BLOCKED; + return true; + } + return false; + } + + public unblock(): boolean { + if (this.state === ProcessState.BLOCKED) { + this.state = ProcessState.READY; + return true; + } + return false; + } + + public terminate(): boolean { + if (this.state !== ProcessState.TERMINATED) { + this.state = ProcessState.TERMINATED; + return true; + } + return false; + } + + public addChild(childPid: number): boolean { + // Check if child already exists + for (let i = 0; i < this.children.length; i++) { + if (this.children[i] === childPid) { + return false; // Already exists + } + } + this.children.push(childPid); + return true; + } + + public removeChild(childPid: number): boolean { + for (let i = 0; i < this.children.length; i++) { + if (this.children[i] === childPid) { + // Remove by shifting elements + for (let j = i; j < this.children.length - 1; j++) { + this.children[j] = this.children[j + 1]; + } + this.children.pop(); + return true; + } + } + return false; + } + + public updateMemoryUsage(newUsage: number): boolean { + if (newUsage < 0) { + return false; // Invalid memory usage + } + this.memoryUsage = newUsage; + return true; + } + + public addCpuTime(additionalTime: number): void { + if (additionalTime > 0) { + this.cpuTime += additionalTime; + } + } + + public setPriority(newPriority: ProcessPriority): boolean { + if (this.isSystemProcess && newPriority < ProcessPriority.HIGH) { + return false; // System processes must have high priority + } + this.priority = newPriority; + return true; + } + + public canBeKilled(): boolean { + if (this.isSystemProcess) { + return false; // System processes cannot be killed + } + if (this.children.length > 0) { + return false; // Cannot kill process with children + } + return this.state !== ProcessState.TERMINATED; + } +} + +export class ProcessManager { + private processes: Process[]; + private nextPid: number; + private maxProcesses: number; + private runningCount: number; + + constructor(maxProcesses: number = 100) { + this.processes = []; + this.nextPid = 1; + this.maxProcesses = maxProcesses; + this.runningCount = 0; + } + + public createProcess(parentPid: number = 0): number { + if (this.processes.length >= this.maxProcesses) { + return -1; // Too many processes + } + + // Verify parent exists if specified + if (parentPid !== 0) { + const parent = this.findProcess(parentPid); + if (parent === null || parent.state === ProcessState.TERMINATED) { + return -1; // Invalid parent + } + } + + const newProcess = new Process(this.nextPid, parentPid); + this.processes.push(newProcess); + + // Add to parent's children list + if (parentPid !== 0) { + const parent = this.findProcess(parentPid); + if (parent !== null) { + parent.addChild(this.nextPid); + } + } + + this.nextPid += 1; + return newProcess.pid; + } + + public startProcess(pid: number): boolean { + const process = this.findProcess(pid); + if (process === null) { + return false; + } + + if (process.start()) { + this.runningCount += 1; + return true; + } + return false; + } + + public killProcess(pid: number): boolean { + const process = this.findProcess(pid); + if (process === null) { + return false; + } + + if (!process.canBeKilled()) { + return false; + } + + // Update running count if needed + if (process.state === ProcessState.RUNNING) { + this.runningCount -= 1; + } + + // Remove from parent's children list + if (process.parentPid !== 0) { + const parent = this.findProcess(process.parentPid); + if (parent !== null) { + parent.removeChild(pid); + } + } + + return process.terminate(); + } + + public getProcessesByState(state: ProcessState): number[] { + const result: number[] = []; + for (let i = 0; i < this.processes.length; i++) { + if (this.processes[i].state === state) { + result.push(this.processes[i].pid); + } + } + return result; + } + + public getProcessesByPriority(priority: ProcessPriority): number[] { + const result: number[] = []; + for (let i = 0; i < this.processes.length; i++) { + if (this.processes[i].priority === priority) { + result.push(this.processes[i].pid); + } + } + return result; + } + + public getTotalMemoryUsage(): number { + let total = 0; + for (let i = 0; i < this.processes.length; i++) { + if (this.processes[i].state !== ProcessState.TERMINATED) { + total += this.processes[i].memoryUsage; + } + } + return total; + } + + public getSystemProcessCount(): number { + let count = 0; + for (let i = 0; i < this.processes.length; i++) { + if (this.processes[i].isSystemProcess && + this.processes[i].state !== ProcessState.TERMINATED) { + count += 1; + } + } + return count; + } + + public findProcess(pid: number): Process | null { + for (let i = 0; i < this.processes.length; i++) { + if (this.processes[i].pid === pid) { + return this.processes[i]; + } + } + return null; + } + + public scheduleNext(): number { + // Simple priority-based scheduling + let bestProcess: Process | null = null; + let highestPriority = 0; + + for (let i = 0; i < this.processes.length; i++) { + const process = this.processes[i]; + if (process.state === ProcessState.READY && + process.priority > highestPriority) { + highestPriority = process.priority; + bestProcess = process; + } + } + + if (bestProcess !== null) { + if (bestProcess.start()) { + this.runningCount += 1; + return bestProcess.pid; + } + } + + return -1; // No process to schedule + } + + public cleanupTerminated(): number { + let cleanedCount = 0; + let i = 0; + + while (i < this.processes.length) { + if (this.processes[i].state === ProcessState.TERMINATED) { + // Remove by shifting elements + for (let j = i; j < this.processes.length - 1; j++) { + this.processes[j] = this.processes[j + 1]; + } + this.processes.pop(); + cleanedCount += 1; + } else { + i += 1; + } + } + + return cleanedCount; + } + + public getRunningCount(): number { + return this.runningCount; + } + + public getProcessCount(): number { + return this.processes.length; + } +} diff --git a/examples/reachability/targets.yml b/examples/reachability/targets.yml new file mode 100644 index 0000000000..3d1080aaf6 --- /dev/null +++ b/examples/reachability/targets.yml @@ -0,0 +1,32 @@ +# YAML format example using Linear Trace structure +targets: + - type: initial + location: + fileName: "FileManager.ts" + className: "FileManager" + methodName: "readFile" + stmtType: "IfStmt" + block: 0 + index: 0 + - location: + fileName: "FileManager.ts" + className: "FileManager" + methodName: "readFile" + stmtType: "AssignStmt" + block: 1 + index: 2 + - location: + fileName: "FileManager.ts" + className: "FileManager" + methodName: "processFile" + stmtType: "CallStmt" + block: 0 + index: 0 + - type: final + location: + fileName: "FileManager.ts" + className: "FileManager" + methodName: "processFile" + stmtType: "ReturnStmt" + block: 2 + index: 5 diff --git a/settings.gradle.kts b/settings.gradle.kts index 428d679fce..a4ea520f7e 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -55,18 +55,18 @@ findProject(":usvm-python:usvm-python-commons")?.name = "usvm-python-commons" // Actually, relative path is enough, but there is a bug in IDEA when the path is a symlink. // As a workaround, we convert it to a real absolute path. // See IDEA bug: https://youtrack.jetbrains.com/issue/IDEA-329756 -// val jacodbPath = file("jacodb").takeIf { it.exists() } -// ?: file("../jacodb").takeIf { it.exists() } -// ?: error("Local JacoDB directory not found") -// includeBuild(jacodbPath.toPath().toRealPath().toAbsolutePath()) { -// dependencySubstitution { -// all { -// val requested = requested -// if (requested is ModuleComponentSelector && requested.group == "com.github.UnitTestBot.jacodb") { -// val targetProject = ":${requested.module}" -// useTarget(project(targetProject)) -// logger.info("Substituting ${requested.group}:${requested.module} with $targetProject") -// } -// } -// } -// } +val jacodbPath = file("jacodb").takeIf { it.exists() } + ?: file("../jacodb").takeIf { it.exists() } + ?: error("Local JacoDB directory not found") +includeBuild(jacodbPath.toPath().toRealPath().toAbsolutePath()) { + dependencySubstitution { + all { + val requested = requested + if (requested is ModuleComponentSelector && requested.group == "com.github.UnitTestBot.jacodb") { + val targetProject = ":${requested.module}" + useTarget(project(targetProject)) + logger.info("Substituting ${requested.group}:${requested.module} with $targetProject") + } + } + } +} diff --git a/usvm-ts/build.gradle.kts b/usvm-ts/build.gradle.kts index 96de26034a..653999d199 100644 --- a/usvm-ts/build.gradle.kts +++ b/usvm-ts/build.gradle.kts @@ -8,6 +8,9 @@ import kotlin.time.Duration plugins { id("usvm.kotlin-conventions") + kotlin("plugin.serialization") version Versions.kotlin + application + id(Plugins.Shadow) } dependencies { @@ -16,6 +19,8 @@ dependencies { implementation(Libs.jacodb_core) implementation(Libs.jacodb_ets) + implementation(Libs.clikt) + implementation(Libs.kotlinx_serialization_json) implementation(Libs.ksmt_yices) implementation(Libs.ksmt_cvc5) @@ -32,6 +37,41 @@ dependencies { testImplementation("org.burningwave:core:12.62.7") } +application { + mainClass = "org.usvm.api.reachability.cli.ReachabilityKt" + applicationDefaultJvmArgs = listOf("-Dfile.encoding=UTF-8", "-Dsun.stdout.encoding=UTF-8") +} + +fun createStartScript(name: String, configure: CreateStartScripts.() -> Unit) = + tasks.register("startScripts$name") { + applicationName = name + outputDir = tasks.startScripts.get().outputDir + classpath = tasks.startScripts.get().classpath + configure() + }.also { + tasks.named("startScripts") { + dependsOn(it) + } + } + +createStartScript("usvm-ts-reachability") { + mainClass = "org.usvm.api.reachability.cli.ReachabilityKt" + defaultJvmOpts = listOf("-Xmx4g", "-Dfile.encoding=UTF-8", "-Dsun.stdout.encoding=UTF-8") +} + +tasks.shadowJar { + archiveBaseName.set("usvm-ts-all") + archiveClassifier.set("") + mergeServiceFiles() + + // minimize { + // // Keep necessary service files and dependencies + // exclude(dependency("com.github.ajalt.mordant:.*:.*")) + // exclude(dependency("ch.qos.logback:.*")) + // exclude(dependency("org.slf4j:.*")) + // } +} + val generateSdkIR by tasks.registering { group = "build" description = "Generates SDK IR using ArkAnalyzer." diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsTarget.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsTarget.kt new file mode 100644 index 0000000000..c7d1a3319b --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsTarget.kt @@ -0,0 +1,6 @@ +package org.usvm.api + +import org.jacodb.ets.model.EtsStmt +import org.usvm.targets.UTarget + +open class TsTarget(location: EtsStmt?) : UTarget(location) diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/targets/ReachabilityObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/api/reachability/TsReachabilityObserver.kt similarity index 92% rename from usvm-ts/src/main/kotlin/org/usvm/api/targets/ReachabilityObserver.kt rename to usvm-ts/src/main/kotlin/org/usvm/api/reachability/TsReachabilityObserver.kt index 4c12c769ed..4cec9ca818 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/targets/ReachabilityObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/reachability/TsReachabilityObserver.kt @@ -1,9 +1,9 @@ -package org.usvm.api.targets +package org.usvm.api.reachability import org.usvm.machine.state.TsState import org.usvm.statistics.UMachineObserver -class ReachabilityObserver : UMachineObserver { +class TsReachabilityObserver : UMachineObserver { override fun onState(parent: TsState, forks: Sequence) { parent .targets diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/targets/TsTarget.kt b/usvm-ts/src/main/kotlin/org/usvm/api/reachability/TsReachabilityTarget.kt similarity index 71% rename from usvm-ts/src/main/kotlin/org/usvm/api/targets/TsTarget.kt rename to usvm-ts/src/main/kotlin/org/usvm/api/reachability/TsReachabilityTarget.kt index 356d2a4b65..1e7a24fd47 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/targets/TsTarget.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/reachability/TsReachabilityTarget.kt @@ -1,9 +1,7 @@ -package org.usvm.api.targets +package org.usvm.api.reachability import org.jacodb.ets.model.EtsStmt -import org.usvm.targets.UTarget - -open class TsTarget(location: EtsStmt?) : UTarget(location) +import org.usvm.api.TsTarget sealed class TsReachabilityTarget(override val location: EtsStmt) : TsTarget(location) { class InitialPoint(location: EtsStmt) : TsReachabilityTarget(location) diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/reachability/cli/Reachability.kt b/usvm-ts/src/main/kotlin/org/usvm/api/reachability/cli/Reachability.kt new file mode 100644 index 0000000000..414887595d --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/api/reachability/cli/Reachability.kt @@ -0,0 +1,641 @@ +package org.usvm.api.reachability.cli + +import com.github.ajalt.clikt.core.CliktCommand +import com.github.ajalt.clikt.core.context +import com.github.ajalt.clikt.core.main +import com.github.ajalt.clikt.output.MordantHelpFormatter +import com.github.ajalt.clikt.parameters.options.default +import com.github.ajalt.clikt.parameters.options.flag +import com.github.ajalt.clikt.parameters.options.multiple +import com.github.ajalt.clikt.parameters.options.option +import com.github.ajalt.clikt.parameters.options.required +import com.github.ajalt.clikt.parameters.types.enum +import com.github.ajalt.clikt.parameters.types.int +import com.github.ajalt.clikt.parameters.types.long +import com.github.ajalt.clikt.parameters.types.path +import kotlinx.serialization.json.Json +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.api.TsTarget +import org.usvm.api.reachability.TsReachabilityObserver +import org.usvm.api.reachability.TsReachabilityTarget +import org.usvm.api.reachability.dto.LocationDto +import org.usvm.api.reachability.dto.TargetDto +import org.usvm.api.reachability.dto.TargetTreeNodeDto +import org.usvm.api.reachability.dto.TargetTypeDto +import org.usvm.api.reachability.dto.TargetsContainerDto +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsState +import java.nio.file.Path +import kotlin.io.path.Path +import kotlin.io.path.createDirectories +import kotlin.io.path.div +import kotlin.io.path.readText +import kotlin.io.path.relativeTo +import kotlin.io.path.writeText +import kotlin.time.Duration +import kotlin.time.Duration.Companion.seconds + +/** + * Reachability Analysis CLI for TypeScript code + * + * This tool performs reachability analysis on TypeScript projects to determine + * which code paths can be reached under various conditions. + */ +class ReachabilityAnalyzer : CliktCommand( + name = "reachability" +) { + init { + context { + helpFormatter = { + MordantHelpFormatter( + it, + requiredOptionMarker = "šŸ”ø", + showDefaultValues = true, + showRequiredTag = true + ) + } + } + } + + // Input Options + private val projectPath by option( + "-p", "--project", + help = "šŸ“ Path to TypeScript project directory" + ).path(mustExist = true).required() + + private val targetsFile by option( + "-t", "--targets", + help = "šŸ“‹ JSON file with target definitions (optional - will analyze all methods if not provided)" + ).path(mustExist = true) + + private val output by option( + "-o", "--output", + help = "šŸ“„ Output directory for analysis results" + ).path().default(Path("./reachability-results")) + + // Analysis Configuration + private val analysisMode by option( + "-m", "--mode", + help = "šŸ” Analysis scope" + ).enum().default(AnalysisMode.PUBLIC_METHODS) + + private val methodFilter by option( + "--method", + help = "šŸŽÆ Filter methods by name pattern" + ).multiple() + + // Solver & Performance Options + private val solverType by option( + "--solver", + help = "āš™ļø SMT solver" + ).enum().default(SolverType.YICES) + + private val timeout by option( + "--timeout", + help = "ā° Analysis timeout (seconds)" + ).int().default(300) + + private val stepsLimit by option( + "--steps", + help = "šŸ‘£ Max steps from last covered statement" + ).long().default(3500L) + + // Output Options + private val verbose by option( + "-v", "--verbose", + help = "šŸ“ Verbose output" + ).flag() + + private val includeStatements by option( + "--include-statements", + help = "šŸ“ Include statement details in output" + ).flag() + + override fun run() { + setupLogging() + + echo("šŸš€ Starting TypeScript Reachability Analysis") + echo( + "" + + "ā”Œā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”\n" + + "ā”‚ USVM Reachability Tool ā”‚\n" + + "ā””ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”€ā”˜" + ) + + val startTime = System.currentTimeMillis() + + try { + val results = performAnalysis() + generateReports(results, startTime) + + echo("āœ… Analysis completed successfully!") + + } catch (e: Exception) { + echo("āŒ Analysis failed: ${e.message}", err = true) + if (verbose) { + e.printStackTrace() + } + throw e + } + + echo("šŸ‘‹ Exiting.") + } + + private fun setupLogging() { + if (verbose) { + System.setProperty("org.slf4j.simpleLogger.defaultLogLevel", "DEBUG") + } + } + + private fun performAnalysis(): ReachabilityResults { + echo("šŸ” Loading TypeScript project...") + + // Load TypeScript project using autoConvert like in tests + val tsFiles = findTypeScriptFiles(projectPath) + if (tsFiles.isEmpty()) { + throw IllegalArgumentException("No TypeScript files found in $projectPath") + } + + echo("šŸ“ Found ${tsFiles.size} TypeScript files") + val scene = EtsScene(tsFiles.map { loadEtsFileAutoConvert(it) }) + echo("šŸ“Š Project loaded: ${scene.projectClasses.size} classes") + + // Configure machine options + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), + exceptionsPropagation = true, + stopOnTargetsReached = true, + timeout = timeout.seconds, + stepsFromLastCovered = stepsLimit, + solverType = solverType, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + + val tsOptions = TsOptions() + val machine = TsMachine(scene, machineOptions, tsOptions, machineObserver = TsReachabilityObserver()) + + // Find methods to analyze + val methodsToAnalyze = findMethodsToAnalyze(scene) + echo("šŸŽÆ Analyzing ${methodsToAnalyze.size} methods") + + // Prepare targets + val targets = if (targetsFile != null) { + val targetTraces = parseTargetDefinitions(targetsFile!!) + val targets = createTargetsFromTraces(methodsToAnalyze, targetTraces) + echo("šŸ“ Created ${targets.size} reachability target trees from ${targetTraces.size} traces") + targets + } else { + val targets = generateDefaultTargets(methodsToAnalyze) + echo("šŸ“ Generated ${targets.size} default reachability targets") + targets + } + + // Run analysis + echo("āš” Running reachability analysis...") + val states = machine.analyze(methodsToAnalyze, targets) + + // Analyze results for reachability + val reachabilityResults = analyzeReachability(targets, states) + + return ReachabilityResults( + methods = methodsToAnalyze, + targets = targets, + states = states, + reachabilityResults = reachabilityResults, + scene = scene + ) + } + + private fun findTypeScriptFiles(projectDir: Path): List { + return projectDir.toFile().walkTopDown() + .filter { it.isFile && (it.extension == "ts" || it.extension == "js") } + .map { it.toPath() } + .toList() + } + + private fun findMethodsToAnalyze(scene: EtsScene): List { + val allMethods = scene.projectClasses.flatMap { it.methods } + + return if (methodFilter.isNotEmpty()) { + allMethods.filter { method -> + val fullName = "${method.enclosingClass?.name ?: "Unknown"}.${method.name}" + methodFilter.any { pattern -> + fullName.contains(pattern, ignoreCase = true) + } + } + } else { + when (analysisMode) { + AnalysisMode.ALL_METHODS -> allMethods + AnalysisMode.PUBLIC_METHODS -> allMethods.filter { it.isPublic } + AnalysisMode.ENTRY_POINTS -> allMethods.filter { + it.name == "main" || it.isPublic + } + } + } + } + + private fun parseTargetDefinitions(targetsFile: Path): List { + val content = targetsFile.readText() + return try { + val json = Json { + ignoreUnknownKeys = true + isLenient = true + } + + val container = json.decodeFromString(content) + val traces = extractTargetTraces(container) + + echo("šŸ“‹ Parsed ${traces.size} target traces from ${targetsFile.fileName}") + traces + + } catch (e: Exception) { + echo("āŒ Error parsing targets file: ${e.message}", err = true) + if (verbose) { + e.printStackTrace() + } + emptyList() + } + } + + private fun extractTargetTraces(container: TargetsContainerDto): List { + return when (container) { + // Single trace (linear or tree) + is TargetsContainerDto.SingleTrace -> { + listOf(extractTargetTrace(container)) + } + + // Multiple traces (can be linear or tree) + is TargetsContainerDto.TraceList -> { + container.traces.map { extractTargetTrace(it) } + } + } + } + + private fun extractTargetTrace(trace: TargetsContainerDto.SingleTrace): TargetTrace { + return when (trace) { + // Single linear trace + is TargetsContainerDto.LinearTrace -> { + TargetTrace.Linear(targets = trace.targets) + } + + // Single tree trace + is TargetsContainerDto.TreeTrace -> { + TargetTrace.Tree(root = trace.root) + } + } + } + + // TODO: remove + private fun buildLinearTrace(targets: List): TargetTreeNodeDto? { + if (targets.isEmpty()) return null + + var current: TargetTreeNodeDto? = null + + for (target in targets.asReversed()) { + current = TargetTreeNodeDto(target, children = listOfNotNull(current)) + } + + return current + } + + private fun generateDefaultTargets(methods: List): List { + return methods.mapNotNull { method -> + val statements = method.cfg.stmts + if (statements.isEmpty()) return@mapNotNull null + + // Initial point - first statement + val initialTarget = TsReachabilityTarget.InitialPoint(statements.first()) + var target: TsTarget = initialTarget + + // Intermediate and final points for control flow statements + statements.forEachIndexed { index, stmt -> + when (stmt) { + is EtsIfStmt, is EtsReturnStmt -> { + val newTarget = if (index == statements.lastIndex) { + TsReachabilityTarget.FinalPoint(stmt) + } else { + TsReachabilityTarget.IntermediatePoint(stmt) + } + target = target.addChild(newTarget) + } + } + } + + initialTarget + } + } + + private fun createTargetsFromTraces( + methods: List, + targetTraces: List, + ): List { + val targets = mutableListOf() + val methodMap = methods.associateBy { "${it.enclosingClass?.name ?: "Unknown"}.${it.name}" } + + targetTraces.forEach { trace -> + val root = when (trace) { + is TargetTrace.Tree -> trace.root + is TargetTrace.Linear -> buildLinearTrace(trace.targets)!! + } + + // For each trace, find the corresponding method and build the target hierarchy + val methodName = "${root.target.location.className}.${root.target.location.methodName}" + val method = methodMap[methodName] ?: return@forEach + + // Resolve the root target and build the hierarchy using addChild + val rootTarget = resolveTargetNode(root, method.cfg.stmts) + if (rootTarget != null) { + targets.add(rootTarget) + } + } + + return targets + } + + private fun resolveTargetNode(node: TargetTreeNodeDto, statements: List): TsTarget? { + // First, resolve the current node to a TsReachabilityTarget + val stmt = findStatementByTarget(statements, node.target) ?: return null + + val currentTarget: TsTarget = when (node.target.type) { + TargetTypeDto.INITIAL -> TsReachabilityTarget.InitialPoint(stmt) + TargetTypeDto.INTERMEDIATE -> TsReachabilityTarget.IntermediatePoint(stmt) + TargetTypeDto.FINAL -> TsReachabilityTarget.FinalPoint(stmt) + } + + // Add all children to build the hierarchical structure + node.children.forEach { childNode -> + val childTarget = resolveTargetNode(childNode, statements) + if (childTarget != null) { + currentTarget.addChild(childTarget) + } + } + + return currentTarget + } + + private fun findStatementByTarget( + statements: List, + target: TargetDto, + ): EtsStmt? { + val targetLocation = target.location + + // Find statement by matching location properties + statements.find { stmt -> + matchesLocation(stmt, targetLocation) + }?.let { return it } + + // Use index-based lookup if index is available + targetLocation.index?.let { index -> + if (index >= 0 && index < statements.size) { + return statements[index] + } + } + + return statements.firstOrNull() + } + + private fun matchesLocation(stmt: EtsStmt, location: LocationDto): Boolean { + // Match by statement type if specified + location.stmtType?.let { expectedType -> + val actualType = stmt.javaClass.simpleName + return actualType.contains(expectedType, ignoreCase = true) + } + + // Match by block and index if both are specified + if (location.block != null && location.index != null) { + // Location matching based on statement position + return matchesByPosition(stmt, location.block, location.index) + } + + // Default to true if no specific matching criteria + return true + } + + private fun matchesByPosition(stmt: EtsStmt, expectedBlock: Int, expectedIndex: Int): Boolean { + // Use statement hash and properties to determine position match + val stmtHash = stmt.hashCode() + val blockMatch = (stmtHash / 1000) % 10 == expectedBlock % 10 + val indexMatch = stmtHash % 100 == expectedIndex % 100 + return blockMatch && indexMatch + } + + private fun analyzeReachability( + targets: List, + states: List, + ): List { + val results = mutableListOf() + + // Get all reached statements across all execution paths + val allReachedStatements = states.flatMap { it.pathNode.allStatements }.toSet() + + targets.forEach { target -> + val targetLocation = target.location + if (targetLocation != null) { + val reachabilityStatus = when { + targetLocation in allReachedStatements -> ReachabilityStatus.REACHABLE + states.isEmpty() -> ReachabilityStatus.UNKNOWN + else -> ReachabilityStatus.UNREACHABLE + } + + val executionPaths = if (reachabilityStatus == ReachabilityStatus.REACHABLE) { + states.filter { targetLocation in it.pathNode.allStatements } + .map { state -> + ExecutionPath( + statements = state.pathNode.allStatements.toList() + ) + } + } else { + emptyList() + } + + results.add( + TargetReachabilityResult( + target = target, + status = reachabilityStatus, + executionPaths = executionPaths, + ) + ) + } + } + + return results + } + + private fun generateReports(results: ReachabilityResults, startTime: Long) { + echo("šŸ“Š Generating analysis reports...") + + output.createDirectories() + val duration = (System.currentTimeMillis() - startTime) / 1000.0 + + generateSummaryReport(results, duration) + generateDetailedReport(results, duration) + + printSummaryToConsole(results, duration) + } + + private fun generateSummaryReport(results: ReachabilityResults, duration: Double) { + val reportFile = output / "reachability_summary.txt" + reportFile.writeText(buildString { + appendLine("šŸŽÆ REACHABILITY ANALYSIS SUMMARY") + appendLine("=".repeat(50)) + appendLine("ā±ļø Duration: ${String.format("%.2f", duration)}s") + appendLine("šŸ” Methods analyzed: ${results.methods.size}") + appendLine("šŸ“ Targets analyzed: ${results.reachabilityResults.size}") + + val statusCounts = results.reachabilityResults.groupingBy { it.status }.eachCount() + appendLine("āœ… Reachable: ${statusCounts[ReachabilityStatus.REACHABLE] ?: 0}") + appendLine("āŒ Unreachable: ${statusCounts[ReachabilityStatus.UNREACHABLE] ?: 0}") + appendLine("ā“ Unknown: ${statusCounts[ReachabilityStatus.UNKNOWN] ?: 0}") + + appendLine("\nšŸ“ˆ DETAILED RESULTS") + appendLine("-".repeat(30)) + + results.reachabilityResults.forEach { result -> + val targetType = when (result.target) { + is TsReachabilityTarget.InitialPoint -> "INITIAL" + is TsReachabilityTarget.IntermediatePoint -> "INTERMEDIATE" + is TsReachabilityTarget.FinalPoint -> "FINAL" + else -> "UNKNOWN" + } + + appendLine("Target: $targetType at ${result.target.location?.javaClass?.simpleName}") + appendLine(" Status: ${result.status}") + if (result.executionPaths.isNotEmpty()) { + appendLine(" Paths found: ${result.executionPaths.size}") + } + appendLine() + } + }) + + echo("šŸ“„ Summary saved to: ${reportFile.relativeTo(Path("."))}") + } + + private fun generateDetailedReport(results: ReachabilityResults, duration: Double) { + val reportFile = output / "reachability_detailed.md" + reportFile.writeText(buildString { + appendLine("# šŸŽÆ TypeScript Reachability Analysis - Detailed Report") + appendLine() + appendLine("**Analysis Duration:** ${String.format("%.2f", duration)}s") + appendLine("**Methods Analyzed:** ${results.methods.size}") + appendLine("**Targets Analyzed:** ${results.reachabilityResults.size}") + appendLine() + + val statusCounts = results.reachabilityResults.groupingBy { it.status }.eachCount() + appendLine("## šŸ“Š Reachability Summary") + appendLine("- āœ… **Reachable:** ${statusCounts[ReachabilityStatus.REACHABLE] ?: 0}") + appendLine("- āŒ **Unreachable:** ${statusCounts[ReachabilityStatus.UNREACHABLE] ?: 0}") + appendLine("- ā“ **Unknown:** ${statusCounts[ReachabilityStatus.UNKNOWN] ?: 0}") + appendLine() + + appendLine("## šŸ” Target Analysis Results") + appendLine() + + results.reachabilityResults.forEach { result -> + val targetType = when (result.target) { + is TsReachabilityTarget.InitialPoint -> "Initial Point" + is TsReachabilityTarget.IntermediatePoint -> "Intermediate Point" + is TsReachabilityTarget.FinalPoint -> "Final Point" + else -> "Unknown Target" + } + + val statusIcon = when (result.status) { + ReachabilityStatus.REACHABLE -> "āœ…" + ReachabilityStatus.UNREACHABLE -> "āŒ" + ReachabilityStatus.UNKNOWN -> "ā“" + } + + appendLine("### $statusIcon $targetType") + appendLine("**Location:** ${result.target.location?.javaClass?.simpleName ?: "Unknown"}") + appendLine("**Status:** ${result.status}") + + if (result.executionPaths.isNotEmpty()) { + appendLine("**Execution Paths Found:** ${result.executionPaths.size}") + + if (includeStatements) { + result.executionPaths.forEachIndexed { pathIndex, path -> + appendLine("#### Path ${pathIndex + 1}") + appendLine("Statements in execution path:") + path.statements.forEachIndexed { stmtIndex, stmt -> + appendLine( + "${stmtIndex + 1}. ${stmt.javaClass.simpleName}: `${ + stmt.toString().take(60) + }...`" + ) + } + appendLine() + } + } + } + appendLine() + } + }) + + echo("šŸ“„ Detailed report saved to: ${reportFile.relativeTo(Path("."))}") + } + + private fun printSummaryToConsole(results: ReachabilityResults, duration: Double) { + echo("") + echo("šŸŽ‰ Analysis Complete!") + echo("ā±ļø Duration: ${String.format("%.2f", duration)}s") + echo("šŸ” Methods: ${results.methods.size}") + echo("šŸ“ Targets: ${results.reachabilityResults.size}") + + val statusCounts = results.reachabilityResults.groupingBy { it.status }.eachCount() + echo("āœ… Reachable: ${statusCounts[ReachabilityStatus.REACHABLE] ?: 0}") + echo("āŒ Unreachable: ${statusCounts[ReachabilityStatus.UNREACHABLE] ?: 0}") + echo("ā“ Unknown: ${statusCounts[ReachabilityStatus.UNKNOWN] ?: 0}") + echo("šŸ“ Reports saved to: ${output.relativeTo(Path("."))}") + } +} + +enum class AnalysisMode { + ALL_METHODS, + PUBLIC_METHODS, + ENTRY_POINTS, +} + +enum class ReachabilityStatus { + REACHABLE, // Confirmed reachable with execution path + UNREACHABLE, // Confirmed unreachable + UNKNOWN, // Could not determine (timeout/approximation/error) +} + +data class ExecutionPath( + val statements: List, +) + +data class TargetReachabilityResult( + val target: TsTarget, + val status: ReachabilityStatus, + val executionPaths: List, +) + +data class ReachabilityResults( + val methods: List, + val targets: List, + val states: List, + val reachabilityResults: List, + val scene: EtsScene, +) + +/** + * Represents a trace - an independent hierarchical structure of targets. + */ +sealed interface TargetTrace { + data class Linear(val targets: List) : TargetTrace + data class Tree(val root: TargetTreeNodeDto) : TargetTrace +} + +fun main(args: Array) { + ReachabilityAnalyzer().main(args) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/reachability/dto/Targets.kt b/usvm-ts/src/main/kotlin/org/usvm/api/reachability/dto/Targets.kt new file mode 100644 index 0000000000..14c871bd67 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/api/reachability/dto/Targets.kt @@ -0,0 +1,109 @@ +package org.usvm.api.reachability.dto + +import kotlinx.serialization.DeserializationStrategy +import kotlinx.serialization.SerialName +import kotlinx.serialization.Serializable +import kotlinx.serialization.json.JsonArray +import kotlinx.serialization.json.JsonContentPolymorphicSerializer +import kotlinx.serialization.json.JsonElement +import kotlinx.serialization.json.JsonObject + +// The `targets.json` can contain the traces in the following formats: +// - { "targets": [...] }, a single linear trace with a list of targets +// - { "target": {...}, "children": [...] }, a single tree-like trace with a tree structure of targets +// - [ {...} ], a list of traces (can contain both linear and tree traces) +// +// Note: +// - A trace is a sequence of targets (points). +// Note: +// - A target is a point, i.e. a statement in the code. +// - A target can be of type: initial, intermediate (default), final. + +@Serializable(with = TargetsContainerSerializer::class) +sealed interface TargetsContainerDto { + + @Serializable(with = SingleTraceSerializer::class) + sealed interface SingleTrace : TargetsContainerDto + + // Format: { "targets": [...] } + @Serializable + data class LinearTrace( + val targets: List, + ) : SingleTrace + + // Format: { "root": {...} } + @Serializable + data class TreeTrace( + val root: TargetTreeNodeDto, + ) : SingleTrace + + // Format: [ {...} ] + @Serializable + data class TraceList( + val traces: List, + ) : TargetsContainerDto +} + +object SingleTraceSerializer : + JsonContentPolymorphicSerializer(TargetsContainerDto.SingleTrace::class) { + + override fun selectDeserializer(element: JsonElement): DeserializationStrategy = + when { + // Object with "targets" field: { "targets": [...] } + element is JsonObject && element.containsKey("targets") -> TargetsContainerDto.LinearTrace.serializer() + + // Object with "root" field: { "root": {...} } + element is JsonObject && element.containsKey("root") -> TargetsContainerDto.TreeTrace.serializer() + + else -> error("Unknown single trace format") + } + + fun deserializeSingleTrace(element: JsonElement): DeserializationStrategy = + selectDeserializer(element) as DeserializationStrategy +} + +object TargetsContainerSerializer : + JsonContentPolymorphicSerializer(TargetsContainerDto::class) { + + override fun selectDeserializer(element: JsonElement): DeserializationStrategy = when { + // Array at top level: [ {...} ] + element is JsonArray -> TargetsContainerDto.TraceList.serializer() + + // Any object: delegate to SingleTraceSerializer + else -> SingleTraceSerializer.deserializeSingleTrace(element) + } +} + +@Serializable +data class TargetTreeNodeDto( + val target: TargetDto, + val children: List = emptyList(), +) + +@Serializable +enum class TargetTypeDto { + @SerialName("initial") + INITIAL, + + @SerialName("intermediate") + INTERMEDIATE, + + @SerialName("final") + FINAL, +} + +@Serializable +data class TargetDto( + val type: TargetTypeDto = TargetTypeDto.INTERMEDIATE, + val location: LocationDto, // TODO: consider inlining +) + +@Serializable +data class LocationDto( + val fileName: String, + val className: String, + val methodName: String, + val stmtType: String? = null, + val block: Int? = null, + val index: Int? = null, +) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index cd7d487192..255c7f4597 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -1,6 +1,7 @@ package org.usvm.machine import mu.KotlinLogging +import org.jacodb.ets.model.EtsLexicalEnvType import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStmt @@ -8,7 +9,7 @@ import org.usvm.CoverageZone import org.usvm.StateCollectionStrategy import org.usvm.UMachine import org.usvm.UMachineOptions -import org.usvm.api.targets.TsTarget +import org.usvm.api.TsTarget import org.usvm.machine.interpreter.TsInterpreter import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState @@ -52,6 +53,10 @@ class TsMachine( methods: List, targets: List = emptyList(), ): List { + val methods = methods.filterNot { + it.parameters.isNotEmpty() && it.parameters.first().type is EtsLexicalEnvType + } + val initialStates = mutableMapOf() methods.forEach { initialStates[it] = interpreter.getInitialState(it, targets) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt index 49616f7db8..3e23181882 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt @@ -1,5 +1,6 @@ package org.usvm.machine +import org.jacodb.ets.dto.StmtDto import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsMethodSignature import org.jacodb.ets.model.EtsStmt @@ -25,6 +26,8 @@ class TsVirtualMethodCallStmt( override val args: List>, override val returnSite: EtsStmt, ) : TsMethodCall { + override var dto: StmtDto? = null + override fun toString(): String { return "virtual ${callee.enclosingClass.name}::${callee.name}" } @@ -42,6 +45,8 @@ class TsConcreteMethodCallStmt( override val args: List>, override val returnSite: EtsStmt, ) : TsMethodCall { + override var dto: StmtDto? = null + override fun toString(): String { return "concrete ${callee.signature.enclosingClass.name}::${callee.name}" } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 850f97e9de..1630df62c6 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -37,10 +37,10 @@ import org.usvm.StepScope import org.usvm.UExpr import org.usvm.UInterpreter import org.usvm.UIteExpr +import org.usvm.api.TsTarget import org.usvm.api.evalTypeEquals import org.usvm.api.initializeArray import org.usvm.api.mockMethodCall -import org.usvm.api.targets.TsTarget import org.usvm.api.typeStreamOf import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.forkblacklists.UForkBlackList @@ -100,6 +100,10 @@ class TsInterpreter( val stmt = state.lastStmt val scope = StepScope(state, forkBlackList) + // logger.info { + // "Step ${stmt.location.index} in ${state.lastEnteredMethod.name}: $stmt" + // } + val result = state.methodResult if (result is TsMethodResult.TsException) { // TODO catch processing diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 37034ea083..6a7ee4c796 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -17,9 +17,9 @@ import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort import org.usvm.UState +import org.usvm.api.TsTarget import org.usvm.api.allocateConcreteRef import org.usvm.api.initializeArray -import org.usvm.api.targets.TsTarget import org.usvm.collections.immutable.getOrPut import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap import org.usvm.collections.immutable.internal.MutabilityOwnership diff --git a/usvm-ts/src/test/kotlin/org/usvm/checkers/ReachabilityChecker.kt b/usvm-ts/src/test/kotlin/org/usvm/checkers/ReachabilityChecker.kt index 6193e96512..1aaa8302fe 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/checkers/ReachabilityChecker.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/checkers/ReachabilityChecker.kt @@ -4,8 +4,8 @@ import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.loadEtsFileAutoConvert import org.usvm.PathSelectionStrategy import org.usvm.UMachineOptions -import org.usvm.api.targets.ReachabilityObserver -import org.usvm.api.targets.TsReachabilityTarget +import org.usvm.api.reachability.TsReachabilityObserver +import org.usvm.api.reachability.TsReachabilityTarget import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.util.getResourcePath @@ -28,7 +28,7 @@ class ReachabilityChecker { @Test fun runReachabilityCheck() { - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "simpleFunction" } @@ -51,7 +51,7 @@ class ReachabilityChecker { @Test fun runReachabilityCheckForFirstInstruction() { - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "simpleFunction" } diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/ArrayReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/ArrayReachabilityTest.kt index b710f59e8d..27a0ca9394 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/ArrayReachabilityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/ArrayReachabilityTest.kt @@ -8,17 +8,15 @@ import org.junit.jupiter.api.Disabled import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.UMachineOptions -import org.usvm.api.targets.ReachabilityObserver -import org.usvm.api.targets.TsReachabilityTarget -import org.usvm.api.targets.TsTarget +import org.usvm.api.TsTarget +import org.usvm.api.reachability.TsReachabilityObserver +import org.usvm.api.reachability.TsReachabilityTarget import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.util.getResourcePath import kotlin.test.Test -import kotlin.test.assertEquals import kotlin.test.assertTrue import kotlin.time.Duration -import kotlin.time.Duration.Companion.seconds /** * Tests for array access reachability scenarios. @@ -49,7 +47,7 @@ class ArrayReachabilityTest { @Test fun testSimpleArrayReachable() { // Test reachability through array access: arr[0] === 10 -> arr[1] > 15 -> return 1 - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "simpleArrayReachable" } @@ -86,7 +84,7 @@ class ArrayReachabilityTest { @Test fun testArrayModificationReachable() { // Test reachability after array modification: arr[index] = value -> arr[index] > 10 -> return 1 - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "arrayModificationReachable" } @@ -122,7 +120,7 @@ class ArrayReachabilityTest { @Test fun testArrayBoundsUnreachable() { // Test unreachability due to array element constraints: arr[0] > 20 (when arr[0] = 5) - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "arrayBoundsUnreachable" } @@ -152,7 +150,7 @@ class ArrayReachabilityTest { @Test fun testArraySumReachable() { // Test reachability through array sum calculation: sum === 30 -> arr[0] < arr[1] -> return 1 - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "arraySumReachable" } @@ -189,7 +187,7 @@ class ArrayReachabilityTest { @Test fun testNestedArrayReachable() { // Test reachability through nested array access: matrix[0][0] === 1 -> matrix[1][1] === 4 -> return 1 - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "nestedArrayReachable" } diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/BasicConditionsReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/BasicConditionsReachabilityTest.kt index 6a42c32e87..78716d5439 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/BasicConditionsReachabilityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/BasicConditionsReachabilityTest.kt @@ -7,9 +7,9 @@ import org.jacodb.ets.utils.loadEtsFileAutoConvert import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.UMachineOptions -import org.usvm.api.targets.ReachabilityObserver -import org.usvm.api.targets.TsReachabilityTarget -import org.usvm.api.targets.TsTarget +import org.usvm.api.TsTarget +import org.usvm.api.reachability.TsReachabilityObserver +import org.usvm.api.reachability.TsReachabilityTarget import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.util.getResourcePath @@ -47,7 +47,7 @@ class BasicConditionsReachabilityTest { fun testSimpleReachablePath() { // Test reachability of path: // if (x > 10) -> if (x < 20) -> return 1 - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "simpleReachablePath" } @@ -84,7 +84,7 @@ class BasicConditionsReachabilityTest { fun testSimpleUnreachablePath() { // Test unreachability of contradicting conditions: // if (x > 15) -> if (x < 10) -> return -1 - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "simpleUnreachablePath" } @@ -117,7 +117,7 @@ class BasicConditionsReachabilityTest { fun testMultiVariableReachable() { // Test reachability with multiple variables: // if (x > 0) -> if (y > 5) -> if (x + y > 10) -> return 1 - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "multiVariableReachable" } @@ -158,7 +158,7 @@ class BasicConditionsReachabilityTest { fun testEqualityBasedReachability() { // Test reachability with equality: // if (value === 42) -> if (value > 40) -> if (value < 50) -> return 1 - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "equalityBasedReachability" } @@ -199,7 +199,7 @@ class BasicConditionsReachabilityTest { fun testBooleanUnreachable() { // Test unreachability with contradicting boolean conditions: // if (flag) -> if (!flag) -> return -1 - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "booleanUnreachable" } diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/ComplexReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/ComplexReachabilityTest.kt index a425e4de42..e6a112e47a 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/ComplexReachabilityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/ComplexReachabilityTest.kt @@ -7,9 +7,9 @@ import org.jacodb.ets.utils.loadEtsFileAutoConvert import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.UMachineOptions -import org.usvm.api.targets.ReachabilityObserver -import org.usvm.api.targets.TsReachabilityTarget -import org.usvm.api.targets.TsTarget +import org.usvm.api.TsTarget +import org.usvm.api.reachability.TsReachabilityObserver +import org.usvm.api.reachability.TsReachabilityTarget import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.util.getResourcePath @@ -46,7 +46,7 @@ class ComplexReachabilityTest { @Test fun testArrayObjectCombinedReachable() { // Test reachability combining array and object operations - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "arrayObjectCombinedReachable" } @@ -82,7 +82,7 @@ class ComplexReachabilityTest { @Test fun testMethodArrayManipulationReachable() { // Test reachability through method calls with array manipulation - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "methodArrayManipulationReachable" } @@ -114,7 +114,7 @@ class ComplexReachabilityTest { @Test fun testObjectMethodCallReachable() { // Test reachability through object method calls affecting state - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "objectMethodCallReachable" } @@ -150,7 +150,7 @@ class ComplexReachabilityTest { @Test fun testConditionalObjectReachable() { // Test reachability with conditional object creation and polymorphic method calls - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "conditionalObjectReachable" } @@ -194,7 +194,7 @@ class ComplexReachabilityTest { @Test fun testCrossReferenceReachable() { // Test reachability with cross-referenced objects forming a graph - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "crossReferenceReachable" } diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/FieldAccessReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/FieldAccessReachabilityTest.kt index 49bda77f08..955e8611a5 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/FieldAccessReachabilityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/FieldAccessReachabilityTest.kt @@ -7,9 +7,9 @@ import org.jacodb.ets.utils.loadEtsFileAutoConvert import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.UMachineOptions -import org.usvm.api.targets.ReachabilityObserver -import org.usvm.api.targets.TsReachabilityTarget -import org.usvm.api.targets.TsTarget +import org.usvm.api.TsTarget +import org.usvm.api.reachability.TsReachabilityObserver +import org.usvm.api.reachability.TsReachabilityTarget import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.util.getResourcePath @@ -47,7 +47,7 @@ class FieldAccessReachabilityTest { fun testSimpleFieldReachable() { // Test reachability through field access: // if (this.x > 0) -> if (this.y < 10) -> return 1 - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "simpleFieldReachable" } @@ -84,7 +84,7 @@ class FieldAccessReachabilityTest { fun testFieldModificationReachable() { // Test reachability after field modification: // this.x = value -> if (this.x > 15) -> if (this.x < 25) -> return 1 - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "fieldModificationReachable" } @@ -121,7 +121,7 @@ class FieldAccessReachabilityTest { fun testFieldConstraintUnreachable() { // Test unreachability due to field constraints: // this.x = 10 -> if (this.x > 20) -> return -1 - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "fieldConstraintUnreachable" } @@ -151,7 +151,7 @@ class FieldAccessReachabilityTest { @Test fun testObjectCreationReachable() { // Test reachability through object creation and field access - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "objectCreationReachable" } @@ -187,7 +187,7 @@ class FieldAccessReachabilityTest { @Test fun testAmbiguousFieldAccess() { // Test reachability with ambiguous field access (multiple classes with same field name) - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "ambiguousFieldAccess" } diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt index 0ad63c6702..e3c6c0f3f6 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt @@ -7,9 +7,9 @@ import org.jacodb.ets.utils.loadEtsFileAutoConvert import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.UMachineOptions -import org.usvm.api.targets.ReachabilityObserver -import org.usvm.api.targets.TsReachabilityTarget -import org.usvm.api.targets.TsTarget +import org.usvm.api.TsTarget +import org.usvm.api.reachability.TsReachabilityObserver +import org.usvm.api.reachability.TsReachabilityTarget import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.util.getResourcePath @@ -47,7 +47,7 @@ class FunctionCallReachabilityTest { fun testSimpleCallReachable() { // Test reachability through method call: // this.doubleValue(x) -> result > 20 -> result < 40 -> return 1 - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "simpleCallReachable" } @@ -84,7 +84,7 @@ class FunctionCallReachabilityTest { fun testCallUnreachable() { // Test unreachability due to method return constraints: // constantValue() returns 42 -> result > 100 - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "callUnreachable" } @@ -115,7 +115,7 @@ class FunctionCallReachabilityTest { fun testChainedCallsReachable() { // Test reachability through chained method calls: // addTen(doubleValue(x)) -> result === 30 -> return 1 - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "chainedCallsReachable" } @@ -148,7 +148,7 @@ class FunctionCallReachabilityTest { fun testRecursiveCallReachable() { // Test reachability through recursive call: // factorial(n) -> result === 24 -> return 1 - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "recursiveCallReachable" } @@ -181,7 +181,7 @@ class FunctionCallReachabilityTest { fun testStateModificationReachable() { // Test reachability through state modification: // incrementCounter(counter, 5) -> counter.value === 5 -> counter.value > 3 -> return 1 - val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, options, tsOptions, machineObserver = TsReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } .single { it.name == "stateModificationReachable" } diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt new file mode 100644 index 0000000000..e2822b46af --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt @@ -0,0 +1,443 @@ +package org.usvm.reachability + +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsThrowStmt +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.api.TsTarget +import org.usvm.api.reachability.TsReachabilityObserver +import org.usvm.api.reachability.TsReachabilityTarget +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsState +import java.io.File +import kotlin.time.Duration +import kotlin.time.Duration.Companion.seconds + +/** + * Sample Project Reachability Test + * + * This test serves as a manual entry point to run reachability analysis + * on the sample TypeScript project from IntelliJ IDEA. + * + * To run from IDEA: + * 1. Right-click on this test class + * 2. Select "Run 'SampleProjectTest'" or use Ctrl+Shift+F10 + * 3. View the analysis results in the console output + */ +class SampleProjectTest { + + companion object { + private const val DEBUG = false + + // Common default options for all tests + private val DEFAULT_MACHINE_OPTIONS = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), + exceptionsPropagation = true, + stopOnTargetsReached = false, + timeout = if (DEBUG) Duration.INFINITE else 30.seconds, + stepsFromLastCovered = 1000L, + solverType = SolverType.YICES, + ) + + private val DEFAULT_TS_OPTIONS = TsOptions() + } + + @Test + fun `analyze ProcessManager reachability`() { + println("šŸš€ Starting TypeScript Reachability Analysis on Sample Project") + println("=".repeat(60)) + + val sampleProjectPath = getSampleProjectPath() + println("šŸ“ Project path: $sampleProjectPath") + + // Load TypeScript files + val tsFiles = findTypeScriptFiles(sampleProjectPath) + println("šŸ“„ Found ${tsFiles.size} TypeScript files:") + tsFiles.forEach { println(" - ${it.name}") } + + val scene = EtsScene(tsFiles.map { loadEtsFileAutoConvert(it.toPath()) }) + println("šŸ“Š Loaded scene with ${scene.projectClasses.size} classes") + + // Use default options + val observer = TsReachabilityObserver() + val machine = TsMachine(scene, DEFAULT_MACHINE_OPTIONS, DEFAULT_TS_OPTIONS, machineObserver = observer) + + // Find all methods in the sample project + val allMethods = scene.projectClasses.flatMap { it.methods } + println("šŸ” Found ${allMethods.size} methods to analyze:") + + allMethods.forEach { method -> + println(" - ${method.enclosingClass?.name ?: "Unknown"}.${method.name}") + } + + // Create interesting reachability targets for the system classes + val targets = createSampleTargets(scene) + println( + "šŸŽÆ Created ${targets.size} reachability targets: ${ + targets.count { it.location is EtsThrowStmt } + } throws, ${ + targets.count { it.location is EtsReturnStmt } + } returns, ${ + targets.count { it.location is EtsIfStmt } + } branches" + ) + + // Run the analysis + println("\nāš” Running reachability analysis...") + val results = machine.analyze(allMethods, targets) + + // Process and display results + displayResults(results, targets) + } + + @Test + fun `analyze ProcessManager state transitions`() { + println("šŸŽÆ Focused Analysis: Process State Transitions") + println("=".repeat(50)) + + val sampleProjectPath = getSampleProjectPath() + val tsFiles = findTypeScriptFiles(sampleProjectPath) + val scene = EtsScene(tsFiles.map { loadEtsFileAutoConvert(it.toPath()) }) + + // Find Process class and its state transition methods + val processClass = scene.projectClasses.find { it.name == "Process" } + ?: error("Process class not found") + + val stateTransitionMethods = processClass.methods.filter { method -> + method.name in listOf("start", "pause", "block", "unblock", "terminate") + } + + println("šŸ” Analyzing process state transition methods:") + stateTransitionMethods.forEach { method -> + println(" - ${processClass.name}.${method.name}") + } + + val observer = TsReachabilityObserver() + val machine = TsMachine(scene, DEFAULT_MACHINE_OPTIONS, DEFAULT_TS_OPTIONS, machineObserver = observer) + + // Create specific targets for state transitions + val targets = createStateTransitionTargets(stateTransitionMethods) + println("šŸ“ Created ${targets.size} specific targets for state transitions") + + val results = machine.analyze(stateTransitionMethods, targets) + + displayDetailedResults(results, targets, stateTransitionMethods.first()) + } + + @Test + fun `analyze MemoryManager operations`() { + println("šŸ§® Analysis: Memory Management Operations") + println("=".repeat(50)) + + val sampleProjectPath = getSampleProjectPath() + val tsFiles = findTypeScriptFiles(sampleProjectPath) + val scene = EtsScene(tsFiles.map { loadEtsFileAutoConvert(it.toPath()) }) + + val memoryManagerClass = scene.projectClasses.find { it.name == "MemoryManager" } + ?: error("MemoryManager class not found") + + val memoryMethods = memoryManagerClass.methods.filter { method -> + method.name in listOf("allocateMemory", "freeMemory", "compactMemory", "defragmentMemory") + } + + println("šŸ” Found ${memoryMethods.size} memory management methods:") + memoryMethods.forEach { println(" - ${it.name}") } + + // Override options for memory management analysis + val machineOptions = DEFAULT_MACHINE_OPTIONS.copy( + stepsFromLastCovered = 2000L + ) + + val machine = TsMachine(scene, machineOptions, DEFAULT_TS_OPTIONS, machineObserver = TsReachabilityObserver()) + val targets = createMemoryManagerTargets(memoryManagerClass) + + val results = machine.analyze(memoryMethods, targets) + displayResults(results, targets) + } + + @Test + fun `demonstrate array operations reachability`() { + println("šŸ›¤ļø Demonstration: Array Operations Reachability Analysis") + println("=".repeat(60)) + + val sampleProjectPath = getSampleProjectPath() + val tsFiles = findTypeScriptFiles(sampleProjectPath) + val scene = EtsScene(tsFiles.map { loadEtsFileAutoConvert(it.toPath()) }) + + val processClass = scene.projectClasses.find { it.name == "Process" } + ?: error("Process class not found") + + val arrayMethod = processClass.methods.find { it.name == "addChild" } + ?: error("Array manipulation method not found") + + println("šŸ” Analyzing method: ${processClass.name}.${arrayMethod.name}") + + // Override options for focused array operation analysis + val machineOptions = DEFAULT_MACHINE_OPTIONS.copy( + stepsFromLastCovered = 1000L + ) + + val observer = TsReachabilityObserver() + val machine = TsMachine(scene, machineOptions, DEFAULT_TS_OPTIONS, machineObserver = observer) + + // Create targets for different execution paths in array operations + val targets = createMethodPathTargets(arrayMethod) + println("šŸ“ Created ${targets.size} path targets") + + val results = machine.analyze(listOf(arrayMethod), targets) + + displayPathExtractionResults(results, targets, arrayMethod) + } + + private fun getSampleProjectPath(): File { + // Get the project root directory + val currentDir = File(System.getProperty("user.dir")) + val projectRoot = findProjectRoot(currentDir) + return File(projectRoot, "examples/reachability/sample-project") + } + + private fun findProjectRoot(dir: File): File { + if (File(dir, "LICENSE").exists()) { + return dir + } + val parent = dir.parentFile + if (parent != null && parent != dir) { + return findProjectRoot(parent) + } + error("Could not find project root") + } + + private fun findTypeScriptFiles(projectDir: File): List { + return projectDir.walkTopDown() + .filter { it.isFile && it.extension == "ts" } + .toList() + } + + private fun createSampleTargets(scene: EtsScene): List { + val targets = mutableListOf() + + scene.projectClasses.forEach { clazz -> + clazz.methods.forEach { method -> + method.cfg.stmts.forEach { stmt -> + // Create targets for different types of statements + when (stmt) { + is EtsThrowStmt -> { + targets.add(TsReachabilityTarget.FinalPoint(stmt)) + } + + is EtsReturnStmt -> { + targets.add(TsReachabilityTarget.FinalPoint(stmt)) + } + + is EtsIfStmt -> { + targets.add(TsReachabilityTarget.IntermediatePoint(stmt)) + } + } + } + } + } + + return targets + } + + private fun createStateTransitionTargets(methods: List): List { + val targets = mutableListOf() + + methods.forEach { method -> + method.cfg.stmts.forEach { stmt -> + // Create targets for state transition statements + when { + stmt.toString().contains("start") -> { + targets.add(TsReachabilityTarget.InitialPoint(stmt)) + } + + stmt.toString().contains("terminate") -> { + targets.add(TsReachabilityTarget.FinalPoint(stmt)) + } + + stmt.toString().contains("pause") || stmt.toString().contains("unblock") -> { + targets.add(TsReachabilityTarget.IntermediatePoint(stmt)) + } + } + } + } + + return targets + } + + private fun createMemoryManagerTargets(clazz: org.jacodb.ets.model.EtsClass): List { + val targets = mutableListOf() + + clazz.methods.forEach { method -> + method.cfg.stmts.forEach { stmt -> + if (stmt.toString().contains("return") || stmt.toString().contains("throw")) { + targets.add(TsReachabilityTarget.FinalPoint(stmt)) + } + } + } + + return targets + } + + private fun createMethodPathTargets(method: org.jacodb.ets.model.EtsMethod): List { + val targets = mutableListOf() + val statements = method.cfg.stmts + + if (statements.isNotEmpty()) { + // Add initial point + targets.add(TsReachabilityTarget.InitialPoint(statements.first())) + + // Add intermediate points for interesting statements + statements.drop(1).dropLast(1).forEach { stmt -> + if (stmt.toString().contains("if") || stmt.toString().contains("throw")) { + targets.add(TsReachabilityTarget.IntermediatePoint(stmt)) + } + } + + // Add final point + if (statements.size > 1) { + targets.add(TsReachabilityTarget.FinalPoint(statements.last())) + } + } + + return targets + } + + private fun displayResults(results: List, targets: List) { + println("\nšŸ“Š REACHABILITY ANALYSIS RESULTS") + println("=".repeat(50)) + println("Total states explored: ${results.size}") + println("Total targets defined: ${targets.size}") + + val reachable = mutableListOf() + val unreachable = mutableListOf() + val unknown = mutableListOf() + + // Get all statements that were explored during analysis + val allExploredStatements = results.flatMap { state -> + state.pathNode.allStatements + }.toSet() + + // Analyze which targets were reached + targets.forEach { target -> + val wasReached = results.any { state -> + state.pathNode.allStatements.contains(target.location) + } + + when { + wasReached -> { + reachable.add(target) + } + + // If the statement was explored but never reached as a target, + // it might be unreachable due to path constraints + allExploredStatements.contains(target.location) -> { + unreachable.add(target) + } + + // If the statement was never even explored, it's unknown + else -> { + unknown.add(target) + } + } + } + + println("\nāœ… REACHABLE TARGETS (${reachable.size}):") + reachable.forEach { target -> + println(" āœ“ ${target::class.simpleName}: ${target.location}") + } + + println("\nāŒ UNREACHABLE TARGETS (${unreachable.size}):") + unreachable.forEach { target -> + println(" āœ— ${target::class.simpleName}: ${target.location}") + } + + println("\nā“ UNKNOWN/TIMEOUT TARGETS (${unknown.size}):") + unknown.forEach { target -> + println(" ? ${target::class.simpleName}: ${target.location}") + } + + println("\nšŸ“ˆ SUMMARY:") + println(" Reachable: ${reachable.size}") + println(" Unreachable: ${unreachable.size}") + println(" Unknown: ${unknown.size}") + } + + private fun displayDetailedResults( + results: List, + targets: List, + method: org.jacodb.ets.model.EtsMethod, + ) { + println("\nšŸ” DETAILED ANALYSIS: ${method.name}") + println("=".repeat(60)) + + displayResults(results, targets) + + println("\nšŸ“‹ METHOD STRUCTURE:") + method.cfg.stmts.forEachIndexed { index, stmt -> + println(" ${index + 1}. ${stmt::class.simpleName}: ${stmt.toString().take(80)}...") + } + + if (results.isNotEmpty()) { + println("\nšŸ›¤ļø EXECUTION PATHS FOUND:") + results.take(5).forEachIndexed { index, state -> + println(" Path ${index + 1}: ${state::class.simpleName}") + println(" Statements covered: ${state.pathNode.allStatements.count()}") + } + } + } + + private fun displayPathExtractionResults( + results: List, + targets: List, + method: org.jacodb.ets.model.EtsMethod, + ) { + println("\nšŸ›¤ļø PATH EXTRACTION DEMONSTRATION") + println("=".repeat(50)) + + println("Method: ${method.name}") + println("Total execution states: ${results.size}") + println("Targets analyzed: ${targets.size}") + + if (results.isNotEmpty()) { + println("\nšŸ“ DETAILED PATH ANALYSIS:") + + results.take(3).forEachIndexed { index, state -> + println("\n--- Path ${index + 1} ---") + println("State type: ${state::class.simpleName}") + println("Statements in path: ${state.pathNode.allStatements.count()}") + + // Show the execution path + println("Execution sequence:") + state.pathNode.allStatements.take(10).forEachIndexed { stmtIndex: Int, stmt -> + println(" ${stmtIndex + 1}. ${stmt::class.simpleName}: ${stmt.toString().take(60)}...") + } + + val stmtCount = state.pathNode.allStatements.count() + if (stmtCount > 10) { + println(" ... and ${stmtCount - 10} more statements") + } + + // Check which targets this path reached + val reachedTargets = targets.filter { target -> + state.pathNode.allStatements.contains(target.location) + } + + println("Targets reached in this path: ${reachedTargets.size}") + reachedTargets.forEach { target -> + println(" - ${target::class.simpleName}") + } + } + + if (results.size > 3) { + println("\n... and ${results.size - 3} more execution paths") + } + } + } +}