Assignment after break in match causes crash error

[Dilan-s]

Dafny version

4.1.0.0

Code to produce this issue

method Main() returns ()
{
  var v_int_32: int := 0;
  while (v_int_32 < 13)
  {
    v_int_32 := (v_int_32 + 1);

    match 12.04 {
      case _ => {
        break;
        var v_int_75: int := 13;
      }
    }
  }
}

Command to run and resulting output

$ dafny /compile:4 test.dfy
Unhandled exception. System.AggregateException: One or more errors occurred. (Value cannot be null. (Parameter 'key'))
...
   at Dafny.Dafny.Main(String[] args) in /home/dilan/dafny/Source/Dafny/Dafny.cs:line 7
Aborted (core dumped)

What happened?

Compiling the program with the compiler caused a crash error.

Full error message

Unhandled exception. System.AggregateException: One or more errors occurred. (Value cannot be null. (Parameter 'key'))
---> System.ArgumentNullException: Value cannot be null. (Parameter 'key')
at System.Collections.Generic.Dictionary2.FindValue(TKey key) at System.Collections.Generic.Dictionary2.TryGetValue(TKey key, TValue& value)
at Microsoft.Dafny.BoogieGenerator.CheckDefiniteAssignment(IdentifierExpr expr, BoogieStmtListBuilder builder) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs:line 165
at Microsoft.Dafny.BoogieGenerator.CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Expr result, Type resultType, List1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, String resultDescription) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs:line 300 at Microsoft.Dafny.BoogieGenerator.CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Expr result, Type resultType, List1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, String resultDescription) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs:line 1210
at Microsoft.Dafny.BoogieGenerator.CheckWellformed(Expression expr, WFOptions options, List1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs:line 254 at Microsoft.Dafny.BoogieGenerator.TrStmt_CheckWellformed(Expression expr, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran, Boolean subsumption, Boolean lValueContext) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 2818
at Microsoft.Dafny.BoogieGenerator.TrAssignmentRhs(IToken tok, IdentifierExpr bGivenLhs, IVariable lhsVar, Type lhsType, AssignmentRhs rhs, Type rhsTypeConstraint, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran, Statement stmt) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 2580 at Microsoft.Dafny.BoogieGenerator.ProcessRhss(List1 lhsBuilder, List1 bLhss, List1 lhss, List1 rhss, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran, Statement stmt) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 2232
at Microsoft.Dafny.BoogieGenerator.TrAssignment(Statement stmt, Expression lhs, AssignmentRhs rhs, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 1147 at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 256
at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 221 at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 484
at Microsoft.Dafny.BoogieGenerator.TrStmtList(List1 stmts, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 2786
at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 305 at Microsoft.Dafny.BoogieGenerator.TrStmtList(List1 stmts, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 2786 at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 305
at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 431 at Microsoft.Dafny.BoogieGenerator.TrStmtList(List1 stmts, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 2786 at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 305
at Microsoft.Dafny.BoogieGenerator.<>c__DisplayClass436_0.b__0(BoogieStmtListBuilder bld, ExpressionTranslator e) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 993
at Microsoft.Dafny.BoogieGenerator.TrLoop(LoopStmt s, Expression Guard, BodyTranslator bodyTr, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran, Expr freeInvariant, Boolean includeTerminationCheck) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 1551 at Microsoft.Dafny.BoogieGenerator.TrWhileStmt(WhileStmt stmt, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 998
at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 318 at Microsoft.Dafny.BoogieGenerator.TrStmtList(List1 stmts, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 2786 at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List1 locals, ExpressionTranslator etran) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs:line 305
at Microsoft.Dafny.BoogieGenerator.AddMethodImpl(Method m, Procedure proc, Boolean wellformednessProc) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs:line 667
at Microsoft.Dafny.BoogieGenerator.AddMethod_Top(Method m, Boolean isByMethod, Boolean includeAllMethods) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs:line 209
at Microsoft.Dafny.BoogieGenerator.AddClassMembers(TopLevelDeclWithMembers c, Boolean includeAllMethods, Boolean includeInformationAboutType) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs:line 79
at Microsoft.Dafny.BoogieGenerator.AddRevealableTypeDecl(RevealableTypeDecl d) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs:line 879
at Microsoft.Dafny.BoogieGenerator.DoTranslation(Program p, ModuleDefinition forModule) in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.cs:line 821
at Microsoft.Dafny.BoogieGenerator.Translate(Program p, ErrorReporter reporter, TranslatorFlags flags)+MoveNext() in /home/dilan/dafny/Source/DafnyCore/Verifier/BoogieGenerator.cs:line 893
at Microsoft.Dafny.CompilerDriver.Translate(ExecutionEngineOptions options, Program dafnyProgram)+MoveNext() in /home/dilan/dafny/Source/DafnyDriver/CompilerDriver.cs:line 224
at System.Collections.Generic.List1..ctor(IEnumerable1 collection)
at System.Linq.Enumerable.ToList[TSource](IEnumerable1 source) at Microsoft.Dafny.CompilerDriver.<>c__DisplayClass4_0.<ProcessFilesAsync>b__0() in /home/dilan/dafny/Source/DafnyDriver/CompilerDriver.cs:line 153 at System.Threading.Tasks.Task1.InnerInvoke()
at System.Threading.Tasks.Task.<>c.<.cctor>b__272_0(Object obj)
at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
--- End of stack trace from previous location ---
at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)
--- End of stack trace from previous location ---
at Microsoft.Dafny.CompilerDriver.ProcessFilesAsync(IReadOnlyList1 dafnyFiles, ReadOnlyCollection1 otherFileNames, DafnyOptions options, ProofDependencyManager depManager, Boolean lookForSnapshots, String programId) in /home/dilan/dafny/Source/DafnyDriver/CompilerDriver.cs:line 152
at Microsoft.Dafny.CompilerDriver.RunCompiler(DafnyOptions options) in /home/dilan/dafny/Source/DafnyDriver/CompilerDriver.cs:line 68
at Microsoft.Dafny.DafnyCli.<>c.<b__4_0>d.MoveNext() in /home/dilan/dafny/Source/DafnyDriver/Commands/DafnyCli.cs:line 59
--- End of stack trace from previous location ---
at Microsoft.Dafny.DafnyCli.Execute(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, String[] arguments, Func2 onLegacyArguments) in /home/dilan/dafny/Source/DafnyDriver/Commands/DafnyCli.cs:line 216 --- End of inner exception stack trace --- at System.Threading.Tasks.Task1.GetResultCore(Boolean waitCompletionNotification)
at System.Threading.Tasks.Task`1.get_Result()
at Microsoft.Dafny.DafnyCli.MainWithWriters(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, String[] args) in /home/dilan/dafny/Source/DafnyDriver/Commands/DafnyCli.cs:line 47
at Microsoft.Dafny.DafnyCli.Main(String[] args) in /home/dilan/dafny/Source/DafnyDriver/Commands/DafnyCli.cs:line 35
at Dafny.Dafny.Main(String[] args) in /home/dilan/dafny/Source/Dafny/Dafny.cs:line 7

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

Linux

[fabiomadge]

I can't reproduce this on either 4.1.0 or master on my Mac. Any ideas beyond trying out Linux?

[Dilan-s]

Strong neither can I, I will reopen the ticket as soon as I am able to, Apologies about this

[Dilan-s]

class C_2 {
  var F_C_2_real_1: real
  var F_C_2_real_2: real
  var F_C_2_real_3: real
  var F_C_2_bool_4: bool
  var F_C_2_real_5: real
  var F_C_2_bool_6: bool
  constructor (F_C_2_real_1: real, F_C_2_real_2: real, F_C_2_real_3: real, F_C_2_bool_4: bool, F_C_2_real_5: real, F_C_2_bool_6: bool) {
    this.F_C_2_real_1 := F_C_2_real_1;
    this.F_C_2_real_2 := F_C_2_real_2;
    this.F_C_2_real_3 := F_C_2_real_3;
    this.F_C_2_bool_4 := F_C_2_bool_4;
    this.F_C_2_real_5 := F_C_2_real_5;
    this.F_C_2_bool_6 := F_C_2_bool_6;
  }
}

method Main() returns ()
{
  var v_int_7: int := 0;
  var v_int_8: int := 1;
  while (v_int_7 < v_int_8)
  {
    v_int_7 := (v_int_7 + 1);
    var v_C_2_1: C_2 := new C_2(-20.01, -22.48, -8.26, false, -5.90, false);
    match 0 {
      case _ => {
        if false {
          continue;
        } else {
          var v_C_2_8: C_2 := new C_2(-28.38, -28.94, 9.05, (2) is int, 0.35, v_C_2_1.F_C_2_bool_6);
        }
      }
    }
  }
}

Reopening as I've been able to reproduce with the code above @fabiomadge

[Dilan-s]

Above code run using the setup:

$ Dafny /version
dafny 4.4.0.0

$ git log
commit 2c39c525c09d092575228e35b30c3470744a0f17 (HEAD -> master, origin/master, origin/HEAD)