CN112231225A - Symbol execution optimization method and device based on array information guidance - Google Patents
Symbol execution optimization method and device based on array information guidance Download PDFInfo
- Publication number
- CN112231225A CN112231225A CN202011197076.XA CN202011197076A CN112231225A CN 112231225 A CN112231225 A CN 112231225A CN 202011197076 A CN202011197076 A CN 202011197076A CN 112231225 A CN112231225 A CN 112231225A
- Authority
- CN
- China
- Prior art keywords
- array
- axiom
- symbol
- axioms
- information
- Prior art date
- Legal status (The legal status is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the status listed.)
- Granted
Links
- 238000000034 method Methods 0.000 title claims abstract description 67
- 238000005457 optimization Methods 0.000 title claims abstract description 20
- 230000008569 process Effects 0.000 claims abstract description 31
- 238000006243 chemical reaction Methods 0.000 claims description 6
- 230000005540 biological transmission Effects 0.000 claims description 3
- 230000002194 synthesizing effect Effects 0.000 claims description 3
- 238000012360 testing method Methods 0.000 description 11
- 238000001514 detection method Methods 0.000 description 4
- 238000013522 software testing Methods 0.000 description 4
- 238000003491 array Methods 0.000 description 2
- 230000004888 barrier function Effects 0.000 description 2
- 238000004590 computer program Methods 0.000 description 2
- 238000010276 construction Methods 0.000 description 2
- 238000005516 engineering process Methods 0.000 description 2
- 238000012986 modification Methods 0.000 description 2
- 230000004048 modification Effects 0.000 description 2
- 230000008859 change Effects 0.000 description 1
- 238000012217 deletion Methods 0.000 description 1
- 230000037430 deletion Effects 0.000 description 1
- 238000013507 mapping Methods 0.000 description 1
- 238000012545 processing Methods 0.000 description 1
- 239000013598 vector Substances 0.000 description 1
Images
Classifications
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING OR COUNTING
- G06F—ELECTRIC DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/36—Preventing errors by testing or debugging software
- G06F11/3668—Software testing
- G06F11/3672—Test management
- G06F11/3684—Test management for test design, e.g. generating new test cases
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING OR COUNTING
- G06F—ELECTRIC DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/36—Preventing errors by testing or debugging software
- G06F11/3668—Software testing
- G06F11/3672—Test management
- G06F11/3688—Test management for test execution, e.g. scheduling of test suites
Landscapes
- Engineering & Computer Science (AREA)
- Theoretical Computer Science (AREA)
- Computer Hardware Design (AREA)
- Quality & Reliability (AREA)
- Physics & Mathematics (AREA)
- General Engineering & Computer Science (AREA)
- General Physics & Mathematics (AREA)
- Debugging And Monitoring (AREA)
- Devices For Executing Special Programs (AREA)
Abstract
The invention discloses a symbol execution optimization method and a symbol execution optimization device based on array information guidance, wherein the method comprises the following steps: s1, performing symbolic execution on a middle code of a source program to be detected, traversing a middle code instruction sequence of each path in the symbolic execution process, and collecting access type information and path constraint of array variables under each path; s2, setting the offset of the character array reading operation in the symbol executor in the array access type in the source program according to the collected access type information; and S3, when the path constraint is solved, the symbol executor transmits the collected access type information and the collected offset information to a constraint solver, the constraint solver judges whether axiom redundancy exists according to the received access type information and the received offset information, if the axiom redundancy exists, the axiom of the corresponding part is not generated, and constraint solving is carried out according to the finally generated axiom. The invention can optimize the symbol execution process, avoid generating a large amount of redundant axioms during constraint solving and improve the symbol execution efficiency.
Description
Technical Field
The invention relates to the technical field of symbol execution in automatic software testing, in particular to a symbol execution optimization method and device based on array information guidance.
Background
In the software development flow, testing is an essential loop. Software testing is expected to discover bugs in software as early as possible by constructing different test cases to execute the software. The conventional test cases are generally constructed manually, so that the problems of high construction cost and low construction efficiency exist, and the ideal coverage rate is difficult to achieve. The automatic test case generation technology aims to realize automatic generation of test cases through a software means, so that the software test efficiency is improved. The symbolic execution is an important branch in the automatic test case generation technology, and the test case with high coverage rate can be effectively generated.
In the symbolic execution process, the input of the program is symbolized, the symbolic executor executes the program through symbolic input, a symbolic path condition is constructed and converted into a path constraint to be solved, and therefore a new test case is obtained. In the above process, the role of constraint solving is crucial, but it also becomes the most dominant performance bottleneck in symbolic execution. On one hand, the number of paths in the program is large, and a symbol executor needs to generate a large amount of path constraints to wait for solving; on the other hand, there are some complex data structures in the program, modeling these data structures results in generating complex path constraints, of which arrays are typical, and many popular data structures are arrays in nature, such as vectors, character strings, hash tables, and the like. Therefore, when a program using these data structures is executed symbolically, the symbolic executor generates a large number of array constraints that are difficult to solve, which results in a very inefficient generation of test cases.
In order to solve the problems, an effective solution at present is to adopt an abstract refinement array constraint solving method (CEGAR method) based on counter-example guidance, and the basic idea of the method is to abstract the original array constraint during solving, namely eliminate the read item and the write item in the original array constraint, and then refine the abstract constraint and solve by gradually adding an array axiom into the abstract constraint, wherein the array axiom is an inclusion relationship formed between an array read index and an array element; when all array axioms are added, the satisfiability of the abstract constraint is completely consistent with the satisfiability of the original array constraint. The above method is expected to obtain a final solution by adding part of array axioms, so as to achieve the purpose of accelerating array constraint solution, but in the scenario of applying to symbolic execution, the CEGAR method is sometimes not efficient. In order to support bit operations, currently, a symbol executor generally models an array by using bytes as basic units, and ignores type information of the array, that is, no matter what type the array in a source program is, the symbol executor is represented in the form of the byte array, and array constraints transmitted to a bottom solver are also in the form of the byte array, so that when the above-mentioned CEGAR method is used in a symbol execution process, a large amount of redundancy exists in an array axiom generated by the CEGAR method, and refinement is performed by using the redundant array axiom, so that not only a final solution cannot be found in advance, but also unnecessary solver calls cannot be introduced, and symbol execution still cannot be completed efficiently.
Disclosure of Invention
The technical problem to be solved by the invention is as follows: aiming at the technical problems in the prior art, the invention provides a symbol execution optimization method and device based on array information guidance, which can optimize the symbol execution process, avoid generating a large number of redundant axioms during constraint solving and improve the symbol execution efficiency.
In order to solve the technical problems, the technical scheme provided by the invention is as follows:
a symbol execution optimization method based on array information guidance comprises the following steps:
s1, performing symbol execution on a source program to be detected by using a symbol executor, traversing a middle code instruction sequence of each path in the symbol execution process, and collecting access type information and path constraint of array variables under each path;
s2, setting the offset of the internal character array reading operation of the symbol executor in the array access type in the source program according to the access type information collected in the step S1 to obtain offset information;
and S3, when the path constraint is solved, the symbol executor transmits the collected access type information and the collected offset information to a constraint solver, the constraint solver judges whether axiom redundancy exists according to the collected access type information and the collected offset information, if the axiom redundancy exists, axioms of corresponding parts are not generated, and constraint solving is carried out according to the finally remaining axioms.
Further, in the step S1, specifically, if the current instruction is an array variable declaration instruction, and the array variable in the declaration is a and the array type is T, the access type size of the array is size (T), and a data pair formed by the array variable a and the access type size (T) is stored in the map; if the current instruction is a type conversion instruction, the converted array variable is a, and the converted type is T ', the access type size of the array in the map is set to be min (size (T)), and size (T ')), wherein size (T) is the access type size of the original array variable, and size (T ') is the size of the type converted by the conversion instruction.
Further, the axiom generating step in step S3 includes:
step 301: obtaining a symbolic array read index set related to each array variable in array constraint;
step 302: traversing each symbol index in the symbolic array read index set, respectively judging whether the offsets of the corresponding character array read operations between each symbol index and the constant index are consistent according to the collected access type information and offset information, if not, judging that axiom redundancy exists, not generating axiom, otherwise, judging that axiom redundancy does not exist, and generating corresponding array axiom;
step 303: and judging whether the offsets of the corresponding character array reading operations between every two symbol indexes in the symbolic array reading index set are consistent or not according to the obtained offset information, if not, judging that axiom redundancy exists, not performing axiom generation, otherwise, judging that the axiom redundancy does not exist, and generating a corresponding array axiom.
Further, the step of determining whether axiomatic redundancy exists in step S302 includes: and performing modular operation on the collected access type information by using the constant indexes to obtain the offset of the character array reading operation corresponding to the constant indexes, obtaining the offset of the character array reading operation corresponding to each symbol index according to the offset information, judging whether the offset of the character array reading operation corresponding to each symbol index is consistent with the offset of the character array reading operation corresponding to each constant index, if not, judging that axiom redundancy exists between the two corresponding indexes, otherwise, judging that the axiom redundancy does not exist.
Further, when the axioms are generated in step S3, the method further includes a step of merging the axioms generated by the character array read operations of the same array access type in the source program.
Further, the concrete step of merging the axioms comprises: scanning all currently generated axioms, calculating the base addresses of two index items in each axiom, if the base addresses of the two index items in the two target axioms are the same, judging that the two target axioms are the axioms generated by character array reading operation in the same type in a source program, merging the two target axioms, wherein the equivalent relation of the base addresses of the two index items is used as a front piece during merging, the conjunction of the back pieces of each axiom is used as a back piece, and finally, a merged axiom is generated.
Further, after the axioms are generated in step S3, the method further includes calculating the priority of each axiom according to the number of variables associated with the index variables in the axiom, setting a plurality of priority gradients, sequentially adding the axioms according to the order of the priorities from large to small, and calling a sat solver to solve after the axiom of each priority gradient is added.
Further, the step of calculating the priority of each axiom comprises: and constructing a relation graph, if two variables appear in the same atomic constraint of the path constraint, constructing an association relation between the two variables in the relation graph, calculating the number of the variables associated with the index variables in the axioms and taking the number of the variables as the weight of the corresponding index variables, synthesizing the weights of the index variables to obtain the weight of the axioms, and setting the priority of the axioms according to the obtained weight of the axioms.
A symbol execution optimization device based on array information guidance comprises a symbol executor and a constraint solver, wherein the symbol executor comprises a type information collection module, and is used for executing symbols on intermediate codes of a source program to be tested by using the symbol executor, traversing intermediate code instruction sequences of various paths in the symbol execution process, and collecting access type information of array variables under the various paths;
the offset information setting module is used for setting the offset of the array access type of the internal character array reading operation of the symbol executor in a source program according to the access type information collected by the type information collecting module to obtain offset information;
the transmission module is used for transmitting the collected access type information and the collected offset information to a constraint solver when the current path constraint is solved;
and the constraint solver judges whether axiom redundancy exists according to the collected access type information and the collected offset information, if the axiom redundancy exists, a corresponding part axiom is not generated, and then constraint solving is carried out according to the finally generated axiom.
Further, after the axiom is generated by the constraint solver, the method also comprises the steps of calculating the priority of each axiom according to the number of variables associated with the index variables in the axiom, setting a plurality of priority gradients, sequentially adding the axioms according to the sequence of the priorities from large to small, and calling the sat solver to solve after the axiom of each priority gradient is added.
Compared with the prior art, the invention has the advantages that:
1. according to the invention, in the symbol execution process, the access type information and the offset information of the array variables under the exploration path are collected, and the collected type information and the collected offset information are transmitted to the constraint solver at the bottom layer, so that the barrier between the symbol execution and the constraint solver can be broken, the constraint solver can delete the redundant axioms by using the collected information, the generation of a large number of redundant array axioms is avoided, the number of the array axioms is effectively reduced, the constraint solver process is assisted to be optimized, the speed of the constraint solver part is effectively increased, and the efficiency of the symbol execution process is improved.
2. After the axioms are generated in the constraint solving process, the axioms generated by the character array reading operation of the same array access type in the source program are further combined, so that the number of the generated axioms can be further reduced, and the symbol execution process is optimized.
3. After the axioms are generated in the constraint solving process, a plurality of priority gradients are set by further calculating the priority of each axiom, and the axioms are sequentially added according to the priority sequence, so that the advantages of the CEGAR method can be fully utilized, heuristic abstract refinement is realized, the efficiency of the symbolic execution process is further improved, and the symbolic execution process is optimized.
Drawings
Fig. 1 is a schematic flowchart of the method for optimizing symbolic execution based on array information guidance to implement software testing according to the present embodiment.
Fig. 2 is a flowchart illustrating a specific implementation of performing constraint solving in this embodiment.
Detailed Description
The invention is further described below with reference to the drawings and specific preferred embodiments of the description, without thereby limiting the scope of protection of the invention.
As shown in fig. 1, the steps of the method for performing optimization based on array information guided symbols in the present embodiment include:
s1, performing symbol execution on a source program to be detected by using a symbol executor, traversing a middle code instruction sequence of each path in the symbol execution process, and collecting access type information and path constraint of array variables under each path;
s2, setting the offset of the internal character array reading operation of the symbol executor in the array access type in the source program according to the access type information collected in the step S1 to obtain offset information;
and S3, when the path constraint is solved, the symbol executor transmits the collected access type information and the collected offset information to a constraint solver, the constraint solver judges whether axiom redundancy exists according to the collected access type information and the collected offset information, if the axiom redundancy exists, axioms of corresponding parts are not generated, and constraint solving is carried out according to the finally remaining axioms.
In the embodiment, in the process of executing the symbol, the access type information and the offset information of the array variables under the exploration path are collected, and the collected type information and the collected offset information are transmitted to the constraint solver at the bottom layer, so that the barrier between the execution of the symbol and the solution of the constraint can be broken, the constraint solver can delete the redundant axiom by using the collected information, the generation of a large number of redundant array axioms is avoided, the number of the array axioms is effectively reduced, the process of solving the constraint is assisted to be optimized, the speed of the solution part of the constraint is effectively increased, the efficiency of the execution process of the symbol is improved, and a new test case is conveniently and efficiently generated.
When the embodiment is applied to software testing, firstly, a source code of software to be tested is input, a compiler is called to compile the software to be tested, and a middle code instruction sequence suitable for symbol execution is generated; then, the intermediate code instruction sequence of the software to be tested is used as the input of a symbol executor, the symbol input is set in the symbol executor, and the symbol execution is started; in the symbol execution process, traversing the intermediate code instruction sequence of each exploration path, collecting access type information and offset information of array variables under each path to generate a required axiom, and continuously exploring the next program path after the exploration under the current path is finished until all paths are traversed.
In this embodiment, collecting the access type information in step S1 is that, specifically, if the current instruction is an array variable declaration instruction, and the array variable in the declaration is a and the array type is T, the access type size of the array is size (T), and a data pair formed by the array variable a and the access type size (T) is stored in the map, the map records the mapping between the array variable and the type size, and the size of the array access type can be obtained by directly searching the array variable in the map subsequently; if the current instruction is a type conversion instruction, the converted array variable is a, and the converted type is T ', the access type size of the array in the map is set to be min (size (T)), and size (T ')), wherein size (T) is the access type size of the original array variable, and size (T ') is the size of the type converted by the conversion instruction. Besides the above instructions, if the current instruction is an instruction of another type, the instruction of another type may not affect the size of the access type of the array variable, and thus the processing may not be performed.
In this embodiment, access type information of array variables under each exploration path is collected from the symbol execution process, an offset of an array access type of an internal character array reading operation of a symbol executor in a source program is set according to the collected access type information, when a current path constraint is solved in step S3, the collected type information and offset information are transmitted to a constraint solver on the bottom layer, and the constraint solver determines whether a redundant axiom exists by using the information, and if so, the redundant axiom is deleted, so that generation of a large number of redundant array axioms is avoided, and the constraint solving process is optimized.
In this embodiment, the concrete steps of the axiom generation in step S3 include:
step 301: obtaining a symbolic array read index set related to each array variable in array constraint;
step 302: traversing each symbol index in the symbolic array read index set, respectively judging whether the offsets of the corresponding character array read operations between each symbol index and the constant index are consistent according to the collected access type information and the offset information, if not, judging that axiom redundancy exists, not generating axiom, otherwise, judging that the axiom redundancy does not exist, and generating corresponding array axiom;
step 303: and judging whether the offsets of the corresponding character array reading operations between every two symbol indexes in the symbolic array reading index set are consistent or not according to the obtained offset information, if not, judging that axiom redundancy exists, not performing axiom generation, otherwise, judging that the axiom redundancy does not exist, and generating a corresponding array axiom.
If the offsets of the corresponding character array reading operations between the symbol index and the constant index are not consistent, or the offsets of the corresponding character array reading operations between every two symbol indexes are not consistent, it is indicated that the axioms corresponding to the two symbol indexes are redundant and do not need to be generated. In this embodiment, each symbol index in the symbolic array read index set is traversed, and symbol indexes and constant indexes with inconsistent offsets and symbol indexes with inconsistent offsets are found according to the collected information, so that an axiom with redundancy is found out for deletion, and a constraint solving process is optimized.
In this embodiment, the specific step of determining whether there is axiom redundancy in step S302 includes: and performing modular operation on the collected access type information by using the constant indexes to obtain the offset of the character array reading operation corresponding to the constant indexes, obtaining the offset of the character array reading operation corresponding to each symbol index according to the offset information, judging whether the offset of the character array reading operation corresponding to each symbol index is consistent with the offset of the character array reading operation corresponding to each constant index, if not, judging that axiom redundancy exists between the two corresponding indexes, otherwise, judging that the axiom redundancy does not exist.
In a specific application embodiment, when axiom generation is performed, firstly, whether the axiom between each symbolic index in a symbolic array read index set is redundant or not is detected, whether the offset of the character array read operation corresponding to the symbolic index is consistent with the offset of the character array read operation corresponding to the constant index or not is specifically judged by a detection mode, wherein the offset of the character array read operation corresponding to the symbolic index is obtained according to the offset information obtained in the step S2, the offset of the character array read operation corresponding to the constant index is obtained by performing modulo operation on the size of an array access type by using the constant index, if the offset is not consistent, the axiom between two indexes at present is judged to be redundant, generation is not required, otherwise, the corresponding axiom is required to be generated; and then detecting whether axioms generated between every two symbol indexes in the symbolic array read index set are redundant, specifically judging whether offsets of character array read operations corresponding to the two symbol indexes are consistent or not by the detection mode, wherein the offsets of the character array read operations corresponding to the symbol indexes are obtained according to the offset information obtained in the step S2, if not, judging that the axioms between the two current indexes are redundant and do not need to be generated, otherwise, generating the corresponding axioms.
In this embodiment, when the axioms are generated in step S3, the method further includes a step of merging the axioms generated by the character array read operations of the same array access type in the source program, and by merging the axioms generated by the character array read operations of the same array access type in the source program, the number of generated axioms can be further reduced, and the symbol execution process is optimized.
In this embodiment, the concrete steps of merging axioms include: scanning all currently generated axioms, calculating the base addresses of two index items in each axiom, if the base addresses of the two index items in the two target axioms are the same, judging that the two target axioms are the axioms generated by character array reading operation in the same type in a source program, merging the two target axioms, wherein the equivalent relation of the base addresses of the two index items is used as a front piece during merging, the conjunction of the back pieces of each axiom is used as a back piece, and finally, a merged axiom is generated. Because the same base address is shared, the merged axiomatic front piece is formed by the base address, and the axiomatic back piece is generated by the axiomatic back piece before merging through conjunction.
When calculating the base address, the offset is subtracted from the index entry, and the axiom that the two base addresses are equal is used as a candidate for merging.
After the axioms are generated in step S3, the method further includes calculating the priority of each axiom according to the number of variables associated with the index variables in the axiom, setting a plurality of priority gradients, sequentially adding the axioms according to the order of the priorities from large to small, and calling an sat solver to solve the axiom when the axiom of each priority gradient is added.
In the embodiment, by calculating the priority of each axiom, setting a plurality of priority gradients and sequentially adding the axioms according to the priority order, the advantages of the CEGAR method can be fully utilized, heuristic abstract refinement is realized, and the efficiency of the symbol execution process is further improved.
In this embodiment, the specific step of calculating the priority of each axiom includes: and constructing a relation graph, if two variables appear in the same atomic constraint of the path constraint, indicating that the two variables are associated, constructing the associated relation between the two variables in the relation graph, calculating the number of the variables associated with the index variables in the axiom and using the number as the weight of the corresponding index variable, synthesizing the weight of each index variable to obtain the weight of the axiom, and setting the priority of each axiom according to the obtained weight of each axiom. In a specific application embodiment, the weight of the axiom may be the sum of the index variables, and the higher the weight, the higher the priority corresponding to the axiom is.
In the embodiment of the specific application, for axioms with the same weight, whether the array element value corresponding to the index is nonzero is checked, and if the array element value is nonzero, the higher the priority of the axiom is.
It is understood that the above-mentioned manner of setting the priority may also adopt other manners of setting according to actual requirements.
As shown in fig. 2, when the constraint solver performs constraint solving in the specific application embodiment, firstly, array constraints and program information including access type information and offset information are obtained from a symbol execution process, redundant axioms are found out according to the program information to be deleted, then axioms generated by character array read operations of the same array access type in a source program are merged according to the program information, then priorities of the axioms are calculated, priority gradients are set, abstract constraints are solved, when the axioms of each priority gradient are added, a sat solver is called to solve current abstract constraints, and if a solution result is an unsat, the solution result of the original array constraints is also an unsat; if the solution result is sat, the current solution needs to be substituted into the original array constraint for detection, wherein if the detection result is sat, the solution result of the original array constraint is sat, otherwise, the axiom of the next priority gradient needs to be added, the process is repeated until all the axioms are added, the solution of the original array constraint is finally obtained, and if the solution result of the original array constraint in the step is sat, a new test case is generated.
The embodiment also comprises a symbol execution optimization device guided by the array information, wherein the device comprises a symbol executor and a constraint solver, the symbol executor comprises a type information collection module, and the type information collection module is used for traversing the intermediate code instruction sequences of each path in the symbol execution process and collecting the access type information of the array variables under each path;
the offset information setting module is used for setting the offset of the array access type of the internal character array reading operation of the symbol executor in the source program according to the access type information collected by the type information collecting module to obtain offset information;
the transmission module is used for transmitting the collected access type information and the collected offset information to the constraint solver when the path constraint is solved;
and the constraint solver judges whether axiom redundancy exists according to the collected access type information and the offset information, if the axiom redundancy exists, a corresponding part axiom is not generated, and then constraint solving is carried out according to the finally generated axiom.
In this embodiment, the constraint solver includes:
the device comprises a first unit, a second unit and a third unit, wherein the first unit is used for acquiring a symbolic array read index set related to each array variable in array constraint;
the second unit is used for traversing each symbolic index in the symbolic array read index set, judging whether the offsets of the corresponding character array read operations between each symbolic index and the constant index are consistent or not according to the collected access type information and the offset information, if the offsets are inconsistent, judging that axiom redundancy exists, not generating axiom, otherwise, judging that the axiom redundancy does not exist, and generating corresponding array axiom;
and the third unit is used for judging whether the offsets of the corresponding character array reading operations between every two symbol indexes in the symbolic array reading index set are consistent or not according to the obtained offset information, judging that axiom redundancy exists and not generating axiom if the offsets are inconsistent, and judging that the axiom redundancy does not exist and generating the corresponding array axiom if the offsets are not consistent.
In this embodiment, the symbol execution optimization device based on array information guiding corresponds to the symbol execution optimization method based on array information guiding one to one, and is not described herein again one to one.
In another embodiment, the apparatus for performing optimization based on array information guided symbols of the present invention may further include: the optimization method is characterized by comprising a processor and a memory, wherein the memory is used for storing a computer program, and the processor is used for executing the computer program so as to execute the optimization method based on the symbol guided by the array information.
The foregoing is considered as illustrative of the preferred embodiments of the invention and is not to be construed as limiting the invention in any way. Although the present invention has been described with reference to the preferred embodiments, it is not intended to be limited thereto. Therefore, any simple modification, equivalent change and modification made to the above embodiments according to the technical spirit of the present invention should fall within the protection scope of the technical scheme of the present invention, unless the technical spirit of the present invention departs from the content of the technical scheme of the present invention.
Claims (10)
1. A symbol execution optimization method based on array information guidance is characterized by comprising the following steps:
s1, performing symbol execution on a source program to be detected by using a symbol executor, traversing a middle code instruction sequence of each path in the symbol execution process, and collecting access type information and path constraint of array variables under each path;
s2, setting the offset of the internal character array reading operation of the symbol executor in the array access type in the source program according to the access type information collected in the step S1 to obtain offset information;
and S3, when the path constraint is solved, the symbol executor transmits the collected access type information and the collected offset information to a constraint solver, the constraint solver judges whether axiom redundancy exists according to the collected access type information and the collected offset information, if the axiom redundancy exists, axioms of corresponding parts are not generated, and constraint solving is carried out according to the finally generated axiom.
2. The method for optimizing symbolic execution based on array information guidance according to claim 1, wherein in step S1, if the current instruction is an array variable declaration instruction, and the array variable in the declaration is a and the array type is T, the access type size of the array is size (T), and a data pair consisting of the array variable a and the access type size (T) is stored in the map; if the current instruction is a type conversion instruction, the converted array variable is a, and the converted type is T ', the access type size of the array in the map is set to be min (size (T)), and size (T ')), wherein size (T) is the access type size of the original array variable, and size (T ') is the size of the type converted by the conversion instruction.
3. The method for performing optimization based on array information guided symbolic execution according to claim 1, wherein the axiom generating step in step S3 comprises:
step 301: obtaining a symbolic array read index set related to each array variable in array constraint;
step 302: traversing each symbol index in the symbolic array read index set, respectively judging whether the offsets of the corresponding character array read operations between each symbol index and the constant index are consistent according to the collected access type information and offset information, if not, judging that axiom redundancy exists, not generating axiom, otherwise, judging that axiom redundancy does not exist, and generating corresponding array axiom;
step 303: and judging whether the offsets of the corresponding character array reading operations between every two symbol indexes in the symbolic array reading index set are consistent or not according to the obtained offset information, if not, judging that axiom redundancy exists, not performing axiom generation, otherwise, judging that the axiom redundancy does not exist, and generating a corresponding array axiom.
4. The method of claim 3, wherein the step of determining whether axiomatic redundancy exists in step S302 comprises: and performing modular operation on the collected access type information by using the constant indexes to obtain the offset of the character array reading operation corresponding to the constant indexes, obtaining the offset of the character array reading operation corresponding to each symbol index according to the offset information, judging whether the offset of the character array reading operation corresponding to each symbol index is consistent with the offset of the character array reading operation corresponding to each constant index, if not, judging that axiom redundancy exists between the two corresponding indexes, otherwise, judging that the axiom redundancy does not exist.
5. The method for optimizing symbolic array execution based on array information guide according to any one of claims 1 to 4, wherein when generating axioms in step S3, the method further comprises the step of merging axioms generated by character array read operations of the same array access type in a source program.
6. The method of claim 5, wherein the specific step of merging the axioms comprises: scanning all currently generated axioms, calculating the base addresses of two index items in each axiom, if the base addresses of the two index items in the two target axioms are the same, judging that the two target axioms are the axioms generated by character array reading operation in the same type in a source program, merging the two target axioms, wherein the equivalent relation of the base addresses of the two index items is used as a front piece during merging, the conjunction of the back pieces of each axiom is used as a back piece, and finally, a merged axiom is generated.
7. The method for performing optimization on symbolic execution based on array information guidance according to any one of claims 1 to 4, wherein after the axioms are generated in step S3, the method further comprises the steps of calculating the priority of each axiom according to the number of variables associated with index variables in the axiom, setting a plurality of priority gradients, sequentially adding the axioms according to the order of the priorities from large to small, and calling an sat solver to solve after the axiom of each priority gradient is added.
8. The method of claim 7, wherein the step of calculating the priority of each axiom comprises: and constructing a relation graph, if two variables appear in the same atomic constraint of the path constraint, constructing the association relation between the two variables in the relation graph, calculating the number of the variables associated with the index variables in the axioms and taking the number of the variables as the weight of the corresponding index variables, synthesizing the weights of the index variables to obtain the weight of the axioms, and setting the priority of the axioms according to the obtained weight of the axioms.
9. The symbol execution optimization device based on array information guidance comprises a symbol executor and a constraint solver, and is characterized in that the symbol executor comprises a type information collection module, wherein the type information collection module is used for performing symbol execution on a middle code of a source program to be tested by using the symbol executor, traversing a middle code instruction sequence of each path in the symbol execution process, and collecting access type information of array variables under each path;
the offset information setting module is used for setting the offset of the array access type of the internal character array reading operation of the symbol executor in a source program according to the access type information collected by the type information collecting module to obtain offset information;
the transmission module is used for transmitting the collected access type information and the collected offset information to a constraint solver when the current path constraint is solved;
and the constraint solver judges whether axiom redundancy exists according to the collected access type information and the collected offset information, if the axiom redundancy exists, a corresponding part axiom is not generated, and then constraint solving is carried out according to the finally generated axiom.
10. The apparatus for performing symbol optimization based on array information guide according to claim 9, wherein the generation of the axioms by the constraint solver further comprises calculating the priority of each axiom according to the number of variables associated with index variables in the axiom, setting a plurality of priority gradients, sequentially adding the axioms according to the order of the priorities from large to small, and calling the sat solver to perform solution after the axiom of each priority gradient is added.
Priority Applications (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN202011197076.XA CN112231225B (en) | 2020-10-30 | 2020-10-30 | Symbol execution optimization method and device based on array information guidance |
Applications Claiming Priority (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN202011197076.XA CN112231225B (en) | 2020-10-30 | 2020-10-30 | Symbol execution optimization method and device based on array information guidance |
Publications (2)
| Publication Number | Publication Date |
|---|---|
| CN112231225A true CN112231225A (en) | 2021-01-15 |
| CN112231225B CN112231225B (en) | 2024-02-27 |
Family
ID=74121615
Family Applications (1)
| Application Number | Title | Priority Date | Filing Date |
|---|---|---|---|
| CN202011197076.XA Active CN112231225B (en) | 2020-10-30 | 2020-10-30 | Symbol execution optimization method and device based on array information guidance |
Country Status (1)
| Country | Link |
|---|---|
| CN (1) | CN112231225B (en) |
Cited By (1)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| CN114238154A (en) * | 2022-02-24 | 2022-03-25 | 湖南泛联新安信息科技有限公司 | Symbol execution method, unit testing method, electronic device and storage medium |
Citations (2)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US20070033576A1 (en) * | 2005-08-04 | 2007-02-08 | Microsoft Corporation | Symbolic execution of object oriented programs with axiomatic summaries |
| CN106599695A (en) * | 2016-06-03 | 2017-04-26 | 南京大学 | Bootable symbolic execution vulnerability detection method based on path combination |
-
2020
- 2020-10-30 CN CN202011197076.XA patent/CN112231225B/en active Active
Patent Citations (2)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US20070033576A1 (en) * | 2005-08-04 | 2007-02-08 | Microsoft Corporation | Symbolic execution of object oriented programs with axiomatic summaries |
| CN106599695A (en) * | 2016-06-03 | 2017-04-26 | 南京大学 | Bootable symbolic execution vulnerability detection method based on path combination |
Non-Patent Citations (2)
| Title |
|---|
| RAIMONDAS SASNAUSKAS: "Integration Testing of Protocol Implementations using Symbolic Distributed Execution", 《IEEE》, pages 1 - 6 * |
| 李领桂: "基于形式化方法的软件代码安全性验证技术", 《中国优秀硕士论文全文数据库信息科技辑》, pages 138 - 285 * |
Cited By (2)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| CN114238154A (en) * | 2022-02-24 | 2022-03-25 | 湖南泛联新安信息科技有限公司 | Symbol execution method, unit testing method, electronic device and storage medium |
| CN114238154B (en) * | 2022-02-24 | 2022-05-06 | 湖南泛联新安信息科技有限公司 | Symbol execution method, unit testing method, electronic device and storage medium |
Also Published As
| Publication number | Publication date |
|---|---|
| CN112231225B (en) | 2024-02-27 |
Similar Documents
| Publication | Publication Date | Title |
|---|---|---|
| US5146594A (en) | Method of producing object program based on interprocedural dataflow analysis of a source program | |
| US8943487B2 (en) | Optimizing libraries for validating C++ programs using symbolic execution | |
| US20040230957A1 (en) | Methods for comparing versions of a program | |
| US10394694B2 (en) | Unexplored branch search in hybrid fuzz testing of software binaries | |
| US20130067441A1 (en) | Profile guided jit code generation | |
| US20050268195A1 (en) | Apparatus and method for improving emulation speed of high-level languages in on-chip emulation systems | |
| CN111104335B (en) | C language defect detection method and device based on multi-level analysis | |
| CN102609241B (en) | hot patch method and device | |
| CN113497809B (en) | MIPS framework vulnerability mining method based on control flow and data flow analysis | |
| He et al. | Sofi: Reflection-augmented fuzzing for javascript engines | |
| CN106599695B (en) | A kind of bootable semiology analysis leak detection method merged based on path | |
| US5396627A (en) | Method of producing object program based on interprocedural dataflow analysis of a source program | |
| CN102099781A (en) | Branch predicting device, branch predicting method thereof, compiler, compiling method thereof, and medium for storing branch predicting program | |
| US20120192162A1 (en) | Optimizing Handlers for Application-Specific Operations for Validating C++ Programs Using Symbolic Execution | |
| US20130262824A1 (en) | Code generation method, and information processing apparatus | |
| CN115017516A (en) | Fuzzy test method based on symbolic execution | |
| CN114138669A (en) | Software automatic testing method based on function level selection symbolized mixed execution | |
| CN112231225B (en) | Symbol execution optimization method and device based on array information guidance | |
| CN114238154B (en) | Symbol execution method, unit testing method, electronic device and storage medium | |
| CN111259619B (en) | Control method and device for configuration object, storage medium and verification platform | |
| JP6955162B2 (en) | Analytical equipment, analysis method and analysis program | |
| CN117331826A (en) | Mixed fuzzy test optimization method for mining security holes | |
| CN112860544B (en) | Code detection method, device, equipment and computer readable storage medium | |
| CN114706759B (en) | Symbol execution optimization method based on partial solution of segmentation and reuse | |
| WO2021104027A1 (en) | Code performance testing method, apparatus and device, and storage medium |
Legal Events
| Date | Code | Title | Description |
|---|---|---|---|
| PB01 | Publication | ||
| PB01 | Publication | ||
| SE01 | Entry into force of request for substantive examination | ||
| SE01 | Entry into force of request for substantive examination | ||
| GR01 | Patent grant | ||
| GR01 | Patent grant |