Skip to content

Instantly share code, notes, and snippets.

@muxator

muxator/execute_z3py_docs.py

Last active September 26, 2025 23:02
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save muxator/eea773ceb9bfc362a32f7522780d5a03 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save muxator/eea773ceb9bfc362a32f7522780d5a03 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
execute_z3py_docs.py
#!/usr/bin/env python
#
# This script goes through the z3guide (https://github.com/microsoft/z3guide)
# python documentation, extracts the z3 snippets and executes them in a
# subintepreter, reporting errors.
#
# This is a follow-up to: https://github.com/microsoft/z3guide/pull/206
#
# Requires python >= 3.14
from __future__ import annotations
import dataclasses
import sys
import textwrap
from concurrent import interpreters
from pathlib import Path
from typing import TYPE_CHECKING, override
import mistletoe
import mistletoe.ast_renderer
if TYPE_CHECKING:
from collections.abc import Generator
SCRIPT_DIR = Path(__file__).parent.resolve()
@dataclasses.dataclass
class ExecutionResult:
stdout: str
stderr: str
error: interpreters.InterpreterError | SyntaxError | None
@property
def is_success(self) -> bool:
return self.error is None
@property
def is_failure(self) -> bool:
return self.error is not None
class SubinterpreterExecutor:
def __init__(self) -> None:
self._interpreter = interpreters.create()
self._stdout_q = interpreters.create_queue()
self._stderr_q = interpreters.create_queue()
self._stdout_id = self._stdout_q.id
self._stderr_id = self._stderr_q.id
@staticmethod
def _get_queue_contents_as_str(queue: interpreters.Queue) -> str:
contents = ""
try:
while True:
contents += queue.get_nowait()
except interpreters.QueueEmpty:
return contents
def execute_code(self, code: str) -> ExecutionResult:
error: interpreters.InterpreterError | SyntaxError | None = None
code_prefix = textwrap.dedent(f"""
### CODE PREFIX - START
import sys
from concurrent import interpreters
class StreamQueue:
def __init__(self, queue: interpreters.Queue):
self._queue = queue
def write(self, msg):
self._queue.put(msg)
stdout_q = StreamQueue(interpreters.Queue({self._stdout_id}))
stderr_q = StreamQueue(interpreters.Queue({self._stderr_id}))
sys.stdout = stdout_q
sys.stderr = stderr_q
### CODE PREFIX - END
""")
wrapped_code = code_prefix + code
try:
self._interpreter.exec(wrapped_code)
except (interpreters.InterpreterError, SyntaxError) as e:
error = e
# gather stdout and stderr contents
stdout = self._get_queue_contents_as_str(self._stdout_q)
stderr = self._get_queue_contents_as_str(self._stderr_q)
return ExecutionResult(stdout, stderr, error)
@dataclasses.dataclass(kw_only=True)
class ExecutionStats:
file_name: str
line_number: int
snippet_id: int
stdout: str
stderr: str
# We also need to catch SyntaxError because of a peculiar behaviour of
# subinterpreters. See https://github.com/python/cpython/issues/139324
error: interpreters.ExecutionFailed | SyntaxError | None
@property
def was_successful(self) -> bool:
return self.error is None
class RawAstRenderer(mistletoe.ast_renderer.AstRenderer):
@override
def render(self, token) -> dict:
return mistletoe.ast_renderer.get_ast(token)
def z3_snippets_from_ast(mistletoe_ast: dict) -> Generator[int, str]:
for child in mistletoe_ast["children"]:
if child["type"] != "CodeFence":
continue
if child["language"] != "z3-python":
continue
assert len(child["children"]) == 1
code_block = child["children"][0]
assert code_block["type"] == "RawText"
z3_snippet = code_block["content"]
yield child["line_number"], z3_snippet
def do_stats(stats_list: list[ExecutionStats]) -> tuple[str, int]:
s = "=== EXECUTION STATS ===\n"
error_count = 0
for execution_stats in stats_list:
if not execution_stats.was_successful:
error_count += 1
s += f"{execution_stats}\n"
s += f"There were {error_count} errors over {len(stats_list)} snippets\n"
return (s, error_count)
def main(base_path: Path) -> int:
base_path = base_path.resolve()
if not base_path.is_dir():
print(f'"{base_path}" is not an existing directory')
return 1
stats_list: list[ExecutionStats] = []
executor = SubinterpreterExecutor()
for md_file in base_path.glob("*.md"):
print(f"=== VALIDATING FILE {md_file.name} - START ===")
with md_file.open("r") as fin:
rendered = mistletoe.markdown(fin, renderer=RawAstRenderer)
i = 0
count_success = 0
for i, (line_number, z3_snippet) in enumerate(
z3_snippets_from_ast(rendered),
start=1,
):
print(f'=== Executing snippet #{i} in "{md_file.name}:{line_number}" ===')
# Execute the z3_snippet program in a python 3.14 subintepreter.
src = "from z3 import *\n\n" + z3_snippet
result = executor.execute_code(src)
stats_list.append(
ExecutionStats(
file_name=md_file.name,
line_number=line_number,
snippet_id=i,
stdout=result.stdout,
stderr=result.stderr,
error=result.error,
),
)
if result.is_success:
print("SUCCESS")
count_success += 1
else:
print("FAILURE")
if i == 0:
print("No z3 snippets found")
print(f"=== FINISHED VALIDATING {md_file.name}. {count_success} out of {i} snippets were successful ===")
(msg, error_count) = do_stats(stats_list)
print(msg)
return 0 if error_count == 0 else 1
if __name__ == "__main__":
if len(sys.argv) > 1:
base_path = Path(sys.argv[1])
else:
base_path = (
SCRIPT_DIR
/ ".."
/ "website"
/ "docs-programming"
/ "02 - Z3 Python - Readonly"
).resolve()
print(f'No path given, using "{base_path}" as default')
sys.exit(main(base_path))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment