Checkers are not merely passive receivers of the analyzer core changes - they actively participate in the ProgramState construction through the GenericDataMap which can be used to store the checker-defined part @@ -123,9 +131,12 @@ opportunity to either report a bug or modify the state. (As a rule of thumb, the checker itself should be stateless.) The checkers are called one after another in the predefined order; thus, calling all the checkers adds a chain to the - ExplodedGraph. + ExplodedGraph. +
During symbolic execution, SVal objects are used to represent the semantic evaluation of expressions. They can represent things like concrete @@ -142,7 +153,9 @@ This represents a case that is outside the realm of the analyzer's reasoning capabilities. SVals are value objects and their values can be viewed using the .dump() method. Often they wrap persistent objects such as - symbols or regions. + symbols or regions. +
+SymExpr (symbol) is meant to represent abstract, but named, symbolic value. Symbols represent @@ -150,7 +163,7 @@ we can associate constraints with that value as we analyze a path. For example, we might record that the value of a symbol is greater than 0, etc. -
+
MemRegion is similar to a symbol. @@ -163,9 +176,12 @@ SymbolicRegion is for. It is a MemRegion that has an associated symbol. Since the symbol is unique and has a unique name; that symbol names the region. +
-+
Let's see how the analyzer processes the expressions in the following example: +
+
int foo(int x) {
@@ -174,6 +190,8 @@
...
}
+
+
Let's look at how x*2 gets evaluated. When x is evaluated, we first construct an SVal that represents the lvalue of x, in @@ -193,6 +211,7 @@ The second line is similar. When we evaluate x again, we do the same dance, and create an SVal that references the symbol $0. Note, two SVals might reference the same underlying values. +
To summarize, MemRegions are unique names for blocks of memory. Symbols are @@ -200,6 +219,7 @@ symbolic chunks of memory, and thus are also based on symbols. SVals are just references to values, and can reference either MemRegions, Symbols, or concrete values (e.g., the number 1). +