source: extracted/interference.ml @ 3043

Last change on this file since 3043 was 3043, checked in by sacerdot, 7 years ago

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 8.6 KB
Line 
1open Preamble
2
3open Fixpoints
4
5open Set_adt
6
7open Extra_bool
8
9open Coqlib
10
11open Values
12
13open FrontEndVal
14
15open GenMem
16
17open FrontEndMem
18
19open Globalenvs
20
21open String
22
23open Sets
24
25open Listb
26
27open LabelledObjects
28
29open BitVectorTrie
30
31open Graphs
32
33open I8051
34
35open Order
36
37open Registers
38
39open CostLabel
40
41open Hide
42
43open Proper
44
45open PositiveMap
46
47open Deqsets
48
49open ErrorMessages
50
51open PreIdentifiers
52
53open Errors
54
55open Extralib
56
57open Lists
58
59open Identifiers
60
61open Integers
62
63open AST
64
65open Division
66
67open Exp
68
69open Arithmetic
70
71open Setoids
72
73open Monad
74
75open Option
76
77open Extranat
78
79open Vector
80
81open FoldStuff
82
83open BitVector
84
85open Positive
86
87open Z
88
89open BitVectorZ
90
91open Pointers
92
93open ByteValues
94
95open BackEndOps
96
97open Joint
98
99open ERTL
100
101open Div_and_mod
102
103open Jmeq
104
105open Russell
106
107open Bool
108
109open Relations
110
111open Nat
112
113open Hints_declaration
114
115open Core_notation
116
117open Pts
118
119open Logic
120
121open Types
122
123open List
124
125open Util
126
127open Liveness
128
129type decision =
130| Decision_spill of Nat.nat
131| Decision_colour of I8051.register
132
133(** val decision_rect_Type4 :
134    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
135let rec decision_rect_Type4 h_decision_spill h_decision_colour = function
136| Decision_spill x_19002 -> h_decision_spill x_19002
137| Decision_colour x_19003 -> h_decision_colour x_19003
138
139(** val decision_rect_Type5 :
140    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
141let rec decision_rect_Type5 h_decision_spill h_decision_colour = function
142| Decision_spill x_19007 -> h_decision_spill x_19007
143| Decision_colour x_19008 -> h_decision_colour x_19008
144
145(** val decision_rect_Type3 :
146    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
147let rec decision_rect_Type3 h_decision_spill h_decision_colour = function
148| Decision_spill x_19012 -> h_decision_spill x_19012
149| Decision_colour x_19013 -> h_decision_colour x_19013
150
151(** val decision_rect_Type2 :
152    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
153let rec decision_rect_Type2 h_decision_spill h_decision_colour = function
154| Decision_spill x_19017 -> h_decision_spill x_19017
155| Decision_colour x_19018 -> h_decision_colour x_19018
156
157(** val decision_rect_Type1 :
158    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
159let rec decision_rect_Type1 h_decision_spill h_decision_colour = function
160| Decision_spill x_19022 -> h_decision_spill x_19022
161| Decision_colour x_19023 -> h_decision_colour x_19023
162
163(** val decision_rect_Type0 :
164    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
165let rec decision_rect_Type0 h_decision_spill h_decision_colour = function
166| Decision_spill x_19027 -> h_decision_spill x_19027
167| Decision_colour x_19028 -> h_decision_colour x_19028
168
169(** val decision_inv_rect_Type4 :
170    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
171    'a1 **)
172let decision_inv_rect_Type4 hterm h1 h2 =
173  let hcut = decision_rect_Type4 h1 h2 hterm in hcut __
174
175(** val decision_inv_rect_Type3 :
176    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
177    'a1 **)
178let decision_inv_rect_Type3 hterm h1 h2 =
179  let hcut = decision_rect_Type3 h1 h2 hterm in hcut __
180
181(** val decision_inv_rect_Type2 :
182    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
183    'a1 **)
184let decision_inv_rect_Type2 hterm h1 h2 =
185  let hcut = decision_rect_Type2 h1 h2 hterm in hcut __
186
187(** val decision_inv_rect_Type1 :
188    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
189    'a1 **)
190let decision_inv_rect_Type1 hterm h1 h2 =
191  let hcut = decision_rect_Type1 h1 h2 hterm in hcut __
192
193(** val decision_inv_rect_Type0 :
194    decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
195    'a1 **)
196let decision_inv_rect_Type0 hterm h1 h2 =
197  let hcut = decision_rect_Type0 h1 h2 hterm in hcut __
198
199(** val decision_discr : decision -> decision -> __ **)
200let decision_discr x y =
201  Logic.eq_rect_Type2 x
202    (match x with
203     | Decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
204     | Decision_colour a0 -> Obj.magic (fun _ dH -> dH __)) y
205
206(** val decision_jmdiscr : decision -> decision -> __ **)
207let decision_jmdiscr x y =
208  Logic.eq_rect_Type2 x
209    (match x with
210     | Decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
211     | Decision_colour a0 -> Obj.magic (fun _ dH -> dH __)) y
212
213type coloured_graph = { colouring : (Liveness.vertex -> decision);
214                        spilled_no : Nat.nat }
215
216(** val coloured_graph_rect_Type4 :
217    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
218    __ -> 'a1) -> coloured_graph -> 'a1 **)
219let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_19063 =
220  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19063 in
221  h_mk_coloured_graph colouring0 spilled_no0 __ __
222
223(** val coloured_graph_rect_Type5 :
224    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
225    __ -> 'a1) -> coloured_graph -> 'a1 **)
226let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_19065 =
227  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19065 in
228  h_mk_coloured_graph colouring0 spilled_no0 __ __
229
230(** val coloured_graph_rect_Type3 :
231    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
232    __ -> 'a1) -> coloured_graph -> 'a1 **)
233let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_19067 =
234  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19067 in
235  h_mk_coloured_graph colouring0 spilled_no0 __ __
236
237(** val coloured_graph_rect_Type2 :
238    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
239    __ -> 'a1) -> coloured_graph -> 'a1 **)
240let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_19069 =
241  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19069 in
242  h_mk_coloured_graph colouring0 spilled_no0 __ __
243
244(** val coloured_graph_rect_Type1 :
245    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
246    __ -> 'a1) -> coloured_graph -> 'a1 **)
247let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_19071 =
248  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19071 in
249  h_mk_coloured_graph colouring0 spilled_no0 __ __
250
251(** val coloured_graph_rect_Type0 :
252    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
253    __ -> 'a1) -> coloured_graph -> 'a1 **)
254let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_19073 =
255  let { colouring = colouring0; spilled_no = spilled_no0 } = x_19073 in
256  h_mk_coloured_graph colouring0 spilled_no0 __ __
257
258(** val colouring :
259    Fixpoints.valuation -> coloured_graph -> Liveness.vertex -> decision **)
260let rec colouring before xxx =
261  xxx.colouring
262
263(** val spilled_no : Fixpoints.valuation -> coloured_graph -> Nat.nat **)
264let rec spilled_no before xxx =
265  xxx.spilled_no
266
267(** val coloured_graph_inv_rect_Type4 :
268    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
269    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
270let coloured_graph_inv_rect_Type4 x1 hterm h1 =
271  let hcut = coloured_graph_rect_Type4 x1 h1 hterm in hcut __
272
273(** val coloured_graph_inv_rect_Type3 :
274    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
275    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
276let coloured_graph_inv_rect_Type3 x1 hterm h1 =
277  let hcut = coloured_graph_rect_Type3 x1 h1 hterm in hcut __
278
279(** val coloured_graph_inv_rect_Type2 :
280    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
281    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
282let coloured_graph_inv_rect_Type2 x1 hterm h1 =
283  let hcut = coloured_graph_rect_Type2 x1 h1 hterm in hcut __
284
285(** val coloured_graph_inv_rect_Type1 :
286    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
287    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
288let coloured_graph_inv_rect_Type1 x1 hterm h1 =
289  let hcut = coloured_graph_rect_Type1 x1 h1 hterm in hcut __
290
291(** val coloured_graph_inv_rect_Type0 :
292    Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
293    -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
294let coloured_graph_inv_rect_Type0 x1 hterm h1 =
295  let hcut = coloured_graph_rect_Type0 x1 h1 hterm in hcut __
296
297(** val coloured_graph_discr :
298    Fixpoints.valuation -> coloured_graph -> coloured_graph -> __ **)
299let coloured_graph_discr a1 x y =
300  Logic.eq_rect_Type2 x
301    (let { colouring = a0; spilled_no = a10 } = x in
302    Obj.magic (fun _ dH -> dH __ __ __ __)) y
303
304(** val coloured_graph_jmdiscr :
305    Fixpoints.valuation -> coloured_graph -> coloured_graph -> __ **)
306let coloured_graph_jmdiscr a1 x y =
307  Logic.eq_rect_Type2 x
308    (let { colouring = a0; spilled_no = a10 } = x in
309    Obj.magic (fun _ dH -> dH __ __ __ __)) y
310
311type coloured_graph_computer =
312  AST.ident List.list -> Joint.joint_internal_function -> Fixpoints.valuation
313  -> coloured_graph
314
Note: See TracBrowser for help on using the repository browser.