From fd89ee96042b9d5cb79565de9fd5ef7bf25788cc Mon Sep 17 00:00:00 2001 From: hunterbrightdesign <70662742+hunterbrightdesign@users.noreply.github.com> Date: Tue, 25 Feb 2025 14:28:55 +0100 Subject: [PATCH 1/9] reel temp docker exec --- dynamic_trace.sh | 27 +++++++++++++--- install.sh | 81 ++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 104 insertions(+), 4 deletions(-) diff --git a/dynamic_trace.sh b/dynamic_trace.sh index 3c1a1ef..be33423 100755 --- a/dynamic_trace.sh +++ b/dynamic_trace.sh @@ -413,6 +413,7 @@ EOF return 0 } + # Function to convert Python to C using LLM with multiple attempts convert_to_c() { local input_file="$SCRIPT_PYTHON" @@ -486,8 +487,15 @@ convert_to_c() { while [ $attempt -le $max_attempts ] && [ "$success" = false ]; do echo "Attempt $attempt of $max_attempts to generate valid C code..." + if command -v timeout >/dev/null 2>&1; then + TIMEOUT_CMD="timeout" + elif command -v gtimeout >/dev/null 2>&1; then + TIMEOUT_CMD="gtimeout" + else + TIMEOUT_CMD="" +fi # Run aider to modify the C file (with a timeout) - timeout 180 aider --no-git --no-show-model-warnings --model "$LLM_MODEL" --yes \ + $TIMEOUT_CMD 180 aider --no-git --no-show-model-warnings --model "$LLM_MODEL" --yes \ --message-file "$TEMP_PROMPT" --file "$output_file" || true # Show the output file contents for debugging @@ -497,11 +505,20 @@ convert_to_c() { # Check if the generated C code is valid if [ "$USE_DOCKER" = true ]; then echo "Checking C syntax in Docker..." - if docker exec "$CONTAINER_ID" esbmc --parse-tree-only "/workspace/$C_FILE_NAME" 2>/dev/null; then + if [ "$USE_DOCKER" = true ]; then + CMDRUN="docker run --rm -v $(pwd):/workspace -w /workspace $DOCKER_IMAGE esbmc" + else + CMDRUN="docker exec "$CONTAINER_ID" esbmc" + fi + + $CMDRUN --parse-tree-only "/workspace/$C_FILE_NAME" + result=$? + + if [ $result -eq 0 ]; then echo "✅ Successfully generated valid C code on attempt $attempt" success=true else - echo "❌ ESBMC parse tree check failed on attempt $attempt" + echo "❌ ESBMC parse tree check failed on attempt $attempt Docker" if [ $attempt -lt $max_attempts ]; then echo "Retrying with additional instructions..." # Add more specific instructions to fix syntax errors @@ -514,7 +531,9 @@ convert_to_c() { fi else # Local ESBMC - if esbmc --parse-tree-only "$output_file" 2>/dev/null; then + esbmc --parse-tree-only "$output_file" + result=$? + if [ $result -eq 0 ]; then echo "✅ Successfully generated valid C code on attempt $attempt" success=true else diff --git a/install.sh b/install.sh index 718c20b..ccd51cd 100755 --- a/install.sh +++ b/install.sh @@ -18,6 +18,87 @@ check_rpm_package() { return $? } +install_timeout() { + echo "🔍 Checking for 'timeout' command..." + + # Check if timeout is available + if command -v timeout >/dev/null 2>&1; then + echo "✅ 'timeout' is already installed." + return + fi + + # macOS: Install GNU coreutils for timeout + if [[ "$OSTYPE" == "darwin"* ]]; then + echo "🍏 Detected macOS: Installing GNU coreutils..." + if ! command -v brew >/dev/null 2>&1; then + echo "🚨 Homebrew not found! Installing Homebrew first..." + /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)" + fi + brew install coreutils + export PATH="$(brew --prefix coreutils)/libexec/gnubin:$PATH" + echo "✅ Installed 'gtimeout' as 'timeout'." + return + fi + + # Linux: Install coreutils package + if [[ "$OSTYPE" == "linux-gnu"* ]]; then + echo "🐧 Detected Linux: Installing coreutils..." + if command -v apt-get >/dev/null 2>&1; then + sudo apt-get update && sudo apt-get install -y coreutils + elif command -v dnf >/dev/null 2>&1; then + sudo dnf install -y coreutils + elif command -v pacman >/dev/null 2>&1; then + sudo pacman -S --noconfirm coreutils + else + echo "❌ Unsupported Linux package manager. Please install 'coreutils' manually." + exit 1 + fi + echo "✅ Installed 'timeout'." + return + fi + + # Windows: Install GNU coreutils in WSL (if available) + if [[ "$OSTYPE" == "msys" || "$OSTYPE" == "cygwin" ]]; then + echo "🪟 Detected Windows (WSL/Cygwin): Installing coreutils..." + if command -v apt-get >/dev/null 2>&1; then + sudo apt-get update && sudo apt-get install -y coreutils + else + echo "❌ Cannot install coreutils automatically. Please install manually from https://gnuwin32.sourceforge.net/packages/coreutils.htm" + exit 1 + fi + echo "✅ Installed 'timeout'." + return + fi + + echo "❌ Could not detect a supported operating system." + exit 1 +} + +check_timeout() { + echo "🔍 Checking if 'timeout' works..." + + # Test timeout command with a simple sleep + if timeout 1 sleep 2 >/dev/null 2>&1; then + echo "✅ 'timeout' works correctly." + return 0 + fi + + # macOS: Check if gtimeout is available + if gtimeout 1 sleep 2 >/dev/null 2>&1; then + echo "✅ 'gtimeout' (GNU timeout) works correctly." + export TIMEOUT_CMD="gtimeout" + return 0 + fi + + # If timeout is missing or not working, return failure + echo "⚠️ 'timeout' is missing or not working." + return 1 +} + +if ! check_timeout; then + install_timeout +fi + # Detect operating system if [[ "$OSTYPE" == "darwin"* ]]; then # macOS From 0f3f8fdea229f2256b46f3c3e167988da9a655a2 Mon Sep 17 00:00:00 2001 From: hunterbrightdesign <70662742+hunterbrightdesign@users.noreply.github.com> Date: Tue, 25 Feb 2025 18:49:30 +0100 Subject: [PATCH 2/9] correct run esbmc docker --- dynamic_trace.sh | 33 ++++++++++++++++++++------------- 1 file changed, 20 insertions(+), 13 deletions(-) diff --git a/dynamic_trace.sh b/dynamic_trace.sh index be33423..a17e687 100755 --- a/dynamic_trace.sh +++ b/dynamic_trace.sh @@ -476,11 +476,11 @@ convert_to_c() { # Use existing container docker exec "$CONTAINER_ID" mkdir -p /workspace debug_log "Using existing container: $CONTAINER_ID" - else - # Start a new container - CONTAINER_ID=$(docker run -d --rm -v "$TEMP_DIR":/workspace -w /workspace "$DOCKER_IMAGE" sleep 3600) - debug_log "Started new container: $CONTAINER_ID" - echo "🐳 Docker container started: $CONTAINER_ID (mounted $TEMP_DIR as /workspace)" + # else + # # Start a new container + # CONTAINER_ID=$(docker run -d --rm -v "$TEMP_DIR":/workspace -w /workspace "$DOCKER_IMAGE" sleep 3600) + # debug_log "Started new container: $CONTAINER_ID" + # echo "🐳 Docker container started: $CONTAINER_ID (mounted $TEMP_DIR as /workspace)" fi fi @@ -493,7 +493,7 @@ convert_to_c() { TIMEOUT_CMD="gtimeout" else TIMEOUT_CMD="" -fi + fi # Run aider to modify the C file (with a timeout) $TIMEOUT_CMD 180 aider --no-git --no-show-model-warnings --model "$LLM_MODEL" --yes \ --message-file "$TEMP_PROMPT" --file "$output_file" || true @@ -504,21 +504,28 @@ fi # Check if the generated C code is valid if [ "$USE_DOCKER" = true ]; then - echo "Checking C syntax in Docker..." - if [ "$USE_DOCKER" = true ]; then - CMDRUN="docker run --rm -v $(pwd):/workspace -w /workspace $DOCKER_IMAGE esbmc" + + filename=$(basename "$output_file") + output_dir=$(dirname "$output_file") + + # Montez le répertoire spécifique qui contient le fichier + if [ -n "$CONTAINER_ID" ]; then + # Pour un conteneur existant, copiez le fichier à l'intérieur + docker cp "$output_file" "$CONTAINER_ID:/workspace/$filename" + docker exec $CONTAINER_ID esbmc --parse-tree-only "/workspace/$filename" + result=$? else - CMDRUN="docker exec "$CONTAINER_ID" esbmc" + # Pour un nouveau conteneur, montez le répertoire contenant le fichier + docker run --rm -v "$output_dir:/workspace" $DOCKER_IMAGE esbmc --parse-tree-only "/workspace/$filename" + result=$? fi - $CMDRUN --parse-tree-only "/workspace/$C_FILE_NAME" - result=$? if [ $result -eq 0 ]; then echo "✅ Successfully generated valid C code on attempt $attempt" success=true else - echo "❌ ESBMC parse tree check failed on attempt $attempt Docker" + echo "❌ ESBMC parse tree check failed on attempt $attempt " if [ $attempt -lt $max_attempts ]; then echo "Retrying with additional instructions..." # Add more specific instructions to fix syntax errors From 76df5cc49fcde4d293343c795875e87b2e736f5f Mon Sep 17 00:00:00 2001 From: hunterbrightdesign <70662742+hunterbrightdesign@users.noreply.github.com> Date: Wed, 26 Feb 2025 18:30:34 +0100 Subject: [PATCH 3/9] pr --- dynamic_trace.sh | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/dynamic_trace.sh b/dynamic_trace.sh index a17e687..1f36338 100755 --- a/dynamic_trace.sh +++ b/dynamic_trace.sh @@ -441,6 +441,7 @@ convert_to_c() { echo "3. Use equivalent C data structures and types" echo "4. Include necessary headers and dependencies" echo "5. Only output proper C code that can be parsed by a C compiler" + cat "$SOURCE_INSTRUCTION_FILE" # Add list of functions we detected to focus on echo -e "\nImplement these functions identified during execution:" @@ -515,8 +516,10 @@ convert_to_c() { docker exec $CONTAINER_ID esbmc --parse-tree-only "/workspace/$filename" result=$? else + echo "❌ Run in docker $TEMP_DIR " + echo "❌ Run in docker $TEMP_DIR " # Pour un nouveau conteneur, montez le répertoire contenant le fichier - docker run --rm -v "$output_dir:/workspace" $DOCKER_IMAGE esbmc --parse-tree-only "/workspace/$filename" + docker run --rm -v $(pwd):/workspace -w /workspace "$DOCKER_IMAGE" esbmc --parse-tree-only "$filename" result=$? fi @@ -585,7 +588,7 @@ run_esbmc_for_function() { function_name="main" fi - local current_cmd="esbmc --function $function_name $C_FILE_NAME" + local current_cmd="esbmc --function $function_name \"$C_OUTPUT\"" echo "----------------------------------------" echo "🛠️ Testing function: $function_name" From cc9e72ebba69f45a03bbfcfe371dacd1e67026cb Mon Sep 17 00:00:00 2001 From: hunterbrightdesign <70662742+hunterbrightdesign@users.noreply.github.com> Date: Wed, 26 Feb 2025 18:38:01 +0100 Subject: [PATCH 4/9] pr --- dynamic_trace.sh | 2 -- 1 file changed, 2 deletions(-) diff --git a/dynamic_trace.sh b/dynamic_trace.sh index 1f36338..36d6a34 100755 --- a/dynamic_trace.sh +++ b/dynamic_trace.sh @@ -516,8 +516,6 @@ convert_to_c() { docker exec $CONTAINER_ID esbmc --parse-tree-only "/workspace/$filename" result=$? else - echo "❌ Run in docker $TEMP_DIR " - echo "❌ Run in docker $TEMP_DIR " # Pour un nouveau conteneur, montez le répertoire contenant le fichier docker run --rm -v $(pwd):/workspace -w /workspace "$DOCKER_IMAGE" esbmc --parse-tree-only "$filename" result=$? From 7416af8ec5fa4176caa4e6a9b8ae0d5a6f56b9eb Mon Sep 17 00:00:00 2001 From: hunterbrightdesign <70662742+hunterbrightdesign@users.noreply.github.com> Date: Fri, 28 Feb 2025 23:42:37 +0100 Subject: [PATCH 5/9] add installation commands in the output --- dynamic_trace.sh | 217 +++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 208 insertions(+), 9 deletions(-) diff --git a/dynamic_trace.sh b/dynamic_trace.sh index 36d6a34..635cac2 100755 --- a/dynamic_trace.sh +++ b/dynamic_trace.sh @@ -99,6 +99,213 @@ extract_function_calls() { sort -u > "$FUNCTIONS_FILE" } +# Wrapper function to assist with automatic dependency installation +aider_wrapper() { + local message_file="$1" + local output_file="$2" + local model="$3" + + # Temporary file to store the output + local TEMP_OUTPUT=$(mktemp) + + # Detect the operating system + OS="unknown" + if [[ "$OSTYPE" == "linux-gnu"* ]]; then + OS="linux" + elif [[ "$OSTYPE" == "darwin"* ]]; then + OS="macos" + elif [[ "$OSTYPE" == "msys" || "$OSTYPE" == "win32" || "$OSTYPE" == "cygwin" ]]; then + OS="windows" + fi + + debug_log "Detected operating system: $OS" + + # Check if a package manager is available + has_brew=false + has_apt=false + has_dnf=false + has_yum=false + has_pacman=false + has_choco=false + has_scoop=false + has_npm=false + has_pip=false + has_gem=false + has_cargo=false + + if command -v brew &> /dev/null; then + has_brew=true + fi + if command -v apt-get &> /dev/null; then + has_apt=true + fi + if command -v dnf &> /dev/null; then + has_dnf=true + fi + if command -v yum &> /dev/null; then + has_yum=true + fi + if command -v pacman &> /dev/null; then + has_pacman=true + fi + if command -v choco &> /dev/null; then + has_choco=true + fi + if command -v scoop &> /dev/null; then + has_scoop=true + fi + if command -v npm &> /dev/null; then + has_npm=true + fi + if command -v pip &> /dev/null || command -v pip3 &> /dev/null; then + has_pip=true + fi + if command -v gem &> /dev/null; then + has_gem=true + fi + if command -v cargo &> /dev/null; then + has_cargo=true + fi + + # Function to install a package with the appropriate manager + install_package() { + local package=$1 + local manager=$2 + + echo "Installing $package with $manager..." + + case $manager in + "brew") + brew install $package + ;; + "apt-get") + sudo apt-get install -y $package + ;; + "dnf") + sudo dnf install -y $package + ;; + "yum") + sudo yum install -y $package + ;; + "pacman") + sudo pacman -S --noconfirm $package + ;; + "choco") + choco install -y $package + ;; + "scoop") + scoop install $package + ;; + "npm") + npm install -g $package + ;; + "pip") + if command -v pip3 &> /dev/null; then + pip3 install $package + else + pip install $package + fi + ;; + "gem") + gem install $package + ;; + "cargo") + cargo install $package + ;; + *) + echo "Unsupported package manager: $manager" + ;; + esac + } + + if command -v timeout >/dev/null 2>&1; then + TIMEOUT_CMD="timeout" + elif command -v gtimeout >/dev/null 2>&1; then + TIMEOUT_CMD="gtimeout" + else + TIMEOUT_CMD="" + fi + # Execute the original aider command and capture its output + debug_log "Running aider with the automatic installation wrapper..." + $TIMEOUT_CMD 180 aider --no-git --no-show-model-warnings --model "$model" --yes \ + --message-file "$message_file" --file "$output_file" | tee "$TEMP_OUTPUT" + + debug_log "Searching for installation commands in the output..." + + # Define the package managers to search for + PACKAGE_MANAGERS=( + "brew install" + "apt-get install"p + "apt install" + "dnf install" + "yum install" + "pacman -S" + "choco install" + "scoop install" + "npm install -g" + "pip install" + "pip3 install" + "gem install" + "cargo install" + ) + + # Search for and execute each type of installation command + for manager_cmd in "${PACKAGE_MANAGERS[@]}"; do + manager=$(echo $manager_cmd | cut -d' ' -f1) + if [[ "$manager" == "pacman" ]]; then + manager="pacman" + fi + if [[ "$manager" == "npm" ]]; then + manager="npm" + fi + if [[ "$manager" == "pip3" ]]; then + manager="pip" + fi + if [[ "$manager" == "apt" ]]; then + manager="apt-get" + fi + + # Check if the manager is available + var_name="has_$manager" + var_name=${var_name//-/_} # Replace dashes with underscores + + if [[ ${!var_name} != true ]]; then + continue + fi + + # Find the installation commands for this manager + INSTALLS=$(grep -o "$manager_cmd [^ ]*" "$TEMP_OUTPUT" | sort | uniq) + + if [ ! -z "$INSTALLS" ]; then + echo "Detected $manager commands:" + echo "$INSTALLS" + echo "Automatically installing $manager packages..." + + for cmd in $INSTALLS; do + # Extract the package name (last word of the command) + package=$(echo $cmd | awk '{print $NF}') + install_package "$package" "$manager" + done + fi + done + + # Special case for Windows: look for more complex installation commands + if [[ "$OS" == "windows" ]]; then + # Search for Windows-specific installation lines + WIN_INSTALLS=$(grep -i "download and install" "$TEMP_OUTPUT" | grep -i "windows") + if [ ! -z "$WIN_INSTALLS" ]; then + echo "Detected Windows installation suggestions:" + echo "$WIN_INSTALLS" + echo "Please manually install these components." + fi + fi + + # Clean up the temporary file + rm -f "$TEMP_OUTPUT" + + debug_log "Automatic installation processing completed." +} + # Create the monkey-patching tracer script create_interceptor_script() { local py_script=$(basename "$SCRIPT_PYTHON") @@ -488,16 +695,8 @@ convert_to_c() { while [ $attempt -le $max_attempts ] && [ "$success" = false ]; do echo "Attempt $attempt of $max_attempts to generate valid C code..." - if command -v timeout >/dev/null 2>&1; then - TIMEOUT_CMD="timeout" - elif command -v gtimeout >/dev/null 2>&1; then - TIMEOUT_CMD="gtimeout" - else - TIMEOUT_CMD="" - fi # Run aider to modify the C file (with a timeout) - $TIMEOUT_CMD 180 aider --no-git --no-show-model-warnings --model "$LLM_MODEL" --yes \ - --message-file "$TEMP_PROMPT" --file "$output_file" || true + aider_wrapper "$TEMP_PROMPT" "$output_file" "$LLM_MODEL" || true # Show the output file contents for debugging debug_log "C code after aider (first 20 lines):" From d0d333131f07bfcc55c0058dded06e00e3f57dc6 Mon Sep 17 00:00:00 2001 From: hunterbrightdesign <70662742+hunterbrightdesign@users.noreply.github.com> Date: Tue, 4 Mar 2025 00:47:29 +0100 Subject: [PATCH 6/9] correct trace dynamic_trace.sh --- dynamic_trace.sh | 418 ++++++++++++++++++++++++++++++++++------------- 1 file changed, 306 insertions(+), 112 deletions(-) diff --git a/dynamic_trace.sh b/dynamic_trace.sh index 635cac2..0a4d6d2 100755 --- a/dynamic_trace.sh +++ b/dynamic_trace.sh @@ -12,7 +12,7 @@ ESBMC_CMD="esbmc" DEBUG=true show_usage() { - echo "Usage: ./trace.sh [--docker] [--image IMAGE_NAME | --container CONTAINER_ID] [--model MODEL_NAME] " + echo "Usage: ./dynamic_trace.sh [--docker] [--image IMAGE_NAME | --container CONTAINER_ID] [--model MODEL_NAME] " echo "Options:" echo " --docker Run ESBMC in Docker container" echo " --image IMAGE_NAME Specify Docker image (default: esbmc)" @@ -99,6 +99,97 @@ extract_function_calls() { sort -u > "$FUNCTIONS_FILE" } +# Analyse statique des fonctions dans un fichier Python +extract_functions_statically() { + local py_file="$1" + local output_file="$2" + + # Créer un script Python temporaire pour l'analyse + local temp_py_script="$TEMP_DIR/extract_functions.py" + + cat > "$temp_py_script" < ", file=sys.stderr) + sys.exit(1) + + file_path = sys.argv[1] + output_file = sys.argv[2] + + functions = extract_functions_from_file(file_path) + + print(f"Fonctions trouvées ({len(functions)}):") + for func in sorted(functions): + print(f"funcname: {func}") + + # Écrire les fonctions dans un fichier + with open(output_file, 'w') as f: + for func in sorted(functions): + f.write(f"{func}\n") + + print(f"\nFonctions écrites dans {output_file}") +EOF + + chmod +x "$temp_py_script" + + # Exécuter le script Python et enregistrer les résultats dans le fichier de sortie + python3 "$temp_py_script" "$py_file" "$output_file" | tee -a "$TRACE_OUTPUT" + + echo "Analyse statique terminée pour $py_file" +} + # Wrapper function to assist with automatic dependency installation aider_wrapper() { local message_file="$1" @@ -235,7 +326,7 @@ aider_wrapper() { # Define the package managers to search for PACKAGE_MANAGERS=( "brew install" - "apt-get install"p + "apt-get install" "apt install" "dnf install" "yum install" @@ -301,7 +392,7 @@ aider_wrapper() { fi # Clean up the temporary file - rm -f "$TEMP_OUTPUT" + # rm -f "$TEMP_OUTPUT" debug_log "Automatic installation processing completed." } @@ -473,10 +564,11 @@ EOF echo "Created interception wrapper at $wrapper_script" } -# Alternative approach using sys.settrace +# Alternative approach using sys.settrace - CORRECTED VERSION create_trace_hook_script() { local py_script=$(basename "$SCRIPT_PYTHON") local hook_script="$TEMP_DIR/trace_hook.py" + local full_path=$(realpath "$SCRIPT_PYTHON") cat > "$hook_script" < "$TEMP_PROMPT" - echo "📤 Sending code to LLM for conversion..." + echo "📤 Sending code to LLM for conversion... : $TEMP_PROMPT" # Prepare Docker for testing if needed if [ "$USE_DOCKER" = true ]; then @@ -704,7 +832,6 @@ convert_to_c() { # Check if the generated C code is valid if [ "$USE_DOCKER" = true ]; then - filename=$(basename "$output_file") output_dir=$(dirname "$output_file") @@ -720,7 +847,6 @@ convert_to_c() { result=$? fi - if [ $result -eq 0 ]; then echo "✅ Successfully generated valid C code on attempt $attempt" success=true @@ -766,7 +892,7 @@ convert_to_c() { echo "🐳 Docker container stopped: $CONTAINER_ID" fi - rm -f "$TEMP_PROMPT" + # rm -f "$TEMP_PROMPT" if [ "$success" = true ]; then echo "✅ LLM conversion completed successfully." @@ -805,113 +931,180 @@ run_esbmc_for_function() { fi } -# Function to run the interactive tracing session using sys.settrace +# Helper function to show user options +show_user_options() { + # Show last 10 lines of program output + echo -e "\nLast 10 lines of program output:" + if [ -s "$PROGRAM_OUTPUT" ]; then + tail -n 10 "$PROGRAM_OUTPUT" + else + echo "No program output available." + fi + + # Ask user what to do + echo -e "\nOptions:" + echo " 1) Convert to C and verify with ESBMC" + echo " 2) Resume tracing" + echo " 3) Exit tracing and cleanup" + read -p "Enter option (1-3): " OPTION + + case $OPTION in + 1) + # Convert and verify + convert_to_c + while read -r function_name; do + if [[ -n "$function_name" ]]; then + run_esbmc_for_function "$function_name" + fi + done < "$FUNCTIONS_FILE" + + # Ask whether to resume or exit + read -p "Resume tracing? (y/n): " RESUME + if [[ "$RESUME" =~ ^[Yy]$ ]]; then + if [ -n "$TRACE_PID" ] && kill -0 $TRACE_PID 2>/dev/null; then + kill -SIGUSR1 $TRACE_PID 2>/dev/null || true # Resume + echo "▶️ Resuming trace collection..." + else + echo "Trace process is not running anymore." + fi + else + if [ -n "$TRACE_PID" ] && kill -0 $TRACE_PID 2>/dev/null; then + kill -SIGUSR2 $TRACE_PID 2>/dev/null || true # Exit + wait $TRACE_PID 2>/dev/null || true + fi + echo "✅ Analysis completed." + return 0 + fi + ;; + 2) + # Resume tracing + if [ -n "$TRACE_PID" ] && kill -0 $TRACE_PID 2>/dev/null; then + kill -SIGUSR1 $TRACE_PID 2>/dev/null || true # Resume + echo "▶️ Resuming trace collection..." + else + echo "Trace process is not running anymore." + fi + ;; + 3) + # Exit tracing + if [ -n "$TRACE_PID" ] && kill -0 $TRACE_PID 2>/dev/null; then + kill -SIGUSR2 $TRACE_PID 2>/dev/null || true # Exit + wait $TRACE_PID 2>/dev/null || true + fi + echo "✅ Analysis completed." + return 0 + ;; + *) + echo "Invalid option, resuming trace collection..." + if [ -n "$TRACE_PID" ] && kill -0 $TRACE_PID 2>/dev/null; then + kill -SIGUSR1 $TRACE_PID 2>/dev/null || true # Resume + fi + ;; + esac +} + +# Function to run the interactive tracing session using sys.settrace and static analysis run_tracing_session() { local py_script="$(basename "$SCRIPT_PYTHON")" echo "📌 Starting tracing for $SCRIPT_PYTHON..." - # Create trace hook script for better function tracking - create_trace_hook_script - - # Run the trace script - cd "$TEMP_DIR" - python3 "trace_hook.py" 2>&1 | tee "$TRACE_OUTPUT" & - TRACE_PID=$! - - echo "📊 Tracing started with PID: $TRACE_PID" - echo "- Press Enter to pause and analyze current trace" + # Essayez d'abord l'analyse statique (nouvelle approche) + echo "🔍 Performing static analysis first..." + extract_functions_statically "$SCRIPT_PYTHON" "$FUNCTIONS_FILE" - # Loop to allow interactive pausing and analysis - while true; do - read -t 1 || true # Non-blocking read with 1-second timeout + # Vérifiez si l'analyse statique a trouvé des fonctions + if [ -s "$FUNCTIONS_FILE" ]; then + echo "✅ Static analysis found $(wc -l < "$FUNCTIONS_FILE") functions." + echo "Detected functions:" + cat "$FUNCTIONS_FILE" - if [ $? -eq 0 ]; then - # User pressed Enter, pause tracing and analyze - kill -SIGUSR1 $TRACE_PID 2>/dev/null || true # Send pause signal - echo "⏸️ Pausing trace collection..." - sleep 1 # Wait for pause to take effect - - # Extract functions from current trace - extract_function_calls - - # Extract program output (non-trace lines) - grep -v "funcname:" "$TRACE_OUTPUT" | grep -v "call function:" > "$PROGRAM_OUTPUT" + # Afficher les options directement si l'analyse statique a réussi + show_user_options + else + echo "⚠️ Static analysis didn't find any functions. Falling back to dynamic tracing." + + # Créer le script de trace et essayer le traçage dynamique + create_trace_hook_script + + # Run the trace script + cd "$TEMP_DIR" + python3 "trace_hook.py" 2>&1 | tee "$TRACE_OUTPUT" & + TRACE_PID=$! + + echo "📊 Tracing started with PID: $TRACE_PID" + echo "- Press Enter to pause and analyze current trace" + + # Loop to allow interactive pausing and analysis + while true; do + read -t 1 || true # Non-blocking read with 1-second timeout - # Check if we have any functions - if [ ! -s "$FUNCTIONS_FILE" ]; then - echo "⚠️ No functions detected in trace so far." - echo "Please let the program run longer or check if tracing is working correctly." + if [ $? -eq 0 ]; then + # User pressed Enter, pause tracing and analyze + kill -SIGUSR1 $TRACE_PID 2>/dev/null || true # Send pause signal + echo "⏸️ Pausing trace collection..." + sleep 1 # Wait for pause to take effect + + # Extract functions from current trace + extract_function_calls - # Show last 20 lines of trace output for debugging - echo "Last 20 lines of trace output:" - tail -n 20 "$TRACE_OUTPUT" + # Si le traçage dynamique échoue, réessayer avec l'analyse statique + if [ ! -s "$FUNCTIONS_FILE" ]; then + echo "⚠️ No functions detected in trace. Using static analysis instead." + extract_functions_statically "$SCRIPT_PYTHON" "$FUNCTIONS_FILE" + fi + + # Extract program output (non-trace lines) + grep -v "funcname:" "$TRACE_OUTPUT" | grep -v "call function:" > "$PROGRAM_OUTPUT" + + # Check if we have any functions + if [ ! -s "$FUNCTIONS_FILE" ]; then + echo "⚠️ No functions detected by either method." + echo "Last 20 lines of trace output:" + tail -n 20 "$TRACE_OUTPUT" + else + # Show detected functions + echo "Detected functions:" + cat "$FUNCTIONS_FILE" + fi + + # Afficher les options pour l'utilisateur + show_user_options + + # Check if trace process is still running + if ! kill -0 $TRACE_PID 2>/dev/null; then + echo "Trace process has ended." + break + fi else - # Show detected functions - echo "Detected functions so far:" - cat "$FUNCTIONS_FILE" - fi - - # Show last 10 lines of program output - echo -e "\nLast 10 lines of program output:" - grep -v "funcname:" "$TRACE_OUTPUT" | grep -v "call function:" | tail -n 10 - - # Ask user what to do - echo -e "\nOptions:" - echo " 1) Convert to C and verify with ESBMC" - echo " 2) Resume tracing" - echo " 3) Exit tracing and cleanup" - read -p "Enter option (1-3): " OPTION - - case $OPTION in - 1) - # Convert and verify - convert_to_c - while read -r function_name; do - if [[ -n "$function_name" ]]; then - run_esbmc_for_function "$function_name" - fi - done < "$FUNCTIONS_FILE" + # Check if trace process is still running + if ! kill -0 $TRACE_PID 2>/dev/null; then + echo "Trace process has ended." - # Ask whether to resume or exit - read -p "Resume tracing? (y/n): " RESUME - if [[ "$RESUME" =~ ^[Yy]$ ]]; then - kill -SIGUSR1 $TRACE_PID 2>/dev/null || true # Resume - echo "▶️ Resuming trace collection..." - else - kill -SIGUSR2 $TRACE_PID 2>/dev/null || true # Exit - wait $TRACE_PID 2>/dev/null || true - echo "✅ Tracing completed." - break + # Si le traçage s'est terminé sans trouver de fonctions, utiliser l'analyse statique + if [ ! -s "$FUNCTIONS_FILE" ]; then + echo "⚠️ Dynamic tracing completed without finding functions. Using static analysis." + extract_functions_statically "$SCRIPT_PYTHON" "$FUNCTIONS_FILE" + + if [ -s "$FUNCTIONS_FILE" ]; then + echo "✅ Static analysis found $(wc -l < "$FUNCTIONS_FILE") functions." + echo "Detected functions:" + cat "$FUNCTIONS_FILE" + + # Montrer les options maintenant que nous avons des fonctions + show_user_options + else + echo "❌ No functions detected by any method. Cannot proceed with analysis." + fi fi - ;; - 2) - # Resume tracing - kill -SIGUSR1 $TRACE_PID 2>/dev/null || true # Resume - echo "▶️ Resuming trace collection..." - ;; - 3) - # Exit tracing - kill -SIGUSR2 $TRACE_PID 2>/dev/null || true # Exit - wait $TRACE_PID 2>/dev/null || true - echo "✅ Tracing completed." + break - ;; - *) - echo "Invalid option, resuming trace collection..." - kill -SIGUSR1 $TRACE_PID 2>/dev/null || true # Resume - ;; - esac - fi + fi + fi + done - # Check if trace process is still running - if ! kill -0 $TRACE_PID 2>/dev/null; then - echo "Trace process has ended." - break - fi - done - - cd - > /dev/null # Return to previous directory + cd - > /dev/null # Return to previous directory + fi } # Main tracing loop @@ -926,6 +1119,7 @@ while true; do [Yy]) break ;; # Restart loop [Nn]) echo "✅ Tracing completed." + # Uncomment to remove temp files if needed rm -rf "$TEMP_DIR" "$TRACE_OUTPUT" "$FUNCTIONS_FILE" "$PROGRAM_OUTPUT" "$LLM_INPUT" exit 0 ;; From 46a4288de7766d61f150e52d17506e858fda7220 Mon Sep 17 00:00:00 2001 From: hunterbrightdesign <70662742+hunterbrightdesign@users.noreply.github.com> Date: Tue, 4 Mar 2025 17:42:09 +0100 Subject: [PATCH 7/9] update dynamic_trace.sh --- dynamic_trace.sh | 454 +++++++++++------------------------------------ 1 file changed, 107 insertions(+), 347 deletions(-) diff --git a/dynamic_trace.sh b/dynamic_trace.sh index 0a4d6d2..71666b7 100755 --- a/dynamic_trace.sh +++ b/dynamic_trace.sh @@ -93,103 +93,12 @@ fi # Function to extract executed functions from trace output extract_function_calls() { # Extract functions from the trace file, filter out system functions - cat "$TRACE_OUTPUT" | grep -E "call function|funcname:" | - sed -E 's/.*call function: ([a-zA-Z0-9_]+).*|.*funcname: ([a-zA-Z0-9_]+).*/\1\2/' | - grep -v "^$" | grep -v "^<" | grep -v "^_" | + cat "$TRACE_OUTPUT" | grep -E "^funcname: " | + sed -E 's/^funcname: ([a-zA-Z0-9_<>]+)$/\1/' | + grep -v "^$" | grep -v "^<" | sort -u > "$FUNCTIONS_FILE" } -# Analyse statique des fonctions dans un fichier Python -extract_functions_statically() { - local py_file="$1" - local output_file="$2" - - # Créer un script Python temporaire pour l'analyse - local temp_py_script="$TEMP_DIR/extract_functions.py" - - cat > "$temp_py_script" < ", file=sys.stderr) - sys.exit(1) - - file_path = sys.argv[1] - output_file = sys.argv[2] - - functions = extract_functions_from_file(file_path) - - print(f"Fonctions trouvées ({len(functions)}):") - for func in sorted(functions): - print(f"funcname: {func}") - - # Écrire les fonctions dans un fichier - with open(output_file, 'w') as f: - for func in sorted(functions): - f.write(f"{func}\n") - - print(f"\nFonctions écrites dans {output_file}") -EOF - - chmod +x "$temp_py_script" - - # Exécuter le script Python et enregistrer les résultats dans le fichier de sortie - python3 "$temp_py_script" "$py_file" "$output_file" | tee -a "$TRACE_OUTPUT" - - echo "Analyse statique terminée pour $py_file" -} - # Wrapper function to assist with automatic dependency installation aider_wrapper() { local message_file="$1" @@ -392,7 +301,7 @@ aider_wrapper() { fi # Clean up the temporary file - # rm -f "$TEMP_OUTPUT" + rm -f "$TEMP_OUTPUT" debug_log "Automatic installation processing completed." } @@ -564,7 +473,7 @@ EOF echo "Created interception wrapper at $wrapper_script" } -# Alternative approach using sys.settrace - CORRECTED VERSION +# Alternative approach using sys.settrace create_trace_hook_script() { local py_script=$(basename "$SCRIPT_PYTHON") local hook_script="$TEMP_DIR/trace_hook.py" @@ -574,123 +483,91 @@ create_trace_hook_script() { #!/usr/bin/env python3 import sys import os -import signal import traceback -import time import inspect +import linecache -# Original script path - USING ABSOLUTE PATH +# Original script path TARGET_SCRIPT = "$full_path" TARGET_SCRIPT_BASENAME = "$(basename "$SCRIPT_PYTHON")" -# Global state -PAUSED = False -CALL_COUNT = 0 -MAX_CALLS = 500 -TRACED_FUNCTIONS = set() +# Track executed functions and lines +executed_functions = set() +executed_lines = set() -# Signal handler for pause/resume -def handle_pause(signum, frame): - global PAUSED - PAUSED = not PAUSED - print(f"\n{'[PAUSED]' if PAUSED else '[RESUMED]'} at {frame.f_code.co_name}") - if PAUSED: - print("\n=== Current Stack ===") - traceback.print_stack(frame) - print("=====================") +# Filter for library code +IGNORE_DIRS = ['/lib/python', '/site-packages/', '/dist-packages/'] -# Signal handler for exit -def handle_exit(signum, frame): - print("\n[EXITING] Trace terminated by signal") - sys.exit(0) - -# Register signal handlers -signal.signal(signal.SIGUSR1, handle_pause) -signal.signal(signal.SIGUSR2, handle_exit) - -# Print PID for external control -print(f"Trace process PID: {os.getpid()}") -print("Send SIGUSR1 (kill -SIGUSR1 PID) to pause/resume") -print("Send SIGUSR2 (kill -SIGUSR2 PID) to exit") - -# Trace function hook -def trace_calls(frame, event, arg): - global PAUSED, CALL_COUNT, TRACED_FUNCTIONS +# Trace function for tracking function calls and line execution +def trace_function(frame, event, arg): + # Get code information + code = frame.f_code + func_name = code.co_name + filename = code.co_filename + lineno = frame.f_lineno - # Wait if paused - while PAUSED: - time.sleep(0.1) + # Skip library code + if any(lib_dir in filename for lib_dir in IGNORE_DIRS): + return trace_function + # Only trace our script and directly related files + script_dir = os.path.dirname(os.path.abspath(TARGET_SCRIPT)) + if not (filename == TARGET_SCRIPT or filename.startswith(script_dir)): + return trace_function + + # Record information based on event type if event == 'call': - # Get function info - func_name = frame.f_code.co_name - filename = frame.f_code.co_filename - - # Improved check for matching our target script - is_target_file = ( - TARGET_SCRIPT == filename or - TARGET_SCRIPT_BASENAME == os.path.basename(filename) or - TARGET_SCRIPT_BASENAME in filename - ) - - # Only trace user functions from our script - if is_target_file and not func_name.startswith('_') and func_name not in TRACED_FUNCTIONS: - if CALL_COUNT < MAX_CALLS: - print(f"funcname: {func_name}") - TRACED_FUNCTIONS.add(func_name) - CALL_COUNT += 1 - - if CALL_COUNT == MAX_CALLS: - print("Trace limit reached (500 functions)") + # Skip dunder methods except main + if func_name.startswith('__') and func_name != '__main__': + return trace_function + + # Record function call if not already recorded + if func_name not in executed_functions: + print(f"funcname: {func_name}") + executed_functions.add(func_name) + + elif event == 'line': + # Record line execution + line_key = (filename, lineno) + if line_key not in executed_lines: + executed_lines.add(line_key) + + # Get the line content + line = linecache.getline(filename, lineno).strip() + if line: # Only print non-empty lines + print(f"line: {os.path.basename(filename)}:{lineno}: {line}") - return trace_calls + # Continue tracing + return trace_function -# Setup trace hook -sys.settrace(trace_calls) +# Set up the trace function +sys.settrace(trace_function) -# Check if the script exists before trying to execute it -if not os.path.exists(TARGET_SCRIPT): - print(f"Error: Script file {TARGET_SCRIPT} does not exist.") - sys.exit(1) +# Add script directory to path for imports +script_dir = os.path.dirname(os.path.abspath(TARGET_SCRIPT)) +if script_dir not in sys.path: + sys.path.insert(0, script_dir) -# Execute the target script +# Run the script try: - print(f"Starting execution of {TARGET_SCRIPT}") - - # Try to load dependencies that might be needed - try: - import botocore - print("Successfully imported botocore") - except ImportError: - print("Warning: botocore module not available, this might cause errors if needed") + print(f"Executing {TARGET_SCRIPT}") - # Read the script content - with open(TARGET_SCRIPT) as f: - script_content = f.read() + # Read and compile the script + with open(TARGET_SCRIPT, 'rb') as f: + code = compile(f.read(), TARGET_SCRIPT, 'exec') - # Set up globals for execution - script_globals = { + # Execute the script + namespace = { '__file__': TARGET_SCRIPT, '__name__': '__main__', } - # Execute the script with error handling - try: - exec(script_content, script_globals) - print("Script execution completed") - except ImportError as e: - print(f"Import error during execution: {e}") - print("This is likely due to missing dependencies.") - print("Consider installing the required packages or using static analysis instead.") - traceback.print_exc() - except Exception as e: - print(f"Error during script execution: {e}") - traceback.print_exc() + exec(code, namespace) + + print(f"Execution completed. Found {len(executed_functions)} executed functions and {len(executed_lines)} executed lines.") -except KeyboardInterrupt: - print("\nScript execution interrupted") except Exception as e: - print(f"Error preparing script execution: {e}") + print(f"Error during execution: {e}") traceback.print_exc() EOF @@ -743,6 +620,7 @@ EOF return 0 } + # Function to convert Python to C using LLM with multiple attempts convert_to_c() { local input_file="$SCRIPT_PYTHON" @@ -770,13 +648,7 @@ convert_to_c() { echo "3. Use equivalent C data structures and types" echo "4. Include necessary headers and dependencies" echo "5. Only output proper C code that can be parsed by a C compiler" - - # Add source instruction file if it exists - if [ -f "$SOURCE_INSTRUCTION_FILE" ]; then - cat "$SOURCE_INSTRUCTION_FILE" - else - echo "Note: Additional instruction file was not found." - fi + cat "$SOURCE_INSTRUCTION_FILE" # Add list of functions we detected to focus on echo -e "\nImplement these functions identified during execution:" @@ -832,6 +704,7 @@ convert_to_c() { # Check if the generated C code is valid if [ "$USE_DOCKER" = true ]; then + filename=$(basename "$output_file") output_dir=$(dirname "$output_file") @@ -847,6 +720,7 @@ convert_to_c() { result=$? fi + if [ $result -eq 0 ]; then echo "✅ Successfully generated valid C code on attempt $attempt" success=true @@ -892,7 +766,7 @@ convert_to_c() { echo "🐳 Docker container stopped: $CONTAINER_ID" fi - # rm -f "$TEMP_PROMPT" + rm -f "$TEMP_PROMPT" if [ "$success" = true ]; then echo "✅ LLM conversion completed successfully." @@ -922,29 +796,49 @@ run_esbmc_for_function() { if [ "$USE_DOCKER" = true ]; then if [ -n "$CONTAINER_ID" ]; then # The file should already be in the container since we're mounting TEMP_DIR - docker exec -w /workspace "$CONTAINER_ID" bash -c "$current_cmd" + docker exec -w /workspace "$CONTAINER_ID" "$current_cmd" else - docker run --rm -v "$TEMP_DIR":/workspace -w /workspace "$DOCKER_IMAGE" bash -c "$current_cmd" + docker run --rm -v $(pwd):/workspace -w /workspace "$DOCKER_IMAGE" "$current_cmd" fi else cd "$TEMP_DIR" && eval "$current_cmd" fi } -# Helper function to show user options -show_user_options() { - # Show last 10 lines of program output - echo -e "\nLast 10 lines of program output:" - if [ -s "$PROGRAM_OUTPUT" ]; then - tail -n 10 "$PROGRAM_OUTPUT" +# Function to run the interactive tracing session using sys.settrace +run_tracing_session() { + local py_script="$(basename "$SCRIPT_PYTHON")" + + echo "📌 Starting tracing for $SCRIPT_PYTHON..." + + # Create trace hook script + create_trace_hook_script + + # Run the trace script directly + cd "$TEMP_DIR" + python3 "trace_hook.py" > "$TRACE_OUTPUT" 2>&1 + + # Extract functions from the trace output + extract_function_calls + + # Check if we have any functions + if [ ! -s "$FUNCTIONS_FILE" ]; then + echo "⚠️ No functions detected in trace." + echo "Last 20 lines of trace output:" + tail -n 20 "$TRACE_OUTPUT" else - echo "No program output available." + # Show detected functions + echo "Detected functions:" + cat "$FUNCTIONS_FILE" fi - # Ask user what to do + # Extract program output (non-trace lines) + grep -v "^funcname:" "$TRACE_OUTPUT" | grep -v "^line:" > "$PROGRAM_OUTPUT" + + # Show options echo -e "\nOptions:" echo " 1) Convert to C and verify with ESBMC" - echo " 2) Resume tracing" + echo " 2) Restart tracing" echo " 3) Exit tracing and cleanup" read -p "Enter option (1-3): " OPTION @@ -957,154 +851,21 @@ show_user_options() { run_esbmc_for_function "$function_name" fi done < "$FUNCTIONS_FILE" - - # Ask whether to resume or exit - read -p "Resume tracing? (y/n): " RESUME - if [[ "$RESUME" =~ ^[Yy]$ ]]; then - if [ -n "$TRACE_PID" ] && kill -0 $TRACE_PID 2>/dev/null; then - kill -SIGUSR1 $TRACE_PID 2>/dev/null || true # Resume - echo "▶️ Resuming trace collection..." - else - echo "Trace process is not running anymore." - fi - else - if [ -n "$TRACE_PID" ] && kill -0 $TRACE_PID 2>/dev/null; then - kill -SIGUSR2 $TRACE_PID 2>/dev/null || true # Exit - wait $TRACE_PID 2>/dev/null || true - fi - echo "✅ Analysis completed." - return 0 - fi ;; 2) - # Resume tracing - if [ -n "$TRACE_PID" ] && kill -0 $TRACE_PID 2>/dev/null; then - kill -SIGUSR1 $TRACE_PID 2>/dev/null || true # Resume - echo "▶️ Resuming trace collection..." - else - echo "Trace process is not running anymore." - fi + # Restart tracing + run_tracing_session ;; 3) # Exit tracing - if [ -n "$TRACE_PID" ] && kill -0 $TRACE_PID 2>/dev/null; then - kill -SIGUSR2 $TRACE_PID 2>/dev/null || true # Exit - wait $TRACE_PID 2>/dev/null || true - fi - echo "✅ Analysis completed." - return 0 + echo "✅ Tracing completed." ;; *) - echo "Invalid option, resuming trace collection..." - if [ -n "$TRACE_PID" ] && kill -0 $TRACE_PID 2>/dev/null; then - kill -SIGUSR1 $TRACE_PID 2>/dev/null || true # Resume - fi + echo "Invalid option, exiting." ;; esac -} - -# Function to run the interactive tracing session using sys.settrace and static analysis -run_tracing_session() { - local py_script="$(basename "$SCRIPT_PYTHON")" - echo "📌 Starting tracing for $SCRIPT_PYTHON..." - - # Essayez d'abord l'analyse statique (nouvelle approche) - echo "🔍 Performing static analysis first..." - extract_functions_statically "$SCRIPT_PYTHON" "$FUNCTIONS_FILE" - - # Vérifiez si l'analyse statique a trouvé des fonctions - if [ -s "$FUNCTIONS_FILE" ]; then - echo "✅ Static analysis found $(wc -l < "$FUNCTIONS_FILE") functions." - echo "Detected functions:" - cat "$FUNCTIONS_FILE" - - # Afficher les options directement si l'analyse statique a réussi - show_user_options - else - echo "⚠️ Static analysis didn't find any functions. Falling back to dynamic tracing." - - # Créer le script de trace et essayer le traçage dynamique - create_trace_hook_script - - # Run the trace script - cd "$TEMP_DIR" - python3 "trace_hook.py" 2>&1 | tee "$TRACE_OUTPUT" & - TRACE_PID=$! - - echo "📊 Tracing started with PID: $TRACE_PID" - echo "- Press Enter to pause and analyze current trace" - - # Loop to allow interactive pausing and analysis - while true; do - read -t 1 || true # Non-blocking read with 1-second timeout - - if [ $? -eq 0 ]; then - # User pressed Enter, pause tracing and analyze - kill -SIGUSR1 $TRACE_PID 2>/dev/null || true # Send pause signal - echo "⏸️ Pausing trace collection..." - sleep 1 # Wait for pause to take effect - - # Extract functions from current trace - extract_function_calls - - # Si le traçage dynamique échoue, réessayer avec l'analyse statique - if [ ! -s "$FUNCTIONS_FILE" ]; then - echo "⚠️ No functions detected in trace. Using static analysis instead." - extract_functions_statically "$SCRIPT_PYTHON" "$FUNCTIONS_FILE" - fi - - # Extract program output (non-trace lines) - grep -v "funcname:" "$TRACE_OUTPUT" | grep -v "call function:" > "$PROGRAM_OUTPUT" - - # Check if we have any functions - if [ ! -s "$FUNCTIONS_FILE" ]; then - echo "⚠️ No functions detected by either method." - echo "Last 20 lines of trace output:" - tail -n 20 "$TRACE_OUTPUT" - else - # Show detected functions - echo "Detected functions:" - cat "$FUNCTIONS_FILE" - fi - - # Afficher les options pour l'utilisateur - show_user_options - - # Check if trace process is still running - if ! kill -0 $TRACE_PID 2>/dev/null; then - echo "Trace process has ended." - break - fi - else - # Check if trace process is still running - if ! kill -0 $TRACE_PID 2>/dev/null; then - echo "Trace process has ended." - - # Si le traçage s'est terminé sans trouver de fonctions, utiliser l'analyse statique - if [ ! -s "$FUNCTIONS_FILE" ]; then - echo "⚠️ Dynamic tracing completed without finding functions. Using static analysis." - extract_functions_statically "$SCRIPT_PYTHON" "$FUNCTIONS_FILE" - - if [ -s "$FUNCTIONS_FILE" ]; then - echo "✅ Static analysis found $(wc -l < "$FUNCTIONS_FILE") functions." - echo "Detected functions:" - cat "$FUNCTIONS_FILE" - - # Montrer les options maintenant que nous avons des fonctions - show_user_options - else - echo "❌ No functions detected by any method. Cannot proceed with analysis." - fi - fi - - break - fi - fi - done - - cd - > /dev/null # Return to previous directory - fi + cd - > /dev/null # Return to previous directory } # Main tracing loop @@ -1119,7 +880,6 @@ while true; do [Yy]) break ;; # Restart loop [Nn]) echo "✅ Tracing completed." - # Uncomment to remove temp files if needed rm -rf "$TEMP_DIR" "$TRACE_OUTPUT" "$FUNCTIONS_FILE" "$PROGRAM_OUTPUT" "$LLM_INPUT" exit 0 ;; From 80875c044caf7c84b44a2127b65b4070f9caa159 Mon Sep 17 00:00:00 2001 From: hunterbrightdesign <70662742+hunterbrightdesign@users.noreply.github.com> Date: Wed, 5 Mar 2025 02:00:00 +0100 Subject: [PATCH 8/9] add dynamic_trace.py --- dynamic_trace.py | 713 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 713 insertions(+) create mode 100644 dynamic_trace.py diff --git a/dynamic_trace.py b/dynamic_trace.py new file mode 100644 index 0000000..7f269ed --- /dev/null +++ b/dynamic_trace.py @@ -0,0 +1,713 @@ +#!/usr/bin/env python3 +import os +import sys +import argparse +import tempfile +import subprocess +import shutil +import signal +import time +import json +import re +from pathlib import Path +from typing import Dict, List, Optional, Tuple, Set, Any +import platform + +# Default configuration +class Config: + USE_DOCKER = False + DOCKER_IMAGE = "esbmc" + LLM_MODEL = "openrouter/anthropic/claude-3.5-sonnet" + CONTAINER_ID = "" + SOURCE_INSTRUCTION_FILE = "prompts/python_prompt.txt" + ESBMC_CMD = "esbmc" + DEBUG = True + + # Paths + temp_dir = None + trace_output = None + functions_file = None + program_output = None + llm_input = None + c_output = None + +config = Config() + +def debug_log(message: str) -> None: + """Log debug messages if DEBUG is enabled.""" + if config.DEBUG: + print(f"[DEBUG] {message}") + +def show_usage() -> None: + """Display usage instructions and exit.""" + print("Usage: python dynamic_trace.py [--docker] [--image IMAGE_NAME | --container CONTAINER_ID] [--model MODEL_NAME] ") + print("Options:") + print(" --docker Run ESBMC in Docker container") + print(" --image IMAGE_NAME Specify Docker image (default: esbmc)") + print(" --container ID Specify existing container ID") + print(" --model MODEL_NAME Specify LLM model (default: openrouter/anthropic/claude-3.5-sonnet)") + sys.exit(1) + +def setup_workspace(script_python: str) -> None: + """Create a temporary workspace and set up necessary files.""" + config.temp_dir = tempfile.mkdtemp() + + # Create all temporary files inside the temp directory + config.trace_output = os.path.join(config.temp_dir, "trace.out") + config.functions_file = os.path.join(config.temp_dir, "functions.list") + config.program_output = os.path.join(config.temp_dir, "program.out") + config.llm_input = os.path.join(config.temp_dir, "llm_input.txt") + + c_file_name = os.path.basename(script_python).replace('.py', '.c') + config.c_output = os.path.join(config.temp_dir, c_file_name) + + # Create empty files + for file_path in [config.trace_output, config.functions_file, config.program_output, config.llm_input]: + with open(file_path, 'w') as f: + pass + + # Copy the Python script to the temp directory + script_dest = os.path.join(config.temp_dir, os.path.basename(script_python)) + shutil.copy2(script_python, script_dest) + + print(f"📂 Temporary workspace: {config.temp_dir}") + print(f"📄 Copied Python script to temporary directory") + +def setup_virtual_env() -> None: + """Set up virtual environment if available.""" + if os.path.isdir("venv"): + # Activate venv (not directly possible in the same process, + # this would require subprocess execution) + print("Virtual environment exists but can't be activated in-script.") + print("If needed, activate it manually before running this script.") + elif os.path.isfile("requirements.txt"): + print("🚀 Creating virtual environment...") + try: + subprocess.run([sys.executable, "-m", "venv", "venv"], check=True) + + # Determine the pip executable path based on OS + if platform.system() == "Windows": + pip_path = "venv\\Scripts\\pip" + else: + pip_path = "venv/bin/pip" + + subprocess.run([pip_path, "install", "-r", "requirements.txt"], check=True) + print("✅ Virtual environment created and dependencies installed") + except subprocess.CalledProcessError as e: + print(f"❌ Failed to set up virtual environment: {e}") + +def extract_function_calls() -> None: + """Extract executed functions from trace output.""" + with open(config.trace_output, 'r') as trace_file, open(config.functions_file, 'w') as functions_file: + functions = set() + for line in trace_file: + if line.startswith("funcname: "): + func_name = line.strip().replace("funcname: ", "") + if func_name and not func_name.startswith("<") and func_name not in functions: + functions.add(func_name) + functions_file.write(f"{func_name}\n") + +def create_trace_hook_script() -> str: + """Create a sys.settrace() hook script to trace Python code execution.""" + py_script = os.path.basename(config.script_python) + hook_script = os.path.join(config.temp_dir, "trace_hook.py") + full_path = os.path.abspath(config.script_python) + + with open(hook_script, 'w') as f: + f.write(f'''#!/usr/bin/env python3 +import sys +import os +import traceback +import inspect +import linecache + +# Original script path +TARGET_SCRIPT = "{full_path}" +TARGET_SCRIPT_BASENAME = "{os.path.basename(config.script_python)}" + +# Track executed functions and lines +executed_functions = set() +executed_lines = set() + +# Filter for library code +IGNORE_DIRS = ['/lib/python', '/site-packages/', '/dist-packages/'] + +# Trace function for tracking function calls and line execution +def trace_function(frame, event, arg): + # Get code information + code = frame.f_code + func_name = code.co_name + filename = code.co_filename + lineno = frame.f_lineno + + # Skip library code + if any(lib_dir in filename for lib_dir in IGNORE_DIRS): + return trace_function + + # Only trace our script and directly related files + script_dir = os.path.dirname(os.path.abspath(TARGET_SCRIPT)) + if not (filename == TARGET_SCRIPT or filename.startswith(script_dir)): + return trace_function + + # Record information based on event type + if event == 'call': + # Skip dunder methods except main + if func_name.startswith('__') and func_name != '__main__': + return trace_function + + # Record function call if not already recorded + if func_name not in executed_functions: + print(f"funcname: {{func_name}}") + executed_functions.add(func_name) + + elif event == 'line': + # Record line execution + line_key = (filename, lineno) + if line_key not in executed_lines: + executed_lines.add(line_key) + + # Get the line content + line = linecache.getline(filename, lineno).strip() + if line: # Only print non-empty lines + print(f"line: {{os.path.basename(filename)}}:{{lineno}}: {{line}}") + + # Continue tracing + return trace_function + +# Set up the trace function +sys.settrace(trace_function) + +# Add script directory to path for imports +script_dir = os.path.dirname(os.path.abspath(TARGET_SCRIPT)) +if script_dir not in sys.path: + sys.path.insert(0, script_dir) + +# Run the script +try: + print(f"Executing {{TARGET_SCRIPT}}") + + # Read and compile the script + with open(TARGET_SCRIPT, 'rb') as f: + code = compile(f.read(), TARGET_SCRIPT, 'exec') + + # Execute the script + namespace = {{ + '__file__': TARGET_SCRIPT, + '__name__': '__main__', + }} + + exec(code, namespace) + + print(f"Execution completed. Found {{len(executed_functions)}} executed functions and {{len(executed_lines)}} executed lines.") + +except Exception as e: + print(f"Error during execution: {{e}}") + traceback.print_exc() +''') + + os.chmod(hook_script, 0o755) + print(f"Created trace hook script at {hook_script}") + return hook_script + +def create_c_file_manually(py_file: str, c_file: str) -> bool: + """Create a basic C version of the Python code with stub functions.""" + functions = [] + + # Read detected functions + if os.path.exists(config.functions_file): + with open(config.functions_file, 'r') as f: + functions = [line.strip() for line in f if line.strip() and line.strip() != ""] + + with open(c_file, 'w') as f: + f.write(f'''#include +#include +#include +#include +#include +#include + +// Converted from {os.path.basename(py_file)} + +''') + + # Write function stubs + for func in functions: + f.write(f'''// Function: {func} +int {func}(int a, int b) {{ + return a + b; +}} + +''') + + # Write main function + f.write(f'''int main() {{ + // Main function converted from Python + printf("Hello from C version of {os.path.basename(py_file)}\\n"); + + // Add assertions for each detected function +''') + + for func in functions: + f.write(f' assert({func}(1, 2) == 3);\n') + + f.write(''' + return 0; +} +''') + + debug_log(f"Created initial C file: {c_file}") + return True + +def aider_wrapper(message_file: str, output_file: str, model: str) -> bool: + """Run aider with automatic dependency installation, preventing history files.""" + # Detect OS and package managers + os_type = platform.system() + has_package_managers = { + "brew": shutil.which("brew") is not None, + "apt-get": shutil.which("apt-get") is not None, + "dnf": shutil.which("dnf") is not None, + "yum": shutil.which("yum") is not None, + "pacman": shutil.which("pacman") is not None, + "choco": shutil.which("choco") is not None, + "scoop": shutil.which("scoop") is not None, + "npm": shutil.which("npm") is not None, + "pip": shutil.which("pip") is not None or shutil.which("pip3") is not None, + "gem": shutil.which("gem") is not None, + "cargo": shutil.which("cargo") is not None + } + + debug_log(f"Detected operating system: {os_type}") + + # Determine timeout command + timeout_cmd = None + if shutil.which("timeout"): + timeout_cmd = "timeout" + elif shutil.which("gtimeout"): + timeout_cmd = "gtimeout" + + # Create temp directory for aider to prevent history files in current directory + aider_temp_dir = tempfile.mkdtemp() + original_dir = os.getcwd() + + try: + # Change to temp directory for aider execution + os.chdir(aider_temp_dir) + + # Run aider with timeout and without creating history files + cmd = ["aider", "--no-git", "--no-show-model-warnings", + f"--model={model}", "--yes", + f"--message-file={message_file}", f"--file={output_file}"] # Prevent history file creation if supported + + if timeout_cmd: + cmd = [timeout_cmd, "180"] + cmd + + process = subprocess.Popen( + cmd, + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + text=True, + bufsize=1 + ) + + # Process output in real-time + package_managers = { + "brew": "brew install", + "apt-get": "apt-get install", + "dnf": "dnf install", + "yum": "yum install", + "pacman": "pacman -S", + "choco": "choco install", + "scoop": "scoop install", + "npm": "npm install -g", + "pip": "pip install", + "gem": "gem install", + "cargo": "cargo install" + } + + detected_installations = {mgr: set() for mgr in package_managers} + + for line in iter(process.stdout.readline, ''): + print(line, end='') + + # Look for installation commands + for mgr, cmd_prefix in package_managers.items(): + if cmd_prefix in line: + # Extract package name + match = re.search(f"{re.escape(cmd_prefix)} ([^ ]+)", line) + if match and has_package_managers[mgr]: + package = match.group(1) + detected_installations[mgr].add(package) + + process.wait() + + # Install detected packages + for mgr, packages in detected_installations.items(): + if packages: + print(f"Detected {mgr} packages to install: {', '.join(packages)}") + for package in packages: + install_package(package, mgr) + + return process.returncode == 0 + + except Exception as e: + print(f"Error running aider: {e}") + return False + finally: + # Return to original directory and clean up + os.chdir(original_dir) + try: + shutil.rmtree(aider_temp_dir) + except Exception as e: + print(f"Warning: Could not clean up temp directory: {e}") + + # Remove any history or parameter files that might have been created + for file_pattern in ['.aider.chat.history.md', '--extra-params=*']: + for file_path in Path('.').glob(file_pattern): + try: + file_path.unlink() + print(f"Removed file: {file_path}") + except Exception: + pass + +def install_package(package: str, manager: str) -> bool: + """Install a package using the appropriate package manager.""" + print(f"Installing {package} with {manager}...") + + try: + if manager == "brew": + subprocess.run(["brew", "install", package], check=True) + elif manager == "apt-get": + subprocess.run(["sudo", "apt-get", "install", "-y", package], check=True) + elif manager == "dnf": + subprocess.run(["sudo", "dnf", "install", "-y", package], check=True) + elif manager == "yum": + subprocess.run(["sudo", "yum", "install", "-y", package], check=True) + elif manager == "pacman": + subprocess.run(["sudo", "pacman", "-S", "--noconfirm", package], check=True) + elif manager == "choco": + subprocess.run(["choco", "install", "-y", package], check=True) + elif manager == "scoop": + subprocess.run(["scoop", "install", package], check=True) + elif manager == "npm": + subprocess.run(["npm", "install", "-g", package], check=True) + elif manager == "pip": + if shutil.which("pip3"): + subprocess.run([shutil.which("pip3"), "install", package], check=True) + else: + subprocess.run([shutil.which("pip"), "install", package], check=True) + elif manager == "gem": + subprocess.run(["gem", "install", package], check=True) + elif manager == "cargo": + subprocess.run(["cargo", "install", package], check=True) + else: + print(f"Unsupported package manager: {manager}") + return False + + return True + except subprocess.CalledProcessError as e: + print(f"Failed to install {package}: {e}") + return False + +def convert_to_c() -> bool: + """Convert Python to C using LLM with multiple attempts.""" + input_file = config.script_python + output_file = config.c_output + max_attempts = 5 + attempt = 1 + success = False + + # Create a temporary file for the prompt + temp_prompt = os.path.join(config.temp_dir, "prompt.txt") + + # Create a simple starting C file to work with + create_c_file_manually(input_file, output_file) + + # Read detected functions + functions = [] + if os.path.exists(config.functions_file): + with open(config.functions_file, 'r') as f: + functions = [line.strip() for line in f if line.strip()] + + # Read source instructions if available + source_instructions = "" + if os.path.exists(config.SOURCE_INSTRUCTION_FILE): + with open(config.SOURCE_INSTRUCTION_FILE, 'r') as f: + source_instructions = f.read() + + # Build message for LLM + with open(temp_prompt, 'w') as f: + f.write("Convert the following Python code directly to C code.\n") + f.write("IMPORTANT: I've already created an initial C file for you to modify. DO NOT create a new file.\n") + f.write("EDIT THE EXISTING FILE DIRECTLY.\n\n") + f.write("The converted code should:\n") + f.write("1. Maintain all essential logic and algorithms\n") + f.write("2. Handle memory management appropriately\n") + f.write("3. Use equivalent C data structures and types\n") + f.write("4. Include necessary headers and dependencies\n") + f.write("5. Only output proper C code that can be parsed by a C compiler\n") + + # Add source instructions if available + if source_instructions: + f.write(source_instructions + "\n") + + # Add list of detected functions + f.write("\nImplement these functions identified during execution:\n") + for func in functions: + f.write(f"{func}\n") + + # Add Python code + f.write("\n=== PYTHON CODE ===\n") + with open(input_file, 'r') as py_file: + f.write(py_file.read()) + + # Add program output if available and not too large + if os.path.exists(config.program_output) and os.path.getsize(config.program_output) > 0: + with open(config.program_output, 'r') as out_file: + lines = out_file.readlines() + if len(lines) < 50: + f.write("\n=== PROGRAM OUTPUT (for reference) ===\n") + f.writelines(lines) + else: + f.write("\n=== PROGRAM OUTPUT SAMPLE (for reference) ===\n") + f.writelines(lines[:25]) + f.write("... (output truncated) ...\n") + + # Add initial C code + f.write("\n=== INITIAL C CODE (MODIFY THIS) ===\n") + with open(output_file, 'r') as c_file: + f.write(c_file.read()) + + print(f"📤 Sending code to LLM for conversion... : {temp_prompt}") + + # Prepare Docker for testing if needed + if config.USE_DOCKER and config.CONTAINER_ID: + # Use existing container + subprocess.run(["docker", "exec", config.CONTAINER_ID, "mkdir", "-p", "/workspace"], check=True) + debug_log(f"Using existing container: {config.CONTAINER_ID}") + + while attempt <= max_attempts and not success: + print(f"Attempt {attempt} of {max_attempts} to generate valid C code...") + + # Run aider to modify the C file + aider_wrapper(temp_prompt, output_file, config.LLM_MODEL) + + # Show the output file contents for debugging + debug_log("C code after aider (first 20 lines):") + with open(output_file, 'r') as f: + for i, line in enumerate(f): + if i < 20: + debug_log(line.rstrip()) + else: + break + + # Check if the generated C code is valid + if config.USE_DOCKER: + filename = os.path.basename(output_file) + output_dir = os.path.dirname(output_file) + + if config.CONTAINER_ID: + # Copy the file into an existing container + subprocess.run(["docker", "cp", output_file, f"{config.CONTAINER_ID}:/workspace/{filename}"], check=True) + result = subprocess.run( + ["docker", "exec", config.CONTAINER_ID, "esbmc", "--parse-tree-only", f"/workspace/{filename}"], + capture_output=True + ).returncode + else: + # Use a new container for the check + result = subprocess.run( + ["docker", "run", "--rm", "-v", f"{os.getcwd()}:/workspace", "-w", "/workspace", config.DOCKER_IMAGE, + "esbmc", "--parse-tree-only", filename], + capture_output=True + ).returncode + else: + # Local ESBMC + result = subprocess.run( + ["esbmc", "--parse-tree-only", output_file], + capture_output=True + ).returncode + + if result == 0: + print(f"✅ Successfully generated valid C code on attempt {attempt}") + success = True + else: + print(f"❌ ESBMC parse tree check failed on attempt {attempt}") + if attempt < max_attempts: + print("Retrying with additional instructions...") + # Add more specific instructions to fix syntax errors + with open(temp_prompt, 'a') as f: + f.write("\n=== CORRECTION INSTRUCTIONS ===\n") + f.write("The previous code had syntax errors. Please fix the C code to make it valid.\n") + f.write("Ensure you include all necessary headers and that all functions are properly defined.\n") + f.write("Use standard C syntax and avoid any C++ features.\n") + time.sleep(1) + + attempt += 1 + + os.remove(temp_prompt) + + if success: + print("✅ LLM conversion completed successfully.") + return True + else: + print(f"❌ Failed to generate valid C code after {max_attempts} attempts.") + return False + +def run_esbmc_for_function(function_name: str) -> int: + """Run ESBMC verification for a specific function.""" + if function_name == "": + function_name = "main" + + current_cmd = f"esbmc --function {function_name} \"{config.c_output}\"" + + print("----------------------------------------") + print(f"🛠️ Testing function: {function_name}") + print("ESBMC command to be executed:") + print(current_cmd) + print("----------------------------------------") + + if config.USE_DOCKER: + if config.CONTAINER_ID: + # The file should already be in the container + cmd = ["docker", "exec", "-w", "/workspace", config.CONTAINER_ID] + current_cmd.split() + return subprocess.run(cmd).returncode + else: + cmd = ["docker", "run", "--rm", "-v", f"{os.getcwd()}:/workspace", "-w", "/workspace", + config.DOCKER_IMAGE] + current_cmd.split() + return subprocess.run(cmd).returncode + else: + # Run locally + original_dir = os.getcwd() + os.chdir(config.temp_dir) + try: + return subprocess.run(current_cmd, shell=True).returncode + finally: + os.chdir(original_dir) + +def run_tracing_session() -> None: + """Run the interactive tracing session using sys.settrace.""" + py_script = os.path.basename(config.script_python) + + print(f"📌 Starting tracing for {config.script_python}...") + + # Create trace hook script + hook_script = create_trace_hook_script() + + # Run the trace script directly + original_dir = os.getcwd() + os.chdir(config.temp_dir) + + try: + with open(config.trace_output, 'w') as trace_file: + subprocess.run([sys.executable, "trace_hook.py"], + stdout=trace_file, + stderr=subprocess.STDOUT, + check=False) + finally: + os.chdir(original_dir) + + # Extract functions from the trace output + extract_function_calls() + + # Check if we have any functions + if not os.path.getsize(config.functions_file): + print("⚠️ No functions detected in trace.") + print("Last 20 lines of trace output:") + with open(config.trace_output, 'r') as f: + lines = f.readlines() + for line in lines[-20:]: + print(line.strip()) + else: + # Show detected functions + print("Detected functions:") + with open(config.functions_file, 'r') as f: + print(f.read()) + + # Extract program output (non-trace lines) + with open(config.trace_output, 'r') as trace_file, open(config.program_output, 'w') as program_file: + for line in trace_file: + if not line.startswith("funcname:") and not line.startswith("line:"): + program_file.write(line) + + # Show options + print("\nOptions:") + print(" 1) Convert to C and verify with ESBMC") + print(" 2) Restart tracing") + print(" 3) Exit tracing and cleanup") + + option = input("Enter option (1-3): ") + + if option == "1": + # Convert and verify + if convert_to_c(): + with open(config.functions_file, 'r') as f: + for function_name in f: + function_name = function_name.strip() + if function_name: + run_esbmc_for_function(function_name) + elif option == "2": + # Restart tracing + run_tracing_session() + elif option == "3": + # Exit tracing + print("✅ Tracing completed.") + else: + print("Invalid option, exiting.") + +def main() -> None: + """Main function to parse arguments and run the script.""" + parser = argparse.ArgumentParser(description="Dynamic trace and analyze Python code") + parser.add_argument("--docker", action="store_true", help="Run ESBMC in Docker container") + parser.add_argument("--image", help="Specify Docker image (default: esbmc)") + parser.add_argument("--container", help="Specify existing container ID") + parser.add_argument("--model", help="Specify LLM model") + parser.add_argument("filename", help="Python script to analyze") + + args = parser.parse_args() + + # Validate file existence + if not os.path.isfile(args.filename): + print(f"❌ Error: Python file '{args.filename}' does not exist.") + sys.exit(1) + + # Configure settings + config.script_python = args.filename + + if args.docker: + config.USE_DOCKER = True + + if args.image: + config.DOCKER_IMAGE = args.image + + if args.container: + config.CONTAINER_ID = args.container + + if args.model: + config.LLM_MODEL = args.model + + # Don't allow both image and container + if args.image and args.container: + print("Error: Cannot use both --image and --container") + show_usage() + + # Setup workspace + setup_workspace(args.filename) + + # Main tracing loop + while True: + run_tracing_session() + + # Ask if tracing should be restarted + while True: + reply = input("\n🔄 Do you want to restart tracing? (y = Yes, n = No): ") + if reply.lower() == 'y': + break # Restart loop + elif reply.lower() == 'n': + print("✅ Tracing completed.") + # Clean up + shutil.rmtree(config.temp_dir) + sys.exit(0) + else: + print("⚠️ Invalid input. Please enter 'y' for Yes or 'n' for No.") + +if __name__ == "__main__": + main() \ No newline at end of file From ef4d8914d2a6ca5b703fbcb012827b8d1a505701 Mon Sep 17 00:00:00 2001 From: hunterbrightdesign <70662742+hunterbrightdesign@users.noreply.github.com> Date: Wed, 5 Mar 2025 20:26:55 +0100 Subject: [PATCH 9/9] add stdout and stderr --- dynamic_trace.py | 93 +++++++++++++++++++++++++++++++++--------------- 1 file changed, 64 insertions(+), 29 deletions(-) diff --git a/dynamic_trace.py b/dynamic_trace.py index 7f269ed..cb79255 100644 --- a/dynamic_trace.py +++ b/dynamic_trace.py @@ -505,27 +505,39 @@ def convert_to_c() -> bool: filename = os.path.basename(output_file) output_dir = os.path.dirname(output_file) - if config.CONTAINER_ID: - # Copy the file into an existing container - subprocess.run(["docker", "cp", output_file, f"{config.CONTAINER_ID}:/workspace/{filename}"], check=True) - result = subprocess.run( - ["docker", "exec", config.CONTAINER_ID, "esbmc", "--parse-tree-only", f"/workspace/{filename}"], - capture_output=True - ).returncode - else: - # Use a new container for the check - result = subprocess.run( - ["docker", "run", "--rm", "-v", f"{os.getcwd()}:/workspace", "-w", "/workspace", config.DOCKER_IMAGE, - "esbmc", "--parse-tree-only", filename], - capture_output=True - ).returncode + try: + if config.CONTAINER_ID: + # Copy the file into an existing container + subprocess.run(["docker", "cp", output_file, f"{config.CONTAINER_ID}:/workspace/{filename}"], check=True) + cmd = ["docker", "exec", config.CONTAINER_ID, "esbmc", "--parse-tree-only", f"/workspace/{filename}"] + result = subprocess.run(cmd,check=True, text=True, capture_output=True) + print(result.stdout) + print(result.stderr) + result = result.returncode + else: + # Use a new container for the check + cmd = ["docker", "run", "--rm", "-v", f"{output_dir}:/workspace", "-w", "/workspace", config.DOCKER_IMAGE,"esbmc", "--parse-tree-only", filename] + result = subprocess.run(cmd,check=True, text=True, capture_output=True) + print(result.stdout) + print(result.stderr) + result = result.returncode + except subprocess.CalledProcessError as e: + print("Command failed with error code :", e.returncode) + print("Error output :", e.stderr) + result = e.returncode + else: # Local ESBMC - result = subprocess.run( - ["esbmc", "--parse-tree-only", output_file], - capture_output=True - ).returncode - + try: + cmd = ["esbmc", "--parse-tree-only", output_file] + result = subprocess.run(cmd,check=True, text=True, capture_output=True) + print(result.stdout) + print(result.stderr) + result = result.returncode + except subprocess.CalledProcessError as e: + print("Command failed with error code :", e.returncode) + print("Error output :", e.stderr) + result = e.returncode if result == 0: print(f"✅ Successfully generated valid C code on attempt {attempt}") success = True @@ -566,20 +578,35 @@ def run_esbmc_for_function(function_name: str) -> int: print("----------------------------------------") if config.USE_DOCKER: - if config.CONTAINER_ID: - # The file should already be in the container - cmd = ["docker", "exec", "-w", "/workspace", config.CONTAINER_ID] + current_cmd.split() - return subprocess.run(cmd).returncode - else: - cmd = ["docker", "run", "--rm", "-v", f"{os.getcwd()}:/workspace", "-w", "/workspace", - config.DOCKER_IMAGE] + current_cmd.split() - return subprocess.run(cmd).returncode + try: + if config.CONTAINER_ID: + # The file should already be in the container + cmd = ["docker", "exec", "-w", "/workspace", config.CONTAINER_ID] + current_cmd.split() + testresult = subprocess.run(cmd,check=True, text=True, capture_output=True) + print(testresult.stdout) + print(testresult.stderr) + else: + testfilename = os.path.basename(config.c_output) + testoutput_dir = os.path.dirname(config.c_output) + + cmd = ["docker", "run", "--rm", "-v", f"{testoutput_dir}:/workspace", "-w", "/workspace",config.DOCKER_IMAGE, "esbmc", "--function", function_name, testfilename] + testresult = subprocess.run(cmd,check=True, text=True, capture_output=True) + print(testresult.stdout) + print(testresult.stderr) + except subprocess.CalledProcessError as e: + print("Command failed with error code :", e.returncode) + print("Error output :", e.stderr) else: # Run locally original_dir = os.getcwd() os.chdir(config.temp_dir) try: - return subprocess.run(current_cmd, shell=True).returncode + testresult = subprocess.run(current_cmd, check=True, text=True, capture_output=True) + print(testresult.stdout) + print(testresult.stderr) + except subprocess.CalledProcessError as e: + print("Command failed with error code :", e.returncode) + print("Error output :", e.stderr) finally: os.chdir(original_dir) @@ -674,15 +701,23 @@ def main() -> None: if args.docker: config.USE_DOCKER = True + else: + config.USE_DOCKER = False if args.image: config.DOCKER_IMAGE = args.image + else : + config.DOCKER_IMAGE = "esbmc" if args.container: config.CONTAINER_ID = args.container + else: + config.CONTAINER_ID = False if args.model: config.LLM_MODEL = args.model + else: + config.LLM_MODEL = "openrouter/anthropic/claude-3.5-sonnet" # Don't allow both image and container if args.image and args.container: @@ -704,7 +739,7 @@ def main() -> None: elif reply.lower() == 'n': print("✅ Tracing completed.") # Clean up - shutil.rmtree(config.temp_dir) + # shutil.rmtree(config.temp_dir) sys.exit(0) else: print("⚠️ Invalid input. Please enter 'y' for Yes or 'n' for No.")