A taint analysis method employing symbolic computation and used for a dynamic parallel program, wherein a constraint expression is constructed according to taint propagation semantics of the parallel program, a constraint solver is used to verify whether or not a variable will be tainted under a certain type of interlacing, and a proof sequence of a tainted variable is generated. The method comprises: executing the program under a given taint input, and collecting a set of tainted variable instances under specific interlacing; executing a symbolic analysis step comprising: converting, according to the taint propagation semantics of the parallel program, an execution path into the constraint expression, so as to verify whether or not the path is a newly tainted variable; performing a path searching step comprising: using a constraint model to verify whether or not there is a branch present that can be negated, so as to search for a new path; finally, continuing to verify new paths, and iteratively performing symbolic analysis and path searching until no new paths are generated. The objective of the method is to verify whether or not certain variables existing under given input and specific scheduling conditions will be tainted by other types of interlacing, and to search for new statements so as to discover new tainted variables.
展开▼
