Havoc assignment vs {:external} result vs auto-init'ed vars

[hmijail]

Dafny version

4.0.0

Code to produce this issue

// I have this verification-only code that seems to behave as I expect it to:
method {:external} myHavoc<T>() returns (res:T)
trait myTrait {
    var bar: int;
}
method myMethod(m: myTrait) returns (b:bool) { return true; }
method mainExternal(){
    var t: myTrait := myHavoc();
    var r:= myMethod(t);
}

//This is very concise and convenient (no need to define a class with the trait, instantiating it, etc).
//However it feels like I'm using some undocumented behavior, even if verification seems to work great.
//So my first question is: is this a correct way to do this? Is there a better way?

//My guess is that Dafny's havoc assignment would be a more legal way, but it balks at the direct usage of the trait:
method mainHavoc(){
    var t: myTrait := *;
    var r:= myMethod(t);    //FAILS: variable 't', which is subject to definite-assignment rules, might be uninitialized here
}
// is this a bug?

//Instantiating a class helps, though it seems to trigger a parser bug.
class boilerplate extends myTrait {
    constructor ctor(b: int) {
        bar := b;
    }
}
method mainClassConstructor(){
    //var b := new boilerplate.ctor(*);   //FAILS: "closeparen expected"
    var i : int := *;
    var b2:= new boilerplate.ctor(i);   //works
    var r:= myMethod(b2);
}
//is this a bug?

//I notice I can just instantiate the class and leave it auto-init'ed:
class boilerplate2 extends myTrait {}
method mainClassAutoinit(){
    var b := new boilerplate2;
    var r:= myMethod(b);
}
// The discussion in the Reference Manual about definite assignment and auto-init types sounds like instantiating an auto-inited class should be equivalent to havoc-assigning its fields, at least as far as the verifier is concerned - which is my case. Is that right?

// Finally, and related to these: how can I declare a class or datatype to be auto-inited? Is it just about recursively making all the fields also auto-inited?

Command to run and resulting output

Just paste into vscode.

What happened?

Repeating here for convenience the questions in the code :

1. Is mainExternal() supported Dafny code, or better use another way?
2. Is mainHavoc() definite-assignment failure a bug?
3. Is mainClassConstructor() closeparen failure a bug?
4. Is mainClassAutoinit()'s usage of an implicit constructor equivalent to a havoc assignment?
5. How to declare a class/datatype to be auto-init'ed? Or is it implicit depending on its fields/params being also auto-init?

What type of operating system are you experiencing the problem on?

Mac

[hmijail]

Another case where havoc assignment causes trouble is when a datatype is built with a trait or class.
I started thinking this might be because they're reference types, but arrays (even arrays of traits!) are accepted.

datatype dt1 = dt1(a: int)
datatype dt2 = dt2(a: int, b: boilerplate)
datatype dt3 = dt3(a: int, b: array<myTrait>)
method myOtherMethod<T>(d: T) returns (b:bool) { return true; }

method main(){
    var d1: dt1 := *;
    var r:= myOtherMethod(d1);  //OK

    var d2: dt2 := *;
    var r2:= myOtherMethod(d2); //FAILS: variable 'd2', which is subject to definite-assignment rules, might be uninitialized here


    var d3: dt3 := *;
    var r3:= myOtherMethod(d3);  //OK
}

[hmijail]

Would it be helpful if I break this issue down into smaller issues?
I created this issue like this because the 5 listed questions seem connected, but if needed I can try to separate them.

[keyboardDrummer]

Would it be helpful if I break this issue down into smaller issues?
I created this issue like this because the 5 listed questions seem connected, but if needed I can try to separate them.

No, this is fine. Sorry for the slow response. I will try to improve our processes so we're faster next time :-)

method {:external} myHavoc<T>() returns (res:T)
trait myTrait {
    var bar: int;
}
method myMethod(m: myTrait) returns (b:bool) { return true; }
method mainExternal(){
    var t: myTrait := myHavoc();
    var r:= myMethod(t);
}

This seems fine, although you don't need the {:external} attribute here. That is only required when integrating with external code.

//My guess is that Dafny's havoc assignment would be a more legal way, but it balks at the direct usage of the trait:
method mainHavoc(){
    var t: myTrait := *;
    var r:= myMethod(t);    //FAILS: variable 't', which is subject to definite-assignment rules, might be uninitialized here
}

I created a ticket to improve our error reporting, that should explain what's going on here: #5362

method mainClassConstructor(){
    //var b := new boilerplate.ctor(*);   //FAILS: "closeparen expected"
    var i : int := *;
    var b2:= new boilerplate.ctor(i);   //works
    var r:= myMethod(b2);
}

I believe the syntax error there is expected, since havoc assignment is a statement, not an expression. I could create a ticket to improve the parser's error reporting, but that's quite far down the line for us, so I'll let this be for now.

Do you have any remaining questions?

[hmijail]

Thank you. Yes, there were 2 remaining questions:

• The discussion in the Reference Manual about definite assignment and auto-init types sounds like instantiating an auto-inited class should be equivalent to havoc-assigning its fields, at least as far as the verifier is concerned. Is that right?
• How can I declare a class or datatype to be auto-inited? Is it enough to recursively make all the fields auto-inited?