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
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
|
open Vericert
open AST
open Abstr
open BinNums
open Coqlib
open Datatypes
open Errors
open GiblePargenproofEquiv
open List0
open Maps
open Optionmonad
open Predicate
open GiblePargen
open Integers
open Op
open Printf
let schedule_oracle l bb bbt =
match abstract_sequence_top bb with
| Some p ->
let (p0, m_expr) = p in
let (bb', reg_expr) = p0 in
(match abstract_sequence_top (concat (concat bbt)) with
| Some p1 ->
let (p2, m_expr_t) = p1 in
let (bbt', reg_expr_t) = p2 in
printf "F1:\n%a\n" PrintAbstr.print_forest bb';
printf "F2:\n%a\n" PrintAbstr.print_forest bbt'; flush stdout;
(&&)
((&&) ((&&) (if check_unhashed [] bb' bbt' then true else (Printf.printf "Failed 1\n"; false)) (empty_trees bb bbt))
(if (check_evaluability1_unhashed bb'.forest_preds bbt'.forest_preds reg_expr reg_expr_t) then true else (Printf.printf "Failed 12\n"; false)))
(if check_evaluability2_unhashed bb'.forest_preds bbt'.forest_preds m_expr m_expr_t then true else (Printf.printf "Failed 13\n"; false))
| None -> (printf "FAILED1\n"; false))
| None -> (printf "FAILED2\n"; false)
(** val check_scheduled_trees :
GibleSeq.SeqBB.t PTree.t -> GiblePar.ParBB.t PTree.t -> bool **)
let z = Camlcoq.Z.of_sint
let int n = Int.repr (z n)
let reg = Camlcoq.P.of_int
let pred = Camlcoq.P.of_int
let node = Camlcoq.P.of_int
let plit b p = Plit (b, pred p)
let const p d c: Gible.instr = RBop (p, Ointconst (z c), [], reg d)
let add p d1 r1 r2: Gible.instr = RBop (p, Olea (Aindexed2 (z 0)), [reg r1; reg r2], reg d1)
let mul p d1 r1 r2: Gible.instr = RBop (p, Omul, [reg r1; reg r2], reg d1)
let div p d1 r1 r2: Gible.instr = RBop (p, Odiv, [reg r1; reg r2], reg d1)
let seteq p d1 r1 r2: Gible.instr = RBsetpred (p, Ccomp Ceq, [reg r1; reg r2], pred d1)
let sett p d1 r1: Gible.instr = RBsetpred (p, Ccompimm (Ceq, int 0), [reg r1], pred d1)
let goto p n: Gible.instr = RBexit (p, (RBgoto (node n)))
let () =
(if schedule_oracle []
[ add None 2 1 4;
seteq (Some (plit true 1)) 3 4 2;
add (Some (plit true 1)) 1 2 4;
mul (Some (Pand (plit false 1, plit false 2))) 3 1 1;
mul (Some (plit true 2)) 3 1 4;
goto (Some (plit true 2)) 10;
mul (Some (plit false 2)) 3 3 3;
goto None 10;
]
[ [ [ mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; ];
[ add None 2 1 4;
add (Some (plit true 1)) 1 2 4;
seteq (Some (plit true 1)) 3 4 2; ] ];
[ [ mul (Some (plit true 2)) 3 1 4; ];
[ mul (Some (plit false 2)) 3 3 3; ];
[ goto None 10; ]
]
]
then Printf.printf "Passed 1\n"
else Printf.printf "Failed 1\n");
(* (if schedule_oracle [] *)
(* [ seteq (Some (plit true 1)) 2 1 2; *)
(* goto None 10; *)
(* ] *)
(* [ [ [ goto (Some (plit false 1)) 10; *)
(* seteq None 2 1 2; *)
(* goto None 10; *)
(* ] ] ] *)
(* then Printf.printf "Passed 1\n" *)
(* else Printf.printf "Failed 1\n"); *)
(* (if schedule_oracle [] *)
(* [ seteq None 2 1 2; *)
(* seteq None 3 1 2; *)
(* seteq (Some (Por (plit true 2, plit false 3))) 4 1 3; *)
(* ] *)
(* [ [ [ seteq None 2 1 2; *)
(* seteq None 3 1 2; *)
(* seteq None 4 1 3; *)
(* ] ] ] *)
(* then Printf.printf "Passed 1\n" *)
(* else Printf.printf "Failed 1\n"); *)
(* (if schedule_oracle [] *)
(* [ sett (Some (plit false 1)) 2 1; *)
(* div (Some (plit true 1)) 1 2 3; *)
(* ] *)
(* [ [ [ div (Some (plit true 1)) 1 2 3; *)
(* sett (Some (plit false 1)) 2 1; *)
(* ] ] ] *)
(* then Printf.printf "Passed 1\n" *)
(* else Printf.printf "Failed 1\n"); *)
(if schedule_oracle []
[ const (Some (plit true 1)) 1 0;
const (Some (Por (plit true 1, plit false 1))) 1 1;
]
[ [ [ const None 1 1;
] ] ]
then Printf.printf "Passed 1\n"
else Printf.printf "Failed 1\n");
(* (if schedule_oracle [(pred 3, pred 2)] *)
(* [ add None 2 1 4; *)
(* seteq None 1 10 11; *)
(* add (Some (plit true 1)) 1 2 4; *)
(* seteq (Some (plit true 1)) 2 12 13; *)
(* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *)
(* goto (Some (Pand (plit true 1, plit true 2))) 10; *)
(* mul (Some (Pand (plit true 1, plit false 2))) 3 3 3; *)
(* goto (Some (Pand (plit true 1, plit false 2))) 10; *)
(* seteq (Some (plit false 1)) 3 12 13; *)
(* mul (Some (Pand (plit false 1, plit true 3))) 3 1 4; *)
(* goto (Some (Pand (plit false 1, plit true 3))) 10; *)
(* mul (Some (Pand (plit false 1, plit false 3))) 3 1 1; *)
(* mul (Some (Pand (plit false 1, plit false 3))) 3 3 3; *)
(* goto (Some (Pand (plit false 1, plit false 3))) 10; *)
(* ] *)
(* [ [ [ seteq None 1 10 11; *)
(* add None 2 1 4; *)
(* seteq (Some (plit false 1)) 3 12 13; *)
(* seteq (Some (plit true 1)) 2 12 13; *)
(* add (Some (plit true 1)) 1 2 4; *)
(* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *)
(* mul (Some (Pand (plit true 1, plit false 2))) 3 3 3; *)
(* mul (Some (Pand (plit false 1, plit true 2))) 3 1 4; *)
(* mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; *)
(* mul (Some (Pand (plit false 1, plit false 2))) 3 3 3; *)
(* goto None 10; *)
(* ] ] ] *)
(* then Printf.printf "Passed 110\n" *)
(* else Printf.printf "Failed 102\n"); *)
(* (if schedule_oracle [(pred 3, pred 2)] *)
(* [ add None 2 1 4; *)
(* seteq None 1 10 11; *)
(* add (Some (plit true 1)) 1 2 4; *)
(* seteq (Some (plit true 1)) 2 12 13; *)
(* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *)
(* goto (Some (Pand (plit true 1, plit true 2))) 10; *)
(* mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; *)
(* goto (Some (Pand (plit true 1, plit false 2))) 10; *)
(* seteq (Some (plit false 1)) 3 12 13; *)
(* mul (Some (Pand (plit false 1, plit true 3))) 3 1 4; *)
(* goto (Some (Pand (plit false 1, plit true 3))) 10; *)
(* mul (Some (Pand (plit false 1, plit false 3))) 3 1 1; *)
(* mul (Some (Pand (plit false 1, plit false 3))) 5 3 3; *)
(* goto (Some (Pand (plit false 1, plit false 3))) 10; *)
(* ] *)
(* [ [ [ seteq None 1 10 11; *)
(* add None 2 1 4; *)
(* seteq (Some (plit false 1)) 3 12 13; *)
(* seteq (Some (plit true 1)) 2 12 13; *)
(* add (Some (plit true 1)) 1 2 4; *)
(* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *)
(* mul (Some (Pand (plit false 1, plit true 2))) 3 1 4; *)
(* mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; *)
(* mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; *)
(* mul (Some (Pand (plit false 1, plit false 2))) 5 3 3; *)
(* goto None 10; *)
(* ] ] ] *)
(* then Printf.printf "Passed 110\n" *)
(* else Printf.printf "Failed 102\n"); *)
(* (if schedule_oracle [(pred 3, pred 2)] *)
(* [ *)
(* seteq None 1 10 11; *)
(* seteq None 3 12 13; *)
(* seteq None 2 12 13; *)
(* add None 2 1 4; *)
(* mul (Some (Pand (plit false 1, plit false 3))) 3 1 1; *)
(* mul (Some (Pand (plit false 1, plit false 3))) 5 3 3; *)
(* goto (Some (Pand (plit false 1, plit false 3))) 10; *)
(* mul (Some (Pand (plit false 1, plit true 3))) 3 1 4; *)
(* goto (Some (Pand (plit false 1, plit true 3))) 10; *)
(* add (Some (plit true 1)) 1 2 4; *)
(* mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; *)
(* goto (Some (Pand (plit true 1, plit false 2))) 10; *)
(* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *)
(* goto (Some (Pand (plit true 1, plit true 2))) 10; *)
(* ] *)
(* [ [ [ seteq None 1 10 11; *)
(* seteq None 3 12 13; *)
(* seteq None 2 12 13; *)
(* mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; *)
(* add None 2 1 4; *)
(* add (Some (plit true 1)) 1 2 4; *)
(* mul (Some (Pand (plit false 1, plit true 2))) 3 1 4; *)
(* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *)
(* mul (Some (Pand (plit false 1, plit false 2))) 5 3 3; *)
(* mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; *)
(* goto None 10; *)
(* ] ] ] *)
(* then Printf.printf "Passed 110\n" *)
(* else Printf.printf "Failed 102\n") *)
|
