Soufflé

News

Download

Docs

Community

View on GitHub

The following example encodes the most simple version of a var-points-to analysis.

The example starts by declaring types for variables, objects and fields. Based on those, four input relations assign , new , ld and st are declared and filled with data corresponding to the small code snippet outlined in the comment above.

The analysis itself is broken up in two parts:

computation of aliases

computation of the var-points-to relation based on aliases

Note that in particular for the last rule of the alias relation the utilisation of typed attributes ensures that connections between attributes are consistently established. Problems caused by e.g. getting the wrong order of parameters can be effectively prevented.

The following example utilises a composed type to model a type hierarchy for instructions.

In this example an instruction is either a read operation, a write operation or a jump instruction. However, to model the control flow through instructions, the flow relation needs to be able to cover any of those.

To model this situation, the union type Instr is introduced and utilised as shown above.

The following example demonstrates one way of integrating context information into a control flow graph.

In this example the flow relation describes a graph where each node consists of a pair of an instruction and some (abstract) context. Although correct, the increased number of attributes causes larger code bases, and thus an increased risk of typos leading to hard-to-identify bugs.

The fact that each node is represented by a pair of elements can be made explicit by utilising records, as demonstrated next.

The following example is a refactored version of the context sensitive flow graph example above.

The type ProgPoint (Program Point) aggregates an instruction and an (abstract) context into a new entity which is utilised as the node type of the flow graph. Note that in this version flow is a simpler, binary relation and typos mixing up instructions and contexts of different program points are effectively prevented.

Also, as we will see below, the flow relation could now be modelled utilising a generalised graph component, thereby inheriting a library of derived relations.

The following example demonstrates the utilisation of recursive records for building sequences of strings over a given alphabet:

The Seq type is a recursive type where each instance is either nil or a pair of a Letter (head) and a tailing Seq r.

The relation seq is defined to contain all sequences of length 5 or less over a given alphabet defined by the relation letter . The relation len is essentially a function assigning each sequence its length.

Finally, the res relation illustrates how to create constant values for recursive record types.

Components provide the means within Souffle’s Datalog to build modular queries, thus fostering the reuse of code.

The given example defines a component DiGraph comprising of four relations: node , edge , reach and clique . Furthermore, defining rules for those relations determining their mutual relation are established utilising ordinary Datalog rules.

To model an undirected graph, the definition of the DiGraph is extended by an additional rule making all edges reflexive. This is expressed by the derived component Graph , which inherits all the declarations and definitions of the DiGraph component and extends it by one additional rule.

Component hierarchies may be arbitrarily deep. A component may also have multiple base types, as long as their declared relations do not cause conflicts (e.g. two relations exhibiting the same name but different attributes).

The .init directive instantiates components by creating a copy of all its contained definitions, including a leading prefix. For instance, in the given example, the component Graph is instantiated for the name Net . Thus, the relations Net.node , Net.edge , Net.reach and Net.clique will be declared and defined accordingly. Those relations may then be accessed by other rules.

Note that components may also be nested. Thus, components may initialise other components within their body.

Frequently, components can be described in an abstract, generic way such that it can be utilised in a wider range of use cases. The following example extends the example above by adding a type parameter describing the node type for a graph:

The type parameter <N> introduces an additional element that can be fixed during the instantiation of a component. This type may be an arbitrary structure, including unions, records and recursive records. As a result, a graph of numbers, a graph of symbols (or a graph of program points as mentioned in the control flow example above) can share the same implementation of the actual graph.

In the following example, component Reachability is parameterised with the name of another component T . When instantiating Reachability one must provide actual component that will be used as T . Component Reachability can use any relations from the instantiated (but as yet unknown) component T .

Welcome

Build Soufflé

A Simple Example

Run Soufflé

Examples

Source Code

Datalog

Types

Strings

Arithmetic

Components

Records

Aggregates

Synthesis

Tuning

Profiler

Magic-Set

Inlining

C++ Interface

Other Systems

Contributors

Publications & Talks