How to compile calls assigned to ghost variables?

[amaurremi]

Currently, Dafny produces compileable output for method calls that are assigned to ghost variables. A Dafny statement ghost var x := methodCall() will be compiled to an invocation of methodCall in the target language (the ghost variable will not be compiled).

Compiling methodCall and not merely ignoring it is necessary if the method has a side effect; but pure methods are compiled, too, when assigned to ghost variables.

Would it make sense to issue a warning for assignment statements that have ghost on the left-, and non-ghost method calls on the right-hand side?

For instance, in the following code:

method foo() returns (r: int) {
  // some expensive computation
}

method Main() {
  ghost var x := foo();
  var y := foo();
}

the user might mistakenly think that the first call to foo would be ignored by the compiler, but the second call would be compiled. By contrast, the compiler will produce two calls to foo.

[MikaelMayer]

Since the following could be ambiguous (is the var ghost or the entire sentence)

ghost var x := foo()

I think warnings should be issued too, depending on the context, of the form

 Warning: Method result assignment to a ghost variable.
   The method has side effects and will be computed at compile-time.
   To remove this warning, remove the ambiguity and accept this behavior,
   prefix the method call with prefix like ghost var x := compiled foo();
   
 Warning: Method result assignment to a ghost variable.
   The method does not have side effects but will be computed at compile-time by default.
   To ensure the method is not computed, prefix the call with 'ghost', such as var x := ghost foo();

[keyboardDrummer]

Would it always be possible to resolve the warnings you propose? I'm not sure I'm in favour of unresolvable warnings, since I don't know how a programmer would effectively use those. If you have unresolvable warnings then over time the list of warnings will grow and a programmer may end up ignoring all of them.

As an alternative to a warning, using the IDE to render which expressions are erased at runtime could help as well. There's an issue for that feature here.

[MikaelMayer]

Good question. For both warnings, the answer is yes. To get rid of the warning (and of the ambiguity by the same occasion), programmers would have to write either, explicitly:

• var x := ghost foo() "I really meant it, I don't want foo() to be run at compile time",-- this is the simplified version of ghost var x := ghost foo()
• ghost var x := compiled foo() "I am effectively discarding the result at compile-time, but I do want it to be computed".