Module AbstrInterp2

From Coq Require Import ZArith Psatz Bool String List FMaps.
From Coq Require Import FunctionalExtensionality.
From CDF Require Import Sequences IMP.
From CDF Require AbstrInterp.

Local Open Scope string_scope.
Local Open Scope Z_scope.

5. Analyse statique par interprétation abstraite, version améliorée


5.5. Interface des domaines abstraits améliorés


Nous ajoutons à l'interface des valeurs abstraites des opérations abstraites pour l'analyse inverse des conditionnelles et pour l'élargissement.

Module Type VALUE_ABSTRACTION.

On reprend toutes les déclarations de l'interface simplifiée.

  Include AbstrInterp.VALUE_ABSTRACTION.

meet calcule un minorant de ses deux arguments.
  Parameter meet: t -> t -> t.
  Axiom meet_1: forall n N1 N2, In n N1 -> In n N2 -> In n (meet N1 N2).

isIn teste si une valeur concrète appartient à une valeur abstraite.
  Parameter isIn: Z -> t -> bool.
  Axiom isIn_1: forall n N, In n N -> isIn n N = true.

Opérateurs abstraits pour l'analyse inverse des comparaisons.

Considérons un test a1 = a2 qui s'évalue à vrai dans le programme. Soit N1 une abstraction de a1 et N2 une abstraction de a2. eq_inv N1 N2 produit une paire de valeurs abstraites N1', N2'. N1' est une abstraction possiblement plus précise pour a1 qui prend en compte le fait que a1 = a2. N2' est une abstraction possiblement plus précise pour a2 qui prend en compte le fait que a1 = a2.

  Parameter eq_inv: t -> t -> t * t.
  Axiom eq_inv_1:
    forall n1 n2 N1 N2,
    In n1 N1 -> In n2 N2 -> n1 = n2 ->
    In n1 (fst (eq_inv N1 N2)) /\ In n2 (snd (eq_inv N1 N2)).

  Parameter ne_inv: t -> t -> t * t.
  Axiom ne_inv_1:
    forall n1 n2 N1 N2,
    In n1 N1 -> In n2 N2 -> n1 <> n2 ->
    In n1 (fst (ne_inv N1 N2)) /\ In n2 (snd (ne_inv N1 N2)).

  Parameter le_inv: t -> t -> t * t.
  Axiom le_inv_1:
    forall n1 n2 N1 N2,
    In n1 N1 -> In n2 N2 -> n1 <= n2 ->
    In n1 (fst (le_inv N1 N2)) /\ In n2 (snd (le_inv N1 N2)).

  Parameter gt_inv: t -> t -> t * t.
  Axiom gt_inv_1:
    forall n1 n2 N1 N2,
    In n1 N1 -> In n2 N2 -> n1 > n2 ->
    In n1 (fst (gt_inv N1 N2)) /\ In n2 (snd (gt_inv N1 N2)).

widen N1 N2 calcule un majorant de son premier arguments, choisi de sorte à garantir et accélérer la convergence de l'itération de point fixe.

  Parameter widen: t -> t -> t.
  Axiom widen_1: forall N1 N2, le N1 (widen N1 N2).

Pour garantir la convergence, on fournit une mesure à valeurs entières positives qui décroît strictement le long de l'itération de point fixe avec élargissement.
  Parameter measure: t -> nat.
  Axiom measure_top: measure top = 0%nat.
  Axiom widen_2: forall N1 N2, (measure (widen N1 N2) <= measure N1)%nat.
  Axiom widen_3:
    forall N1 N2, ble N2 N1 = false -> (measure (widen N1 N2) < measure N1)%nat.

End VALUE_ABSTRACTION.

Nous ajoutons à l'interface des états abstraits une opération d'élargissement.

Module Type STORE_ABSTRACTION.

  Declare Module V: VALUE_ABSTRACTION.
  Parameter t: Type.
  Parameter get: ident -> t -> V.t.
  Definition In (s: store) (S: t) : Prop := forall x, V.In (s x) (get x S).
  Parameter set: ident -> V.t -> t -> t.
  Axiom set_1: forall x n N s S, V.In n N -> In s S -> In (update x n s) (set x N S).
  Definition le (S1 S2: t) : Prop :=
    forall s, In s S1 -> In s S2.
  Parameter ble: t -> t -> bool.
  Axiom ble_1: forall S1 S2, ble S1 S2 = true -> le S1 S2.
  Parameter bot: t.
  Axiom bot_1: forall s, ~(In s bot).
  Parameter top: t.
  Parameter top_1: forall s, In s top.
  Parameter join: t -> t -> t.
  Axiom join_1: forall s S1 S2, In s S1 -> In s (join S1 S2).
  Axiom join_2: forall s S1 S2, In s S2 -> In s (join S1 S2).

Voici le nouvel opérateur d'élargissement.

  Parameter widen: t -> t -> t.
  Axiom widen_1: forall S1 S2, le S1 (widen S1 S2).

L'ordre ci-dessous correspond aux itérations successives de l'itération de point fixe avec élargissement. Il faut qu'il soit bien fondé afin de garantir la terminaison.

  Definition widen_order (S S1: t) :=
    exists S2, S = widen S1 S2 /\ ble S2 S1 = false.

  Axiom widen_order_wf: well_founded widen_order.

End STORE_ABSTRACTION.

5.6. L'analyseur générique amélioré.


Module Analysis (ST: STORE_ABSTRACTION).

Module V := ST.V.

Calcul de post-points fixes avec élargissement et rétrécissement


Section FIXPOINT.

Variable F: ST.t -> ST.t.

Program Definition is_true (b: bool) : { b = true } + { b = false } :=
  match b with true => left _ | false => right _ end.

Lemma iter_up_acc:
  forall (S: ST.t) (acc: Acc ST.widen_order S) (S': ST.t),
  ST.ble S' S = false ->
  Acc ST.widen_order (ST.widen S S').
Proof.
  intros. eapply Acc_inv; eauto. exists S'. auto.
Defined.

Fixpoint iter_up (S: ST.t) (acc: Acc ST.widen_order S) : ST.t :=
  let S' := F S in
  match is_true (ST.ble S' S) with
  | left LE => S
  | right NOTLE => iter_up (ST.widen S S') (iter_up_acc S acc S' NOTLE)
  end.

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

Definition niter_down := 3%nat.

Definition postfixpoint : ST.t :=
  iter_down niter_down (iter_up ST.bot (ST.widen_order_wf ST.bot)).

Lemma iter_up_sound:
  forall S acc, ST.le (F (iter_up S acc)) (iter_up S acc).
Proof.
  induction S using (well_founded_induction ST.widen_order_wf).
  intros acc. destruct acc. cbn. destruct (is_true (ST.ble (F S) S)).
- apply ST.ble_1; auto.
- apply H. exists (F S); auto.
Qed.

Lemma iter_down_sound:
  forall n S, ST.le (F S) S -> ST.le (F (iter_down n S)) (iter_down n S).
Proof.
  induction n; intros; cbn.
- auto.
- destruct (ST.ble (F (F S)) (F S)) eqn:BLE.
  + apply IHn. apply ST.ble_1; auto.
  + auto.
Qed.

Lemma postfixpoint_sound: ST.le (F postfixpoint) postfixpoint.
Proof.
  apply iter_down_sound. apply iter_up_sound.
Qed.

End FIXPOINT.

Interprétation abstraite des expressions arithmétiques


Même définition que dans la version simplifiée.

Fixpoint Aeval (a: aexp) (S: ST.t) : V.t :=
  match a with
  | CONST n => V.const n
  | VAR x => ST.get x S
  | PLUS a1 a2 => V.add (Aeval a1 S) (Aeval a2 S)
  | MINUS a1 a2 => V.sub (Aeval a1 S) (Aeval a2 S)
  end.

Lemma Aeval_sound:
  forall s S a,
  ST.In s S -> V.In (aeval a s) (Aeval a S).
Proof.
  induction a; cbn; intros.
- apply V.const_1.
- apply H.
- apply V.add_1; auto.
- apply V.sub_1; auto.
Qed.

Analyse inverse des expressions arithmétiques et booléennes


En supposant que la valeur concrète de a appartient à la valeur abstraite Res, qu'apprenons-nous sur les valeurs des variables qui apparaissent dans a? Les faits que nous apprenons sont utilisés pour affiner les valeurs abstraites de ces variables dans l'état abstrait S.

Fixpoint assume_eval (a: aexp) (Res: V.t) (S: ST.t) : ST.t :=
  match a with
  | CONST n =>
      if V.isIn n Res then S else ST.bot
  | VAR x =>
      ST.set x (V.meet Res (ST.get x S)) S
  | PLUS a1 a2 =>
      let N1 := Aeval a1 S in
      let N2 := Aeval a2 S in
      let Res1 := V.meet N1 (V.sub Res N2) in
      let Res2 := V.meet N2 (V.sub Res N1) in
      assume_eval a1 Res1 (assume_eval a2 Res2 S)
  | MINUS a1 a2 =>
      let N1 := Aeval a1 S in
      let N2 := Aeval a2 S in
      let Res1 := V.meet N1 (V.add Res N2) in
      let Res2 := V.meet N2 (V.sub N1 Res) in
      assume_eval a1 Res1 (assume_eval a2 Res2 S)
  end.

Lemma assume_eval_sound:
  forall a Res S s,
  V.In (aeval a s) Res -> ST.In s S -> ST.In s (assume_eval a Res S).
Proof.
  induction a; cbn; intros.
- (* CONST *)
  rewrite V.isIn_1 by auto. auto.
- (* VAR *)
  replace s with (update x (s x) s).
  apply ST.set_1; auto.
  apply V.meet_1; auto.
  apply functional_extensionality; intros y.
  unfold update; destruct (string_dec x y); congruence.
- (* PLUS *)
  set (n1 := aeval a1 s) in *. set (n2 := aeval a2 s) in *.
  set (N1 := Aeval a1 S). set (N2 := Aeval a2 S).
  assert (V.In n1 N1) by (apply Aeval_sound; auto).
  assert (V.In n2 N2) by (apply Aeval_sound; auto).
  apply IHa1; fold n1.
  apply V.meet_1. auto. replace n1 with ((n1 + n2) - n2) by lia. apply V.sub_1; auto.
  apply IHa2; fold n2.
  apply V.meet_1. auto. replace n2 with ((n1 + n2) - n1) by lia. apply V.sub_1; auto.
  auto.
- (* MINUS *)
  set (n1 := aeval a1 s) in *. set (n2 := aeval a2 s) in *.
  set (N1 := Aeval a1 S). set (N2 := Aeval a2 S).
  assert (V.In n1 N1) by (apply Aeval_sound; auto).
  assert (V.In n2 N2) by (apply Aeval_sound; auto).
  apply IHa1; fold n1.
  apply V.meet_1. auto. replace n1 with ((n1 - n2) + n2) by lia. apply V.add_1; auto.
  apply IHa2; fold n2.
  apply V.meet_1. auto. replace n2 with (n1 - (n1 - n2)) by lia. apply V.sub_1; auto.
  auto.
Qed.

En supposant que l'expression booléenne b s'évalue concrètement à res, qu'apprenons-nous sur les valeurs des variables qui apparaissent dans b? Les faits que nous apprenons sont utilisés pour affiner les valeurs abstraites de ces variables dans l'état abstrait S.

Fixpoint assume_test (b: bexp) (res: bool) (S: ST.t): ST.t :=
  match b with
  | TRUE => if res then S else ST.bot
  | FALSE => if res then ST.bot else S
  | EQUAL a1 a2 =>
      let (Res1, Res2) :=
        if res
        then V.eq_inv (Aeval a1 S) (Aeval a2 S)
        else V.ne_inv (Aeval a1 S) (Aeval a2 S) in
      assume_eval a1 Res1 (assume_eval a2 Res2 S)
  | LESSEQUAL a1 a2 =>
      let (Res1, Res2) :=
        if res
        then V.le_inv (Aeval a1 S) (Aeval a2 S)
        else V.gt_inv (Aeval a1 S) (Aeval a2 S) in
      assume_eval a1 Res1 (assume_eval a2 Res2 S)
  | NOT b1 =>
      assume_test b1 (negb res) S
  | AND b1 b2 =>
      if res
      then assume_test b1 true (assume_test b2 true S)
      else ST.join (assume_test b1 false S) (assume_test b2 false S)
  end.

Lemma assume_test_sound:
  forall b res S s,
  beval b s = res -> ST.In s S -> ST.In s (assume_test b res S).
Proof.
  induction b; cbn; intros.
- (* TRUE *)
  subst res; auto.
- (* FALSE *)
  subst res; auto.
- (* EQUAL *)
  set (Res := if res
              then V.eq_inv (Aeval a1 S) (Aeval a2 S)
              else V.ne_inv (Aeval a1 S) (Aeval a2 S)).
  assert (A: V.In (aeval a1 s) (fst Res) /\ V.In (aeval a2 s) (snd Res)).
  { unfold Res; destruct res;
    [ apply V.eq_inv_1 | apply V.ne_inv_1 ]; auto using Aeval_sound.
  - apply Z.eqb_eq; auto.
  - apply Z.eqb_neq; auto.
  }
  destruct A as [A1 A2]. destruct Res as [Res1 Res2]. auto using assume_eval_sound.
- (* LESSEQUAL *)
  set (Res := if res
              then V.le_inv (Aeval a1 S) (Aeval a2 S)
              else V.gt_inv (Aeval a1 S) (Aeval a2 S)).
  assert (A: V.In (aeval a1 s) (fst Res) /\ V.In (aeval a2 s) (snd Res)).
  { unfold Res; destruct res;
    [ apply V.le_inv_1 | apply V.gt_inv_1 ]; auto using Aeval_sound.
  - apply Z.leb_le; auto.
  - apply Z.leb_nle in H. lia.
  }
  destruct A as [A1 A2]. destruct Res as [Res1 Res2]. auto using assume_eval_sound.
- (* NOT *)
  apply IHb; auto. rewrite <- H. rewrite negb_involutive; auto.
- (* AND *)
  destruct res.
  + (* AND, true *)
    destruct (andb_prop _ _ H).
    auto.
  + (* AND, false *)
    destruct (andb_false_elim _ _ H); [apply ST.join_1 | apply ST.join_2]; auto.
Qed.

Interprétation abstraite améliorée des commandes


On ajoute des appels à assume_test à chaque fois qu'une condition booléenne est connue comme vraie ou comme fausse.

Fixpoint Cexec (c: com) (S: ST.t) : ST.t :=
  match c with
  | SKIP => S
  | ASSIGN x a => ST.set x (Aeval a S) S
  | SEQ c1 c2 => Cexec c2 (Cexec c1 S)
  | IFTHENELSE b c1 c2 =>
      ST.join (Cexec c1 (assume_test b true S))
              (Cexec c2 (assume_test b false S))
  | WHILE b c =>
      assume_test b false
        (postfixpoint (fun X => ST.join S (Cexec c (assume_test b true X))))
  end.

Theorem Cexec_sound:
  forall c s s' S,
  ST.In s S -> cexec s c s' -> ST.In s' (Cexec c S).
Proof.
Opaque niter_down.
  induction c; intros s s' S PRE EXEC; cbn.
- (* SKIP *)
  inversion EXEC; subst. auto.
- (* ASSIGN *)
  inversion EXEC; subst. apply ST.set_1; auto. apply Aeval_sound; auto.
- (* SEQ *)
  inversion EXEC; subst. eauto.
- (* IFTHENELSE *)
  inversion EXEC; subst. destruct (beval b s) eqn:B.
  apply ST.join_1. eapply IHc1; eauto. apply assume_test_sound; auto.
  apply ST.join_2. eapply IHc2; eauto. apply assume_test_sound; auto.
- (* WHILE *)
  set (F := fun X => ST.join S (Cexec c (assume_test b true X))).
  set (X := postfixpoint F).
  assert (L : ST.le (F X) X) by (apply postfixpoint_sound).
  assert (REC: forall s1 c1 s2,
               cexec s1 c1 s2 ->
               c1 = WHILE b c ->
               ST.In s1 X ->
               ST.In s2 (assume_test b false X)).
  { induction 1; intro EQ; inversion EQ; subst; intros.
  - (* WHILE done *)
    apply assume_test_sound; auto.
  - (* WHILE loop *)
    apply IHcexec2; auto. apply L. unfold F. apply ST.join_2.
    eapply IHc; eauto. apply assume_test_sound; auto.
  }
  eapply REC; eauto. apply L. unfold F. apply ST.join_1. auto.
Qed.

End Analysis.

5.7. Un domaine abstrait des états mémoire


On reprend le domaine abstrait du fichier AbstrInterp, section 5.3, et on lui ajoute l'opérateur d'élargissement et ses propriétés.

Module IdentMap := AbstrInterp.IdentMap.
Module IMFact := AbstrInterp.IMFact.
Module IMProp := AbstrInterp.IMProp.

Module StoreAbstr (VA: VALUE_ABSTRACTION) <: STORE_ABSTRACTION.

Module V := VA.

Inductive abstr_state : Type :=
  | Bot
  | Top_except (m: IdentMap.t V.t).

Definition t := abstr_state.

Definition get (x: ident) (S: t) : V.t :=
  match S with
  | Bot => V.bot
  | Top_except m =>
      match IdentMap.find x m with
      | None => V.top
      | Some v => v
      end
  end.

Definition In (s: store) (S: t) : Prop :=
  forall x, V.In (s x) (get x S).

Definition set (x: ident) (N: V.t) (S: t): t :=
  if V.ble N V.bot then Bot else
  match S with
  | Bot => Bot
  | Top_except m => Top_except (IdentMap.add x N m)
  end.

Lemma set_1:
  forall x n N s S,
  V.In n N -> In s S -> In (update x n s) (set x N S).
Proof.
  unfold In, get, set; intros.
  destruct (V.ble N V.bot) eqn:BLE; [ | destruct S ].
- apply V.ble_1 in BLE. apply BLE in H. elim (V.bot_1 n); auto.
- elim (V.bot_1 (s "")). auto.
- rewrite IMFact.add_o. change IdentMap.E.eq_dec with string_dec. unfold update.
  destruct (string_dec x x0); auto.
Qed.

L'ordre entre les états abstraits.

Definition le (S1 S2: t) : Prop :=
  forall s, In s S1 -> In s S2.

Definition ble (S1 S2: t) : bool :=
  match S1, S2 with
  | Bot, _ => true
  | _, Bot => false
  | Top_except m1, Top_except m2 =>
      IMProp.for_all (fun x v => V.ble (get x S1) v) m2
  end.

Lemma ble_1: forall S1 S2, ble S1 S2 = true -> le S1 S2.
Proof.
  unfold ble, le; intros.
  destruct S1 as [ | m1].
- elim (V.bot_1 (s "")). apply H0.
- destruct S2 as [ | m2]. discriminate.
  red; cbn; intros. destruct (IdentMap.find x m2) as [N2|] eqn:F2.
  + apply IdentMap.find_2 in F2. eapply IMProp.for_all_iff in H; eauto.
    apply V.ble_1 in H. apply H. apply H0.
    hnf. intros; subst x0. hnf; intros. subst x0. auto.
  + apply V.top_1.
Qed.

Lemma ble_false: forall s1 s2,
  s2 <> Bot -> ble s1 s2 = false -> exists x, V.ble (get x s1) (get x s2) = false.
Proof.
  unfold ble; intros.
  destruct s1 as [ | m1]. discriminate. destruct s2 as [ | m2]. congruence.
- set (p := fun (x: IdentMap.key) v => V.ble (get x (Top_except m1)) v) in *.
  set (m' := IMProp.filter (fun x v => negb (p x v)) m2).
  destruct (IdentMap.elements m') as [ | [x1 v1] l1] eqn:ELT.
+ assert (IMProp.for_all p m2 = true).
  { apply IMProp.for_all_iff.
    repeat (hnf; intros). congruence.
    intros. destruct (p k e) eqn:P; auto.
    assert (M: IdentMap.MapsTo k e m').
    { apply IMProp.filter_iff.
      repeat (hnf; intros). congruence.
      rewrite P; auto. }
    apply IdentMap.elements_1 in M. rewrite ELT in M. inversion M.
  }
  congruence.
+ assert (M: IdentMap.MapsTo x1 v1 m').
  { apply IdentMap.elements_2. rewrite ELT. constructor. hnf; auto. }
  apply IMProp.filter_iff in M. destruct M as [M N]. apply negb_true_iff in N.
  exists x1. unfold get at 2. erewrite IdentMap.find_1 by eauto. exact N.
  repeat (hnf; intros). congruence.
Qed.

Les opérations de treillis.

Definition bot: t := Bot.

Lemma bot_1: forall s, ~(In s bot).
Proof.
  unfold In; cbn. intros s IN. apply (V.bot_1 (s "")). apply IN.
Qed.

Definition top: t := Top_except (IdentMap.empty V.t).

Lemma top_1: forall s, In s top.
Proof.
  unfold In, top, get; cbn. intros. apply V.top_1.
Qed.

Definition join_aux (ov1 ov2: option V.t) : option V.t :=
  match ov1, ov2 with
  | Some v1, Some v2 => Some (V.join v1 v2)
  | _, _ => None
  end.

Definition join (S1 S2: t) : t :=
  match S1, S2 with
  | Bot, _ => S2
  | _, Bot => S1
  | Top_except m1, Top_except m2 =>
      Top_except (IdentMap.map2 join_aux m1 m2)
  end.

Lemma join_1:
  forall s S1 S2, In s S1 -> In s (join S1 S2).
Proof.
  unfold join; intros.
  destruct S1 as [ | m1]. elim (bot_1 s); auto.
  destruct S2 as [ | m2]. auto.
- red; unfold get; intros. rewrite IMFact.map2_1bis; auto.
  unfold join_aux. specialize (H x). unfold get in H.
  destruct (IdentMap.find x m1).
  + destruct (IdentMap.find x m2).
    * apply V.join_1; auto.
    * apply V.top_1.
  + apply V.top_1.
Qed.

Lemma join_2:
  forall s S1 S2, In s S2 -> In s (join S1 S2).
Proof.
  unfold join; intros.
  destruct S1 as [ | m1]. auto.
  destruct S2 as [ | m2]. elim (bot_1 s); auto.
- red; unfold get; intros. rewrite IMFact.map2_1bis; auto.
  unfold join_aux. specialize (H x). unfold get in H.
  destruct (IdentMap.find x m1).
  + destruct (IdentMap.find x m2).
    * apply V.join_2; auto.
    * apply V.top_1.
  + apply V.top_1.
Qed.

L'opérateur d'élargissement. On applique point-à-point l'élargissement V.widen fourni par le domaine des valeurs, avec des cas par défaut pour les variables non décrites, qui sont implicitement à V.top.

Definition widen_aux (ov1 ov2: option V.t) : option V.t :=
  match ov1, ov2 with
  | Some v1, Some v2 => Some (V.widen v1 v2)
  | None, _ => None
  | _, None => None
  end.

Definition widen (s1 s2: t) : t :=
  match s1, s2 with
  | Bot, _ => s2
  | _, Bot => s1
  | Top_except m1, Top_except m2 => Top_except (IdentMap.map2 widen_aux m1 m2)
  end.

Lemma widen_1: forall s1 s2, le s1 (widen s1 s2).
Proof.
  unfold le, widen; intros.
  destruct s1 as [ | m1]. elim (bot_1 _ H).
  destruct s2 as [ | m2]. auto.
  red; unfold get; intros. specialize (H x); cbn in H.
  rewrite IMFact.map2_1bis; auto. unfold widen_aux.
  destruct (IdentMap.find x m1); destruct (IdentMap.find x m2);
  auto using V.top_1.
  apply V.widen_1; auto.
Qed.

La construction de l'ordre bien fondé qui garantit la terminaison est délicate. On commence par définir une mesure à valeurs entières positives pour une fonction finie IdentMap.t V.t, qui est la somme des mesures des valeurs abstraites dans l'image de cette fonction finie.

Definition measure_map (m: IdentMap.t V.t) : nat :=
  IdentMap.fold (fun x v n => (V.measure v + n)%nat) m 0%nat.

Remark measure_map_empty:
  forall m, IdentMap.Empty m -> measure_map m = 0%nat.
Proof.
  intros. apply IMProp.fold_Empty; auto.
Qed.

Remark measure_map_add:
  forall m x v m', ~IdentMap.In x m -> IMProp.Add x v m m' ->
  measure_map m' = (V.measure v + measure_map m)%nat.
Proof.
  intros. unfold measure_map; eapply IMProp.fold_Add with (f := fun x v n => (V.measure v + n)%nat); eauto.
  repeat (hnf; intros). congruence.
  hnf; intros. lia.
Qed.

Remark measure_map_remove:
  forall m x,
  measure_map m = (V.measure (get x (Top_except m)) + measure_map (IdentMap.remove x m))%nat.
Proof.
  intros. unfold get. destruct (IdentMap.find x m) as [v|] eqn:F.
- apply measure_map_add with x.
  apply IMFact.not_find_in_iff. rewrite IMFact.remove_eq_o; auto.
  red; intros. rewrite IMFact.add_o, IMFact.remove_o.
  destruct (AbstrInterp.IdentMap.E.eq_dec x y); congruence.
- rewrite V.measure_top. unfold measure_map. eapply IMProp.fold_Equal. auto.
  repeat (hnf; intros). congruence.
  hnf; intros; lia.
  red; intros. rewrite IMFact.remove_o.
  destruct (AbstrInterp.IdentMap.E.eq_dec x y); congruence.
Qed.

Lemma measure_map_le: forall m1 m2,
  (forall x, V.measure (get x (Top_except m1)) <= V.measure (get x (Top_except m2)))%nat ->
  (measure_map m1 <= measure_map m2)%nat.
Proof.
  intros m0. pattern m0. unfold measure_map at 1; apply IMProp.fold_rec.
- intros m EMPTY m2 LE. lia.
- intros x v1 n m' m'' MAP NOTIN ADD REC m2 LE.
  set (m2' := IdentMap.remove x m2).
  assert (LE': forall x, (V.measure (get x (Top_except m')) <= V.measure (get x (Top_except m2')))%nat).
  { intros y. generalize (LE y). unfold get, m2'. rewrite ADD, IMFact.add_o, IMFact.remove_o.
    destruct (AbstrInterp.IdentMap.E.eq_dec x y).
    + subst y. apply IMFact.not_find_in_iff in NOTIN. rewrite NOTIN. rewrite ! V.measure_top. lia.
    + auto. }
  apply REC in LE'.
  rewrite (measure_map_remove m2 x). fold m2'.
  specialize (LE x). unfold get at 1 in LE. rewrite ADD, IMFact.add_eq_o in LE by auto.
  lia.
Qed.

Lemma measure_map_lt: forall m1 m2,
  (forall x, V.measure (get x (Top_except m1)) <= V.measure (get x (Top_except m2)))%nat ->
  (exists x, V.measure (get x (Top_except m1)) < V.measure (get x (Top_except m2)))%nat ->
  (measure_map m1 < measure_map m2)%nat.
Proof.
  intros m1 m2 LE (x & LT).
  rewrite (measure_map_remove m1 x), (measure_map_remove m2 x).
  assert ((measure_map (IdentMap.remove x m1) <= measure_map (IdentMap.remove x m2))%nat).
  { apply measure_map_le.
    intros y; unfold get. rewrite ! IMFact.remove_o.
    destruct (AbstrInterp.IdentMap.E.eq_dec x y).
    lia.
    apply LE. }
  lia.
Qed.

On montre ensuite que cette mesure décroît strictement lors d'une étape d'élargissement qui n'implique pas Bot.

Lemma measure_widen_lt: forall m1 m2,
  ble (Top_except m2) (Top_except m1) = false ->
  (measure_map (IdentMap.map2 widen_aux m1 m2) < measure_map m1)%nat.
Proof.
  intros. apply ble_false in H. 2: congruence. destruct H as (x & BL).
  apply measure_map_lt.
- intros y. unfold get. rewrite IMFact.map2_1bis by auto. unfold widen_aux.
  destruct (IdentMap.find y m1) as [ v1 |].
  destruct (IdentMap.find y m2) as [ v2 |].
  apply V.widen_2.
  rewrite V.measure_top; lia.
  rewrite V.measure_top; lia.
- exists x. unfold get in *. rewrite IMFact.map2_1bis by auto. unfold widen_aux.
  destruct (IdentMap.find x m1) as [ v1 |].
  destruct (IdentMap.find x m2) as [ v2 |].
  apply V.widen_3 in BL; auto.
  apply V.widen_3 in BL; rewrite V.measure_top; lia.
  assert (T: forall z, V.ble z V.top = true).
  { intros. apply V.ble_2. red; intros. apply V.top_1. }
  rewrite T in BL. congruence.
Qed.

On en déduit que l'ordre d'élargissement est bien fondé.

Definition widen_order (S S1: t) := exists S2, S = widen S1 S2 /\ ble S2 S1 = false.

Lemma widen_order_wf: well_founded widen_order.
Proof.
  assert (A: forall m, Acc widen_order (Top_except m)).
  { induction m using (well_founded_ind (well_founded_ltof _ measure_map)).
    constructor. intros S (S2 & EQ & BLE). subst S.
    destruct S2. discriminate. apply H. apply measure_widen_lt. auto. }
  assert (B: Acc widen_order Bot).
  { constructor. intros S (S2 & EQ & BLE). subst S.
    unfold ble in BLE. destruct S2. discriminate. apply A. }
  red. destruct a; auto.
Defined.

End StoreAbstr.

5.8. Le domaine abstrait des intervalles


Nous définissons d'abord le type zinf des entiers relatifs complétés par "plus l'infini".

Inductive zinf : Type := Fin (h: Z) | Inf.

Coercion Fin : Z >-> zinf.

Module Zinf.
  Definition In (n: Z) (N: zinf) : Prop :=
    match N with Fin h => n <= h | Inf => True end.

  Lemma In_mono: forall n1 n2 N, n1 <= n2 -> In n2 N -> In n1 N.
Proof.
    unfold In; destruct N; intros. lia. auto.
  Qed.

  Definition le (N1 N2: zinf) : Prop :=
    forall n, In n N1 -> In n N2.

  Lemma le_Fin: forall n1 N2, le (Fin n1) N2 <-> In n1 N2.
Proof.
    unfold le; cbn; intros; split; intros.
  - apply H. lia.
  - destruct N2; cbn in *; auto. lia.
  Qed.

  Lemma le_is_Inf: forall N h, (forall n, h <= n -> In n N) -> N = Inf.
Proof.
    destruct N; cbn; intros; auto.
    specialize (H (Z.max h0 (h + 1))). lia.
  Qed.

  Lemma le_Inf: forall N, le Inf N <-> N = Inf.
Proof.
    unfold le; intros; split; intros.
  - apply le_is_Inf with 0. intros; apply H; exact I.
  - subst N; exact I.
  Qed.

  Definition ble (N1 N2: zinf) : bool :=
    match N1, N2 with _, Inf => true | Inf, _ => false | Fin h1, Fin h2 => h1 <=? h2 end.

  Lemma ble_1: forall N1 N2, ble N1 N2 = true -> le N1 N2.
Proof.
    unfold ble, le, In; intros.
    destruct N1, N2; auto.
    apply Z.leb_le in H. lia.
    discriminate.
  Qed.

  Lemma ble_2: forall N1 N2, le N1 N2 -> ble N1 N2 = true.
Proof.
    unfold ble; intros. destruct N1.
  - apply le_Fin in H. destruct N2; auto. apply Z.leb_le; auto.
  - apply le_Inf in H. rewrite H. auto.
  Qed.

  Definition max (N1 N2: zinf) : zinf :=
    match N1, N2 with Inf, _ => Inf | _, Inf => Inf | Fin h1, Fin h2 => Fin (Z.max h1 h2) end.

  Lemma max_1: forall n N1 N2, In n N1 -> In n (max N1 N2).
Proof.
    unfold In, max; intros. destruct N1; auto. destruct N2; auto. lia.
  Qed.

  Lemma max_2: forall n N1 N2, In n N2 -> In n (max N1 N2).
Proof.
    unfold In, max; intros. destruct N1; auto. destruct N2; auto. lia.
  Qed.

  Definition min (N1 N2: zinf) : zinf :=
    match N1, N2 with Inf, _ => N2 | _, Inf => N1 | Fin h1, Fin h2 => Fin (Z.min h1 h2) end.

  Lemma min_1: forall n N1 N2, In n N1 -> In n N2 -> In n (min N1 N2).
Proof.
    unfold In, min; intros. destruct N1; auto. destruct N2; auto. lia.
  Qed.

  Definition add (N1 N2: zinf) : zinf :=
    match N1, N2 with Inf, _ => Inf | _, Inf => Inf | Fin h1, Fin h2 => Fin (h1 + h2) end.

  Lemma add_1: forall n1 n2 N1 N2, In n1 N1 -> In n2 N2 -> In (n1 + n2) (add N1 N2).
Proof.
    unfold In, add; intros. destruct N1; auto. destruct N2; auto. lia.
  Qed.

  Definition isIn (n: Z) (N: zinf) : bool :=
    match N with Fin h => n <=? h | Inf => true end.

  Lemma isIn_1:
    forall n N, In n N -> isIn n N = true.
Proof.
    unfold In, isIn; intros. destruct N; auto. apply Z.leb_le; auto.
  Qed.

  Definition pred (N: zinf) : zinf :=
    match N with Inf => Inf | Fin n => Fin (n - 1) end.

  Lemma pred_1: forall n N, In n N -> In (n - 1) (pred N).
Proof.
    unfold pred, In; intros; destruct N; auto. lia.
  Qed.

On définit l'élargissement entre deux entiers possiblement infinis comme suit: si l'entier augmente strictement, on part à l'infini, sinon on conserve le premier entier.

  Definition widen (N1 N2: zinf) : zinf :=
     if ble N2 N1 then N1 else Inf.

  Lemma widen_1: forall N1 N2, le N1 (widen N1 N2).
Proof.
    unfold widen; intros. destruct (ble N2 N1) eqn:LE.
    red; auto.
    red; unfold In; auto.
  Qed.

  Definition measure (N: zinf) : nat :=
    match N with Inf => 0%nat | Fin _ => 1%nat end.

  Lemma measure_1: forall N, (measure N <= 1)%nat.
Proof.
    destruct N; cbn; lia.
  Qed.

  Lemma widen_2:
    forall N1 N2, (measure (widen N1 N2) <= measure N1)%nat.
Proof.
    intros. unfold widen. destruct (ble N2 N1) eqn:BLE.
  - lia.
  - destruct N1. cbn; lia. destruct N2; discriminate.
  Qed.

  Lemma widen_3:
    forall N1 N2, ble N2 N1 = false -> (measure (widen N1 N2) < measure N1)%nat.
Proof.
    destruct N1, N2; cbn; intros; auto; try discriminate.
    unfold widen. cbn. rewrite H. cbn. lia.
  Qed.

End Zinf.

Un intervalle est représenté par une paire de zinf. Le second est la borne supérieure, le premier est l'opposé de la borne inférieure. Cette astuce de représentation permet de n'avoir qu'un infini Inf, au lieu d'avoir un infini négatif pour les bornes inférieures et un infini positif pour les bornes supérieures.

Module Intervals <: VALUE_ABSTRACTION.

Le type des valeurs abstraites.
  Record interval : Type := intv { low: zinf; high: zinf }.
  Definition t := interval.

L'appartenance: n doit être en dessous de la borne supérieure, et l'opposé de n en dessous de l'opposé de la borne inférieure.

  Definition In (n: Z) (N: t) : Prop :=
    Zinf.In n (high N) /\ Zinf.In (-n) (low N).

  Definition le (N1 N2: t) : Prop :=
    forall n, In n N1 -> In n N2.

Teste si un intervalle est vide.

  Definition isempty (N: t) : bool :=
    match N with
    | {| low := Fin l; high := Fin h |} => h <? (-l)
    | _ => false
    end.

  Lemma isempty_1: forall n N, isempty N = true -> In n N -> False.
Proof.
    unfold isempty, In; intros. destruct N as [[l|] [h|]]; try discriminate.
    apply Z.ltb_lt in H. cbn in H0. lia.
  Qed.

  Lemma isempty_2: forall N, isempty N = false -> exists n, In n N.
Proof.
    unfold isempty, In; intros. destruct N as [[l|] [h|]]; cbn.
  - apply Z.ltb_ge in H. exists h; lia.
  - exists (- l); lia.
  - exists h; lia.
  - exists 0; auto.
  Qed.

  Lemma nonempty_le: forall N1 N2,
    le N1 N2 -> isempty N1 = false -> (Zinf.le (high N1) (high N2) /\ Zinf.le (low N1) (low N2)).
Proof.
    unfold le, In, isempty; intros.
    destruct N1 as [[l1 |] [h1|]]; cbn in *; rewrite ? Zinf.le_Fin, ? Zinf.le_Inf.
  - apply Z.ltb_ge in H0. split.
    + apply H; lia.
    + replace l1 with (- - l1) by lia. apply H. lia.
  - split.
    + apply Zinf.le_is_Inf with (-l1). intros; apply H. intuition lia.
    + replace l1 with (- - l1) by lia. apply H. intuition lia.
  - split.
    + apply H. intuition lia.
    + apply Zinf.le_is_Inf with(- h1).
      intros. replace n with (- - n) by lia. apply H. intuition lia.
  - split; apply Zinf.le_is_Inf with 0; intros.
    + apply H; auto.
    + replace n with (- - n) by lia. apply H. auto.
  Qed.

ble est une fonction à valeurs booléennes qui décide la relation le.

  Definition ble (N1 N2: t) : bool :=
    isempty N1 || (Zinf.ble (high N1) (high N2) && Zinf.ble (low N1) (low N2)).

  Lemma ble_1: forall N1 N2, ble N1 N2 = true -> le N1 N2.
Proof.
    unfold ble, le, In; intros.
    destruct (isempty N1) eqn:E.
    elim (isempty_1 _ _ E H0).
    apply andb_prop in H. destruct H as [B1 B2].
    apply Zinf.ble_1 in B1. apply Zinf.ble_1 in B2.
    intuition.
  Qed.

  Lemma ble_2: forall N1 N2, le N1 N2 -> ble N1 N2 = true.
Proof.
    unfold ble; intros. destruct (isempty N1) eqn:E; auto.
    destruct (nonempty_le N1 N2) as [P Q]; auto.
    apply andb_true_intro; split; apply Zinf.ble_2; auto.
  Qed.

const n est la valeur abstraite pour l'ensemble singleton {n}.
  Definition const (n: Z) : t := {| low := Fin (-n); high := Fin n |}.

  Lemma const_1: forall n, In n (const n).
Proof.
    unfold const, In, Zinf.In; intros; cbn. lia.
  Qed.

bot représente l'ensemble vide.
  Definition bot: t := {| low := Fin 0; high := Fin (-1) |}.

  Lemma bot_1: forall n, ~(In n bot).
Proof.
    unfold bot, In, Zinf.In; intros; cbn. lia.
  Qed.

top représente l'ensemble de tous les entiers.
  Definition top: t := {| low := Inf; high := Inf |}.

  Lemma top_1: forall n, In n top.
Proof.
    intros. split; exact I.
  Qed.

join calcule un majorant de ses deux arguments.
  Definition join (N1 N2: t) : t :=
    {| low := Zinf.max (low N1) (low N2);
       high := Zinf.max (high N1) (high N2) |}.

  Lemma join_1:
    forall n N1 N2, In n N1 -> In n (join N1 N2).
Proof.
    unfold In, join; intros; cbn. split; apply Zinf.max_1; tauto.
  Qed.

  Lemma join_2:
    forall n N1 N2, In n N2 -> In n (join N1 N2).
Proof.
    unfold In, join; intros; cbn. split; apply Zinf.max_2; tauto.
  Qed.

Les opérateurs abstraits correspondant à l'addition et à la soustraction.

  Definition add (N1 N2: t) : t :=
    if isempty N1 || isempty N2 then bot else
    {| low := Zinf.add (low N1) (low N2);
       high := Zinf.add (high N1) (high N2) |}.

  Lemma add_1:
    forall n1 n2 N1 N2, In n1 N1 -> In n2 N2 -> In (n1 + n2) (add N1 N2).
Proof.
    unfold add; intros.
    destruct (isempty N1) eqn:E1. elim (isempty_1 n1 N1); auto.
    destruct (isempty N2) eqn:E2. elim (isempty_1 n2 N2); auto.
    destruct H; destruct H0; split; cbn.
    apply Zinf.add_1; auto.
    replace (- (n1 + n2)) with ((-n1) + (-n2)) by lia. apply Zinf.add_1; auto.
  Qed.

  Definition opp (v: t) : t := {| low := high v; high := low v |}.

  Lemma opp_1:
    forall n v, In n v -> In (-n) (opp v).
Proof.
    unfold In, opp; intros; cbn. replace (- - n) with n by lia. tauto.
  Qed.

  Definition sub (N1 N2: t) : t := add N1 (opp N2).

  Lemma sub_1:
    forall n1 n2 N1 N2, In n1 N1 -> In n2 N2 -> In (n1 - n2) (sub N1 N2).
Proof.
    intros. apply add_1; auto. apply opp_1; auto.
  Qed.

meet calcule un minorant de ses deux arguments.
  Definition meet (N1 N2: t) : t :=
    {| low := Zinf.min (low N1) (low N2);
       high := Zinf.min (high N1) (high N2) |}.

  Lemma meet_1:
    forall n N1 N2, In n N1 -> In n N2 -> In n (meet N1 N2).
Proof.
    unfold In, meet; intros; cbn. split; apply Zinf.min_1; tauto.
  Qed.

isIn teste si une valeur concrète appartient à une valeur abstraite.
  Definition isIn (n: Z) (v: t) : bool :=
    Zinf.isIn n (high v) && Zinf.isIn (-n) (low v).

  Lemma isIn_1:
    forall n v, In n v -> isIn n v = true.
Proof.
    unfold In, isIn; intros.
    apply andb_true_intro; split; apply Zinf.isIn_1; tauto.
  Qed.

Opérateurs abstraits pour l'analyse inverse des comparaisons.

  Definition eq_inv (N1 N2: t) : t * t := (meet N1 N2, meet N1 N2).

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

  Definition ne_inv (N1 N2: t) : t * t := (N1, N2).

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

Pour la relation <=, la borne supérieure de N1 est au plus celle de N2, et la borne inférieure de N2 est au moins celle de N1.

  Definition le_inv (N1 N2: t) : t * t :=
    ( {| low := low N1; high := Zinf.min (high N1) (high N2) |},
      {| low := Zinf.min (low N1) (low N2); high := high N2 |} ).

  Lemma le_inv_1:
    forall n1 n2 a1 a2,
    In n1 a1 -> In n2 a2 -> n1 <= n2 ->
    In n1 (fst (le_inv a1 a2)) /\ In n2 (snd (le_inv a1 a2)).
Proof.
    unfold In, le_inv; intros; cbn.
    intuition auto; apply Zinf.min_1; auto.
    apply Zinf.In_mono with n2; auto.
    apply Zinf.In_mono with (-n1); auto. lia.
  Qed.

Pour la relation >, la borne supérieure de N1 est au moins celle de N2 + 1, et la borne supérieure de N2 est au moins celle de N1 - 1.

  Definition gt_inv (N1 N2: t) : t * t :=
    ( {| low := Zinf.min (low N1) (Zinf.pred (low N2)); high := high N1 |},
      {| low := low N2; high := Zinf.min (high N2) (Zinf.pred (high N1)) |} ).

  Lemma gt_inv_1:
    forall n1 n2 a1 a2,
    In n1 a1 -> In n2 a2 -> n1 > n2 ->
    In n1 (fst (gt_inv a1 a2)) /\ In n2 (snd (gt_inv a1 a2)).
Proof.
    unfold In, gt_inv; intros; cbn.
    intuition auto; apply Zinf.min_1; auto.
    apply Zinf.In_mono with ((-n2) - 1). lia. apply Zinf.pred_1; auto.
    apply Zinf.In_mono with (n1 - 1). lia. apply Zinf.pred_1; auto.
  Qed.

L'opérateur d'élargissement.

  Definition widen (N1 N2: t) : t :=
    if isempty N1 then N2 else
    if isempty N2 then N1 else
    {| low := Zinf.widen (low N1) (low N2); high := Zinf.widen (high N1) (high N2) |}.

  Lemma widen_1: forall N1 N2, le N1 (widen N1 N2).
Proof.
    unfold le, widen; intros.
    destruct (isempty N1) eqn:E1. elim (isempty_1 n N1); auto.
    destruct (isempty N2) eqn:E2. auto.
    destruct H. split; apply Zinf.widen_1; auto.
  Qed.

  Definition measure (v: t) : nat :=
    if isempty v then 3%nat else (Zinf.measure (low v) + Zinf.measure (high v))%nat.

  Lemma measure_top: measure top = 0%nat.
Proof.
    auto.
  Qed.


  Remark isempty_widen: forall N1 N2,
    isempty N1 = false -> isempty N2 = false -> isempty (widen N1 N2) = false.
Proof.
    intros. destruct (isempty (widen N1 N2)) eqn:E; auto.
    destruct (isempty_2 _ H) as (n1 & IN1).
    elim (isempty_1 n1 _ E). apply widen_1; auto.
  Qed.
  
  Lemma widen_2:
    forall N1 N2, (measure (widen N1 N2) <= (measure N1))%nat.
Proof.
    unfold measure; intros.
    destruct (isempty N1) eqn:E1. unfold widen; rewrite E1.
    generalize (Zinf.measure_1 (low N2)) (Zinf.measure_1 (high N2)); intros.
    destruct (isempty N2); lia.
    destruct (isempty N2) eqn:E2. unfold widen; rewrite E1, E2, E1. lia.
    rewrite isempty_widen by auto.
    unfold widen; rewrite E1, E2; cbn.
    generalize (Zinf.widen_2 (low N1) (low N2)) (Zinf.widen_2 (high N1) (high N2)). lia.
  Qed.

  Lemma widen_3:
    forall N1 N2, ble N2 N1 = false -> (measure (widen N1 N2) < measure N1)%nat.
Proof.
    unfold ble, measure; intros.
    destruct (isempty N2) eqn:E2. discriminate.
    destruct (isempty N1) eqn:E1.
  - unfold widen; rewrite E1, E2.
    generalize (Zinf.measure_1 (low N2)) (Zinf.measure_1 (high N2)). lia.
  - rewrite isempty_widen by auto.
    unfold widen; rewrite E1, E2. cbn.
    generalize (Zinf.widen_2 (low N1) (low N2)) (Zinf.widen_2 (high N1) (high N2)); intros.
    destruct (Zinf.ble (high N2) (high N1)) eqn:LE.
    + cbn in H. apply Zinf.widen_3 in H. lia.
    + apply Zinf.widen_3 in LE. lia.
  Qed.

End Intervals.

5.9. Application: une analyse d'intervalles pour IMP


On applique l'analyseur générique au domaine des intervalles.

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

Premier programme:
    x := 0; y := 100; z := x + y;
    while x <= 10 do x := x + 1; y := y - 1 end

Definition prog1 :=
  ASSIGN "x" (CONST 0) ;;
  ASSIGN "y" (CONST 100) ;;
  ASSIGN "z" (PLUS (VAR "x") (VAR "y")) ;;
  WHILE (LESSEQUAL (VAR "x") (CONST 10))
        (ASSIGN "x" (PLUS (VAR "x") (CONST 1)) ;;
         ASSIGN "y" (MINUS (VAR "y") (CONST 1))).

Compute (let S := AIntervals.Cexec prog1 SIntervals.top in
           (SIntervals.get "x" S, SIntervals.get "y" S, SIntervals.get "z" S)).

Résultat:
      ({| Intervals.low := -11; Intervals.high := 11 |},
       {| Intervals.low := Inf; Intervals.high := 100 |},
       {| Intervals.low := -100; Intervals.high := 100 |})
c'est à dire: x est dans [11,11], y dans [-inf,100], et z dans [100,100].

Second programme:
    x := 0; y := 0;
    while x <= 1000 do y := x; x := x + 1 end

Definition prog2 :=
  ASSIGN "x" (CONST 0) ;;
  ASSIGN "y" (CONST 0) ;;
  WHILE (LESSEQUAL (VAR "x") (CONST 1000))
    (ASSIGN "y" (VAR "x") ;;
     ASSIGN "x" (PLUS (VAR "x") (CONST 1))).

Compute (let S := AIntervals.Cexec prog2 SIntervals.top in
           (SIntervals.get "x" S, SIntervals.get "y" S)).

Résultat:
      ({| Intervals.low := -1001; Intervals.high := 1001 |},
       {| Intervals.low := 0; Intervals.high := 1000 |})
c'est à dire: x est dans [1001,1001], et y dans [0,1000].