Checking SQL code with SQLGlot

[andrew222651]

SQLGlot has a pure Python SQL engine. So it would be cool if we could use CrossHair to check SQL code.

from typing import TypedDict

from sqlglot.executor import Table, execute


class Part(TypedDict):
    pnum: int
    qoh: int

def silly1(parts: list[Part]) -> list[tuple[int]]:
    stmt = """
    select parts.pnum
    from parts
    """
    return execute(
        stmt,
        tables=dict(parts=parts),
        schema=dict(parts=dict(pnum="int", qoh="int")),
    ).rows

def silly2(parts: list[Part]) -> list[tuple[int]]:
    stmt = """
    select parts.pnum
    from parts
    where false
    """
    return execute(
        stmt,
        tables=dict(parts=parts),
        schema=dict(parts=dict(pnum="int", qoh="int")),
    ).rows

However, crosshair diffbehavior on silly1 and silly2 gives "All paths exhausted, functions are likely the same!". What would we need to do to make this work?

[andrew222651]

Hmm

752834.407|      |describe_behavior() user-level exception found
TypeError('TypedDict does not support instance and class checks') <FrameSummary
file
/code/sqlcross/.venv/lib/python3.10/site-packages/crosshair/diff_behavior.py,
line 69 in describe_behavior> <FrameSummary file
/code/sqlcross/p.py, line 45 in silly1> <FrameSummary file
/code/sqlcross/.venv/lib/python3.10/site-packages/sqlglot/executor/__init__.py,
line 33 in execute> <FrameSummary file
/code/sqlcross/.venv/lib/python3.10/site-packages/sqlglot/executor/table.py,
line 110 in ensure_tables> <FrameSummary file
/code/sqlcross/.venv/lib/python3.10/site-packages/sqlglot/executor/table.py,
line 128 in _ensure_tables> <FrameSummary file
/code/sqlcross/.venv/lib/python3.10/site-packages/sqlglot/executor/table.py,
line 128 in <listcomp>> <FrameSummary file
/code/sqlcross/.venv/lib/python3.10/site-packages/crosshair/libimpl/builtinslib.py,
line 1808 in __iter__> <FrameSummary file
/code/sqlcross/.venv/lib/python3.10/site-packages/crosshair/libimpl/builtinslib.py,
line 388 in smt_to_ch_value> <FrameSummary file
/code/sqlcross/.venv/lib/python3.10/site-packages/crosshair/statespace.py,
line 927 in find_key_in_heap> <FrameSummary file
/code/sqlcross/.venv/lib/python3.10/site-packages/crosshair/dynamic_typing.py,
line 123 in unify> <FrameSummary file
/nix/store/dlhmz1f440qvxdxcbpnx3xqwdz4m1c7x-python3-3.10.4/lib/python3.10/typing.py,
line 2384 in __subclasscheck__>

[andrew222651]

I guess TypedDicts are a no-go.

...
from dataclasses import dataclass

@dataclass
class PartClass:
    pnum: int
    qoh: int

...

def silly1(parts: list[PartClass]) -> list[tuple[int]]:
    stmt = """
    select parts.pnum
    from parts
    """
    dict_parts = [
        {"pnum": p.pnum, "qoh": p.qoh}
        for p in parts
    ]
    return execute(
        stmt,
        tables=dict(parts=dict_parts),
        schema=dict(parts=dict(pnum="int", qoh="int")),
    ).rows

def silly2(parts: list[PartClass]) -> list[tuple[int]]:
    stmt = """
    select parts.pnum
    from parts
    where false
    """
    dict_parts = [
        {"pnum": p.pnum, "qoh": p.qoh}
        for p in parts
    ]
    return execute(
        stmt,
        tables=dict(parts=dict_parts),
        schema=dict(parts=dict(pnum="int", qoh="int")),
    ).rows

Output:

Given: (parts=[PartClass(pnum=0, qoh=0)]),
  p.silly1 : returns [(0,)]
  p.silly2 : returns []

[andrew222651]

So thanks to @tobymao we get functionality similar to @akcheung's Cosette. Cosette is probably a little more powerful than this but it only supports integer types and requires a special form of SQL.

I wonder what other languages have pure-Python interpreters.

[tobymao]

cool! fyi you shouldn’t need to pass schema

[pschanely]

Oh wow. It would be amazing to get this working.

Indeed, you've run into an issue with TypedDicts, specifically when inside containers. It'll take me a day or two to make sure I fix that correctly.

I'm sort of shocked to see that the rest of the process works out. (even a small difference like where pnum > 42 vs where pnum > 43 is detectable!)

[pschanely]

Yup! I should be able to get the regular TypedDicts to work as well with a fix. I'm curious whether this scales to realistic SQL.

[tobymao]

the execution engine is new, but we can pass around 17 tpc-h queries

[pschanely]

the execution engine is new, but we can pass around 17 tpc-h queries

Very cool! To clarify, though, my curiosity was mostly about CrossHair's ability (or inability) to effectively reason about SQLGlot's SQL execution code. To the extent it doesn't, I'd love to add examples to CrossHair's benchmark suite.

[petrusboniatus]

I think this is almost equivalent to the dataframe discussion and the associated issue in terms of performance. Though you are starting from sql equality instead of pre and post conditions, I think it ultimately boils down improve the same parts (mainly how to scale when you add a bigger number of columns and different types). So If one is solved the other is solved, I will keep an eye on this.

[andrew222651]

A note in regards to "realistic SQL":

These two queries come from the "count bug" here.

from typing import TypedDict

from sqlglot.executor import execute


class Part(TypedDict):
    pnum: int
    qoh: int

class Supply(TypedDict):
    pnum: int
    shipdate: int

schema = dict(
    parts=dict(pnum="int", qoh="int"),
    supplies=dict(pnum="int", shipdate="int"),
)

def q1td(parts: list[Part], supplies: list[Supply]) -> list[tuple[int]]:
    stmt = """
    select parts.pnum
    from parts
    where parts.qoh = (
        select count(supplies.shipdate)
        from supplies
        where supplies.pnum = parts.pnum and supplies.shipdate < 10
    )
    """
    return execute(
        stmt,
        tables=dict(parts=parts, supplies=supplies),
        schema=schema,
    ).rows

def q2td(parts: list[Part], supplies: list[Supply]) -> list[tuple[int]]:
    stmt = """
    select parts.pnum
    from parts, (
        select supplies.pnum as pnum, count(supplies.shipdate) as cnt
        from supplies
        where supplies.shipdate < 10
        group by supplies.pnum
    ) temp
    where parts.qoh = temp.cnt and parts.pnum = temp.pnum
    """
    return execute(
        stmt,
        tables=dict(parts=parts, supplies=supplies),
        schema=schema,
    ).rows

The diffbehavior command with a high --per_condition_timeout (e.g. 1000) gave

Given: (parts=[{'pnum': 0, 'qoh': 0}], supplies=[{'pnum': 0, 'shipdate': 10}]),
  file.q1td : returns [(0,)]
  file.q2td : returns []

which is awesome (although parts=[{'pnum': 0, 'qoh': 0}], supplies=[] is a "simpler" counterexample).

With the default --per_condition_timeout, however, it was giving

Given: (parts=[], supplies=[{'pnum': 0, 'shipdate': 0}]),
  file.q1td : raises ExecuteError("Step 'Scan: supplies (140433704447536)' failed: ")
  file.q2td : raises ExecuteError("Step 'Scan: supplies (140433730083888)' failed: ")

which is confusing because when you run the functions on those inputs they don't raise those exceptions.

[pschanely]

Thanks for the example @amacfie! While improving performance is a priority, false positives are always bugs, so I've filed #196. (as you may have guessed, sqlglot's exception handling is handling CrossHair's timeout exception) Solving that particular problem shouldn't be a huge lift, though I am spread a little thin these days - hopefully soon.