1 of 42

Lec 20, Fixpoint Theory, Static Analysis

CS 6110, Software Correctness Analysis, Spring 2023

Ganesh Gopalakrishnan

School of Computing

University of Utah

Salt Lake City, UT 84112

2 of 42

Outline, Motivations

  • We are studying program correctness analysis
    • Model-Checking
    • Dynamic Analysis
    • Static Analysis
      • New topic
      • Good for issuing guarantees over entire input ranges
        • It may produce false alarms
  • The main purpose of this lecture
    • To give you pointers to the literature
    • To expose you to two key concepts / algorithms in CS
      • Fixpoint theory
        • Fixpoint iterations in a finite lattice is how static analyzers use it
          • Shown in the context of flow-sensitive static analysis
      • Unification
        • A basic technique for type-inference (e.g. in languages like Ocaml and Haskell)
          • Shown in the context of flow-insensitive static analysis

3 of 42

The topic is vast; good material online also

4 of 42

Gives me a chance to talk about Fixpoints also

  • The notion of fixpoints arises in many areas of CS
    • This is how Lambda Calculus models recursion
      • Study it from https://github.com/ganeshutah/Jove.git
        • I include Jove notebooks on studying this interactively

5 of 42

Overview of fixpoints

  • Relevant whenever we solve things through recursion
  • x = f(x) is a fixpoint (or fixed-point) of x
  • Often x is unique
    • Not always though
  • Whenever there are multiple fixpoints, we know which solution "matters"

​

6 of 42

Overview of fixpoints

7 of 42

Overview of fixpoints: Mutual Recursion

8 of 42

Overview of fixpoints

9 of 42

Overview of fixpoints

10 of 42

Overview of fixpoints

11 of 42

Overview of fixpoints

12 of 42

Overview of fixpoints

13 of 42

Overview of fixpoints

14 of 42

Overview of fixpoints: BDDs to compute … these were done using an interactive BDD calculator called BED

​

We can revive such a system and write a CTL forward model-checker or a backward checker…

15 of 42

Overview of fixpoints using CTL (McMillan)

16 of 42

Overview of fixpoints

17 of 42

Overview of fixpoints

18 of 42

Overview of fixpoints

19 of 42

Overview of fixpoints: in solving for recursion

20 of 42

Overview of fixpoints: in solving for recursion

If you lambda-abstract F and write it in fixpoint form we get'

​

F = lambda x: lambda y: (x==y) → y+1 , F(x, F(x-1, y+1))

​

or

​

F = [ lambda G : (lambda x : lambda y: (x==y) → y+1 , G(x, G(x-1, y+1))) ] F

​

Thus compute the LFP of

​

[ lambda G : (lambda x : lambda y: (x==y) → y+1 , G(x, G(x-1, y+1))) ]

​

by starting with F_0 = bottom (fully undefined function

​

F_1 = [ lambda G : (lambda x : lambda y: (x==y) → y+1 , G(x, G(x-1, y+1))) ] F_0

​

This reduces to F_1 = lambda x: lambda y: (x==y) → y+1 , bottom

​

In the limit, we get f3 .

​

f1 and f2 are unattainable (through computational rules) fixpoints!

21 of 42

E.g., Analysis (from Moller/Schwartzbach)

22 of 42

E.g., Analysis (from Moller/Schwartzbach)

23 of 42

E.g., Analysis (from Moller/Schwartzbach)

24 of 42

E.g., Analysis (from Moller/Schwartzbach)

25 of 42

E.g., Analysis (from Moller/Schwartzbach)

See the recursion here!

26 of 42

E.g., Analysis (from Moller/Schwartzbach)

27 of 42

E.g., Analysis (from Moller/Schwartzbach)

28 of 42

Flow-Sensitive Type Inference

  • Details
    • We will use lattices (and perform Abstract Interpretation)

​

  • Lattices help establish an information-theoretic order

​

  • We will perform fixed-point iterations on lattices

​

  • All this will be broken down via examples and then illustrations using Alloy

29 of 42

Lattice-Engineering is important!

  • Used in studying denotational semantics using fixed-point theory
  • Used in type-inference
  • Used in circuit simulation

Solving Recursion

​

The “f” function that is recursively defined

Has an increasing chain of approximations

Going top to bottom

And these functions can all

Be situated in

Lattice-Like structures

(often Complete Partial Orders)

30 of 42

Lattices in Circuit Simulation

31 of 42

Definitions pertaining to lattices in Alloy

  • Loosely (see spa.pdf for precise definitions…) Lattices are partially ordered sets with the notion of “le” or [= showing the ordering. There is a notion of upper-bound and lower-bound for any subset of the lattice. There is a notion of a greatest lower-bound and least upper bound. They prove to be unique (because of the set being a partial order).
  • A partial order is a lattice if the GLB and LUB exist for any pair of elements. Finite lattices are complete (only those will be illustrated using Alloy). Infinite lattices require there to be a GLB and LUB for every set – even empty sets. Think of the set of all finite subsets of Nat ordered by [=. We can make this a complete lattice using subset inclusion, but must artificially add a “top” element.

​

  • All this flies past – let’s pin it down using Alloy!

32 of 42

Lattices in Alloy

33 of 42

Static Analysis

  • Let us follow the slides at https://cs.au.dk/~amoeller/spa/
  • Then learn the basics by doing some exercises, encoding things in Prolog (for the flow-insensitive parts)

34 of 42

Why Prolog? Why Prolog in 6110?

  • Prolog is a useful declarative language to know
  • Type inference illustrated in spa.pdf uses unification
    • Unification is central to Prolog – happens at each “clause call”
    • Unification is “two-way pattern matching”
      • computes the most general unifier – e.g. mgu below is X=4, Y=2, Z=2
        • This substitution when applied to both sides makes them both the same
        • In this case makes them both plus(times(4), add(2,2))
      • Information flows both ways
    • Example of Unification ====🡺
    • Pattern matching: one-way info flow

35 of 42

Prolog Illustration: �a ‘map’ of linearly situated states a,b,c,d,e,f

  • Prolog’s goal : compute the “mgu” at each clause call
  • Suppose six states a,b,c,d,e,f are situated like that, going east to west
  • Here is a Prolog program that calculates the state positions relative to each other:

36 of 42

Prolog Illustration: �a ‘map’ of linearly situated states a,b,c,d,e,f

37 of 42

Prolog Illustration: �appending lists reversed (and a 2-line Append relation)

38 of 42

Unification in type-inference : We will study flow-insensitive type inference

39 of 42

Unification in type-inference

40 of 42

Unification in type-inference

41 of 42

Unification in type-inference

42 of 42

Unification in type-inference