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.
  Hypothesis add_1:
    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.add_1; auto.
  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.
    contradiction.
    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.

Proof.

    unfold vmatch, join; intros.
    destruct v1.
    contradiction.
    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.
    contradiction.
    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).
  Lemma add_1:
    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.
Admitted.

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.

Module Analyzer1

1. Interface of abstract domains.

2. The generic analyzer.

3. An implementation of a state abstraction.

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

Exercise (3 stars)

Exercise (4 stars)