Working with precise/unprecise DomainValues in Abstract Interpretation is OPAL

Question

In my OPAL-analysis, I create domain values in the following manner:

domain.TypedValue(org.opalj.ai.parameterToValueIndex(
    caller.isStatic, caller.descriptor, index), typeApproximation.upperTypeBound)

In my typeApproximation objects, I have the information, whether its type is an upper type bound or a precise runtime type. However, I do not know, how to pass this information to the respective DomainValue.

I pass these DomainValues to the BaseAI.perform method to perform an abstract interpretation of a java method:

BaseAI.perform(classFile, caller, domain)(Some(parameters))

The DomainValues are contained in the parameters value.

Is there any possibility to tell the abstract interpretation, that some of my parameters are precise runtime types, while some other parameters are only upper type bounds?

Answer 1

The factory methods defined by org.opalj.ai.ReferenceValuesFactory (which are always available) enable you to create values that have the required properties. E.g. using InitializedObjectValue a DomainValue will be created where the type is assumed to be precise. Using the factory method: ReferenceValue the given type is treated as an upper type bound. Additionally, org.opalj.ai.l1.DefaultReferenceValuesBinding defines the generic factory method:

def ObjectValue(
    origin:            ValueOrigin,
    isNull:            Answer,
    isPrecise:         Boolean,
    theUpperTypeBound: ObjectType,
    t:                 Timestamp
): SObjectValue 

which gives you complete control.