extracted/rTL.ml

   1 open Preamble
   2
   3 open Extra_bool
   4
   5 open Coqlib
   6
   7 open Values
   8
   9 open FrontEndVal
  10
  11 open GenMem
  12
  13 open FrontEndMem
  14
  15 open Globalenvs
  16
  17 open String
  18
  19 open Sets
  20
  21 open Listb
  22
  23 open LabelledObjects
  24
  25 open BitVectorTrie
  26
  27 open Graphs
  28
  29 open I8051
  30
  31 open Order
  32
  33 open Registers
  34
  35 open CostLabel
  36
  37 open Hide
  38
  39 open Proper
  40
  41 open PositiveMap
  42
  43 open Deqsets
  44
  45 open ErrorMessages
  46
  47 open PreIdentifiers
  48
  49 open Errors
  50
  51 open Extralib
  52
  53 open Lists
  54
  55 open Identifiers
  56
  57 open Integers
  58
  59 open AST
  60
  61 open Division
  62
  63 open Exp
  64
  65 open Arithmetic
  66
  67 open Setoids
  68
  69 open Monad
  70
  71 open Option
  72
  73 open Extranat
  74
  75 open Vector
  76
  77 open Div_and_mod
  78
  79 open Jmeq
  80
  81 open Russell
  82
  83 open List
  84
  85 open Util
  86
  87 open FoldStuff
  88
  89 open BitVector
  90
  91 open Types
  92
  93 open Bool
  94
  95 open Relations
  96
  97 open Nat
  98
  99 open Hints_declaration
 100
 101 open Core_notation
 102
 103 open Pts
 104
 105 open Logic
 106
 107 open Positive
 108
 109 open Z
 110
 111 open BitVectorZ
 112
 113 open Pointers
 114
 115 open ByteValues
 116
 117 open BackEndOps
 118
 119 open Joint
 120
 121 type rtl_seq =
 122 | Rtl_stack_address of Registers.register * Registers.register
 123
 124 (** val rtl_seq_rect_Type4 :
 125     (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
 126 let rec rtl_seq_rect_Type4 h_rtl_stack_address = function
 127 | Rtl_stack_address (x_18151, x_18150) -> h_rtl_stack_address x_18151 x_18150
 128
 129 (** val rtl_seq_rect_Type5 :
 130     (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
 131 let rec rtl_seq_rect_Type5 h_rtl_stack_address = function
 132 | Rtl_stack_address (x_18155, x_18154) -> h_rtl_stack_address x_18155 x_18154
 133
 134 (** val rtl_seq_rect_Type3 :
 135     (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
 136 let rec rtl_seq_rect_Type3 h_rtl_stack_address = function
 137 | Rtl_stack_address (x_18159, x_18158) -> h_rtl_stack_address x_18159 x_18158
 138
 139 (** val rtl_seq_rect_Type2 :
 140     (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
 141 let rec rtl_seq_rect_Type2 h_rtl_stack_address = function
 142 | Rtl_stack_address (x_18163, x_18162) -> h_rtl_stack_address x_18163 x_18162
 143
 144 (** val rtl_seq_rect_Type1 :
 145     (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
 146 let rec rtl_seq_rect_Type1 h_rtl_stack_address = function
 147 | Rtl_stack_address (x_18167, x_18166) -> h_rtl_stack_address x_18167 x_18166
 148
 149 (** val rtl_seq_rect_Type0 :
 150     (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
 151 let rec rtl_seq_rect_Type0 h_rtl_stack_address = function
 152 | Rtl_stack_address (x_18171, x_18170) -> h_rtl_stack_address x_18171 x_18170
 153
 154 (** val rtl_seq_inv_rect_Type4 :
 155     rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
 156 let rtl_seq_inv_rect_Type4 hterm h1 =
 157   let hcut = rtl_seq_rect_Type4 h1 hterm in hcut __
 158
 159 (** val rtl_seq_inv_rect_Type3 :
 160     rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
 161 let rtl_seq_inv_rect_Type3 hterm h1 =
 162   let hcut = rtl_seq_rect_Type3 h1 hterm in hcut __
 163
 164 (** val rtl_seq_inv_rect_Type2 :
 165     rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
 166 let rtl_seq_inv_rect_Type2 hterm h1 =
 167   let hcut = rtl_seq_rect_Type2 h1 hterm in hcut __
 168
 169 (** val rtl_seq_inv_rect_Type1 :
 170     rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
 171 let rtl_seq_inv_rect_Type1 hterm h1 =
 172   let hcut = rtl_seq_rect_Type1 h1 hterm in hcut __
 173
 174 (** val rtl_seq_inv_rect_Type0 :
 175     rtl_seq -> (Registers.register -> Registers.register -> __ -> 'a1) -> 'a1 **)
 176 let rtl_seq_inv_rect_Type0 hterm h1 =
 177   let hcut = rtl_seq_rect_Type0 h1 hterm in hcut __
 178
 179 (** val rtl_seq_discr : rtl_seq -> rtl_seq -> __ **)
 180 let rtl_seq_discr x y =
 181   Logic.eq_rect_Type2 x
 182     (let Rtl_stack_address (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __))
 183     y
 184
 185 (** val rtl_seq_jmdiscr : rtl_seq -> rtl_seq -> __ **)
 186 let rtl_seq_jmdiscr x y =
 187   Logic.eq_rect_Type2 x
 188     (let Rtl_stack_address (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __))
 189     y
 190
 191 (** val rTL_uns : Joint.unserialized_params **)
 192 let rTL_uns =
 193   { Joint.ext_seq_labels = (fun x -> List.Nil); Joint.has_tailcalls =
 194     Bool.False }
 195
 196 (** val rTL_functs : Joint.get_pseudo_reg_functs **)
 197 let rTL_functs =
 198   { Joint.acc_a_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
 199     Joint.acc_b_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
 200     Joint.acc_a_args = (fun a ->
 201     match Obj.magic a with
 202     | Joint.Reg r -> List.Cons (r, List.Nil)
 203     | Joint.Imm x -> List.Nil); Joint.acc_b_args = (fun a ->
 204     match Obj.magic a with
 205     | Joint.Reg r -> List.Cons (r, List.Nil)
 206     | Joint.Imm x -> List.Nil); Joint.dpl_regs = (fun r -> List.Cons
 207     ((Obj.magic r), List.Nil)); Joint.dph_regs = (fun r -> List.Cons
 208     ((Obj.magic r), List.Nil)); Joint.dpl_args = (fun a ->
 209     match Obj.magic a with
 210     | Joint.Reg r -> List.Cons (r, List.Nil)
 211     | Joint.Imm x -> List.Nil); Joint.dph_args = (fun a ->
 212     match Obj.magic a with
 213     | Joint.Reg r -> List.Cons (r, List.Nil)
 214     | Joint.Imm x -> List.Nil); Joint.snd_args = (fun a ->
 215     match Obj.magic a with
 216     | Joint.Reg r -> List.Cons (r, List.Nil)
 217     | Joint.Imm x -> List.Nil); Joint.pair_move_regs = (fun x ->
 218     List.append (List.Cons ((Obj.magic x).Types.fst, List.Nil))
 219       (match (Obj.magic x).Types.snd with
 220        | Joint.Reg r -> List.Cons (r, List.Nil)
 221        | Joint.Imm x0 -> List.Nil)); Joint.f_call_args = (fun l ->
 222     Util.foldl (fun l1 a ->
 223       List.append l1
 224         (match a with
 225          | Joint.Reg r -> List.Cons (r, List.Nil)
 226          | Joint.Imm x -> List.Nil)) List.Nil (Obj.magic l));
 227     Joint.f_call_dest = (fun x -> Obj.magic x); Joint.ext_seq_regs =
 228     (fun ext ->
 229     let Rtl_stack_address (r1, r2) = Obj.magic ext in
 230     List.Cons (r1, (List.Cons (r2, List.Nil)))); Joint.params_regs =
 231     (fun x -> Obj.magic x) }
 232
 233 (** val rTL : Joint.graph_params **)
 234 let rTL =
 235   { Joint.u_pars = rTL_uns; Joint.functs = rTL_functs }
 236
 237 type rtl_program = Joint.joint_program
 238
 239 (** val dpi1__o__reg_to_rtl_snd_argument__o__inject :
 240     (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
 241 let dpi1__o__reg_to_rtl_snd_argument__o__inject x2 =
 242   Joint.psd_argument_from_reg x2.Types.dpi1
 243
 244 (** val eject__o__reg_to_rtl_snd_argument__o__inject :
 245     Registers.register Types.sig0 -> Joint.psd_argument Types.sig0 **)
 246 let eject__o__reg_to_rtl_snd_argument__o__inject x2 =
 247   Joint.psd_argument_from_reg (Types.pi1 x2)
 248
 249 (** val reg_to_rtl_snd_argument__o__inject :
 250     Registers.register -> Joint.psd_argument Types.sig0 **)
 251 let reg_to_rtl_snd_argument__o__inject x1 =
 252   Joint.psd_argument_from_reg x1
 253
 254 (** val dpi1__o__reg_to_rtl_snd_argument :
 255     (Registers.register, 'a1) Types.dPair -> Joint.psd_argument **)
 256 let dpi1__o__reg_to_rtl_snd_argument x1 =
 257   Joint.psd_argument_from_reg x1.Types.dpi1
 258
 259 (** val eject__o__reg_to_rtl_snd_argument :
 260     Registers.register Types.sig0 -> Joint.psd_argument **)
 261 let eject__o__reg_to_rtl_snd_argument x1 =
 262   Joint.psd_argument_from_reg (Types.pi1 x1)
 263
 264 (** val dpi1__o__byte_to_rtl_snd_argument__o__inject :
 265     (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
 266 let dpi1__o__byte_to_rtl_snd_argument__o__inject x2 =
 267   Joint.psd_argument_from_byte x2.Types.dpi1
 268
 269 (** val eject__o__byte_to_rtl_snd_argument__o__inject :
 270     BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0 **)
 271 let eject__o__byte_to_rtl_snd_argument__o__inject x2 =
 272   Joint.psd_argument_from_byte (Types.pi1 x2)
 273
 274 (** val byte_to_rtl_snd_argument__o__inject :
 275     BitVector.byte -> Joint.psd_argument Types.sig0 **)
 276 let byte_to_rtl_snd_argument__o__inject x1 =
 277   Joint.psd_argument_from_byte x1
 278
 279 (** val dpi1__o__byte_to_rtl_snd_argument :
 280     (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument **)
 281 let dpi1__o__byte_to_rtl_snd_argument x1 =
 282   Joint.psd_argument_from_byte x1.Types.dpi1
 283
 284 (** val eject__o__byte_to_rtl_snd_argument :
 285     BitVector.byte Types.sig0 -> Joint.psd_argument **)
 286 let eject__o__byte_to_rtl_snd_argument x1 =
 287   Joint.psd_argument_from_byte (Types.pi1 x1)
 288
 289 (** val rTL_premain : rtl_program -> Joint.joint_closed_internal_function **)
 290 let rTL_premain p =
 291   let l1 = Positive.One in
 292   let l2 = Positive.P0 Positive.One in
 293   let l3 = Positive.P1 Positive.One in
 294   let rs = List.Cons (Positive.One, (List.Cons ((Positive.P0 Positive.One),
 295     (List.Cons ((Positive.P1 Positive.One), (List.Cons ((Positive.P0
 296     (Positive.P0 Positive.One)), List.Nil)))))))
 297   in
 298   let res = { Joint.joint_if_luniverse = (Positive.P0 (Positive.P0
 299     Positive.One)); Joint.joint_if_runiverse = (Positive.P1 (Positive.P0
 300     Positive.One)); Joint.joint_if_result = (Obj.magic List.Nil);
 301     Joint.joint_if_params = (Obj.magic rs); Joint.joint_if_stacksize = Nat.O;
 302     Joint.joint_if_local_stacksize = Nat.O; Joint.joint_if_code =
 303     (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
 304     Joint.joint_if_entry = (Obj.magic l1) }
 305   in
 306   let res0 =
 307     Joint.add_graph rTL
 308       (Joint.prog_names (Joint.graph_params_to_params rTL) p) l1
 309       (Joint.Sequential ((Joint.COST_LABEL p.Joint.init_cost_label),
 310       (Obj.magic l2))) res
 311   in
 312   let res1 =
 313     Joint.add_graph rTL
 314       (Joint.prog_names (Joint.graph_params_to_params rTL) p) l2
 315       (Joint.Sequential ((Joint.CALL ((Types.Inl
 316       p.Joint.joint_prog.AST.prog_main), (Obj.magic List.Nil),
 317       (Obj.magic rs))), (Obj.magic l3))) res0
 318   in
 319   let res2 =
 320     Joint.add_graph rTL
 321       (Joint.prog_names (Joint.graph_params_to_params rTL) p) l3 (Joint.Final
 322       (Joint.GOTO l3)) res1
 323   in
 324   res2
 325