Phases

Fixen programs enjoy compositionality: given two disjoint programs (sharing no relations), their union is a valid program whose evaluation is the union of the individual results. But what if you want to compose programs that share relations? For example, in static analysis, you might want to combine an interval analysis and a parity analysis, allowing them to exchange information during computation. A naive union of their rules fails because over-approximated facts subsume refined ones.

Phases of execution solve this by stratifying the program state into multiple fact databases, cycling through them as rules execute. This enables post-composition of rule sets and the modular composition of non-disjoint programs.

Motivating Example: Composing Analyses

To motivate phases, consider building a static analyzer for a simple imperative language. Programs in this language have variable declarations, assignments, conditional branches, and sequence points. An example program is as follows (taken from ¹):

example.imp

v <- 1
while v <= 9 do
    v <- v + 2
done
if v = 11 then
    v <- 0
fi

Running this program shows us that v is equal to 0 at the end of the program. Let us statically determine that this is the case.

First, we lower this program as an intermediate representation via a de-sugaring to basic statements in an assembly-like language:

example.imp-ir

  0: var v
  1: v <- 1
  2: branch v <= 9, 3, 5
  3: v <- v + 2
  4: jump 2
  5: branch v = 11, 6, 101
  6: v <- 0
101: END

This allows us to easily represent the program using Fixen facts. The relation declarations are as follows:

Relations for representing imperative programs

rel Var: Label, String
rel Assign: Label, String, Expr
rel Branch: Label, Expr, Label, Label
rel Seq: Label, Label

• Var l v states that program point l declares variable v.
• Assign l x e states that program point l assigns expression e to variable x.
• Branch l e t f states that program point l branches on expression e, jumping to t (true) or f (false) (unfortunately, like most languages, this language also assumes the law of the excluded middle).
• Seq l l' states that program point l is followed by l'.
• Labels are aliases for Haskell’s Natural, and Expr is a datatype we will define later for capturing expressions in the imperative language.

For instance, the example program example.imp-ir is represented using the following Fixen facts:

Facts for representing example.imp-ir

Var 0 "v"
Seq 0 1
Assign 1 "v" (Num 1)
Seq 1 2
Branch 2 (Leq "v" (Num 9)) 3 5
Assign 3 "v" (Plus (Id "v") (Num 2))
Seq 3 2
Branch 5 (Eq "v" (Num 11)) 6 101
Assign 6 "v" (Num 0)
Seq 6 101
Var 101 "END"

Interval Analysis

An interval analysis ascribes a range of possible values to each variable at each program point. Ideally, we should conclude that v belongs to the interval at the end of the program.

Intervals assemble into a lattice, ordered by inclusion, i.e., whenever and . Interval joins and meets follow immediately from this order. Presume that we define the Interval data type (and associated order, join and meet functions) in Haskell (we show this later).

Then, we track program states with a relation:

Lattice and relation for interval analysis

lat StateI where
  type = HashMap String Interval
  leq  = leq
  join = (\/)
  meet = (/\)

rel StateBeforeI: Label, StateI

StateI is a map lattice, ordered by inclusion of map keys and the interval order on map values. The StateBeforeI relation maps each program label to a StateI. Essentially, at every program point, we track the intervals assigned to each variable that exists within the program. The leq, join and meet functions are standard, so we use definitions from the lattices library.

The analysis rules initialize states and propagate them through assignments and branches:

Interval analysis rules

rule assignInitI: Assign l _ _   |- StateBeforeI l HashMap.empty
rule branchInitI: Branch l _ _ _ |- StateBeforeI l HashMap.empty
rule varInitI:    Var l _        |- StateBeforeI l HashMap.empty

rule assignStepI: Assign l x e, Seq l l', StateBeforeI l st
                  |- StateBeforeI l' (HashMap.insert x (evalI e st) st)

rule branchTrueI: Branch l e t _, StateBeforeI l st,
                  if BTrue `leq` (evalCondI e st)
                  |- StateBeforeI t (refineTI e st)

rule branchFalseI: Branch l e _ f, StateBeforeI l st,
                   if BFalse `leq` (evalCondI e st)
                   |- StateBeforeI f (refineFI e st)

• The assignInitI, branchInitI and varInitI rules initialize the state before each program point to the empty map
• The assignStepI rule is a transfer function that inserts the variable-interval map entry x and evalI e st into the state before the label it jumps to. evalI receives an expression and the current state st and evaluates it into an interval. We define the evalI function later.
• The branchTrueI and branchFalseI rules are transfer functions for conditional branching. There are several aspects to these. Firstly, we should visit the true (resp. false) branches only if the condition allows it. This is represented by the condition BTrue `leq` (evalCondI e st) (resp. BFalse `leq` (evalCondI e st)). The BTrue and BFalse construtors belong to a boolean lattice, with values representing no information, BTrue representing “definitely true”, BFalse representing “definitely false”, and representing “either true or false”. Secondly, if a true (resp. false) branch is visited, we refine the intervals in the state based on the condition itself using refineTI (resp. refineFI), which we define in Haskell later. As an intuitive example, suppose the condition is x <= 10 and st has x being within the interval . Then, in the true branch, x must be within , while in the false branch x must be within .

Complete Example

Download: interval-analysis.tar.gz

SHA-256: 346bec4dc24879e7c23efdb8410e263646fcdce716c2dfe681bb02ddd275ec84

Let us make these ideas concrete by implementing the interval analysis, executing it, and observing the state at the end of the program. Our project is going to have the following structure:

• Directorystatic-analysis

  • static-analysis.cabal
  • Directoryapp

    • Main.hs
    • Common.hs
    • IntervalUtils.hs
  • Directoryfix

    • Program.fix
    • IntervalAnalysis.fix

The cabal configuration file will be as follows. Note the use of the lattices library which contains definitions that will simplify our implementation, and the hashable library so that expressions can be used as map keys.

static-analysis.cabal

cabal-version:      3.0
name:               static-analysis
version:            0.1.0.0
build-type:         Simple
common warnings
    ghc-options: -Wall
executable static-analysis
    import:           warnings
    main-is:          Main.hs
    other-modules:    Common
                    , IntervalAnalysis
                    , IntervalUtils
    build-depends:    base
                    , pqueue
                    , unordered-containers
                    , hashable
                    , lattices
    hs-source-dirs:   app
    default-language: GHC2021

Common Definitions

First, populate app/Common.hs with some common definitions.

app/Common.hs

module Common where

import Algebra.PartialOrd
import Data.Hashable
import GHC.Generics
import Numeric.Natural

data Expr
  = Id String -- x
  | Num Int -- 1
  | Plus Expr Expr -- e + e'
  | Leq String Expr -- x <= e
  | Eq String Expr -- x = e
  deriving (Eq, Generic, Show)

instance Hashable Expr

type Label = Natural

data BBool = BTop | BBot | BTrue | BFalse
  deriving (Eq, Generic, Show)

instance PartialOrd BBool where
  BBot `leq` _ = True
  _ `leq` BTop = True
  x `leq` y = x == y

1. The Expr data type captures the kind of expressions we are expecting in the program:
   • Id refers to variables
   • Num refers to integers
   • Plus refers to additions in the form of e + e'
   • Leq refers to variable inequalities in the form of x <= e. Note that in other languages we typically have these in the form of e <= e' where both e and e' are expressions. For our example, the version of Leq we have will suffice.
   • Eq refers to variable equalities in the form of x = e. Note again that we typically have equalities in the form of e = e' in other languages.
2. We make Exprs Hashable by deriving Generic Expr and by declaring an instance of Hashable Expr. This allows Expr to be used as map keys in the Fixen-generated fact database.
3. Labels in our language are Natural numbers.
4. The BBool data type, as mentioned above, describes a lattice of boolean values. To endow this structure with a partial order, we declare an instance of PartialOrd, which comes from the lattices package. It is not always necessary to use lattices with Fixen, but can be idiomatic when using existing partially ordered or lattice types.

Utilities for the Interval Analysis

Next, we define the functions and data structures used by the interval analysis in app/IntervalUtils.hs:

app/IntervalUtils.hs

{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverlappingInstances #-}

module IntervalUtils where

import Algebra.Lattice
import Algebra.PartialOrd
import Common
import Data.HashMap.Strict (HashMap)
import Data.HashMap.Strict qualified as HashMap
import Data.List (intercalate)

data Interval = Pair Int Int | ITop | IBot
  deriving Eq

instance Show Interval where
  show (Pair a b) = "[" ++ show a ++ ", " ++ show b ++ "]"
  show ITop = "[-inf, inf]"
  show IBot = "empty"

instance Show (HashMap String Interval) where
  show m = "{ " ++ intercalate ", " (fmap (\(k, v) -> k ++ ": " ++ show v) (HashMap.toList m)) ++ " }"

(...) :: Int -> Int -> Interval
a ... b = if a > b then IBot else Pair a b

infix 5 ...

instance PartialOrd Interval where
  leq IBot _ = True
  leq _ ITop = True
  leq ITop _ = False
  leq _ IBot = False
  Pair a b `leq` Pair c d = a >= c && b <= d

instance Lattice Interval where
  ITop \/ _ = ITop
  _ \/ ITop = ITop
  IBot \/ x = x
  x \/ IBot = x
  Pair a b \/ Pair c d = min a c ... max b d

  IBot /\ _ = IBot
  _ /\ IBot = IBot
  ITop /\ x = x
  x /\ ITop = x
  Pair a b /\ Pair c d = max a c ... min b d

-- Easy lookups for intervals in state
lookupInterval :: String -> HashMap String Interval -> Interval
lookupInterval = HashMap.lookupDefault IBot

-- Puts a cap on the upper bound of an interval.
withUpperBound :: Int -> Interval -> Interval
withUpperBound n (Pair a b) = if n < b then a ... n else a ... b
withUpperBound _ x = x

-- Puts a minimum on the lower bound of an interval.
withLowerBound :: Int -> Interval -> Interval
withLowerBound n (Pair a b) = if n > a then n ... b else a ... b
withLowerBound _ x = x

-- Evaluates an expression, giving an interval.
evalI :: Expr -> HashMap String Interval -> Interval
evalI (Id x) st = lookupInterval x st
evalI (Num i) _ = i ... i
evalI (Plus e e') st = case (evalI e st, evalI e' st) of
  (Pair a b, Pair c d) -> a + c ... b + d
  (IBot, _) -> IBot
  (_, IBot) -> IBot
  _ -> ITop
evalI _ _ = IBot

-- Evaluates a condition, giving a BBool.
evalCondI :: Expr -> HashMap String Interval -> BBool
evalCondI (Leq x e) st = case (lookupInterval x st, evalI e st) of
  (Pair a b, Pair c d) ->
    if
      | b <= c -> BTrue
      | a > d -> BFalse
      | otherwise -> BTop
  (IBot, _) -> BBot
  (_, IBot) -> BBot
  _ -> BTop
evalCondI (Eq x e) st = case (lookupInterval x st, evalI e st) of
  (Pair a b, Pair c d) ->
    if
      | a == b && a == c && b == d -> BTrue
      | b < c || a > d -> BFalse
      | otherwise -> BTop
  (IBot, _) -> BBot
  (_, IBot) -> BBot
  _ -> BTop
evalCondI _ _ = BBot

-- Refines intervals assuming a condition is true.
refineTI :: Expr -> HashMap String Interval -> HashMap String Interval
refineTI (Leq x e) st = case evalI e st of
  Pair _ b ->
    let int = withUpperBound b $ lookupInterval x st
     in HashMap.insert x int st
  _ -> st
refineTI (Eq x e) st =
  let int = lookupInterval x st /\ evalI e st
   in HashMap.insert x int st
refineTI _ st = st

-- Refines intervals assuming a condition is true.
refineFI :: Expr -> HashMap String Interval -> HashMap String Interval
refineFI (Leq x e) st = case evalI e st of
  Pair a _ ->
    let int = withLowerBound (a + 1) $ lookupInterval x st
     in HashMap.insert x int st
  _ -> st
refineFI (Eq x e) st = case (lookupInterval x st, evalI e st) of
  (Pair a b, Pair c d) ->
    if c == d then
      if
        | b == c -> HashMap.insert x (a ... b - 1) st
        | a == c -> HashMap.insert x (a + 1 ... b) st
        | otherwise -> st
    else
      st
  _ -> st
refineFI _ st = st

Let us break down this monstrosity:

1. The first portion defines some basics of Intervals. In addition, we introduce a smart constructor ... so that nonsensical intervals like [1, 0] become the bottom, empty interval IBot.
2. We introduce instances of PartialOrd and Lattice for Interval. This allows HashMap String Interval to also be lattices (leq, /\ and \/ need these to work).
3. We write some convenience functions lookupInterval, withUpperBound and withLowerBound. These are thoroughly pedestrian.
4. The purpose of the functions evalI, evalCondI, refineTI and refineFI are as described earlier.

Relations for the Program

Next, we define the relations needed for capturing the statements in the program in fix/Program.fix. We separate these out from the interval analysis because we want these to be re-used for other analyses for the same imperative language.

fix/Program.fix

module Program where

rel Var: Label, String
rel Assign: Label, String, Expr
rel Branch: Label, Expr, Label, Label
rel Seq: Label, Label

Interval Analysis

Finally, we can write the Fixen program expressing the interval analysis in fix/IntervalAnalysis.fix:

fix/IntervalAnalysis.fix

module IntervalAnalysis where

import Algebra.PartialOrd
import Algebra.Lattice
import Common
import IntervalUtils

include "Program"

lat StateI where
  type = HashMap String Interval
  leq  = leq
  join = (\/)
  meet = (/\)

rel StateBeforeI: Label, StateI

rule assignInitI: Assign l _ _   |- StateBeforeI l HashMap.empty
rule branchInitI: Branch l _ _ _ |- StateBeforeI l HashMap.empty
rule varInitI:    Var l _        |- StateBeforeI l HashMap.empty

rule assignStepI: Assign l x e, Seq l l', StateBeforeI l st
                  |- StateBeforeI l' (HashMap.insert x (evalI e st) st)

rule branchTrueI: Branch l e t _, StateBeforeI l st,
                  if BTrue `leq` (evalCondI e st)
                  |- StateBeforeI t (refineTI e st)

rule branchFalseI: Branch l e _ f, StateBeforeI l st,
                   if BFalse `leq` (evalCondI e st)
                   |- StateBeforeI f (refineFI e st)

query stateBeforeI: StateBeforeI + -

1. This program imports all the Haskell modules needed for the analysis to work.
2. The program consists of an include statement, which essentially copies all definitions in another Fixen program into the current one. Include statements copy everything except priorities and phases declarations (which we will cover shortly). The argument to the include keyword is a path to the Fixen program to copy, where the .fix extension is optional.
3. The lattice, relation and rule declarations are as described before.
4. We introduce a stateBeforeI query to obtain analysis results.

In Progress

A less naive module system is being designed. Please reach out to us if you have ideas!

Building and Running

Let’s run the program!

1. Compile the Fixen program into a Haskell module. Note that fix/Program.fix does not need to be compiled, since fix/IntervalAnalysis.fix already contains every definition in it.

   Terminal

    ~/static-analysis $ fixen --output app/IntervalAnalysis.hs fix/IntervalAnalysis.fix

2. As always, we need some driver module. Populate app/Main.hs with the following, which performs the analysis, reads user input (program point) and shows the state before that program point:

   app/Main.hs

   module Main where
   
   import Common
   import IntervalAnalysis
   import Numeric.Natural
   
   main :: IO ()
   main = do
     let facts =
           [ Var 0 "v"
           , Seq 0 1
           , Assign 1 "v" (Num 1)
           , Seq 1 2
           , Branch 2 (Leq "v" (Num 9)) 3 5
           , Assign 3 "v" (Plus (Id "v") (Num 2))
           , Seq 3 2
           , Branch 5 (Eq "v" (Num 11)) 6 101
           , Assign 6 "v" (Num 0)
           , Seq 6 101
           , Var 101 "END"
           ]
         db = solve facts
     (label :: Natural) <- readLn
     print (stateBeforeI label db)

3. Run it and supply the label 101!

   Terminal

   ~/static-analysis $ cabal run
   101
   [StateBeforeI 101 { v: [0, 10] }]

Understanding the Results

Weird. Why does the analysis conclude that v is within , instead of being exactly to 0 (i.e., within the interval )? Let us inspect the states before other program points:

Terminal

~/static-analysis $ cabal run
2
[StateBeforeI 2 { v: [1, 11] }]
~/static-analysis $ cabal run
5
[StateBeforeI 5 { v: [10, 11] }]

That’s right!

• The state before entering the while loop (program point 2) has v within as expected, since the loop increments (by 2) v from 1 to 11.
• Exiting the while loop allows us to refine the interval for v to since the condition is v <= 9.
• This means that the condition in the if statement (program point 5) could be either true or false; it is true if v is 11, false if it is 10. Both branches could be visited, and thus the best we can conclude is that v is either
  • 0 (caused by the update in the true branch of the if statement) or
  • 10 (caused by not visiting the true branch in the if statement)!

Parity Analysis

How do we deal with the imprecision of the interval analysis? One approach is to ditch it altogether and instead perform a constant-propagation analysis. This is the simplest approach. However, for the sake of illustrating the purpose of Fixen’s phases, we can make the following observation: the variable v remains odd throughout loop execution.

• v is initialized as 1, which is odd.
• v is incremented by 2 at every loop iteration. Thus, exiting the loop, v remains odd.

Therefore, before the if statement at program point 5, v is within the interval and is odd. Crucially, we can use the oddness of v to refine the interval down to , ensuring that we never visit the false branch of the if statement!

As such, we shall work towards (1) adding a parity analysis (which determines if each variable is even or odd), then (2) composing it with the interval analysis, obtaining what’s known as their reduced product.

Let us define the parity analysis.

Download: parity-analysis.tar.gz

SHA-256: 2d6d4960de0cb8b91bec10032654a28b6c1d10e8559cb7b68b73ca28fa3d2475

Make the following changes to your existing project:

New Files

• Directorystatic-analysis

  • static-analysis.cabal
  • Directoryapp

    • Main.hs
    • Common.hs
    • IntervalUtils.hs
    • ParityUtils.hs
  • Directoryfix

    • Program.fix
    • IntervalAnalysis.fix
    • ParityAnalysis.fix

Add two files to your project:

1. app/ParityUtils.hs: utilities for the parity analysis, similar to app/IntervalUtils.hs.
2. fix/ParityAnalysis.fix: the parity analysis itself.

---

Cabal configuration

static-analysis.cabal

cabal-version:      3.0
name:               static-analysis
version:            0.1.0.0
build-type:         Simple
common warnings
    ghc-options: -Wall
executable static-analysis
    import:           warnings
    main-is:          Main.hs
    other-modules:    Common
                    , IntervalAnalysis
                    , IntervalUtils
                    , ParityAnalysis
                    , ParityUtils
    build-depends:    base
                    , pqueue
                    , unordered-containers
                    , hashable
                    , lattices
    hs-source-dirs:   app
    default-language: GHC2021

Add the two modules for the parity analysis to your project.

---

Utilities

app/ParityUtils.hs

{-# LANGUAGE OverlappingInstances #-}

module ParityUtils where

import Algebra.Lattice
import Algebra.PartialOrd
import Common
import Data.HashMap.Strict (HashMap)
import Data.HashMap.Strict qualified as HashMap
import Data.List (intercalate)

data Parity = PBot | Even | Odd | PTop
  deriving (Eq, Show)

instance Show (HashMap String Parity) where
  show m = "{ " ++ intercalate ", " (fmap (\(k, v) -> k ++ ": " ++ show v) (HashMap.toList m)) ++ " }"

instance PartialOrd Parity where
  leq PBot _ = True
  leq _ PTop = True
  leq PTop _ = False
  leq _ PBot = False
  x `leq` y = x == y

instance Lattice Parity where
  PTop \/ _ = PTop
  _ \/ PTop = PTop
  PBot \/ x = x
  x \/ PBot = x
  x \/ y
    | x == y = x
    | otherwise = PTop

  PBot /\ _ = PBot
  _ /\ PBot = PBot
  PTop /\ x = x
  x /\ PTop = x
  x /\ y
    | x == y = x
    | otherwise = PBot

-- Easy lookups for parities in state
lookupParity :: String -> HashMap String Parity -> Parity
lookupParity = HashMap.lookupDefault PBot

-- Evaluates an expression, giving a parity.
evalP :: Expr -> HashMap String Parity -> Parity
evalP (Id x) st = lookupParity x st
evalP (Num i) _ = if even i then Even else Odd
evalP (Plus e e') st = case (evalP e st, evalP e' st) of
  (Even, Odd) -> Odd
  (Odd, Even) -> Odd
  (Odd, Odd) -> Even
  (Even, Even) -> Even
  (PBot, _) -> PBot
  (_, PBot) -> PBot
  _ -> PTop
evalP _ _ = PBot

-- Evaluates a condition, giving a BBool.
evalCondP :: Expr -> HashMap String Parity -> BBool
evalCondP (Eq x e) st = case (lookupParity x st, evalP e st) of
  (Even, Odd) -> BFalse
  (Odd, Even) -> BFalse
  (PBot, _) -> BBot
  (_, PBot) -> BBot
  _ -> BTop
evalCondP (Leq _ _) _ = BTop
evalCondP _ _ = BBot

-- Refines parities assuming a condition is true.
refineTP :: Expr -> HashMap String Parity -> HashMap String Parity
refineTP (Eq x e) st =
  let p = evalP e st
   in HashMap.insert x (lookupParity x st /\ p) st
refineTP _ st = st

-- Refines parities assuming a condition is false.
refineFP :: Expr -> HashMap String Parity -> HashMap String Parity
refineFP (Eq x e) st =
  let p = if evalP e st == Even then Odd else Even
   in HashMap.insert x (lookupParity x st /\ p) st
refineFP _ st = st

The utilities for the parity analysis mirror app/IntervalUtils.hs. All of these operate over the parity lattice (notice that it is essentially identical to the BBool lattice).

---

Analysis

fix/ParityAnalysis.fix

module ParityAnalysis where

import Algebra.PartialOrd
import Algebra.Lattice
import Common
import ParityUtils

include "Program"

lat StateP where
  type = HashMap String Parity
  leq  = leq
  join = (\/)
  meet = (/\)

rel StateBeforeP: Label, StateP

rule assignInitP: Assign l _ _   |- StateBeforeP l HashMap.empty
rule branchInitP: Branch l _ _ _ |- StateBeforeP l HashMap.empty
rule varInitP:    Var l _        |- StateBeforeP l HashMap.empty

rule assignStepP: Assign l x e, Seq l l', StateBeforeP l st
                  |- StateBeforeP l' (HashMap.insert x (evalP e st) st)

rule branchTrueP: Branch l e t _, StateBeforeP l st,
                  if BTrue `leq` (evalCondP e st)
                  |- StateBeforeP t (refineTP e st)

rule branchFalseP: Branch l e _ f, StateBeforeP l st,
                   if BFalse `leq` (evalCondP e st)
                   |- StateBeforeP f (refineFP e st)

query stateBeforeP: StateBeforeP + -

The actual parity analysis is virtually identical to the interval analysis, except that it operates over the parity lattice.

---

Driver

app/Main.hs

module Main where

import Common
import IntervalAnalysis
import Numeric.Natural
import ParityAnalysis

main :: IO ()
main = do
  let facts =
        [ Var 0 "v"
        , Seq 0 1
        , Assign 1 "v" (Num 1)
        , Seq 1 2
        , Branch 2 (Leq "v" (Num 9)) 3 5
        , Assign 3 "v" (Plus (Id "v") (Num 2))
        , Seq 3 2
        , Branch 5 (Eq "v" (Num 11)) 6 101
        , Assign 6 "v" (Num 0)
        , Seq 6 101
        , Var 101 "END"
        ]
      db = solve facts
  (label :: Natural) <- readLn
  print (stateBeforeI label db)
  print (stateBeforeP label db)

Modify the driver program to emit StateBeforeP facts.

---

In Progress

Notice that most of the Fixen code written for the parity analysis is identical to the interval analysis. Support for rule templates/schema are underway.

Build and run the project, and observe the parity of v at crucial portions of the program:

1. Compile the parity analysis into a Haskell module.

   Terminal

    ~/static-analysis $ fixen --output app/ParityAnalysis.hs fix/ParityAnalysis.fix

2. Run the program, and supplying labels like 2, 5 and 101:

   Terminal

   ~/static-analysis $ cabal run
   2
   [StateBeforeP 2 { v: Odd }]
   ~/static-analysis $ cabal run
   5
   [StateBeforeP 5 { v: Odd }]
   ~/static-analysis $ cabal run
   101
   [StateBeforeP 101 { v: Even }]

It works! Particularly, we see that exiting the loop at program label 5, v remains Odd. This means that the interval for v at that same program point can be reduced from to , allowing us to conclude that the false branch of the if statement is never visited, so v must be exactly equal 0 at the end of the program!

The Reduced Product Problem

Now that we have everything set up, we compose the interval and parity analysis and perform a state reduction via a rule.

Download: naive-reduced-product.tar.gz

SHA-256: 94c192b4364c5946272da698ba6e7e7479da762d743051993284f8b0f6a485ee

Make the following changes to the project:

New Files

• Directorystatic-analysis

  • static-analysis.cabal
  • Directoryapp

    • Main.hs
    • Common.hs
    • IntervalUtils.hs
    • ParityUtils.hs
    • ReducedProductUtils.hs
  • Directoryfix

    • Program.fix
    • IntervalAnalysis.fix
    • ParityAnalysis.fix
    • ReducedProduct.fix

Add two files to your project:

1. app/ReducedProductUtils.hs contains definitions needed to perform the state reduction
2. fix/ReducedProduct.fix contains the union of the interval and parity analyses, along with a rule for state reduction.

Cabal Configuration

static-analysis.cabal

cabal-version:      3.0
name:               static-analysis
version:            0.1.0.0
build-type:         Simple
common warnings
    ghc-options: -Wall
executable static-analysis
    import:           warnings
    main-is:          Main.hs
    other-modules:    Common
                    , IntervalUtils
                    , ParityAnalysis
                    , ParityUtils
                    , ReducedProduct
                    , ReducedProductUtils
    build-depends:    base
                    , pqueue
                    , unordered-containers
                    , hashable
                    , lattices
    hs-source-dirs:   app
    default-language: GHC2021

Add the two modules for the parity analysis to your project.

Utilities

app/ReducedProductUtils.hs

module ReducedProductUtils where

import Data.HashMap.Strict (HashMap)
import Data.HashMap.Strict qualified as HashMap
import IntervalUtils
import ParityUtils

reducedExchangeI
  :: HashMap String Parity
  -> HashMap String Interval
  -> HashMap String Interval
reducedExchangeI st st' = HashMap.fromList $ do
  (v, int) <- HashMap.toList st'
  return $ case int of
    Pair a b -> case lookupParity v st of
      Odd ->
        let a' = if even a then a + 1 else a
            b' = if even b then b - 1 else b
         in (v, a' ... b')
      Even ->
        let a' = if odd a then a + 1 else a
            b' = if odd b then b - 1 else b
         in (v, a' ... b')
      PBot -> (v, IBot)
      _ -> (v, int)
    _ -> (v, int)

The reducedExchangeI function modifies the interval states by checking against the parity states. Essentially, it refines interval bounds based on the parity of the variable.

Analysis

fix/ReducedProduct.fix

module ReducedProduct where

include "IntervalAnalysis"
include "ParityAnalysis"

import ReducedProductUtils

rule reducedExchangeI: StateBeforeP l st, StateBeforeI l st'
                       |- StateBeforeI l (reducedExchangeI st st')

The reduced product obtains the union of the interval analysis and the parity analysis. This is done simply by include-ing the individual analyses into the program. The state reduction is performed via the reducedExchangeI rule, which invokes the reducedExchangeI function defined in our utilities file.

Driver

module Main where

import Common
import Numeric.Natural
import ParityAnalysis
import ReducedProduct

main :: IO ()
main = do
  let facts =
        [ Var 0 "v"
        , Seq 0 1
        , Assign 1 "v" (Num 1)
        , Seq 1 2
        , Branch 2 (Leq "v" (Num 9)) 3 5
        , Assign 3 "v" (Plus (Id "v") (Num 2))
        , Seq 3 2
        , Branch 5 (Eq "v" (Num 11)) 6 101
        , Assign 6 "v" (Num 0)
        , Seq 6 101
        , Var 101 "END"
        ]
      db = solve facts
  (label :: Natural) <- readLn
  print (stateBeforeI label db)
  print (stateBeforeP label db)

Now, modify the driver to use the reduced product analysis. Since the reduced product performs both the interval analysis and the parity analysis, we can query both StateBeforeI and StateBeforeP facts at the end of the analysis.

---

Build and run the project, and observe the interval and parity of v at crucial portions of the program:

1. Compile the reduced product analysis into a Haskell module.

   Terminal

    ~/static-analysis $ fixen --output app/ReducedProduct.hs fix/ReducedProduct.fix

2. Run the program, and supplying labels like 2, 5 and 101:

   Terminal

   ~/static-analysis $ cabal run
   2
   [StateBeforeI 2 { v: [1, 11] }]
   [StateBeforeP 2 { v: Odd }]
   ~/static-analysis $ cabal run
   5
   [StateBeforeI 5 { v: [10, 11] }]
   [StateBeforeP 5 { v: Odd }]
   ~/static-analysis $ cabal run
   101
   [StateBeforeI 101 { v: [0, 10] }]
   [StateBeforeP 101 { v: Even }]

Notice that our state reduction is completely inert. This is because even if the state reduction rule derives the tighter interval [11, 11] at program point 5 (since v is Odd at that program point), the over-approximated [10, 11] from the interval analysis rules subsumes it. The solver drops the refined fact as redundant work, and continues with the transfer functions using the over-approximated states!

Our actual intention of defining the reduced product is to post-compose the domain reduction rule onto the original rules from our analyses, before committing the StateBeforeI facts back into the database. Essentially, if we let the original analyses rules be organized as a function and the domain reduction rule as a function , then one step of fact inference should be , not . What we require is a way to compose sets of rules so that we can modularly and meaningfully compose non-disjoint programs.

Phases of Execution

Fixen supports phases of execution. Phases stratify the fact database into independent databases, . Facts in different databases do not subsume each other. Phases are assigned a set of rules. Phase rules draw premises only from the database, , and commits their conclusions only to the database, . This stratified architecture is illustrated in Figure 1. The result is that phase 0 facts are the results of the composition of phase , phase , …, down to phase rules.

Figure 1. Illustration of N-phase program.

Let us post-compose our state reduction rules onto the original analysis rules. We do so using a phases declaration, describing a list of sets of rules:

fix/ReducedProduct.fix

module ReducedProduct where

include "IntervalAnalysis"
include "ParityAnalysis"

import ReducedProductUtils

rule reducedExchangeI: StateBeforeP l st, StateBeforeI l st'
                       |- StateBeforeI l (reducedExchangeI st st')
rule reducedExchangeP: StateBeforeP l st |- StateBeforeP l st

phases: [ * , { reducedExchangeP, reducedExchangeI } ]

This makes our reduced product program consist of two phases:

1. Phase 0 (*): the wildcard * captures all rules not explicitly listed in the phases declaration. In our program, these are the transfer functions/rules defined in IntervalAnalysis.fix and ParityAnalysis.fix.
2. Phase 1: the exchange rules that refine intervals using parity states. Note that we additionally define a reducedExchangeP rule which forwards parity states from phase 1 back to phase 0 untouched, since parity states should remain invariant across phase 1. If we do not have this, then no StateBeforeP facts make it back to phase 0 for subsequent transfers.

The architecture result of this declaration is illustrated in Figure 2. The phase 0 rules (the interval and parity transfer functions) draw premises from the phase 0 database () and stream their unrefined conclusions to the phase 1 database (). The phase 1 rules (the state reduction/exchange rules) consume these unrefined states from , apply the cross-domain refinements, and route the tighter facts back to . Wider, unrefined facts and narrower, refined facts never coexist within the same database.

Note

Initial facts are, by default, considered as premiseless phase rules. The result is that the initial facts are committed to the phase 0 database.

Figure 2. Phases for the reduced product.

Phases In Action

Download: reduced-product.tar.gz

SHA-256: d23ee25b25ed63dcccd1ffc2f11d879868a8ebc31ec4bd59ba656ac9640828af

Let us run the proper reduced-product analysis and observe the outputs:

1. Recompile fix/ReducedProduct.fix:

   Terminal

    ~/static-analysis $ fixen --output app/ReducedProduct.hs fix/ReducedProduct.fix

2. Now that we are using a multi-phase architecture, the result of fixed-point solving is a pair of databases. As such, the generated query functions also receive a phase selector for you to decide which database you want to query from. We want the refined facts, so we query from phase 0:

   app/Main.hs

   module Main where
   
   import Common
   import Numeric.Natural
   import ReducedProduct
   
   main :: IO ()
   main = do
     let facts =
           [ Var 0 "v"
           , Seq 0 1
           , Assign 1 "v" (Num 1)
           , Seq 1 2
           , Branch 2 (Leq "v" (Num 9)) 3 5
           , Assign 3 "v" (Plus (Id "v") (Num 2))
           , Seq 3 2
           , Branch 5 (Eq "v" (Num 11)) 6 101
           , Assign 6 "v" (Num 0)
           , Seq 6 101
           , Var 101 "END"
           ]
         db = solve facts
     (label :: Natural) <- readLn
     print (stateBeforeI label db)
     print (stateBeforeP label db)
     print (stateBeforeI label db Phase0)
     print (stateBeforeP label db Phase0)

3. Run the program, and supplying labels like 2, 5 and 101:

   Terminal

   ~/static-analysis $ cabal run
   2
   [StateBeforeI 2 { v: [1, 11] }]
   [StateBeforeP 2 { v: Odd }]
   ~/static-analysis $ cabal run
   5
   [StateBeforeI 5 { v: [11, 11] }]
   [StateBeforeP 5 { v: Odd }]
   ~/static-analysis $ cabal run
   101
   [StateBeforeI 101 { v: [0, 0] }]
   [StateBeforeP 101 { v: Even }]

Success!

Tip

1. Not every rule must be used in a phases declaration. A rule can occur multiple times in a phases declaration.
2. You can have any positive number of phases. For instance, you can perform widening after state reduction by appending a ruleset of widening rules after your state reduction ruleset.
3. phases declarations are optional. By default, every program has phases: [*] declared.
4. There can only be one phases declaration per program. phases are not imported via include statements.

Note

Phases are not strictly necessary for defining the reduced product. An alternative is to redefine all the original rules and manually post-compose state-reduction operations. However, phases allow users to compose rulesets modularly without having to re-define individual Fixen programs.

Key Properties

• Monotonicity is preserved: the overall fixed-point computation remains monotone despite the multi-phase architecture.
• State stratification: facts in different databases are independent, preventing subsumption between refined and unrefined facts.
• Modular composition: individual analyses or rule sets can be developed independently and composed via phases.

Summary

• include imports every declaration (except priorities and phases) of a Fixen program into the current program being defined. The argument to the include keyword is a relative filepath of the Fixen program to include.
• Phases stratify the fact database into independent databases, cycling through them during execution.
• Rules in phase read from write to .
• The * wildcard captures all unassigned rules.
• Phases enable post-composition of rule sets, supporting the modular composition of non-disjoint programs.
• This is essential for patterns like the reduced product of abstract interpretations, where cross-domain refinement must bypass subsumption.

---

Footnotes

1. Antoine Miné et al. 2017. Tutorial on static inference of numeric invariants by abstract interpretation. Foundations and Trends® in Programming Languages 4, 3—4(2017), 120—372. ↩