source: extracted/semantics.ml @ 2829

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

Semantics files committed.

File size: 8.9 KB
Line 
1open Preamble
2
3open UtilBranch
4
5open ASMCostsSplit
6
7open AbstractStatus
8
9open StatusProofs
10
11open Interpret
12
13open ASMCosts
14
15open Assembly
16
17open Status
18
19open Fetch
20
21open PolicyFront
22
23open PolicyStep
24
25open Policy
26
27open ASM
28
29open BitVectorTrieSet
30
31open LINToASM
32
33open LIN
34
35open Linearise
36
37open LTLToLIN
38
39open Fixpoints
40
41open Set_adt
42
43open Liveness
44
45open Interference
46
47open Joint_LTL_LIN
48
49open LTL
50
51open ERTLptrToLTL
52
53open ERTLptr
54
55open ERTLToERTLptr
56
57open ERTL
58
59open RegisterSet
60
61open RTLToERTL
62
63open State
64
65open Bind_new
66
67open BindLists
68
69open Blocks
70
71open TranslateUtils
72
73open String
74
75open LabelledObjects
76
77open I8051
78
79open BackEndOps
80
81open Joint
82
83open RTL
84
85open RTLabsToRTL
86
87open Executions
88
89open StructuredTraces
90
91open RTLabs_semantics
92
93open RTLabs_abstract
94
95open RTLabs_traces
96
97open CostInj
98
99open Deqsets_extra
100
101open CostMisc
102
103open Listb_extra
104
105open CostSpec
106
107open CostCheck
108
109open Initialisation
110
111open BitVectorTrie
112
113open Graphs
114
115open Order
116
117open Registers
118
119open RTLabs_syntax
120
121open ToRTLabs
122
123open FrontEndOps
124
125open Cminor_syntax
126
127open ToCminor
128
129open MemProperties
130
131open MemoryInjections
132
133open Fresh
134
135open SwitchRemoval
136
137open Sets
138
139open Listb
140
141open Star
142
143open Frontend_misc
144
145open CexecInd
146
147open CexecSound
148
149open Casts
150
151open ClassifyOp
152
153open Smallstep
154
155open Extra_bool
156
157open FrontEndVal
158
159open Hide
160
161open ByteValues
162
163open GenMem
164
165open FrontEndMem
166
167open Globalenvs
168
169open Csem
170
171open SmallstepExec
172
173open Division
174
175open Z
176
177open BitVectorZ
178
179open Pointers
180
181open Values
182
183open Events
184
185open IOMonad
186
187open IO
188
189open Cexec
190
191open TypeComparison
192
193open SimplifyCasts
194
195open CostLabel
196
197open Coqlib
198
199open Proper
200
201open PositiveMap
202
203open Deqsets
204
205open ErrorMessages
206
207open PreIdentifiers
208
209open Errors
210
211open Extralib
212
213open Lists
214
215open Positive
216
217open Identifiers
218
219open Exp
220
221open Arithmetic
222
223open Vector
224
225open Div_and_mod
226
227open Util
228
229open FoldStuff
230
231open BitVector
232
233open Jmeq
234
235open Russell
236
237open List
238
239open Setoids
240
241open Monad
242
243open Option
244
245open Extranat
246
247open Bool
248
249open Relations
250
251open Nat
252
253open Integers
254
255open Hints_declaration
256
257open Core_notation
258
259open Pts
260
261open Logic
262
263open Types
264
265open AST
266
267open Csyntax
268
269open Label
270
271open Compiler
272
273open Measurable
274
275open Clight_abstract
276
277open Clight_classified_system
278
279open Cminor_semantics
280
281open Cminor_abstract
282
283open Cminor_classified_system
284
285open RTLabs_classified_system
286
287open ExtraGlobalenvs
288
289open I8051bis
290
291open BEMem
292
293open Joint_semantics
294
295open Traces
296
297open Joint_fullexec
298
299open ExtraMonads
300
301open SemanticsUtils
302
303open RTL_semantics
304
305open ERTL_semantics
306
307open ERTLptr_semantics
308
309open Joint_LTL_LIN_semantics
310
311open LTL_semantics
312
313open LIN_semantics
314
315type preclassified_system_pass =
316  Measurable.preclassified_system
317  (* singleton inductive, whose constructor was mk_preclassified_system_pass *)
318
319(** val preclassified_system_pass_rect_Type4 :
320    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
321    preclassified_system_pass -> 'a1 **)
322let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_198 =
323  let pcs_pcs = x_198 in h_mk_preclassified_system_pass pcs_pcs __
324
325(** val preclassified_system_pass_rect_Type5 :
326    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
327    preclassified_system_pass -> 'a1 **)
328let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_200 =
329  let pcs_pcs = x_200 in h_mk_preclassified_system_pass pcs_pcs __
330
331(** val preclassified_system_pass_rect_Type3 :
332    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
333    preclassified_system_pass -> 'a1 **)
334let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_202 =
335  let pcs_pcs = x_202 in h_mk_preclassified_system_pass pcs_pcs __
336
337(** val preclassified_system_pass_rect_Type2 :
338    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
339    preclassified_system_pass -> 'a1 **)
340let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_204 =
341  let pcs_pcs = x_204 in h_mk_preclassified_system_pass pcs_pcs __
342
343(** val preclassified_system_pass_rect_Type1 :
344    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
345    preclassified_system_pass -> 'a1 **)
346let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_206 =
347  let pcs_pcs = x_206 in h_mk_preclassified_system_pass pcs_pcs __
348
349(** val preclassified_system_pass_rect_Type0 :
350    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
351    preclassified_system_pass -> 'a1 **)
352let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_208 =
353  let pcs_pcs = x_208 in h_mk_preclassified_system_pass pcs_pcs __
354
355(** val pcs_pcs :
356    Compiler.pass -> preclassified_system_pass ->
357    Measurable.preclassified_system **)
358let rec pcs_pcs p xxx =
359  let yyy = xxx in yyy
360
361(** val preclassified_system_pass_inv_rect_Type4 :
362    Compiler.pass -> preclassified_system_pass ->
363    (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
364let preclassified_system_pass_inv_rect_Type4 x1 hterm h1 =
365  let hcut = preclassified_system_pass_rect_Type4 x1 h1 hterm in hcut __
366
367(** val preclassified_system_pass_inv_rect_Type3 :
368    Compiler.pass -> preclassified_system_pass ->
369    (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
370let preclassified_system_pass_inv_rect_Type3 x1 hterm h1 =
371  let hcut = preclassified_system_pass_rect_Type3 x1 h1 hterm in hcut __
372
373(** val preclassified_system_pass_inv_rect_Type2 :
374    Compiler.pass -> preclassified_system_pass ->
375    (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
376let preclassified_system_pass_inv_rect_Type2 x1 hterm h1 =
377  let hcut = preclassified_system_pass_rect_Type2 x1 h1 hterm in hcut __
378
379(** val preclassified_system_pass_inv_rect_Type1 :
380    Compiler.pass -> preclassified_system_pass ->
381    (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
382let preclassified_system_pass_inv_rect_Type1 x1 hterm h1 =
383  let hcut = preclassified_system_pass_rect_Type1 x1 h1 hterm in hcut __
384
385(** val preclassified_system_pass_inv_rect_Type0 :
386    Compiler.pass -> preclassified_system_pass ->
387    (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
388let preclassified_system_pass_inv_rect_Type0 x1 hterm h1 =
389  let hcut = preclassified_system_pass_rect_Type0 x1 h1 hterm in hcut __
390
391(** val pcs_pcs__o__pcs_exec :
392    Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
393    SmallstepExec.fullexec **)
394let pcs_pcs__o__pcs_exec x0 x1 =
395  (pcs_pcs x0 x1).Measurable.pcs_exec
396
397(** val pcs_pcs__o__pcs_exec__o__es1 :
398    Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
399    SmallstepExec.trans_system **)
400let pcs_pcs__o__pcs_exec__o__es1 x0 x1 =
401  Measurable.pcs_exec__o__es1 (pcs_pcs x0 x1)
402
403(** val preclassified_system_of_pass :
404    Compiler.pass -> preclassified_system_pass **)
405let preclassified_system_of_pass = function
406| Compiler.Clight_pass -> Clight_classified_system.clight_pcs
407| Compiler.Clight_switch_removed_pass -> Clight_classified_system.clight_pcs
408| Compiler.Clight_label_pass -> Clight_classified_system.clight_pcs
409| Compiler.Clight_simplified_pass -> Clight_classified_system.clight_pcs
410| Compiler.Cminor_pass -> Cminor_classified_system.cminor_pcs
411| Compiler.Rtlabs_pass -> RTLabs_classified_system.rTLabs_pcs
412| Compiler.Rtl_separate_pass ->
413  Joint_fullexec.joint_preclassified_system
414    (SemanticsUtils.sem_graph_params_to_sem_params
415      RTL_semantics.rTL_semantics_separate)
416| Compiler.Rtl_uniq_pass ->
417  Joint_fullexec.joint_preclassified_system
418    (SemanticsUtils.sem_graph_params_to_sem_params
419      RTL_semantics.rTL_semantics_unique)
420| Compiler.Ertl_pass ->
421  Joint_fullexec.joint_preclassified_system
422    (SemanticsUtils.sem_graph_params_to_sem_params
423      ERTL_semantics.eRTL_semantics)
424| Compiler.Ertlptr_pass ->
425  Joint_fullexec.joint_preclassified_system
426    (SemanticsUtils.sem_graph_params_to_sem_params
427      ERTLptr_semantics.eRTLptr_semantics)
428| Compiler.Ltl_pass ->
429  Joint_fullexec.joint_preclassified_system LTL_semantics.lTL_semantics
430| Compiler.Lin_pass ->
431  Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics
432
433(** val run_and_print :
434    Compiler.pass -> Compiler.syntax_of_pass -> Nat.nat -> (Compiler.pass ->
435    Types.unit0) -> (StructuredTraces.intensional_event -> Types.unit0) ->
436    (Errors.errmsg -> Types.unit0) -> (Integers.int -> Types.unit0) ->
437    Types.unit0 **)
438let run_and_print pass prog n print_pass print_event print_error print_exit =
439  let pcs = preclassified_system_of_pass pass in
440  let prog0 = prog in
441  let g = (pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_global prog0 in
442  (match (pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_initial_state
443           prog0 with
444   | Errors.OK s0 ->
445     let i = print_pass pass in
446     let { Types.fst = trace; Types.snd = res } =
447       Measurable.observe_all_in_measurable n
448         (Measurable.pcs_to_cs (pcs_pcs pass pcs)
449           ((pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_global prog0))
450         print_event List.Nil s0
451     in
452     (match res with
453      | Errors.OK n0 -> print_exit n0
454      | Errors.Error msg -> print_error msg)
455   | Errors.Error msg -> print_error msg)
456
Note: See TracBrowser for help on using the repository browser.