Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:forward_symbolic_execution [2009/03/10 23:00] vkuncak |
sav08:forward_symbolic_execution [2009/03/11 10:47] vkuncak |
||
|---|---|---|---|
| Line 126: | Line 126: | ||
| assume (x=1) | assume (x=1) | ||
| Then symbolic execution knows the exact values and can work as an interpreter. | Then symbolic execution knows the exact values and can work as an interpreter. | ||
| + | |||
| ===== Underapproximations ===== | ===== Underapproximations ===== | ||
| Line 132: | Line 133: | ||
| If there are no loop invariants, we can still execute program on concrete inputs. For symbolic initial state (e.g. giving upper bound of loop) execution need not terminate. | If there are no loop invariants, we can still execute program on concrete inputs. For symbolic initial state (e.g. giving upper bound of loop) execution need not terminate. | ||
| - | * Bounding depth: stop executing for path | + | * Bounding depth: stop executing for paths longer than some value |
| * Bounding state: small integer width, small number of objects in heap | * Bounding state: small integer width, small number of objects in heap | ||
| - | * Loop unrolling: replace loop( c ) with c;c;c for some number of times | + | * Loop unrolling: replace loop( c ) with c[]c;c[]c;c;c for some number of times |
| * Instantiating values: find a satisfying assignment for R, take value v of x in it and replace e_x with v (moves towards concrete execution) | * Instantiating values: find a satisfying assignment for R, take value v of x in it and replace e_x with v (moves towards concrete execution) | ||
| + | |||
| ===== Overaproximation ===== | ===== Overaproximation ===== | ||
| Line 145: | Line 147: | ||
| * maintain only linear or certain polynomial constraints - if actual constraints are more complex, keep only the polynomial constraints that are guaranteed to hold | * maintain only linear or certain polynomial constraints - if actual constraints are more complex, keep only the polynomial constraints that are guaranteed to hold | ||
| - | Why we approximate: we can obtain | + | Why we approximate we can obtain |
| - | * termination | + | * termination even for programs that have loops |
| - | * useful information (not exactly all information that we are interested in, depends on the approximation) | + | * useful information about the program (not exactly all information that we are interested in, depends on the approximation) |
| ===== References ===== | ===== References ===== | ||