Description: FORM 2

THE PATENTS ACT, 1970
(39 of 1970)
&
THE PATENT RULES, 2003

COMPLETE SPECIFICATION
(See Section 10 and Rule 13)

Title of invention:
METHOD AND SYSTEM FOR DIRECTED TEST BASED CHECKING OF PROGRAM NON-TERMINATION

Applicant

Tata Consultancy Services Limited
A company Incorporated in India under the Companies Act, 1956
Having address:
Nirmal Building, 9th floor,
Nariman point, Mumbai 400021,
Maharashtra, India

Preamble to the description:

The following specification particularly describes the invention and the manner in which it is to be performed.
TECHNICAL FIELD
The disclosure herein generally relates to the field of software testing and, more particularly, to a method and system for directed test based checking of program non-termination.
BACKGROUND
Software testing evaluates and verifies that a software product or application does what it is supposed to do. The benefits of testing include preventing bugs, reducing development costs, and improving performance. Software test automation is a method of utilizing software other than the software being tested to control the execution of tests and the comparison of actual outcomes with predicted outcomes. For example, automated testing/test automation is performed using automated testing tools for checking whether the software being developed is serving its purpose before it is released into production. Generally, the software product under testing may include non-terminating programming code. A non-terminating code can contain a condition which is never ending which leads to non-termination of a software. If a program does not terminate, it indicates flaw in the functionality of the program. For example - in a banking application, if a program that is supposed to affect a transfer of money from one account to another, does not terminate then the transaction will not occur. Similarly, a reactive system may become unresponsive if it waits for input from a non-terminating program as that input will never arrive. Hence it is crucial to identify a non-terminating programming code in the software under test.
Conventional methods rely on program analysis for proving program non-termination and hence the conventional methods do not scale or remain inconclusive. Further, the conventional methods take more time to generate non-terminating test inputs and still fail to generate such inputs in a practically acceptable time. Hence generating optimal test input for non-termination checking and thereby testing program non-termination using automated testing in a scalable manner remains unaddressed.

SUMMARY
Embodiments of the present disclosure present technological improvements as solutions to one or more of the above-mentioned technical problems recognized by the inventors in conventional systems. For example, in one embodiment, a method for Directed test based checking of program non-termination is provided. The method includes receiving, by one or more hardware processors, a programming code to be tested for non-termination, wherein the programming code comprises a plurality of looping structures. Further, the method includes selecting, by the one or more hardware processors, a regular expression from a plurality of regular expressions associated with the programming code, wherein the regular expression is selected randomly and, wherein each of the plurality of regular expressions comprises a plurality of characters and a set of quantifiers representing a specific data pattern. Furthermore, the method includes generating, by the one or more hardware processors, a test input pattern based on the regular expression using a bounded model checker for a bounded part of the programming code, wherein the test input pattern comprises a value corresponding to each of the plurality of characters associated with the regular expression. Furthermore, the method includes generating, by the one or more hardware processors, an Application Programming Interface (API) code to generate a program test input based on the generated test input pattern using a code generation technique, wherein the generated test input pattern is iteratively fed to the code generation technique by expanding values associated with the set of quantifiers in a way that conforms to the regular expression. Furthermore, the method includes generating, by the one or more hardware processors, an instrumented version of the programming code based on the generated API code and a state printing code. Furthermore, the method includes executing, by the one or more hardware processors, the instrumented version of the programming code based on the program test input generated using the generated API code until a predefined termination time and, wherein an execution trace is obtained during the execution of the instrumented version of the programming code. Furthermore, the method includes identifying, by the one or more hardware processors, a plurality of recurrent program states associated with the instrumented version of the programming code based on the execution trace. Finally, the method includes marking, by the one or more hardware processors, the programming code as one of a) a probably terminating code and b) a non-terminating code based on the plurality of recurrent program states, wherein the programming code is marked as non-terminating if there is at least one recurrent program state from among the plurality of recurrent programs states.
In another aspect, a system for Directed test based checking of program non-termination is provided. The system includes at least one memory storing programmed instructions, one or more Input /Output (I/O) interfaces, and one or more hardware processors operatively coupled to the at least one memory, wherein the one or more hardware processors are configured by the programmed instructions to receive a programming code to be tested for non-termination, wherein the programming code comprises a plurality of looping structures. Further, the one or more hardware processors are configured by the programmed instructions to select a regular expression from a plurality of regular expressions associated with the programming code, wherein the regular expression is selected randomly and, wherein each of the plurality of regular expressions comprises a plurality of characters and a set of quantifiers representing a specific data pattern. Furthermore, the one or more hardware processors are configured by the programmed instructions to generate a test input pattern based on the regular expression using a bounded model checker for a bounded part of the programming code, wherein the test input pattern comprises a value corresponding to each of the plurality of characters associated with the regular expression. Furthermore, the one or more hardware processors are configured by the programmed instructions to generate an Application Programming Interface (API) code to generate a program test input based on the generated test input pattern using a code generation technique, wherein the generated test input pattern is iteratively fed to the code generation technique by expanding values associated with the set of quantifiers in a way that conforms to the regular expression. Furthermore, the one or more hardware processors are configured by the programmed instructions to generate an instrumented version of the programming code based on the generated API code and a state printing code. Furthermore, the one or more hardware processors are configured by the programmed instructions to execute the instrumented version of the programming code based on the program test input generated using the generated API code until a predefined termination time and, wherein an execution trace is obtained during the execution of the instrumented version of the programming code. Furthermore, the one or more hardware processors are configured by the programmed instructions to identify a plurality of recurrent program states associated with the instrumented version of the programming code based on the execution trace. Finally, the one or more hardware processors are configured by the programmed instructions to mark the programming code as one of a) a probably terminating code and b) a non-terminating code based on the plurality of recurrent program states, wherein the programming code is marked as non-terminating if there is at least one recurrent program state from among the plurality of recurrent programs states.
In yet another aspect, a computer program product including a non-transitory computer-readable medium having embodied therein a computer program for Directed test based checking of program non-termination is provided. The computer readable program, when executed on a computing device, causes the computing device to receive a programming code to be tested for non-termination, wherein the programming code comprises a plurality of looping structures. Further, the computer readable program, when executed on a computing device, causes the computing device to select a regular expression from a plurality of regular expressions associated with the programming code, wherein the regular expression is selected randomly and, wherein each of the plurality of regular expressions comprises a plurality of characters and a set of quantifiers representing a specific data pattern. Furthermore, the computer readable program, when executed on a computing device, causes the computing device to generate a test input pattern based on the regular expression using a bounded model checker for a bounded part of the programming code, wherein the test input pattern comprises a value corresponding to each of the plurality of characters associated with the regular expression. Furthermore, the computer readable program, when executed on a computing device, causes the computing device to generate an Application Programming Interface (API) code to generate a program test input based on the generated test input pattern using a code generation technique, wherein the generated test input pattern is iteratively fed to the code generation technique by expanding values associated with the set of quantifiers in a way that conforms to the regular expression. Furthermore, the computer readable program, when executed on a computing device, causes the computing device to generate an instrumented version of the programming code based on the generated API code and a state printing code. Furthermore, the computer readable program, when executed on a computing device, causes the computing device to execute the instrumented version of the programming code based on the program test input generated using the generated API code until a predefined termination time and, wherein an execution trace is obtained during the execution of the instrumented version of the programming code. Furthermore, the computer readable program, when executed on a computing device, causes the computing device to identify a plurality of recurrent program states associated with the instrumented version of the programming code based on the execution trace. Finally, the computer readable program, when executed on a computing device, causes the computing device to mark the programming code as one of a) a probably terminating code and b) a non-terminating code based on the plurality of recurrent program states, wherein the programming code is marked as non-terminating if there is at least one recurrent program state from among the plurality of recurrent programs states.
It is to be understood that both the foregoing general description and the following detailed description are exemplary and explanatory only and are not restrictive of the invention, as claimed.
BRIEF DESCRIPTION OF THE DRAWINGS
The accompanying drawings, which are incorporated in and constitute a part of this disclosure, illustrate exemplary embodiments and, together with the description, serve to explain the disclosed principles:
FIG. 1 is a functional block diagram of a system for directed test based checking of program non-termination, in accordance with some embodiments of the present disclosure.
FIG. 2 illustrates a functional architecture of the system of FIG. 1, for directed test based checking of program non-termination, in accordance with some embodiments of the present disclosure.
FIG. 3A and FIG. 3B is an exemplary flow diagram illustrating a processor implemented method 300 for directed test based checking of program non-termination implemented by the system of FIG. 1 according to some embodiments of the present disclosure.
FIG. 4A through 4C depict exemplary program codes for the processor implemented method for directed test based checking of program non-termination implemented by the system of FIG. 1 according to some embodiments of the present disclosure.
FIG. 5 is an exemplary flow diagram illustrating end to end flow of data for the processor implemented method for directed test based checking of program non-termination implemented by the system of FIG. 1 according to some embodiments of the present disclosure.
DETAILED DESCRIPTION OF EMBODIMENTS
Exemplary embodiments are described with reference to the accompanying drawings. In the figures, the left-most digit(s) of a reference number identifies the figure in which the reference number first appears. Wherever convenient, the same reference numbers are used throughout the drawings to refer to the same or like parts. While examples and features of disclosed principles are described herein, modifications, adaptations, and other implementations are possible without departing from the spirit and scope of the disclosed embodiments.
Generally, a software product under testing may include non-terminating programming code. A non-terminating programming code can include a condition which is never ending which leads to non-termination of a software itself. If a program does not terminate, it indicates flaw in the functionality of the program. For example, if a program that is supposed to affect a transfer of money from one account to another in a banking application does not terminate, then the transaction will not occur. Similarly, a reactive system may become unresponsive if it waits for input from a non-terminating program as that input will never arrive. Hence it is crucial to identify a non-terminating programming code in the software under test.
Conventional methods rely on program analysis for proving program non-termination and hence the conventional methods do not scale or remain inconclusive. Further, the conventional methods take more time to generate non-terminating test inputs and still fails to generate such inputs in a practically acceptable time. Hence generating optimal test input for non-termination checking and thereby testing program non-termination using automated testing in a scalable manner remains unaddressed.
To overcome the challenges of the present disclosure, embodiments herein provide a method and system for directed test based checking of program non-termination. The present disclosure provides a system and method based on a combination of regular expressions on test inputs and bounded model checking. This novel method of test generation can detect non-termination in any kind of programming code which makes it scalable. Further, given a non-termination test input sequence, the present disclosure proves the non-termination of the test run by mining the trace for recurrent sets, which were earlier being computed statically on entire program instead of just a trace.
Initially, the system guesses a regular expression pattern for test inputs. Further the source program is transformed into another program use bound testing to generate test inputs that are likely to lead to non-terminating executions of a program. Further, the given program is transformed to restrict its inputs to the guessed regular expression of inputs. Further, bounded model checking is applied to generate a test input as per the regular expression but restricting the program execution to a small unwind bound for each of the loops in the program. The original program is executed with the test inputs generated by the model checker, such that each loop iterates up to a large, user-specified bound, such as 1 million iterations. If the program does not terminate with in the specified number of iterations, then mine the trace generated by the program execution for recurrent sets. If a recurrent set is found, then this program execution never terminates, thereby demonstrating non-termination. On the other hand, if the program terminates, then the above process is repeated by generating new test inputs.
Referring now to the drawings, and more particularly to FIGS. 1 through 5, where similar reference characters denote corresponding features consistently throughout the figures, there are shown preferred embodiments and these embodiments are described in the context of the following exemplary system and/or method.
FIG. 1 is a functional block diagram a system 100 for a directed test based checking of program non-termination, in accordance with some embodiments of the present disclosure. The system 100 includes or is otherwise in communication with hardware processors 102, at least one memory such as a memory 104, an I/O interface 112. The hardware processors 102, memory 104, and the Input /Output (I/O) interface 112 may be coupled by a system bus such as a system bus 108 or a similar mechanism. In an embodiment, the hardware processors 102 can be one or more hardware processors.
The I/O interface 112 may include a variety of software and hardware interfaces, for example, a web interface, a graphical user interface, and the like. The I/O interface 112 may include a variety of software and hardware interfaces, for example, interfaces for peripheral device(s), such as a keyboard, a mouse, an external memory, a printer and the like. Further, the I/O interface 112 may enable the system 100 to communicate with other devices, such as web servers, and external databases.
The I/O interface 112 can facilitate multiple communications within a wide variety of networks and protocol types, including wired networks, for example, local area network (LAN), cable, etc., and wireless networks, such as Wireless LAN (WLAN), cellular, or satellite. For the purpose, the I/O interface 112 may include one or more ports for connecting several computing systems with one another or to another server computer. The I/O interface 112 may include one or more ports for connecting several devices to one another or to another server.
The one or more hardware processors 102 may be implemented as one or more microprocessors, microcomputers, microcontrollers, digital signal processors, central processing units, node machines, logic circuitries, and/or any devices that manipulate signals based on operational instructions. Among other capabilities, the one or more hardware processors 102 is configured to fetch and execute computer-readable instructions stored in the memory 104.
The memory 104 may include any computer-readable medium known in the art including, for example, volatile memory, such as static random access memory (SRAM) and dynamic random access memory (DRAM), and/or non-volatile memory, such as read only memory (ROM), erasable programmable ROM, flash memories, hard disks, optical disks, and magnetic tapes. In an embodiment, the memory 104 includes a plurality of modules 106. The memory 104 also includes a data repository (or repository) 110 for storing data processed, received, and generated by the plurality of modules 106.
The plurality of modules 106 include programs or coded instructions that supplement applications or functions performed by the system 100 for directed test based checking of program non-termination. The plurality of modules 106, amongst other things, can include routines, programs, objects, components, and data structures, which performs particular tasks or implement particular abstract data types. The plurality of modules 106 may also be used as, signal processor(s), node machine(s), logic circuitries, and/or any other device or component that manipulates signals based on operational instructions. Further, the plurality of modules 106 can be used by hardware, by computer-readable instructions executed by the one or more hardware processors 102, or by a combination thereof. The plurality of modules 106 can include various sub-modules (not shown). The plurality of modules 106 may include computer-readable instructions that supplement applications or functions performed by the system 100 for directed test based checking of program non-termination. In an embodiment, the modules 106 includes a regular expression selection module (shown in FIG. 2), a test input pattern generation module (shown in FIG. 2), an Application Programming Interface (API) code generation module (shown in FIG. 2), an Instrumented version generation module (shown in FIG. 2), an Instrumented version execution module (shown in FIG. 2), a recurrent program states identification module (shown in FIG. 2), and a marking module (shown in FIG. 2). In an embodiment, FIG. 2 illustrates a functional architecture of the system of FIG. 1, for directed test based checking of program non-termination, in accordance with some embodiments of the present disclosure.
The data repository (or repository) 110 may include a plurality of abstracted piece of code for refinement and data that is processed, received, or generated as a result of the execution of the plurality of modules in the module(s) 106.
Although the data repository 110 is shown internal to the system 100, it will be noted that, in alternate embodiments, the data repository 110 can also be implemented external to the system 100, where the data repository 110 may be stored within a database (repository 110) communicatively coupled to the system 100. The data contained within such external database may be periodically updated. For example, new data may be added into the database (not shown in FIG. 1) and/or existing data may be modified and/or non-useful data may be deleted from the database. In one example, the data may be stored in an external system, such as a Lightweight Directory Access Protocol (LDAP) directory and a Relational Database Management System (RDBMS). Working of the components of the system 100 are explained with reference to the method steps depicted in FIG. 3A, FIG. 3B and FIG. 5.
FIG. 3A and FIG. 3B (creferred as FIG.3) is an exemplary flow diagram illustrating a method 300 for directed test based checking of program non-termination implemented by the system of FIG. 1 according to some embodiments of the present disclosure. In an embodiment, the system 100 includes one or more data storage devices or the memory 104 operatively coupled to the one or more hardware processor(s) 102 and is configured to store instructions for execution of steps of the method 300 by the one or more hardware processors 102. The steps of the method 300 of the present disclosure will now be explained with reference to the components or blocks of the system 100 as depicted in FIG. 1 and the steps of flow diagram as depicted in FIG. 3. The method 300 may be described in the general context of computer executable instructions. Generally, computer executable instructions can include routines, programs, objects, components, data structures, procedures, modules, functions, etc., that perform particular functions or implement particular abstract data types. The method 300 may also be practiced in a distributed computing environment where functions are performed by remote processing devices that are linked through a communication network. The order in which the method 300 is described is not intended to be construed as a limitation, and any number of the described method blocks can be combined in any order to implement the method 300, or an alternative method. Furthermore, the method 300 can be implemented in any suitable hardware, software, firmware, or combination thereof.
At step 302 of the method 300, the one or more hardware processors 102 are configured by the programmed instructions to receive a programming code to be tested for non-termination, wherein the programming code comprises a plurality of looping structures. For example, an example programming code with looping structure is illustrated in FIG. 4A. Now referring to FIG. 4A, while loop is the looping structure with non-terminating condition “x=0”. Another similar example is shown in FIG. 4C.
At step 304 of the method 300, the regular expression selection module 202 executed by one or more hardware processors 102 is configured by the programmed instructions to select a regular expression from a plurality of regular expressions associated with the programming code. In an embodiment, the regular expression is selected randomly from a regular expression database and each of the plurality of regular expressions includes a plurality of characters and a set of quantifiers representing a specific data pattern. For example, considering the regular expression “v1v2v3*”, for the example code shown in FIG. 4A, the pattern is variable v1, followed by variable v2, followed by infinite instance of variable v3. Here the ‘*’ symbol along with the variable v3 is a quantifier which can be expanded to infinite number of times. Considering the example code shown in FIG. 4C, the regular expression pattern is (v1,v2)*.
At step 306 of the method 300, the test input pattern generation module 204 executed by the one or more hardware processors 102 is configured by the programmed instructions to generate a test input pattern based on the regular expression using a bounded model checker for a bounded part of the programming code. The test input pattern includes a value corresponding to each of the plurality of characters associated with the regular expression. For example, considering the regular expression “v1v2v3*”, for the example code shown in FG. 4A, the test input pattern is “534*”. Considering the example code shown in FIG. 4C, the input pattern is (1,2)*. In an embodiment, generating the test data for the regular expression using the bounded model checker includes generating a first test data for the programming code based on the regular expression using a bounded model checker, wherein a loop bound is set to one. A second test data is generated by incrementing the loop bound by one if the first test data is generated and no recurrent states are found with loop bound one. A third test data is generated by incrementing the loop bound by one if the second test data is generated and no recurrent states are found with the incremented loop bound, wherein the loop bound is incremented until a predefined threshold and corresponding test data are generated. The next regular expression other than tested regular expression is selected one of, (i) if the loop bound associated with the current regular expression reaches the predefined threshold and (ii) no test data is generated.
At step 308 of the method 300, the Application Programming Interface (API) code generation module 206 executed by the one or more hardware processors 102 is configured by the programmed instructions to generate an Application Programming Interface (API) code to generate a program test input based on the generated test input pattern using a code generation technique. For example, the code generation technique generates code that pumps inputs according to the chosen regular expression pattern by storing repeated values in an array and returning input values by reading from the array. The generated test input pattern is iteratively inputted to the code generation technique by expanding values associated with the set of quantifiers in a way that conforms to the regular expression. For example, considering the test data “534*”, the test input pattern iteratively inputted to the code generation technique is “543”,“5433”,“543333” and the like.
At step 310 of the method 300, the instrumented version generation module 208 executed by the one or more hardware processors 102 is configured by the programmed instructions to generating an instrumented version of the programming code based on the generated API code and a state printing code. For example, considering the FIG. 4B, the code given in FIG. 4B is an instrumented version of the programming code given in FIG. 4A. Here, the values of the variables x and y are assigned with values 1.
At step 312 of the method 300, the instrumented version execution module 210 executed by the one or more hardware processors 102 is configured by the programmed instructions to execute the instrumented version of the programming code based on the program test input generated using the generated API code until a predefined termination time. An execution trace is obtained during the execution of the instrumented version of the programming code. Considering the example program given in FIG. 4A, the program consists of two variables, x and y. So, the program state is represented by the values of x and y at each line. For example, the execution trace includes:
Line 2: x = 1;
Line 3; x= 1;
Line 4: y<=0 is false;
Line 5. x >= 0 is true;
Line 6. x = 5;
Line 7: x = 3;
Line 5. x >=0 is true.
Line 6. x = 5;
Line 7: x = 3;
Line 5: x>=0 is true // recurrent state
In an embodiment, considering another example shown in FIG. 4C, the execution trace is given below:
Trace:-Line 1: x=1, inp=1
Line 2: // Program State 1
Line 3: inp=1
Line 5: x=2
Line 3: // Program State 2
Line 3: inp=2
Line 9: x=1
Line 3: // Program state 3
Line 3: inp=1
Line 5: x=2
Line 3: // Recurrent state!; same as Program State 2;
At step 314 of the method 300, the recurrent program states identification module 212 executed by the one or more hardware processors 102 is configured by the programmed instructions to identify a plurality of recurrent program states associated with the instrumented version of the programming code based on the execution trace. A recurrent state is a repeating program state which leads to non-termination of the program/software under execution. In an embodiment, the plurality of recurrent program states are identified using a token matching technique. For example, in the above mentioned trace, is a recurrent state of the program (shown in FIG. 4A and 4B), as it repeated in the second and third iterations of the loop on Line 5. This shows that it is possible to repeat a particular program state in the loop. So, to make the program run infinitely, one just has to keep supplying the same inputs to drive the loop execution to the same state. Considering the trace for the example code shown in FIG. 4C, the recurrent state is .
At step 316 of the method 300, the marking module 214 executed by the one or more hardware processors 102 is configured by the programmed instructions to mark the programming code as one of a) a probably terminating code and b) a non-terminating code based on the plurality of recurrent program states. The programming code is marked as non-terminating if there is at least one recurrent program state from among the plurality of recurrent programs states.
FIG. 5 is an exemplary flow diagram illustrating end to end flow of data for the processor implemented method for directed test based checking of program non-termination implemented by the system of FIG. 1 according to some embodiments of the present disclosure. Now referring to FIG. 5, the non-termination checking process of the present disclosure is explained as two phases, for example Generate Input() is Phase 1 and Generate Input Repeater as Phase 2. In Phase 1, at step 1, a regular expression r is selected randomly that has not yet been tried from RegXDB. RegXDB is a database including the plurality of regular expression patterns of inputs along with the implementation code of the patterns. Further at step 2, a test input t is generated based on r using a C Bounded Model Checker (CBMC), and a loop bound of 1 (that is each loop is allowed to execute only one iteration at most). At step 3, if the previous step 2 successfully generates a test inputt, then the process proceeds to Phase 2. Else, the loop bound is incremented by 1. If the new loop bound is less than U, the previous step is repeated with the new loop bound. If the new loop bound is equal to U, that means that the current pattern r may not be a good candidate for detecting non-termination, and the control is redirected to previous step 2. Step 4 constitutes Phase-2. Here, at step 4, the API is generated (RegEx API), that produces inputs for P by repeating t according to r. The resulting RegEx API is then passed to the Instrumentor, described in Step 5. At step 5, the Instrumentor generates an instrumented version of P, say P', by adding (1) the RegEx API code to P, and (2) additional code to print the state of Pat the end of each iteration of each loop in P. It then passes P' to the Executor described in Step 6. At step 6, the Executor takes as input P' and a timeout Time. It compiles and executes P' for a timeout of at most "Time". That is, if the execution does not terminate until "Time", then the Executor forcefully terminates the execution of P'. This execution of P' produces a trace of program states due to the instrumentation mentioned in Step 5. This trace is captured in an output file called "Trace", which is then passed to RS Detector, described in Step 7. At step 7, the RS Detector checks if any program state S recurred in Trace. Such a recurrence of a program state S implies that the program does not terminate. Therefore, if RS Detector finds such a recurrent S, then RegNT reports P to be non-terminating and stops. On the other hand, if such a recurrent S is not found, then the current regular expression r may not be a good candidate for revealing non-termination of P. If RegXDB has been exhausted, RegNT declares "UNKNOWN" to indicated that we are unable to conclude if P does not terminate. If RegXDB has not been exhausted, then go back to Step 1.
In an embodiment, the present disclosure is experimented as follows. Considering the source program given below, by repeatedly generating any value for input between 1 and 6, the program will run infinitely. In order to terminate, the program must receive some value outside of the range [1..6] in the if-condition. Therefore, a simple patten such as v*, that is repeat the same input v infinitely, is able to detect the non-termination by repeating either 1, or 2, or 3, or 4, or 5, or 6 , infinitely. That is, 1*, 2*, 3*, 4*, 5*, and 6* all lead to non-termination. Some other input patterns too cause non-termination. For example: 1, 2, 3, 1, 2. 4 6, 1 2, 4, 5, , 5…. : also leads to a non-terminating run. However, the non-terminating test inputs can be identified much more efficiently by focusing on the recurring patterns such as 1*, or 2*.
// source program: x.c
int main()
{
int input, output;
while (1) {
input = __VERIFIER_nondet_int();
if ((input != 1) && (input != 2) && (input != 3) && (input != 4) && (input != 5) && (input != 6)) return -2;
output = calculate_output(input);
}
return 0;
}
int calculate_output(int input)
{
return 0;
}
// Transformed program: source-x.c
int main()
{
int input, output;
input = __VERIFIER_nondet_int();
if ((input != 1) && (input != 2) && (input != 3) && (input != 4) && (input != 5) && (input != 6)) return -2;
while (1) {
output = calculate_output(input);
}
return 0;
}
int calculate_output(int input)
{
return 0;
}
cbmc --unwind 10 --no-built-in-assertions --unwinding-assertions --no-assertions source-x.c
CBMC version 5.68.0 (cbmc-5.68.0-88-g4b12cb5ed6-dirty) 64-bit x86_64 linux
Parsing source-x.c
Converting
Type-checking source-x
file source-x.c line 4 function main: function '__VERIFIER_nondet_int' is not declared
file source-x.c line 9 function main: function 'calculate_output' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Unwinding loop main.0 iteration 1 file source-x.c line 6 function main thread 0
Unwinding loop main.0 iteration 2 file source-x.c line 6 function main thread 0
Unwinding loop main.0 iteration 3 file source-x.c line 6 function main thread 0
Unwinding loop main.0 iteration 4 file source-x.c line 6 function main thread 0
Unwinding loop main.0 iteration 5 file source-x.c line 6 function main thread 0
Unwinding loop main.0 iteration 6 file source-x.c line 6 function main thread 0
Unwinding loop main.0 iteration 7 file source-x.c line 6 function main thread 0
Unwinding loop main.0 iteration 8 file source-x.c line 6 function main thread 0
Unwinding loop main.0 iteration 9 file source-x.c line 6 function main thread 0
Not unwinding loop main.0 iteration 10 file source-x.c line 6 function main thread 0
Runtime Symex: 0.00212947s
size of program expression: 123 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.0662e-05s
Passing problem to propositional reduction
METTA converting SSA
METTA 1
METTA 2
METTA: Converting Assertions <1>
METTA 3
Runtime Convert SSA: 0.000912632s
Running propositional reduction
Post-processing
Runtime Post-process: 1.7159e-05s
Solving with Glucose Syrup with simplifier
509 variables, 808 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000153937s
Runtime decision procedure: 0.00140707s
Results:
source-x.c function main
[main.unwind.0] line 6 unwinding assertion loop 0: FAILURE
1 of 1 failed (2 iterations)
VERIFICATION FAILED
The written description describes the subject matter herein to enable any person skilled in the art to make and use the embodiments. The scope of the subject matter embodiments is defined by the claims and may include other modifications that occur to those skilled in the art. Such other modifications are intended to be within the scope of the claims if they have similar elements that do not differ from the literal language of the claims or if they include equivalent elements with insubstantial differences from the literal language of the claims.
The embodiments of present disclosure herein address the unresolved problem of directed test based checking of program non-termination. The present disclosure is a combination of regular expressions on test inputs and bounded model checking which can detect non-termination in any kind of programming code which makes it scalable. Further, given a non-termination test input sequence, the present disclosure proves the non-termination of the test run by mining the trace for recurrent sets, which were earlier being computed statically on entire program instead of just a trace. Since the present disclosure generates optimal test inputs, the efficiency of the present disclosure has been improved. Hence the present disclosure is scalable and more efficient.
It is to be understood that the scope of the protection is extended to such a program and in addition to a computer-readable means having a message therein such computer-readable storage means contain program-code means for implementation of one or more steps of the method when the program runs on a server or mobile device or any suitable programmable device. The hardware device can be any kind of device which can be programmed including e.g. any kind of computer like a server or a personal computer, or the like, or any combination thereof. The device may also include means which could be e.g. hardware means like e.g. an application-specific integrated circuit (ASIC), a field-programmable gate array (FPGA), or a combination of hardware and software means, e.g. an ASIC and an FPGA, or at least one microprocessor and at least one memory with software modules located therein. Thus, the means can include both hardware means and software means. The method embodiments described herein could be implemented in hardware and software. The device may also include software means. Alternatively, the embodiments may be implemented on different hardware devices, e.g. using a plurality of CPUs, GPUs and edge computing devices.
The embodiments herein can comprise hardware and software elements. The embodiments that are implemented in software include but are not limited to, firmware, resident software, microcode, etc. The functions performed by various modules described herein may be implemented in other modules or combinations of other modules. For the purposes of this description, a computer-usable or computer readable medium can be any apparatus that can comprise, store, communicate, propagate, or transport the program for use by or in connection with the instruction execution system, apparatus, or device. The illustrated steps are set out to explain the exemplary embodiments shown, and it should be anticipated that ongoing technological development will change the manner in which particular functions are performed. These examples are presented herein for purposes of illustration, and not limitation. Further, the boundaries of the functional building blocks have been arbitrarily defined herein for the convenience of the description. Alternative boundaries can be defined so long as the specified functions and relationships thereof are appropriately performed. Alternatives (including equivalents, extensions, variations, deviations, etc., of those described herein) will be apparent to persons skilled in the relevant art(s) based on the teachings contained herein. Such alternatives fall within the scope and spirit of the disclosed embodiments. Also, the words “comprising,” “having,” “containing,” and “including,” and other similar forms are intended to be equivalent in meaning and be open ended in that an item or items following any one of these words is not meant to be an exhaustive listing of such item or items, or meant to be limited to only the listed item or items. It must also be noted that as used herein and in the appended claims, the singular forms “a,” “an,” and “the” include plural references unless the context clearly dictates otherwise. Furthermore, one or more computer-readable storage media may be utilized in implementing embodiments consistent with the present disclosure. A computer-readable storage medium refers to any type of physical memory on which information or data readable by a processor may be stored. Thus, a computer-readable storage medium may store instructions for execution by one or more processors, including instructions for causing the processor(s) to perform steps or stages consistent with the embodiments described herein. The term “computer-readable medium” should be understood to include tangible items and exclude carrier waves and transient signals, i.e. non-transitory. Examples include random access memory (RAM), read-only memory (ROM), volatile memory, nonvolatile memory, hard drives, CD ROMs, DVDs, flash drives, disks, and any other known physical storage media.
It is intended that the disclosure and examples be considered as exemplary only, with a true scope of disclosed embodiments being indicated by the following claims.
, Claims:WE CLAIM:

1. A processor implemented method (300), the method comprising:
receiving (302), by one or more hardware processors, a programming code to be tested for non-termination, wherein the programming code comprises a plurality of looping structures;
selecting (304), by the one or more hardware processors, a regular expression from a plurality of regular expressions associated with the programming code, wherein the regular expression is selected randomly and, wherein each of the plurality of regular expressions comprises a plurality of characters and a set of quantifiers representing a specific data pattern;
generating (306), by the one or more hardware processors, a test input pattern based on the regular expression using a bounded model checker for a bounded part of the programming code, wherein the test input pattern comprises a value corresponding to each of the plurality of characters associated with the regular expression;
generating (308), by the one or more hardware processors, an Application Programming Interface (API) code to generate a program test input based on the generated test input pattern using a code generation technique, wherein the generated test input pattern is iteratively fed to the code generation technique by expanding values associated with the set of quantifiers in a way that conforms to the regular expression;
generating (310), by the one or more hardware processors, an instrumented version of the programming code based on the generated API code and a state printing code;
executing (312), by the one or more hardware processors, the instrumented version of the programming code based on the program test input generated using the generated API code until a predefined termination time and, wherein an execution trace is obtained during the execution of the instrumented version of the programming code;
identifying (314), by the one or more hardware processors, a plurality of recurrent program states associated with the instrumented version of the programming code based on the execution trace; and
marking (316), by the one or more hardware processors, the programming code as one of a) a probably terminating code and b) a non-terminating code based on the plurality of recurrent program states, wherein the programming code is marked as non-terminating if there is at least one recurrent program state from among the plurality of recurrent programs states.
2. The method as claimed in claim 1, wherein a next regular expression is selected from the plurality of regular expressions for non-termination testing if no recurrent state is found using a current regular expression.
3. The method as claimed in claim 1, wherein the method of generating the test data for the regular expression using the bounded model checker comprises generating a first test data for the programming code based on the regular expression using a bounded model checker,
wherein a loop bound is set to one,
wherein a second test data is generated by incrementing the loop bound by one if the first test data is generated and no recurrent states are found with the loop bound one,
wherein a third test data is generated by incrementing the loop bound by one if the second test data is generated and no recurrent states are found with the incremented loop bound, wherein the loop bound is incremented until a predefined threshold and corresponding test data are generated, and wherein the next regular expression other than tested regular expression is selected for non-termination checking if one of, (i) if the loop bound associated with the current regular expression reaches the predefined threshold and (ii) if no test data is generated, is satisfied.
4. A system (100) comprising:
at least one memory (104) storing programmed instructions; one or more Input /Output (I/O) interfaces (112); and one or more hardware processors (102) operatively coupled to the at least one memory (104), wherein the one or more hardware processors (102) are configured by the programmed instructions to:
receive a programming code to be tested for non-termination, wherein the programming code comprises a plurality of looping structures;
select a regular expression from a plurality of regular expressions associated with the programming code, wherein the regular expression is selected randomly and, wherein each of the plurality of regular expressions comprises a plurality of characters and a set of quantifiers representing a specific data pattern;
generate a test input pattern based on the regular expression using a bounded model checker for a bounded part of the programming code, wherein the test input pattern comprises a value corresponding to each of the plurality of characters associated with the regular expression;
generate an Application Programming Interface (API) code to generate a program test input based on the generated test input pattern using a code generation technique, wherein the generated test input pattern is iteratively fed to the code generation technique by expanding values associated with the set of quantifiers in a way that conforms to the regular expression;
generate an instrumented version of the programming code based on the generated API code and a state printing code;
execute the instrumented version of the programming code based on the program test input generated using the generated API code until a predefined termination time and, wherein an execution trace is obtained during the execution of the instrumented version of the programming code;
identify a plurality of recurrent program states associated with the instrumented version of the programming code based on the execution trace; and
mark the programming code as one of a) a probably terminating code and b) a non-terminating code based on the plurality of recurrent program states, wherein the programming code is marked as non-terminating if there is at least one recurrent program state from among the plurality of recurrent programs states.
5. The system of claim 4, wherein a next regular expression is selected from the plurality of regular expressions for non-termination testing if no recurrent state is found using a current regular expression.
6. The system of claim 4, wherein the method of generating the test data for the regular expression using the bounded model checker comprises generating a first test data for the programming code based on the regular expression using a bounded model checker,
wherein a loop bound is set to one,
wherein a second test data is generated by incrementing the loop bound by one if the first test data is generated and no recurrent states are found with the loop bound one,
wherein a third test data is generated by incrementing the loop bound by one if the second test data is generated and no recurrent states are found with the incremented loop bound, wherein the loop bound is incremented until a predefined threshold and corresponding test data are generated, and wherein the next regular expression other than tested regular expression is selected for non-termination checking if one of, (i) if the loop bound associated with the current regular expression reaches the predefined threshold and (ii) if no test data is generated, is satisfied.

Dated this 10th Day of April 2023

Tata Consultancy Services Limited
By their Agent & Attorney

(Adheesh Nargolkar)
of Khaitan & Co
Reg No IN-PA-1086