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