Vo 5

The symbolic state consists of:

1. A preficx of a path in the CFG

2. A symbolic map, which maps each variable of the program to an expression over the symbolic variables

3. A path condition (a constraint over the symbolic variables), which holds if and only if the execution takes the current path

A search strategy defines how the next path is chosen

1. The first path is chosen randomly

2. The next path is determined by negating a conjunct of the path condition

3. The foreach statement determines which conjunct to negate

Long first:

The foreach statement considers longer prefixes first

Short first:

The foreach statement considers shorter prefixes first

Branching and assume statements append both append and element to the sequence

-> treated identically except assumptions are never negated to explore new paths

• Might not terminate

  -> we cannot enumerate all paths for loops in general

• Every additional recursion just tests one more loop iteration

  -> by adding the negation of the loop condition

• Some branches might not be covered

  -> because SE gets stuck exploring a loop

Bound the number of loop iterations or use a time-out

Issues:

• Scalability

• Modularity

• Non-linear constraint over reals is difficult to solve

• Without solution no test data will be provided

  ( - neither for the other branches)

Concolic testing or whitebox testing

Exactly like symbolic execution, but we may use concrete values when constraint solving fails

DSE:

1. Randomly picks values for x,y

2. Observes the concrete value c of Hash(y)

3. Changes the calue of x to c in the next run

The results of method calls may be used as conditions

-> In DSE expressions that cannot be encoded are replaced by their concrete values

Expressions that cannot be encoded as constraints are replaced by their concrete values by…

• by adapting the defintion of procedure ExecuteSymbolic

• by fixing method arguments with assumptions

When method results are constrained by values other than symbolic values, the resulting contraints do not provide useful conditions

When the solver returns “unknown”, simplify constraint by replacing a symbolic value and retry solving

Pros:

Replacing a variable with a concrete value:

• Might reduce the complexity

  (e.g. replacing A in AxB > 0)

• Reduces the size

  (number of free variables)

Cons:

Strategy does not necessarily succeed

• New Constraint might be unsatisfiable

• Solver might still yield “unknown

When:

• There are finitely many paths

• And all feasable branches are explored