source: Deliverables/D2.2/8051/cparser/SimplExpr.ml @ 486

Last change on this file since 486 was 486, checked in by ayache, 8 years ago

Deliverable D2.2

File size: 18.8 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
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.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* Pulling side-effects out of expressions *)
17
18(* Assumes: nothing
19   Produces: simplified code *)
20
21open C
22open Cutil
23open Transform
24
25(* Grammar of simplified expressions:
26      e ::= EConst cst
27          | ESizeof ty
28          | EVar id
29          | EUnop pure-unop e
30          | EBinop pure-binop e e
31          | EConditional e e e
32          | ECast ty e
33
34   Grammar of statements produced to reflect side-effects in expressions:
35      s ::= Sskip
36          | Sdo (EBinop Oassign e e)
37          | Sdo (EBinop Oassign e (ECall e e* ))
38          | Sdo (Ecall e el)
39          | Sseq s s
40          | Sif e s s
41*)
42
43let rec is_simpl_expr e =
44  match e.edesc with
45  | EConst cst -> true
46  | ESizeof ty -> true
47  | EVar id -> true
48  | EUnop((Ominus|Oplus|Olognot|Onot|Oderef|Oaddrof), e1) ->
49      is_simpl_expr 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
55  | ECast(ty, e1) ->
56      is_simpl_expr e1
57  | _ ->
58      false
59
60(* "Destination" of a simplified expression *)
61
62type 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. *)
67
68let voidconst = { nullconst with etyp = TVoid [] }
69
70(* Reads from volatile lvalues are also considered as side-effects if
71   [volatilize] is true. *)
72
73let volatilize = ref false
74
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. *)
83
84let simpl_expr loc env e act =
85
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. *)
89
90  let new_temp ty =
91    Transform.new_temp (erase_attributes_type env ty) in
92
93  let eboolvalof e =
94    { edesc = EBinop(One, e, intconst 0L IInt, TInt(IInt, []));
95      etyp = TInt(IInt, []) } in
96
97  let sseq s1 s2 = Cutil.sseq loc s1 s2 in
98
99  let sassign e1 e2 =
100    { sdesc = Sdo {edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp}; 
101      sloc = loc } in
102
103  let sif e s1 s2 =
104    { sdesc = Sif(e, s1, s2); sloc = loc } in
105
106  let is_volatile_read e =
107    !volatilize
108    && List.mem AVolatile (attributes_of_type env e.etyp)
109    && is_lvalue env e in
110
111  let lhs_to_rhs e =
112    if is_volatile_read e
113    then (let t = new_temp e.etyp in (sassign t e, t))
114    else (sskip, e) in
115
116  let finish act s e =
117    match act with
118    | RHS ->
119        if is_volatile_read e
120        then (let t = new_temp e.etyp in (sseq s (sassign t e), t))
121        else (s, e)
122    | LHS ->
123        (s, e)
124    | Drop -> 
125        if is_volatile_read e
126        then (let t = new_temp e.etyp in (sseq s (sassign t e), voidconst))
127        else (s, voidconst)
128    | Set lhs ->
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
133
134   let rec simpl e act =
135    match e.edesc with
136
137    | EConst cst -> 
138        finish act sskip e
139
140    | ESizeof ty -> 
141        finish act sskip e
142
143    | EVar id ->
144        finish act sskip e
145
146    | EUnop(op, e1) ->
147
148        begin match op with
149
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}
153
154        | Oaddrof ->
155            let (s1, e1') = simpl e1 LHS in
156            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}
157
158        | Odot _ ->
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}
161
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
167            let e3 =
168              {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in
169            begin match act with
170            | Drop ->
171                (sseq s1 (sseq s2 (sassign e1' e3)), voidconst)
172            | _ ->
173                let tmp = new_temp e.etyp in
174                finish act (sseq s1 (sseq s2 (sseq (sassign tmp e3)
175                                                   (sassign e1' tmp))))
176                       tmp
177            end
178
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
183            begin match act with
184            | Drop ->
185                let (s2, e2') = lhs_to_rhs e1' in
186                let e3 =
187                  {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in
188                (sseq s1 (sseq s2 (sassign e1' e3)), voidconst)
189            | _ ->
190                let tmp = new_temp e.etyp in
191                let e3 =
192                  {edesc = EBinop(op', tmp, intconst 1L IInt, ty); etyp = ty} in
193                finish act (sseq s1 (sseq (sassign tmp e1') (sassign e1' e3))) 
194                       tmp
195            end
196
197        end
198
199    | EBinop(op, e1, e2, ty) ->
200
201        begin match op with
202
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}
209
210        | Oassign ->
211            if act = Drop && is_simpl_expr e1 then
212              simpl e2 (Set e1)
213            else begin
214              match act with
215              | Drop ->
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)
219              | _ ->
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)))
224                             tmp
225            end
226
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
233            let op' =
234              match op with
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
241            let e3 =
242              { edesc = EBinop(op', e11', e2', ty); etyp = ty } in
243            begin match act with
244            | Drop ->
245                (sseq s1 (sseq s11 (sseq s2 (sassign e1' e3))), voidconst)
246            | _ ->
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)))))
250                           tmp
251            end
252
253        | Ocomma ->
254            let (s1, _) = simpl e1 Drop in
255            let (s2, e2') = simpl e2 act in
256            (sseq s1 s2, e2')
257
258        | Ologand ->
259            let (s1, e1') = simpl e1 RHS in
260            if is_simpl_expr e2 then begin
261              finish act s1
262                     {edesc = EBinop(Ologand, e1', e2, ty); etyp = e.etyp}
263            end else begin
264              match act with
265              | Drop ->
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
271                  (sseq s1 (sif e1'
272                              (sseq s2 (sassign tmp (eboolvalof e2')))
273                              (sassign tmp (intconst 0L IInt))),
274                   tmp)
275              | Set lv ->
276                  let (s2, e2') = simpl e2 RHS in
277                  (sseq s1 (sif e1'
278                              (sseq s2 (sassign lv (eboolvalof e2')))
279                              (sassign lv (intconst 0L IInt))),
280                   voidconst)
281            end             
282
283        | Ologor ->
284            let (s1, e1') = simpl e1 RHS in
285            if is_simpl_expr e2 then begin
286              finish act s1
287                     {edesc = EBinop(Ologor, e1', e2, ty); etyp = e.etyp}
288            end else begin
289              match act with
290              | Drop ->
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
296                  (sseq s1 (sif e1'
297                              (sassign tmp (intconst 1L IInt))
298                              (sseq s2 (sassign tmp (eboolvalof e2')))),
299                   tmp)
300              | Set lv ->
301                  let (s2, e2') = simpl e2 RHS in
302                  (sseq s1 (sif e1'
303                              (sassign lv (intconst 1L IInt))
304                              (sseq s2 (sassign lv (eboolvalof e2')))),
305                   voidconst)
306            end             
307
308        end
309
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}
314        end else begin
315          match act with
316          | Drop ->
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)
325          | Set lv ->
326              let (s2, _) = simpl e2 (Set lv) in
327              let (s3, _) = simpl e3 (Set lv) in
328              (sseq s1 (sif e1' s2 s3), voidconst)
329        end
330
331    | ECast(ty, e1) ->
332        if is_void_type env ty then begin
333          if act <> Drop then
334            Errors.warning "%acast to 'void' in a context expecting a value\n"
335                           formatloc loc;
336            simpl e1 act
337        end else begin
338          let (s1, e1') = simpl e1 RHS in
339          finish act s1 {edesc = ECast(ty, e1'); etyp = e.etyp}
340        end
341
342    | ECall(e1, el) ->
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
346        begin match act with
347        | Drop ->
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)
354        | _ ->
355            let tmp = new_temp e.etyp in
356            finish act (sseq s1 (sseq s2 (sassign tmp e2))) tmp
357        end
358
359  and simpl_list = function
360    | [] -> (sskip, [])
361    | e1 :: el ->
362        let (s1, e1') = simpl e1 RHS in
363        let (s2, el') = simpl_list el in
364        (sseq s1 s2, e1' :: el')
365
366  in simpl e act
367
368(* Simplification of an initializer *)
369
370let simpl_initializer loc env i =
371
372  let rec simpl_init = function
373  | Init_single e ->
374      let (s, e') = simpl_expr loc env e RHS in
375      (s, Init_single e)
376  | Init_array il ->
377      let rec simpl = function
378      | [] -> (sskip, [])
379      | i1 :: il ->
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
384      (s, Init_array il')
385  | Init_struct(id, il) ->
386      let rec simpl = function
387      | [] -> (sskip, [])
388      | (f1, i1) :: il ->
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'))
397
398  in simpl_init i
399
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. *)
404
405let rec simpl_if loc env e s1 s2 =
406  match e.edesc with
407  | EUnop(Olognot, e1) ->
408      simpl_if loc env e1 s2 s1
409  | EBinop(Ologand, e1, e2, _) ->
410      simpl_if loc env e1
411        (simpl_if loc env e2 s1 s2)
412        s2
413  | EBinop(Ologor, e1, e2, _) ->
414      simpl_if loc env e1
415        s1
416        (simpl_if loc env e2 s1 s2)
417  | EConditional(e1, e2, e3) ->
418      simpl_if loc env e1
419        (simpl_if loc env e2 s1 s2)
420        (simpl_if loc env e3 s1 s2)
421  | _ ->
422      let (s, e') = simpl_expr loc env e RHS in
423      sseq loc s {sdesc = Sif(e', s1, s2); sloc = loc}
424
425(* Trivial statements for which [simpl_if] is applicable *)
426
427let trivial_stmt s =
428  match s.sdesc with
429  | Sskip | Scontinue | Sbreak | Sgoto _ -> true
430  | _ -> false
431
432(* Construct a simplified statement equivalent to [if (!e) exit; ]. *)
433
434let break_if_false loc env e =
435  simpl_if loc env e
436           {sdesc = Sskip; sloc = loc}
437           {sdesc = Sbreak; sloc = loc}
438
439(* Simplification of a statement *)
440
441let simpl_statement env s =
442
443  let rec simpl_stmt s =
444    match s.sdesc with
445
446  | Sskip ->
447      s
448
449  | Sdo e ->
450      let (s', _) = simpl_expr s.sloc env e Drop in
451      s'
452
453  | Sseq(s1, s2) ->
454      {sdesc = Sseq(simpl_stmt s1, simpl_stmt s2); sloc = s.sloc}
455
456  | Sif(e, s1, s2) ->
457      if trivial_stmt s1 && trivial_stmt s2 then
458        simpl_if s.sloc env e (simpl_stmt s1) (simpl_stmt s2)
459      else begin
460        let (s', e') = simpl_expr s.sloc env e RHS in
461        sseq s.sloc s'
462          {sdesc = Sif(e', simpl_stmt s1, simpl_stmt s2);
463           sloc = s.sloc}
464      end
465
466  | Swhile(e, s1) ->
467      if is_simpl_expr e then
468        {sdesc = Swhile(e, simpl_stmt s1); sloc = s.sloc}
469      else
470        {sdesc =
471           Swhile(intconst 1L IInt,
472                  sseq s.sloc (break_if_false s.sloc env e)
473                              (simpl_stmt s1));
474         sloc = s.sloc}
475
476  | Sdowhile(s1, e) ->
477      if is_simpl_expr e then
478        {sdesc = Sdowhile(simpl_stmt s1, e); sloc = s.sloc}
479      else begin
480        let tmp = new_temp (TInt(IInt, [])) in
481        let (s', _) = simpl_expr s.sloc env e (Set tmp) in
482        let s_init =
483          {sdesc = Sdo {edesc = EBinop(Oassign, tmp, intconst 1L IInt, tmp.etyp);
484                        etyp = tmp.etyp};
485           sloc = s.sloc} in
486        {sdesc = Sfor(s_init, tmp, s', simpl_stmt s1); sloc = s.sloc}
487      end
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.
491        {sdesc =
492           Sfor(sskip,
493                intconst 1L IInt,
494                break_if_false s.sloc env e,
495                simpl_stmt s1);
496         sloc = s.sloc}
497***)
498
499  | Sfor(s1, e, s2, s3) ->
500      if is_simpl_expr e then
501        {sdesc = Sfor(simpl_stmt s1,
502                      e,
503                      simpl_stmt s2,
504                      simpl_stmt s3);
505         sloc = s.sloc}
506      else
507        let (s', e') = simpl_expr s.sloc env e RHS in
508        {sdesc = Sfor(sseq s.sloc (simpl_stmt s1) s',
509                      e',
510                      sseq s.sloc (simpl_stmt s2) s',
511                      simpl_stmt s3);
512         sloc = s.sloc}
513
514  | Sbreak ->
515      s
516  | Scontinue ->
517      s
518
519  | Sswitch(e, s1) ->
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}
522
523  | Slabeled(lbl, s1) ->
524      {sdesc = Slabeled(lbl, simpl_stmt s1); sloc = s.sloc}
525
526  | Sgoto lbl ->
527      s
528
529  | Sreturn None ->
530      s
531
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}
535
536  | Sblock sl ->
537      {sdesc = Sblock(simpl_block sl); sloc = s.sloc}
538
539  | Sdecl d -> assert false
540
541  and simpl_block = function
542  | [] -> []
543  | ({sdesc = Sdecl(sto, id, ty, None)} as s) :: sl ->
544      s :: simpl_block sl
545  | ({sdesc = Sdecl(sto, id, ty, Some i)} as s) :: sl ->
546      let (s', i') = simpl_initializer s.sloc env i in
547      let sl' =
548           {sdesc = Sdecl(sto, id, ty, Some i'); sloc = s.sloc}
549        :: simpl_block sl in
550      if s'.sdesc = Sskip then sl' else s' :: sl'
551  | s :: sl ->
552      simpl_stmt s :: simpl_block sl
553
554  in simpl_stmt s
555
556(* Simplification of a function definition *)
557
558let simpl_fundef env f =
559  reset_temps();
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' }
563
564(* Entry point *)
565
566let program ?(volatile = false) p =
567  volatilize := volatile;
568  Transform.program ~fundef:simpl_fundef p
Note: See TracBrowser for help on using the repository browser.