KLEE, the involuntary base64 decoder

It is not by chance that I use the term involuntary instead of incidental, because this lil' piece of software has quite a personality. I'd ask it out for a coffee, but am scared it will say 'Yes'.

Let's let it rock: find a base64encode function, and write a short preamble, calling it twice, first on "Hello, world!", and the second time on the symbolic buffer "new_src" (this tells KLEE "new_src" could contain anything): http://pastebin.com/1SgupULp

Surely, the output could not be same, right? Right?! http://pastebin.com/Z3REbH0H

I would call this pattern of KLEE-based computing "contrarian computing". You: "Isn't it that you can't do X?" KLEE: "Oh, yes, you can!" Or a German-speaking KLEE might say "Doch." :-)

Thus, KLEE has really computed base64decode(dest), without knowing it. This is not a problem for it, because it doesn't know that it doesn't know it. I am scared of what will happen if I try the same for zip, DES, AES, MD5, SHA1. Or an English to Russian translator. Or the halting problem. Or dog-food it: compile KLEE itself and assert it cannot prove everything about any program.

So, who knows to decode base64 in this case? We just provided the source of the encoder, not the decoder. I don't know how to write the decoder off the top of my mind for sure. I doubt that many programmers know. So who knows? KLEE? It has no klue about base64 encoding or decoding, any more than about Einstein's Enigma, or solving mazes. Is it clang + klee? clang + klee + base64encode.c? 

"Any sufficiently advanced technology is indistinguishable from magic."

Just like us - robots, pondering over the "Hard Problem of [our] Consciousness", with all its glorious caps. When it's just layers upon layers. Really, layers all the way down, Alice. The ghost in the shell is "only" software.