From 902054e8a979b89c590eb9b3babd59fd2e68beba Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 16 Sep 2025 14:28:02 +0300 Subject: [PATCH 01/18] Draft CLI API for reachability analysis --- examples/reachability/README.md | 227 +++++++ examples/reachability/reachability-cli.sh | 184 ++++++ .../reachability/sample-project/Calculator.ts | 68 ++ .../reachability/sample-project/MathUtils.ts | 47 ++ examples/reachability/targets.jsonc | 26 + usvm-ts/build.gradle.kts | 25 + .../org/usvm/api/targets/dto/Targets.kt | 11 + .../usvm/machine/interpreter/TsInterpreter.kt | 4 + .../org/usvm/reachability/cli/Reachability.kt | 579 ++++++++++++++++++ .../usvm/reachability/SampleProjectTest.kt | 407 ++++++++++++ 10 files changed, 1578 insertions(+) create mode 100644 examples/reachability/README.md create mode 100755 examples/reachability/reachability-cli.sh create mode 100644 examples/reachability/sample-project/Calculator.ts create mode 100644 examples/reachability/sample-project/MathUtils.ts create mode 100644 examples/reachability/targets.jsonc create mode 100644 usvm-ts/src/main/kotlin/org/usvm/api/targets/dto/Targets.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt diff --git a/examples/reachability/README.md b/examples/reachability/README.md new file mode 100644 index 0000000000..de45fdeb48 --- /dev/null +++ b/examples/reachability/README.md @@ -0,0 +1,227 @@ +# šŸŽÆ TypeScript Reachability Analysis CLI + +A powerful command-line tool for performing sophisticated reachability analysis on TypeScript projects using the USVM framework. + +## Features + +- āœ… **REACHABLE**: Paths confirmed to be executable with complete execution traces +- āŒ **UNREACHABLE**: Paths confirmed to be impossible under any conditions +- ā“ **UNKNOWN**: Paths that could not be determined due to timeout, errors, or approximations + +## Installation & Setup + +1. Ensure you have the USVM project built: + +```bash +cd /path/to/usvm +./gradlew build +``` + +2. The CLI is ready to use via the wrapper script or Gradle. + +## Usage + +### Quick Start with Wrapper Script + +```bash +# Analyze a TypeScript project with default settings +./reachability-cli.sh -p ./my-typescript-project + +# Use custom targets and verbose output +./reachability-cli.sh -p ./my-project -t ./targets.jsonc -v + +# Analyze specific methods with detailed statement output +./reachability-cli.sh -p ./project --method Calculator --include-statements +``` + +### Direct Gradle Usage + +```bash +./gradlew :usvm-ts:run --args="--project ./examples/reachability/sample-project --verbose" +``` + +## Command Line Options + +### Required + +- `-p, --project PATH` - Path to TypeScript project directory + +### Optional Analysis Configuration + +- `-t, --targets FILE` - JSON file with target definitions (uses auto-generated targets if not provided) +- `-m, --mode MODE` - Analysis scope: `ALL_METHODS`, `PUBLIC_METHODS`, `ENTRY_POINTS` (default: PUBLIC_METHODS) +- `--method PATTERN` - Filter methods by name pattern + +### Solver & Performance Options + +- `--solver SOLVER` - SMT solver: `YICES`, `Z3`, `CVC5` (default: YICES) +- `--timeout SECONDS` - Overall analysis timeout (default: 300) +- `--steps LIMIT` - Maximum steps from last covered statement (default: 3500) +- `--strategy STRATEGY` - Path selection strategy (default: TARGETED) + +### Output Options + +- `-o, --output DIR` - Output directory (default: ./reachability-results) +- `-v, --verbose` - Enable verbose logging +- `--include-statements` - Include detailed statement information in reports + +## Target Definitions Format + +Create a JSON file to specify custom reachability targets: + +```json +[ + { + "type": "initial", + "method": "Calculator.add", + "statement": 0 + }, + { + "type": "intermediate", + "method": "Calculator.add", + "statement": 1 + }, + { + "type": "final", + "method": "Calculator.add", + "statement": 4 + } +] +``` + +### Target Types + +- **initial**: Entry point of the analysis path +- **intermediate**: Checkpoint along the execution path +- **final**: Target endpoint to reach + +### Hierarchical Structure + +Targets are automatically organized into hierarchical chains per method: +`Initial Point ā†’ Intermediate Point(s) ā†’ Final Point` + +## Output Reports + +The tool generates comprehensive analysis reports: + +### Summary Report (`reachability_summary.txt`) + +- Overall statistics and execution time +- Reachability status counts +- Per-target analysis results + +### Detailed Report (`reachability_detailed.md`) + +- Markdown-formatted comprehensive analysis +- Method-by-method breakdown +- Execution paths with statements (when `--include-statements` is used) + +## Example Project Structure + +``` +my-typescript-project/ +ā”œā”€ā”€ Calculator.ts # TypeScript source files +ā”œā”€ā”€ MathUtils.ts +ā””ā”€ā”€ ... + +targets.jsonc # Optional target definitions +reachability-results/ # Generated output directory +ā”œā”€ā”€ reachability_summary.txt +ā””ā”€ā”€ reachability_detailed.md +``` + +## Reachability Analysis Results + +### Status Categories + +1. **REACHABLE** āœ… + - Path is definitely executable + - Includes complete execution trace with all statements + - Shows path conditions and variable states + +2. **UNREACHABLE** āŒ + - Path is proven to be impossible + - No valid execution can reach this target + - Useful for dead code detection + +3. **UNKNOWN** ā“ + - Analysis couldn't determine reachability + - Common causes: timeout, solver limitations, complex approximations + - Requires further investigation or different analysis parameters + +### Execution Paths + +For REACHABLE targets, the tool provides: + +- Complete statement sequence from execution start to target +- All intermediate statements traversed +- Path conditions (when available) +- Variable state information + +## Example Usage Scenarios + +### 1. Dead Code Detection + +```bash +./reachability-cli.sh -p ./src --mode ALL_METHODS -v +``` + +### 2. Critical Path Analysis + +```bash +./reachability-cli.sh -p ./src -t ./critical-paths.json --include-statements +``` + +### 3. Method-Specific Analysis + +```bash +./reachability-cli.sh -p ./src --method "authenticate" --solver Z3 +``` + +### 4. High-Precision Analysis + +```bash +./reachability-cli.sh -p ./src --timeout 600 --steps 10000 --solver CVC5 +``` + +## Implementation Details + +The CLI leverages the USVM framework's powerful reachability analysis capabilities: + +- **Project Loading**: Uses `loadEtsFileAutoConvert()` for automatic TypeScript to IR conversion +- **Target Creation**: Builds hierarchical target structures using `TsReachabilityTarget` classes +- **Analysis Engine**: Utilizes `TsMachine` with configurable solver backends +- **Path Extraction**: Extracts execution paths from `TsState.pathNode.allStatements` + +## Troubleshooting + +### Common Issues + +1. **"No TypeScript files found"** + - Ensure the project path contains `.ts` or `.js` files + - Check file permissions + +2. **"Analysis timeout"** + - Increase `--timeout` value + - Reduce `--steps` limit + - Try different `--solver` + +3. **"Target not found"** + - Verify method names in targets.jsonc match exactly + - Check statement indices are within bounds + +### Debug Mode + +Enable verbose output with `-v` to see detailed analysis progress and any warnings. + +## Contributing + +The CLI is part of the USVM project. To extend functionality: + +1. Add new options to `ReachabilityAnalyzer` class +2. Update the wrapper script with corresponding parameters +3. Add appropriate documentation + +## License + +This tool is part of the USVM project and follows the same licensing terms. diff --git a/examples/reachability/reachability-cli.sh b/examples/reachability/reachability-cli.sh new file mode 100755 index 0000000000..a1ac9b000f --- /dev/null +++ b/examples/reachability/reachability-cli.sh @@ -0,0 +1,184 @@ +#!/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 + +# 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 " -v, --verbose Enable verbose output" + echo " --include-statements Include statement details in output" + echo " -h, --help Show this help message" + echo "" + echo "Examples:" + echo " # Analyze all public methods in a project" + echo " $0 -p ./my-typescript-project" + echo "" + echo " # Use custom targets and verbose output" + echo " $0 -p ./my-project -t ./targets.jsonc -v" + echo "" + echo " # Analyze specific methods with detailed output" + echo " $0 -p ./project --method Calculator --include-statements" +} + +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 + ;; + -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 + +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 + +echo -e "${BLUE}šŸš€ Starting TypeScript Reachability Analysis${NC}" +echo "šŸ“ Project: $PROJECT_PATH" +echo "šŸ“„ Output: $OUTPUT_DIR" +echo "šŸ” Mode: $MODE" +echo "āš™ļø Solver: $SOLVER" + +# Path to the shadow JAR +SHADOW_JAR="$USVM_ROOT/usvm-ts/build/libs/usvm-ts-reachability.jar" + +# Check if shadow JAR exists +if [[ ! -f "$SHADOW_JAR" ]]; then + echo -e "${RED}āŒ Error: Shadow JAR not found at $SHADOW_JAR${NC}" + echo "Please run the following commands first:" + echo " cd $USVM_ROOT" + echo " ./gradlew :usvm-ts:shadowJar" + exit 1 +fi + +# Build the Java command arguments +JAVA_ARGS=() +JAVA_ARGS+=("--project" "$PROJECT_PATH") +JAVA_ARGS+=("--output" "$OUTPUT_DIR") +JAVA_ARGS+=("--mode" "$MODE") +JAVA_ARGS+=("--solver" "$SOLVER") +JAVA_ARGS+=("--timeout" "$TIMEOUT") +JAVA_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 + JAVA_ARGS+=("--targets" "$TARGETS_FILE") + echo "šŸ“‹ Targets: $TARGETS_FILE" +fi + +if [[ -n "$METHOD_FILTER" ]]; then + JAVA_ARGS+=("--method" "$METHOD_FILTER") + echo "šŸŽÆ Method filter: $METHOD_FILTER" +fi + +if [[ "$VERBOSE" == true ]]; then + JAVA_ARGS+=("--verbose") + echo "šŸ“ Verbose mode enabled" +fi + +if [[ "$INCLUDE_STATEMENTS" == true ]]; then + JAVA_ARGS+=("--include-statements") + echo "šŸ“ Including statement details" +fi + +echo "" +echo -e "${YELLOW}āš” Running analysis...${NC}" + +# Execute the JAR directly +echo -e "ARGS: ${JAVA_ARGS[*]}" +java -Dfile.encoding=UTF-8 -Dsun.stdout.encoding=UTF-8 -jar "$SHADOW_JAR" "${JAVA_ARGS[@]}" + +echo "" +echo -e "${GREEN}āœ… Analysis complete! Check the results in: $OUTPUT_DIR${NC}" diff --git a/examples/reachability/sample-project/Calculator.ts b/examples/reachability/sample-project/Calculator.ts new file mode 100644 index 0000000000..91acbec330 --- /dev/null +++ b/examples/reachability/sample-project/Calculator.ts @@ -0,0 +1,68 @@ +// Sample TypeScript project for reachability analysis +export class Calculator { + private value: number = 0; + + constructor(initialValue: number = 0) { + this.value = initialValue; + } + + public add(num: number): Calculator { + if (num < 0) { + throw new Error("Negative numbers not allowed"); + } + this.value += num; + return this; + } + + public subtract(num: number): Calculator { + this.value -= num; + return this; + } + + public multiply(num: number): Calculator { + if (num === 0) { + this.value = 0; + return this; + } + this.value *= num; + return this; + } + + public divide(num: number): Calculator { + if (num === 0) { + throw new Error("Division by zero"); + } + this.value /= num; + return this; + } + + public getValue(): number { + return this.value; + } + + public reset(): Calculator { + this.value = 0; + return this; + } + + // Method with complex control flow for testing + public complexOperation(a: number, b: number, c: number): number { + if (a > 0) { + if (b > 0) { + if (c > 0) { + return a + b + c; // Target: reachable path + } else { + return a + b - c; // Target: reachable path + } + } else { + return a - b; // Target: reachable path + } + } else { + if (b === 0 && c === 0) { + return 0; // Target: hard to reach path + } else { + return -1; // Target: unreachable in some contexts + } + } + } +} diff --git a/examples/reachability/sample-project/MathUtils.ts b/examples/reachability/sample-project/MathUtils.ts new file mode 100644 index 0000000000..41e1721423 --- /dev/null +++ b/examples/reachability/sample-project/MathUtils.ts @@ -0,0 +1,47 @@ +export class MathUtils { + public static factorial(n: number): number { + if (n < 0) { + throw new Error("Factorial of negative number"); + } + if (n === 0 || n === 1) { + return 1; + } + return n * MathUtils.factorial(n - 1); + } + + public static fibonacci(n: number): number { + if (n < 0) { + return -1; // Error case + } + if (n <= 1) { + return n; + } + return MathUtils.fibonacci(n - 1) + MathUtils.fibonacci(n - 2); + } + + public static isPrime(num: number): boolean { + if (num <= 1) { + return false; + } + if (num === 2) { + return true; + } + if (num % 2 === 0) { + return false; // Even numbers > 2 are not prime + } + + for (let i = 3; i * i <= num; i += 2) { + if (num % i === 0) { + return false; // Found a divisor + } + } + return true; // Prime number + } + + public static gcd(a: number, b: number): number { + if (b === 0) { + return a; // Base case for recursion + } + return MathUtils.gcd(b, a % b); + } +} diff --git a/examples/reachability/targets.jsonc b/examples/reachability/targets.jsonc new file mode 100644 index 0000000000..c349264ecb --- /dev/null +++ b/examples/reachability/targets.jsonc @@ -0,0 +1,26 @@ +[ + // Calculator class targets + {"type": "initial", "method": "Calculator.add", "statement": 0}, + {"type": "intermediate", "method": "Calculator.add", "statement": 1}, + {"type": "final", "method": "Calculator.add", "statement": 4}, + + {"type": "initial", "method": "Calculator.divide", "statement": 0}, + {"type": "intermediate", "method": "Calculator.divide", "statement": 1}, + {"type": "final", "method": "Calculator.divide", "statement": 4}, + + // Complex operation with multiple paths + {"type": "initial", "method": "Calculator.complexOperation", "statement": 0}, + {"type": "intermediate", "method": "Calculator.complexOperation", "statement": 2}, + {"type": "intermediate", "method": "Calculator.complexOperation", "statement": 4}, + {"type": "final", "method": "Calculator.complexOperation", "statement": 6}, + + // MathUtils targets + {"type": "initial", "method": "MathUtils.factorial", "statement": 0}, + {"type": "intermediate", "method": "MathUtils.factorial", "statement": 3}, + {"type": "final", "method": "MathUtils.factorial", "statement": 6}, + + {"type": "initial", "method": "MathUtils.isPrime", "statement": 0}, + {"type": "intermediate", "method": "MathUtils.isPrime", "statement": 5}, + {"type": "intermediate", "method": "MathUtils.isPrime", "statement": 8}, + {"type": "final", "method": "MathUtils.isPrime", "statement": 12} +] diff --git a/usvm-ts/build.gradle.kts b/usvm-ts/build.gradle.kts index 96de26034a..67154f5343 100644 --- a/usvm-ts/build.gradle.kts +++ b/usvm-ts/build.gradle.kts @@ -8,6 +8,8 @@ import kotlin.time.Duration plugins { id("usvm.kotlin-conventions") + application + id(Plugins.Shadow) } dependencies { @@ -16,6 +18,7 @@ dependencies { implementation(Libs.jacodb_core) implementation(Libs.jacodb_ets) + implementation(Libs.clikt) implementation(Libs.ksmt_yices) implementation(Libs.ksmt_cvc5) @@ -32,6 +35,28 @@ dependencies { testImplementation("org.burningwave:core:12.62.7") } +application { + mainClass = "org.usvm.reachability.cli.ReachabilityKt" + applicationDefaultJvmArgs = listOf("-Dfile.encoding=UTF-8", "-Dsun.stdout.encoding=UTF-8") +} + +tasks.startScripts { + applicationName = "usvm-ts-reachability" +} + +tasks.shadowJar { + archiveBaseName.set("usvm-ts-reachability") + 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/targets/dto/Targets.kt b/usvm-ts/src/main/kotlin/org/usvm/api/targets/dto/Targets.kt new file mode 100644 index 0000000000..d614f37a72 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/api/targets/dto/Targets.kt @@ -0,0 +1,11 @@ +package org.usvm.api.targets.dto + +import org.jacodb.ets.dto.StmtDto + +sealed interface TargetDto { + val location: StmtDto + + class InitialPoint(override val location: StmtDto) : TargetDto + class IntermediatePoint(override val location: StmtDto) : TargetDto + class FinalPoint(override val location: StmtDto) : TargetDto +} 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..0e3b2f9496 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 @@ -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/reachability/cli/Reachability.kt b/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt new file mode 100644 index 0000000000..a48ea50346 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt @@ -0,0 +1,579 @@ +package org.usvm.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 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.targets.ReachabilityObserver +import org.usvm.api.targets.TsReachabilityTarget +import org.usvm.api.targets.TsTarget +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) + + private val pathStrategy by option( + "--strategy", + help = "šŸ›¤ļø Path selection strategy" + ).enum().default(PathSelectionStrategy.TARGETED) + + // 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 + } + } + + 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(pathStrategy), + 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 = ReachabilityObserver()) + + // Find methods to analyze + val methodsToAnalyze = findMethodsToAnalyze(scene) + echo("šŸŽÆ Analyzing ${methodsToAnalyze.size} methods") + + // Create targets + val targetDefinitions = if (targetsFile != null) { + parseTargetDefinitions(targetsFile!!) + } else { + generateDefaultTargets(methodsToAnalyze) + } + + val targets = createTargets(methodsToAnalyze, targetDefinitions) + echo("šŸ“ Created ${targets.size} reachability 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, + targetDefinitions = targetDefinitions, + 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 { + // Simple JSON parsing for target definitions + // Expected format: [{"type": "initial|intermediate|final", "method": "ClassName.methodName", "statement": index}] + val lines = content.lines() + .map { it.trim() } + .filter { it.isNotEmpty() && !it.startsWith("//") && !it.startsWith("[") && !it.startsWith("]") } + .filter { it.contains("\"type\"") } + + lines.mapNotNull { line -> + try { + val typeMatch = Regex("\"type\"\\s*:\\s*\"(\\w+)\"").find(line) + val methodMatch = Regex("\"method\"\\s*:\\s*\"([^\"]+)\"").find(line) + val statementMatch = Regex("\"statement\"\\s*:\\s*(\\d+)").find(line) + + if (typeMatch != null && methodMatch != null && statementMatch != null) { + val type = when (typeMatch.groupValues[1].lowercase()) { + "initial" -> TargetType.INITIAL + "intermediate" -> TargetType.INTERMEDIATE + "final" -> TargetType.FINAL + else -> return@mapNotNull null + } + + TargetDefinition( + type = type, + methodName = methodMatch.groupValues[1], + statementIndex = statementMatch.groupValues[1].toInt() + ) + } else null + } catch (_: Exception) { + echo("āš ļø Warning: Could not parse target definition: $line", err = true) + null + } + } + } catch (_: Exception) { + echo("āŒ Error parsing targets file", err = true) + emptyList() + } + } + + private fun generateDefaultTargets(methods: List): List { + return methods.flatMap { method -> + val statements = method.cfg.stmts + if (statements.isEmpty()) return@flatMap emptyList() + + val targets = mutableListOf() + + // Initial point + targets.add( + TargetDefinition( + type = TargetType.INITIAL, + methodName = "${method.enclosingClass?.name ?: "Unknown"}.${method.name}", + statementIndex = 0 + ) + ) + + // Intermediate points for control flow statements + statements.forEachIndexed { index, stmt -> + when (stmt) { + is EtsIfStmt, is EtsReturnStmt -> { + targets.add( + TargetDefinition( + type = if (stmt == statements.last()) TargetType.FINAL else TargetType.INTERMEDIATE, + methodName = "${method.enclosingClass?.name ?: "Unknown"}.${method.name}", + statementIndex = index + ) + ) + } + } + } + + targets + } + } + + private fun createTargets(methods: List, targetDefs: List): List { + val targets = mutableListOf() + val methodMap = methods.associateBy { "${it.enclosingClass?.name ?: "Unknown"}.${it.name}" } + + // Group targets by method to build hierarchical structure + val targetsByMethod = targetDefs.groupBy { it.methodName } + + targetsByMethod.forEach { (methodName, methodTargets) -> + val method = methodMap[methodName] ?: return@forEach + val statements = method.cfg.stmts + + if (statements.isEmpty()) return@forEach + + // Find initial target + val initialTarget = methodTargets.find { it.type == TargetType.INITIAL } + ?.let { targetDef -> + if (targetDef.statementIndex < statements.size) { + TsReachabilityTarget.InitialPoint(statements[targetDef.statementIndex]) + } else null + } ?: return@forEach + + targets.add(initialTarget) + + // Build chain of intermediate and final targets + var currentTarget: TsTarget = initialTarget + methodTargets.filter { it.type != TargetType.INITIAL } + .sortedBy { it.statementIndex } + .forEach { targetDef -> + if (targetDef.statementIndex < statements.size) { + val stmt = statements[targetDef.statementIndex] + val target = when (targetDef.type) { + TargetType.INTERMEDIATE -> TsReachabilityTarget.IntermediatePoint(stmt) + TargetType.FINAL -> TsReachabilityTarget.FinalPoint(stmt) + else -> return@forEach + } + currentTarget = currentTarget.addChild(target) + } + } + } + + return targets + } + + 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(), + pathConditions = emptyList() // TODO: Extract path conditions + ) + } + } 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("."))}") + } +} + +// Enums and data classes +enum class AnalysisMode { + ALL_METHODS, + PUBLIC_METHODS, + ENTRY_POINTS +} + +enum class TargetType { + INITIAL, + INTERMEDIATE, + FINAL +} + +enum class ReachabilityStatus { + REACHABLE, // Confirmed reachable with execution path + UNREACHABLE, // Confirmed unreachable + UNKNOWN // Could not determine (timeout/approximation/error) +} + +data class TargetDefinition( + val type: TargetType, + val methodName: String, + val statementIndex: Int, +) + +data class ExecutionPath( + val statements: List, + val pathConditions: List, // Simplified - would contain actual conditions +) + +data class TargetReachabilityResult( + val target: TsTarget, + val status: ReachabilityStatus, + val executionPaths: List, +) + +data class ReachabilityResults( + val methods: List, + val targets: List, + val targetDefinitions: List, + val states: List, + val reachabilityResults: List, + val scene: EtsScene, +) + +fun main(args: Array) { + ReachabilityAnalyzer().main(args) +} 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..22c2412c6a --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt @@ -0,0 +1,407 @@ +package org.usvm.reachability + +import org.jacodb.ets.model.EtsScene +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.targets.ReachabilityObserver +import org.usvm.api.targets.TsReachabilityTarget +import org.usvm.api.targets.TsTarget +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 { + + @Test + fun `analyze Calculator class reachability`() { + println("šŸš€ Starting TypeScript Reachability Analysis on Sample Project") + println("=" + "=".repeat(59)) + + 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") + + // Configure analysis options + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), + exceptionsPropagation = true, + stopOnTargetsReached = false, // Continue to find all paths + timeout = Duration.INFINITE, + stepsFromLastCovered = 3500L, + solverType = SolverType.YICES, + ) + + val tsOptions = TsOptions() + val observer = ReachabilityObserver() + val machine = TsMachine(scene, machineOptions, tsOptions, 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 Calculator class + val targets = createSampleTargets(scene) + println("šŸŽÆ Created ${targets.size} reachability targets") + + // Run the analysis + println("\nāš” Running reachability analysis...") + val results = machine.analyze(allMethods, targets) + + // Process and display results + displayResults(results, targets) + } + + @Test + fun `analyze specific Calculator methods`() { + println("šŸŽÆ Focused Analysis: Calculator Complex Operations") + println("=" + "=".repeat(49)) + + val sampleProjectPath = getSampleProjectPath() + val tsFiles = findTypeScriptFiles(sampleProjectPath) + val scene = EtsScene(tsFiles.map { loadEtsFileAutoConvert(it.toPath()) }) + + // Find Calculator class and its complexOperation method + val calculatorClass = scene.projectClasses.find { it.name.contains("Calculator") } + ?: throw IllegalStateException("Calculator class not found") + + val complexOperationMethod = calculatorClass.methods + .find { it.name == "complexOperation" } + ?: throw IllegalStateException("complexOperation method not found") + + println("šŸ” Analyzing: ${calculatorClass.name}.${complexOperationMethod.name}") + + // Configure for detailed analysis + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), + exceptionsPropagation = true, + stopOnTargetsReached = false, + timeout = Duration.INFINITE, + stepsFromLastCovered = 5000L, + solverType = SolverType.YICES, + ) + + val observer = ReachabilityObserver() + val machine = TsMachine(scene, machineOptions, TsOptions(), machineObserver = observer) + + // Create specific targets for different branches in complexOperation + val targets = createComplexOperationTargets(complexOperationMethod) + println("šŸ“ Created ${targets.size} specific targets for complex operation branches") + + val results = machine.analyze(listOf(complexOperationMethod), targets) + + displayDetailedResults(results, targets, complexOperationMethod) + } + + @Test + fun `analyze MathUtils static methods`() { + println("šŸ§® Analysis: MathUtils Static Methods") + println("=" + "=".repeat(44)) + + val sampleProjectPath = getSampleProjectPath() + val tsFiles = findTypeScriptFiles(sampleProjectPath) + val scene = EtsScene(tsFiles.map { loadEtsFileAutoConvert(it.toPath()) }) + + val mathUtilsClass = scene.projectClasses.find { it.name.contains("MathUtils") } + ?: throw IllegalStateException("MathUtils class not found") + + val staticMethods = mathUtilsClass.methods.filter { it.isStatic } + println("šŸ” Found ${staticMethods.size} static methods:") + staticMethods.forEach { println(" - ${it.name}") } + + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), + timeout = Duration.INFINITE, + stepsFromLastCovered = 2000L, + solverType = SolverType.Z3, + ) + + val machine = TsMachine(scene, machineOptions, TsOptions(), machineObserver = ReachabilityObserver()) + val targets = createMathUtilsTargets(mathUtilsClass).filter { it.location!!.location.method.name == "gcd" } + + val results = machine.analyze(staticMethods, targets) + displayResults(results, targets) + } + + @Test + fun `demonstrate path extraction from reachability results`() { + println("šŸ›¤ļø Demonstration: Path Extraction from Reachability Analysis") + println("=" + "=".repeat(58)) + + val sampleProjectPath = getSampleProjectPath() + val tsFiles = findTypeScriptFiles(sampleProjectPath) + val scene = EtsScene(tsFiles.map { loadEtsFileAutoConvert(it.toPath()) }) + + val calculatorClass = scene.projectClasses.find { it.name.contains("Calculator") } + ?: throw IllegalStateException("Calculator class not found") + + val addMethod = calculatorClass.methods.find { it.name == "add" } + ?: throw IllegalStateException("add method not found") + + println("šŸ” Analyzing method: ${calculatorClass.name}.${addMethod.name}") + + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), + exceptionsPropagation = true, + stopOnTargetsReached = false, + timeout = Duration.INFINITE, + stepsFromLastCovered = 1000L, + solverType = SolverType.YICES, + ) + + val observer = ReachabilityObserver() + val machine = TsMachine(scene, machineOptions, TsOptions(), machineObserver = observer) + + // Create targets for different execution paths in the add method + val targets = createMethodPathTargets(addMethod) + println("šŸ“ Created ${targets.size} path targets") + + val results = machine.analyze(listOf(addMethod), targets) + + displayPathExtractionResults(results, targets, addMethod) + } + + 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) + } + throw IllegalStateException("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.toString().contains("throw") -> { + targets.add(TsReachabilityTarget.FinalPoint(stmt)) + } + stmt.toString().contains("return") -> { + targets.add(TsReachabilityTarget.FinalPoint(stmt)) + } + stmt.toString().contains("if") -> { + targets.add(TsReachabilityTarget.IntermediatePoint(stmt)) + } + } + } + } + } + + return targets + } + + private fun createComplexOperationTargets(method: org.jacodb.ets.model.EtsMethod): List { + val targets = mutableListOf() + val statements = method.cfg.stmts + + statements.forEachIndexed { index, stmt -> + when (index) { + 0 -> targets.add(TsReachabilityTarget.InitialPoint(stmt)) + statements.size - 1 -> targets.add(TsReachabilityTarget.FinalPoint(stmt)) + else -> targets.add(TsReachabilityTarget.IntermediatePoint(stmt)) + } + } + + return targets + } + + private fun createMathUtilsTargets(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(49)) + println("Total states explored: ${results.size}") + println("Total targets defined: ${targets.size}") + + val reachable = mutableListOf() + val unreachable = mutableListOf() + val unknown = mutableListOf() + + // Analyze which targets were reached + targets.forEach { target -> + val wasReached = results.any { state -> + state.pathNode.allStatements.contains(target.location) + } + + when { + wasReached -> reachable.add(target) + else -> unknown.add(target) // For this demo, we'll mark others as unknown + } + } + + 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(59)) + + 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(49)) + + 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") + } + } + } +} From 01cdf55110f5bf397c597dfeb3ba935d720ad323 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 16 Sep 2025 15:50:56 +0300 Subject: [PATCH 02/18] Replace sample project --- examples/reachability/README.md | 50 ++- examples/reachability/reachability-cli.sh | 9 +- .../reachability/sample-project/Calculator.ts | 68 ---- .../reachability/sample-project/FileSystem.ts | 317 +++++++++++++++++ .../reachability/sample-project/MathUtils.ts | 47 --- .../sample-project/MemoryManager.ts | 291 ++++++++++++++++ .../sample-project/ProcessManager.ts | 327 ++++++++++++++++++ .../usvm/machine/interpreter/TsInterpreter.kt | 6 +- .../usvm/reachability/SampleProjectTest.kt | 197 ++++++----- 9 files changed, 1096 insertions(+), 216 deletions(-) delete mode 100644 examples/reachability/sample-project/Calculator.ts create mode 100644 examples/reachability/sample-project/FileSystem.ts delete mode 100644 examples/reachability/sample-project/MathUtils.ts create mode 100644 examples/reachability/sample-project/MemoryManager.ts create mode 100644 examples/reachability/sample-project/ProcessManager.ts diff --git a/examples/reachability/README.md b/examples/reachability/README.md index de45fdeb48..74d5989938 100644 --- a/examples/reachability/README.md +++ b/examples/reachability/README.md @@ -8,6 +8,22 @@ A powerful command-line tool for performing sophisticated reachability analysis - āŒ **UNREACHABLE**: Paths confirmed to be impossible under any conditions - ā“ **UNKNOWN**: Paths that could not be determined due to timeout, errors, or approximations +## Sample Project + +The included sample project demonstrates a **System Applications** simulator with: + +- **ProcessManager.ts**: Process management with state transitions (CREATED ā†’ READY ā†’ RUNNING ā†’ BLOCKED/TERMINATED) +- **MemoryManager.ts**: Memory allocation, deallocation, compaction, and defragmentation +- **FileSystem.ts**: Basic file system operations and navigation + +These examples use only SMT-solver friendly constructs: + +- Integer operations (no floating-point or modulo operations) +- Array operations (length, indexing, push/pop) +- Object field access and updates +- Conditional logic and control flow +- Function calls without complex inheritance + ## Installation & Setup 1. Ensure you have the USVM project built: @@ -17,27 +33,43 @@ cd /path/to/usvm ./gradlew build ``` -2. The CLI is ready to use via the wrapper script or Gradle. +2. Build the shadow JAR for faster execution: + +```bash +./gradlew :usvm-ts:shadowJar +``` + +3. The CLI is ready to use via the wrapper script or direct JAR execution. ## Usage -### Quick Start with Wrapper Script +### Quick Start with Sample Project + +```bash +# Analyze the sample system applications project +./reachability-cli.sh -p ./sample-project + +# Analyze specific process management methods +./reachability-cli.sh -p ./sample-project --method Process --include-statements + +# Focus on memory management operations with verbose output +./reachability-cli.sh -p ./sample-project --method MemoryManager -v +``` + +### Analyze Your Own Project ```bash -# Analyze a TypeScript project with default settings +# Analyze any TypeScript project with default settings ./reachability-cli.sh -p ./my-typescript-project # Use custom targets and verbose output -./reachability-cli.sh -p ./my-project -t ./targets.jsonc -v - -# Analyze specific methods with detailed statement output -./reachability-cli.sh -p ./project --method Calculator --include-statements +./reachability-cli.sh -p ./my-project -t ./targets.json -v ``` -### Direct Gradle Usage +### Direct JAR Execution (Faster) ```bash -./gradlew :usvm-ts:run --args="--project ./examples/reachability/sample-project --verbose" +java -jar usvm-ts/build/libs/usvm-ts-reachability.jar --project ./sample-project --verbose ``` ## Command Line Options diff --git a/examples/reachability/reachability-cli.sh b/examples/reachability/reachability-cli.sh index a1ac9b000f..6ac87784c4 100755 --- a/examples/reachability/reachability-cli.sh +++ b/examples/reachability/reachability-cli.sh @@ -47,14 +47,17 @@ usage() { echo " -h, --help Show this help message" echo "" echo "Examples:" - echo " # Analyze all public methods in a project" + echo " # Analyze all public methods in a TypeScript project" echo " $0 -p ./my-typescript-project" echo "" + echo " # Analyze the sample system applications project" + echo " $0 -p ../examples/reachability/sample-project" + echo "" echo " # Use custom targets and verbose output" - echo " $0 -p ./my-project -t ./targets.jsonc -v" + echo " $0 -p ./my-project -t ./targets.json -v" echo "" echo " # Analyze specific methods with detailed output" - echo " $0 -p ./project --method Calculator --include-statements" + echo " $0 -p ./project --method ProcessManager --include-statements" } while [[ $# -gt 0 ]]; do diff --git a/examples/reachability/sample-project/Calculator.ts b/examples/reachability/sample-project/Calculator.ts deleted file mode 100644 index 91acbec330..0000000000 --- a/examples/reachability/sample-project/Calculator.ts +++ /dev/null @@ -1,68 +0,0 @@ -// Sample TypeScript project for reachability analysis -export class Calculator { - private value: number = 0; - - constructor(initialValue: number = 0) { - this.value = initialValue; - } - - public add(num: number): Calculator { - if (num < 0) { - throw new Error("Negative numbers not allowed"); - } - this.value += num; - return this; - } - - public subtract(num: number): Calculator { - this.value -= num; - return this; - } - - public multiply(num: number): Calculator { - if (num === 0) { - this.value = 0; - return this; - } - this.value *= num; - return this; - } - - public divide(num: number): Calculator { - if (num === 0) { - throw new Error("Division by zero"); - } - this.value /= num; - return this; - } - - public getValue(): number { - return this.value; - } - - public reset(): Calculator { - this.value = 0; - return this; - } - - // Method with complex control flow for testing - public complexOperation(a: number, b: number, c: number): number { - if (a > 0) { - if (b > 0) { - if (c > 0) { - return a + b + c; // Target: reachable path - } else { - return a + b - c; // Target: reachable path - } - } else { - return a - b; // Target: reachable path - } - } else { - if (b === 0 && c === 0) { - return 0; // Target: hard to reach path - } else { - return -1; // Target: unreachable in some contexts - } - } - } -} 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/MathUtils.ts b/examples/reachability/sample-project/MathUtils.ts deleted file mode 100644 index 41e1721423..0000000000 --- a/examples/reachability/sample-project/MathUtils.ts +++ /dev/null @@ -1,47 +0,0 @@ -export class MathUtils { - public static factorial(n: number): number { - if (n < 0) { - throw new Error("Factorial of negative number"); - } - if (n === 0 || n === 1) { - return 1; - } - return n * MathUtils.factorial(n - 1); - } - - public static fibonacci(n: number): number { - if (n < 0) { - return -1; // Error case - } - if (n <= 1) { - return n; - } - return MathUtils.fibonacci(n - 1) + MathUtils.fibonacci(n - 2); - } - - public static isPrime(num: number): boolean { - if (num <= 1) { - return false; - } - if (num === 2) { - return true; - } - if (num % 2 === 0) { - return false; // Even numbers > 2 are not prime - } - - for (let i = 3; i * i <= num; i += 2) { - if (num % i === 0) { - return false; // Found a divisor - } - } - return true; // Prime number - } - - public static gcd(a: number, b: number): number { - if (b === 0) { - return a; // Base case for recursion - } - return MathUtils.gcd(b, a % b); - } -} 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/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 0e3b2f9496..3babb464da 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 @@ -100,9 +100,9 @@ class TsInterpreter( val stmt = state.lastStmt val scope = StepScope(state, forkBlackList) - logger.info { - "Step ${stmt.location.index} in ${state.lastEnteredMethod.name}: $stmt" - } + // logger.info { + // "Step ${stmt.location.index} in ${state.lastEnteredMethod.name}: $stmt" + // } val result = state.methodResult if (result is TsMethodResult.TsException) { diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt index 22c2412c6a..04c17acccc 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt @@ -29,8 +29,24 @@ import kotlin.time.Duration.Companion.seconds */ 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 60.seconds, + stepsFromLastCovered = 1000L, + solverType = SolverType.YICES, + ) + + private val DEFAULT_TS_OPTIONS = TsOptions() + } + @Test - fun `analyze Calculator class reachability`() { + fun `analyze ProcessManager reachability`() { println("šŸš€ Starting TypeScript Reachability Analysis on Sample Project") println("=" + "=".repeat(59)) @@ -45,19 +61,9 @@ class SampleProjectTest { val scene = EtsScene(tsFiles.map { loadEtsFileAutoConvert(it.toPath()) }) println("šŸ“Š Loaded scene with ${scene.projectClasses.size} classes") - // Configure analysis options - val machineOptions = UMachineOptions( - pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), - exceptionsPropagation = true, - stopOnTargetsReached = false, // Continue to find all paths - timeout = Duration.INFINITE, - stepsFromLastCovered = 3500L, - solverType = SolverType.YICES, - ) - - val tsOptions = TsOptions() + // Use default options val observer = ReachabilityObserver() - val machine = TsMachine(scene, machineOptions, tsOptions, machineObserver = observer) + 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 } @@ -67,7 +73,7 @@ class SampleProjectTest { println(" - ${method.enclosingClass?.name ?: "Unknown"}.${method.name}") } - // Create interesting reachability targets for the Calculator class + // Create interesting reachability targets for the system classes val targets = createSampleTargets(scene) println("šŸŽÆ Created ${targets.size} reachability targets") @@ -80,112 +86,102 @@ class SampleProjectTest { } @Test - fun `analyze specific Calculator methods`() { - println("šŸŽÆ Focused Analysis: Calculator Complex Operations") + fun `analyze ProcessManager state transitions`() { + println("šŸŽÆ Focused Analysis: Process State Transitions") println("=" + "=".repeat(49)) val sampleProjectPath = getSampleProjectPath() val tsFiles = findTypeScriptFiles(sampleProjectPath) val scene = EtsScene(tsFiles.map { loadEtsFileAutoConvert(it.toPath()) }) - // Find Calculator class and its complexOperation method - val calculatorClass = scene.projectClasses.find { it.name.contains("Calculator") } - ?: throw IllegalStateException("Calculator class not found") + // Find Process class and its state transition methods + val processClass = scene.projectClasses.find { it.name.contains("Process") && !it.name.contains("Manager") } + ?: throw IllegalStateException("Process class not found") - val complexOperationMethod = calculatorClass.methods - .find { it.name == "complexOperation" } - ?: throw IllegalStateException("complexOperation method not found") - - println("šŸ” Analyzing: ${calculatorClass.name}.${complexOperationMethod.name}") + val stateTransitionMethods = processClass.methods.filter { method -> + method.name in listOf("start", "pause", "block", "unblock", "terminate") + } - // Configure for detailed analysis - val machineOptions = UMachineOptions( - pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), - exceptionsPropagation = true, - stopOnTargetsReached = false, - timeout = Duration.INFINITE, - stepsFromLastCovered = 5000L, - solverType = SolverType.YICES, - ) + println("šŸ” Analyzing process state transition methods:") + stateTransitionMethods.forEach { method -> + println(" - ${processClass.name}.${method.name}") + } val observer = ReachabilityObserver() - val machine = TsMachine(scene, machineOptions, TsOptions(), machineObserver = observer) + val machine = TsMachine(scene, DEFAULT_MACHINE_OPTIONS, DEFAULT_TS_OPTIONS, machineObserver = observer) - // Create specific targets for different branches in complexOperation - val targets = createComplexOperationTargets(complexOperationMethod) - println("šŸ“ Created ${targets.size} specific targets for complex operation branches") + // Create specific targets for state transitions + val targets = createStateTransitionTargets(stateTransitionMethods) + println("šŸ“ Created ${targets.size} specific targets for state transitions") - val results = machine.analyze(listOf(complexOperationMethod), targets) + val results = machine.analyze(stateTransitionMethods, targets) - displayDetailedResults(results, targets, complexOperationMethod) + displayDetailedResults(results, targets, stateTransitionMethods.first()) } @Test - fun `analyze MathUtils static methods`() { - println("šŸ§® Analysis: MathUtils Static Methods") - println("=" + "=".repeat(44)) + fun `analyze MemoryManager operations`() { + println("šŸ§® Analysis: Memory Management Operations") + println("=" + "=".repeat(45)) val sampleProjectPath = getSampleProjectPath() val tsFiles = findTypeScriptFiles(sampleProjectPath) val scene = EtsScene(tsFiles.map { loadEtsFileAutoConvert(it.toPath()) }) - val mathUtilsClass = scene.projectClasses.find { it.name.contains("MathUtils") } - ?: throw IllegalStateException("MathUtils class not found") + val memoryManagerClass = scene.projectClasses.find { it.name.contains("MemoryManager") } + ?: throw IllegalStateException("MemoryManager class not found") - val staticMethods = mathUtilsClass.methods.filter { it.isStatic } - println("šŸ” Found ${staticMethods.size} static methods:") - staticMethods.forEach { println(" - ${it.name}") } + val memoryMethods = memoryManagerClass.methods.filter { method -> + method.name in listOf("allocateMemory", "freeMemory", "compactMemory", "defragmentMemory") + } - val machineOptions = UMachineOptions( - pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), - timeout = Duration.INFINITE, - stepsFromLastCovered = 2000L, - solverType = SolverType.Z3, + 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, TsOptions(), machineObserver = ReachabilityObserver()) - val targets = createMathUtilsTargets(mathUtilsClass).filter { it.location!!.location.method.name == "gcd" } + val machine = TsMachine(scene, machineOptions, DEFAULT_TS_OPTIONS, machineObserver = ReachabilityObserver()) + val targets = createMemoryManagerTargets(memoryManagerClass) - val results = machine.analyze(staticMethods, targets) + val results = machine.analyze(memoryMethods, targets) displayResults(results, targets) } @Test - fun `demonstrate path extraction from reachability results`() { - println("šŸ›¤ļø Demonstration: Path Extraction from Reachability Analysis") + fun `demonstrate array operations reachability`() { + println("šŸ›¤ļø Demonstration: Array Operations Reachability Analysis") println("=" + "=".repeat(58)) val sampleProjectPath = getSampleProjectPath() val tsFiles = findTypeScriptFiles(sampleProjectPath) val scene = EtsScene(tsFiles.map { loadEtsFileAutoConvert(it.toPath()) }) - val calculatorClass = scene.projectClasses.find { it.name.contains("Calculator") } - ?: throw IllegalStateException("Calculator class not found") + val processClass = scene.projectClasses.find { it.name.contains("Process") && !it.name.contains("Manager") } + ?: throw IllegalStateException("Process class not found") - val addMethod = calculatorClass.methods.find { it.name == "add" } - ?: throw IllegalStateException("add method not found") + val arrayMethod = processClass.methods.find { it.name == "addChild" || it.name == "removeChild" } + ?: throw IllegalStateException("Array manipulation method not found") - println("šŸ” Analyzing method: ${calculatorClass.name}.${addMethod.name}") + println("šŸ” Analyzing method: ${processClass.name}.${arrayMethod.name}") - val machineOptions = UMachineOptions( - pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), - exceptionsPropagation = true, - stopOnTargetsReached = false, - timeout = Duration.INFINITE, - stepsFromLastCovered = 1000L, - solverType = SolverType.YICES, + // Override options for focused array operation analysis + val machineOptions = DEFAULT_MACHINE_OPTIONS.copy( + stepsFromLastCovered = 1000L ) val observer = ReachabilityObserver() - val machine = TsMachine(scene, machineOptions, TsOptions(), machineObserver = observer) + val machine = TsMachine(scene, machineOptions, DEFAULT_TS_OPTIONS, machineObserver = observer) - // Create targets for different execution paths in the add method - val targets = createMethodPathTargets(addMethod) + // Create targets for different execution paths in array operations + val targets = createMethodPathTargets(arrayMethod) println("šŸ“ Created ${targets.size} path targets") - val results = machine.analyze(listOf(addMethod), targets) + val results = machine.analyze(listOf(arrayMethod), targets) - displayPathExtractionResults(results, targets, addMethod) + displayPathExtractionResults(results, targets, arrayMethod) } private fun getSampleProjectPath(): File { @@ -223,9 +219,11 @@ class SampleProjectTest { stmt.toString().contains("throw") -> { targets.add(TsReachabilityTarget.FinalPoint(stmt)) } + stmt.toString().contains("return") -> { targets.add(TsReachabilityTarget.FinalPoint(stmt)) } + stmt.toString().contains("if") -> { targets.add(TsReachabilityTarget.IntermediatePoint(stmt)) } @@ -237,22 +235,32 @@ class SampleProjectTest { return targets } - private fun createComplexOperationTargets(method: org.jacodb.ets.model.EtsMethod): List { + private fun createStateTransitionTargets(methods: List): List { val targets = mutableListOf() - val statements = method.cfg.stmts - statements.forEachIndexed { index, stmt -> - when (index) { - 0 -> targets.add(TsReachabilityTarget.InitialPoint(stmt)) - statements.size - 1 -> targets.add(TsReachabilityTarget.FinalPoint(stmt)) - else -> targets.add(TsReachabilityTarget.IntermediatePoint(stmt)) + 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 createMathUtilsTargets(clazz: org.jacodb.ets.model.EtsClass): List { + private fun createMemoryManagerTargets(clazz: org.jacodb.ets.model.EtsClass): List { val targets = mutableListOf() clazz.methods.forEach { method -> @@ -300,6 +308,11 @@ class SampleProjectTest { 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 -> @@ -307,8 +320,20 @@ class SampleProjectTest { } when { - wasReached -> reachable.add(target) - else -> unknown.add(target) // For this demo, we'll mark others as unknown + 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) + } } } @@ -336,7 +361,7 @@ class SampleProjectTest { private fun displayDetailedResults( results: List, targets: List, - method: org.jacodb.ets.model.EtsMethod + method: org.jacodb.ets.model.EtsMethod, ) { println("\nšŸ” DETAILED ANALYSIS: ${method.name}") println("=" + "=".repeat(59)) @@ -360,7 +385,7 @@ class SampleProjectTest { private fun displayPathExtractionResults( results: List, targets: List, - method: org.jacodb.ets.model.EtsMethod + method: org.jacodb.ets.model.EtsMethod, ) { println("\nšŸ›¤ļø PATH EXTRACTION DEMONSTRATION") println("=" + "=".repeat(49)) From 0c0da9cddc5c1bc2142c2a6128e69dcc3fdf455d Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 16 Sep 2025 15:59:38 +0300 Subject: [PATCH 03/18] Fixes --- .../org/usvm/reachability/cli/Reachability.kt | 2 +- .../usvm/reachability/SampleProjectTest.kt | 26 +++++++++---------- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt b/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt index a48ea50346..8b3c785a9a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt @@ -517,7 +517,7 @@ class ReachabilityAnalyzer : CliktCommand( private fun printSummaryToConsole(results: ReachabilityResults, duration: Double) { echo("") echo("šŸŽ‰ Analysis Complete!") - echo("ā±ļø Duration: ${String.format("%.2f", duration)}s") + echo("ā±ļø Duration: ${String.format("%.2f", duration)}s") echo("šŸ” Methods: ${results.methods.size}") echo("šŸ“ Targets: ${results.reachabilityResults.size}") diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt index 04c17acccc..874977aae2 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt @@ -37,7 +37,7 @@ class SampleProjectTest { pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), exceptionsPropagation = true, stopOnTargetsReached = false, - timeout = if (DEBUG) Duration.INFINITE else 60.seconds, + timeout = if (DEBUG) Duration.INFINITE else 30.seconds, stepsFromLastCovered = 1000L, solverType = SolverType.YICES, ) @@ -48,7 +48,7 @@ class SampleProjectTest { @Test fun `analyze ProcessManager reachability`() { println("šŸš€ Starting TypeScript Reachability Analysis on Sample Project") - println("=" + "=".repeat(59)) + println("=".repeat(60)) val sampleProjectPath = getSampleProjectPath() println("šŸ“ Project path: $sampleProjectPath") @@ -88,14 +88,14 @@ class SampleProjectTest { @Test fun `analyze ProcessManager state transitions`() { println("šŸŽÆ Focused Analysis: Process State Transitions") - println("=" + "=".repeat(49)) + 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.contains("Process") && !it.name.contains("Manager") } + val processClass = scene.projectClasses.find { it.name == "Process" } ?: throw IllegalStateException("Process class not found") val stateTransitionMethods = processClass.methods.filter { method -> @@ -122,7 +122,7 @@ class SampleProjectTest { @Test fun `analyze MemoryManager operations`() { println("šŸ§® Analysis: Memory Management Operations") - println("=" + "=".repeat(45)) + println("=".repeat(50)) val sampleProjectPath = getSampleProjectPath() val tsFiles = findTypeScriptFiles(sampleProjectPath) @@ -153,17 +153,17 @@ class SampleProjectTest { @Test fun `demonstrate array operations reachability`() { println("šŸ›¤ļø Demonstration: Array Operations Reachability Analysis") - println("=" + "=".repeat(58)) + 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.contains("Process") && !it.name.contains("Manager") } - ?: throw IllegalStateException("Process class not found") + val processClass = scene.projectClasses.find { it.name == "Process" } + ?: error("Process class not found") - val arrayMethod = processClass.methods.find { it.name == "addChild" || it.name == "removeChild" } - ?: throw IllegalStateException("Array manipulation method not found") + val arrayMethod = processClass.methods.find { it.name == "addChild" } + ?: error("Array manipulation method not found") println("šŸ” Analyzing method: ${processClass.name}.${arrayMethod.name}") @@ -300,7 +300,7 @@ class SampleProjectTest { private fun displayResults(results: List, targets: List) { println("\nšŸ“Š REACHABILITY ANALYSIS RESULTS") - println("=" + "=".repeat(49)) + println("=".repeat(50)) println("Total states explored: ${results.size}") println("Total targets defined: ${targets.size}") @@ -364,7 +364,7 @@ class SampleProjectTest { method: org.jacodb.ets.model.EtsMethod, ) { println("\nšŸ” DETAILED ANALYSIS: ${method.name}") - println("=" + "=".repeat(59)) + println("=".repeat(60)) displayResults(results, targets) @@ -388,7 +388,7 @@ class SampleProjectTest { method: org.jacodb.ets.model.EtsMethod, ) { println("\nšŸ›¤ļø PATH EXTRACTION DEMONSTRATION") - println("=" + "=".repeat(49)) + println("=".repeat(50)) println("Method: ${method.name}") println("Total execution states: ${results.size}") From 8e0f3db80060670449c1dc60fc282156e23be5e2 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 16 Sep 2025 16:09:17 +0300 Subject: [PATCH 04/18] Remove --strategy option --- .../kotlin/org/usvm/reachability/cli/Reachability.kt | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt b/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt index 8b3c785a9a..98f93c7390 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt @@ -103,11 +103,6 @@ class ReachabilityAnalyzer : CliktCommand( help = "šŸ‘£ Max steps from last covered statement" ).long().default(3500L) - private val pathStrategy by option( - "--strategy", - help = "šŸ›¤ļø Path selection strategy" - ).enum().default(PathSelectionStrategy.TARGETED) - // Output Options private val verbose by option( "-v", "--verbose", @@ -145,6 +140,8 @@ class ReachabilityAnalyzer : CliktCommand( } throw e } + + echo("šŸ‘‹ Exiting.") } private fun setupLogging() { @@ -168,7 +165,7 @@ class ReachabilityAnalyzer : CliktCommand( // Configure machine options val machineOptions = UMachineOptions( - pathSelectionStrategies = listOf(pathStrategy), + pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), exceptionsPropagation = true, stopOnTargetsReached = true, timeout = timeout.seconds, From b3397bda3c4f4b819c88a44ef4c6e63090f931de Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 16 Sep 2025 16:27:53 +0300 Subject: [PATCH 05/18] Update targets --- examples/reachability/targets.jsonc | 98 ++++++++++++++++++++++------- 1 file changed, 74 insertions(+), 24 deletions(-) diff --git a/examples/reachability/targets.jsonc b/examples/reachability/targets.jsonc index c349264ecb..becbe28519 100644 --- a/examples/reachability/targets.jsonc +++ b/examples/reachability/targets.jsonc @@ -1,26 +1,76 @@ [ - // Calculator class targets - {"type": "initial", "method": "Calculator.add", "statement": 0}, - {"type": "intermediate", "method": "Calculator.add", "statement": 1}, - {"type": "final", "method": "Calculator.add", "statement": 4}, - - {"type": "initial", "method": "Calculator.divide", "statement": 0}, - {"type": "intermediate", "method": "Calculator.divide", "statement": 1}, - {"type": "final", "method": "Calculator.divide", "statement": 4}, - - // Complex operation with multiple paths - {"type": "initial", "method": "Calculator.complexOperation", "statement": 0}, - {"type": "intermediate", "method": "Calculator.complexOperation", "statement": 2}, - {"type": "intermediate", "method": "Calculator.complexOperation", "statement": 4}, - {"type": "final", "method": "Calculator.complexOperation", "statement": 6}, - - // MathUtils targets - {"type": "initial", "method": "MathUtils.factorial", "statement": 0}, - {"type": "intermediate", "method": "MathUtils.factorial", "statement": 3}, - {"type": "final", "method": "MathUtils.factorial", "statement": 6}, - - {"type": "initial", "method": "MathUtils.isPrime", "statement": 0}, - {"type": "intermediate", "method": "MathUtils.isPrime", "statement": 5}, - {"type": "intermediate", "method": "MathUtils.isPrime", "statement": 8}, - {"type": "final", "method": "MathUtils.isPrime", "statement": 12} + // Process class state transition targets + {"type": "initial", "method": "Process.start", "statement": 0}, + {"type": "intermediate", "method": "Process.start", "statement": 1}, + {"type": "final", "method": "Process.start", "statement": 3}, + + {"type": "initial", "method": "Process.terminate", "statement": 0}, + {"type": "intermediate", "method": "Process.terminate", "statement": 1}, + {"type": "final", "method": "Process.terminate", "statement": 2}, + + // Process child management with array operations + {"type": "initial", "method": "Process.addChild", "statement": 0}, + {"type": "intermediate", "method": "Process.addChild", "statement": 2}, + {"type": "intermediate", "method": "Process.addChild", "statement": 5}, + {"type": "final", "method": "Process.addChild", "statement": 7}, + + {"type": "initial", "method": "Process.removeChild", "statement": 0}, + {"type": "intermediate", "method": "Process.removeChild", "statement": 2}, + {"type": "intermediate", "method": "Process.removeChild", "statement": 6}, + {"type": "final", "method": "Process.removeChild", "statement": 10}, + + // ProcessManager complex operations + {"type": "initial", "method": "ProcessManager.createProcess", "statement": 0}, + {"type": "intermediate", "method": "ProcessManager.createProcess", "statement": 3}, + {"type": "intermediate", "method": "ProcessManager.createProcess", "statement": 8}, + {"type": "final", "method": "ProcessManager.createProcess", "statement": 15}, + + {"type": "initial", "method": "ProcessManager.killProcess", "statement": 0}, + {"type": "intermediate", "method": "ProcessManager.killProcess", "statement": 5}, + {"type": "intermediate", "method": "ProcessManager.killProcess", "statement": 8}, + {"type": "final", "method": "ProcessManager.killProcess", "statement": 12}, + + // MemoryManager allocation targets + {"type": "initial", "method": "MemoryManager.allocateMemory", "statement": 0}, + {"type": "intermediate", "method": "MemoryManager.allocateMemory", "statement": 2}, + {"type": "intermediate", "method": "MemoryManager.allocateMemory", "statement": 6}, + {"type": "final", "method": "MemoryManager.allocateMemory", "statement": 10}, + + {"type": "initial", "method": "MemoryManager.freeMemory", "statement": 0}, + {"type": "intermediate", "method": "MemoryManager.freeMemory", "statement": 2}, + {"type": "intermediate", "method": "MemoryManager.freeMemory", "statement": 6}, + {"type": "final", "method": "MemoryManager.freeMemory", "statement": 8}, + + // MemoryManager defragmentation - complex algorithm with loops + {"type": "initial", "method": "MemoryManager.defragmentMemory", "statement": 0}, + {"type": "intermediate", "method": "MemoryManager.defragmentMemory", "statement": 3}, + {"type": "intermediate", "method": "MemoryManager.defragmentMemory", "statement": 8}, + {"type": "final", "method": "MemoryManager.defragmentMemory", "statement": 12}, + + // MemoryBlock operations + {"type": "initial", "method": "MemoryBlock.allocate", "statement": 0}, + {"type": "intermediate", "method": "MemoryBlock.allocate", "statement": 1}, + {"type": "final", "method": "MemoryBlock.allocate", "statement": 5}, + + // FileSystemNode path resolution + {"type": "initial", "method": "FileSystemNode.getPath", "statement": 0}, + {"type": "intermediate", "method": "FileSystemNode.getPath", "statement": 3}, + {"type": "intermediate", "method": "FileSystemNode.getPath", "statement": 6}, + {"type": "final", "method": "FileSystemNode.getPath", "statement": 10}, + + // FileSystem navigation with error handling + {"type": "initial", "method": "FileSystem.createFile", "statement": 0}, + {"type": "intermediate", "method": "FileSystem.createFile", "statement": 4}, + {"type": "intermediate", "method": "FileSystem.createFile", "statement": 8}, + {"type": "final", "method": "FileSystem.createFile", "statement": 12}, + + {"type": "initial", "method": "FileSystem.deleteFile", "statement": 0}, + {"type": "intermediate", "method": "FileSystem.deleteFile", "statement": 6}, + {"type": "intermediate", "method": "FileSystem.deleteFile", "statement": 10}, + {"type": "final", "method": "FileSystem.deleteFile", "statement": 13}, + + // FileSystem search with recursive traversal + {"type": "initial", "method": "FileSystem.findFiles", "statement": 0}, + {"type": "intermediate", "method": "FileSystem.findFiles", "statement": 5}, + {"type": "final", "method": "FileSystem.findFiles", "statement": 7} ] From 458c1a586cf27c24cdd5b1c1832b6f32e6115bcd Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Tue, 16 Sep 2025 16:28:46 +0300 Subject: [PATCH 06/18] Use error --- .../kotlin/org/usvm/reachability/SampleProjectTest.kt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt index 874977aae2..5f01d70006 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt @@ -96,7 +96,7 @@ class SampleProjectTest { // Find Process class and its state transition methods val processClass = scene.projectClasses.find { it.name == "Process" } - ?: throw IllegalStateException("Process class not found") + ?: error("Process class not found") val stateTransitionMethods = processClass.methods.filter { method -> method.name in listOf("start", "pause", "block", "unblock", "terminate") @@ -128,8 +128,8 @@ class SampleProjectTest { val tsFiles = findTypeScriptFiles(sampleProjectPath) val scene = EtsScene(tsFiles.map { loadEtsFileAutoConvert(it.toPath()) }) - val memoryManagerClass = scene.projectClasses.find { it.name.contains("MemoryManager") } - ?: throw IllegalStateException("MemoryManager class not found") + 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") @@ -199,7 +199,7 @@ class SampleProjectTest { if (parent != null && parent != dir) { return findProjectRoot(parent) } - throw IllegalStateException("Could not find project root") + error("Could not find project root") } private fun findTypeScriptFiles(projectDir: File): List { From 0a8ff8cfd2bdc574651664aa3cf7022ccc8f79d1 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 17 Sep 2025 17:42:54 +0300 Subject: [PATCH 07/18] tmp --- examples/reachability/README.md | 423 +++++++++--------- examples/reachability/reachability-cli.sh | 37 +- examples/reachability/targets.jsonc | 76 ---- examples/reachability/targets.yml | 32 ++ settings.gradle.kts | 30 +- usvm-ts/build.gradle.kts | 14 +- .../src/main/kotlin/org/usvm/api/TsTarget.kt | 6 + .../org/usvm/api/targets/dto/Targets.kt | 11 - .../kotlin/org/usvm/machine/TsMethodCall.kt | 5 + .../api/TsReachabilityObserver.kt} | 3 +- .../api/TsReachabilityTarget.kt} | 6 +- .../org/usvm/reachability/cli/Reachability.kt | 252 +++++++++-- .../org/usvm/reachability/dto/Targets.kt | 107 +++++ .../usvm/reachability/SampleProjectTest.kt | 21 +- 14 files changed, 625 insertions(+), 398 deletions(-) delete mode 100644 examples/reachability/targets.jsonc create mode 100644 examples/reachability/targets.yml create mode 100644 usvm-ts/src/main/kotlin/org/usvm/api/TsTarget.kt delete mode 100644 usvm-ts/src/main/kotlin/org/usvm/api/targets/dto/Targets.kt rename usvm-ts/src/main/kotlin/org/usvm/{api/targets/ReachabilityObserver.kt => reachability/api/TsReachabilityObserver.kt} (92%) rename usvm-ts/src/main/kotlin/org/usvm/{api/targets/TsTarget.kt => reachability/api/TsReachabilityTarget.kt} (71%) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/reachability/dto/Targets.kt diff --git a/examples/reachability/README.md b/examples/reachability/README.md index 74d5989938..dbebe444c4 100644 --- a/examples/reachability/README.md +++ b/examples/reachability/README.md @@ -1,259 +1,258 @@ -# šŸŽÆ TypeScript Reachability Analysis CLI +# USVM Reachability Analysis - Target File Formats -A powerful command-line tool for performing sophisticated reachability analysis on TypeScript projects using the USVM framework. +This document describes the supported target file formats for the USVM TypeScript Reachability Analysis tool. -## Features +## Supported Formats -- āœ… **REACHABLE**: Paths confirmed to be executable with complete execution traces -- āŒ **UNREACHABLE**: Paths confirmed to be impossible under any conditions -- ā“ **UNKNOWN**: Paths that could not be determined due to timeout, errors, or approximations +The tool automatically detects and supports three different JSON formats for specifying targets: -## Sample Project +### 1. Linear Trace Format - `{ "targets": [...] }` -The included sample project demonstrates a **System Applications** simulator with: +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"`) -- **ProcessManager.ts**: Process management with state transitions (CREATED ā†’ READY ā†’ RUNNING ā†’ BLOCKED/TERMINATED) -- **MemoryManager.ts**: Memory allocation, deallocation, compaction, and defragmentation -- **FileSystem.ts**: Basic file system operations and navigation - -These examples use only SMT-solver friendly constructs: - -- Integer operations (no floating-point or modulo operations) -- Array operations (length, indexing, push/pop) -- Object field access and updates -- Conditional logic and control flow -- Function calls without complex inheritance - -## Installation & Setup - -1. Ensure you have the USVM project built: - -```bash -cd /path/to/usvm -./gradlew build -``` - -2. Build the shadow JAR for faster execution: - -```bash -./gradlew :usvm-ts:shadowJar -``` - -3. The CLI is ready to use via the wrapper script or direct JAR execution. - -## Usage - -### Quick Start with Sample Project - -```bash -# Analyze the sample system applications project -./reachability-cli.sh -p ./sample-project - -# Analyze specific process management methods -./reachability-cli.sh -p ./sample-project --method Process --include-statements - -# Focus on memory management operations with verbose output -./reachability-cli.sh -p ./sample-project --method MemoryManager -v +**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 + } + } + ] +} ``` -### Analyze Your Own Project +### 2. Tree Trace Format - `{ "target": {...}, "children": [...] }` -```bash -# Analyze any TypeScript project with default settings -./reachability-cli.sh -p ./my-typescript-project - -# Use custom targets and verbose output -./reachability-cli.sh -p ./my-project -t ./targets.json -v -``` +A single tree-like trace with hierarchical target structure. -### Direct JAR Execution (Faster) - -```bash -java -jar usvm-ts/build/libs/usvm-ts-reachability.jar --project ./sample-project --verbose +**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 + } + } + } + ] + } + ] +} ``` -## Command Line Options - -### Required - -- `-p, --project PATH` - Path to TypeScript project directory - -### Optional Analysis Configuration - -- `-t, --targets FILE` - JSON file with target definitions (uses auto-generated targets if not provided) -- `-m, --mode MODE` - Analysis scope: `ALL_METHODS`, `PUBLIC_METHODS`, `ENTRY_POINTS` (default: PUBLIC_METHODS) -- `--method PATTERN` - Filter methods by name pattern - -### Solver & Performance Options - -- `--solver SOLVER` - SMT solver: `YICES`, `Z3`, `CVC5` (default: YICES) -- `--timeout SECONDS` - Overall analysis timeout (default: 300) -- `--steps LIMIT` - Maximum steps from last covered statement (default: 3500) -- `--strategy STRATEGY` - Path selection strategy (default: TARGETED) - -### Output Options +### 3. Trace List Format - `[ {...} ]` -- `-o, --output DIR` - Output directory (default: ./reachability-results) -- `-v, --verbose` - Enable verbose logging -- `--include-statements` - Include detailed statement information in reports - -## Target Definitions Format - -Create a JSON file to specify custom reachability targets: +An array of traces that can contain both linear and tree traces. +**Example: `targets-mixed.json`** ```json [ { - "type": "initial", - "method": "Calculator.add", - "statement": 0 - }, - { - "type": "intermediate", - "method": "Calculator.add", - "statement": 1 + "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 + } + } + ] }, { - "type": "final", - "method": "Calculator.add", - "statement": 4 + "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 +## Target Types -- **initial**: Entry point of the analysis path -- **intermediate**: Checkpoint along the execution path -- **final**: Target endpoint to reach +Each target can have one of three types: -### Hierarchical Structure +- **`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) -Targets are automatically organized into hierarchical chains per method: -`Initial Point ā†’ Intermediate Point(s) ā†’ Final Point` +## Location Structure -## Output Reports +Each target must specify a location with the following fields: -The tool generates comprehensive analysis reports: +- **`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 -### Summary Report (`reachability_summary.txt`) +## Common Statement Types -- Overall statistics and execution time -- Reachability status counts -- Per-target analysis results +The `stmtType` field should contain the IR name of the statement at the specified coordinates: -### Detailed Report (`reachability_detailed.md`) +- **`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 -- Markdown-formatted comprehensive analysis -- Method-by-method breakdown -- Execution paths with statements (when `--include-statements` is used) - -## Example Project Structure - -``` -my-typescript-project/ -ā”œā”€ā”€ Calculator.ts # TypeScript source files -ā”œā”€ā”€ MathUtils.ts -ā””ā”€ā”€ ... - -targets.jsonc # Optional target definitions -reachability-results/ # Generated output directory -ā”œā”€ā”€ reachability_summary.txt -ā””ā”€ā”€ reachability_detailed.md -``` +## Linear Trace Rules -## Reachability Analysis Results +For linear traces (both standalone and within trace lists): -### Status Categories +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 -1. **REACHABLE** āœ… - - Path is definitely executable - - Includes complete execution trace with all statements - - Shows path conditions and variable states +## Automatic Format Detection -2. **UNREACHABLE** āŒ - - Path is proven to be impossible - - No valid execution can reach this target - - Useful for dead code detection +The tool automatically detects which format is being used based on the JSON structure: -3. **UNKNOWN** ā“ - - Analysis couldn't determine reachability - - Common causes: timeout, solver limitations, complex approximations - - Requires further investigation or different analysis parameters +- 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 -### Execution Paths +No manual format specification is required! -For REACHABLE targets, the tool provides: - -- Complete statement sequence from execution start to target -- All intermediate statements traversed -- Path conditions (when available) -- Variable state information - -## Example Usage Scenarios - -### 1. Dead Code Detection +## Usage Examples ```bash -./reachability-cli.sh -p ./src --mode ALL_METHODS -v -``` +# Using linear trace format +./reachability -p ./my-project -t targets.json -### 2. Critical Path Analysis +# Using hierarchical (tree-like) format +./reachability -p ./my-project -t targets-tree.json -```bash -./reachability-cli.sh -p ./src -t ./critical-paths.json --include-statements -``` +# Using mixed array format +./reachability -p ./my-project -t targets-mixed.json -### 3. Method-Specific Analysis - -```bash -./reachability-cli.sh -p ./src --method "authenticate" --solver Z3 +# Auto-generate targets (no file needed) +./reachability -p ./my-project ``` -### 4. High-Precision Analysis - -```bash -./reachability-cli.sh -p ./src --timeout 600 --steps 10000 --solver CVC5 -``` - -## Implementation Details - -The CLI leverages the USVM framework's powerful reachability analysis capabilities: - -- **Project Loading**: Uses `loadEtsFileAutoConvert()` for automatic TypeScript to IR conversion -- **Target Creation**: Builds hierarchical target structures using `TsReachabilityTarget` classes -- **Analysis Engine**: Utilizes `TsMachine` with configurable solver backends -- **Path Extraction**: Extracts execution paths from `TsState.pathNode.allStatements` - -## Troubleshooting - -### Common Issues - -1. **"No TypeScript files found"** - - Ensure the project path contains `.ts` or `.js` files - - Check file permissions - -2. **"Analysis timeout"** - - Increase `--timeout` value - - Reduce `--steps` limit - - Try different `--solver` - -3. **"Target not found"** - - Verify method names in targets.jsonc match exactly - - Check statement indices are within bounds - -### Debug Mode - -Enable verbose output with `-v` to see detailed analysis progress and any warnings. - -## Contributing - -The CLI is part of the USVM project. To extend functionality: - -1. Add new options to `ReachabilityAnalyzer` class -2. Update the wrapper script with corresponding parameters -3. Add appropriate documentation - -## License +## Legacy Format Support -This tool is part of the USVM project and follows the same licensing terms. +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 index 6ac87784c4..6f1aec2299 100755 --- a/examples/reachability/reachability-cli.sh +++ b/examples/reachability/reachability-cli.sh @@ -18,6 +18,7 @@ TIMEOUT=300 STEPS=3500 VERBOSE=false INCLUDE_STATEMENTS=false +METHOD_FILTER="" # Colors for output RED='\033[0;31m' @@ -50,9 +51,6 @@ usage() { echo " # Analyze all public methods in a TypeScript project" echo " $0 -p ./my-typescript-project" echo "" - echo " # Analyze the sample system applications project" - echo " $0 -p ../examples/reachability/sample-project" - echo "" echo " # Use custom targets and verbose output" echo " $0 -p ./my-project -t ./targets.json -v" echo "" @@ -60,6 +58,7 @@ usage() { echo " $0 -p ./project --method ProcessManager --include-statements" } +# Parse command line arguments while [[ $# -gt 0 ]]; do case $1 in -p|--project) @@ -114,6 +113,7 @@ while [[ $# -gt 0 ]]; do esac done +# Validate required arguments if [[ -z "$PROJECT_PATH" ]]; then echo -e "${RED}āŒ Error: Project path is required${NC}" usage @@ -125,25 +125,27 @@ if [[ ! -d "$PROJECT_PATH" ]]; then 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" -# Path to the shadow JAR -SHADOW_JAR="$USVM_ROOT/usvm-ts/build/libs/usvm-ts-reachability.jar" +# Path to the compiled shadow JAR +JAR_PATH="$USVM_ROOT/usvm-ts/build/libs/usvm-ts-all.jar" -# Check if shadow JAR exists -if [[ ! -f "$SHADOW_JAR" ]]; then - echo -e "${RED}āŒ Error: Shadow JAR not found at $SHADOW_JAR${NC}" - echo "Please run the following commands first:" - echo " cd $USVM_ROOT" - echo " ./gradlew :usvm-ts:shadowJar" - exit 1 +# 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 -# Build the Java command arguments +# Build the command arguments JAVA_ARGS=() JAVA_ARGS+=("--project" "$PROJECT_PATH") JAVA_ARGS+=("--output" "$OUTPUT_DIR") @@ -179,9 +181,12 @@ fi echo "" echo -e "${YELLOW}āš” Running analysis...${NC}" -# Execute the JAR directly -echo -e "ARGS: ${JAVA_ARGS[*]}" -java -Dfile.encoding=UTF-8 -Dsun.stdout.encoding=UTF-8 -jar "$SHADOW_JAR" "${JAVA_ARGS[@]}" +# Execute the analysis +java -Dfile.encoding=UTF-8 \ + -Dsun.stdout.encoding=UTF-8 \ + -cp "$JAR_PATH" \ + org.usvm.reachability.cli.ReachabilityKt \ + "${JAVA_ARGS[@]}" echo "" echo -e "${GREEN}āœ… Analysis complete! Check the results in: $OUTPUT_DIR${NC}" diff --git a/examples/reachability/targets.jsonc b/examples/reachability/targets.jsonc deleted file mode 100644 index becbe28519..0000000000 --- a/examples/reachability/targets.jsonc +++ /dev/null @@ -1,76 +0,0 @@ -[ - // Process class state transition targets - {"type": "initial", "method": "Process.start", "statement": 0}, - {"type": "intermediate", "method": "Process.start", "statement": 1}, - {"type": "final", "method": "Process.start", "statement": 3}, - - {"type": "initial", "method": "Process.terminate", "statement": 0}, - {"type": "intermediate", "method": "Process.terminate", "statement": 1}, - {"type": "final", "method": "Process.terminate", "statement": 2}, - - // Process child management with array operations - {"type": "initial", "method": "Process.addChild", "statement": 0}, - {"type": "intermediate", "method": "Process.addChild", "statement": 2}, - {"type": "intermediate", "method": "Process.addChild", "statement": 5}, - {"type": "final", "method": "Process.addChild", "statement": 7}, - - {"type": "initial", "method": "Process.removeChild", "statement": 0}, - {"type": "intermediate", "method": "Process.removeChild", "statement": 2}, - {"type": "intermediate", "method": "Process.removeChild", "statement": 6}, - {"type": "final", "method": "Process.removeChild", "statement": 10}, - - // ProcessManager complex operations - {"type": "initial", "method": "ProcessManager.createProcess", "statement": 0}, - {"type": "intermediate", "method": "ProcessManager.createProcess", "statement": 3}, - {"type": "intermediate", "method": "ProcessManager.createProcess", "statement": 8}, - {"type": "final", "method": "ProcessManager.createProcess", "statement": 15}, - - {"type": "initial", "method": "ProcessManager.killProcess", "statement": 0}, - {"type": "intermediate", "method": "ProcessManager.killProcess", "statement": 5}, - {"type": "intermediate", "method": "ProcessManager.killProcess", "statement": 8}, - {"type": "final", "method": "ProcessManager.killProcess", "statement": 12}, - - // MemoryManager allocation targets - {"type": "initial", "method": "MemoryManager.allocateMemory", "statement": 0}, - {"type": "intermediate", "method": "MemoryManager.allocateMemory", "statement": 2}, - {"type": "intermediate", "method": "MemoryManager.allocateMemory", "statement": 6}, - {"type": "final", "method": "MemoryManager.allocateMemory", "statement": 10}, - - {"type": "initial", "method": "MemoryManager.freeMemory", "statement": 0}, - {"type": "intermediate", "method": "MemoryManager.freeMemory", "statement": 2}, - {"type": "intermediate", "method": "MemoryManager.freeMemory", "statement": 6}, - {"type": "final", "method": "MemoryManager.freeMemory", "statement": 8}, - - // MemoryManager defragmentation - complex algorithm with loops - {"type": "initial", "method": "MemoryManager.defragmentMemory", "statement": 0}, - {"type": "intermediate", "method": "MemoryManager.defragmentMemory", "statement": 3}, - {"type": "intermediate", "method": "MemoryManager.defragmentMemory", "statement": 8}, - {"type": "final", "method": "MemoryManager.defragmentMemory", "statement": 12}, - - // MemoryBlock operations - {"type": "initial", "method": "MemoryBlock.allocate", "statement": 0}, - {"type": "intermediate", "method": "MemoryBlock.allocate", "statement": 1}, - {"type": "final", "method": "MemoryBlock.allocate", "statement": 5}, - - // FileSystemNode path resolution - {"type": "initial", "method": "FileSystemNode.getPath", "statement": 0}, - {"type": "intermediate", "method": "FileSystemNode.getPath", "statement": 3}, - {"type": "intermediate", "method": "FileSystemNode.getPath", "statement": 6}, - {"type": "final", "method": "FileSystemNode.getPath", "statement": 10}, - - // FileSystem navigation with error handling - {"type": "initial", "method": "FileSystem.createFile", "statement": 0}, - {"type": "intermediate", "method": "FileSystem.createFile", "statement": 4}, - {"type": "intermediate", "method": "FileSystem.createFile", "statement": 8}, - {"type": "final", "method": "FileSystem.createFile", "statement": 12}, - - {"type": "initial", "method": "FileSystem.deleteFile", "statement": 0}, - {"type": "intermediate", "method": "FileSystem.deleteFile", "statement": 6}, - {"type": "intermediate", "method": "FileSystem.deleteFile", "statement": 10}, - {"type": "final", "method": "FileSystem.deleteFile", "statement": 13}, - - // FileSystem search with recursive traversal - {"type": "initial", "method": "FileSystem.findFiles", "statement": 0}, - {"type": "intermediate", "method": "FileSystem.findFiles", "statement": 5}, - {"type": "final", "method": "FileSystem.findFiles", "statement": 7} -] 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 67154f5343..d9dec8f2a5 100644 --- a/usvm-ts/build.gradle.kts +++ b/usvm-ts/build.gradle.kts @@ -8,7 +8,7 @@ import kotlin.time.Duration plugins { id("usvm.kotlin-conventions") - application + kotlin("plugin.serialization") version Versions.kotlin id(Plugins.Shadow) } @@ -19,6 +19,7 @@ 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) @@ -35,17 +36,8 @@ dependencies { testImplementation("org.burningwave:core:12.62.7") } -application { - mainClass = "org.usvm.reachability.cli.ReachabilityKt" - applicationDefaultJvmArgs = listOf("-Dfile.encoding=UTF-8", "-Dsun.stdout.encoding=UTF-8") -} - -tasks.startScripts { - applicationName = "usvm-ts-reachability" -} - tasks.shadowJar { - archiveBaseName.set("usvm-ts-reachability") + archiveBaseName.set("usvm-ts-all") archiveClassifier.set("") mergeServiceFiles() 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/dto/Targets.kt b/usvm-ts/src/main/kotlin/org/usvm/api/targets/dto/Targets.kt deleted file mode 100644 index d614f37a72..0000000000 --- a/usvm-ts/src/main/kotlin/org/usvm/api/targets/dto/Targets.kt +++ /dev/null @@ -1,11 +0,0 @@ -package org.usvm.api.targets.dto - -import org.jacodb.ets.dto.StmtDto - -sealed interface TargetDto { - val location: StmtDto - - class InitialPoint(override val location: StmtDto) : TargetDto - class IntermediatePoint(override val location: StmtDto) : TargetDto - class FinalPoint(override val location: StmtDto) : TargetDto -} 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/api/targets/ReachabilityObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/reachability/api/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/reachability/api/TsReachabilityObserver.kt index 4c12c769ed..ecd17419c9 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/targets/ReachabilityObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/reachability/api/TsReachabilityObserver.kt @@ -1,5 +1,6 @@ -package org.usvm.api.targets +package org.usvm.reachability.api +import org.usvm.reachability.api.TsReachabilityTarget import org.usvm.machine.state.TsState import org.usvm.statistics.UMachineObserver diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/targets/TsTarget.kt b/usvm-ts/src/main/kotlin/org/usvm/reachability/api/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/reachability/api/TsReachabilityTarget.kt index 356d2a4b65..ee007a6b18 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/targets/TsTarget.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/reachability/api/TsReachabilityTarget.kt @@ -1,9 +1,7 @@ -package org.usvm.api.targets +package org.usvm.reachability.api import org.jacodb.ets.model.EtsStmt -import org.usvm.targets.UTarget - -open class TsTarget(location: EtsStmt?) : UTarget(location) +import org.usvm.api.targets.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/reachability/cli/Reachability.kt b/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt index 98f93c7390..2087d69052 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt @@ -13,6 +13,14 @@ 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 kotlinx.serialization.json.JsonArray +import kotlinx.serialization.json.JsonElement +import kotlinx.serialization.json.JsonObject +import kotlinx.serialization.json.intOrNull +import kotlinx.serialization.json.jsonArray +import kotlinx.serialization.json.jsonObject +import kotlinx.serialization.json.jsonPrimitive import org.jacodb.ets.model.EtsIfStmt import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsReturnStmt @@ -156,7 +164,7 @@ class ReachabilityAnalyzer : CliktCommand( // Load TypeScript project using autoConvert like in tests val tsFiles = findTypeScriptFiles(projectPath) if (tsFiles.isEmpty()) { - throw IllegalArgumentException("No TypeScript files found in ${projectPath}") + throw IllegalArgumentException("No TypeScript files found in $projectPath") } echo("šŸ“ Found ${tsFiles.size} TypeScript files") @@ -240,41 +248,121 @@ class ReachabilityAnalyzer : CliktCommand( private fun parseTargetDefinitions(targetsFile: Path): List { val content = targetsFile.readText() return try { - // Simple JSON parsing for target definitions - // Expected format: [{"type": "initial|intermediate|final", "method": "ClassName.methodName", "statement": index}] - val lines = content.lines() - .map { it.trim() } - .filter { it.isNotEmpty() && !it.startsWith("//") && !it.startsWith("[") && !it.startsWith("]") } - .filter { it.contains("\"type\"") } - - lines.mapNotNull { line -> - try { - val typeMatch = Regex("\"type\"\\s*:\\s*\"(\\w+)\"").find(line) - val methodMatch = Regex("\"method\"\\s*:\\s*\"([^\"]+)\"").find(line) - val statementMatch = Regex("\"statement\"\\s*:\\s*(\\d+)").find(line) - - if (typeMatch != null && methodMatch != null && statementMatch != null) { - val type = when (typeMatch.groupValues[1].lowercase()) { - "initial" -> TargetType.INITIAL - "intermediate" -> TargetType.INTERMEDIATE - "final" -> TargetType.FINAL - else -> return@mapNotNull null + val json = Json { + ignoreUnknownKeys = true + isLenient = true + } + + val jsonElement = json.parseToJsonElement(content) + val targetDefinitions = parseJsonTargets(jsonElement) + + echo("šŸ“‹ Parsed ${targetDefinitions.size} target definitions from ${targetsFile.fileName}") + targetDefinitions + + } catch (e: Exception) { + echo("āŒ Error parsing targets file: ${e.message}", err = true) + if (verbose) { + e.printStackTrace() + } + emptyList() + } + } + + private fun parseJsonTargets(jsonElement: JsonElement): List { + return when (jsonElement) { + is JsonObject -> { + when { + // Linear trace format: { "targets": [...] } + jsonElement.containsKey("targets") -> { + val targetsArray = jsonElement["targets"]?.jsonArray + targetsArray?.mapNotNull { parseTargetFromJson(it) } ?: emptyList() + } + // Tree trace format: { "target": {...}, "children": [...] } + jsonElement.containsKey("target") -> { + val target = jsonElement["target"]?.let { parseTargetFromJson(it) } + val childrenTargets = jsonElement["children"]?.jsonArray?.let { children -> + children.flatMap { parseTargetsFromTreeNode(it) } + } ?: emptyList() + listOfNotNull(target) + childrenTargets + } + + else -> emptyList() + } + } + + is JsonArray -> { + // Array format: [ {...} ] + jsonElement.flatMap { element -> + when { + element is JsonObject && element.containsKey("targets") -> { + val targetsArray = element["targets"]?.jsonArray + targetsArray?.mapNotNull { parseTargetFromJson(it) } ?: emptyList() } - TargetDefinition( - type = type, - methodName = methodMatch.groupValues[1], - statementIndex = statementMatch.groupValues[1].toInt() - ) - } else null - } catch (_: Exception) { - echo("āš ļø Warning: Could not parse target definition: $line", err = true) - null + element is JsonObject && element.containsKey("target") -> { + val target = element["target"]?.let { parseTargetFromJson(it) } + val childrenTargets = element["children"]?.jsonArray?.let { children -> + children.flatMap { parseTargetsFromTreeNode(it) } + } ?: emptyList() + listOfNotNull(target) + childrenTargets + } + + else -> emptyList() + } } } + + else -> emptyList() + } + } + + private fun parseTargetsFromTreeNode(nodeElement: JsonElement): List { + val nodeObj = nodeElement.jsonObject + val target = nodeObj["target"]?.let { parseTargetFromJson(it) } + val childrenTargets = nodeObj["children"]?.jsonArray?.let { children -> + children.flatMap { parseTargetsFromTreeNode(it) } + } ?: emptyList() + return listOfNotNull(target) + childrenTargets + } + + private fun parseTargetFromJson(jsonElement: JsonElement): TargetDefinition? { + return try { + val obj = jsonElement.jsonObject + val typeStr = obj["type"]?.jsonPrimitive?.content ?: "intermediate" + val location = obj["location"]?.jsonObject + + val type = when (typeStr.lowercase()) { + "initial" -> TargetType.INITIAL + "intermediate" -> TargetType.INTERMEDIATE + "final" -> TargetType.FINAL + else -> TargetType.INTERMEDIATE + } + + if (location != null) { + val fileName = location["fileName"]?.jsonPrimitive?.content ?: "" + val className = location["className"]?.jsonPrimitive?.content ?: "" + val methodName = location["methodName"]?.jsonPrimitive?.content ?: "" + val stmtType = location["stmtType"]?.jsonPrimitive?.content + val block = location["block"]?.jsonPrimitive?.intOrNull + val index = location["index"]?.jsonPrimitive?.intOrNull + + TargetDefinition( + type = type, + methodName = "$className.$methodName", + locationInfo = LocationInfo( + fileName = fileName, + className = className, + methodName = methodName, + stmtType = stmtType, + block = block, + index = index + ) + ) + } else { + null + } } catch (_: Exception) { - echo("āŒ Error parsing targets file", err = true) - emptyList() + null } } @@ -283,26 +371,44 @@ class ReachabilityAnalyzer : CliktCommand( val statements = method.cfg.stmts if (statements.isEmpty()) return@flatMap emptyList() + val className = method.enclosingClass?.name ?: "Unknown" + val methodName = method.name + val fullMethodName = "$className.$methodName" + val targets = mutableListOf() - // Initial point + // Initial point - first statement targets.add( TargetDefinition( type = TargetType.INITIAL, - methodName = "${method.enclosingClass?.name ?: "Unknown"}.${method.name}", - statementIndex = 0 + methodName = fullMethodName, + locationInfo = LocationInfo( + fileName = "$className.ts", + className = className, + methodName = methodName, + stmtType = statements.firstOrNull()?.javaClass?.simpleName, + block = 0, + index = 0 + ) ) ) - // Intermediate points for control flow statements + // Intermediate and final points for control flow statements statements.forEachIndexed { index, stmt -> when (stmt) { is EtsIfStmt, is EtsReturnStmt -> { targets.add( TargetDefinition( type = if (stmt == statements.last()) TargetType.FINAL else TargetType.INTERMEDIATE, - methodName = "${method.enclosingClass?.name ?: "Unknown"}.${method.name}", - statementIndex = index + methodName = fullMethodName, + locationInfo = LocationInfo( + fileName = "$className.ts", + className = className, + methodName = methodName, + stmtType = stmt.javaClass.simpleName, + block = index / 10, // Estimate block from index + index = index + ) ) ) } @@ -329,9 +435,9 @@ class ReachabilityAnalyzer : CliktCommand( // Find initial target val initialTarget = methodTargets.find { it.type == TargetType.INITIAL } ?.let { targetDef -> - if (targetDef.statementIndex < statements.size) { - TsReachabilityTarget.InitialPoint(statements[targetDef.statementIndex]) - } else null + findStatementByDefinition(statements, targetDef)?.let { stmt -> + TsReachabilityTarget.InitialPoint(stmt) + } } ?: return@forEach targets.add(initialTarget) @@ -339,10 +445,9 @@ class ReachabilityAnalyzer : CliktCommand( // Build chain of intermediate and final targets var currentTarget: TsTarget = initialTarget methodTargets.filter { it.type != TargetType.INITIAL } - .sortedBy { it.statementIndex } + .sortedWith(compareBy { it.locationInfo.index ?: 0 }) .forEach { targetDef -> - if (targetDef.statementIndex < statements.size) { - val stmt = statements[targetDef.statementIndex] + findStatementByDefinition(statements, targetDef)?.let { stmt -> val target = when (targetDef.type) { TargetType.INTERMEDIATE -> TsReachabilityTarget.IntermediatePoint(stmt) TargetType.FINAL -> TsReachabilityTarget.FinalPoint(stmt) @@ -356,6 +461,52 @@ class ReachabilityAnalyzer : CliktCommand( return targets } + private fun findStatementByDefinition( + statements: List, + targetDef: TargetDefinition, + ): EtsStmt? { + val targetLocation = targetDef.locationInfo + + // 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: LocationInfo): 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) { + // Enhanced 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, @@ -378,8 +529,7 @@ class ReachabilityAnalyzer : CliktCommand( states.filter { targetLocation in it.pathNode.allStatements } .map { state -> ExecutionPath( - statements = state.pathNode.allStatements.toList(), - pathConditions = emptyList() // TODO: Extract path conditions + statements = state.pathNode.allStatements.toList() ) } } else { @@ -545,15 +695,23 @@ enum class ReachabilityStatus { UNKNOWN // Could not determine (timeout/approximation/error) } +data class LocationInfo( + val fileName: String, + val className: String, + val methodName: String, + val stmtType: String?, + val block: Int?, + val index: Int?, +) + data class TargetDefinition( val type: TargetType, val methodName: String, - val statementIndex: Int, + val locationInfo: LocationInfo, ) data class ExecutionPath( val statements: List, - val pathConditions: List, // Simplified - would contain actual conditions ) data class TargetReachabilityResult( diff --git a/usvm-ts/src/main/kotlin/org/usvm/reachability/dto/Targets.kt b/usvm-ts/src/main/kotlin/org/usvm/reachability/dto/Targets.kt new file mode 100644 index 0000000000..7a5527cf79 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/reachability/dto/Targets.kt @@ -0,0 +1,107 @@ +package org.usvm.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: { "target": {...}, "children": [...] } + @Serializable + data class TreeTrace( + val target: TargetDto, + val children: List = emptyList(), + ) : 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 "target" field: { "target": {...}, "children": [...] } + element is JsonObject && element.containsKey("target") -> 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/test/kotlin/org/usvm/reachability/SampleProjectTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt index 5f01d70006..1925eb5ab4 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt @@ -1,6 +1,9 @@ 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 @@ -75,7 +78,15 @@ class SampleProjectTest { // Create interesting reachability targets for the system classes val targets = createSampleTargets(scene) - println("šŸŽÆ Created ${targets.size} reachability targets") + 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...") @@ -215,16 +226,16 @@ class SampleProjectTest { clazz.methods.forEach { method -> method.cfg.stmts.forEach { stmt -> // Create targets for different types of statements - when { - stmt.toString().contains("throw") -> { + when (stmt) { + is EtsThrowStmt -> { targets.add(TsReachabilityTarget.FinalPoint(stmt)) } - stmt.toString().contains("return") -> { + is EtsReturnStmt -> { targets.add(TsReachabilityTarget.FinalPoint(stmt)) } - stmt.toString().contains("if") -> { + is EtsIfStmt -> { targets.add(TsReachabilityTarget.IntermediatePoint(stmt)) } } From f3d0008545d91ab31cefa51f437b52a727220bf7 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 17 Sep 2025 17:42:58 +0300 Subject: [PATCH 08/18] tmp --- .../main/kotlin/org/usvm/machine/TsMachine.kt | 2 +- .../usvm/machine/interpreter/TsInterpreter.kt | 2 +- .../kotlin/org/usvm/machine/state/TsState.kt | 2 +- .../api/TsReachabilityObserver.kt | 3 +- .../reachability/api/TsReachabilityTarget.kt | 2 +- .../org/usvm/reachability/cli/Reachability.kt | 34 ++++++++++++++----- .../org/usvm/reachability/dto/Targets.kt | 4 +-- .../org/usvm/checkers/ReachabilityChecker.kt | 8 ++--- .../reachability/ArrayReachabilityTest.kt | 18 +++++----- .../BasicConditionsReachabilityTest.kt | 16 ++++----- .../reachability/ComplexReachabilityTest.kt | 16 ++++----- .../FieldAccessReachabilityTest.kt | 16 ++++----- .../FunctionCallReachabilityTest.kt | 16 ++++----- .../usvm/reachability/SampleProjectTest.kt | 14 ++++---- 14 files changed, 83 insertions(+), 70 deletions(-) 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..0d42bfd582 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -8,7 +8,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 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 3babb464da..bab7b4e6e9 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 @@ -40,7 +40,7 @@ import org.usvm.UIteExpr 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.TsTarget import org.usvm.api.typeStreamOf import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.forkblacklists.UForkBlackList 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..b72c6735cb 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 @@ -19,7 +19,7 @@ import org.usvm.USort import org.usvm.UState import org.usvm.api.allocateConcreteRef import org.usvm.api.initializeArray -import org.usvm.api.targets.TsTarget +import org.usvm.api.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/main/kotlin/org/usvm/reachability/api/TsReachabilityObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/reachability/api/TsReachabilityObserver.kt index ecd17419c9..c1d8db3d8c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/reachability/api/TsReachabilityObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/reachability/api/TsReachabilityObserver.kt @@ -1,10 +1,9 @@ package org.usvm.reachability.api -import org.usvm.reachability.api.TsReachabilityTarget 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/reachability/api/TsReachabilityTarget.kt b/usvm-ts/src/main/kotlin/org/usvm/reachability/api/TsReachabilityTarget.kt index ee007a6b18..b39b3d9923 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/reachability/api/TsReachabilityTarget.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/reachability/api/TsReachabilityTarget.kt @@ -1,7 +1,7 @@ package org.usvm.reachability.api import org.jacodb.ets.model.EtsStmt -import org.usvm.api.targets.TsTarget +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/reachability/cli/Reachability.kt b/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt index 2087d69052..455f175b65 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt @@ -30,12 +30,13 @@ 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.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.machine.state.TsState +import org.usvm.reachability.api.TsReachabilityObserver +import org.usvm.reachability.api.TsReachabilityTarget +import org.usvm.reachability.dto.TargetsContainerDto import java.nio.file.Path import kotlin.io.path.Path import kotlin.io.path.createDirectories @@ -184,7 +185,7 @@ class ReachabilityAnalyzer : CliktCommand( ) val tsOptions = TsOptions() - val machine = TsMachine(scene, machineOptions, tsOptions, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, machineOptions, tsOptions, machineObserver = TsReachabilityObserver()) // Find methods to analyze val methodsToAnalyze = findMethodsToAnalyze(scene) @@ -253,8 +254,8 @@ class ReachabilityAnalyzer : CliktCommand( isLenient = true } - val jsonElement = json.parseToJsonElement(content) - val targetDefinitions = parseJsonTargets(jsonElement) + val targetsDto = json.decodeFromString(content) + val targetDefinitions = convertToDefinitions(targetsDto) echo("šŸ“‹ Parsed ${targetDefinitions.size} target definitions from ${targetsFile.fileName}") targetDefinitions @@ -268,6 +269,22 @@ class ReachabilityAnalyzer : CliktCommand( } } + private fun convertToDefinitions(targetsDto: TargetsContainerDto) : List { + val result = mutableListOf() + + when (targetsDto) { + is TargetsContainerDto.LinearTrace -> { + result += convertToDefinition(targetsDto.targets) + } + + is TargetsContainerDto.TreeTrace -> TODO() + + is TargetsContainerDto.TraceList -> TODO() + } + + return result + } + private fun parseJsonTargets(jsonElement: JsonElement): List { return when (jsonElement) { is JsonObject -> { @@ -491,7 +508,7 @@ class ReachabilityAnalyzer : CliktCommand( // Match by block and index if both are specified if (location.block != null && location.index != null) { - // Enhanced location matching based on statement position + // Location matching based on statement position return matchesByPosition(stmt, location.block, location.index) } @@ -540,7 +557,7 @@ class ReachabilityAnalyzer : CliktCommand( TargetReachabilityResult( target = target, status = reachabilityStatus, - executionPaths = executionPaths + executionPaths = executionPaths, ) ) } @@ -706,7 +723,6 @@ data class LocationInfo( data class TargetDefinition( val type: TargetType, - val methodName: String, val locationInfo: LocationInfo, ) diff --git a/usvm-ts/src/main/kotlin/org/usvm/reachability/dto/Targets.kt b/usvm-ts/src/main/kotlin/org/usvm/reachability/dto/Targets.kt index 7a5527cf79..6b2ac26acc 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/reachability/dto/Targets.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/reachability/dto/Targets.kt @@ -79,7 +79,7 @@ data class TargetTreeNodeDto( ) @Serializable -enum class TargetTypeDto { +enum class TargetType { @SerialName("initial") INITIAL, @@ -92,7 +92,7 @@ enum class TargetTypeDto { @Serializable data class TargetDto( - val type: TargetTypeDto = TargetTypeDto.INTERMEDIATE, + val type: TargetType = TargetType.INTERMEDIATE, val location: LocationDto, // TODO: consider inlining ) 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..657d00a1d2 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.reachability.api.TsReachabilityObserver +import org.usvm.reachability.api.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..47e57a0095 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.reachability.api.TsReachabilityObserver +import org.usvm.reachability.api.TsReachabilityTarget +import org.usvm.api.TsTarget 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..c86276c5ad 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.reachability.api.TsReachabilityObserver +import org.usvm.reachability.api.TsReachabilityTarget +import org.usvm.api.TsTarget 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..25e5bce488 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.reachability.api.TsReachabilityObserver +import org.usvm.reachability.api.TsReachabilityTarget +import org.usvm.api.TsTarget 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..edbc713461 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.reachability.api.TsReachabilityObserver +import org.usvm.reachability.api.TsReachabilityTarget +import org.usvm.api.TsTarget 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..cbcb852c19 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.reachability.api.TsReachabilityObserver +import org.usvm.reachability.api.TsReachabilityTarget +import org.usvm.api.TsTarget 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 index 1925eb5ab4..da8fe1ca99 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt @@ -9,9 +9,9 @@ import org.junit.jupiter.api.Test 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.reachability.api.TsReachabilityObserver +import org.usvm.reachability.api.TsReachabilityTarget +import org.usvm.api.TsTarget import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.machine.state.TsState @@ -65,7 +65,7 @@ class SampleProjectTest { println("šŸ“Š Loaded scene with ${scene.projectClasses.size} classes") // Use default options - val observer = ReachabilityObserver() + val observer = TsReachabilityObserver() val machine = TsMachine(scene, DEFAULT_MACHINE_OPTIONS, DEFAULT_TS_OPTIONS, machineObserver = observer) // Find all methods in the sample project @@ -118,7 +118,7 @@ class SampleProjectTest { println(" - ${processClass.name}.${method.name}") } - val observer = ReachabilityObserver() + val observer = TsReachabilityObserver() val machine = TsMachine(scene, DEFAULT_MACHINE_OPTIONS, DEFAULT_TS_OPTIONS, machineObserver = observer) // Create specific targets for state transitions @@ -154,7 +154,7 @@ class SampleProjectTest { stepsFromLastCovered = 2000L ) - val machine = TsMachine(scene, machineOptions, DEFAULT_TS_OPTIONS, machineObserver = ReachabilityObserver()) + val machine = TsMachine(scene, machineOptions, DEFAULT_TS_OPTIONS, machineObserver = TsReachabilityObserver()) val targets = createMemoryManagerTargets(memoryManagerClass) val results = machine.analyze(memoryMethods, targets) @@ -183,7 +183,7 @@ class SampleProjectTest { stepsFromLastCovered = 1000L ) - val observer = ReachabilityObserver() + val observer = TsReachabilityObserver() val machine = TsMachine(scene, machineOptions, DEFAULT_TS_OPTIONS, machineObserver = observer) // Create targets for different execution paths in array operations From d51875afad95256d05ebd9cf40752d00589d2292 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 17 Sep 2025 18:48:44 +0300 Subject: [PATCH 09/18] tmp --- .../org/usvm/reachability/cli/Reachability.kt | 310 +++++++----------- 1 file changed, 125 insertions(+), 185 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt b/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt index 455f175b65..968fbebf4d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt @@ -14,13 +14,6 @@ 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 kotlinx.serialization.json.JsonArray -import kotlinx.serialization.json.JsonElement -import kotlinx.serialization.json.JsonObject -import kotlinx.serialization.json.intOrNull -import kotlinx.serialization.json.jsonArray -import kotlinx.serialization.json.jsonObject -import kotlinx.serialization.json.jsonPrimitive import org.jacodb.ets.model.EtsIfStmt import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsReturnStmt @@ -36,6 +29,10 @@ import org.usvm.machine.TsOptions import org.usvm.machine.state.TsState import org.usvm.reachability.api.TsReachabilityObserver import org.usvm.reachability.api.TsReachabilityTarget +import org.usvm.reachability.dto.LocationDto +import org.usvm.reachability.dto.TargetDto +import org.usvm.reachability.dto.TargetTreeNodeDto +import org.usvm.reachability.dto.TargetType import org.usvm.reachability.dto.TargetsContainerDto import java.nio.file.Path import kotlin.io.path.Path @@ -191,15 +188,16 @@ class ReachabilityAnalyzer : CliktCommand( val methodsToAnalyze = findMethodsToAnalyze(scene) echo("šŸŽÆ Analyzing ${methodsToAnalyze.size} methods") - // Create targets - val targetDefinitions = if (targetsFile != null) { + // Create target traces (hierarchical intermediate structures) + val targetTraces = if (targetsFile != null) { parseTargetDefinitions(targetsFile!!) } else { generateDefaultTargets(methodsToAnalyze) } - val targets = createTargets(methodsToAnalyze, targetDefinitions) - echo("šŸ“ Created ${targets.size} reachability targets") + // Convert traces to resolved TsTarget hierarchies + val targets = createTargetsFromTraces(methodsToAnalyze, targetTraces) + echo("šŸ“ Created ${targets.size} reachability target trees from ${targetTraces.size} traces") // Run analysis echo("āš” Running reachability analysis...") @@ -211,7 +209,7 @@ class ReachabilityAnalyzer : CliktCommand( return ReachabilityResults( methods = methodsToAnalyze, targets = targets, - targetDefinitions = targetDefinitions, + targetTraces = targetTraces, states = states, reachabilityResults = reachabilityResults, scene = scene @@ -246,7 +244,7 @@ class ReachabilityAnalyzer : CliktCommand( } } - private fun parseTargetDefinitions(targetsFile: Path): List { + private fun parseTargetDefinitions(targetsFile: Path): List { val content = targetsFile.readText() return try { val json = Json { @@ -255,10 +253,10 @@ class ReachabilityAnalyzer : CliktCommand( } val targetsDto = json.decodeFromString(content) - val targetDefinitions = convertToDefinitions(targetsDto) + val traces = extractTargetTraces(targetsDto) - echo("šŸ“‹ Parsed ${targetDefinitions.size} target definitions from ${targetsFile.fileName}") - targetDefinitions + echo("šŸ“‹ Parsed ${traces.size} target traces from ${targetsFile.fileName}") + traces } catch (e: Exception) { echo("āŒ Error parsing targets file: ${e.message}", err = true) @@ -269,137 +267,79 @@ class ReachabilityAnalyzer : CliktCommand( } } - private fun convertToDefinitions(targetsDto: TargetsContainerDto) : List { - val result = mutableListOf() - - when (targetsDto) { + private fun extractTargetTraces(targetsDto: TargetsContainerDto): List { + return when (targetsDto) { is TargetsContainerDto.LinearTrace -> { - result += convertToDefinition(targetsDto.targets) + // Single linear trace + val rootNode = buildLinearTraceNode(targetsDto.targets) + listOfNotNull(rootNode?.let { TargetTrace(it) }) } - is TargetsContainerDto.TreeTrace -> TODO() + is TargetsContainerDto.TreeTrace -> { + // Single tree trace + val rootNode = buildTreeNode(targetsDto.target, targetsDto.children) + listOf(TargetTrace(rootNode)) + } - is TargetsContainerDto.TraceList -> TODO() + is TargetsContainerDto.TraceList -> { + // Multiple traces (can be linear or tree) + targetsDto.traces.flatMap { trace -> + extractTargetTraces(trace) + } + } } - - return result } - private fun parseJsonTargets(jsonElement: JsonElement): List { - return when (jsonElement) { - is JsonObject -> { - when { - // Linear trace format: { "targets": [...] } - jsonElement.containsKey("targets") -> { - val targetsArray = jsonElement["targets"]?.jsonArray - targetsArray?.mapNotNull { parseTargetFromJson(it) } ?: emptyList() - } - // Tree trace format: { "target": {...}, "children": [...] } - jsonElement.containsKey("target") -> { - val target = jsonElement["target"]?.let { parseTargetFromJson(it) } - val childrenTargets = jsonElement["children"]?.jsonArray?.let { children -> - children.flatMap { parseTargetsFromTreeNode(it) } - } ?: emptyList() - listOfNotNull(target) + childrenTargets - } + private fun buildLinearTraceNode(targets: List): TargetNode? { + if (targets.isEmpty()) return null - else -> emptyList() - } - } + // Build linear chain forwards using simple iteration + // Start from the last element and work backwards to build parent-child relationships + var currentNode: TargetNode? = null - is JsonArray -> { - // Array format: [ {...} ] - jsonElement.flatMap { element -> - when { - element is JsonObject && element.containsKey("targets") -> { - val targetsArray = element["targets"]?.jsonArray - targetsArray?.mapNotNull { parseTargetFromJson(it) } ?: emptyList() - } + // Build from end to start so each node can reference the next one as its child + for (i in targets.indices.reversed()) { + currentNode = TargetNode(targets[i], listOfNotNull(currentNode)) + } - element is JsonObject && element.containsKey("target") -> { - val target = element["target"]?.let { parseTargetFromJson(it) } - val childrenTargets = element["children"]?.jsonArray?.let { children -> - children.flatMap { parseTargetsFromTreeNode(it) } - } ?: emptyList() - listOfNotNull(target) + childrenTargets - } + return currentNode + } - else -> emptyList() - } - } - } + private fun buildTreeNode(targetDto: TargetDto, children: List): TargetNode { + val childNodes = children.map { buildTreeNodeFromDto(it) } - else -> emptyList() + return if (childNodes.isEmpty()) { + TargetNode(targetDto) + } else { + TargetNode(targetDto, childNodes) } } - private fun parseTargetsFromTreeNode(nodeElement: JsonElement): List { - val nodeObj = nodeElement.jsonObject - val target = nodeObj["target"]?.let { parseTargetFromJson(it) } - val childrenTargets = nodeObj["children"]?.jsonArray?.let { children -> - children.flatMap { parseTargetsFromTreeNode(it) } - } ?: emptyList() - return listOfNotNull(target) + childrenTargets - } + private fun buildTreeNodeFromDto(nodeDto: TargetTreeNodeDto): TargetNode { + val childNodes = nodeDto.children.map { buildTreeNodeFromDto(it) } - private fun parseTargetFromJson(jsonElement: JsonElement): TargetDefinition? { - return try { - val obj = jsonElement.jsonObject - val typeStr = obj["type"]?.jsonPrimitive?.content ?: "intermediate" - val location = obj["location"]?.jsonObject - - val type = when (typeStr.lowercase()) { - "initial" -> TargetType.INITIAL - "intermediate" -> TargetType.INTERMEDIATE - "final" -> TargetType.FINAL - else -> TargetType.INTERMEDIATE - } - - if (location != null) { - val fileName = location["fileName"]?.jsonPrimitive?.content ?: "" - val className = location["className"]?.jsonPrimitive?.content ?: "" - val methodName = location["methodName"]?.jsonPrimitive?.content ?: "" - val stmtType = location["stmtType"]?.jsonPrimitive?.content - val block = location["block"]?.jsonPrimitive?.intOrNull - val index = location["index"]?.jsonPrimitive?.intOrNull - - TargetDefinition( - type = type, - methodName = "$className.$methodName", - locationInfo = LocationInfo( - fileName = fileName, - className = className, - methodName = methodName, - stmtType = stmtType, - block = block, - index = index - ) - ) - } else { - null - } - } catch (_: Exception) { - null + return if (childNodes.isEmpty()) { + TargetNode(nodeDto.target) + } else { + TargetNode(nodeDto.target, childNodes) } } - private fun generateDefaultTargets(methods: List): List { - return methods.flatMap { method -> + private fun generateDefaultTargets(methods: List): List { + return methods.mapNotNull { method -> val statements = method.cfg.stmts - if (statements.isEmpty()) return@flatMap emptyList() + if (statements.isEmpty()) return@mapNotNull null val className = method.enclosingClass?.name ?: "Unknown" val methodName = method.name - val fullMethodName = "$className.$methodName" - val targets = mutableListOf() + val targets = mutableListOf() // Initial point - first statement targets.add( - TargetDefinition( + TargetDto( type = TargetType.INITIAL, - methodName = fullMethodName, - locationInfo = LocationInfo( + location = LocationDto( fileName = "$className.ts", className = className, methodName = methodName, @@ -415,16 +355,19 @@ class ReachabilityAnalyzer : CliktCommand( when (stmt) { is EtsIfStmt, is EtsReturnStmt -> { targets.add( - TargetDefinition( - type = if (stmt == statements.last()) TargetType.FINAL else TargetType.INTERMEDIATE, - methodName = fullMethodName, - locationInfo = LocationInfo( + TargetDto( + type = if (stmt == statements.last()) { + TargetType.FINAL + } else { + TargetType.INTERMEDIATE + }, + location = LocationDto( fileName = "$className.ts", className = className, methodName = methodName, stmtType = stmt.javaClass.simpleName, block = index / 10, // Estimate block from index - index = index + index = index, ) ) ) @@ -432,57 +375,58 @@ class ReachabilityAnalyzer : CliktCommand( } } - targets + // Create a linear trace for each method (each target follows the previous one) + buildLinearTraceNode(targets)?.let { root -> + TargetTrace(root) + } } } - private fun createTargets(methods: List, targetDefs: List): List { + private fun createTargetsFromTraces(methods: List, targetTraces: List): List { val targets = mutableListOf() val methodMap = methods.associateBy { "${it.enclosingClass?.name ?: "Unknown"}.${it.name}" } - // Group targets by method to build hierarchical structure - val targetsByMethod = targetDefs.groupBy { it.methodName } - - targetsByMethod.forEach { (methodName, methodTargets) -> + targetTraces.forEach { trace -> + // For each trace, find the corresponding method and build the target hierarchy + val methodName = "${trace.root.targetDto.location.className}.${trace.root.targetDto.location.methodName}" val method = methodMap[methodName] ?: return@forEach - val statements = method.cfg.stmts - - if (statements.isEmpty()) return@forEach - // Find initial target - val initialTarget = methodTargets.find { it.type == TargetType.INITIAL } - ?.let { targetDef -> - findStatementByDefinition(statements, targetDef)?.let { stmt -> - TsReachabilityTarget.InitialPoint(stmt) - } - } ?: return@forEach - - targets.add(initialTarget) - - // Build chain of intermediate and final targets - var currentTarget: TsTarget = initialTarget - methodTargets.filter { it.type != TargetType.INITIAL } - .sortedWith(compareBy { it.locationInfo.index ?: 0 }) - .forEach { targetDef -> - findStatementByDefinition(statements, targetDef)?.let { stmt -> - val target = when (targetDef.type) { - TargetType.INTERMEDIATE -> TsReachabilityTarget.IntermediatePoint(stmt) - TargetType.FINAL -> TsReachabilityTarget.FinalPoint(stmt) - else -> return@forEach - } - currentTarget = currentTarget.addChild(target) - } - } + // Resolve the root target and build the hierarchy using addChild + val rootTarget = resolveTargetNode(trace.root, method.cfg.stmts) + if (rootTarget != null) { + targets.add(rootTarget) + } } return targets } - private fun findStatementByDefinition( + private fun resolveTargetNode(node: TargetNode, statements: List): TsTarget? { + // First, resolve the current node to a TsReachabilityTarget + val stmt = findStatementByTargetDto(statements, node.targetDto) ?: return null + + val currentTarget = when (node.targetDto.type) { + TargetType.INITIAL -> TsReachabilityTarget.InitialPoint(stmt) + TargetType.INTERMEDIATE -> TsReachabilityTarget.IntermediatePoint(stmt) + TargetType.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 findStatementByTargetDto( statements: List, - targetDef: TargetDefinition, + targetDto: TargetDto, ): EtsStmt? { - val targetLocation = targetDef.locationInfo + val targetLocation = targetDto.location // Find statement by matching location properties statements.find { stmt -> @@ -499,7 +443,7 @@ class ReachabilityAnalyzer : CliktCommand( return statements.firstOrNull() } - private fun matchesLocation(stmt: EtsStmt, location: LocationInfo): Boolean { + private fun matchesLocation(stmt: EtsStmt, location: LocationDto): Boolean { // Match by statement type if specified location.stmtType?.let { expectedType -> val actualType = stmt.javaClass.simpleName @@ -693,39 +637,18 @@ class ReachabilityAnalyzer : CliktCommand( } } -// Enums and data classes enum class AnalysisMode { ALL_METHODS, PUBLIC_METHODS, - ENTRY_POINTS -} - -enum class TargetType { - INITIAL, - INTERMEDIATE, - FINAL + ENTRY_POINTS, } enum class ReachabilityStatus { REACHABLE, // Confirmed reachable with execution path UNREACHABLE, // Confirmed unreachable - UNKNOWN // Could not determine (timeout/approximation/error) + UNKNOWN, // Could not determine (timeout/approximation/error) } -data class LocationInfo( - val fileName: String, - val className: String, - val methodName: String, - val stmtType: String?, - val block: Int?, - val index: Int?, -) - -data class TargetDefinition( - val type: TargetType, - val locationInfo: LocationInfo, -) - data class ExecutionPath( val statements: List, ) @@ -739,12 +662,29 @@ data class TargetReachabilityResult( data class ReachabilityResults( val methods: List, val targets: List, - val targetDefinitions: List, + val targetTraces: List, val states: List, val reachabilityResults: List, val scene: EtsScene, ) +// Intermediate structures for building hierarchical targets before statement resolution +/** + * A hierarchical node representing a target with its children. + * Can represent linear chains (single child), trees (multiple children), or leaves (no children). + */ +data class TargetNode( + val targetDto: TargetDto, + val children: List = emptyList(), +) + +/** + * Represents a trace - an independent hierarchical structure of targets + */ +data class TargetTrace( + val root: TargetNode, +) + fun main(args: Array) { ReachabilityAnalyzer().main(args) } From ad281ececca5f223e3c3820fa57f49f003b227ed Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 17 Sep 2025 18:51:57 +0300 Subject: [PATCH 10/18] Format --- .../main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt | 2 +- usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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 bab7b4e6e9..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.TsTarget import org.usvm.api.typeStreamOf import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.forkblacklists.UForkBlackList 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 b72c6735cb..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.TsTarget import org.usvm.collections.immutable.getOrPut import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap import org.usvm.collections.immutable.internal.MutabilityOwnership From 1a9eabb36136379875e82b6913749f79eba6c4a5 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 18 Sep 2025 15:34:05 +0300 Subject: [PATCH 11/18] Comment --- .../src/main/kotlin/org/usvm/reachability/cli/Reachability.kt | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt b/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt index 968fbebf4d..1b5d7e3ab3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt @@ -668,7 +668,6 @@ data class ReachabilityResults( val scene: EtsScene, ) -// Intermediate structures for building hierarchical targets before statement resolution /** * A hierarchical node representing a target with its children. * Can represent linear chains (single child), trees (multiple children), or leaves (no children). @@ -679,7 +678,7 @@ data class TargetNode( ) /** - * Represents a trace - an independent hierarchical structure of targets + * Represents a trace - an independent hierarchical structure of targets. */ data class TargetTrace( val root: TargetNode, From 647eea20c05645c8c26a6f43884372e3b2e2c9ec Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 18 Sep 2025 16:44:42 +0300 Subject: [PATCH 12/18] Refine --- .../reachability}/TsReachabilityObserver.kt | 2 +- .../reachability}/TsReachabilityTarget.kt | 2 +- .../reachability/cli/Reachability.kt | 272 ++++++++++-------- .../{ => api}/reachability/dto/Targets.kt | 22 +- .../org/usvm/checkers/ReachabilityChecker.kt | 4 +- .../reachability/ArrayReachabilityTest.kt | 4 +- .../BasicConditionsReachabilityTest.kt | 4 +- .../reachability/ComplexReachabilityTest.kt | 4 +- .../FieldAccessReachabilityTest.kt | 4 +- .../FunctionCallReachabilityTest.kt | 4 +- .../usvm/reachability/SampleProjectTest.kt | 4 +- 11 files changed, 173 insertions(+), 153 deletions(-) rename usvm-ts/src/main/kotlin/org/usvm/{reachability/api => api/reachability}/TsReachabilityObserver.kt (97%) rename usvm-ts/src/main/kotlin/org/usvm/{reachability/api => api/reachability}/TsReachabilityTarget.kt (91%) rename usvm-ts/src/main/kotlin/org/usvm/{ => api}/reachability/cli/Reachability.kt (77%) rename usvm-ts/src/main/kotlin/org/usvm/{ => api}/reachability/dto/Targets.kt (84%) diff --git a/usvm-ts/src/main/kotlin/org/usvm/reachability/api/TsReachabilityObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/api/reachability/TsReachabilityObserver.kt similarity index 97% rename from usvm-ts/src/main/kotlin/org/usvm/reachability/api/TsReachabilityObserver.kt rename to usvm-ts/src/main/kotlin/org/usvm/api/reachability/TsReachabilityObserver.kt index c1d8db3d8c..4cec9ca818 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/reachability/api/TsReachabilityObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/reachability/TsReachabilityObserver.kt @@ -1,4 +1,4 @@ -package org.usvm.reachability.api +package org.usvm.api.reachability import org.usvm.machine.state.TsState import org.usvm.statistics.UMachineObserver diff --git a/usvm-ts/src/main/kotlin/org/usvm/reachability/api/TsReachabilityTarget.kt b/usvm-ts/src/main/kotlin/org/usvm/api/reachability/TsReachabilityTarget.kt similarity index 91% rename from usvm-ts/src/main/kotlin/org/usvm/reachability/api/TsReachabilityTarget.kt rename to usvm-ts/src/main/kotlin/org/usvm/api/reachability/TsReachabilityTarget.kt index b39b3d9923..1e7a24fd47 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/reachability/api/TsReachabilityTarget.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/reachability/TsReachabilityTarget.kt @@ -1,4 +1,4 @@ -package org.usvm.reachability.api +package org.usvm.api.reachability import org.jacodb.ets.model.EtsStmt import org.usvm.api.TsTarget diff --git a/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt b/usvm-ts/src/main/kotlin/org/usvm/api/reachability/cli/Reachability.kt similarity index 77% rename from usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt rename to usvm-ts/src/main/kotlin/org/usvm/api/reachability/cli/Reachability.kt index 1b5d7e3ab3..00598f9eae 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/reachability/cli/Reachability.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/reachability/cli/Reachability.kt @@ -1,4 +1,4 @@ -package org.usvm.reachability.cli +package org.usvm.api.reachability.cli import com.github.ajalt.clikt.core.CliktCommand import com.github.ajalt.clikt.core.context @@ -24,16 +24,16 @@ 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 org.usvm.reachability.api.TsReachabilityObserver -import org.usvm.reachability.api.TsReachabilityTarget -import org.usvm.reachability.dto.LocationDto -import org.usvm.reachability.dto.TargetDto -import org.usvm.reachability.dto.TargetTreeNodeDto -import org.usvm.reachability.dto.TargetType -import org.usvm.reachability.dto.TargetsContainerDto import java.nio.file.Path import kotlin.io.path.Path import kotlin.io.path.createDirectories @@ -188,17 +188,18 @@ class ReachabilityAnalyzer : CliktCommand( val methodsToAnalyze = findMethodsToAnalyze(scene) echo("šŸŽÆ Analyzing ${methodsToAnalyze.size} methods") - // Create target traces (hierarchical intermediate structures) - val targetTraces = if (targetsFile != null) { - parseTargetDefinitions(targetsFile!!) + // Prepare targets + val targets = if (targetsFile != null) { + val targetTraces = parseTargetDefinitions(targetsFile!!) + createTargetsFromTraces(methodsToAnalyze, targetTraces).also { + echo("šŸ“ Created ${it.size} reachability target trees from ${targetTraces.size} traces") + } } else { - generateDefaultTargets(methodsToAnalyze) + generateDefaultTargets(methodsToAnalyze).also { + echo("šŸ“ Generated ${it.size} default reachability targets") + } } - // Convert traces to resolved TsTarget hierarchies - val targets = createTargetsFromTraces(methodsToAnalyze, targetTraces) - echo("šŸ“ Created ${targets.size} reachability target trees from ${targetTraces.size} traces") - // Run analysis echo("āš” Running reachability analysis...") val states = machine.analyze(methodsToAnalyze, targets) @@ -209,7 +210,6 @@ class ReachabilityAnalyzer : CliktCommand( return ReachabilityResults( methods = methodsToAnalyze, targets = targets, - targetTraces = targetTraces, states = states, reachabilityResults = reachabilityResults, scene = scene @@ -252,8 +252,8 @@ class ReachabilityAnalyzer : CliktCommand( isLenient = true } - val targetsDto = json.decodeFromString(content) - val traces = extractTargetTraces(targetsDto) + val container = json.decodeFromString(content) + val traces = extractTargetTraces(container) echo("šŸ“‹ Parsed ${traces.size} target traces from ${targetsFile.fileName}") traces @@ -267,148 +267,112 @@ class ReachabilityAnalyzer : CliktCommand( } } - private fun extractTargetTraces(targetsDto: TargetsContainerDto): List { - return when (targetsDto) { - is TargetsContainerDto.LinearTrace -> { - // Single linear trace - val rootNode = buildLinearTraceNode(targetsDto.targets) - listOfNotNull(rootNode?.let { TargetTrace(it) }) - } - - is TargetsContainerDto.TreeTrace -> { - // Single tree trace - val rootNode = buildTreeNode(targetsDto.target, targetsDto.children) - listOf(TargetTrace(rootNode)) + 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 -> { - // Multiple traces (can be linear or tree) - targetsDto.traces.flatMap { trace -> - extractTargetTraces(trace) - } + container.traces.map { extractTargetTrace(it) } } } } - private fun buildLinearTraceNode(targets: List): TargetNode? { - if (targets.isEmpty()) return null - - // Build linear chain forwards using simple iteration - // Start from the last element and work backwards to build parent-child relationships - var currentNode: TargetNode? = null + private fun extractTargetTrace(trace: TargetsContainerDto.SingleTrace): TargetTrace { + return when (trace) { + // Single linear trace + is TargetsContainerDto.LinearTrace -> { + TargetTrace.Linear(targets = trace.targets.map { it.toDomain() }) + } - // Build from end to start so each node can reference the next one as its child - for (i in targets.indices.reversed()) { - currentNode = TargetNode(targets[i], listOfNotNull(currentNode)) + // Single tree trace + is TargetsContainerDto.TreeTrace -> { + TargetTrace.Tree(root = trace.root.toDomain()) + } } - - return currentNode } - private fun buildTreeNode(targetDto: TargetDto, children: List): TargetNode { - val childNodes = children.map { buildTreeNodeFromDto(it) } - - return if (childNodes.isEmpty()) { - TargetNode(targetDto) - } else { - TargetNode(targetDto, childNodes) - } - } + // TODO: remove + private fun buildLinearTrace(targets: List): TargetTreeNode? { + if (targets.isEmpty()) return null - private fun buildTreeNodeFromDto(nodeDto: TargetTreeNodeDto): TargetNode { - val childNodes = nodeDto.children.map { buildTreeNodeFromDto(it) } + var current: TargetTreeNode? = null - return if (childNodes.isEmpty()) { - TargetNode(nodeDto.target) - } else { - TargetNode(nodeDto.target, childNodes) + for (target in targets.asReversed()) { + current = TargetTreeNode(target, children = listOfNotNull(current)) } + + return current } - private fun generateDefaultTargets(methods: List): List { + private fun generateDefaultTargets(methods: List): List { return methods.mapNotNull { method -> val statements = method.cfg.stmts if (statements.isEmpty()) return@mapNotNull null - val className = method.enclosingClass?.name ?: "Unknown" - val methodName = method.name - - val targets = mutableListOf() - // Initial point - first statement - targets.add( - TargetDto( - type = TargetType.INITIAL, - location = LocationDto( - fileName = "$className.ts", - className = className, - methodName = methodName, - stmtType = statements.firstOrNull()?.javaClass?.simpleName, - block = 0, - index = 0 - ) - ) - ) + 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 -> { - targets.add( - TargetDto( - type = if (stmt == statements.last()) { - TargetType.FINAL - } else { - TargetType.INTERMEDIATE - }, - location = LocationDto( - fileName = "$className.ts", - className = className, - methodName = methodName, - stmtType = stmt.javaClass.simpleName, - block = index / 10, // Estimate block from index - index = index, - ) - ) - ) + val newTarget = if (index == statements.lastIndex) { + TsReachabilityTarget.FinalPoint(stmt) + } else { + TsReachabilityTarget.IntermediatePoint(stmt) + } + target = target.addChild(newTarget) } } } - // Create a linear trace for each method (each target follows the previous one) - buildLinearTraceNode(targets)?.let { root -> - TargetTrace(root) - } + initialTarget } } - private fun createTargetsFromTraces(methods: List, targetTraces: List): List { + private fun createTargetsFromTraces( + methods: List, + targetTraces: List, + ): List { val targets = mutableListOf() val methodMap = methods.associateBy { "${it.enclosingClass?.name ?: "Unknown"}.${it.name}" } targetTraces.forEach { trace -> - // For each trace, find the corresponding method and build the target hierarchy - val methodName = "${trace.root.targetDto.location.className}.${trace.root.targetDto.location.methodName}" - val method = methodMap[methodName] ?: return@forEach - - // Resolve the root target and build the hierarchy using addChild - val rootTarget = resolveTargetNode(trace.root, method.cfg.stmts) - if (rootTarget != null) { - targets.add(rootTarget) + when (trace) { + is TargetTrace.Linear -> { + + } + + is TargetTrace.Tree -> { + // For each trace, find the corresponding method and build the target hierarchy + val methodName = "${trace.root.target.location.className}.${trace.root.target.location.methodName}" + val method = methodMap[methodName] ?: return@forEach + + // Resolve the root target and build the hierarchy using addChild + val rootTarget = resolveTargetNode(trace.root, method.cfg.stmts) + if (rootTarget != null) { + targets.add(rootTarget) + } + } } } return targets } - private fun resolveTargetNode(node: TargetNode, statements: List): TsTarget? { + private fun resolveTargetNode(node: TargetTreeNode, statements: List): TsTarget? { // First, resolve the current node to a TsReachabilityTarget - val stmt = findStatementByTargetDto(statements, node.targetDto) ?: return null + val stmt = findStatementByTarget(statements, node.target) ?: return null - val currentTarget = when (node.targetDto.type) { - TargetType.INITIAL -> TsReachabilityTarget.InitialPoint(stmt) - TargetType.INTERMEDIATE -> TsReachabilityTarget.IntermediatePoint(stmt) - TargetType.FINAL -> TsReachabilityTarget.FinalPoint(stmt) + 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 @@ -422,11 +386,11 @@ class ReachabilityAnalyzer : CliktCommand( return currentTarget } - private fun findStatementByTargetDto( + private fun findStatementByTarget( statements: List, - targetDto: TargetDto, + target: Target, ): EtsStmt? { - val targetLocation = targetDto.location + val targetLocation = target.location // Find statement by matching location properties statements.find { stmt -> @@ -443,7 +407,7 @@ class ReachabilityAnalyzer : CliktCommand( return statements.firstOrNull() } - private fun matchesLocation(stmt: EtsStmt, location: LocationDto): Boolean { + private fun matchesLocation(stmt: EtsStmt, location: Location): Boolean { // Match by statement type if specified location.stmtType?.let { expectedType -> val actualType = stmt.javaClass.simpleName @@ -662,26 +626,80 @@ data class TargetReachabilityResult( data class ReachabilityResults( val methods: List, val targets: List, - val targetTraces: List, val states: List, val reachabilityResults: List, val scene: EtsScene, ) +private fun TargetDto.toDomain(): Target { + return Target( + type = this.type.toDomain(), + location = this.location.toDomain(), + ) +} + +// TODO: replace return type with domain and fix the mapping +private fun TargetTypeDto.toDomain(): TargetTypeDto { + return when (this) { + TargetTypeDto.INITIAL -> TargetTypeDto.INITIAL + TargetTypeDto.INTERMEDIATE -> TargetTypeDto.INTERMEDIATE + TargetTypeDto.FINAL -> TargetTypeDto.FINAL + } +} + +private fun LocationDto.toDomain(): Location { + return Location( + fileName = this.fileName, + className = this.className, + methodName = this.methodName, + stmtType = this.stmtType, + block = this.block, + index = this.index, + ) +} + +private fun TargetTreeNodeDto.toDomain(): TargetTreeNode { + return TargetTreeNode( + target = this.target.toDomain(), + children = this.children.map { it.toDomain() }, + ) +} + +/** + * Represents a trace - an independent hierarchical structure of targets. + */ +sealed interface TargetTrace { + data class Linear(val targets: List) : TargetTrace + data class Tree(val root: TargetTreeNode) : TargetTrace +} + /** * A hierarchical node representing a target with its children. * Can represent linear chains (single child), trees (multiple children), or leaves (no children). */ -data class TargetNode( - val targetDto: TargetDto, - val children: List = emptyList(), +data class TargetTreeNode( + val target: Target, + val children: List = emptyList(), ) /** - * Represents a trace - an independent hierarchical structure of targets. + * A specific target point in the code with its location. + */ +data class Target( + val type: TargetTypeDto, // TODO: domain enum + val location: Location, +) + +/** + * Location details of a target point in the code. */ -data class TargetTrace( - val root: TargetNode, +data class Location( + val fileName: String?, + val className: String?, + val methodName: String?, + val stmtType: String?, + val block: Int?, + val index: Int?, ) fun main(args: Array) { diff --git a/usvm-ts/src/main/kotlin/org/usvm/reachability/dto/Targets.kt b/usvm-ts/src/main/kotlin/org/usvm/api/reachability/dto/Targets.kt similarity index 84% rename from usvm-ts/src/main/kotlin/org/usvm/reachability/dto/Targets.kt rename to usvm-ts/src/main/kotlin/org/usvm/api/reachability/dto/Targets.kt index 6b2ac26acc..14c871bd67 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/reachability/dto/Targets.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/reachability/dto/Targets.kt @@ -1,4 +1,4 @@ -package org.usvm.reachability.dto +package org.usvm.api.reachability.dto import kotlinx.serialization.DeserializationStrategy import kotlinx.serialization.SerialName @@ -31,11 +31,10 @@ sealed interface TargetsContainerDto { val targets: List, ) : SingleTrace - // Format: { "target": {...}, "children": [...] } + // Format: { "root": {...} } @Serializable data class TreeTrace( - val target: TargetDto, - val children: List = emptyList(), + val root: TargetTreeNodeDto, ) : SingleTrace // Format: [ {...} ] @@ -47,13 +46,14 @@ sealed interface 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 "target" field: { "target": {...}, "children": [...] } - element is JsonObject && element.containsKey("target") -> TargetsContainerDto.TreeTrace.serializer() + // Object with "root" field: { "root": {...} } + element is JsonObject && element.containsKey("root") -> TargetsContainerDto.TreeTrace.serializer() else -> error("Unknown single trace format") } @@ -62,7 +62,9 @@ object SingleTraceSerializer : selectDeserializer(element) as DeserializationStrategy } -object TargetsContainerSerializer : JsonContentPolymorphicSerializer(TargetsContainerDto::class) { +object TargetsContainerSerializer : + JsonContentPolymorphicSerializer(TargetsContainerDto::class) { + override fun selectDeserializer(element: JsonElement): DeserializationStrategy = when { // Array at top level: [ {...} ] element is JsonArray -> TargetsContainerDto.TraceList.serializer() @@ -79,7 +81,7 @@ data class TargetTreeNodeDto( ) @Serializable -enum class TargetType { +enum class TargetTypeDto { @SerialName("initial") INITIAL, @@ -87,12 +89,12 @@ enum class TargetType { INTERMEDIATE, @SerialName("final") - FINAL + FINAL, } @Serializable data class TargetDto( - val type: TargetType = TargetType.INTERMEDIATE, + val type: TargetTypeDto = TargetTypeDto.INTERMEDIATE, val location: LocationDto, // TODO: consider inlining ) 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 657d00a1d2..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.reachability.api.TsReachabilityObserver -import org.usvm.reachability.api.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 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 47e57a0095..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,9 +8,9 @@ import org.junit.jupiter.api.Disabled import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.UMachineOptions -import org.usvm.reachability.api.TsReachabilityObserver -import org.usvm.reachability.api.TsReachabilityTarget 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 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 c86276c5ad..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.reachability.api.TsReachabilityObserver -import org.usvm.reachability.api.TsReachabilityTarget 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 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 25e5bce488..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.reachability.api.TsReachabilityObserver -import org.usvm.reachability.api.TsReachabilityTarget 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 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 edbc713461..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.reachability.api.TsReachabilityObserver -import org.usvm.reachability.api.TsReachabilityTarget 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 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 cbcb852c19..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.reachability.api.TsReachabilityObserver -import org.usvm.reachability.api.TsReachabilityTarget 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 diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt index da8fe1ca99..e2822b46af 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/SampleProjectTest.kt @@ -9,9 +9,9 @@ import org.junit.jupiter.api.Test import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.UMachineOptions -import org.usvm.reachability.api.TsReachabilityObserver -import org.usvm.reachability.api.TsReachabilityTarget 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 From 8aeab90ffa995db6668a0dd08a6d1021ff571922 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 18 Sep 2025 17:37:09 +0300 Subject: [PATCH 13/18] Refine --- .../usvm/api/reachability/cli/Reachability.kt | 120 ++++-------------- 1 file changed, 27 insertions(+), 93 deletions(-) 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 index 00598f9eae..a83e95f183 100644 --- 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 @@ -191,13 +191,13 @@ class ReachabilityAnalyzer : CliktCommand( // Prepare targets val targets = if (targetsFile != null) { val targetTraces = parseTargetDefinitions(targetsFile!!) - createTargetsFromTraces(methodsToAnalyze, targetTraces).also { - echo("šŸ“ Created ${it.size} reachability target trees from ${targetTraces.size} traces") - } + val targets = createTargetsFromTraces(methodsToAnalyze, targetTraces) + echo("šŸ“ Created ${targets.size} reachability target trees from ${targetTraces.size} traces") + targets } else { - generateDefaultTargets(methodsToAnalyze).also { - echo("šŸ“ Generated ${it.size} default reachability targets") - } + val targets = generateDefaultTargets(methodsToAnalyze) + echo("šŸ“ Generated ${targets.size} default reachability targets") + targets } // Run analysis @@ -285,24 +285,24 @@ class ReachabilityAnalyzer : CliktCommand( return when (trace) { // Single linear trace is TargetsContainerDto.LinearTrace -> { - TargetTrace.Linear(targets = trace.targets.map { it.toDomain() }) + TargetTrace.Linear(targets = trace.targets) } // Single tree trace is TargetsContainerDto.TreeTrace -> { - TargetTrace.Tree(root = trace.root.toDomain()) + TargetTrace.Tree(root = trace.root) } } } // TODO: remove - private fun buildLinearTrace(targets: List): TargetTreeNode? { + private fun buildLinearTrace(targets: List): TargetTreeNodeDto? { if (targets.isEmpty()) return null - var current: TargetTreeNode? = null + var current: TargetTreeNodeDto? = null for (target in targets.asReversed()) { - current = TargetTreeNode(target, children = listOfNotNull(current)) + current = TargetTreeNodeDto(target, children = listOfNotNull(current)) } return current @@ -343,29 +343,26 @@ class ReachabilityAnalyzer : CliktCommand( val methodMap = methods.associateBy { "${it.enclosingClass?.name ?: "Unknown"}.${it.name}" } targetTraces.forEach { trace -> - when (trace) { - is TargetTrace.Linear -> { - - } + val root = when (trace) { + is TargetTrace.Tree -> trace.root + is TargetTrace.Linear -> buildLinearTrace(trace.targets)!! + } - is TargetTrace.Tree -> { - // For each trace, find the corresponding method and build the target hierarchy - val methodName = "${trace.root.target.location.className}.${trace.root.target.location.methodName}" - val method = methodMap[methodName] ?: return@forEach + // 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(trace.root, method.cfg.stmts) - if (rootTarget != null) { - targets.add(rootTarget) - } - } + // 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: TargetTreeNode, statements: List): TsTarget? { + private fun resolveTargetNode(node: TargetTreeNodeDto, statements: List): TsTarget? { // First, resolve the current node to a TsReachabilityTarget val stmt = findStatementByTarget(statements, node.target) ?: return null @@ -388,7 +385,7 @@ class ReachabilityAnalyzer : CliktCommand( private fun findStatementByTarget( statements: List, - target: Target, + target: TargetDto, ): EtsStmt? { val targetLocation = target.location @@ -407,7 +404,7 @@ class ReachabilityAnalyzer : CliktCommand( return statements.firstOrNull() } - private fun matchesLocation(stmt: EtsStmt, location: Location): Boolean { + private fun matchesLocation(stmt: EtsStmt, location: LocationDto): Boolean { // Match by statement type if specified location.stmtType?.let { expectedType -> val actualType = stmt.javaClass.simpleName @@ -631,77 +628,14 @@ data class ReachabilityResults( val scene: EtsScene, ) -private fun TargetDto.toDomain(): Target { - return Target( - type = this.type.toDomain(), - location = this.location.toDomain(), - ) -} - -// TODO: replace return type with domain and fix the mapping -private fun TargetTypeDto.toDomain(): TargetTypeDto { - return when (this) { - TargetTypeDto.INITIAL -> TargetTypeDto.INITIAL - TargetTypeDto.INTERMEDIATE -> TargetTypeDto.INTERMEDIATE - TargetTypeDto.FINAL -> TargetTypeDto.FINAL - } -} - -private fun LocationDto.toDomain(): Location { - return Location( - fileName = this.fileName, - className = this.className, - methodName = this.methodName, - stmtType = this.stmtType, - block = this.block, - index = this.index, - ) -} - -private fun TargetTreeNodeDto.toDomain(): TargetTreeNode { - return TargetTreeNode( - target = this.target.toDomain(), - children = this.children.map { it.toDomain() }, - ) -} - /** * Represents a trace - an independent hierarchical structure of targets. */ sealed interface TargetTrace { - data class Linear(val targets: List) : TargetTrace - data class Tree(val root: TargetTreeNode) : TargetTrace + data class Linear(val targets: List) : TargetTrace + data class Tree(val root: TargetTreeNodeDto) : TargetTrace } -/** - * A hierarchical node representing a target with its children. - * Can represent linear chains (single child), trees (multiple children), or leaves (no children). - */ -data class TargetTreeNode( - val target: Target, - val children: List = emptyList(), -) - -/** - * A specific target point in the code with its location. - */ -data class Target( - val type: TargetTypeDto, // TODO: domain enum - val location: Location, -) - -/** - * Location details of a target point in the code. - */ -data class Location( - val fileName: String?, - val className: String?, - val methodName: String?, - val stmtType: String?, - val block: Int?, - val index: Int?, -) - fun main(args: Array) { ReachabilityAnalyzer().main(args) } From 4eb516ace2a5161561634fb652bbc20a0a95184d Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 18 Sep 2025 18:30:25 +0300 Subject: [PATCH 14/18] Allow dist exec mode --- examples/reachability/reachability-cli.sh | 114 +++++++++++++++------- usvm-ts/build.gradle.kts | 18 ++++ 2 files changed, 98 insertions(+), 34 deletions(-) diff --git a/examples/reachability/reachability-cli.sh b/examples/reachability/reachability-cli.sh index 6f1aec2299..d5fc3e27e1 100755 --- a/examples/reachability/reachability-cli.sh +++ b/examples/reachability/reachability-cli.sh @@ -19,6 +19,7 @@ STEPS=3500 VERBOSE=false INCLUDE_STATEMENTS=false METHOD_FILTER="" +EXECUTION_MODE="shadow" # Options: shadow, dist # Colors for output RED='\033[0;31m' @@ -43,16 +44,24 @@ usage() { 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" + echo " # Analyze all public methods in a TypeScript project (using shadow JAR)" echo " $0 -p ./my-typescript-project" echo "" - echo " # Use custom targets and verbose output" - echo " $0 -p ./my-project -t ./targets.json -v" + 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" @@ -93,6 +102,18 @@ while [[ $# -gt 0 ]]; do 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 @@ -131,62 +152,87 @@ echo "šŸ“ Project: $PROJECT_PATH" echo "šŸ“„ Output: $OUTPUT_DIR" echo "šŸ” Mode: $MODE" echo "āš™ļø Solver: $SOLVER" +echo "šŸ“¦ Execution mode: $EXECUTION_MODE" -# 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 - -# Build the command arguments -JAVA_ARGS=() -JAVA_ARGS+=("--project" "$PROJECT_PATH") -JAVA_ARGS+=("--output" "$OUTPUT_DIR") -JAVA_ARGS+=("--mode" "$MODE") -JAVA_ARGS+=("--solver" "$SOLVER") -JAVA_ARGS+=("--timeout" "$TIMEOUT") -JAVA_ARGS+=("--steps" "$STEPS") +# 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 - JAVA_ARGS+=("--targets" "$TARGETS_FILE") + CMD_ARGS+=("--targets" "$TARGETS_FILE") echo "šŸ“‹ Targets: $TARGETS_FILE" fi if [[ -n "$METHOD_FILTER" ]]; then - JAVA_ARGS+=("--method" "$METHOD_FILTER") + CMD_ARGS+=("--method" "$METHOD_FILTER") echo "šŸŽÆ Method filter: $METHOD_FILTER" fi if [[ "$VERBOSE" == true ]]; then - JAVA_ARGS+=("--verbose") + CMD_ARGS+=("--verbose") echo "šŸ“ Verbose mode enabled" fi if [[ "$INCLUDE_STATEMENTS" == true ]]; then - JAVA_ARGS+=("--include-statements") + CMD_ARGS+=("--include-statements") echo "šŸ“ Including statement details" fi echo "" echo -e "${YELLOW}āš” Running analysis...${NC}" -# Execute the analysis -java -Dfile.encoding=UTF-8 \ - -Dsun.stdout.encoding=UTF-8 \ - -cp "$JAR_PATH" \ - org.usvm.reachability.cli.ReachabilityKt \ - "${JAVA_ARGS[@]}" +# 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.reachability.cli.ReachabilityKt \ + "${CMD_ARGS[@]}" +fi echo "" echo -e "${GREEN}āœ… Analysis complete! Check the results in: $OUTPUT_DIR${NC}" diff --git a/usvm-ts/build.gradle.kts b/usvm-ts/build.gradle.kts index d9dec8f2a5..0f418fa7a8 100644 --- a/usvm-ts/build.gradle.kts +++ b/usvm-ts/build.gradle.kts @@ -9,6 +9,7 @@ import kotlin.time.Duration plugins { id("usvm.kotlin-conventions") kotlin("plugin.serialization") version Versions.kotlin + application id(Plugins.Shadow) } @@ -36,6 +37,23 @@ dependencies { testImplementation("org.burningwave:core:12.62.7") } +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("") From e4d2f78980b1862b13e2f3fbc5f1cd26dce36ada Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 18 Sep 2025 19:15:10 +0300 Subject: [PATCH 15/18] Customize application --- usvm-ts/build.gradle.kts | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/usvm-ts/build.gradle.kts b/usvm-ts/build.gradle.kts index 0f418fa7a8..653999d199 100644 --- a/usvm-ts/build.gradle.kts +++ b/usvm-ts/build.gradle.kts @@ -37,6 +37,11 @@ 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 From fc62497d6b86a64474b399a19ac448a2ec2b5b7b Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 18 Sep 2025 19:15:17 +0300 Subject: [PATCH 16/18] Fix package --- examples/reachability/reachability-cli.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/reachability/reachability-cli.sh b/examples/reachability/reachability-cli.sh index d5fc3e27e1..058796660c 100755 --- a/examples/reachability/reachability-cli.sh +++ b/examples/reachability/reachability-cli.sh @@ -230,7 +230,7 @@ else java -Dfile.encoding=UTF-8 \ -Dsun.stdout.encoding=UTF-8 \ -cp "$JAR_PATH" \ - org.usvm.reachability.cli.ReachabilityKt \ + org.usvm.api.reachability.cli.ReachabilityKt \ "${CMD_ARGS[@]}" fi From d32d67ed6db9d0a654a886a18496de9d5008df7a Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 18 Sep 2025 19:22:24 +0300 Subject: [PATCH 17/18] Filter out closures from analysis --- usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt | 5 +++++ 1 file changed, 5 insertions(+) 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 0d42bfd582..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 @@ -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) } From f9c06546d44c47a460837588f2f19d331a776973 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 18 Sep 2025 19:27:58 +0300 Subject: [PATCH 18/18] Fix space --- .../main/kotlin/org/usvm/api/reachability/cli/Reachability.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 index a83e95f183..414887595d 100644 --- 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 @@ -488,7 +488,7 @@ class ReachabilityAnalyzer : CliktCommand( reportFile.writeText(buildString { appendLine("šŸŽÆ REACHABILITY ANALYSIS SUMMARY") appendLine("=".repeat(50)) - appendLine("ā±ļø Duration: ${String.format("%.2f", duration)}s") + appendLine("ā±ļø Duration: ${String.format("%.2f", duration)}s") appendLine("šŸ” Methods analyzed: ${results.methods.size}") appendLine("šŸ“ Targets analyzed: ${results.reachabilityResults.size}")