Link Search Menu Expand Document
Software testing (TDDD04)

Lab 5: Symbolic execution and test-case generation

Purpose

Symbolic execution is a white box testing technique that detects which parts of the code are triggered by what combination of inputs. It is useful for the generation of test cases that give a high coverage of the software. In this lab we will use a tool to apply symbolic execution techniques to analyse and improve code and detect bugs.

We will use KLEE, a popular open source symbolic execution engine (see KLEE’s homepage and the OSDI’08 paper for more information).

On thinlinc, we have installed the lab material under /courses/TDDD04/symbolic. You can access executables such klee, ktest-tool, klee-replay, extract-bc or wllvm by adding /courses/TDDD04/symbolic/bin to your path variable. You can also access libraries needed by klee by adding /courses/TDDD04/symbolic/lib to the library path variable:

export PATH=$PATH:/courses/TDDD04/symbolic/bin
export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/courses/TDDD04/symbolic/lib

Some parts might also require a path to the build directory of KLEE. This is for instance used in the first tutorial testing a small function to run test cases generated by KLEE. The path to the build directory of KLEE is /courses/TDDD04/symbolic/klee/build.

You are encouraged to checkout the following steps in the KLEE tutorials:

  • tutorial 1: all steps. Important for basic runs and test executions. Observe that KLEE operates on llvm bytecode (i.e., .bc file). You need to include the header files for KLEE when generating the bytecode files. The path to the KLEE header files on thinlinc is /courses/TDDD04/symbolic/include, so generating the bytecode in the first tutorial should be with: 
    clang -I /courses/TDDD04/symbolic/include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone get_sign.c
  • turorials 2 and 3: all steps. Important for types or errors, klee_assumeand flags such as --only-output-states-covering-new, and for using symbolic arguments or input files.
  • tutorial 4 for the optional part. All steps except steps 6 and 8. Important for working with standard library for analyzing coreutils.
    • in step 1: You do not have to make -C src arch hostname
    • in step 2: wllvm is already installed under /courses/TDDD04/symbolic/bin. No need to install it again.
    • in step 3: You can directly, from within the obj-llvm/src do a extract-bc ./cat to extract the .bc file of the executable catinstead of the find . -executable -type f | xargs -I '{}' extract-bc '{}' which will extract it for all executables there.

Make sure you check how to:

  • generate tests with klee, to read them with ktest-tool and to replay them with ktest-replay
  • to use options such as --only-output-states-covering-new and -max-forks=N to control the symbolic execution
  • to check if errors such as ptr and assert have been generated
  • to use klee_make_symbolicand klee_assume to make some variables symbolic or to add constraints to the symbolic execution
  • how to use symbolic environments such as -symb-arg and sym-files to have symbolic inputs

For this lab, part 1 is mandatory for the passing grade, part 2 is for those aiming for a 4 or 5.

Part 1 : Mandatory

In this part you will implement the main method from the car insurance application Lab 2 in C and test it with KLEE.

Run KLEE on your implementation. Do you detect any bugs? Document any bugs found in your report and fix the implementation.

Add 2 assertions to check that the implementation is correct, for example that the deductible is always within the correct range.

In the lectures we talk about defensive programming (ensuring you can deal with unexpected inputs) versus assuming some guarantees on the data that you receive as well as testing behaviour accordinging to the specification. For example we can test if the age is over 18, as that is the legal driving age in most countries, and a driver aged 12 should not be possible, but it is not part of the specification. Add an assertion that tests for behaviour not covered by the specification. Document the results in your report.

Here is a skeleton using the insurance method, with the signature modified to avoid using objects:

#include <stdio.h>
/*
 * Calculate the deductible for the client
 * Base cost is 5000 SEK if the client is above 30 or has had a driving licence for more that 5 years and 8000 SEK otherwise
 * With every accident for that calendar the deductible increases:
 * 1 accident 	: by 1000 SEK
 * 2 accidents  : by 2500 SEK
 * 3 accidents	: by 4000 SEK
 * 4 accidents and more by : 10000 SEK
 * If the client if a gold member, then for the first 2 accidents, there is no increase
 * but for 3 accidents and more normal rates apply
 */
int getClientDeductible (int clientAge, int yearOfLicence, int numberOfAccidents, int isGoldMember) {
  return -1;
}
int main() {
  int clientAge = 0;
  int yearOfLicence = 0;
  int numberOfAccidents = 0;
  int isGoldMember = 0;

  int result = 0;
  result = getClientDeductible (clientAge, yearOfLicence, numberOfAccidents, isGoldMember);
  printf("Result was %d\n", result);
  return 0;
}

Part 2 : Optional

Carefully read the tutorial on testing coreutils and download your own copy of coreutils (for instance coreutils-9.1 from the coreutil page). Read the remaining part of this lab before you go through the tutorial.

The first step introduces gcov. After the configure and make in step 1, do not cd into “src”. Instead, run the compiled programs from within gcov-obj (e.g., with ./src/echo). You can delete the stale gcov files with rm -f src/*.gcda. Once you gcov src/echo you get an echo.c.gcov file that you can open with a text editor to get statistics on which lines have been covered. This is useful to realize what lines of the code have not yet been executed. Observe that the coverage results of running several tests is accumulated (reflected when running gcov src/echo after a series of src/echo executions). Deleting src/echo.gcda resets the coverage statistics.

You do not have to install wllvm (should be available after the export at the start of the lab), however you need to use clang as the LLVM_COMPILER:

export LLVM_COMPILER=clang

Part 2.a

Introduce a total of 3 different bugs in the source code coreutile examples (i.e., in 1 to 3 examples under coreutils-X.X/src). Do not forget to recompile the source files under obj-llvm for running KLEE and under obj-gcov for computing coverage (if it helps). Examples of bugs include assertion violations, a pointer error, a double free, an abort or a div. The errors should not be trivial in the start of the example. Get KLEE to detect them and explain if you had to control the complexity of the symbolic execution.

Part 2.b

Choose one example, other than echo, and use KLEE to generate tests that result in more than 95% line coverage as measured by gcov. You might need to control the complexity of symbolic execution by only considering tests that result in additional coverage.

Reporting your results See the instructions on the course page

See the instructions on the course page general submission instructions.

  • For part 1, include the code for the method, the assertions you have added and a one page report documenting your approach, reflections and any bugs you found.

  • For part 2.a include the diff of the original example(s) and the one(s) with the introduced bugs and 2-3 paragraph explanation of how you got Klee to detect them.

  • For part 2.b give the arguments to the klee runs, explain why you chose them (based on your analysis of the example’s source code) and give the additional line coverage they contributed with.