|
 |
[02 Nov][1] Advantages:1- They dont lose information at control flow merge points. They do it by propagating the condition with the datflow fact ("property"). By this they eliminate some ifeasible paths. 2- They keep it scalable by tracking only those paths that affect the "property" they want to track. Drawbacks: 1- Based on flow-insensitive pointer analysis. So cant tackle aliasing problems well. A example of this is given in [2]. About metal[5] this paper says, "The core engine of Metal is a local dataflow analysis similar to the standard dataflow analysis described in Section 3". [2] Advantages: 1- Being based on shape analysis, it can verify/check many complex heap properties. Aliasing is taken care of, of course. Disadvantages: 1- Single-level points, no procedures! 2- Does not scale up. "A shallow program denotes a procedure-free program where all variables are pointers to Objects of given type T, and whose statements are either allocation, copy assignments or invokation of an operation on an variable. Shallow programs allow multiple pointers to the same allocated object, but allocated objects may not themselves contain pointers(i.e. pointers in shallow programs are single-level[])". Nice discussion on the challenges of type-state verification/checking. (1) Aliasing (2) Infeasible Paths. Infeasible path problem is addressed by "predicate abstraction" in tools like SLAM and BLAST. [3] I am yet to read it well. Looks like some orthogonal techniques to ours. "Instead of associating a single state with each object, our system instead models each typestate as an abstract set of objects. If an object is in given typestate, it is a member of the set that corresponds to that typestate." About aliasing problem: "Sharing via aliased object references has caused problems for standard typestate systems – it has been difficult to ensure that if the program uses one reference to access the object and change its typestate, the declared type of other references is appropriately adjusted...Role system[4] is the only typestate system to support both sharing and nonmonotonic typestate changes." [4] have not read yet. But being a type system.... [5] metal work! [6] Interesting example inside. "monotonic" because typestate does not change after it attains a particular value. [1] ESP: Path-sensitive Program Verification in Polynomial Time [2] Typestate Verification: Abstraction Techniues and Complexity results [3] Generalized Typestate Checking Using Set Interfaces and Pluggable Analyses [4] Role Analysis [5] Checking System Rules using system-specific, programmer-written compiler extensions. [6] Heap Monotonic Type States Last modified 5 November 2004 at 12:25 pm by Saswat Anand |