File size: 6,214 Bytes
8a23fcf 6ed9a00 8a23fcf 6ed9a00 8a23fcf | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 | """
Rhodawk AI — Lightweight Formal Verification Gate
=================================================
Uses Z3 (SMT solver) to perform bounded symbolic verification of
simple integer arithmetic, array bounds, and null-safety properties
extracted from Python diffs.
This is NOT a full program verifier. It covers:
1. Array/list index bounds — catches IndexError when indices are computable
2. Integer arithmetic — overflow / divide-by-zero on constant expressions
3. Assert statement reachability — checks user asserts are satisfiable
For complex code (loops, recursion, string ops) it returns SKIP, which does
NOT block the diff — Z3 gate is advisory, not blocking, unless a definitive
UNSAFE result is obtained.
Install: z3-solver (pip install z3-solver)
Enable: RHODAWK_Z3_ENABLED=true
"""
import os
import re
# W-004 FIX: Z3 formal verification gate is now ON by default.
# z3-solver is already pinned in requirements.txt. Operators may explicitly
# disable it with RHODAWK_Z3_ENABLED=false. A loud startup warning is emitted
# whenever Z3 is skipped (either disabled or import failure).
Z3_ENABLED = os.getenv("RHODAWK_Z3_ENABLED", "true").lower() == "true"
_IMPORT_OK = False
try:
import z3 as _z3
_IMPORT_OK = True
except ImportError:
pass
import sys as _sys
if not Z3_ENABLED:
print(
"[STARTUP WARNING] Z3 formal verification gate is DISABLED "
"(RHODAWK_Z3_ENABLED=false). Step 7b of the healing loop will "
"be skipped and no UNSAFE diffs will be blocked by Z3.",
file=_sys.stderr,
)
elif not _IMPORT_OK:
print(
"[STARTUP WARNING] Z3 formal verification gate is ENABLED but "
"z3-solver is not installed. Run: pip install z3-solver. "
"Step 7b of the healing loop will return SKIP.",
file=_sys.stderr,
)
def _extract_added_lines(diff_text: str) -> list[str]:
return [
line[1:].strip()
for line in diff_text.splitlines()
if line.startswith("+") and not line.startswith("+++")
]
def _check_divide_by_zero(lines: list[str]) -> list[str]:
"""Detect literal divide-by-zero: x / 0 or x % 0."""
issues = []
div_pat = re.compile(r"\b(\w+)\s*/\s*0\b")
mod_pat = re.compile(r"\b(\w+)\s*%\s*0\b")
for line in lines:
if div_pat.search(line):
issues.append(f"Literal divide-by-zero: {line}")
if mod_pat.search(line):
issues.append(f"Literal modulo-by-zero: {line}")
return issues
def _check_index_bounds(lines: list[str]) -> list[str]:
"""
Detect patterns like arr[N] where N is a literal integer and can use Z3
to verify the index is non-negative. For constant-length list literals
we also check upper bound.
"""
if not _IMPORT_OK:
return []
issues = []
idx_pat = re.compile(r"\b\w+\s*\[\s*(-?\d+)\s*\]")
for line in lines:
for m in idx_pat.finditer(line):
idx_val = int(m.group(1))
solver = _z3.Solver()
i = _z3.Int("i")
solver.add(i == idx_val)
solver.add(i < 0)
if solver.check() == _z3.sat:
issues.append(f"Negative literal index [{idx_val}]: {line}")
return issues
def _check_assert_satisfiability(lines: list[str]) -> list[str]:
"""
Check assert statements with simple integer inequalities using Z3.
assert x > 0 where x appears to be assigned a negative literal.
"""
if not _IMPORT_OK:
return []
issues = []
assign_pat = re.compile(r"(\w+)\s*=\s*(-?\d+)")
assert_pat = re.compile(r"assert\s+(\w+)\s*([><=!]+)\s*(-?\d+)")
assignments: dict[str, int] = {}
for line in lines:
for m in assign_pat.finditer(line):
assignments[m.group(1)] = int(m.group(2))
for line in lines:
m = assert_pat.search(line)
if m:
var, op, val_str = m.group(1), m.group(2), m.group(3)
if var in assignments:
lhs = assignments[var]
rhs = int(val_str)
solver = _z3.Solver()
x = _z3.Int("x")
solver.add(x == lhs)
op_map = {
">": x > rhs, ">=": x >= rhs, "<": x < rhs,
"<=": x <= rhs, "==": x == rhs, "!=": x != rhs,
}
constraint = op_map.get(op)
if constraint is not None:
solver.add(_z3.Not(constraint))
if solver.check() == _z3.sat:
issues.append(
f"Assert always fails: `{var} {op} {rhs}` "
f"but {var}={lhs}: {line}"
)
return issues
def run_formal_verification(diff_text: str) -> dict:
"""
Run Z3-backed formal verification on the diff.
Returns:
{
"verdict": "SAFE" | "UNSAFE" | "SKIP",
"issues": list[str],
"summary": str,
}
"""
if not Z3_ENABLED:
return {"verdict": "SKIP", "issues": [], "summary": "Z3 verification disabled"}
if not _IMPORT_OK:
return {
"verdict": "SKIP",
"issues": [],
"summary": "z3-solver not installed (pip install z3-solver)",
}
python_lines = _extract_added_lines(diff_text)
if not python_lines:
return {"verdict": "SKIP", "issues": [], "summary": "No added lines to verify"}
all_issues: list[str] = []
try:
all_issues.extend(_check_divide_by_zero(python_lines))
all_issues.extend(_check_index_bounds(python_lines))
all_issues.extend(_check_assert_satisfiability(python_lines))
except Exception as e:
return {
"verdict": "SKIP",
"issues": [],
"summary": f"Z3 verification exception (non-blocking): {e}",
}
if all_issues:
return {
"verdict": "UNSAFE",
"issues": all_issues,
"summary": f"Z3 found {len(all_issues)} formal issue(s): {all_issues[0]}",
}
return {
"verdict": "SAFE",
"issues": [],
"summary": "Z3 found no definitive integer/bounds violations in added lines",
}
|