3.1.1 Analyzed Program: assign_expression.c

int foo(int y1, int y2){
    y2 = y1 + y1;
} 

It is straightforward to observe that this program has a polynomial growth bound. The precise value of that bound is \(\texttt{y1}^\prime = \texttt{y1} \land \texttt{y2}^\prime \leq 2 * \texttt{y1}\). Although the program is simple, it is interesting because binary operations introduce complexity in program analysis.

3.1.2 CLI Command

The current working directory should be the location of unzipped examples from Installation Step 4.

pymwp basics/assign_expression.c --fin --info --no_time

Output:

INFO (result): Bound: y1' ≤ y1 ∧ y2' ≤ y1
INFO (result): Bounds: 3
INFO (result): Total time: 0.0 s (0 ms)
INFO (file_io): saved result in output/assign_expression.json

3.1.3 Discussion

The analysis correctly assigns a polynomial bound to the program. The bound obtained by the analyzer is \(\texttt{y1}^\prime \leq \texttt{y1} \land \texttt{y2}^\prime \leq \texttt{y1}\). Comparing to the precise value determined earlier, this bound is correct, because we omit constants in the analysis results.

Due to non-determinism, the analyzer finds three different derivations that yield a bound. From the .json file, that captures the analysis result in more technical detail, it is possible to determine these three bounds are:

• \(\texttt{y1}^\prime \leq \texttt{y1} \land \texttt{y2}^\prime \leq \texttt{max(0,0) + y1}\)
• \(\texttt{y1}^\prime \leq \texttt{y1} \land \texttt{y2}^\prime \leq \texttt{max(0,0) + y1}\)
• \(\texttt{y1}^\prime \leq \texttt{y1} \land \texttt{y2}^\prime \leq \texttt{max(0,y1) + 0}\)

They all simplify to \(\texttt{y1}^\prime \leq \texttt{y1} \land \texttt{y2}^\prime \leq \texttt{y1}\). This concludes the obtained result matches the expected result.

3.2.1 Analyzed Program: exponent_2.c

int foo(int base, int exp, int i, int result){
    while (i < exp){
        result = result * base;
        i = i + 1;
    }
}

This program’s variable \(\texttt{result}\) grows exponentially. It is impossible to find a polynomial growth bound, and the analysis is expected to report \(\infty\)-result. This example demonstrates how pymwp arrives to that conclusion.

3.2.2 CLI Command

pymwp infinite/exponent_2.c --fin --info --no_time

Output:

INFO (result): foo is infinite
INFO (result): Possibly problematic flows:
INFO (result): base ➔ result ‖ exp ➔ result ‖ i ➔ result ‖ result ➔ result
INFO (result): Total time: 0.0 s (2 ms)
INFO (file_io): saved result in output/exponent_2.json

3.2.3 Discussion

The output shows that the analyzer correctly detects that no bound can be established, and we obtain \(\infty\)-result. The output also gives a list of problematic flows. This list indicates all variable pairs, that along some derivation paths, cause \(\infty\) coefficients to occur. The arrow direction means data flows from source ➔ target. We can see the problem with this program is the data flowing to \(\texttt{result}\) variable. This clearly indicates the origin of the problem, and allows programmer to determine if the issue can be repaired, to improve program’s complexity properties.

3.3.1 Analyzed Program: notinfinite_3.c

int foo(int X0, int X1, int X2, int X3){
    if (X1 == 1){
        X1 = X2+X1;
        X2 = X3+X2;
    }
    while(X0<10){
        X0 = X1+X2;
    }
}

This program contains decision logic, iteration, and multiple variables. Determining if a polynomial growth bound exists is not immediate by inspection. It is therefore an interesting candidate for analysis with pymwp!

3.3.2 CLI Command

pymwp not_infinite/notinfinite_3.c --fin --info --no_time

Output:

INFO (result): Bound: X0' ≤ max(X0,X1)+X2*X3 ∧ X1' ≤ X1+X2 ∧ X2' ≤ X2+X3 ∧ X3' ≤ X3
INFO (result): Bounds: 9
INFO (result): Total time: 0.0 s (3 ms)
INFO (file_io): saved result in output/notinfinite_3.json

3.3.3 Discussion

Compared to previous examples, the analysis is now getting more complicated. We can observe this in the number of discovered bounds and the form of the bound expression. The number of times the loop iterates, or which branch of the if statement is taken, is not a barrier to determining the result.

From the bound expression, we can determine the following.

• \(\texttt{X0}\) has the most complicated dependency relation. Its mwp-bound combines the impact of the if statement, the while loop, and the chance that the loop may not execute.

• \(\texttt{X1}\) and \(\texttt{X2}\) have fairly simple growth dependencies, originating from the if statement.

• \(\texttt{X3}\) is the simplest case – it never changes. Therefore, it only depends on itself.

Overall, the analysis concludes the program has a polynomial growth bound.

3.4.1 Analyzed Program: infinite_3.c

int foo(int X1, int X2, int X3){
    if (X1 == 1){
        X1 = X2+X1;
        X2 = X3+X2;
    }
    while(X1<10){
        X1 = X2+X1;
    }
}

If you studied the previous example carefully, you might notice that this example is very similar. There is a subtle differences: variable \(\texttt{X0}\) has been removed and its usages changed to \(\texttt{X1}\). This example demonstrates how this seemingly small change impacts the analysis result.

3.4.2 CLI Command

pymwp infinite/infinite_3.c --fin --info --no_time

Output:

INFO (result): foo is infinite
INFO (result): Possibly problematic flows:
INFO (result): X1 ➔ X1 ‖ X2 ➔ X1 ‖ X3 ➔ X1
INFO (result): Total time: 0.0 s (2 ms)
INFO (file_io): saved result in output/infinite_3.json

3.4.3 Discussion

We can observe the result is \(\infty\). Thus, even a small change can change the analysis result entirely.

The output reveals the problem arises from how data flows from source variables \(\texttt{X1}\), \(\texttt{X2}\), and \(\texttt{X3}\), to target variable \(\texttt{X1}\). Observe that even though there is no direct assignment from \(\texttt{X3}\) to \(\texttt{X1}\), the analysis correctly identifies this dependency relation, that occurs through \(\texttt{X2}\).

From the output, we have identified the point and source of failure. Conversely, we know other variable pairs are not problematic. By focusing on how to avoid “too strong” dependencies targeting variable \(\texttt{X1}\), programmer may be able to refactor and improve the program’s complexity properties.

3.5.1 Analyzed Program

int foo(int X0, int X1, int X2){
    if (X0) {
      X2 = X0 + X1;
    }
    else{
      X2 = X2 + X1;
    }
    X0 = X2 + X1;
    X1 = X0 + X2;
    while(X2){
      X2 = X1 + X0;
    }
}

After seeing the various preceding examples – with and without polynomial bounds – we present the following challenge. By inspection, try to determine if this program is polynomially bounded w.r.t. its input values.

It is unknown which if branch will be taken, and whether the while loop will terminate, but this is not a problem for determining the result.