For function postcondition violations, point to the problematic expression branch

[keyboardDrummer]

Description

If the result of an expression does not satisfy the constraints of its context, then an error is reported in the branch of the expression that does not satisfy the context.

Effected contexts:

• Function postconditions
• Witness expressions
• Expression default values
• Subset type checks for function call arguments
• Assignment to a subset type local

Example of improved error reporting:

function ElseError(x: int): int // previous primary error location
  ensures ElseError(x) == 0 // related error location
{
  if x == 0 then
    0 
  else 
    1 // new primary error location
}
function ThenError(x: int): int // previous primary error location
  ensures ThenError(x) == 0 // related error location
{
  if x == 0 then
    1 // new primary error location
  else 
    0 
}

function CaseError(x: int): int // previous primary error location
  ensures CaseError(x) == 1 // related error location
{
  match x {
    case 0 => 1
    case 1 => 0 // new primary error location
    case _ => 1 
  }
}

function LetError(x: int): int // previous primary error location
  ensures LetError(x) == 1 // related error location
{
  var r := 3;
  r // new primary error location
}

How has this been tested?

• Added CLI test ast/functions/ensuresReporting.dfy
• ast/subsetTypes/errorReporting.dfy
• ast/expression/functionCall.dfy
• ast/statement/localAssignment.dfy

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[MikaelMayer]

I think it would match better C# idioms to write.

Suggested change

	var substMapPrime = SetupBoundVarsAsLocals(lhsVars, builder, locals, etran);
	var substMap2 = SetupBoundVarsAsLocals(lhsVars, builder, locals, etran);

The original code looks like written by someone who missed the substMap' notation Dafny offers 😁

[keyboardDrummer]

Really??? I don't think it improves anything. But sure I'll rename it.

[MikaelMayer]

For me it improves maintainability. At first when I looked at "substMapPrime" I was thinking of prime numbers, which had nothing to do with that. Then I looked everywhere to see what "prime" was referring to and I did not find that. Then I realized it could be a character encoding of the ' and it made sense. Just want to avoid future confusion.
We could also replace the "2" by something more self-explaining, like substMapLocalVars

[MikaelMayer]

Only two comments. Still a few check warnings in BoogieExtractor.cs line 190 as well.
Otherwise looks good.

[MikaelMayer]

Useful renaming.

[MikaelMayer]

Suggested change

	witnessExpr = decl.Constraint != null ? Substitute(decl.Constraint, decl.Var, decl.Witness) : null;
	witnessExpr = decl.Constraint != null ? Substitute(decl.Constraint, decl.Var, decl.Witness) : decl.Witness;

?

[MikaelMayer]

Same question as above. I'm surprised that witnessExpr can be null even if there is a witness given.

[keyboardDrummer]

I copied these changes from #5547. I'm afraid I don't understand them myself. @ssomayyajula do you?

[MikaelMayer]

Suggested change

	// var delayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, constraintCheckBuilder);
	// delayer.DoWithDelayedReadsChecks(false, wfo => {
	// CheckWellformedAndAssume(decl.Constraint, wfo, locals, constraintCheckBuilder, etran, "predicate subtype constraint");
	// });

[MikaelMayer]

All the warnings at the bottom that are unrelated to your PR will be fixed by #5694
Great job for making this to work.