FORM 2
THE PATENTS ACT, 1970
(39 of 1970)
&
THE PATENTS RULES, 2003
COMPLETE SPECIFICATION
(See section 10, rule 13)
1. Title of the invention: ABSTRACTION OF LOOPS IN PROGRAMS
2. Applicant(s)
NAME
NATIONALITY
ADDRESS
TATA CONSULTANCY SERVICES LIMITED
Indian
Nirmal Building, 9th Floor, Nariman Point, Mumbai, Maharashtra 400021, India
3. Preamble to the description
COMPLETE SPECIFICATION
The following specification particularly describes the invention and the manner in which it is to be performed.
1
2
FIELD OF INVENTION
[0001] The present subject matter relates to data abstraction and, particularly but not exclusively, to loop abstraction in a computer program.
BACKGROUND
[0002] A computer program is a sequence of codes written in a programming language to perform a specified task in a computing device, such as a computer and a laptop. The computer program, also referred to as a program, usually includes one or more execution statements that are executed for performing the specified task. The statements are generally provided in a sequential form with the program execution beginning from execution of a first statement and ending with execution of a last statement. However, in complex programs, the statements may be provided in the form of loops such that a particular set of statements is executed in a given sequence repeatedly until a loop termination condition is reached. On execution of the last statement in such cases, it is first determined whether the termination condition has been achieved or not. If the termination condition is not achieved, the given sequence starting from the first statement is executed again, otherwise the loop in the program is terminated.
[0003] While executing such programs having loops, errors may be encountered in cases of indefinite loops or loops having large loop bounds. The loop bounds may be understood as the maximum number of times a loop has to be executed. Generally, in order to ensure error free execution of the program, the program is initially checked for errors, for example, by a program analyzer or a model checker of the computer device. The model checker is configured to analyze the program and check for various errors that may occur on execution of the program.
[0004] However, loops for which either the loop bounds are very large or the loop bounds can not be identified during the analysis, the model to analyze the loops by unrolling the loops a finite number of times based on loop bound of the loop being analyzed. The loop bound may be defined as a loop limit corresponding to the maximum number of times a loop may be executed. Large loop bounds or failure of the compiler in identifying such loop bounds may result in failure of the checking process.
[0005] Generally, loops for which a bound can be determined statically, i.e., without actually testing the program code through execution are unrolled a finite number of times
3
properly without any errors. However, for the loops having indefinite or large bounds, an upper bound, i.e., a maximum limit for loop execution is explicitly provided by the model checker. Determining the upper bound may however, be a time consuming and difficult task for the model checker as the model checker may not have sufficient intelligence for ascertaining such a bound. Further, providing an inadequate, i.e., a smaller bound than required may cause the bounded model checker to produce results, such as a loop unwinding assertion failure. Additionally, in both the cases of a smaller bound and a larger bound the model checker may produce an “out of memory” failure. Therefore it may not be feasible to verify loops having indefinite or large bounds using a bounded model checker.
[0006] Other conventional techniques involve loop abstraction for model checking and verification. Loop abstraction, as will be understood, refers to an abstraction technique in which behavior of a loop of the program is abstracted and the loop, hereinafter referred to as an original loop, is replaced by another loop, hereinafter referred to as an abstracted loop. The abstracted loop is defined such that apart from having the same behavior as the original loop, the abstracted loop also shows additional behavior, such as capability of executing variables having such values with which the original loop may not have executed as compared to the original loop. One such approach relates to loop abstraction based on number of transitions that a loop goes through. Abstracting loops based on the number of transitions may however not be efficient for indefinite loops as in such cases the number of transitions may not be determined accurately, thus affecting the efficiency of model checking.
[0007] Another conventional technique of loop abstraction involves unrolling a given loop twice. Initially, the given loop is unrolled n number of times followed by resetting all variables updated in the loop body during the unrolling. The loop is subsequently unrolled m number of times. However, using the present technique may not be useful for verifying certain loops having complex conditions as all the variables updated during loop unrolling are not reset in every iteration of the loop unrolling, thus affecting subsequent unrolling. Further, the value of m is a configurable parameter and is not evaluated for efficiency. The model checker may thus either run out of memory or cause loop unwinding assertion failures.
[0008] Yet another conventional technique involves predicate abstraction for verification. The predicate abstraction typically involves mapping concrete data types to abstract data types
4
through predicates over the concrete data. However, using predicate abstraction for large programs may be infeasible due to the computational costs associated with the technique.
[0009] According to an embodiment of the present subject matter, systems and methods implementing loop abstraction in a program written in a programming language are described. The systems and methods can be implemented in a variety of computing devices. The computing devices include, but are not limited to, desktop computers, hand-held devices, laptops or other portable computers, and the like. In one implementation, the systems and methods implementing loop abstraction may be provided for loop abstraction in programs written using programming languages including, but not limited to, C, C++, VC++, C#, and the like.
[0010] In one implementation, the program to be executed in the computing device includes an original loop having an original loop body and an original loop statement defining, among other things, a termination condition for the original loop. The program is initially received for verification and error analysis before being executed. In one implementation, the original loop is analyzed to determine one or more loop parameters associated with the original loop. The loop parameters may include, for example, and not as a limitation, an original loop condition, one or more loop variables, and number of paths.
[0011] The original loop condition may be understood as the termination condition present in the original loop statement. The loop variables may be understood as the variables provided in the original loop for being used or modified during loop execution. The loop variables may be further classified as input variables, output variables, and input-output (IO) variables. The input variables are the variables that are read only, i.e., just provide input to the original loop, and are thus not modified during loop execution. The output variables on the other hand are the ones that are modified during the loop execution and also used outside the loop. The IO variables are the ones that are used for providing input and are modified during the loop execution.
[0012] The number of paths may refer to the number of paths possible during execution of the original loop. A path may be understood as a particular sequence of statements followed during the loop execution. Thus if the original loop can be executed by following different sequences of the statements, the original loop may have more than one paths.
5
[0013] Further, a finite loop bound for the abstracted loop is ascertained based on the loop parameters of the original loop. In one implementation, the loop bound is ascertained based on the number of paths and the number of output variables. For instance, the loop bound may be equal to a minimum value from among the number of paths and the number of output variables. Subsequently, the original loop may be replaced by an abstracted loop. For the purpose, the original loop may be removed from the program and an abstracted loop statement having the original loop condition and the loop bound may be added to the program to initiate the abstracted loop. Further, the original loop body may be added to complete the abstracted loop. Using the original loop condition and the original loop body in the abstracted loop helps in ensuring that the abstracted loop at least has the same properties as the original loop.
[0014] In one implementation, the IO variables in the abstracted loop may be defined by assigning non-deterministic values to each of the IO variables. In one implementation, the non-deterministic values may be assigned using a nondet (v) configured to non-deterministically assign values to all variables in set “v”. In one implementation, the values may be selected from a range determined based on predefined parameters, such as an user input or a data type of the IO variables. For example, for an unsigned character type IO variable "v” in C language, the non-deterministic values may be assigned from a range between 0 and 255. Providing the non-deterministic values to the IO variables helps in ensuring that the loop is able to assign all possible values to the IO variables during execution, irrespective of whether those values could have been assigned during execution of the original loop or not. Additionally, a first assume statement and a second assume statement may be inserted after the IO variables and the abstracted loop, respectively in the abstracted loop. In one implementation, the first assume statement holds the original loop condition as true while the loop is being executed. The second assume statement, on the other hand, holds the original loop condition as false after the abstracted loop is executed. Adding the first assume statement helps in ensuing that the abstracted loop is always executed with the original loop condition true even if the non-deterministic values assigned to the IO variables do not satisfy the original loop condition. Similarly, adding the second assume statement helps in ensuring that the original loop condition is false after the abstracted loop is executed to ensure that for the rest of the program the original loop condition is always provided as false as it would have been in the original loop where the loop would have terminated only on the original loop condition being false.
6
[0015] The systems and methods of the present subject matter thus facilitate in implementing loop abstraction in a program for replacing erroneous loops in the program. Providing the finite loop bound helps in ensuring that the loop is executed only a fixed number of times thus reducing the costs and errors, such as memory overflow or loop unwinding assertion failures caused due to execution of loops having indefinite or large loop bounds. Further, defining the finite loop bound based on the number of paths and the number of output variables helps in ensuring that the loop is executed a minimum number of times the original loop might have executed.
[0016] These and other advantages of the present subject matter would be described in greater detail in conjunction with the following figures. While aspects of described systems and methods for loop abstraction in a program can be implemented in any number of different computing systems, environments, and/or configurations, the embodiments are described in the context of the following exemplary system(s).
[0017] Figure 1 illustrates exemplary components of a computing device 102 implementing loop abstraction in a program written in a programming language, in accordance with an embodiment of the present subject matter. Examples of the computing device 102 include, but are not limited to, mainframe computers, workstations, personal computers, desktop computers, minicomputers, servers, multiprocessor systems, laptops, a cellular communicating device, such as a personal digital assistant, a smart phone, and a mobile phone; and the like. The computing device 102 includes one or more processor(s) 104, I/O interface(s) 106, and a memory 108 coupled to the processor 104. The processor 104 can be a single processing unit or a number of units, all of which could also include multiple computing units. The processor 104 may 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 104 is configured to fetch and execute computer-readable instructions and data stored in the memory 108.
[0018] Functions of the various elements shown in the figures, including any functional blocks labeled as “processor(s)”, may be provided through the use of dedicated hardware as well as hardware capable of executing software in association with appropriate software. When
7
provided by a processor, the functions may be provided by a single dedicated processor, by a single shared processor, or by a plurality of individual processors, some of which may be shared. Moreover, explicit use of the term “processor” should not be construed to refer exclusively to hardware capable of executing software, and may implicitly include, without limitation, digital signal processor (DSP) hardware, network processor, application specific integrated circuit (ASIC), field programmable gate array (FPGA), read only memory (ROM) for storing software, random access memory (RAM), and non volatile storage. Other hardware, conventional and/or customized, may also be included.
[0019] The I/O interfaces 106 may include a variety of software and hardware interfaces, for example, interface for peripheral device(s), such as a keyboard, a mouse, an external memory, and a printer. Further, the I/O interfaces 106 may enable the computing device 102 to communicate with other computing devices, such as a personal computer, a laptop, and like.
[0020] The memory 108 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 108 also includes module(s) 110 and data 112.
[0021] The module(s) 110 include routines, programs, objects, components, data structures, etc., which perform particular tasks or implement particular abstract data types. The module(s) 110 further include a program analysis module 114, an abstraction module 116, and other module(s) 118. The other module(s) 118 may include programs or coded instructions that supplement applications and functions of the computing device 102.
[0022] On the other hand, the data 112, amongst other things, serves as a repository for storing data processed, received, and generated by one or more of the module(s) 110. The data 112 includes, for example, original loop data 120, abstraction data 122, and other data 124. The other data 124 includes data generated as a result of the execution of one or more modules in the other module(s) 118.
[0023] In one implementation, the computing device 102 is configured to abstract loops included in a computer program, hereinafter referred to as a program. For the purpose, the program is initially received by the program analysis module 114. In one implementation, the
8
program analysis module 114 may receive the program from a compilation module (not shown in the figure) internal to the computing device 102. In another implementation, the program analysis module 114 may receive the program from a compilation module (not shown in the figure) external to the computing device 102.
[0024] For example, the computing device 102 may receive the following program for loop abstraction
void xmi t (int nP, struct reqr) ........... (1)
{ ........... (2)
nPO = nP − 1; ........... (3)
while (nP!=nPO) ........... (4)
{ ........... (5)
state = L; ........... (6)
nPO = nP; ........... (7)
r = glb; ........... (8)
if (r && r−>status) ........... (9)
{ ........... (10)
glb = r−>Next; ........... (11)
state= U; ........... (12)
r−>status = 0; ........... (13)
nP ++; ........... (14)
} ........... (15)
} ........... (16)
assert (state!=U); ........... (17)
state= U; ........... (18)
} ........... (19)
[0025] On receiving the program, the program analysis module 114 saves the program in the original loop data 120 and analyzes syntax of the program to identify an original loop for which the loop abstraction may be performed. The original loop may include an original loop body and an original loop statement. The original loop statement may be defined as the statement in the program that is provided to initiate a loop. The original loop statement typically includes, among other things, a termination condition for the original loop. For example, in a “for” loop,
9
the first statement “(for i =0; i<10; i++)” defining the “for loop” may be referred to as the original loop statement. Further, the original loop body may be defined as a set of one or more statements involving loop variables that are executed during the loop execution. For instance, in the previous example of the program received by the computing device 102, the program analysis module 114 may analyze the program to identify the original loop as beginning from the line (4), i.e., “while (nP!=nPO)” and ending at the line (16), i.e., “}”. Further, the program analysis module 114 may analyze the original loop to identify the original loop body and the original loop statement. In said example, the program analysis module 114 may identify the statement at the line (4), i.e., “while (nP!=nPO)” as the original loop statement. On analyzing the line (4), the program analysis module 114 may ascertain that the original loop is a while loop with the original loop statement having just the termination condition for the original loop. The program analysis module 114 may further analyze the original loop to identify the original loop body as beginning from the line (6), i.e., “state=L;” and ending at the line (15), i.e., “}”. The program analysis module 114 may subsequently save the original loop statement and the original loop body in the original loop data 120.
[0026] Further, the program analysis module 114 may analyze the original loop to determine one or more loop parameters associated with the original loop. In one implementation, the loop parameters include an original loop condition, one or more loop variables, and number of paths. The original loop condition may be understood as the termination condition present in the original loop statement. Thus, for all loop iterations with the original loop condition being true the original loop gets executed and as soon as the original loop condition becomes false the loop is terminated. In one implementation, the program analysis module 114 may analyze the original loop statement to identify the original loop condition. For example, in the previous example of the program received by the computing device 102, the program analysis module 114 may analyze the original loop statement to identify the original loop condition as “nP!=nPO”.
[0027] The program analysis module 114 may further analyze the original loop to identify the loop variables. In one implementation, the loop variables are further classified as input variables, output variables, and input-output (IO) variables. The variables that provide input to the original loop and are not modified during loop execution are identified as the input variables. The variables that are modified during the loop execution and read later, i.e., outside the loop, are defined as the output variables. The variables that are provided both for being read,
10
i.e., providing input and for modification during the loop execution are ascertained as the IO variables. For example, in the previous example of the program received by the computing device 102, the program analysis module 114 may analyze the original loop body to identify the variable “state” as the output variable, the variables “nPO”; “nP”; “r”; and “glb” as the IO variables, and the variables “L” and “U” as the input variables. In one implementation, the program analysis module 114 identifies the loop variables by statically analyzing the original loop. Further, in case loop includes the output variables in the form of arrays, the program analysis module 114 may determine the number of output variables based on number of elements of the array that will be used outside the loop if that array is present on the left hand side of an assignment statement indexed by an expression containing IO variables in the loop. However, in case the number of array elements that will be used outside the loop is not known, the program analysis module 114 may determine the number of output variables based on the total number of array elements. For instance, in case a loop includes an array of size five, i.e., the array includes five array elements out of which elements 1, 2, and 3 are being accessed outside the loop, then the program analysis module 114 may determine the array elements 1, 2, and 3 as the output variables. However, if all elements are being accessed outside the loop, then the program analysis module 114 may determine the array elements 1, 2, 3, 4, and 5 as the output variables. In one implementation, the program analysis module 114 may determine the number of output variables by statically analyzing the original loop body.
[0028] The program analysis module 114 further determines the number of paths in the original loop body. The number of paths may be defined as the number of paths that may be possibly followed during execution of the original loop. As will be understood, during different executions of a loop body, the statements may be executed in different sequences depending on control structures, i.e., the statements controlling the loop execution present inside the loop body. Each such sequence of statements followed during the loop execution may thus be understood as a path. Thus, if the original loop can be executed by following different sequences of the statements, the original loop may have more than one path. Further, in case a loop includes the IO variables in the form of arrays, the program analysis module 114 may determine the number of paths based on number of elements of the array that will be used outside the loop. However, in case the number of elements that will be used outside the loop is not known, the program analysis module 114 may determine the number of paths based on the total number of elements
11
of the array. For instance, in case a loop includes an array of size five, i.e., the array includes five elements out of which elements 1, 2, and 3 are being accessed outside the loop, then the program analysis module 114 may determine the number of paths as three. However, if all elements are being accessed outside the loop, then the program analysis module 114 may determine the number of paths as five. In one implementation, the program analysis module 114 may determine the number of paths by statically analyzing the original loop body.
[0029] For instance, in the previous example of the program received by the computing device 102, the program analysis module 114 may analyze the original loop body to ascertain the number of paths as two.
[0030] The program analysis module 114 may subsequently save the loop parameters in the original loop data 120. The program analysis module 114 subsequently ascertains a finite loop bound for the abstracted loop. The program analysis module 114 is configured to ascertain the finite loop bound based on the loop parameters of the original loop. In one implementation, the program analysis module 114 ascertains the finite loop bound based on the number of paths and the number of output variables. The program analysis module 114 initially compares the number of paths and the number of output variables to determine a minimum value from among them. The minimum value thus determined may be assigned as the finite loop bound by the program analysis module 114. Further, the program analysis module 114 may save the finite loop bound in the original loop data 120. Assigning the minimum value from among the number of paths and the number of output variables ensures that the finite bound is not too large to cause any model checker to go out of memory. Further, the minimum value also helps in ensuring that the loop is at least executed a minimum number of times that would have been required to modify variables that are available outside the original loop body thus avoiding loop unwinding assertion failures.
[0031] For instance, in the previous example of the program received by the computing device 102, the program analysis module 114 may compare the number of paths, i.e., two and the number of output variables, i.e., one to determine the finite loop bound as one.
[0032] The loop parameters, the finite loop bound, the original loop statement, and the original loop body may then be used to replace the original loop with the abstracted loop. In one implementation, the abstraction module 116 is configured to replace the original loop with the
12
abstracted loop. For the purpose, the abstraction module 116 initially removes the original loop from the program. The abstraction module 116 subsequently adds an abstracted loop statement to the program to define and initiate the abstracted loop. In one implementation, the abstraction module 116 defines the abstracted loop statement with the termination condition based on the original loop condition and the loop bound. Thus, the abstracted loop is executed until either of the original loop condition and the loop bound becomes false, i.e., until either the number of iterations gone through by the abstracted loop exceeds the finite loop bound or the original loop condition becomes false. In one implementation, the abstraction module 116 defines a “for loop” as the abstracted loop and thus adds a “for loop statement” as the abstracted loop statement.
[0033] For instance, in the previous example of the program received by the computing device 102, the abstraction module 116 may remove the original loop and add the abstracted loop statement, with loop bound as one, to obtain the program as follows:
void xmi t (int nP, struct reqr) ........... (1)
{ ........... (2)
nPO = nP − 1; ........... (3)
for (i =0; i <1 && (nP!=nPO); i ++)........... (20)
{ ........... (5)
} ........... (16)
assert (state!=U); ........... (17)
state= U; ........... (18)
} ........... (19)
[0034] Further, the abstraction module 116 may assign non-deterministic values to each of the IO variables while defining the IO variables in the abstracted loop. In one implementation, the non-deterministic values may be assigned using a nondeterministic function, i.e., nondet (v) configured to non-deterministically assign values to all variables in set “v”. Nondeterministic functions, as will be understood, are functions that may return different results each time they are called. In one implementation, the IO variables may be assigned the values selected from a range based on predetermined parameters, such as a user input or a data type of the IO variable which has to be assigned the non-deterministic value. For example, for an unsigned character type variable v in C language, the non-deterministic values may be assigned from a range between 0
13
and 255. The abstraction module 116 may assign the non-deterministic values to the IO variables as the abstraction module 116 may not be able to determine what values may be assigned to these IO variables during the actual execution of the original loop. Thus, by providing the non-deterministic values to the IO variables the abstraction module 116 may ensure that apart from being assigned the values that would have been assigned during actual execution, the IO variables are also assigned some additional values which may never have been assigned in the original loop. The additional values thus help in providing abstraction property to the abstracted loop.
[0035] For instance, in the previous example of the program received by the computing device 102, the abstraction module 116 may assign the non-deterministic values to IO variables to obtain the program as follows:
void xmi t (int nP, struct reqr) ........... (1)
{ ........... (2)
nPO = nP − 1; ........... (3)
for (i =0; i <1 && (nP!=nPO); i ++) ........... (20)
{ ........... (5)
nondet(nPO); ........... (21)
nondet(nP); ........... (22)
nondet(r); ........... (23)
nondet(glb); ........... (24)
} ........... (16)
assert (state!=U); ........... (17)
state= U; ........... (18)
} ........... (19)
[0036] The abstraction module 116 may further insert the original loop body as a part of the abstracted loop. Inserting the original loop body as a part of the loop body in the abstracted loop helps in ensuring that the abstracted loop has the same properties as the original loop. For instance, in the previous example of the program received by the computing device 102, the abstraction module 116 may insert the original loop body to obtain the program as follows:
void xmi t (int nP, struct reqr) ........... (1)
{ ........... (2)
14
nPO = nP − 1; ........... (3)
for (i =0; i <1 && (nP!=nPO); i ++) ........... (20)
{ ........... (5)
nondet(nPO); ........... (21)
nondet(nP); ........... (22)
nondet(r); ........... (23)
nondet(glb); ........... (24)
state = L; ........... (6)
nPO = nP; ........... (7)
r = glb; ........... (8)
if (r && r−>status) ........... (9)
{ ........... (10)
glb = r−>Next; ........... (11)
state= U; ........... (12)
r−>status = 0; ........... (13)
nP ++; ........... (14)
} ........... (15)
} ........... (16)
assert (state!=U); ........... (17)
state= U; ........... (18)
} ........... (19)
[0037] Further, the abstraction module 116 may insert a first assume statement and a second assume statement in the program. In one implementation, the abstraction module 116 may insert the first assume statement after the IO variables to ensure that the abstracted loop is always executed with the original loop condition true. For example, inserting the first assume statement after the IO variables indicates that the values attained by nPO, nP, r, glb are such that they satisfy the original loop condition and the abstracted loop may thus be executed to give same result as the original loop. Further, the abstraction module 116 may insert the second assume statement after the abstracted loop ensuring that the original loop condition is false after the abstracted loop is executed. Adding the second assume statement ensures that for the rest of the program the original loop condition is always provided as false as it would have been in the
15
original loop where the loop would have terminated only on the original loop condition being false.
[0038] For instance, in the previous example of the program received by the computing device 102, the abstraction module 116 may insert the first assume statement and the second assume statement to obtain the program as follows:
void xmi t (int nP, struct reqr) ........... (1)
{ ........... (2)
nPO = nP − 1; ........... (3)
for (i =0; i <1 && (nP!=nPO); i ++) ........... (20)
{ ........... (5)
nondet(nPO); ........... (21)
nondet(nP); ........... (22)
nondet(r); ........... (23)
nondet(glb); ........... (24)
assume (nPO!= nP); ........... (25)
state = L; ........... (6)
nPO = nP; ........... (7)
r = glb; ........... (8)
if (r && r−>status) ........... (9)
{ ........... (10)
glb = r−>Next; ........... (11)
state= U; ........... (12)
r−>status = 0; ........... (13)
nP ++; ........... (14)
} ........... (15)
} ........... (16)
assume (nPO == nP); ........... (26)
/ / release the lock ........... (27)
assert (state!=U); ........... (17)
state= U; ........... (18)
} ........... (19)
16
[0039] The program with the abstracted loop thus obtained may be saved by the abstraction module 116 in the abstraction data 122. Further, the program with the abstracted loop may be provided to a model checker unit for being analyzed for errors. Providing the program with the abstracted loop to the model checker helps in facilitating a successful execution of the program as the loop was executed a finite number of times, terminating on reaching the finite loop bound provided in the abstracted loop.
[0040] Although the present subject matter has been defined with reference with to a “while loop” and a “for loop”, it will be understood that the computing device 102 implementing the loop abstraction may be used for loop abstraction in other types of loops as well, albeit with few modifications/alterations as will be understood by a person skilled in the art.
[0041] Although the present subject matter has been defined in reference with loops used in c language, it will be understood that the computing device 102 implementing the loop abstraction may be used for loop abstraction in programs written using other programming languages, albeit with few modifications.
[0042] Figure 2 illustrates a method for implementing loop abstraction in a program, according to an embodiment of the present subject matter. The order in which the method 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 200 or any alternative methods. Additionally, individual blocks may be deleted from the methods without departing from the spirit and scope of the subject matter described herein. Furthermore, the methods can be implemented in any suitable hardware, software, firmware, or combination thereof.
[0043] The method(s) 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 may also be practiced in a distributed computing environment where functions are performed by remote processing devices that are linked through a communications network. In a distributed computing environment, computer executable instructions may be located in both local and remote computer storage media, including memory storage devices.
17
[0044] A person skilled in the art will readily recognize that steps of the methods can be performed by programmed computers. Herein, some embodiments are also intended to cover program storage devices, for example, digital data storage media, which are machine or computer readable and encode machine-executable or computer-executable programs of instructions, where said instructions perform some or all of the steps of the described method. The program storage devices may be, for example, digital memories, magnetic storage media, such as a magnetic disks and magnetic tapes, hard drives, or optically readable digital data storage media. The embodiments are also intended to cover both communication network and communication devices configured to perform said steps of the exemplary methods.
[0045] At block 202, an original loop condition of an original loop is determined. In one implementation, a program having the original loop is received by a program analysis module, for example, the program analysis module 114 from a compilation module. The original loop, having an original loop statement and an original loop body, is subsequently analyzed to determine the original loop condition provided in the original loop statement. Further, the original loop condition, the original loop body, and the original loop statement may be saved in original loop data, such as the original loop data 120 of the computing device 102.
[0046] At block 204, one or more loop variables of the original loop are ascertained. In one implementation, the original loop body of the original loop is analyzed to ascertain one the loop variables of the original loop. For example, the program analysis module 114 of the computing device 102 statically analyzes the original loop body to determine the loop variables. Further, the loop variables are classified into input variables, output variables, and input-output (IO) variables. The input variables may be defined as the variables that are read only and are thus not modified during loop execution. The output variables on the other hand are the ones that are modified during the loop execution but read outside the loop. The IO variables may be defined as the variables that are both read and modified during the loop execution. Further, the loop variables may be saved in the original loop data, such as the original loop data 120 of the computing device 102.
[0047] At block 206, a number of paths of the original loop are ascertained. For example, the program analysis module 114 of the computing device 102 statically analyzes the original loop body to determine the number of paths possible in the original loop. Further, the number of
18
paths may be saved in the original loop data, such as the original loop data 120 of the computing device 102.
[0048] At block 208, a finite loop bound is determined for the abstracted loop. In one implementation, the finite loop bound is determined based on the number of paths and the number of output variables. For the purpose, the number of paths and the number of output variables are compared. Based on the comparison, a minimum from among the number of paths and the number of output variables is ascertained as the finite loop bound. For example, the program analysis module 114 of the computing device 102 compares the number of paths and the number of output variables to determine the finite loop bound. Further, the finite loop bound may be saved in the original loop data, such as the original loop data 120 of the computing device 102.
[0049] At block 210, the original loop is removed from the program. In one implementation, an abstraction module, for example, the abstraction module 116 may remove the original loop from the program.
[0050] At block 212, an abstracted loop statement defining the abstracted loop is inserted in the program. The abstracted loop statement includes, among other things, the finite loop bound and the original loop condition as loop conditions for the abstracted loop. For example, the abstraction module 116 may define the abstracted loop statement in the program with the loop conditions for the abstracted loop based on the finite loop bound and the original loop condition, such that the abstracted may terminate on either the original loop condition getting false or the number of iterations exceeding the finite loop bound.
[0051] At block 214, non-deterministic values are assigned to each of the IO variables. In one example, the abstraction module 116 defines the IO variables in the abstracted loop by assigning non-deterministic values to each of the IO variables. Providing the non-deterministic values facilitates in implementing the abstraction in the program as the non-deterministic values facilitates in assigning any value to the IO variables irrespective of whether those values could have been assigned to the IO variables during execution of the original loop.
[0052] At block 216, the original loop body is inserted in the abstracted loop. For example, the abstraction module 116 inserts the original loop body in the abstracted loop in order to ensure that the abstracted loop includes all properties of the original loop.
19
[0053] At block 218, a first assume statement and a second assume statement are inserted in the abstracted loop. In one implementation, the first assume statement is inserted after the IO variables and before the original loop body, while the second assume statement is inserted after the abstracted loop. Adding the first assume statement ensures that the nondeterministic values assigned to the IO variables are such that the abstracted loop is always executed with the original loop condition true. Adding the second assume statement on the other hand helps in ensuring that the original loop condition gets false after the abstracted loopis executed.
[0054] Although implementations for loop abstraction in a program have been described in language specific to structural features and/or methods, it is to be understood that the appended claims are not necessarily limited to the specific features or methods described. Rather, the specific features and methods are disclosed as exemplary implementations for loop abstraction.
20
I/We claim:
1. A computer implementable method for loop abstraction in a program, the method comprising:
determining one or more loop parameters of an original loop having an original loop statement and an original loop body, wherein the one or more loop parameters include at least one of an original loop condition, input variables, output variables, input-output (IO) variables, and number of paths in the original loop body;
ascertaining, based on the number of paths and the output variables, a loop bound for defining an abstracted loop;
removing the original loop from the program; and
inserting an abstracted loop statement and at least the original loop body for defining the abstracted loop in the program, wherein the abstracted loop statement includes a termination condition based on the loop bound and the original loop condition.
2. The method as claimed in claim 1, wherein the method further comprises:
assigning non-deterministic values to the IO variables; and
adding the IO variables between the abstracted loop statement and the original loop body in the program.
3. The method as claimed in claim 2, wherein the method further comprises:
inserting a first assume statement in the abstracted loop, wherein the first assume statement is inserted between the IO variables and the original loop body, and wherein the first assume statement holds the original loop condition as true; and
adding a second assume statement after the abstracted loop in the program, wherein the second assume statement holds the original loop condition as false.
4. The method as claimed in any of the preceding claims, wherein the method further comprises:
receiving a program having the original loop; and
analyzing the original loop statically to determine the original loop statement and the original loop body of the original loop.
5. The method as claimed in any of the preceding claims, wherein the ascertaining further comprises:
21
determining a minimum value from among the number of paths and number of the output variables; and
setting the minimum value as the loop bound.
6. A computing device (102) comprising:
a processor (104); and
a memory (108) coupled to the processor (104), the memory (108) comprising:
a program analysis module (114) configured to:
determine one or more loop parameters of an original loop having an original loop statement and an original loop body, wherein the one or more loop parameters include at least one of an original loop condition, input variables, output variables, input-output (IO) variables, and number of paths of the original loop body; and
an abstraction module (116) configured to:
ascertain, based on the number of paths and the output variables, a loop bound for defining an abstracted loop; and
replace the original loop in the program with an abstracted loop having an abstracted statement and at least the original loop body, wherein the abstracted loop statement includes a termination condition based on the loop bound and the original loop condition.
7. The computing device (102) as claimed in claim 6, wherein the abstraction module (116) is further configured to insert the abstracted loop statement and the original loop body for defining the abstracted loop in the program.
8. The computing device (102) as claimed in any of the preceding claims, wherein the abstraction module (116) is further configured to:
assign non-deterministic values to the IO variables; and
insert the IO variables between the abstracted loop statement and the original loop body in the program.
9. The computing device (102) as claimed in claim 8, wherein the abstraction module (116) is further configured to:
22
insert a first assume statement in the abstracted loop, wherein the first assume statement is inserted between the IO variables and the original loop body, and wherein the first assume statement holds the original loop condition as true; and
insert a second assume statement after the abstracted loop in the program, wherein the second assume statement holds the original loop condition as false.
10. The computing device (102) as claimed in any of the preceding claims, wherein the program analysis module (114) is further configured to:
compare the number of paths and number of the output variables; and
determine a minimum value from among the number of paths and the output variables based on the comparing; and
setting the minimum value as the loop bound.
11. A computer-readable medium having embodied thereon a computer program for executing a method of privacy protected clustering of interest profiles of end users, the method comprising:
determining one or more loop parameters of an original loop, wherein the one or more loop parameters include at least one of an original loop condition, input variables, output variables, input-output (IO) variables, and number of paths, and wherein the original loop includes an original loop statement and an original loop body;
ascertaining, based on the number of paths and the output variables, a loop bound for defining an abstracted loop;
removing the original loop from the program; and
inserting an abstracted loop statement and the original loop body for defining the abstracted loop in the program, wherein the abstracted loop statement includes a termination condition defined based on the loop bound and the original loop condition.