2

What is the difference between implementation of static analysis and symbolic execution?

Cactus
  • 27,075
  • 9
  • 69
  • 149
any
  • 325
  • 5
  • 17

2 Answers2

7

I really like this slide by Julian Cohen's Contemporary Automatic Program Analysis talk. In a nutshell, people like to divide program analysis into two broad categories of static and dynamic analysis. But there is really a broad spectrum of program analysis techniques that range from static to dynamic and manual to fully automatic. Symbolic execution is an interesting technique that falls somewhere in between static and dynamic analysis and is generally applied as a fully automatic approach.

Dimensions of Program Analysis

Ben Holland
  • 2,309
  • 4
  • 34
  • 50
  • 1
    thanks. Do you know what kind of errors static analysis (e.g. compiler) can detect and symbolic execution can not detect? – any Nov 11 '16 at 21:43
  • It's hard to say (especially in a comment). Static analysis deals with issues of path feasibility, whereas dynamic analysis tends to deal with path coverage. Symbolic analysis is sort of in between and deals with state space explosion by logically forking the analysis at branches and solving for a set of satisfiable constraints. Most implementations I've seen spend lots of processing time in SAT/SMT solvers. This is also hard to answer because many implementations are a blend of techniques. Static analysis can be fully automatic for instance. – Ben Holland Nov 12 '16 at 00:11
  • I create new question about that in this link: http://stackoverflow.com/questions/38540082/error-detection-in-static-analysis-and-symbolic-execution – any Nov 13 '16 at 06:29
4

Static analysis is any off-line computation that inspects code and produces opinions about the code quality. You can apply this to source code, to virtual machine code for Java/C#/... virtual machine instruction sets, and even to binary object code. There is no "one" static analysis (although classic compiler control and dataflow often figure prominently as foundation machinery for SA); the term collectively applies to all types of mechanisms that might be used offline.

Symbolic execution is a specific kind of off-line computation that computes some approximation of what the program actually does by constructing formulas representing the program state at various points. It is called "symbolic" because the approximation is usually some kind of formula involving program variables and constraints on their values.

Static analysis may use symbolic execution and inspect the resulting formula. Or it may use some other technique (regular expressions, classic compiler flow analyses, ...) or some combination. But static analysis does not have to use symbolic execution.

Symbolic execution may be used just to show an expected symbolic result of a computation. That isn't static analysis by the above definition because there isn't any opinion formed about how good that result is. Or, the formula may be subjected to analysis, at which point it becomes part of a static analysis. As a practical matter, one may use other program analysis techniques to support symbolic execution ("this formula for variable is propagated to which reads of variable x?" is a question usually answered well by flow analysis).

You may insist that static analysis is any offline computation over your source code, at which point symbolic execution is just a special case. I don't find this definition helpful, because it doesn't discriminate between use cases well enough.

Ira Baxter
  • 93,541
  • 22
  • 172
  • 341
  • thanks. In general way which implementation is less time-consuming? – any Sep 22 '16 at 14:28
  • "which is less time consuming?" This isn't about effort to implement. You choose a technology/architecture to achieve a purpose, from among the set of choices you have. But without a specific statement of purpose, you have no way to rank which of these is more sensible. If you have no specific purpose and want to do the least amount of work, you simply do nothing. – Ira Baxter Sep 22 '16 at 14:34
  • Now, you may have a specific task in mind. What you will discover is that no matter which of these technologies you'd like to use, they all take significant time to build from scratch. If you want to accomplish your purpose, what you should do is acquire the technologies you need in a way that integrates neatly, so you can focus on tuning them to solve your specific problem. My experience is that you mostly can't find these together, and so I set out to solve that problem. See http://www.semdesigns.com/Products/DMS/LifeAfterParsing.html – Ira Baxter Sep 22 '16 at 14:37
  • I said that because my time is limited. When I read articles about static analysis for example http://modeling-languages.com/anatlyzer-static-analysis-atl-transformations-uncover-errors/ link and compare it with what you said in http://stackoverflow.com/questions/39490607/implement-symbolic-execution-without-model-checking/39493738?noredirect=1#comment66515194_39493738 I found several similarities for example both of them use Abstract syntax tree. This isn't clear for me what is exactly difference between them from the aspect of implementation and technologies used (not goal). – any Sep 22 '16 at 17:12
  • Your best bet is to use the understanding and experience that other people in the community have painfully acquired. Abstract syntax trees are sort of a good idea, but doing it the way most folks do adds complexity beleive it or not, you want abstract syntax trees derived from concrete ones if you don't want the "abstract" part to create *more* work. See http://stackoverflow.com/a/1916687/120163. But the trees are the *easy* part by far; Life After Parsing tells you what you need in practice, if you want to honor the fact that your time is limited. Otherwise you reinvent it all, badly. – Ira Baxter Sep 22 '16 at 19:20
  • You've avoided stating your actual goal. That goal will help decide which supporting technologies you might like to use. Then you'll need implementations of those technologies; yes, you can build everything yourself but if you attempt to do that, you'll never get around to actually working on your stated goal. Better to get those technologies already packaged and running. So, what exactly are you trying to do? – Ira Baxter Sep 23 '16 at 09:11
  • I want to implement symbolic execution of programs that are written in particular language which have imperative and declarative parts (and specially ocl expression parts). I want to know in which I should start. Also I read the link above about static analysis of particular language and I found similarities between this way of static analysis and what you said before for symbolic execution. I want to know what is the defference between this way of static analysis and symbolic execution. And for symbolic execution that I want to do what steps must taken in order? – any Sep 23 '16 at 11:16
  • Symbolic execution and static analyses by themselves aren't interesting goals. Your question is like "I want to use a carpenter's toolbox" and "I see value in tools for plumbing, ... which toolbox should I implement first?" You haven't stated your real goal yet, IMHO. I've revised my answer to help clarify the distinction between SA and SE, but they are still both complex topics and you don't want to implement these yourself if you expect to achieve your real goal in any reasonable time duration (did you read Life After Parsing carefully?). If this is unclear, you aren't ready to do this. – Ira Baxter Sep 23 '16 at 12:54
  • I want to verifying pre/post conditions or test case generation of programs written in particular language. – any Sep 23 '16 at 13:25
  • If you truly want to *verify* pre/post conditions, you may want to consider theorem proving (that's where the term comes from). TP shares a lot with symbolic execution in the sense that you are constructing formulas about the program state, but it is also about proving theorems which is actually pretty hard. But symbolic execution will give you a formula for the program state along a particular path (maybe along all paths if you do it for all paths) and now you have something to match against the postcondition. You didn't answer the question about whether you had read LifeAfterParsing. – Ira Baxter Sep 23 '16 at 13:43
  • You can generate test cases from the code by enumerating control flow paths through it to some postcondition, and for each specific flow path, and each conditional along that path, generate a test program that will force that conditional to be true. So now your test program exercises a path, and the tested program arrives at the postcondition which is presumably compilable and thus determines if the postcondition for the procedure along that path is "correct". To test an entire function, you need to generate tests for each path; that can be a lot of paths. ... – Ira Baxter Sep 24 '16 at 21:33
  • When you start getting to tasks like this, you want as much static analysis and symbolic execution machinery as you can get, because you will use each of them a number of times in trying to accomplish this purpose. If you attempt to choose just one, you'll discover you want the other, too. – Ira Baxter Sep 24 '16 at 21:34