github/tinygrad
1
1
Fork 0
mirror of https://github.com/tinygrad/tinygrad.git synced 2026-01-10 23:48:01 -05:00
Code Issues Packages Projects Releases Wiki Activity

profile z3 (#12248)

Browse Source
This commit is contained in:
Sieds Lykles
2025-09-19 22:52:06 +02:00
committed by GitHub
parent 7e06d3ebba
commit bb1f376ae6
1 changed files with 7 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

13
tinygrad/uop/spec.py
View File

@@ -1,7 +1,7 @@
from typing import cast, Callable
from tinygrad.uop.ops import PatternMatcher, UPat, GroupOp, Ops, UOp, print_uops, python_alu, graph_rewrite
from tinygrad.dtype import DType, ImageDType, dtypes, PtrDType, AddrSpace, Invalid
from tinygrad.helpers import all_same, prod, DEBUG, ContextVar, Context
from tinygrad.helpers import all_same, prod, DEBUG, ContextVar, Context, cpu_profile
from tinygrad.shape.shapetracker import ShapeTracker
try:
import z3
@@ -138,11 +138,12 @@ def validate_index(idx:UOp, gate:UOp=UOp.const(dtypes.bool, True)):
solver = z3.Solver(ctx=z3.Context())
z3_idx, z3_mask = uops_to_z3(solver, idx.src[1], mask)
solver.add(z3_mask)
if solver.check((z3_idx<0)|(sz<=z3_idx)) == z3.sat:
print(f"idx={idx.src[1].render(simplify=False)}")
print(f"mask & gate={mask.render(simplify=False)}")
print(f"# OUT OF BOUNDS ACCESS: at {solver.model()} INDEX not in 0 - {sz}\nconstraints = {solver}")
return False
with cpu_profile("validate index with z3", "TINY"):
if solver.check((z3_idx<0)|(sz<=z3_idx)) == z3.sat:
print(f"idx={idx.src[1].render(simplify=False)}")
print(f"mask & gate={mask.render(simplify=False)}")
print(f"# OUT OF BOUNDS ACCESS: at {solver.model()} INDEX not in 0 - {sz}\nconstraints = {solver}")
return False
return True
def validate_store(idx:UOp, val:UOp, gate:UOp=UOp.const(dtypes.bool, True)):