ArgumentNullException in Translator.CheckDefiniteAssignment

[xtrm0]

repro:

function Succ(x: int): int
{
  x + 1
}

function FailingLemma(): nat
{
  var st : set<int> :| forall x | x in st :: Succ(x) > 0;
  assert true by {
    if x: nat :| Succ(x) > 1 {
      assert Succ(x) > 0;
    }
  }
  0
}

output:

$ dafny /version
Dafny 3.6.0.40511
$ dafny repro.dfy 
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.Dictionary`2.FindValue(TKey key)
   at System.Collections.Generic.Dictionary`2.TryGetValue(TKey key, TValue& value)
   at Microsoft.Dafny.Translator.CheckDefiniteAssignment(IdentifierExpr expr, BoogieStmtListBuilder builder)
   at Microsoft.Dafny.Translator.CheckWellformedWithResult(Expression expr, WFOptions options, Expr result, Type resultType, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.CheckWellformed(Expression expr, WFOptions options, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.CheckWellformedWithResult(Expression expr, WFOptions options, Expr result, Type resultType, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.CheckWellformed(Expression expr, WFOptions options, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.CheckWellformedWithResult(Expression expr, WFOptions options, Expr result, Type resultType, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.CheckWellformed(Expression expr, WFOptions options, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.TrStmt_CheckWellformed(Expression expr, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran, Boolean subsumption, Boolean lValueContext)
   at Microsoft.Dafny.Translator.TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.TrStmtList(List`1 stmts, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.TrStmt2StmtList(BoogieStmtListBuilder builder, Statement block, List`1 locals, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.TrIfStmt(IfStmt stmt, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.TrStmtList(List`1 stmts, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.CheckWellformedWithResult(Expression expr, WFOptions options, Expr result, Type resultType, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.CheckWellformedLetExprWithResult(LetExpr e, WFOptions options, Expr result, Type resultType, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, Boolean checkRhs)
   at Microsoft.Dafny.Translator.CheckWellformedWithResult(Expression expr, WFOptions options, Expr result, Type resultType, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.AddWellformednessCheck(Function f)
   at Microsoft.Dafny.Translator.AddFunction_Top(Function f, Boolean includeAllMethods)
   at Microsoft.Dafny.Translator.AddClassMembers(TopLevelDeclWithMembers c, Boolean includeAllMethods)
   at Microsoft.Dafny.Translator.AddTypeDecl(RevealableTypeDecl d)
   at Microsoft.Dafny.Translator.DoTranslation(Program p, ModuleDefinition forModule)
   at Microsoft.Dafny.Translator.Translate(Program p, ErrorReporter reporter, TranslatorFlags flags)+MoveNext()
   at Microsoft.Dafny.DafnyDriver.Translate(ExecutionEngineOptions options, Program dafnyProgram)+MoveNext()
   at System.Collections.Generic.List`1..ctor(IEnumerable`1 collection)
   at System.Linq.Enumerable.ToList[TSource](IEnumerable`1 source)
   at Microsoft.Dafny.DafnyDriver.ProcessFiles(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId)
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
   at System.Threading.Tasks.Task`1.GetResultCore(Boolean waitCompletionNotification)
   at System.Threading.Tasks.Task`1.get_Result()
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args)
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass6_0.<Main>b__0()
   at System.Threading.Thread.StartCallback()
Aborted

Related to #2264, this was the kind of exception I was getting that led me to #2264

[xtrm0]

This only happens inside functions, if it's inside a lemma, we get the same error as in #2264

[xtrm0]

My temporary solution for this is to manually expand:

if x :| prop(x) {
 ///...A...
}

Into:

if exist x :: prop(x) {
 var x :| prop(x);
 ///...A...
}

[atomb]

Internally, what's going on here is that the reference to x in assert Succ(x) > 0 doesn't have a UniqueName assigned yet so it's impossible to look it up in the definite assignment tracker. I haven't yet tracked down which piece of code should be (but isn't) assigning it a unique name yet, though.

I wonder whether @RustanLeino or @cpitclaudel have thoughts.

[atomb]

I think this could use attention from someone familiar with the resolver code, so I'm unassigning myself for now.

[jtristan]

Modified example, simpler and closer to actual AST:

module DefaultModule {
  class DefaultClass {
    static function BrokenFunction(): nat {
      var y := 0;
			assert true by {
        if x: bool :| true {
          assert x;
        }
      }
      0
    }
  }
}

[robin-aws]

Hi @jtristan! FYI I edited your snippet to add dafny as the language (```dafny ... ```). I enjoy the syntax highlighting so much I can't resist spreading the word that it works. :)

[jtristan]

Additional information. The error is introduced during the verifier's translation. Checking that the let expression is well-formed triggers a variable substitution in the body of the let. The substitution appears to be erroneous when the body contains an if statement whose guard contains an existential. Indeed, in function Substitute, in the case where the expression is an existential expression, the substitution is forced when calling CreateBoundVarSubstitutions. However, this substitution is not forced in the body of the if statement. As a result, only one occurrence of the variable is substituted. I do not know yet what is the right way to fix this problem, but at least, not forcing the substitution leads to a successful translation, for this specific program. The key file is Substituter.cs, the function is Substitute, and the case is expr is ComprehensionExpr.

[RustanLeino]

The AST node for a "binding if statement" is an if statement where .IsBindingGuard is true and .Guard is an ExistsExpr (with .Range == null says the ObjectInvariant() in IfStmt). Since a binding if needs the same kind of machinery as an exists expression, it was convenient to represent the AST in this way (if I recall correctly).

As you correctly noticed, @jtristan, the substituter should not generate a new bound variable for the bound variable that's part of the .Guard, because the bound variable that sits inside that ExistsExpr has a scope that goes beyond the body of the ExistsExpr (again, the reason for this was just because it was convenient to put package up what the binding if needed inside an ExistsExpr).

A good fix, thus, seems to be the following. Extract the ComprehensionExpr case from the Substitute method (into a method SubstituteComprehensionExpr, say) and parameterize SubstituteComprehensionExpr with a forceSubstituteOfBoundVars parameter. Then, in IfStmt case in SubstStmt, if s.IsBindingGuard is true, then dissect the .Guard (which will be an ExistsExpr) and call SubstituteComprehensionExpr directly.

While you're at it, please also fix any binding case of an if-case statement, which suffers from the same problem. Here is a test case:

function AnotherBrokenFunction(): nat {
  var y := 0;
  assert true by {
    if
    case x: bool :| true =>
      assert x;
  }
  0
}

[jtristan]

OK, I think it makes sense, will do. Thanks for the suggestion.

[jtristan]

Building on Rustan's suggested solution, for the record, there are at least two issues to watch for:

1. The binding guard could be a split quantifier, and we want to avoid doing substitution of the guard bound variable on these as well
2. In function SubstituteComprehensionExpr it is possible to have no substitution, yet, we might need to return the expression and not Null. However, perhaps, the proper solution is to return Null in such a case?