source: src/Clight/test/sum.test.ma @ 2353

Last change on this file since 2353 was 2353, checked in by campbell, 7 years ago

Put the post-loop cost label into the Clight while statement to get rid
of extra skips. (Soon to be followed by other loop constructs.)

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