extracted/label.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 (** val labels_of_expr : Csyntax.expr -> CostLabel.costlabel List.list **)
  78 let rec labels_of_expr = function
  79 | Csyntax.Expr (e', x) ->
  80   (match e' with
  81    | Csyntax.Econst_int (x0, x1) -> List.Nil
  82    | Csyntax.Evar x0 -> List.Nil
  83    | Csyntax.Ederef e1 -> labels_of_expr e1
  84    | Csyntax.Eaddrof e1 -> labels_of_expr e1
  85    | Csyntax.Eunop (x0, e1) -> labels_of_expr e1
  86    | Csyntax.Ebinop (x0, e1, e2) ->
  87      List.append (labels_of_expr e1) (labels_of_expr e2)
  88    | Csyntax.Ecast (x0, e1) -> labels_of_expr e1
  89    | Csyntax.Econdition (e1, e2, e3) ->
  90      List.append (labels_of_expr e1)
  91        (List.append (labels_of_expr e2) (labels_of_expr e3))
  92    | Csyntax.Eandbool (e1, e2) ->
  93      List.append (labels_of_expr e1) (labels_of_expr e2)
  94    | Csyntax.Eorbool (e1, e2) ->
  95      List.append (labels_of_expr e1) (labels_of_expr e2)
  96    | Csyntax.Esizeof x0 -> List.Nil
  97    | Csyntax.Efield (e1, x0) -> labels_of_expr e1
  98    | Csyntax.Ecost (cl, e1) -> List.Cons (cl, (labels_of_expr e1)))
  99
 100 (** val labels_of_statement :
 101     Csyntax.statement -> CostLabel.costlabel List.list **)
 102 let rec labels_of_statement = function
 103 | Csyntax.Sskip -> List.Nil
 104 | Csyntax.Sassign (e1, e2) ->
 105   List.append (labels_of_expr e1) (labels_of_expr e2)
 106 | Csyntax.Scall (oe, e1, es) ->
 107   List.append (Types.option_map_def labels_of_expr List.Nil oe)
 108     (List.append (labels_of_expr e1)
 109       (Util.foldl (fun ls e -> List.append (labels_of_expr e) ls) List.Nil
 110         es))
 111 | Csyntax.Ssequence (s1, s2) ->
 112   List.append (labels_of_statement s1) (labels_of_statement s2)
 113 | Csyntax.Sifthenelse (e1, s1, s2) ->
 114   List.append (labels_of_expr e1)
 115     (List.append (labels_of_statement s1) (labels_of_statement s2))
 116 | Csyntax.Swhile (e1, s1) ->
 117   List.append (labels_of_expr e1) (labels_of_statement s1)
 118 | Csyntax.Sdowhile (e1, s1) ->
 119   List.append (labels_of_expr e1) (labels_of_statement s1)
 120 | Csyntax.Sfor (s1, e1, s2, s3) ->
 121   List.append (labels_of_statement s1)
 122     (List.append (labels_of_expr e1)
 123       (List.append (labels_of_statement s2) (labels_of_statement s3)))
 124 | Csyntax.Sbreak -> List.Nil
 125 | Csyntax.Scontinue -> List.Nil
 126 | Csyntax.Sreturn oe -> Types.option_map_def labels_of_expr List.Nil oe
 127 | Csyntax.Sswitch (e1, ls) ->
 128   List.append (labels_of_expr e1) (labels_of_labeled_statements ls)
 129 | Csyntax.Slabel (x, s1) -> labels_of_statement s1
 130 | Csyntax.Sgoto x -> List.Nil
 131 | Csyntax.Scost (cl, s1) -> List.Cons (cl, (labels_of_statement s1))
 132 (** val labels_of_labeled_statements :
 133     Csyntax.labeled_statements -> CostLabel.costlabel List.list **)
 134 and labels_of_labeled_statements = function
 135 | Csyntax.LSdefault s1 -> labels_of_statement s1
 136 | Csyntax.LScase (x, x0, s1, ls1) ->
 137   List.append (labels_of_statement s1) (labels_of_labeled_statements ls1)
 138
 139 (** val labels_of_clight_fundef :
 140     (AST.ident, Csyntax.clight_fundef) Types.prod -> CostLabel.costlabel
 141     List.list **)
 142 let labels_of_clight_fundef ifd =
 143   match ifd.Types.snd with
 144   | Csyntax.CL_Internal f -> labels_of_statement f.Csyntax.fn_body
 145   | Csyntax.CL_External (x, x0, x1) -> List.Nil
 146
 147 (** val labels_of_clight :
 148     Csyntax.clight_program -> CostLabel.costlabel List.list **)
 149 let labels_of_clight p =
 150   Util.foldl (fun ls f -> List.append (labels_of_clight_fundef f) ls)
 151     List.Nil p.AST.prog_funct
 152
 153 type in_clight_label = CostLabel.costlabel Types.sig0
 154
 155 type clight_cost_map = CostLabel.costlabel -> Nat.nat
 156
 157 (** val clight_label_free : Csyntax.clight_program -> Bool.bool **)
 158 let clight_label_free p =
 159   match labels_of_clight p with
 160   | List.Nil -> Bool.True
 161   | List.Cons (x, x0) -> Bool.False
 162
 163 (** val add_cost_before :
 164     Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
 165     Identifiers.universe) Types.prod **)
 166 let add_cost_before s gen =
 167   let { Types.fst = l; Types.snd = gen0 } =
 168     Identifiers.fresh PreIdentifiers.CostTag gen
 169   in
 170   { Types.fst = (Csyntax.Scost (l, s)); Types.snd = gen0 }
 171
 172 (** val add_cost_after :
 173     Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
 174     Identifiers.universe) Types.prod **)
 175 let add_cost_after s gen =
 176   let { Types.fst = l; Types.snd = gen0 } =
 177     Identifiers.fresh PreIdentifiers.CostTag gen
 178   in
 179   { Types.fst = (Csyntax.Ssequence (s, (Csyntax.Scost (l, Csyntax.Sskip))));
 180   Types.snd = gen0 }
 181
 182 (** val add_cost_expr :
 183     Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
 184     Identifiers.universe) Types.prod **)
 185 let add_cost_expr e gen =
 186   let { Types.fst = l; Types.snd = gen0 } =
 187     Identifiers.fresh PreIdentifiers.CostTag gen
 188   in
 189   { Types.fst = (Csyntax.Expr ((Csyntax.Ecost (l, e)), (Csyntax.typeof e)));
 190   Types.snd = gen0 }
 191
 192 (** val const_int : AST.intsize -> Nat.nat -> Csyntax.expr **)
 193 let const_int sz n =
 194   Csyntax.Expr ((Csyntax.Econst_int (sz, (AST.repr sz n))), (Csyntax.Tint
 195     (sz, AST.Signed)))
 196
 197 (** val label_expr :
 198     Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
 199     Identifiers.universe) Types.prod **)
 200 let rec label_expr e costgen =
 201   let Csyntax.Expr (ed, ty) = e in
 202   let { Types.fst = ed0; Types.snd = costgen0 } =
 203     label_expr_descr ed costgen ty
 204   in
 205   { Types.fst = (Csyntax.Expr (ed0, ty)); Types.snd = costgen0 }
 206 (** val label_expr_descr :
 207     Csyntax.expr_descr -> Identifiers.universe -> Csyntax.type0 ->
 208     (Csyntax.expr_descr, Identifiers.universe) Types.prod **)
 209 and label_expr_descr e costgen ty =
 210   match e with
 211   | Csyntax.Econst_int (x, x0) -> { Types.fst = e; Types.snd = costgen }
 212   | Csyntax.Evar x -> { Types.fst = e; Types.snd = costgen }
 213   | Csyntax.Ederef e' ->
 214     let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
 215     { Types.fst = (Csyntax.Ederef e'0); Types.snd = costgen0 }
 216   | Csyntax.Eaddrof e' ->
 217     let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
 218     { Types.fst = (Csyntax.Eaddrof e'0); Types.snd = costgen0 }
 219   | Csyntax.Eunop (op, e') ->
 220     let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
 221     { Types.fst = (Csyntax.Eunop (op, e'0)); Types.snd = costgen0 }
 222   | Csyntax.Ebinop (op, e1, e2) ->
 223     let { Types.fst = e10; Types.snd = costgen0 } = label_expr e1 costgen in
 224     let { Types.fst = e20; Types.snd = costgen1 } = label_expr e2 costgen0 in
 225     { Types.fst = (Csyntax.Ebinop (op, e10, e20)); Types.snd = costgen1 }
 226   | Csyntax.Ecast (ty0, e') ->
 227     let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
 228     { Types.fst = (Csyntax.Ecast (ty0, e'0)); Types.snd = costgen0 }
 229   | Csyntax.Econdition (e', e1, e2) ->
 230     let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
 231     let { Types.fst = e10; Types.snd = costgen1 } = label_expr e1 costgen0 in
 232     let { Types.fst = e11; Types.snd = costgen2 } =
 233       add_cost_expr e10 costgen1
 234     in
 235     let { Types.fst = e20; Types.snd = costgen3 } = label_expr e2 costgen2 in
 236     let { Types.fst = e21; Types.snd = costgen4 } =
 237       add_cost_expr e20 costgen3
 238     in
 239     { Types.fst = (Csyntax.Econdition (e'0, e11, e21)); Types.snd =
 240     costgen4 }
 241   | Csyntax.Eandbool (e1, e2) ->
 242     let { Types.fst = e10; Types.snd = costgen0 } = label_expr e1 costgen in
 243     let { Types.fst = e20; Types.snd = costgen1 } = label_expr e2 costgen0 in
 244     (match ty with
 245      | Csyntax.Tvoid ->
 246        let { Types.fst = et; Types.snd = costgen2 } =
 247          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
 248        in
 249        let { Types.fst = ef; Types.snd = costgen3 } =
 250          add_cost_expr (const_int AST.I32 Nat.O) costgen2
 251        in
 252        let { Types.fst = e21; Types.snd = costgen4 } =
 253          add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
 254            ty)) costgen3
 255        in
 256        let { Types.fst = ef0; Types.snd = costgen5 } =
 257          add_cost_expr (const_int AST.I32 Nat.O) costgen4
 258        in
 259        { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
 260        costgen5 }
 261      | Csyntax.Tint (sz, sg) ->
 262        let { Types.fst = et; Types.snd = costgen2 } =
 263          add_cost_expr (const_int sz (Nat.S Nat.O)) costgen1
 264        in
 265        let { Types.fst = ef; Types.snd = costgen3 } =
 266          add_cost_expr (const_int sz Nat.O) costgen2
 267        in
 268        let { Types.fst = e21; Types.snd = costgen4 } =
 269          add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
 270            ty)) costgen3
 271        in
 272        let { Types.fst = ef0; Types.snd = costgen5 } =
 273          add_cost_expr (const_int sz Nat.O) costgen4
 274        in
 275        { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
 276        costgen5 }
 277      | Csyntax.Tpointer x ->
 278        let { Types.fst = et; Types.snd = costgen2 } =
 279          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
 280        in
 281        let { Types.fst = ef; Types.snd = costgen3 } =
 282          add_cost_expr (const_int AST.I32 Nat.O) costgen2
 283        in
 284        let { Types.fst = e21; Types.snd = costgen4 } =
 285          add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
 286            ty)) costgen3
 287        in
 288        let { Types.fst = ef0; Types.snd = costgen5 } =
 289          add_cost_expr (const_int AST.I32 Nat.O) costgen4
 290        in
 291        { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
 292        costgen5 }
 293      | Csyntax.Tarray (x, x0) ->
 294        let { Types.fst = et; Types.snd = costgen2 } =
 295          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
 296        in
 297        let { Types.fst = ef; Types.snd = costgen3 } =
 298          add_cost_expr (const_int AST.I32 Nat.O) costgen2
 299        in
 300        let { Types.fst = e21; Types.snd = costgen4 } =
 301          add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
 302            ty)) costgen3
 303        in
 304        let { Types.fst = ef0; Types.snd = costgen5 } =
 305          add_cost_expr (const_int AST.I32 Nat.O) costgen4
 306        in
 307        { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
 308        costgen5 }
 309      | Csyntax.Tfunction (x, x0) ->
 310        let { Types.fst = et; Types.snd = costgen2 } =
 311          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
 312        in
 313        let { Types.fst = ef; Types.snd = costgen3 } =
 314          add_cost_expr (const_int AST.I32 Nat.O) costgen2
 315        in
 316        let { Types.fst = e21; Types.snd = costgen4 } =
 317          add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
 318            ty)) costgen3
 319        in
 320        let { Types.fst = ef0; Types.snd = costgen5 } =
 321          add_cost_expr (const_int AST.I32 Nat.O) costgen4
 322        in
 323        { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
 324        costgen5 }
 325      | Csyntax.Tstruct (x, x0) ->
 326        let { Types.fst = et; Types.snd = costgen2 } =
 327          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
 328        in
 329        let { Types.fst = ef; Types.snd = costgen3 } =
 330          add_cost_expr (const_int AST.I32 Nat.O) costgen2
 331        in
 332        let { Types.fst = e21; Types.snd = costgen4 } =
 333          add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
 334            ty)) costgen3
 335        in
 336        let { Types.fst = ef0; Types.snd = costgen5 } =
 337          add_cost_expr (const_int AST.I32 Nat.O) costgen4
 338        in
 339        { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
 340        costgen5 }
 341      | Csyntax.Tunion (x, x0) ->
 342        let { Types.fst = et; Types.snd = costgen2 } =
 343          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
 344        in
 345        let { Types.fst = ef; Types.snd = costgen3 } =
 346          add_cost_expr (const_int AST.I32 Nat.O) costgen2
 347        in
 348        let { Types.fst = e21; Types.snd = costgen4 } =
 349          add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
 350            ty)) costgen3
 351        in
 352        let { Types.fst = ef0; Types.snd = costgen5 } =
 353          add_cost_expr (const_int AST.I32 Nat.O) costgen4
 354        in
 355        { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
 356        costgen5 }
 357      | Csyntax.Tcomp_ptr x ->
 358        let { Types.fst = et; Types.snd = costgen2 } =
 359          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
 360        in
 361        let { Types.fst = ef; Types.snd = costgen3 } =
 362          add_cost_expr (const_int AST.I32 Nat.O) costgen2
 363        in
 364        let { Types.fst = e21; Types.snd = costgen4 } =
 365          add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
 366            ty)) costgen3
 367        in
 368        let { Types.fst = ef0; Types.snd = costgen5 } =
 369          add_cost_expr (const_int AST.I32 Nat.O) costgen4
 370        in
 371        { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
 372        costgen5 })
 373   | Csyntax.Eorbool (e1, e2) ->
 374     let { Types.fst = e10; Types.snd = costgen0 } = label_expr e1 costgen in
 375     let { Types.fst = e20; Types.snd = costgen1 } = label_expr e2 costgen0 in
 376     (match ty with
 377      | Csyntax.Tvoid ->
 378        let { Types.fst = et; Types.snd = costgen2 } =
 379          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
 380        in
 381        let { Types.fst = ef; Types.snd = costgen3 } =
 382          add_cost_expr (const_int AST.I32 Nat.O) costgen2
 383        in
 384        let { Types.fst = e21; Types.snd = costgen4 } =
 385          add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
 386            ty)) costgen3
 387        in
 388        let { Types.fst = et0; Types.snd = costgen5 } =
 389          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
 390        in
 391        { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
 392        costgen5 }
 393      | Csyntax.Tint (sz, sg) ->
 394        let { Types.fst = et; Types.snd = costgen2 } =
 395          add_cost_expr (const_int sz (Nat.S Nat.O)) costgen1
 396        in
 397        let { Types.fst = ef; Types.snd = costgen3 } =
 398          add_cost_expr (const_int sz Nat.O) costgen2
 399        in
 400        let { Types.fst = e21; Types.snd = costgen4 } =
 401          add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
 402            ty)) costgen3
 403        in
 404        let { Types.fst = et0; Types.snd = costgen5 } =
 405          add_cost_expr (const_int sz (Nat.S Nat.O)) costgen4
 406        in
 407        { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
 408        costgen5 }
 409      | Csyntax.Tpointer x ->
 410        let { Types.fst = et; Types.snd = costgen2 } =
 411          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
 412        in
 413        let { Types.fst = ef; Types.snd = costgen3 } =
 414          add_cost_expr (const_int AST.I32 Nat.O) costgen2
 415        in
 416        let { Types.fst = e21; Types.snd = costgen4 } =
 417          add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
 418            ty)) costgen3
 419        in
 420        let { Types.fst = et0; Types.snd = costgen5 } =
 421          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
 422        in
 423        { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
 424        costgen5 }
 425      | Csyntax.Tarray (x, x0) ->
 426        let { Types.fst = et; Types.snd = costgen2 } =
 427          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
 428        in
 429        let { Types.fst = ef; Types.snd = costgen3 } =
 430          add_cost_expr (const_int AST.I32 Nat.O) costgen2
 431        in
 432        let { Types.fst = e21; Types.snd = costgen4 } =
 433          add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
 434            ty)) costgen3
 435        in
 436        let { Types.fst = et0; Types.snd = costgen5 } =
 437          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
 438        in
 439        { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
 440        costgen5 }
 441      | Csyntax.Tfunction (x, x0) ->
 442        let { Types.fst = et; Types.snd = costgen2 } =
 443          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
 444        in
 445        let { Types.fst = ef; Types.snd = costgen3 } =
 446          add_cost_expr (const_int AST.I32 Nat.O) costgen2
 447        in
 448        let { Types.fst = e21; Types.snd = costgen4 } =
 449          add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
 450            ty)) costgen3
 451        in
 452        let { Types.fst = et0; Types.snd = costgen5 } =
 453          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
 454        in
 455        { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
 456        costgen5 }
 457      | Csyntax.Tstruct (x, x0) ->
 458        let { Types.fst = et; Types.snd = costgen2 } =
 459          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
 460        in
 461        let { Types.fst = ef; Types.snd = costgen3 } =
 462          add_cost_expr (const_int AST.I32 Nat.O) costgen2
 463        in
 464        let { Types.fst = e21; Types.snd = costgen4 } =
 465          add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
 466            ty)) costgen3
 467        in
 468        let { Types.fst = et0; Types.snd = costgen5 } =
 469          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
 470        in
 471        { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
 472        costgen5 }
 473      | Csyntax.Tunion (x, x0) ->
 474        let { Types.fst = et; Types.snd = costgen2 } =
 475          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
 476        in
 477        let { Types.fst = ef; Types.snd = costgen3 } =
 478          add_cost_expr (const_int AST.I32 Nat.O) costgen2
 479        in
 480        let { Types.fst = e21; Types.snd = costgen4 } =
 481          add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
 482            ty)) costgen3
 483        in
 484        let { Types.fst = et0; Types.snd = costgen5 } =
 485          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
 486        in
 487        { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
 488        costgen5 }
 489      | Csyntax.Tcomp_ptr x ->
 490        let { Types.fst = et; Types.snd = costgen2 } =
 491          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
 492        in
 493        let { Types.fst = ef; Types.snd = costgen3 } =
 494          add_cost_expr (const_int AST.I32 Nat.O) costgen2
 495        in
 496        let { Types.fst = e21; Types.snd = costgen4 } =
 497          add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
 498            ty)) costgen3
 499        in
 500        let { Types.fst = et0; Types.snd = costgen5 } =
 501          add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
 502        in
 503        { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
 504        costgen5 })
 505   | Csyntax.Esizeof x -> { Types.fst = e; Types.snd = costgen }
 506   | Csyntax.Efield (e', id) ->
 507     let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
 508     { Types.fst = (Csyntax.Efield (e'0, id)); Types.snd = costgen0 }
 509   | Csyntax.Ecost (l, e') ->
 510     let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
 511     { Types.fst = (Csyntax.Ecost (l, e'0)); Types.snd = costgen0 }
 512
 513 (** val label_exprs :
 514     Csyntax.expr List.list -> Identifiers.universe -> (Csyntax.expr
 515     List.list, Identifiers.universe) Types.prod **)
 516 let rec label_exprs l costgen =
 517   match l with
 518   | List.Nil -> { Types.fst = List.Nil; Types.snd = costgen }
 519   | List.Cons (e, es) ->
 520     let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
 521     let { Types.fst = es0; Types.snd = costgen1 } = label_exprs es costgen0
 522     in
 523     { Types.fst = (List.Cons (e0, es0)); Types.snd = costgen1 }
 524
 525 (** val label_opt_expr :
 526     Csyntax.expr Types.option -> Identifiers.universe -> (Csyntax.expr
 527     Types.option, Identifiers.universe) Types.prod **)
 528 let label_opt_expr oe costgen =
 529   match oe with
 530   | Types.None -> { Types.fst = Types.None; Types.snd = costgen }
 531   | Types.Some e ->
 532     let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
 533     { Types.fst = (Types.Some e0); Types.snd = costgen0 }
 534
 535 (** val label_statement :
 536     Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
 537     Identifiers.universe) Types.prod **)
 538 let rec label_statement s costgen =
 539   match s with
 540   | Csyntax.Sskip -> { Types.fst = Csyntax.Sskip; Types.snd = costgen }
 541   | Csyntax.Sassign (e1, e2) ->
 542     let { Types.fst = e10; Types.snd = costgen0 } = label_expr e1 costgen in
 543     let { Types.fst = e20; Types.snd = costgen1 } = label_expr e2 costgen0 in
 544     { Types.fst = (Csyntax.Sassign (e10, e20)); Types.snd = costgen1 }
 545   | Csyntax.Scall (e_ret, e_fn, e_args) ->
 546     let { Types.fst = e_ret0; Types.snd = costgen0 } =
 547       label_opt_expr e_ret costgen
 548     in
 549     let { Types.fst = e_fn0; Types.snd = costgen1 } =
 550       label_expr e_fn costgen0
 551     in
 552     let { Types.fst = e_args0; Types.snd = costgen2 } =
 553       label_exprs e_args costgen1
 554     in
 555     { Types.fst = (Csyntax.Scall (e_ret0, e_fn0, e_args0)); Types.snd =
 556     costgen2 }
 557   | Csyntax.Ssequence (s1, s2) ->
 558     let { Types.fst = s10; Types.snd = costgen0 } =
 559       label_statement s1 costgen
 560     in
 561     let { Types.fst = s20; Types.snd = costgen1 } =
 562       label_statement s2 costgen0
 563     in
 564     { Types.fst = (Csyntax.Ssequence (s10, s20)); Types.snd = costgen1 }
 565   | Csyntax.Sifthenelse (e, s1, s2) ->
 566     let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
 567     let { Types.fst = s10; Types.snd = costgen1 } =
 568       label_statement s1 costgen0
 569     in
 570     let { Types.fst = s11; Types.snd = costgen2 } =
 571       add_cost_before s10 costgen1
 572     in
 573     let { Types.fst = s20; Types.snd = costgen3 } =
 574       label_statement s2 costgen2
 575     in
 576     let { Types.fst = s21; Types.snd = costgen4 } =
 577       add_cost_before s20 costgen3
 578     in
 579     { Types.fst = (Csyntax.Sifthenelse (e0, s11, s21)); Types.snd =
 580     costgen4 }
 581   | Csyntax.Swhile (e, s') ->
 582     let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
 583     let { Types.fst = s'0; Types.snd = costgen1 } =
 584       label_statement s' costgen0
 585     in
 586     let { Types.fst = s'1; Types.snd = costgen2 } =
 587       add_cost_before s'0 costgen1
 588     in
 589     let { Types.fst = s0; Types.snd = costgen3 } =
 590       add_cost_after (Csyntax.Swhile (e0, s'1)) costgen2
 591     in
 592     { Types.fst = s0; Types.snd = costgen3 }
 593   | Csyntax.Sdowhile (e, s') ->
 594     let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
 595     let { Types.fst = s'0; Types.snd = costgen1 } =
 596       label_statement s' costgen0
 597     in
 598     let { Types.fst = s'1; Types.snd = costgen2 } =
 599       add_cost_before s'0 costgen1
 600     in
 601     let { Types.fst = s0; Types.snd = costgen3 } =
 602       add_cost_after (Csyntax.Sdowhile (e0, s'1)) costgen2
 603     in
 604     { Types.fst = s0; Types.snd = costgen3 }
 605   | Csyntax.Sfor (s1, e, s2, s3) ->
 606     let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
 607     let { Types.fst = s10; Types.snd = costgen1 } =
 608       label_statement s1 costgen0
 609     in
 610     let { Types.fst = s20; Types.snd = costgen2 } =
 611       label_statement s2 costgen1
 612     in
 613     let { Types.fst = s30; Types.snd = costgen3 } =
 614       label_statement s3 costgen2
 615     in
 616     let { Types.fst = s31; Types.snd = costgen4 } =
 617       add_cost_before s30 costgen3
 618     in
 619     let { Types.fst = s0; Types.snd = costgen5 } =
 620       add_cost_after (Csyntax.Sfor (s10, e0, s20, s31)) costgen4
 621     in
 622     { Types.fst = s0; Types.snd = costgen5 }
 623   | Csyntax.Sbreak -> { Types.fst = Csyntax.Sbreak; Types.snd = costgen }
 624   | Csyntax.Scontinue ->
 625     { Types.fst = Csyntax.Scontinue; Types.snd = costgen }
 626   | Csyntax.Sreturn opt_e ->
 627     let { Types.fst = opt_e0; Types.snd = costgen0 } =
 628       label_opt_expr opt_e costgen
 629     in
 630     { Types.fst = (Csyntax.Sreturn opt_e0); Types.snd = costgen0 }
 631   | Csyntax.Sswitch (e, ls) ->
 632     let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
 633     let { Types.fst = ls0; Types.snd = costgen1 } =
 634       label_lstatements ls costgen0
 635     in
 636     { Types.fst = (Csyntax.Sswitch (e0, ls0)); Types.snd = costgen1 }
 637   | Csyntax.Slabel (l, s') ->
 638     let { Types.fst = s'0; Types.snd = costgen0 } =
 639       label_statement s' costgen
 640     in
 641     let { Types.fst = s'1; Types.snd = costgen1 } =
 642       add_cost_before s'0 costgen0
 643     in
 644     { Types.fst = (Csyntax.Slabel (l, s'1)); Types.snd = costgen1 }
 645   | Csyntax.Sgoto l -> { Types.fst = (Csyntax.Sgoto l); Types.snd = costgen }
 646   | Csyntax.Scost (l, s') ->
 647     let { Types.fst = s'0; Types.snd = costgen0 } =
 648       label_statement s' costgen
 649     in
 650     { Types.fst = (Csyntax.Scost (l, s'0)); Types.snd = costgen0 }
 651 (** val label_lstatements :
 652     Csyntax.labeled_statements -> Identifiers.universe ->
 653     (Csyntax.labeled_statements, Identifiers.universe) Types.prod **)
 654 and label_lstatements ls costgen =
 655   match ls with
 656   | Csyntax.LSdefault s ->
 657     let { Types.fst = s0; Types.snd = costgen0 } = label_statement s costgen
 658     in
 659     let { Types.fst = s1; Types.snd = costgen1 } =
 660       add_cost_before s0 costgen0
 661     in
 662     { Types.fst = (Csyntax.LSdefault s1); Types.snd = costgen1 }
 663   | Csyntax.LScase (sz, i, s, ls') ->
 664     let { Types.fst = s0; Types.snd = costgen0 } = label_statement s costgen
 665     in
 666     let { Types.fst = s1; Types.snd = costgen1 } =
 667       add_cost_before s0 costgen0
 668     in
 669     let { Types.fst = ls'0; Types.snd = costgen2 } =
 670       label_lstatements ls' costgen1
 671     in
 672     { Types.fst = (Csyntax.LScase (sz, i, s1, ls'0)); Types.snd = costgen2 }
 673
 674 (** val label_function :
 675     Identifiers.universe -> Csyntax.function0 -> (Csyntax.function0,
 676     Identifiers.universe) Types.prod **)
 677 let label_function costgen f =
 678   let { Types.fst = body; Types.snd = costgen0 } =
 679     label_statement f.Csyntax.fn_body costgen
 680   in
 681   let { Types.fst = body0; Types.snd = costgen1 } =
 682     add_cost_before body costgen0
 683   in
 684   { Types.fst = { Csyntax.fn_return = f.Csyntax.fn_return;
 685   Csyntax.fn_params = f.Csyntax.fn_params; Csyntax.fn_vars =
 686   f.Csyntax.fn_vars; Csyntax.fn_body = body0 }; Types.snd = costgen1 }
 687
 688 (** val label_fundef :
 689     Identifiers.universe -> Csyntax.clight_fundef -> (Csyntax.clight_fundef,
 690     Identifiers.universe) Types.prod **)
 691 let label_fundef gen = function
 692 | Csyntax.CL_Internal f0 ->
 693   let { Types.fst = f'; Types.snd = gen' } = label_function gen f0 in
 694   { Types.fst = (Csyntax.CL_Internal f'); Types.snd = gen' }
 695 | Csyntax.CL_External (id, args, ty) ->
 696   { Types.fst = (Csyntax.CL_External (id, args, ty)); Types.snd = gen }
 697
 698 (** val clight_label :
 699     Csyntax.clight_program -> (Csyntax.clight_program, CostLabel.costlabel)
 700     Types.prod **)
 701 let rec clight_label p =
 702   let costgen = Identifiers.new_universe PreIdentifiers.CostTag in
 703   let { Types.fst = init_cost; Types.snd = costgen0 } =
 704     Identifiers.fresh PreIdentifiers.CostTag costgen
 705   in
 706   { Types.fst =
 707   (AST.transform_program_gen PreIdentifiers.CostTag costgen0 p (fun x ->
 708     label_fundef)).Types.fst; Types.snd = init_cost }
 709