Modeling uninitialized variables

[Paul Sandoz]

> On Oct 24, 2024, at 5:30 AM, Maurizio Cimadamore <maurizio.cimadamore at oracle.com> wrote:
> 
> I'm not sure about the generic type - e.g. is there an undefined for `int` that is different from the undefined for `String` ?

Yes. The naming is not quite right it should be something like:

  %0 : unknown<int> = unknown.value;

A value whose type is unknown<T> has a value of T but that value is unknown.

The intent was to allow for easier derivation of the variable's type, Var<T>, and potentially for other hints such as size/storage information, or transformations to a default value (if available).


> 
> I think this is what Scala calls Nothing ? E.g. the bottom of all the hierarchy - and you need to refer to a "value" of this bottom type. It's not `null`, but kind of close (a generalization of it, in fact).
> 

Ah yes that’s the kind of thing I was wondering about. We could have:

  %0 : nothing = nothing.value;

That would also work, and is simpler. (FWIW I nearly considered using a void value.)

Paul.

> Maurizio
> 
> On 23/10/2024 19:15, Paul Sandoz wrote:
>> Currently we model an uninitialized variable as if it were initialized with the default value. So we loose the distinction between the following assignment statements:
>> 
>>   int x = 0;
>>   int x;
>> 
>> It becomes problematic when generating and lifting bytecode. It will be problematic for value types that have no default. And, I think is generally problematic when reasoning about variables and definite assignment rules.
>> 
>> Consider the Java code and the models at the end of this email. Notice that for the lowered pure SSA model the initialization value is no longer used, which makes sense due to the Java language’s rules about definite assignment.
>> 
>> I think we can solve this by introducing an undefined operation whose result would be used instead of the constant default value:
>> 
>>     %0 : undefined<int> = undefined;
>>     %1 : Var<int> = var %0 @"x";
>> 
>> The above models an uninitialized variable. It states the var is initialized with an undefined value whose type is of int. Allowing var to uniformly accept an operand should allow for more uniform processing and better analysis e.g., when an undefined value shows up in places it should not.
>> 
>> There is probably some other, possibly better, name/concept for this in academic literature.
>> 
>> Paul.
>> 
>>     @CodeReflection
>>     public static int f() {
>>         int x;
>>         // x is definitely unassigned
>>         if (true) {
>>             x = 1;
>>         } else {
>>             x = 0;
>>         }
>>         // x is definitely assigned
>>         return x;
>>     }
>> 
>> 
>> Model produced by the compiler:
>> 
>> func @"f" ()int -> {
>>     %0 : int = constant @"0";
>>     %1 : Var<int> = var %0 @"x";
>>     java.if
>>         ()boolean -> {
>>             %2 : boolean = constant @"true";
>>             yield %2;
>>         }
>>         ()void -> {
>>             %3 : int = constant @"1";
>>             var.store %1 %3;
>>             yield;
>>         }
>>         ()void -> {
>>             %4 : int = constant @"0";
>>             var.store %1 %4;
>>             yield;
>>         };
>>     %5 : int = var.load %1;
>>     return %5;
>> };
>> 
>> 
>> Lowered model:
>> 
>> func @"f" ()int -> {
>>     %0 : int = constant @"0";
>>     %1 : Var<int> = var %0 @"x";
>>     %2 : boolean = constant @"true";
>>     cbranch %2 ^block_1 ^block_2;
>>      ^block_1:
>>     %3 : int = constant @"1";
>>     var.store %1 %3;
>>     branch ^block_3;
>>      ^block_2:
>>     %4 : int = constant @"0";
>>     var.store %1 %4;
>>     branch ^block_3;
>>      ^block_3:
>>     %5 : int = var.load %1;
>>     return %5;
>> };
>> 
>> 
>> Lowered and pure SSA model:
>> 
>> func @"f" ()int -> {
>>     %0 : int = constant @"0";
>>     %1 : boolean = constant @"true";
>>     cbranch %1 ^block_1 ^block_2;
>>      ^block_1:
>>     %2 : int = constant @"1";
>>     branch ^block_3(%2);
>>      ^block_2:
>>     %3 : int = constant @"0";
>>     branch ^block_3(%3);
>>      ^block_3(%4 : int):
>>     return %4;
>> };
>> 
>> 
>>