ACTIVE PROPERTY CHECKING

• US 20090265692A1
• Filed: 04/21/2008
• Published: 10/22/2009
• Est. Priority Date: 04/21/2008
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Levin, Michael Y., Molnar, David, Godefroid, Patrice
• Granted Patent: US 8,549,486 B2
• Time in Patent Office: Days
• US Class Current: 717/128
• CPC Class Codes: G06F 11/3688 for test execution, e.g. scheduling of test suites
• CPC Class Codes: G06F 9/44589 Program code verification, e.g. Java bytecode verification, proof-carrying code high-level semantic checks G06F8/43; testing and debugging software G06F11/36

Abstract

An exemplary method includes providing software for testing; during execution of the software, performing a symbolic execution of the software to produce path constraints; injecting issue constraints into the software where each issue constraint comprises a coded formula; solving the constraints using a constraint solver; based at least in part on the solving, generating input for testing the software; and testing the software using the generated input to check for violations of the injected issue constraints. Such a method can actively check properties of the software. Checking can be performed on a path for a given input using a constraint solver where, if the check fails for the given input, the constraint solver can also generate an alternative input for further testing of the software. Various exemplary methods, devices, systems, etc., are disclosed.

Claims

1. A method, implemented by a computing device, comprising:

providing software for testing;

during execution of the software, performing a symbolic execution of the software to produce path constraints;

injecting issue constraints into the software wherein each issue constraint comprises a coded formula;

solving the constraints using a constraint solver;

based at least in part on the solving, generating input for testing the software; and

testing the software using the generated input to check for violations of the injected issue constraints.

2. The method of claim 1 wherein the issue constraints comprise property constraints.

3. The method of claim 1 wherein the path constraints comprise a sequence of constraints on input to the software.

4. The method of claim 1 wherein a violation comprises a property violation.

5. The method of claim 1 wherein one or more active checkers perform the injecting.

6. The method of claim 5 comprising an active checker for division by zero.

7. The method of claim 5 comprising an active checker for array bounds.

8. The method of claim 5 comprising an active checker for Null pointer de-reference.

9. The method of claim 5 wherein an active checker for a property comprises a function that takes as input a finite program execution and returns a formula that is satisfiable if and only if there exists some finite program execution that violates the property.

10. The method of claim 9 wherein the finite program execution and some existing finite program execution adhere to a common, specified path constraint.

11. The method of claim 1 wherein the solving identifies at least one concrete input that causes a runtime check of the software to fail.

12. The method of claim 1 wherein the generating comprises dynamic test generating that attempts to exercise all feasible paths in at least a portion of the code.

13. The method of claim 1 further comprising optimizing injection of constraints to minimize calls to a constraint solver.

14. The method of claim 1 further comprising implementing one or more caching schemes to reduce calls to a constraint solver.

15. A method, implemented by a computing device, comprising:

providing software;

adding a cast to a type in the software wherein the cast pertains to an issue;

executing the software with the added cast for a concrete input; and

actively checking for an input that causes the issue.

16. The method of claim 15 wherein the added cast gives rise to a checker for a property.

17. The method of claim 15 wherein the cast comprises a cast to the type <

nonzero> and

wherein the issue comprises division by zero.

18. The method of claim 15 wherein the issue comprises an issue selected from a group consisting of division by zero, underflow and overflow.

19. A system for testing software, the system comprising:

one or more processors;

memory; and

processor executable instructions to injecting constraints into software during symbolic execution of the software wherein each constraints comprises a coded formula, to solve the constraints via using a constraint solver, to generate input for testing the software based on a solution provided by the constraint solver, and to test the software using the generated input to check for violations of the injected constraints.

20. The system of claim 20 wherein the constraints are associated with one or more issues.