source: extracted/semantics.ml @ 2951

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

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