Function methods only ever have one return path, which makes debugging harder

[cpitclaudel]

Consider these two equivalent programs:

function method fIncorrectInOneCase(x: int) : (y: int)
  ensures y > 0
{
  if (x < -3) then 5
  else if (x < 5) then -2
  else 4
}

method mIncorrectInOneCase(x: int) returns (y: int)
  ensures y > 0
{
  if (x < -3) { return 5; }
  else if (x < 5) { return -2; }
  else { return 4; }
}

Here's Dafny's output:

The error is correctly positioned in the method, but not in the function. This makes debugging function methods much less pleasant than methods.

Here's the textual output:

test.dfy(1,16): Error: A postcondition might not hold on this return path.
test.dfy(2,12): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
    (0,0): anon9_Else
    (0,0): anon10_Else
    (0,0): anon11_Then
    (0,0): anon8
test.dfy(13,20): Error: A postcondition might not hold on this return path.
test.dfy(10,12): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
    (0,0): anon5_Else
    (0,0): anon6_Then

Btw, what's up with line numbers in execution traces?

[robin-aws]

+1, I've seen this frequently irritate Dafny users (including myself!)

It also makes Boogie-level techniques for measuring verification cost like {:vcs_split_on_every_assert} less effective, since you can only measure the cost of the one post-condition assertion in the unified return block.

[MikaelMayer]

You nailed a very good problem. People like me prefer to write function methods because it's easier to reason about anyway, coming out of functional programming background. Moreover, it's possible to nest calls to function methods, whereas for methods it's only one method call at a time.
As you mention, the lack of debugging tool makes it hard to reason about when it fails.

[MikaelMayer]

I thought about this problem over the week-end, and here is maybe how we should tackle it.

When encountering a "return" statement in boogie, instead of translating literally the return expression, we should translate "if expressions", "let-var" and "match expressions" to their respective statements.
That way, it would work only for functions, but also for methods who return an expression.

[cpitclaudel]

When encountering a "return" statement in boogie,

In Boogie or in Dafny?

[MikaelMayer]

Actually, it looks like Boogie knows exactly the path in which a function's postcondition does not hold. It's in the trace. For example:

function test_function(x: bool): (r: int)
  ensures r == 2
 {
  if x then
    1
  else
    2
}

Boogie trace

function-implementation.bpl(2947,5): Error: A postcondition might not hold on th
is return path.
function-implementation.bpl(2910,3): Related location: This is the postcondition
 that might not hold.
Execution trace:
    function-implementation.bpl(2920,13): anon0
    function-implementation.bpl(2929,17): anon6_Else
    function-implementation.bpl(2933,13): anon7_Then
    function-implementation.bpl(2946,9): anon5

Boogie code:

2907:procedure CheckWellformed$$_module.__default.test__function(x#0: bool) returns (r#0: int);
2908:  free requires 0 == $FunctionContextHeight;
2909:  modifies $Heap, $Tick;
2910:  ensures r#0 == LitInt(2);
2911:
2912:
2913:
2914:implementation CheckWellformed$$_module.__default.test__function(x#0: bool) returns (r#0: int)
2915:{
2916:  var $_Frame: <beta>[ref,Field beta]bool;
2917:
2918:
2919:    // AddWellformednessCheck for function test_function
2920:    $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: 
2921:      $o != null && read($Heap, $o, alloc) ==> false);
2922:    if (*)
2923:    {
2924:        assume r#0 == LitInt(2);
2925:        assume false;
2926:    }
2927:    else
2928:    {
2929:        $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: 
2930:          $o != null && read($Heap, $o, alloc) ==> false);
2931:        if (x#0)
2932:        {
2933:            assume _module.__default.test__function(x#0) == LitInt(1);
2934:            assume true;
2935:            // CheckWellformedWithResult: any expression
2936:            assume $Is(_module.__default.test__function(x#0), TInt);
2937:        }
2938:        else
2939:        {
2940:            assume _module.__default.test__function(x#0) == LitInt(2);
2941:            assume true;
2942:            // CheckWellformedWithResult: any expression
2943:            assume $Is(_module.__default.test__function(x#0), TInt);
2944:        }
2945:
2946:        assume _module.__default.test__function(x#0) == r#0;
2947:    }
2948:}

See how in the trace it refers to the path 2933 which is the failing path. It looks like Dafny is not "catching" it properly

[cpitclaudel]

Good catch! Still pretty hard to map back since this is part of the trace but not the final element of it. Similar to this:

[MikaelMayer]

Indeed !
In both cases, since Boogie has more information, we should display nicer "related errors" messages.

[cpitclaudel]

In fact maybe this should be part of our improved UI: when we hover over an error we would show the trace that led to it.

[cpitclaudel]

But I still think that when a conditional is in tail position we should directly position the error on the failing branch(es)

[keyboardDrummer]

Although it is not mentioned in the release notes, this problem has been fixed in Dafny 4.8 by #5681