Modeling uninitialized variables

[Paul Sandoz]

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;
};