source: Deliverables/D2.3/8051-memoryspaces-branch/cparser/SimplExpr.ml @ 460

Last change on this file since 460 was 460, checked in by campbell, 9 years ago

Port memory spaces changes to latest prototype compiler.

File size: 19.0 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, []);
96      espace = Any } in
97
98  let sseq s1 s2 = Cutil.sseq loc s1 s2 in
99
100  let sassign e1 e2 =
101    { sdesc = Sdo {edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp; espace = e1.espace}; 
102      sloc = loc } in
103
104  let sif e s1 s2 =
105    { sdesc = Sif(e, s1, s2); sloc = loc } in
106
107  let is_volatile_read e =
108    !volatilize
109    && List.mem AVolatile (attributes_of_type env e.etyp)
110    && is_lvalue env e in
111
112  let lhs_to_rhs e =
113    if is_volatile_read e
114    then (let t = new_temp e.etyp in (sassign t e, t))
115    else (sskip, e) in
116
117  let finish act s e =
118    match act with
119    | RHS ->
120        if is_volatile_read e
121        then (let t = new_temp e.etyp in (sseq s (sassign t e), t))
122        else (s, e)
123    | LHS ->
124        (s, e)
125    | Drop -> 
126        if is_volatile_read e
127        then (let t = new_temp e.etyp in (sseq s (sassign t e), voidconst))
128        else (s, voidconst)
129    | Set lhs ->
130        if is_volatile_read e
131        then (let t = new_temp e.etyp in
132                 (sseq s (sseq (sassign t e) (sassign lhs t)), voidconst))
133        else (sseq s (sassign lhs e), voidconst) in
134
135   let rec simpl e act =
136    match e.edesc with
137
138    | EConst cst -> 
139        finish act sskip e
140
141    | ESizeof ty -> 
142        finish act sskip e
143
144    | EVar id ->
145        finish act sskip e
146
147    | EUnop(op, e1) ->
148
149        begin match op with
150
151        | Ominus | Oplus | Olognot | Onot | Oderef | Oarrow _ ->
152            let (s1, e1') = simpl e1 RHS in
153            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp; espace = e.espace}
154
155        | Oaddrof ->
156            let (s1, e1') = simpl e1 LHS in
157            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp; espace = e.espace}
158
159        | Odot _ ->
160            let (s1, e1') = simpl e1 (if act = LHS then LHS else RHS) in
161            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp; espace = e.espace}
162
163        | Opreincr | Opredecr ->
164            let (s1, e1') = simpl e1 LHS in
165            let (s2, e2') = lhs_to_rhs e1' in
166            let op' = match op with Opreincr -> Oadd | _ -> Osub in
167            let ty = unary_conversion env e.etyp in
168            let e3 =
169              {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty; espace = Any} in
170            begin match act with
171            | Drop ->
172                (sseq s1 (sseq s2 (sassign e1' e3)), voidconst)
173            | _ ->
174                let tmp = new_temp e.etyp in
175                finish act (sseq s1 (sseq s2 (sseq (sassign tmp e3)
176                                                   (sassign e1' tmp))))
177                       tmp
178            end
179
180        | Opostincr | Opostdecr ->
181            let (s1, e1') = simpl e1 LHS in
182            let op' = match op with Opostincr -> Oadd | _ -> Osub in
183            let ty = unary_conversion env e.etyp in
184            begin match act with
185            | Drop ->
186                let (s2, e2') = lhs_to_rhs e1' in
187                let e3 =
188                  {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty; espace = Any} in
189                (sseq s1 (sseq s2 (sassign e1' e3)), voidconst)
190            | _ ->
191                let tmp = new_temp e.etyp in
192                let e3 =
193                  {edesc = EBinop(op', tmp, intconst 1L IInt, ty); etyp = ty; espace = Any} in
194                finish act (sseq s1 (sseq (sassign tmp e1') (sassign e1' e3))) 
195                       tmp
196            end
197
198        end
199
200    | EBinop(op, e1, e2, ty) ->
201
202        begin match op with
203
204        | Oadd | Osub | Omul | Odiv | Omod | Oand | Oor | Oxor
205        | Oshl | Oshr | Oeq | One | Olt | Ogt | Ole | Oge | Oindex ->
206            let (s1, e1') = simpl e1 RHS in
207            let (s2, e2') = simpl e2 RHS in
208            finish act (sseq s1 s2)
209                       {edesc = EBinop(op, e1', e2', ty); etyp = e.etyp; espace = Any}
210
211        | Oassign ->
212            if act = Drop && is_simpl_expr e1 then
213              simpl e2 (Set e1)
214            else begin
215              match act with
216              | Drop ->
217                  let (s1, e1') = simpl e1 LHS in
218                  let (s2, e2') = simpl e2 RHS in
219                  (sseq s1 (sseq s2 (sassign e1' e2')), voidconst)
220              | _ ->
221                  let tmp = new_temp e.etyp in
222                  let (s1, e1') = simpl e1 LHS in
223                  let (s2, e2') = simpl e2 (Set tmp) in
224                  finish act (sseq s1 (sseq s2 (sassign e1' tmp)))
225                             tmp
226            end
227
228        | Oadd_assign | Osub_assign | Omul_assign | Odiv_assign
229        | Omod_assign | Oand_assign | Oor_assign  | Oxor_assign
230        | Oshl_assign | Oshr_assign ->
231            let (s1, e1') = simpl e1 LHS in
232            let (s11, e11') = lhs_to_rhs e1' in
233            let (s2, e2') = simpl e2 RHS in
234            let op' =
235              match op with
236              | Oadd_assign -> Oadd    | Osub_assign -> Osub
237              | Omul_assign -> Omul    | Odiv_assign -> Odiv
238              | Omod_assign -> Omod    | Oand_assign -> Oand
239              | Oor_assign  -> Oor     | Oxor_assign -> Oxor
240              | Oshl_assign -> Oshl    | Oshr_assign -> Oshr
241              | _ -> assert false in
242            let e3 =
243              { edesc = EBinop(op', e11', e2', ty); etyp = ty; espace = Any } in
244            begin match act with
245            | Drop ->
246                (sseq s1 (sseq s11 (sseq s2 (sassign e1' e3))), voidconst)
247            | _ ->
248                let tmp = new_temp e.etyp in
249                finish act (sseq s1 (sseq s11 (sseq s2
250                               (sseq (sassign tmp e3) (sassign e1' tmp)))))
251                           tmp
252            end
253
254        | Ocomma ->
255            let (s1, _) = simpl e1 Drop in
256            let (s2, e2') = simpl e2 act in
257            (sseq s1 s2, e2')
258
259        | Ologand ->
260            let (s1, e1') = simpl e1 RHS in
261            if is_simpl_expr e2 then begin
262              finish act s1
263                     {edesc = EBinop(Ologand, e1', e2, ty); etyp = e.etyp; espace = e.espace}
264            end else begin
265              match act with
266              | Drop ->
267                  let (s2, _) = simpl e2 Drop in
268                  (sseq s1 (sif e1' s2 sskip), voidconst)
269              | RHS | LHS ->  (* LHS should not happen *)
270                  let (s2, e2') = simpl e2 RHS in
271                  let tmp = new_temp e.etyp in
272                  (sseq s1 (sif e1'
273                              (sseq s2 (sassign tmp (eboolvalof e2')))
274                              (sassign tmp (intconst 0L IInt))),
275                   tmp)
276              | Set lv ->
277                  let (s2, e2') = simpl e2 RHS in
278                  (sseq s1 (sif e1'
279                              (sseq s2 (sassign lv (eboolvalof e2')))
280                              (sassign lv (intconst 0L IInt))),
281                   voidconst)
282            end             
283
284        | Ologor ->
285            let (s1, e1') = simpl e1 RHS in
286            if is_simpl_expr e2 then begin
287              finish act s1
288                     {edesc = EBinop(Ologor, e1', e2, ty); etyp = e.etyp; espace = e.espace}
289            end else begin
290              match act with
291              | Drop ->
292                  let (s2, _) = simpl e2 Drop in
293                  (sseq s1 (sif e1' sskip s2), voidconst)
294              | RHS | LHS ->  (* LHS should not happen *)
295                  let (s2, e2') = simpl e2 RHS in
296                  let tmp = new_temp e.etyp in
297                  (sseq s1 (sif e1'
298                              (sassign tmp (intconst 1L IInt))
299                              (sseq s2 (sassign tmp (eboolvalof e2')))),
300                   tmp)
301              | Set lv ->
302                  let (s2, e2') = simpl e2 RHS in
303                  (sseq s1 (sif e1'
304                              (sassign lv (intconst 1L IInt))
305                              (sseq s2 (sassign lv (eboolvalof e2')))),
306                   voidconst)
307            end             
308
309        end
310
311    | EConditional(e1, e2, e3) ->
312        let (s1, e1') = simpl e1 RHS in
313        if is_simpl_expr e2 && is_simpl_expr e3 then begin
314          finish act s1 {edesc = EConditional(e1', e2, e3); etyp = e.etyp; espace = e.espace}
315        end else begin
316          match act with
317          | Drop ->
318              let (s2, _) = simpl e2 Drop in
319              let (s3, _) = simpl e3 Drop in
320              (sseq s1 (sif e1' s2 s3), voidconst)
321          | RHS | LHS ->  (* LHS should not happen *)
322              let tmp = new_temp e.etyp in
323              let (s2, _) = simpl e2 (Set tmp) in
324              let (s3, _) = simpl e3 (Set tmp) in
325              (sseq s1 (sif e1' s2 s3), tmp)
326          | Set lv ->
327              let (s2, _) = simpl e2 (Set lv) in
328              let (s3, _) = simpl e3 (Set lv) in
329              (sseq s1 (sif e1' s2 s3), voidconst)
330        end
331
332    | ECast(ty, e1) ->
333        if is_void_type env ty then begin
334          if act <> Drop then
335            Errors.warning "%acast to 'void' in a context expecting a value\n"
336                           formatloc loc;
337            simpl e1 act
338        end else begin
339          let (s1, e1') = simpl e1 RHS in
340          finish act s1 {edesc = ECast(ty, e1'); etyp = e.etyp; espace = e.espace}
341        end
342
343    | ECall(e1, el) ->
344        let (s1, e1') = simpl e1 RHS in
345        let (s2, el') = simpl_list el in
346        let e2 = { edesc = ECall(e1', el'); etyp = e.etyp; espace = e.espace } in
347        begin match act with
348        | Drop ->
349            (sseq s1 (sseq s2 {sdesc = Sdo e2; sloc=loc}), voidconst)
350        | Set({edesc = EVar _} as lhs) ->
351            (* CompCert wants the destination of a call to be a variable,
352               not a more complex lhs.  In the latter case, we
353               fall through the catch-all case below *)
354            (sseq s1 (sseq s2 (sassign lhs e2)), voidconst)
355        | _ ->
356            let tmp = new_temp e.etyp in
357            finish act (sseq s1 (sseq s2 (sassign tmp e2))) tmp
358        end
359
360  and simpl_list = function
361    | [] -> (sskip, [])
362    | e1 :: el ->
363        let (s1, e1') = simpl e1 RHS in
364        let (s2, el') = simpl_list el in
365        (sseq s1 s2, e1' :: el')
366
367  in simpl e act
368
369(* Simplification of an initializer *)
370
371let simpl_initializer loc env i =
372
373  let rec simpl_init = function
374  | Init_single e ->
375      let (s, e') = simpl_expr loc env e RHS in
376      (s, Init_single e)
377  | Init_array il ->
378      let rec simpl = function
379      | [] -> (sskip, [])
380      | i1 :: il ->
381          let (s1, i1') = simpl_init i1 in
382          let (s2, il') = simpl il in
383          (sseq loc s1 s2, i1' :: il') in
384      let (s, il') = simpl il in
385      (s, Init_array il')
386  | Init_struct(id, il) ->
387      let rec simpl = function
388      | [] -> (sskip, [])
389      | (f1, i1) :: il ->
390          let (s1, i1') = simpl_init i1 in
391          let (s2, il') = simpl il in
392          (sseq loc s1 s2, (f1, i1') :: il') in
393      let (s, il') = simpl il in
394      (s, Init_struct(id, il'))
395  | Init_union(id, f, i) ->
396      let (s, i') = simpl_init i in
397      (s, Init_union(id, f, i'))
398
399  in simpl_init i
400
401(* Construct a simplified statement equivalent to [if (e) s1; else s2;].
402   Optimizes the case where e contains [&&] or [||] or [?].
403   [s1] or [s2] can be duplicated, so use only for small [s1] and [s2]
404   that do not define any labels. *)
405
406let rec simpl_if loc env e s1 s2 =
407  match e.edesc with
408  | EUnop(Olognot, e1) ->
409      simpl_if loc env e1 s2 s1
410  | EBinop(Ologand, e1, e2, _) ->
411      simpl_if loc env e1
412        (simpl_if loc env e2 s1 s2)
413        s2
414  | EBinop(Ologor, e1, e2, _) ->
415      simpl_if loc env e1
416        s1
417        (simpl_if loc env e2 s1 s2)
418  | EConditional(e1, e2, e3) ->
419      simpl_if loc env e1
420        (simpl_if loc env e2 s1 s2)
421        (simpl_if loc env e3 s1 s2)
422  | _ ->
423      let (s, e') = simpl_expr loc env e RHS in
424      sseq loc s {sdesc = Sif(e', s1, s2); sloc = loc}
425
426(* Trivial statements for which [simpl_if] is applicable *)
427
428let trivial_stmt s =
429  match s.sdesc with
430  | Sskip | Scontinue | Sbreak | Sgoto _ -> true
431  | _ -> false
432
433(* Construct a simplified statement equivalent to [if (!e) exit; ]. *)
434
435let break_if_false loc env e =
436  simpl_if loc env e
437           {sdesc = Sskip; sloc = loc}
438           {sdesc = Sbreak; sloc = loc}
439
440(* Simplification of a statement *)
441
442let simpl_statement env s =
443
444  let rec simpl_stmt s =
445    match s.sdesc with
446
447  | Sskip ->
448      s
449
450  | Sdo e ->
451      let (s', _) = simpl_expr s.sloc env e Drop in
452      s'
453
454  | Sseq(s1, s2) ->
455      {sdesc = Sseq(simpl_stmt s1, simpl_stmt s2); sloc = s.sloc}
456
457  | Sif(e, s1, s2) ->
458      if trivial_stmt s1 && trivial_stmt s2 then
459        simpl_if s.sloc env e (simpl_stmt s1) (simpl_stmt s2)
460      else begin
461        let (s', e') = simpl_expr s.sloc env e RHS in
462        sseq s.sloc s'
463          {sdesc = Sif(e', simpl_stmt s1, simpl_stmt s2);
464           sloc = s.sloc}
465      end
466
467  | Swhile(e, s1) ->
468      if is_simpl_expr e then
469        {sdesc = Swhile(e, simpl_stmt s1); sloc = s.sloc}
470      else
471        {sdesc =
472           Swhile(intconst 1L IInt,
473                  sseq s.sloc (break_if_false s.sloc env e)
474                              (simpl_stmt s1));
475         sloc = s.sloc}
476
477  | Sdowhile(s1, e) ->
478      if is_simpl_expr e then
479        {sdesc = Sdowhile(simpl_stmt s1, e); sloc = s.sloc}
480      else begin
481        let tmp = new_temp (TInt(IInt, [])) in
482        let (s', _) = simpl_expr s.sloc env e (Set tmp) in
483        let s_init =
484          {sdesc = Sdo {edesc = EBinop(Oassign, tmp, intconst 1L IInt, tmp.etyp);
485                        etyp = tmp.etyp; espace = tmp.espace};
486           sloc = s.sloc} in
487        {sdesc = Sfor(s_init, tmp, s', simpl_stmt s1); sloc = s.sloc}
488      end
489(*** Alternate translation that unfortunately puts a "break" in the
490     "next" part of a "for", something that is not supported
491     by Clight semantics, and has unknown behavior in gcc.
492        {sdesc =
493           Sfor(sskip,
494                intconst 1L IInt,
495                break_if_false s.sloc env e,
496                simpl_stmt s1);
497         sloc = s.sloc}
498***)
499
500  | Sfor(s1, e, s2, s3) ->
501      if is_simpl_expr e then
502        {sdesc = Sfor(simpl_stmt s1,
503                      e,
504                      simpl_stmt s2,
505                      simpl_stmt s3);
506         sloc = s.sloc}
507      else
508        let (s', e') = simpl_expr s.sloc env e RHS in
509        {sdesc = Sfor(sseq s.sloc (simpl_stmt s1) s',
510                      e',
511                      sseq s.sloc (simpl_stmt s2) s',
512                      simpl_stmt s3);
513         sloc = s.sloc}
514
515  | Sbreak ->
516      s
517  | Scontinue ->
518      s
519
520  | Sswitch(e, s1) ->
521      let (s', e') = simpl_expr s.sloc env e RHS in
522      sseq s.sloc s' {sdesc = Sswitch(e', simpl_stmt s1); sloc = s.sloc}
523
524  | Slabeled(lbl, s1) ->
525      {sdesc = Slabeled(lbl, simpl_stmt s1); sloc = s.sloc}
526
527  | Sgoto lbl ->
528      s
529
530  | Sreturn None ->
531      s
532
533  | Sreturn (Some e) ->
534      let (s', e') = simpl_expr s.sloc env e RHS in
535      sseq s.sloc s' {sdesc = Sreturn(Some e'); sloc = s.sloc}
536
537  | Sblock sl ->
538      {sdesc = Sblock(simpl_block sl); sloc = s.sloc}
539
540  | Sdecl d -> assert false
541
542  and simpl_block = function
543  | [] -> []
544  | ({sdesc = Sdecl(sto, id, ty, None)} as s) :: sl ->
545      s :: simpl_block sl
546  | ({sdesc = Sdecl(sto, id, ty, Some i)} as s) :: sl ->
547      let (s', i') = simpl_initializer s.sloc env i in
548      let sl' =
549           {sdesc = Sdecl(sto, id, ty, Some i'); sloc = s.sloc}
550        :: simpl_block sl in
551      if s'.sdesc = Sskip then sl' else s' :: sl'
552  | s :: sl ->
553      simpl_stmt s :: simpl_block sl
554
555  in simpl_stmt s
556
557(* Simplification of a function definition *)
558
559let simpl_fundef env f =
560  reset_temps();
561  let body' = simpl_statement env f.fd_body in
562  let temps = get_temps() in
563  { f with fd_locals = f.fd_locals @ temps; fd_body = body' }
564
565(* Entry point *)
566
567let program ?(volatile = false) p =
568  volatilize := volatile;
569  Transform.program ~fundef:simpl_fundef p
Note: See TracBrowser for help on using the repository browser.