Abstract Interpretation (2/2)
Martin Kellogg

Reading quiz: abstract interpretation

Reading quiz: abstract interpretation● today’s quiz is on paper, and also covers the topics of last week’sclass● you have 15 minutes to complete it. When you’re ﬁnished, bringit to Kazi in the back.
● you may use any hand-written notes that you took during lastclass
○ this includes notes on a tablet or similar, if you wrote themwith a stylus■ but I will be looking over your shoulder if you do :)Agenda: abstract interpretation, part 2
●
●
●
●
●
●

review and clariﬁcations from last week
more on soundness
reﬁnement and branching
widening
Stein’s algorithm example
analysis implementation demoAgenda: abstract interpretation, part 2
●
●
●
●
●
●

review and clariﬁcations from last week
more on soundness
reﬁnement and branching
widening
Stein’s algorithm example
analysis implementation demo

Review: deﬁnitions

Review: deﬁnitions
An abstract interpretation formally has two components:

Review: deﬁnitions
An abstract interpretation formally has two components:● an abstract domain over which to reason, which is composed of:Review: deﬁnitions
An abstract interpretation formally has two components:● an abstract domain over which to reason, which is composed of:○ a set of abstract values

Review: deﬁnitions
An abstract interpretation formally has two components:● an abstract domain over which to reason, which is composed of:○ a set of abstract values○ an ordering operation (e.g., LUB)

Review: deﬁnitions
An abstract interpretation formally has two components:● an abstract domain over which to reason, which is composed of:○ a set of abstract values○ an ordering operation (e.g., LUB)
○ together these form a lattice

Review: deﬁnitions
An abstract interpretation formally has two components:● an abstract domain over which to reason, which is composed of:○ a set of abstract values○ an ordering operation (e.g., LUB)
○ together these form a lattice● a set of transfer functions that tell the abstract interpreter how
to reason over that abstract domain

Review: deﬁnitions
An abstract interpretation formally has two components:● an abstract domain over which to reason, which is composed of:○ a set of abstract values○ an ordering operation (e.g., LUB)
○ together these form a lattice● a set of transfer functions that tell the abstract interpreter how
to reason over that abstract domain○ one for each kind of operation in the underlying
programming language (e.g., one for +, one for -, etc.)

Review: deﬁnitions
An abstract interpretation formally has two components:● an abstract domain over which to reason, which is composed of:○ a set of abstract values○ an ordering operation (e.g., LUB)
○ together these form a lattice● a set of transfer functions that tell the abstract interpreter how
to reason over that abstract domain○ one for each kind of operation in the underlying
programming language (e.g., one for +, one for -, etc.)○ usually represented as tables

Concrete vs abstract domains

Concrete vs abstract domains● the concrete domain of a variable is the set of values that thevariable might actually take on during execution

Concrete vs abstract domains● the concrete domain of a variable is the set of values that thevariable might actually take on during execution

concretedomainConcrete vs abstract domains● the concrete domain of a variable is the set of values that thevariable might actually take on during execution● an abstract domain is a layer of indirection on top of the concrete
domain that splits it into a smaller number of sets
concretedomainConcrete vs abstract domains● the concrete domain of a variable is the set of values that thevariable might actually take on during execution● an abstract domain is a layer of indirection on top of the concrete
domain that splits it into a smaller number of sets
concretedomainabstract
domainConcrete vs abstract domains● the concrete domain of a variable is the set of values that thevariable might actually take on during execution● an abstract domain is a layer of indirection on top of the concrete
domain that splits it into a smaller number of sets
concretedomainabstract
domainαConcrete vs abstract domains● the concrete domain of a variable is the set of values that thevariable might actually take on during execution● an abstract domain is a layer of indirection on top of the concrete
domain that splits it into a smaller number of sets
concretedomainγ
αabstract
domainReview: abstract vs concrete interpretation

Concrete state

concrete
execution

Concrete stateReview: abstract vs concrete interpretation

Concrete state
abstraction
function (α)
Abstract state

concrete
execution

Concrete stateReview: abstract vs concrete interpretation

Concrete state
abstraction
function (α)
Abstract state

concrete
executiontransferfunctionsConcrete state

Abstract stateReview: abstract vs concrete interpretation

Concrete state
abstraction
function (α)
Abstract state

concrete
executiontransferfunctionsConcrete state
concretization
function (γ)
Abstract stateReview: abstract vs concrete interpretation

Concrete state
abstraction
function (α)
Abstract state

concrete
executiontransferfunctionsConcrete state
concretization
function (γ)
Abstract statesoundness means that the green path is a subset of the orange path

Review: clariﬁcations

Review: clariﬁcations● last week, I went through an extended example of how to get aparity analysis to work on one programReview: clariﬁcations● last week, I went through an extended example of how to get aparity analysis to work on one program○ however, that was just an example!
■ an abstract interpretation is applicable to any programReview: clariﬁcations● last week, I went through an extended example of how to get aparity analysis to work on one program○ however, that was just an example!
■ an abstract interpretation is applicable to any program○ one of the key challenges in abstract interpretation design isﬁguring out the right set of examples to handle precisely

Review: clariﬁcations● last week, I went through an extended example of how to get aparity analysis to work on one program○ however, that was just an example!
■ an abstract interpretation is applicable to any program○ one of the key challenges in abstract interpretation design isﬁguring out the right set of examples to handle precisely■ when you’re implementing your divide-by-zero analysis, I
strongly recommend that you write out some examples
as test cases!
● you can just add them to the existing test

Agenda: abstract interpretation, part 2
●
●
●
●
●
●

review and clariﬁcations from last week
more on soundness
reﬁnement and branching
widening
Stein’s algorithm example
analysis implementation demoMore on soundness: using a Galois connection

Concrete state
abstraction
function (α)
Abstract state

concrete
executiontransferfunctionsConcrete state
concretization
function (γ)
Abstract statesoundness means that the green path is a subset of the orange pathMore on soundness: using a Galois connection● how would we actually show that a particular abstract
interpretation is sound?

More on soundness: using a Galois connection● how would we actually show that a particular abstract
interpretation is sound?
● here’s an algorithm for doing so:More on soundness: using a Galois connection● how would we actually show that a particular abstract
interpretation is sound?
● here’s an algorithm for doing so:○ for each transfer function Top for some operation op:

More on soundness: using a Galois connection● how would we actually show that a particular abstract
interpretation is sound?
● here’s an algorithm for doing so:○ for each transfer function Top for some operation op:■ prove that for all concrete states c:More on soundness: using a Galois connection● how would we actually show that a particular abstract
interpretation is sound?
● here’s an algorithm for doing so:○ for each transfer function Top for some operation op:■ prove that for all concrete states c:
op(c) ⊆ γ(Top(α(c)))

More on soundness: using a Galois connection● how would we actually show that a particular abstract
interpretation is sound?
● here’s an algorithm for doing so:○ for each transfer function Top for some operation op:■ prove that for all concrete states c:
op(c) ⊆ γ(Top(α(c)))

possible results of concrete
execution (green line)

More on soundness: using a Galois connection● how would we actually show that a particular abstract
interpretation is sound?
● here’s an algorithm for doing so:○ for each transfer function Top for some operation op:■ prove that for all concrete states c:
op(c) ⊆ γ(Top(α(c)))
concretization

More on soundness: using a Galois connection● how would we actually show that a particular abstract
interpretation is sound?
● here’s an algorithm for doing so:○ for each transfer function Top for some operation op:■ prove that for all concrete states c:
op(c) ⊆ γ(Top(α(c)))
concretization of the result of applying
the transfer functionMore on soundness: using a Galois connection● how would we actually show that a particular abstract
interpretation is sound?
● here’s an algorithm for doing so:○ for each transfer function Top for some operation op:■ prove that for all concrete states c:
op(c) ⊆ γ(Top(α(c)))
concretization of the result of applying
the transfer function to the abstraction of
the original concrete stateMore on soundness: using a Galois connection● how would we actually show that a particular abstract
interpretation is sound?
● here’s an algorithm for doing so:○ for each transfer function Top for some operation op:■ prove that for all concrete states c:
op(c) ⊆ γ(Top(α(c)))
concretization of the result of applying
the transfer function to the abstraction of
the original concrete state (orange line)

More on soundness: example proof● let’s carry out an example proof using this technique ourselves on
the plus transfer function from our simple parity analysis

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● let’s carry out an example proof using this technique ourselves on
the plus transfer function from our simple parity analysis

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● let’s carry out an example proof using this technique ourselves on
the plus transfer function from our simple parity analysis{ even, odd } = top/\{even}{odd}\/{} = bottom

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● let’s carry out an example proof using this technique ourselves on
the plus transfer function from our simple parity analysis+{ even, odd } = top/\{even}{odd}\/{} = bottomTeven odd

丄

T

丄

T

even odd

丄

odd

T

odd even

丄

丄

丄

丄

丄

T

T

even

T

丄

More on soundness: example proof● Let’s ﬁrst dispense with the easy cases:

op(c) ⊆ γ(Top(α(c)))

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Let’s ﬁrst dispense with the easy cases:○ if the transfer function entry is top, then it’s easy:

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Let’s ﬁrst dispense with the easy cases:○ if the transfer function entry is top, then it’s easy:■ ∀ c. op(c) ⊆ { all integers } is trivially true!

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Let’s ﬁrst dispense with the easy cases:+
T evenodd
丄then it’s easy:○ if the transfer
functionentry
is top,■ ∀ c. op(c) ⊆ { all integers } is trivially true!
T
T
T
T
丄
even

T

even odd

丄

odd

T

odd even

丄

丄

丄

丄

丄

丄

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Let’s ﬁrst dispense with the easy cases:+
T evenodd
丄then it’s easy:○ if the transfer
functionentry
is top,■ ∀ c. op(c) ⊆ { all integers } is trivially true!
T
T
T
T
丄
even

T

even odd

丄

odd

T

odd even

丄

丄

丄

丄

丄

丄

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Let’s ﬁrst dispense with the easy cases:○ if the transfer function entry is top, then it’s easy:■ ∀ c. op(c) ⊆ { all integers } is trivially true!
○ if the transfer function entry is bottom, it’s still pretty easy:

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Let’s ﬁrst dispense with the easy cases:○ if the transfer function entry is top, then it’s easy:■ ∀ c. op(c) ⊆ { all integers } is trivially true!
○ if the transfer function entry is bottom, it’s still pretty easy:■ for every entry in our transfer function that’s bottom, oneof the inputs is also bottom

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Let’s ﬁrst dispense with the easy cases:○ if the transfer function entry is top, then it’s easy:■ ∀ c. op(c) ⊆ { all integers } is trivially true!
○ if the transfer function entry is bottom, it’s still pretty easy:■ for every entry in our transfer function that’s bottom, oneof the inputs is also bottom■ op({}) is always the empty set (it can’t be executed)

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Let’s ﬁrst dispense with the easy cases:○ if the transfer function entry is top, then it’s easy:■ ∀ c. op(c) ⊆ { all integers } is trivially true!
○ if the transfer function entry is bottom, it’s still pretty easy:■ for every entry in our transfer function that’s bottom, oneof the inputs is also bottom■ op({}) is always the empty set (it can’t be executed)■ {} ⊆ {}More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Let’s ﬁrst dispense with the easy cases:○ if the transfer function entry is top, then it’s easy:■ ∀ c. op(c) ⊆ { all integers } is trivially true!
○ if the transfer function entry is bottom, it’s still pretty easy:■ for every entry in our transfer function that’s bottom, oneof the inputs is also bottom■ op({}) is always the empty set (it can’t be executed)■ {} ⊆ {}■ QEDMore on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Let’s ﬁrst dispense with the easy cases:+
T evenodd
丄then it’s easy:○ if the transfer
functionentry
is top,■ ∀ c. op(c) ⊆ { all integers } is trivially true!
T
T
T
T
丄
○ if the transfer function entry is bottom, it’s still pretty easy:■ forevenevery entry
our transfer
function that’s bottom, one
T in
even
odd 丄
of the inputs is also bottom■ op({})is always
empty
set (it丄can’t be executed)
odd
T the
odd
even
■ {} ⊆ {}丄丄丄丄■ QED丄

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Let’s ﬁrst dispense with the easy cases:+
T evenodd
丄then it’s easy:○ if the transfer
functionentry
is top,■ ∀ c. op(c) ⊆ { all integers } is trivially true!
T
T
T
T
丄
○ if the transfer function entry is bottom, it’s still pretty easy:■ forevenevery entry
our transfer
function that’s bottom, one
T in
even
odd 丄
of the inputs is also bottom■ op({})is always
empty
set (it丄can’t be executed)
odd
T the
odd
even
■ {} ⊆ {}丄丄丄丄■ QED丄

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Now we need to handle the more complex cases in the middle

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Now we need to handle the more complex cases in the middle○ we could do them one-by-one…

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Now we need to handle the more complex cases in the middle○ we could do them one-by-one…
○ but we can skip some because addition is commutative■ so we don’t need to worry about orderMore on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Now we need to handle the more complex cases in the middle+ do them
T one-by-one…
even odd 丄○ we could○ but we can skip some because addition is commutative
T
T
T
T
丄
■ so we don’t need to worry about ordereven

Teven odd

丄

odd

T

odd even

丄

丄

丄

丄

丄

丄

in other words, thetwo orange cases
are the same!

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Now we need to handle the more complex cases in the middle○ we could do them one-by-one…
○ but we can skip some because addition is commutative■ so we don’t need to worry about order● So, we have three cases to deal with:

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Now we need to handle the more complex cases in the middle○ we could do them one-by-one…
○ but we can skip some because addition is commutative■ so we don’t need to worry about order● So, we have three cases to deal with:
1. even integer + even integer is an even integer
2. odd integer + odd integer is an even integer
3. odd integer + even integer is an odd integer

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Now we need to handle the more complex cases in the middle○ we could do them one-by-one…
○ but we can skip some because addition is commutative■ so we don’t need to worry about order● So, we have three cases to deal with:
1. even integer + even integer is an even integer
2. odd integer + odd integer is an even integer
3. odd integer + even integer is an odd integer● we dispatch these three by considering each case individually○ they’re all basically the same, so we’re only going to do oneMore on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● Now we need to handle the more complex cases in the middle○ we could do them one-by-one…
○ but we can skip some because addition is commutative■ so we don’t need to worry about order● So, we have three cases to deal with:
1. even integer + even integer is an even integer
2. odd integer + odd integer is an even integer
3. odd integer + even integer is an odd integer● we dispatch these three by considering each case individually○ they’re all basically the same, so we’re only going to do oneMore on soundness: example proof● c is some addition statement x + y

op(c) ⊆ γ(Top(α(c)))

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● c is some addition statement x + y○ we know that concretely x is odd and y is even (why?)■ formally, we would state this as x % 2 = 1 and y % 2 = 0

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● c is some addition statement x + y○ we know that concretely x is odd and y is even (why?)■ formally, we would state this as x % 2 = 1 and y % 2 = 0● what is op(c)?

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● c is some addition statement x + y○ we know that concretely x is odd and y is even (why?)■ formally, we would state this as x % 2 = 1 and y % 2 = 0● what is op(c)?
○ represent x as 2a + 1 and y as 2b for some a, b (how?)More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● c is some addition statement x + y○ we know that concretely x is odd and y is even (why?)■ formally, we would state this as x % 2 = 1 and y % 2 = 0● what is op(c)?
○ represent x as 2a + 1 and y as 2b for some a, b (how?)○ 2a + 1 + 2b = 2(a+b) + 1, which we can easily prove is the set of
all odd integers

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● c is some addition statement x + y○ we know that concretely x is odd and y is even (why?)■ formally, we would state this as x % 2 = 1 and y % 2 = 0● what is op(c)?
○ represent x as 2a + 1 and y as 2b for some a, b (how?)○ 2a + 1 + 2b = 2(a+b) + 1, which we can easily prove is the set of
all odd integers● what’s α(c)?

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● c is some addition statement x + y○ we know that concretely x is odd and y is even (why?)■ formally, we would state this as x % 2 = 1 and y % 2 = 0● what is op(c)?
○ represent x as 2a + 1 and y as 2b for some a, b (how?)○ 2a + 1 + 2b = 2(a+b) + 1, which we can easily prove is the set of
all odd integers● what’s α(c)?
○ α(x) is odd (the abstract value), and α(y) is even (the AV)

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● c is some addition statement x + y○ we know that concretely x is odd and y is even (why?)■ formally, we would state this as x % 2 = 1 and y % 2 = 0● what is op(c)?
○ represent x as 2a + 1 and y as 2b for some a, b (how?)○ 2a + 1 + 2b = 2(a+b) + 1, which we can easily prove is the set of
all odd integers● what’s α(c)?
○ α(x) is odd (the abstract value), and α(y) is even (the AV)● T+(α(c)) is just applying our transfer function: result is the odd AV

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● c is some addition statement x + y○ we know that concretely x is odd and y is even (why?)■ formally, we would state this as x % 2 = 1 and y % 2 = 0● what is op(c)?
○ represent x as 2a + 1 and y as 2b for some a, b (how?)○ 2a + 1 + 2b = 2(a+b) + 1, which we can easily prove is the set of
all odd integers● what’s α(c)?
○ α(x) is odd (the abstract value), and α(y) is even (the AV)● T+(α(c)) is just applying our transfer function: result is the odd AV● γ(odd) is the set of all odd integers, which does contain itself

More on soundness: example proof

op(c) ⊆ γ(Top(α(c)))● c is some addition statement x + y○ we know that concretely x is odd and y is even (why?)■ formally, we would state this as x % 2 = 1 and y % 2 = 0● what is op(c)?
○ represent x as 2a + 1 and y as 2b for some a, b (how?)○ 2a + 1 + 2b = 2(a+b) + 1, which we can easily prove is the set of
all odd integers● what’s α(c)?
○ α(x) is odd (the abstract value), and α(y) is even (the AV)● T+(α(c)) is just applying our transfer function: result is the odd AV● γ(odd) is the set of all odd integers, which does contain itself

Agenda: abstract interpretation, part 2
●
●
●
●
●
●

review and clariﬁcations from last week
more on soundness
reﬁnement and branching
widening
Stein’s algorithm example
analysis implementation demo

Reﬁnement
Consider the following program:
x = 0
while (x < 3):x = x + 1
print xReﬁnement
Consider the following program:
x = 0
while (x < 3):x = x + 1
print xWhat value is printed?

Reﬁnement
Consider the following program:
x = 0
while (x < 3):x = x + 1
print xWhat value is printed?
How do you know?

Reﬁnement
Consider the following program:
x = 0
while (x < 3):x = x + 1
print xWhat value is printed?
How do you know?
Insight: anything you can ﬁgureout by reasoning through theprogram by hand, an abstract
interpretation can do too!

Reﬁnement
Consider the following program:
x = 0
while (x < 3):x = x + 1
print xtop
… -2 -1 0

1bottom2…

Reﬁnement
Consider the following program:
x = 0
while (x < 3):x = x + 1
print xtop
… -2 -1 0

1

2…

bottomnot enough! need sets

Reﬁnement
Consider the following program:
x = 0
while (x < 3):x = x + 1
print xdraw in the correct
lattice here:Reﬁnementdraw in the correct
lattice here:
top

Consider the following program:
x = 0
while (x < 3):x = x + 1
print x… {-1, 0}{0, 1}… -2 -1 0

1

…
2

…

bottom(actually need to extend this to 4 layers,
but there’s not room on the slide)Reﬁnementdraw in the correct
lattice here:
top

Consider the following program:
x = 0
while (x < 3):x = x + 1
print xDoes this permit us to provethe value of x at the end?

… {-1, 0}{0, 1}… -2 -1 0

1

…
2

…

bottom(actually need to extend this to 4 layers,
but there’s not room on the slide)Reﬁnementdraw in the correct
lattice here:
top

Consider the following program:
x = 0
while (x < 3):x = x + 1
print xDoes this permit us to provethe value of x at the end?
NO (need transfer function)… {-1, 0}{0, 1}… -2 -1 0

1

…
2

…

bottom(actually need to extend this to 4 layers,
but there’s not room on the slide)Reﬁnement● We need a transfer function for branchingReﬁnement● We need a transfer function for branching○ when we exit the while loop, we know the loop guard is false

Reﬁnement● We need a transfer function for branching○ when we exit the while loop, we know the loop guard is false● These transfer functions are called reﬁnements because they
typically involve a greatest lower boundReﬁnement● We need a transfer function for branching○ when we exit the while loop, we know the loop guard is false● These transfer functions are called reﬁnements because they
typically involve a greatest lower bound○ a reﬁnement rules out some possible states

Reﬁnement● We need a transfer function for branching○ when we exit the while loop, we know the loop guard is false● These transfer functions are called reﬁnements because they
typically involve a greatest lower bound○ a reﬁnement rules out some possible states● Reﬁnements are deﬁned over the boolean operators of thelanguage

Reﬁnement● We need a transfer function for branching○ when we exit the while loop, we know the loop guard is false● These transfer functions are called reﬁnements because they
typically involve a greatest lower bound○ a reﬁnement rules out some possible states● Reﬁnements are deﬁned over the boolean operators of thelanguage○ for our example, we need a reﬁnement for >=Reﬁnement● We need a transfer function for branching○ when we exit the while loop, we know the loop guard is false● These transfer functions are called reﬁnements because they
typically involve a greatest lower bound○ a reﬁnement rules out some possible states● Reﬁnements are deﬁned over the boolean operators of thelanguage○ for our example, we need a reﬁnement for >=○ why >= and not < ?

Reﬁnement● We need a transfer function for branching○ when we exit the while loop, we know the loop guard is false● These transfer functions are called reﬁnements because they
typically involve a greatest lower bound○ a reﬁnement rules out some possible states● Reﬁnements are deﬁned over the boolean operators of thelanguage○ for our example, we need a reﬁnement for >=○ why >= and not < ?
■ loop guard is false, so we invert the operator

Reﬁnement
Consider the following program:
x = 0
while (x < 3):x = x + 1
print x(on the whiteboard. Start by drawing a CFG, then execute the algorithm. Put the CFG to the side and don’t erase it.)

Widening● What if we want to build a bigger constant propagation lattice?

Widening● What if we want to build a bigger constant propagation lattice?
○ the previous example only worked because we knew that weonly needed at most 4 values at a timeWidening● What if we want to build a bigger constant propagation lattice?
○ the previous example only worked because we knew that weonly needed at most 4 values at a time○ in the real world, we don’t know how many values we’ll needfor any given program!

Widening● What if we want to build a bigger constant propagation lattice?
○ the previous example only worked because we knew that weonly needed at most 4 values at a time○ in the real world, we don’t know how many values we’ll needfor any given program!
○ it would be nice if we could have sets of arbitrary sizeWidening● What if we want to build a bigger constant propagation lattice?
○ the previous example only worked because we knew that weonly needed at most 4 values at a time○ in the real world, we don’t know how many values we’ll needfor any given program!
○ it would be nice if we could have sets of arbitrary size
■ and we shouldn’t need to reimplement our analysis eachtime we need to reason about differently-sized sets

Widening● What if we want to build a bigger constant propagation lattice?
○ the previous example only worked because we knew that weonly needed at most 4 values at a time○ in the real world, we don’t know how many values we’ll needfor any given program!
○ it would be nice if we could have sets of arbitrary size
■ and we shouldn’t need to reimplement our analysis eachtime we need to reason about differently-sized sets
○ do you think that’s possible?

Widening● What if we want to build a bigger constant propagation lattice?
○ the previous example only worked because we knew that weonly needed at most 4 values at a time○ in the real world, we don’t know how many values we’ll needfor any given program!
○ it would be nice if we could have sets of arbitrary size
■ and we shouldn’t need to reimplement our analysis eachtime we need to reason about differently-sized sets
○ do you think that’s possible?
■ We can use widening operators to allow this (sort of)WideningDeﬁnition: a widening operator is a predeﬁned policy to take aparticular upper bound if the abstract value at a particular location
has changed too many times

WideningDeﬁnition: a widening operator is a predeﬁned policy to take aparticular upper bound if the abstract value at a particular location
has changed too many times● effectively, this guarantees termination by bounding the numberof times that a particular value can change, even if the lattice is of
inﬁnite sizeWideningDeﬁnition: a widening operator is a predeﬁned policy to take aparticular upper bound if the abstract value at a particular location
has changed too many times● effectively, this guarantees termination by bounding the numberof times that a particular value can change, even if the lattice is of
inﬁnite size
● this is safe because the analysis isn’t required to take the least
upper bound so long as it chooses an upper boundWideningDeﬁnition: a widening operator is a predeﬁned policy to take aparticular upper bound if the abstract value at a particular location
has changed too many times● effectively, this guarantees termination by bounding the numberof times that a particular value can change, even if the lattice is of
inﬁnite size
● this is safe because the analysis isn’t required to take the least
upper bound so long as it chooses an upper bound● example widening operator for constant propagation:○ if an abstract value has changed at least ﬁve times, go to top

WideningLet’s return to the previous example:
x = 0
while (x < 3):x = x + 1
print xWideningLet’s return to the previous example:
x = 0
while (x < 3 10):x = x + 1
print xWidening● The main advantage of widening is that it permits lattices with
inﬁnite heightWidening● The main advantage of widening is that it permits lattices with
inﬁnite height● The downside is that it introduces additional imprecision○ but abstract interpretation was always imprecise, so that’sokayWidening● The main advantage of widening is that it permits lattices with
inﬁnite height● The downside is that it introduces additional imprecision○ but abstract interpretation was always imprecise, so that’sokay● A nice fact about implementing an abstract interpretation is that
it is always safe to apply a widening operator

Widening● The main advantage of widening is that it permits lattices with
inﬁnite height● The downside is that it introduces additional imprecision○ but abstract interpretation was always imprecise, so that’sokay● A nice fact about implementing an abstract interpretation is that
it is always safe to apply a widening operator○ this means it’s easy to support complex language features: just
immediately widen any values that they impact■ “go to top” is a sound policy in all situations

Agenda: abstract interpretation, part 2
●
●
●
●
●
●

review and clariﬁcations from last week
more on soundness
reﬁnement and branching
widening
Stein’s algorithm example
analysis implementation demoAnother example: Stein’s algorithm
def gcd(int a, int b):
if a == 0 or b == 0:
return 0
int expt = 0
while a is even and b is even:a = a / 2b = b / 2
expt = expt + 1
while a != b:
if a is even: a = a / 2
elif b is even: b = b / 2
elif a > b: a = (a - b) / 2
else: b = (b - a) / 2
return a * 2^exptAnother example: Stein’s algorithm
def gcd(int a, int b):
if a == 0 or b == 0:
return 0
int expt = 0
while a is even and b is even:a = a / 2b = b / 2
expt = expt + 1
while a != b:
if a is even: a = a / 2
elif b is even: b = b / 2
elif a > b: a = (a - b) / 2
else: b = (b - a) / 2
return a * 2^expt

First question: does thisprogram ever divide by zero?
Take a moment and discuss.

Another example: Stein’s algorithm
def gcd(int a, int b):
if a == 0 or b == 0:
return 0
int expt = 0
while a is even and b is even:a = a / 2b = b / 2
expt = expt + 1
while a != b:
if a is even: a = a / 2
elif b is even: b = b / 2
elif a > b: a = (a - b) / 2
else: b = (b - a) / 2
return a * 2^expt

First question: does thisprogram ever divide by zero?
Take a moment and discuss.
Answer: deﬁnitely not!

Another example: Stein’s algorithm
def gcd(int a, int b):
if a == 0 or b == 0:
return 0
int expt = 0
while a is even and b is even:a = a / 2b = b / 2
expt = expt + 1
while a != b:
if a is even: a = a / 2
elif b is even: b = b / 2
elif a > b: a = (a - b) / 2
else: b = (b - a) / 2
return a * 2^expt

First question: does thisprogram ever divide by zero?
Take a moment and discuss.
Answer: deﬁnitely not!
● all divisions are by 2
○ 2 != 0Another example: Stein’s algorithm
def gcd(int a, int b):
if a == 0 or b == 0:
return 0
int expt = 0
while a is even and b is even:a = a / 2b = b / 2
expt = expt + 1
while a != b:
if a is even: a = a / 2
elif b is even: b = b / 2
elif a > b: a = (a - b) / 2
else: b = (b - a) / 2
return a * 2^expt

First question: does thisprogram ever divide by zero?
Take a moment and discuss.
Answer: deﬁnitely not!
● all divisions are by 2
○ 2 != 0● “constant propagation”
can prove no divisions byzero!

Another example: Stein’s algorithm
def gcd(int a, int b):
if a == 0 or b == 0:
return 0
int expt = 0
while a is even and b is even:a = a / 2b = b / 2
expt = expt + 1
while a != b:
if a is even: a = a / 2
elif b is even: b = b / 2
elif a > b: a = (a - b) / 2
else: b = (b - a) / 2
return a * 2^expt

First
Nextquestion:question:does
doesthis
this
programdivide byprogramever
terminate
onzero?
allTakea moment
discuss.
inputs?
Take a andmomentanddiscuss. (Hint: draw a CFG.)

Another example: Stein’s algorithm
def gcd(int a, int b):
if a == 0 or b == 0:
return 0
int expt = 0
while a is even and b is even:a = a / 2b = b / 2
expt = expt + 1
while a != b:
if a is even: a = a / 2
elif b is even: b = b / 2
elif a > b: a = (a - b) / 2
else: b = (b - a) / 2
return a * 2^expt

First
Nextquestion:question:does
doesthis
this
programdivide byprogramever
terminate
onzero?
allTakea moment
discuss.
inputs?
Take a andmomentanddiscuss. (Hint: draw a CFG.)
To prove termination, we needto show that both while loop
guards are eventually false.

Another example: Stein’s algorithm
def gcd(int a, int b):
if a == 0 or b == 0:
return 0
int expt = 0
while a is even and b is even:a = a / 2b = b / 2
expt = expt + 1
while a != b:
if a is even: a = a / 2
elif b is even: b = b / 2
elif a > b: a = (a - b) / 2
else: b = (b - a) / 2
return a * 2^expt

First
Nextquestion:question:does
doesthis
this
programdivide byprogramever
terminate
onzero?
allTakea moment
discuss.
inputs?
Take a andmomentanddiscuss. (Hint: draw a CFG.)
To prove termination, we needto show that both while loop
guards are eventually false.
● 1st: a is odd or b is odd

Another example: Stein’s algorithm
def gcd(int a, int b):
if a == 0 or b == 0:
return 0
int expt = 0
while a is even and b is even:a = a / 2b = b / 2
expt = expt + 1
while a != b:
if a is even: a = a / 2
elif b is even: b = b / 2
elif a > b: a = (a - b) / 2
else: b = (b - a) / 2
return a * 2^expt

First
Nextquestion:question:does
doesthis
this
programdivide byprogramever
terminate
onzero?
allTakea moment
discuss.
inputs?
Take a andmomentanddiscuss. (Hint: draw a CFG.)
To prove termination, we needto show that both while loop
guards are eventually false.
● 1st: a is odd or b is odd● 2nd: a eventually equals b

Another example: Stein’s algorithm: parity
def gcd(int a, int b):
if a == 0 or b == 0:
return 0
int expt = 0
while a is even and b is even:a = a / 2b = b / 2
expt = expt + 1
while a != b:
if a is even: a = a / 2
elif b is even: b = b / 2
elif a > b: a = (a - b) / 2
else: b = (b - a) / 2
return a * 2^expt

Fortunately, we already know ananalysis for parity. Let’s use it (onthe board; requires a CFG).

Another example: Stein’s algorithm: parity
def gcd(int a, int b):
if a == 0 or b == 0:
return 0
int expt = 0
while a is even and b is even:a = a / 2b = b / 2
expt = expt + 1
while a != b:
if a is even: a = a / 2
elif b is even: b = b / 2
elif a > b: a = (a - b) / 2
else: b = (b - a) / 2
return a * 2^expt

Fortunately, we already know ananalysis for parity. Let’s use it (onthe board; requires a CFG).
● we ran into a problem: wecan’t prove that a and b are
eventually odd!
○ the transfer function foreven / is2 returns TAnother example: Stein’s algorithm: parity
def gcd(int a, int b):
if a == 0 or b == 0:
return 0
int expt = 0
while a is even and b is even:a = a / 2b = b / 2
expt = expt + 1
while a != b:
if a is even: a = a / 2
elif b is even: b = b / 2
elif a > b: a = (a - b) / 2
else: b = (b - a) / 2
return a * 2^expt

Fortunately, we already know ananalysis for parity. Let’s use it (onthe board; requires a CFG).
● we ran into a problem: wecan’t prove that a and b are
eventually odd!
○ the transfer function foreven / is2 returns T● in this case, that’s actuallycorrect!
○ the program does not
terminate on all inputs○ -1, 1 is a counterexample

Agenda: abstract interpretation, part 2
●
●
●
●
●
●

review and clariﬁcations from last week
more on soundness
reﬁnement and branching
widening
Stein’s algorithm example
analysis implementation demo

Course announcements● This week’s homework is individual (you may not work with apartner)○ this is a difference from previous homeworks!
● early next week I will send out a survey (via Discord) about what
topic we should cover in the last week of class (April 25)○ please give this some serious thought!
○ the survey will be open until next week’s class, and I will
announce the result during class