Gno type check

[ltzmaxwell]

Description:

The issue is from #1376 , and here gives an analysis and solution.

Q: Does this code successfully compile? If so, what is the expected output?

package main

import (
    "errors"
    "strconv"
)

type Error int64

func (e Error) Error() string {
    return "error: " + strconv.Itoa(int(e))
}

var errCmp = errors.New("XXXX")

func main() {
    if Error(0) == errCmp {
        println("what the firetruck?")
    } else {
        println("something else")
    }
}

A: The code is expected to compile without issues, and logically, the output should be something else. However, when run in the gnovm environment, it produces the result what the firetruck?.

The code successfully compiles because Error(0) is assignable to the type of errCmp. This is due to the fact that the type Error fulfills the same interface requirements as errCmp, making them compatible in terms of type assignment.
according to spec: "In any comparison, the first operand must be assignable to the type of the second operand, or vice versa."

Moreover, at runtime, they ought to be evaluated as unequal, given that they have distinct underlying types . The reason for the incorrect output lies in a type-checking issue: both Error(0) and errCmp are erroneously treated as if they are of the same int64 type, which is the underlying type of Error(0). Consequently, when evaluated as int64, their values are both 0, leading the comparison to incorrectly yield true.

Deeper analysis:

Upon further investigation, it was discovered that there are more issues with type checking.

• Absence of Type Mixture Verification

func main() {
    println(int(1) == int8(1))
}

In this instance, the code is expected to fail compilation because of a type mismatch. Surprisingly, it compiles and runs without error. This anomaly can be attributed to the absence of standard type checking, resulting in a forced and inappropriate type casting for all consts.

• Absence of Compile-Time Validation for Operand Compatibility with Operators

package main

// one untyped const, one typed const
func main() {
println(1 / "a")
}

This code operates correctly, identifying an error with the illegal operand for the / operator. However, in the current setup, checks related to operators are performed at runtime. Ideally, these checks could and should be conducted during the preprocessing stage for enhanced efficiency and error handling.

This approach can be extended to multiple scenarios involving a variety of operators such as +, -, *, /, %, &, and others, encompassing a broader range of use cases and operator interactions.

• Lack of implicit conversion from unnamed types to named types

package main

type word uint
type nat []word

func (n nat) add() bool {
    return true
}

func Gen() nat {
    n := []word{0}
    return n
}

func main() {
    r := Gen()
    switch r.(type) {
    case nat:
        println("nat")
        println(r.add())
    default:
        println("should not happen")
    }
}

Conclusion:

In this scenario, nat is a named type whose underlying type is []word. However, within the main function, the variable r should be recognized as type nat, but it is not being correctly asserted as such.

In conclusion, during the preprocessing stage, there is a noticeable absence of crucial checks. These include the verification of type mixtures, validation of operand compatibility, and the implicit conversion of types from unnamed to named.

Solution:

The solution is straight forward based on the analysis above.

1.regular type check for const.

This ensures standard scenarios, such as converting an untyped constant to a typed constant, function as intended (e.g., int(1) + 0). At the same time, it prohibits illegal conversions, like int(1) + int(8). It's important to note that in certain specific cases, this check may be bypassed. For example, an int8 can be used as a slice index since it will be forcefully converted to an int type.
e.g.

package main

func main() {
	a := [...]int{
		int8(0): 1,
	}
	println(a[0])
}

2. check operand compatibility with operators.

For binary expressions, unary expressions, and increment/decrement statements, it is essential to check the compatibility of operands during the preprocessing stage. This approach will effectively filter out most issues related to type compatibility. For example, it would identify and flag incompatible operations like 1 / "a".

3. checkOperand for special case

with / and %, divisor should not be zero.

4. check implicit unamed -> named, and convert

Expriment:

Here is a (WIP) PR that addresses all the aforementioned issues. While it is not yet complete, any feedback or suggestions for improvement would be greatly appreciated. #1426

======update:
also with this issue #1462

[jaekwon]

what the firetruck?.

I think there was typechecking in isEql but it got removed over time. Good catch. I'm a bit amused as to how none of the tests caught this thus far. Thank you for catching it.

Maybe there ought to be two operators. One that does what isEql does now, and another that does type checking, and the preprocessor can figure out whether runtime type checking is needed or not. There are a range of solutions, and let's discuss the pros and cons of them before implementing, unless you're happy to delete work and try another route. (I am, so if you are no problem. Or if you're feeling lucky...).

Absence of Type Mixture Verification

func main() {
println(int(1) == int8(1))
}

In this instance, the code is expected to fail compilation because of a type mismatch. Surprisingly, it compiles and runs
without error. This anomaly can be attributed to the absence of standard type checking, resulting in a forced and
inappropriate type casting for all consts.

Here's the type checking model we should be gunning for.

1. We should piggy back on the Go typechecker by translating Gno to Go and making sure it compiles, before accepting a package in AddPkg. This is why we have gno precompiling. This is because there is a good chance we will miss something even if we try to make it perfect.
2. After launch we can work toward perfecting the type checking system. But any work toward improving it will be merged as long as every pull request is complete (and well factored).
3. I'm not sure why we aren't already doing 1, but we should start doing it asap. The precompiled files should be persisted in a directory that is safe (in GNOHOME somewhere NOT GOPATH) and new AddPkg calls should compile against the precompiled dummy files.

There's nothing wrong with the VM itself doing useful work with invalid Go code. The solution should be in the precompiler.

Lack of implicit conversion from unnamed types to named types

We do, but it seems we missed a case for switch case assignments.

[ltzmaxwell]

Here's the type checking model we should be gunning for.

1. We should piggy back on the Go typechecker by translating Gno to Go and making sure it compiles, before accepting a package in AddPkg. This is why we have gno precompiling. This is because there is a good chance we will miss something even if we try to make it perfect.
2. After launch we can work toward perfecting the type checking system. But any work toward improving it will be merged as long as every pull request is complete (and well factored).
3. I'm not sure why we aren't already doing 1, but we should start doing it asap. The precompiled files should be persisted in a directory that is safe (in GNOHOME somewhere NOT GOPATH) and new AddPkg calls should compile against the precompiled dummy files.

There's nothing wrong with the VM itself doing useful work with invalid Go code. The solution should be in the precompiler.

I agree with this 100%. If I understand correctly, we plan to leverage Go's type-check tools as the first assurance before relying on GnoVM type check, and keep on perfecting the gno type check features, right?

In addition to this, I propose executing precompiled files in Go during the test, and catch the result as a comparison with the GnoVM, like:

// Gno(0.9) Output:
// what the firetruck?

// Go(1.21) Output:
// something else

Introducing this approach will make it more convenient for individuals to identify differences, ensuring that Gno not only matches Go in terms of type-checking but also in the execution behavior.

[moul]

This could enhance our lives, but I don't think it's essential for the launch. Does anyone disagree?