JP2018190219A - Software specification analysis apparatus and software specification analysis method - Google Patents

Abstract

PROBLEM TO BE SOLVED: To improve the efficiency of software specification analysis. SOLUTION: A specification analyzer generates a path condition and a path execution result by executing a symbol in a part other than the loop statement of the source code, executes the symbol for the loop statement, and executes the loop statement n-1. Generates the path information in the generalized loop, which is the relational expression between the value of the variable after executing the loop statement n times and the value of the variable after executing the loop statement n times, and only any number of the path information in the specialized loop. By acquiring the first specialized loop path information including the value of the variable when the loop is executed and applying the generalized loop path information to the first specialized loop path information, the first feature Generates a second in-specialized loop path information that has one more loop count than the in-loop path information, and based on the second in-loop path information and the out-of-loop path information, software specifications (rules). Generate information about. [Selection diagram] Fig. 1

Description

  The present invention relates to a software specification analysis apparatus and a software specification analysis method.

  Patent Document 1 states that “from a program to be analyzed, a repeated control variable is changed to search for a specific case and a repeated block that matches a pattern of performing a specific process in the specific case is extracted and analyzed. In the target program, the extracted repeated block and the block immediately following the repeated block are subjected to specific processing when true, and the processing of the immediately following block is performed when false, and the predicate function relating to the true or false When a logical constraint is generated for the predicate function included in the bifurcated structure, and when the upper descriptive function is detected during symbolic execution of the converted program, A path condition at the position where the predicate function appears is generated from the logical constraints associated with the predicate function. Is described as additional registration to "in the management data Rick execution unit.

Japanese Unexamined Patent Publication No. 2011-191985 C.L. Liu, written by Hiroshi Narishima / Jin Akiyama, Introduction to Discrete Mathematics for Computer Science, McGraw-Hill Book, Inc., 1986

  Patent Document 1 states that “in symbolic execution, all possible execution paths in a conditional branch are automatically generated to enable comprehensive execution of a program. However, due to its completeness, a combined explosion occurs. There is a possibility, and in particular, the above mechanism solves the above problem for the problem that it generates a lot of combinations that are not necessary in symbolic execution due to algorithms specific to the implementation language, and repeats useless searches. I am trying.

  However, in Patent Document 1, a loop statement for retrieving specific data from an array is replaced with an equivalent conditional branch statement, and a source including a loop statement other than a loop statement for retrieving specific data from an array It cannot be applied when extracting rules from code.

  The present invention has been made in view of such a background, and an object of the present invention is to provide a software specification analysis apparatus and a software specification analysis method that contribute to efficiency improvement of software specification analysis.

One aspect of the present invention for achieving the above object is an apparatus for analyzing software specifications, which is included in a storage unit that stores a source code of a program that realizes software to be analyzed, and the source code. A loop statement that is information including a pass condition and a pass execution result of the source code by performing symbol execution on the description of the source code other than the specified loop statement Out-of-loop symbol execution unit that generates outer path information using the value of the variable before execution of the loop statement and the value of the variable after execution of the loop statement, and symbol execution for the identified loop statement For each variable included in the source code, the value of the variable after the loop statement is executed n-1 times and the rule A generalized loop path information that is information indicating a relationship with the value of the variable after n times of execution of the loop statement, and an in-loop symbol execution unit, and the source code when the loop is executed a specific number of times When the loop is executed an arbitrary number of times in the in-loop path specialization unit that generates path information in the special loop that is information on the path, and in the special loop inside path information generated by the in-loop path specialization unit The first special loop is obtained by acquiring first special loop path information including the value of the variable in and applying the general loop path information to the first special loop path information. The second specialized loop path information having a loop count one greater than the inner path information is generated, and the software specification is expressed based on the second specialized loop path information and the out-of-loop path information. Rule generator for generating a rule information is information including a Lumpur, comprising a.

  In addition, the subject which this application discloses, and its solution method are clarified by the column of the form for inventing, and drawing.

  According to the present invention, it is possible to efficiently analyze software specifications.

It is a functional block diagram of the specification analyzer of a 1st embodiment. It is an example of the hardware used for implementation | achievement of a specification analyzer. This is an example of source code. It is an example of an out-loop path search tree. It is an example of out-of-loop symbol execution information. It is an example of out-of-loop symbol execution information. It is an example of path information outside a loop. It is an example of a path search tree in a loop. It is a flowchart explaining the symbol execution process in a loop. It is an example of the symbol execution information in a loop. It is an example of the path information in generalization loop. It is a flowchart explaining the path specialization process in a loop. (A), (b) is an example of path information in the special loop where the number of loops is zero. It is an example of path information in a special loop with one loop. It is a flowchart explaining a rule production | generation process. It is an example of a rule when the number of loops is 0. It is an example of a rule when the number of loops is one. It is an example of a rule when the upper limit number of loops is specified as 1. It is a functional block diagram of the specification analyzer of 2nd Embodiment. This is an example of source code. It is an example of an out-loop path search tree. It is an example of out-of-loop symbol execution information. It is an example of out-of-loop symbol execution information. It is an example of path information outside a loop. It is an example of a path search tree in a loop. It is an example of the symbol execution information in a loop. It is an example of the path information in generalization loop. It is an example of the path information in generalization loop. It is an example of generalization rule information. It is an example of a generalization rule display screen. It is an example of the designation | designated screen of a loop upper limit frequency | count.

  Hereinafter, embodiments will be described with reference to the drawings. In the following description, the same or similar components may be denoted by the same reference numerals and redundant description may be omitted.

[First Embodiment]
FIG. 1 shows a functional block diagram of a software specification analyzer (hereinafter referred to as a specification analyzer 100) described as the first embodiment. The specification analysis apparatus 100 generates information related to the software specifications (hereinafter also referred to as rule information 157) by performing symbol execution on the source code 151 of the program that implements the software to be analyzed.

In symbol execution, an argument passed to a parameter of the source code is represented by a symbol value, and processing of the source code is executed on the symbol value. At this time, for each execution path of the source code, information (hereinafter, also referred to as a path condition) indicating what value the symbol value is to execute is acquired. In addition, as a result of executing the pass, finally, a value held by each variable (hereinafter also referred to as a pass execution result) is acquired. Note that the symbol value may also appear in the pass execution result. The combination of the path condition and the path execution result indicates a condition for executing the path and a result when the path is executed, and can be expressed in an IF-THEN rule format. Such an IF-THEN relationship is also called a rule. A set of rules generated by searching all paths of the source code 151 corresponds to the specification of the source code.

  Here, the source code is a description related to loop processing (for example, when the source code is described in C language, a description block such as a while statement, a do statement, a for statement, etc. Hereinafter, a description block related to the loop processing is referred to as a loop statement. ). If the source code contains a loop statement, symbol execution is a loop statement that does not execute the loop statement once, a path that executes the loop statement only once, a path that executes the loop statement only twice, and so on. A path is generated for each execution. For example, if there is a possibility of executing a loop statement four times at the maximum, the path when the loop statement is executed 0 times, the pass 1 time, the pass 2 times, the pass 3 times A total of five paths, that is, four paths, are generated. Now consider the case where the loop condition of the loop statement depends on the argument. As described above, in symbol execution, an argument passed to a parameter is represented by a symbol value. Therefore, when the loop condition depends on the argument, the symbol value appears in the loop condition. This symbol value has no actual value, and it may not be possible to determine whether the loop condition including the symbol value is satisfied or not, and also determine how many times the loop statement may be executed. I can't.

  If the maximum number of executions of the loop statement cannot be determined in this way, the number of paths to be searched becomes infinite, and the symbol execution process cannot be terminated. As a method for avoiding this problem, for example, there is a method in which an upper limit number of loop statements is set in advance and the loop is escaped when the loop number exceeds the upper limit number. According to this method, the number of paths to be searched can be limited.

However, for example, when the upper limit number of loops is set to L times, it is necessary to repeat symbol execution L times for a loop sentence when searching for a path when the L loops are executed. Therefore, for example, when the number of steps of a loop sentence is large, a lot of resources are consumed by symbol execution, and the time until acquiring a rule representing a specification also becomes long.

  Further, when the upper limit number is smaller than the actual maximum number of executions of the loop, rule extraction omission occurs. For example, when a symbol statement is executed with the upper limit set to 3 for a loop statement with an actual maximum execution count of 5, the rule for the loop statement execution count of 4 and the case of 5 Cannot extract rules.

  For the above reasons, when the target source code includes a loop statement, the user needs to determine whether or not there is a rule extraction omission. If it is determined that there is omission of rule extraction, the user increases the upper limit number of loops and executes the symbol again. As described above, when a rule is extracted from a source code including a loop sentence, the upper limit number of times must be changed and a plurality of symbol executions must be performed, and the user is forced to perform complicated work. The specification analyzing apparatus 100 according to the present embodiment solves such problems that occur when analyzing software specifications by symbol execution.

  As shown in FIG. 1, the specification analyzing apparatus 100 includes an information storage unit 110, a loop sentence specifying unit 111, an out-loop symbol executing unit 112, an in-loop symbol executing unit 113, an in-loop path specializing unit 114, and a rule generating unit 115. And an input / output processing unit 116. In addition to these functions, the specification analysis apparatus 100 may include, for example, an operating system, a device driver, a DBMS (DataBase Management System), and the like.

  FIG. 2 shows an example of hardware (information processing apparatus 50) used for realizing the specification analysis apparatus 100. The information processing device 50 includes each configuration of a processor 51, a main storage device 52, an auxiliary storage device 53, an input device 54, an output device 55, and a communication device 56. These are communicably connected to each other via a communication means such as a bus. In addition, you may implement | achieve all or one part of the information processing apparatus 50 using virtual resources, such as a cloud server in a cloud system, for example.

  The processor 51 is configured using, for example, a CPU (Central Processing Unit), an MPU (Micro Processing Unit), a GPU (Graphics Processing Unit), a DSP (Digital Signal Processor), and the like. The processor 51 reads out and executes a program stored in the main storage device 52, thereby realizing all or part of the functions of the specification analysis device 100. The main storage device 52 is, for example, a ROM (Read Only Memory), a RAM (Random Access Memory), a nonvolatile semiconductor memory (NVRAM (Non Volatile RAM)), etc., and stores programs and data.

  Each of the above functions provided in the specification analysis apparatus 100 is realized by, for example, the processor 51 reading and executing a program stored in the main storage device 52 or the auxiliary storage device 53. These functions are realized by, for example, hardware (FPGA (Field-Programmable Gate Array), ASIC (Application Specific Integrated Circuit), etc.) provided in the specification analysis apparatus 100.

The auxiliary storage device 53 is, for example, a hard disk drive, SSD (Solid State Drive)
), Optical storage devices (CD (Compact Disc), DVD (Digital Versatile Disc), etc.), storage systems, IC cards, SD memory cards, and data reading / writing devices for recording media such as optical recording media is there. Programs and data stored in the auxiliary storage device 53 are loaded into the main storage device 52 as needed. The auxiliary storage device 53 may have a configuration independent of the specification analysis device 100, such as a network storage.

  The input device 54 is an interface that accepts input of data from the outside. For example, a data reading device from a recording medium (nonvolatile memory, optical recording medium, magnetic recording medium, magneto-optical recording medium, etc.), keyboard, Mouse, touch panel, etc. For example, the specification analysis device 100 may be configured to receive data input from another device via the communication device 56.

The output device 55 is a user interface that provides data and information such as processing progress and processing results to the outside. For example, a screen display device (liquid crystal display, projector, graphic card, etc.), printing device, recording For example, a recording device for recording data on a medium. For example, the specification analysis device 100 may provide data such as processing progress and processing results to other devices via the communication device 56.

  The communication device 56 is a wired or wireless communication interface that realizes communication with other devices and elements, and is, for example, a NIC (Network Interface Card), a wireless communication module, or the like.

  Returning to FIG. 1, among the functions described above, the information storage unit 110 includes the source code 151, out-of-loop symbol execution information 152, out-of-loop path information 153, in-loop symbol execution information 154, generalized in-loop path information 155, special information. In-loop path information 156 and rule information 157 are stored. The information storage unit 110 manages these pieces of information using, for example, a file system or a DBMS.

  The loop sentence specifying unit 111 specifies (extracts) a loop sentence from the description of the source code 151. For example, the specification analysis apparatus 100 acquires the source code 151 from the user, another information processing system, or the like via the input device 54 or the communication device 56.

  The out-of-loop symbol executing unit 112 performs symbol execution on the description other than the loop statement specified by the loop statement specifying unit 111 (hereinafter also referred to as “out-of-loop description”) in the source code 151, thereby obtaining out-of-loop path information 153. Generate. The out-of-loop symbol execution unit 112 manages various types of information used when performing symbol execution as out-of-loop symbol execution information 152, and refers to the out-of-loop symbol execution information 152 as appropriate when executing the above symbol execution. Details of the out-of-loop symbol execution information 152 and the out-of-loop path information 153 will be described later.

  The in-loop symbol execution unit 113 generates the generalized in-loop path information 155 by performing symbol execution on the loop statement (hereinafter also referred to as “in-loop description”) specified by the loop statement specifying unit 111. The in-loop symbol execution unit 113 manages various types of information used when performing symbol execution as the in-loop symbol execution information 154, and appropriately refers to the in-loop symbol execution information 154 when executing the symbol. Details of the in-loop symbol execution information 154 and the generalized loop path information 155 will be described later.

  The in-loop path specialization unit 114 instantiates the generalized loop path information 155 based on an instruction from the rule generation unit 115 to generate the special loop path information 156. Note that, when generating new specialized loop path information 156, the intra-loop path specializing unit 114 may use the already-created specialized loop path information 156. Details of the specialized loop path information 156 will be described later.

  The rule generation unit 115 comprehensively controls each function (the information storage unit 110, the out-loop symbol execution unit 112, the in-loop symbol execution unit 113, and the in-loop path specialization unit 114) included in the specification analysis apparatus 100. For example, the rule generation unit 115 executes the intra-loop path specialization unit 114 based on the upper limit number of loops (hereinafter also referred to as the loop upper limit number) received from the user or the like via the input device 54 or the communication device 56. To control. Further, the rule generation unit 115 generates the rule information 157 based on, for example, the out-loop path information 153 and the specialized loop path information 156.

The input / output processing unit 116 provides a user interface for receiving information and presenting information. For example, the input / output processing unit 116 receives designation of information such as the upper limit number of loops via the input device 54 and the communication device 56. For example, the input / output processing unit 116 outputs the rule information 157 generated by the rule generation unit 115 to the output device 55 and the communication device 56. Note that the input / output processing unit 116 accepts designation of the upper limit number of loops for each loop sentence, for example. For example, the input / output processing unit 116 accepts designation of the upper limit number of loops by batch designation for all the loop statements included in the source code 151. Further, the input / output processing unit 116 acquires the source code 151 and displays it on the output device 55 when receiving the input of the upper limit number of loops from the user.

  Next, a specific operation of the specification analysis apparatus 100 will be described using the source code 151 illustrated in FIG. 3 as an example. The source code 151 is described in C language and includes a loop statement 301.

  The loop sentence specifying unit 111 specifies the loop sentence 301 from the source code 151. The out-of-loop symbol execution unit 112 executes symbol execution for a description (outside loop description) other than the loop statement 301 of the source code 151. The in-loop symbol execution unit 113 executes symbol execution for the description (in-loop description) of the loop statement 301 of the source code 151.

  FIG. 4 shows a search tree (hereinafter referred to as an out-of-loop path search tree 400) generated by the outside-loop symbol execution unit 112 based on the source code 151 shown in FIG. The out-of-loop symbol execution unit 112 uses the out-of-loop path search tree 400 to generate out-of-loop symbol execution information 152. As shown in the figure, the out-loop path search tree 400 has eight nodes assigned identifiers (hereinafter referred to as node names) of “N0” to “N7”, respectively.

Among the eight nodes, the node whose node name is “N0” corresponds to the description of the first line of the source code 151 in FIG. 3 and includes a procedure “START” which means the start point of the source code 151. The node whose node name is “N1” corresponds to the description on the second line of the source code 151 shown in FIG. 3 and includes a procedure “z = 0”. The node whose node name is “N2” corresponds to the description of the 3rd to 10th lines of the source code 151 shown in FIG. In this way, the out-of-loop symbol execution unit 112 handles the description of the loop statement 301 as a black box.

The node whose node name is “N3” corresponds to the eleventh line of the source code 151 shown in FIG. The conditional branch description “if (x% 2 == 0) {” is described in the relevant line, and the out-of-loop symbol execution unit 112 uses the relevant line as a branch point and the condition is “True”. Two paths in the case of “False” are searched. In the following description, “P1” and “P2” are assigned to each of these two paths as identifiers (hereinafter referred to as path names).

  5 and 6 show the out-of-loop symbol execution information 152 generated by the out-of-loop symbol execution unit 112 based on the out-of-loop path search tree 400 of FIG. Of these, the out-of-loop symbol execution information 152 shown in FIG. 5 corresponds to the path whose path name is “P1”, while the out-of-loop symbol execution information 152 shown in FIG. 6 corresponds to the path whose path name is “P2”. To do. As shown in these figures, the out-of-loop symbol execution information 152 is composed of one or more records including items of a node name 1521, a line number 1522, a path condition 1523, a pre-loop variable state 1524, and a variable state 1525. Has been. One of the records of the out-of-loop symbol execution information 152 corresponds to one of the nodes in the out-of-loop path search tree.

  Among the above items, a node name is set in the node name 1521. In the line number 1522, the line number of the source code 151 shown in FIG. 3 corresponding to the node is set.

In the path condition 1523, a condition for reaching the node (hereinafter also referred to as a path condition) is set. Here, FIG. 5 corresponds to the case where the search for the path “P1” on the “True” side is selected in the eleventh line of the source code 151, so that the path condition 1523 of the node whose node name is “N3” is 11 The condition “AL_x% 2 == 0” for setting the branch condition of the line to “True” is set. On the other hand, FIG. 6 corresponds to the case where it is selected to search for the path “P2” on the “False” side in the 11th line of the source code 151, so that the path condition 1523 of the node whose node name is “N3” is 11 A condition “! (AL_x% 2 == 0)” for setting the branch condition of the line to “False” is set.

In the pre-loop variable state 1524, a value of each variable before the execution of the loop statement 301 (hereinafter also referred to as a pre-loop variable state) is set. In this example, the node whose node name is “N2” holds the values of the variables “x”, “y”, and “z” before the loop statement 301 is executed. “BL_x”, “BL_y”, and BL_y shown in FIG. 5 or 6 are variables “x” and “y” before execution of the loop statement 301, respectively.
”And“ z ”are symbol values (“ BL ”is an abbreviation of“ Before Loop ”). “BL_x == X” indicates that the value of the variable “x” before execution of the loop statement 301 is the symbol value “X”, and “BL_y == Y” indicates that the variable “y” before execution of the loop statement 301 “BL_z == 0” indicates that the value of the variable “z” before execution of the loop statement 301 is “0”.

In the variable state 1525, a value of a variable in each of the above nodes (hereinafter also referred to as a variable state) is set. For example, in the node whose node name is “N0”, the values of the variables “x” and “y” are “X” and “Y”, respectively. "X" and "Y" are parameter variables "x"
, A symbol value representing an argument passed to “y”.

In the node whose node name is “N2”, “AL_x” is substituted into the variable “x” as a result of executing the loop statement 301. Here, “AL_x” is a symbol value representing the value of the variable “x” after execution of the loop statement (“AL” is an abbreviation of “After Loop”). As described above, since the out-of-loop symbol execution unit 112 handles the loop statement 301 as a black box, the new symbol value is substituted into the variable as described above as the execution result of the loop statement 301.

  FIG. 7 shows the out-of-loop path information 153 generated by the out-of-loop symbol execution unit 112. The out-loop path information 153 includes one or more records including items of a path name 1531, a path end node 1532, a path condition 1533, a pre-loop variable state 1534, and a variable state 1535. One record of the out-loop path information 153 corresponds to one path.

  Among the above items, the path name 1531 is set with the path name of the path. In the path termination node 1532, the node name of the termination node of the path is set. In the case of the out-loop path search tree shown in FIG. 4, nodes with node names “N5” and “N7” are terminal nodes.

  In the path condition 1533, a path condition at the time when the terminal node is reached is set. The pre-loop variable state 1534 is set to the pre-loop variable state when the terminal node is reached. The variable state 1535 is set with the value of each variable (variable state) when the terminal node is reached.

  FIG. 8 shows a search tree (hereinafter referred to as an in-loop path search tree 800) generated when the in-loop symbol execution unit 113 executes symbol execution for the description of the loop statement 301 (hereinafter also referred to as an in-loop description). It is. The in-loop symbol execution unit 113 uses the in-loop path search tree 800 to generate out-loop symbol execution information 152. As shown in the figure, the in-loop path search tree 800 has nine nodes assigned node names “M0” to “M8”, respectively.

Among the above nine nodes, the node whose node name is “M0” is the source code 151 shown in FIG.
Corresponding to the description on the third line of “”, and includes a procedure “START” which means the starting point of the source code 151. The node whose node name is “M1” corresponds to the description on the third line of the source code 151 shown in FIG. 3, and the description of the condition “while (z <y) {” (hereinafter also referred to as a loop condition). including.

The node whose node name is “M2” corresponds to the fourth line of the source code 151. Nodes with node names “M5” and “M8” represent nodes after exiting from the loop statement 301, and a node with node name “M5” is a loop condition “z% 3 == 0” on the third line. The node with the node name “M8” is the end node of the path where the loop condition “z% 3 == 0” is “False”, respectively. Correspond. In the following description, “Q1” and “Q2” are given as path names to each of these two paths.

  FIG. 9 is a flowchart for explaining processing related to symbol execution of the in-loop description performed by the in-loop symbol execution unit 113 (hereinafter referred to as “in-loop symbol execution processing S900”). The in-loop symbol execution processing S900 will be described below with reference to FIG. In the following, the letter “S” added in front of the reference sign means a processing step.

  First, the in-loop symbol execution unit 113 acquires the in-loop description specified by the loop statement specifying unit 111 (the loop statement 301 in the example of FIG. 3) (S911).

Subsequently, the in-loop symbol execution unit 113 generates (stores and sets) a value of a variable (hereinafter also referred to as the first term) before the execution of the loop before starting the symbol execution of the in-loop description. The content of the inner symbol execution information 154 (first term 1543 described later) is updated. In this example, the in-loop symbol execution unit 113 sets “x _{0” as the} first term for the variable x, and generates the value “BL_x” of the variable “x” before the loop execution (S912).

Subsequently, the in-loop symbol execution unit 113 performs a path search for the in-loop description, and updates the contents of the in-loop symbol execution information 154 (a path condition 1544 and a variable state 1545 described later) (S913). When searching for the path, the in-loop symbol execution unit 113 uses the value of the variable after the execution of n−1 loops to generate the value of the variable at the time of execution of the n loops. For example,
When performing symbol execution for the description on the third line of the loop statement 301 in FIG. 3, the in-loop symbol execution unit 113 sets the value of the variable after execution of n−1 loops based on the loop condition “z <y”. Using “z _n-1 ” and “y _n-1 ”, a path condition of “z _n-1 <y _n-1 ” (where n> 0, hereinafter omitted)) is generated. Similarly, when performing symbol execution for the description on the fifth line, the in-loop symbol execution unit 113 sets n
The value of the variable “x _n ” when the loop is executed is expressed as “x _n = x _n-1 * 2 + 2” using the value of the variable after the loop is executed n−1 times.

  Subsequently, the in-loop symbol execution unit 113 determines whether or not the end of the in-loop description has been reached as a result of the path search for the in-loop description (S914). For example, the description on the 10th line of the loop statement 301 in FIG. 3 corresponds to the end of the description in the loop. If the in-loop symbol execution unit 113 determines that the end of the in-loop description has been reached (S914: YES), the process proceeds to S915. If the in-loop symbol execution unit 113 determines that the end of the in-loop description has not been reached (S914: NO), the process returns to S913.

In S915, the in-loop symbol execution unit 113 adds a condition corresponding to the negation of the loop condition in the in-loop description to the path condition. Here, the negation of the loop condition is generated using the value of the variable after n loop executions. For example, the negation of the loop condition “z _n <y _n ” ”in the loop statement 301 of FIG. 3 becomes“! (Z _n <y _n ) ”(provided that n ≧ 0, hereinafter omitted). In the following description, the conditional expression added in S915 is referred to as a generalized escape conditional expression.

Subsequently, the in-loop symbol execution unit 113 generates generalized in-loop path information 155 based on the path condition and variable state generated in the path search process in S913 (S916). Specifically, the in-loop symbol execution unit 113 first acquires the node name, the first term, the path condition, and the variable state at the time of S915. Then, the in-loop symbol execution unit 113 uses the value of the variable after the n-1 loop executions appearing in the acquired path condition as an expression using the value of the variable after the n loop executions based on the acquired variable state. Replace with For example, the path condition “z _n-1 <y _n-1 ” generated for the loop statement 301 of the source code 151 in FIG. 3 is the variable state “y _n = y _n-1 ” at the node whose node name is “M5”. And “z _n −1 <y _n ” based on “z _n = z _n−1 +1”. The in-loop symbol execution unit 113 stores the node name 1541, the first term 1543, and the variable state 1545 acquired from the in-loop symbol execution information 154 as the generalized loop path information 155 in addition to the path condition thus generated.

  Subsequently, the in-loop symbol execution unit 113 determines whether or not all paths included in the loop sentence have been searched (S917). If the in-loop symbol execution unit 113 determines that all paths have been searched (S917: YES), the in-loop symbol execution processing S900 ends. On the other hand, if the in-loop symbol execution unit 113 determines that all paths have not been searched (there is an unsearched path) (S917: NO), the process proceeds to S918.

  In S918, the in-loop symbol execution unit 113 starts the process from S913 to search for an unsearched path.

  FIG. 10 shows in-loop symbol execution information 154 based on the loop statement 301 of FIG. As shown in the figure, the in-loop symbol execution information 154 is composed of one or more records including items of a node name 1541, a line number 1542, an initial term 1543, a path condition 1544, and a variable state 1545. . One record of the in-loop symbol execution information 154 corresponds to one of the nodes.

Among the above items, a node name is set in the node name 1541. In the line number 1542, the line number of the source code 151 corresponding to the node is set. The first term described above is set in the first term 1543. In the path condition 1544, the above-described path condition of the node is set. As described above, the pass condition is expressed using the value of the variable after the loop is executed n-1 times. In the variable state 1545, the above-described variable state in the node is set. As described above, the variable state at the time of executing the loop n times is expressed using the variable state after the execution of the loop n-1 times.

  FIG. 11 shows the generalized loop path information 155 generated based on the loop statement 301 of FIG. As shown in the figure, the generalized loop path information 155 is composed of one or more records having items of a path name 1551, a path end node 1552, an initial term 1553, a path condition 1554, and a variable state 1555. ing. One record of the generalized loop path information 155 corresponds to one of the paths (hereinafter also referred to as a generalized loop path).

  Among the above items, the path name 1551 is set to the path name of the path. In the path termination node 1552, a node at the end of the path is set. In the first term 1553, the first term is set. In the path condition 1554, a path condition is set. A variable state is set in the variable state 1555.

  FIG. 12 is a flowchart for describing processing performed by the in-loop path specializing unit 114 (hereinafter referred to as in-loop path specializing process S1200). The in-loop path specialization process S1200 will be described below with reference to FIG.

First, the in-loop path specialization unit 114 acquires the generalized loop path information 155 (S121).
1). Subsequently, the intra-loop path specialization unit 114 refers to the special loop inner path information 156 and determines whether or not special loop inner path information with the number of loops of 0 has been generated (S1212). When the in-loop path specializing unit 114 determines that the in-loop information about the special loop with the loop count of 0 has been generated (S1212: YES), the process proceeds to S1215. If the in-loop path specializing unit 114 determines that the in-loop information about the special loop with 0 loops has not been generated (not generated) (S1212: NO), the process proceeds to S1213.

  The intra-loop path specialization unit 114 generates special loop internal path information 156 with the number of loops being 0 based on the generalized loop internal path information 155 acquired in S1211 (S1213).

FIG. 13A shows specialized loop path information 156 with zero loops, which is generated by the in-loop path specialization unit 114 based on the generalized loop path information 155 of FIG. As shown in the figure, the path information 156 in the specialized loop is composed of one or more records including items of a path name 1561, a path end node 1562, an initial term 1563, a path condition 1564, and a variable status 1565. ing. One of the records of the specialized loop path information 156 corresponds to one path (hereinafter also referred to as a specialized loop path). The intra-loop path specialization unit 114 generates one special intra-loop path for each general intra-loop path with the above loop count of zero.

  Among the above items, the path termination node 1562 and the first term 1563 inherit the path termination node 1552 and the first term 1553 in the generalized loop path information 155. The path condition 1564 and the variable state 1565 are generated based on the path condition 1554 and the first term 1553 by the in-loop path specializing unit 114 as described below.

First, the intra-loop path specializing unit 114 instantiates the path condition 1554 of the generalized loop intra-path information 155 with the number of loops of zero. Specifically, the in-loop path specializing unit 114 substitutes n = 0 for the value of the variable that appears in the path condition 1554 after executing n loops. Since n = 0, the in-loop path specializing unit 114 does not use the logical expression with the condition “n> 0” among the logical expressions constituting the path condition 1554, and the generalization escape condition described above. Use only expressions. For example, when the path name 1551 of the path information 155 in the generalized loop in FIG. 11 is “Q1”, the in-loop path specializing unit 114 selects “(z _n −1) <y _n ” and “(z _n -1) For each expression of% 3 == 0, there is a condition that “n> 0”, so these are not used, and in the generalized escape conditional expression “! (Z _n <y _n )”, n A path condition of “! (Z ₀ <y ₀ )” obtained by setting = 0 is used. In the following description, a conditional expression obtained by instantiating the generalized escape conditional expression is referred to as a specialized escape conditional expression.

Subsequently, the in-loop path specialization unit 114 generates a variable state 1565. Here, when the number of loops is 0, the variable state 1565 coincides with the first term 1563, and the first term 1563 corresponds to the value of the variable before the loop execution. Therefore, the in-loop path specializing unit 114 represents the value of the variable after executing the loop 0 times as the value of the variable before the loop execution held as the first term. For example, when the path name 1551 of the path information 155 in the generalized loop shown in FIG. 11 is “Q1”, the value “x _0” of the variable after executing 0 loops is expressed by the expression “x _” in the first term 1553. _From “ ₀ = BL_x”, it is expressed as “x ₀ = BL_x”.

Returning to FIG. 12, subsequently, the in-loop path specialization unit 114 replaces the first term appearing in the path condition generated in S1213 with an expression including the value of the variable before the loop execution (S1214). For example, in the case of “Q1” in the generalized loop path information 155 shown in FIG. 11, the in-loop path specialization unit 114 sets the path condition “! (Z ₀ <y ₀ )” to the expression “z” in the first term 1553. Based on “ ₀ = BL_z” and “y ₀ = BL_y”, it is expressed as “! (BL_z <BL_y)”.

FIG. 13B shows the specialized loop path information 156 after the above-described replacement is performed on the specialized loop path information 156 having the loop count of 0 in FIG.

  Returning to FIG. 12, subsequently, the in-loop path specialization unit 114 acquires the generated in-specialized loop path information 156 having the maximum number of loops (S1215). In the following description, the loop count of the specialized loop path information 156 acquired at this time is K-1 times.

Subsequently, the intra-loop path specializing unit 114 performs the processing between the acquired special loop inner path information (the number of loops is K-1) and the generalized intra-loop path information 155 acquired in S1211. Based on the combination, the path information 156 in the special loop with the loop count K times is generated (S1).
216). For example, when there are two specialized loop path information 156 and two generalized loop path information 155 with a loop count of K−1, the intra-loop path specialization unit 114 determines that the loop count is K. Four pieces of special loop in-loop path information 156 are generated.

First, the in-loop path specializing unit 114 instantiates n and n−1 included in the generalized loop path information 155 into K and K−1 in order to generate the variable state 1565. Further, the in-loop path specializing unit 114 calculates the value of the variable after executing the loop K-1 times based on the variable state of the specialized loop path information 156 having the number of loops K−1 times, and the variable before the loop execution. Replace with an expression containing the value of.

For example, from the variable state “x _n = x _n-1 * 2 + 2” of the path whose path name is “Q1” in the generalized loop path information 155 in FIG. When generating information, the in-loop path specializing unit 114 first instantiates “x _n = x _n−1 * 2 +2” as “x ₁ = x ₀ * 2 +2”. Further, the in-loop path specializing unit 114 specifies the in-loop path information 1 with 0 loops.
Based on the variable state “x ₀ = BL_x” with the path name “Q1” in 56, “x ₁ = BL_x * 2 + 2” is generated. Further, the in-loop path specializing unit 114 performs “y ₁ = BL_y” and “z ₁ = BL_z” in the same manner as described above. + 1 ”is generated.

Subsequently, in order to generate the path condition 1564, the in-loop path specializing unit 114 excludes the above-described specialized escape condition expression from the path condition 1564 of the specialized loop path information 156 acquired in S1215. For example, when the path name in the path information 156 in the special loop with the loop count of 0 is “Q1”, the path specialization unit 114 in the loop sets the special escape conditional expression “! (BL_z <BL_y)”. exclude. In the following, an expression remaining after excluding the specialized escape conditional expression is referred to as an escape expression exclusion expression.

Subsequently, the in-loop path specializing unit 114 instantiates the path condition of the generalized loop path by the number of loops K times. For example, when instantiating the path condition of “Q1” in the generalized loop path information 155 with one loop count, the intra-loop path specialization unit 114 reads “(z _n −1) <y _n && (z _n -1)% 3 == 0 &&! (z _n <y _n ) '' by substituting 1 for n, we get `` (z ₁ -1) <y ₁ && (z ₁ -1)% 3 == 0 &&! (Z ₁ <y ₁ ) ”. Further, the in-loop path specializing unit 114 replaces the value of the variable after executing the loop K times with an expression including the value of the variable before executing the loop based on the variable state of the in-loop path information. In the case of the above example, the in-loop path specializing unit 114 sets “y ₁ = BL_y”.
And (z ₁ = BL_z + 1) from ((z ₁ -1) <y ₁ && (z ₁ -1)% 3 == 0 &&! (Z ₁ <y ₁ )) to ((BL_z + 1) -1) <BL_y && ((BL_z + 1) -1)% 3 == 0 &&! ((BL_z + 1) <BL_y) ''
Is generated. Then, the in-loop path specializing unit 114 ANDs the generated expression with the escape expression exclusion expression.

FIG. 14 shows an example of the specialized loop path information 156 with one loop. In the figure,
“Q1-Q1” in the path name 1561 is based on a path whose path name 1561 of the path information 156 in the specialized loop is “Q1” and a path whose path name 1551 of the path information 1155 in the generalized loop is “Q1”. Indicates the generated path. The path termination node 1562 inherits the path termination node 1552 of the generation source generalized loop path information 155. The first term 1563 inherits the first term 1563 of the special loop path information 156 of the generation source. The variable state 1565 is generated by the above-described method based on the variable state 1555 of the generalized loop path information 155 and the variable state 1565 of the specialized loop path information 156. The path condition 1564 is generated based on the path condition 1564 of the path information 156 in the specialized loop, the path condition 1554 of the path information 155 in the generalized loop, and the variable state 1565 of the path information 156 in the specialized loop.

  FIG. 15 shows that the rule generation unit 115 uses the functions described above (the information storage unit 110, the out-loop symbol execution unit 112, the in-loop symbol execution unit 113, and the in-loop path specialization unit 114). It is a flowchart explaining the process (henceforth rule generation process S1500) which produces | generates information. The rule generation process S1500 will be described below with reference to FIG.

  First, the rule generation unit 115 acquires the loop upper limit count via the input device 54 and the communication device 56 (S1511).

  Subsequently, the rule generation unit 115 refers to the rule information 157 and determines whether or not a rule corresponding to the acquired loop upper limit count has been generated (S1512). When the rule generation unit 115 determines that the rule corresponding to the upper limit number has been generated (S1512: YES), the rule generation processing S1500 ends. When the rule generation unit 115 determines that the rule corresponding to the upper limit number has not been generated (S1512: NO), the process proceeds to S1513.

In S1513, the rule generation unit 115 controls the in-loop path specialization unit 114 to execute the in-loop path specialization process S1200, thereby allowing the number of loops already generated to be K-1 times in the special loop. Based on the information 156, the path information 156 in the specialized loop with the number of loops of K times
Is generated.

Subsequently, the rule generation unit 115 acquires the out-loop path information 153 (S1514). Subsequently, the rule generation unit 115 creates a rule with the number of loops of K times based on the combination of the specialized loop path information 156 with the number of loops generated at S1513 and the out-loop path information 153 acquired at S1514. Is generated (S1515). For example, the rule generation unit 115
Has four special loop paths in the special loop path information 156 with K loops, and
If there are two out-of-loop paths in the acquired out-of-loop path information 153, eight rules with a loop count of K times are generated.

  First, the rule generation unit 115 generates a rule path condition by combining the path condition 1564 of the path information 156 in the specialized loop and the path condition 1533 of the path information 153 outside the loop by a logical product. Then, the rule generation unit 115 replaces the symbol value representing the value of the variable after executing the loop appearing in the path condition of the generated rule with an expression including the symbol value representing the value of the variable before executing the loop. Further, based on the pre-loop variable state 1534 of the out-of-loop path information 153, the rule generation unit 115 replaces the symbol value representing the value of the variable before the loop execution with the value actually held by the variable.

For example, the path name 1531 of the out-of-loop path information 153 shown in FIG. 7 is “P1”, and the path name 1561 of the in-loop information 156 with 0 loops shown in FIG. 13B is “Q1”.
When the path condition is generated from the path “”, it is as follows. First, the rule generation unit 115 sets “AL_x% 2 == 0” for the path condition 1533 for the path whose path name 1531 is “P1”, and the path condition 1564 for the path information 156 in the specialized loop with the loop count 0 is “ ! (BL_z <BL_y) ”, so that“ AL_x% 2 == 0 &&! (BL_z <BL_y) ”is generated by ANDing these. Here, note that the value “AL_x” of the variable after loop execution appearing in the above equation matches “x ₀ ”. Further, the value of “x ₀ ” is the variable state 156 of the path information 156 in the specialized loop.
5 to “x ₀ = BL_x”. Therefore, the rule generation unit 115 generates “BL_x% 2 == 0 &&! (BL_z <BL_y)” by replacing “AL_x” with “BL_x”. Further, “BL_x == X”, “BL_y == Y”, “BL_z == 0” from the pre-loop variable state 1534 of the out-of-loop path information 153.
Therefore, based on these, the rule generation unit 115 generates a path condition “X% 2 == 0 &&! (0 <Y)”.

  Subsequently, the rule generation unit 115 generates a path execution result based on the variable state 1535 of the out-loop path information 153 and the variable state 1565 of the specialized loop path information 156. Specifically, the rule generation unit 115 replaces the symbol value representing the value of the variable after loop execution appearing in the variable state 1535 of the out-of-loop path information 153 with the symbol value representing the value of the variable before loop execution. That is, based on the pre-loop variable state 1534 of the out-of-loop path information 153, the rule generation unit 115 replaces the symbol value representing the value of the variable before executing the loop with the value actually held by the variable. .

For example, the rule generation unit 115 determines that the path name 1531 of the out-of-loop path information 153 is “P1” and the path name 1561 of the specialized loop path information 156 whose number of loops is 0 is “Q1”. When generating a pass execution result based on this, it is as follows. First, the variable state 1535 of the out-of-loop path information 153 is “x = AL_x”, and the variable state 1565 of the in-loop information 156 is “x ₀ = BL_x”. As described above, “AL_x” matches “x ₀ ”, so that “x = BL_x” is obtained. Then, the rule generation unit 115 obtains “x = X” based on the pre-loop variable state 1534 of the out-loop path information 153. The rule generation unit 115 obtains “y = Y” and “z = X” by the same method. Here, for example, when only the value of the variable returned as the return value in the source code 151 is adopted as the rule path execution result, the rule generation unit 115 describes the 16th line of the source code 151 shown in FIG. Based on the above, “z = X” representing the value of the variable z is taken as the pass execution result.

  Subsequently, when there is an overlap in the plurality of generated rules, the rule generation unit 115 deletes the overlapping rule. Further, the possibility of satisfying the path condition of the generated rule is confirmed, and if it is found that the rule is unsatisfiable, the rule is deleted (S1516). As a method for confirming the satisfiability of a logical expression, for example, there is a method using an inference rule, but the method for confirming the satisfiability is not necessarily limited.

FIG. 16 shows the path information 153 outside the loop and the path information 156 in the specialized loop with the loop count being zero.
This is an example of the rule information 157 generated by the rule generation unit 115 based on the above and when the number of loops is zero. As shown in the figure, the rule information 157 is composed of one or more records having three items: a path name 1571, a path condition 1572, and a path execution result 1573.

In the path name 1571, information for specifying the generation source is set. For example, “P1-Q1” indicates that the rule is generated based on “P1” of the out-of-loop path information 153 and “Q1” of the specialized in-loop path information 156 with the loop count of 0. In the path condition 1572 and the path execution result 1573, values generated by the above-described method are set. In this example, the contents of the records “P1-Q2” and “P1-Q1” are duplicated. In this case, the rule generation unit 115 deletes one (for example, “P1-Q2”) in S1516 described above. To do. Similarly, since “P2-Q2” is also duplicated with “P2-Q1”, the rule generation unit 115 deletes one in the process of S1516.

FIG. 17 is an example of the rule information 157 when the number of loops is one, which is generated by the rule generation unit 115 based on the out-loop path information 153 and the specialized loop path information 156 with one loop. As shown in the figure, this rule information 157 is composed of one or more records having three items: a path name 1571, a path condition 1572, and a path execution result 1573.

In the path name 1571, information for specifying the generation source is set. For example, the path name “P1-Q1-Q1” is generated based on “P1” of the out-loop path information 153 and “Q1-Q1” of the in-loop path information 156 of one loop number. It shows that. In the pass condition 1572 and the pass execution result 1573, values generated by the above-described method are set. In this example, the records “P1-Q2-Q1”, “P1-Q2-Q2”, “P2-Q2-Q1”, and “P2-Q2-Q2” are “P1-Q1-Q1”, respectively. , “P1-Q1-Q2”, “P2-Q1-Q1”, and “P2-Q1-Q2”, the rule generator 115 deletes one of them in the process of S1516. Further, since the path condition 1713 cannot be satisfied for “P1-Q1-Q2”, “P2-Q1-Q1”, and “P2-Q1-Q2”, the rule generation unit 115 deletes them in the process of S1516. .

FIG. 18 shows an example of the rule information 157 when the upper limit number of loops is designated as one. As described above, the input / output processing unit 116 receives designation of the upper limit number from the user. Then, by executing the rule generation unit 115, the rule information 157 is generated for each of the cases where the number of loops is 0 times, 1 time,... K-1 times, and K times. The input / output processing unit 116 acquires a rule when the number of loops is 0 to K from the rule information 157 and outputs (displays) the rule to the output device 55. The rule information 157 when the upper limit number of loops shown in FIG.
1, and includes three records including items of a path condition 1572 and a path execution result 1573. The rules “P1-Q1”, “P2-Q1”, and “P1-Q1-Q1” set in the path name 1571 are the rule information 157 shown in FIG. 16 and the rule information 157 shown in FIG. From “P1-Q2”, “P2-Q2”, “P1-Q2-Q1”, “P1-Q2-Q2”, “P2-Q2-Q1”, “P2-Q2” in the process of S1516 in FIG. -Q2 "," P1-Q1-Q2 "," P2-Q1-Q1 ", and" P2-Q1-Q2 "are deleted, and the rules remaining after the deletion are aggregated.

In order to obtain the rule information 157 when the loop upper limit number is 1, the rule information 157
However, the rule information 157 has already been generated, for example, when the symbol has been executed with the loop upper limit set to 0 before executing the symbol execution with the loop upper limit set to 1. If it is already completed, there is no need to generate the rule information 157 again. For this reason, the rule generation unit 115 may check in advance whether the rule for the loop upper limit count 0 is stored in the rule information 157 and generate the rule information 157 only when the rule is not stored.

As described above, the specification analysis apparatus 100, when reproducing the rule from the source code including the loop statement, displays the path execution result for the loop statement, the variable value after executing the loop n-1 times, and the loop n It is stored as a relational expression of variable values after the first execution. Therefore, for example, when the rule when the loop count is K-1 has been reproduced, based on the above relational expression and the path information generated in the process of generating the rule when the loop count is K-1 Without executing symbol execution, it is possible to generate a rule when the number of loops is K by simple substitution processing or logical operation processing. In other words, by recursively using the above relational expression generated in a single symbol execution, a rule for any number of loops can be generated by simple substitution processing and logical operation processing without repeating symbol execution. . For this reason, it is possible to suppress the consumption of computer resources for symbol execution, and it is possible to reduce the time required to acquire the rule.

Further, since the specification analysis apparatus 100 stores the rules generated by the symbol execution, it is possible to reduce the processing amount when the symbol execution is performed a plurality of times by changing the loop upper limit count. For example, when symbol execution is performed with the loop upper limit count set to L times, rules corresponding to each of the loop count from 0 to L times are generated and stored.For example, after that, the loop upper limit count is set to L + 1
If you want to execute the symbol again after changing to the number of times, you only need to create a new rule for the loop count L + 1 and add it to the rule for the loop count from 0 to L times. The consumption of the resources of the computer can be suppressed, and the time required to acquire the rule can be shortened.

As described above, according to the specification analyzing apparatus 100 of the present embodiment, symbol execution can be efficiently performed on source code including an arbitrary loop sentence.
[Second Embodiment]

  FIG. 19 is a functional block diagram of the specification analysis apparatus 100 described as the second embodiment. The specification analysis apparatus 100 of the second embodiment is also realized by the same hardware as the specification analysis apparatus 100 of the first embodiment.

  The specification analysis apparatus 100 according to the second embodiment includes functions equivalent to those of the specification analysis apparatus 100 according to the first embodiment, and further includes the functions of the in-loop path generalization unit 121 and the generalization rule generation unit 122. The information storage unit 110 of the specification analysis apparatus 100 according to the second embodiment stores the same information as the information storage unit 110 according to the first embodiment, and further includes generalized loop path information 161 and generalized rule information. 162 is stored.

  The in-loop path generalization unit 121 generates the generalized loop path information 161 by generalizing the generalized loop path information 155. The generalization rule generation unit 122 generates a rule expressed in a general term based on the out-of-loop path information 153 and the generalized in-loop path information 161, and stores the generated rule as generalization rule information 162.

  The input / output processing unit 116 outputs (displays) the generalization rule information 162 to the output device 55. Further, the input / output processing unit 116 instantiates and outputs (displays) the generalization rule information 162 to the loop upper limit number acquired via the input device 54 or the communication device 56.

  Next, a specific operation of the specification analysis apparatus 100 according to the second embodiment will be described using the source code 151 illustrated in FIG. 20 as an example. As shown in the figure, the source code 151 is written in C language and includes a loop statement 302.

  FIG. 21 shows a search tree (hereinafter referred to as an out-of-loop path search tree 2100) generated by the outside-loop symbol execution unit 112 based on the source code 151 shown in FIG. The out-of-loop symbol execution unit 112 uses the out-of-loop path search tree 2100 to generate out-of-loop symbol execution information 152. As shown in the figure, the out-loop path search tree 2100 has eight nodes assigned node names “N0” to “N7”, respectively.

Of the above eight nodes, the node whose node name is “N0” corresponds to the description of the first line of the source code 151 in FIG. 21 and includes a procedure “START” which means the start point of the source code 151. The node whose node name is “N1” corresponds to the description on the second line of the source code 151 shown in FIG. 21 and includes a procedure “z = 0”. The node whose node name is “N2” is shown in FIG.
3 corresponds to the description of the third to sixth lines of the source code 151 shown in FIG. The node whose node name is “N3” corresponds to the seventh line of the source code 151 shown in FIG. A conditional branch of “if (x% 2 == 0) {” is described in the line, and the out-of-loop symbol execution unit 112 uses the line as a branch point and the condition is “True” and “ Two paths in the case of “False” are searched. In the following description, “P1” and “P2” are given to each of these two paths as path names.

22 and 23 show the out-of-loop symbol execution information 152 generated by the out-of-loop symbol execution unit 112 based on the out-of-loop path search tree 2100 of FIG. Of these, the out-of-loop symbol execution information 152 shown in FIG. 22 corresponds to the path whose path name is “P1”, while the out-of-loop symbol execution information 152 shown in FIG. 23 corresponds to the path whose path name is “P2”. To do.

  FIG. 24 shows the out-of-loop path information 153 generated by the out-of-loop symbol execution unit 112. In the path termination node 1532, the node name of the termination node of the path is set. In the case of the out-loop path search tree shown in FIG. 4, nodes with node names “N5” and “N7” are terminal nodes.

  FIG. 25 is a search tree (hereinafter referred to as an in-loop path search tree 2500) generated when the in-loop symbol execution unit 113 executes symbol execution for the loop statement 302. The in-loop symbol execution unit 113 uses the in-loop path search tree 2500 to generate the out-loop symbol execution information 152. As shown in the figure, the in-loop path search tree 2500 has five nodes assigned node names “M0” to “M4”, respectively.

Of the above five nodes, the node whose node name is “M0” corresponds to the description of the third line of the source code 151 shown in FIG. 20 and includes a procedure “START” which means the starting point of the source code 151. The node whose node name is “M1” corresponds to the description on the third line of the source code 151 shown in FIG. 20 and is a condition “while ((3 * z) <x) {” (hereinafter referred to as a loop condition). .) Description. A node whose node name is “M2” corresponds to the fourth line of the source code 151 shown in FIG. A node whose node name is “M3” corresponds to the fifth line of the source code 151 shown in FIG. A node whose node name is “M4” corresponds to a terminal node of the path. In the following description, “Q1” is given as the path name of the above path.

  FIG. 26 shows in-loop symbol execution information 154 generated based on the loop statement 302 of FIG. The in-loop symbol execution information 154 shown in the figure is generated by the in-loop symbol execution unit 113 in the same manner as in the first embodiment.

  FIG. 27 shows generalized loop path information 155 generated based on the loop statement 302 of FIG. The generalized in-loop path information 155 shown in the figure is generated by the in-loop symbol execution unit 113 in the same manner as in the first embodiment.

  FIG. 28 shows generalized loop internal path information 161 generated by the internal loop path generalization unit 121 based on the generalized loop internal path information 155. As shown in the drawing, the path information 161 in the generalized loop is composed of one or more records each having items of a path name 1611, a path end node 1612, an initial term 1613, a path condition 1614, and a general term 1615. Has been. The in-loop path generalization unit 121 obtains the general term by regarding the variable state 1555 of the generalized loop path information 155 as a recurrence formula. As a method for obtaining the general term from the recurrence formula, for example, there is a method described in Chapter 10 of Non-Patent Document 1.

  FIG. 29 shows the generalization rule information 162 generated by the generalization rule generation unit 122 based on the out-loop path information 153 and the generalization loop path information 161. The generalization rule generation unit 122 generates generalization rule information 162 by combining the generalization loop path information 161 and the out-loop path information 153. In this example, the generalization rule generation unit 122 generates two generalization rules.

  First, the generalization rule generation unit 122 generates a path condition 1622 of the generalization rule information 162 based on the path condition 1533 of the out-of-loop path information 153. The generalization rule generation unit 122 replaces the symbol value representing the value of the variable after loop execution appearing in the path condition 1533 of the out-of-loop path information 153 with an expression including the symbol value representing the value of the variable before loop execution. . Further, based on the pre-loop variable state 1534, the generalization rule generation unit 122 replaces the symbol value representing the value of the variable before the loop execution with a value actually held by the variable.

For example, consider a case in which a path condition is generated based on a path whose path name 1531 of the out-of-loop path information 153 is “P1” and a path whose path name 1611 of the generalized loop path information 161 is “Q1”. As shown in FIG. 24, the path condition 1533 of the out-of-loop path information 153 is “AL_x% 2 == 0”. Here, note that the variable value “AL_x” after loop execution in the path condition 1533 matches “x _n ” of the general term 1615 of the generalized loop internal path information 161 of FIG. Since the value of “x _n ” is “x _n = x ₀ + 2 * n” from the general term 1615 and “x ₀ = BL_x” from the first term 1613, the generalization rule generation The unit 122 converts the path condition 1533 into “(BL_x + 2 * n)% 2 == 0”. Also, variable state before loop 1534
Since “BL_x == X”, based on this, the generalization rule generation unit 122 “(X + 2 * n)
% 2 == 0 ”is generated.

  Subsequently, the generalization rule generation unit 122 generates a path execution result 1623 of the generalization rule information 162 from the variable state 1535 of the outside-loop path information 153 and the general term 1615 of the generalization loop internal path information 161. To do. Specifically, the generalization rule generation unit 122 converts the symbol value representing the value of the variable after loop execution appearing in the variable state 1535 of the out-of-loop path information 153 to the symbol value representing the value of the variable before loop execution. Replace. Furthermore, based on the pre-loop variable state 1534 of the out-of-loop path information 153, the generalization rule generation unit 122 replaces the symbol value representing the value of the variable before the loop execution with a value actually held by the variable.

For example, the path execution result 1623 of the generalized rule information 162 is based on the path whose path name 1531 of the out-of-loop path information 153 is “P1” and the path name 1611 of the path information 161 of the generalized loop information 161 is “Q1”. Consider the case of generating Here, the variable state 1535 of the out-of-loop path information 153 is “x = AL_x”, and the general term 1615 of the generalized in-loop path information 161 is “x _n = x ₀ + 2 * n”. As described above, since “AL_x” matches “x _n ” and “x ₀ = BL_x” from the first term 1613, the general termization rule generation unit 122 sets “x = BL_x + 2 * n”. obtain. Then, the generalization rule generation unit 122 obtains “x = X + 2 * n” based on the pre-loop variable state 1534 of the out-loop path information 153. “Z = X + 2 * n” is obtained by the same method. Here, if only the value of the variable returned as the return value in the source code 151 shown in FIG. 20 is adopted as the rule path execution result, the generalization rule generation unit 122 reads the 12th line of the source code 151. Based on this, “z = X + 2 * n” representing the value of the variable z is adopted as the pass execution result.

Subsequently, the generalization rule generation unit 122 generates a constraint condition 1624 for the number of loops n in the generalization rule information 162 based on the path condition 1554 of the generalized loop path information 155. First, the generalization rule generation unit 122 replaces the value of the variable when the number of loop executions included in the path condition 1554 is n times with the general term 1615 of the generalization loop internal path information 161. Furthermore, the generalization rule generation unit 122 performs symbol value replacement based on the first term 1613 of the generalized in-loop path information 161 and the pre-loop variable state 1534 of the out-of-loop path information 153.

For example, based on the path whose path name 1531 of the out-of-loop path information 153 is “P1” and the path name 1611 of the path information 1611 in the generalized loop information 161 is “Q1”, Consider a case where the constraint condition 1624 for the number of loops n in the generalization rule information 162 is generated. First, the generalization rule generation unit 122 generates the expression “3 * (z _n −1) <x _n −2 (where n> 0) &&! (3 * z) of the path condition 1614 of the path information 161 in the generalization loop. _n <x _n ) (where n ≧ 0) ”, based on the general term 1615,“ 3 * ((z ₀ + n) −1) <(x ₀ + 2 * n) −2 (where n> 0) &&! (3 * (z ₀ + n) <(x ₀ + 2 * n)) (where n ≧ 0) ”. Then, the generalization rule generation unit 122 converts the above expression into 3 * ((BL_z + n) -1) <(BL_x + 2 * n) -2 (where n> 0) &&! (3 * (BL_z + n) <(BL_x + 2 * n)) (where n ≧ 0) ”. Further, the generalization rule generation unit 122 converts the above expression to “3 * (n −1) <based on the pre-loop variable state 1534.
X + 2 * n-2 (where n> 0) &&! (3 * n <X + 2 * n) (where n ≧ 0) ”.

  FIG. 30 shows an example of a screen that displays generalized rule that the input / output processor 116 outputs to the output device 55 based on the generalized rule information 162 (hereinafter referred to as a generalized rule display screen 3000). It is.

  The input / output processing unit 116 receives an input of the loop upper limit count from the user via the loop upper limit count input receiving column 3010 provided on the same screen. When the rule expansion execution button 3012 provided on the same screen is pressed, the input / output processing unit 116 sets a variable n representing the number of loops included in the generalized rule information 162 from 0 to the above loop upper limit number. Substitute values sequentially to get the result.

For example, when the user inputs 1 into the loop upper limit count input reception field 3011 and presses the rule expansion execution button 3012 for the generalized rule information 162, the input / output processing unit 11
6. First, by substituting 0 for n of “P1-Q1” and “P2-Q1” of the generalization rule information 162, “P1-Q1-0” and “P2-Q2” in the expanded rule display column 3013 are displayed. The contents of “Q1-0” (information that embodies the rules expressed in general terms) are generated. Next, the input / output processing unit 116 reads “P1-Q1”.
And by substituting 1 for n in “P2-Q1”, the contents of “P1-Q1-1” and “P2-Q1-1” in the expanded rule display field 3013 (specify the rules expressed in the general terms) Information).

The restriction condition 1624 for the number of loops n in the generalized rule information 162 is generated based on the restriction condition 3014 in the expanded rule display field 3013. Based on the path condition 3015, the input / output processing unit 116 determines whether or not the logical product of the constraint conditions 3014 is satisfiable, and if it cannot be satisfied, the rule is hidden or highlighted (bold frame display, grayout, etc.), etc. And In this example, “P1-Q1-1” is displayed in a thick frame.

  As described above, the specification analyzing apparatus 100 according to the second embodiment obtains the general term of the recurrence formula expressing the path information in the generalized loop, thereby obtaining the value of the variable and the above n when the loop statement is executed n times. A general termization loop path information 161 that is a relational expression with the containing expression is generated, and a general termization that is a rule expressed by a general term based on the general termization loop inner path information 161 and the out-loop path information 153 is generated. Since the rule information is generated, it is possible to provide information related to software specifications (rules) in a form that is easy for the user to use.

  By the way, it goes without saying that the present invention is not limited to the above-described embodiment, and various modifications can be made without departing from the scope of the invention. For example, the above embodiment has been described in detail for easy understanding of the present invention, and is not necessarily limited to the one having all the configurations described. In addition, it is possible to add, delete, and replace other configurations for a part of the configuration of the above embodiment.

For example, for an arbitrary K, when comparing the rule when the number of loops is K-1 with the rule when the number of loops is K, for example, the rule is such that the coefficient value increases or decreases regularly. Some regularity can be found during the period. In that case, the deviation of the regularity may be seen when the number of loop executions exceeds the actual (preliminarily assumed) maximum number of loop executions. Therefore, for example, the rule generation unit 115 has a rule for when the number of loops is 0, a rule for 1 time, a rule for K-1 times, a rule for K times, a K + 1 time rule, The rules are continuously monitored, and information such as a warning is automatically output to the user when a deviation from the regularity is detected. As a result, the user can easily and accurately grasp the maximum number of executions of the actual loop. As a method of detecting the regularity, for example, there is a method of extracting information on numbers and operators constituting the rule and classifying the information by using a machine learning algorithm.

  For example, when a plurality of loop statements are included in the source code, the specification analysis apparatus 100 accepts designation of the upper limit number of loops for each loop statement, and the information storage unit 110 stores the feature number for each loop statement. The path information 156 having the maximum number of loops is acquired from the path information 156 in the generalized loop, and for each loop statement, the path information 155 in the generalized loop is recursively applied to the acquired path information 156 in the specialized loop. The path information 156 in the special loop up to the upper limit number may be generated.

  FIG. 31 shows an example of a designation screen 3100 for specifying the upper limit number of loops that the input / output processing unit 116 outputs (displays) to the output device 55. The loop upper limit count designation screen 3100 includes a source code display field 3111 and a loop upper limit count registration field 3112. The loop upper limit count registration field 3112 includes a loop sentence position specifying result 3113, a loop upper limit count input receiving unit 3114, a loop upper limit count batch input receiving unit 3115, a loop upper limit count batch setting button 3116, a loop sentence extracting button 3117, and a loop upper limit count. A registration button 3118 is included.

  First, the input / output processing unit 116 acquires the source code and displays it in the source code display field 3111. When the user presses the loop sentence extraction button 3117, the input / output processing unit 116 refers to the source code and specifies the position of the loop sentence. In this embodiment, the start and end lines of the loop statements 3151 and 3152 are specified. Then, the input / output processing unit 116 displays the start and end lines of the loop statements 3151 and 3152 in the loop statement position specifying result 3113.

  The user inputs the loop upper limit number of each loop sentence shown in the loop sentence position specifying result 3113 to the corresponding loop upper limit number input receiving unit 3114. In addition, the user inputs the loop upper limit number to be applied to all loop statements to the loop upper limit number batch input receiving unit 3115 and presses the loop upper limit number batch setting button 3116, so that the same value is given to the loop upper limit number input receiving unit 3114. It is also possible to set all at once (the same upper limit for each loop statement).

  After the loop upper limit count is input as described above, when the user presses the loop upper limit count registration button 3118, the input / output processing unit 116 acquires the loop upper limit count for each loop sentence.

Each of the above-described configurations, function units, processing units, processing means, and the like may be realized in hardware by designing some or all of them, for example, with an integrated circuit. Each of the above-described configurations, functions, and the like may be realized by software by the processor interpreting and executing a program that realizes each function. Information such as programs, tables, and files for realizing each function can be stored in a recording device such as a memory, a hard disk, or an SSD (Solid State Drive), or a recording medium such as an IC card, an SD card, or a DVD.

  Further, in each of the above drawings, control lines and information lines indicate what is considered necessary for explanation, and not all control lines and information lines on the mounting are necessarily shown. For example, it may be considered that almost all configurations are actually connected to each other.

  Moreover, the arrangement | positioning form of the various function parts of the specification analyzer 100 demonstrated above, various process parts, and various databases is only an example. The arrangement form of the various functional units, the various processing units, and the various databases can be changed to an optimum arrangement form from the viewpoint of the performance of hardware and software provided in the specification analysis apparatus 100, processing efficiency, communication efficiency, and the like.

The database configuration (schema) described above can be flexibly changed from the viewpoints of efficient use of resources, improvement of processing efficiency, improvement of access efficiency, improvement of search efficiency, and the like.

100 specification analyzer, 110 information storage unit, 111 loop sentence specifying unit, 112 out-of-loop symbol execution unit, 113 in-loop symbol execution unit, 114 in-loop path specialization unit, 115 rule generation unit, 116 input / output processing unit 116 Output processing unit, 121 In-loop path generalization unit, 122 Generalization rule generation unit, 151 Source code, 152 Out-of-loop symbol execution information, 153 Out-of-loop path information, 154 In-loop symbol execution information, 155 In generalized loop Path information, 156 Out-of-loop path information, 157 Rule information, 161 Generalized looped path information, 162 Generalized ruled information, 301 Loop sentence, 302 Loop sentence, 400 Outer loop path search tree,
800 In-loop path search tree, 3000 Generalized rule display screen, S1200 In-loop path specialization process, S1500 rule generation process

Claims (10)

A device for analyzing software specifications,
A storage unit that stores a source code of a program that realizes software to be analyzed;
A loop statement specifying unit for specifying a description of a loop statement included in the source code;
By performing symbol execution on the description of the source code other than the identified loop statement, path information outside the loop, which is information including the path condition of the source code and the path execution result, is stored in the variable before the execution of the loop statement. An out-of-loop symbol execution unit that generates a value and a value of a variable after execution of the loop statement;
By executing symbol execution for the identified loop statement, for each variable included in the source code, the value of the variable after executing the loop statement n-1 times and the loop statement n times An in-loop symbol execution unit that generates path information in the generalized loop that is information indicating a relationship with the value of the variable after
An in-loop path specialization unit that generates path information in a special loop that is information on the path of the source code when the loop is executed a specific number of times;
Among the path information in the special loop generated by the path specialization unit in the loop, first path information in the special loop including a variable value when the loop is executed an arbitrary number of times is acquired, and the first By applying the generalized loop path information to the specialized loop path information, the second specialized loop path information whose number of loops is one greater than the first specialized loop path information is generated. A rule generation unit that generates rule information that is information including a rule representing the software specifications based on the second specialized loop path information and the non-loop path information;
A software specification analyzer comprising: The software specification analyzer according to claim 1,
A storage unit for storing the path information in the specialized loop generated by the path specializing unit in the loop;
The rule generation unit accepts designation of the upper limit number of loops, acquires the specialized loop path information stored in the storage unit and has the maximum number of loops, and acquires the acquired specialized loop path By recursively applying the generalized loop path information to the information to generate the specialized loop path information up to the upper limit number of loops, the generated specialized loop path information and the out-of-loop path information, Generate the rule using
Software specification analyzer. The software specification analyzer according to claim 1,
The rule generation unit receives designation of the upper limit number of loops for each loop statement included in the source code, and for each loop statement, out of the specialized loop path information stored in the storage unit The loop having the maximum number of loops is acquired, and the path information in the generalized loop is recursively applied to the acquired path information in the specialized loop for each loop statement, so that the special number up to the upper limit number of loops is obtained. Generate path information in the optimization loop,
Software specification analyzer. The software specification analyzer according to claim 1,
A general term that is a relational expression between the value of the variable and the formula including n when the loop statement is executed n times by obtaining a general term of a recurrence formula that expresses the generalized loop path information. An in-loop path generalization unit that generates in-loop path information;
A generalization rule generation unit that generates generalization rule information that is a rule expressed in a general term based on the path information in the generalization loop and the path information outside the loop;
A software specification analyzer further comprising: The software specification analyzer according to claim 4,
An output processing unit is provided that receives designation of the number of executions of the loop statement, and outputs information embodying the rule expressed by the general term by substituting the accepted number of executions into the generalized rule information. ,
Software specification analyzer. Information processing device
Storing a source code of a program realizing the software to be analyzed;
Identifying a description of a loop statement included in the source code;
By performing symbol execution on the description of the source code other than the identified loop statement, path information outside the loop, which is information including the path condition of the source code and the path execution result, is stored in the variable before the execution of the loop statement. Generating using the value and the value of the variable after execution of the loop statement;
By executing symbol execution for the identified loop statement, for each variable included in the source code, the value of the variable after executing the loop statement n-1 times and the loop statement n times Generating generalized loop path information that is information indicating the relationship with the value of the variable after
Generating path information in a specialized loop that is information on the path of the source code when the loop is executed a specific number of times;
Among the generated special loop path information, first special loop path information including a variable value when a loop is executed an arbitrary number of times is acquired, and the first special loop path information is obtained as the first special loop path information. By applying the generalized loop path information, second specialized loop path information having a loop count one greater than the first specialized loop path information is generated, and the second specialized loop information is generated. Generating rule information, which is information including rules representing the software specifications, based on the in-loop path information and the out-of-loop path information;
Execute the software specification analysis method. A software specification analysis method according to claim 6,
The information processing apparatus is
Storing the generated path information in the specialized loop;
The specification of the upper limit number of loops is accepted, the stored path information in the specialized loop is acquired with the maximum number of loops, and the path information in the generalized loop is added to the acquired path information in the specialized loop. Generating the special loop path information up to the upper limit number of loops by applying recursively, and generating the rule using the generated special loop path information and the non-loop path information;
The software specification analysis method is further executed. A software specification analysis method according to claim 6,
The information processing apparatus accepts designation of the upper limit number of loops for each loop statement included in the source code, and the maximum number of loops is stored in the stored special loop path information for each loop statement. For each loop statement, and recursively applying the path information in the generalized loop to the acquired path information in the specialized loop, and the path in the specialized loop up to the upper limit number of times of the loop Generating information,
The software specification analysis method is further executed. A software specification analysis method according to claim 6,
The information processing apparatus is
A general term that is a relational expression between the value of the variable and the formula including n when the loop statement is executed n times by obtaining a general term of a recurrence formula that expresses the generalized loop path information. Generating path information in the initialization loop,
Generating generalized rule information that is a rule expressed in a general term based on the path information in the generalized loop and the path information outside the loop;
The software specification analysis method is further executed. A software specification analysis method according to claim 9,
The information processing apparatus accepts designation of the number of executions of the loop statement, and outputs information embodying the rule expressed in the general term by substituting the accepted number of executions into the generalized rule information Step to do,
The software specification analysis method is further executed.

Images