source: extracted/semantics.ml @ 3080

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

New extraction.

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