open Preamble

open CostLabel

open Coqlib

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Positive

open Identifiers

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Jmeq

open Russell

open List

open Setoids

open Monad

open Option

open Extranat

open Bool

open Relations

open Nat

open Integers

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open AST

open Csyntax

(** val labels_of_expr : Csyntax.expr -> CostLabel.costlabel List.list **)
let rec labels_of_expr = function
| Csyntax.Expr (e', x) ->
  (match e' with
   | Csyntax.Econst_int (x0, x1) -> List.Nil
   | Csyntax.Evar x0 -> List.Nil
   | Csyntax.Ederef e1 -> labels_of_expr e1
   | Csyntax.Eaddrof e1 -> labels_of_expr e1
   | Csyntax.Eunop (x0, e1) -> labels_of_expr e1
   | Csyntax.Ebinop (x0, e1, e2) ->
     List.append (labels_of_expr e1) (labels_of_expr e2)
   | Csyntax.Ecast (x0, e1) -> labels_of_expr e1
   | Csyntax.Econdition (e1, e2, e3) ->
     List.append (labels_of_expr e1)
       (List.append (labels_of_expr e2) (labels_of_expr e3))
   | Csyntax.Eandbool (e1, e2) ->
     List.append (labels_of_expr e1) (labels_of_expr e2)
   | Csyntax.Eorbool (e1, e2) ->
     List.append (labels_of_expr e1) (labels_of_expr e2)
   | Csyntax.Esizeof x0 -> List.Nil
   | Csyntax.Efield (e1, x0) -> labels_of_expr e1
   | Csyntax.Ecost (cl, e1) -> List.Cons (cl, (labels_of_expr e1)))

(** val labels_of_statement :
    Csyntax.statement -> CostLabel.costlabel List.list **)
let rec labels_of_statement = function
| Csyntax.Sskip -> List.Nil
| Csyntax.Sassign (e1, e2) ->
  List.append (labels_of_expr e1) (labels_of_expr e2)
| Csyntax.Scall (oe, e1, es) ->
  List.append (Types.option_map_def labels_of_expr List.Nil oe)
    (List.append (labels_of_expr e1)
      (Util.foldl (fun ls e -> List.append (labels_of_expr e) ls) List.Nil
        es))
| Csyntax.Ssequence (s1, s2) ->
  List.append (labels_of_statement s1) (labels_of_statement s2)
| Csyntax.Sifthenelse (e1, s1, s2) ->
  List.append (labels_of_expr e1)
    (List.append (labels_of_statement s1) (labels_of_statement s2))
| Csyntax.Swhile (e1, s1) ->
  List.append (labels_of_expr e1) (labels_of_statement s1)
| Csyntax.Sdowhile (e1, s1) ->
  List.append (labels_of_expr e1) (labels_of_statement s1)
| Csyntax.Sfor (s1, e1, s2, s3) ->
  List.append (labels_of_statement s1)
    (List.append (labels_of_expr e1)
      (List.append (labels_of_statement s2) (labels_of_statement s3)))
| Csyntax.Sbreak -> List.Nil
| Csyntax.Scontinue -> List.Nil
| Csyntax.Sreturn oe -> Types.option_map_def labels_of_expr List.Nil oe
| Csyntax.Sswitch (e1, ls) ->
  List.append (labels_of_expr e1) (labels_of_labeled_statements ls)
| Csyntax.Slabel (x, s1) -> labels_of_statement s1
| Csyntax.Sgoto x -> List.Nil
| Csyntax.Scost (cl, s1) -> List.Cons (cl, (labels_of_statement s1))
(** val labels_of_labeled_statements :
    Csyntax.labeled_statements -> CostLabel.costlabel List.list **)
and labels_of_labeled_statements = function
| Csyntax.LSdefault s1 -> labels_of_statement s1
| Csyntax.LScase (x, x0, s1, ls1) ->
  List.append (labels_of_statement s1) (labels_of_labeled_statements ls1)

(** val labels_of_clight_fundef :
    (AST.ident, Csyntax.clight_fundef) Types.prod -> CostLabel.costlabel
    List.list **)
let labels_of_clight_fundef ifd =
  match ifd.Types.snd with
  | Csyntax.CL_Internal f -> labels_of_statement f.Csyntax.fn_body
  | Csyntax.CL_External (x, x0, x1) -> List.Nil

(** val labels_of_clight :
    Csyntax.clight_program -> CostLabel.costlabel List.list **)
let labels_of_clight p =
  Util.foldl (fun ls f -> List.append (labels_of_clight_fundef f) ls)
    List.Nil p.AST.prog_funct

type in_clight_label = CostLabel.costlabel Types.sig0

type clight_cost_map = CostLabel.costlabel -> Nat.nat

(** val clight_label_free : Csyntax.clight_program -> Bool.bool **)
let clight_label_free p =
  match labels_of_clight p with
  | List.Nil -> Bool.True
  | List.Cons (x, x0) -> Bool.False

(** val add_cost_before :
    Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
    Identifiers.universe) Types.prod **)
let add_cost_before s gen =
  let { Types.fst = l; Types.snd = gen0 } =
    Identifiers.fresh PreIdentifiers.CostTag gen
  in
  { Types.fst = (Csyntax.Scost (l, s)); Types.snd = gen0 }

(** val add_cost_after :
    Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
    Identifiers.universe) Types.prod **)
let add_cost_after s gen =
  let { Types.fst = l; Types.snd = gen0 } =
    Identifiers.fresh PreIdentifiers.CostTag gen
  in
  { Types.fst = (Csyntax.Ssequence (s, (Csyntax.Scost (l, Csyntax.Sskip))));
  Types.snd = gen0 }

(** val add_cost_expr :
    Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
    Identifiers.universe) Types.prod **)
let add_cost_expr e gen =
  let { Types.fst = l; Types.snd = gen0 } =
    Identifiers.fresh PreIdentifiers.CostTag gen
  in
  { Types.fst = (Csyntax.Expr ((Csyntax.Ecost (l, e)), (Csyntax.typeof e)));
  Types.snd = gen0 }

(** val const_int : AST.intsize -> Nat.nat -> Csyntax.expr **)
let const_int sz n =
  Csyntax.Expr ((Csyntax.Econst_int (sz, (AST.repr sz n))), (Csyntax.Tint
    (sz, AST.Signed)))

(** val label_expr :
    Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
    Identifiers.universe) Types.prod **)
let rec label_expr e costgen =
  let Csyntax.Expr (ed, ty) = e in
  let { Types.fst = ed0; Types.snd = costgen0 } =
    label_expr_descr ed costgen ty
  in
  { Types.fst = (Csyntax.Expr (ed0, ty)); Types.snd = costgen0 }
(** val label_expr_descr :
    Csyntax.expr_descr -> Identifiers.universe -> Csyntax.type0 ->
    (Csyntax.expr_descr, Identifiers.universe) Types.prod **)
and label_expr_descr e costgen ty =
  match e with
  | Csyntax.Econst_int (x, x0) -> { Types.fst = e; Types.snd = costgen }
  | Csyntax.Evar x -> { Types.fst = e; Types.snd = costgen }
  | Csyntax.Ederef e' ->
    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
    { Types.fst = (Csyntax.Ederef e'0); Types.snd = costgen0 }
  | Csyntax.Eaddrof e' ->
    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
    { Types.fst = (Csyntax.Eaddrof e'0); Types.snd = costgen0 }
  | Csyntax.Eunop (op, e') ->
    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
    { Types.fst = (Csyntax.Eunop (op, e'0)); Types.snd = costgen0 }
  | Csyntax.Ebinop (op, e1, e2) ->
    let { Types.fst = e10; Types.snd = costgen0 } = label_expr e1 costgen in
    let { Types.fst = e20; Types.snd = costgen1 } = label_expr e2 costgen0 in
    { Types.fst = (Csyntax.Ebinop (op, e10, e20)); Types.snd = costgen1 }
  | Csyntax.Ecast (ty0, e') ->
    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
    { Types.fst = (Csyntax.Ecast (ty0, e'0)); Types.snd = costgen0 }
  | Csyntax.Econdition (e', e1, e2) ->
    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
    let { Types.fst = e10; Types.snd = costgen1 } = label_expr e1 costgen0 in
    let { Types.fst = e11; Types.snd = costgen2 } =
      add_cost_expr e10 costgen1
    in
    let { Types.fst = e20; Types.snd = costgen3 } = label_expr e2 costgen2 in
    let { Types.fst = e21; Types.snd = costgen4 } =
      add_cost_expr e20 costgen3
    in
    { Types.fst = (Csyntax.Econdition (e'0, e11, e21)); Types.snd =
    costgen4 }
  | Csyntax.Eandbool (e1, e2) ->
    let { Types.fst = e10; Types.snd = costgen0 } = label_expr e1 costgen in
    let { Types.fst = e20; Types.snd = costgen1 } = label_expr e2 costgen0 in
    (match ty with
     | Csyntax.Tvoid ->
       let { Types.fst = et; Types.snd = costgen2 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
       in
       let { Types.fst = ef; Types.snd = costgen3 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen2
       in
       let { Types.fst = e21; Types.snd = costgen4 } =
         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
           ty)) costgen3
       in
       let { Types.fst = ef0; Types.snd = costgen5 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen4
       in
       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
       costgen5 }
     | Csyntax.Tint (sz, sg) ->
       let { Types.fst = et; Types.snd = costgen2 } =
         add_cost_expr (const_int sz (Nat.S Nat.O)) costgen1
       in
       let { Types.fst = ef; Types.snd = costgen3 } =
         add_cost_expr (const_int sz Nat.O) costgen2
       in
       let { Types.fst = e21; Types.snd = costgen4 } =
         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
           ty)) costgen3
       in
       let { Types.fst = ef0; Types.snd = costgen5 } =
         add_cost_expr (const_int sz Nat.O) costgen4
       in
       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
       costgen5 }
     | Csyntax.Tpointer x ->
       let { Types.fst = et; Types.snd = costgen2 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
       in
       let { Types.fst = ef; Types.snd = costgen3 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen2
       in
       let { Types.fst = e21; Types.snd = costgen4 } =
         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
           ty)) costgen3
       in
       let { Types.fst = ef0; Types.snd = costgen5 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen4
       in
       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
       costgen5 }
     | Csyntax.Tarray (x, x0) ->
       let { Types.fst = et; Types.snd = costgen2 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
       in
       let { Types.fst = ef; Types.snd = costgen3 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen2
       in
       let { Types.fst = e21; Types.snd = costgen4 } =
         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
           ty)) costgen3
       in
       let { Types.fst = ef0; Types.snd = costgen5 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen4
       in
       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
       costgen5 }
     | Csyntax.Tfunction (x, x0) ->
       let { Types.fst = et; Types.snd = costgen2 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
       in
       let { Types.fst = ef; Types.snd = costgen3 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen2
       in
       let { Types.fst = e21; Types.snd = costgen4 } =
         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
           ty)) costgen3
       in
       let { Types.fst = ef0; Types.snd = costgen5 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen4
       in
       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
       costgen5 }
     | Csyntax.Tstruct (x, x0) ->
       let { Types.fst = et; Types.snd = costgen2 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
       in
       let { Types.fst = ef; Types.snd = costgen3 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen2
       in
       let { Types.fst = e21; Types.snd = costgen4 } =
         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
           ty)) costgen3
       in
       let { Types.fst = ef0; Types.snd = costgen5 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen4
       in
       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
       costgen5 }
     | Csyntax.Tunion (x, x0) ->
       let { Types.fst = et; Types.snd = costgen2 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
       in
       let { Types.fst = ef; Types.snd = costgen3 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen2
       in
       let { Types.fst = e21; Types.snd = costgen4 } =
         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
           ty)) costgen3
       in
       let { Types.fst = ef0; Types.snd = costgen5 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen4
       in
       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
       costgen5 }
     | Csyntax.Tcomp_ptr x ->
       let { Types.fst = et; Types.snd = costgen2 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
       in
       let { Types.fst = ef; Types.snd = costgen3 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen2
       in
       let { Types.fst = e21; Types.snd = costgen4 } =
         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
           ty)) costgen3
       in
       let { Types.fst = ef0; Types.snd = costgen5 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen4
       in
       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
       costgen5 })
  | Csyntax.Eorbool (e1, e2) ->
    let { Types.fst = e10; Types.snd = costgen0 } = label_expr e1 costgen in
    let { Types.fst = e20; Types.snd = costgen1 } = label_expr e2 costgen0 in
    (match ty with
     | Csyntax.Tvoid ->
       let { Types.fst = et; Types.snd = costgen2 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
       in
       let { Types.fst = ef; Types.snd = costgen3 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen2
       in
       let { Types.fst = e21; Types.snd = costgen4 } =
         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
           ty)) costgen3
       in
       let { Types.fst = et0; Types.snd = costgen5 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
       in
       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
       costgen5 }
     | Csyntax.Tint (sz, sg) ->
       let { Types.fst = et; Types.snd = costgen2 } =
         add_cost_expr (const_int sz (Nat.S Nat.O)) costgen1
       in
       let { Types.fst = ef; Types.snd = costgen3 } =
         add_cost_expr (const_int sz Nat.O) costgen2
       in
       let { Types.fst = e21; Types.snd = costgen4 } =
         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
           ty)) costgen3
       in
       let { Types.fst = et0; Types.snd = costgen5 } =
         add_cost_expr (const_int sz (Nat.S Nat.O)) costgen4
       in
       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
       costgen5 }
     | Csyntax.Tpointer x ->
       let { Types.fst = et; Types.snd = costgen2 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
       in
       let { Types.fst = ef; Types.snd = costgen3 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen2
       in
       let { Types.fst = e21; Types.snd = costgen4 } =
         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
           ty)) costgen3
       in
       let { Types.fst = et0; Types.snd = costgen5 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
       in
       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
       costgen5 }
     | Csyntax.Tarray (x, x0) ->
       let { Types.fst = et; Types.snd = costgen2 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
       in
       let { Types.fst = ef; Types.snd = costgen3 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen2
       in
       let { Types.fst = e21; Types.snd = costgen4 } =
         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
           ty)) costgen3
       in
       let { Types.fst = et0; Types.snd = costgen5 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
       in
       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
       costgen5 }
     | Csyntax.Tfunction (x, x0) ->
       let { Types.fst = et; Types.snd = costgen2 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
       in
       let { Types.fst = ef; Types.snd = costgen3 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen2
       in
       let { Types.fst = e21; Types.snd = costgen4 } =
         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
           ty)) costgen3
       in
       let { Types.fst = et0; Types.snd = costgen5 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
       in
       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
       costgen5 }
     | Csyntax.Tstruct (x, x0) ->
       let { Types.fst = et; Types.snd = costgen2 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
       in
       let { Types.fst = ef; Types.snd = costgen3 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen2
       in
       let { Types.fst = e21; Types.snd = costgen4 } =
         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
           ty)) costgen3
       in
       let { Types.fst = et0; Types.snd = costgen5 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
       in
       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
       costgen5 }
     | Csyntax.Tunion (x, x0) ->
       let { Types.fst = et; Types.snd = costgen2 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
       in
       let { Types.fst = ef; Types.snd = costgen3 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen2
       in
       let { Types.fst = e21; Types.snd = costgen4 } =
         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
           ty)) costgen3
       in
       let { Types.fst = et0; Types.snd = costgen5 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
       in
       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
       costgen5 }
     | Csyntax.Tcomp_ptr x ->
       let { Types.fst = et; Types.snd = costgen2 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
       in
       let { Types.fst = ef; Types.snd = costgen3 } =
         add_cost_expr (const_int AST.I32 Nat.O) costgen2
       in
       let { Types.fst = e21; Types.snd = costgen4 } =
         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
           ty)) costgen3
       in
       let { Types.fst = et0; Types.snd = costgen5 } =
         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
       in
       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
       costgen5 })
  | Csyntax.Esizeof x -> { Types.fst = e; Types.snd = costgen }
  | Csyntax.Efield (e', id) ->
    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
    { Types.fst = (Csyntax.Efield (e'0, id)); Types.snd = costgen0 }
  | Csyntax.Ecost (l, e') ->
    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
    { Types.fst = (Csyntax.Ecost (l, e'0)); Types.snd = costgen0 }

(** val label_exprs :
    Csyntax.expr List.list -> Identifiers.universe -> (Csyntax.expr
    List.list, Identifiers.universe) Types.prod **)
let rec label_exprs l costgen =
  match l with
  | List.Nil -> { Types.fst = List.Nil; Types.snd = costgen }
  | List.Cons (e, es) ->
    let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
    let { Types.fst = es0; Types.snd = costgen1 } = label_exprs es costgen0
    in
    { Types.fst = (List.Cons (e0, es0)); Types.snd = costgen1 }

(** val label_opt_expr :
    Csyntax.expr Types.option -> Identifiers.universe -> (Csyntax.expr
    Types.option, Identifiers.universe) Types.prod **)
let label_opt_expr oe costgen =
  match oe with
  | Types.None -> { Types.fst = Types.None; Types.snd = costgen }
  | Types.Some e ->
    let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
    { Types.fst = (Types.Some e0); Types.snd = costgen0 }

(** val label_statement :
    Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
    Identifiers.universe) Types.prod **)
let rec label_statement s costgen =
  match s with
  | Csyntax.Sskip -> { Types.fst = Csyntax.Sskip; Types.snd = costgen }
  | Csyntax.Sassign (e1, e2) ->
    let { Types.fst = e10; Types.snd = costgen0 } = label_expr e1 costgen in
    let { Types.fst = e20; Types.snd = costgen1 } = label_expr e2 costgen0 in
    { Types.fst = (Csyntax.Sassign (e10, e20)); Types.snd = costgen1 }
  | Csyntax.Scall (e_ret, e_fn, e_args) ->
    let { Types.fst = e_ret0; Types.snd = costgen0 } =
      label_opt_expr e_ret costgen
    in
    let { Types.fst = e_fn0; Types.snd = costgen1 } =
      label_expr e_fn costgen0
    in
    let { Types.fst = e_args0; Types.snd = costgen2 } =
      label_exprs e_args costgen1
    in
    { Types.fst = (Csyntax.Scall (e_ret0, e_fn0, e_args0)); Types.snd =
    costgen2 }
  | Csyntax.Ssequence (s1, s2) ->
    let { Types.fst = s10; Types.snd = costgen0 } =
      label_statement s1 costgen
    in
    let { Types.fst = s20; Types.snd = costgen1 } =
      label_statement s2 costgen0
    in
    { Types.fst = (Csyntax.Ssequence (s10, s20)); Types.snd = costgen1 }
  | Csyntax.Sifthenelse (e, s1, s2) ->
    let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
    let { Types.fst = s10; Types.snd = costgen1 } =
      label_statement s1 costgen0
    in
    let { Types.fst = s11; Types.snd = costgen2 } =
      add_cost_before s10 costgen1
    in
    let { Types.fst = s20; Types.snd = costgen3 } =
      label_statement s2 costgen2
    in
    let { Types.fst = s21; Types.snd = costgen4 } =
      add_cost_before s20 costgen3
    in
    { Types.fst = (Csyntax.Sifthenelse (e0, s11, s21)); Types.snd =
    costgen4 }
  | Csyntax.Swhile (e, s') ->
    let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
    let { Types.fst = s'0; Types.snd = costgen1 } =
      label_statement s' costgen0
    in
    let { Types.fst = s'1; Types.snd = costgen2 } =
      add_cost_before s'0 costgen1
    in
    let { Types.fst = s0; Types.snd = costgen3 } =
      add_cost_after (Csyntax.Swhile (e0, s'1)) costgen2
    in
    { Types.fst = s0; Types.snd = costgen3 }
  | Csyntax.Sdowhile (e, s') ->
    let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
    let { Types.fst = s'0; Types.snd = costgen1 } =
      label_statement s' costgen0
    in
    let { Types.fst = s'1; Types.snd = costgen2 } =
      add_cost_before s'0 costgen1
    in
    let { Types.fst = s0; Types.snd = costgen3 } =
      add_cost_after (Csyntax.Sdowhile (e0, s'1)) costgen2
    in
    { Types.fst = s0; Types.snd = costgen3 }
  | Csyntax.Sfor (s1, e, s2, s3) ->
    let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
    let { Types.fst = s10; Types.snd = costgen1 } =
      label_statement s1 costgen0
    in
    let { Types.fst = s20; Types.snd = costgen2 } =
      label_statement s2 costgen1
    in
    let { Types.fst = s30; Types.snd = costgen3 } =
      label_statement s3 costgen2
    in
    let { Types.fst = s31; Types.snd = costgen4 } =
      add_cost_before s30 costgen3
    in
    let { Types.fst = s0; Types.snd = costgen5 } =
      add_cost_after (Csyntax.Sfor (s10, e0, s20, s31)) costgen4
    in
    { Types.fst = s0; Types.snd = costgen5 }
  | Csyntax.Sbreak -> { Types.fst = Csyntax.Sbreak; Types.snd = costgen }
  | Csyntax.Scontinue ->
    { Types.fst = Csyntax.Scontinue; Types.snd = costgen }
  | Csyntax.Sreturn opt_e ->
    let { Types.fst = opt_e0; Types.snd = costgen0 } =
      label_opt_expr opt_e costgen
    in
    { Types.fst = (Csyntax.Sreturn opt_e0); Types.snd = costgen0 }
  | Csyntax.Sswitch (e, ls) ->
    let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
    let { Types.fst = ls0; Types.snd = costgen1 } =
      label_lstatements ls costgen0
    in
    { Types.fst = (Csyntax.Sswitch (e0, ls0)); Types.snd = costgen1 }
  | Csyntax.Slabel (l, s') ->
    let { Types.fst = s'0; Types.snd = costgen0 } =
      label_statement s' costgen
    in
    let { Types.fst = s'1; Types.snd = costgen1 } =
      add_cost_before s'0 costgen0
    in
    { Types.fst = (Csyntax.Slabel (l, s'1)); Types.snd = costgen1 }
  | Csyntax.Sgoto l -> { Types.fst = (Csyntax.Sgoto l); Types.snd = costgen }
  | Csyntax.Scost (l, s') ->
    let { Types.fst = s'0; Types.snd = costgen0 } =
      label_statement s' costgen
    in
    { Types.fst = (Csyntax.Scost (l, s'0)); Types.snd = costgen0 }
(** val label_lstatements :
    Csyntax.labeled_statements -> Identifiers.universe ->
    (Csyntax.labeled_statements, Identifiers.universe) Types.prod **)
and label_lstatements ls costgen =
  match ls with
  | Csyntax.LSdefault s ->
    let { Types.fst = s0; Types.snd = costgen0 } = label_statement s costgen
    in
    let { Types.fst = s1; Types.snd = costgen1 } =
      add_cost_before s0 costgen0
    in
    { Types.fst = (Csyntax.LSdefault s1); Types.snd = costgen1 }
  | Csyntax.LScase (sz, i, s, ls') ->
    let { Types.fst = s0; Types.snd = costgen0 } = label_statement s costgen
    in
    let { Types.fst = s1; Types.snd = costgen1 } =
      add_cost_before s0 costgen0
    in
    let { Types.fst = ls'0; Types.snd = costgen2 } =
      label_lstatements ls' costgen1
    in
    { Types.fst = (Csyntax.LScase (sz, i, s1, ls'0)); Types.snd = costgen2 }

(** val label_function :
    Identifiers.universe -> Csyntax.function0 -> (Csyntax.function0,
    Identifiers.universe) Types.prod **)
let label_function costgen f =
  let { Types.fst = body; Types.snd = costgen0 } =
    label_statement f.Csyntax.fn_body costgen
  in
  let { Types.fst = body0; Types.snd = costgen1 } =
    add_cost_before body costgen0
  in
  { Types.fst = { Csyntax.fn_return = f.Csyntax.fn_return;
  Csyntax.fn_params = f.Csyntax.fn_params; Csyntax.fn_vars =
  f.Csyntax.fn_vars; Csyntax.fn_body = body0 }; Types.snd = costgen1 }

(** val label_fundef :
    Identifiers.universe -> Csyntax.clight_fundef -> (Csyntax.clight_fundef,
    Identifiers.universe) Types.prod **)
let label_fundef gen = function
| Csyntax.CL_Internal f0 ->
  let { Types.fst = f'; Types.snd = gen' } = label_function gen f0 in
  { Types.fst = (Csyntax.CL_Internal f'); Types.snd = gen' }
| Csyntax.CL_External (id, args, ty) ->
  { Types.fst = (Csyntax.CL_External (id, args, ty)); Types.snd = gen }

(** val clight_label :
    Csyntax.clight_program -> (Csyntax.clight_program, CostLabel.costlabel)
    Types.prod **)
let rec clight_label p =
  let costgen = Identifiers.new_universe PreIdentifiers.CostTag in
  let { Types.fst = init_cost; Types.snd = costgen0 } =
    Identifiers.fresh PreIdentifiers.CostTag costgen
  in
  { Types.fst =
  (AST.transform_program_gen PreIdentifiers.CostTag costgen0 p (fun x ->
    label_fundef)).Types.fst; Types.snd = init_cost }