How to find the fixpoint of a loop and why do we need this?



  • I know that in static analysis of program, we need to find fixpoint to analysis the info loop provided.

    I have read the wiki as well as related meterials in the book Secure_programming_with_Static_Analysis.

    But I am still confused with the concept fixpoint, so my questions are:

    1. could anyone give me some explanations of the concept, fixpoint?

    2. What is the practical way(ways) to find the fixpoint in static analysis?

    3. What information can we get after finding the fixpoint?

    Thank you!



  • Most of this comes from Wikipedia and these lecture notes.

    Wikipedia defines a fixed point this way:

    In mathematics, a fixed point [...] of a function is an element of the function's domain that is mapped to itself by the function. [...] That is to say, c is a fixed point of the function f(x) if and only if f(c) = c.

    For example, for the function f(x) = x*x, 0 and 1 are fixed points.

    One form of static analysis is control flow analysis. In control flow analysis, you derive a control flow graph (CFG) of the program, and then you analyze the CFG to deduce things, e.g. whether a variable is still live at a certain statement, or whether a variable is always initialized by the time it reaches a certain statement. Based on what you want to deduce, you define a set of functions in terms of the CFG, and then you solve the functions using a fixed point algorithm.

    The lecture notes give the example of analyzing liveness: for each point in the program, which variables defined before that point have a value that is read at that point or in some later point. For example, consider this code:

    1: a = 4
    2: b = 5
    3: c = a+b
    4: d = 3
    

    The live variables for each statement are:

    (1) none
    (2) a (a was defined in statement 1 and read in statement 3)
    (3) a,b (a and b are read in statement 3)
    (4) none
    

    Now consider this program with a loop:

    var x,y,z;
    x = input;
    while (x>1) {
      y = x/2;
      if (y>3) x = x-y;
      z = x-4;
      if (z>0) x = x/2;
      z = z-1;
    }
    output x;
    

    The control flow graph looks like this:

    enter image description here

    What are the live variables for each statement? Using the rules stated in the lecture notes, here are the equations to solve:

    [var x,y,z;] = [x=input] \ {x, y, z}
    [x=input] = [x>1] \ {x}
    [x>1] = ([y=x/2] ∪ [output x]) ∪ {x}
    [y=x/2] = ([y>3] \ {y}) ∪ {x}
    [y>3] = [x=x-y] ∪ [z=x-4] ∪ {y}
    [x=x-y] = ([z=x-4] \ {x}) ∪ {x,y}
    [z=x-4] = ([z>0] \ {z}) ∪ {x}
    [z>0] = [x=x/2] ∪ [z=z-1] ∪ {z}
    [x=x/2] = ([z=z-1] \ {x}) ∪ {x}
    [z=z-1] = ([x>1] \ {z}) ∪ {z}
    [output x] = [exit] ∪ {x}
    [exit] = {}
    

    where [X] denotes the set of variables that are live at statement [X], is the union operator, {} denotes a set, and \ is the set difference operator.

    You can solve those equations using a fixed point algorithm. You can imagine how you might solve this by hand; everywhere that you see [some-statement] on the right hand side of an equation, you would substitute the definition of [some-statement]. You might do that iteratively, substituting until eventually all of the equations have nothing but sets (and no [some-statement]) on their right-hand sides. That's essentially what the fixed point algorithm does. The function is the set of equations, and the fixed point is the point where performing substitution on the equations no longer causes them to change.

    By the way, the answer for the above problem is this:

    [entry] = {}
    [var x,y,z;] = {}
    [x=input] = {}
    [x>1] = {x}
    [y=x/2] = {x}
    [y>3] = {x, y}
    [x=x-y] = {x, y}
    [z=x-4] = {x}
    [z>0] = {x, z}
    [x=x/2] = {x, z}
    [z=z-1] = {x, z}
    [output x] = {x}
    [exit] = {}
    

    If you read the lecture notes, you can see how you might use that answer.

    Most of us will never write fixed point algorithms, much less static analysis tools, and so I won't try describe practical ways to find the fixed point in static analysis. The more important point -- and perhaps the point of the book you mentioned -- is that (1) fixed point algorithms are tools for performing static analysis and (2) you can use static analysis to find bugs in your code.


Log in to reply
 

Suggested Topics

  • 2
  • 2
  • 2
  • 2
  • 2
  • 2
  • 2
  • 2