1 | include "Clight/test/forcont.c.ma". |
---|
2 | |
---|
3 | example exec: finishes_with (repr I32 9) ? (exec_up_to clight_fullexec myprog 1000 [ ]). |
---|
4 | normalize (* you can examine the result here *) |
---|
5 | % |
---|
6 | qed. |
---|
7 | |
---|
8 | include "Clight/SimplifyCasts.ma". |
---|
9 | |
---|
10 | example es: finishes_with (repr I32 9) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]). |
---|
11 | normalize (* you can examine the result here *) |
---|
12 | % |
---|
13 | qed. |
---|
14 | |
---|
15 | include "Clight/toCminor.ma". |
---|
16 | include "Cminor/Cminor_semantics.ma". |
---|
17 | |
---|
18 | example e1: finishes_with (repr I32 9) ? |
---|
19 | (bind ? (snapshot state) (clight_to_cminor (simplify_program myprog)) |
---|
20 | (λp. exec_up_to Cminor_fullexec p 1000 [ ])). |
---|
21 | normalize |
---|
22 | % |
---|
23 | qed. |
---|
24 | |
---|
25 | include "Cminor/toRTLabs.ma". |
---|
26 | include "RTLabs/RTLabs_semantics.ma". |
---|
27 | include "Clight/label.ma". |
---|
28 | |
---|
29 | example e2: finishes_with (repr I32 9) ? ( |
---|
30 | let 〈p0,init〉 ≝ clight_label myprog in |
---|
31 | bind ? (snapshot state) (clight_to_cminor (simplify_program p0)) |
---|
32 | (λp1. let p2 ≝ cminor_to_rtlabs init p1 in |
---|
33 | exec_up_to RTLabs_fullexec p2 1000 [ ])). |
---|
34 | normalize |
---|
35 | % |
---|
36 | qed. |
---|
37 | |
---|
38 | include "RTLabs/CostCheck.ma". |
---|
39 | |
---|
40 | definition readable_body ≝ |
---|
41 | λfn. insert_sort ? |
---|
42 | (λx,y. leb (succ (match \fst x with [an_identifier z ⇒ z])) (match \fst y with [an_identifier z ⇒ z])) |
---|
43 | (elements ?? (f_graph fn)). |
---|
44 | (* |
---|
45 | example c2: result ? ( |
---|
46 | let 〈p0,init〉 ≝ clight_label myprog in |
---|
47 | ! p1 ← clight_to_cminor (simplify_program p0); |
---|
48 | let p2 ≝ cminor_to_rtlabs init p1 in |
---|
49 | match prog_funct … p2 with |
---|
50 | [ nil ⇒ Error ? (msg MISSING) |
---|
51 | | cons h _ ⇒ |
---|
52 | match \snd h with |
---|
53 | [ External _ ⇒ Error ? (msg EXTERNAL) |
---|
54 | | Internal fn ⇒ return 〈pi1 … (f_entry fn), readable_body fn〉 |
---|
55 | ] |
---|
56 | ]). |
---|
57 | normalize |
---|
58 | *) |
---|
59 | example c2: ( |
---|
60 | let 〈p0,init〉 ≝ clight_label myprog in |
---|
61 | ! p1 ← clight_to_cminor (simplify_program p0); |
---|
62 | let p2 ≝ cminor_to_rtlabs init p1 in |
---|
63 | return (check_cost_program p2)) = OK bool true. |
---|
64 | normalize |
---|
65 | % |
---|
66 | qed. |
---|
67 | |
---|
68 | |
---|
69 | |
---|
70 | (* |
---|
71 | include "RTLabs/RTLabsToRTL.ma". |
---|
72 | include alias "basics/lists/list.ma". |
---|
73 | |
---|
74 | definition take_out: ∀A. res A → A ≝ |
---|
75 | λA,a. match a with [ OK x ⇒ x | Error _ ⇒ ?]. |
---|
76 | cases daemon |
---|
77 | qed. |
---|
78 | |
---|
79 | example CSC: True. |
---|
80 | letin xxx ≝ |
---|
81 | (let p ≝ take_out … (clight_to_cminor myprog) in |
---|
82 | let p ≝ take_out … (cminor_to_rtlabs p) in |
---|
83 | (* (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p)) *) |
---|
84 | let p ≝ rtlabs_to_rtl p in |
---|
85 | (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ joint_if_code … f]) (prog_funct … p)) |
---|
86 | ) |
---|
87 | [2: cases daemon] |
---|
88 | normalize in xxx; |
---|
89 | |
---|
90 | |
---|
91 | [2: |
---|
92 | OK (list (codeT (prog_var_names … p) (rtl_params (prog_var_names … p)))) (list_map … (λx. match (\snd x) return λ_.codeT (prog_var_names … p) (rtl_params ?) with [External _ ⇒ ? | Internal f ⇒ ?(*joint_if_code ? (rtl_params ?) f*)]) (prog_funct … p))) |
---|
93 | (* OK ? (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p))) |
---|
94 | *) |
---|
95 | [2: check (joint_if_code (prog_var_names … p) ? f) |3: cases daemon ] |
---|
96 | normalize in xxx |
---|
97 | *) |
---|