The COAL Language

This is the documentation for the COAL language. Many of the examples are adapted from IC3, a tool for Android Inter-Component Communication Analysis based on COAL. The complete COAL specification used in IC3 can be found at the corresponding source page. A BNF grammar for the language is also available.

Structure of a COAL Model

The general structure of the COAL model of a class is as follows:

class android.content.Intent {
  <field declarations>

  <modifier method declarations>

  <query declarations>

  <source declarations>

  <constant declarations>
}
The delared class name should be fully qualified (i.e., android.content.Intent instead of Intent). The field declarations specify field names and fields types for the modeled class. The modifier declarations describe the methods that modify the fields. The queries specify at which program locations the solver should compute object values. Finally, sources model field getters and constants model the case where there are modeled object constants.

Field Declarations

Field declarations specify the name and type of fields that should be modeled. The field name need not necessarily be the same as the one in the original class, as long as the naming scheme is consistent with the modifier declarations. For example, the following declares three fields.

String action;
Set<int> flags;
Set<String> categories;
Currently supported types are:
  • int: integer or long integer.
  • String: string of characters.
  • Class: class type.
  • Set<int>: Set of integers or long integers.
  • Set<String>: Set of strings of characters.
  • Set<Class>: Set of class types.

Modifier Declarations

A modifier declaration has the following general form:

mod <method signature> {
  <modifier argument 1>
  <modifier argument 2>
}

Modifier Arguments

A modifier argument is composed of the following.
  • A method argument index, which indicates the argument that is used to modify a field of the class.
  • An operation that is performed on the field.
  • A field name.
For example, consider the following modifier.
mod <android.content.Intent: android.content.Intent addFlags(int)> {
  0: add flags;
}
The 0 index means that the first argument to the method (at index 0) is used to modify field flags by adding to it. Currently available operations for simple scalar types are:
  • null: Make the field null (no argument required).
  • replace: Replace the field with an argument.
Operations available for sets are:
  • add: Add to a set.
  • remove: Remove from a set.
  • clear: Clear a set (no argument required).
  • addAll: Add several elements to a set.
  • replaceAll: Replace all elements of a set.
By default the type of the argument is assumed to be the declared type of the field. However, it is possible to override the type of the argument with a type annotation. For example the argument above could also be declared as:
0: add flags, type int;

Arguments can be declared separately, outside of method modifiers, which is useful when a given argument is reused in different modifiers. The following shows an example of this.

argument replacePackage0 = 0: replace package;
argument replaceClass1 = 1: replace clazz;

mod <android.content.Intent: void setClassName(java.lang.String,java.lang.String)> {
  argument replacePackage;
  argument replaceClass1;
}

An argument might be a class that is modeled using COAL. Consider the following:

mod <android.content.Intent: void setComponent(android.content.ComponentName)> {
  0: replace package, type android.content.ComponentName:package;
  0: replace clazz, type android.content.ComponentName:clazz;
}
Each argument specifies a type annotation. For example, the first argument indicates that the package field of the ComponentName class is used to replace the package field of the Intent class.

It is possible to specify a literal value for cases where a field is modified using a constant. In this case, no argument number is necessary. For example, the following code always replaces the action field with string value android.intent.action.MAIN.

replace action "android.content.action.MAIN";
If several constants are possible, this can also be encoded as follows:
add flags (0, 1, 2);

Modifier Types

Most modifiers only use the mod keyword. It is possible to model other types of modifiers. First, copy constructors are modeled using the copy keyword.

copy <android.content.Intent: void <init>(android.content.Intent)> {
  0;
}
This declaration specifies that the value of the first argument flows to the value of the modeled object.

Some methods create modeled objects. It is possible to let the solver traverse these methods and figure out the resulting value. It is also possible to model these methods by using the gen keyword.

mod gen <android.content.Intent: android.content.Intent generate(ComponentName)> {
  0: replace package, type ComponentName:package;
  0: replace clazz, type ComponentName:clazz;
  replace action "android.intent.action.MAIN";
  replaceAll categories "android.intent.category.LAUNCHER";
}

Query Declarations

Queries have the following general form:

query <method signature> {
  <query argument 1>
  <query argument 2>
}
The argument declarations indicate the index and types of the method arguments that should be inferred.
super context = android.content.Context;

query context : void sendBroadcast(android.content.Intent,java.lang.String) {
  0: type android.content.Intent;
  1: type String;
}
Note that it is possible to infer primitive value types such as String or int, in addition to COAL-modeled arguments. Notice also the method signature indicates that the declaration applies to all subclasses of android.content.Context.

Source Declarations

Source declarations are meant to model field getters. They are useful when the field value of a COAL-modeled object flows to a field value of another object modeled with COAL. The general form of a source declaration is the following:

source <method signature> {
  <field name>
}
For example, the following is a valid source declaration:
source <android.content.Intent: java.lang.String getAction()> {
  action;
}

Constant Declarations

Programs occasionally declare modeled objects that are constants (static final fields in Java). The solver can infer these constants by propagating through static class initializers, but this usually comes at a cost, since the constants are then propagated throughout the entire program. Thus it is recommended to declare the constants as part of the COAL specification.

There are two ways to declare constants. The first one can only be used if only a single field value is defined for the constant. For example, in the following, only the uri field is defined for the BOOKMARKS_URI constant.

staticfield uri <android.provider.Browser: android.net.Uri BOOKMARKS_URI> = 
    "content://browser/bookmarks";

If more than one field is defined for the constant, then it is possible to use the following declaration.

staticfield <android.provider.Browser: android.net.Uri BOOKMARKS_URI> {
  replace scheme "content";
  replace schemeSpecificPart "browser/bookmarks";
}

Help with the COAL Language

For any questions or issues with the COAL language, please file an issue at the issue tracker for the COAL solver.