[HN Gopher] Symbolic Execution by Overloading __bool__
       ___________________________________________________________________
        
       Symbolic Execution by Overloading __bool__
        
       Author : philzook
       Score  : 67 points
       Date   : 2024-12-24 03:48 UTC (19 hours ago)
        
 (HTM) web link (www.philipzucker.com)
 (TXT) w3m dump (www.philipzucker.com)
        
       | pizza wrote:
       | This is the kind of thing I love to come across on a holiday
       | break that seems ripe for side projects... :)
        
       | PhilipRoman wrote:
       | 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 wrote:
       | Isn't this kind of thing exactly why Lisp was so popular for
       | symbolic computation historically?
        
       | tracnar wrote:
       | This is exactly what the CrossHair library does:
       | https://github.com/pschanely/CrossHair
       | 
       | It also overloads other methods to provide kind of symbolic
       | objects.
        
         | philzook wrote:
         | 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?
        
           | tracnar wrote:
           | 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_dobrev wrote:
       | 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
        
         | philzook wrote:
         | 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_dobrev wrote:
           | 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..
        
       ___________________________________________________________________
       (page generated 2024-12-24 23:01 UTC)