COAL: The Constant Propagation Language

Many program analyses require statically inferring the possible values of object variables. However, current approaches either do not account for correlations between object fields or do so in an ad hoc manner. The COAL project enables the specification and solution of these problems in a principled way. The project includes a language that is used to describe the classes of the objects whose value should be inferred. It also includes a solver, which computes the object values.

The COAL Language

The COAL language allows easy specification of composite constant propagation problems. For example, consider the following method:
public void sendMessage() {
  Message message = new Message();
  message.setTarget("target");
  message.addData("secret");
  MessagingClass.send(message);
}
We would like to automatically infer the possible values of the message variable at the call to send(). Consider that the Message class is defined as follows:
public class Message {
  private String target;
  private Set<String> data = new HashSet<>();

  public void setTarget(String target) {
    this.target = target;
  }

  public String getTarget() {
    return this.target;
  }

  public void addDataItem(String dataItem) {
    this.data.add(dataItem);
  }

  public Set<String> getData() {
    return this.data;
  }
}
Then the COAL specification for the problem is the following.
class Message {
  String target;
  Set<String> data;

  mod <Message: void setTarget(java.lang.String)> {
    0: replace target;
  }

  mod <Message: void addData(java.lang.String)> {
    0: add data;
  }

  query <MessagingClass: void send(Message)> {
    0: type Message;
  }
}
By using this specification, our COAL solver can automatically infer the possible values of the message variable at the call to send.

The COAL Solver

The COAL solver takes as inputs a COAL specification and the code that needs to be analyzed and automatically outputs the value of the fields of the message variable. Note that in programs where there are several possible values for a given object, the COAL solver infers all possible values, taking into account the correlations between the fields on different execution paths.

The COAL solver uses COAL specifications to automatically perform the data flow analysis without having the analyst write complex data flow functions. This makes it easy to write analyses without advanced knowledge of data flow analysis. Additional information can be found on the installation, language and tutorial pages.

This research was supported by the National Science Foundation Grants No. CNS-1064900, CNS-1228700, CNS-1228620 and CNS-1219495 and by a Google Faculty Award.