Symbolic execution of alternative branches

Patent metadata

Field	Value
Publication number	US-2017286271-A1
Application number	US-201615084617-A
Country	US
Kind code	A1
Filing date	Mar 30, 2016
Priority date	Mar 30, 2016
Publication date	Oct 5, 2017
Grant date	—

Abstract

Method, apparatus and product for symbolic execution of alternative branches. The method comprising reaching, during symbolic execution of a Control Flow Graph (CFG) of a program, a branching node in the CFG with a first symbolic state, wherein the branching has at least a first branch and a second branch, wherein the first and second branches end at a joining node in the CFG. The method further comprises symbolically executing the first branch using the first symbolic state so as to determine a second symbolic state. The method further comprises symbolically executing the second branch using the second symbolic state so as to determine a third symbolic state. Accordingly, the third symbolic state is based on sequential symbolic execution of alternative branches

First claim

What is claimed is:

1 . A computer-implemented method for performing symbolic execution of a computer program, wherein the symbolic execution traverses a Control Flow Graph (CFG) of the computer program while updating a symbolic state of the computer program, the method comprising:
reaching a branching node in the CFG with a first symbolic state, wherein the branching has at least a first branch and a second branch, wherein the first and second branches end at a joining node in the CFG; symbolically executing the first branch using the first symbolic state, whereby a second symbolic state is determined; and symbolically executing the second branch using the second symbolic state, whereby a third symbolic state is determined, the third symbolic state is based on sequential symbolic execution of alternative branches.

2 . The computer-implemented method of claim 1 , wherein the first branch comprises an assignment instruction, wherein the first branch is taken under a first branching condition, wherein said symbolically executing the first branch comprises updating the first symbolic state to reflect a conditional assignment in accordance with the assignment instruction that is conditioned on the first branching condition.

3 . The computer-implemented method of claim 2 , wherein the assignment instruction is an assignment instruction to a variable having a definition scope that extends beyond the first branch.

4 . The computer-implemented method of claim 2 , wherein the first branch comprises a second assignment instruction to a local variable, wherein the local variable having a definition scope that is internal to the first branch, wherein said symbolically executing the first branch comprises updating the first symbolic state to reflect an unconditional assignment in accordance with the second assignment instruction.

5 . The computer-implemented method of claim 2 , wherein the second branch comprises a second assignment instruction, wherein the second branch is taken under a second branching condition, wherein said symbolically executing the second branch comprises updating the second symbolic state to reflect a conditional assignment in accordance with the second assignment instruction that is conditioned on the second branching condition.

6 . The computer-implemented method of claim 1 , wherein the first branch comprises an instruction having a side effect external to the first branch, wherein the first branch is taken under a first branching condition, wherein said symbolically executing the first branch comprises updating the first symbolic state to reflect execution of the instruction conditioned on the first branching condition.

7 . The computer-implemented method of claim 1 further comprising: upon reaching the branching node, dynamically determining to perform sequential symbolic execution of the alternative branches.

8 . The computer-implemented method of claim 7 , wherein said dynamically determining comprises determining that the first branch and the second branch are feasible according to the first symbolic state.

9 . The computer-implemented method of claim 1 further comprises: detecting the joining node, wherein said detecting comprises identifying a cut in a subset of the CFG beginning in the branching node that has a cut size of one.

10 . The computer-implemented method of claim 1 , wherein the symbolic execution of the computer program is a concolic execution of the computer program comprising a symbolic state and a concrete state.

11 . An apparatus for performing symbolic execution of a computer program, wherein the symbolic execution traverses a Control Flow Graph (CFG) of the computer program while updating a symbolic state of the computer program, wherein the apparatus comprising a processor being adapted to perform the steps of:
reaching a branching node in the CFG with a first symbolic state, wherein the branching has at least a first branch and a second branch, wherein the first and second branches end at a joining node in the CFG; symbolically executing the first branch using the first symbolic state, whereby a second symbolic state is determined; and symbolically executing the second branch using the second symbolic state, whereby a third symbolic state is determined, the third symbolic state is based on sequential symbolic execution of alternative branches.

12 . The apparatus of claim 11 , wherein the first branch comprises an assignment instruction, wherein the first branch is taken under a first branching condition, wherein said symbolically executing the first branch comprises updating the first symbolic state to reflect a conditional assignment in accordance with the assignment instruction that is conditioned on the first branching condition.

13 . The apparatus of claim 12 , wherein the assignment instruction is an assignment instruction to a variable having a definition scope that extends beyond the first branch.

14 . The apparatus of claim 12 , wherein the first branch comprises a second assignment instruction to a local variable, wherein the local variable having a definition scope that is internal to the first branch, wherein said symbolically executing the first branch comprises updating the first symbolic state to reflect an unconditional assignment in accordance with the second assignment instruction.

15 . The apparatus of claim 12 , wherein the second branch comprises a second assignment instruction, wherein the second branch is taken under a second branching condition, wherein said symbolically executing the second branch comprises updating the second symbolic state to reflect a conditional assignment in accordance with the second assignment instruction that is conditioned on the second branching condition.

16 . The apparatus of claim 11 , wherein the first branch comprises an instruction having a side effect external to the first branch, wherein the first branch is taken under a first branching condition, wherein said symbolically executing the first branch comprises updating the first symbolic state to reflect execution of the instruction conditioned on the first branching condition.

17 . The apparatus of claim 11 , wherein said processor is further adapted to perform: upon the symbolic execution reaching the branching node, dynamically determining to perform sequential symbolic execution of the alternative branches.

18 . The apparatus of claim 17 , wherein said dynamically determining comprises determining that the first branch and the second branch are feasible according to the first symbolic state.

19 . The apparatus of claim 11 , wherein the symbolic execution of the computer program is a concolic execution of the computer program comprising a symbolic state and a concrete state.

20 . A computer program product for performing symbolic execution of a computer program, wherein the symbolic execution traverses a Control Flow Graph (CFG) of the computer program while updating a symbolic state of the computer program, wherein the computer program product comprising a computer readable storage medium retaining program instructions, which program instructions when read by a processor, cause the processor to perform a method comprising:
reaching a branching node in the CFG with a first symbolic state, wherein the branching has at least a first branch and a second branch, wherein the first and second branches end at a joining node in the CFG; symbolically executing the first branch using the first symbolic state, whereby a second symbolic state is det

Assignees

• IBM

Inventors

• Pidan Dmitry
• Veksler Tatyana

Classifications

• G06F11/3668 Primary

  Testing of software · CPC title

• G06F11/3608

  using formal methods, e.g. model checking, abstract interpretation (theorem proving G06N5/013) · CPC title

• G06F11/3688 Primary

  for test execution, e.g. scheduling of test suites · CPC title