Module Analyzer2

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

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

In this chapter: various improvements on the generic program analyzer presented in chapter Analyzer1.

1. Interface of abstract domains.


Value abstractions are extended with

Module Type VALUE_ABSTRACTION.

Same operations as before

  Variable t: Type.

  Variable vmatch: nat -> t -> Prop.

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

  Variable ble: t -> t -> bool.
  Hypothesis ble_1: forall v1 v2, ble v1 v2 = true -> le v1 v2.

  Variable of_const: nat -> t.
  Hypothesis of_const_1: forall n, vmatch n (of_const n).

  Variable bot: t.
  Hypothesis bot_1: forall n, ~(vmatch n bot).

  Variable top: t.
  Hypothesis top_1: forall n, vmatch n top.

  Variable meet: t -> t -> t.
  Hypothesis meet_1:
    forall n v1 v2, vmatch n v1 -> vmatch n v2 -> vmatch n (meet v1 v2).

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

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

A boolean-valued function that decides the vmatch predicate.

  Variable test_vmatch: nat -> t -> bool.
  Hypothesis test_vmatch_1:
    forall n v, vmatch n v -> test_vmatch n v = true.
  Hypothesis test_vmatch_2:
    forall n v, test_vmatch n v = true -> vmatch n v.

Abstract operators for inverse analysis of comparisons. Consider a test a1 = a2 in the program, which we know evaluates to true. Let v1 be an abstraction of a1 and v2 an abstraction of a2. eq_inv v1 v2 returns a pair of abstract values v1', v2'. v1' is a (possibly more precise) abstraction for a1, taking into account the fact that a1 = a2. Likewise for v2' and a2.

  Variable eq_inv: t -> t -> t * t.
  Hypothesis eq_inv_1:
    forall n1 n2 a1 a2,
    vmatch n1 a1 -> vmatch n2 a2 -> n1 = n2 ->
    vmatch n1 (fst (eq_inv a1 a2)) /\ vmatch n2 (snd (eq_inv a1 a2)).

  Variable ne_inv: t -> t -> t * t.
  Hypothesis ne_inv_1:
    forall n1 n2 a1 a2,
    vmatch n1 a1 -> vmatch n2 a2 -> n1 <> n2 ->
    vmatch n1 (fst (ne_inv a1 a2)) /\ vmatch n2 (snd (ne_inv a1 a2)).

  Variable le_inv: t -> t -> t * t.
  Hypothesis le_inv_1:
    forall n1 n2 a1 a2,
    vmatch n1 a1 -> vmatch n2 a2 -> n1 <= n2 ->
    vmatch n1 (fst (le_inv a1 a2)) /\ vmatch n2 (snd (le_inv a1 a2)).

  Variable gt_inv: t -> t -> t * t.
  Hypothesis gt_inv_1:
    forall n1 n2 a1 a2,
    vmatch n1 a1 -> vmatch n2 a2 -> n1 > n2 ->
    vmatch n1 (fst (gt_inv a1 a2)) /\ vmatch n2 (snd (gt_inv a1 a2)).

Abstract operators for inverse analysis of expressions. Consider an addition expression a1 + a2. Let v1 be an abstraction of a1 v2 an abstraction of a2 v an abstraction for the result of a1 + a2, possibly more precise than add v1 v2. Then, add_inv v1 v2 v returns a pair of abstract values v1', v2' that are (possibly more precise) abstractions for a1 and a2.

  Variable add_inv: t -> t -> t -> t * t.
  Hypothesis add_inv_1:
    forall n1 n2 v1 v2 v,
    vmatch n1 v1 -> vmatch n2 v2 -> vmatch (n1+n2) v ->
    vmatch n1 (fst (add_inv v1 v2 v)) /\ vmatch n2 (snd (add_inv v1 v2 v)).

  Variable sub_inv: t -> t -> t -> t * t.
  Hypothesis sub_inv_1:
    forall n1 n2 v1 v2 v,
    vmatch n1 v1 -> vmatch n2 v2 -> vmatch (n1-n2) v ->
    vmatch n1 (fst (sub_inv v1 v2 v)) /\ vmatch n2 (snd (sub_inv v1 v2 v)).

  Variable mul_inv: t -> t -> t -> t * t.
  Hypothesis mul_inv_1:
    forall n1 n2 v1 v2 v,
    vmatch n1 v1 -> vmatch n2 v2 -> vmatch (n1*n2) v ->
    vmatch n1 (fst (mul_inv v1 v2 v)) /\ vmatch n2 (snd (mul_inv v1 v2 v)).

widen v1 v2 returns a majorant of v2, chosen so that the convergence of fixpoint iteration is accelerated.
  Variable widen: t -> t -> t.
  Hypothesis widen_1: forall v1 v2, le v2 (widen v1 v2).

End VALUE_ABSTRACTION.

The abstraction of states is enriched with widening operators, extending those of the value domain.

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

  Variable widen: t -> t -> t.

End STATE_ABSTRACTION.

2. The generic analyzer.

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

Fixpoint iteration with convergence acceleration.

Section FIXPOINT.

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

Iterate F a bounded number of times, applying the widening operator at each iteration. We stop if a post-fixpoint is encountered, or return S.top otherwise.

Fixpoint iter_up (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_up n1 (S.widen s s')
  end.

We then iterate F some more times. If s stops to be a post-fixpoint, we stop immediately.

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

Definition num_iter_up := 10.
Definition num_iter_down := 3.

Definition fixpoint (start: S.t) : S.t :=
  iter_down num_iter_down (iter_up num_iter_up start).

Lemma iter_up_post_fixpoint:
  forall n s, S.le (F (iter_up n s)) (iter_up n s).
Proof.
  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.

Lemma iter_down_post_fixpoint:
  forall n s, S.le (F s) s -> S.le (F (iter_down n s)) (iter_down n s).
Proof.
  induction n; simpl; intros.
  auto.
  remember (S.ble (F (F s)) (F s)). destruct b.
  apply IHn. apply S.ble_1. auto.
  auto.
Qed.

Lemma fixpoint_ok:
  forall s, S.le (F (fixpoint s)) (fixpoint s).
Proof.
  intro start. unfold fixpoint.
  apply iter_down_post_fixpoint.
  apply iter_up_post_fixpoint.
Qed.

End FIXPOINT.

Abstract interpretation of arithmetic expressions. Like in Analyzer1.

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.

Inverse analysis of arithmetic expressions. Assuming that the result of a matches the abstract value res, what do we learn about the values of variables occurring in a? Whatever we learn is used to refine the abstract values of these variables.

Fixpoint learn_from_eval (s: S.t) (a: aexp) (res: V.t) : S.t :=
  match a with
  | ANum n => if V.test_vmatch n res then s else S.bot
  | AId x => S.set s x (V.meet res (S.get s x))
  | APlus a1 a2 =>
      let (res1, res2) := V.add_inv (abstr_eval s a1) (abstr_eval s a2) res in
      learn_from_eval (learn_from_eval s a1 res1) a2 res2
  | AMinus a1 a2 =>
      let (res1, res2) := V.sub_inv (abstr_eval s a1) (abstr_eval s a2) res in
      learn_from_eval (learn_from_eval s a1 res1) a2 res2
  | AMult a1 a2 =>
      let (res1, res2) := V.mul_inv (abstr_eval s a1) (abstr_eval s a2) res in
      learn_from_eval (learn_from_eval s a1 res1) a2 res2
  end.

Inverse analysis of boolean expressions. Assuming that the result of b is equal to the boolean res, what do we learn about the values of variables occurring in b?

Fixpoint learn_from_test (s: S.t) (b: bexp) (res: bool) : S.t :=
  match b with
  | BTrue => if res then s else S.bot
  | BFalse => if res then S.bot else s
  | BEq a1 a2 =>
      let (res1, res2) :=
        if res
        then V.eq_inv (abstr_eval s a1) (abstr_eval s a2)
        else V.ne_inv (abstr_eval s a1) (abstr_eval s a2) in
      learn_from_eval (learn_from_eval s a1 res1) a2 res2
  | BLe a1 a2 =>
      let (res1, res2) :=
        if res
        then V.le_inv (abstr_eval s a1) (abstr_eval s a2)
        else V.gt_inv (abstr_eval s a1) (abstr_eval s a2) in
      learn_from_eval (learn_from_eval s a1 res1) a2 res2
  | BNot b1 =>
      learn_from_test s b1 (negb res)
  | BAnd b1 b2 =>
      if res
      then learn_from_test (learn_from_test s b1 true) b2 true
      else S.join (learn_from_test s b1 false) (learn_from_test s b2 false)
  end.

Abstract interpretation of commands. We use learn_from_test every time a conditional branch is taken / not taken.

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 (learn_from_test s b true) c1)
             (abstr_interp (learn_from_test s b false) c2)
  | WHILE b DO c END =>
      let s' :=
        fixpoint
         (fun x => S.join s (abstr_interp (learn_from_test x b true) c))
         s in
      learn_from_test s' b false
  end.

Soundness of abstract interpretation of expressions. No change.

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 inverse analysis of expressions.

Lemma learn_from_eval_sound:
  forall st a s res,
  S.smatch st s -> V.vmatch (aeval st a) res ->
  S.smatch st (learn_from_eval s a res).
Proof.
  induction a; simpl; intros.
Case "ANum".
  remember (S.V.test_vmatch n res). destruct b.
  auto.
  assert (S.V.test_vmatch n res = true). apply S.V.test_vmatch_1; auto.
  congruence.
Case "AId".
  replace st with (update st i (st i)).
  apply S.set_1. apply V.meet_1. auto. apply H. auto.
  apply functional_extensionality. intros.
  remember (beq_id i x). destruct b.
  replace x with i. rewrite update_eq. auto. apply beq_id_eq; auto.
  rewrite update_neq. auto. auto.
Case "APlus".
  generalize (S.V.add_inv_1 (aeval st a1) (aeval st a2) (abstr_eval s a1) (abstr_eval s a2) res).
  destruct (S.V.add_inv (abstr_eval s a1) (abstr_eval s a2) res) as [res1 res2].
  simpl; intros.
  destruct H1; auto; apply abstr_eval_sound; auto.
Case "AMinuas".
  generalize (S.V.sub_inv_1 (aeval st a1) (aeval st a2) (abstr_eval s a1) (abstr_eval s a2) res).
  destruct (S.V.sub_inv (abstr_eval s a1) (abstr_eval s a2) res) as [res1 res2].
  simpl; intros.
  destruct H1; auto; apply abstr_eval_sound; auto.
Case "AMult".
  generalize (S.V.mul_inv_1 (aeval st a1) (aeval st a2) (abstr_eval s a1) (abstr_eval s a2) res).
  destruct (S.V.mul_inv (abstr_eval s a1) (abstr_eval s a2) res) as [res1 res2].
  simpl; intros.
  destruct H1; auto; apply abstr_eval_sound; auto.
Qed.

Soundness of inverse analysis of boolean expressions.

Lemma learn_from_test_sound:
  forall st b s res,
  S.smatch st s -> beval st b = res ->
  S.smatch st (learn_from_test s b res).
Proof.
  induction b; simpl; intros.
Case "BTrue".
  subst res. auto.
Case "BFalse".
  subst res. auto.
Case "BEq".
  remember (if res
            then S.V.eq_inv (abstr_eval s a) (abstr_eval s a0)
            else S.V.ne_inv (abstr_eval s a) (abstr_eval s a0)) as res12.
  assert (V.vmatch (aeval st a) (fst res12) /\ V.vmatch (aeval st a0) (snd res12)).
    rewrite Heqres12.
    destruct res.
    apply S.V.eq_inv_1. apply abstr_eval_sound; auto. apply abstr_eval_sound; auto.
    apply beq_nat_true; auto.
    apply S.V.ne_inv_1. apply abstr_eval_sound; auto. apply abstr_eval_sound; auto.
    apply beq_nat_false; auto.
  destruct res12 as [res1 res2]; simpl in *.
  apply learn_from_eval_sound. apply learn_from_eval_sound. auto. tauto. tauto.
Case "BLe".
  remember (if res
            then S.V.le_inv (abstr_eval s a) (abstr_eval s a0)
            else S.V.gt_inv (abstr_eval s a) (abstr_eval s a0)) as res12.
  assert (V.vmatch (aeval st a) (fst res12) /\ V.vmatch (aeval st a0) (snd res12)).
    rewrite Heqres12.
    destruct res.
    apply S.V.le_inv_1. apply abstr_eval_sound; auto. apply abstr_eval_sound; auto.
    apply ble_nat_true; auto.
    apply S.V.gt_inv_1. apply abstr_eval_sound; auto. apply abstr_eval_sound; auto.
    generalize (ble_nat_false _ _ H0). omega.
  destruct res12 as [res1 res2]; simpl in *.
  apply learn_from_eval_sound. apply learn_from_eval_sound. auto. tauto. tauto.
Case "BNot".
  apply IHb; auto. rewrite <- H0. rewrite negb_involutive; auto.
Case "BAnd".
  destruct res.
  SCase "BAnd, true".
    destruct (andb_prop _ _ H0).
    auto.
  SCase "BAnd, false".
    destruct (andb_false_elim _ _ H0).
    apply S.join_1. auto.
    apply S.join_2. auto.
Qed.

Soundness of 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. apply learn_from_test_sound; auto.
  SCase "if false".
    apply S.join_2. apply IHc2 with st; auto. apply learn_from_test_sound; auto.
Case "while".
  set (F := fun x =>
               S.join s (abstr_interp (learn_from_test x b true) 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 (learn_from_test s' b false)).
  induction 1; intro EQ; inv EQ; intros.
  SCase "while end".
    apply learn_from_test_sound; auto.
  SCase "while loop".
    apply IHceval2; auto.
    apply FIX. unfold F.
    apply S.join_2. apply IHc with st0. apply learn_from_test_sound; auto. auto.

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

End Analysis.


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

Module V := VA.

We represent abstract states by either:

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.

Fixpoint map2 (f: V.t -> V.t -> V.t) (l1 l2: list V.t) {struct l2} : list V.t :=
  match l2, l1 with
  | nil, _ => nil
  | hd2 :: tl2, nil => hd2 :: map2 f nil tl2
  | hd2 :: tl2, hd1 :: tl1 => f hd1 hd2 :: map2 f tl1 tl2
  end.

The widening operator V.widen is applied point-wise to the abstractions of each variable. Bottom is neutral. If s1 x is top, we keep s2 x unchanged.

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

End StateAbstr.


Require Import Min.
Require Import Max.

Module Intervals <: VALUE_ABSTRACTION.

  Inductive natinf : Type := Fin (n: nat) | Inf.

  Definition t := (nat * natinf)%type.

  Definition low (v: t) := fst v.
  Definition high (v: t) := snd v.

  Definition vmatch (n: nat) (v: t) : Prop :=
    low v <= n /\ match high v with Fin hi => n <= hi | Inf => True end.

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

  Definition ble (v1 v2: t) : bool :=
    ble_nat (low v2) (low v1) &&
    match high v1, high v2 with
    | Fin hi1, Fin hi2 => ble_nat hi1 hi2
    | _, Inf => true
    | _, _ => false
    end.

  Lemma ble_1: forall v1 v2, ble v1 v2 = true -> le v1 v2.
Proof.
    unfold ble, le, vmatch; intros.
    destruct v1 as [lo1 hi1]; destruct v2 as [lo2 hi2]; simpl in *.
    destruct (andb_prop _ _ H); clear H.
    destruct H0.
    split.
    assert (lo2 <= lo1). apply ble_nat_true; auto. omega.
    destruct hi1; destruct hi2; auto.
    assert (n0 <= n1). apply ble_nat_true; auto. omega.
    congruence.
  Qed.

  Definition test_vmatch (n: nat) (v: t) : bool :=
    ble_nat(low v) n && match high v with Fin hi => ble_nat n hi | Inf => true end.

  Remark ble_nat_is_true:
    forall n m, n <= m -> ble_nat n m = true.
Proof.
    intros. remember (ble_nat n m). destruct b; auto.
    assert (~(n <= m)). apply ble_nat_false; auto. contradiction.
  Qed.

  Remark ble_nat_is_false:
    forall n m, n > m -> ble_nat n m = false.
Proof.
    intros. remember (ble_nat n m). destruct b; auto.
    assert (n <= m). apply ble_nat_true; auto. elimtype False; omega.
  Qed.

  Lemma test_vmatch_1:
    forall n v, vmatch n v -> test_vmatch n v = true.
Proof.
    unfold vmatch, test_vmatch; intros. destruct H.
    rewrite ble_nat_is_true; auto.
    destruct (high v). rewrite ble_nat_is_true. auto. omega. auto.
  Qed.

  Lemma test_vmatch_2:
    forall n v, test_vmatch n v = true -> vmatch n v.
Proof.
    unfold vmatch, test_vmatch; intros.
    destruct (andb_prop _ _ H). split.
    apply ble_nat_true; auto.
    destruct (high v). apply ble_nat_true; auto. auto.
  Qed.

  Definition of_const (n: nat) : t := (n, Fin n).

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

  Definition bot : t := (1, Fin 0).

  Lemma bot_1: forall n, ~(vmatch n bot).
Proof.
    unfold bot, vmatch; intros. simpl. red; intros [A B]. omega.
  Qed.

  Definition top : t := (0, Inf).

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

  Definition meet (v1 v2: t) : t :=
    (max (low v1) (low v2),
     match (high v1), (high v2) with
     | Fin hi1, Fin hi2 => Fin (min hi1 hi2)
     | hi1, Inf => hi1
     | Inf, hi2 => hi2
     end).

  Lemma meet_1:
    forall n v1 v2, vmatch n v1 -> vmatch n v2 -> vmatch n (meet v1 v2).
Proof.
     unfold meet, vmatch; intros. simpl. destruct H. destruct H0. split.
     apply max_case; auto.
     destruct (high v1); destruct (high v2); auto.
     apply min_case; auto.
  Qed.

  Definition join (v1 v2: t) : t :=
    (min (low v1) (low v2),
     match (high v1), (high v2) with
     | Fin hi1, Fin hi2 => Fin (max hi1 hi2)
     | _, _ => Inf
     end).

  Lemma join_1:
    forall n v1 v2, vmatch n v1 -> vmatch n (join v1 v2).
Proof.
    unfold vmatch, join; intros. simpl. destruct H. split.
    apply le_trans with (low v1). apply le_min_l. auto.
    destruct (high v1); destruct (high v2); auto.
    apply le_trans with n0. auto. apply le_max_l.
  Qed.

  Lemma join_2:
    forall n v1 v2, vmatch n v2 -> vmatch n (join v1 v2).
Proof.
    unfold vmatch, join; intros. simpl. destruct H. split.
    apply le_trans with (low v2). apply le_min_r. auto.
    destruct (high v1); destruct (high v2); auto.
    apply le_trans with n1. auto. apply le_max_r.
  Qed.

  Definition add (v1 v2: t) : t :=
    (low v1 + low v2,
     match high v1, high v2 with
     | Fin hi1, Fin hi2 => Fin(hi1 + hi2)
     | _, _ => Inf
     end).

  Lemma add_1:
    forall n1 n2 v1 v2, vmatch n1 v1 -> vmatch n2 v2 -> vmatch (n1+n2) (add v1 v2).
Proof.
    unfold vmatch, add; intros. destruct H; destruct H0; simpl; split.
    omega.
    destruct (high v1); destruct (high v2); auto. omega.
  Qed.

  Definition sub (v1 v2: t) : t :=
    match v1, v2 with
    | (lo1, Fin hi1), (lo2, Fin hi2) => (lo1 - hi2, Fin (hi1 - lo2))
    | (lo1, Fin hi1), (lo2, Inf) => (0, Fin (hi1 - lo2))
    | (lo1, Inf) , (lo2, Fin hi2) => (lo1 - hi2, Inf)
    | (lo1, Inf) , (lo2, Inf) => top
    end.

  Lemma sub_1:
    forall n1 n2 v1 v2, vmatch n1 v1 -> vmatch n2 v2 -> vmatch (n1-n2) (sub v1 v2).
Proof.
    unfold vmatch, sub; intros. destruct v1 as [lo1 hi1]. destruct v2 as [lo2 hi2]. simpl in *.
    destruct H; destruct H0.
    destruct hi1 as [hi1 | ]; destruct hi2 as [hi2 | ]; simpl; split; auto; omega.
  Qed.

  Definition mul (v1 v2: t) : t :=
    (low v1 * low v2,
     match high v1, high v2 with
     | Fin hi1, Fin hi2 => Fin(hi1 * hi2)
     | _, _ => Inf
     end).

  Lemma mul_1:
    forall n1 n2 v1 v2, vmatch n1 v1 -> vmatch n2 v2 -> vmatch (n1*n2) (mul v1 v2).
Proof.
    unfold vmatch, add; intros. destruct H; destruct H0; simpl; split.
    apply mult_le_compat; auto.
    destruct (high v1); destruct (high v2); auto. apply mult_le_compat; auto.
  Qed.

  Definition add_inv (v1 v2 vres: t) : t * t :=
    (meet v1 (sub vres v2), meet v2 (sub vres v1)).

  Lemma add_inv_1:
    forall n1 n2 v1 v2 v,
    vmatch n1 v1 -> vmatch n2 v2 -> vmatch (n1+n2) v ->
    vmatch n1 (fst (add_inv v1 v2 v)) /\ vmatch n2 (snd (add_inv v1 v2 v)).
Proof.
    unfold add_inv. simpl. intros. split.
    apply meet_1; auto. replace n1 with ((n1 + n2) - n2) by omega. apply sub_1; auto.
    apply meet_1; auto. replace n2 with ((n1 + n2) - n1) by omega. apply sub_1; auto.
  Qed.

  Definition sub_inv (v1 v2 vres: t) : t * t :=
    if beq_nat (low vres) 0
    then (v1, v2)
    else (meet v1 (add vres v2), meet v2 (sub v1 vres)).

  Lemma sub_inv_1:
    forall n1 n2 v1 v2 v,
    vmatch n1 v1 -> vmatch n2 v2 -> vmatch (n1-n2) v ->
    vmatch n1 (fst (sub_inv v1 v2 v)) /\ vmatch n2 (snd (sub_inv v1 v2 v)).
Proof.
    unfold sub_inv. simpl. intros.
    remember (beq_nat (low v) 0). destruct b.
    simpl; auto.
    assert (low v <> 0). apply beq_nat_false; auto.
    assert (n1 - n2 > 0). destruct H1. omega.
    simpl; split.
    apply meet_1; auto. replace n1 with ((n1 - n2) + n2) by omega. apply add_1; auto.
    apply meet_1; auto. replace n2 with (n1 - (n1 - n2)) by omega. apply sub_1; auto.
  Qed.

  Definition mul_inv (v1 v2 vres: t) : t * t := (v1, v2).

  Lemma mul_inv_1:
    forall n1 n2 v1 v2 v,
    vmatch n1 v1 -> vmatch n2 v2 -> vmatch (n1*n2) v ->
    vmatch n1 (fst (mul_inv v1 v2 v)) /\ vmatch n2 (snd (mul_inv v1 v2 v)).
Proof.
    unfold mul_inv. simpl; intros; auto.
  Qed.

  Definition eq_inv (v1 v2: t) : t * t := (meet v1 v2, meet v1 v2).

  Lemma eq_inv_1:
    forall n1 n2 a1 a2,
    vmatch n1 a1 -> vmatch n2 a2 -> n1 = n2 ->
    vmatch n1 (fst (eq_inv a1 a2)) /\ vmatch n2 (snd (eq_inv a1 a2)).
Proof.
    intros. unfold eq_inv; simpl. subst n2.
    split; apply meet_1; auto.
  Qed.

  Definition ne_inv (v1 v2: t) : t * t := (v1, v2).

  Lemma ne_inv_1:
    forall n1 n2 a1 a2,
    vmatch n1 a1 -> vmatch n2 a2 -> n1 <> n2 ->
    vmatch n1 (fst (ne_inv a1 a2)) /\ vmatch n2 (snd (ne_inv a1 a2)).
Proof.
    intros. unfold ne_inv; simpl. auto.
  Qed.

  Definition le_inv (v1 v2: t) : t * t :=
    ((low v1,
      match high v1, high v2 with
      | Inf, hi2 => hi2
      | Fin hi1, Inf => Fin hi1
      | Fin hi1, Fin hi2 => Fin (min hi1 hi2)
      end),
     (max (low v1) (low v2), high v2)).

  Lemma le_inv_1:
    forall n1 n2 a1 a2,
    vmatch n1 a1 -> vmatch n2 a2 -> n1 <= n2 ->
    vmatch n1 (fst (le_inv a1 a2)) /\ vmatch n2 (snd (le_inv a1 a2)).
Proof.
    unfold ne_inv, vmatch; simpl. intros. destruct H; destruct H0.
    split.
    split. auto. destruct (high a1); destruct (high a2); auto.
    apply min_case. auto. omega.
    omega.
    split. apply max_case; auto. omega.
    destruct (high a2); auto.
  Qed.

  Definition gt_inv (v1 v2: t) : t * t :=
    ((max (low v1) (low v2 + 1), high v1),
     (low v2,
      match high v2, high v1 with
      | Inf, Inf => Inf
      | Inf, Fin hi1 => Fin (hi1 - 1)
      | Fin hi2, Inf => Fin hi2
      | Fin hi2, Fin hi1 => Fin (min (hi1 - 1) hi2)
      end)).

  Lemma gt_inv_1:
    forall n1 n2 a1 a2,
    vmatch n1 a1 -> vmatch n2 a2 -> n1 > n2 ->
    vmatch n1 (fst (gt_inv a1 a2)) /\ vmatch n2 (snd (gt_inv a1 a2)).
Proof.
    unfold gt_inv, vmatch; simpl. intros. destruct H; destruct H0.
    split.
    split. apply max_case. auto. omega. auto.
    split. auto.
    destruct (high a2); destruct (high a1).
    apply min_case. omega. auto.
    auto.
    omega.
    auto.
  Qed.

  Definition widen (v1 v2: t) :=
    ((if ble_nat (low v1) (low v2) then low v2 else 0),
     match high v1, high v2 with
      | Fin hi1, Fin hi2 => if ble_nat hi2 hi1 then Fin hi2 else Inf
      | _, _ => high v2
      end).

  Lemma widen_1: forall v1 v2, le v2 (widen v1 v2).
Proof.
    unfold widen, le, vmatch; intros. destruct H. simpl. split.
    destruct (ble_nat (low v1) (low v2)). auto. omega.
    destruct (high v1); destruct (high v2); auto.
    destruct (ble_nat n1 n0). auto. auto.
  Qed.

End Intervals.

We now instantiate our generic analyzer over this domain.

Module SIntervals := StateAbstr(Intervals).
Module AIntervals := Analysis(Intervals)(SIntervals).

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

Sample program #1: 
    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 (AIntervals.abstr_interp SIntervals.top prog1).

Result is: 
SIntervals.Top_except
  [(11, Intervals.Fin 11), (0, Intervals.Fin 100), (100, Intervals.Fin 100)]
that is, x is in [11,11], y is in [0,100], and z is in [100,100].

Sample program #2: 
    x := 0; y := 0;
    while x <= 1000 do y := x; x := x + 1 end

Definition prog2 :=
  (vx ::= ANum 0;
   vy ::= ANum 0;
   WHILE BLe (AId vx) (ANum 1000) DO vy ::= AId vx; vx ::= APlus (AId vx) (ANum 1) END).

Eval vm_compute in (AIntervals.abstr_interp SIntervals.top prog2).

Result is: 
SIntervals.Top_except [(1001, Intervals.Fin 1001), (0, Intervals.Fin 1000)]
that is, x is in [1001,1001] and y is in [0,1000].



Generated by coq2html