extracted/rTL_semantics.ml

   1 open Preamble
   2
   3 open ExtraMonads
   4
   5 open Deqsets_extra
   6
   7 open State
   8
   9 open Bind_new
  10
  11 open BindLists
  12
  13 open Blocks
  14
  15 open TranslateUtils
  16
  17 open ExtraGlobalenvs
  18
  19 open I8051bis
  20
  21 open String
  22
  23 open Sets
  24
  25 open Listb
  26
  27 open LabelledObjects
  28
  29 open BitVectorTrie
  30
  31 open Graphs
  32
  33 open I8051
  34
  35 open Order
  36
  37 open Registers
  38
  39 open BackEndOps
  40
  41 open Joint
  42
  43 open BEMem
  44
  45 open CostLabel
  46
  47 open Events
  48
  49 open IOMonad
  50
  51 open IO
  52
  53 open Extra_bool
  54
  55 open Coqlib
  56
  57 open Values
  58
  59 open FrontEndVal
  60
  61 open Hide
  62
  63 open ByteValues
  64
  65 open Division
  66
  67 open Z
  68
  69 open BitVectorZ
  70
  71 open Pointers
  72
  73 open GenMem
  74
  75 open FrontEndMem
  76
  77 open Proper
  78
  79 open PositiveMap
  80
  81 open Deqsets
  82
  83 open Extralib
  84
  85 open Lists
  86
  87 open Identifiers
  88
  89 open Exp
  90
  91 open Arithmetic
  92
  93 open Vector
  94
  95 open Div_and_mod
  96
  97 open Util
  98
  99 open FoldStuff
 100
 101 open BitVector
 102
 103 open Extranat
 104
 105 open Integers
 106
 107 open AST
 108
 109 open ErrorMessages
 110
 111 open Option
 112
 113 open Setoids
 114
 115 open Monad
 116
 117 open Jmeq
 118
 119 open Russell
 120
 121 open Positive
 122
 123 open PreIdentifiers
 124
 125 open Bool
 126
 127 open Relations
 128
 129 open Nat
 130
 131 open List
 132
 133 open Hints_declaration
 134
 135 open Core_notation
 136
 137 open Pts
 138
 139 open Logic
 140
 141 open Types
 142
 143 open Errors
 144
 145 open Globalenvs
 146
 147 open Joint_semantics
 148
 149 open SemanticsUtils
 150
 151 open RTL
 152
 153 type reg_sp = { reg_sp_env : ByteValues.beval Identifiers.identifier_map;
 154                 stackp : ByteValues.xpointer }
 155
 156 (** val reg_sp_rect_Type4 :
 157     (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
 158     'a1) -> reg_sp -> 'a1 **)
 159 let rec reg_sp_rect_Type4 h_mk_reg_sp x_25168 =
 160   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25168 in
 161   h_mk_reg_sp reg_sp_env0 stackp0
 162
 163 (** val reg_sp_rect_Type5 :
 164     (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
 165     'a1) -> reg_sp -> 'a1 **)
 166 let rec reg_sp_rect_Type5 h_mk_reg_sp x_25170 =
 167   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25170 in
 168   h_mk_reg_sp reg_sp_env0 stackp0
 169
 170 (** val reg_sp_rect_Type3 :
 171     (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
 172     'a1) -> reg_sp -> 'a1 **)
 173 let rec reg_sp_rect_Type3 h_mk_reg_sp x_25172 =
 174   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25172 in
 175   h_mk_reg_sp reg_sp_env0 stackp0
 176
 177 (** val reg_sp_rect_Type2 :
 178     (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
 179     'a1) -> reg_sp -> 'a1 **)
 180 let rec reg_sp_rect_Type2 h_mk_reg_sp x_25174 =
 181   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25174 in
 182   h_mk_reg_sp reg_sp_env0 stackp0
 183
 184 (** val reg_sp_rect_Type1 :
 185     (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
 186     'a1) -> reg_sp -> 'a1 **)
 187 let rec reg_sp_rect_Type1 h_mk_reg_sp x_25176 =
 188   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25176 in
 189   h_mk_reg_sp reg_sp_env0 stackp0
 190
 191 (** val reg_sp_rect_Type0 :
 192     (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
 193     'a1) -> reg_sp -> 'a1 **)
 194 let rec reg_sp_rect_Type0 h_mk_reg_sp x_25178 =
 195   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25178 in
 196   h_mk_reg_sp reg_sp_env0 stackp0
 197
 198 (** val reg_sp_env :
 199     reg_sp -> ByteValues.beval Identifiers.identifier_map **)
 200 let rec reg_sp_env xxx =
 201   xxx.reg_sp_env
 202
 203 (** val stackp : reg_sp -> ByteValues.xpointer **)
 204 let rec stackp xxx =
 205   xxx.stackp
 206
 207 (** val reg_sp_inv_rect_Type4 :
 208     reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
 209     ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
 210 let reg_sp_inv_rect_Type4 hterm h1 =
 211   let hcut = reg_sp_rect_Type4 h1 hterm in hcut __
 212
 213 (** val reg_sp_inv_rect_Type3 :
 214     reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
 215     ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
 216 let reg_sp_inv_rect_Type3 hterm h1 =
 217   let hcut = reg_sp_rect_Type3 h1 hterm in hcut __
 218
 219 (** val reg_sp_inv_rect_Type2 :
 220     reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
 221     ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
 222 let reg_sp_inv_rect_Type2 hterm h1 =
 223   let hcut = reg_sp_rect_Type2 h1 hterm in hcut __
 224
 225 (** val reg_sp_inv_rect_Type1 :
 226     reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
 227     ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
 228 let reg_sp_inv_rect_Type1 hterm h1 =
 229   let hcut = reg_sp_rect_Type1 h1 hterm in hcut __
 230
 231 (** val reg_sp_inv_rect_Type0 :
 232     reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
 233     ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
 234 let reg_sp_inv_rect_Type0 hterm h1 =
 235   let hcut = reg_sp_rect_Type0 h1 hterm in hcut __
 236
 237 (** val reg_sp_discr : reg_sp -> reg_sp -> __ **)
 238 let reg_sp_discr x y =
 239   Logic.eq_rect_Type2 x
 240     (let { reg_sp_env = a0; stackp = a1 } = x in
 241     Obj.magic (fun _ dH -> dH __ __)) y
 242
 243 (** val reg_sp_jmdiscr : reg_sp -> reg_sp -> __ **)
 244 let reg_sp_jmdiscr x y =
 245   Logic.eq_rect_Type2 x
 246     (let { reg_sp_env = a0; stackp = a1 } = x in
 247     Obj.magic (fun _ dH -> dH __ __)) y
 248
 249 (** val dpi1__o__reg_sp_env__o__inject :
 250     (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
 251     Types.sig0 **)
 252 let dpi1__o__reg_sp_env__o__inject x2 =
 253   x2.Types.dpi1.reg_sp_env
 254
 255 (** val eject__o__reg_sp_env__o__inject :
 256     reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map
 257     Types.sig0 **)
 258 let eject__o__reg_sp_env__o__inject x2 =
 259   (Types.pi1 x2).reg_sp_env
 260
 261 (** val reg_sp_env__o__inject :
 262     reg_sp -> ByteValues.beval Identifiers.identifier_map Types.sig0 **)
 263 let reg_sp_env__o__inject x1 =
 264   x1.reg_sp_env
 265
 266 (** val dpi1__o__reg_sp_env :
 267     (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map **)
 268 let dpi1__o__reg_sp_env x1 =
 269   x1.Types.dpi1.reg_sp_env
 270
 271 (** val eject__o__reg_sp_env :
 272     reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map **)
 273 let eject__o__reg_sp_env x1 =
 274   (Types.pi1 x1).reg_sp_env
 275
 276 (** val reg_sp_store :
 277     PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp **)
 278 let reg_sp_store reg v locals =
 279   let locals' = SemanticsUtils.reg_store reg v locals.reg_sp_env in
 280   { reg_sp_env = locals'; stackp = locals.stackp }
 281
 282 (** val reg_sp_retrieve :
 283     reg_sp -> Registers.register -> ByteValues.beval Errors.res **)
 284 let reg_sp_retrieve locals =
 285   SemanticsUtils.reg_retrieve locals.reg_sp_env
 286
 287 (** val reg_sp_empty : ByteValues.xpointer -> reg_sp **)
 288 let reg_sp_empty x =
 289   { reg_sp_env = (Identifiers.empty_map PreIdentifiers.RegisterTag); stackp =
 290     x }
 291
 292 type frame = { fr_ret_regs : Registers.register List.list;
 293                fr_pc : ByteValues.program_counter;
 294                fr_carry : ByteValues.bebit; fr_regs : reg_sp }
 295
 296 (** val frame_rect_Type4 :
 297     (Registers.register List.list -> ByteValues.program_counter ->
 298     ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
 299 let rec frame_rect_Type4 h_mk_frame x_25194 =
 300   let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
 301     fr_regs = fr_regs0 } = x_25194
 302   in
 303   h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
 304
 305 (** val frame_rect_Type5 :
 306     (Registers.register List.list -> ByteValues.program_counter ->
 307     ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
 308 let rec frame_rect_Type5 h_mk_frame x_25196 =
 309   let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
 310     fr_regs = fr_regs0 } = x_25196
 311   in
 312   h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
 313
 314 (** val frame_rect_Type3 :
 315     (Registers.register List.list -> ByteValues.program_counter ->
 316     ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
 317 let rec frame_rect_Type3 h_mk_frame x_25198 =
 318   let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
 319     fr_regs = fr_regs0 } = x_25198
 320   in
 321   h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
 322
 323 (** val frame_rect_Type2 :
 324     (Registers.register List.list -> ByteValues.program_counter ->
 325     ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
 326 let rec frame_rect_Type2 h_mk_frame x_25200 =
 327   let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
 328     fr_regs = fr_regs0 } = x_25200
 329   in
 330   h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
 331
 332 (** val frame_rect_Type1 :
 333     (Registers.register List.list -> ByteValues.program_counter ->
 334     ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
 335 let rec frame_rect_Type1 h_mk_frame x_25202 =
 336   let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
 337     fr_regs = fr_regs0 } = x_25202
 338   in
 339   h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
 340
 341 (** val frame_rect_Type0 :
 342     (Registers.register List.list -> ByteValues.program_counter ->
 343     ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
 344 let rec frame_rect_Type0 h_mk_frame x_25204 =
 345   let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
 346     fr_regs = fr_regs0 } = x_25204
 347   in
 348   h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
 349
 350 (** val fr_ret_regs : frame -> Registers.register List.list **)
 351 let rec fr_ret_regs xxx =
 352   xxx.fr_ret_regs
 353
 354 (** val fr_pc : frame -> ByteValues.program_counter **)
 355 let rec fr_pc xxx =
 356   xxx.fr_pc
 357
 358 (** val fr_carry : frame -> ByteValues.bebit **)
 359 let rec fr_carry xxx =
 360   xxx.fr_carry
 361
 362 (** val fr_regs : frame -> reg_sp **)
 363 let rec fr_regs xxx =
 364   xxx.fr_regs
 365
 366 (** val frame_inv_rect_Type4 :
 367     frame -> (Registers.register List.list -> ByteValues.program_counter ->
 368     ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
 369 let frame_inv_rect_Type4 hterm h1 =
 370   let hcut = frame_rect_Type4 h1 hterm in hcut __
 371
 372 (** val frame_inv_rect_Type3 :
 373     frame -> (Registers.register List.list -> ByteValues.program_counter ->
 374     ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
 375 let frame_inv_rect_Type3 hterm h1 =
 376   let hcut = frame_rect_Type3 h1 hterm in hcut __
 377
 378 (** val frame_inv_rect_Type2 :
 379     frame -> (Registers.register List.list -> ByteValues.program_counter ->
 380     ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
 381 let frame_inv_rect_Type2 hterm h1 =
 382   let hcut = frame_rect_Type2 h1 hterm in hcut __
 383
 384 (** val frame_inv_rect_Type1 :
 385     frame -> (Registers.register List.list -> ByteValues.program_counter ->
 386     ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
 387 let frame_inv_rect_Type1 hterm h1 =
 388   let hcut = frame_rect_Type1 h1 hterm in hcut __
 389
 390 (** val frame_inv_rect_Type0 :
 391     frame -> (Registers.register List.list -> ByteValues.program_counter ->
 392     ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
 393 let frame_inv_rect_Type0 hterm h1 =
 394   let hcut = frame_rect_Type0 h1 hterm in hcut __
 395
 396 (** val frame_discr : frame -> frame -> __ **)
 397 let frame_discr x y =
 398   Logic.eq_rect_Type2 x
 399     (let { fr_ret_regs = a0; fr_pc = a1; fr_carry = a2; fr_regs = a3 } = x in
 400     Obj.magic (fun _ dH -> dH __ __ __ __)) y
 401
 402 (** val frame_jmdiscr : frame -> frame -> __ **)
 403 let frame_jmdiscr x y =
 404   Logic.eq_rect_Type2 x
 405     (let { fr_ret_regs = a0; fr_pc = a1; fr_carry = a2; fr_regs = a3 } = x in
 406     Obj.magic (fun _ dH -> dH __ __ __ __)) y
 407
 408 (** val rTL_state_params : Joint_semantics.sem_state_params **)
 409 let rTL_state_params =
 410   { Joint_semantics.empty_framesT = (Obj.magic List.Nil);
 411     Joint_semantics.empty_regsT = (Obj.magic reg_sp_empty);
 412     Joint_semantics.load_sp = (fun env -> Errors.OK (Obj.magic env).stackp);
 413     Joint_semantics.save_sp = (fun env ->
 414     Obj.magic (fun x -> { reg_sp_env = (Obj.magic env).reg_sp_env; stackp =
 415       x })) }
 416
 417 type rTL_state = Joint_semantics.state
 418
 419 (** val rtl_arg_retrieve :
 420     reg_sp -> Joint.psd_argument -> ByteValues.beval Errors.res **)
 421 let rtl_arg_retrieve env = function
 422 | Joint.Reg r -> SemanticsUtils.reg_retrieve env.reg_sp_env r
 423 | Joint.Imm b -> Errors.OK (ByteValues.BVByte b)
 424
 425 (** val rtl_fetch_ra :
 426     rTL_state -> (rTL_state, ByteValues.program_counter) Types.prod
 427     Errors.res **)
 428 let rtl_fetch_ra st =
 429   Obj.magic
 430     (Monad.m_bind0 (Monad.max_def Errors.res0)
 431       (Obj.magic
 432         (Errors.opt_to_res (List.Cons ((Errors.MSG
 433           ErrorMessages.FrameErrorOnPop), List.Nil))
 434           st.Joint_semantics.st_frms)) (fun frms ->
 435       match frms with
 436       | List.Nil ->
 437         Obj.magic (Errors.Error (List.Cons ((Errors.MSG
 438           ErrorMessages.EmptyStack), List.Nil)))
 439       | List.Cons (hd, tl) ->
 440         Obj.magic (Errors.OK { Types.fst = st; Types.snd = hd.fr_pc })))
 441
 442 (** val rtl_init_local : Registers.register -> reg_sp -> reg_sp **)
 443 let rtl_init_local local =
 444   reg_sp_store local ByteValues.BVundef
 445
 446 (** val rtl_setup_call_separate :
 447     Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
 448     -> rTL_state -> rTL_state Errors.res **)
 449 let rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st =
 450   (let { Types.fst = mem; Types.snd = b } =
 451      GenMem.alloc st.Joint_semantics.m (Z.z_of_nat Nat.O)
 452        (Z.z_of_nat stacksize)
 453    in
 454   (fun _ ->
 455   let sp = { Pointers.pblock = b; Pointers.poff =
 456     (BitVector.zero Pointers.offset_size) }
 457   in
 458   Obj.magic
 459     (Monad.m_bind0 (Monad.max_def Errors.res0)
 460       (Obj.magic
 461         (Errors.mfold_left2 (fun lenv dest src ->
 462           Obj.magic
 463             (Monad.m_bind0 (Monad.max_def Errors.res0)
 464               (Obj.magic
 465                 (rtl_arg_retrieve (Obj.magic st.Joint_semantics.regs) src))
 466               (fun v -> Obj.magic (Errors.OK (reg_sp_store dest v lenv)))))
 467           (Errors.OK (reg_sp_empty sp)) formal_arg_regs actual_arg_regs))
 468       (fun new_regs ->
 469       Obj.magic (Errors.OK
 470         (Joint_semantics.set_regs rTL_state_params new_regs
 471           (Joint_semantics.set_m rTL_state_params mem st))))))) __
 472
 473 (** val rtl_setup_call_separate_overflow :
 474     Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
 475     -> rTL_state -> rTL_state Errors.res **)
 476 let rtl_setup_call_separate_overflow stacksize formal_arg_regs actual_arg_regs st =
 477   match Nat.leb (Nat.S (Nat.plus stacksize st.Joint_semantics.stack_usage))
 478           (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 479             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 480             (Nat.S (Nat.S Nat.O))))))))))))))))) with
 481   | Bool.True ->
 482     rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st
 483   | Bool.False ->
 484     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.StackOverflow),
 485       List.Nil))
 486
 487 (** val rtl_setup_call_unique :
 488     Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
 489     -> rTL_state -> rTL_state Errors.res **)
 490 let rtl_setup_call_unique stacksize formal_arg_regs actual_arg_regs st =
 491   Obj.magic
 492     (Monad.m_bind0 (Monad.max_def Errors.res0)
 493       (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
 494       let newsp =
 495         Pointers.neg_shift_pointer (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 496           (Nat.S (Nat.S Nat.O)))))))) (Types.pi1 sp)
 497           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 498             (Nat.S (Nat.S (Nat.S Nat.O)))))))) stacksize)
 499       in
 500       Monad.m_bind0 (Monad.max_def Errors.res0)
 501         (Obj.magic
 502           (Errors.mfold_left2 (fun lenv dest src ->
 503             Obj.magic
 504               (Monad.m_bind0 (Monad.max_def Errors.res0)
 505                 (Obj.magic
 506                   (rtl_arg_retrieve (Obj.magic st.Joint_semantics.regs) src))
 507                 (fun v -> Obj.magic (Errors.OK (reg_sp_store dest v lenv)))))
 508             (Errors.OK (reg_sp_empty newsp)) formal_arg_regs actual_arg_regs))
 509         (fun new_regs ->
 510         Obj.magic (Errors.OK
 511           (Joint_semantics.set_regs rTL_state_params new_regs st)))))
 512
 513 type rTL_state_pc = Joint_semantics.state_pc
 514
 515 (** val rtl_save_frame :
 516     Registers.register List.list -> rTL_state_pc -> __ **)
 517 let rtl_save_frame retregs st =
 518   Monad.m_bind0 (Monad.max_def Errors.res0)
 519     (Obj.magic
 520       (Errors.opt_to_res (List.Cons ((Errors.MSG
 521         ErrorMessages.FrameErrorOnPush), List.Nil))
 522         st.Joint_semantics.st_no_pc.Joint_semantics.st_frms)) (fun frms ->
 523     let frame0 = List.Cons ({ fr_ret_regs = retregs; fr_pc =
 524       st.Joint_semantics.pc; fr_carry =
 525       st.Joint_semantics.st_no_pc.Joint_semantics.carry; fr_regs =
 526       (Obj.magic st.Joint_semantics.st_no_pc.Joint_semantics.regs) }, frms)
 527     in
 528     Obj.magic (Errors.OK
 529       (Joint_semantics.set_frms rTL_state_params (Obj.magic frame0)
 530         st.Joint_semantics.st_no_pc)))
 531
 532 (** val rtl_fetch_external_args :
 533     AST.external_function -> rTL_state -> Joint.psd_argument List.list ->
 534     Values.val0 List.list Errors.res **)
 535 let rtl_fetch_external_args _ =
 536   failwith "AXIOM TO BE REALIZED"
 537
 538 (** val rtl_set_result :
 539     Values.val0 List.list -> Registers.register List.list -> rTL_state ->
 540     rTL_state Errors.res **)
 541 let rtl_set_result _ =
 542   failwith "AXIOM TO BE REALIZED"
 543
 544 (** val rtl_reg_store :
 545     PreIdentifiers.identifier -> ByteValues.beval -> Joint_semantics.state ->
 546     Joint_semantics.state **)
 547 let rtl_reg_store r v st =
 548   let mem = reg_sp_store r v (Obj.magic st.Joint_semantics.regs) in
 549   Joint_semantics.set_regs rTL_state_params (Obj.magic mem) st
 550
 551 (** val rtl_reg_retrieve :
 552     Joint_semantics.state -> Registers.register -> ByteValues.beval
 553     Errors.res **)
 554 let rtl_reg_retrieve st l =
 555   reg_sp_retrieve (Obj.magic st.Joint_semantics.regs) l
 556
 557 (** val rtl_read_result :
 558     Registers.register List.list -> rTL_state -> ByteValues.beval List.list
 559     Errors.res **)
 560 let rtl_read_result rets st =
 561   Obj.magic
 562     (Monad.m_list_map (Monad.max_def Errors.res0)
 563       (Obj.magic (rtl_reg_retrieve st)) rets)
 564
 565 (** val rtl_pop_frame_separate :
 566     Registers.register List.list -> rTL_state -> (rTL_state,
 567     ByteValues.program_counter) Types.prod Errors.res **)
 568 let rtl_pop_frame_separate ret st =
 569   Obj.magic
 570     (Monad.m_bind0 (Monad.max_def Errors.res0)
 571       (Obj.magic
 572         (Errors.opt_to_res (List.Cons ((Errors.MSG
 573           ErrorMessages.FrameErrorOnPop), List.Nil))
 574           st.Joint_semantics.st_frms)) (fun frms ->
 575       match frms with
 576       | List.Nil ->
 577         Obj.magic (Errors.Error (List.Cons ((Errors.MSG
 578           ErrorMessages.EmptyStack), List.Nil)))
 579       | List.Cons (hd, tl) ->
 580         Monad.m_bind0 (Monad.max_def Errors.res0)
 581           (Obj.magic (rtl_read_result ret st)) (fun ret_vals ->
 582           let reg_vals = Util.zip_pottier hd.fr_ret_regs ret_vals in
 583           Monad.m_bind0 (Monad.max_def Errors.res0)
 584             (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
 585             let st0 =
 586               Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
 587                 (Joint_semantics.set_regs rTL_state_params
 588                   (Obj.magic hd.fr_regs)
 589                   (Joint_semantics.set_carry rTL_state_params hd.fr_carry
 590                     (Joint_semantics.set_m rTL_state_params
 591                       (GenMem.free st.Joint_semantics.m
 592                         (Types.pi1 sp).Pointers.pblock) st)))
 593             in
 594             let pc = hd.fr_pc in
 595             let st1 =
 596               Util.foldl (fun st1 reg_val ->
 597                 rtl_reg_store reg_val.Types.fst reg_val.Types.snd st1) st0
 598                 reg_vals
 599             in
 600             Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
 601               Types.snd = pc }))))
 602
 603 (** val rtl_pop_frame_unique :
 604     Registers.register List.list -> rTL_state -> (rTL_state,
 605     ByteValues.program_counter) Types.prod Errors.res **)
 606 let rtl_pop_frame_unique ret st =
 607   Obj.magic
 608     (Monad.m_bind0 (Monad.max_def Errors.res0)
 609       (Obj.magic
 610         (Errors.opt_to_res (List.Cons ((Errors.MSG
 611           ErrorMessages.FrameErrorOnPop), List.Nil))
 612           st.Joint_semantics.st_frms)) (fun frms ->
 613       match frms with
 614       | List.Nil ->
 615         Obj.magic (Errors.Error (List.Cons ((Errors.MSG
 616           ErrorMessages.EmptyStack), List.Nil)))
 617       | List.Cons (hd, tl) ->
 618         Monad.m_bind0 (Monad.max_def Errors.res0)
 619           (Obj.magic (rtl_read_result ret st)) (fun ret_vals ->
 620           let reg_vals = Util.zip_pottier hd.fr_ret_regs ret_vals in
 621           Monad.m_bind0 (Monad.max_def Errors.res0)
 622             (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
 623             let st0 =
 624               Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
 625                 (Joint_semantics.set_regs rTL_state_params
 626                   (Obj.magic hd.fr_regs)
 627                   (Joint_semantics.set_carry rTL_state_params hd.fr_carry st))
 628             in
 629             let pc = hd.fr_pc in
 630             let st1 =
 631               Util.foldl (fun st1 reg_val ->
 632                 rtl_reg_store reg_val.Types.fst reg_val.Types.snd st1) st0
 633                 reg_vals
 634             in
 635             Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
 636               Types.snd = pc }))))
 637
 638 (** val block_of_register_pair :
 639     Registers.register -> Registers.register -> rTL_state -> Pointers.block
 640     Errors.res **)
 641 let block_of_register_pair r1 r2 st =
 642   Obj.magic
 643     (Monad.m_bind0 (Monad.max_def Errors.res0)
 644       (Obj.magic (rtl_reg_retrieve st r1)) (fun v1 ->
 645       Monad.m_bind0 (Monad.max_def Errors.res0)
 646         (Obj.magic (rtl_reg_retrieve st r2)) (fun v2 ->
 647         Monad.m_bind0 (Monad.max_def Errors.res0)
 648           (Obj.magic
 649             (BEMem.pointer_of_address { Types.fst = v1; Types.snd = v2 }))
 650           (fun ptr -> Obj.magic (Errors.OK ptr.Pointers.pblock)))))
 651
 652 (** val eval_rtl_seq :
 653     RTL.rtl_seq -> AST.ident -> rTL_state -> rTL_state Errors.res **)
 654 let eval_rtl_seq stm curr_fn st =
 655   let RTL.Rtl_stack_address (dreg1, dreg2) = stm in
 656   Obj.magic
 657     (Monad.m_bind0 (Monad.max_def Errors.res0)
 658       (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
 659       let { Types.fst = dpl; Types.snd = dph } =
 660         ByteValues.beval_pair_of_pointer (Types.pi1 sp)
 661       in
 662       let st0 = rtl_reg_store dreg1 dpl st in
 663       Monad.m_return0 (Monad.max_def Errors.res0)
 664         (rtl_reg_store dreg2 dph st0)))
 665
 666 (** val reg_res_store :
 667     PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
 668     Errors.res **)
 669 let reg_res_store r v s =
 670   Errors.OK (reg_sp_store r v s)
 671
 672 (** val rTL_semantics_separate : SemanticsUtils.sem_graph_params **)
 673 let rTL_semantics_separate =
 674   { SemanticsUtils.sgp_pars =
 675     (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
 676     SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
 677     rTL_state_params; Joint_semantics.acca_store_ =
 678     (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
 679     (Obj.magic reg_sp_retrieve); Joint_semantics.acca_arg_retrieve_ =
 680     (Obj.magic rtl_arg_retrieve); Joint_semantics.accb_store_ =
 681     (Obj.magic reg_res_store); Joint_semantics.accb_retrieve_ =
 682     (Obj.magic reg_sp_retrieve); Joint_semantics.accb_arg_retrieve_ =
 683     (Obj.magic rtl_arg_retrieve); Joint_semantics.dpl_store_ =
 684     (Obj.magic reg_res_store); Joint_semantics.dpl_retrieve_ =
 685     (Obj.magic reg_sp_retrieve); Joint_semantics.dpl_arg_retrieve_ =
 686     (Obj.magic rtl_arg_retrieve); Joint_semantics.dph_store_ =
 687     (Obj.magic reg_res_store); Joint_semantics.dph_retrieve_ =
 688     (Obj.magic reg_sp_retrieve); Joint_semantics.dph_arg_retrieve_ =
 689     (Obj.magic rtl_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
 690     (Obj.magic rtl_arg_retrieve); Joint_semantics.pair_reg_move_ =
 691     (fun env p ->
 692     let { Types.fst = dest; Types.snd = src } = Obj.magic p in
 693     Obj.magic
 694       (Monad.m_bind0 (Monad.max_def Errors.res0)
 695         (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
 696         Monad.m_return0 (Monad.max_def Errors.res0)
 697           (reg_sp_store dest v (Obj.magic env)))));
 698     Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
 699     Joint_semantics.setup_call = (Obj.magic rtl_setup_call_separate);
 700     Joint_semantics.fetch_external_args =
 701     (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
 702     (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
 703     (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
 704     (Obj.magic (List.Cons (Positive.One, (List.Cons ((Positive.P0
 705       Positive.One), (List.Cons ((Positive.P1 Positive.One), (List.Cons
 706       ((Positive.P0 (Positive.P0 Positive.One)), List.Nil)))))))));
 707     Joint_semantics.read_result = (fun x x0 -> Obj.magic rtl_read_result);
 708     Joint_semantics.eval_ext_seq = (fun x x0 -> Obj.magic eval_rtl_seq);
 709     Joint_semantics.pop_frame = (fun x x0 x1 ->
 710     Obj.magic rtl_pop_frame_separate) });
 711     SemanticsUtils.graph_pre_main_generator = RTL.rTL_premain }
 712
 713 (** val rTL_semantics_separate_overflow : SemanticsUtils.sem_graph_params **)
 714 let rTL_semantics_separate_overflow =
 715   { SemanticsUtils.sgp_pars =
 716     (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
 717     SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
 718     rTL_state_params; Joint_semantics.acca_store_ =
 719     (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
 720     (Obj.magic reg_sp_retrieve); Joint_semantics.acca_arg_retrieve_ =
 721     (Obj.magic rtl_arg_retrieve); Joint_semantics.accb_store_ =
 722     (Obj.magic reg_res_store); Joint_semantics.accb_retrieve_ =
 723     (Obj.magic reg_sp_retrieve); Joint_semantics.accb_arg_retrieve_ =
 724     (Obj.magic rtl_arg_retrieve); Joint_semantics.dpl_store_ =
 725     (Obj.magic reg_res_store); Joint_semantics.dpl_retrieve_ =
 726     (Obj.magic reg_sp_retrieve); Joint_semantics.dpl_arg_retrieve_ =
 727     (Obj.magic rtl_arg_retrieve); Joint_semantics.dph_store_ =
 728     (Obj.magic reg_res_store); Joint_semantics.dph_retrieve_ =
 729     (Obj.magic reg_sp_retrieve); Joint_semantics.dph_arg_retrieve_ =
 730     (Obj.magic rtl_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
 731     (Obj.magic rtl_arg_retrieve); Joint_semantics.pair_reg_move_ =
 732     (fun env p ->
 733     let { Types.fst = dest; Types.snd = src } = Obj.magic p in
 734     Obj.magic
 735       (Monad.m_bind0 (Monad.max_def Errors.res0)
 736         (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
 737         Monad.m_return0 (Monad.max_def Errors.res0)
 738           (reg_sp_store dest v (Obj.magic env)))));
 739     Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
 740     Joint_semantics.setup_call =
 741     (Obj.magic rtl_setup_call_separate_overflow);
 742     Joint_semantics.fetch_external_args =
 743     (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
 744     (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
 745     (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
 746     (Obj.magic (List.Cons (Positive.One, (List.Cons ((Positive.P0
 747       Positive.One), (List.Cons ((Positive.P1 Positive.One), (List.Cons
 748       ((Positive.P0 (Positive.P0 Positive.One)), List.Nil)))))))));
 749     Joint_semantics.read_result = (fun x x0 -> Obj.magic rtl_read_result);
 750     Joint_semantics.eval_ext_seq = (fun x x0 -> Obj.magic eval_rtl_seq);
 751     Joint_semantics.pop_frame = (fun x x0 x1 ->
 752     Obj.magic rtl_pop_frame_separate) });
 753     SemanticsUtils.graph_pre_main_generator = RTL.rTL_premain }
 754
 755 (** val rTL_semantics_unique : SemanticsUtils.sem_graph_params **)
 756 let rTL_semantics_unique =
 757   { SemanticsUtils.sgp_pars =
 758     (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
 759     SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
 760     rTL_state_params; Joint_semantics.acca_store_ =
 761     (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
 762     (Obj.magic reg_sp_retrieve); Joint_semantics.acca_arg_retrieve_ =
 763     (Obj.magic rtl_arg_retrieve); Joint_semantics.accb_store_ =
 764     (Obj.magic reg_res_store); Joint_semantics.accb_retrieve_ =
 765     (Obj.magic reg_sp_retrieve); Joint_semantics.accb_arg_retrieve_ =
 766     (Obj.magic rtl_arg_retrieve); Joint_semantics.dpl_store_ =
 767     (Obj.magic reg_res_store); Joint_semantics.dpl_retrieve_ =
 768     (Obj.magic reg_sp_retrieve); Joint_semantics.dpl_arg_retrieve_ =
 769     (Obj.magic rtl_arg_retrieve); Joint_semantics.dph_store_ =
 770     (Obj.magic reg_res_store); Joint_semantics.dph_retrieve_ =
 771     (Obj.magic reg_sp_retrieve); Joint_semantics.dph_arg_retrieve_ =
 772     (Obj.magic rtl_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
 773     (Obj.magic rtl_arg_retrieve); Joint_semantics.pair_reg_move_ =
 774     (fun env p ->
 775     let { Types.fst = dest; Types.snd = src } = Obj.magic p in
 776     Obj.magic
 777       (Monad.m_bind0 (Monad.max_def Errors.res0)
 778         (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
 779         Monad.m_return0 (Monad.max_def Errors.res0)
 780           (reg_sp_store dest v (Obj.magic env)))));
 781     Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
 782     Joint_semantics.setup_call = (Obj.magic rtl_setup_call_unique);
 783     Joint_semantics.fetch_external_args =
 784     (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
 785     (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
 786     (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
 787     (Obj.magic (List.Cons (Positive.One, (List.Cons ((Positive.P0
 788       Positive.One), (List.Cons ((Positive.P1 Positive.One), (List.Cons
 789       ((Positive.P0 (Positive.P0 Positive.One)), List.Nil)))))))));
 790     Joint_semantics.read_result = (fun x x0 -> Obj.magic rtl_read_result);
 791     Joint_semantics.eval_ext_seq = (fun x x0 -> Obj.magic eval_rtl_seq);
 792     Joint_semantics.pop_frame = (fun x x0 x1 ->
 793     Obj.magic rtl_pop_frame_unique) });
 794     SemanticsUtils.graph_pre_main_generator = RTL.rTL_premain }
 795