-Unreachable code fragments in software, despite not having a negative impact on the functional behavior, can have a bad effect in other areas, such as code optimization or coverage-based code validation and certification. Especially the latter is important in industrial, safety critical environments, where detecting such dead code is a major goal to adjust the coverage of software tests. In the context of embedded systems we focus on C programs which are reactive, control-oriented, and floating-point dominated. Such programs are either automatically generated from Simulink-plus-Stateflow models or hand-written according to coding guidelines. While there are various techniques e. g. abstract interpretation or Counterexample guided abstraction refinement (CEGAR) - to deal with individual issues of this domain, there is none which can cover all of them. The AVACS transfer project T1 aims at the combination of these techniques in order to provide an accurate and efficient dead code detection. In this paper we present the ideas and goals of the project as well as the current status (including very promising experimental results) and future challenges.
Index Terms—formal specification, formal verification, SMT, floating-point, dead code detection, CEGAR, abstract interpretation
The occurence of dead (i. e. unreachable) code fragments in sizable software development projects is a regular phenomenon – it can be created either intentionally (e. g. defensive programming) or unintentionally (e. g. reusing of code, modification of program context) in hand-written programs or as a byproduct of automated code generation. Although dead code has no negative impact on the functional behavior of the software, it can have a bad effect e. g. on code optimization or coverage-based code validation and certification. Especially the latter is important in industrial, safety critical environments, where standards (e. g. ISO 26262) for high-integrity software demand, among other criteria, reaching a certain test coverage or the absence of dead code. Obviously the presence of dead code violates the latter demand but also affects the interpretation of coverage-based criteria negatively. Therefore it is a major goal to detect dead code from high-integrity software and thereby be able to adjust the test coverage.
The classical dead code detection in compilers is not suitable to meet these demands. Compilers have to be fast which does not allow complex dead code analysis at compiletime, but the analysis itself has to be sound, which means that only really unreachable code may be marked as dead. The consequence of this tradeoff is a vastly incomplete detection, where substantial amounts of dead code are not discovered. In our use cases we also need a sound method to securely detect dead code, but additionally it has to be highly accurate with respect to both the amount (enhancing the interpretation of the test coverage) and localization (approching the demand of dead code free programs) of the dead code detected.
In the context of embedded systems our focus lies on reactive, control-oriented, and floating-point dominated C programs, in particular those automatically generated from Simulink-plus-Stateflow models of embedded control applications or those hand-written according to coding guidelines. Dead code detection in this domain is quite difficult because there might be no clear distinction between control and data in the C code. Considering automatically generated code this lack of distinction is caused by encoding the major part of the model’s control flow into the data part of the C code. Hand-written embedded control software on the other hand often has a central control loop which defers obligations to a set of dedicated handlers. Some of these handlers are generic, offering both a state and data dependent control flow. This construction also blurs the distinction between control and data. An additional difficulty is the dependency of the control flow on complex floating-point computations.
The development of a method to handle these challenges, namely: (1) handling the lack of distinction between control and data (2) dealing with the dominant impact of (often non-linear) floating-point computations on the reachability of code (3) scaling to industrial-size programs is the main goal of the AVACS1 transfer project T1. This project is a transregional collaboration between the University of Freiburg2, the Carl von Ossietzky University of Oldenburg3 and the industrial partners BTC Embedded Systems AG4 in
Oldenburg and Sick AG5 in Waldkirch.
There are various techniques which are able to deal with
individual issues of the list above. Abstract interpretation (AI)
[
The transfer project aims at the combination of those techniques in order to handle all required challenges and to provide an accurate and efficient dead code detection. This paper presents the current status of the project, ideas and possible solutions to unresolved issues and further challenges.
Structure of the paper: After introducing the goals and challenges of the AVACS transfer project in the current section, we describe the model checking-based tool chain for structural code coverage analysis of BTC Embedded Systems in Section II. In Section III we speak about the integration of our SMTsolver iSAT3 as an alternative backend solver into this tool chain and the experimental results vs. the standard backend solver. Section IV gives an outlook about future challenges, before Section V concludes this paper.
STRUCTURAL CODE COVERAGE ANALYSIS
One of the most prominent test criteria for production code
in industrial and in particular safety-critical domains relies on
structural code coverage such as function, statement, branch,
and condition coverage or MC/DC [
In the following, we describe by way of example a typical tool chain for automatic analysis of code coverage being based on model checking backend tools.
In Listing 1, a small excerpt of a C code under test is given.
Though – for illustration reasons – the code fragment is rather
simple, it however contains some frequent code constructs
occuring in practice which need to be handled within the tool
5https://www.sick.com
1 #include <math.h>
2
3 typedef struct { double x, y; } point_t;
4
5 double distance(int length, point_t p[]) {
6 double sum = 0;
7 unsigned int i;
8 for (i = 0; i < length-1; i++) {
9 sum += sqrt((p[i].x - p[i+1].x) * (p[i].y - p[i+1].y)
);
10 }
11 return sum;
12 }
13
14 unsigned char step(int length, point_t p_array[]) {
15 double dist_value = distance(length, p_array);
16 unsigned char dist_level_ok;
17 if (dist_value <= 10.0) {
18 dist_level_ok = 0;
19 } else {
20 dist_level_ok = 1;
21 }
22 return dist_level_ok;
23 }
24
25 point_t p_array[
Listing 1. example 1 orig.c chain. The “main”-function sketches a typical reactive program with an unbounded feedback loop: first, all input data for the current iteration or step are received, then the actual function is executed, and finally the computed outputs are transmitted. Thereafter the program waits for the next loop iteration.
In each step, the “step”-function takes an array of three two-dimensional points (modelled by struct type “point t” consisting of two variables of scalar type “double”) as input and returns, whether the level of the aggregated distance of consecutive points is okay or not.
Please note that the C code contains several floating-point computations and, moreover, relies on the function “sqrt” from the standard C library “math.h”. This actually is representative as there is an increasing trend of using floating-point processors and production code in industrial applications.
With regard to the use of the “math.h” library, we remark that there are two major ways of dealing with such complex mathematical functions such as “sqrt” in a model checking context: first, the production code itself resolves the problem, namely by reducing such complex functions to basic operations, or, second, to keep these functions in the code and apply a model checker that has dedicated support for such complex functions. Concerning performance, the second option has a clear benefit over the first one as implementations of mathematical functions are frequently very complex and contain several hundreds lines of code. A model checker with native “math.h” support can exploit dedicated algorithms which are generally much more efficient. In the following, we assume a model-checking backend tool that is able to handle the function “sqrt”.
In the first step of the tool chain for analyzing code coverage, we need to annotate the original program with additional constructs to automatically deal with code coverage metrics. In our example we concentrate on statement coverage and – for the sake of simplicity – we just aim at covering the statements in lines 18 and 20. For the purpose of observing the reachability of the corresponding lines, two new variables “LINE X REACHED”, “LINE Y REACHED” are introduced. Listing 2 shows the neccessary changes for one possible annotation method.
[...] // new observer variables for coverage unsigned char LINE_X_REACHED = 0; unsigned char LINE_Y_REACHED = 0; [...] if (dist_value <= 10.0) {
LINE_X_REACHED = 1; dist_level_ok = 0; } else {
LINE_Y_REACHED = 1; dist_level_ok = 1;
After this annotation with coverage goals, normally the C code is translated to an intermediate language called SMI (which is a C-like programming language). To keep this example simple, we skip this translation and explain the further steps on C code also.
The original code is now instrumented in such a way that automatic analysis w. r. t. code coverage by a model checker is rendered possible. In order to reach the input language of a model checker, e. g. a declarative, logical description as in a SAT or SMT solver, the instrumented code needs to be transformed into a syntactically simpler form. Two usual transformation steps are the following: function calls are resolved complex structural data types are flattened
Usually, a model checker is called separately per proof obligation, in our context per coverage goal. To further optimize the code in that respect, a cone-of-influence reduction is performed, i. e. all code fragments that do not directly or indirectly influence the state of the corresponding goal expression are removed. Listing 3 shows the result of the two transformation steps mentioned above as well as an example for the cone of the goal “variable LINE X REACHED becomes 1”.
Depending on the capabilities and requirements of the concrete model checker, further transformations might be applied, such as: loop unwinding (naive or optimized; see Listing 4 for the optimized variant) static single assignment form, cf. Listing 5
The resulting code in static single assignment form can then be translated in a rather simple way into a corresponding SMT formula (k) with loop iteration depth k such that the following property holds:
Property 1: The goal “variable LINE X REACHED becomes 1” is covered within k steps (meaning that the statement in line 18 of the original code is reached) if and only if the SMT formula (k) is satisfiable.
One very important feature of the above approach is that a satisfying assignment of (k) corresponds to a test case of the original program that proves coverage of the corresponding goal. We remark that construction of such a test case is a layered approach starting from the satisfying assignment of the lowermost SMT layer up to the original C code layer.
If it turns out that the SMT formula (k) is unsatisfiable then the corresponding coverage goal is unreachable within k iterations. This may be a hint for dead code.
BTC Embedded Systems solves the SMT formula (k) with the BMC solver CBMC in the backend using k-induction to perform unreachability proofs. In the following section we will use the interval constraint solver iSAT36 with Craig interpolation as backend solver and compare it to CBMC. The iSAT algorithm was developed in AVACS project H1/2.
While SAT solving aims at finding solutions for propositional formulas (or proving the absence thereof), SMT aims at solving boolean combinations of so-called theory atoms. Such atoms may for example contain linear arithmetic over the reals or constraints involving floating-point arithmetic.
In eager SMT the Boolean structure as well as all theory atoms are translated into one big propositional formula. A SAT solver is then called once in order to determine whether there is a solution or not. This approach is also called bit-blasting. While it is in general not applicable to all theories, it is up to now the most prominent approach for SMT solvers addressing floating-point arithmetic – e.g. Z37, Mathsat8 and CBMC9 rely on this technique.
When doing SMT lazily, the formula is split into a set of theory atoms and a Boolean skeleton which abstracts the truthvalues of the theory atoms with Boolean literals. The Boolean skeleton is processed by a SAT-solver in order to search for a satisfying assignment. If such an assignment is found, a separate theory solver is used to check whether the theory atoms are consistent under the truth values determined by 6https://projects.informatik.uni-freiburg.de/projects/isat3 7https://github.com/Z3Prover/z3/ 8http://mathsat.fbk.eu/ 9http://www.cprover.org/cbmc/ the SAT-solver. In case of an inconsistency, the theory solver identifies an infeasible subset of the theory atoms which is then encoded into a clause and added to the Boolean skeleton. Thus, in lazy SMT the SAT solver is called multiple times and operates together with a theory solver in order to refine the Boolean skeleton incrementally. Therefore, this scheme is also abbreviated as DPLL(T) or CDCL(T) – with T being the theory used within the atoms.
In contrast to CDCL(T), the iSAT algorithm [
In this paper we build on the third implementation of
the iSAT algorithm which is called iSAT3 [
Thus, ICP contractors are responsible for performing the
arithmetic reasoning. Adding support for new operations
essentially requires adding further ICP contractors. Recently,
we adapted iSAT3 in order to support accurate reasoning
for floating-point arithmetic [
Supporting the floating-point domain also affects the completeness of the ICP-based decision procedure. While ICP reasoning is in general incomplete on real arithmetics, it gains completeness in the finite floating-point domain.
In the following we give a summary of the experiments
performed in [
In our measurements, we used the version of SMI-CBMC
which is part of BTC EmbeddedTester R 3.4 (July 2014).
SMICBMC supports incremental BMC [
Similar to SMI-CBMC, SMI-iSAT3 operates on SMI files as well. It is a prototypical implementation which runs in a Cygwin environment and uses a bunch of wrapper scripts in order to (1) translate the given SMI file into the iSAT3 input language, and to (2) validate every satisfying assignment found by iSAT3 by an SMI simulator. All experiments were performed on an Intel Core i7-2600 with 3.4 GHz and 8 GB RAM under Windows 7 (64 bit). We set a time limit of 60 seconds per benchmark. Setting a memory limit within the Cygwin environment did not work properly. Therefore, we omitted such a limit.
0
The benchmarks are encoded as BMC problems. For both solvers we allowed up to 51 BMC unwindings per benchmark. The results are shown in Figure 1. The diagram depicts the number of solved benchmarks together with the run time needed per benchmark. In the table, the columns S+U, SAT, U51 and U1 show the number of solved instances (SAT: satisfiable; U51: unsatisfiable until depth 51; U1: unsatisfiable for all depths proved with k-induction or Craig interpolation; S+U: SAT + U51 + U1). The column TO shows the number of aborted benchmarks due to a timeout.
In order to detect unreachability (e. g. dead-code), CBMC uses k-induction, while iSAT3 uses Craig interpolation. Both solvers perform equally well when counting the number of solved satisfiable instances. The picture changes when looking 11http://www.cprover.org/svn/cbmc/releases/cbmc-4.8-incremental/ SMI-CBMC SMI-iSAT3 60s 40s e m i
T 20s 0s at the number of solved U1 instances – which are of special interest in the context of dead-code detection. Here, SMIiSAT3 proves for 831 instances that the code fragment of interest is unreachable, which is an improvement of 30% compared to the 631 instances found by SMI-CBMC. Similarly, the number of solved U51 instances is higher in SMIiSAT3: 172 compared to 44. Furthermore, when looking at the accumulated number of solved instances, SMI-iSAT3 solves 331 instances more than SMI-CBMC.
Due to the prototypical Cygwin-based integration, SMIiSAT3 has some sort of initial runtime-offset (as revealed by the diagram in Figure 1). Despite this penalty SMI-iSAT3 outperforms SMI-CBMC in terms of runtime. E. g. when considering the instances which were solved within 3 seconds then SMI-CBMC solved 5305 such instances, while SMIiSAT3 finished 6960.
A. Counterexample Guided Abstraction Refinement
CEGAR [
Craig interpolation (CI) thus is our workhorse for
abstraction refinement in the CEGAR loop. In conjunction with
CEGAR, in software verification with lazy abstraction
technique [
CEGAR has been applied successfully in the context of
programs [
As the transfer project aims at covering analysis of handwritten embedded C code also, the ability to deal with the implicit transfer of control flow mediated by external interrupts is of importance, as interrupt handlers are a traditional means of ensuring reactivity to asynchronous events. The specific problem here is that in contrast to the control flow mediated by explicit control structures, interrupts can divert the control flow at any time. Analyzing such code by means of symbolic path enumeration in SMT-based bounded model checking would be prohibitively expensive due to the enormous branching width of the computation tree induced by unconstrained interrupts. To handle this problem, we are setting out to combine a number of techniques, the two most prominent of which are described in the following.
Semantics-preserving restriction of interrupt points: As interrupt handlers in embedded software tend to share only a small set of global variables with the main program, extensive assignment sinking or lifting is possible between statements in the main program and the interrupt routine. This implies that formally possible interrupt points can be eliminated from the analysis, as the execution sequences are confluent with those obtained from somewhat earlier or later interrupts. The analysis can thus w. l. o. g. confine control flow to interrupts happening at a limited subset of the factually possible interrupt points, e. g. just before the main program reads variables affected by the interrupt handler. This reduction reduces branching in the execution tree and helps SMT-based analysis.
Computation of summaries for interrupt routines: In order to accelerate analysis of the possible effect of interrupts on the main program’s control flow (and thus, code reachability), we will take advantage of summaries for interrupt routines obtained using abstract interpretation and inter-procedural analysis. Abstract interpretation here is based on exploiting iSAT’s floating-point and integer domains as abstract domains and iSAT’s corresponding contractors as abstract transformers when analyzing straight-line code. Inter-procedural (or interinterrupt-handler) analysis is then achieved by mutually using abstract interpretation on the individual interrupt handlers to compute safe approximations of the possible return values based on (over-approximate) knowledge of the possible entry values and on the main program to compute safe approximations of the possible entry values to interrupt handlers based on (over-approximate) knowledge of the possible return values.
The summaries thus obtained will later be exploited in the exact SMT-based analysis, where they can prune the search space tremendously before unfolding detailed statement sequences across interrupts.
Currently iSAT3 only supports floating-point reasoning for the basic arithmetic operations (Addition, Subtraction, Multiplication and Division). In the industrial context the support of more complex arithmetic operations such as exp, sin, cos, sqrt is mandatory and should be included in the current solver. Implementing these operations in iSAT3 might also have an advantage compared to bit-blasting solutions since in the latter context all those operations have to be translated into one big propositional formula while iSAT3 can handle them on the arithmetic level.
Alongside k-induction (CBMC) and Craig interpretation
(iSAT3) there exist other techniques (e. g. IC3 [
Symbolic Computation methods (such as Gro¨ bner bases
[
The AVACS transfer project T1 aims at a method for accurate dead code detection in embedded C code using arithmetic constraint solving. While in the target domain of reactive, control-oriented, and floating-point dominated embedded C programs several methods exist to deal with parts of the difficulties induced by this domain, there is none which can cover all of them. Thus a combination of these techniques as a solution seems obvious.
As a first step we integrated iSAT3 (with added support for floating-point arithmetic and Craig interpolation) into the tool chain of BTC Embedded Systems as an alternative backend solver. This allows us to perform code coverage analysis on automatically generated C code of industrial size including floating-point operations. The experimental results show, that iSAT3 is competitive in this environment – it is even able to prove more code fragments of interest as unreachable.
To tackle the remaining challenges of the transfer project there is work in progress concerning CEGAR and interrupt handling. Furthermore there are some ideas to improve the current method.
This work has been supported by the German Research Foundation (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (DFG, SFB/TR 14 AVACS).