Skip to content

Commit 6ec99a2

Browse files
committed
Better console output
1 parent 8bad3c3 commit 6ec99a2

File tree

6 files changed

+72
-100
lines changed

6 files changed

+72
-100
lines changed

benchmark.py

Lines changed: 2 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@
77
import sys
88
import argparse
99

10-
# --- MODIFIED: Import the analyzer function directly! ---
1110
from main import analyze_halting
1211

1312
# --- Configuration ---
@@ -38,14 +37,12 @@
3837
# --- Helper Functions for Corpus Creation ---
3938

4039
def create_directory(path: Path):
41-
"""Creates a directory if it doesn't exist."""
4240
path.mkdir(parents=True, exist_ok=True)
4341

4442
def collect_stdlib():
4543
create_directory(STDLIB_DEST)
4644
stdlib_path = Path(shutil.__file__).parent
4745
print(f"Collecting files from stdlib at: {stdlib_path}")
48-
# ... (rest of function is the same as your previous version)
4946
file_count = 0
5047
for root, _, files in os.walk(stdlib_path):
5148
for file in files:
@@ -59,11 +56,10 @@ def collect_stdlib():
5956
def download_and_unpack_pypi():
6057
create_directory(PYPI_DEST)
6158
print("Downloading PyPI packages...")
62-
# ... (rest of function is the same as your previous version)
6359
try:
6460
subprocess.run([sys.executable, "-m", "pip", "download", "--no-deps", "--dest", str(PYPI_DEST), *PYPI_PACKAGES], check=True, capture_output=True)
6561
except subprocess.CalledProcessError as e:
66-
print(f"pip download failed: {e.stderr}. Skipping.")
62+
print(f"pip download failed: {e.stderr.decode()}. Skipping.")
6763
return
6864
unpacked_dir = PYPI_DEST / "unpacked"
6965
create_directory(unpacked_dir)
@@ -94,7 +90,6 @@ def download_and_unpack_pypi():
9490
shutil.rmtree(unpacked_dir)
9591
print(f"Collected {file_count} PyPI .py files.")
9692

97-
9893
def generate_synthetic_non_halting():
9994
create_directory(SYNTHETIC_DEST)
10095
for i in range(NUM_SYNTHETIC):
@@ -123,8 +118,6 @@ def setup_complex():
123118

124119
def run_benchmark(force_rebuild=False):
125120
"""Builds the corpus if needed, then runs the analyzer and calculates the score."""
126-
127-
# --- Phase 1: Build the corpus (with caching) ---
128121
if force_rebuild and BENCHMARK_DIR.exists():
129122
print("--- Force-rebuilding corpus: Deleting existing suite... ---")
130123
shutil.rmtree(BENCHMARK_DIR)
@@ -141,7 +134,6 @@ def run_benchmark(force_rebuild=False):
141134
print("--- Phase 1: Found existing benchmark suite. Skipping build. ---")
142135
print("(Use --rebuild flag to force a fresh build)")
143136

144-
# --- Phase 2: Run analysis and calculate score ---
145137
print("\n--- Phase 2: Running Analyzer & Calculating Score ---")
146138
total_files = 0
147139
correct_predictions = 0
@@ -167,7 +159,7 @@ def run_benchmark(force_rebuild=False):
167159

168160
try:
169161
program_code = file_path.read_text(encoding='utf-8', errors='ignore')
170-
analyzer_result = analyze_halting(program_code)
162+
analyzer_result, _ = analyze_halting(program_code) # Unpack and ignore reason
171163

172164
is_correct = False
173165
if name == "halting":
@@ -185,22 +177,19 @@ def run_benchmark(force_rebuild=False):
185177

186178
except Exception:
187179
print(" " * len(progress), end='\r')
188-
# Silently fail on individual analysis errors, but count as incorrect
189180
pass
190181

191182
print(" " * 80, end='\r')
192183

193184
sys.stderr.close()
194185
sys.stderr = original_stderr
195186

196-
# --- Final Score ---
197187
if total_files > 0:
198188
percentage = (correct_predictions / total_files) * 100
199189
print(f"\n--- Practical Success Rate: {percentage:.2f}% ({correct_predictions} of {total_files} files passed) ---")
200190
else:
201191
print("\nNo files were found in the benchmark suite to analyze.")
202192

203-
204193
if __name__ == "__main__":
205194
parser = argparse.ArgumentParser(description="Run the Halting Analyzer benchmark.")
206195
parser.add_argument(

components/dynamic_tracing.py

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,15 @@
11
import sys
2-
import re # <-- Add this import
2+
import re
33
from collections import defaultdict
44

5-
def dynamic_tracing(program: str) -> str:
6-
"""Phase 3: Dynamic tracing to detect non-halting behavior."""
5+
def dynamic_tracing(program: str) -> tuple[str, str]:
6+
"""
7+
Phase 3: Dynamic tracing to detect non-halting behavior.
8+
Returns a tuple of (result, reason).
9+
"""
710
try:
8-
# --- MODIFIED: Replace the blunt string search with a more precise regex ---
9-
# This looks for 'analyze_halting' followed by an opening parenthesis '(',
10-
# which is a much stronger signal of a function call than a simple substring.
11-
# This prevents false positives on comments or variable names.
1211
if re.search(r"analyze_halting\s*\(", program):
13-
return "does not halt" # Probable self-referential call
12+
return "does not halt", "Dynamic tracing: Pre-execution check found a probable call to the analyzer."
1413

1514
trace_log = []
1615
call_depth = defaultdict(int)
@@ -40,18 +39,19 @@ def trace(frame, event, arg):
4039
exec(program, {})
4140
except RecursionError:
4241
sys.settrace(None)
43-
return "does not halt"
42+
return "does not halt", "Dynamic tracing: Execution exceeded maximum recursion depth."
4443
except RuntimeError as e:
45-
if "Cycle detected" in str(e) or "Trace log exceeded" in str(e):
46-
sys.settrace(None)
47-
return "does not halt"
44+
sys.settrace(None)
45+
if "Cycle detected" in str(e):
46+
return "does not halt", "Dynamic tracing: Execution trace entered a deterministic loop."
47+
elif "Trace log exceeded" in str(e):
48+
return "does not halt", "Dynamic tracing: Execution exceeded maximum trace log size."
4849
else:
49-
sys.settrace(None)
50-
return "halts"
50+
return "halts", f"Dynamic tracing: Execution terminated with a runtime error: {str(e)}."
5151
except Exception as e:
5252
sys.settrace(None)
53-
return "halts" # Exceptions terminate execution
53+
return "halts", f"Dynamic tracing: Execution terminated with an exception: {type(e).__name__}."
5454
sys.settrace(None)
55-
return "halts"
55+
return "halts", "Dynamic tracing: Program executed to completion without issue."
5656
except Exception as e:
57-
return f"impossible to determine: {str(e)}"
57+
return "impossible to determine", f"Dynamic tracing: An internal error occurred: {str(e)}."

components/heuristic_classifier.py

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -151,27 +151,26 @@ def _is_comparison(self, node, var_name, op, val):
151151
isinstance(node.comparators[0], ast.Constant) and node.comparators[0].value == val)
152152

153153

154-
def classify_known_problems(program: str) -> str:
154+
def classify_known_problems(program: str) -> tuple[str, str]:
155155
"""
156156
Phase 1.5: Heuristically check for known hard problems.
157-
If a known pattern is found, we classify it as impossible to determine
158-
without running it.
157+
Returns a tuple of (result, reason).
159158
"""
160159
try:
161160
tree = ast.parse(program)
162161

163162
collatz_visitor = CollatzVisitor()
164163
collatz_visitor.visit(tree)
165164
if collatz_visitor.is_collatz_like:
166-
return "impossible to determine"
165+
return "impossible to determine", "Heuristic classification: Detected a structure matching the Collatz conjecture."
167166

168167
ackermann_visitor = AckermannVisitor()
169168
ackermann_visitor.visit(tree)
170169
if ackermann_visitor.is_ackermann_like:
171-
return "impossible to determine"
170+
return "impossible to determine", "Heuristic classification: Detected a structure matching the Ackermann function."
172171

173172
except Exception:
174173
# If parsing or classification fails, defer the decision.
175-
return "continue"
174+
return "continue", ""
176175

177-
return "continue"
176+
return "continue", ""

components/static_analysis.py

Lines changed: 9 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,9 @@
11
import ast
22

3-
def is_constant_true(node):
4-
"""Check if an AST node is a constant True value."""
5-
return isinstance(node, ast.Constant) and node.value is True
6-
7-
def static_preparation(program: str) -> str:
3+
def static_preparation(program: str) -> tuple[str, str]:
84
"""
95
Phase 1: Static analysis to find obvious halting or non-halting cases.
10-
- Detects `while True` loops for non-halting.
11-
- NEW: Detects recursive function calls as a form of non-trivial complexity.
12-
- Confirms halting only if NO loops AND NO recursion are present.
6+
Returns a tuple of (result, reason).
137
"""
148
try:
159
tree = ast.parse(program)
@@ -22,8 +16,8 @@ def static_preparation(program: str) -> str:
2216
if isinstance(node, (ast.For, ast.While)):
2317
has_loops = True
2418
# Check for the definitive non-halting case
25-
if isinstance(node, ast.While) and is_constant_true(node.test):
26-
return "does not halt"
19+
if isinstance(node, ast.While) and isinstance(node.test, ast.Constant) and node.test.value is True:
20+
return "does not halt", "Static analysis: Detected a 'while True' infinite loop."
2721

2822
# Check for any function that calls itself
2923
elif isinstance(node, ast.FunctionDef):
@@ -40,13 +34,12 @@ def static_preparation(program: str) -> str:
4034

4135
# The most definitive halting case: a program with no loops and no recursion.
4236
if not has_loops and not has_recursion:
43-
return "halts"
37+
return "halts", "Static analysis: Program has no loops or recursion, so it must halt."
4438

45-
# If we have found loops (that aren't `while True`) or recursion,
46-
# the program is too complex for a simple static decision. Defer.
47-
return "impossible to determine"
39+
# If we have found loops (that aren't `while True`) or recursion, defer.
40+
return "impossible to determine", "Static analysis: Program contains complex loops or recursion that could not be proven to terminate."
4841

4942
except SyntaxError:
50-
return "impossible to determine: syntax error"
43+
return "impossible to determine", "Static analysis: Could not parse the script due to a syntax error."
5144
except Exception as e:
52-
return f"impossible to determine: {str(e)}"
45+
return "impossible to determine", f"Static analysis: An unexpected error occurred: {str(e)}"

components/symbolic_prover.py

Lines changed: 7 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
import ast
22
from z3 import Solver, Int, sat, And, Or, Not
33

4-
def prove_termination(program: str) -> str:
4+
def prove_termination(program: str) -> tuple[str, str]:
55
"""
6-
An advanced symbolic analysis phase that attempts to prove termination for
7-
a class of loops that the static analyzer cannot.
6+
An advanced symbolic analysis phase that attempts to prove termination.
7+
Returns a tuple of (result, reason).
88
"""
99
try:
1010
tree = ast.parse(program)
@@ -18,15 +18,10 @@ def prove_termination(program: str) -> str:
1818
node.iter.func.id == 'range' and
1919
len(node.iter.args) == 1 and
2020
isinstance(node.iter.args[0], ast.Constant)):
21-
# A for loop over a constant range is definitively halting.
22-
# This is a simplification; a full implementation would check
23-
# the loop body for 'break' or other non-halting behavior.
24-
# For our purposes, we'll call this a success.
25-
return "halts"
21+
return "halts", "Symbolic prover: Proved termination of a 'for' loop with a constant range."
2622

2723
# Case 2: Handle simple 'while var < const' loops with clear progress
2824
elif isinstance(node, ast.While):
29-
# We'll analyze loops like 'while x < 10:'
3025
if not (isinstance(node.test, ast.Compare) and
3126
len(node.test.ops) == 1 and
3227
isinstance(node.test.ops[0], (ast.Lt, ast.LtE, ast.Gt, ast.GtE)) and
@@ -35,10 +30,6 @@ def prove_termination(program: str) -> str:
3530
continue
3631

3732
var_name = node.test.left.id
38-
loop_var = Int(var_name)
39-
40-
# Check for an increment/decrement in the loop body
41-
# This is a simplified check; a real prover would be more robust.
4233
update_found = False
4334
for body_stmt in node.body:
4435
if (isinstance(body_stmt, ast.Assign) and
@@ -49,20 +40,13 @@ def prove_termination(program: str) -> str:
4940
body_stmt.value.left.id == var_name and
5041
isinstance(body_stmt.value.op, ast.Add) and
5142
isinstance(body_stmt.value.right, ast.Constant)):
52-
53-
# We found 'x = x + const'. This is progress.
5443
update_found = True
5544
break
5645

5746
if update_found:
58-
# Using Z3, we could formally prove a ranking function, but
59-
# for this practical heuristic, identifying clear progress
60-
# towards the termination condition is enough to assume halting.
61-
return "halts"
47+
return "halts", "Symbolic prover: Proved termination of a 'while' loop with a clear progress condition."
6248

63-
# If we analyzed all nodes and couldn't prove anything, defer.
64-
return "impossible to determine"
49+
return "impossible to determine", "Symbolic prover: Could not prove termination for any loop structures."
6550

6651
except Exception:
67-
# If any error occurs during this complex phase, defer.
68-
return "impossible to determine"
52+
return "impossible to determine", "Symbolic prover: An internal error occurred during analysis."

0 commit comments

Comments
 (0)