Analysis Internals

This page documents the basics of how CTADL’s analysis works internally but glosses over implementation details.

Global Variables

Introduction

The CTADL IR language supports global variables. They are used to model variables like public static variables in Java. Unlike tidy intraprocedural data flow, globals can flow data from one function to many others. A typical example is below, where a flows to b in main because of a global variable g.

var g;
main() {
    WriteGlobal(a);
    b = ReadGlobal();
}
WriteGlobal(p) {
    g = p;
}
ReadGlobal() {
    return g;
}

CTADL uses a threading strategy to model globals.

Compositional strategy: Threading globals as parameters

One way to handle global variables compositionally is by threading them through each function as a parameter. This way they are handled like local variables, they can occur in function summaries, be instantiated, etc. Below is the same program as above, but transformed by removing and threading the global variable:

// var g; is removed
main(globals) {
    F(a, globals);
    b = H(globals);
}
WriteGlobal(p, globals) {
    globals.g = p;
}
ReadGlobal(, globals) {
    return globals.g;
}

An in-out parameter globals is added to each function, each global access is translated into a corresponding access of the globals parameter, and each call site threads the parameter. For this instrumentation, one more thing needs to be done, which is not shown: the set of access paths is augmented with paths for each global. The path added for this example is .g.