Keywords

1 Introduction

The technical progress achieved by academia as well as industry within the last decades led to more and more complex systems. These systems, which are composed of software and hardware components, have made their way into our daily life and are especially very important in terms of functional safety applications. To this end, it is of utter most importance to ensure that applications like the trigger unit of an airbag or a breathing apparatus for medial emergencies work as intended.

In order to ensure that such systems are getting realized correctly, the hardware as well as the software part of the system has to be checked for correctness. Since the hardware and the software part of the system are getting designed with abstract programming languages, program analysis techniques can be applied for this purpose. To this end, static program analysis like Control-Flow-Analysis  [1] as well as dynamic program analysis like Dynamic-Program-Slicing  [2] have emerged in the past. However, static as well as dynamic program analysis techniques both have major limitations (e.g. a significant number of false positives). Hence, in contrast to these program analysis techniques, the approach of symbolic execution emerged in the past  [3]. Symbolic execution has been investigated heavily in the past and already led to a significant number of tools. These tools—including KLEE  [4], DIVINE  [5], Forest  [6], or CBMC  [7]—allow to symbolically execute programming languages like C/C++. However, symbolic execution is not limited to C/C++ only. Approaches like  [8] also show that those methods can even be utilized for the execution of abstract hardware descriptions such as provided in SystemC.

In this work, we present the tool YASSi (Yet Another Symbolic Simulator) as our state-of-the-art approach for the realization of symbolic execution for academic research. Our approach is capable to symbolically execute program code written in the C/C++ language. To this end, YASSi is based on the Low Level Virtual Machine (LLVM) compiler infrastructure  [9] and utilizes the power of modern reasoning engines like Z3  [10] or Boolector  [11] for decision finding. Applying YASSi allows the user to symbolically explore his/her design and, therefore, to check certain design properties or to perform reachability analysis. Compared to other state-of-the-art symbolic execution tools, we intentionally have designed YASSi in a fashion that it is easily extendable for academic research purposes.

The remainder of this paper is structured as follows. The next section briefly reviews the principle of symbolic execution for program analysis. Based on this, we are introducing YASSi as our approach for an academic tool for symbolic execution in Sect. 3. Afterwards, we discuss the applicability of YASSi for specific applications in Sect. 4, before we conclude the paper in Sect. 5.

2 Background

This section briefly reviews the approach of symbolic execution as an advanced program analysis technique  [3]. In general, symbolic execution rests on the idea of rather than using concrete values for so-called free variables (e.g. the inputs of a function), the value of such variables is treated symbolically.

Example 1

Figure 1a shows a code snippet composed of using two free variables and three conditional statements. Depending on the value held by the variables variable_a and variable_b, the execution of the code snippet returns a different value back to the host system.

In order to perform a symbolic execution, the system has to keep track of all possible execution possibilities. To this end, symbolic execution has to evaluate all possible outcomes of branches within the source code. Moreover, the execution engine keeps track of the positive branches (i.e. the taken branch) as well as the negative branches (i.e. the non-taken branch).

Example 2

Consider again Fig. 1b which shows the Control Flow Graph (CFG) of the code snippet. Every time the execution reaches a branching condition, it is checked whether there is a possible valid assignment for the branching variable. In case of the branch as shown on top of Fig. 1b, the symbolic execution engine has to ensure that there is a valid assignment possible for variable_a which ends up in taking the branch as well as not taking the branch.

Fig. 1.
figure 1

Source code and according CFG showing nested branches.

Full size image

The symbolic execution engine has to decide whether a branch can be taken or not. To this end, modern symbolic execution engines are invoking the power of modern reasoning engines, e.g. for Satisfiability Modulo Theories (SMT), for this purpose. Moreover, the so-called branching conditions can be formulated using the so-called SMT2 constraint language  [12]. The reasoning engine decides for every branching condition if there is an assignment possible for every free variable in order to take or not take the branch. The solutions generated by the reasoning engine are then directly applied by the symbolic execution engine to perform the execution of the target code.

3 The YASSi Tool

This section now introduces the YASSi symbolic simulation toolFootnote 1. To this end, the section first introduces the modular architecture of YASSi in general before the major components of YASSi (i.e. the front-end and the back-ends) are getting discussed.

Fig. 2.
figure 2

Basic architecture of YASSi.

Full size image

The basic architecture of YASSi is illustrated in Fig. 2. As can be seen in the figure, YASSi performs several steps before the symbolic execution can be performed by running a special binary. To this end, the generation of this binary is controlled YASSi’s front-end. This binary is linked to particular YASSi back-end which keep track of the symbolic execution and commands over a reasoning engine for decisions making. In the following, we are now describing the YASSi front-end as well as the YASSi symbolic execution core back-end.

3.1 YASSi’s Frontend

In the architecture of YASSi, we are using the front-end in order to prepare the program we want to execute symbolically. As can be seen in Fig. 2, the first step is the compilation of C/C++ sources into LLVM’s Intermediate Representation (IR) format  [13]. LLVM’s IR format is based on a load and store architecture and breaks down the complexity of C/C++ codes into a basic instruction set. In the second step, the generated IR code is getting instrumented using LLVM’s optimization tool. To this end, we are going to alternate LLVM’s IR code and add special function calls for each particular instruction which is needed for the eventual symbolic execution. Once the code instrumentation has been done, we are linking the instrumented code to our back end which resolves the inserted function calls. The result of YASSi’s front-end is a binary which is ready for symbolic execution. After the execution of the binary has terminated, the front-end can access the database in order to analyze the results generated by the symbolic execution run.

3.2 YASSi’s Backends

YASSi commands over multiple back-ends. However, in this work we are only introducing YASSi’s symbolic execution core back-end. As introduced above, YASSi’s front-end performs code instrumentation by inserting callback function calls which are getting resolved by the back-end. Instead of executing the LLVM instructions, we are calling YASSi’s back-end which processes the information internally. To this end, YASSi is controlling the program execution based on Z3 which is getting used as reasoning engine in the back. Moreover, every-time the program branches, YASSi considers both execution paths and tries to find a valid solution for both paths. Therefore, YASSi creates clauses for each path-condition and forwards them to the reasoning engine. If the reasoning engine determines a valid solution, the branch is getting considered successfully and the execution continues. Same as for branches is getting used for assertions as well as other exceptions.

4 Application of YASSi

This section finally discusses some of the applications YASSi can be used for. Since the principle of symbolic execution allows it to target a wide variety of applications, we focus on those which we successfully applied with YASSi thus far.

  • Assertion Checking:

    YASSi is capable to check certain properties during execution. To this end, YASSi is capable to check assertion and to work with non-deterministic variables. Therefore, YASSi tries to violate the assertion by invoking the SMT solver. YASSi is not only capable to check assertions, it is also capable to check for traps like division by zero or out of boundary index accessing of data-structures like arrays.

  • Reachability Analysis:

    Another application case for YASSi which has been applied successfully is reachability analysis. To this end, we have applied YASSi in order to check, that certain parts of the code are unreachable which we could use to exclude certain functional safety issues.

  • Stimuli Generation:

    Next to exception checking and reachability analysis, we were able to use YASSi for stimuli generation. To this end, we were able to generate stimuli with a coverage for abstract descriptions of digital circuits. Our approach allowed it to extract these stimuli into a database and directly to apply them for checking the model. As already mentioned above, YASSi commands over multiple back-ends. Moreover, YASSi commands over a so-called replay back-end which directly can be applied to check the reached branch and line coverage  [14] for a particular set of generated stimuli.

5 Conclusion

In this work, we considered symbolic simulation as program analysis technique for C/C++ codes. This is motivated by the ever growing complexity of modern systems build up using hardware as well as software components designed using programming languages like C/C++. In order to address this, we introduced the tool YASSi as our approach for a state-of-the-art symbolic simulator for academic research. We have build YASSi in a modular fashion, which allows it directly to extend the tool for eventual later applications. YASSi has been build on top of the LLVM toolkit for compiler construction together with modern reasoning engines like Z3. YASSi is further under heavy development, and we keep adding more applications. The next milestone for the tool will be the support of floating-point variable based on the SMT2 bitvector floating-point type. YASSi is available at http://github.com/gledr/YASSi.