Re: [tlaplus] Re: PlusCal: implicit label Error (PlusCal translator bug?)

[Jaak Ristioja <jaak.r...@xxxxxxxx>]

On 01.12.2015 18:28, Leslie Lamport wrote:
> A goto to the "Error" label is supposed to be executed when execution
> reaches the end of a procedure without finding a return statement.  I
> suspect that in this case, the return is returning to someplace that
> drops it off the end of a calling procedure.  I can't tell exactly
> what's happening without seeing a complete example.  If you have an
> example in which such a goto is being executed when it shouldn't be,
> please send it to me.  (But please try to pare it down to the smallest
> example you can find.)

I've attached a minimum testcase to this email. It seems that a
workaround is to write

  if (cond) {
    call g();
  };
  return;

instead of simply:

  if (cond)
    call g();
  return;

> The translator does not produce an error because it doesn't know
> whether that goto "Error" can actually be executed.  Determining
> whether a particular statement in a program will be executed is an
> unsolvable problem, and we had more important things to do than add
> heuristics to the translator for attempting to solve this problem.

I agree, but I don't currently see why anybody would want to or should
be allowed to write PlusCal procedures which fall off the end. Can you
present an use-case for this? Wouldn't it just be better for the PlusCal
procedure to always return implicitly when it reaches the end of the
procedure block?


Best regards,
Jaak

-------------------------------- MODULE bug --------------------------------
EXTENDS Sequences

(* --algorithm bug {

procedure g() { return; }

procedure f() {
  if (FALSE)
    call g();
  return;
} 

{ call f(); } \* Single process

} *)

\* BEGIN TRANSLATION
VARIABLES pc, stack

vars == << pc, stack >>

Init == /\ stack = << >>
        /\ pc = "Lbl_3"

Lbl_1 == /\ pc = "Lbl_1"
         /\ pc' = Head(stack).pc
         /\ stack' = Tail(stack)

g == Lbl_1

Lbl_2 == /\ pc = "Lbl_2"
         /\ IF FALSE
               THEN /\ stack' = << [ procedure |->  "g",
                                     pc        |->  Head(stack).pc ] >>
                                 \o Tail(stack)
                    /\ pc' = "Lbl_1"
               ELSE /\ pc' = "Error"
                    /\ stack' = stack

f == Lbl_2

Lbl_3 == /\ pc = "Lbl_3"
         /\ stack' = << [ procedure |->  "f",
                          pc        |->  "Done" ] >>
                      \o stack
         /\ pc' = "Lbl_2"

Next == g \/ f \/ Lbl_3
           \/ (* Disjunct to prevent deadlock on termination *)
              (pc = "Done" /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION

=============================================================================