313
edits
Abstract Interpretation: Difference between revisions
Jump to navigation
Jump to search
no edit summary
No edit summary |
No edit summary |
||
| Line 35: | Line 35: | ||
Abstract interpretation operates on a flowchart representation of the function called a '''control flow graph''' or '''CFG'''. Here is the CFG for the example function: | Abstract interpretation operates on a flowchart representation of the function called a '''control flow graph''' or '''CFG'''. Here is the CFG for the example function: | ||
[[Image:treehydra-cfg.png]] | [[Image:treehydra-cfg.png]] | ||
It looks like a pretty normal flowchart. Some features to note: | |||
* All possible control transitions are shown as explicit edges. | |||
* Statements always have exactly one operation and at most one assignment. Temporary variables are added if necessary. This will really simplify our job: instead of handling every kind of C++ statement, we have only have to analyze these simple statements. | |||
A little terminology: | |||
* Each node is called a '''basic block'''. The defining feature of a basic block is that there is a single entry point and a single exit--basic blocks are straight-line code. | |||
* In different sources, statements may be called ''statements'', ''instructions'', ''triples'' (of a destination and up to 2 operands), ''quadruples'' or ''quads'' (counting the operator), or even ''tuples''. We'll call them ''instructions'', as that's the name used in Treehydra code. | |||
* A '''program point''' is the (notional) point just before or after each instruction. The function has a well-defined state at program points, so our analysis facts will always refer to program points. E.g., at the program point just before 't1 := k + m', k is constant with value 2. | |||
=Concrete Interpretation= | =Concrete Interpretation= | ||