David Alexander Molnar and David Wagner

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2007-23
February 4, 2007

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-23.pdf

We propose an approach that combines symbolic execution and run-time type inference from a sample program run to generate test cases, and we apply our approach to signed/unsigned conversion errors in programs. A signed/unsigned conversion error occurs when a program makes control flow decisions about a value based on treating it as a signed integer, but then later converts the value to an unsigned integer in a way that breaks the program's implicit assumptions. Our tool follows the approach of Larson and Austin in using an example input to pick a program path for analysis, and we use symbolic execution to attempt synthesis of a program input exhibiting an error. We describe a proof of concept implementation that uses the Valgrind binary analysis framework and the STP decision procedure, and we report on preliminary experiences. Our implementation is available at http://www.sf.net/projects/catchconv .

BibTeX citation:

@techreport{Molnar:EECS-2007-23,
    Author = {Molnar, David Alexander and Wagner, David},
    Title = {Catchconv: Symbolic execution and run-time type inference for integer conversion errors},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2007},
    Month = {Feb},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-23.html},
    Number = {UCB/EECS-2007-23},
    Abstract = {We propose an approach that combines symbolic execution and run-time type inference from a sample program run to generate test cases, and we apply our approach to signed/unsigned conversion errors in programs. A signed/unsigned conversion error occurs when a program makes control flow decisions about a value based on treating it as a signed integer, but then later converts the value to an unsigned integer in a way that breaks the program's implicit assumptions. Our tool follows the approach of Larson and Austin in using an example input to pick a program path for analysis, and we use symbolic
execution to attempt synthesis of a program input exhibiting an error. We describe a proof of concept implementation that uses the Valgrind binary analysis framework and the STP decision procedure, and we report on preliminary experiences. Our implementation is available at http://www.sf.net/projects/catchconv .}
}

EndNote citation:

%0 Report
%A Molnar, David Alexander
%A Wagner, David
%T Catchconv: Symbolic execution and run-time type inference for integer conversion errors
%I EECS Department, University of California, Berkeley
%D 2007
%8 February 4
%@ UCB/EECS-2007-23
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-23.html
%F Molnar:EECS-2007-23