[nem-bug] [Nemerle 0000703]: [0.9.3] Immutable fields are not marked with initonly

[feedback at nemerle.org]

The following issue has been RESOLVED.
======================================================================
<http://nemerle.org/bugs/view.php?id=703> 
======================================================================
Reported By:                Snaury
Assigned To:                nazgul
======================================================================
Project:                    Nemerle
Issue ID:                   703
Category:                   Compiler
Reproducibility:            always
Severity:                   major
Priority:                   normal
Status:                     resolved
Resolution:                 fixed
Fixed in Version:           
======================================================================
Date Submitted:             07-01-2006 19:10 CEST
Last Modified:              07-06-2006 23:10 CEST
======================================================================
Summary:                    [0.9.3] Immutable fields are not marked with
initonly
Description: 
This allows the following code:

using Nemerle.Collections;

public class Program
{
  public static void Main()
  {
    RList<int>.Empty = null;
  }
}

to run successfully, which might lead (theoretically) to hard to trace
bugs later. In contrary, in C#, the following declarations:

  public static readonly object Field = new System.Object();
  public readonly object InstanceField = new System.Object();

are marked with initonly:

  .field public static initonly object Field
  .field public initonly object InstanceField

which prevents field modifications by any .NET code, not only Nemerle.
======================================================================

----------------------------------------------------------------------
 nazgul - 07-02-06 13:55 
----------------------------------------------------------------------
The problem with initonly is when such field gets into closure created
inside the constructor:

class A {
  foo : int;

  public this () {
    def bar (x)  {
      foo = x;
    }
    if (waz)
      bar (1);
    else
      bar (2);
  }
}

This code is valid, but does not verify when 'foo' is marked initonly.
Though in my opinion we should just disallow such code, especially that
here you can really store bar function somewhere and using it violates the
immutability of field.

----------------------------------------------------------------------
 malekith - 07-05-06 20:13 
----------------------------------------------------------------------
What about:

y : int;

public this() {
  while (y < 10) {
    y++;
  }
}

because syntactically y is also inside a local function here.

We can check if the function is inlined, but this doesn't seem like a
user-friendly rule. OTOH we use it for goto's (like block returns and the
like) already anyway...

----------------------------------------------------------------------
 nazgul - 07-06-06 01:21 
----------------------------------------------------------------------
I almost have the patch to forbid the closurising of assigned immutable
fields (it performs a check in Typer4). Currently it fails only on an ugly
hack used in list comprehensions to assign to Cons.tl

I guess we should use macro attribute [CompilerMutable] to mark fields,
which are immutable from user code, but compiler (or macro) can override
this behaviour in some specific scenarios.

I wonder if runtime does additional optimizations for initonly fields.
Also, maybe  Spec# / boogie require that some fields are marked initonly
to yield better results?

----------------------------------------------------------------------
 malekith - 07-06-06 06:58 
----------------------------------------------------------------------
I think boogie makes use of it. Specifically "public initonly" is much
different verification-wise from "public mutable".

----------------------------------------------------------------------
 nazgul - 07-06-06 23:10 
----------------------------------------------------------------------
Fixed on trunk (r6432).

Issue History
Date Modified  Username       Field                    Change              
======================================================================
07-01-06 19:10 Snaury         New Issue                                    
07-01-06 20:02 Snaury         File Added: bug-initonly.patch                    
07-02-06 13:55 nazgul         Note Added: 0001338                          
07-05-06 20:13 malekith       Note Added: 0001349                          
07-06-06 01:21 nazgul         Note Added: 0001350                          
07-06-06 06:58 malekith       Note Added: 0001351                          
07-06-06 23:10 nazgul         Status                   new => resolved     
07-06-06 23:10 nazgul         Resolution               open => fixed       
07-06-06 23:10 nazgul         Assigned To               => nazgul          
07-06-06 23:10 nazgul         Note Added: 0001352                          
======================================================================