-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathPolyLoop.v
158 lines (140 loc) · 6.09 KB
/
PolyLoop.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
(* *****************************************************************)
(* *)
(* Verified polyhedral AST generation *)
(* *)
(* Nathanaël Courant, Inria Paris *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 2.1 *)
(* of the License, or (at your option) any later version. *)
(* *)
(* *****************************************************************)
Require Import ZArith.
Require Import List.
Require Import Bool.
Require Import Psatz.
Require Import Linalg.
Require Import Misc.
Require Import Semantics.
Require Import Instr.
Require Import PolyTest.
Require Import PolyOperations.
Require Import ImpureAlarmConfig.
Open Scope Z_scope.
Notation affine_expr := (positive * (list Z * Z))%type.
Definition eval_affine_expr env (e : affine_expr) :=
(dot_product (fst (snd e)) (rev env) + snd (snd e)) / (Zpos (fst e)).
Definition affine_expr_ok env (e : affine_expr) :=
((dot_product (fst (snd e)) (rev env) + snd (snd e)) mod (Zpos (fst e)) =? 0).
Inductive poly_stmt :=
| PLoop : polyhedron -> poly_stmt -> poly_stmt
| PInstr : instr -> list affine_expr -> poly_stmt
| PSkip : poly_stmt
| PSeq : poly_stmt -> poly_stmt -> poly_stmt
| PGuard : polyhedron -> poly_stmt -> poly_stmt.
(* | PStrideGuard : list affine_expr -> poly_stmt -> poly_stmt. *)
Inductive poly_loop_semantics : poly_stmt -> list Z -> mem -> mem -> Prop :=
| PLInstr : forall i es env mem1 mem2,
(* forallb (affine_expr_ok env) es = true -> *)
instr_semantics i (map (eval_affine_expr env) es) mem1 mem2 ->
poly_loop_semantics (PInstr i es) env mem1 mem2
| PLSkip : forall env mem, poly_loop_semantics PSkip env mem mem
| PLSeq : forall env st1 st2 mem1 mem2 mem3,
poly_loop_semantics st1 env mem1 mem2 ->
poly_loop_semantics st2 env mem2 mem3 ->
poly_loop_semantics (PSeq st1 st2) env mem1 mem3
| PLGuardTrue : forall env t st mem1 mem2,
poly_loop_semantics st env mem1 mem2 ->
in_poly (rev env) t = true ->
poly_loop_semantics (PGuard t st) env mem1 mem2
| PLGuardFalse : forall env t st mem,
in_poly (rev env) t = false -> poly_loop_semantics (PGuard t st) env mem mem
| PLLoop : forall env p lb ub st mem1 mem2,
(forall x, in_poly (rev (x :: env)) p = true <-> lb <= x < ub) ->
iter_semantics (fun x => poly_loop_semantics st (x :: env)) (Zrange lb ub) mem1 mem2 ->
poly_loop_semantics (PLoop p st) env mem1 mem2.
Lemma PLInstr_inv_sem :
forall i es env mem1 mem2,
poly_loop_semantics (PInstr i es) env mem1 mem2 ->
instr_semantics i (map (eval_affine_expr env) es) mem1 mem2.
Proof.
intros i es env mem1 mem2 Hsem. inversion_clear Hsem. auto.
Qed.
Lemma PLLoop_inv_sem :
forall env p st mem1 mem2,
poly_loop_semantics (PLoop p st) env mem1 mem2 ->
exists lb ub, (forall x, in_poly (rev (x :: env)) p = true <-> lb <= x < ub) /\ iter_semantics (fun x => poly_loop_semantics st (x :: env)) (Zrange lb ub) mem1 mem2.
Proof.
intros env p st mem1 mem2 H. inversion_clear H.
eexists; eexists; eauto.
Qed.
Lemma PLGuard_inv_sem :
forall env p st mem1 mem2,
poly_loop_semantics (PGuard p st) env mem1 mem2 ->
if in_poly (rev env) p then poly_loop_semantics st env mem1 mem2 else mem1 = mem2.
Proof.
intros env p st mem1 mem2 H.
inversion_clear H.
- rewrite H1; simpl; auto.
- rewrite H0; simpl; auto.
Qed.
Lemma PLSeq_inv_sem :
forall env st1 st2 mem1 mem3,
poly_loop_semantics (PSeq st1 st2) env mem1 mem3 ->
exists mem2, poly_loop_semantics st1 env mem1 mem2 /\ poly_loop_semantics st2 env mem2 mem3.
Proof.
intros env p st mem1 mem3 H.
inversion_clear H. exists mem2; auto.
Qed.
Lemma PLSkip_inv_sem :
forall env mem1 mem2, poly_loop_semantics PSkip env mem1 mem2 -> mem1 = mem2.
Proof.
intros env mem1 mem2 H; inversion H; congruence.
Qed.
Fixpoint make_seq l :=
match l with
| nil => PSkip
| x :: l => PSeq x (make_seq l)
end.
Lemma make_seq_semantics :
forall l env mem1 mem2, poly_loop_semantics (make_seq l) env mem1 mem2 <->
iter_semantics (fun s => poly_loop_semantics s env) l mem1 mem2.
Proof.
induction l.
- intros; split; intros H; inversion_clear H; constructor.
- intros; split; simpl; intros H; inversion_clear H; econstructor; eauto; rewrite IHl in *; eauto.
Qed.
Fixpoint flatten_seq_rec stmt atend :=
match stmt with
| PSeq st1 st2 => flatten_seq_rec st1 (flatten_seq_rec st2 atend)
| PSkip => atend
| stmt => PSeq stmt atend
end.
Lemma flatten_seq_rec_semantics :
forall s atend env mem1 mem2, poly_loop_semantics (flatten_seq_rec s atend) env mem1 mem2 <-> poly_loop_semantics (PSeq s atend) env mem1 mem2.
Proof.
induction s; intros atend env mem1 mem2; simpl in *; try reflexivity.
- split.
+ intros H; econstructor; [constructor|auto].
+ intros H; apply PLSeq_inv_sem in H; destruct H as [mem3 [H1 H2]]; apply PLSkip_inv_sem in H1; congruence.
- rewrite IHs1. split.
+ intros H.
apply PLSeq_inv_sem in H; destruct H as [mem3 [H1 H2]]; rewrite IHs2 in H2.
apply PLSeq_inv_sem in H2; destruct H2 as [mem4 [H2 H3]].
econstructor; [econstructor|]; eauto.
+ intros H.
apply PLSeq_inv_sem in H; destruct H as [mem3 [H1 H2]].
apply PLSeq_inv_sem in H1; destruct H1 as [mem4 [H1 H3]].
econstructor; [eauto|].
rewrite IHs2; econstructor; eauto.
Qed.
Definition flatten_seq stmt := flatten_seq_rec stmt PSkip.
Lemma flatten_seq_semantics :
forall s env mem1 mem2, poly_loop_semantics (flatten_seq s) env mem1 mem2 <-> poly_loop_semantics s env mem1 mem2.
Proof.
intros s env mem1 mem2; unfold flatten_seq; rewrite flatten_seq_rec_semantics.
split.
- intros H; apply PLSeq_inv_sem in H; destruct H as [mem3 [H1 H2]]; apply PLSkip_inv_sem in H2. congruence.
- intros H; econstructor; [|constructor]; eauto.
Qed.