Type definitions in components

[souffle-lang]

Type definitions in components

[b-scholz]

I made preliminary changes for implementing types in components. My principle assumption was that types are global entities and have not a component scoping. This assumption differs to relations in components which can be distinguished by there instantiation path. My changes can be found in

https://github.com/b-scholz/souffle.git

in branch "component-type". I am still unhappy about the solution.

With this extension, we can have conditional types, e.g.,

.comp X<C> {
  .comp isNumber {
     .type T = number
     A(1).
  } 
  .comp isSymbol { 
     .type T
     A("a").
  } 
  .decl A(x:T) printsize
  .init select = C
}
.init myComp=X<isNumber>

Type T is either a number or a symbol depending on the value of parameter C (i.e. either isNumber or isSymbol). The type T becomes globally visible by the component instantiation "select" inside the component X and subsequently by instantiation myComp.

With this approach we could finally solve Behnaz' request to have different context types for points-to. For example, Behnaz could specify,

.comp PointsTo<flavour> {
  .comp TwoObjOneHeap {
     .type Context = [o1:Object, o2:Object] 
     // more code here 
  } 
  .comp Insensitive { 
     .type Context = number
     // more code here
  } 
  .init select = flavour
}
.init myPts=PointsTo<TwoObjOneHeap>

However, there is a problem with the current approach. For example, it is not possible to have two instances of the different flavours of points to. Example,

 .init myPts1 = PointsTo<TwoObjOneHeap>
 .init myPts2 = PointsTo<Insensitive> 

would lead to a type clash of two globally defined type definitions for T, i.e.,

     .type Context = number
     .type Context = [o1:Object, o2:Object] 

due to our initial assumption that type declarations are globally visible and not just in the local scope.
I believe more work is required to overcome this issue.

I believe there are now two ways to overcome this issue:

Parameters become type names

.comp PointsTo<flavour> {
  .comp TwoObjOneHeap<Context> {
     .type  Context = [o1:Object, o2:Object] 
     // more code here 
  } 
  .comp Insensitive<Context> { 
     .type Context = number
     // more code here
  } 
  .init select = flavour<flavour>
}
.init myPts=points_to<TwoObjOneHeap> 
.init myPts=points_to<Insensitive> 

As a result, we will have two types with the names of the parameter values, respectively, i.e.,

     .type TwoObjOneHeap = number
     .type Insensitive = [o1:Object, o2:Object] 

The problem with this solution is that we cannot have more than one parameterised type. The current instantiation mechanism would not permit it. I believe this solution is sub-optimal.

Local component scoping for types

We use a similar mechanism as for relations to add a prefix to the types and have local scoping.
More thought on this is required.

[HerbertJordan]

This has become a thread about two issues:

Issue 1 - nested types
For nested type definitions, using component instance names as scopes similar to the relation names should work. Did you encounter any problem with this?

Issue 2 - type specific specialization
I somehow have problems to understand the issue. Why can't you use the context type itself as a parameter for the points-to similar to this:

.comp PointsTo<Context> {
    .rel pointsTo( c : Context, v : Variable, o : Object )
   // more declarations and rules ...
}

and instantiate it with

.init insensitive_points_to = PointsTo<[]>
.init sensitive_points_to = PointsTo< [ o1:CallSite, o2:CallSite ] >

If the answer is that the implementations of the points-to must be different, depending on the type, it is probably not a good idea to try to wrap it up in the same component. Maybe, by refactoring you can isolate the common parts into an extra component and then use inheritance to create the specialized versions.

But if you think you need to have parameter type specific component implementations, taking inspiration from C++ partial template specialization may be useful here. For instance, one may define a general form of a component like this:

.comp Component<T,U> {
   /* general case */
}

and if a special handling for some type is desired, one may write

.comp Component<T <: number, U > {
    // specialized version for cases where T is a number
}

and when instantiating the component with some types, the tightest fitting overload is selected.

What do you think about that?

[behnazh]

Issue 2 - type specific specialization

For the PointsTo example, as you said, different implementations share common parts which have to be isolated in a generic CommonPointsTo component. This common part can be inherited by different implementations and this is what we might really look for:

.comp PointsTo<flavour> {

  .comp CommonPointsTo<Context>{
      // more code here 
  }
  .comp TwoObjOneHeap: CommonPointsTo<Context> {
     .type  Context = [o1:Object, o2:Object] 
     // more code here 
  } 
  .comp Insensitive : CommonPointsTo<Context>  { 
     .type Context = number
     // more code here
  } 
  .init select = flavour<flavour>
}
.init myPts=points_to<TwoObjOneHeap> 
.init myPts=points_to<Insensitive>

The specific rules which are dependent on the parameter types have to be implemented separately in sub-components. So the following suggested solution shouldn't work:

.comp PointsTo<Context> {
    .rel pointsTo( c : Context, v : Variable, o : Object )
   // more declarations and rules ...
}
.init insensitive_points_to = PointsTo<[]>
.init sensitive_points_to = PointsTo< [ o1:CallSite, o2:CallSite ] >

On the other hand, it is important to have two instances of different flavours of points to in one run. Staged analysis is one usecase. For instance, analysis starts with context-insensitive PointsTo and the results are utilized by a subsequent 2O1H PointsTo.

Is it possible to use nested types to solve the type specific specialization issue?

[b-scholz]

I had another look at the current implementation of components. I forgot that we implemented parameterizable types, i.e., the attribute types of a relation can be component parameters.

Hence, I believe we can get away without extending the current implementation. With keeping it as is, I suggest the following implementation for points-to with the current realisation of components in Souffle (without my latest changes).

// Object Creation-Site
.type Variable
.type Object

// Type Declarations for 2Obj1Heap
.type Ctx2Obj1Heap = [o1:Object,o2:Object]
.type HCtx2Obj1Heap = [o:Object]

// Type Declarations for 1Obj1Heap
.type Ctx1Obj1Heap = [o:Object]
.type HCtx1Obj1Heap = [o:Object]

// EDB

.decl LocalAssign(v1:Variable, v2:Variable) input 

// Components 
.comp PointsTo<sensitivity> { 

  .comp Pts2Obj1Heap { 
      // pack relation def in a component 
      .comp relations<ctx,hctx> {
         // relations for a specific sensitivity 
         .decl PointsTo(v:Variable, c:ctx, o:Object, hc:hctx) printsize
      } 
      .init rel = relations<Ctx2Obj1Heap, HCtx2Obj1Heap> 
  } 

  .comp Pts1Obj1Heap { 
      // pack relation def in a component 
      .comp relations<ctx,hctx> { 
         .decl PointsTo(v:Variable, c:ctx, o:Object, hc:hctx) printsize
      } 
      .init rel = relations<Ctx1Obj1Heap, HCtx1Obj1Heap> 
  }

  .init analysis = sensitivity

  // add generic part 
  analysis.rel.PointsTo(v1,c,o,h) :- 
     LocalAssign(v1,v2), 
     analysis.rel.PointsTo(v2,c,o,h). 
}

.init p1 = PointsTo<Pts2Obj1Heap> 
.init p2 = PointsTo<Pts1Obj1Heap> 

The only problem which I see is that we cannot declare a namespace like in C++.
In the generic part, we need to refer to the specialized relations using a prefix, e.g., analysis.rel.PointsTo.

To overcome this issue we could pack the generic part into a component and expand it at the scope of the relations. For example,

// Object Creation-Site
.type Variable
.type Object

// Type Declarations for 2Obj1Heap
.type Ctx2Obj1Heap = [o1:Object,o2:Object]
.type HCtx2Obj1Heap = [o:Object]

// Type Declarations for 1Obj1Heap
.type Ctx1Obj1Heap = [o:Object]
.type HCtx1Obj1Heap = [o:Object]

// EDB

.decl LocalAssign(v1:Variable, v2:Variable) input 

// Components 
.comp PointsTo<sensitivity> { 

  .comp generic { 
     // add generic part 
     PointsTo(v1,c,o,h) :- 
        LocalAssign(v1,v2), 
        PointsTo(v2,c,o,h). 
  } 

  .comp Pts2Obj1Heap { 
      // pack relation def in a component 
      .comp relations<ctx,hctx> { 
         .decl PointsTo(v:Variable, c:ctx, o:Object, hc:hctx) printsize
         .init g = generic
      } 
      .init rel = relations<Ctx2Obj1Heap, HCtx2Obj1Heap> 
  } 

  .comp Pts1Obj1Heap { 
      // pack relation def in a component 
      .comp relations<ctx,hctx> { 
         .decl PointsTo(v:Variable, c:ctx, o:Object, hc:hctx) printsize
         .init g = generic
      } 
      .init rel = relations<Ctx1Obj1Heap, HCtx1Obj1Heap> 
  } 

  .init analysis = sensitivity
}

.init p1 = PointsTo<Pts2Obj1Heap> 
.init p2 = PointsTo<Pts1Obj1Heap> 

If you are not sure, what is expanded, have a look at the debug output, i.e., souffle pts.dl --debug-report=pts.html using an internet browser. Note that if there are generic relations required, they should be defined in the outer scope of PointsTo.

The only problems which remains is that the access path of relations from outer scopes become quite long. For example, p1.analysis.rel.PointsTo(v1,c,h,hc) for accessing the points-to info of p1.

[b-scholz]

I forgot to answer Herbert's question:

• Issue 2 is implemented and works correctly. No further action is required. I double-checked this today.
• Issue 1: at the moment we exclude type definitions in components. Indeed, we could extend types with scoping/access paths; my current patch is not satisfactory more work is required.

[b-scholz]

I forgot to answer Behnaz' question:

The example

.comp PointsTo<Context> {
    .rel pointsTo( c : Context, v : Variable, o : Object )
   // more declarations and rules ...
}
.init insensitive_points_to = PointsTo<[]>
.init sensitive_points_to = PointsTo< [ o1:CallSite, o2:CallSite ] >

does not work because we can only pass on symbols as parameters. To overcome this issue, we just have two type definitions as Herbert pointed out.

.type NoCtx = []
.type CtxObjObj = [o1:Object,o1:Object]
.init insensitive_points_to = PointsTo<NoCtx>
.init sensitive_points_to = PointsTo<CtxObjObj>

Another solution is to do a wrapper class that wires the attribute types

.type Variable
.type Object
.type NoObj = []
.type Obj = [ o:Object ]
.type ObjObj = [ o1:Object, o2:Object ]

.comp PointsTo<Sensitivity> {

 .comp PointsToEmbedded<Sensitivity, Context, HContext> {

    // declaration
    .decl pointsTo( v : Variable, c: Context, o : Object, hc:  HContext) printsize

    // generic code for all flavours of sensitivity

    // two-object-one-heap sensitivity
    .comp TwoObjOneHeap {
       // ...
    }

    // insensitive
    .comp Insensitive {
       // ...
    }

    // select sensitivity
    .init analysis = Sensitivity
 }

 // use the right types for each sensitivity
 .comp TwoObjOneHeap<Sensitvity> {
    .init s = PointsToEmbedded<Sensitivity,ObjObj,Obj>
 }
 .comp Insensitive<Sensitvity> {
    .init s = PointsToEmbedded<Sensitivity,NoObj,NoObj>
 }
 // select sensitivity
 .init a = Sensitivity
}

.init p1 = PointsTo<TwoObjOneHeap>
.init p2 = PointsTo<Insensitive>

The code snippet above compiles and produces the correct solution.

[b-scholz]

Perhaps my favourite option would be to hard-code the types in the choice. That might be the easiest solution:

// Object Creation-Site
.type Variable
.type Object

// Type Declarations for 2Obj1Heap
.type Ctx2Obj1Heap = [o1:Object,o2:Object]
.type HCtx2Obj1Heap = [o:Object]

// Type Declarations for 1Obj1Heap
.type Ctx1Obj1Heap = [o:Object]
.type HCtx1Obj1Heap = [o:Object]

// EDB

.decl LocalAssign(v1:Variable, v2:Variable) input 

// Components 
.comp PointsTo<sensitivity> { 

  .comp generic { 
     // add generic part 
     PointsTo(v1,c,o,h) :- 
        LocalAssign(v1,v2), 
        PointsTo(v2,c,o,h). 
  } 

  .comp Pts2Obj1Heap { 
      // pack relation def in a component    
      .decl PointsTo(v:Variable, c:Ctx2Obj1Heap, o:Object, hc:HCtx2Obj1Heap) printsize
      .init g = generic
  } 

  .comp Pts1Obj1Heap { 
      .decl PointsTo(v:Variable, c:Ctx1Obj1Heap, o:Object, hc::Ctx1Obj1Heap) printsize
      .init g = generic
  } 
  .init analysis = sensitivity
}

.init p1 = PointsTo<Pts2Obj1Heap> 
.init p2 = PointsTo<Pts1Obj1Heap> 

[b-scholz]

And I believe an even better way of implementing PointsTo with different flavours is to use super/sub-components as an idiom:

// Object Creation-Site
.type Variable
.type Object

// Type Declarations for 2Obj1Heap
.type Ctx2Obj1Heap = [o1:Object,o2:Object]
.type HCtx2Obj1Heap = [o:Object]

// Type Declarations for 1Obj1Heap
.type Ctx1Obj1Heap = [o:Object]
.type HCtx1Obj1Heap = [o:Object]

// EDB

.decl LocalAssign(v1:Variable, v2:Variable) input 

// Components 
.comp PointsTo { 
     // add generic part 
     PointsTo(v1,c,o,h) :- 
        LocalAssign(v1,v2), 
        PointsTo(v2,c,o,h). 
} 

.comp Pts2Obj1Heap : PointsTo { 
      .decl PointsTo(v:Variable, c:Ctx2Obj1Heap, o:Object, hc:HCtx2Obj1Heap) printsize
} 

.comp Pts1Obj1Heap : PointsTo { 
      .decl PointsTo(v:Variable, c:Ctx1Obj1Heap, o:Object, hc:Ctx1Obj1Heap) printsize
} 

.init p1 = Pts1Obj1Heap 
.init p2 = Pts2Obj1Heap

which permits access to the points-to relation with p1.PointsTo.

[b-scholz]

Unfortunately, this thread covers now three issues:

• Finding an appropriate idiom for Behnaz' points-to problem; perhaps no type declarations inside components are required?
• Adding types to components with scoping. My current branch http://github.com/b-scholz/scholz:component-types pushes type definitions in components to the global scope which is insufficient from an implementation viewpoint. This needs to be enhanced.
• Herbert's suggestion of having type constraints for component instantiation which would make the component model even more powerful.

[HerbertJordan]

Today I was attempting to use a type declaration within a component, however I could not make it work. What I tried was similar to this:

.comp Collection<Element> {
   .decl values( e : Element )
   // ... some operations ...
}
.comp Map<Key,Value> {
   .type pair = [ k : Key , v : Value ]
   .init Data = Collection<pair>
}
.init Stuff = Map<symbol,number>

This is just a small example, the actual use case is a bit more complicated. But it seems like souffle does not allow me to define types in components, as requested by this thread.

I was wondering whether this was a) me not able to formulate it properly, b) a bug in the implementation, c) a feature not yet merged into the main version, or d) a feature not yet implemented to be added to the system. If d), should I add it?

[HerbertJordan]

Note: that this also is an example where "push-to-global-scope" policy would not be sufficient since the pair type may be different for every instantiation.

For symmetry reasons I'd suggest to treat nested types identical to nested relations and prefix their names with a instantiation name. If acceptable, I can implement it by monday.

[behnazh]

I think the nested-type feature is not implemented. I solved my points-to problem using the wrapper class that wires the attribute types. However, I also believe that the "push-to-global-scope" policy is not sufficient.

[b-scholz]

I have only a patch that solves the problem partially. I.e., type definitions are global and do not have a scoping. As soon as the semester is over, I will implement it.

[b-scholz]

By the way - you find my patch for push to global scope under
http://github.com/b-scholz/souffle:component-types