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 CHECKING NON-TERMINATING LOOP IN SOFTWARE PROGRAMS

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 checking software programs, and, more particularly, to method and system for checking non-terminating loop in software programs.

BACKGROUND
Determining whether a given program will terminate on all possible inputs is a classical undecidable problem in computer science. Termination properties of programs are crucial for liveness and safety, where a piece of software which does not terminate can have vast consequences, especially when employed in critical environments. The latter concerns in particular library code or frameworks, whose specific use is often unknown at the time of development. Program non-termination, where there is at least one input with which a given program does not terminate, is an important problem to consider while checking software for vulnerabilities. The non-terminating loop execution may cause the program to become unresponsive leading to undesirable outcomes such as a Denial-of-Service (DoS), especially in critical software such as Open security software layers (SSL), as well as others in the past like the Microsoft Zune Z2K and the Microsoft Azure Storage service interruption. Thus, the problem of program non-termination is of great practical importance.
Existing techniques mainly focus on software verification tools which find proofs of termination and but not line of program code liable for non-terminating loop execution. While the problem of proving termination has now been extensively studied, relatively less work has been done on finding line of source code which leads to non-terminating loop in the program. The search for reliable and scalable automated methods for finding such line of program code is still widely open.
There are several techniques to check the program non-termination. The tools based on these techniques, such as automated program verification environment (AProVE), and an ultimate automizer, are standalone checkers that take a program and apply specialized pre-processing and transformations techniques before checking for non-terminating executions. However, these tools emit the evidence to non-termination as proofs in a specialized format that are hard to interpret by the developers. Further, these tools do not scale well on large programs, making it harder to adopt and integrate into the software development life cycle.

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 system for checking non-terminating loop in software programs is provided. The system includes performing a non-termination check over an input program to identify at least one non-terminating loop execution. The input program comprises one or more loops having one or more variable values. An instrumented program comprising one or more instrumented program statements is generated for the input program. Further, a coverage guided fuzzer (CGF) is performed over the input program with one or more initial test input values and store the coverage guided fuzzer generated one or more test input values in a test input database. Further, a program trace is generated for the instrumented program with each test input value to track one or more changes observed in each loop execution while assigning each variable value. The input program is further transformed into a path specified program by selecting a prefix of each terminating test input according to a prefix bound value and assigning each prefixed terminating test input value to one or more variables in sequence for loop unrolling to match with a prefix length and the program trace. The path specified program is checked to identify at least one non-terminating loop where assignment of each prefixed variable value in the one or more lines satisfies non-terminating execution.
In accordance with an embodiment of the present disclosure the input program into the path specified program by obtaining the one or more test input values and the program trace. The prefix bound is selected heuristically for loop unrolling in the program trace corresponding to each test input value in every loop of the input program, wherein the program trace includes one or more branches associated with each loop, one or more loop conditions, and one or more similar variable values occurred in each loop. The one or more prefixed variable values are substituted in the one or more lines of the input program with a numerical constant value to transform the input program into the path specified program.
In another aspect, a method for checking non-terminating loop in software programs is provided. The method includes performing a non-termination check over an input program to identify at least one non-terminating loop execution. The input program comprises one or more loops having one or more variable values. An instrumented program comprising one or more instrumented program statements is generated for the input program. Further, a coverage guided fuzzer (CGF) is performed over the input program with one or more initial test input values and store the coverage guided fuzzer generated one or more test input values in a test input database. Further, a program trace is generated for the instrumented program with each test input value to track one or more changes observed in each loop execution while assigning each variable value. The input program is further transformed into a path specified program by selecting a prefix of each terminating test input according to a prefix bound value and assigning each prefixed terminating test input value to one or more variables in sequence for loop unrolling to match with a prefix length and the program trace. The path specified program is checked to identify at least one non-terminating loop where assignment of each prefixed variable value in the one or more lines satisfies non-terminating execution.
In accordance with an embodiment of the present disclosure the input program into the path specified program by obtaining the one or more test input values and the program trace. The prefix bound is selected heuristically for loop unrolling in the program trace corresponding to each test input value in every loop of the input program, wherein the program trace includes one or more branches associated with each loop, one or more loop conditions, and one or more similar variable values occurred in each loop. The one or more prefixed variable values are substituted in the one or more lines of the input program with a numerical constant value to transform the input program into the path specified program.
In yet another aspect, a non-transitory computer readable medium for performing a non-termination check over an input program to identify at least one non-terminating loop execution. The input program comprises one or more loops having one or more variable values. An instrumented program comprising one or more instrumented program statements is generated for the input program. Further, a coverage guided fuzzer (CGF) is performed over the input program with one or more initial test input values and store the coverage guided fuzzer generated one or more test input values in a test input database. Further, a program trace is generated for the instrumented program with each test input value to track one or more changes observed in each loop execution while assigning each variable value. The input program is further transformed into a path specified program by selecting a prefix of each terminating test input according to a prefix bound value and assigning each prefixed terminating test input value to one or more variables in sequence for loop unrolling to match with a prefix length and the program trace. The path specified program is checked to identify at least one non-terminating loop where assignment of each prefixed variable value in the one or more lines satisfies non-terminating execution.
In accordance with an embodiment of the present disclosure the input program into the path specified program by obtaining the one or more test input values and the program trace. The prefix bound is selected heuristically for loop unrolling in the program trace corresponding to each test input value in every loop of the input program, wherein the program trace includes one or more branches associated with each loop, one or more loop conditions, and one or more similar variable values occurred in each loop. The one or more prefixed variable values are substituted in the one or more lines of the input program with a numerical constant value to transform the input program into the path specified program.
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 illustrates an exemplary title system for checking non-terminating loop in a software program according to some embodiments of the present disclosure.
FIG. 2 is a functional block diagram for checking non-terminating loop that is operable in the software program using the system of FIG.1, in accordance with some embodiments of the present disclosure.
FIG. 3 is a flow diagram that schematically illustrates a method for checking non-terminating loop for an example software program using the system of FIG.1, in accordance with some embodiments of the present disclosure.
FIG.4 illustrates an example execution profile for the given example software program using the system of FIG.1, in accordance with some embodiments of the present disclosure.
FIG.5 illustrates a graphical representation of comparing result evaluation of the example input program which performed for checks non-terminating loop with existing software checker tools (2LS, and Uatomizer), using the system of FIG.1, in accordance with 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 scope of the disclosed embodiments.
Embodiments herein provide a method and system for checking non-terminating loop in software programs. The system determines unintended non-termination of software program that could lead to attacks such as Denial-of-Service(DoS). The software program may be alternatively referred as an input program P. The input program P (Table 1) which embodies aspects of the present invention, is typically maintained in a permanent storage, such as a computer readable medium. The input program is said to be non-terminating if there exists an infinite run of that program from some initial states. Existing software testing techniques are not geared to detect such non-terminating loop errors. The method of the present disclosure provides a hybrid testing technique to check nontermination of the input program by combining a coverage guided fuzzing (CGF) and abstract interpretation based static analysis.
Given the input program P and the coverage test inputs generated using the CGF, the input program P is transformed into a set of smaller programs, each of which under-approximates the input program P. Abstract interpretation is then used to compute abstract reachable states for each of the set of smaller programs to check non-termination. The method provides an efficient approach for checking non-termination that reuses the test input database created as part of application testing during software development and maintenance. The disclosed system is further explained with the method as described in conjunction with FIG.1 to FIG.5 below.
Referring now to the drawings, and more particularly to FIG. 1 through FIG.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 illustrates an exemplary title system for checking non-terminating loop in a software program according to some embodiments of the present disclosure. In an embodiment, the system 100 includes one or more hardware processors 104, communication interface device(s) or input/output (I/O) interface(s) 106 (also referred as interface(s)), and one or more data storage devices or memory 102 operatively coupled to the one or more hardware processors 104. The one or more processors 104 may be one or more software processing components and/or hardware processors. In an embodiment, the hardware processors can be implemented as one or more microprocessors, microcomputers, microcontrollers, digital signal processors, central processing units, state machines, logic circuitries, and/or any devices that manipulate signals based on operational instructions. Among other capabilities, the processor(s) is/are configured to fetch and execute computer-readable instructions stored in the memory. In an embodiment, the system 100 can be implemented in a variety of computing systems, such as laptop computers, notebooks, hand-held devices, workstations, mainframe computers, servers, a network cloud, and the like.
The I/O interface device(s) 106 can include a variety of software and hardware interfaces, for example, a web interface, a graphical user interface, and the like and can facilitate multiple communications within a wide variety of networks N/W and protocol types, including wired networks, for example, LAN, cable, etc., and wireless networks, such as WLAN, cellular, or satellite. In an embodiment, the I/O interface device(s) can include one or more ports for connecting a number of devices to one another or to another server.
The memory 102 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. The memory 102 further comprises (or may further comprise) information pertaining to input(s)/output(s) of each step performed by the systems and methods of the present disclosure. In other words, input(s) fed at each step and output(s) generated at each step are comprised in the memory 102 and can be utilized in further processing and analysis.
FIG. 2 is a functional block diagram for checking non-terminating loop in a software program that is operable using the system of FIG.1, in accordance with some embodiments of the present disclosure. FIG.2 includes an instrumentation module 202, a fuzzer module 204, a test input database 206, a trace generation module 208, a path specification module 210, and a non-termination checker module 212.
The instrumentation module 202 of the system 100 generates an instrumented program P_I comprising one or more instrumented program statements for the input program. The one or more instrumented program statements are then used to generate a program trace.
The fuzzer module 204 of the system 100 generates one or more test input values to be stored in a test input database by performing a coverage guided fuzzer (CGF) over the input program and one or more initial test input values. The instrumented program P_I is compiled to generate an executable P_e and a call to the function Fuzz(P,t_i) runs the CGF over the input program P with initial test inputs t_i to generate the test input database. The CGF runs for a predefined timeout period. For each test input t?T inputs), the first P_e is executed with each test input t to generate the program trace T_P.
The test input database 206 of the system 100 stores the one or more test input values are obtained from the trace generation module 208 and the path specification module 210 for further processing.
The trace generation module 208 of the system 100 generates a program trace for the instrumented program based on each test input value.
The path specification module 210 of the system 100 transforms the input program into the path specified program. Subsequently, the function Pathspecify (P,t,T_P ) is called with original input program P, the test input t and the program trace TP which returns path specified program P_t^c. The function AbstractNTCheck (P_t^c) runs the abstract reachability based static analysis on the P_t^c to conclude if there is a loop in the input program P that does not terminate atleast once during execution.
The non-termination checker module 212 of the system 100 checks the path specified program for identifying at least one non-terminating loop. If such non-terminating loop is found in the input program P, the function returns True along with the path specified program P_t^c and the test input t for non-termination. This process repeats until every test input value in the test input database 206 are examined. If no non-terminating input is found, the method returns Unknown. The above-mentioned modules are implemented as at least one of a logically self-contained part of a software program, a self-contained hardware component, and/or, a self-contained hardware component with a logically self-contained part of a software program embedded into each of the hardware component that when executed perform the above method described herein. The present disclosure is further explained considering an example, where the system 100 identifies at least one non-terminating loop execution in the input program using the system of FIG.1 and FIG.2.
FIG. 3 is a flow diagram that schematically illustrates a method for checking non-terminating loop for an example input program using the system of FIG.1, in accordance with some embodiments of the present disclosure. In an embodiment, the system 100 comprises one or more data storage devices or the memory 102 operatively coupled to the processor(s) 104 and is configured to store instructions for execution of steps of the method 300 by the processor(s) or one or more hardware processors 104. 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 FIG.5 and the steps of flow diagram as depicted in FIG.3. Although process steps, method steps, techniques or the like may be described in a sequential order, such processes, methods, and techniques may be configured to work in alternate orders. In other words, any sequence or order of steps that may be described does not necessarily indicate a requirement that the steps to be performed in that order. The steps of processes described herein may be performed in any order practical. Further, some steps may be performed simultaneously.
Referring now to the steps of the method 300, at step 302, the one or more hardware processors 104 perform a non-termination check over an input program to identify at least one non-terminating loop execution. The input program P comprises one or more loops having one or more variable values that are read from the input program. In general, the input program P may include one or more infinite loops. To facilitate the operation, the input program P referring ( Table 1) as an example for checking non-terminating loop execution. The input program P contains one endless loop which does not terminate.
Table 1 – Example input program P
Line 1 int x,y;
Line 2 x=read_int(); // (x=1) and (y =1) are the input variables
Line 3 y=read_int();
Line 4 if(y<=0)x=-1;
Line 5 while (x>=0) // x>=0 && y==0 (non-terminating loop execution)
{
Line 6 x=read_int(); // x=5
Line 7 x=x-y*y-1;
}

In one embodiment, Table 2 depicts steps performing non-termination check using abstract reachability for the given input program P. The system 100 receives an input program P to check if the given input program P has a feasible non-terminating execution. The system 100 also has a test input database 206 generated as part of functional testing or security testing using the coverage-guided fuzzer (CGF) for non-termination check. Here, each test input value t consists of a sequence of inputs to be supplied to the input program P. Further, a prefix length t_p of the given test input value t is estimated. Then, a path specified program P' of the input program P is generated with each test input by reading function call of the P' with concrete value from the prefix length t_p. Further, the path specified program P' is then checked using an abstract interpretation based check for non-termination. If the test input value t is used to construct P' along with T_P shows non-termination of the input program P. This process is repeated for the one or more test inputs until either non-terminating behavior of the one or more test inputs are exhausted.
Table 2 –Non-termination check using abstract reachability
Input Program P, Initial test inputs t_i
P_I= Instrumented program (P),P_e=compile (P_I ),T=Fuzz(P,t_i);
For Each t?T do
T_P=Execute (P_e,t);
P_t^c=Pathspecify (P,t,T_P );
If AbstractNTCheck(P_t^c) then
return (True,P_t^c,t)
End if
End for
return (unknown, _,_)

Referring now to the steps of the method 300, at step 304, the one or more hardware processors 104, generate an instrumented program comprising one or more instrumented program statements for the input program.
The instrumentation module 204 performs the function of generating the instrumented program for the input program P. The instrumentation module 204 identifies a start line number and an end line number of each loop head comprising a loop condition for the input program P. Further, the input program is evaluated during execution of each loop condition at each conditional statement. The loop condition includes at least either one of a true condition or a false condition. Then, name variable value with associated data type are extracted to execute the start line number during the input program execution. Here, the instrumentation module 202 obtains the one or more instrumented program statements for the input program P that includes,
Source line number of each loop head having the loop condition (for example a while loop, a do-while loop, a for loop, and the like) and loop end.
Start source line number and the end line number of each conditional (for example, an If-Then-Else loop and the like) and go to statements.
Evaluated status of each conditional statement in each loop or otherwise conditional check statements satisfying either one of a true condition or a false condition as the input program executes.
Source location and data type of each variable having values assigned that are read from the input program P.
Referring now to the steps of the method 300, at step 306, the one or more hardware processors 104 perform a coverage guided fuzzer (CGF) over the input program with one or more initial test input values and store the coverage guided fuzzer generated one or more test input values in a test input database.
The fuzzer module 204 of the system 100 generates one or more test input values to be stored in the test input database 206 by performing a coverage guided fuzzer (CGF) over the input program and one or more initial test input values. The instrumentation module 202 compiles the input program P, where the fuzzer module 204 takes one or more initial test input values and fuzzes them to produce the one or more test input values that are stored into the test input database 206.
Referring now again the input program P (Table 1) considers the one or more variable inputs for,
Where, l_i:x=c denotes that x is assigned with c at the line l_i. In the input program, the non-terminating test inputs are identified by using the Coverage Guided Fuzzer (CGF). Such CGFs are widely adopted for security testing to detect vulnerabilities in the software. The CGF starts with an initial set of one or more initial test input values. Then, using a biased random search, the CGF incrementally builds the test input database 206 that covers different paths for the input program. The fuzzer module 204 also generates one or more new test inputs by randomly mutating the existing initial test input values in the test input database 206.The fuzzer module 204 identifies the prefixes of the one or more test inputs generated by the CGF and transforms the input program P into a new program using these prefixes. Further, the abstract interpretation based analysis are performed to check if the transformed program has such non-terminating loop execution.
Referring now to the steps of the method 300, at step 308, the one or more hardware processors 104 generate a program trace for the instrumented program based on each test input value to track one or more changes observed in each loop execution while assigning each variable value. The trace generation module 210 generates a program trace for each test input value for loop unrolling. Here, loop unrolling is a loop transformation technique that attempts to optimize the input program execution speed at the expense of its binary size. This program trace captures a location of one or more lines of the instrumented program, a data type of each variable associated in each loop, a loop head location, a loop exit location, and locations of go to statements that appear inside the corresponding loop. The program trace also captures the input values read with prefix bound and the location information in the program trace to map and identify the program locations in the unrolled program that requires substitution of one or more test input values from the program trace. The loop unrolled input program is transformed using this mapping information and the one or more test input values generates the path specified program P’ as depicted below in Table 3.
Table 3 – Path specified program P’ of the input program P
Line 1 int x,y;
Line 2 x=1 //(x=1) and (y=1) are the input variables
Line 3 y=1;
Line 4 if(y<=0) x=-1;
Line 5 while (x=0) //x>=0 && y==0
{ //(non-terminating loop execution)
Line 6 x=5; x=5
Line 7 x=x-y*y-1;
}

Referring now to the steps of the method 300, at step 310, the one or more hardware processors 104 transform the input program into a path specified program based on selecting a prefix for each terminating test input according to a prefix bound value and assigning each prefixed terminating test input value to one or more variables in sequence for loop unrolling to match with a prefix length and the program trace. The prefix of each terminating test input value is selected according to the prefix bound causing non-terminating execution for the input program.
The path specification program module 210 obtains one or more test input values and the program trace as input. In every loop of the input program P, the prefix bound is selected heuristically for loop unrolling in the program trace corresponding to each test input value. The program trace includes one or more branches associated with each loop, one or more loop conditions, and occurrence of one or more similar variable values in each loop. Then, the one or more prefixed variable values are substituted in the one or more lines of the input program with a numerical constant value for transforming the input program into the path specified program.
Referring now to the above example along with FIG.4, the transformation of the input program into the path specified program with one or more test input values are represented in the execution profile. FIG.4 illustrates an example execution profile for the given example software program using the system of FIG.1, in accordance with some embodiments of the present disclosure. FIG.4 shows the execution E_1, E_2 and E_3 of the input program P when it is executed with terminating test input values such as t_1, t_2, and t_3. Here, each test input value is a terminating test input value for the input program P. If an execution E_i with the newly generated test input t_i obtains a path in the input program P that is not covered in any previous run. Then, each test input t_i is added to the test input database 206 and considered for further fuzzing. If the execution E_i leads to crash or hangs (or does not process further) due to exceeding a preset duration of time, each test input t_i is stored separately for further analysis or otherwise each test input t_i is discarded. Three test inputs are considered by the present disclosure:
t_1=
t_2=
t_3=
Here, the executions E_1, E_2 and E_3 of the input program P when it is executed with test input values such as t_1, t_2, and t_3. Out of these three executions, E_1 is a non-terminating execution in which x is uniformly assigned value with x=5 in every loop iteration at line number 6. However, due to biased random search, the CGF is significantly less likely to generate such non-terminating test input t_1, when compared to t_2 and t_3. It is observed and noted that t_2 is the test input for non-termination because its prefix t_2^',
? prefix t?_2^'=
gives a way to specialize the input program in which x is uniformly assigned with value x=5 at line number 6 in every loop iteration, which manifests the non-terminating execution E_1. Thus, the search for non-terminating executions can be implemented as a search for the one or more input variables of the type terminating test input t_2, which have the prefix of the type t_2^' that can manifest the non-terminating execution, when extended suitably. The prefix of each terminating test input is selected according to a prefix bound causing non-terminating execution for the input program. It is noted that, the CGF may still generate each test input value such as t_1, whose corresponding execution E_1 leads to hang (or improper execution wherein no output is produced) and such test input value is stored separately by the CGF. Such suspended inputs are always readily available for the non-termination analysis. Even if such hanging inputs are not identified by the CGF, the prefix of other terminating provides inputs such as t_2. The prefix of each test input of type t_2^' generates the path specified program P’ for the input program P and with this prefix, wherein it checks if the resulting path specified program manifests such non-terminating execution.
The important aspect of the path specification module 210 is the ability to determine from the terminating test input value to one or more variable values that are most likely to lead non-termination of loop execution. For example, assignment x=read_int() at line 6 in the input program P. As mentioned earlier, the non-terminating execution manifests if the variable is assigned with x=5 in each of the infinite iterations of the loop as the input program executes. However, the one or more test input values are generated by the CGF which is of only a finite prefix length. It is noted that such assignments leads to terminating execution, or it has timed out. For the terminating test input value t_2,
t_2= of the input program P it is observed that the first two assignments x = 4 and x = 5 at line number 6, continues the execution within the loop.
In one embodiment for loop unroll the while loop in the input program P is used once and then the prefix of t_2 is t_2',
t_2^'= are the assigned values for the variable values. The transformed path specified program with loop unrolling is represented in Table 4, and the transformation manifests the non-terminating execution. The number of times each such loop needs to be unrolled for it to manifest the non-terminating execution, if it exists, is called the prefix bound of that loop which is a configurable parameter.
Table 4 – Loop unrolling P_(u )of the input program P
Line 1int x,y;
Line 2 x=1;
Line 3 y=1;
Line 4 if (y<=0)x=-1;
Line 5 x=4;
Line 6 x=x-y*y+1;
Line 7 while (x>=0) {
Line 8 x=5;
Line 9 x=x-y*y-1;
}
The path specified program P’ of the input program P is transformed into a specialized program by replacing statements of the type x=read_int(), with statement variable of x = 1 that assigns a constant value to variable x. The path specified program is given to the static analyser that performs an abstract reachability analysis. If the abstract reachability check concludes that the loop l in the path specified program whose exit is unreachable, then the loop does not terminate. Here, the line number is returned for the beginning of loop and the output of the loop is non-terminating.
Referring now to the steps of the method 300, at step 312, the one or more hardware processors 104 check the path specified program to identify at least one non-terminating loop where the assignment of each prefixed variable value in the one or more lines satisfies non-terminating execution.
The non-termination checker module 210 obtains the path specified program P’ as input. Here, the prefix bound is made resulting for the loop unrolled path specified program P_u, and checks if P_u manifests the non-terminating loop execution. The non-termination check is evaluated by using the abstract reachability (AI) based static analysis on the path specified program P’ using one or more domain intervals.
The non-termination checker module 210 checks and finds that the input program P has at least one non-terminating execution. If after a pre-specified duration of time (timeout) is unable to detect a non-terminating loop, it returns UNKNOWN.
Table 5 depicts abstract reachability analysis for the loop unrolling path specified program P_u. Table 5 shows the abstract program states using the interval abstract domain. Let I_x,I_y be the intervals computed by the abstract interpretation analysis.
Table 5 – Abstract reachability of loop unrolled path specified program P_u
Line 1 int x,y; //I_x,I_y :[-8,8]
Line 2 x=1; //I_x:[1,1]
Line 3 y=1; //I_x,I_y:[1,1]
Line 4 if (y<=0)x=-1;
Line 5 x=4; //I_x:[4,4]
Line 6 x=x-y*y-1; //I_x:[2,2] //I_x^(loop(0)):[2,2] //I_x^(loop(1)):[2,2]
Line 7 while (x>=0) {
Line 8 x=5; //I_x:[5,5]
Line 9 x=x-y*y-1; //I_x:[3,3]
}

They over-approximate all values that can ever be assigned to x;y when P_u executes. The importance are the interval over-approximations I_x^(loop(0)) and I_x^(loop(1)). The interval I_x^(loop(0)), x is equal to the interval value I_x after line number 6 and represents all values of variable x at the loop head just before the while loop is executed for the first time. Similarly, I_x^(loop(1)) where, x is the interval representing all values of x after executing the while loop once. It is observed that the intervals at the loop head I_x^(loop(2)), I_x^(loop(3)),…..n and after successive iterations are all equal to the I_x^(loop(1)) and represent a fixed-point or an invariant of the AI analysis. Since, I_x^(loop(1)), x is an over-approximation, immediately see that there is no value of x that can cause it to satisfy the loop exit condition i.e., x < 0 and the loop exit. Hence, the abstract interpretation analysis concludes the while loop can never terminate or alternatively P_u has the non-terminating execution.
FIG.5 illustrates a graphical representation of comparing result evaluation of the example software program which performed for checks non-terminating loop with existing software checker tools (2LS, and Uatomizer), using the system of FIG.1, in accordance with some embodiments of the present disclosure. FIG.5 shows the number of cumulative programs solved by each of the existing software checker tools over an increasing time duration. Experimental evaluation has initial fuzzing time which is upper bounded by 106 seconds, after which the trace generation and the static abstract reachability checks are performed. It is observed that there are around 300 programs for which the generation of test inputs and the non-termination check finishes in about 50 seconds. The remaining solved one or more programs utilizes the entire 106 seconds to generate the set of test inputs for non-termination. However, after this point, bulk time is spent in trace generation and the abstract reachability check. when subtract the initial test input generation time, for example by reusing each test input already generated as part of a standard test cycle. The method of the present disclosure performs non-termination check for all the 589 programs in around 50 seconds, which is comparable to the run times of the other convention tools.
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 addresses unresolved problem of checking software programs. The embodiment, thus provides method and system for checking non-terminating loop in software programs. Moreover, the embodiments herein further enables to perform non-termination check over the programs leading to denial of service. The disclosed method enables non-termination check by CGF, and abstract interpretation based static analysis. It is capable of re-using the set of test inputs generated as part of standard test cycle, allowing easy integration into a DevOps workflow.
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 processing components 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.
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 components described herein may be implemented in other components or combinations of other components. 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 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., be 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 for checking non-terminating loop in software programs, comprising:
performing (302) via one or more hardware processors, a non-termination check over an input program to identify at least one non-terminating loop execution, wherein the input program comprises one or more loops having one or more variable values;
generating (304) via the one or more hardware processors, an instrumented program comprising one or more instrumented program statements for the input program;
performing (306) via the one or more hardware processors, a coverage guided fuzzer (CGF) over the input program with one or more initial test input values and store the coverage guided fuzzer generated one or more test input values in a test input database;
generating (308), via the one or more hardware processors, a program trace for the instrumented program with each test input value to track one or more changes observed in each loop execution while assigning each variable value;
transforming (310), via the one or more hardware processors, the input program into a path specified program by selecting a prefix of each terminating test input according to a prefix bound value, and assigning each prefixed terminating test input value to one or more variables in sequence for loop unrolling to match with a prefix length and the program trace; and
checking (312), via the one or more hardware processors, the path specified program to identify at least one non-terminating loop when the assignment of each prefixed variable value in the one or more lines satisfies non-terminating execution.

2. The processor implemented method as claimed in claim 1, wherein transforming the input program into the path specified program by,
obtaining the one or more test input values and the program trace;
selecting the prefix bound heuristically for loop unrolling in the program trace corresponding to each test input value in every loop of the input program, wherein the program trace includes one or more branches associated with each loop, one or more loop conditions, and one or more similar variable values occurred in each loop; and
substituting the one or more prefixed variable values in the one or more lines of the input program with a numerical constant value for transforming the input program into the path specified program.

3. The processor implemented method as claimed in claim 1, wherein the program trace comprises a location of one or more lines of the instrumented program, a data type of each variable associated in each loop, a loop head location, and a loop exit location.

4. The processor implemented method as claimed in claim 1, wherein generating the instrumented program from the input program by,
identifying for the input program, a start line number and an end line number of each loop head having a loop condition;
evaluating the loop condition at each conditional statement of every loop associated with the input program during execution, wherein the loop condition includes at least either one of a true condition or a false condition; and
extracting each variable value with its associated data type to execute the start line number during the input program execution.

5. A system (100), for checking non-terminating loop in software programs comprising:
a memory (102) storing instructions;
one or more communication interfaces (106); and
one or more hardware processors (104) coupled to the memory (102) via the one or more communication interfaces (106), wherein the one or more hardware processors (104) are configured by the instructions to:
. perform, a non-termination check over an input program to identify at least one non-terminating loop execution, wherein the input program comprises one or more loops having one or more variable values;
generate, an instrumented program comprising one or more instrumented program statements for the input program;
perform, a coverage guided fuzzer (CGF) over the input program with one or more initial test input values and store the coverage guided fuzzer generated one or more test input values in a test input database;
generate, a program trace for the instrumented program with each test input value to track one or more changes observed in each loop execution while assigning each variable value;
transform, the input program into a path specified program by selecting a prefix of each terminating test input according to a prefix bound value, and assigning each prefixed terminating test input value to one or more variables in sequence for loop unrolling to match with a prefix length and the program trace; and
check, the path specified program to identify at least one non-terminating loop when the assignment of each prefixed variable value in the one or more lines satisfies non-terminating execution.

6. The system of claim 5, wherein transforming the input program into the path specified program by,
obtaining the one or more test input values and the program trace;
selecting the prefix bound heuristically for loop unrolling in the program trace corresponding to each test input value in every loop of the input program, wherein the program trace includes one or more branches associated with each loop, one or more loop conditions, and one or more similar variable values occurred in each loop; and
substituting the one or more prefixed variable values in the one or more lines of the input program with a numerical constant value for transforming the input program into the path specified program.

7. The system of claim 5, wherein the program trace comprises a location of one or more lines of the instrumented program, a data type of each variable associated in each loop, a loop head location, and a loop exit location.

8. The system of claim 5, wherein generating the instrumented program from the input program by,
identifying for the input program, a start line number and an end line number of each loop head having a loop condition;
evaluating the loop condition at each conditional statement of every loop associated with the input program during execution, wherein the loop condition includes at least either one of a true condition or a false condition; and
extracting each variable value with its associated data type to execute the start line number during the input program execution.

Dated this 2nd Day of November 2022

Tata Consultancy Services Limited
By their Agent & Attorney

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