source: src/semantics.ma @ 2876

Last change on this file since 2876 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: 2.7 KB
Line 
1include "compiler.ma".
2include "Clight/Clight_classified_system.ma".
3include "Cminor/Cminor_classified_system.ma".
4include "RTLabs/RTLabs_classified_system.ma".
5include "joint/joint_fullexec.ma".
6include "RTL/RTL_semantics.ma".
7include "ERTL/ERTL_semantics.ma".
8include "ERTLptr/ERTLptr_semantics.ma".
9include "LTL/LTL_semantics.ma".
10include "LIN/LIN_semantics.ma".
11include "ASM/Interpret2.ma".
12
13record preclassified_system_pass (P:pass) : Type[2] ≝
14 { pcs_pcs:> preclassified_system
15 ; pcs_ok: syntax_of_pass P = program … pcs_pcs
16 }.
17
18definition preclassified_system_of_pass:
19 ∀pass. syntax_of_pass pass → preclassified_system_pass pass ≝
20 λpass.
21  match pass return λpass.syntax_of_pass pass → preclassified_system_pass pass with
22  [ clight_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs …
23  | clight_switch_removed_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs …
24  | clight_label_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs …
25  | clight_simplified_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs …
26  | cminor_pass ⇒ λ_.mk_preclassified_system_pass … Cminor_pcs …
27  | rtlabs_pass ⇒ λ_.mk_preclassified_system_pass … RTLabs_pcs …
28  | rtl_separate_pass ⇒
29     λ_.mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_separate) …
30  | rtl_uniq_pass ⇒
31     λ_.mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_unique) …
32  | ertl_pass ⇒
33     λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTL_semantics) …
34  | ertlptr_pass ⇒
35     λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTLptr_semantics) …
36  | ltl_pass ⇒
37     λ_.mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) …
38  | lin_pass ⇒
39     λ_.mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ?
40  | assembly_pass ⇒
41     ?
42  | object_code_pass ⇒
43     λprog. mk_preclassified_system_pass ? (OC_preclassified_system prog) …
44  ].
45try % cases daemon
46qed.
47
48definition run_and_print:
49 ∀pass'. syntax_of_pass pass' → nat →
50  (pass → unit) → (intensional_event → unit) → (errmsg → unit) → (int → unit) → unit
51
52 λpass,prog,n,print_pass,print_event,print_error,print_exit.
53 let pcs ≝ preclassified_system_of_pass pass prog in
54  let prog ≝ prog⌈syntax_of_pass pass ↦ ?⌉ in
55  let g ≝ make_global … pcs prog in
56  match make_initial_state … pcs prog with
57  [ Error msg ⇒ print_error msg
58  | OK s0 ⇒
59     let i ≝ print_pass pass in
60     let 〈trace,res〉 ≝ observe_all_in_measurable n (pcs_to_cs pcs …) print_event [ ] s0 in
61     match res with
62     [ OK n ⇒ print_exit n
63     | Error msg ⇒ print_error msg ]].
64@pcs_ok
65qed.
Note: See TracBrowser for help on using the repository browser.