Regression: dafny run not working with include

[davidcok]

Dafny version

4.1.0

Code to produce this issue

test.dfy:
include "main.dfy"

method Main() {
  var undertest := new TestLogic''TopLevel();
  print "COMPLETED OK\n";
}

main.dfy:
class TestLogic''TopLevel {
  constructor () 
  {
  }
}

Command to run and resulting output

dafny run --no-verify test.dfy

test.dfy(4,19): Error: call to undeclared procedure: Call$$_module.TestLogic_k_kTopLevel.__ctor
1 name resolution errors detected in /var/folders/89/bc5ryf6x55l_pm4w3347kd200000gn/T/test__module.bpl

*** Encountered internal translation error - re-running Boogie to get better debug information

/var/folders/89/bc5ryf6x55l_pm4w3347kd200000gn/T/test__module.bpl(2882,4): Error: call to undeclared procedure: Call$$_module.TestLogic_k_kTopLevel.__ctor
1 name resolution errors detected in /var/folders/89/bc5ryf6x55l_pm4w3347kd200000gn/

What happened?

1. It does not work as it should
2. Why is there any reference to bpl files at all? No verification is called for.
3. It works fine if the files are combined into one file, without using include.

4!!!) If one includes the option --verify-included-files, enven though one also has --no-verify, then it works.

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

Mac

[robin-aws]

Tagging as release blocker to be conservative, if indeed a regression.

[MikaelMayer]

This issue was first introduced by the PR #4059 after bisecting. @keyboardDrummer before I dive into it, would you know what in your PR caused that trouble?

[keyboardDrummer]

The translation code decides what to skip translation for based on whether it was included or not, and apparently it's skipping things too aggressively here causing the translated code from the including file to have a reference to something that wasn't translated. I guess the bug starts in Translator.InVerificationScope(Declaration d) or Translator.ShouldVerifyModule(..)

--no-verify apparently doesn't prevent translation from happening so that's not significant to this.

[MikaelMayer]

Ok, after investigation, here is what I found so far.
Since #4059, translation happens in this order

Before #4059, translation happened in this order:

So before, it was translating the main module, and then adding "_ctor" as a referenced method.
Then it proceeded to translate the class and, because _ctor was referenced, it would adds it procedure.

After, it would translate the class first, and because _ctor is not referenced yet and out of scope, it would not add it to the translation. Then it proceeded to translate _default and adds a reference to the _ctor method, but it's too late.
I'll look into why that happens.