WO2016038741A1 - Source code equivalence verifying device, and source code equivalence verifying method - Google Patents

Abstract

A source code equivalence verifying device comprises: a symbolic execution calculating unit which performs a symbolic execution calculation with respect to a source code before modification, and a source code after modification, being the source code before modification that has been modified; an equivalence verification formula generating unit which, on the basis of a symbolic execution summary, which is the result of the symbolic execution calculation performed by the symbolic execution calculating unit, generates an equivalence verification formula for verifying the equivalence, which indicates that the same output is obtained in response to the same input, between the source code before modification and the source code after modification; an equivalence verification formula verifying unit which verifies the equivalence verification formula generated by the equivalence verification formula generating unit; and a verification result generating unit which generates a verification result report using the result of the verification carried out by the equivalence verification formula verifying unit.

Description

Source code equivalence verification apparatus and source code equivalence verification method

The present invention relates to an apparatus and a verification method for verifying that execution contents between source codes before and after the change are equivalent when the source code is changed.

There is a technique described in Patent Document 1 as a method for verifying equivalence of source codes. Japanese Patent Application Laid-Open No. 2004-228561 discloses a method of performing a test on a portion where a difference is caused by source code comparison and comparing the result.

Further, Non-Patent Document 1 discloses a technique for verifying that execution contents are maintained using symbol execution.

US Patent Application Publication No. 2007/0033576

S. Person, M. B. Dwyer, S. Elbaum, C. S. Pasareanu, "Differential Symbolic Execution", Proc. Of ACM SIGSOFT International Symposium on the Foundations of Software Engineering 2008, pp. 226-237,

In recent years, with the development of the information processing society, software systems have penetrated the general society, and the reliability required for software has become extremely high. On the other hand, software is becoming increasingly complex and large-scale due to many years of differential / derivative development, and there is a problem of deterioration in maintainability such as ease of software expansion and ease of understanding.

∙ Refactoring and language replacement are methods for improving software maintainability. Refactoring is a general term for methods for improving the design quality of software by changing the internal structure without changing the execution contents of the software. Language replacement is the replacement of software developed using a programming language with low maintainability by recreating the same function as that software using another programming language with high maintainability.

This refactoring and language replacement technique is a promising technique for ensuring the maintainability of software that is becoming increasingly complex and large-scale. However, if the execution content of the target source code is changed when the source code of the software is changed or recreated, there is a possibility that a new defect may be mixed. Therefore, there is a possibility that the software developer fears that a defect is mixed in software that has been operating correctly due to refactoring or language replacement, and may decide not to do so. In order to actively perform refactoring and language replacement in the software maintenance stage, a method for verifying that there is no change in the execution contents of the source code before and after the change of the source code is required.

In the present specification, both sources indicate that the external execution contents of the two source codes before and after the change are the same, that is, the same output is obtained at the time of execution for any same input. Define the code to be “equivalent”. Further, verifying whether the source code before the change and the source code after the change are equivalent is referred to as “equivalence verification”.

Conditions required for the method for verifying that the source code before the change and the source code after the change are equivalent include the following conditions.
(1) One condition is that most of the work is automated, and there are few manual work. Traditionally, source code equivalence has been verified by manual review and testing. By realizing automatic verification using a tool, verification man-hours are reduced, and refactoring and the like are promoted.
(2) Another condition is to provide the developer with information on the basis and information on a portion to be corrected when it is determined that they are not equivalent by the equivalence checking method. By providing the developer with easy-to-understand information on points to be corrected, the developer can easily make corrections, leading to a reduction in the development period and man-hours.
(3) Still another condition is that the verification time by the tool is short or can be shortened by parallelization. Even if the verification work is automated, if a long-time calculation is required for the verification, it is difficult to repeat the cycle of correcting and verifying again after verification. Therefore, it is necessary to use a verification method with a small amount of calculation or a verification method that can reduce the calculation time by parallelization even if the amount of calculation is large.

The method according to Patent Document 1 requires a test and cannot satisfy the condition (1). In addition, the method according to Non-Patent Document 1 cannot obtain information on a portion to be corrected to be equivalent in a non-equivalent case, and cannot satisfy the condition (2). Furthermore, in Non-Patent Document 1, a logical expression for verifying equivalence is generated and verified using a solver. However, this verification expression cannot be executed in parallel and satisfies the condition (3). I can't.

Therefore, in the source code equivalence verification device using symbol execution, when the verification result is not equivalent, it is equivalent to the technology that provides information on the correction part on the source code necessary for the developer to make it equivalent. And a technology for executing the verification of the property in parallel.

The disclosed source code equivalence verification apparatus includes a symbol execution calculation unit that performs symbol execution calculation on a source code before change and a source code after change that has changed the source code before change. Based on the symbol execution summary, the equivalence that generates the equivalence verification formula for verifying the equivalence that the same output is obtained for the same input of the source code before the change and the source code after the change Verification result generator that generates verification result report using verification result in verification formula generator, equivalence verification formula verification unit that verifies equivalence verification formula generated by equivalence verification formula generation unit, and equivalence verification formula verification unit Part.

According to the disclosed source code equivalence verification device, verification time is shortened by parallelizing individual verifications in order to verify equivalence for each control flow path on the source code for verifying equivalence. can do.

In addition, by using equivalence verification results for each path of the control flow, it is possible to narrow down the range that needs to be investigated on the source code when making corrections for equivalence, and the time for correction by the developer And man-hours can be reduced.

It is an example of the source code before a change used for source code equivalence verification. It is a figure which shows the example of the structure graph obtained as a result of a source code analysis. It is a figure which shows the execution tree obtained by calculating symbol execution. It is a hardware block diagram of a source code equivalence verification apparatus. It is a software block diagram of a source code equivalence verification apparatus. It is a functional block diagram of a source code equivalence verification apparatus. It is the figure which showed the data flow of the control part and memory | storage part of a source code equivalence verification apparatus. It is a processing flowchart of source code equivalence verification. It is an example of the source code after a change which implemented the change which becomes equivalent used for source code equivalence verification. It is a figure which shows the execution tree obtained by calculating symbol execution. It is a figure which shows the example of the verification result report which an equivalence verification apparatus outputs. It is an example of the source code after a change which implemented the change which becomes non-equivalent used for source code equivalence verification. It is a figure which shows the execution tree obtained by calculating symbol execution. It is a figure which shows the example of the verification result report which an equivalence verification apparatus outputs. It is a process flowchart of an equivalence verification formula production | generation part. It is an example of a verification result of each path equivalence verification formula in the equivalence verification formula verification unit. It is a figure which shows the example of the verification result report which an equivalence verification apparatus outputs. It is a figure which shows the example of a display when a some snapshot is selected. It is a process flowchart of the equivalence verification type | formula verification process part in a source code equivalence verification apparatus.

The symbol execution that is a premise technique of this embodiment will be described. Symbol execution refers to execution using symbols instead of executing source code while substituting specific values for variables (input variables, global variables, etc.) used in source code when verifying source code A combination of a variable state (hereinafter also referred to as a variable state) in a source code execution process and a conditional expression (hereinafter also referred to as a path constraint) for passing through the control path in the source code (hereinafter referred to as a snap). This is a technique for obtaining the input / output relationship of the software indicated by the source code using the “Shot”.

記号 According to symbol execution, it is possible to verify the source code covering all possible paths of the source code. Hereinafter, a case where symbol execution is performed using the information processing apparatus for the source code C100 described in the C language in FIG. 1 will be described as an example.

In the symbol execution, the information processing apparatus generates the structure graph N100 shown in FIG. 2 by performing lexical analysis and syntax analysis similar to the compilation on the source code C100. The structure graph N100 is obtained by removing the information that is not related to the meaning of the language and extracting only the information that is related to the meaning (abstracted) from the syntax tree. A control flow is shown. A solid line arrow indicates an unconditional control flow, and a broken line arrow indicates a conditional control flow.

In the structure graph N100 of the function foo shown in FIG. 2, each control flow starting from the node N1 corresponding to the function entry point and ending at the node N5 corresponding to the return statement that is the exit of the function is illustrated. In addition, it is shown that there are a plurality of conditional control flows from the node N2 corresponding to the if statement, and there are different control flows depending on whether or not the condition of the if statement is satisfied.

In generating the structure graph N100, the information processing apparatus gives position information on the source code C100 corresponding to each node. In the example illustrated in FIG. 2, the information processing apparatus assigns the line number in the source code C100 as position information. For example, in response to the if statement on the fourth line of the source code C100, the information processing apparatus stores L4 Position information is given.

The information processing apparatus generates an execution tree S100 shown in FIG. 3 based on the structure graph N100. Each node of the execution tree S100 is represented by a combination of the path constraint (upper column) and the variable state (middle column) described above, and further, position information (lower column) indicating the position via the source code is represented. ing. A root node (root node) S101 of the execution tree S100 corresponds to an initial state of execution of the source code. The information processing apparatus adds new nodes to the execution tree S100 each time a variable is updated as the source code is executed.

When generating the execution tree S100, the information processing apparatus assigns a symbol variable corresponding to the value of the variable that becomes the input variable of the function foo. The value of a variable serving as an input variable is a value of a variable that is given from outside the function and affects the operation of the function, and includes a function variable and a global variable that is accessed within the function.

In the illustrated source code C100, a function argument a and a global variable g are input variables. In this example, the information processing apparatus assigns “α” and “γ” to the variables a and g as symbolic variables.

The information processing apparatus generates a root node S101 in the execution tree S100 based on the node N1 of the structure graph N100. In this example, the information processing apparatus sets “no condition” indicating “no constraint” in the path constraint (upper column) S101a of the root node S101, and inputs variable a and g in the variable state (middle column) S101b. “A = α, g = γ” is set to indicate that symbol values α and γ are assigned respectively. Further, the position information L2 acquired from the node N1 is set in the position information (lower column) S101c.

The information processing apparatus executes processing based on the next node N2 on the control flow of the node N1 of the structure graph N100. The node N2 is a conditional branch node having two conditional control flows N21 and N22. The information processing apparatus includes a child node S102 corresponding to the conditional control flow N21 and a child node S105 corresponding to the conditional control flow N22. Are generated as child nodes of the node S101.

Since the conditional expression in the node N2 is “g == 0” and the variable state of the variable g in S101b is γ, the branch condition in the conditional control flow N21 can be expressed as “γ = 0”. Therefore, the path constraint (upper column) of the node S102 is set to “γ = 0” together with the path constraint “no constraint” in S101a.

The variable state (middle column) of the node S102 is set to be the same as the variable state S101b of the parent node S101 because the variable state is not changed by the if statement. In addition, the position information (lower column) is “L2, 4” by adding the position information (L4) of the node N2 to the position information S101c of the parent node S101, and the second and fourth lines of the source code. Means you have been through.

The branch condition in the conditional control flow N22 can be expressed as “￢ (γ = 0)” because the control flow N22 is a flow corresponding to the case where the condition of the if statement is not satisfied. Therefore, the path constraint (upper column) of the node S105 is set to “￢ (γ = 0)” together with the path constraint “no constraint” in S101a.

The variable state (middle column) in the node S105 is set to be the same as the variable state S101b of the parent node S101 because the variable state is not changed by the if statement. Further, the position information (lower column) is “L2, 4” by adding the position information (L4) of the node N2 to the position information S101c of the parent node S101.

The information processing apparatus executes processing based on N3 which is the next node on the control flow N21 of the node N2. The information processing apparatus generates a child node S103 of S102 as a node in the execution tree S100 corresponding to the node N3.

In node S103, since there is no conditional branch, the path constraint (upper column) is set the same as S102. Since the value 0 is substituted for the variable r at the node N3, “r = 0” is added to the variable state (middle column). In the position information (lower column), “L5” that is the position information of the node N3 is added to the position information in S102.

The information processing apparatus executes processing based on N5 which is the next node on the control flow of the node N3. A child node S104 of S103 is generated as a node in the execution tree S100 corresponding to the node N5. Since the node N5 corresponds to the return statement whose return value is the variable r, the variable state (in the middle column) is set to 0, which is the current value of the variable r, for the variable R representing the return value. The assigned “R = 0” is added. Since the execution of the function is terminated by the return statement, the information processing apparatus ends the generation of this branch in the execution tree S100, and shifts to generation of a branch that has not yet been generated.

The information processing apparatus executes processing based on N4 which is the next node on the control flow N22 of N2. The node N4 is a conditional branch node having two conditional control flows N41 and N42, and the information processing apparatus displays a child node S106 corresponding to the conditional control flow N41 and a child node S110 corresponding to the conditional control flow N42. , Respectively, under the node S105.

Since the conditional expression of the “if” statement at the node N4 is “a> 0” and the value corresponding to “a” is α from the variable state, the branch condition in the conditional control flow N41 is expressed as “α> 0”. Therefore, the path constraint (upper column) in S106 is “を (γ = 0) ∧ (α> 0)” which is the logical product of the path constraint “￢ (γ = 0)” and “α> 0” in S105. Set.

Hereinafter, the information processing apparatus repeats the above processing until the generation of all branches is completed for each branch.

In the process for the node N6, the information processing apparatus generates a child node S108 of the node S107. Node N6 updates the value of variable g to g-1. At this time, the value corresponding to the variable g is found to be γ from the variable state (middle column) in S107. Therefore, in the child node S108, the information processing apparatus updates the variable state (middle column) for the variable g to “g = γ−1”. In this way, for calculations involving symbolic variables, the variable state is retained in the form of an expression rather than a specific value.

The information processing apparatus finally obtains an execution tree S100 as shown in FIG. 3 from the structure graph N100 shown in FIG. 2 by the above processing. In symbol execution, child nodes corresponding to conditional branches are generated in the execution tree so that all possible control flows are covered.

It can be said that a leaf node in an execution tree is to obtain a set of a set of a condition (path constraint) for an input value of a source code and a state (variable state) of an output variable. In the following description, the leaf node of the execution tree at the time when the symbol execution is completed is referred to as “snapshot”, and the collection of snapshots is referred to as “symbol execution summary”. However, among the variables included in the variable state, local variables (including function arguments) are discarded when the function execution is completed, so the variable state of the local variable is excluded from the snapshot and symbol execution summary. .

The leaf nodes in the execution tree S100 are the three nodes S104, S109, and S113, which are snapshots, and these sets are the symbol execution summary S120. However, the variable states of variables r and a which are local variables are excluded.

In this example, the symbol execution is described using the source code written in the C language. However, the present invention is not limited to the C language, and can be similarly applied to the source code written using another programming language. .

Hereinafter, the configuration and processing of the source code equivalence verification apparatus 1000 according to the first embodiment will be described with reference to FIGS.

FIG. 4 shows the hardware configuration of the source code equivalence verification apparatus of this embodiment. The source code equivalence verification apparatus of the present embodiment is realized by a general computer as shown in FIG. 4, for example. The source code equivalence verification apparatus 1000 includes a CPU (Central Processing Unit) 101, a main storage device 102, a network I / F 103, a graphic I / F 104, an input / output I / F 105, and an auxiliary storage device I / F 106 connected by a bus. It has become a form.

The CPU 101 controls each part of the source code equivalence verification apparatus 1000, loads the source code equivalence verification program 200 to the main storage device 102, and executes it.

The main storage device 102 is usually composed of a volatile memory such as a RAM, and a program executed by the CPU 101 and data to be referenced are loaded from an auxiliary storage device or the like and stored.

The network I / F 103 is an interface for connecting to the external network 150.

The graphic I / F 104 is an interface for connecting a display device 120 such as an LCD (Liquid Crystal Display).

The input / output I / F 105 is an interface for connecting an input / output device. In the example of FIG. 4, a keyboard 131 and a mouse 132 as a pointing device are connected.

The auxiliary storage device I / F 106 is an interface for connecting an auxiliary storage device such as an HDD (Hard Disk Drive) 141 or a DVD (Digital Versatile Disk) drive device 142.

The HDD 141 has a large storage capacity, and stores a source code equivalence verification program 200 for executing the processing of this embodiment.

The DVD drive device 142 is a device that writes data to or reads data from an optical disk such as a DVD or a CD. The source code equivalence verification program 200 is provided by, for example, a CD-ROM. Can be installed.

The test data generation apparatus 1000 of the present embodiment installs the source code equivalence verification program 200 in the computer as described above and executes each function.

FIG. 5 shows a software configuration of the source code equivalence verification apparatus of the present embodiment. A source code equivalence verification program 200 executed by the source code equivalence verification apparatus 1000 includes a source code reading module 201, a structure graph generation module 202, a symbol execution calculation module 203, an equivalence verification expression generation module 204, and an equivalence verification expression verification. A module 205 and a verification result display module 206 are included.

The program equivalence verification program 200 is application software that runs on an OS (Operating System). The software configuration of the source code equivalence verification device includes an OS and a library program, but is omitted in FIG. .

The source code reading module 201 is a module that reads the pre-change source code and the post-change source code to be verified from the HDD or another computer and stores them in the storage unit.

The structure graph generation module 202 is a module that generates a structure graph (for example, N100 described above) by performing lexical analysis / syntactic analysis of a source code (for example, C100 described above) and extracting a control flow.

The symbol execution calculation module 203 performs symbol execution based on the structure graph generated by the structure graph generation module 202 to calculate an execution tree (for example, S100 described above), and collects the leaf nodes of the symbol execution summary (for example, for example, This module generates S120) described above.

The equivalence verification expression generation module 204 is a verification logical expression for determining equivalence between the symbol execution summary of the source code before change and the symbol execution summary of the source code after change generated by the symbol execution calculation module 203. This module generates a certain equivalence verification formula.

The equivalence verification formula verification module 205 is a module that solves the equivalence verification formula generated by the equivalence verification formula generation module 204 as a satisfiability problem in graph theory using a SAT (SAT fidelity) solver or an SMT (Satisfiability Modulo Theories) solver. It is.

The verification result generation module 206 is a module that generates a verification result report using the verification result, symbol execution summary, and source code information output from the equivalence verification expression verification module 205, and displays or notifies the verification result report.

FIG. 6 shows a functional configuration diagram of the source code equivalence verification apparatus 1000. The control unit 110 is realized by the CPU 101 and the main storage device 102 in FIG. 4, and the storage unit 140 is mainly realized by the HDD 141 in FIG. 4, but may include the main storage device 102. The input device 130 includes the input / output I / F 105, the keyboard 131, the mouse 132, and the like of FIG. 4, and may further include a configuration for reading from the DVD drive device 142 via the auxiliary storage device I / F 106. The output device 121 includes a graphic I / F 104, a display device 120, and the like, and may further include a configuration for writing to the DVD drive device 142 via the auxiliary storage device I / F 106. The communication unit 103 represents the network I / F 103 in FIG. 4 and is connected to, for example, an external computer 160 via the network 150. Details of the control unit 110 and the storage unit 140 of FIG. 6 will be described with reference to FIG.

FIG. 7 shows a configuration and a data flow in the control unit 110 and the storage unit 140 of the source code equivalence verification apparatus 1000. The source code input unit 111 reads the pre-change source code 301 and the post-change source code 302 to be verified, and stores them in the pre-change / post-change source code storage area 201.

In this embodiment, the pre-change source code 301 and the post-change source code 302 are described using an example described in C language. However, the structure graph generation unit 112 and the symbol execution calculation unit corresponding to other languages are also described. By using 113, it is also possible to use source code written in another programming language. Different programming languages may be used for the source code 301 before change and the source code 302 after change.

The structure graph generation unit 112 executes source code analysis of each of the pre-change source code and the post-change source code stored in the pre-change / post-source code storage area 201, and the pre-change structure graph which is the analysis result The post-change structure graph is stored in the pre-change / post-structure graph storage area 202.

The symbol execution calculation unit 113 performs symbol execution on each of the pre-change / post-structure graphs stored in the pre-change / post-structure graph storage area 202 for the post-change structure graph, and a symbol that is a calculation result (execution result) The execution summary is stored in the before / after symbol execution result storage area 203.

The equivalence verification expression generation unit 114 uses a logic for verifying equivalence of both before and after the change from the before / after change execution summary stored in the before / after change execution result storage area 203. An equivalence verification expression that is an expression is generated and stored in the equivalence verification expression storage area 204.

The equivalence verification formula verification unit 115 executes verification of the equivalence verification formula stored in the equivalence verification formula storage area 204 and stores the verification result of the verification formula in the equivalence verification formula result storage area 205.

The verification result generation unit 116 generates a verification result report 310 using information on the verification result of the equivalence verification formula, the symbol execution summary, and the source code, stores the verification result report 310 in the verification result storage area 206, and uses the output device 121. Displayed on the screen or transmitted to the external computer 160 using the communication unit 103.

As is clear from the above description, the operation of each unit included in the control unit 110 is realized by the source code equivalence verification apparatus 1000 executing each module of the source code equivalence verification program shown in FIG. .

FIG. 8 is a process flowchart of source code equivalence verification. An example will be described in which the pre-change source code C100 shown in FIG. 1 is input as the pre-change source code, and the post-change source code C200 shown in FIG.

The source code input unit 111 reads the pre-change source code 301 to be verified and stores it in the pre-change / post-source code storage area 201. (P110). The structure graph generation unit 112 performs source code analysis of the pre-change source code stored in the pre-change / post-change source code storage area 201, generates a pre-change structure graph as a result of the analysis, and before / after the change The data is stored in the structure graph storage area 202 (P120). The symbol execution calculation unit 113 executes symbol execution with respect to the pre-change structure graph stored in the pre-change / post-structure graph storage area 202, generates the execution result as the change issue execution summary, and displays the pre-change / post-change symbols. The result is stored in the execution result storage area 203 (P130).

Similarly, the process of the source code input unit 111 (P111), the process of the structure graph generation unit 112 (P121), and the process of the symbol execution calculation unit 113 (P131) are executed for the changed source code, and The symbol execution summary is stored in the before / after symbol execution result storage area 203.

Since the processing steps P110, P120, and P130 for the source code before the change and the processing steps P111, P121, and P131 for the source code after the change can be executed independently, they may be processed in parallel.

In addition, when processing is executed on the source code having the same content before, the structure graph generation and re-use can be performed by reusing the previous processing result stored in the pre-change / post-symbol execution result storage area 203. Symbolic execution calculations can be omitted.

The equivalence verification formula generator 114 generates an equivalence verification formula using the symbol execution summary of the source code before the change and the symbol execution summary of the source code after the change (P140). FIG. 9 shows a post-change source code C200 that is changed from the pre-change source code C100. FIG. 10 shows a symbol execution summary S220 generated from the changed source code C200. Using the symbol execution summary S120 shown in FIG. 3 generated from the source code C100 before change shown in FIG. 1 and the symbol execution summary S220 shown in FIG. 10 generated from the source code C200 after change shown in FIG. The generation of the expression will be specifically described.

∙ For each snapshot in the symbol execution summary, a snapshot constraint expression is generated by taking the conjunction of the path constraint and the equal sign condition of each variable state.

For example, for snapshots S104, S109, and S113, (γ = 0) ∧ (g = γ) ∧ (R = 0), ￢ (γ = 0) ∧ (α> 0) ∧ (g = γ), respectively. -1) Constraint expressions such as ∧ (R = α), ￢ (γ = 0) ∧￢ (α> 0) ∧ (g = γ-1) ∧ (R = -α) are generated. At this time, as described above, the equality constraint of the variable state for the variables r and a which are local variables is excluded.

Next, a symbol execution summary constraint expression is generated by taking a disjunction of each snapshot constraint expression. For example, the symbol execution summary constraint expression for the symbol execution summary S120 is {(γ = 0) ∧ (g = γ) ∧ (R = 0)} ∨ {￢ (γ = 0) ∧ (α> 0) ∧ (g = Γ−1) ∧ (R = α)} ∨ {￢ (γ = 0) ∧￢ (α> 0) ∧ (g = γ−1) ∧ (R = −α)}.

Similarly, the symbol execution summary constraint expression {(γ = 0) ∧ (g ′ = γ) ∧ (R ′ = 0)} ∨ {is also applied to the post-change symbol execution summary S220 generated from the changed source code. ￢ (γ = 0) ∧ (α <0) ∧ (g ′ = γ−1) ∧ (R ′ = − α)} ∨ {￢ (γ = 0) ∧￢ (α <0) ∧ (g ′ = γ−1) ∧ (R ′ = α)}. However, the output variables g and R in the changed symbol execution summary constraint expression are replaced with g ′ and R ′, respectively, in order to avoid a conflict with the variable name in the change execution summary constraint expression. Yes.

∙ When the source code before change and the source code after change are equivalent, the output variable becomes equal to any input variable, so the conjunction of equality constraints between corresponding output variables always holds. Accordingly, negation of this expression and change The above-mentioned symbol execution summary constraint expression and the post-change symbol execution summary constraint expression are taken together as an equivalence verification expression and stored in the equivalence verification expression storage area 204.

場合 If this equivalence verification formula is not satisfactory, it means that the output variable is equal to any input variable, so it is determined that both source codes are equivalent. Further, if it can be satisfied, it means that there are cases where the output variables are different, so it is determined that they are not equivalent.

In this example, (R = R ′) ∧ (g = g ′) is negated, and the modified sign execution summary constraint expression and the modified symbol execution summary constraint expression are joint statements of ￢ ((R = R ′ ) ∧ (g = g ′)) ∧ ((γ = 0) ∧ (g = γ) ∧ (R = 0) ∨￢ (γ = 0) ∧ (α> 0) ∧ (g = γ−1) ∧ (R = α) ∨￢ (γ = 0) ∧￢ (α> 0) ∧ (g = γ−1) ∧ (R = −α)) ∧ ((γ = 0) ∧ (g ′ = γ) ∧ (R ′ = 0) ∨￢ (γ = 0) ∧ (α <0) ∧ (g ′ = γ−1) ∧ (R ′ = − α) ∨￢ (γ = 0) ∧￢ (α <0) ∧ (g ′ = γ−1) ∧ (R ′ = α)) is an equivalence checking formula.

The equivalence verification formula verification unit 115 determines satisfiability of the equivalence verification formula generated by the equivalence verification formula generation unit 114 using a SAT solver, an SMT solver, or the like (P150). The equivalence verification formula verification unit 115 verifies whether the equivalence verification formula is satisfiable or not, and a counter example that is an example of a satisfiable variable value that is output if the equivalence verification formula is satisfiable. As a result, it is stored in the equivalence verification formula verification result storage area 205. In this example, since it is determined that the equivalence checking expression is unsatisfiable, it is stored as unsatisfiable.

The verification result generation unit 116 generates, for example, a verification result report 500 as shown in FIG. 11 based on the verification result by the equivalence verification formula verification unit 115 (P160). In the verification result report 500, as the verification result display 510, “equivalent” is displayed when the equivalence verification expression verification result cannot be satisfied, and “non-equivalent” when it can be satisfied. In this example, since the equivalence verification formula is stored as being unsatisfiable, the verification result 510 is displayed as “equivalent”.

Further, the verification result report 500 may include a display of the source code 521 before the change and the source code 522 after the change using the source code stored in the before / after source code storage area 201. Further, the verification result report 500 may include a display of the changed symbol execution summary 531 and the changed symbol execution summary 532 using the symbol execution summary information stored in the before / after symbol execution result storage area 203. . In the symbol execution summary displays 531 and 532 in FIG. 11, the path constraints and variable states are displayed in one line for each snapshot.

Next, regarding the source code equivalency verification process shown in FIG. 8, the change source code C100 shown in FIG. 1 as the source code before change is changed to the source code C100 shown in FIG. A case where the post source code C300 is input will be described as an example.

Each process of the control unit 110 is as described above, and an execution tree S300 and a symbol execution summary S320 as shown in FIG. 13 are generated from the changed source code C300 by the process (P131) of the symbol execution calculation unit 113. .

The symbol execution summary constraint expression corresponding to the symbol execution summary S320 is (γ = 0) ∧ (g ′ = γ) ∧ (R ′ = 0) ∨￢ (γ = 0) ∧ (α <0) ∧ (g ′ = γ + 1) ∧ (R ′ = − α) ∨￢ (γ = 0) ∧￢ (α <0) ∧ (g ′ = γ + 1) ∧ (R ′ = α).

Therefore, the equivalence verification formula generated by the equivalence verification formula generation processing step P140 is ￢ ((R = R ′) ∧ (g = g ′)) ∧ ((γ = 0) ∧ (g = γ) ∧ ( R = 0) ∨￢ (γ = 0) ∧ (α> 0) ∧ (g = γ−1) ∧ (R = α) ∨￢ (γ = 0) ∧￢ (α> 0) ∧ (g = γ −1) ∧ (R = −α)) ∧ ((γ = 0) ＝ (g ′ = γ) ∧ (R ′ = 0) ∨￢ (γ = 0) ∧ (α <0) ∧ (g ′ = γ + 1) ∧ (R ′ = − α) ∨￢ (γ = 0) ∧￢ (α <0) ∧ (g ′ = γ + 1) ∧ (R ′ = α)).

The valence verification formula verification unit 115 determines whether the above equivalence verification formula is satisfiable by using a SAT solver or the like, for example, α = 1, γ = 1, R = 1, g = Since counterexamples of 0, R ′ = 1, and g ′ = 2 are obtained, these are stored as verification results.

The verification result generation unit 116 generates a verification result report 550 as shown in FIG.

In the verification result report 550, since the equivalence verification formula verification result can be satisfied, “not equivalent” is displayed as the verification result display 560. Moreover, the display of the source code 571 before the change and the source code 572 after the change and the display of the changed code execution summary 581 and the changed symbol execution summary 582 may be included.

Furthermore, the verification result report 550 may include a display of counterexample information 590 that is not equivalent using counterexample information stored in the equivalence verification formula verification result storage area 205.

In the counterexample information 590, the counterexample is classified into an input variable, an output variable of the source code before change, and an output variable of the source code after change, and a value obtained as a counterexample is displayed. Variables having different values between the output variable before change and the output variable after change may be highlighted by underlining. By this display, the developer can know the value of the input variable that is specifically unequal, and the value of the output variable before and after the change at that time.

A specific example of the processing of the source code equivalence verification apparatus according to the second embodiment will be described with reference to FIGS. In this embodiment, the equivalence (referred to as path equivalence) between when a specific path of the source code before the change and the specific path of the source code after the change is taken is a combination of all paths. Equivalence verification is realized by verifying against.

An example will be described in which the pre-change source code C100 shown in FIG. 1 is input as the pre-change source code, and the post-change source code C300 shown in FIG. 12 is input as the post-change source code that is a non-equivalent change to C100.

In this embodiment, the processes of the source code input unit 111, the structure graph generation unit 112, and the symbol execution calculation unit 113 are the same as those in the first embodiment, and a description thereof is omitted.

FIG. 15 is a processing flowchart of the equivalence verification expression generation unit 114 in this embodiment. The equivalence verification formula generation unit 114 acquires the symbol execution summary of the source code before the change from the pre-change / post-symbol execution result storage area 203 (P141). If there is no unprocessed snapshot before change (P142), the equivalence verification expression generation unit 114 ends the process.

The equivalence verification expression generation unit 114 selects one snapshot from the pre-change execution summary (P143), and acquires the post-change symbol execution summary from the pre-change / post-code execution result storage area 203 (P144). If there is no unprocessed snapshot after change (P145), the equivalence verification expression generation unit 114 returns to P142. The equivalence verification formula generation unit 114 selects one snapshot of the post-change symbol execution summary (P146), generates a path equivalence verification formula (step P147), and returns to P145. If there is no unprocessed pre-change snapshot (P145), the equivalence verification formula generation unit 114 returns to P142, and therefore generates a path equivalence verification formula for all combinations of the pre-change snapshot and the post-change snapshot. it can.

The equivalence verification expression generation unit 114 generates a path equivalence verification expression for verifying equivalence in the range that has passed through the path corresponding to the snapshot, for the selected pre-change snapshot and post-change snapshot. It is generated and stored in the equivalence verification formula storage area 204 (P147).

The path equivalence verification expression consists of the negation expression of the conjunction of the equality constraint expression between the corresponding output variables, the snapshot constraint expression of the selected before-change snapshot, and the snapshot constraint expression of the selected after-change snapshot. It becomes the conjunction of

For example, when the snapshot S104 in the change execution summary S120 and the snapshot S321 in the post-change symbol execution summary S320 are selected, the path equivalence verification formula is ￢ ((R = R ′) ∧ (g = g ′ )) ∧ ((γ = 0) ∧ (g = γ) ∧ (R = 0)) ∧ ((γ = 0) ∧ (g ′ = γ) ∧ (R ′ = 0)).

In the example described above, the equivalence verification expression generation unit 114 selects one snapshot at a time and generates a path equivalence verification expression. The equivalence verification expression generation unit 114 may select a plurality of snapshots at a time. In that case, the selection of the snapshot constraint formula corresponding to the selected snapshot is used instead of the snapshot constraint formula used to generate the path equivalence verification formula.

In the example described above, the equivalence verification expression generation unit 114 that generates the path equivalence verification expression starts processing after the processing of the symbol execution calculation part 113 is completed. When the generation of a part of the snapshot is completed during execution of the above, even if the processing of the equivalence verification expression generation unit 114 is started to generate a path equivalence verification expression for the combination related to the snapshot good.

The equivalence verification formula verification unit 115 determines satisfiability using a SAT solver or the like for each of the plurality of path equivalence verification formulas generated by the equivalence verification formula generation unit 114. The equivalence verification formula verification unit 115 is an example of the result of whether each path equivalence verification formula is satisfiable or not, and the value of a variable that the solver outputs if it can be satisfied. A counterexample is recorded in the equivalence verification expression verification result storage area 205.

FIG. 16 shows a verification result 700 of each path equivalence verification formula in this example. Of the nine combinations of the pre-change snapshot and the post-change snapshot, six are unsatisfactory. Further, the remaining three patterns can be satisfied, and for example, a counter example as shown in the counter example column of FIG. 16 can be obtained.

In the verification result generation step P160, the verification result generation unit 116 generates a verification result report 600 as shown in FIG.

In the verification result report 600, the verification result display 610 shows “equivalent” when all path equivalence verification expression verification results are unsatisfiable and “non-existence” when there is a satisfiable path equivalence verification expression. “Equivalent” is displayed. In this example, for example, “not equivalent” is displayed because the path equivalence verification formula when the snapshot S113 and the snapshot S322 are selected can be satisfied.

The verification result report 600 may include the display of the change issue execution summary 631 and the post-change symbol execution summary 632 using the symbol execution summary information stored in the pre-change / post-change symbol execution result storage area 203. At this time, the snapshot verification result 639 can be displayed.

The verification result 639 of the snapshot refers to the verification result 700 of each path equivalence verification expression. If all the verification results of the path equivalence verification expression that selected the snapshot are unsatisfiable, “equivalent” can be satisfied. If there is a valid path equivalence verification expression, “not equivalent” is displayed.

In this example, since all the path equivalence verification expressions that select the snapshot S104 and all the path equivalence verification expressions that select the snapshot S321 cannot be satisfied, the corresponding verification result is “Equivalent” is displayed. On the other hand, other snapshots are displayed as “non-equivalent” because they include a satisfying path equivalence verification formula.

The verification result report may include a display of counterexample information 640 that is non-equivalent using counterexample information stored in the equivalence verification formula verification result storage area 205. At this time, a check box 638 for selecting a snapshot may be provided while the symbol execution summary is displayed, and a counter-example of the path equivalence verification formula for the selected combination of snapshots may be displayed.

In the example illustrated in FIG. 17, when the check boxes corresponding to the snapshot S113 and the snapshot S322 are selected, the path equivalence verification formula generated from the snapshot S113 and the snapshot S322 illustrated in FIG. Displayed information is displayed.

The verification result report 600 may further include a display of the pre-change source code 621 and the post-change source code 622 using the source code stored in the pre-change / post-source code storage area 201. At this time, for the snapshot selected using the check box 638 for selecting a snapshot, the path of the snapshot may be displayed on the source code from the position information of the snapshot.

In the example shown in FIG. 17, the path of the snapshot S113 is displayed as an underline on the source code 621 before the change using the position information of the snapshot S113. Further, the path of the snapshot S322 is displayed as an underline on the changed source code 622 using the position information of the snapshot S322.

As a method of displaying the route, in addition to the method of displaying with the underline shown in FIG. 17, the background is displayed in a different color, the font is highlighted by changing the font or character size, and the display other than the route is deleted. Then, there is a method such that only the route is displayed.

When investigating the cause of non-equivalence of the equivalence verification results for a combination of snapshots and investigating the cause of non-equivalence, the cause exists on the path of the snapshot, and the location other than the path is the result of the snapshot. There is no need to investigate because there is no impact.

The path corresponding to the selected snapshot is displayed on the source code, and the counter example corresponding to the combination of them is displayed. It becomes possible to narrow down the range to be investigated, and it becomes easy to find the cause that is not equivalent.

FIG. 18 shows an example of display when a plurality of snapshots are selected in the check box 638 for selecting a snapshot in the verification result report 600. When a plurality of snapshots are selected, there are a plurality of snapshot paths. Therefore, a radio button 650 for selecting a display method for a plurality of snapshot paths can be provided, and the paths can be displayed according to the display method selected there.

As the snapshot path display method 650, “common” and “merger” are prepared. When “common” is selected, only a portion through which all the selected snapshots pass is displayed as a route. When “Merger” is selected, a portion through which at least one of the selected snapshots passes is displayed as a route.

In the example shown in the changed source code 622 in FIG. 18, snapshots S322 and S323 which are non-equivalent snapshots are selected, and “common” is selected as the display method. Therefore, only the part where both snapshots pass is displayed as a route.

In general, when equivalence verification results are unequal for multiple snapshots, the possibility of inequality due to the same factor is higher than the possibility of inequality due to individual causes. Is expensive. In the case of non-equivalence due to the same cause, the cause exists in the common part of the paths of a plurality of snapshots. Therefore, by displaying the common part of the path, it is possible to narrow down the range that the developer should investigate on the source code.

In the example of FIG. 18, only the processing of g = g + 1 on the sixth line is performed except for the condition evaluation and the return statement in the displayed route. In fact, it is possible to obtain an equivalent change by correcting this line to g = g-1, and by displaying a common path, the developer can narrow down the investigation range necessary for the correction. It has become.

As a method of displaying a plurality of snapshot paths, in addition to the method of displaying the common part and the merged range shown in FIG. 18, the color density is changed according to the number of snapshots that pass through, or There are methods to change the character size.

A specific example of processing of the source code equivalence verification apparatus of the present embodiment will be described with reference to FIG.

The equivalence verification formula generation unit 114 compares the equivalence verification formula generated in the first embodiment (referred to as an overall equivalence verification formula in the description of this embodiment) with the path equivalence verification formula generated in the second embodiment. Then, the number of terms in each path equivalence verification formula is smaller than the number of terms in the overall equivalence verification formula, and the amount of calculation is also small, so the verification time in the solver is also shortened. On the other hand, the total calculation amount of all the path equivalence verification formulas is larger than the calculation amount of the overall equivalence verification formulas.

In the present embodiment, using these features, the source code equivalence verification apparatus 1000 executes a combination of verification based on the overall equivalence verification formula and verification based on the path equivalence verification formula.

In this embodiment, it is assumed that the source code equivalence verification apparatus 1000 has a plurality of CPUs 101 or CPU cores and can execute a plurality of calculations simultaneously in parallel. Instead of performing parallel calculation with a plurality of CPU cores, parallel calculation may be realized by using an external computer 160 in a cloud computing environment or a grid computing environment through the external network 150.

FIG. 15 is a process flowchart in process step P140 of the equivalence verification expression generation unit 114 in the present embodiment. The details are shown in FIG. In acquisition step P141 of the change previous execution summary, the equivalence verification formula generation unit 114 acquires the symbol execution summary of the source code before change from the pre-change / post-symbol execution result storage area 203 (P141).

In this embodiment, the processes of the source code input unit 111, the structure graph generation unit 112, and the symbol execution calculation unit 113 are the same as those in the first embodiment, and a description thereof is omitted. Further, the equivalence verification formula generation unit 114 of the present embodiment executes both the equivalence verification formula generation unit 114 shown in the first embodiment and the equivalence verification formula generation unit 114 shown in the second embodiment. Then, both the overall equivalence verification formula and the path equivalence verification formula are stored in the equivalence verification formula storage area 204.

FIG. 19 is an example of a processing flowchart of the equivalence verification formula verification unit 115 in the present embodiment. The equivalence verification formula verification unit 115 starts verification of the overall equivalence verification formula (P201).

The equivalence verification expression verification unit 115 determines whether or not there remains an expression that has not yet been verified among the path equivalence verification expressions (P202). Transition.

The equivalence verification formula verification unit 115 determines whether there is a free CPU core in order to newly start verification of the path equivalence verification formula (P203). To do.

The equivalence verification formula verification unit 115 selects one of the path equivalence verification formulas that have not yet been verified (P204). The equivalence verification formula verification unit 115 starts verification of the selected path equivalence verification formula on an available CPU core (P205), and proceeds to P206.

The equivalence verification formula verification unit 115 subsequently determines the end of verification of each equivalence verification formula that has started verification. The equivalence verification formula verification unit 115 determines whether or not the verification of the overall equivalence verification formula has been completed (P206). If the verification is complete, the process proceeds to P207. If not, the process proceeds to P208.

The equivalence verification formula verification unit 115 determines whether the verification result of the overall equivalence verification formula is unsatisfactory (P207). If it cannot be satisfied, the equivalence verification result is “equivalent”, so there is no need to continue the verification of the path equivalence verification formula, and the equivalence verification formula verification unit 115 ends the processing.

If the verification result is satisfiable, the equivalence verification result is “non-equivalent”, but the equivalence information in snapshot units cannot be obtained only by the verification result of the overall equivalence verification formula. Therefore, the equivalence verification formula verification unit 115 proceeds to P208 and continues to verify the path equivalence verification formula.

The equivalence verification expression verification unit 115 determines whether there is a path equivalence verification expression that has been newly verified (P208). If there is, the process proceeds to P209, and if not, the process proceeds to P211.

The equivalence verification formula verification unit 115 determines whether the verification result of the path equivalence verification formula that has been newly verified is satisfiable (P209). If the verification result is satisfiable, the process proceeds to P210 and cannot be satisfied. If not, the process proceeds to P211.

The equivalence verification formula verification unit 115 generates a partial verification result report (P210). This process (P210) is executed when a new “non-equivalent” snapshot combination is discovered.

The partial verification result report is generated by the same method as the processing of the verification result generation unit 116 described in the second embodiment, using the completed path equivalence verification expression verification result. By using this partial verification result report, before the verification of all path equivalence verification expressions is completed, the developer can know the combination of snapshots that are not equivalent and the path of those snapshots. It becomes.

In step P211, the equivalence verification formula verifying unit 115 determines whether or not the verification of all the path equivalence verification formulas has been completed (P211).

If there is a verification formula that has not been completed (including verification formulas that have not yet started), the equivalence verification formula verification unit 115 proceeds to P202 and starts or ends verification of a new path equivalence verification formula. Repeat the waiting process.

As a method for selecting one of the path equivalence verification formulas that have not yet started verification in P204, a method for selecting a verification formula with a small number of terms in the path equivalence verification formula, or a method used in the formula is used. There is a method of selecting a verification formula with a small number of types of variables. These have the effect that the verification of many verification formulas can be completed in a short time by executing the verification formulas that have a high possibility of shortening the verification time first.

As another selection method, there is a method of selecting a path equivalence verification formula relating to a snapshot passing through a corrected location on the source code. This is because snapshots that go through the modified part are likely to be unequal, and by verifying this first, it is possible to present a snapshot that is unequal to the developer at an earlier timing. There is an effect.

As a modification of the present embodiment, verification using the overall equivalence verification formula can be omitted. Specifically, P201, P206, and P207 can be omitted from the processing steps shown in FIG.

This is because the verification of each path equivalence verification expression is performed when it is predicted that the verification result is likely to be non-equivalent, and before the verification of the entire equivalence verification expression is completed. When it is expected to end, verification of the entire equivalence verification formula that is unnecessary as a result is omitted, and the amount of calculation can be reduced.

As another modification of the present embodiment, partial verification result generation can be omitted. Specifically, P208, P209, and P210 can be omitted from the processing steps shown in FIG.

This is useful if you do not need to quickly show non-equivalent parts to the developer, and if you want to display partial verification results and avoid correcting places other than those that should be corrected. This has the effect of reducing the amount of calculation for generating the verification result.

Note that the present invention is not limited to the first to third embodiments described above, and includes various modifications. For example, the above-described embodiments have been described in detail for easy understanding of the present invention, and are not necessarily limited to those having all the configurations described. Further, a part of the configuration of a certain embodiment can be replaced with another embodiment, and the configuration of another embodiment can be added to the configuration of a certain embodiment. Further, it is possible to add, delete, and replace other configurations for a part of the configuration of each embodiment. Each of the above-described configurations, functions, processing units, processing means, and the like may be realized by hardware by designing a part or all of them with, for example, an integrated circuit.

DESCRIPTION OF SYMBOLS 1000 ... Source code equivalence verification apparatus, 101 ... CPU, 102 ... Main storage device, 103 ... Network I / F, 105 ... Input / output I / F, 106 ... Auxiliary storage device I / F, 110 ... Control part, 120 ... Display / output device 130 ... Input device 140 ... Storage unit 150 ... External network 160 ... External computer 200 ... Source code equivalence verification program 201 ... Before / after source code storage area 202 ... Before change / Post structure graph storage area, 203 ... Pre-change / post symbol execution result storage area, 204 ... Equivalence verification expression storage area, 205 ... Equivalence verification expression verification result storage area, 206 ... Verification result storage area, 111 ... Source code input , 112... Structure graph generation unit, 113... Symbol execution calculation unit, 114... Equivalence verification expression generation unit, 115. ... verification result generation unit, 301 ... source code before change, 302 ... source code after change, 310 ... verification result report, S100, S200, S300 ... execution tree for symbol execution, S120, S220, S320 ... symbol execution summary, S104, S109, S113, S321 to S323 ... Snapshot in symbol execution, 500, 550, 600 ... Verification result report.

Claims (12)

Symbol execution calculation unit (113) for performing symbol execution calculation on the source code before change and the source code after change obtained by changing the source code before change,
Based on the symbol execution summary, which is the symbol execution calculation result of the symbol execution calculation unit, the equivalence that the same output is obtained for the same input of the source code before change and the source code after change is verified. An equivalence verification expression generation unit for generating an equivalence verification expression for
An equivalence verification formula verification unit that verifies the equivalence verification formula generated by the equivalence verification formula generation unit, and a verification result generation unit that generates a verification result report using the verification result in the equivalence verification formula verification unit A source code equivalence verification apparatus comprising: The source code equivalence verification apparatus according to claim 1, wherein the equivalence verification expression generation unit is configured to perform a combination of snapshots constituting the symbol execution summary of the pre-change source code and the post-change source code. An equality constraint between output variables corresponding to the source code before the change and the source code after the change, the snapshot constraint formula of the snapshot of the source code before the change, and the snapshot of the snapshot of the source code after the change A source code equivalence verification apparatus that generates a path equivalence verification expression including a snapshot constraint expression. The source code equivalence verification apparatus according to claim 2, wherein the verification result generation unit includes a path corresponding to the snapshot of the pre-change source code and the post-change source code for the snapshot combination. A source code equivalence verification apparatus that generates a verification result report that displays a counterexample when a verification result of a path and the path combination by the equivalence verification expression verification unit is not equivalent. 4. The source code equivalence verification apparatus according to claim 3, wherein when a plurality of the snapshots are selected, the verification result generation unit includes a common part and a merged part of the path paths corresponding to the snapshots. A verification result report for displaying one of the above, a source code equivalence verification device. The source code equivalence verification apparatus according to claim 2, wherein the equivalence verification expression verification unit passes through a specific path of the source code before change and a specific path of the source code after change. A path equivalence verification expression for verifying equivalence between and a source code equivalence verification apparatus for verifying the equivalence verification expression in parallel. In the source code equivalence verification apparatus according to claim 5, according to the end of verification of the equivalence verification expression and the verification expression of the path equivalence verification expression verified in parallel by the equivalence verification expression verification unit, A source code equivalence verification apparatus that generates the verification result report. A source code equivalence verification method in a source code equivalence verification apparatus, wherein the source code equivalence verification apparatus includes:
Symbol execution calculation is performed on the source code before change and the source code after change after changing the source code before change,
Equivalence for verifying equivalence that the same output is obtained for the same input of the source code before change and the source code after change based on the symbol execution summary that is the result of the symbol execution calculation Generate a validation expression
Validate the generated equivalence verification formula,
A source code equivalence verification method, wherein a verification result report is generated using the verification result. 8. The source code equivalence verification method according to claim 7, wherein the source code equivalence verification apparatus is configured for each combination of snapshots constituting the symbol execution summary of the pre-change source code and the post-change source code. , An equality constraint expression between output variables corresponding to the source code before change and the source code after change, a snapshot constraint expression of the snapshot of the source code before change, and the snapshot of the source code after change A source code equivalence verification method, comprising: generating a path equivalence verification formula including the snapshot constraint formula. 9. The source code equivalence verification method according to claim 8, wherein the source code equivalence verification apparatus corresponds to the snapshot of the pre-change source code and the post-change source code for the combination of snapshots. A source code equivalence verification method, comprising: generating a verification result report that displays a counterexample when a verification result for a path and a combination of paths is not equivalent. The source code equivalence verification method according to claim 9, wherein when the plurality of snapshots are selected, the source code equivalence verification device is configured to share a common part of the path of the path corresponding to each snapshot. And generating the verification result report displaying one of the merged portions. 9. The source code equivalence verification method according to claim 8, wherein the source code equivalence verification device passes through a specific path of the pre-change source code and a specific path of the post-change source code. A path equivalence verification formula for verifying equivalence between and a source code equivalence verification method, wherein the equivalence verification formula is verified in parallel. The source code equivalence verification method according to claim 11, wherein the source code equivalence verification apparatus is configured to verify in parallel the verification of the equivalence verification expression and the verification expression of the path equivalence verification expression in parallel. A method for verifying source code equivalence, wherein the verification result report is generated.

Images