Symbolic execution of object oriented programs with axiomatic summaries

A system for testing programs comprising:

• a digital processor;
• and
• digital memory tangibly embodying computer executable program instructions comprising:
• a parameterized unit test of an implementation under test,
• instructions for creating at least one axiom summarizing behavior of at least one method of the parameterized unit test, wherein creating a given axiom comprises (a)-(c) for a given method:
• (a) exploring the given method with a modified one-step relation starting with a variable intensional heap, wherein the variable intensional heap is described by a history of method invocations;
• and
• (b) for the modified one-step relation, treating calls to Assert.IsTrue(c) as calls to a test statement that specifies the assertion is assumed true;
• and
• (c) whenever a call to Assert.IsTrue(c) is encountered, generating and conjoining a new axiom formula for further explorations;
• a symbolic executor symbolically executing the parameterized unit test of the implementation under test to identify one or more execution paths associated with a series of constraints generated during symbolic execution, and
• a constraint solver that generates a set of a minimal number of test cases that cover the identified one or more execution paths associated with the series of constraints generated during the symbolic execution by solving for values that satisfy a the series of constraints generated during the symbolic execution of the parameterized unit test;
• wherein the symbolic execution includes using at least an extensional heap represented by nested applications of an update function, and wherein the symbolic execution further includes symbolic notations comprising an application of the update function notating symbolic objects and symbolic values assigned to fields of symbolic objects, wherein the application of the update function has input parameters comprising a first parameter indicating a previous state of the extensional heap before a present update, a second parameter indicating a symbolic instantiation of a class, a third parameter indicating an identifier of a field in the symbolic instantiation of the class, and a fourth parameter indicating a symbolic value assigned to the field in the symbolic instantiation of the class, wherein the application of the update function operates on a mapping from the fields to the assigned symbolic values;
• during symbolic execution of the parameterized unit test of the implementation under test, the at least one method of the parameterized unit test is emulated by reusing the at least one axiom summarizing behavior of the at least one method of the parameterized unit test based on a textual decoration to reuse the at least one axiom summarizing behavior, wherein the at least one axiom summarizing behavior is generated from a previous symbolic execution of a parameterized unit test;
• and
• from the mapping and the fourth parameter indicating a symbolic value assigned to the field in the symbolic instantiation of the class, creating a test case, of the set of the minimal number of test cases, comprising a concrete assignment to an input parameter of the parameterized unit test;
• and
• wherein the variable intensional heap that is described by a history of method invocations is partitioned from the extensional heap of the parameterized unit test for the at least one method that is represented by nested applications of the update function.

A computer readable medium tangibly embodying computer executable instructions comprising:

• instructions for receiving a parameterized unit test of an implementation under test;
• instructions for creating at least one axiom summarizing behavior of at least one method of the parameterized unit test, wherein creating a given axiom comprises (a)-(c) for a given method:
• (a) exploring the given method with a modified one-step relation starting with a variable intensional heap, wherein the variable intensional heap is described by a history of method invocations;
• and
• (b) for the modified one-step relation, treating calls to Assert.IsTrue(c) as calls to a test statement that specifies the assertion is assumed true;
• and
• (c) whenever a call to Assert.IsTrue(c) is encountered, generating and conjoining a new axiom formula for further explorations;
• instructions for symbolically executing the parameterized unit test, wherein the instructions for symbolically executing the parameterized unit test comprise instructions for, during symbolic execution, emulating the at least one method of the parameterized unit test by reusing the at least one axiom summarizing behavior of the at least one method of the parameterized unit test based on a textual decoration to reuse the at least one axiom summarizing behavior, wherein the at least one axiom summarizing behavior is generated from a previous symbolic execution of a parameterized unit test;
• instructions for notating updates on symbolic objects accessed while symbolically executing the parameterized unit test using at least an extensional heap represented by nested applications of an update function, the notating comprising an application of the update function notating symbolic objects and symbolic values assigned to fields of symbolic objects, wherein the application of the update function comprises input parameters comprising a first parameter indicating a previous state of the extensional heap before a present update, a second parameter indicating a symbolic instantiation of a class, a third parameter indicating an identifier of a field in the symbolic instantiation of the class, and a fourth parameter indicating a symbolic value assigned to the field in the symbolic instantiation of the class, wherein the update function operates on a mapping from the fields to the assigned symbolic values;
• instructions for identifying one or more execution paths with sets of constraints that are generated during symbolic execution of the parameterized unit test;
• and
• instructions for creating a test case comprising a concrete assignment to an input parameter of the parameterized unit test from the mapping and the fourth parameter indicating a symbolic value assigned to the field in the symbolic instantiation of the class;
• and
• instructions for automatically generating a set of a minimal number of test cases, that includes the created test case, that cover the one or more identified execution paths with the sets of constraints, that are generated during the symbolic execution, at least by identifying values that solve the sets of constraints, that are generated during the symbolic execution, of the identified one or more execution paths of the symbolically executed parameterized unit test;
• and
• wherein the variable intensional heap that is described by a history of method invocations is partitioned from the extensional heap of the parameterized unit test for the at least one method, that is represented by nested applications of the update function.

One or more computer readable media tangibly embodying computer executable instructions for performing a method comprising:

• receiving, in a computer, a parameterized unit test of an implementation under test;
• creating at least one axiom summarizing behavior of at least one method of the parameterized unit test, wherein creating a given axiom comprises (a)-(c) for a given method:
• (a) exploring the given method with a modified one-step relation starting with a variable intensional heap h, wherein the variable intensional heap h is described by a history of method invocations;
• (b) for the modified one-step relation, treating calls to Assert.IsTrue(c) as calls to Assume.IsTrue(c);
• and
• (c) whenever a call to Assert.IsTrue(c) is encountered, generating and conjoining a new axiom formula for further explorations;
• symbolically executing the parameterized unit test of the implementation under test to identify a plurality of terminated execution paths with associated sets of constraints that are generated during the symbolic execution, wherein a terminated execution path ends in a state with an empty stack of activation records;
• wherein during symbolic execution, symbolically recording evolving symbolic objects and encapsulated fields with symbolic updates, wherein symbolically recording comprises recording with an update function having input parameters comprising a first parameter indicating a previous state of a heap before a present update, a second parameter indicating a symbolic instantiation of a class, a third parameter indicating an identifier of a field in the symbolic instantiation of the class, and a fourth parameter indicating a symbolic value assigned to the field in the symbolic instantiation of the class, wherein the update function operates on a mapping from the encapsulated fields to assigned symbolic values;
• explicitly updating object fields or array elements with an extensional heap, wherein the extensional heap is represented by nested applications of the update function;
• emulating the at least one method of the parameterized unit test by reusing the at least one axiom summarizing behavior of the at least one method of the parameterized unit test based on a textual decoration to reuse the at least one axiom summarizing behavior, wherein the at least one axiom summarizing behavior is generated from a previous symbolic execution of a parameterized unit test;
• from the mapping and the fourth parameter indicating a symbolic value assigned to the field in the symbolic instantiation of the class, creating a first test case comprising a concrete assignment to an input parameter of the parameterized unit test;
• and
• automatically generating a set of a minimal number of test cases, that includes the created first test case, that cover the identified plurality of terminated execution paths with associated sets of constraints at least by identifying values that solve the associated sets of constraints, that are generated during the symbolic execution, of the identified plurality of terminated execution paths of the symbolically executed parameterized unit test, and at least by choosing one respective assignment per the identified plurality of terminated execution paths;
• wherein the first test case comprises a first respective assignment of the chosen one respective assignment per the identified plurality of terminated execution paths, the first respective assignment comprising the concrete assignment to the input parameter of the parameterized unit test;
• wherein the variable intensional heap h summarizes calls to a method of an object without indicating whether or what fields the method affects within the object;
• and
• the intensional heap described by a history of method invocation is partitioned from the extensional heap of the parameterized unit test for the at least one method represented by nested applications of the update function.