extracted/simplifyCasts.ml

   1 open Preamble
   2
   3 open CostLabel
   4
   5 open Coqlib
   6
   7 open Proper
   8
   9 open PositiveMap
  10
  11 open Deqsets
  12
  13 open ErrorMessages
  14
  15 open PreIdentifiers
  16
  17 open Errors
  18
  19 open Extralib
  20
  21 open Lists
  22
  23 open Positive
  24
  25 open Identifiers
  26
  27 open Exp
  28
  29 open Arithmetic
  30
  31 open Vector
  32
  33 open Div_and_mod
  34
  35 open Util
  36
  37 open FoldStuff
  38
  39 open BitVector
  40
  41 open Jmeq
  42
  43 open Russell
  44
  45 open List
  46
  47 open Setoids
  48
  49 open Monad
  50
  51 open Option
  52
  53 open Extranat
  54
  55 open Bool
  56
  57 open Relations
  58
  59 open Nat
  60
  61 open Integers
  62
  63 open Hints_declaration
  64
  65 open Core_notation
  66
  67 open Pts
  68
  69 open Logic
  70
  71 open Types
  72
  73 open AST
  74
  75 open Csyntax
  76
  77 open TypeComparison
  78
  79 open ClassifyOp
  80
  81 open Smallstep
  82
  83 open Extra_bool
  84
  85 open FrontEndVal
  86
  87 open Hide
  88
  89 open ByteValues
  90
  91 open GenMem
  92
  93 open FrontEndMem
  94
  95 open Globalenvs
  96
  97 open Csem
  98
  99 open SmallstepExec
 100
 101 open Division
 102
 103 open Z
 104
 105 open BitVectorZ
 106
 107 open Pointers
 108
 109 open Values
 110
 111 open Events
 112
 113 open IOMonad
 114
 115 open IO
 116
 117 open Cexec
 118
 119 open Casts
 120
 121 open CexecInd
 122
 123 open Sets
 124
 125 open Listb
 126
 127 open Star
 128
 129 open Frontend_misc
 130
 131 (** val reduce_bits :
 132     Nat.nat -> Nat.nat -> Bool.bool -> BitVector.bitVector ->
 133     BitVector.bitVector Types.option **)
 134 let rec reduce_bits n m exp v =
 135   (match n with
 136    | Nat.O -> (fun v0 -> Types.Some v0)
 137    | Nat.S n' ->
 138      (fun v0 ->
 139        match BitVector.eq_b (Vector.head' (Nat.plus n' (Nat.S m)) v0) exp with
 140        | Bool.True ->
 141          reduce_bits n' m exp (Vector.tail (Nat.plus n' (Nat.S m)) v0)
 142        | Bool.False -> Types.None)) v
 143
 144 (** val pred_bitsize_of_intsize : AST.intsize -> Nat.nat **)
 145 let pred_bitsize_of_intsize sz =
 146   Nat.pred (AST.bitsize_of_intsize sz)
 147
 148 (** val signed : AST.signedness -> Bool.bool **)
 149 let signed = function
 150 | AST.Signed -> Bool.True
 151 | AST.Unsigned -> Bool.False
 152
 153 (** val simplify_int :
 154     AST.intsize -> AST.intsize -> AST.signedness -> AST.signedness ->
 155     AST.bvint -> AST.bvint Types.option **)
 156 let rec simplify_int sz sz' sg sg' i =
 157   let bit =
 158     Bool.andb (signed sg)
 159       (Vector.head'
 160         (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 161           Nat.O)))))))
 162           (Nat.times (AST.pred_size_intsize sz) (Nat.S (Nat.S (Nat.S (Nat.S
 163             (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) i)
 164   in
 165   (match Extranat.nat_compare (pred_bitsize_of_intsize sz)
 166            (pred_bitsize_of_intsize sz') with
 167    | Extranat.Nat_lt (x, x0) -> (fun i0 -> Types.None)
 168    | Extranat.Nat_eq x -> (fun i0 -> Types.Some i0)
 169    | Extranat.Nat_gt (x, y) ->
 170      (fun i0 ->
 171        match reduce_bits (Nat.S x) y bit i0 with
 172        | Types.None -> Types.None
 173        | Types.Some i' ->
 174          (match signed sg' with
 175           | Bool.True ->
 176             (match BitVector.eq_b bit (Vector.head' y i') with
 177              | Bool.True -> Types.Some i'
 178              | Bool.False -> Types.None)
 179           | Bool.False -> Types.Some i'))) i
 180
 181 (** val size_lt_dec : AST.intsize -> AST.intsize -> (__, __) Types.sum **)
 182 let size_lt_dec = function
 183 | AST.I8 ->
 184   (fun clearme0 ->
 185     match clearme0 with
 186     | AST.I8 -> Types.Inr __
 187     | AST.I16 -> Types.Inl __
 188     | AST.I32 -> Types.Inl __)
 189 | AST.I16 ->
 190   (fun clearme0 ->
 191     match clearme0 with
 192     | AST.I8 -> Types.Inr __
 193     | AST.I16 -> Types.Inr __
 194     | AST.I32 -> Types.Inl __)
 195 | AST.I32 ->
 196   (fun clearme0 ->
 197     match clearme0 with
 198     | AST.I8 -> Types.Inr __
 199     | AST.I16 -> Types.Inr __
 200     | AST.I32 -> Types.Inr __)
 201
 202 (** val size_not_lt_to_ge :
 203     AST.intsize -> AST.intsize -> (__, __) Types.sum **)
 204 let size_not_lt_to_ge clearme sz2 =
 205   (match clearme with
 206    | AST.I8 ->
 207      (fun clearme0 ->
 208        match clearme0 with
 209        | AST.I8 -> (fun _ -> Types.Inl __)
 210        | AST.I16 -> (fun _ -> Types.Inr __)
 211        | AST.I32 -> (fun _ -> Types.Inr __))
 212    | AST.I16 ->
 213      (fun clearme0 ->
 214        match clearme0 with
 215        | AST.I8 -> (fun _ -> Types.Inr __)
 216        | AST.I16 -> (fun _ -> Types.Inl __)
 217        | AST.I32 -> (fun _ -> Types.Inr __))
 218    | AST.I32 ->
 219      (fun clearme0 ->
 220        match clearme0 with
 221        | AST.I8 -> (fun _ -> Types.Inr __)
 222        | AST.I16 -> (fun _ -> Types.Inr __)
 223        | AST.I32 -> (fun _ -> Types.Inl __))) sz2 __
 224
 225 (** val sign_eq_dect :
 226     AST.signedness -> AST.signedness -> (__, __) Types.sum **)
 227 let sign_eq_dect = function
 228 | AST.Signed ->
 229   (fun clearme0 ->
 230     match clearme0 with
 231     | AST.Signed -> TypeComparison.sg_eq_dec AST.Signed AST.Signed
 232     | AST.Unsigned -> TypeComparison.sg_eq_dec AST.Signed AST.Unsigned)
 233 | AST.Unsigned ->
 234   (fun clearme0 ->
 235     match clearme0 with
 236     | AST.Signed -> TypeComparison.sg_eq_dec AST.Unsigned AST.Signed
 237     | AST.Unsigned -> TypeComparison.sg_eq_dec AST.Unsigned AST.Unsigned)
 238
 239 (** val necessary_conditions :
 240     AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness ->
 241     Bool.bool **)
 242 let necessary_conditions src_sz src_sg target_sz target_sg =
 243   match size_lt_dec target_sz src_sz with
 244   | Types.Inl _ -> Bool.True
 245   | Types.Inr _ ->
 246     (match TypeComparison.sz_eq_dec target_sz src_sz with
 247      | Types.Inl _ ->
 248        (match sign_eq_dect src_sg target_sg with
 249         | Types.Inl _ -> Bool.False
 250         | Types.Inr _ -> Bool.True)
 251      | Types.Inr _ -> Bool.False)
 252
 253 (** val assert_int_value :
 254     Values.val0 Types.option -> AST.intsize -> BitVector.bitVector
 255     Types.option **)
 256 let rec assert_int_value v expected_size =
 257   match v with
 258   | Types.None -> Types.None
 259   | Types.Some v0 ->
 260     (match v0 with
 261      | Values.Vundef -> Types.None
 262      | Values.Vint (sz, i) ->
 263        (match TypeComparison.sz_eq_dec sz expected_size with
 264         | Types.Inl _ ->
 265           Types.Some
 266             (Extralib.eq_rect_Type0_r expected_size (fun i0 -> i0) sz i)
 267         | Types.Inr _ -> Types.None)
 268      | Values.Vnull -> Types.None
 269      | Values.Vptr x -> Types.None)
 270
 271 (** val binop_simplifiable : Csyntax.binary_operation -> Bool.bool **)
 272 let binop_simplifiable = function
 273 | Csyntax.Oadd -> Bool.True
 274 | Csyntax.Osub -> Bool.True
 275 | Csyntax.Omul -> Bool.False
 276 | Csyntax.Odiv -> Bool.False
 277 | Csyntax.Omod -> Bool.False
 278 | Csyntax.Oand -> Bool.False
 279 | Csyntax.Oor -> Bool.False
 280 | Csyntax.Oxor -> Bool.False
 281 | Csyntax.Oshl -> Bool.False
 282 | Csyntax.Oshr -> Bool.False
 283 | Csyntax.Oeq -> Bool.False
 284 | Csyntax.One -> Bool.False
 285 | Csyntax.Olt -> Bool.False
 286 | Csyntax.Ogt -> Bool.False
 287 | Csyntax.Ole -> Bool.False
 288 | Csyntax.Oge -> Bool.False
 289
 290 (** val simplify_expr :
 291     Csyntax.expr -> AST.intsize -> AST.signedness -> (Bool.bool,
 292     Csyntax.expr) Types.prod Types.sig0 **)
 293 let rec simplify_expr e target_sz target_sg =
 294   (let Csyntax.Expr (ed, ty) = e in
 295   (fun _ ->
 296   (match ed with
 297    | Csyntax.Econst_int (cst_sz, i) ->
 298      (fun _ ->
 299        (match ty with
 300         | Csyntax.Tvoid ->
 301           (fun _ -> { Types.fst = Bool.False; Types.snd = e })
 302         | Csyntax.Tint (ty_sz, sg) ->
 303           (fun _ ->
 304             match TypeComparison.sz_eq_dec cst_sz ty_sz with
 305             | Types.Inl _ ->
 306               (match TypeComparison.type_eq_dec ty (Csyntax.Tint (target_sz,
 307                        target_sg)) with
 308                | Types.Inl _ -> { Types.fst = Bool.True; Types.snd = e }
 309                | Types.Inr _ ->
 310                  (match simplify_int cst_sz target_sz sg target_sg i with
 311                   | Types.None ->
 312                     (fun _ -> { Types.fst = Bool.False; Types.snd = e })
 313                   | Types.Some i' ->
 314                     (fun _ -> { Types.fst = Bool.True; Types.snd =
 315                       (Csyntax.Expr ((Csyntax.Econst_int (target_sz, i')),
 316                       (Csyntax.Tint (target_sz, target_sg)))) })) __)
 317             | Types.Inr _ -> { Types.fst = Bool.False; Types.snd = e })
 318         | Csyntax.Tpointer x ->
 319           (fun _ -> { Types.fst = Bool.False; Types.snd = e })
 320         | Csyntax.Tarray (x, x0) ->
 321           (fun _ -> { Types.fst = Bool.False; Types.snd = e })
 322         | Csyntax.Tfunction (x, x0) ->
 323           (fun _ -> { Types.fst = Bool.False; Types.snd = e })
 324         | Csyntax.Tstruct (x, x0) ->
 325           (fun _ -> { Types.fst = Bool.False; Types.snd = e })
 326         | Csyntax.Tunion (x, x0) ->
 327           (fun _ -> { Types.fst = Bool.False; Types.snd = e })
 328         | Csyntax.Tcomp_ptr x ->
 329           (fun _ -> { Types.fst = Bool.False; Types.snd = e })) __)
 330    | Csyntax.Evar id ->
 331      (fun _ -> { Types.fst =
 332        (TypeComparison.type_eq ty (Csyntax.Tint (target_sz, target_sg)));
 333        Types.snd = (Csyntax.Expr (ed, ty)) })
 334    | Csyntax.Ederef e1 ->
 335      (fun _ ->
 336        (let e2 = simplify_inside e1 in
 337          (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
 338          ((Csyntax.Ederef e2), ty)) })) __)
 339    | Csyntax.Eaddrof e1 ->
 340      (fun _ ->
 341        (let e2 = simplify_inside e1 in
 342          (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
 343          ((Csyntax.Eaddrof e2), ty)) })) __)
 344    | Csyntax.Eunop (op, e1) ->
 345      (fun _ ->
 346        (let e2 = simplify_inside e1 in
 347          (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
 348          ((Csyntax.Eunop (op, e2)), ty)) })) __)
 349    | Csyntax.Ebinop (op, lhs, rhs) ->
 350      (fun _ ->
 351        (match binop_simplifiable op with
 352         | Bool.True ->
 353           (fun _ ->
 354             match TypeComparison.assert_type_eq ty (Csyntax.typeof lhs) with
 355             | Errors.OK _ ->
 356               (match TypeComparison.assert_type_eq (Csyntax.typeof lhs)
 357                        (Csyntax.typeof rhs) with
 358                | Errors.OK _ ->
 359                  (let eta2011 = simplify_expr lhs target_sz target_sg in
 360                    (fun _ ->
 361                    (let { Types.fst = desired_type_lhs; Types.snd = lhs1 } =
 362                       eta2011
 363                     in
 364                    (fun _ ->
 365                    (let eta2010 = simplify_expr rhs target_sz target_sg in
 366                      (fun _ ->
 367                      (let { Types.fst = desired_type_rhs; Types.snd =
 368                         rhs1 } = eta2010
 369                       in
 370                      (fun _ ->
 371                      (match Bool.andb desired_type_lhs desired_type_rhs with
 372                       | Bool.True ->
 373                         (fun _ -> { Types.fst = Bool.True; Types.snd =
 374                           (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)),
 375                           (Csyntax.Tint (target_sz, target_sg)))) })
 376                       | Bool.False ->
 377                         (fun _ ->
 378                           (let lhs10 = simplify_inside lhs in
 379                             (fun _ ->
 380                             (let rhs10 = simplify_inside rhs in
 381                               (fun _ -> { Types.fst = Bool.False; Types.snd =
 382                               (Csyntax.Expr ((Csyntax.Ebinop (op, lhs10,
 383                               rhs10)), ty)) })) __)) __)) __)) __)) __)) __))
 384                    __
 385                | Errors.Error x ->
 386                  (let lhs1 = simplify_inside lhs in
 387                    (fun _ ->
 388                    (let rhs1 = simplify_inside rhs in
 389                      (fun _ -> { Types.fst = Bool.False; Types.snd =
 390                      (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)),
 391                      ty)) })) __)) __)
 392             | Errors.Error x ->
 393               (let lhs1 = simplify_inside lhs in
 394                 (fun _ ->
 395                 (let rhs1 = simplify_inside rhs in
 396                   (fun _ -> { Types.fst = Bool.False; Types.snd =
 397                   (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)) }))
 398                   __)) __)
 399         | Bool.False ->
 400           (fun _ ->
 401             (let lhs1 = simplify_inside lhs in
 402               (fun _ ->
 403               (let rhs1 = simplify_inside rhs in
 404                 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
 405                 ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)) })) __)) __)) __)
 406    | Csyntax.Ecast (cast_ty, castee) ->
 407      (fun _ ->
 408        (match cast_ty with
 409         | Csyntax.Tvoid ->
 410           (fun _ ->
 411             (let castee1 = simplify_inside castee in
 412               (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
 413               ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
 414         | Csyntax.Tint (cast_sz, cast_sg) ->
 415           (fun _ ->
 416             match TypeComparison.type_eq_dec ty cast_ty with
 417             | Types.Inl _ ->
 418               (match necessary_conditions cast_sz cast_sg target_sz target_sg with
 419                | Bool.True ->
 420                  (fun _ ->
 421                    (let eta2013 = simplify_expr castee target_sz target_sg in
 422                      (fun _ ->
 423                      (let { Types.fst = desired_type; Types.snd = castee1 } =
 424                         eta2013
 425                       in
 426                      (fun _ ->
 427                      (match desired_type with
 428                       | Bool.True ->
 429                         (fun _ -> { Types.fst = Bool.True; Types.snd =
 430                           castee1 })
 431                       | Bool.False ->
 432                         (fun _ ->
 433                           (let eta2012 = simplify_expr castee cast_sz cast_sg
 434                            in
 435                             (fun _ ->
 436                             (let { Types.fst = desired_type2; Types.snd =
 437                                castee2 } = eta2012
 438                              in
 439                             (fun _ ->
 440                             (match desired_type2 with
 441                              | Bool.True ->
 442                                (fun _ -> { Types.fst = Bool.False;
 443                                  Types.snd = castee2 })
 444                              | Bool.False ->
 445                                (fun _ -> { Types.fst = Bool.False;
 446                                  Types.snd = (Csyntax.Expr ((Csyntax.Ecast
 447                                  (ty, castee2)), cast_ty)) })) __)) __)) __))
 448                        __)) __)) __)
 449                | Bool.False ->
 450                  (fun _ ->
 451                    (let eta2014 = simplify_expr castee cast_sz cast_sg in
 452                      (fun _ ->
 453                      (let { Types.fst = desired_type2; Types.snd =
 454                         castee2 } = eta2014
 455                       in
 456                      (fun _ ->
 457                      (match desired_type2 with
 458                       | Bool.True ->
 459                         (fun _ -> { Types.fst = Bool.False; Types.snd =
 460                           castee2 })
 461                       | Bool.False ->
 462                         (fun _ -> { Types.fst = Bool.False; Types.snd =
 463                           (Csyntax.Expr ((Csyntax.Ecast (ty, castee2)),
 464                           cast_ty)) })) __)) __)) __)) __
 465             | Types.Inr _ ->
 466               (let castee1 = simplify_inside castee in
 467                 (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
 468                 ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
 469         | Csyntax.Tpointer x ->
 470           (fun _ ->
 471             (let castee1 = simplify_inside castee in
 472               (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
 473               ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
 474         | Csyntax.Tarray (x, x0) ->
 475           (fun _ ->
 476             (let castee1 = simplify_inside castee in
 477               (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
 478               ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
 479         | Csyntax.Tfunction (x, x0) ->
 480           (fun _ ->
 481             (let castee1 = simplify_inside castee in
 482               (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
 483               ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
 484         | Csyntax.Tstruct (x, x0) ->
 485           (fun _ ->
 486             (let castee1 = simplify_inside castee in
 487               (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
 488               ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
 489         | Csyntax.Tunion (x, x0) ->
 490           (fun _ ->
 491             (let castee1 = simplify_inside castee in
 492               (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
 493               ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
 494         | Csyntax.Tcomp_ptr x ->
 495           (fun _ ->
 496             (let castee1 = simplify_inside castee in
 497               (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
 498               ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)) __)
 499    | Csyntax.Econdition (cond, iftrue, iffalse) ->
 500      (fun _ ->
 501        (let cond1 = simplify_inside cond in
 502          (fun _ ->
 503          match TypeComparison.assert_type_eq ty (Csyntax.typeof iftrue) with
 504          | Errors.OK _ ->
 505            (match TypeComparison.assert_type_eq (Csyntax.typeof iftrue)
 506                     (Csyntax.typeof iffalse) with
 507             | Errors.OK _ ->
 508               (let eta2016 = simplify_expr iftrue target_sz target_sg in
 509                 (fun _ ->
 510                 (let { Types.fst = desired_true; Types.snd = iftrue1 } =
 511                    eta2016
 512                  in
 513                 (fun _ ->
 514                 (let eta2015 = simplify_expr iffalse target_sz target_sg in
 515                   (fun _ ->
 516                   (let { Types.fst = desired_false; Types.snd = iffalse1 } =
 517                      eta2015
 518                    in
 519                   (fun _ ->
 520                   (match Bool.andb desired_true desired_false with
 521                    | Bool.True ->
 522                      (fun _ -> { Types.fst = Bool.True; Types.snd =
 523                        (Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1,
 524                        iffalse1)), (Csyntax.Tint (target_sz, target_sg)))) })
 525                    | Bool.False ->
 526                      (fun _ ->
 527                        (let iftrue10 = simplify_inside iftrue in
 528                          (fun _ ->
 529                          (let iffalse10 = simplify_inside iffalse in
 530                            (fun _ -> { Types.fst = Bool.False; Types.snd =
 531                            (Csyntax.Expr ((Csyntax.Econdition (cond1,
 532                            iftrue10, iffalse10)), ty)) })) __)) __)) __)) __))
 533                   __)) __)) __
 534             | Errors.Error x ->
 535               (let iftrue1 = simplify_inside iftrue in
 536                 (fun _ ->
 537                 (let iffalse1 = simplify_inside iffalse in
 538                   (fun _ -> { Types.fst = Bool.False; Types.snd =
 539                   (Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1,
 540                   iffalse1)), ty)) })) __)) __)
 541          | Errors.Error x ->
 542            (let iftrue1 = simplify_inside iftrue in
 543              (fun _ ->
 544              (let iffalse1 = simplify_inside iffalse in
 545                (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
 546                ((Csyntax.Econdition (cond1, iftrue1, iffalse1)), ty)) })) __))
 547              __)) __)
 548    | Csyntax.Eandbool (lhs, rhs) ->
 549      (fun _ ->
 550        (let lhs1 = simplify_inside lhs in
 551          (fun _ ->
 552          (let rhs1 = simplify_inside rhs in
 553            (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
 554            ((Csyntax.Eandbool (lhs1, rhs1)), ty)) })) __)) __)
 555    | Csyntax.Eorbool (lhs, rhs) ->
 556      (fun _ ->
 557        (let lhs1 = simplify_inside lhs in
 558          (fun _ ->
 559          (let rhs1 = simplify_inside rhs in
 560            (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
 561            ((Csyntax.Eorbool (lhs1, rhs1)), ty)) })) __)) __)
 562    | Csyntax.Esizeof t ->
 563      (fun _ -> { Types.fst =
 564        (TypeComparison.type_eq ty (Csyntax.Tint (target_sz, target_sg)));
 565        Types.snd = (Csyntax.Expr (ed, ty)) })
 566    | Csyntax.Efield (rec_expr, f) ->
 567      (fun _ ->
 568        (let rec_expr1 = simplify_inside rec_expr in
 569          (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
 570          ((Csyntax.Efield (rec_expr1, f)), ty)) })) __)
 571    | Csyntax.Ecost (l, e1) ->
 572      (fun _ ->
 573        match TypeComparison.type_eq_dec ty (Csyntax.typeof e1) with
 574        | Types.Inl _ ->
 575          (let eta2017 = simplify_expr e1 target_sz target_sg in
 576            (fun _ ->
 577            (let { Types.fst = desired_type; Types.snd = e2 } = eta2017 in
 578            (fun _ -> { Types.fst = desired_type; Types.snd = (Csyntax.Expr
 579            ((Csyntax.Ecost (l, e2)), (Csyntax.typeof e2))) })) __)) __
 580        | Types.Inr _ ->
 581          (let e2 = simplify_inside e1 in
 582            (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
 583            ((Csyntax.Ecost (l, e2)), ty)) })) __)) __)) __
 584 (** val simplify_inside : Csyntax.expr -> Csyntax.expr Types.sig0 **)
 585 and simplify_inside e =
 586   (let Csyntax.Expr (ed, ty) = e in
 587   (fun _ ->
 588   (match ed with
 589    | Csyntax.Econst_int (x, x0) -> (fun _ -> e)
 590    | Csyntax.Evar x -> (fun _ -> e)
 591    | Csyntax.Ederef e1 ->
 592      (fun _ ->
 593        (let e2 = simplify_inside e1 in
 594          (fun _ -> Csyntax.Expr ((Csyntax.Ederef e2), ty))) __)
 595    | Csyntax.Eaddrof e1 ->
 596      (fun _ ->
 597        (let e2 = simplify_inside e1 in
 598          (fun _ -> Csyntax.Expr ((Csyntax.Eaddrof e2), ty))) __)
 599    | Csyntax.Eunop (op, e1) ->
 600      (fun _ ->
 601        (let e2 = simplify_inside e1 in
 602          (fun _ -> Csyntax.Expr ((Csyntax.Eunop (op, e2)), ty))) __)
 603    | Csyntax.Ebinop (op, lhs, rhs) ->
 604      (fun _ ->
 605        (let lhs1 = simplify_inside lhs in
 606          (fun _ ->
 607          (let rhs1 = simplify_inside rhs in
 608            (fun _ -> Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)))
 609            __)) __)
 610    | Csyntax.Ecast (cast_ty, castee) ->
 611      (fun _ ->
 612        match TypeComparison.type_eq_dec ty cast_ty with
 613        | Types.Inl _ ->
 614          (match cast_ty with
 615           | Csyntax.Tvoid -> (fun _ -> e)
 616           | Csyntax.Tint (cast_sz, cast_sg) ->
 617             (fun _ ->
 618               (let eta2018 = simplify_expr castee cast_sz cast_sg in
 619                 (fun _ ->
 620                 (let { Types.fst = success; Types.snd = castee1 } = eta2018
 621                  in
 622                 (fun _ ->
 623                 (match success with
 624                  | Bool.True -> (fun _ -> castee1)
 625                  | Bool.False ->
 626                    (fun _ -> Csyntax.Expr ((Csyntax.Ecast (cast_ty,
 627                      castee1)), ty))) __)) __)) __)
 628           | Csyntax.Tpointer x -> (fun _ -> e)
 629           | Csyntax.Tarray (x, x0) -> (fun _ -> e)
 630           | Csyntax.Tfunction (x, x0) -> (fun _ -> e)
 631           | Csyntax.Tstruct (x, x0) -> (fun _ -> e)
 632           | Csyntax.Tunion (x, x0) -> (fun _ -> e)
 633           | Csyntax.Tcomp_ptr x -> (fun _ -> e)) __
 634        | Types.Inr _ -> e)
 635    | Csyntax.Econdition (cond, iftrue, iffalse) ->
 636      (fun _ ->
 637        (let cond1 = simplify_inside cond in
 638          (fun _ ->
 639          (let iftrue1 = simplify_inside iftrue in
 640            (fun _ ->
 641            (let iffalse1 = simplify_inside iffalse in
 642              (fun _ -> Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1,
 643              iffalse1)), ty))) __)) __)) __)
 644    | Csyntax.Eandbool (lhs, rhs) ->
 645      (fun _ ->
 646        (let lhs1 = simplify_inside lhs in
 647          (fun _ ->
 648          (let rhs1 = simplify_inside rhs in
 649            (fun _ -> Csyntax.Expr ((Csyntax.Eandbool (lhs1, rhs1)), ty))) __))
 650          __)
 651    | Csyntax.Eorbool (lhs, rhs) ->
 652      (fun _ ->
 653        (let lhs1 = simplify_inside lhs in
 654          (fun _ ->
 655          (let rhs1 = simplify_inside rhs in
 656            (fun _ -> Csyntax.Expr ((Csyntax.Eorbool (lhs1, rhs1)), ty))) __))
 657          __)
 658    | Csyntax.Esizeof x -> (fun _ -> e)
 659    | Csyntax.Efield (rec_expr, f) ->
 660      (fun _ ->
 661        (let rec_expr1 = simplify_inside rec_expr in
 662          (fun _ -> Csyntax.Expr ((Csyntax.Efield (rec_expr1, f)), ty))) __)
 663    | Csyntax.Ecost (l, e1) ->
 664      (fun _ ->
 665        (let e2 = simplify_inside e1 in
 666          (fun _ -> Csyntax.Expr ((Csyntax.Ecost (l, e2)), ty))) __)) __)) __
 667
 668 (** val simplify_e : Csyntax.expr -> Csyntax.expr **)
 669 let simplify_e e =
 670   Types.pi1 (simplify_inside e)
 671
 672 (** val simplify_statement : Csyntax.statement -> Csyntax.statement **)
 673 let rec simplify_statement = function
 674 | Csyntax.Sskip -> Csyntax.Sskip
 675 | Csyntax.Sassign (e1, e2) ->
 676   Csyntax.Sassign ((simplify_e e1), (simplify_e e2))
 677 | Csyntax.Scall (eo, e, es) ->
 678   Csyntax.Scall ((Types.option_map simplify_e eo), (simplify_e e),
 679     (List.map simplify_e es))
 680 | Csyntax.Ssequence (s1, s2) ->
 681   Csyntax.Ssequence ((simplify_statement s1), (simplify_statement s2))
 682 | Csyntax.Sifthenelse (e, s1, s2) ->
 683   Csyntax.Sifthenelse ((simplify_e e), (simplify_statement s1),
 684     (simplify_statement s2))
 685 | Csyntax.Swhile (e, s1) ->
 686   Csyntax.Swhile ((simplify_e e), (simplify_statement s1))
 687 | Csyntax.Sdowhile (e, s1) ->
 688   Csyntax.Sdowhile ((simplify_e e), (simplify_statement s1))
 689 | Csyntax.Sfor (s1, e, s2, s3) ->
 690   Csyntax.Sfor ((simplify_statement s1), (simplify_e e),
 691     (simplify_statement s2), (simplify_statement s3))
 692 | Csyntax.Sbreak -> Csyntax.Sbreak
 693 | Csyntax.Scontinue -> Csyntax.Scontinue
 694 | Csyntax.Sreturn eo -> Csyntax.Sreturn (Types.option_map simplify_e eo)
 695 | Csyntax.Sswitch (e, ls) ->
 696   Csyntax.Sswitch ((simplify_e e), (simplify_ls ls))
 697 | Csyntax.Slabel (l, s1) -> Csyntax.Slabel (l, (simplify_statement s1))
 698 | Csyntax.Sgoto l -> Csyntax.Sgoto l
 699 | Csyntax.Scost (l, s1) -> Csyntax.Scost (l, (simplify_statement s1))
 700 (** val simplify_ls :
 701     Csyntax.labeled_statements -> Csyntax.labeled_statements **)
 702 and simplify_ls = function
 703 | Csyntax.LSdefault s -> Csyntax.LSdefault (simplify_statement s)
 704 | Csyntax.LScase (sz, i, s, ls') ->
 705   Csyntax.LScase (sz, i, (simplify_statement s), (simplify_ls ls'))
 706
 707 (** val simplify_function : Csyntax.function0 -> Csyntax.function0 **)
 708 let simplify_function f =
 709   { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params =
 710     f.Csyntax.fn_params; Csyntax.fn_vars = f.Csyntax.fn_vars;
 711     Csyntax.fn_body = (simplify_statement f.Csyntax.fn_body) }
 712
 713 (** val simplify_fundef : Csyntax.clight_fundef -> Csyntax.clight_fundef **)
 714 let simplify_fundef f = match f with
 715 | Csyntax.CL_Internal f0 -> Csyntax.CL_Internal (simplify_function f0)
 716 | Csyntax.CL_External (x, x0, x1) -> f
 717
 718 (** val simplify_program :
 719     Csyntax.clight_program -> Csyntax.clight_program **)
 720 let simplify_program p =
 721   AST.transform_program p (fun x -> simplify_fundef)
 722