Mixed flow graphs are very likely not my idea -- but this was the theory I used while defining my programs. I wouldn't know what to call it otherwise, so I came up with a way to express this concept for my own applications.

Suppose you have the following function:

int diamond(int x, int y) {
    int c = x + y; // 1
    if (c == 0) {
        return c; // 2
    } else if (x == 5) {
        c += 15; // 3
    } else if (y == 5) {
        c += 32; // 4
    } else {
        c += 6; // 5
    }
    return c; // 6
}

You'll end up with the following control flow:

The control flow graph for the function above

And data flow:

The data flow graph for the function above

Now, suppose that I wanted to ask questions like, "what value is in the return when x is 5 and y is -5?" With either of the graphs above, you wouldn't be able to tell me -- one just tells you where you can go, and the other tells you what values can exist. To ask questions about the results of a program, expressed as a path, you would need to be able to say which values do exist based on where you did go.

To express this, I propose a mixed-flow graph. To do this, I use custom nodes, which I call "psi nodes", with the following inputs/outputs:

The psi node here has the following behaviour:

By implementing the psi node in this fashion, we can emulate control flow nods with chains of psi nodes. Moreover, we can more specifically state which value a phi-node will result in.

As the function above gets very difficult to draw very fast, consider the following (simpler) function:

int simple_conditional(int x) {
    if (x != 0) {
        return 1;
    } else {
        return 0;
    }
}

We can express a mixed-flow graph for this function:

The mixed flow graph for the function above

Now, we can make assertions about data, e.g. "x is equal to 0", and determine that the return of the function is indeed 0 as psi node 2 is active and psi node 1 is not (as psi node 2's boolean input is inverted to true when psi node 1 is not active).

For a more complex example, consider a nested if statement:

int complex_conditional(int x) {
    int c = x + 10;
    if (x != 5) {
        c += 10;
        if (c > 30) {
            c = 30;
        }
    } else {
        c -= 1;
    }
    return c;
}

To handle this, we need two other considerations:

For example, we could consider:

c += 10;
if (c > 30) {
    c = 30;
}

As:

c += 10;
if (c > 30) {
    c1 = 30;
} else {
    c1 = c; // redundant, but explicit
}
c = c1;

With these replacements in mind, a mixed flow graph for complex_conditional could be drawn as:

The mixed flow graph for the function above

I apologise for the complexity of this graph, but it gets to be a lot of nodes very fast!

Take a moment to verify this for yourself by tracing through the various possibilities. You'll find that it neatly defines complex_conditional for various inputs of x.

The specific organisation of this graph makes it possible to quite easily represent functions as theorems. Lovely for us, as you can see by my discussion on MFG to SMT conversion.