In OPAL, fixed-point analyses need to represent their results using values from an explicitly defined lattices.

This article will discuss a few possibilities when defining them.

You should have read the tutorial on Writing Fixed-Point Analyses first that introduces the basic concepts.

There are two basic kinds of lattices that are typically used in OPAL: singleton-based lattices and set-based lattices.
It is also possible to combine them.

Before discussing each of them individually, let's have a look at what they have in common.

A lattice in OPAL consists of three parts.

The first one is the `PropertyMetaInformation`

:

```
sealed trait ClassImmutabilityPropertyMetaInformation extends PropertyMetaInformation {
final type Self = ClassImmutability
}
```

We use it to provide the type of the property.

Second, the property companion object provides the PropertyKey:

```
object ClassImmutability extends ClassImmutabilityPropertyMetaInformation {
final val key: PropertyKey[ClassImmutability] = PropertyKey.create(
"ClassImmutability",
MutableClass
)
}
```

We discuss more on the `PropertyKey`

below.

A second use of the companion object would be to provide factory methods to create your lattice values conveniently.

Finally, the actual properties.

If you have more than one class, you should provide a trait through which the `PropertyKey`

can be accessed:

```
sealed trait ClassImmutability extends ClassImmutabilityPropertyMetaInformation {
final def key: PropertyKey[ClassImmutability] = ClassImmutability.key
}
```

Implement your lattice using classes that implement this trait.

If you only need a single class for your lattice, you can of course define the `key`

method there and omit defining a trait.

You can also use this trait to declare methods that you need for lattice, like `meet`

or `join`

methods or methods to extract data from your lattice values conveniently.

Singleton-based lattices are very common in OPAL.

They consist of a number of case objects each of which represents a singleton value of the lattice:

```
case object TransitivelyImmutableClass extends ClassImmutability
case object NonTransitivelyImmutableClass extends ClassImmutability
case object MutableClass extends ClassImmutability
```

Of course, you may need to implement any methods defined in your trait above.

The second common type of lattices in OPAL is set-based lattices. They typically consist of one (or sometimes several) case classes that hold the set of values:

```
case class InstantiatedTypes(classes: UIDSet[ObjectType]) extends InstantiatedTypesPropertyMetaInformation {
final def key: PropertyKey[InstantiatedTypes] = InstantiatedTypes.key
}
```

Note that here we extended the `PropertyMetaInformation`

directly without an additional trait as we need only one class.

You can combine both concepts in a single lattice if you need to.

For example, you could extend the above `ClassImmutability`

lattice with this set-based case class:

```
case class DependentlyImmutableClass(dependentTypeParameters: Set[String])
```

Or you could provide a singleton object as a convenient extension for the above `InstantiatedTypes`

lattice:

```
object NoInstantiatedTypes extends InstantiatedTypes(UIDSet.empty)
```

However, always take care that what you implement really has the semantics of a lattice (i.e., the values form a partial order and there exist a unique least upper bound and unique greatest lower bound for every two values).

There are two additional classes that you might want to consider when implementing your lattice.

The first one is `OrderedProperty`

.

If your lattice values extend this trait, you get additional checks in the PropertyStore whether your analyses refine their results monotonically with respect to your lattice's partial order.

`OrderedProperty`

requires that you implement a method `checkIsEqualOrBetterThan(e: Entity, other: Self)`

that should throw an exception if `other`

is greater than the current value with respect to the lattice's partial order.

If you defined a `meet`

method, you can simply implement it like this:

```
override def checkIsEqualOrBetterThan(e: Entity, other: ClassImmutability): Unit = {
if (meet(other) != other) {
throw new IllegalArgumentException(s"$e: impossible refinement: $other ⇒ $this")
}
}
```

However, it may be better to provide optimized implementations for your individual lattice values if the `meet`

operation is not trivial.

The second option to consider is `AggregatedProperty`

.

Some properties really represent an aggregation of another property, e.g., `ClassImmutability`

aggregates the `FieldImmutability`

of a class' instance fields.

In such cases, one often needs to convert between corresponding values of the two lattices.

Also, the partial order and thus `meet`

operator are equivalent and need to be defined only once.

In order to use `AggregatedProperty`

, the base lattice has to extend `IndividualProperty[BaseLattice, AggregateLattice]`

, implement the `meet`

method as well as an `aggregatedProperty`

method that maps each value to its corresponding value of the aggregated lattice.

The aggregate lattice then has to extend `AggregatedProperty[BaseLattice, AggregateLattice]`

.

It has to implement the `individualProperty`

method that maps each value to the corresponding value of the base lattice.

The `meet`

method on the aggregate lattice is provided for you based on the `meet`

operator of the base lattice.

The `PropertyKey`

makes your lattice known to OPAL and gives it a unique identifier.

You create it using one of two methods:

```
final val classImmutabilityKey: PropertyKey[ClassImmutability] = PropertyKey.create(
"ClassImmutability",
MutableClass
)
final val instantiatedTypesKey: PropertyKey[InstantiatedTypes] = PropertyKey.create(
"InstantiatedTypes",
(_: PropertyStore, reason: FallbackReason, _: Entity) ⇒ reason match {
case PropertyIsNotDerivedByPreviouslyExecutedAnalysis ⇒ InstantiatedTypes(UIDSet.empty)
case _ ⇒ throw new IllegalStateException(s"No analysis is scheduled for property InstantiatedTypes")
}
)
```

For both, you provide a unique name for your lattice and a fallback if a value from your lattice is queried but not computed.

The difference is in the fallback: You can either provide a single lattice value to use in all cases.

It should be your lattice's bottom element in order to be sound.

Or you can provide a function to compute the fallback value on demand.

This has two benefits: First, you can use some information about your entity to compute a sound but more precise fallback value.

Additionally, as shown above, this function gets a `FallbackReason`

.

This tells you whether no analysis was executed to compute any values of your lattice at all (`PropertyIsNotComputedByAnyAnalysis`

), in which case you should provide a sound over-approximation as before.

Or it tells you that an analysis was executed, but it did not provide a result for the respective entity (`PropertyIsNotDerivedByPreviouslyExecutedAnalysis`

), in which case you may be able to provide a precise result, because you know that, e.g., the entity belongs to dead code.