JP6659955B2 - Program analysis method, program analysis device, and analysis program - Google Patents

Description

  The present invention relates to a program analysis method, a program analysis device, and an analysis program.

  When a program includes a conditional branch statement, a sequence of instructions to be executed (execution path) changes according to an input to the program. Therefore, the created program may be analyzed to extract an execution path from the program. For example, when modifying or exchanging an existing information processing system, there may be cases where sufficient design materials created at the beginning of the development of the information processing system do not remain. In this case, the specification of the information processing system may be understood by extracting an execution path from a program as an implementation and determining the relationship between input and output for each execution path. Further, for example, when testing a created program, an execution path may be extracted from the program, and a test plan may be created for the extracted execution path.

  One of the program analysis methods is symbolic execution (symbol execution). In symbolic execution, a symbol (symbol value) indicating a constant is assigned to a variable that stores an input value to a program, instead of a specific numerical value or a specific character. The value of a variable that is updated in a program may be represented as an expression that includes a symbol. By pseudo-executing the program instructions using the symbols, the execution path of the program can be extracted more efficiently than when the program is repeatedly executed by inputting specific values one after another.

  When a program includes a conditional branch statement, the symbol represents an arbitrary constant, and thus the branch direction may not be narrowed down to one. When the determination of the branch condition may be YES or NO depending on the specific value, the execution path is divided using the conditional branch statement as a division point. That is, both the execution path when the determination of the branch condition is YES and the execution path when the determination of the branch condition is NO exist. As the number of conditional branch statements increases, the number of execution paths extracted from the program often increases exponentially.

  Note that a test data generation device that extracts an execution path from a program using symbolic execution and generates test data that covers the extracted execution path has been proposed. The proposed test data generation device assigns a symbol to only some of a plurality of variables and assigns a specific value other than a symbol to other variables in order to reduce the amount of calculation for symbolic execution. When symbolic execution is performed using a combination of a symbol and a specific value, a part of the plurality of execution paths included in the program is extracted. The test data generation device extracts all execution paths to be tested from the program by repeating symbolic execution while switching variables to which symbols are assigned.

  In addition, a software test method for searching for an execution path inside a function using symbolic execution has been proposed. In the proposed software test method, a symbol is assigned to a return value of a function, a constraint indicating a range of possible values of the symbol is derived, and the execution path searched is limited by performing symbol execution on the function so as to satisfy the constraint. .

JP 2014-153908 A JP-A-2006-12343

  In a program, one module may call another module. The module may be a partial program included in the program, such as a function, procedure, method section, or the like, as long as it is sometimes called from another module. In this case, the problem is how to analyze the program and extract the execution path.

If an attempt is made to directly extract an execution path that extends over both the caller module and the callee module, a path explosion problem arises in that the number of execution paths to be searched becomes enormous. For example, if the caller module contains N serial conditional branch statements executed once each, and the callee module contains M serial conditional branch statements executed once each, (N and M are integers of 2 or more). In that case, at most 2 ^{M + N} execution paths are extracted from the two modules. If ^{2M + N} execution paths are to be searched directly, the amount of calculation greatly increases as the number (N or M) of conditional branch statements of each module increases.

  On the other hand, just extracting the execution path independently for each module does not mean that the calling module has been correctly analyzed. This is because the instruction executed by the calling module after calling another module depends on the execution result of the called module.

  In one aspect, an object of the present invention is to provide a program analysis method, a program analysis device, and an analysis program capable of efficiently analyzing a program execution path.

  In one aspect, a computer-executable program analysis method is provided. The first module acquires a program including a call instruction for calling the second module, the program including a first module and a second module. A first symbol is assigned to an input of the first module, first information representing a first processing result before the call instruction is represented using the first symbol, and a second information is generated as a call result of the call instruction. , And generates second information indicating the second processing result after the call instruction of each of the plurality of first execution paths included in the first module by using the second symbol. A third symbol is assigned to the input of the second module, and third information representing a third processing result of each of the plurality of second execution paths included in the second module using the third symbol is represented by: Generate. The first processing result indicated by the first information is associated with the third symbol used for the third information, and the third processing result indicated by the third information is used for the second information. By using the first symbol, a processing result of each of a plurality of combined execution paths obtained by combining the plurality of first execution paths and the plurality of second execution paths by associating the plurality of first execution paths with the plurality of second execution paths. Generate information.

  In one aspect, a program analysis device having a storage unit and a calculation unit is provided. In one aspect, an analysis program to be executed by a computer is provided.

  In one aspect, the execution path of a program can be analyzed efficiently.

FIG. 1 is a diagram illustrating an example of a program analysis device according to a first embodiment. FIG. 3 is a block diagram illustrating an example of hardware of a program analysis device. FIG. 6 is a diagram illustrating a first example of a program. FIG. 4 is a diagram illustrating a first example of a logic table. FIG. 9 is a diagram illustrating a second example of the program. FIG. 9 is a diagram illustrating a second example of the logic table. It is a figure showing an example of division of symbolic execution, and combination of partial logic. FIG. 14 is a diagram illustrating an example of an update variable table and a symbol assignment table. It is a figure showing an example of extraction of a hierarchical update variable. It is a figure showing an example of a logic table of an intermediate point, a call destination, and an end point. It is a figure which shows the example of simplification of partial logic. It is a figure showing the example of combination of partial logic. FIG. 14 is a diagram (continuation) illustrating an example of combining partial logics; FIG. 14 is a diagram illustrating a third example of the program. It is a block diagram showing an example of a function of a program analysis device. It is a flowchart which shows the example of a procedure of a program analysis. It is a flowchart which shows the example of a procedure of update variable extraction. It is a flowchart which shows the example of a procedure of symbolic execution. It is a flowchart (continuation) which shows the example of a procedure of symbolic execution. 9 is a flowchart illustrating an example of a procedure for simplifying logic. It is a flowchart which shows the example of a procedure of a logic connection.

Hereinafter, the present embodiment will be described with reference to the drawings.
[First Embodiment]
A first embodiment will be described.

FIG. 1 is a diagram illustrating an example of a program analysis device according to the first embodiment.
The program analyzer 10 according to the first embodiment analyzes a program by symbolic execution and extracts an execution path from the program. The program to be analyzed may be a source code described in a programming language, or may be something other than the source code such as an executable object code. For example, the program analyzer 10 can be used when extracting an execution path from a program created in the past for the purpose of understanding the specifications of an existing information processing system. Further, for example, the program analyzer 10 can be used to extract an execution path to be tested from a newly created program for the purpose of testing an information processing system to be newly constructed.

The program analyzer 10 may be a client computer or a server computer. The program analysis device 10 has a storage unit 11 and a calculation unit 12.
The storage unit 11 stores a program 20 to be analyzed. The storage unit 11 may be a volatile semiconductor memory such as a RAM (Random Access Memory) or a non-volatile storage device such as a HDD (Hard Disk Drive) or a flash memory.

  The operation unit 12 analyzes an execution path included in the program 20 stored in the storage unit 11. The calculation unit 12 may be a processor such as a CPU (Central Processing Unit) or a DSP (Digital Signal Processor). The arithmetic unit 12 may include an electronic circuit for a specific use such as an ASIC (Application Specific Integrated Circuit) or an FPGA (Field Programmable Gate Array). The processor executes a program stored in a memory such as a RAM (or the storage unit 11). The program executed by the processor includes an analysis program describing the processing described below. A set of multiple processors may be referred to as a “multiprocessor” or simply “processor”.

  The program 20 includes a module 21 (first module) and a module 26 (second module). The modules 21 and 26 may be partial programs included in the program 20 and may be called from other modules. For example, the modules 21 and 26 include functions, procedures, method sections, and the like. The name of each module depends on the programming language.

  Module 21 includes a call instruction 22 that calls module 26. Module 21 is a calling module, and module 26 is a called module. An example of the call instruction 22 is a PERFORM statement that calls another section.

  The arithmetic unit 12 performs symbolic execution on the module 21. At this time, the calculation unit 12 assigns the symbol c1 (first symbol) to the input of the module 21. For example, the calculation unit 12 assigns the symbol c1 to a variable that stores a value provided from outside the module 21 among the variables used in the module 21.

  The operation unit 12 generates first information 24 representing the processing result (first processing result) before the calling instruction 22 using the symbol c1. The first information 24 is, for example, a value of a variable used before the call instruction 22 among variables used in the module 21 that is represented by an expression including the symbol c1. The first information 24 can be generated, for example, by symbolically executing instructions up to the call instruction 22 using the symbol c1 in a pseudo manner. As an example, the first information 24 indicates a processing result that the value of the variable x immediately before the call instruction 22 is c1 + 1.

  The operation unit 12 assigns a symbol c2 (second symbol) independent of the symbol c1 to the call result of the call instruction 22. As a result, the module 26 is stubbed, and the module 21 can be symbolically executed independently of the module 26. For example, the calculation unit 12 assigns the symbol c2 to a variable that may be updated by the module 26 among the variables used in the module 21. As an example, the calculation unit 12 assigns the symbol c2 to the variable y updated by the module 21.

  The call instruction 22 may be described in a form that does not explicitly indicate the operation of the module 26. For example, a case where a variable that stores a value to be updated by the module 26 is not specified in the module 21, such as a case where the module 26 updates a global variable. In this case, for example, the calculation unit 12 searches the module 26 for an update variable that is likely to be updated by the module 26 among the variables used in the module 21.

  The calculation unit 12 detects a plurality of first execution paths including the first execution paths 23a and 23b from the module 21. The plurality of first execution paths are branched by one or more conditional branch instructions included in the module 21. The conditional branch instruction may exist before the call instruction 22 or may exist after the call instruction 22.

  The calculation unit 12 generates second information 25 that represents a processing result (second processing result) after the call instruction 22 of each of the plurality of first execution paths using the symbol c2. The second information 25 is, for example, a value of a variable updated after the call instruction 22 among the variables used in the module 21, represented by an expression including the symbol c2. The expression may further include the symbol c1. The second information 25 can be generated, for example, by symbolically executing the instruction subsequent to the call instruction 22 using the symbol c2 in a pseudo manner.

  The processing result indicated by the second information 25 may be different depending on the first execution path. As an example, the second information 25 indicates a processing result that the value of the variable z at the end point of the first execution path 23a is c2 + 3. Further, the second information 25 indicates a processing result that the value of the variable z at the end point of the first execution path 23b is c2-3. When a conditional branch instruction is present before the call instruction 22, the processing result indicated by the first information 24 may be different depending on the first execution path as in the case of the second information 25.

  In addition, the arithmetic unit 12 performs symbolic execution on the module 26 independently of the module 21. The symbolic execution of the module 26 may be performed before the symbolic execution of the module 21 or may be performed after the symbolic execution of the module 21. Further, the symbolic execution of the module 26 may be performed between the symbolic execution before the call instruction 22 and the symbolic execution after the call instruction 22.

  At this time, the calculation unit 12 assigns a symbol c3 (third symbol) independent of the symbols c1 and c2 to the input of the module 26. For example, the calculation unit 12 assigns the symbol c3 to a variable that stores a value provided from outside the module 26 among the variables used in the module 26. The calculation unit 12 detects a plurality of second execution paths including the second execution paths 27a and 27b from the module 26. The plurality of second execution paths are branched by one or more conditional branch instructions included in the module 26.

  The calculation unit 12 generates third information 28 representing the processing result (third processing result) of each of the plurality of second execution paths using the symbol c3. The third information 28 is, for example, a value of a variable updated in the module 26 among variables used in the module 26, which is represented by an expression including the symbol c3. The third information 28 can be generated, for example, by symbolically executing the instructions of the module 26 in a pseudo manner using the symbol c3.

  The processing result indicated by the third information 28 may be different depending on the second execution path. As an example, the third information 28 indicates a processing result that the value of the variable y at the end point of the second execution path 27a is c3 + 2. Further, the third information 28 indicates a processing result that the value of the variable y at the end point of the second execution path 27b is c3-2. Although variables x, y, and z are used in FIG. 1, some or all of these variables may be the same.

  Then, the arithmetic unit 12 combines the plurality of first execution paths and the plurality of second execution paths, and generates a plurality of combined execution paths including the combined execution paths 31a, 31b, 31c, and 31d. The synthesis execution path is an execution path that extends over the modules 21 and 26, and is equivalent to an execution path obtained when an instruction in the module 26 is also executed following the instruction before the call instruction 22.

  At this time, the calculation unit 12 acquires the first information 24, the second information 25, and the third information 28. The calculation unit 12 associates the processing result indicated by the first information 24 with the symbol c3 used for the third information 28. This is because the processing result before the calling instruction 22 is used as an input to the module 26. For example, an expression indicating the value of the variable x is associated with the symbol c3. In addition, the calculation unit 12 associates the processing result indicated by the third information 28 with the symbol c2 used for the second information 25. This is because the processing result of the module 26 is used as an input of an instruction after the calling instruction 22. For example, an expression indicating the value of the variable y is associated with the symbol c2.

  The arithmetic unit 12 generates path information indicating the processing result of each of the plurality of combined execution paths by using the symbol c1 according to the first information 24, the second information 25, and the third information 28, and the above association. 32 is generated. The path information 32 expresses the relationship between the input and output of the module 21 for each synthesis execution path in consideration of the call instruction 22.

  As an example, the calculation unit 12 substitutes x = c1 + 1 indicated by the first information 24 into the symbol c3 of the third information 28. Thus, the processing result of the second execution path 27a is represented as y = c1 + 3, and the processing result of the second execution path 27b is represented as y = c1-1.

  Further, the calculation unit 12 substitutes the processing results of the second execution paths 27a and 27b into the symbol c2 of the second information 25. At this time, the operation unit 12 examines a combination of an arbitrary first execution path and an arbitrary second execution path. Here, the combined execution path 31a is generated by combining the first execution path 23a and the second execution path 27a. The first execution path 23a and the second execution path 27b are combined to generate a combined execution path 31b. A combined execution path 31c is generated by combining the first execution path 23b and the second execution path 27a. The combined execution path 31d is generated by combining the first execution path 23b and the second execution path 27b.

  The calculation unit 12 substitutes y = c1 + 3 of the second execution path 27a into a symbol c2 of z = c2 + 3 of the first execution path 23a. Thus, the processing result of the synthesis execution path 31a is expressed as z = c1 + 6. In addition, the calculation unit 12 substitutes y = c1-1 of the second execution path 27b into the symbol c2 of z = c2 + 3 of the first execution path 23a. Thus, the processing result of the synthesis execution path 31b is represented as z = c1 + 2. The calculation unit 12 substitutes y = c1 + 3 of the second execution path 27a for the symbol c2 of z = c2-3 of the first execution path 23b. Thus, the processing result of the synthesis execution path 31c is represented as z = c1. The calculation unit 12 substitutes y = c1-1 of the second execution path 27b for the symbol c2 of z = c2-3 of the first execution path 23b. Accordingly, the processing result of the synthesis execution path 31d is represented as z = c1-4.

  However, all of the combined execution paths obtained by combining the arbitrary first execution path and the arbitrary second execution path may not be valid execution paths actually executed in the program 20. In that case, the calculation unit 12 may select only a valid combination from all combinations between the plurality of first execution paths and the plurality of second execution paths.

  For example, the second information 25 may represent the execution condition (first execution condition) of each first execution path using at least one of the symbols c1 and c2. The execution condition of the first execution path can be determined from the branch condition of the conditional branch instruction included in the module 21. Further, the third information 28 may represent the execution condition (second execution condition) of each second execution path using the symbol c3. The execution condition of the second execution path can be determined from the branch condition of the conditional branch instruction included in the module 26.

  In this case, for example, when the execution condition of a certain first execution path and the execution condition of a certain second execution path do not contradict each other, the calculation unit 12 compares the first execution path and the second execution path. It is possible to determine that the combined execution path is valid. On the other hand, when the execution condition of a certain first execution path and the execution condition of a certain second execution path are inconsistent, the calculation unit 12 synthesizes the first execution path and the second execution path. The execution path can be determined to be invalid.

  According to the program analyzer 10 of the first embodiment, the symbolic execution of the module 21 and the symbolic execution of the module 26 are executed independently. The symbolic execution of the module 21 collects first information 24 before the call instruction 22 and second information 25 after the call instruction 22. The third information 28 is collected by the symbolic execution of the module 26. Then, based on the first information 24, the second information 25, and the third information 28, a plurality of first execution paths detected from the module 21 and a plurality of second execution paths detected from the module 26 Are synthesized.

Thus, it is possible to suppress a path explosion when analyzing an execution path extending over the modules 21 and 26, and to efficiently analyze the execution path of the program 20. For example, it is assumed that the module 21 includes N serial conditional branch instructions, and the module 26 includes M serial conditional branch instructions. When an execution path extending over the modules 21 and 26 is directly detected by symbolic execution, a maximum of 2 ^{M + N} execution paths are detected. On the other hand, according to the first embodiment, the maximum number of execution paths to be detected by symbolic execution is 2 ^M +2 ^N. For this reason, it is possible to reduce the calculation amount of symbolic execution.

  Further, in the first embodiment, the processing of the module 26 called from the module 21 is not ignored, and the second execution path detected from the module 26 is not ignored. Combined with the path. Therefore, the generated path information 32 can correctly represent the relationship between the input and the output of the module 21.

[Second embodiment]
Next, a second embodiment will be described.
The program analyzer according to the second embodiment extracts an execution path from a program by symbolic execution, and generates logic information indicating a relationship between an input and an output.

FIG. 2 is a block diagram illustrating an example of hardware of the program analysis device.
The program analyzer 100 includes a processor 101, a RAM 102, an HDD 103, an image signal processing unit 104, an input signal processing unit 105, a medium reader 106, and a communication interface 107. The above units of the program analyzer 100 are connected to the bus 108. Note that the program analyzer 100 corresponds to the program analyzer 10 of the first embodiment. The processor 101 corresponds to the calculation unit 12 according to the first embodiment. The RAM 102 or the HDD 103 corresponds to the storage unit 11 according to the first embodiment.

  The processor 101 is a processor including an arithmetic circuit that executes a program instruction. The processor 101 is, for example, a CPU. The processor 101 loads at least a part of the program and data stored in the HDD 103 into the RAM 102, and executes the loaded program. Note that the processor 101 may include a plurality of processor cores, or the program analyzer 100 may include a plurality of processors. The processing described below may be executed in parallel using a plurality of processors or processor cores.

  The RAM 102 is a volatile semiconductor memory that temporarily stores a program executed by the processor 101 and data used for calculation. Note that the program analysis device 100 may include a memory of a type other than the RAM, or may include a plurality of memories.

  The HDD 103 is a nonvolatile storage device that stores an OS (Operating System), software programs such as middleware and application software, and data. The program includes an analysis program. Note that the program analysis device 100 may include another type of storage device such as a flash memory or an SSD (Solid State Drive), or may include a plurality of nonvolatile storage devices.

  The image signal processing unit 104 outputs an image to a display 111 connected to the program analysis device 100 according to a command from the processor 101. As the display 111, any type of display such as a CRT (Cathode Ray Tube) display, a liquid crystal display (LCD), a plasma display, and an organic EL (OEL: Organic Electro-Luminescence) display can be used.

  The input signal processing unit 105 acquires an input signal from the input device 112 connected to the program analyzer 100 and outputs the signal to the processor 101. As the input device 112, a pointing device such as a mouse, a touch panel, a touch pad, and a trackball, a keyboard, a remote controller, and a button switch can be used. Further, a plurality of types of input devices may be connected to the program analyzer 100.

  The medium reader 106 is a reading device that reads programs and data recorded on the recording medium 113. As the recording medium 113, for example, a magnetic disk, an optical disk, a magneto-optical disk (MO: Magneto-Optical disk), a semiconductor memory, or the like can be used. Magnetic disks include a flexible disk (FD: Flexible Disk) and an HDD. The optical disc includes a CD (Compact Disc) and a DVD (Digital Versatile Disc).

  The medium reader 106 copies a program or data read from the recording medium 113 to another recording medium such as the RAM 102 or the HDD 103, for example. The read program is executed by the processor 101, for example. The recording medium 113 may be a portable recording medium, and may be used for distributing programs and data. Further, the recording medium 113 and the HDD 103 may be referred to as a computer-readable recording medium.

  The communication interface 107 is an interface that is connected to the network 114 and communicates with other devices via the network 114. The communication interface 107 may be a wired communication interface connected to a communication device such as a switch by a cable, or a wireless communication interface connected to a base station via a wireless link.

Next, analysis of a program by symbolic execution will be described.
FIG. 3 is a diagram illustrating a first example of the program.
The program 141 is an example of a program to be analyzed. The program 141 receives a character string of two characters as the value of the variable “sex” and outputs one character as the value of the variable “output”. The program 141 includes the first conditional branch statement on the 14th line, and the second conditional branch statement on the 19th line. In the conditional branch statement on the 14th line, it is determined whether the value of the variable “sex” is “male”. If the value of the variable “sex” is “male”, the value of the variable “output” is updated to “M”; otherwise, the value of the variable “output” is updated to “” (blank) . In the conditional branch statement on line 19, it is determined whether the value of the variable “sex” is “female”. If the value of the variable “sex” is “female”, the value of the variable “output” is updated to “F”; otherwise, the value of the variable “output” does not change. Then, the program 141 ends.

  The program 141 has three execution paths. One of these three execution paths is executed according to the value of the variable “sex”. When the value of the variable “sex” is “male”, the branch condition on the 14th line is determined as YES, and the branch condition on the 19th line is determined as NO. In this execution path, the value of the variable “output” is “M”. When the value of the variable “sex” is “female”, the branch condition on the 14th line is determined to be NO, and the branch condition on the 19th line is determined to be YES. In this execution path, the value of the variable “output” is “F”. When the value of the variable “sex” is neither “male” nor “female”, both the branch condition on the 14th line and the branch condition on the 19th line are determined to be NO. In this execution path, the value of the variable “output” is “” (blank).

  Since the program 141 includes two serial conditional branch statements, there are four execution path candidates if the contents of the branch conditions are ignored. However, since the value of the variable “sex” is “male” and the value of the variable “sex” is “female”, both the branch condition on the 14th line and the branch condition on the 19th line are changed. No determination is made of YES. Therefore, among the four execution path candidates, there are three effective execution paths that may be executed.

  In a conditional branch statement, when there is at least one variable value that satisfies a condition for proceeding in a certain branch direction (YES direction or NO direction), the branch direction may be referred to as “satisfiable”. On the other hand, when there is no value of a variable that satisfies the condition for proceeding in a certain branch direction, the branch direction may be referred to as “not satisfyable”.

  In the program 141, in the conditional branch statement on the 14th line, the value of the variable “sex” is not restricted, so that both branch directions can be satisfied. On the other hand, the satisfiability of the conditional branch statement in the 19th line depends on the branch direction selected in the conditional branch statement in the 14th line. When the YES direction on the 14th line is selected, the YES direction on the 19th line cannot be satisfied and only the NO direction can be satisfied. When the NO direction on the 14th line is selected, both branch directions on the 19th line can be satisfied. Therefore, it can be determined that there are three effective execution paths.

  Here, an example in which the program 141 is symbolically executed will be described. The program analyzer 100 assigns an abstract symbol (symbol value) indicating an arbitrary constant instead of a specific character to the variable “sex” indicating the input to the program 141. Here, the same “sex” as the variable name is used as a symbol. The program analysis device 100 executes the instructions of the program 141 in a pseudo manner using the symbols.

  There is no execution path branch from the start of the program 141 to before the conditional branch statement on the 14th line. At this point, there is no condition (path condition) for selecting the execution path of the conditional branch statement on the 14th line, and both branch directions can be satisfied. Therefore, the program analysis device 100 divides the execution path in the conditional branch statement on the 14th line and selects one of the execution paths. Here, it is assumed that the program analyzer 100 has selected an execution path in the YES direction.

  Next, regarding the conditional branch statement on the 19th line, the path condition at this point is that the symbol “sex” is “male”, so the YES direction cannot be satisfied and the NO direction can be satisfied. Therefore, the program analyzer 100 selects the NO direction. Thereafter, this first execution pass ends. The program analysis device 100 determines that the symbol “sex” is “male” and the symbol “sex” is not “female” as the path condition of the first execution pass. Further, the program analysis device 100 determines that the value of the variable “output” is “M” from the processing result (path output) of the first execution path.

  When the first execution path is completed, the program analysis device 100 returns to the nearest division point of the execution path and selects an unselected execution path. Here, the program analyzer 100 returns to the conditional branch statement on the 14th line and selects an execution path in the NO direction.

  Regarding the conditional branch statement on the 19th line, the path condition at this point is that the symbol “sex” is not “male”, so that both the YES direction and the NO direction can be satisfied. Therefore, the program analysis device 100 further divides the execution path in the conditional branch statement on the 19th line, and selects one execution path. Here, it is assumed that the program analyzer 100 has selected an execution path in the YES direction. Thereafter, this second execution pass ends. The program analysis device 100 determines that the symbol “sex” is not “male” and the symbol “sex” is “female” as the path condition of the second execution path. Further, the program analysis device 100 determines that the value of the variable “output” is “F” for the path output of the second execution path.

  When the second execution path is completed, the program analyzer 100 returns to the conditional branch statement on the 19th line and selects an execution path in the NO direction. Thereafter, this third execution pass ends. The program analysis device 100 determines that the symbol “sex” is not “male” and the symbol “sex” is not “female” as the path condition of the third execution path. Further, the program analyzer 100 determines that the value of the variable “output” is “” (blank) for the path output of the third execution path. Then, since there is no unselected execution path, the symbolic execution ends.

  The program analyzer 100 stores the path conditions at that time and the values of the variables at the division points of the execution path. When one execution path is completed and backtracked to the division point, the program analysis device 100 takes over the stored path condition and the value of each variable to execute another execution corresponding to the unselected branch direction. Continue searching for a path.

FIG. 4 is a diagram illustrating a first example of the logic table.
The program analyzer 100 generates the logic table 142 as a result of the symbolic execution of the program 141. The program analysis device 100 displays the generated logic table 142 on a display provided in the program analysis device 100.

  The logic table 142 shows a relationship (logic) between an input to the program 141 and an output from the program 141. The logic table 142 has items of a path number, a path condition, and a path output. The identification number of the execution path detected by the symbolic execution is described in the item of the path number. In the path condition item, an input condition for selecting an execution path is described. In the path output item, the value of an output variable at the end point of the execution path is described. Path conditions and path outputs may be represented using symbols.

  As described above, the pass condition of the first execution pass is that “sex is male” and “sex is not female”. This can be simplified as "sex is male". The path output of the first execution path is “output is M”. The pass condition of the second execution pass is that “sex is not male” and “sex is female”. This can be simplified as "sex is female". The path output of the second execution pass is "output is F". The pass condition of the third execution pass is that “sex is not male” and “sex is not female”. The path output of the third execution pass is "output is blank".

  It should be noted that a mathematical processing technique can be used to determine the satisfiability of the conditional branch statement and to simplify the path condition. The program analyzer 100 may use a SMT (Satisfiability Modulo Theories) solver or a SAT (Satisfiability) solver. The path condition can be simplified, for example, by solving an expression including the symbol for the symbol.

Next, a path explosion in symbolic execution will be described.
FIG. 5 is a diagram illustrating a second example of the program.
The program 121 is an example of an analysis target program different from the program 141. The program 121 receives a numerical value of three decimal digits or less as the value of “input 1”, and outputs a numerical value of three decimal digits or less as the value of “output 1”. The program 121 includes two modules, section A and section B. Further, the program 121 includes a variable “variable 1”. “Variable 1” is a global variable that can be referenced and updated from both section A and section B.

  The program 121 calls the section A by substituting the received value of “input 1” into “variable 1”. When the section A ends, the program 121 assigns the value of “variable 1” to “output 1”. Then, the processing of the program 121 ends.

  Section A contains conditional branch statements on lines 17 and 25, and a call statement for calling section B on line 23. Section A uses the value of “variable 1” given from the outside of section A. Section A increases the value of “variable 1” by 1 when the value of “variable 1” is greater than 10, and increases the value of “variable 1” by 1 when the value of “variable 1” is 10 or less. Decrease. Next, section A calls section B. The variable that stores the return value is not specified in the PERFORM statement that calls the section B. Therefore, whether or not the value of “variable 1” is updated by section B is unknown only from the statement of section A. That is, in the PERFORM statement, the effect of the called section is unknown. Thereafter, section A increases the value of “variable 1” by 3 when the value of “variable 1” is smaller than 30, and increases the value of “variable 1” when the value of “variable 1” is 30 or more. Is reduced by 3. Then, the processing of the section A ends.

  Section B includes a conditional branch statement on line 34. The section B uses the value of “variable 1” given from the outside of the section B. Section B increases the value of “variable 1” by 2 when the value of “variable 1” is larger than 20, and increases the value of “variable 1” by 2 when the value of “variable 1” is 20 or less. Decrease. Then, the processing of the section B ends.

  The program analysis device 100 can also limit the analysis range to be analyzed by symbolic execution to some modules in the program such as some sections instead of the entire program. Thereby, the calculation amount of symbolic execution can be reduced. The analysis range can be specified by the user of the program analysis device 100. Regarding the program 121, it is assumed that the section A is designated as an analysis range. However, here, it is assumed that the call destination of the section A also follows the execution path continuously.

  Section A contains two conditional branch statements, and section B contains one conditional branch statement. Therefore, there are eight execution path candidates that span section A and section B. However, as described below, there are four effective execution paths.

  The program analyzer 100 assigns the symbol “variable 1_A” to “variable 1” in which the input of section A is stored. Since the variable 1_A is not restricted on the 17th line, both of the two branch directions can be satisfied. The program analysis device 100 selects the YES direction and updates the value of “variable 1” to variable 1_A + 1. Next, in the 34th line, the path condition is that the variable 1_A is larger than 10, so that both of the two branch directions can be satisfied. The program analysis device 100 selects the YES direction and updates the value of “variable 1” to variable 1_A + 1 + 2 = variable 1_A + 3. Next, in the 25th line, the path condition is that the variable 1_A is larger than 10 and the variable 1_A + 1 is larger than 20, so that both of the two branch directions can be satisfied. The program analysis device 100 selects the YES direction and updates the value of “variable 1” to variable 1_A + 1 + 2 + 3 = variable 1_A + 6.

  Thus, the first execution pass ends. The path condition of the first execution path is that variable 1_A is larger than 10, variable 1_A + 1 is larger than 20, and variable 1_A + 1 + 2 is smaller than 30. That is, the path condition of the first execution path is that the variable 1_A is larger than 19 and smaller than 27. The path output of the first execution path is that the value of “variable 1” is variable 1_A + 6.

  Similarly, the program analysis device 100 detects the remaining three execution paths from the program 121. In the second execution pass, the YES direction on the 17th line, the YES direction on the 34th line, and the NO direction on the 25th line are selected. Therefore, the path condition of the second execution path is that the variable 1_A is larger than 10, the variable 1_A + 1 is larger than 20, and the variable 1_A + 1 + 2 is 30 or more. That is, the path condition of the second execution path is that the variable 1_A is 27 or more. The path output of the second execution pass is that the value of “variable 1” is variable 1_A + 1 + 2−3 = variable 1_A.

  In the third execution path, the YES direction on the 17th line, the NO direction on the 34th line, and the YES direction on the 25th line are selected. Therefore, the path condition of the third execution path is that the variable 1_A is larger than 10, the variable 1_A + 1 is 20 or smaller, and the variable 1_A + 1-2 is smaller than 30. That is, the path condition of the third execution path is that the variable 1_A is larger than 10 and equal to or smaller than 19. The path output of the third execution pass is that the value of “variable 1” is variable 1_A + 1−2 + 3 = variable 1_A + 2.

  In the fourth execution path, the NO direction on the 17th line, the NO direction on the 34th line, and the YES direction on the 25th line are selected. Therefore, the path condition of the fourth execution path is that the variable 1_A is 10 or less, the variable 1_A-1 is 20 or less, and the variable 1_A-1-2 is less than 30. That is, the path condition of the fourth execution path is that the variable 1_A is 10 or less. The path output of the fourth execution path is that the value of “variable 1” is variable 1_A-1-2 + 3 = variable 1_A. Other branch direction combinations are not satisfiable.

FIG. 6 is a diagram illustrating a second example of the logic table.
The program analyzer 100 generates the logic table 129 as a result of the symbolic execution. The program analysis device 100 displays the generated logic table 129 on a display provided in the program analysis device 100.

  The logic table 129 indicates a relationship between an input to the section A, which is an analysis range, and an output from the section A. The logic table 129 has items of a path number, a path condition, and a path output, similarly to the logic table 142. The logic of the four execution paths detected is described in the logic table 129. The path condition and the path output may be displayed in a simplified manner or may be displayed without being simplified. FIG. 6 shows both the path condition and the path output before the reduction and the path condition and the path output after the reduction.

  By the way, in the example of the symbolic execution described above, an execution path extending between the analysis range section A and the call destination section B is directly detected. However, in this symbolic execution method, there is a problem of a path explosion in which an execution path detected exponentially increases according to an increase in conditional branch statements. On the other hand, ignoring the call statement and analyzing only section A does not mean that the logic of section A has been correctly analyzed. This is because section B updates the value of “variable 1” used by section A. Therefore, the program analyzer 100 performs symbolic execution in the following manner.

FIG. 7 is a diagram illustrating an example of division of symbolic execution and combination of partial logic.
The program analyzer 100 divides the symbolic execution of the section A, which is the analysis range, and the symbolic execution of the section B, which is the call destination, and performs the division independently. When section A includes N conditional branch statements and section B includes M conditional branch statements, the computational complexity of symbolic execution without division is 2 ^{N + M.} On the other hand, the calculation amount of the divided symbolic execution is 2 ^N +2 ^M , which is smaller than that of the case without division. The program analysis device 100 subsequently couples the partial logic acquired by the symbolic execution of the section A and the partial logic acquired by the symbolic execution of the section B.

  Specifically, the program analysis device 100 assigns the symbol “X” to “variable 1” storing the input of the section A, and starts the symbolic execution of the section A. The program analysis device 100 stores the halfway point logic immediately before the call statement that calls the section B. Immediately before the call statement, a logic whose path output is variable 1 = X + 1 and a logic whose path output is variable 1 = X-1 are detected.

  Next, in the symbolic execution of the section A, the program analyzer 100 stubs the section B without executing the call statement. In stubbing, the program analysis device 100 assigns a symbol independent of the symbol “X” to an update variable that may be updated by the section B. The update variable can be searched for by scanning the statement in section B in advance. Here, the program analyzer 100 assigns the symbol “Z” to “variable 1”. The program analyzer 100 continues the symbolic execution of the section A using the symbol “Z”, and stores the end point logic at the end point of the section A. At the end point of section A, the logic whose path output is variable 1 = Z + 3 and the logic whose path output is variable 1 = Z-3 are detected.

  Further, the program analysis device 100 assigns the symbol “Y” to “variable 1” storing the input of the section B, and starts the symbolic execution of the section B. The program analyzer 100 saves the call destination logic at the end point of the section B. At the end point of section B, the logic whose path output is variable 1 = Y + 2 and the logic whose path output is variable 1 = Y-2 are detected.

  Then, the program analysis device 100 combines the halfway point logic, the end point logic, and the call destination logic, and reproduces the logic extending over the section A and the section B. The program analysis device 100 associates the path output indicated by the halfway logic with the symbol “Y” indicating the input of the section B. Further, the program analysis device 100 associates the path output indicated by the call destination logic with the symbol “Z” used for stubbing the section B. As shown in the path candidate table 143 of FIG. 7, there are eight possible combinations of the intermediate logic, the end logic, and the call destination logic.

  That is, a path output of variable 1 = X + 1 + 2 + 3 can be considered from a combination of variable 1 = X + 1, variable 1 = Y + 2, and variable 1 = Z + 3. From the combination of variable 1 = X + 1, variable 1 = Y + 2, and variable 1 = Z-3, a path output of variable 1 = X + 1 + 2-3 can be considered. From the combination of variable 1 = X + 1, variable 1 = Y-2 and variable 1 = Z + 3, a path output of variable 1 = X + 1-2 + 3 can be considered. From a combination of variable 1 = X + 1, variable 1 = Y-2, and variable 1 = Z-3, a path output of variable 1 = X + 1-2-3 can be considered.

  From the combination of variable 1 = X-1, variable 1 = Y + 2, and variable 1 = Z + 3, a path output of variable 1 = X-1 + 2 + 3 can be considered. From the combination of variable 1 = X-1, variable 1 = Y + 2, and variable 1 = Z-3, a path output of variable 1 = X-1 + 2-3 can be considered. From the combination of variable 1 = X-1, variable 1 = Y-2, and variable 1 = Z + 3, a path output of variable 1 = X-1-2 + 3 can be considered. From the combination of variable 1 = X-1, variable 1 = Y-2, and variable 1 = Z-3, a path output of variable 1 = X-1-2-3 can be considered.

  However, as described above, not all of the above eight logics are valid. The program analysis device 100 selects only a combination that does not contradict the path condition among the combinations of the halfway point logic, the end point logic, and the call destination logic. That is, the program analysis device 100 combines the path condition of the intermediate logic, the path condition of the end logic, and the path condition of the call destination logic, and determines whether the combined path condition can be satisfied.

Next, a procedure of dividing the symbolic execution and combining the partial logics will be described.
FIG. 8 is a diagram illustrating an example of the update variable table and the symbol assignment table.
The program analysis device 100 detects, from the analysis range, a call statement having no description of an action (a call statement whose action is unknown), such as a PERFORM statement. The program analysis device 100 searches for an update variable from a module called by the detected call statement and generates an update variable table 122. The update variable table 122 has items of a module name and an update variable. In the item of the module name, module identification information such as a section name is described. In the item of the update variable, a variable name of a variable whose value is updated in the called module is described. There may be more than one update variable per module. The update variable is, for example, a variable described in the left side of the assignment expression or the second argument of the MOVE statement.

  When detecting a call statement in which no action is described during the symbolic execution, the program analysis device 100 assigns a symbol to an update variable described in the update variable table 122. The program analysis device 100 generates a symbol assignment table 123. The symbol assignment table 123 has items of variable names and symbols. In the item of the variable name, the variable name of the update variable is described. The symbol item describes the symbol assigned to the update variable immediately after the call statement. As an example, the symbol assigned to the update variable is a concatenation of the variable name, a character string indicating that the call statement is a PERFORM statement, the line number of the call statement, the name of the called module, and the execution count of the call statement. is there. Therefore, for example, immediately after passing the 23rd line of the program 121, the symbol “variable 1_Perform_23_section B_1” is assigned to “variable 1”.

FIG. 9 is a diagram illustrating an example of extracting hierarchical update variables.
If a module called from the analysis scope calls another module, the update variables are searched hierarchically. Here, it is assumed that the analysis range is the section 144, the section 144 is called from the section 144a (section A1) and the section 144b (section B1), and the section 144b is called from the section 144c (section B2). The section 144a updates the variables “a11” and “a12”. The section 144b updates the variables “b11” and “b12”. Section 144c updates variable "b21". In this case, the program analyzer 100 generates an update variable table 145 corresponding to the update variable table 122.

  The program analyzer 100 traces the section 144a from the section 144, and detects the variables “a11” and “a12” as update variables for the first call statement of the section 144. The program analysis device 100 associates the section 144a with the variables “a11” and “a12” and registers them in the update variable table 145. Further, the program analyzer 100 traces the sections 144b and 144c from the section 144, and detects the variables “b11”, “b12” and “b21” as update variables for the second call statement in the section 144. The program analyzer 100 associates the section 144b with the variables “b11”, “b12”, and “b21” and registers them in the update variable table 145.

FIG. 10 is a diagram illustrating an example of a logic table of an intermediate point, a call destination, and an end point.
The program analysis device 100 generates a midway point logic table 124, a call destination logic table 125, and an end point logic table 126 by symbolic execution.

  The halfway point logic table 124 has items of a path number, a path condition, and a path output. In the item of the path number, the identification number of the logic detected before the call statement of the calling module is described. In the path condition item, the path condition immediately before the call statement is described. In the path output item, the value of the variable immediately before the call statement is described. A symbol assigned to an input of a calling module can be used for the path condition and the path output of the halfway point logic table 124.

  Regarding the program 121, the logic that the path condition is “variable 1_A is greater than 10” and the path output is “variable 1 = variable 1_A + 1” is registered in the halfway point logic table 124. In the halfway point logic table 124, a logic that the path condition is “variable 1_A is 10 or less” and the path output is “variable 1 = variable 1_A−1” is registered.

  The call destination logic table 125 has items of a path number, a path condition, and a path output. In the item of the path number, the identification number of the logic detected between the start point and the end point of the called module is described. In the path condition item, a path condition at the end point of the called module is described. In the path output item, the value of a variable at the end point of the called module is described. The symbol assigned to the input of the called module can be used for the path condition and the path output of the called logic table 125.

  For the program 121, the logic that the path condition is “variable 1_B is larger than 20” and the path output is “variable 1 = variable 1_B + 2” is registered in the call destination logic table 125. In the call destination logic table 125, a logic that the path condition is "variable 1_B is 20 or less" and the path output is "variable 1 = variable 1_B-2" is registered. Note that the symbol “variable 1_B” indicates the input of section B.

  The end point logic table 126 has items of a path number, a path condition, and a path output. In the item of the path number, the identification number of the logic detected between the start point and the end point of the calling module is described. The path condition item describes the path condition at the end point of the calling module. The path output item describes the value of a variable at the end point of the calling module. For the path condition and the path output of the end point logic table 126, a symbol assigned to the input of the calling module or a symbol assigned to the update variable immediately after the call statement can be used.

  For the program 121, the logic that the path condition is “variable 1_A is larger than 10” and “variable 1_Perform_23_section B_1 is smaller than 30” and the path output is “variable 1 = variable 1_Perform_23_section B_1 + 3” is registered in the end point logic table 126. Is done. In the end point logic table 126, the logic that the path condition is “variable 1_A is greater than 10” and “variable 1_Perform_23_section B_1 is 30 or more” and the path output is “variable 1 = variable 1_Perform_23_section B_1-3” are registered. You.

  In the end point logic table 126, the logic that the path condition is “variable 1_A is 10 or less” and “variable 1_Perform_23_section B_1 is smaller than 30” and the path output is “variable 1 = variable 1_Perform_23_section B_1 + 3” are registered. In the end point logic table 126, the logic that the path condition is “variable 1_A is 10 or less” and “variable 1_Perform_23_section B_1 is 30 or more” and the path output is “variable 1 = variable 1_Perform_23_section B_1-3” are registered. . The symbol “variable 1_Perform_23_section B” is a symbol assigned to “variable 1” immediately after the call statement.

FIG. 11 is a diagram illustrating a simplified example of the partial logic.
When the symbolic execution ends, the program analysis device 100 acquires the halfway point logic table 124, the call destination logic table 125, and the end point logic table 126. The program analyzer 100 simplifies the midpoint logic table 124, the call destination logic table 125, and the end point logic table 126, respectively. Since the intermediate logic table 124 and the call destination logic table 125 shown in FIG. 10 have no room for reduction, an example of the reduction of the end point logic table 126 will be described here.

  The program analysis apparatus 100 searches the end point logic table 126 for logic having the same path output but different path conditions. The program analyzer 100 integrates the corresponding logics into one by connecting the path conditions of the corresponding logics with disjunction (OR). In the example of FIG. 11, the logic # 1 and the logic # 3 of the end point logic table 126 of FIG. 10 are integrated and converted into the logic # 1x. Also, logic # 2 and logic # 4 are integrated and converted to logic # 2x.

  The path condition of the logic # 1x is “variable 1_A is greater than 10 and variable 1_Perform_23_section B_1 is smaller than 30” or “variable 1_A is 10 or less and variable 1_Perform_23_section B_1 is smaller than 30”. The path output of the logic # 1x is “variable 1 = variable 1_Perform_23_section B_1 + 3”. The path condition of logic # 2x is “variable 1_A is greater than 10 and variable 1_Perform_23_section B_1 is 30 or more” or “variable 1_A is 10 or less and variable 1_Perform_23_section B_1 is 30 or more”. The path output of the logic # 2x is “variable 1 = variable 1_Perform_23_section B_1-3”.

  The program analysis device 100 simplifies the integrated logic path condition by using a mathematical processing technique. In the example of FIG. 11, the path condition of the logic # 1x can be modified to “variable 1_A is greater than 10 or variable 1_A is 10 or less” and “variable 1_Perform_23_section B_1 is less than 30”. Therefore, the path condition of the logic # 1x is reduced to “variable 1_Perform_23_section B_1 is smaller than 30”. In addition, the path condition of the logic # 2x can be modified to “variable 1_A is greater than 10 or variable 1_A is 10 or less” and “variable 1_Perform_23_section B_1 is 30 or more”. Therefore, the path condition of the logic # 2x is reduced to “variable 1_Perform_23_section B_1 is 30 or more”. For simplification of the above pass conditions, for example, the Quine-McCluskey method can be used.

  The program analysis device 100 further searches for logics having the same simplified path conditions but different path outputs. The program analysis device 100 integrates the corresponding logics into one by connecting the path outputs of the corresponding logics with conjunction (AND). However, in the example of FIG. 11, there is no corresponding logic.

FIG. 12 is a diagram illustrating an example of combining partial logics.
When the program analysis device 100 simplifies the intermediate logic table 124, the call destination logic table 125, and the end logic table 126, the logic of these three logic tables is combined. First, the program analysis device 100 combines the logic of the intermediate logic table 124 and the logic of the callee logic table 125 to generate an intermediate combined logic table 127.

  The program analysis device 100 selects one intermediate logic from the intermediate logic table 124 and selects one call destination logic from the call destination logic table 125. The program analyzer 100 substitutes the path output of the selected halfway point logic into the symbol used for the path condition of the selected call destination logic. Then, the program analyzer 100 calculates a conjunction (AND) between the assignment result and the path condition of the intermediate point logic as the path condition of the intermediate combination logic. The program analysis device 100 determines whether the calculated path condition of the intermediate combination logic is satisfiable. If the path condition is satisfiable, the program analysis device 100 adopts the combination of the halfway point logic and the call destination logic as an effective combination. On the other hand, if the program analysis device 100 cannot satisfy the condition, it does not adopt the combination of the halfway point logic and the called destination logic as an invalid combination.

  For a valid combination, the program analysis device 100 substitutes the path output of the halfway logic for the symbol used for the path output of the called logic, and calculates the path output of the intermediate combination logic. The program analysis device 100 registers the path condition and the path output calculated for the valid combination in the intermediate combination logic table 127.

  In the case of the program 121, the program analyzer 100 substitutes the value of “variable 1” of the path output of the halfway logic into the symbol “variable 1_B” of the called logic. The program analysis device 100 selects the halfway point logic # 1 and the call destination logic # 1, and calculates a path condition of “variable 1_A is greater than 10” and “variable 1_A + 1 is greater than 20”. This is equivalent to “variable 1_A + 1 is greater than 20”. Since this path condition is satisfiable (there is a symbol “variable 1_A” that satisfies this path condition), the program analysis device 100 performs intermediate coupling of the combination of the halfway point logic # 1 and the call destination logic # 1. Adopted as logic # 1. The path output of the intermediate combination logic # 1 is “variable 1 = variable 1_A + 1 + 2”.

  Further, the program analysis device 100 selects the halfway point logic # 1 and the call destination logic # 2, and calculates a path condition of “variable 1_A is greater than 10” and “variable 1_A + 1 is 20 or less”. Since this path condition can be satisfied, the program analysis device 100 adopts a combination of the halfway point logic # 1 and the call destination logic # 2 as the intermediate combination logic # 2. The path output of the intermediate combination logic # 2 is “variable 1 = variable 1_A + 1-2”. Further, the program analysis device 100 selects the halfway point logic # 2 and the call destination logic # 1, and calculates a path condition of “variable 1_A is equal to or less than 10” and “variable 1_A + 1 is greater than 20”. Since this path condition cannot be satisfied, the program analyzer 100 does not employ the combination of the halfway point logic # 2 and the call destination logic # 1.

  Further, the program analysis device 100 selects the halfway point logic # 2 and the call destination logic # 2, and calculates a path condition of “variable 1_A is 10 or less” and “variable 1_A + 1 is 20 or less”. This is equivalent to “variable 1_A + 1 is 10 or less”. Since this path condition can be satisfied, the program analysis device 100 adopts a combination of the halfway point logic # 2 and the call destination logic # 2 as the intermediate combination logic # 3. The path output of the intermediate combination logic # 3 is “variable 1 = variable 1_A-1-2”.

FIG. 13 is a diagram (continuation) illustrating an example of combining partial logics.
Next, the program analysis device 100 combines the logic of the intermediate combination logic table 127 and the logic of the end point logic table 126 to generate a logic table 128.

  The program analysis device 100 selects one intermediate combination logic from the intermediate combination logic table 127 and selects one end point logic from the end point logic table 126. The program analyzer 100 substitutes the path output of the selected intermediate combination logic into the symbol used for the path condition of the selected end point logic. Then, the program analyzer 100 calculates a conjunction (AND) between the assignment result and the path condition of the intermediate combination logic as the path condition of the combined logic. The program analysis device 100 determines whether the calculated logic path condition is satisfiable. If the path condition is satisfiable, the program analyzer 100 adopts the combination of the intermediate combination logic and the end point logic as an effective combination. On the other hand, if the program analysis device 100 is not satisfiable, the combination of the intermediate combination logic and the end point logic is not adopted as an invalid combination.

  The program analysis device 100 calculates the path output of the combined logic by substituting the path output of the intermediate combination logic into the symbol used for the path output of the end point logic for the valid combination. The program analysis device 100 registers the path condition and the path output calculated for the valid combination in the logic table 128.

  In the case of the program 121, the program analysis device 100 substitutes the value of “variable 1” of the path output of the intermediate combination logic into the symbol “variable 1_Perform_23_section B_1” of the end point logic. The program analysis device 100 selects the intermediate combination logic # 1 and the end point logic # 1x, and calculates a path condition of “variable 1_A + 1 is larger than 20” and “variable 1_A + 1 + 2 is smaller than 30”. Since this path condition can be satisfied, the program analyzer 100 adopts a combination of the intermediate combination logic # 1 and the end point logic # 1x as the logic # 1. The path output of the logic # 1 is “variable 1 = variable 1_A + 1 + 2 + 3”.

  Further, the program analysis device 100 selects the intermediate combination logic # 1 and the end point logic # 2x, and calculates a path condition of “variable 1_A + 1 is greater than 20” and “variable 1_A + 1 + 2 is 30 or more”. This is equivalent to “variable 1_A + 1 + 2 is 30 or more”. Since this path condition can be satisfied, the program analysis device 100 adopts a combination of the intermediate combination logic # 1 and the end point logic # 2x as the logic # 2. The path output of the logic # 2 is “variable 1 = variable 1_A + 1 + 2−3”.

  Further, the program analyzer 100 selects the intermediate combination logic # 2 and the end point logic # 1x, and states that "variable 1_A is greater than 10", "variable 1_A + 1 is less than 20", and "variable 1_A + 1-2 is less than 30". Calculate path conditions. This is equivalent to "variable 1_A is greater than 10". Since this path condition can be satisfied, the program analyzer 100 adopts a combination of the intermediate combination logic # 2 and the end point logic # 1x as the logic # 3. The pass output of the logic # 3 is “variable 1 = variable 1_A + 1-2 + 3”.

  In addition, the program analysis device 100 selects the intermediate combination logic # 2 and the end point logic # 2x, and selects the path “variable 1_A is greater than 10”, “variable 1_A + 1 is 20 or less”, and “variable 1_A + 1-2 is 30 or more” Calculate the condition. Since this path condition cannot be satisfied, the program analysis device 100 does not employ the combination of the intermediate combination logic # 2 and the end point logic # 2x.

  Further, the program analysis device 100 selects the intermediate combination logic # 3 and the end point logic # 1x, and calculates a path condition that “variable 1_A is 10 or less” and “variable 1_A-1-2 is less than 30”. This is equivalent to “variable 1_A is 10 or less”. Since this path condition can be satisfied, the program analysis device 100 adopts a combination of the intermediate combination logic # 3 and the end point logic # 1x as the logic # 4. The pass output of logic # 4 is “variable 1 = variable 1_A-1-2 + 3”.

  In addition, the program analysis device 100 selects the intermediate combination logic # 3 and the end point logic # 2x, and calculates a path condition of “variable 1_A is 10 or less” and “variable 1_A-1-2 is 30 or more”. Since this path condition cannot be satisfied, the program analysis device 100 does not employ the combination of the intermediate combination logic # 3 and the end point logic # 2x.

As a result, a logic table 128 in which four logics are registered is generated. The logic table 128 is equivalent to the logic table 129 of FIG. 6 generated when an execution path extending between the section A and the section B is directly detected. In this manner, the program analysis device 100 can correctly extract the logic of the module within the analysis range even if the amount of calculation for symbolic execution is reduced. Incidentally, in the example of a program 121, a candidate execution paths to be symbolic execution is reduced from one ^{2 2 × 2 1 = 8 2} 2 +2 1 = 6 one on. The effect of reducing the amount of calculation increases as the number of conditional branch statements increases.

FIG. 14 is a diagram illustrating a third example of the program.
The program 146 includes a section A and a section B similarly to the program 121. However, in the program 146, a conditional branch statement is added to the section B. In the added statement, the value of “variable 1” is increased by 4 when the value of “variable 1” is less than 25, and the value of “variable 1” is increased when the value of “variable 1” is 25 or more. Decrease by 4.

When an execution path extending between section A and section B is directly detected by symbolic execution, the number of execution path candidates to be searched is 2 ² × 2 ² = 16. On the other hand, according to the method of dividing the symbolic execution of the section A and the symbolic execution of the section B and combining the partial logic a posteriori, the number of execution path candidates to be searched is 2 ² +2 ² = 8. In this case, the number of execution path candidates to be searched is reduced by half.

Next, functions and processing procedures of the program analyzer 100 will be described.
FIG. 15 is a block diagram illustrating a function example of the program analysis device.
The program analysis device 100 has a storage unit 120. The storage unit 120 is implemented using a storage area secured in the RAM 102 or the HDD 103, for example. The storage unit 120 stores a program 121, an update variable table 122, a symbol assignment table 123, an intermediate logic table 124, a call destination logic table 125, an end logic table 126, an intermediate combination logic table 127, and a logic table 128.

  Further, the program analyzer 100 includes an update variable extraction unit 131, an update value assignment unit 132, a symbolic execution unit 133, a partial logic collection unit 134, a logic reduction unit 135, a partial logic combination unit 136, and an analysis result display unit 137. . The update variable extraction unit 131, the update value assignment unit 132, the symbolic execution unit 133, the partial logic collection unit 134, the logic reduction unit 135, the partial logic combination unit 136, and the analysis result display unit 137 are, for example, programs executed by the processor 101. Implemented using modules.

  When a program 121 to be analyzed and an analysis range in the program 121 are designated, the update variable extraction unit 131 calls a module outside the analysis range from the analysis range and has no description of the action (for example, PERFORM statement). The update variable extraction unit 131 searches the call destination module of the searched call statement for an update variable whose value may be updated in the call destination module. Thereby, the update variable extraction unit 131 generates the update variable table 122 and stores it in the storage unit 120.

  The update value assignment unit 132 generates the symbol assignment table 123 and stores the symbol assignment table 123 in the storage unit 120. The update value assignment unit 132 detects that the symbolic execution by the symbolic execution unit 133 reaches a call statement that calls a module outside the analysis range and has no description of the operation. Then, the update value allocating unit 132 searches the update variable table 122 for an update variable corresponding to the called module, and allocates a new symbol to each of the searched update variables. The update value assignment unit 132 registers the assigned symbols in the symbol assignment table 123 and notifies the symbolic execution unit 133.

  The symbolic execution unit 133 starts symbolic execution after the update variable extraction unit 131 extracts the update variables. The target of symbolic execution is a specified analysis range in the program 121. However, if there is a call statement, the symbolic execution unit 133 performs symbolic execution of the called module independently of the calling module. The symbolic execution unit 133 assigns a symbol to the input of the module at the head of each module. Further, when the symbolic execution unit 133 reaches a call statement that calls a module outside the analysis range and has no description of the action, the symbolic execution unit 133 stubs the call destination module and acquires a symbol of an update variable from the update value assignment unit 132. . After the call statement, symbolic execution is continued using the acquired symbol.

  The partial logic collection unit 134 generates the halfway point logic table 124, the call destination logic table 125, and the end point logic table 126 and stores them in the storage unit 120. The partial logic collection unit 134 collects various types of logic information in the course of symbolic execution by the symbolic execution unit 133. When the symbolic execution reaches the call statement, the partial logic collection unit 134 acquires the midpoint logic immediately before the call statement and registers it in the midpoint logic table 124. Further, when the symbolic execution reaches the end point of the called module, the partial logic collection unit 134 acquires the called logic at that time and registers it in the called logic table 125. When the symbolic execution reaches the end point of the calling module, the partial logic collection unit 134 acquires the calling logic at that time and registers it in the end logic table 126.

  After completing the symbolic execution, the logic simplification unit 135 simplifies the midpoint logic registered in the midpoint logic table 124. Further, after the symbolic execution is completed, the logic simplifying unit 135 reduces the call destination logic registered in the call destination logic table 125. After the symbolic execution ends, the logic simplifying unit 135 reduces the end point logic registered in the end point logic table 126.

  The partial logic combining unit 136 generates the intermediate combined logic table 127 and the logic table 128 and stores them in the storage unit 120. The partial logic combining unit 136 combines the waypoint logic registered in the waypoint logic table 124 with the call destination logic registered in the callee logic table 125, and registers the intermediate combined logic in the intermediate combined logic table 127. In the connection between the halfway point logic and the call destination logic, only the logic that can satisfy the path condition after the connection is adopted. The partial logic combining unit 136 combines the intermediate combined logic with the end point logic registered in the end point logic table 126, and registers the combined logic in the logic table 128. In the connection between the intermediate connection logic and the end point logic, only the path conditions after the connection that can be run vertically are adopted.

  The analysis result display unit 137 displays the generated logic table 128 on the display 111. However, the program analysis device 100 may transmit the generated logic table 128 to another device. Further, the program analyzer 100 may output the logic table 128 by another method, such as reproducing a voice reading out the contents of the logic table 128 from a speaker, outputting the logic table 128 to a printing device, or the like.

FIG. 16 is a flowchart illustrating an example of a procedure of program analysis.
(S1) The program analysis device 100 acquires the specification of the program 121 to be analyzed and the specification of one or more modules to be analyzed in the program 121. These designations are input by the user using the input device 112, for example.

(S2) The update variable extraction unit 131 extracts update variables of modules outside the analysis range that may be called when the analysis range is executed. Details of the update variable extraction will be described later.
(S3) The symbolic execution unit 133 separately performs symbolic execution on the module in the analysis range and the module outside the analysis range, which is the call destination. The partial logic collection unit 134 collects midway point logic, call destination logic, and end point logic while symbolic execution is being performed. The details of the symbolic execution will be described later.

(S4) The logic simplification unit 135 simplifies the collected intermediate logic, call destination logic, and end logic, respectively. Details of the logic simplification will be described later.
(S5) The partial logic combining unit 136 combines the simplified halfway point logic and the call destination logic. Details of the logic connection will be described later.

(S6) The partial logic combination unit 136 combines the intermediate combination logic and the end point logic generated in step S5. The algorithm of the logic combination is the same as in step S5.
(S7) The analysis result display unit 137 causes the display 111 to display the logic table 128 indicating the logic combined in step S6.

FIG. 17 is a flowchart illustrating an example of a procedure for extracting update variables.
The update variable extraction is performed in step S2 described above.
(S10) The update variable extraction unit 131 acquires the specification of the program 121 to be analyzed and the specification of one or more modules to be analyzed in the program 121. The update variable extraction unit 131 focuses on the modules in the specified analysis range.

(S11) The update variable extraction unit 131 searches the module of interest for a call statement that calls a module outside the analysis range and has no description of the action.
(S12) The update variable extraction unit 131 determines whether or not the corresponding call statement has been searched in step S11. If there is a corresponding call statement, the process proceeds to step S13; otherwise, steps S13 to S16 are skipped.

(S13) The update variable extraction unit 131 acquires a called module.
(S14) The update variable extraction unit 131 searches the call destination module for a variable update statement for updating the value of the variable. The variable whose value is updated (updated variable) is, for example, a variable described on the left side of the assignment statement, a variable described as the second argument of the MOVE statement, or the like.

  (S15) The update variable extraction unit 131 associates the module name of the called module with the variable name of the update variable retrieved in step S14, and registers it in the update variable table 122. However, when the call is performed hierarchically, the module name of the first-stage module called from the analysis range is used as the module name.

  (S16) The update variable extraction unit 131 pays attention to the call destination module acquired in step S13, and recursively executes the processes of steps S11 to S16 for the call destination module. When the called module further includes a call statement (sub-call statement) for calling another module, the update variable is searched recursively.

FIG. 18 is a flowchart illustrating an example of a symbolic execution procedure.
Symbolic execution is performed in the above-described step S3.
(S20) The symbolic execution unit 133 acquires the specification of the program 121 to be analyzed and the specification of one or more modules to be analyzed in the program 121. The symbolic execution unit 133 focuses on modules in the specified analysis range.

  (S21) The symbolic execution unit 133 assigns an independent symbol to an input variable in which the input of the module of interest is stored. For example, the symbolic execution unit 133 assigns the symbol “variable 1_A” to “variable 1” in section A of FIG.

(S22) The symbolic execution unit 133 acquires one command statement to be executed next from the program 121 in accordance with the processing order of the program 121.
(S23) The symbolic execution unit 133 determines whether a command statement other than the end statement has been acquired in step S22. If a command statement other than the end statement has been acquired, the process proceeds to step S24. If the end statement has been acquired or the corresponding statement does not exist, the process proceeds to step S29.

  (S24) The symbolic execution unit 133 determines whether the command statement acquired in step S22 is a call statement for calling a module outside the analysis range and has no description of the operation. A call statement in which an update variable to be updated by the callee module is not specified, such as the PERFORM statement in FIG. 5, is a call statement in which the operation is not described. If the acquired statement is a corresponding calling statement, the process proceeds to step S25. If the acquired statement is other than that, the process proceeds to step S31.

  (S25) The partial logic collection unit 134 registers the path condition and the path output immediately before the call statement in the halfway point logic table 124. The path condition is obtained by accumulating the conditions in the branch direction selected from the head of the module of interest to immediately before the call statement. The path output is the value of the variable immediately before the call statement. The symbols assigned in step S21 may be used for the path condition and the path output.

  (S26) The symbolic execution unit 133 determines whether the called module indicated by the calling statement has been analyzed. If the called module has been analyzed, the process proceeds to step S28; if not, the process proceeds to step S27.

  (S27) The symbolic execution unit 133 focuses on the call destination module, and recursively executes the processing of steps S21 to S30. At this time, the symbolic execution unit 133 saves information during the analysis of the calling module and performs symbolic execution on the called module independently of the calling module. When the symbolic execution of the called module ends, the symbolic execution unit 133 continues the symbolic execution of the calling module using the saved information in the course of the analysis. In the flowchart of FIG. 18, the symbolic execution of the calling module is interrupted and the symbolic execution of the called module is performed. However, the symbolic execution of the called module may be started after the symbolic execution of the calling module is completed.

  (S28) The update value assignment unit 132 searches the update variable table 122 for an update variable corresponding to the called module. The update value assigning unit 132 assigns an independent symbol to the searched update variable, and registers the assigned symbol in the symbol assignment table 123. Further, the update value assignment unit 132 notifies the symbolic execution unit 133 of the assigned symbol. If the symbolic execution unit 133 holds the value of the update variable immediately before the call statement, the symbolic execution unit 133 discards the value and saves the symbol notified from the update value assignment unit 132. That is, the symbolic execution unit 133 treats the value of the update variable as being overwritten by the notified symbol. Then, the process proceeds to step S22.

  (S29) The symbolic execution unit 133 determines that the execution path has reached the end point. The partial logic collection unit 134 registers the path condition and the path output at that time in the end point logic table 126. However, in the case of symbolic execution for the called module, the partial logic collection unit 134 registers the path condition and the path output at that time in the called logic table 125. The path condition is obtained by accumulating the conditions in the branch direction selected from the head to the end point of the module of interest. The path output is the value of a variable at the end point of the module of interest. The symbols assigned in step S21 and the symbols assigned in step S28 may be used for the path condition and the path output.

  (S30) The symbolic execution unit 133 determines whether an unselected execution path remains among the execution paths divided by the conditional branch statement. If there is an unselected execution path, the symbolic execution unit 133 backtracks to the previous division point, and acquires the stored path condition and path output at that division point. The symbolic execution unit 133 selects an unselected branch direction, and continues symbolically executing the execution path using the acquired path condition and path output. Then, the process proceeds to step S22. On the other hand, if there is no unselected execution path, the symbolic execution of the module of interest ends.

FIG. 19 is a flowchart (continued) illustrating a procedure example of symbolic execution.
(S31) The symbolic execution unit 133 determines whether the statement acquired in step S22 is a variable update statement for updating the value of a variable. The variable update statement is, for example, an assignment statement or a MOVE statement in which the left side and the right side are connected by an equal sign. If the acquired statement is a variable update statement, the process proceeds to step S32; otherwise, the process proceeds to step S33.

(S32) The symbolic execution unit 133 updates the value of the variable according to the variable update statement. The value of a variable may be represented by an expression containing a symbol. Then, the process proceeds to step S22.
(S33) The symbolic execution unit 133 determines whether the statement acquired in step S22 is a conditional branch statement. If the acquired statement is a conditional branch statement, the process proceeds to step S34; otherwise, the process proceeds to step S37.

  (S34) The symbolic execution unit 133 can satisfy the two branch directions of the YES direction and the NO direction based on the branch condition described in the conditional branch statement, the value of the variable at that time, and the path condition at that time. Determine gender. If the value of the variable is an expression including a symbol, it may be determined that both of the two branch directions are satisfiable.

  (S35) The symbolic execution unit 133 determines whether both of the two branch directions can be satisfied. If both branch directions can be satisfied, the process proceeds to step S36. If only one branch direction can be satisfied, the process proceeds to step S37.

  (S36) The symbolic execution unit 133 divides the execution path. The symbolic execution unit 133 selects one of the two branch directions (for example, the YES direction) and sets it as the traveling direction of the current execution path. Further, the symbolic execution unit 133 saves the path condition and the path output at that time. The divided execution path corresponding to the unselected branch direction is set as an unselected execution path. Then, the process proceeds to step S22.

  (S37) The symbolic execution unit 133 performs a process according to the statement acquired in step S22. If it is determined in step S35 that only one branch direction can be satisfied, the symbolic execution unit 133 selects a satisfiable branch direction according to the conditional branch statement. At this time, the execution path is not divided. Then, the process proceeds to step S22.

FIG. 20 is a flowchart illustrating an example of a procedure for simplifying logic.
Logic simplification is performed in step S4 described above.
(S40) The logic simplification unit 135 selects one of the halfway logic table 124, the called logic table 125, and the end logic table 126.

(S41) The logic simplifying unit 135 searches the logic table selected in step S40 for a plurality of logics having the same path output but different path conditions.
(S42) When a plurality of logics corresponding to step S41 are searched, the logic simplification unit 135 connects the searched plurality of logics to one by connecting the path conditions of the searched plurality of logics by OR. Integrate into your logic.

(S43) The logic simplification unit 135 simplifies the path conditions of each logic after integration in step S42 by reducing redundancy.
(S44) The logic simplifying unit 135 searches the logics simplified in step S43 for a plurality of logics having the same path condition but different path outputs.

  (S45) When a plurality of logics corresponding to step S44 are searched, the logic simplification unit 135 connects the path outputs of the searched plurality of logics by AND to combine the searched plurality of logics into one. Integrate into your logic.

  (S46) In step S40, the logic simplifying unit 135 determines whether all of the intermediate logic table 124, the call destination logic table 125, and the end logic table 126 have been selected. If there is an unselected logic table, the process proceeds to step S40, and if all three logic tables have been selected, the logic simplification ends.

FIG. 21 is a flowchart illustrating an example of the procedure of the logic combination.
The logic combination is performed in steps S5 and S6 described above. In steps S5 and S6, a common logic combination algorithm can be used.

  (S50) The partial logic combining unit 136 acquires the logic table T1 and the logic table T2 to be combined. In step S5, the logic table T1 is the midpoint logic table 124, and the logic table T2 is the call destination logic table 125. In step S6, the logic table T1 is the intermediate combination logic table 127, and the logic table T2 is the end point logic table 126.

(S51) The partial logic combination unit 136 selects the record R1 from the logic table T1. Record R1 represents one logic in logic table T1.
(S52) The partial logic combining unit 136 selects the record R2 from the logic table T2. Record R2 represents one logic in logic table T2.

  (S53) The partial logic combining unit 136 substitutes the path output of the record R1 for the symbol used for the path condition of the record R2. The partial logic combining unit 136 connects the assignment result and the path condition of the record R1 by AND, and calculates the combined path condition.

  (S54) The partial logic combination unit 136 determines whether the combined path conditions calculated in step S53 can be satisfied. If the combined path condition can be satisfied, the process proceeds to step S55; otherwise, the process proceeds to step S57.

(S55) The partial logic combining unit 136 substitutes the path output of the record R1 for the symbol used for the path output of the record R2, and calculates the combined path output.
(S56) The partial logic combination unit 136 registers the path condition calculated in step S53 and the path output calculated in step S55 in the logic table of the result of the combination. In step S5, the logic table of the combination result is the intermediate combination logic table 127. In step S6, the logic table of the combination result is the logic table 128.

  (S57) The partial logic combination unit 136 determines whether there is a record not selected in step S52 in the logic table T2. If there are unselected records, the process proceeds to step S52, and if all records have been selected, the process proceeds to step S58.

  (S58) The partial logic combination unit 136 determines whether there is a record not selected in step S51 in the logic table T1. If there is an unselected record, the process proceeds to step S51, and if all records have been selected, the logic combination ends.

  According to the program analyzer 100 of the second embodiment, the symbolic execution of the calling module and the symbolic execution of the called module are performed independently. In the symbolic execution of the calling module, the path condition and path output immediately before the calling statement are saved, the calling statement is skipped, and a new symbol is assigned to an update variable that may be updated in the called module. . Then, the logic information immediately before the call statement, the logic information at the end point of the caller module, and the logic information at the end point of the callee module are combined, and the execution path is reproduced.

  As a result, it is possible to suppress a path explosion when analyzing an execution path spanning a plurality of modules, and to reduce the amount of calculation of symbolic execution. Therefore, the execution path can be analyzed efficiently. Also, since the processing contents of the called module are not ignored, the reproduced execution path correctly represents the relationship between the input and output of the calling module.

DESCRIPTION OF SYMBOLS 10 Program analysis apparatus 11 Storage part 12 Operation part 20 Program 21, 26 module 22 Call instruction 23a, 23b 1st execution path 24 1st information 25 2nd information 27a, 27b 2nd execution path 28 3rd information 31a, 31b, 31c, 31d Synthesis execution path 32 Path information c1, c2, c3 Symbol

Claims (6)

A computer-implemented program analysis method,
A first module and a second module, wherein the first module obtains a program including a call instruction for calling the second module;
Assigning a first symbol to an input of the first module, generating first information indicating a first processing result before the call instruction using the first symbol, and calling the call instruction; A second symbol is assigned to the result, and a second processing result after the call instruction of each of the plurality of first execution paths included in the first module is expressed by using the second symbol. Generates the information for
A third symbol is assigned to an input of the second module, and a third processing result of each of a plurality of second execution paths included in the second module is represented by using the third symbol. Generates the information for
The first processing result indicated by the first information is associated with the third symbol used for the third information, and the third processing result indicated by the third information is associated with the third symbol. By associating the plurality of first execution paths with the plurality of second execution paths, a processing result of each of a plurality of synthesis execution paths obtained by synthesizing the plurality of first execution paths and the plurality of second execution paths is associated with the second symbol used for the second information. Generating path information represented by using the first symbol;
Program analysis method. The second information indicates a first execution condition of each of the plurality of first execution paths using at least one of the first and second symbols, and the third information indicates a plurality of first execution paths. The second execution condition of each of the two execution paths is expressed using the third symbol,
In the generation of the path information, when the first execution condition corresponding to one first execution path and the second execution condition corresponding to one second execution path do not contradict, the one Combining a first execution path with the one second execution path;
The program analysis method according to claim 1. The first information indicates the first processing result for each of a plurality of partial execution paths that are detected when the plurality of first execution paths are executed up to before the call instruction,
In the generation of the path information, the first processing result of the plurality of partial execution paths, the second processing result of the plurality of first execution paths, and the third processing result of the plurality of second execution paths Combine with the processing result,
The program analysis method according to claim 1. Searching the program for an update variable updated by the second module among the variables used in the first module;
Generating the second information, allocating the second symbol to the update variable;
The program analysis method according to claim 1. A storage unit that includes a first module and a second module, wherein the first module stores a program that includes a call instruction that calls the second module;
Assigning a first symbol to an input of the first module, generating first information indicating a first processing result before the call instruction using the first symbol, and calling the call instruction; A second symbol is assigned to the result, and a second processing result after the call instruction of each of the plurality of first execution paths included in the first module is expressed by using the second symbol. Generates the information for
A third symbol is assigned to an input of the second module, and a third processing result of each of a plurality of second execution paths included in the second module is represented by using the third symbol. Generates the information for
The first processing result indicated by the first information is associated with the third symbol used for the third information, and the third processing result indicated by the third information is associated with the third symbol. By associating the plurality of first execution paths with the plurality of second execution paths, a processing result of each of a plurality of synthesis execution paths obtained by synthesizing the plurality of first execution paths and the plurality of second execution paths is associated with the second symbol used for the second information. An operation unit that generates path information represented by using the first symbol;
A program analyzer having: On the computer,
A first module and a second module, wherein the first module obtains a program including a call instruction for calling the second module;
Assigning a first symbol to an input of the first module, generating first information indicating a first processing result before the call instruction using the first symbol, and calling the call instruction; A second symbol is assigned to the result, and a second processing result after the call instruction of each of the plurality of first execution paths included in the first module is expressed by using the second symbol. Generates the information for
A third symbol is assigned to an input of the second module, and a third processing result of each of a plurality of second execution paths included in the second module is represented by using the third symbol. Generates the information for
The first processing result indicated by the first information is associated with the third symbol used for the third information, and the third processing result indicated by the third information is associated with the third symbol. By associating the plurality of first execution paths with the plurality of second execution paths, a processing result of each of a plurality of synthesis execution paths obtained by synthesizing the plurality of first execution paths and the plurality of second execution paths is associated with the second symbol used for the second information. Generating path information represented by using the first symbol;
An analysis program that executes processing.

Images