source: src/Clight/label.ma @ 1521

Last change on this file since 1521 was 1515, checked in by campbell, 10 years ago

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File size: 7.3 KB
Line 
1include "Clight/Csyntax.ma".
2
3definition add_cost_before : statement → universe CostTag → statement × (universe CostTag) ≝
4λs,gen.
5  let 〈l,gen〉 ≝ fresh … gen in
6  〈Scost l s, gen〉.
7
8definition add_cost_after : statement → universe CostTag → statement × (universe CostTag) ≝
9λs,gen.
10  let 〈l,gen〉 ≝ fresh … gen in
11  〈Ssequence s (Scost l Sskip), gen〉.
12
13definition add_cost_expr : expr → universe CostTag → expr × (universe CostTag) ≝
14λe,gen.
15  let 〈l,gen〉 ≝ fresh … gen in
16  〈Expr (Ecost l e) (typeof e), gen〉.
17
18let rec label_expr (e:expr) (costgen:universe CostTag)
19        on e : expr × (universe CostTag) ≝
20match e with
21[ Expr ed ty ⇒ let 〈ed,costgen〉 ≝ label_expr_descr ed costgen in
22               〈Expr ed ty, costgen〉
23]
24and label_expr_descr (e:expr_descr) (costgen:universe CostTag)
25    on e : expr_descr × (universe CostTag) ≝
26match e with
27[ Ederef e' ⇒
28    let 〈e',costgen〉 ≝ label_expr e' costgen in
29    〈Ederef e', costgen〉
30| Eaddrof e' ⇒
31    let 〈e',costgen〉 ≝ label_expr e' costgen in
32    〈Eaddrof e', costgen〉
33| Eunop op e' ⇒
34    let 〈e',costgen〉 ≝ label_expr e' costgen in
35    〈Eunop op e', costgen〉
36| Ebinop op e1 e2 ⇒
37    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
38    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
39    〈Ebinop op e1 e2, costgen〉
40| Ecast ty e' ⇒
41    let 〈e',costgen〉 ≝ label_expr e' costgen in
42    〈Ecast ty e', costgen〉
43| Econdition e' e1 e2 ⇒
44    let 〈e',costgen〉 ≝ label_expr e' costgen in
45    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
46    let 〈e1,costgen〉 ≝ add_cost_expr e1 costgen in
47    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
48    let 〈e2,costgen〉 ≝ add_cost_expr e2 costgen in
49    〈Econdition e' e1 e2, costgen〉
50(* andbool and orbool are changed to conditionals to capture their
51   short-circuiting cost difference *)
52| Eandbool e1 e2 ⇒
53    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
54    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
55    let 〈e2,costgen〉 ≝ add_cost_expr e2 costgen in
56    let 〈ef,costgen〉 ≝ add_cost_expr (Expr (Econst_int I32 (zero ?)) (Tint I32 Signed)) costgen in
57    〈Econdition e1 e2 ef, costgen〉
58| Eorbool e1 e2 ⇒
59    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
60    let 〈et,costgen〉 ≝ add_cost_expr (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed)) costgen in
61    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
62    let 〈e2,costgen〉 ≝ add_cost_expr e2 costgen in
63    〈Econdition e1 et e2, costgen〉
64
65| Efield e' id ⇒
66    let 〈e',costgen〉 ≝ label_expr e' costgen in
67    〈Efield e' id, costgen〉
68(* The prototype asserts on preexisting cost labels, but I'd quite like to
69   keep them. *)
70| Ecost l e' ⇒
71    let 〈e',costgen〉 ≝ label_expr e' costgen in
72    〈Ecost l e', costgen〉
73
74(* The remaining expressions don't have subexpressions. *)
75| _ ⇒ 〈e,costgen〉
76].
77
78let rec label_exprs (l:list expr) (costgen:universe CostTag)
79        on l : list expr × (universe CostTag) ≝
80match l with
81[ nil ⇒ 〈nil ?,costgen〉
82| cons e es ⇒
83    let 〈e,costgen〉 ≝ label_expr e costgen in
84    let 〈es,costgen〉 ≝ label_exprs es costgen in
85    〈e::es,costgen〉
86].
87
88definition label_opt_expr ≝
89λoe,costgen. match oe with
90[ None ⇒ 〈None ?, costgen〉
91| Some e ⇒ let 〈e,costgen〉 ≝ label_expr e costgen in 〈Some ? e,costgen〉
92].
93
94
95let rec label_statement (s:statement) (costgen:universe CostTag)
96        on s : statement × (universe CostTag) ≝
97match s with
98[ Sskip ⇒ 〈Sskip,costgen〉
99| Sassign e1 e2 ⇒
100    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
101    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
102    〈Sassign e1 e2, costgen〉
103| Scall e_ret e_fn e_args ⇒
104    let 〈e_ret,costgen〉 ≝ label_opt_expr e_ret costgen in
105    let 〈e_fn,costgen〉 ≝ label_expr e_fn costgen in
106    let 〈e_args,costgen〉 ≝ label_exprs e_args costgen in
107    〈Scall e_ret e_fn e_args, costgen〉
108| Ssequence s1 s2 ⇒
109    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
110    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
111    〈Ssequence s1 s2, costgen〉
112| Sifthenelse e s1 s2 ⇒
113    let 〈e,costgen〉 ≝ label_expr e costgen in
114    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
115    let 〈s1,costgen〉 ≝ add_cost_before s1 costgen in
116    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
117    let 〈s2,costgen〉 ≝ add_cost_before s2 costgen in
118    〈Sifthenelse e s1 s2, costgen〉
119| Swhile e s' ⇒
120    let 〈e,costgen〉 ≝ label_expr e costgen in
121    let 〈s',costgen〉 ≝ label_statement s' costgen in
122    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
123    let 〈s,costgen〉 ≝ add_cost_after (Swhile e s') costgen in
124    〈s,costgen〉
125| Sdowhile e s' ⇒
126    let 〈e,costgen〉 ≝ label_expr e costgen in
127    let 〈s',costgen〉 ≝ label_statement s' costgen in
128    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
129    let 〈s,costgen〉 ≝ add_cost_after (Sdowhile e s') costgen in
130    〈s,costgen〉
131| Sfor s1 e s2 s3 ⇒
132    let 〈e,costgen〉 ≝ label_expr e costgen in
133    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
134    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
135    let 〈s3,costgen〉 ≝ label_statement s3 costgen in
136    let 〈s3,costgen〉 ≝ add_cost_before s3 costgen in
137    let 〈s,costgen〉 ≝ add_cost_after (Sfor s1 e s2 s3) costgen in
138    〈s,costgen〉
139| Sbreak ⇒ 〈Sbreak,costgen〉
140| Scontinue ⇒ 〈Scontinue,costgen〉
141| Sreturn opt_e ⇒
142    let 〈opt_e,costgen〉 ≝ label_opt_expr opt_e costgen in
143    〈Sreturn opt_e,costgen〉
144| Sswitch e ls ⇒
145    let 〈e,costgen〉 ≝ label_expr e costgen in
146    let 〈ls,costgen〉 ≝ label_lstatements ls costgen in
147    〈Sswitch e ls, costgen〉
148| Slabel l s' ⇒
149    let 〈s',costgen〉 ≝ label_statement s' costgen in
150    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
151    〈Slabel l s', costgen〉
152| Sgoto l ⇒ 〈Sgoto l, costgen〉
153
154(* The prototype asserts on preexisting cost labels, but I'd quite like to
155   keep them. *)
156| Scost l s' ⇒
157    let 〈s',costgen〉 ≝ label_statement s' costgen in
158    〈Scost l s', costgen〉
159]
160and label_lstatements (ls:labeled_statements) (costgen:universe CostTag)
161        on ls : labeled_statements × (universe CostTag) ≝
162match ls with
163[ LSdefault s ⇒
164    let 〈s,costgen〉 ≝ label_statement s costgen in
165    let 〈s,costgen〉 ≝ add_cost_before s costgen in
166    〈LSdefault s, costgen〉
167| LScase sz i s ls' ⇒
168    let 〈s,costgen〉 ≝ label_statement s costgen in
169    let 〈s,costgen〉 ≝ add_cost_before s costgen in
170    let 〈ls',costgen〉 ≝ label_lstatements ls' costgen in
171    〈LScase sz i s ls', costgen〉
172].
173
174definition label_function : function → function ≝
175λf.
176  let costgen ≝ new_universe CostTag in
177  let 〈body,costgen〉 ≝ label_statement (fn_body f) costgen in
178  let 〈body,costgen〉 ≝ add_cost_before body costgen in
179    mk_function (fn_return f) (fn_params f) (fn_vars f) body.
180
181definition label_fundef : clight_fundef → clight_fundef ≝
182λf. match f with
183[ CL_Internal f ⇒ CL_Internal (label_function f)
184| CL_External id args ty ⇒ CL_External id args ty
185].
186
187definition clight_label : clight_program → clight_program ≝
188 λp. transform_program … p label_fundef.
Note: See TracBrowser for help on using the repository browser.