SSA: Global variables

[vezenovm]

Problem

Now that the compiler supports inlining Brillig functions based off of an aggressiveness setting, we can potentially have non-inlined functions in our final SSA. Previously, when we used to inline all functions a global would simply be a local constant that was constructed in the top block of a function. With multiple functions being able to re-use the same global, we may now be duplicating initialization of the those constants across functions.

e.g. let's take the modified regression_4709 test:

global EXPONENTIATE: [[Field; 2]; 2] = [
    [1, 1],
    [0, 0],
];
fn main(x: Field, y: pub Field) {
    let mut acc: Field = 0;
    for i in 0..2 {
        for j in 0..2 {
            acc += EXPONENTIATE[i][j];
        }
    }
    assert(!acc.lt(x));
    assert(x != y);

    dummy_again(x, y);
}
fn dummy_again(x: Field, y: pub Field) {
    let mut acc: Field = 0;
    for i in 0..2 {
        for j in 0..2 {
            acc += EXPONENTIATE[i][j];
        }
    }
    assert(!acc.lt(x));
    assert(x != y);
} 

If compiled with a really low inliner aggressiveness, while compiling to Brillig we will get the following SSA for main:

brillig(inline) fn main f0 {
  b0(v0: Field, v1: Field):
    v3 = allocate -> &mut Field
    store Field 0 at v3
    v6 = make_array [Field 1, Field 1] : [Field; 2]
    v7 = make_array [Field 0, Field 0] : [Field; 2]
    v8 = make_array [v6, v7] : [[Field; 2]; 2]
    jmp b1(u32 0)
  b1(v2: u32):
    v11 = lt v2, u32 2
    jmpif v11 then: b3, else: b2
  b2():
    v12 = load v3 -> Field
    v14 = call f2(v12, v0) -> u1
    constrain v14 == u1 0
    v16 = eq v0, v1
    constrain v16 == u1 0
    call f3(v0, v1)
    return
  b3():
    v21 = array_get v8, index v2 -> [Field; 2]
    v22 = load v3 -> Field
    ...
    inc_rc v21
    v23 = array_get v21, index u32 0 -> Field
    v24 = add v22, v23
    ...
    inc_rc v21
    v26 = array_get v21, index u32 1 -> Field
    v27 = add v24, v26
    store v27 at v3
    v28 = add v2, u32 1
    jmp b1(v28)
}

We will see the exact same SSA for dummy_again. This means everytime dummy_again is called we are going to reinitialize the EXPONENTIATE global array.

Happy Case

We should add global variables to SSA. These must be compile time values and must be immutable.

An example of what it could like in SSA pseudocode:

@v0 = global make_array [Field 1, Field 1] : [Field; 2]

brillig(inline) fn main f0 {
  b0:
  ...
  b3():
    v21 = array_get @v0, index v2 -> [Field; 2]
}

brillig(inline) fn dummy_again f0 {
  b0:
  ...
  b3():
    v21 = array_get @v0, index v2 -> [Field; 2]
}

Some of the handling of constants in Brillig will also have to be updated to share global constants across functions.

LLVM has global variables as well (https://llvm.org/docs/LangRef.html#global-variables), from which the inspiration for the @ marker came.

Workaround

None

Workaround Description

If you want non-inlined functions there is not really a workaround as the workaround is to inline all functions.

Additional Context

No response

Project Impact

None

Blocker Context

No response

Would you like to submit a PR for this Issue?

Yes

Support Needs

No response

[jfecher]

We could also take inspiration from cranelift's global values here since our SSA is based more off of it