Journal "Software Engineering"
a journal on theoretical and applied science and technology
ISSN 2220-3397

Issue N7 2017 year

DOI: 10.17587/prin.8.291-299
Program Source Code Static Analysis for Memory Access Error Detection Using Backwards Execution
D. A. Orlov, orlovdmal@mpei.ru, National Research University Moscow Power Engineering Institute, Moscow, 111250, Russian Federation
Corresponding author: Orlov Dmitry A., Assistant Professor, National Research University Moscow Power Engineering Institute, 111250, Moscow, Russian Federation, E-mail: orlovdmal@mpei.ru
Received on September 04, 2016
Accepted on April 05, 2017

This paper is dedicated to static source code analysis for memory access error detection. Brief review of static source code analysis methods is given. Backwards execution method is considered. Such technique is often used in debuggers to make inspection of program state preceding to error state possible. But this method is also applicable to static source code analysis. Symbolic backward execution in some cases can simplify static analysis. For example, it simplifies analysis of conditions which must be satisfied after the loop execution. An algorithm of static source code analysis using backwards symbolic execution is proposed. The algorithm in consideration is finding if out of bounds memory access is possible in input program. The usage of algorithm proposed is restricted to a subset of programs which can be effectively executed backwards, i.e., algorithms which operations are restricted to loops, conditional jumps, indirect memory access, value copying and addition with constant. This restriction simplifies conditions generated during symbolic execution. Most of text data processing algorithms and file format parsing functions belong to this subset. A test implementation of the proposed algorithm was created. The implementation is tested using input programs which implement the following algorithms: strlen without border checking, strlen with border checking and algorithm counting number of utf-8 codepoints in string.

Keywords: static source code analysis, memory access errors, programming, algorithm theory, program testing, program verification, backwards execution, symbolic execution
pp. 291–299
For citation:
Orlov D. А. Program Source Code Static Analysis for Memory Access Error Detection Using Backwards Execution, Programmnaya Ingeneria, 2017, vol. 8, no. 7, pp. 291—299.