PICASSO Dynamic Package Interfaces
Downloading and using Picasso
The sources of Picasso can be obtained from the tool webpage. Currently only the version in the SVN repository contains the dynamic package interfaces features.
To compile and run Picasso from the sources you will need sbt. (tested with sbt 0.11.3) When sbt is installed simply execute sbt compile in Picasso's folder.
To run Picasso with the interface generate enabled use the runGraph.sh script with the -r and --interface options.
Assuming that this file is named input.dbp, it is possible to run the example with the command:
# runGraph.sh -r --interface input.dbp
Picasso produces a file called input-report.html that contains the interface.
Graph-rewriting system from code.
Picasso accepts graph-rewriting rules for concrete graphs (i.e., rules over graphs that have nodes with nesting levels 0). Therefore, we have to first transform the code into graph-rewriting rules. A graph rewriting rule is composed of two graphs and a mapping bewteen them. We call the two graphs the left- and right-hand side of the rule. Informally, the LHS of a rule is matched against a configuration and the matched part is then replaced by the RHS. The mapping is used to handle the frame, i.e. the nodes not matched by the LHS. Those nodes might still have edges from/to matched nodes and the mapping tells how to update those edges.
Both the objects and their corresponding abstraction predicates are represented as graph nodes. The nodes have labels that determine whether they represent an object or a predicate. The labels also carry information like the class for an object and the predicate name and valuation for a predicate. Furthermore, nodes can have annotations such as the role in a method call.
The edges between two object nodes represent reference between those two objects. The edges between an object node and a predicate node tells the valuation of the predicate for the corresponding object. If a predicate is defined over the attributes of two objects, then their corresponding nodes are connected to a mutual predicate node; e.g., the ``sync'' predicate for a set and an iterator is modelled as a node that is pointed by both the set and iterator objects.
For each method call, we manually encode its semantics as a graph rewriting rule that specifies how the objects in the scope of the method are changed. Due to the limited precision of the abstraction it is possible that some predicates take either the valuation true or false after the update. When this occurs for a concrete object we creates multiple graph-rewriting rule, one for each case. When this occurs for abstract objects we add a ``loop'' that non-deterministically update the value of the predicate for the objects one at the time. Such a case is when an iterator removes an item from a set, an indeterminate number of iterators pointing to the set become non-movers. The graph rewriting rules to model the semantics of a package can all be automatically computed, as outlined in the paper.
Set iterator example
The abstraction requires an additional binary predicate "iterator.iver ≤ set.sver". This predicate is needed to improve the precision of the post computation. However, it is always true, therefore, we omit it in the rule.