Module Analyzer1

Require Import Coq.Program.Equality.
Require Import Imp.
Require Import Semantics.

In this chapter: a generic program analyzer based on abstract interpretation with non-relational domains. A more sophisticated version is presented in chapter Analyzer2.

1. Interface of abstract domains.

The analyzer operates over abstract values: compile-time approximations of sets of integer values. We specify the type of abstract values and the associated operations as a Coq module interface.

Module Type VALUE_ABSTRACTION.

The type of abstract values.
Variable t: Type.

vmatch n v holds if the integer n belongs to the set represented by the abstract value v.

Variable vmatch: nat -> t -> Prop.

Abstract values are naturally ordered by inclusion.
Definition le (v1 v2: t) : Prop :=
forall n, vmatch n v1 -> vmatch n v2.

ble is a boolean function that approximates the le relation.
Variable ble: t -> t -> bool.
Hypothesis ble_1: forall v1 v2, ble v1 v2 = true -> le v1 v2.

of_const n returns the abstract value for the singleton set {n}.
Variable of_const: nat -> t.
Hypothesis of_const_1: forall n, vmatch n (of_const n).

bot represents the empty set of integers.
Variable bot: t.
Hypothesis bot_1: forall n, ~(vmatch n bot).

top represents the set of all integers.
Variable top: t.
Hypothesis top_1: forall n, vmatch n top.

join computes an upper bound (union).
Variable join: t -> t -> t.
Hypothesis join_1:
forall n v1 v2, vmatch n v1 -> vmatch n (join v1 v2).
Hypothesis join_2:
forall n v1 v2, vmatch n v2 -> vmatch n (join v1 v2).

Abstract counterpart of the +, - and * operations.
Variable add: t -> t -> t.
forall n1 n2 v1 v2, vmatch n1 v1 -> vmatch n2 v2 -> vmatch (n1+n2) (add v1 v2).

Variable sub: t -> t -> t.
Hypothesis sub_1:
forall n1 n2 v1 v2, vmatch n1 v1 -> vmatch n2 v2 -> vmatch (n1-n2) (sub v1 v2).

Variable mul: t -> t -> t.
Hypothesis mul_1:
forall n1 n2 v1 v2, vmatch n1 v1 -> vmatch n2 v2 -> vmatch (n1*n2) (mul v1 v2).

End VALUE_ABSTRACTION.

Similarly, we define the interface for abstractions of concrete states.

Module Type STATE_ABSTRACTION.

Declare Module V: VALUE_ABSTRACTION.

Variable t: Type.

Variable get: t -> id -> V.t.
Variable set: t -> id -> V.t -> t.

Definition smatch (st: state) (s: t) : Prop :=
forall x, V.vmatch (st x) (get s x).

Hypothesis set_1:
forall id n st v s,
V.vmatch n v -> smatch st s -> smatch (update st id n) (set s id v).

Definition le (s1 s2: t) : Prop :=
forall st, smatch st s1 -> smatch st s2.

Variable ble: t -> t -> bool.
Hypothesis ble_1: forall s1 s2, ble s1 s2 = true -> le s1 s2.

Variable bot: t.
Hypothesis bot_1: forall s, ~(smatch s bot).

Variable top: t.
Hypothesis top_1: forall s, smatch s top.

Variable join: t -> t -> t.
Hypothesis join_1:
forall st s1 s2, smatch st s1 -> smatch st (join s1 s2).
Hypothesis join_2:
forall st s1 s2, smatch st s2 -> smatch st (join s1 s2).

End STATE_ABSTRACTION.

2. The generic analyzer.

The analyzer is presented as a module parameterized by a value abstraction and a matching state abstraction.

Module Analysis (V: VALUE_ABSTRACTION) (S: STATE_ABSTRACTION with Module V := V).

Computation of a post-fixpoint for an operator F: S.t -> S.t.
Section FIXPOINT.

Variable F: S.t -> S.t.

We use the engineer's approach:
• iterate F a number of times
• stop if an abstract state s is found that satisfies S.le (F s) s and return s;
• if no such state is found after a fixed number of iterations, return S.top.

Fixpoint iter (n: nat) (s: S.t) : S.t :=
match n with
| 0 => S.top
| S n1 =>
let s' := F s in
if S.ble s' s then s else iter n1 s'
end.

Definition num_iter := 10.

Definition fixpoint (s: S.t) : S.t := iter num_iter s.

Lemma fixpoint_ok:
forall s, S.le (F (fixpoint s)) (fixpoint s).
Proof.
unfold fixpoint. generalize num_iter. induction n; simpl; intros.
red. intros. apply S.top_1.
remember (S.ble (F s) s). destruct b.
apply S.ble_1. auto.
apply IHn.
Qed.

End FIXPOINT.

Abstract interpretation of arithmetic expressions.

Fixpoint abstr_eval (s: S.t) (a: aexp) : V.t :=
match a with
| ANum n => V.of_const n
| AId x => S.get s x
| APlus a1 a2 => V.add (abstr_eval s a1) (abstr_eval s a2)
| AMinus a1 a2 => V.sub (abstr_eval s a1) (abstr_eval s a2)
| AMult a1 a2 => V.mul (abstr_eval s a1) (abstr_eval s a2)
end.

Abstract interpretation of commands.

Fixpoint abstr_interp (s: S.t) (c: com) : S.t :=
match c with
| SKIP => s
| (x ::= a) => S.set s x (abstr_eval s a)
| (c1; c2) => abstr_interp (abstr_interp s c1) c2
| IFB b THEN c1 ELSE c2 FI =>
S.join (abstr_interp s c1) (abstr_interp s c2)
| WHILE b DO c END =>
fixpoint (fun x => S.join s (abstr_interp x c)) s
end.

Soundness of the abstract interpretation of arithmetic expressions.

Lemma abstr_eval_sound:
forall st s, S.smatch st s ->
forall a, V.vmatch (aeval st a) (abstr_eval s a).
Proof.
induction a; simpl.
apply V.of_const_1.
apply H.
apply V.sub_1; auto.
apply V.mul_1; auto.
Qed.

Soundness of the abstract interpretation of commands.

Ltac inv H := inversion H; subst; clear H.

Theorem abstr_interp_sound:
forall c st st' s,
S.smatch st s ->
c / st || st' ->
S.smatch st' (abstr_interp s c).
Proof.
induction c; intros st st' s MATCH EVAL; simpl.
Case "skip".
inv EVAL. auto.
Case ":=".
inv EVAL. apply S.set_1. apply abstr_eval_sound. auto. auto.
Case "seq".
inv EVAL.
apply IHc2 with st'0. apply IHc1 with st. auto. auto. auto.
Case "if".
inv EVAL.
SCase "if true".
apply S.join_1. apply IHc1 with st; auto.
SCase "if false".
apply S.join_2. apply IHc2 with st; auto.
Case "while".
set (F := fun x => S.join s (abstr_interp x c)).
set (s' := fixpoint F s).
assert (FIX: S.le (F s') s').
apply fixpoint_ok.
assert (INNER: forall st1 c1 st2,
c1 / st1 || st2 ->
c1 = CWhile b c ->
S.smatch st1 s' ->
S.smatch st2 s').
induction 1; intro EQ; inv EQ; intros.
SCase "while end".
auto.
SCase "while loop".
apply IHceval2; auto.
apply FIX. unfold F. apply S.join_2. apply IHc with st0. auto. auto.

eapply INNER; eauto.
apply FIX. unfold F. apply S.join_1. auto.
Qed.

End Analysis.

3. An implementation of a state abstraction.

Module StateAbstr(VA: VALUE_ABSTRACTION) <: STATE_ABSTRACTION with Module V := VA.

Module V := VA.

We represent abstract states by either:
• All_bot, meaning that all variables have abstract value V.top
• Top_except l, where l is a list of abstract values. The abstract value for variable Id n is the n-th element of this list, if present, or V.top if absent.

Inductive astate : Type :=
| All_bot
| Top_except(l: list V.t).

Definition t := astate.

Fixpoint get_aux (l: list V.t) (x: nat) {struct l} : V.t :=
match l, x with
| nil, _ => V.top
| hd :: tl, O => hd
| hd :: tl, S x1 => get_aux tl x1
end.

Definition get (s: t) (x: id) : V.t :=
match s, x with
| All_bot, _ => V.bot
| Top_except l, Id n => get_aux l n
end.

Definition smatch (st: state) (s: t) : Prop :=
forall x, V.vmatch (st x) (get s x).

Fixpoint set_aux (l: list V.t) (x: nat) (v: V.t) {struct x} : list V.t :=
match l, x with
| nil, O => v :: nil
| nil, S x1 => V.top :: set_aux nil x1 v
| hd :: tl, O => v :: tl
| hd :: tl, S x1 => hd :: set_aux tl x1 v
end.

Definition set (s: t) (x: id) (v: V.t) : t :=
match s, x with
| All_bot, _ => All_bot
| Top_except l, Id n => Top_except(set_aux l n v)
end.

Opaque eq_nat_dec.

Remark get_aux_set_aux_same:
forall v x l,
get_aux (set_aux l x v) x = v.
Proof.
induction x; simpl; intros.
destruct l; auto.
destruct l; simpl; auto.
Qed.

Remark get_aux_set_aux_other:
forall v x y l,
x <> y -> get_aux (set_aux l x v) y = get_aux l y.
Proof.
induction x; intros; simpl.
destruct y. congruence. destruct l; auto.
destruct y.
destruct l; simpl; auto.
destruct l; simpl. rewrite IHx. auto. congruence. apply IHx. congruence.
Qed.

Lemma set_1:
forall x n st v s,
V.vmatch n v -> smatch st s -> smatch (update st x n) (set s x v).
Proof.
intros; red; intros.
unfold get, set. destruct s.
Case "All_bot".
elim (V.bot_1 (st (Id 0))). apply H0.
Case "Top_except".
destruct x; destruct x0.
remember (beq_nat n0 n1). destruct b.
replace n1 with n0. rewrite update_eq. rewrite get_aux_set_aux_same. auto.
apply beq_nat_true; auto.
rewrite update_neq. rewrite get_aux_set_aux_other. apply H0.
apply beq_nat_false; auto.
unfold beq_id. auto.
Qed.

Definition le (s1 s2: t) : Prop :=
forall st, smatch st s1 -> smatch st s2.

Lemma le_1:
forall s1 s2,
(forall x, V.le (get s1 x) (get s2 x)) -> le s1 s2.
Proof.
intros; red; intros; red; intros.
apply (H x (st x)). apply H0.
Qed.

Fixpoint ble_aux (l1 l2: list V.t) {struct l2}: bool :=
match l2, l1 with
| nil, _ => true
| hd2 :: tl2, nil => V.ble V.top hd2 && ble_aux nil tl2
| hd2 :: tl2, hd1 :: tl1 => V.ble hd1 hd2 && ble_aux tl1 tl2
end.

Definition ble (s1 s2: t) : bool :=
match s1, s2 with
| All_bot, _ => true
| Top_except l1, All_bot => false
| Top_except l1, Top_except l2 => ble_aux l1 l2
end.

Lemma ble_aux_get:
forall l2 l1 x,
ble_aux l1 l2 = true ->
V.le (get_aux l1 x) (get_aux l2 x).
Proof.
induction l2; simpl; intros.
red; intros. apply V.top_1.
destruct l1; destruct (andb_prop _ _ H).
destruct x; simpl.
apply V.ble_1; auto.
change VA.top with (get_aux [] x). auto.
destruct x; simpl.
apply V.ble_1; auto.
auto.
Qed.

Lemma ble_1: forall s1 s2, ble s1 s2 = true -> le s1 s2.
Proof.
intros. apply le_1; intros.
destruct x. unfold ble in H. destruct s1; destruct s2; unfold get.
red; intros. elim (V.bot_1 _ H0).
red; intros. elim (V.bot_1 _ H0).
congruence.
apply ble_aux_get; auto.
Qed.

Definition bot : t := All_bot.

Lemma bot_1: forall s, ~(smatch s bot).
Proof.
intros; red; intros.
elim (V.bot_1 (s (Id 0))). apply H.
Qed.

Definition top : t := Top_except nil.

Lemma top_1: forall s, smatch s top.
Proof.
intros; red; intros. destruct x; unfold get; simpl. apply V.top_1.
Qed.

Fixpoint join_aux (l1 l2: list V.t) : list V.t :=
match l1, l2 with
| nil, _ => nil
| _, nil => nil
| hd1 :: tl1, hd2 :: tl2 => V.join hd1 hd2 :: join_aux tl1 tl2
end.

Definition join (s1 s2: t) : t :=
match s1, s2 with
| All_bot, _ => s2
| _, All_bot => s1
| Top_except l1, Top_except l2 => Top_except (join_aux l1 l2)
end.

Lemma join_get_aux:
forall l1 l2 x,
V.le (get_aux l1 x) (get_aux (join_aux l1 l2) x)
/\ V.le (get_aux l2 x) (get_aux (join_aux l1 l2) x).
Proof.
assert (TOP: forall x, V.le x V.top).
intros; red; intros; apply V.top_1.
induction l1; simpl; intros.
auto.
destruct l2; destruct x; simpl; auto.
split; red; intros. apply V.join_1; auto. apply V.join_2; auto.
Qed.

Lemma join_1:
forall st s1 s2, smatch st s1 -> smatch st (join s1 s2).
Proof.
intros; red; intros. unfold join.
destruct s1. elim (bot_1 _ H).
destruct s2. apply H.
destruct x; unfold get.
destruct (join_get_aux l l0 n). apply H0. apply H.
Qed.

Lemma join_2:
forall st s1 s2, smatch st s2 -> smatch st (join s1 s2).
Proof.
intros; red; intros. unfold join.
destruct s1. apply H.
destruct s2. elim (bot_1 _ H).
destruct x; unfold get.
destruct (join_get_aux l l0 n). apply H1. apply H.
Qed.

End StateAbstr.

4. An example of an abstract domain: constant propagation.

Module ConstProp <: VALUE_ABSTRACTION.

Inductive val : Type :=
| Bot (* empty set of values *)
| Inj (n: nat) (* the singleton set {n} *)
| Top. (* all values *)

Definition t := val.

Definition vmatch (n: nat) (v: t) : Prop :=
match v with
| Bot => False
| Inj m => m = n
| Top => True
end.

Definition le (v1 v2: t) : Prop :=
forall n, vmatch n v1 -> vmatch n v2.

Definition ble (v1 v2: t) : bool :=
match v1, v2 with
| Bot, _ => true
| _, Top => true
| Inj m, Inj n => beq_nat m n
| _, _ => false
end.

Lemma ble_1: forall v1 v2, ble v1 v2 = true -> le v1 v2.
Proof.
unfold ble, le, vmatch; intros.
destruct v1.
subst n0. destruct v2. congruence. symmetry; apply beq_nat_true; auto. auto.
destruct v2. congruence. congruence. auto.
Qed.

Definition of_const (n: nat) := Inj n.

Lemma of_const_1: forall n, vmatch n (of_const n).
Proof.
unfold vmatch, of_const; intros. auto.
Qed.

Definition bot := Bot.

Lemma bot_1: forall n, ~(vmatch n bot).
Proof.
unfold bot, vmatch; intros. tauto.
Qed.

Definition top := Top.

Lemma top_1: forall n, vmatch n top.
Proof.
unfold vmatch, top; intros. auto.
Qed.

Definition join (v1 v2: t) : t :=
match v1, v2 with
| Bot, _ => v2
| _, Bot => v1
| Top, _ => Top
| _, Top => Top
| Inj m, Inj n => if beq_nat m n then Inj m else Top
end.

Lemma join_1:
forall n v1 v2, vmatch n v1 -> vmatch n (join v1 v2).
Proof.
unfold vmatch, join; intros.
destruct v1.
subst n0. destruct v2; auto. destruct (beq_nat n n0); auto.
destruct v2; auto.
Qed.

Lemma join_2:
forall n v1 v2, vmatch n v2 -> vmatch n (join v1 v2).
Proof.
unfold vmatch, join; intros.
destruct v2.
subst n0. destruct v1; auto.
remember (beq_nat n0 n). destruct b; auto. apply beq_nat_true; auto.
destruct v1; auto.
Qed.

Definition binop (f: nat -> nat -> nat) (v1 v2: t) : t :=
match v1, v2 with
| Bot, _ => Bot
| _, Bot => Bot
| Top, _ => Top
| _, Top => Top
| Inj m, Inj n => Inj (f m n)
end.

Lemma binop_sound:
forall f n1 n2 v1 v2,
vmatch n1 v1 -> vmatch n2 v2 -> vmatch (f n1 n2) (binop f v1 v2).
Proof.
unfold vmatch, binop; intros.
destruct v1; destruct v2; contradiction || auto.
Qed.

Definition add := binop (fun n1 n2 => n1+n2).
forall n1 n2 v1 v2, vmatch n1 v1 -> vmatch n2 v2 -> vmatch (n1+n2) (add v1 v2).
Proof.
apply binop_sound. Qed.

Definition sub := binop (fun n1 n2 => n1-n2).
Lemma sub_1:
forall n1 n2 v1 v2, vmatch n1 v1 -> vmatch n2 v2 -> vmatch (n1-n2) (sub v1 v2).
Proof.
apply binop_sound. Qed.

Definition mul := binop (fun n1 n2 => n1*n2).
Lemma mul_1:
forall n1 n2 v1 v2, vmatch n1 v1 -> vmatch n2 v2 -> vmatch (n1*n2) (mul v1 v2).
Proof.
apply binop_sound. Qed.

End ConstProp.

We now instantiate our generic analyzer over this domain.

Module SConstProp := StateAbstr(ConstProp).
Module AConstProp := Analysis(ConstProp)(SConstProp).

Notation vx := (Id 0).
Notation vy := (Id 1).
Notation vz := (Id 2).

A sample program:
```    x := 0; y := 100; z := x + y;
while x <= 10 do x := x + 1; y := y - 1 end```
Definition prog1 :=
(vx ::= ANum 0;
vy ::= ANum 100;
vz ::= APlus (AId vx) (AId vy);
WHILE BLe (AId vx) (ANum 10) DO
(vx ::= APlus (AId vx) (ANum 1);
vy ::= AMinus (AId vy) (ANum 1))
END).

Eval vm_compute in (AConstProp.abstr_interp SConstProp.top prog1).

Result is:
`SConstProp.Top_except [ConstProp.Top, ConstProp.Top, ConstProp.Inj 100].`
Or, in other terms: x is Top, y is Top, z is 100.

Exercise (3 stars)

A compiler can exploit the results of the ConstProp analysis to optimize programs:
• Assignments x ::= a can be replaced by x ::= AConst n whenever the analysis tells us that a abstractly evaluates to Inj n.
• The statement IFB b THEN c1 ELSE c2 FI can be replaced by c1 or by c2 if, based on the results of the analysis, we know that b always evaluate to true or to false.
Implement the corresponding program transformation, as a function from commands and initial abstract state to commands:

Fixpoint constprop (s: SConstProp.t) (c: com) : com :=
match c with
| SKIP => SKIP
| (x ::= a) =>
c (* TO BE IMPROVED *)
| (c1; c2) =>
(constprop s c1; constprop (AConstProp.abstr_interp s c1) c2)
| IFB b THEN c1 ELSE c2 FI =>
let c1' := constprop s c1 in
let c2' := constprop s c2 in
IFB b THEN c1' ELSE c2' FI (* TO BE IMPROVED *)
| WHILE b DO c1 END =>
WHILE b DO constprop s c1 END
end.

Then, prove semantic preservation for your optimization:

Theorem constprop_correct_terminating:
forall c st st',
c / st || st' ->
forall s, SConstProp.smatch st s ->
constprop s c / st || st'.
Proof.
induction 1; intros.

Exercise (4 stars)

Taking inspiration from the ConstProp module, define a value abstraction appropriate for parity analysis. Namely, for each variable, we track whether its value is even, or odd, or its parity is unknown.

Require Import Even. (* from Coq's standard library *)

Module Parity. (* an instance of VALUE_ABSTRACTION *)

Inductive parity : Type :=
| Bot (* empty set of integers *)
| Even (* the set of even integers *)
| Odd (* the set of odd integers *)
| Top. (* the set of all integers *)

Definition t := parity.

Definition vmatch (n: nat) (v: t) : Prop :=
match v with
| Bot => False
| Even => even n
| Odd => odd n
| Top => True
end.

TO BE COMPLETED

End Parity.