Model verifier

[asotona]

This patch starts work on model Verifier and implements following verifications:

• operands declaration dominance
• BranchOp reference arguments matching target block parameters (simple matching by TypeKind with erased int sub-types)
• ArithmeticOperation, TestOperation and ConvOp verified presence of relevant method handler in InvokableLeafOps

TestSmallCorpus is improved to verify code model.

Fixes of bugs newly discovered by the TestSmallCorpus:

• missing methods in InvokableLeafOps
• Interpreter use of provided lookup for resolveToMethodType
• Interpreter erase sub-int types for InvokeOp execution + added TestLiftCustomBytecode::testEraseInts
• Removed complex sub-int types calculation from BytecodeLift and LocalsToVarMapper
• BytecodeLift fixed to avoid production of some obsolete block parameters

---

Progress

• Change must not contain extraneous whitespace

Reviewing

Using git

Checkout this PR locally:
$ git fetch https://git.openjdk.org/babylon.git pull/247/head:pull/247
$ git checkout pull/247

Update a local copy of the PR:
$ git checkout pull/247
$ git pull https://git.openjdk.org/babylon.git pull/247/head

Using Skara CLI tools

Checkout this PR locally:
$ git pr checkout 247

View PR using the GUI difftool:
$ git pr show -t 247

Using diff file

Download this PR as a diff file:
https://git.openjdk.org/babylon/pull/247.diff

Webrev

Link to Webrev Comment

[bridgekeeper]

👋 Welcome back asotona! A progress list of the required criteria for merging this PR into code-reflection will be added to the body of your pull request. There are additional pull request commands available for use with this pull request.

[openjdk]

@asotona This change is no longer ready for integration - check the PR body for details.

[mlbridge]

Webrevs

• 01: Full - Incremental (2155ccb3)
• 00: Full (104ef7dd)

[PaulSandoz]

Can you provide an example of why this is required? I think i can guess based on changes to the lifter. Can this impact other areas too like field and array access?

I think in general we have to be careful here. The properties of lifted models are having a broader impact. Arguably, this could be a code model transformation instead.

Terminology-wise "erase" is reserved for references. IIUC correctly we are operating on values of basic primitive types and i believe converting to them non-basic types based on corresponding method parameter types.

[asotona]

Example is provided by the test:

babylon/test/jdk/java/lang/reflect/code/bytecode/TestLiftCustomBytecode.java

Line 74 in 104ef7d

public void testEraseInts() throws Throwable {

Yes, it can impact also other areas and more similar Interpreter corrections might be necessary.

I'm aware of the impact of "erasing" int sub-types. We have to make a decision if all int sub-types are freely assignable (according to JVMS) or their assignability is strictly specified (as in JLS). This PR is a step toward the first option, where Interpreter should not fail on an attempt to call a method with short parameter when passing a boolean as an argument.

A transformation inserting explicit type conversions is the option if we decide to go the assignability-strict way.

Exactly the same issue is with objects assignability. Should we allow to pass an argument declared as of j.l.Object type to a method with other specific type parameter or should we inject explicit casts?

[PaulSandoz]

The interpreter is indeed "relaxed" about references and boxing conversions, opting to use Method/VarHandle.invoke rather than invokeExact etc, guarding at runtime with casts and boxing/unboxing conversions.

This does mean there is some possible ambiguity when building code models explicitly and invoking say method m(int ) when the method's argument's type is unintentionally declared to be symbolically an Integer. We don't differentiate because all runtime values are boxed and it is simpler not to track in more detail.

e.g.,

        CoreOp.FuncOp f = CoreOp.func("f", FunctionType.functionType(JavaType.VOID, JavaType.J_L_INTEGER))
                .body(b -> {
                    Block.Parameter i = b.parameters().get(0);
                    b.op(CoreOp.invoke(MethodRef.method(T.class, "m", void.class, int.class), i));
                    b.op(CoreOp._return());
                });
        System.out.println(f.toText());

        // Works, the Integer parameter is unboxed to an int argument
        Interpreter.invoke(MethodHandles.lookup(),
                f, 1);

Change to:

        CoreOp.FuncOp f = CoreOp.func("f", FunctionType.functionType(JavaType.VOID, JavaType.J_L_STRING))
                .body(b -> {
                    Block.Parameter i = b.parameters().get(0);
                    b.op(CoreOp.invoke(MethodRef.method(T.class, "m", void.class, int.class), i));
                    b.op(CoreOp._return());
                });
        System.out.println(f.toText());

And the interpreter will rightly fail in MethodHandle.asType conversion when interpreting the invoke operation.

We could make the interpreter perform stronger runtime checks according to the symbolic types thereby identify issues closer to the problem. Although perhaps that is a validation step? So far though I like the simplicity and using reflection to catch the issues.

However, I think basic narrowing primitive conversions (int to short etc) are a little different because they can in general be lossy and there is no failure, by design, in such cases. This strongly suggests to me that such implicit and lossy primitive conversions should be something that is not the default behaviour and we should opt in. Then that behaviour can be used for models lifted from bytecode that operate on basic primitive types.

In effect what we have now is this kind of transformation pipeline

Java source -> Model-high -> Model-low -> bytecode -> Model-low-basic

Then ideally we round trip on:

bytecode -> Model-low-basic -> bytecode -> Model-low-basic

And ideally we could also support reverse engineering to sharper types

Model-low-basic -> Model-low

And we could of course support

Model-low -> Model-low-basic

But what i am wary of right now is making Model-low become Model-low-basic or some blurring of two.

[asotona]

OK, I think I understand the direction, relaxed rules have ugly side effects. I'll change this PR the other way - lift will insert explicit int conversions to the identified places where Interpreter would clearly fail. Interpreter stay more strict and Verifier follow the Interpreter.

[PaulSandoz]

Ok, we can always go with passing an option to the Interpreter if the transformation approach does not work out.

[PaulSandoz]

I would avoid extending Error as it signals some serious abnormal condition when thrown, and these are not intended to be thrown.

[asotona]

I'll fix it, thanks.