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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Lemma join_2:
forall s S1 S2,
In s S2 ->
In s (
join S1 S2).
Proof.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Lemma ble_2:
forall N1 N2,
le N1 N2 ->
ble N1 N2 =
true.
Proof.
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.
bot représente l'ensemble vide.
Definition bot:
t := {|
low :=
Fin 0;
high :=
Fin (-1) |}.
Lemma bot_1:
forall n, ~(
In n bot).
Proof.
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.
Lemma join_2:
forall n N1 N2,
In n N2 ->
In n (
join N1 N2).
Proof.
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.
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.
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.
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.
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.
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.
Lemma widen_2:
forall N1 N2, (
measure (
widen N1 N2) <= (
measure N1))%
nat.
Proof.
Lemma widen_3:
forall N1 N2,
ble N2 N1 =
false -> (
measure (
widen N1 N2) <
measure N1)%
nat.
Proof.
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
:=
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
:=
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].