Add HighStrata

[keyboardDrummer]

Changes

Introduce a HighStrata language that serves as a target for compilation for Java. It contains features that we expect will make it useful for compilation from other languages as well, such as Python, JavaScript and TypeScript. However, this first version may contain only all the features required for compilation from Java. This PR adds a type that defines the language and an interpreter to define its semantics.

Example programs, written using a Java-like syntax.

Mixed statements and expressions

@Pure
int nesting(int a) {
    precondition(a > 0 && a < 100);
    var b = a + 2;
    if (b > 2) {
        var c = b + 3;
        if (c > 3) {
            return c + 4;
        }
        var d = c + 5;
        
        return d + 6;
    }
    var e = b + 1;
    return e;
}

int nestedImpureExpression() {
    if (impureM(1) == 1) {
        var x = impureM(impureM(2));
        return x;
    }
    return impureM(3);
}

// impure because it is not marked as Pure
int impureMethod(int input) {
    return input;
}

Immutable fields

class HasImmutableField {
  final int x;

  int returnX() {
     return x; // this does not need a reads clause, because is final
  }
}

Test test + pattern match

class C implements I {
    int x;
}

int ifThenElseFlow(I i) {
    if (i instanceof C c) {
        return c.x;
    }
    return 3;
}

class I {}
class J extends I {
    @Pure
    I anotherI() abstract
    int value() {
        return 3;
    }
}
class G extends I {
    int value() {
        return 0;
    }
}
boolean andOperatorFlow(I i) {
    if (i instanceof J j && j.anotherI() instanceof G g) {
        return j.value() + g.value() == 3;
    }
    return true;
}

Inheritance + Partial types/methods

NOTE: Partial types/methods need a design review. They are needed to fully support Java constructors

class Extender extends Base {
    int z;

   @Partial
    Extender Construct(int input) {
        super.Construct(input + 2);
        precondition(input < 10);
        postcondition((Extender r) -> r.x == 3);
        z = 2;
        return complete(this);
    }

    @Pure
    int computeX(int input) {
        return 3;
    }

    int virtualMethod() {
        postcondition((int r) -> r >= 20);
        return 20;
    }
}


class Base {
    int x;
    final int y;
    
    @Partial
    Base Construct(int input) {
        postcondition((Base r) -> r.x == r.computeX(input));
        x = computeX(input);
        y = 3;
        return complete(this);
    }

    @Pure
    int getX() {
        reads(this);
        return x;
    }

    @Partial
    int computeX(int input) abstract
    
    int virtualMethod() {
        postcondition((int r) -> r >= 10);
        return 10;
    }
}

Inheritance + further constraining postconditions

class Extendee {
    int virtualMethod() {
        postcondition((int r) -> r >= 10);
        return 10;
    }
}

class Extender extends Extendee {
    int virtualMethod() {
        postcondition((int r) -> r >= 20);
        return 20;
    }
}

Polymorphism

class Pet {
    void feed() abstract
}

class Canid {
    void socialize() abstract
}

class Dog implements Pet, Canid {
    void feed() assumed
    void socialize() assumed
}

class Cat implements Pet {
    void feed() assumed
}

class PetContainer<T extends Pet> {
    T value;

    void doFeed() {
        value.feed();
    }
}

void root() {
    var dog = new Dog();
    var cat = new Cat();
    PetContainer<Dog> container = new PetContainer<Dog>(dog);
    container.doFeed();

    PetContainer<Cat> container2 = new PetContainer<Cat>(cat);
    container2.doFeed();

    feedAndSocialize(dog);
}

static void feedAndSocialize<T extends Canid & Pet>(T a) {
    a.feed();
    a.socialize();
    takesAPet(a);
}

void takesAPet(Pet pet) {
    pet.feed();
}

void polymorphicBound<T extends Polymorphic<T>>(T t) {
    t.foo();
}

class Polymorphic<T> {
    void foo() abstract
}

Static field and static constructors

Static constructors are not in the AST yet and need more thought related to ordering when multiple static constructors are present

static int y;
    
static {
  y = 2;
}

Alternative design options

Instead of supporting type polymorphism, we could also let the source language inject type assumptions at locations where polymorphisms allows us to know what type a value has. This means doing additional work in the compilation to high-strata, but avoids having a complicated feature in the strata language. In particular, variance of polymorphic types is complicated and that could be avoided using type assumptions as well.

Testing

WIP. Right now this PR includes as unfinished operational semantics of the high strata dialect.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[atomb]

What are these used for? Reals don't exist in any of the languages we're considering modeling. I'd have thought we'd call them floats, with the semantics of floats, and have the option of modeling them (inexactly) as reals during analysis.

[keyboardDrummer]

Good point. Initially I thought one of our customers would be using a BigRational in Java, but they won't be, so I think we can leave this out for now

[atomb]

Do we actually need to declare composite types? I'm tempted by the approach that Viper uses: https://viper.ethz.ch/tutorial/#fields

[keyboardDrummer]

I think there are two uses for declaring fields:

• You can specify whether they are mutable or not, which affects the heap permissions needed to access them.
• You can specify the type of the field, which allows you to know the type of an expression reading that field, which when there are invariants on that type, allows you to verify more things about the result of reading that field.

[atomb]

Yeah, I think declaring fields is probably essential. But the types surrounding them might not need to exist. If you look at the Viper doc I linked to, they talk a little about that.

[keyboardDrummer]

But the types surrounding them might not need to exist

Ah I see. Good point. You could have the field access operations use a unique identifier for the field, so you don't need to know the containing type to resolve which field it is. It could be interesting to define the fields separately.

Something that I imagine the containing types are needed for, is for type tests, since they depend on the type hierarchy of the composite types.

[atomb]

The alternative approach, for type tests, would be to do the following:

• declare an abstract type of types, with a unique constant of this type for each class or interface that exists in Java
• have a field in every object that stores its type
• have an extends predicate which indicates which types extend which others

All of the features needed for this already exist in the Boogie dialect, so it'd be easy to have them in HighStrata.

It would be possible, given information about type parameters at the Java level, to introduce assumptions about the type of, for example, an element selected from a generic collection. So then we might not need type parameters in HighStrata.

[keyboardDrummer]

All of the features needed for this already exist in the Boogie dialect, so it'd be easy to have them in HighStrata.

I think those features might already be in the high strata language in this PR as well. You can define extends as a static function.

However, this alternative approach means that the client that's compiling to high strata would have to do more work right? In particular, then they need to define the extends predicate.

It would be possible, given information about type parameters at the Java level, to introduce assumptions about the type of, for example, an element selected from a generic collection.

Yes, I think indeed you can use type-assumptions to remove the need for polymorphism. You would insert the assumptions for example when assigning something of type T to a concrete type, but also when using type bounds on T to access a member from a value of type T. However, the client then needs to do decide where to add these assumptions, so it is more work for the client.

Also, we should be careful to add the correct type in the assumption, for example, if I have a List<Integer> xs and then I do Object o = xs.get(0), then the type assumption for the retrieved value still needs to be Integer, not Object, since code that follows might need to know that.

Do you think that polymorphism, as it is added to high-strata in this PR, won't be useful for source languages other than Java? I think for Kotlin it would be.

My thinking is, let's add the information we have at the simplified Java level, which includes type definitions and their type parameters, and add it in high-strata. Just having that information in the AST will not cost us any effort. If you then find that some of this information you don't actually need, then sure remove it from the AST.

[atomb]

When it comes to polymorphism, it's not so much that I think it wouldn't be useful for other source languages as that it might not be compatible with other source languages. Although I don't think Rust would likely go through this dialect, I've been thinking about the differences between its notion of generics and Java's, as one example. That said, I'm not necessarily opposed to including it.

A client would need to define the extends predicate, but that seems like not any more work than emitting class declarations with superclasses (though it does have a slightly different structure, so it's perhaps easier to get it wrong).

[atomb]

If there were algebraic data types, would that be a convenient alternative?

[keyboardDrummer]

For verification from Java, I don't see a use for algebraic datatypes. There's nothing in Java that would map to them. The concept of a ADT in Java can be modeled using a sealed interface and several implementing records, but that can not be mapped to an actual ADT since in the Java version, each implementing record is a type on its own, which can occur in for example a type test or be the type of a local variable, while in an ADT the constructors are not types.

[atomb]

Yeah, I wouldn't expect them to directly model Java types. I was more wondering whether you were using things like Option for internal purposes. But if it's just the representation of an Option type that exists at the Java level, then I agree.

[atomb]

And I think this answers my question about composite types above. :) If you don't have named type, you can't create a constrained version of it.

[keyboardDrummer]

I was more wondering whether you were using things like Option for internal purposes.

We're not

[keyboardDrummer]

I was wondering whether we could get rid of the need of a ConstrainedType, by adding instead an invariant: StmtExpr field to CompositeType, but the issue is then the composite type would always wrap whatever type you want to add a constraint to, so it doesn't seem like it would work as a replacement