[Oberon] Serious type loophole in type case statements and a possible fix

[Andreas Pirklbauer]

Several people have asked (via email) why the following restrictions 

    1. The case variable must be either a local variable or value parameter of
       pointer type (pointing to a record) or a variable parameter of record type.

    2. Assignments to the case variable are not allowed in the statements Si.
       However, individual elements (record fields) of case variables may be modified.

    3. A case variable of pointer type cannot be passed as a variable parameter to a procedure.

have been proposed for the type case statement (=WITH statement in original Oberon-2)

   CASE p OF
     T1: S1 |
     T2: S2
   END ;

By design, this choice makes it *impossible* to alter a case variable p of a type case statement
within the scope of the CASE p OF … END block, and there cannot ever be any type loopholes.
 
See references [1] and [2] and the example in the appendix below.

It has been noted that this choice stands in contrast with e.g. the "Oakwood guidelines for Oberon-2",

    http://www.edm2.com/index.php/The_Oakwood_Guidelines_for_Oberon-2_Compiler_Developers

where it is possible to "alter a guarded pointer variable within the scope of a guarding WITH statement”.

* * *

The rationale for *not* adopting the Oakwood guidelines, but rather choosing the
more restrictive approach outlined above was the following:

a. If one allowed changing the case variable p of a type case statement *within* the scope
   of the case statement block, then the compiler would have to insert additional hidden
   type guards p(T) in the statements of the case statement. This constitutes a “hidden
   mechanism”, which seems to be "against the spirit of Oberon”.

b. Inserting hidden type guards would also negatively impact performance. Of course, a
   sophisticated compiler may be able to “detect” (at least in some cases) whether a type
   guard is actually needed, but in general this is not possible (for example if a global
   variable is passed as a parameter to a procedure containing a type case statement).

c. In the entire Oberon system (I am referring to Project Oberon 2013), there is not a
   single module, where the above restrictions cause a problem. Not one. In other words,
   these restrictions are not “real” restrictions, but represent good programming style.

d. If one *really* wants to change the value or type of variable p, one can always use
   the construct of a type test (using IS) instead, and insert type tests explicitly. This is
   not a bad, but a good thing, as it trains the programmer to use *explicit* type guards
   when needed, while allowing him/her to omit them when they are not needed.

      IF p IS T1 THEN p(T1).x := ..
      ELSIF p IS T2 THEN p(T2).y := 
      END

-ap

References:

[1] https://github.com/andreaspirklbauer/Oberon-extended/blob/master/Documentation/The-Revised-Oberon2-Programming-Language.pdf

[2] https://github.com/andreaspirklbauer/Oberon-type-case-statement-without-loopholes

-----------------------------------------------------------------------------------------------

APPENDIX: Test program

MODULE TestTypeCase;  (*test type case statements with restrictions*)

  TYPE R0 = RECORD fld0: INTEGER END ;
    R1 = RECORD (R0) fld1: INTEGER END ;
    R2 = RECORD (R0) fld2: INTEGER END ;

    P0 = POINTER TO R0;
    P1 = POINTER TO R1;
    P2 = POINTER TO R2;

  VAR p0: P0; p1: P1; p2: P2;
    r0: R0; r1: R1; r2: R2;

  PROCEDURE AssignGlobal();
  BEGIN p0 := p2
  END AssignGlobal;

  PROCEDURE Proc1(p0: P0); BEGIN END Proc1;
  PROCEDURE Proc2(VAR p1: P1); BEGIN END Proc2;
  PROCEDURE Proc3(VAR r0: R0); BEGIN r0 := r2 (*projection*) END Proc3;
  PROCEDURE Proc4(r0: R0); BEGIN END Proc4;
  PROCEDURE Proc5(VAR i: INTEGER); BEGIN END Proc5;
  PROCEDURE Proc6(b: BOOLEAN); BEGIN END Proc6;

  PROCEDURE check0();
  BEGIN p0 := p1;
    CASE p0 OF  (*ERROR "invalid case variable" - global case variables are not allowed*)
      P1:
        AssignGlobal();  (*if p0 were allowed to be global, the dynamic type of p0 would be set to P2 here*)
        p0.fld1 := 123  (*and there would be a type violation here, as p0 is considered of type P1*)
    END
  END check0;

  PROCEDURE check1();
    VAR p, pa: P0;
  BEGIN p := p1;
    CASE p OF
      P1:
        pa := p;
        Proc1(p);
        Proc2(p);  (*ERROR "invalid parameter" - cannot pass a case variable of a pointer type as a VAR parameter*)
        Proc5(p.fld1);
        p := p2;  (*ERROR "invalid assignment"  - cannot modify a case variable through an assignment*)
        p.fld1 := 123;
        CASE p OF
          P1:
            p := p1;  (*ERROR "invalid assignment" - cannot modify a case variable through an assignment*)
            Proc1(p);
            Proc2(p)   (*ERROR "invalid parameter" - cannot pass a case variable of a pointer type as a VAR parameter*)
        END ;
        p := p1  (*ERROR "invalid assignment" - cannot modify a case variable through an assignment*)
    END
  END check1;

  PROCEDURE check2();
  BEGIN p0 := p1;
    IF p0 IS P1 THEN
      AssignGlobal();  (*the runtime type of p0 is not P1 anymore, but P2, after this statement*)
      p0(P1).fld1 := 123;  (*thereore, there (correctly) will be a type guard failure at runtime here*)
    END
  END check2;

  PROCEDURE check3(VAR r: R0);
    VAR rr: R1;
  BEGIN r := r1; (*projection of the fields of R1 onto the fiels of R0*)
    CASE r OF
      R1:
        rr := r;
        r := r1;  (*ERROR "invalid assignment" - cannot modify a case variable through an assignment*)
        Proc3(r);
        Proc4(r);
        r.fld1 := 234
    END
  END check3;

  PROCEDURE check4();
    VAR r: R1;
  BEGIN r := r1;
    CASE r OF  (*ERROR "invalid case variable" - a record must be a variable parameter*)
      R1: r.fld1 := 345
    END
  END check4;

  PROCEDURE check5(p: P0);
  BEGIN
    CASE p OF
      P1: Proc6(p IS P1)
    END
  END check5;

  PROCEDURE check6(VAR p: P0);
  BEGIN
    CASE p OF P1:  (*ERROR "invalid case variable" - a pointer must be either a local variable or a value parameter*)
      p0 := p2;
      p.fld1 := {4,1}
    END
  END check6;

  PROCEDURE Go*;
  BEGIN
    check0();
    check1();
    check2();
    check3(r0);
    check4();
    check5(p0);
    p0 := p1; check6(p0)
  END Go;

BEGIN NEW(p0); NEW(p1); NEW(p2)
END TestTypeCase.