Rechnerarchitektur - Universität Freiburg

Projekte

Accurate Dead Code Detection in Embedded C Code by Arithmetic Constraint Solving

Projektbeschreibung

The transfer project aims at efficient and precise detection of dead code in reactive, control- oriented, and floating-point dominated C programs, in particular those derived from Simulink- plus-Stateflow models of embedded control applications via automatic C-code generation or those hand-coded according to guidelines as imposed in the embedded domain. Dead, i.e. dynamically unreachable, code segments occur regularly in generated code due to case distinctions, exception handling, etc. necessary for a semantically adequate implementation of, e.g., a Simulink block in unrestricted application context being rendered redundant in a specific context. Likewise, dead code is regularly introduced into hand-written code either intentionally by proven engineering methods like defensive programming or inadvertently during the course of code reuse. Finding such dead code is more than just a commodity: (1) it facilitates code optimization enhancing space (less code volume) and time (fewer branching, enhanced cacheability and code prefetch) efficiency; (2) it adds to the readability of the resulting code corpus, thus making it less prone to the addition of further errors as well as positively influencing the time needed for development and maintenance, and last but not least, (3) it permits a more rigorous interpretation of coverage-based criteria in code validation and certification, as present in testing regimes recommended in various standards for embedded system development, as well as meeting the demand for absence of dead code imposed by some standards for high-integrity software. Dead code detection for code generated from model-based design tools, like Simulink, is com- plicated by the fact that their code generators tend to encode the major part of the model’s control flow into the data part of the C code generated, for example the hierarchical state of Stateflow charts by vectors of Booleans, thereby blurring the distinction between control and data. On top of this comes an intrinsic dependency of control flow on deep histories of complex floating-point computations, e.g., having to answer questions like “can this saturating integrator in the middle of a large Simulink model ever receive a sequence of inputs causing it to wind up?”. Deciding this question, which may qualify code associated to wind-up control as redundant, would in principle require tracing the integrator’s possible inputs over an unbounded temporal horizon, where in each time instant, this input may depend on a complex computation involving numerous floating-point and discrete data entities. Constructions blurring the distinction between control and data are also commonplace in hand-written embedded control software, where a central control loop often defers obligations to a set of dedicated handlers, some of which may be generic by offering state and data dependent control flow. With respect to a clear architectural structure of the program this must in many cases be considered as good programming style and therefore can not simply be eliminated by more restrictive coding guidelines (though there exist attempts to do so, e.g. in MISRA). The main goal of the transfer project is to develop a method which (1) is able to cope with the lacking distinction between control and data as well as the dominant impact of (frequently non-linear) floating-point computations on reachability of code and (2) at the same time scales to industrial-size programs. Various techniques for dealing with individual issues have been proposed in the recent past. Abstract interpretation (AI) provides scalability to very large programs, yet falls short on exactness when data operations can fraction and reshuffle the data part of the state space quite arbitrarily. Counter-example guided abstraction refinement (CEGAR) has been shown to provide adaptive abstraction of the state-space by often being able to uncover surprisingly concise abstractions of the interplay of control and data in a property-driven manner, but is as of now constrained to analysis either of programs exploiting confined fragments of arithmetic (mostly linear) only or of full-fledged hybrid systems featuring just tiny control skeletons. Recent breakthroughs in non-linear arithmetic constraint solving based on conflict-driven clause learning over arithmetic theories (CDCL(T)), to a significant extent originating in AVACS project H1/2, can solve extremely large arithmetic constraint systems with complex Boolean structure and linear, polynomial, and transcendental arithmetic, yet fail to provide summaries for loops in the control flow and do not scale enough to cover the full branching structure of a complex program in just one sweep. While adequate building blocks for the desired analysis technology are thus available, none of them in isolation would be able to solve the problem at hand, calling for a combination of these technologies and for tuning on real application code, which motivates the proposed transfer project. It is expected that this combination will provide dead code detection of unprecedented accuracy in floating-point dominated reactive C code, as originating from code generation in model-based development environments as well as hand-coding in the embedded control domain.

Laufzeit

01.07.2014 bis 31.12.2016

Projektleitung

Bernd Becker

WWW: https://ira.informatik.uni-freiburg.de/src/projects_view.php?projectID=87

Kooperationspartner

Prof. Dr. Martin Fränzle (Universität Oldenburg) Dr. Thomas Scheidsteger (Universität Oldenburg) M.Sc. Ahmed Mahdi (Universität Oldenburg) Dr. Tom Bienmüller (BTC Embedded Systems AG) Dr. Tino Teige (BTC Embedded Systems AG) Dr. Detlef Fehrer (Sick AG)

Publikationen

Jahre: 2017 | 2016

2017

nach oben zur Jahresübersicht

Felix Neubauer, Karsten Scheibler, Bernd Becker, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer
Accurate Dead Code Detection in Embedded C Code by Arithmetic Constraint Solving
2017 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
KurzfassungUnreachable 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.

2016

nach oben zur Jahresübersicht

Felix Neubauer, Karsten Scheibler, Bernd Becker, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer
Accurate Dead Code Detection in Embedded C Code by Arithmetic Constraint Solving
2016 First International Workshop on Satisfiability Checking and Symbolic Computation - FETOPEN-CSA SC2 Workshop - Affiliated with SYNASC 2016
KurzfassungUnreachable 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.
Karsten Scheibler, Felix Neubauer, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer, Bernd Becker
Accurate ICP-based Floating-Point Reasoning
2016 Formal Methods in Computer-Aided Design, Seiten: 177 - 184
KurzfassungIn scientific and technical software, floating-point arithmetic is often used to approximate arithmetic on physical quantities natively modeled as reals. Checking properties for such programs (e.g. proving unreachability of code fragments) requires accurate reasoning over floating-point arithmetic. Currently, most of the SMT-solvers addressing this problem class rely on bit-blasting. Recently, methods based on reasoning in interval lattices have been lifted from the reals (where they traditionally have been successful) to the floating-point numbers. The approach presented in this paper follows the latter line of interval-based reasoning, but extends it by including bitwise integer operations and cast operations between integer and floating-point arithmetic. Such operations have hitherto been omitted, as they tend to define sets not concisely representable in interval lattices, and were consequently considered the domain of bit-blasting approaches. By adding them to interval-based reasoning, the full range of basic data types and operations of C programs is supported. Furthermore, we propose techniques in order to mitigate the problem of aliasing during interval reasoning. The experimental results confirm the efficacy of the proposed techniques. Our approach outperforms solvers relying on bit-blasting as well as the existing interval-based SMT-solver.
Ahmed Mahdi, Karsten Scheibler, Felix Neubauer, Martin Fränzle, Bernd Becker
Advancing software model checking beyond linear arithmetic theories
2016 12th International Haifa Verification Conference, HVC 2016, Haifa, Israel, November 14-17, 2016 Twelfth Haifa Verification Conference 2016, Bloem, Roderick, Arbel, Eli (Eds.), Band: 10028, Seiten: 186 - 201
KurzfassungMotivated by the practical need for verifying embedded control programs involving linear, polynomial, and transcendental arithmetics, we demonstrate in this paper a CEGAR technique addressing reachability checking over that rich fragment of arithmetics. In contrast to previous approaches, it is neither based on bit-blasting of floating- point implementations nor confined to decidable fragments of real arithmetic, namely linear or polynomial arithmetic. Its CEGAR loop is based on Craig interpolation within the iSAT3 SMT solver, which employs (abstract) conflict-driven clause learning (CDCL) over interval domains together with interval constraint propagation. As usual, the interpolants thus obtained on spurious counterexamples are used to subsequently refine the abstraction, yet in contrast to manipulating and refining the state set of a discrete-state abstraction, we propose a novel technique for refining the abstraction, where we annotate the abstract model’s transitions with side-conditions summarizing their effect. We exploit this for implementing case-based reasoning based on assumption-commitment predicates extracted from the stepwise interpolants in a lazy abstraction mechanism. We implemented our approach within iSAT3 and demonstrate its effectiveness by verifying several benchmarks.
Karsten Scheibler, Felix Neubauer, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer, Bernd Becker
Extending iSAT3 with ICP-Contractors for Bitwise Integer Operations
AVACS Technical Report, SFB/TR 14 AVACS, Subproject T1, Band: 116, 2016