Discover more branches by inspecting the AST

[Zac-HD]

What's the idea?

Let's consider the simple function f, and imagine executing it with a symbolic value x=0:

def f(x: int) -> Optional[bool]:
     if x > 0:
        if x % 2:
           return True
       return False
    return None

Because we execute if x > 0:, we discover both the False (taken) branch and it's negation but don't discover the un-executed inner branch if x % 2:. Execution isn't the only way to discover what code does though - we could also read it, or write a program to analyse the abstract syntax tree of f:

body=[
  If(
    test=Compare(left=Name(id='x', ctx=Load()), ops=[Gt()], comparators=[Num(n=0)]),  # We already found this one
    body=[
      If(
        test=BinOp(left=Name(id='x', ctx=Load()), op=Mod(), right=Num(n=2)),  # but *didn't* see this branch
        body=[Return(value=NameConstant(value=True))],
        orelse=[]),
      Return(value=NameConstant(value=False))
    ],
    orelse=[]),
  Return(value=NameConstant(value=None))
]

The Fuzzing Book has a chapter on symbolic fuzzing for Python, which is both useful background reading and a good source of starter code!

Why bother?

A trivial answer is that finding more branches per executed example is faster, and who doesn't like improved performance? More seriously, I think this would allow CrossHair to support more programs as well as improving how it tests those which are already supported.

The current "concolic" analysis is fantastic, and handles cases such as dict-based control flow which cannot be inferred from a simple syntactic analysis (but doesn't see inner branches). On the other hand, this AST-based approach can handle cases where it's very difficult to patch in symbolic objects at runtime (but doesn't handle complicated scoping or control-flow issues).

I think it's possible, and feasible, to combine these approaches at runtime using e.g. ast.parse(inspect.getsource(f)) and therefore to keep the strengths and work around the weaknesses of each 🙂

[pschanely]

Thanks for writing this up, Zac! I like this idea a lot. It will be a while before I would be able to personally prioritize an effort like this, but for all you internet folks, I am very willing to consult with anyone who wants to give it a try!

[Zac-HD]

I think this is the approach that life4/deal#72 is taking - maybe a chance to share some code?

[pschanely]

I'm hoping so; I've started a conversation with @orsinium :)

The general case is so challenging: operator overloads, the descriptor protocol, variable scoping rules, aliasing in the heap, evaluation order issues. By leaning on the real interpreter, CrossHair gets a lot of stuff for free.

Of course, our solution is: don't handle the general case! What remains to be understood, in my mind, is how far we can get.

Notably, I chatted quickly with @jpolitz after @jeanqasaur's PLTalk recently who worked on this formalization of Python semantics. Joe described it as "how much of Python can we implement with other parts of Python," which feels like it might be helpful in an endeavor like this.

[orsinium]

Last weekend, I bought a binary wristwatch. And while doing a conversion from 2-base to 10-base I noticed that sum of 2^n + 2^(n+2) ends on 0 in 10-base for all integer n > 0. In other words:

(2^n + 2^(n+2)) % 10 == 0

It's easy to prove:

(2^n + 2^(n+2)) % 10 == 0
(2^n * 1 + 2^n * 2^2) % 10 == 0
(2^n * 5) % 10 == 0
2^n % 2 == 0  # <- true for any n > 0, let's just stop here

Can we prove it using z3? Let's try:

import z3
s = z3.Solver()
n = z3.Int('n')
s.add(n > 0)
s.add(z3.Not((2**n + 2**(n+2)) % 10 == 0))
s.check()
# unknown

The result is unknown and s.model() raises "model is not available". Why so? IDK. Something is up with powers, I suppose:

z3.solve(2 ** n == 2)
# failed to solve

Another issue is that SeqSort doesn't have an implementation for str.count, so I implemented it as a recursive function. It works for simple examples but freezes dead trying to prove when the given sequence is a z3.Const.

Another topic is how many things I patch to make arithmetic work as in Python (special thanks to Hypothesis for catching it all, BTW). For example:

# "rounds" to 0
-5 // 2
# -3

# rounds to the closest even
z3.solve(z3.Int('n') == z3.IntVal(-5) / z3.IntVal(3))
# [n = -2]

Why am I telling it all? Well, because I doubt my decision to 100% rely on z3 solving everything I feed in it. So, probably, the best approach is somewhere between CrossHair and deal, closer to CrossHair: try to be strict and convert as much as possible but at the same time not so heavily rely on z3.

[andrew222651]

Z3 might not be able to solve 2ⁿ = 2 but Mathematica can, over integers and rationals.

[pschanely]

@orsinium everything you are saying here is VERY familiar to me!

Nonlinear arithmetic is not decidable, and indeed, you can pretty much forget about raising to a symbolic power. For this kind of problem (and for others that get too complex for Z3), we gradually fall back to supplying a mixture of concrete & symbolic values. (because taking a symbolic to a constant power sometimes does work!) (example CrossHair test case)

CrossHair does this for floordiv. Another tactic you'll see in there is the smt_fork() call - this specializes execution to one branch or the other. Essentially, adding assumptions along the way can help put less load on Z3 (at the cost of having to do more executions to cover all the possible cases).

Probably this should move to another discussion, but I am very curious about the kinds of use cases you're targeting, and whether CrossHair could be extended for those. I'd be more than willing to implement DEAL support for CrossHair if that meant that we could combine forces, for instance. There are also lighter ways that we could help each other, for instance, just by chatting more, sharing experiences, etc.

[orsinium]

When I started it, I had a dream to make a support for holes like in idris. For example:

@deal.ensure(lambda _: _.result > _.x)
def f(x):
  return ...

Here, ... is a hole. It is a place for code that we haven't written yet. And the smart machine can fill the hole, at least good enough for TDD. How to represent a hole in terms of z3? Well, it's just a function that accepts as arguments all variables in the current scope. How to solve it? Quantifiers! We know that the post-condition must be true for all input values. And so we get:

import z3
x = z3.Int('x')
f = z3.Function('f', z3.IntSort(), z3.IntSort())
z3.solve(z3.ForAll([x], f(x) > x))

And it just freezes. Why? Because z3 is bad at quantifiers. Really bad. Even worse than at powers. That's really sad. Now, I have a choice either to give up this idea for a while or implement it in hope that someday z3 will get much better.

That's interesting how it can't even do some simple optimizations for this structure:

# this one is solved because you just say the exact implementation for f
z3.solve(z3.ForAll([x], f(x) == x * 2))

# but this one is freezed to death ¯\_(ツ)_/¯
z3.solve(z3.ForAll([x], f(x)/2 == x)) 

UPD: the answer to the first hole is x+1, for example. I always thought that machines are better at math than me. Turned out, it's not always the case...

[pschanely]

Ah, I think this is called "program synthesis." I am not an expert, but I think the solutions here usually boil down to some kind of search, hopefully guided by the types. It's a bit of a holy grail.

I think dependent type systems generally restrict the language of the dependent types in ways that ensure verification of a potential solution is at least decidable. So they've got that leg up on us. :)

[orsinium]

That's the point, actually. I consider contracts as another way to "refine" types. Refined types, liquid types, dependant types, contracts, it's all the same: a way to narrow down the set of values the type includes. The only difference in syntax. And DbC beat everything else here, having the same syntax as the language itself. The only difference is that it is harder to statically analyze because of the bigger syntax. So, yeah, our way is harder but possibilities are the same.

I think the solutions here usually boil down to some kind of search, hopefully guided by the types.

I'm more not an expert 😉 and this description is how I understand the work of SAT solvers, so I see no reason why z3 shouldn't be able to handle it.

I have this video in my TODO list: A peek inside SAT solvers. The title sounds promising.

I dropped an issue in z3, BTW: Z3Prover/z3#5019

[pschanely]

That's the point, actually

Yes. We want the same future. :)

I see no reason why z3 shouldn't be able to handle it.

I like your optimism! From Nikolaj's response, it sounds like Z3 could play a part in doing synthesis, but a lot of the search would have to happen outside.

One interesting avenue (for synthesis and potentially verification) that I haven't tried yet is an opcode-level model. In this case, you'd be asking Z3 to generate the python stack machine instructions to accomplish a task. (turning the "code" into regular data that Z3 can solve for) But I suspect that this ultimately just turns into a tree of ite()s that explodes after a few instructions, and only solves trivial problems. But it would be an interesting experiment regardless.

[orsinium]

What I understood from the answer on my issue above, is that I must provide a formula instead of a function. However, it still works really bad:

import z3
a,b,c,d,x,y = z3.Ints('a b c d x y')

z3.solve(z3.ForAll([x], x*a/b-c < x/2))
# failed to solve

z3.solve(z3.ForAll([x], x/b-c < x/2))
# [c = 2, b = 2]

Looks like quantifiers is a dead end. That's discouraging.

[pschanely]

Yeah, things go south quickly when you start using quantifiers.
One minor point is that integer division is quite a bit harder to reason about than normal division. Your example over the reals, for instance works out ok:

>>> a,b,c,d,x,y = z3.Reals('a b c d x y')
>>> z3.solve(z3.ForAll([x], x*a/b-c < x/2))
[b = -1,
 a = -1/2,
 c = 1,
 /0 = [(1, -1) -> -1, (2, -1) -> -2, else -> 0]]

Anyway. I just saw this talk, and I think it's highly relevant to the sort of thing you want to do (I think): https://www.youtube.com/watch?v=uBthag5kOLw

I'd add a note that I think the fact that rosette wants an interpreter is sort of critical to how synthesis works - because the code supplied to the interpreter becomes data, which can then be solved for. Well, potentially: I suspect there's a lot of custom heuristics/search going on inside rosette.

[Zac-HD]

One minor point is that integer division is quite a bit harder to reason about than normal division [over the reals]

Ignoring, of course, that Python floats are discrete like integers rather than continuous like reals 😜

(we all do this, but "float != real" is sometimes important... for numerical stability, for example)

[pschanely]

Oh golly, don't get me started on this.

For most pythons, the correct sort to use for floats is z3.Float64(). Good luck trying to convert those to and from z3.IntSort() though!

I still haven't implemented the feature where CrossHair will attempt both approaches for floats, but it's high on the list.

[Zac-HD]

Klara (repo, docs) is a recently released - and very very alpha - symbolic analysis tool which works only based on the Python AST. It's still very limited, but I can imagine a "sometimes this helps" fully-static analysis being useful.

[pschanely]

I don't know how you discover all this Zac, but I hope you keep doing it. :)
Just started a conversation. And yes, there are opportunities for this to be useful, probably in ways I haven't even thought of. One idea, given that the nemesis of concolic execution is path explosion:

Let's say we have a complex function (that's hard to AST-analyze) that repeatedly calls a simple function (maybe with just a few "if" statements). Transforming that simple function into a Z3 conditional expression would let the concolic engine handle the complex function, and avoid forking the execution path on each invocation of the simple function.

There are still a lot of challenges here. For one, we're just shifting the case explosion analysis into Z3; often that's a good call, but sometimes it isn't. Perhaps a general theme of CrossHair's evolution has been to aim for less solver difficulty at the cost of more executions.

[orsinium]

Another interesting but abandoned project:
https://github.com/JuanmaCopia/PySEAT

[kubajal]

Hi, I'm interested in implementing this feature but I am not sure what is its current state. Can anyone give me an overview (even a non-detailed / high-level one) of what needs to be done to enable this feature or what are the fundamental limitations?

I'm especially interested in:

• where should the new static AST analysis logic go? (ie. which source code file or step in the general CrossHair execution logic)
• which datatypes or operators are feasible for exhaustive search? or what are some good approaches for non-exhaustive search?
• what about static analysis of side-effects? to make initial things simpler, could we assume that the user writes their code as pure functions?

[pschanely]

Exciting! For the moment, I'll assume that we're happy to only swap functions wholesale: importantly, this means we have easy access to the parameter and return types. There are maybe 3 pieces for a working solution here: one is easy, one is interesting, and one is neither:

1. [easy] We need a way for CrossHair to run symbolic friendly code instead of the branchy code. Fortunately, this exists already - you can use the register_patch function documented here.
2. [interesting] We need a way to understand the existing code and decide whether it can be implemented in a branchless way by (a) applying regular python transformations (e.g. z and y => all([x, y])), or (b) by inspecting symbolics, extracting Z3 values, operating on those, and constructing new symbolics to return.
3. [neither easy nor interesting] We need a way to figure out what code to inspect for opportunities. Open to suggestions here. One might imagine that we'd ideally start searching and inspect call stacks where decisions are made. However, you cannot alter the path tree while a search is happening, so adding a register_patch between path explorations is not ok. My initial ideas:
   • Perhaps we could add some kind of special "intercept everything" handler that can indicate whether or not it wants to continue to be notified at the current point (like how sys.monitoring works). This uber-handler will perform the AST analysis at the initial invocation of every function. It could either create, cache, and use the replacement code, or decline future interceptions for this function.
   • Alternatively, we start with something simple for a proof of concept, like analyze the modules of all given entry points.

Ah, and I started writing all this without even carefully reading your questions. More directly!:

where should the new static AST analysis logic go? (ie. which source code file or step in the general CrossHair execution logic)

I think this is roughly my 3rd bullet above - let's discuss!

which datatypes or operators are feasible for exhaustive search? or what are some good approaches for non-exhaustive search?

Making some guesses here - you'll need to figure some of this out yourself! To start, I'd be looking for the symbolic counterparts of deeply immutable types like str, int, bool, frozenset. Tuples may or may not be immutable - it depends on the types of their contents. Furthermore, looking at the signature types likely isn't enough: it's valid to pass a subtype of int to an int parameter, which might behave differently. You'll want to inspect the real types (in a NoTracing block) at runtime and check that the int you got is exaclty a SymbolicInt. As for operations, this is where your AST analysis needs to enter the picture, along with your knowledge of the exact (concrete or symbolic) argument types. Perhaps it's implemented like an AST-level partial evaluator (and could double as an optimizer later?!).
Note: Unfortunately, you won't be able to make optional-parameter-functions branchless, because you can't inspect an optional type without forcing the None decision; returning an optional without branching is only partially supported. (same things apply for any union type) I have a long-running set of tasks that may eventually enable these use cases, however.

what about static analysis of side-effects? to make initial things simpler, could we assume that the user writes their code as pure functions?

I would instead limit myself to functions where we can know the replacement code will not change behavior. That means we could ship something that actually helps people sooner. Unfortunately, we'll rarely be able to apply the AST-optimized function; simply accessing a field person.age can invoke arbitrary, and possibly mutating, code. Execution order semantics also matter more than you might naively think. You'll likely have to limit yourself to "leaf" functions that don't call anything else.
In theory, CrossHair could support some sort of execution mode where we assume and expect that mutations never happen. But in practice, nobody writes Python code this way, and CrossHair tries to target practical use cases.

I think maybe the next step is for you to dig into some of what I've said, ask questions, and we can begin to clarify the shape and scope of the thing, at least for v0. If you're serious about this, I'll handle some of the supporting pieces; consider grabbing me on discord or a chat tool of your preference for higher bandwidth discussion too.

[pschanely]

Oh, and just to play a little devil's advocate - I'm not fully convinced that AST analysis will be the best way to go about performing the code translation. (and not convinced it isn't) But here is a counter-proposal:

1. We determine whether the function is going to be side-effect-free, by looking at the runtime argument types and the AST. (just like the original proposal, but less work because you only need to produce a known-pure / unsure-pure decision).
2. If known-pure, we run a miniature CrossHair path exploration loop over the candidate function and collect paths. If we exhaust the paths before some timeout, and every path returns a symbolic of the same type, then we can return a fresh symbolic, X, and add this constraint to the solver:

<path 1 conditions> and X = <path 1 return var> OR
<path 2 conditions> and X = <path 2 return var> OR
...

And then we're done! Sort of. There are still many details to work out.