Journal "Software Engineering"
a journal on theoretical and applied science and technology
ISSN 2220-3397
Issue N7 2017 year
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.