JP6079201B2 - Symbolic execution method, symbolic execution program, and symbolic execution device - Google Patents

Description

  The present invention relates to a symbolic execution technique.

  Symbolic execution is a technique for executing a program by converting variables into symbols (that is, with symbols) without embodying variables in the program. Variables that are symbolized are called symbol variables. During symbolic execution, not a specific value but a condition to be satisfied by a symbol variable (hereinafter referred to as a path condition) is held in a memory or the like as a symbol variable value. When the symbolic execution is completed, a path condition is obtained for each path in the program. Therefore, test data for testing the program can be obtained by obtaining a specific value of the symbol variable that satisfies the path condition.

  For example, consider performing symbolic execution on a program having the control structure shown in FIG. This control structure includes two branches. The first branch is a branch for determining whether or not the symbol variable b is 0. When the symbol variable b is 0, the process proceeds to the path 11, and when it is not 0, the process proceeds to the path 12. The second branch is a branch for determining whether or not the symbol variable b is 5 or less. If the symbol variable b is 5 or less, the process proceeds to the path 21 for decrementing the variable a. Proceed to path 22 for incrementing.

  FIG. 2 shows an example of a program having the control structure shown in FIG. In this program, “@Symbolic (“ true ”)” on the first line indicates that symbolic execution is performed. When symbolic execution is actually performed on this program, test data of b = 0 (pass condition is (b = 0) ∧ (b ≦ 5)) and test data of b = 1 (pass condition is (b ≠ 0) ∧ (b ≦ 5)) and test data b = 6 (pass condition is (b ≠ 0) ∧ (b> 5)).

  Here, the control structure shown in FIG. 1 is changed as shown in FIG. In the control structure shown in FIG. 3, the first branch is the same as in FIG. A process of outputting the value of the symbol variable b to a file named “Test.txt” between the first branch and the second branch, and reading the value from the file named “Test.txt” Processing. In the second branch, if the value read from the file is 5 or less, the process proceeds to the path 21 for decrementing the variable a, and if it is greater than 5, the process proceeds to the path 22 for incrementing the variable a.

  FIG. 4 shows an example of a program having the control structure shown in FIG. This program is a program obtained by adding five lines of code surrounded by a dotted line to the program shown in FIG. When symbolic execution is actually performed on this program, test data of b = 0 (pass condition is (b = 0)) and test data of b = 1 (pass condition is (b ≠ 0)) are obtained. be able to. This test data is different from the test data obtained in the example of FIG.

  Thus, if the value of the symbol variable is made permanent in the middle of the program, appropriate test data may not be obtained. This is because symbol variables disappear due to persistence. In the example of FIG. 4, since the value read from the file by the instruction “dis.readInt ()” is not recognized as the value of the symbol variable b and the symbol variable b disappears, the symbol variable b is set for symbolic execution. I can't take over. Such a problem is not examined in the conventional technique regarding symbolic execution.

JP 2012-68869 A

  In one aspect, an object of the present invention is to provide a technique for enabling symbolic execution even when the value of a symbol variable is made permanent.

  In the symbolic execution method according to the present invention, when executing a write command instructing to write the first data including the value of the symbol variable to the file, the first data is written to the file according to the write command, and the internal representation When the value of the symbol variable is stored in the storage device and the read command for instructing to read the first data from the file is executed, the value of the symbol variable of the internal representation is read from the storage device, and the value of the symbol variable of the internal representation Includes a process of setting the first data including the value to the return value of the read command.

  Symbolic execution can be performed even when the value of a symbol variable is made persistent.

FIG. 1 is a diagram showing a control structure of a program. FIG. 2 is a diagram illustrating an example of a program. FIG. 3 is a diagram showing a control structure of the program. FIG. 4 is a diagram illustrating an example of a program. FIG. 5 is a functional block diagram of the information processing apparatus according to this embodiment. FIG. 6 is a diagram illustrating a processing flow of processing executed when writing to a file. FIG. 7 is a diagram illustrating an example of data stored in the symbol variable storage unit. FIG. 8 is a diagram illustrating an example of data stored in the symbol value storage unit. FIG. 9 is a diagram illustrating an example of data stored in the file storage unit. FIG. 10 is a diagram illustrating a processing flow of processing executed when reading from a file. FIG. 11 is a functional block diagram of a computer.

  FIG. 5 shows a functional block diagram of the information processing apparatus 1 in the present embodiment. The information processing apparatus 1 includes a target class storage unit 110 that stores a target class that is a target of symbolic execution, and a symbolic execution unit that includes a model class group 101, a determination unit 102, a symbol variable storage unit 104, and an execution engine 103. 100, an input / output processing unit 105 including a first processing unit 106 and a second processing unit 107, a symbol value storage unit 109, and a file storage unit 108.

  The execution engine 103 is a module that performs symbolic execution, and is, for example, Java (registered trademark) PathFinder. The execution engine 103 manages symbol variables in symbolic execution using the symbol variable storage unit 104.

  The model class group 101 includes a plurality of model classes. The model class is a class for executing processing such as writing data to a file or reading data from a file, and is called from the target class.

  When a model class for executing writing of data to a file or reading of data from a file in the model class group 101 is called, the determination unit 102 is called from the model class. The determination unit 102 uses the data stored in the symbol variable storage unit 104 to determine whether or not a symbol variable is included in the output data. If it is included, the data related to the write method is input. The data is output to the output processing unit 105. In addition, the determination unit 102 determines whether the information of the file to be read is stored in the symbol value storage unit 109, and outputs the data related to the read method to the input / output processing unit 105 if stored.

  The first processing unit 106 in the input / output processing unit 105 performs processing using data related to the write method received from the determination unit 102. The second processing unit 107 in the input / output processing unit 105 performs processing using the data related to the reading method received from the determination unit 102.

  Next, the operation of the information processing apparatus 1 will be described with reference to FIGS. First, processing executed when writing to a file will be described with reference to FIGS.

  When the execution engine 103 in the symbolic execution unit 100 receives an instruction from the user, the execution engine 103 starts symbolic execution using the target class stored in the target class storage unit 110. During symbolic execution, the execution engine 103 executes a file write command (for example, dos.writeInt (b) in the example of FIG. 4) (FIG. 6: step S1). In the case of Java (registered trademark), the file write command is a command including, for example, writeInt, writeChar, or writeLong.

  When the execution engine 103 executes a write command to a file, a model class that executes a write method is called from the model class group 101. The called model class calls the determination unit 102 (step S3), and outputs data related to the write method to the determination unit 102. This process is realized, for example, by providing a part for calling the determination unit 102 in the model class “DataOutputStream”, in addition to the part for executing the write method. Note that the data related to the write method includes output data, file name, write start position information, output data length information, type information, and the like.

  The determination unit 102 determines whether the symbol variable stored in the symbol variable storage unit 104 is included in the output data (step S5).

  FIG. 7 shows an example of data stored in the symbol variable storage unit 104. In the example of FIG. 7, symbol variables and variable types are stored. For example, in the case of the program shown in FIG. 4, since the first two lines correspond to the part defining the symbol variable, when this part is executed, data as shown in FIG. 7 is stored.

  For example, if the write method is writeInt (b), b is output data, but b is registered in the symbol variable storage unit 104 as a symbol variable, so that the symbol variable is included in the output data.

  If the symbol variable is not included in the output data (step S7: No route), since it is a normal writing method, the process proceeds to step S9. Then, the model class that executes the write method writes the output data to the file in the file storage unit 108 according to the data related to the write method (step S9).

  On the other hand, when the symbol variable is included in the output data (step S <b> 7: Yes route), the determination unit 102 outputs the data related to the write method to the input / output processing unit 105. Then, the first processing unit 106 in the input / output processing unit 105 acquires the value of the symbol variable of the internal representation from the memory area used by the execution engine 103 (step S11). The value of the symbol variable in the internal representation includes the path condition stored in the memory area at the time of step S11.

  The first processing unit 106 adds the file information included in the data related to the write method and the value of the acquired symbol variable of the internal representation to the symbol value storage unit 109 (step S13).

  FIG. 8 shows an example of data stored in the symbol value storage unit 109. In the example of FIG. 8, the file name, the information of the write start position and the information of the output data length, and the value of the symbol variable in the internal representation are stored.

  The first processing unit 106 writes the output data to the file in the file storage unit 108 according to the data related to the write method received from the determination unit 102 (step S15). Then, the process ends.

  FIG. 9 shows an example of a file stored in the file storage unit 108. The file shown in FIG. 9 has a file name “Test.txt” and output data “0”. The value of the symbol variable b in the internal representation is the value shown in the third column of the second row in FIG. 8, but is “0” because it is represented by an integer type (Int) on the file.

  By executing the processing as described above, the output data at the time of writing to the file can be saved, so that it can be used later when reading from the file.

  Next, processing executed when reading from a file will be described with reference to FIG.

  When the execution engine 103 in the symbolic execution unit 100 receives an instruction from the user, the execution engine 103 starts symbolic execution using the target class stored in the target class storage unit 110. During symbolic execution, the execution engine 103 executes a file read command (for example, dis.readInt () in the example of FIG. 4) (FIG. 10: Step S21). In the case of Java (registered trademark), the file read command is a command including, for example, readInt, readChar, or readLong.

  When the execution engine 103 executes a file read instruction, a model class that executes a read method is called from the model class group 101. In addition, the called model class calls the determination unit 102 (step S23), and outputs data related to the read method to the determination unit 102. For example, it is realized by providing a part for calling the determination unit 102 in the model class “DataInputStream” in addition to the part for executing the reading method. Note that the data related to the reading method includes a file name, reading start position information, data length information, type information, and the like.

  The determination unit 102 determines whether the information of the file to be read (here, the file name, the read start position information, and the data length information) is stored in the symbol value storage unit 109 (step S25).

  If it is not stored (step S27: No route), since it is a normal reading method, the model class that executes the reading method reads data from the file in the file storage unit 108 according to the data related to the reading method. Then, the model class that executes the reading method sets the data read from the file as the return value of the reading method (step S29).

  On the other hand, if it is stored (step S <b> 27: Yes route), the determination unit 102 outputs data related to the read method to the input / output processing unit 105. Then, the second processing unit 107 in the input / output processing unit 105 acquires the value of the symbol variable of the internal representation corresponding to the information of the file to be read from the symbol value storage unit 109 (step S31). The value of the symbol variable in the internal representation stored in the symbol value storage unit 109 includes the path condition stored in the memory area at the time of writing.

  The second processing unit 107 generates a setting value that includes the value of the symbol variable of the acquired internal representation (step S33). For example, in the command writeInt (b), since the output data itself is a symbol variable, the processing in step S33 may be skipped. On the other hand, when a symbol variable is included in part of the output data, the process of step S33 is executed. Then, the second processing unit 107 outputs the generated setting value to the determination unit 102.

  The determination unit 102 sets the setting value received from the second processing unit 107 as the return value of the reading method (step S35). For example, the second processing unit 107 sets Symbolic Exp [(s_b_3_SYMINT_STATIC_FIELD + CONST_1)] as a return value. Then, the process ends. As a result, the value of the symbol variable can be taken over by the execution engine 103.

  By executing the above process, the symbol variable value of the internal representation can be taken over by symbolic execution instead of the value on the file, so symbolic execution can be performed even if the value of the symbol variable is made permanent. You can do it.

  Although one embodiment of the present invention has been described above, the present invention is not limited to this. For example, the functional block configuration of the information processing apparatus 1 described above may not correspond to the actual program module configuration.

  Further, the configuration of each table described above is an example, and the configuration as described above is not necessarily required. Further, in the processing flow, the processing order can be changed if the processing result does not change. Further, it may be executed in parallel.

  For example, while a Java (registered trademark) program has been described above as an example, a program of another programming language may be used.

  The information processing apparatus 1 described above is a computer apparatus, and as shown in FIG. 11, a memory 2501, a CPU (Central Processing Unit) 2503, a hard disk drive (HDD: Hard Disk Drive) 2505, and a display device. A display control unit 2507 connected to 2509, a drive device 2513 for the removable disk 2511, an input device 2515, and a communication control unit 2517 for connecting to a network are connected by a bus 2519. An operating system (OS) and an application program for executing the processing in this embodiment are stored in the HDD 2505, and are read from the HDD 2505 to the memory 2501 when executed by the CPU 2503. The CPU 2503 controls the display control unit 2507, the communication control unit 2517, and the drive device 2513 according to the processing content of the application program, and performs a predetermined operation. Further, data in the middle of processing is mainly stored in the memory 2501, but may be stored in the HDD 2505. In the embodiment of the present invention, an application program for performing the above-described processing is stored in a computer-readable removable disk 2511 and distributed, and installed in the HDD 2505 from the drive device 2513. In some cases, the HDD 2505 may be installed via a network such as the Internet and the communication control unit 2517. Such a computer apparatus realizes various functions as described above by organically cooperating hardware such as the CPU 2503 and the memory 2501 described above and programs such as the OS and application programs. .

  The embodiment of the present invention described above is summarized as follows.

  In the symbolic execution method according to the present embodiment, (A) when executing a write command instructing to write the first data including the value of the symbol variable to the file, the first data is written to the file according to the write command. At the same time, the value of the symbol variable of the internal representation is stored in the storage device, and (B) the value of the symbol variable of the internal representation is read from the storage device when executing a read command that instructs to read the first data from the file. The first data including the value of the symbol variable of the internal representation is set as the return value of the read instruction.

  In this way, the value of the symbol variable in the internal representation instead of the value of the symbol variable on the file can be inherited to the symbolic execution, so the symbolic execution can be performed even if the value of the symbol variable is made permanent. It becomes like this.

  When the symbolic execution method executes (C) a second read instruction for instructing to read second data not including the value of the symbol variable from a second file other than the above file, A process of reading the second data from the second file in accordance with the second read command and setting the return value of the second read command may be further included. In this way, when data including no symbol variable value is read from a file, it can be read as usual.

  In the process of storing the value of the symbol variable of the internal representation described above in the storage device, (a1) the information of the file to which the first data is written is associated with the symbol variable of the internal representation and stored in the storage device. In the process of setting the return value of the read command described above, (b1) The value of the symbol variable of the internal representation stored in association with the file information specified in the read command is read from the storage device. You may do it. In this way, for example, even when handling a plurality of symbol variables, an appropriate value can be read from the storage device.

  A program for causing a computer to perform the processing according to the above method can be created. The program can be a computer-readable storage medium such as a flexible disk, a CD-ROM, a magneto-optical disk, a semiconductor memory, or a hard disk. It is stored in a storage device. The intermediate processing result is temporarily stored in a storage device such as a main memory.

  The following supplementary notes are further disclosed with respect to the embodiments including the above examples.

(Appendix 1)
When executing a write command for instructing to write first data including a value of a symbol variable to a file, the first data is written to the file according to the write command, and the value of the symbol variable of an internal representation is set Stored in a storage device,
When executing a read instruction for instructing to read the first data from the file, the value of the symbol variable of the internal representation is read from the storage device, and the value of the symbol variable of the internal representation is included. A symbolic execution method in which a computer executes processing for setting data as a return value of the read instruction.

(Appendix 2)
When executing a second read instruction that instructs to read second data that does not include the value of the symbol variable from a second file that is a file other than the file, the second read instruction is executed according to the second read instruction. The symbolic execution method according to appendix 1, wherein the computer further executes a process of reading the data from the second file and setting the return value of the second read instruction.

(Appendix 3)
In the process of storing the value of the symbol variable of the internal representation in a storage device,
Storing the information of the file in which the first data is written in the storage device in association with the symbol variable of the internal representation;
In the process of setting the return value of the read instruction,
The symbolic execution method according to claim 1, wherein the value of the symbol variable of the internal representation stored in association with the file information specified in the read instruction is read from the storage device.

(Appendix 4)
When executing a write command for instructing to write first data including a value of a symbol variable to a file, the first data is written to the file according to the write command, and the value of the symbol variable of an internal representation is set Stored in a storage device,
When executing a read instruction for instructing to read the first data from the file, the value of the symbol variable of the internal representation is read from the storage device, and the value of the symbol variable of the internal representation is included. A symbolic execution program for causing a computer to execute processing for setting data as a return value of the read instruction.

(Appendix 5)
When executing a write command for instructing to write first data including a value of a symbol variable to a file, the first data is written to the file according to the write command, and the value of the symbol variable of an internal representation is set A write processing unit to be stored in the storage device;
A read processing unit that reads a value of a symbol variable of the internal representation from the storage device when executing a read command for instructing to read the first data from the file;
A symbolic execution device comprising: a setting unit configured to set the first data including the value of the symbol variable of the internal representation read by the read processing unit as a return value of the read command.

DESCRIPTION OF SYMBOLS 1 Information processing apparatus 100 Symbolic execution apparatus 101 Model class group 102 Judgment part 103 Execution engine 104 Symbol variable storage part 105 Input / output processing part 106 1st process part 107 2nd process part 108 File storage part 109 Symbol value storage part 110 Target class Storage

Claims (5)

When executing a write command for instructing to write first data including a value of a symbol variable to a file, the first data is written to the file according to the write command, and the value of the symbol variable of an internal representation is set Stored in a storage device,
When executing a read instruction that instructs the reading the first data from the file, reads the value of the symbol variable internal representation from the storage device, the second containing the value of the symbol variable internal representation A symbolic execution method in which a computer executes a process of generating the first data based on the first data and setting the second data as a return value of the read instruction. When executing the second read instruction to instruction to read the third data not including the value of the symbol variable from the second file is a file other than the file, the third according to the second read instruction The symbolic execution method according to claim 1, wherein the computer further executes a process of reading the data from the second file and setting a return value of the second read instruction. The value of the symbol variable internal representation in the process of storing in the storage device,
In association with information of the files that the first data is written to the value of the symbol variable internal representation and stored in the storage device,
In the process of setting the second data as a return value of the read command,
The value of the symbol variable internal representation which is stored in association with the information of the file specified in the read command, the symbolic execution method according to claim 1, wherein the reading from the storage device. When executing a write command for instructing to write first data including a value of a symbol variable to a file, the first data is written to the file according to the write command, and the value of the symbol variable of an internal representation is set Stored in a storage device,
When executing a read instruction that instructs the reading the first data from the file, reads the value of the symbol variable internal representation from the storage device, the second containing the value of the symbol variable internal representation A symbolic execution program for causing a computer to execute the process of generating the data based on the first data and setting the second data as a return value of the read instruction. When executing a write command for instructing to write first data including a value of a symbol variable to a file, the first data is written to the file according to the write command, and the value of the symbol variable of an internal representation is set A write processing unit to be stored in the storage device;
When executing a read instruction that instructs the reading the first data from the file, and the read processing unit to read the value of the symbol variable internal representation from the storage device,
Setting said second data including a value of the symbol variable internal representations read by read processing unit generates, based on the first data, setting the second data to the return value of the read instruction And a symbolic execution device.

Images