Extend to more than one block

[zenna]

Currently we are assuming we have only one block, of course we need to extend to more than one. This requires first figuring out the correct semantics #3

[zenna]

Structure of Blocks

A basic block is a straight line Blocks are themselves elements of a language. The grammar is something like:

block   ::= blockid : v* line*
line    ::= v = e*
e       ::= v | literal
literal ::= + | - | & | / | ... | 1 | 2 | 3 | ...

An example Block is then

b2 : x y z
a = f x y
z = g 1 a

Transitions

Inversion

When inverting a function in CFG form there are several possibilities with respect to the control flow order (CFO): the sequence of blocks to visit

1. In the forward function, the CFO is fixed, -- not dependent on the inputs to the function -- and its fixedness can be inferred just from analysis of which variables are used in the transitions. Example:

function f(x)
  for i = 1:5
    x += 1
  end
  x
end

ulia> @code_ir f(3)
1: (%1, %2)
  %3 = 1:5
  %4 = Base.iterate(%3)
  %5 = %4 === nothing
  %6 = Base.not_int(%5)
  br 3 (%2) unless %6
  br 2 (%4, %2)
2: (%7, %8)
  %9 = Core.getfield(%7, 1)
  %10 = Core.getfield(%7, 2)
  %11 = %8 + 1
  %12 = Base.iterate(%3, %10)
  %13 = %12 === nothing
  %14 = Base.not_int(%13)
  br 3 (%11) unless %14
  br 2 (%12, %11)
3: (%15)
  return %15

The transition predicate in the first block is %6, which depends on %5, %4, %3, but not on the input %2. The transition predicate in the second block is %14, which depends on %13, 12, 3, 10, 10, 7, 9, 7, where 7 is 4 in Block 1. None of these are the input. Hence, we can safely say that the forward execution CFO is independent of the input and its inverse will be too (confirm this is necessarily true).

2. In the forward function, the CFO is fixed, but this cannot be inferred just from looking at dependencies between variables

julia> function g(x)
         if x > 0 & x < 0
           x = x + 1
         else
           x = x - 1
         end
       end
g (generic function with 1 method)

julia> @code_ir g(10)
1: (%1, %2)
  %3 = 0 & %2
  %4 = %2 > %3
  br 3 unless %4
  br 2
2:
  %5 = %3 < 0
  br 4 (%5)
3:
  br 4 (false)
4: (%6)
  br 6 unless %6
  br 5
5:
  %7 = %2 + 1
  return %7
6:
  %8 = %2 - 1
  return %8

Here in the first block the switch depends on 4, which depends in turn on the input 2. The only way to infer that the CFO is fixed is to reason about the values themselves.

3. The CFO order is in general dynamic but given the input to the inverse is fixed

function h(x)
  if x > 0
    x * x
  else
    x - 10
  end
end

julia> @code_ir h(10)
1: (%1, %2)
  %3 = %2 > 0
  br 3 unless %3
2:
  %4 = %2 * %2
  return %4
3:
  %5 = %2 - 10
  return %5

Here given the sign of the output (input to inverse) we can infer which of the two paths must have been taken.

4. The CFO is truly dynamic -- given the output, there are many possible CFOs.

function i(x)
  if x > 0
    x + x
  else
    x * x
  end
end

julia> @code_ir i(-4)
1: (%1, %2)
  %3 = %2 > 0
  br 3 unless %3
2:
  %4 = %2 + %2
  return %4
3:
  %5 = %2 * %2
  return %5

So for instance given the input to the inverse 16, it could have been 8 + 8 or -4 * -4

6. Combinations: We can imagine each of these scenarions happening in different combinations of the sub graphs.

[zenna]

Let's be more concrete about the analysis

Let f be a function and its control flow graph be G = (N, E). A path is a sequence of edges (which satisfies the typical path conditions), whose first node is n0 and whose last is nf.

I say an input to f produces a path p if executing f(args...) visits the blocks in order specified by p.

A path if feasible if there exists at least one input that produces it.

A procedure has static control flow if the number of feasible paths is exactly 1.

[zenna]

julia> ir = @code_ir f(3)
1: (%1, %2)
  br 2 (0, 0)
2: (%3, %4)
  %5 = %3 <= %2
  br 4 unless %5
  br 3
3:
  %6 = %4 + %3
  %7 = %3 + 1
  br 2 (%7, %6)
4:
  return %4

## Explicit form

julia> ir = @code_ir f(3)
1: (%1, %2)
  br 2 (0, 0, %2)
2: (%3, %4, %22)
  %5 = %3 <= %2
  br 4 unless %5
  br 3 (%3, %4, %22)
3: (%23, %24, %22b)
  %6 = %23 + %24
  %7 = %23 + 1
  br 2 (%7, %6, %22b)
4: 
  return %4

## Inverse
0: (%1, %2, %3[phi]) 
  %1 = choose((4,), %3)
  %2 = $1 == 4
  br 4 (%2) unless %2 

4: (%3)
  %4 = choose((2,), %3)
  %5 = $1 == 2
  br 2 (%2) unless %2   

2: 
  ...

  %34 = invertapply(...)
  %3 = getindex(%34, 1)
  %4 = getindex(%34, 1)
  %6 = choose((1, 3), %3)
  %7 = %6 == 1
  %8 = %6 == 3
  br 1 (%3, %4) unless %8
  br 3 (%3, %4) unless %7