Type resolve /check error when dealing with values (the placement in the class file matters)

[lausdahl]

During the development vdm2c generator we discovered that AVariableExp's some times gets a vardef of type VariableDefinition and some times of UntypedDefinition. The same applies to the type AIntType or AUnknownType.

The following three models all work as intended:

class ExpressionSetRange

values
val1 = 1;
val2 = 2;
VAL2 = 2;

functions

setRange: () -> bool
setRange()== card {val1, ... ,2} = 2;

seqSetRange : ()->bool
seqSetRange()==len [0 | i in set {val1,...,2}] =2;

seqSetRange2 : ()->bool
seqSetRange2()==len [0 | i in set {val1,...,val2}] =2;

instance variables
private inst1: seq of real := [0 | i in set {val1,...,VAL2}];

end ExpressionSetRange

and

class ExpressionSetRange

values
val1:int = 1;
val2:int = 2;
VAL2:int = 2;

functions

setRange: () -> bool
setRange()== card {val1, ... ,2} = 2;

seqSetRange : ()->bool
seqSetRange()==len [0 | i in set {val1,...,2}] =2;

seqSetRange2 : ()->bool
seqSetRange2()==len [0 | i in set {val1,...,val2}] =2;

instance variables
private inst1: seq of real := [0 | i in set {val1,...,VAL2}];

end ExpressionSetRange

and

class ExpressionSetRange
functions

setRange: () -> bool
setRange()== card {val1, ... ,2} = 2;

seqSetRange : ()->bool
seqSetRange()==len [0 | i in set {val1,...,2}] =2;

seqSetRange2 : ()->bool
seqSetRange2()==len [0 | i in set {val1,...,val2}] =2;

instance variables
private inst1: seq of real := [0 | i in set {val1,...,VAL2}];

values
val1:int = 1;
val2:int = 2;
VAL2:int = 2;

end ExpressionSetRange

However, this model here does not work as indented all references (AVariableExps) becomes AUnknownType and AUntypedDefinition

class ExpressionSetRange
functions

setRange: () -> bool
setRange()== card {val1, ... ,2} = 2;

seqSetRange : ()->bool
seqSetRange()==len [0 | i in set {val1,...,2}] =2;

seqSetRange2 : ()->bool
seqSetRange2()==len [0 | i in set {val1,...,val2}] =2;

instance variables
private inst1: seq of real := [0 | i in set {val1,...,VAL2}];

values
val1 = 1;
val2 = 2;
VAL2 = 2;

end ExpressionSetRange

[nickbattle]

Can you tell us how this problem shows itself? The spec that fails does seem to operate correctly (I tried with the Overture-2.3.0.jar), but it's possible that the type information in the the AST is wrong. Is that what you mean? Is there a way to see this other than looking in a debugger? :)

@peterwvj, do these specs code generate differently for you?

[nickbattle]

I've looked at the AST for setRange, and the val1 in the set range expression, but it's coming up with a ANatOneNumericbaseType and an ALocalDefinition, which is what I would expect.

Maybe I don't understand the issue?

[peterwvj]

Considering the last spec, which allegedly is causing problems for the type checker, the code generator seems to work. I should say that I had to comment out the instance variable, because the Java code generator only supports comprehensions inside functions and operations.

The code compiles as well. I'm pretty sure the code generator would try to narrow the arguments passed to the set range operator if the argument was considered to be of type "unknown".

So to me it looks fine.

....
@SuppressWarnings("all")
public class ExpressionSetRange {
    private static final Number val1 = 1L;
    private static final Number val2 = 2L;
    private static final Number VAL2 = 2L;

    /* M.vdmpp 1:7 */
    public ExpressionSetRange() {
    }

    /* M.vdmpp 4:1 */
    private static Boolean setRange() {
        /* M.vdmpp 5:34 */
        return Utils.equals(SetUtil.range(ExpressionSetRange.val1, 2L).size(),
            2L);
    }

    /* M.vdmpp 7:1 */
    private static Boolean seqSetRange() {
        VDMSeq seqCompResult_1 = SeqUtil.seq();

        /* M.vdmpp 8:34 */
        VDMSet set_1 = SetUtil.range(ExpressionSetRange.val1, 2L);

        for (Iterator iterator_1 = set_1.iterator(); iterator_1.hasNext();) {
            Number i = ((Number) iterator_1.next());
            seqCompResult_1.add(0L);
        }

        /* M.vdmpp 8:48 */
        return Utils.equals(seqCompResult_1.size(), 2L);
    }

    /* M.vdmpp 10:1 */
    private static Boolean seqSetRange2() {
        VDMSeq seqCompResult_2 = SeqUtil.seq();

        /* M.vdmpp 11:35 */
        VDMSet set_2 = SetUtil.range(ExpressionSetRange.val1,
                ExpressionSetRange.val2);

        for (Iterator iterator_2 = set_2.iterator(); iterator_2.hasNext();) {
            Number i = ((Number) iterator_2.next());
            seqCompResult_2.add(0L);
        }

        /* M.vdmpp 11:52 */
        return Utils.equals(seqCompResult_2.size(), 2L);
    }

    public String toString() {
        return "ExpressionSetRange{" + "val1 = " + Utils.toString(val1) +
        ", val2 = " + Utils.toString(val2) + ", VAL2 = " +
        Utils.toString(VAL2) + "}";
    }
}

[lausdahl]

Hi @nickbattle

Look at this:

and for the untyped stuff:

The thing that happens here is that the instance variable is checked before the values are resolved / checked and thus gets the initial unknown type. Then later the values are corrected but then the instance variable setrange is already done.

For some reason the type checker behaves correctly event with this issue, it can detect that the values used in the set range expression are integers even through the information it stored in the nodes are clearly not correct. So maybe it checks in one way and records the type and definitions in another way.

The screenshots are made by placing a breakpoint in the end of TypeCheckerExpVisitor.caseASetRangeSetExp

[peterwvj]

I can confirm this. Kenneth and I can produce this on my machine too.