Symbolic Execution by Overloading bool

https://www.philipzucker.com/overload_bool/

by philzook • 2 years ago

81 10 2 years ago

pizza• 2 years ago

This is the kind of thing I love to come across on a holiday break that seems ripe for side projects... :)

Impressive work. I once implemented sybolic execution in Lua to automate calculating error propagation for physics class, but when I tried to extend the system, I couldn't figured out how to deal with control structures and resorted to writing functions like ifElse(x, y, z). Feels good to find out it is possible after all.

int_19h• 2 years ago

Isn't this kind of thing exactly why Lisp was so popular for symbolic computation historically?

throw-qqqqq• 2 years ago

Lisp-like languages with their S-expression syntax (or lave of same) makes this very easy to do at least.

Abstract interpretation is super easy to implement over Lisp-like languages IMO.

tracnar2• 2 years ago

This is exactly what the CrossHair library does: https://github.com/pschanely/CrossHair

It also overloads other methods to provide kind of symbolic objects.

philzook2• 2 years ago

This looks great! The paper linked in your README https://hoheinzollern.files.wordpress.com/2008/04/seer1.pdf also seems like a nice explanation of similar ideas.

The reason I'm exploring this idea is to use more natural looking python as dsl for function definitions in my proof assistant https://github.com/philzook58/knuckledragger

Also to see if I can make a nice-looking staged metaprogramming framework in python like buildit, but maybe to generate C/C++ rather than more python.

Could Crosshair be used in these ways?

tracnar2• 2 years ago

To be clear I did not make CrossHair.

I was also looking into it to turn normal python functions into some kind of constraints. But as you point out in your article it cannot really work through python imperative statements like conditions and loops, so you either need to find a way to cover all code paths, or only use a subset of Python (like Z3 does to some degree I believe). I still need to try it out further.

For your proof assistant it seems you could indeed use it if you limit yourself to Python expressions. Interesting stuff!

svilen_dobrev2• 2 years ago

Here some expression builder, with few renderers thereof, in one file, with some tests (beware: from 2012-2016)

Was used to turn a python function into plain text (textualize itself), into SQL-text (applicable as query), evaluate-numerically, translate into other languages, and the like.

https://github.com/svilendobrev/svd_util/blob/master/expr.py

philzook2• 2 years ago

This looks like a nice reflection of python into a syntax tree, but unless I'm mistaken, it can't reflect python control structures like if-then-else? Z3 or sympy already are kind of ready to go systems that overload all the typical operators. Is there something you've done here they are missing?

svilen_dobrev2• 2 years ago

This is only expressions - what you can put inside a lambda. if-then-else are statements. The ternary op (Y if X else Z) probably was not yet there in 2012 - or i did not needed it. But You can add all other dunder operators if u need them..

Symbolic Execution by Overloading __bool__

Related Stories

Symbolic Execution by Overloading bool