source: src/Clight/label.ma @ 1224

Last change on this file since 1224 was 1224, checked in by sacerdot, 8 years ago

Type of programs in common/AST made more dependent.
In particular, the type of internal functions is now dependent on the
list of global variables. This is already used in the back-end to rule
out from the syntax programs that have free variables.

Note: only the test Clight/test/search.c.ma has been ported to the new type.
The porting requires two very minor changes.

File size: 7.4 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 → res 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  do u ← check_universe_ok ? costgen;
180  OK ? (mk_function (fn_return f) (fn_params f) (fn_vars f) body).
181
182definition label_fundef : clight_fundef → res clight_fundef ≝
183λf. match f with
184[ CL_Internal f ⇒ do f ← label_function f; OK ? (CL_Internal f)
185| CL_External id args ty ⇒ OK ? (CL_External id args ty)
186].
187
188definition clight_label : clight_program → res clight_program ≝
189 λp. transform_partial_program … p label_fundef.
Note: See TracBrowser for help on using the repository browser.