source: extracted/semantics.ml @ 3043

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 9.3 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 CexecSound
138
139open Casts
140
141open ClassifyOp
142
143open Smallstep
144
145open Extra_bool
146
147open FrontEndVal
148
149open Hide
150
151open ByteValues
152
153open GenMem
154
155open FrontEndMem
156
157open Globalenvs
158
159open Csem
160
161open SmallstepExec
162
163open Division
164
165open Z
166
167open BitVectorZ
168
169open Pointers
170
171open Values
172
173open Events
174
175open IOMonad
176
177open IO
178
179open Cexec
180
181open TypeComparison
182
183open SimplifyCasts
184
185open CostLabel
186
187open Coqlib
188
189open Proper
190
191open PositiveMap
192
193open Deqsets
194
195open ErrorMessages
196
197open PreIdentifiers
198
199open Errors
200
201open Extralib
202
203open Lists
204
205open Positive
206
207open Identifiers
208
209open Exp
210
211open Arithmetic
212
213open Vector
214
215open Div_and_mod
216
217open Util
218
219open FoldStuff
220
221open BitVector
222
223open Jmeq
224
225open Russell
226
227open List
228
229open Setoids
230
231open Monad
232
233open Option
234
235open Extranat
236
237open Bool
238
239open Relations
240
241open Nat
242
243open Integers
244
245open Hints_declaration
246
247open Core_notation
248
249open Pts
250
251open Logic
252
253open Types
254
255open AST
256
257open Csyntax
258
259open Label
260
261open Compiler
262
263open Stacksize
264
265open Executions
266
267open Measurable
268
269open Clight_abstract
270
271open Clight_classified_system
272
273open Cminor_semantics
274
275open Cminor_abstract
276
277open Cminor_classified_system
278
279open RTLabs_semantics
280
281open RTLabs_abstract
282
283open RTLabs_classified_system
284
285open ExtraMonads
286
287open ExtraGlobalenvs
288
289open I8051bis
290
291open BEMem
292
293open Joint_semantics
294
295open SemanticsUtils
296
297open Traces
298
299open Joint_fullexec
300
301open RTL_semantics
302
303open ERTL_semantics
304
305open Joint_LTL_LIN_semantics
306
307open LTL_semantics
308
309open LIN_semantics
310
311open Interpret2
312
313type preclassified_system_pass =
314  Measurable.preclassified_system
315  (* singleton inductive, whose constructor was mk_preclassified_system_pass *)
316
317(** val preclassified_system_pass_rect_Type4 :
318    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
319    preclassified_system_pass -> 'a1 **)
320let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_56 =
321  let pcs_pcs = x_56 in h_mk_preclassified_system_pass pcs_pcs __
322
323(** val preclassified_system_pass_rect_Type5 :
324    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
325    preclassified_system_pass -> 'a1 **)
326let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_58 =
327  let pcs_pcs = x_58 in h_mk_preclassified_system_pass pcs_pcs __
328
329(** val preclassified_system_pass_rect_Type3 :
330    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
331    preclassified_system_pass -> 'a1 **)
332let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_60 =
333  let pcs_pcs = x_60 in h_mk_preclassified_system_pass pcs_pcs __
334
335(** val preclassified_system_pass_rect_Type2 :
336    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
337    preclassified_system_pass -> 'a1 **)
338let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_62 =
339  let pcs_pcs = x_62 in h_mk_preclassified_system_pass pcs_pcs __
340
341(** val preclassified_system_pass_rect_Type1 :
342    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
343    preclassified_system_pass -> 'a1 **)
344let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_64 =
345  let pcs_pcs = x_64 in h_mk_preclassified_system_pass pcs_pcs __
346
347(** val preclassified_system_pass_rect_Type0 :
348    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
349    preclassified_system_pass -> 'a1 **)
350let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_66 =
351  let pcs_pcs = x_66 in h_mk_preclassified_system_pass pcs_pcs __
352
353(** val pcs_pcs :
354    Compiler.pass -> preclassified_system_pass ->
355    Measurable.preclassified_system **)
356let rec pcs_pcs p xxx =
357  let yyy = xxx in yyy
358
359(** val preclassified_system_pass_inv_rect_Type4 :
360    Compiler.pass -> preclassified_system_pass ->
361    (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
362let preclassified_system_pass_inv_rect_Type4 x1 hterm h1 =
363  let hcut = preclassified_system_pass_rect_Type4 x1 h1 hterm in hcut __
364
365(** val preclassified_system_pass_inv_rect_Type3 :
366    Compiler.pass -> preclassified_system_pass ->
367    (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
368let preclassified_system_pass_inv_rect_Type3 x1 hterm h1 =
369  let hcut = preclassified_system_pass_rect_Type3 x1 h1 hterm in hcut __
370
371(** val preclassified_system_pass_inv_rect_Type2 :
372    Compiler.pass -> preclassified_system_pass ->
373    (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
374let preclassified_system_pass_inv_rect_Type2 x1 hterm h1 =
375  let hcut = preclassified_system_pass_rect_Type2 x1 h1 hterm in hcut __
376
377(** val preclassified_system_pass_inv_rect_Type1 :
378    Compiler.pass -> preclassified_system_pass ->
379    (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
380let preclassified_system_pass_inv_rect_Type1 x1 hterm h1 =
381  let hcut = preclassified_system_pass_rect_Type1 x1 h1 hterm in hcut __
382
383(** val preclassified_system_pass_inv_rect_Type0 :
384    Compiler.pass -> preclassified_system_pass ->
385    (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
386let preclassified_system_pass_inv_rect_Type0 x1 hterm h1 =
387  let hcut = preclassified_system_pass_rect_Type0 x1 h1 hterm in hcut __
388
389(** val pcs_pcs__o__pcs_exec :
390    Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
391    SmallstepExec.fullexec **)
392let pcs_pcs__o__pcs_exec x0 x1 =
393  (pcs_pcs x0 x1).Measurable.pcs_exec
394
395(** val pcs_pcs__o__pcs_exec__o__es1 :
396    Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
397    SmallstepExec.trans_system **)
398let pcs_pcs__o__pcs_exec__o__es1 x0 x1 =
399  Measurable.pcs_exec__o__es1 (pcs_pcs x0 x1)
400
401(** val preclassified_system_of_pass :
402    Compiler.pass -> Compiler.syntax_of_pass -> preclassified_system_pass **)
403let preclassified_system_of_pass = function
404| Compiler.Clight_pass -> (fun x -> Clight_classified_system.clight_pcs)
405| Compiler.Clight_switch_removed_pass ->
406  (fun x -> Clight_classified_system.clight_pcs)
407| Compiler.Clight_label_pass ->
408  (fun x -> Clight_classified_system.clight_pcs)
409| Compiler.Clight_simplified_pass ->
410  (fun x -> Clight_classified_system.clight_pcs)
411| Compiler.Cminor_pass -> (fun x -> Cminor_classified_system.cminor_pcs)
412| Compiler.Rtlabs_pass -> (fun x -> RTLabs_classified_system.rTLabs_pcs)
413| Compiler.Rtl_separate_pass ->
414  (fun x ->
415    Joint_fullexec.joint_preclassified_system
416      (SemanticsUtils.sem_graph_params_to_sem_params
417        RTL_semantics.rTL_semantics_separate))
418| Compiler.Rtl_uniq_pass ->
419  (fun x ->
420    Joint_fullexec.joint_preclassified_system
421      (SemanticsUtils.sem_graph_params_to_sem_params
422        RTL_semantics.rTL_semantics_unique))
423| Compiler.Ertl_pass ->
424  (fun x ->
425    Joint_fullexec.joint_preclassified_system
426      (SemanticsUtils.sem_graph_params_to_sem_params
427        ERTL_semantics.eRTL_semantics))
428| Compiler.Ltl_pass ->
429  (fun x ->
430    Joint_fullexec.joint_preclassified_system
431      (SemanticsUtils.sem_graph_params_to_sem_params
432        LTL_semantics.lTL_semantics))
433| Compiler.Lin_pass ->
434  (fun x ->
435    Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics)
436| Compiler.Assembly_pass ->
437  (fun prog ->
438    let { Types.fst = eta13; Types.snd = policy } = Obj.magic prog in
439    let { Types.fst = code; Types.snd = sigma } = eta13 in
440    Interpret2.aSM_preclassified_system code sigma policy)
441| Compiler.Object_code_pass ->
442  (fun prog -> Interpret2.oC_preclassified_system (Obj.magic prog))
443
444(** val run_and_print :
445    Compiler.pass -> Compiler.syntax_of_pass -> Nat.nat -> (Compiler.pass ->
446    Types.unit0) -> (StructuredTraces.intensional_event -> Types.unit0) ->
447    (Errors.errmsg -> Types.unit0) -> (Integers.int -> Types.unit0) ->
448    Types.unit0 **)
449let run_and_print pass prog n print_pass print_event print_error print_exit =
450  let res =
451    let pcs = preclassified_system_of_pass pass prog in
452    let prog0 = prog in
453    let g = (pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_global prog0
454    in
455    Monad.m_bind0 (Monad.max_def Errors.res0)
456      (Obj.magic
457        ((pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_initial_state
458          prog0)) (fun s0 ->
459      let i = print_pass pass in
460      let { Types.fst = trace; Types.snd = res } =
461        Measurable.observe_all_in_measurable n
462          (Measurable.pcs_to_cs (pcs_pcs pass pcs)
463            ((pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_global prog0))
464          print_event List.Nil s0
465      in
466      Obj.magic res)
467  in
468  (match Obj.magic res with
469   | Errors.OK n0 -> print_exit n0
470   | Errors.Error msg -> print_error msg)
471
Note: See TracBrowser for help on using the repository browser.