source: extracted/semantics.ml @ 2875

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

Pretty printing of object code integrated too.
A couple of axioms make execution via the preclassified_system
raise assert false.

File size: 9.4 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_3 =
329  let pcs_pcs = x_3 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_5 =
335  let pcs_pcs = x_5 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_7 =
341  let pcs_pcs = x_7 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_9 =
347  let pcs_pcs = x_9 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_11 =
353  let pcs_pcs = x_11 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_13 =
359  let pcs_pcs = x_13 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
409exception NotImplementedYet
410
411(** val preclassified_system_of_pass :
412    Compiler.pass -> Compiler.syntax_of_pass -> preclassified_system_pass **)
413let preclassified_system_of_pass = function
414| Compiler.Clight_pass -> (fun x -> Clight_classified_system.clight_pcs)
415| Compiler.Clight_switch_removed_pass ->
416  (fun x -> Clight_classified_system.clight_pcs)
417| Compiler.Clight_label_pass ->
418  (fun x -> Clight_classified_system.clight_pcs)
419| Compiler.Clight_simplified_pass ->
420  (fun x -> Clight_classified_system.clight_pcs)
421| Compiler.Cminor_pass -> (fun x -> Cminor_classified_system.cminor_pcs)
422| Compiler.Rtlabs_pass -> (fun x -> RTLabs_classified_system.rTLabs_pcs)
423| Compiler.Rtl_separate_pass ->
424  (fun x ->
425    Joint_fullexec.joint_preclassified_system
426      (SemanticsUtils.sem_graph_params_to_sem_params
427        RTL_semantics.rTL_semantics_separate))
428| Compiler.Rtl_uniq_pass ->
429  (fun x ->
430    Joint_fullexec.joint_preclassified_system
431      (SemanticsUtils.sem_graph_params_to_sem_params
432        RTL_semantics.rTL_semantics_unique))
433| Compiler.Ertl_pass ->
434  (fun x ->
435    Joint_fullexec.joint_preclassified_system
436      (SemanticsUtils.sem_graph_params_to_sem_params
437        ERTL_semantics.eRTL_semantics))
438| Compiler.Ertlptr_pass ->
439  (fun x ->
440    Joint_fullexec.joint_preclassified_system
441      (SemanticsUtils.sem_graph_params_to_sem_params
442        ERTLptr_semantics.eRTLptr_semantics))
443| Compiler.Ltl_pass ->
444  (fun x ->
445    Joint_fullexec.joint_preclassified_system
446      (SemanticsUtils.sem_graph_params_to_sem_params
447        LTL_semantics.lTL_semantics))
448| Compiler.Lin_pass ->
449  (fun x ->
450    Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics)
451| Compiler.Assembly_pass -> (fun prog -> raise NotImplementedYet)
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 try
462  let pcs = preclassified_system_of_pass pass prog in
463  let prog0 = prog in
464  let g = (pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_global prog0 in
465  (match (pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_initial_state
466           prog0 with
467   | Errors.OK s0 ->
468     let i = print_pass pass in
469     let { Types.fst = trace; Types.snd = res } =
470       Measurable.observe_all_in_measurable n
471         (Measurable.pcs_to_cs (pcs_pcs pass pcs)
472           ((pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_global prog0))
473         print_event List.Nil s0
474     in
475     (match res with
476      | Errors.OK n0 -> print_exit n0
477      | Errors.Error msg -> print_error msg)
478   | Errors.Error msg -> print_error msg)
479 with
480  NotImplementedYet -> Types.It
481
Note: See TracBrowser for help on using the repository browser.