From Coq Require Import Arith ZArith Psatz Bool String List FMaps Recdef.
Require Import Sequences IMP.
Local Open Scope string_scope.
Local Open Scope Z_scope.
Local Open Scope list_scope.
8. An optimization: constant propagation
8.1 Simplifying expressions using smart constructors
mk_PLUS_CONST a n produces an expression equivalent to PLUS a (CONST n)
but further simplified.
Function mk_PLUS_CONST (
a:
aexp) (
n:
Z) :
aexp :=
if n =? 0
then a else
match a with
|
CONST m =>
CONST (
m +
n)
|
PLUS a (
CONST m) =>
PLUS a (
CONST (
m +
n))
|
_ =>
PLUS a (
CONST n)
end.
We use Function instead of Definition because Function produces
a nicer case analysis principle, with exactly one case per line
of the matching. This simplifies the proofs of correctness.
mk_PLUS a1 a2 produces a simplified expression equivalent to PLUS a1 a2.
It uses associativity and commutativity to find the pattern
"an expression plus a constant", then uses mk_PLUS_CONST to simplify
further.
Function mk_PLUS (
a1 a2:
aexp) :
aexp :=
match a1,
a2 with
|
CONST m,
_ =>
mk_PLUS_CONST a2 m
|
_,
CONST m =>
mk_PLUS_CONST a1 m
|
PLUS a1 (
CONST m1),
PLUS a2 (
CONST m2) =>
mk_PLUS_CONST (
PLUS a1 a2) (
m1 +
m2)
|
PLUS a1 (
CONST m1),
_ =>
mk_PLUS_CONST (
PLUS a1 a2)
m1
|
_,
PLUS a2 (
CONST m2) =>
mk_PLUS_CONST (
PLUS a1 a2)
m2
|
_,
_ =>
PLUS a1 a2
end.
mk_MINUS a1 a2 produces an expression equivalent to MINUS a1 a2
using similar tricks. Note that "expression minus constant" is
always normalized into "expression plus opposite constant",
simplifying the case analyses.
Function mk_MINUS (
a1 a2:
aexp) :
aexp :=
match a1,
a2 with
|
_,
CONST m =>
mk_PLUS_CONST a1 (-
m)
|
PLUS a1 (
CONST m1),
PLUS a2 (
CONST m2) =>
mk_PLUS_CONST (
MINUS a1 a2) (
m1 -
m2)
|
PLUS a1 (
CONST m1),
_ =>
mk_PLUS_CONST (
MINUS a1 a2)
m1
|
_,
PLUS a2 (
CONST m2) =>
mk_PLUS_CONST (
MINUS a1 a2) (-
m2)
|
_,
_ =>
MINUS a1 a2
end.
To simplify an expression, we rewrite it bottom-up, applying the smart
constructors at each step.
Fixpoint simplif_aexp (
a:
aexp) :
aexp :=
match a with
|
CONST n =>
CONST n
|
VAR x =>
VAR x
|
PLUS a1 a2 =>
mk_PLUS (
simplif_aexp a1) (
simplif_aexp a2)
|
MINUS a1 a2 =>
mk_MINUS (
simplif_aexp a1) (
simplif_aexp a2)
end.
An example:
Compute (
simplif_aexp (
MINUS (
PLUS (
VAR "
x") (
CONST 1)) (
PLUS (
VAR "
y") (
CONST 1)))).
Result is: MINUS (VAR "x") (VAR "y").
To show the soundness of these simplifications, we show that the
optimized expressions evaluate to the same values as the original expressions.
Lemma mk_PLUS_CONST_sound:
forall s a n,
aeval s (
mk_PLUS_CONST a n) =
aeval s a +
n.
Proof.
intros.
functional induction (
mk_PLUS_CONST a n).
-
assert (
n = 0)
by (
apply Z.eqb_eq;
auto).
lia.
-
auto.
-
cbn.
lia.
-
auto.
Qed.
Lemma mk_PLUS_sound:
forall s a1 a2,
aeval s (
mk_PLUS a1 a2) =
aeval s a1 +
aeval s a2.
Proof.
Lemma mk_MINUS_sound:
forall s a1 a2,
aeval s (
mk_MINUS a1 a2) =
aeval s a1 -
aeval s a2.
Proof.
Lemma simplif_aexp_sound:
forall s a,
aeval s (
simplif_aexp a) =
aeval s a.
Proof.
We can play the same game for Boolean expressions.
Here are the smart constructors and their proofs of correctness.
Function mk_EQUAL (
a1 a2:
aexp) :
bexp :=
match a1,
a2 with
|
CONST n1,
CONST n2 =>
if n1 =?
n2 then TRUE else FALSE
|
PLUS a1 (
CONST n1),
CONST n2 =>
EQUAL a1 (
CONST (
n2 -
n1))
|
_,
_ =>
EQUAL a1 a2
end.
Function mk_LESSEQUAL (
a1 a2:
aexp) :
bexp :=
match a1,
a2 with
|
CONST n1,
CONST n2 =>
if n1 <=?
n2 then TRUE else FALSE
|
PLUS a1 (
CONST n1),
CONST n2 =>
LESSEQUAL a1 (
CONST (
n2 -
n1))
|
_,
_ =>
LESSEQUAL a1 a2
end.
Function mk_NOT (
b:
bexp) :
bexp :=
match b with
|
TRUE =>
FALSE
|
FALSE =>
TRUE
|
NOT b =>
b
|
_ =>
NOT b
end.
Function mk_AND (
b1 b2:
bexp) :
bexp :=
match b1,
b2 with
|
TRUE,
_ =>
b2
|
_,
TRUE =>
b1
|
FALSE,
_ =>
FALSE
|
_,
FALSE =>
FALSE
|
_,
_ =>
AND b1 b2
end.
Lemma mk_EQUAL_sound:
forall s a1 a2,
beval s (
mk_EQUAL a1 a2) = (
aeval s a1 =?
aeval s a2).
Proof.
Lemma mk_LESSEQUAL_sound:
forall s a1 a2,
beval s (
mk_LESSEQUAL a1 a2) = (
aeval s a1 <=?
aeval s a2).
Proof.
Lemma mk_NOT_sound:
forall s b,
beval s (
mk_NOT b) =
negb (
beval s b).
Proof.
intros.
functional induction (
mk_NOT b);
cbn.
-
auto.
-
auto.
-
rewrite negb_involutive.
auto.
-
auto.
Qed.
Lemma mk_AND_sound:
forall s b1 b2,
beval s (
mk_AND b1 b2) =
beval s b1 &&
beval s b2.
Proof.
Exercise (2 stars, recommended)
Write a simplification function for Boolean expressions and prove its soundness.
Fixpoint simplif_bexp (
b:
bexp) :
bexp :=
b.
Lemma simplif_bexp_sound:
forall s b,
beval s (
simplif_bexp b) =
beval s b.
Proof.
Abort.
Exercise (2-3 stars, optional)
Can you think of other algebraic simplifications on arithmetic and
Boolean expressions that would be beneficial? By this, I mean that
the compiler would produce shorter code for the simplified expression.
Try to add them to the smart constructors and update their proofs
accordingly.
Even commands can benefit from smart constructors! Here is a smart
IFTHENELSE and a smart WHILE that take known conditions into account.
Function mk_IFTHENELSE (
b:
bexp) (
c1 c2:
com) :
com :=
match b with
|
TRUE =>
c1
|
FALSE =>
c2
|
_ =>
IFTHENELSE b c1 c2
end.
Function mk_WHILE (
b:
bexp) (
c:
com) :
com :=
match b with
|
FALSE =>
SKIP
|
_ =>
WHILE b c
end.
Lemma cexec_mk_IFTHENELSE:
forall s1 b c1 c2 s2,
cexec s1 (
if beval s1 b then c1 else c2)
s2 ->
cexec s1 (
mk_IFTHENELSE b c1 c2)
s2.
Proof.
Lemma cexec_mk_WHILE_done:
forall s1 b c,
beval s1 b =
false ->
cexec s1 (
mk_WHILE b c)
s1.
Proof.
Lemma cexec_mk_WHILE_loop:
forall b c s1 s2 s3,
beval s1 b =
true ->
cexec s1 c s2 ->
cexec s2 (
mk_WHILE b c)
s3 ->
cexec s1 (
mk_WHILE b c)
s3.
Proof.
8.2 A static analysis for constant propagation
Require Import FMaps.
The static analysis we need operates over finite maps from variables (strings)
to values (integers). Coq's standard library provides a rich, efficient
implementation of finite sets and finite maps. Before being able to use it, however,
we must provide it with a Coq module equipping the type of strings
with a decidable equality. The implementation of this module follows.
Module Ident_Decidable <:
DecidableType with Definition t :=
ident.
Definition t :=
ident.
Definition eq (
x y:
t) :=
x =
y.
Definition eq_refl := @
eq_refl t.
Definition eq_sym := @
eq_sym t.
Definition eq_trans := @
eq_trans t.
Definition eq_dec :=
string_dec.
End Ident_Decidable.
We then instantiate the finite maps modules from Coq's standard library
with strings as the type of keys.
Module IdentMap :=
FMapWeakList.Make(
Ident_Decidable).
Module IMFact :=
FMapFacts.WFacts(
IdentMap).
Module IMProp :=
FMapFacts.WProperties(
IdentMap).
Our static analysis is going to compute "abstract stores", that is,
compile-time approximations of run-time stores. This is an instance
of the general theory of abstract interpretation.
(Notational convention: we use Capitalized identifiers to refer to
abstract things and lowercase identifiers to refer to concrete things.)
Abstract stores Store are represented as finite maps from variable names
to integers. If a variable x is mapped to n, it means that
we statically know that the run-time value of x is n. If x is not mapped,
it means that the run-time value of x can be anything.
This meaning is captured by the matches s s' predicate below,
which says whether a concrete store s belongs to an
abstract store s' obtained by static analysis.
(A bit like a term belongs to a type in a type system.)
Definition Store :=
IdentMap.t Z.
Definition matches (
s:
store) (
S:
Store):
Prop :=
forall x n,
IdentMap.find x S =
Some n ->
s x =
n.
Abstract stores have a lattice structure, with an order Le, a top element,
and a join operation. We can also test whether two abstract stores are equal.
Definition Le (
S1 S2:
Store) :
Prop :=
forall x n,
IdentMap.find x S2 =
Some n ->
IdentMap.find x S1 =
Some n.
Definition Top :
Store :=
IdentMap.empty Z.
Definition Join_aux (
N1 N2:
option Z):
option Z :=
match N1,
N2 with
|
Some n1,
Some n2 =>
if n1 =?
n2 then Some n1 else None
|
_,
_ =>
None
end.
Definition Join (
S1 S2:
Store) :
Store :=
IdentMap.map2 Join_aux S1 S2.
Definition Equal (
S1 S2:
Store) :
bool :=
IdentMap.equal Z.eqb S1 S2.
We show the soundness of these lattice operations with respect to
the matches and the Le relations.
Lemma matches_Le:
forall s S1 S2,
Le S1 S2 ->
matches s S1 ->
matches s S2.
Proof.
Lemma Le_Top:
forall S,
Le S Top.
Proof.
Lemma Join_characterization:
forall S1 S2 x n,
IdentMap.find x (
Join S1 S2) =
Some n <->
IdentMap.find x S1 =
Some n /\
IdentMap.find x S2 =
Some n.
Proof.
unfold Join;
intros.
rewrite IMFact.map2_1bis by auto.
unfold Join_aux.
split.
-
intros.
destruct (
IdentMap.find x S1)
as [
n1|];
try discriminate.
destruct (
IdentMap.find x S2)
as [
n2|];
try discriminate.
destruct (
n1 =?
n2)
eqn:
E;
try discriminate.
assert (
n1 =
n2)
by (
apply Z.eqb_eq;
auto).
split;
congruence.
-
intros [
FIND1 FIND2].
rewrite FIND1,
FIND2.
rewrite Z.eqb_refl.
auto.
Qed.
Lemma Le_Join_l:
forall S1 S2,
Le S1 (
Join S1 S2).
Proof.
Lemma Le_Join_r:
forall S1 S2,
Le S2 (
Join S1 S2).
Proof.
Lemma Equal_Le:
forall S1 S2,
Equal S1 S2 =
true ->
Le S1 S2.
Proof.
The abstract, compile-time evaluation of expressions returns Some v
if the value v of the expression can be determined based on what
the abstract store S tells us about the values of variables.
Otherwise, None is returned.
Definition lift1 {
A B:
Type} (
f:
A ->
B) (
o:
option A) :
option B :=
match o with Some x =>
Some (
f x) |
None =>
None end.
Definition lift2 {
A B C:
Type} (
f:
A ->
B ->
C) (
o1:
option A) (
o2:
option B) :
option C :=
match o1,
o2 with Some x1,
Some x2 =>
Some (
f x1 x2) |
_,
_ =>
None end.
Fixpoint Aeval (
S:
Store) (
a:
aexp) :
option Z :=
match a with
|
CONST n =>
Some n
|
VAR x =>
IdentMap.find x S
|
PLUS a1 a2 =>
lift2 Z.add (
Aeval S a1) (
Aeval S a2)
|
MINUS a1 a2 =>
lift2 Z.sub (
Aeval S a1) (
Aeval S a2)
end.
Fixpoint Beval (
S:
Store) (
b:
bexp) :
option bool :=
match b with
|
TRUE =>
Some true
|
FALSE =>
Some false
|
EQUAL a1 a2 =>
lift2 Z.eqb (
Aeval S a1) (
Aeval S a2)
|
LESSEQUAL a1 a2 =>
lift2 Z.leb (
Aeval S a1) (
Aeval S a2)
|
NOT b1 =>
lift1 negb (
Beval S b1)
|
AND b1 b2 =>
lift2 andb (
Beval S b1) (
Beval S b2)
end.
These compile-time evaluations are sound, in the following sense.
Lemma Aeval_sound:
forall s S,
matches s S ->
forall a n,
Aeval S a =
Some n ->
aeval s a =
n.
Proof.
intros s S AG;
induction a;
cbn;
intros.
-
congruence.
-
apply AG;
auto.
-
destruct (
Aeval S a1)
as [
n1|];
destruct (
Aeval S a2)
as [
n2|];
try discriminate.
cbn in H;
inversion H.
f_equal;
auto.
-
destruct (
Aeval S a1)
as [
n1|];
destruct (
Aeval S a2)
as [
n2|];
try discriminate.
cbn in H;
inversion H.
f_equal;
auto.
Qed.
Lemma Beval_sound:
forall s S,
matches s S ->
forall b n,
Beval S b =
Some n ->
beval s b =
n.
Proof.
intros s S AG;
induction b;
cbn;
intros.
-
congruence.
-
congruence.
-
destruct (
Aeval S a1)
as [
n1|]
eqn:
A1;
destruct (
Aeval S a2)
as [
n2|]
eqn:
A2;
try discriminate.
cbn in H;
inversion H.
erewrite !
Aeval_sound by eauto.
auto.
-
destruct (
Aeval S a1)
as [
n1|]
eqn:
A1;
destruct (
Aeval S a2)
as [
n2|]
eqn:
A2;
try discriminate.
cbn in H;
inversion H.
erewrite !
Aeval_sound by eauto.
auto.
-
destruct (
Beval S b)
as [
n1|];
cbn in H;
inversion H.
f_equal;
auto.
-
destruct (
Beval S b1)
as [
n1|];
destruct (
Beval S b2)
as [
n2|];
try discriminate.
cbn in H;
inversion H.
f_equal;
auto.
Qed.
To analyze assignments, we need to update abstract stores with the result
of Aeval.
Definition Update (
x:
ident) (
N:
option Z) (
S:
Store) :
Store :=
match N with
|
None =>
IdentMap.remove x S
|
Some n =>
IdentMap.add x n S
end.
Lemma Update_characterization:
forall S x N y,
IdentMap.find y (
Update x N S) =
if string_dec x y then N else IdentMap.find y S.
Proof.
Lemma matches_update:
forall s S x n N,
matches s S ->
(
forall i,
N =
Some i ->
n =
i) ->
matches (
update x n s) (
Update x N S).
Proof.
To analyze loops, we will need to find fixpoints of a function from
abstract states to abstract states. Intuitively, this corresponds
to executing the loop in the abstract, stopping iterations when the
abstract state is stable.
Computing exact fixpoints with guaranteed termination is not easy;
we will return to this question at the end of the lectures.
In the meantime, we will use the simple, approximate algorithm below,
which stops after a fixed number of iterations and returns Top
if no fixpoint has been found earlier.
Fixpoint fixpoint_rec (
F:
Store ->
Store) (
fuel:
nat) (
S:
Store) :
Store :=
match fuel with
|
O =>
Top
|
S fuel =>
let S' :=
F S in
if Equal S'
S then S else fixpoint_rec F fuel S'
end.
Let's say that we will do at most 20 iterations.
Definition num_iter := 20%
nat.
Definition fixpoint (
F:
Store ->
Store) (
init_S:
Store) :
Store :=
fixpoint_rec F num_iter init_S.
The result S of fixpoint F is sound, in that it satisfies
F S <= S in the lattice ordering.
Lemma fixpoint_sound:
forall F init_S,
let S :=
fixpoint F init_S in Le (
F S)
S.
Proof.
Now we can analyze commands by executing them "in the abstract".
Given an abstract store S that represents what we statically know
about the values of the variables before executing command c,
cexec' returns an abstract store that describes the values of
the variables after executing c.
Fixpoint Cexec (
S:
Store) (
c:
com) :
Store :=
match c with
|
SKIP =>
S
|
ASSIGN x a =>
Update x (
Aeval S a)
S
|
SEQ c1 c2 =>
Cexec (
Cexec S c1)
c2
|
IFTHENELSE b c1 c2 =>
match Beval S b with
|
Some true =>
Cexec S c1
|
Some false =>
Cexec S c2
|
None =>
Join (
Cexec S c1) (
Cexec S c2)
end
|
WHILE b c1 =>
fixpoint (
fun x =>
Join S (
Cexec x c1))
S
end.
The soundness of the analysis follows.
Ltac inv H :=
inversion H;
clear H;
subst.
Lemma Cexec_sound:
forall c s1 s2 S1,
cexec s1 c s2 ->
matches s1 S1 ->
matches s2 (
Cexec S1 c).
Proof.
Exercise (3 stars, optional)
Extend the analysis to take advantage of equality tests against constants.
For example, in the following program,
if x = 0
then y = x + 1
else y = 1
we could notice that
x = 0 in the "then" branch, hence
y = 1 at
the end of both branches. To this end, write a function
Binvert S b that returns a pair of abstract stores
S1, S0,
where
S1 is
S enriched from equalities that hold when
b
evaluates to
true, and
S0 is
S enriched from equalities that
hold when
b evaluates to
false. Then use
Binvert to refine
the analysis of
IFTHENELSE and
WHILE.
Exercise (4 stars, optional)
Modify the static analysis to infer variation intervals instead of
constant values. Abstract stores map variables to pairs
(lo,hi)
of two integers, meaning that the concrete value of the variable is
between
lo and
hi inclusive:
Definition matches (s: store) (S: Store) : Prop :=
forall x lo hi, IdentMap.find x S = Some (lo, hi) -> lo <= s x <= hi.
(You could also support special values "minus infinity" for
lo
and "infinity" for
hi.)
Adapt the operations over abstract stores and the abstract interpreters
for expressions and commands accordingly.
8.3 The constant propagation optimization
We can use the results of the static analysis to simplify expressions
further, replacing variables with known values by these values, then
applying the smart constructors.
Fixpoint cp_aexp (
S:
Store) (
a:
aexp) :
aexp :=
match a with
|
CONST n =>
CONST n
|
VAR x =>
match IdentMap.find x S with Some n =>
CONST n |
None =>
VAR x end
|
PLUS a1 a2 =>
mk_PLUS (
cp_aexp S a1) (
cp_aexp S a2)
|
MINUS a1 a2 =>
mk_MINUS (
cp_aexp S a1) (
cp_aexp S a2)
end.
Fixpoint cp_bexp (
S:
Store) (
b:
bexp) :
bexp :=
match b with
|
TRUE =>
TRUE
|
FALSE =>
FALSE
|
EQUAL a1 a2 =>
mk_EQUAL (
cp_aexp S a1) (
cp_aexp S a2)
|
LESSEQUAL a1 a2 =>
mk_LESSEQUAL (
cp_aexp S a1) (
cp_aexp S a2)
|
NOT b =>
mk_NOT (
cp_bexp S b)
|
AND b1 b2 =>
mk_AND (
cp_bexp S b1) (
cp_bexp S b2)
end.
Under the assumption that the concrete store matchess with the abstract store,
these optimized expressions evaluate to the same values as the original
expressions.
Lemma cp_aexp_sound:
forall s S,
matches s S ->
forall a,
aeval s (
cp_aexp S a) =
aeval s a.
Proof.
intros s S AG;
induction a;
cbn.
-
auto.
-
destruct (
IdentMap.find x S)
as [
n|]
eqn:
FIND.
+
symmetry.
apply AG.
auto.
+
auto.
-
rewrite mk_PLUS_sound,
IHa1,
IHa2.
auto.
-
rewrite mk_MINUS_sound,
IHa1,
IHa2.
auto.
Qed.
Lemma cp_bexp_sound:
forall s S,
matches s S ->
forall b,
beval s (
cp_bexp S b) =
beval s b.
Proof.
The optimization of commands consists in propagating constants
in expressions and simplifying the expressions, as above.
In addition, conditionals and loops whose conditions are statically
known will be simplified too, thanks to the smart constructors.
The S parameter is the abstract store "before" the execution of c.
When recursing through c, it must be updated like the static analysis
Cexec does. For example, if c is SEQ c1 c2, c2 is optimized
using Cexec S c1 as abstract store "before". Likewise, if
c is a loop WHILE b c1, the loop body c1 is optimized using
Cexec S (WHILE b c1) as the abstract store "before".
Fixpoint cp_com (
S:
Store) (
c:
com) :
com :=
match c with
|
SKIP =>
SKIP
|
ASSIGN x a =>
ASSIGN x (
cp_aexp S a)
|
SEQ c1 c2 =>
SEQ (
cp_com S c1) (
cp_com (
Cexec S c1)
c2)
|
IFTHENELSE b c1 c2 =>
mk_IFTHENELSE (
cp_bexp S b) (
cp_com S c1) (
cp_com S c2)
|
WHILE b c =>
let sfix :=
Cexec S (
WHILE b c)
in
mk_WHILE (
cp_bexp sfix b) (
cp_com sfix c)
end.
Example: let's "optimize" Euclidean division under the dubious assumption
that the divisor is 0...
Compute (
cp_com (
Update "
b" (
Some 0)
Top)
Euclidean_division).
Result is (in pseudocode):
r := a;
q := 0;
while 0 <= r do
r := r; q := q + 1
done
The proof of semantic preservation needs an unusual induction pattern:
structural induction on the command c, plus an inner induction
on the number of iterations if c is a loop WHILE b c1.
This pattern follows closely the structure of the abstract interpreter
Cexec: structural induction on the command + local fixpoint for loops.
Lemma cp_com_correct_terminating:
forall c s1 s2 S1,
cexec s1 c s2 ->
matches s1 S1 ->
cexec s1 (
cp_com S1 c)
s2.
Proof.