Donut domains—efficient non-convex domains for abstract interpretation

• US 8,719,790 B2
• Filed: 03/23/2012
• Issued: 05/06/2014
• Est. Priority Date: 03/23/2011
• Status: Expired due to Fees

• Current Assignee: NEC Corporation
• Original Assignee: NEC Laboratories America Inc (NEC Corporation)
• Inventors: Ivancic, Franjo, Balakrishnan, Gogul, Maeda, Naoto, Ghorbal, Khalil
• Primary Examiner(s): Wong, Don
• Assistant Examiner(s): KABIR, MOHAMMAD H
• Application Number:
  US13/428,608
• Publication Number:
  US 20120246626A1
• Time in Patent Office: 774 Days
• Field of Search: None
• US Class Current: 717/124
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013

Abstract

A computer implemented program analysis method employing a set of new abstract domains applicable to non-convex invarients. The method analyzes programs statically using abstract interpretation while advantageously considering non-convex structures and in particular those situations in which an internal region of an unreachable state exists within a larger region of reachable states. The method employs a new set of non-convex domains (donut domains) based upon the notion of an outer convex region of reachable states (Domain D1) and an inner region of unreachable states (Domain D2) which advantageously permits capture of non-convex properties by using convex regions and operations.

Claims

1. A computer implemented method for computer program analysis comprising the steps of:

generating an outer convex region of all reachable states for the computer program wherein the outer region (D1) represents an over-approximation of all of the reachable states;

generating an inner convex region of all unreachable states for the computer program wherein the inner region (D2) represents an under-approximation of all of the unreachable states; and

generating a set of possible program errors using abstract interpretation over the difference between the two regions.

2. The computer implemented method of claim 1 wherein the under-approximated inner region is instantiated as a powerset domain of an elementary domain.

3. The computer implemented method of claim 1 further comprising the steps of:

constructing a control flow graph of the computer program;

propagating region D1 along the control flow graph;

propagating region D2 along the control flow graph;

determining the differences between the two propagations; and

generating a set of reachable states from the difference so determined.

4. The method of claim 3 wherein said regions are ones selected from the group consisting of:

intervals, octagons, and polyhedron.

5. The method of claim 4 wherein domains are combined for abstract interpretation and said combination is performed according to an operation selected from the group consisting of:

join, meet, widening, update functions, and interpretation of tests.

6. The method of claim 1 further comprising the steps of:

determining a maximal inner polyhedron τ

={x ε

R^P|Tx≦

c of a given

template matrix T that lies within a given non-empty polyhedron P=[x ε

R^P|Ax≦

b], by;

computing an auxiliary matrix Λ

with non-negative elements Λ

T=A,

computing c such that Λ

c≦

b and Tx≦

c is consistent,

and outputting such inner polyhedron τ

.

7. The method of claim 1 further comprising the step of using an LP-solver to find matrixΛ

.

8. The method of claim 7 further comprising the step of determining the saturation of Λ

c≦

b, namely Λ

c=b.

9. The method of claim 8 wherein the output polyhedron is used for computer program analysis.

10. A computer implemented method for determining a maximal inner polyhedron τ

={x ε

R^P |Tx ≦

c of a given

template matrix T that lies within a given non-empty polyhedron P=[x ε

R^P|Ax≦

b], comprising the steps of;

computing an auxiliary matrix Λ

with non-negative elements Λ

T=A,

computing c such that Λ

c≦

b and Tx≦

c is consistent,

and outputting such inner polyhedron τ

.

11. The method of claim 10 further comprising the step of using an LP-solver to find Matrix Λ

.

12. The method of claim 10 further comprising the step of determining the saturation of Λ

c ≦

b, namely Λ

c=b.

13. The method of claim 10 wherein the output polyhedron is used for computer program analysis.

14. The method of claim 10 wherein the output polyhedron is used for test vector generation.

15. The method of claim 10 wherein the output polyhedron is used for computer graphics applications.