Catchconv: Symbolic execution and run-time type inference for integer conversion errors
David Alexander Molnar and David Wagner
EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2007-23
February 4, 2007
http://www.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://www.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://www.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-23.html %F Molnar:EECS-2007-23