Modeling uninitialized variables

[Paul Sandoz]

Here’s a PR that more concretely expresses this approach:

  https://github.com/openjdk/babylon/pull/263/

Paul.

On Oct 23, 2024, at 11:15 AM, Paul Sandoz <paul.sandoz at oracle.com> 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;
};




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/babylon-dev/attachments/20241023/a0e03847/attachment-0001.htm>