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.

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 (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.

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 (4 stars)