1 (* *********************************************************************)
3 (* The Compcert verified compiler *)
5 (* Xavier Leroy, INRIA Paris-Rocquencourt *)
7 (* Copyright Institut National de Recherche en Informatique et en *)
8 (* Automatique. All rights reserved. This file is distributed *)
9 (* under the terms of the GNU General Public License as published by *)
10 (* the Free Software Foundation, either version 2 of the License, or *)
11 (* (at your option) any later version. This file is also distributed *)
12 (* under the terms of the INRIA Non-Commercial License Agreement. *)
14 (* *********************************************************************)
16 (* Pulling side-effects out of expressions *)
19 Produces: simplified code *)
25 (* Grammar of simplified expressions:
30 | EBinop pure-binop e e
34 Grammar of statements produced to reflect side-effects in expressions:
36 | Sdo (EBinop Oassign e e)
37 | Sdo (EBinop Oassign e (ECall e e* ))
43 let rec is_simpl_expr e =
48 | EUnop((Ominus|Oplus|Olognot|Onot|Oderef|Oaddrof), e1) ->
50 | EBinop((Oadd|Osub|Omul|Odiv|Omod|Oand|Oor|Oxor|Oshl|Oshr|
51 Oeq|One|Olt|Ogt|Ole|Oge|Oindex|Ologand|Ologor), e1, e2, _) ->
52 is_simpl_expr e1 && is_simpl_expr e2
53 | EConditional(e1, e2, e3) ->
54 is_simpl_expr e1 && is_simpl_expr e2 && is_simpl_expr e3
60 (* "Destination" of a simplified expression *)
62 type exp_destination =
63 | RHS (* evaluate as a r-value *)
64 | LHS (* evaluate as a l-value *)
65 | Drop (* drop its value, we only need the side-effects *)
66 | Set of exp (* assign it to the given simplified l.h.s. *)
68 let voidconst = { nullconst with etyp = TVoid [] }
70 (* Reads from volatile lvalues are also considered as side-effects if
71 [volatilize] is true. *)
73 let volatilize = ref false
75 (* [simpl_expr loc env e act] returns a pair [s, e'] of
76 a statement that performs the side-effects present in [e] and
77 a simplified, side-effect-free expression [e'].
78 If [act] is [RHS], [e'] evaluates to the same value as [e].
79 If [act] is [LHS], [e'] evaluates to the same location as [e].
80 If [act] is [Drop], [e'] is not meaningful and must be ignored.
81 If [act] is [Set lhs], [s] also performs an assignment
82 equivalent to [lhs = e]. [e'] is not meaningful. *)
84 let simpl_expr loc env e act =
86 (* Temporaries should not be [const] because we assign into them,
87 and need not be [volatile] because no one else is writing into them.
88 As for [restrict] it doesn't make sense anyway. *)
91 Transform.new_temp (erase_attributes_type env ty) in
94 { edesc = EBinop(One, e, intconst 0L IInt, TInt(IInt, []));
95 etyp = TInt(IInt, []) } in
97 let sseq s1 s2 = Cutil.sseq loc s1 s2 in
100 { sdesc = Sdo {edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp};
104 { sdesc = Sif(e, s1, s2); sloc = loc } in
106 let is_volatile_read e =
108 && List.mem AVolatile (attributes_of_type env e.etyp)
109 && is_lvalue env e in
112 if is_volatile_read e
113 then (let t = new_temp e.etyp in (sassign t e, t))
119 if is_volatile_read e
120 then (let t = new_temp e.etyp in (sseq s (sassign t e), t))
125 if is_volatile_read e
126 then (let t = new_temp e.etyp in (sseq s (sassign t e), voidconst))
129 if is_volatile_read e
130 then (let t = new_temp e.etyp in
131 (sseq s (sseq (sassign t e) (sassign lhs t)), voidconst))
132 else (sseq s (sassign lhs e), voidconst) in
134 let rec simpl e act =
150 | Ominus | Oplus | Olognot | Onot | Oderef | Oarrow _ ->
151 let (s1, e1') = simpl e1 RHS in
152 finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}
155 let (s1, e1') = simpl e1 LHS in
156 finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}
159 let (s1, e1') = simpl e1 (if act = LHS then LHS else RHS) in
160 finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}
162 | Opreincr | Opredecr ->
163 let (s1, e1') = simpl e1 LHS in
164 let (s2, e2') = lhs_to_rhs e1' in
165 let op' = match op with Opreincr -> Oadd | _ -> Osub in
166 let ty = unary_conversion env e.etyp in
168 {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in
171 (sseq s1 (sseq s2 (sassign e1' e3)), voidconst)
173 let tmp = new_temp e.etyp in
174 finish act (sseq s1 (sseq s2 (sseq (sassign tmp e3)
179 | Opostincr | Opostdecr ->
180 let (s1, e1') = simpl e1 LHS in
181 let op' = match op with Opostincr -> Oadd | _ -> Osub in
182 let ty = unary_conversion env e.etyp in
185 let (s2, e2') = lhs_to_rhs e1' in
187 {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in
188 (sseq s1 (sseq s2 (sassign e1' e3)), voidconst)
190 let tmp = new_temp e.etyp in
192 {edesc = EBinop(op', tmp, intconst 1L IInt, ty); etyp = ty} in
193 finish act (sseq s1 (sseq (sassign tmp e1') (sassign e1' e3)))
199 | EBinop(op, e1, e2, ty) ->
203 | Oadd | Osub | Omul | Odiv | Omod | Oand | Oor | Oxor
204 | Oshl | Oshr | Oeq | One | Olt | Ogt | Ole | Oge | Oindex ->
205 let (s1, e1') = simpl e1 RHS in
206 let (s2, e2') = simpl e2 RHS in
207 finish act (sseq s1 s2)
208 {edesc = EBinop(op, e1', e2', ty); etyp = e.etyp}
211 if act = Drop && is_simpl_expr e1 then
216 let (s1, e1') = simpl e1 LHS in
217 let (s2, e2') = simpl e2 RHS in
218 (sseq s1 (sseq s2 (sassign e1' e2')), voidconst)
220 let tmp = new_temp e.etyp in
221 let (s1, e1') = simpl e1 LHS in
222 let (s2, e2') = simpl e2 (Set tmp) in
223 finish act (sseq s1 (sseq s2 (sassign e1' tmp)))
227 | Oadd_assign | Osub_assign | Omul_assign | Odiv_assign
228 | Omod_assign | Oand_assign | Oor_assign | Oxor_assign
229 | Oshl_assign | Oshr_assign ->
230 let (s1, e1') = simpl e1 LHS in
231 let (s11, e11') = lhs_to_rhs e1' in
232 let (s2, e2') = simpl e2 RHS in
235 | Oadd_assign -> Oadd | Osub_assign -> Osub
236 | Omul_assign -> Omul | Odiv_assign -> Odiv
237 | Omod_assign -> Omod | Oand_assign -> Oand
238 | Oor_assign -> Oor | Oxor_assign -> Oxor
239 | Oshl_assign -> Oshl | Oshr_assign -> Oshr
240 | _ -> assert false in
242 { edesc = EBinop(op', e11', e2', ty); etyp = ty } in
245 (sseq s1 (sseq s11 (sseq s2 (sassign e1' e3))), voidconst)
247 let tmp = new_temp e.etyp in
248 finish act (sseq s1 (sseq s11 (sseq s2
249 (sseq (sassign tmp e3) (sassign e1' tmp)))))
254 let (s1, _) = simpl e1 Drop in
255 let (s2, e2') = simpl e2 act in
259 let (s1, e1') = simpl e1 RHS in
260 if is_simpl_expr e2 then begin
262 {edesc = EBinop(Ologand, e1', e2, ty); etyp = e.etyp}
266 let (s2, _) = simpl e2 Drop in
267 (sseq s1 (sif e1' s2 sskip), voidconst)
268 | RHS | LHS -> (* LHS should not happen *)
269 let (s2, e2') = simpl e2 RHS in
270 let tmp = new_temp e.etyp in
272 (sseq s2 (sassign tmp (eboolvalof e2')))
273 (sassign tmp (intconst 0L IInt))),
276 let (s2, e2') = simpl e2 RHS in
278 (sseq s2 (sassign lv (eboolvalof e2')))
279 (sassign lv (intconst 0L IInt))),
284 let (s1, e1') = simpl e1 RHS in
285 if is_simpl_expr e2 then begin
287 {edesc = EBinop(Ologor, e1', e2, ty); etyp = e.etyp}
291 let (s2, _) = simpl e2 Drop in
292 (sseq s1 (sif e1' sskip s2), voidconst)
293 | RHS | LHS -> (* LHS should not happen *)
294 let (s2, e2') = simpl e2 RHS in
295 let tmp = new_temp e.etyp in
297 (sassign tmp (intconst 1L IInt))
298 (sseq s2 (sassign tmp (eboolvalof e2')))),
301 let (s2, e2') = simpl e2 RHS in
303 (sassign lv (intconst 1L IInt))
304 (sseq s2 (sassign lv (eboolvalof e2')))),
310 | EConditional(e1, e2, e3) ->
311 let (s1, e1') = simpl e1 RHS in
312 if is_simpl_expr e2 && is_simpl_expr e3 then begin
313 finish act s1 {edesc = EConditional(e1', e2, e3); etyp = e.etyp}
317 let (s2, _) = simpl e2 Drop in
318 let (s3, _) = simpl e3 Drop in
319 (sseq s1 (sif e1' s2 s3), voidconst)
320 | RHS | LHS -> (* LHS should not happen *)
321 let tmp = new_temp e.etyp in
322 let (s2, _) = simpl e2 (Set tmp) in
323 let (s3, _) = simpl e3 (Set tmp) in
324 (sseq s1 (sif e1' s2 s3), tmp)
326 let (s2, _) = simpl e2 (Set lv) in
327 let (s3, _) = simpl e3 (Set lv) in
328 (sseq s1 (sif e1' s2 s3), voidconst)
332 if is_void_type env ty then begin
334 Errors.warning "%acast to 'void' in a context expecting a value\n"
338 let (s1, e1') = simpl e1 RHS in
339 finish act s1 {edesc = ECast(ty, e1'); etyp = e.etyp}
343 let (s1, e1') = simpl e1 RHS in
344 let (s2, el') = simpl_list el in
345 let e2 = { edesc = ECall(e1', el'); etyp = e.etyp } in
348 (sseq s1 (sseq s2 {sdesc = Sdo e2; sloc=loc}), voidconst)
349 | Set({edesc = EVar _} as lhs) ->
350 (* CompCert wants the destination of a call to be a variable,
351 not a more complex lhs. In the latter case, we
352 fall through the catch-all case below *)
353 (sseq s1 (sseq s2 (sassign lhs e2)), voidconst)
355 let tmp = new_temp e.etyp in
356 finish act (sseq s1 (sseq s2 (sassign tmp e2))) tmp
359 and simpl_list = function
362 let (s1, e1') = simpl e1 RHS in
363 let (s2, el') = simpl_list el in
364 (sseq s1 s2, e1' :: el')
368 (* Simplification of an initializer *)
370 let simpl_initializer loc env i =
372 let rec simpl_init = function
374 let (s, e') = simpl_expr loc env e RHS in
377 let rec simpl = function
380 let (s1, i1') = simpl_init i1 in
381 let (s2, il') = simpl il in
382 (sseq loc s1 s2, i1' :: il') in
383 let (s, il') = simpl il in
385 | Init_struct(id, il) ->
386 let rec simpl = function
389 let (s1, i1') = simpl_init i1 in
390 let (s2, il') = simpl il in
391 (sseq loc s1 s2, (f1, i1') :: il') in
392 let (s, il') = simpl il in
393 (s, Init_struct(id, il'))
394 | Init_union(id, f, i) ->
395 let (s, i') = simpl_init i in
396 (s, Init_union(id, f, i'))
400 (* Construct a simplified statement equivalent to [if (e) s1; else s2;].
401 Optimizes the case where e contains [&&] or [||] or [?].
402 [s1] or [s2] can be duplicated, so use only for small [s1] and [s2]
403 that do not define any labels. *)
405 let rec simpl_if loc env e s1 s2 =
407 | EUnop(Olognot, e1) ->
408 simpl_if loc env e1 s2 s1
409 | EBinop(Ologand, e1, e2, _) ->
411 (simpl_if loc env e2 s1 s2)
413 | EBinop(Ologor, e1, e2, _) ->
416 (simpl_if loc env e2 s1 s2)
417 | EConditional(e1, e2, e3) ->
419 (simpl_if loc env e2 s1 s2)
420 (simpl_if loc env e3 s1 s2)
422 let (s, e') = simpl_expr loc env e RHS in
423 sseq loc s {sdesc = Sif(e', s1, s2); sloc = loc}
425 (* Trivial statements for which [simpl_if] is applicable *)
429 | Sskip | Scontinue | Sbreak | Sgoto _ -> true
432 (* Construct a simplified statement equivalent to [if (!e) exit; ]. *)
434 let break_if_false loc env e =
436 {sdesc = Sskip; sloc = loc}
437 {sdesc = Sbreak; sloc = loc}
439 (* Simplification of a statement *)
441 let simpl_statement env s =
443 let rec simpl_stmt s =
450 let (s', _) = simpl_expr s.sloc env e Drop in
454 {sdesc = Sseq(simpl_stmt s1, simpl_stmt s2); sloc = s.sloc}
457 if trivial_stmt s1 && trivial_stmt s2 then
458 simpl_if s.sloc env e (simpl_stmt s1) (simpl_stmt s2)
460 let (s', e') = simpl_expr s.sloc env e RHS in
462 {sdesc = Sif(e', simpl_stmt s1, simpl_stmt s2);
467 if is_simpl_expr e then
468 {sdesc = Swhile(e, simpl_stmt s1); sloc = s.sloc}
471 Swhile(intconst 1L IInt,
472 sseq s.sloc (break_if_false s.sloc env e)
477 if is_simpl_expr e then
478 {sdesc = Sdowhile(simpl_stmt s1, e); sloc = s.sloc}
480 let tmp = new_temp (TInt(IInt, [])) in
481 let (s', _) = simpl_expr s.sloc env e (Set tmp) in
483 {sdesc = Sdo {edesc = EBinop(Oassign, tmp, intconst 1L IInt, tmp.etyp);
486 {sdesc = Sfor(s_init, tmp, s', simpl_stmt s1); sloc = s.sloc}
488 (*** Alternate translation that unfortunately puts a "break" in the
489 "next" part of a "for", something that is not supported
490 by Clight semantics, and has unknown behavior in gcc.
494 break_if_false s.sloc env e,
499 | Sfor(s1, e, s2, s3) ->
500 if is_simpl_expr e then
501 {sdesc = Sfor(simpl_stmt s1,
507 let (s', e') = simpl_expr s.sloc env e RHS in
508 {sdesc = Sfor(sseq s.sloc (simpl_stmt s1) s',
510 sseq s.sloc (simpl_stmt s2) s',
520 let (s', e') = simpl_expr s.sloc env e RHS in
521 sseq s.sloc s' {sdesc = Sswitch(e', simpl_stmt s1); sloc = s.sloc}
523 | Slabeled(lbl, s1) ->
524 {sdesc = Slabeled(lbl, simpl_stmt s1); sloc = s.sloc}
532 | Sreturn (Some e) ->
533 let (s', e') = simpl_expr s.sloc env e RHS in
534 sseq s.sloc s' {sdesc = Sreturn(Some e'); sloc = s.sloc}
537 {sdesc = Sblock(simpl_block sl); sloc = s.sloc}
539 | Sdecl d -> assert false
541 and simpl_block = function
543 | ({sdesc = Sdecl(sto, id, ty, None)} as s) :: sl ->
545 | ({sdesc = Sdecl(sto, id, ty, Some i)} as s) :: sl ->
546 let (s', i') = simpl_initializer s.sloc env i in
548 {sdesc = Sdecl(sto, id, ty, Some i'); sloc = s.sloc}
550 if s'.sdesc = Sskip then sl' else s' :: sl'
552 simpl_stmt s :: simpl_block sl
556 (* Simplification of a function definition *)
558 let simpl_fundef env f =
560 let body' = simpl_statement env f.fd_body in
561 let temps = get_temps() in
562 { f with fd_locals = f.fd_locals @ temps; fd_body = body' }
566 let program ?(volatile = false) p =
567 volatilize := volatile;
568 Transform.program ~fundef:simpl_fundef p