| 1. |
- Bygde, Stefan, et al.
(author)
-
Fully Bounded Polyhedral Analysis of Integers with Wrapping
- 2011
-
In: Electronic Notes in Theoretical Computer Science. - : Elsevier BV. - 1571-0661. ; 288, s. 3-13
-
Journal article (peer-reviewed)abstract
- analysis technique to discover linear relationships among variables in a program. However, the classical way of performing polyhedral analysis does not model the fact that values typically are stored as fixed-size binary strings and usually have a wrap-around semantics in the case of overflows. In embedded systems where 16-bit or even 8-bit processors are used, wrapping behaviour may even be used intentionally. Thus, to accurately and correctly analyse such systems, the wrapping has to be modelled. We present an approach to polyhedral analysis which derives polyhedra that are bounded in all dimensions and thus provides polyhedra that contain a finite number of integer points. Our approach uses a previously suggested wrapping technique for polyhedra but combines it in a novel way with limited widening, a suitable placement of widening points and restrictions on unbounded variables. We show how our method has the potential to significantly increase the precision compared to the previously suggested wrapping method.
|
|
| 2. |
- Bygde, Stefan, et al.
(author)
-
Improved Precision in Polyhedral Analysis with Wrapping
- 2017
-
In: Science of Computer Programming. - : Elsevier BV. - 0167-6423 .- 1872-7964. ; 133, s. 74-87
-
Journal article (peer-reviewed)abstract
- Abstract interpretation using convex polyhedra is a common and powerful program analysis technique to discover linear relationships among variables in a program. However, the classical way of performing polyhedral analysis does not model the fact that values typically are stored as xed-size binary strings and usually have wrap-around semantics in the case of over ows. In resource-constrained embedded systems, where 8- or 16-bit processors are used, wrapping behaviour may even be used intentionally to save instructions and execution time. Thus, to analyse such systems accurately and correctly, the wrapping has to be modelled. We present an approach to polyhedral analysis which derives polyhedra that are bounded in all dimensions. Our approach is based on a previously suggested wrapping technique by Simon and King, combined with limited widening, a suitable placement of widening points and size-induced restrictions on unbounded variables. With this method, we can derive fully bounded polyhedra in every step of the analysis. We have implemented our method and Simon and King's method compared them. Our experiments show that for a suite of benchmark programs it gives at least as precise result as Simon and King's method. In some cases we obtain a significantly improved result.
|
|
| 3. |
- Bygde, Stefan, et al.
(author)
-
Static Analysis of Bounded Polyhedra
- 2011
-
Conference paper (peer-reviewed)abstract
- We present a method for polyhedral abstract interpretation which derives fully bounded polyhedra for every step in the analysis. Contrary to classical polyhedral analysis, this method is sound for integer-valued variables stored as fixed-size binary strings; wrap-arounds are correctly modelled. Our work is based on earlier work by Axel Simon and Andy King but aims to significantly reduce the precision loss introduced in their method.
|
|
| 4. |
- Holsti, Niklas, et al.
(author)
-
Combining Bound-T and SWEET to Analyse Dynamic Control Flow in Machine-Code Programs
- 2014
-
Reports (other academic/artistic)abstract
- The first step in the static analysis of a machine-code subprogram is to construct the control-flow graph. The typical method is to start from the known entry-point address of the subprogram, retrieve and decode the instruction at that point, insert it in the control-flow graph, determine the address(es) of the successor instruction(s) from the known semantics of the instruction set, and repeat the process for the successor instructions until all reachable instructions and control flows are discovered and entered in the control-flow graph. This procedure is straight-forward as long as the successors of each instruction are statically defined. However, most instruction sets allow for dynamically determined successors, usually by allowing the target address of a branch to be set by the run-time, dynamically computed value of a register. We call such instructions dynamic branches. To construct the control-flow graph, a static analyser must somehow discover the possible values of the target address, in other words, it must perform a value-analysis of the program. This is problematic for two reasons. Firstly, the value-analysis must be applied to an incomplete control-flow graph, which means that the value-analysis will also be incomplete, and may be an under-estimate of the value-set for the complete subprogram. Second, value-analyses typically over-estimate the value-set, which means that the set of possible target addresses of the dynamic branch may be over-estimated, which leads to an over-estimate of the control- flow graph. The over-estimated graph may include instructions and control flows that do not really belong to the subprogram under analysis. This report describes how we connected two analysis tools, Bound-T from Tidorum Ltd and SWEET from Mälardalen University, so that the powerful "abstract execution" analysis in SWEET can be invoked from Bound-T to resolve dynamic branches that Bound-T finds in the machine-code program under analysis. The program-representation language ALF, defined by the SWEET group, is used as an interface language between Bound-T and SWEET. We evaluate the combined analysis on example programs, including both synthetic and real ones, and conclude that the approach is promising but not yet a great improvement. Bound-T contains several special-case analyses for dynamic branches, which currently perform slightly better than SWEET's more general analyses. However, planned improvements to SWEET may result in an analysis which is at least as powerful but more robust than the analyses in Bound-T alone.
|
|
| 5. |
- von Hanxleden, Reinhard, et al.
(author)
-
WCET Tool Challenge 2011: Report
- 2011
-
In: Proc. 11th International Workshop on Worst-Case Execution Time (WCET) Analysis (WCET 2011). - 9781632663153 ; , s. 104-138
-
Conference paper (peer-reviewed)abstract
- Following the successful WCET Tool Challenges in 2006 and 2008, the third event in this series was organized in 2011, again with support from the ARTIST DESIGN Network of Excellence. Following the practice established in the previous Challenges, the WCET Tool Challenge 2011 (WCC'11) defined two kinds of problems to be solved by the Challenge participants with their tools, WCET problems, which ask for bounds on the execution time, and flow-analysis problems, which ask for bounds on the number of times certain parts of the code can be executed. The benchmarks to be used in WCC'11 were debie1, PapaBench, and an industrial-strength application from the automotive domain provided by Daimler. Two default execution platforms were suggested to the participants, the ARM7 as "simple target" and the MPC5553/5554 as a "complex target", but participants were free to use other platforms as well. Ten tools participated in WCC'11: aiT, AstrEe, Bound-T, FORTAS, METAMOC, OTAWA, SWEET, TimeWeaver, TuBound and WCA.
|
|
| 6. |
|
|
| 7. |
- Wilhelm, Reinhard, et al.
(author)
-
The worst-case execution-time problem—overview of methods and survey of tools
- 2008
-
In: ACM Transactions on Embedded Computing Systems. - : Association for Computing Machinery (ACM). - 1539-9087 .- 1558-3465. ; 7:3, s. article nr: 36-
-
Journal article (peer-reviewed)abstract
- The determination of upper bounds on execution times, commonly called worst-case execution times (WCETs), is a necessary step in the development and validation process for hard real-time systems. This problem is hard if the underlying processor architecture has components, such as caches, pipelines, branch prediction, and other speculative components. This article describes different approaches to this problem and surveys several commercially available tools(1) and research prototypes.
|
|
