Withdrawal by retrospective symbolic design

摘要

Possible values for a computed destination address of an execution transfer instruction are found by a backward search through a flowgraph of a program. During the search, a symbolic expression for the destination address is successively modified to reflect the effect of each prior instruction until the symbolic expression represents an absolute or program-counter relative address, or until the search can no longer continue. The search can no longer continue, for example, when an instruction is reached that affects the value of the expression in an indefinite way. When backward symbolic execution reaches the entry point of a block in the flowgraph, backward symbolic execution proceeds backward to each predecessor block that has not 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 while constructing the flowgraph, in order to find the locations of additional instructions. As additional instructions are found, new blocks and new paths between blocks are added to the flowgraph. Backward symbolic execution is repeated when the new paths may provide additional values for the computed destination addresses.