Symbolic Execution Over Native X86 [pdf] | Hacker News Reader

Symbolic Execution Over Native X86 [pdf]

dtic.mil

32 pointsluu7 comments

If I understand correctly, modeling a program at the x86 instruction set level is cool but it would have a more complicated list of states than a high level language. More states means more computation to do the symbolic execution, therefore it is harder to optimize well enough to get useful results on large programs.

The intro implies that the main motivation for doing this on x86 instructions is uncertainty that a high-level language's abstraction is faithfully translated into x86 instructions. I recognize that this language->assembly conversion was accepted to be correct as a basic assumption when I did graduate work in validation techniques. I think there are some PL theorists that have more rigorous mathematical proofs for their compilers, but I'm not sure how many of those get all the way down to the x86 instruction set.

ISA has never meant Industry Standard Architecture.

Why did they get that wrong? It's just such a weird error to make, especially at the postgraduate level.

An unfortunate typo in the abstract, in the glossary it's defined as "Instruction Set Architecture"

ISA has been used to mean Industry Standard Architecture much more often than it has been used to mean Instruction Set Architecture -- just not in this context, and probably not in the last 20 years.

Industry Standard Architecture was the standard bus interface in PCs, before PCI et cetera.

So the term has certainly been used a great deal with that meaning, although it's of course a typo in this context where it should mean Instruction Set Architecture.

See https://en.wikipedia.org/wiki/Industry_Standard_Architecture.

Right. I forgot the Not Micro Channel Bus. ;)

Next I'll be forgetting what PCMCIA stands for, I guess.

> what PCMCIA stands for

I will remember this to the day I die: People Can't Memorize Computer Industry Acronyms. ;)

Reply on news.ycombinator.com