cparser/SimplExpr.ml

   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
  21 open C
  22 open Cutil
  23 open 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
  43 let 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
  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. *)
  67
  68 let voidconst = { nullconst with etyp = TVoid [] }
  69
  70 (* Reads from volatile lvalues are also considered as side-effects if
  71    [volatilize] is true. *)
  72
  73 let 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
  84 let 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
 370 let 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
 405 let 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
 427 let 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
 434 let 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
 441 let 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
 558 let 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
 566 let program ?(volatile = false) p =
 567   volatilize := volatile;
 568   Transform.program ~fundef:simpl_fundef p