What is the Static Single Assignment Form (SSA) and when to use it?

When coding, we are used to reassigning variables repeatedly. Just take for (int i = 0; i < 100; i++) { } as an example, where the value of i changes a hundred times after its initialization. But what happens when we allow variables to be assigned only once? And why should we even do it?

By applying static single assignment form, or short SSA, each variable is assigned exactly once. This concept is utilized, for instance, in intermediate representations such as in compilers. For achieving SSA, variables get versioned, usually by adding an index to the variable’s name. For example, let’s translate the following lines of code into SSA:

a = 1
a = 2
b = a

a_0 = 1
a_1 = 2
b_0 = a_1

The variables a_0, a_1 and b_0 are assigned to a value only once whereas a is set twice, resulting in two versions of the variable name in SSA.

Why is SSA important?

In the example above, it is easy for the human eye to see that the first assignment a = 1 is not necessary since this value of the variable is never used. For a computer, however, it is not, as it would need to perform further analysis to spot this. But when SSA is applied to the code, even a computer can immediately recognize that a_0 is not used at all.

In this manner, SSA enables different kinds of optimization in compilers. It aids tasks such as eliminating dead code (i.e. code that has no effect on the outcome) or determining when two operations are equivalent in order to replace expensive computations with cheaper, equivalent ones.

What does SSA have to do with Symflower’s core technology?

Similarly to a compiler, Symflower’s symbolic execution needs to traverse the given source code, or respectively, an intermediate representation of it and translate it to something it can work with. By symbolically executing all parts of a program, Symflower can find all relevant paths through the code and, at the same time, the corresponding conditions around how the paths are reached. In order to assemble these constraints, we use the translation of the code into what you might have already guessed: SSA. This way, a constraint solver can efficiently produce values that satisfy the collected requirements.

The results computed by the symbolic execution are program inputs that trigger certain behavior. Read the first blog post of this series on Symflower’s Core Technology to learn more about symbolic execution.

The example we investigated in the first blog post was the following function:

func f(a int, b int) int {
  x, y := 1, 0
  if a != 0 {
    y = x + 3
    if b == 0 {
      x = 2 * (a + b)
    }
  }
  return (a + b) / (x - y)
}

We applied symbolic execution by hand to the problem of finding a division by zero in the last statement of the function. Let’s see how the collected constraints look like in SSA.

Please note that the variables which we want the solver to compute the value for are not given a value, they are only defined, so that the assignment can still be done by the solver. Due to this, the SSA variables in Symflower’s symbolic execution have exactly one value only after we query the results from the solver. Until that point, they have at most one. In these pictures, we represent the definition of variables without assignments with the prefix “var”. Therefore, the first assignments of the variables x and y and their corresponding constraints look as follows:

Please check out the blog post on the topic to find out how the paths and their constraints are collected. The result in SSA is the following:

Along each path, every SSA variable is assigned at most once. In the solvable case, each variable has exactly one value as expected.

Don’t forget to subscribe to our newsletter, and follow us on Twitter, Facebook, and LinkedIn for more content.