Support of UTypeStreams and casts in JcInterpreter

[sergeypospelov]

This PR introduces an initial support of types in JcInterpreter. Also, some other improvements were made, including fix of binary operations for integral types. The Java tests were revised, some of them were enabled. Disabling reasons were updated.

Details

UIsExpr

Represents a constraint that either some ref is null, or it's not null and its type is a subtype of some other type. This corresponds to a reference cast in Java, but not to instanceof. It brings confusion, so maybe we should rename it, or change its semantics.

UTypeSystem

A base interface, instantiated in target machines. Provides information about types and topTypeStream, representing all possible types in the system.

UTypeStream

A base interface representing persistent type constraints and a way to access types satisfying them. Consists of a conjunction of constraints of four kinds:

1. x <: T, i.e. object referenced in x inherits T (supertype constraints for x)
2. T <: x, i.e. object referenced in x inherited by T (subtype constraints for x)
3. x </: T, i.e. object referenced in x does not inherit T (notSupertype constraints for x)
4. T </: x, i.e. object referenced in x is not inherited by T (notSubtype constraints for x)

It doesn't have references to an actual ref expression.

USupportTypeStream

A generic implementation of UTypeStream interface based on support type. It works as follows:

• we maintain a support type instance and type predicates
• a support type is one of the super types, or object in the beginning
• if the type from a supertype constraint is a subtype of the current support type, we update the support type
• we use caching sequences to prevent extra queries to the type system

Type constraints solving

It's a DPLL(T)-like procedure. Briefly, getting complete UModelBase with type assignment, satisfying pc: UPathConstraints, works as follows:

1. Get KModel
2. Decode it into model: UModelBase without any type information
3. Check that references in the model satisfies the type constraints. There could be 4 results:
   1. References satisfy type constraints, so we can fill model with a type model and return the complete UModelBase
   2. References doesn't satisfy in the current model, but there can be another one, so we get constraints on reference equalities and try again from the step 1
   3. References doesn't satisfy type constraints in any model, so we return pc is unsatisfiable
   4. Some UTypeStream evaluation didn't finish, so we return unknown result.

The disequality constraints determined as follows:

1. Groups symbolic references into clusters by their concrete interpretation in the [model] and filters out nulls
2. For each cluster, processes symbolic references one by one and intersects their type regions
3. If the current region became empty, then we found a conflicting group, so add reference disequality
4. If no conflicting references were found, builds a type model

Example:

a <: T1 | T2
b <: T2 | T3
c <: T3 | T1
d <: T1 | T2
e <: T2
cluster: (a, b, c, d, e)

Suppose we have the single cluster, so we process it as follows:

1. Peek a. The current region is empty, so it becomes T1 | T2. Potential conflicting refs = {a}.
2. Peek b. The current region becomes T2. Potential conflicting refs = {a, b}.
3. Peek c. The intersection of the current region with T3 | T1 is empty, so we add the following constraint: a != c || b != c || a == null || b == null || c == null. The region becomes T3 | T1. Potential conflicting refs = `{c}.
4. Peek d. The current region becomes T1. Potential conflicting refs = {c, d}.
5. Peek e. The intersection of the current region with T2 is empty, so we add the following constraint: c != e || d != e || c == null || d == null || e == null.

Note that symbolic objects of definitely incomparable types resolve to different concrete references thanks to UEqualityConstraints.

UTypeModel

It's a storage for types of input values. We assume, that no allocated references can leak to the UModelBase, so it throws in such case. For every input reference, it stores a UTypeStream. Resolution of the evalIs(ref: UHeapRef, type: Type) processes in the next steps:

1. Search for the (ref as UConcreteHeapRef).address in the cache. If no UTypeStream found, take the top type stream.
2. Intersect the type stream from the previous step with the supertype constraint <: type.
3. If the result type stream is empty, return false. Otherwise, return true and update the cached type stream to the narrowed one.

This lazy procedure allows reducing the number of requests to the solver.

UReadOnlyTypedMemory

To unify types handling in a memory and in a model, I introduced UReadOnlyTypedMemory interface with a single method:

    /**
     * @return a type stream corresponding to the [ref].
     */
    fun typeStreamOf(ref: HeapRef): UTypeStream<Type>

JcTestResolver

It was noticeably improved to support the type resolution. Also fixed some problems with arrays. The type resolution works as follows:

• Primitive types are always resolved statically based on JacoDB.
• Reference types are resolved based on their concrete address.
  1. If the address corresponds to an input object, we take the type stream from the model. Model returns the top type stream, if there is no information about the reference.
  2. If the address corresponds to an allocated object, we take the type stream from the memory type constraints.
• In the first case, we intersect the taken type stream with the static type from JacoDB.

Further work

• Propositional type variables and support of (a instanceof T).not()
• Virtual invokes
• A connection between constraints on array element types and an array type.
• Prioritize types somehow
• Generics

Questions

• Do we really need isTerminated flag as a return value in UTypeStream? (No, let's assume take works negligibly little time.)
• Maybe rename UIsExpr, because it isn't instanceof?
• How to get rid of the silly cast in JcTestResolver? (Make UTypedReadOnlyMemory)

Other

• Update JacoDB version to 1.1.3
• Update reasons of disabling tests
• Fix several issues in JcTestResolver
• Fix binary operations for integral types (boolean, char, byte, short)
• Several renames
• Add an option to ignore null refs in heap ref splitting utility functions

PR TODO

• Description
• Review failing tests
• Add comments
• Add more tests

[Damtev]

We store this field for each type constraint although it depends only on the type system. Isn't it better to keep it in a type system, for memory optimization purposes?

[sergeypospelov]

Hm, I'd prefer keeping it as it is, because UTypeRegion is something internal, whereas UTypeSystem is an open interface for target languages.

[Damtev]

What about using by lazy instead of getter?

[sergeypospelov]

Don't want to have extra memory allocations. Evaluation of typeStream.isEmpty for subsequent calls works fast

[Damtev]

LGTM