Components | Soufflé • A Datalog Synthesis Tool for Static Analysis

Edit me

A component is a modular part of a program that may encapsulate component elements, including relation declarations, type declarations, rules, facts, directives, and other components. A component has component declarations and component instantiations.

A component declaration starts with the keyword .comp followed by the name of the component and a block between curly brackets (i.e. { ... }) containing the component elements.

For example,

.comp MyComponent {
    .type myType = number
    .decl TheAnswer(x:myType)    // component relation
    TheAnswer(42).               // component fact
}

declares a new component with the name MyComponent. The component elements are a type myType, a relation TheAnswer, and a fact.

We instantiate a component using the .init keyword followed by a unique name of the instance, the = symbol, and the name of the component declaration.

In this example,

.init myInstance1 = MyComponent

.decl Test(x:number)
Test(x) :- myInstance1.TheAnswer(x).
.output Test

we instantiate the component MyComponent with the name myInstance1. Internally, Soufflé flattens the component instantiation creating for each component instantiation its own namespace. The qualified names of component elements are prepended using the name of the instantiation.

For the above example, Soufflé internally expands the component instantiation as follows:

.type myInstance1.myType = number
.decl myInstance1.TheAnswer(x:myType)    // relation of myInstance1
myInstance1.TheAnswer(42).               // fact of myInstance1

.decl Test(x:number)
Test(x) :- myInstance1.TheAnswer(x).
.output Test

You can display the expansion using the specifying the command-line option --show=transformed-datalog.

In the following example, we have two component instantiation of MyComponent:

.init myInstance1 = MyComponent
.init myInstance2 = MyComponent
myInstance2.TheAnswer(33).

.decl Test(x:number)
Test(x) :- myInstance1.TheAnswer(x). 
Test(x) :- myInstance2.TheAnswer(x). 
.output Test

producing internally the following logic program,

.type myInstance1.myType = number
.decl myInstance1.TheAnswer(x:myType)    // relation of myInstance1
myInstance1.TheAnswer(42).               // fact of myInstance1
.type myInstance2.myType = number
.decl myInstance2.TheAnswer(x:myType)    // relation of myInstance1
myInstance2.TheAnswer(42).               // fact of myInstance1
myInstance2.TheAnswer(33).

.decl Test(x:number)
Test(x) :- myInstance1.TheAnswer(x).
Test(x) :- myInstance2.TheAnswer(x).
.output Test

Note that the two relations TheAnswer of both component instantiations are disambiguated by the prefix myInstance1 and myInstance2 to avoid a name clash.

Suppose rules/facts are defined in a component for which there are no relation declarations. In that case, no prefix is prepended, and the resolution is deferred to the actual component instantiation.

For example, in the following example we have facts and rules defined whose relations reside outside of the component in which they are defined.

.decl Out(x:number) 
.comp A { 
   .decl R(x:number) 
   .comp Count { 
       R(1).                  // fact accessing R outside of Count
       R(x+1):- R(x), x<10.   // rule accessing R outside of Count
   } 
   .init myCount = Count      // instantiate Count
   Out(x) :- R(x).            // rule accessing Out outside of A 
}
.init myA = A
.output Out

Soufflé expands the code above as follows:

.decl Out(x:number) 
.decl myA.R(x:number) 
myA.R(1).
myA.R((x+1)) :- myA.R(x), x < 10.
Out(x) :- 
   myA.R(x).
.output Out

Prefices are prepended to relations in rules and facts if they are instantiated in the local scope.

Type Parameterisation

Components can be parametrized by unqualified type names. In the example,

.comp ParamComponent<myType> {
    .decl TheAnswer(x:myType)    // component relation
    TheAnswer(42).               // component fact
    .output TheAnswer            // component output directive
}
.init numberInstance = ParamComponent<number>
.init floatInstance = ParamComponent<float>

two different instances are generated whose relation’s attribute are either of type number or float. Internally, Soufflé produces the program showing the different attribute types of the instantiated relations TheAnswer.

.decl numberInstance.TheAnswer(x:number)     // relation of numberInstance
numberInstance.TheAnswer(42).                // fact of numberInstance
.output numberInstance.TheAnswer             // output directive of numberInstance

.decl floatInstance.TheAnswer(x:float)       // relation of floatInstance
floatInstance.TheAnswer(42).                 // fact of floatInstance
.output floatInstance.TheAnswer              // output directive of floatInstance

Parameters can also be used to parameter a component name in a component instantiation. This mechanism is useful to model different behaviours in component since the component instantiation is controlled by the user of the component. For example,

.decl R(x:number)
.comp Case<Selector> {
   .comp One { 
     R(1). 
   } 
   .comp Two { 
     R(2).
   } 
   .init selection = Selector // instantiation depending on type parameter "Selector" 
} 
.init myCase = Case<One> 
.output R

produces internally the following program

.decl R(x:number) 
R(1). 
.output R

since One was passed on in the component instantiation of myCase.

By changing the instantiation from .init myCase = Case<One> to .init myCase = Case<Two>, the fact R(2). would be issued for relation R.

Inheritance

One component can inherit from multiple super components using inheritance. The component elements of the super-components are passed on to the sub-component. Using inheritance is helpful for larger programs and libraries and avoids code duplication.

In the following example,

.comp Base1 {
    .type myNumber = number
    .decl TheAnswer(x:myNumber)
    TheAnswer(42).
}
.comp Base2 { 
    TheAnswer(41). 
}
.comp Sub  : Base1, Base2 { // inherit from Base1 and Base2
    .decl WhatIsTheAnswer(n:myNumber)
    WhatIsTheAnswer(n) :- TheAnswer(n).
    .output WhatIsTheAnswer
}
.init mySub = Sub

the components Base1 and Base2 pass on all component elements to the component Sub. Soufflé produces internally the following code for the component instantiation mySub:

.type mySub.myNumber = number
.decl mySub.TheAnswer(x:mySub.myNumber) 
.decl mySub.WhatIsTheAnswer(n:mySub.myNumber) 
mySub.TheAnswer(42).
mySub.TheAnswer(41).
mySub.WhatIsTheAnswer(n) :- mySub.TheAnswer(n).
.output mySub.WhatIsTheAnswer

Overridable Relations

If a relation is declared as overridable in the super-component, a subcomponent may override its associated rules and facts from its super-component. The facts and rules of the super-component are discarded of an overridable relation with the directive override in the subcomponent.

For this example,

.comp Base {
    .decl R(x:number) overridable
    R(1).
    R(x+1) :- R(x), x < 5. 
    .output R
}
.comp Sub : Base {
    .override R
    R(2).
    R(x+1) :- R(x), x < 4. 
}
.init mySub = Sub

the sub-components discards fact R(1). and rule R(x+1) :- R(x), x < 5. since the relation R has been declared with the relation qualifier overrideable and the sub-component has the .override R directive, which let Soufflé drop the facts and rules of its super component. Soufflé will produce internally the following code for the sub-component instantiation mySub:

.decl mySub.R(x:number)overridable 
mySub.R(2).
mySub.R((x+1)) :- 
   mySub.R(x),
   x < 4.
.output mySub.R

In the following, we show a use case for override in a more practical setup. For example, a more precise version of an existing analysis can be implemented by using the override semantics as follows,

.comp AbstractPointsto{
    .decl HeapAllocationMerge(heap,mergeHeap) overridable
    HeapAllocationMerge(heap,"<<string-constant>>") :-
        StringConstant(heap).
    // ...
}

.comp PrecisePointsto : AbstractPointsto{
    .override HeapAllocationMerge
    HeapAllocationMerge(heap,"<<string-constant>>") :-
        StringConstant(heap),
        !ClassNameStringConstant(heap),
        !SimpleNameStringConstant(heap).
}

.init precise_pointsto = PrecisePointsto

In this example, PrecisePointsto inherits all the relations from AbstractPointsto, but only implements the HeapAllocationMerge relation differently. This feature avoids code duplications when we need several implementations of a generic analysis with minor variations and want to overwrite behaviour of the super component.

Type Parameterisation and Inheritance

Type parameters of super-components can be explicitly specified in sub-component declarations. For example,

.comp A<T> { .... }
.comp B<K> : A<K> { ... }

defines a sub-component B with parameter K that is used to instantiate the super component with parameter K for inheriting for B.

The type parameter can also be used as the base class

.comp A<T> : T { ... }

building a selective inheritance based on the type parameter T. The instantiation of A<T> defines which super component A is inheriting.

With inheritance, complex component instantiatons are implementable. In the example below

.init reach = Reachability<Graph<number>>   // syntax error

we would like to us a complex component parameter Graph<number>, but leads to syntax parameter because the parameter is not a simple identifier. By introducing a new component, the above instantiation can be rewritten as followes

.comp NumberGraph : Graph<number> { } // NumberGraph inherits  
.init reach = Reachability<NumberGraph>

Syntax

In the following, we define the component model more formally using syntax diagrams and EBNF. The syntax diagrams were produced with Bottlecaps.

Component Declaration

A component declaration may consist of type declarations, relation declarations, rules, facts, directives, override directives, component declarations and initialisations.

Component Declaration

component_decl ::= 
  '.comp' component_type ( ( ':' | ',' ) component_type )* 
    '{' 
        ( type_decl | relation_decl | rule | fact | directive | '.override' IDENT | component_init | component_decl )* 
    '}'

Component Initialisation

A component initialisation has a name and the component declaration name with its parameters.

Component Initialisation

component_init ::= '.init' IDENT '=' component_type

Component Type

A component type is a signature of a component either used for initialisation, super-component references, or declaration of a component.

Component Type

component_type ::= IDENT ( '<' IDENT ( ',' IDENT )* '>' )?