source: extracted/semantics.ml @ 2902

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

Quick hack to allow printing of OC code. It will be automatically removed
when exporting again (tonight).

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