March 2000 (Revised) | Moory Sagiv, Thomas Reps, Reinhard Wilhelm
This paper presents a parametric framework for shape analysis using 3-valued logic. The framework allows for the generation of different shape-analysis algorithms by varying the predicates used in the 3-valued logic. The key innovation is the use of 3-valued logical structures to represent possible stores during program execution. These structures provide truth values for every formula, enabling the evaluation of predicate-logic formulae using Kleene's semantics of 3-valued logic. This approach allows for the determination of "shape invariants" of programs that perform destructive updating on dynamically allocated storage.
The paper introduces a parametric framework for shape analysis, which provides a basis for generating different shape-analysis algorithms by varying the predicates used in the 3-valued logic. The analysis algorithms handle every program, but may produce conservative results due to the class of predicates employed. The framework includes a language for specifying abstraction properties and a method for generating shape-analysis algorithms from such specifications. The paper also discusses the use of logic for shape analysis, including the representation of store properties and the use of 3-valued logic to capture the semantics of program statements.
The paper presents a technique for shape analysis via 3-valued logic, which uses Kleene's 3-valued logic to create a shape-analysis algorithm automatically from a specification. The framework allows for the creation of algorithms that are more precise than previous shape-analysis algorithms by tracking which heap cells are reachable from which program variables. The paper also discusses the limitations of the framework, including the fact that it creates intraprocedural shape-analysis algorithms and that the number of possible shape-nodes may be potentially exponential in the size of the specification.
The paper also discusses the implementation of the algorithms in Java and the organization of the paper, which includes an overview of the parametric framework, the use of 3-valued logic, and the properties of 3-valued logic. The paper concludes with a discussion of the embedding theorem, which provides a tool for relating 2-valued and 3-valued interpretations. The paper also discusses the properties of 3-valued logic, including the double-negation, De Morgan laws, associativity, commutativity, and distributivity laws. The paper concludes with a discussion of the limitations of the framework and the potential for future research.This paper presents a parametric framework for shape analysis using 3-valued logic. The framework allows for the generation of different shape-analysis algorithms by varying the predicates used in the 3-valued logic. The key innovation is the use of 3-valued logical structures to represent possible stores during program execution. These structures provide truth values for every formula, enabling the evaluation of predicate-logic formulae using Kleene's semantics of 3-valued logic. This approach allows for the determination of "shape invariants" of programs that perform destructive updating on dynamically allocated storage.
The paper introduces a parametric framework for shape analysis, which provides a basis for generating different shape-analysis algorithms by varying the predicates used in the 3-valued logic. The analysis algorithms handle every program, but may produce conservative results due to the class of predicates employed. The framework includes a language for specifying abstraction properties and a method for generating shape-analysis algorithms from such specifications. The paper also discusses the use of logic for shape analysis, including the representation of store properties and the use of 3-valued logic to capture the semantics of program statements.
The paper presents a technique for shape analysis via 3-valued logic, which uses Kleene's 3-valued logic to create a shape-analysis algorithm automatically from a specification. The framework allows for the creation of algorithms that are more precise than previous shape-analysis algorithms by tracking which heap cells are reachable from which program variables. The paper also discusses the limitations of the framework, including the fact that it creates intraprocedural shape-analysis algorithms and that the number of possible shape-nodes may be potentially exponential in the size of the specification.
The paper also discusses the implementation of the algorithms in Java and the organization of the paper, which includes an overview of the parametric framework, the use of 3-valued logic, and the properties of 3-valued logic. The paper concludes with a discussion of the embedding theorem, which provides a tool for relating 2-valued and 3-valued interpretations. The paper also discusses the properties of 3-valued logic, including the double-negation, De Morgan laws, associativity, commutativity, and distributivity laws. The paper concludes with a discussion of the limitations of the framework and the potential for future research.