search

TikhonJelvis / imp

Some scripts for analyzing IMP programs with the Z3 automatic theorem prover, originally written for my Compose 2016 talk.
http://jelv.is/talks/compose-2016
BSD 3-Clause "New" or "Revised" License
17 stars 1 forks source link

Feature request: IMP Array support #2

Open void4 opened 3 months ago

void4 commented 3 months ago

It would be pretty cool if IMP supported arrays or some other form of indexable memory, since this would enable applications like (attempting to) finding Universal Turing Machine programs that compute a specific output :)

TikhonJelvis commented 3 months ago

Hey, yeah, that would make it a lot more like a real language. I expect that any SMT solver would choke on difficult problems with even a moderate amount of memory involved, but it's always hard to predict ahead of time. There's a good chance it would perform well enough for some problems.

I know of two options for modeling memory: either with Z3's theory of arrays or as a bunch of bitvector variables. On the program synthesis project I worked on at Berkeley we roughly took the latter approach and it worked well enough for small, self-contained programs (and very small amounts of memory).

I probably won't have the time to try something like that myself, but happy to help if you want to give it a go.

TikhonJelvis commented 3 months ago

Oh, forgot to mention: Souper is a non-toy implementation of the same idea for LLVM IR. If you haven't seen it, it's a good example of how this technique could be useful in the real world.

Skimming over their paper it looks like they don't model memory in Souper at all. Which makes sense because dealing with arrays and arbitrary loads/stores massively expands the search space in a way that SMT solvers are not particularly adept at handling.

void4 commented 3 months ago

it worked well enough for small, self-contained programs (and very small amounts of memory).

I've put a (24,2)-Universal Turing Machine into the Java frontend of AProVE (I had to rewrite it into an absolute monstrosity of if-statements for it to even work), and it could prove the (non-)terminating behavior for all configurations of very short tapes (I forgot how many exactly but around 8 cells maybe). Trying to use any longer tapes resulted in it either running out of memory or just not stopping its analysis in a reasonable amount of time. Unfortunately not even the shortest program description for that particular UTM would fit onto that short of a tape. It would be a cool metric for research progress, or cool art, to visualize which configurations of various tape lengths we are able to prove, and which not (yet).