source: src/Clight/label.ma @ 2896

Last change on this file since 2896 was 2588, checked in by garnier, 7 years ago

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

File size: 11.4 KB
Line 
1include "Clight/Csyntax.ma".
2
3(* Extract cost labels from a program. *)
4
5let rec labels_of_expr (e:expr) : list costlabel ≝
6match e with
7[ Expr e' _ ⇒
8  match e' with
9  [ Ederef e1 ⇒ labels_of_expr e1
10  | Eaddrof e1 ⇒ labels_of_expr e1
11  | Eunop _ e1 ⇒ labels_of_expr e1
12  | Ebinop _ e1 e2 ⇒ labels_of_expr e1 @ labels_of_expr e2
13  | Ecast _ e1 ⇒ labels_of_expr e1
14  | Econdition e1 e2 e3 ⇒ labels_of_expr e1 @ labels_of_expr e2 @ labels_of_expr e3
15  | Eandbool e1 e2 ⇒ labels_of_expr e1 @ labels_of_expr e2
16  | Eorbool e1 e2 ⇒ labels_of_expr e1 @ labels_of_expr e2
17  | Efield e1 _ ⇒ labels_of_expr e1
18  | Ecost cl e1 ⇒ cl::(labels_of_expr e1)
19  | _ ⇒ [ ]
20  ]
21].
22
23let rec labels_of_statement (s:statement) : list costlabel ≝
24match s with
25[ Sassign e1 e2 ⇒ labels_of_expr e1 @ labels_of_expr e2
26| Scall oe e1 es ⇒ option_map_def … labels_of_expr [ ] oe @ labels_of_expr e1 @ foldl … (λls,e. labels_of_expr e @ ls) [ ] es
27| Ssequence s1 s2 ⇒ labels_of_statement s1 @ labels_of_statement s2
28| Sifthenelse e1 s1 s2 ⇒ labels_of_expr e1 @ labels_of_statement s1 @ labels_of_statement s2
29| Swhile e1 s1 ⇒ labels_of_expr e1 @ labels_of_statement s1
30| Sdowhile e1 s1 ⇒ labels_of_expr e1 @ labels_of_statement s1
31| Sfor s1 e1 s2 s3 ⇒ labels_of_statement s1 @ labels_of_expr e1 @ labels_of_statement s2 @ labels_of_statement s3
32| Sreturn oe ⇒ option_map_def … labels_of_expr [ ] oe
33| Sswitch e1 ls ⇒ labels_of_expr e1 @ labels_of_labeled_statements ls
34| Slabel _ s1 ⇒ labels_of_statement s1
35| Scost cl s1 ⇒ cl::(labels_of_statement s1)
36| _ ⇒ [ ]
37] and labels_of_labeled_statements (ls:labeled_statements) : list costlabel ≝
38match ls with
39[ LSdefault s1 ⇒ labels_of_statement s1
40| LScase _ _ s1 ls1 ⇒ labels_of_statement s1 @ labels_of_labeled_statements ls1
41].
42
43definition labels_of_clight_fundef : ident × clight_fundef → list costlabel ≝
44λifd. match \snd ifd with
45[ CL_Internal f ⇒ labels_of_statement (fn_body f)
46| _ ⇒ [ ]
47].
48
49definition labels_of_clight : clight_program → list costlabel ≝
50λp. foldl … (λls,f. labels_of_clight_fundef f @ ls) [ ] (prog_funct ?? p).
51
52definition in_clight_program : clight_program → costlabel → Prop ≝
53λp,l. Exists … (λx.x=l) (labels_of_clight p).
54
55definition in_clight_label ≝
56  λp. Σl. in_clight_program p l.
57
58definition clight_cost_map ≝
59  λp. (in_clight_label p) → ℕ.
60
61definition clight_label_free : clight_program → bool ≝
62λp. match labels_of_clight p with [ nil ⇒ true | _ ⇒ false ].
63
64(* Adding labels *)
65
66definition add_cost_before : statement → universe CostTag → statement × (universe CostTag) ≝
67λs,gen.
68  let 〈l,gen〉 ≝ fresh … gen in
69  〈Scost l s, gen〉.
70
71definition add_cost_after : statement → universe CostTag → statement × (universe CostTag) ≝
72λs,gen.
73  let 〈l,gen〉 ≝ fresh … gen in
74  〈Ssequence s (Scost l Sskip), gen〉.
75
76definition add_cost_expr : expr → universe CostTag → expr × (universe CostTag) ≝
77λe,gen.
78  let 〈l,gen〉 ≝ fresh … gen in
79  〈Expr (Ecost l e) (typeof e), gen〉.
80
81definition const_int : intsize → nat → expr ≝
82λsz,n. Expr (Econst_int ? (repr sz n)) (Tint sz Signed).
83
84let rec label_expr (e:expr) (costgen:universe CostTag)
85        on e : expr × (universe CostTag) ≝
86match e with
87[ Expr ed ty ⇒ let 〈ed,costgen〉 ≝ label_expr_descr ed costgen ty in
88               〈Expr ed ty, costgen〉
89]
90and label_expr_descr (e:expr_descr) (costgen:universe CostTag) (ty:type)
91    on e : expr_descr × (universe CostTag) ≝
92match e with
93[ Ederef e' ⇒
94    let 〈e',costgen〉 ≝ label_expr e' costgen in
95    〈Ederef e', costgen〉
96| Eaddrof e' ⇒
97    let 〈e',costgen〉 ≝ label_expr e' costgen in
98    〈Eaddrof e', costgen〉
99| Eunop op e' ⇒
100    let 〈e',costgen〉 ≝ label_expr e' costgen in
101    〈Eunop op e', costgen〉
102| Ebinop op e1 e2 ⇒
103    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
104    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
105    〈Ebinop op e1 e2, costgen〉
106| Ecast ty e' ⇒
107    let 〈e',costgen〉 ≝ label_expr e' costgen in
108    〈Ecast ty e', costgen〉
109| Econdition e' e1 e2 ⇒
110    let 〈e',costgen〉 ≝ label_expr e' costgen in
111    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
112    let 〈e1,costgen〉 ≝ add_cost_expr e1 costgen in
113    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
114    let 〈e2,costgen〉 ≝ add_cost_expr e2 costgen in
115    〈Econdition e' e1 e2, costgen〉
116(* andbool and orbool are changed to conditionals to capture their
117   short-circuiting cost difference; note that we have to return 0 or 1, and
118   we get rather more cost labels than I'd like *)
119| Eandbool e1 e2 ⇒
120    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
121    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
122    match ty with
123    [ Tint sz sg ⇒
124      let 〈et,costgen〉 ≝ add_cost_expr (const_int sz 1) costgen in
125      let 〈ef,costgen〉 ≝ add_cost_expr (const_int sz 0) costgen in
126      let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
127      let 〈ef,costgen〉 ≝ add_cost_expr (const_int sz 0) costgen in
128      〈Econdition e1 e2 ef, costgen〉
129    | _ ⇒ (* default on 32 bit consts if inconsistent type. *)
130      let 〈et,costgen〉 ≝ add_cost_expr (const_int I32 1) costgen in
131      let 〈ef,costgen〉 ≝ add_cost_expr (const_int I32 0) costgen in
132      let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
133      let 〈ef,costgen〉 ≝ add_cost_expr (const_int I32 0) costgen in
134      〈Econdition e1 e2 ef, costgen〉       
135    ]
136| Eorbool e1 e2 ⇒
137    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
138    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
139    match ty with
140    [ Tint sz sg ⇒   
141      let 〈et,costgen〉 ≝ add_cost_expr (const_int sz 1) costgen in
142      let 〈ef,costgen〉 ≝ add_cost_expr (const_int sz 0) costgen in
143      let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
144      let 〈et,costgen〉 ≝ add_cost_expr (const_int sz 1) costgen in
145      〈Econdition e1 et e2, costgen〉
146    | _ ⇒
147      let 〈et,costgen〉 ≝ add_cost_expr (const_int I32 1) costgen in
148      let 〈ef,costgen〉 ≝ add_cost_expr (const_int I32 0) costgen in
149      let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
150      let 〈et,costgen〉 ≝ add_cost_expr (const_int I32 1) costgen in
151      〈Econdition e1 et e2, costgen〉
152    ]
153| Efield e' id ⇒
154    let 〈e',costgen〉 ≝ label_expr e' costgen in
155    〈Efield e' id, costgen〉
156(* The prototype asserts on preexisting cost labels, but I'd quite like to
157   keep them. *)
158| Ecost l e' ⇒
159    let 〈e',costgen〉 ≝ label_expr e' costgen in
160    〈Ecost l e', costgen〉
161
162(* The remaining expressions don't have subexpressions. *)
163| _ ⇒ 〈e,costgen〉
164].
165
166let rec label_exprs (l:list expr) (costgen:universe CostTag)
167        on l : list expr × (universe CostTag) ≝
168match l with
169[ nil ⇒ 〈nil ?,costgen〉
170| cons e es ⇒
171    let 〈e,costgen〉 ≝ label_expr e costgen in
172    let 〈es,costgen〉 ≝ label_exprs es costgen in
173    〈e::es,costgen〉
174].
175
176definition label_opt_expr ≝
177λoe,costgen. match oe with
178[ None ⇒ 〈None ?, costgen〉
179| Some e ⇒ let 〈e,costgen〉 ≝ label_expr e costgen in 〈Some ? e,costgen〉
180].
181
182
183let rec label_statement (s:statement) (costgen:universe CostTag)
184        on s : statement × (universe CostTag) ≝
185match s with
186[ Sskip ⇒ 〈Sskip,costgen〉
187| Sassign e1 e2 ⇒
188    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
189    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
190    〈Sassign e1 e2, costgen〉
191| Scall e_ret e_fn e_args ⇒
192    let 〈e_ret,costgen〉 ≝ label_opt_expr e_ret costgen in
193    let 〈e_fn,costgen〉 ≝ label_expr e_fn costgen in
194    let 〈e_args,costgen〉 ≝ label_exprs e_args costgen in
195    〈Scall e_ret e_fn e_args, costgen〉
196| Ssequence s1 s2 ⇒
197    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
198    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
199    〈Ssequence s1 s2, costgen〉
200| Sifthenelse e s1 s2 ⇒
201    let 〈e,costgen〉 ≝ label_expr e costgen in
202    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
203    let 〈s1,costgen〉 ≝ add_cost_before s1 costgen in
204    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
205    let 〈s2,costgen〉 ≝ add_cost_before s2 costgen in
206    〈Sifthenelse e s1 s2, costgen〉
207| Swhile e s' ⇒
208    let 〈e,costgen〉 ≝ label_expr e costgen in
209    let 〈s',costgen〉 ≝ label_statement s' costgen in
210    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
211    let 〈s,costgen〉 ≝ add_cost_after (Swhile e s') costgen in
212    〈s,costgen〉
213| Sdowhile e s' ⇒
214    let 〈e,costgen〉 ≝ label_expr e costgen in
215    let 〈s',costgen〉 ≝ label_statement s' costgen in
216    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
217    let 〈s,costgen〉 ≝ add_cost_after (Sdowhile e s') costgen in
218    〈s,costgen〉
219| Sfor s1 e s2 s3 ⇒
220    let 〈e,costgen〉 ≝ label_expr e costgen in
221    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
222    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
223    let 〈s3,costgen〉 ≝ label_statement s3 costgen in
224    let 〈s3,costgen〉 ≝ add_cost_before s3 costgen in
225    let 〈s,costgen〉 ≝ add_cost_after (Sfor s1 e s2 s3) costgen in
226    〈s,costgen〉
227| Sbreak ⇒ 〈Sbreak,costgen〉
228| Scontinue ⇒ 〈Scontinue,costgen〉
229| Sreturn opt_e ⇒
230    let 〈opt_e,costgen〉 ≝ label_opt_expr opt_e costgen in
231    〈Sreturn opt_e,costgen〉
232| Sswitch e ls ⇒
233    let 〈e,costgen〉 ≝ label_expr e costgen in
234    let 〈ls,costgen〉 ≝ label_lstatements ls costgen in
235    〈Sswitch e ls, costgen〉
236| Slabel l s' ⇒
237    let 〈s',costgen〉 ≝ label_statement s' costgen in
238    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
239    〈Slabel l s', costgen〉
240| Sgoto l ⇒ 〈Sgoto l, costgen〉
241
242(* The prototype asserts on preexisting cost labels, but I'd quite like to
243   keep them. *)
244| Scost l s' ⇒
245    let 〈s',costgen〉 ≝ label_statement s' costgen in
246    〈Scost l s', costgen〉
247]
248and label_lstatements (ls:labeled_statements) (costgen:universe CostTag)
249        on ls : labeled_statements × (universe CostTag) ≝
250match ls with
251[ LSdefault s ⇒
252    let 〈s,costgen〉 ≝ label_statement s costgen in
253    let 〈s,costgen〉 ≝ add_cost_before s costgen in
254    〈LSdefault s, costgen〉
255| LScase sz i s ls' ⇒
256    let 〈s,costgen〉 ≝ label_statement s costgen in
257    let 〈s,costgen〉 ≝ add_cost_before s costgen in
258    let 〈ls',costgen〉 ≝ label_lstatements ls' costgen in
259    〈LScase sz i s ls', costgen〉
260].
261
262definition label_function : universe CostTag → function → function × (universe CostTag) ≝
263λcostgen,f.
264  let 〈body,costgen〉 ≝ label_statement (fn_body f) costgen in
265  let 〈body,costgen〉 ≝ add_cost_before body costgen in
266    〈mk_function (fn_return f) (fn_params f) (fn_vars f) body, costgen〉.
267
268definition label_fundef : universe CostTag → clight_fundef → clight_fundef × (universe CostTag) ≝
269λgen,f. match f with
270[ CL_Internal f ⇒
271    let 〈f',gen'〉 ≝ label_function gen f in
272    〈CL_Internal f', gen'〉
273| CL_External id args ty ⇒ 〈CL_External id args ty, gen〉
274].
275
276
277
278definition clight_label : clight_program → clight_program × costlabel ≝
279λp.
280  let costgen ≝ new_universe CostTag in
281  let 〈init_cost, costgen〉 ≝ fresh … costgen in
282  〈\fst (transform_program_gen … costgen p (λ_.label_fundef)), init_cost〉.
Note: See TracBrowser for help on using the repository browser.