BRANCH RESOLUTION VIA BACKWARD SYMBOLIC EXECUTION

摘要

Possible values for a computed destination address of anexecution transfer instruction are found by a backward searchthrough a flowgraph of a program. During the search, a symbolicexpression for the destination address is successivelymodified to reflect the effect of each prior instruction until thesymbolic expression represents an absolute or program-counterrelative address, or until the search can no longer continue. Thesearch can no longer continue, for example, when an instructionis reached that affects the value of the expression in anindefinite way. When backward symbolic execution reaches theentry point of a block in the flowgraph, backward symbolicexecution proceeds backward to each predecessor block that hasnot already been examined for the execution transfer instruction.Therefore multiple definite values as well as a value of"unknown" may be found for a computed destination address.Preferably backward symbolic execution is performed whileconstructing the flowgraph, in order to find the locations ofadditional instructions. As additional instructions are found, newblocks and new paths between blocks are added to the flowgraph.Backward symbolic execution is repeated when the newpaths may provide additional values for the computed destinationaddresses.