Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTL_semantics.ml

    r2933 r2951  
    150150
    151151open RTL
     152
     153type 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 **)
     159let rec reg_sp_rect_Type4 h_mk_reg_sp x_6032 =
     160  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6032 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 **)
     166let rec reg_sp_rect_Type5 h_mk_reg_sp x_6034 =
     167  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6034 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 **)
     173let rec reg_sp_rect_Type3 h_mk_reg_sp x_6036 =
     174  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6036 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 **)
     180let rec reg_sp_rect_Type2 h_mk_reg_sp x_6038 =
     181  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6038 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 **)
     187let rec reg_sp_rect_Type1 h_mk_reg_sp x_6040 =
     188  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6040 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 **)
     194let rec reg_sp_rect_Type0 h_mk_reg_sp x_6042 =
     195  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6042 in
     196  h_mk_reg_sp reg_sp_env0 stackp0
     197
     198(** val reg_sp_env :
     199    reg_sp -> ByteValues.beval Identifiers.identifier_map **)
     200let rec reg_sp_env xxx =
     201  xxx.reg_sp_env
     202
     203(** val stackp : reg_sp -> ByteValues.xpointer **)
     204let 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 **)
     210let 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 **)
     216let 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 **)
     222let 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 **)
     228let 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 **)
     234let 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 -> __ **)
     238let 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 -> __ **)
     244let 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 **)
     252let 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 **)
     258let 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 **)
     263let 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 **)
     268let 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 **)
     273let 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 **)
     278let 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 **)
     284let reg_sp_retrieve locals =
     285  SemanticsUtils.reg_retrieve locals.reg_sp_env
     286
     287(** val reg_sp_empty : ByteValues.xpointer -> reg_sp **)
     288let reg_sp_empty x =
     289  { reg_sp_env = (Identifiers.empty_map PreIdentifiers.RegisterTag); stackp =
     290    x }
    152291
    153292type frame = { fr_ret_regs : Registers.register List.list;
    154293               fr_pc : ByteValues.program_counter;
    155                fr_carry : ByteValues.bebit; fr_regs : SemanticsUtils.reg_sp }
     294               fr_carry : ByteValues.bebit; fr_regs : reg_sp }
    156295
    157296(** val frame_rect_Type4 :
    158297    (Registers.register List.list -> ByteValues.program_counter ->
    159     ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
    160 let rec frame_rect_Type4 h_mk_frame x_26392 =
     298    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
     299let rec frame_rect_Type4 h_mk_frame x_6058 =
    161300  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    162     fr_regs = fr_regs0 } = x_26392
     301    fr_regs = fr_regs0 } = x_6058
    163302  in
    164303  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    166305(** val frame_rect_Type5 :
    167306    (Registers.register List.list -> ByteValues.program_counter ->
    168     ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
    169 let rec frame_rect_Type5 h_mk_frame x_26394 =
     307    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
     308let rec frame_rect_Type5 h_mk_frame x_6060 =
    170309  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    171     fr_regs = fr_regs0 } = x_26394
     310    fr_regs = fr_regs0 } = x_6060
    172311  in
    173312  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    175314(** val frame_rect_Type3 :
    176315    (Registers.register List.list -> ByteValues.program_counter ->
    177     ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
    178 let rec frame_rect_Type3 h_mk_frame x_26396 =
     316    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
     317let rec frame_rect_Type3 h_mk_frame x_6062 =
    179318  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    180     fr_regs = fr_regs0 } = x_26396
     319    fr_regs = fr_regs0 } = x_6062
    181320  in
    182321  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    184323(** val frame_rect_Type2 :
    185324    (Registers.register List.list -> ByteValues.program_counter ->
    186     ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
    187 let rec frame_rect_Type2 h_mk_frame x_26398 =
     325    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
     326let rec frame_rect_Type2 h_mk_frame x_6064 =
    188327  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    189     fr_regs = fr_regs0 } = x_26398
     328    fr_regs = fr_regs0 } = x_6064
    190329  in
    191330  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    193332(** val frame_rect_Type1 :
    194333    (Registers.register List.list -> ByteValues.program_counter ->
    195     ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
    196 let rec frame_rect_Type1 h_mk_frame x_26400 =
     334    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
     335let rec frame_rect_Type1 h_mk_frame x_6066 =
    197336  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    198     fr_regs = fr_regs0 } = x_26400
     337    fr_regs = fr_regs0 } = x_6066
    199338  in
    200339  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    202341(** val frame_rect_Type0 :
    203342    (Registers.register List.list -> ByteValues.program_counter ->
    204     ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
    205 let rec frame_rect_Type0 h_mk_frame x_26402 =
     343    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
     344let rec frame_rect_Type0 h_mk_frame x_6068 =
    206345  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    207     fr_regs = fr_regs0 } = x_26402
     346    fr_regs = fr_regs0 } = x_6068
    208347  in
    209348  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    221360  xxx.fr_carry
    222361
    223 (** val fr_regs : frame -> SemanticsUtils.reg_sp **)
     362(** val fr_regs : frame -> reg_sp **)
    224363let rec fr_regs xxx =
    225364  xxx.fr_regs
     
    227366(** val frame_inv_rect_Type4 :
    228367    frame -> (Registers.register List.list -> ByteValues.program_counter ->
    229     ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1 **)
     368    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
    230369let frame_inv_rect_Type4 hterm h1 =
    231370  let hcut = frame_rect_Type4 h1 hterm in hcut __
     
    233372(** val frame_inv_rect_Type3 :
    234373    frame -> (Registers.register List.list -> ByteValues.program_counter ->
    235     ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1 **)
     374    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
    236375let frame_inv_rect_Type3 hterm h1 =
    237376  let hcut = frame_rect_Type3 h1 hterm in hcut __
     
    239378(** val frame_inv_rect_Type2 :
    240379    frame -> (Registers.register List.list -> ByteValues.program_counter ->
    241     ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1 **)
     380    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
    242381let frame_inv_rect_Type2 hterm h1 =
    243382  let hcut = frame_rect_Type2 h1 hterm in hcut __
     
    245384(** val frame_inv_rect_Type1 :
    246385    frame -> (Registers.register List.list -> ByteValues.program_counter ->
    247     ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1 **)
     386    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
    248387let frame_inv_rect_Type1 hterm h1 =
    249388  let hcut = frame_rect_Type1 h1 hterm in hcut __
     
    251390(** val frame_inv_rect_Type0 :
    252391    frame -> (Registers.register List.list -> ByteValues.program_counter ->
    253     ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1 **)
     392    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
    254393let frame_inv_rect_Type0 hterm h1 =
    255394  let hcut = frame_rect_Type0 h1 hterm in hcut __
     
    270409let rTL_state_params =
    271410  { Joint_semantics.empty_framesT = (Obj.magic List.Nil);
    272     Joint_semantics.empty_regsT = (Obj.magic SemanticsUtils.reg_sp_init);
    273     Joint_semantics.load_sp = (fun env -> Errors.OK
    274     (Obj.magic env).SemanticsUtils.stackp); Joint_semantics.save_sp =
    275     (fun env ->
    276     Obj.magic (fun x -> { SemanticsUtils.reg_sp_env =
    277       (Obj.magic env).SemanticsUtils.reg_sp_env; SemanticsUtils.stackp = x })) }
     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 })) }
    278416
    279417type rTL_state = Joint_semantics.state
    280418
    281419(** val rtl_arg_retrieve :
    282     SemanticsUtils.reg_sp -> Joint.psd_argument -> ByteValues.beval
    283     Errors.res **)
     420    reg_sp -> Joint.psd_argument -> ByteValues.beval Errors.res **)
    284421let rtl_arg_retrieve env = function
    285 | Joint.Reg r -> SemanticsUtils.reg_retrieve env.SemanticsUtils.reg_sp_env r
     422| Joint.Reg r -> SemanticsUtils.reg_retrieve env.reg_sp_env r
    286423| Joint.Imm b -> Errors.OK (ByteValues.BVByte b)
    287424
     
    303440        Obj.magic (Errors.OK { Types.fst = st; Types.snd = hd.fr_pc })))
    304441
    305 (** val rtl_init_local :
    306     Registers.register -> SemanticsUtils.reg_sp -> SemanticsUtils.reg_sp **)
     442(** val rtl_init_local : Registers.register -> reg_sp -> reg_sp **)
    307443let rtl_init_local local =
    308   SemanticsUtils.reg_sp_store local ByteValues.BVundef
     444  reg_sp_store local ByteValues.BVundef
    309445
    310446(** val rtl_setup_call_separate :
     
    328464              (Obj.magic
    329465                (rtl_arg_retrieve (Obj.magic st.Joint_semantics.regs) src))
    330               (fun v ->
    331               Obj.magic (Errors.OK (SemanticsUtils.reg_sp_store dest v lenv)))))
    332           (Errors.OK (SemanticsUtils.reg_sp_init sp)) formal_arg_regs
    333           actual_arg_regs)) (fun new_regs ->
     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 ->
    334469      Obj.magic (Errors.OK
    335470        (Joint_semantics.set_regs rTL_state_params new_regs
    336471          (Joint_semantics.set_m rTL_state_params mem st))))))) __
     472
     473(** val stackOverflow : ErrorMessages.errorMessage **)
     474let stackOverflow = ErrorMessages.MISSING
     475
     476(** val rtl_setup_call_separate_overflow :
     477    Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
     478    -> rTL_state -> rTL_state Errors.res **)
     479let rtl_setup_call_separate_overflow stacksize formal_arg_regs actual_arg_regs st =
     480  match Nat.leb (Nat.S (Nat.plus stacksize st.Joint_semantics.stack_usage))
     481          (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     482            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     483            (Nat.S (Nat.S Nat.O))))))))))))))))) with
     484  | Bool.True ->
     485    rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st
     486  | Bool.False ->
     487    Errors.Error (List.Cons ((Errors.MSG stackOverflow), List.Nil))
    337488
    338489(** val rtl_setup_call_unique :
     
    356507                (Obj.magic
    357508                  (rtl_arg_retrieve (Obj.magic st.Joint_semantics.regs) src))
    358                 (fun v ->
    359                 Obj.magic (Errors.OK
    360                   (SemanticsUtils.reg_sp_store dest v lenv))))) (Errors.OK
    361             (SemanticsUtils.reg_sp_init newsp)) formal_arg_regs
    362             actual_arg_regs)) (fun new_regs ->
     509                (fun v -> Obj.magic (Errors.OK (reg_sp_store dest v lenv)))))
     510            (Errors.OK (reg_sp_empty newsp)) formal_arg_regs actual_arg_regs))
     511        (fun new_regs ->
    363512        Obj.magic (Errors.OK
    364513          (Joint_semantics.set_regs rTL_state_params new_regs st)))))
     
    386535    AST.external_function -> rTL_state -> Joint.psd_argument List.list ->
    387536    Values.val0 List.list Errors.res **)
    388 let rtl_fetch_external_args _ =
    389   failwith "AXIOM TO BE REALIZED"
     537let rtl_fetch_external_args _ = assert false
    390538
    391539(** val rtl_set_result :
    392540    Values.val0 List.list -> Registers.register List.list -> rTL_state ->
    393541    rTL_state Errors.res **)
    394 let rtl_set_result _ =
    395   failwith "AXIOM TO BE REALIZED"
     542let rtl_set_result _ = assert false
    396543
    397544(** val rtl_reg_store :
     
    399546    Joint_semantics.state **)
    400547let rtl_reg_store r v st =
    401   let mem =
    402     SemanticsUtils.reg_sp_store r v (Obj.magic st.Joint_semantics.regs)
    403   in
     548  let mem = reg_sp_store r v (Obj.magic st.Joint_semantics.regs) in
    404549  Joint_semantics.set_regs rTL_state_params (Obj.magic mem) st
    405550
     
    408553    Errors.res **)
    409554let rtl_reg_retrieve st l =
    410   SemanticsUtils.reg_sp_retrieve (Obj.magic st.Joint_semantics.regs) l
     555  reg_sp_retrieve (Obj.magic st.Joint_semantics.regs) l
    411556
    412557(** val rtl_read_result :
     
    438583          Monad.m_bind0 (Monad.max_def Errors.res0)
    439584            (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
    440             let st1 =
     585            let st0 =
    441586              Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
    442587                (Joint_semantics.set_regs rTL_state_params
     
    448593            in
    449594            let pc = hd.fr_pc in
    450           let st1 =
    451             Util.foldl (fun st0 reg_val ->
    452 prerr_endline ("SALVO IL REGISTRO: r_" ^ string_of_int (Glue.int_of_matitapos reg_val.Types.fst));
    453               rtl_reg_store reg_val.Types.fst reg_val.Types.snd st0) st1
    454               reg_vals
    455           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
    456600            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
    457601              Types.snd = pc }))))
     
    475619          (Obj.magic (rtl_read_result ret st)) (fun ret_vals ->
    476620          let reg_vals = Util.zip_pottier hd.fr_ret_regs ret_vals in
    477           let st0 =
    478             Util.foldl (fun st0 reg_val ->
    479               rtl_reg_store reg_val.Types.fst reg_val.Types.snd st0) st
    480               reg_vals
    481           in
    482621          Monad.m_bind0 (Monad.max_def Errors.res0)
    483             (Obj.magic (Joint_semantics.sp rTL_state_params st0)) (fun sp ->
    484             let st1 =
     622            (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
     623            let st0 =
    485624              Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
    486625                (Joint_semantics.set_regs rTL_state_params
    487626                  (Obj.magic hd.fr_regs)
    488                   (Joint_semantics.set_carry rTL_state_params hd.fr_carry
    489                     st0))
     627                  (Joint_semantics.set_carry rTL_state_params hd.fr_carry st))
    490628            in
    491629            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
    492635            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
    493636              Types.snd = pc }))))
     
    522665
    523666(** val reg_res_store :
    524     PreIdentifiers.identifier -> ByteValues.beval -> SemanticsUtils.reg_sp ->
    525     SemanticsUtils.reg_sp Errors.res **)
     667    PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
     668    Errors.res **)
    526669let reg_res_store r v s =
    527   Errors.OK (SemanticsUtils.reg_sp_store r v s)
     670  Errors.OK (reg_sp_store r v s)
    528671
    529672(** val rTL_semantics_separate : SemanticsUtils.sem_graph_params **)
     
    534677    rTL_state_params; Joint_semantics.acca_store_ =
    535678    (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
    536     (Obj.magic SemanticsUtils.reg_sp_retrieve);
    537     Joint_semantics.acca_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
    538     Joint_semantics.accb_store_ = (Obj.magic reg_res_store);
    539     Joint_semantics.accb_retrieve_ =
    540     (Obj.magic SemanticsUtils.reg_sp_retrieve);
    541     Joint_semantics.accb_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
    542     Joint_semantics.dpl_store_ = (Obj.magic reg_res_store);
    543     Joint_semantics.dpl_retrieve_ =
    544     (Obj.magic SemanticsUtils.reg_sp_retrieve);
    545     Joint_semantics.dpl_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
    546     Joint_semantics.dph_store_ = (Obj.magic reg_res_store);
    547     Joint_semantics.dph_retrieve_ =
    548     (Obj.magic SemanticsUtils.reg_sp_retrieve);
    549     Joint_semantics.dph_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
    550     Joint_semantics.snd_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
    551     Joint_semantics.pair_reg_move_ = (fun env p ->
     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 ->
    552692    let { Types.fst = dest; Types.snd = src } = Obj.magic p in
    553693    Obj.magic
     
    555695        (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
    556696        Monad.m_return0 (Monad.max_def Errors.res0)
    557           (SemanticsUtils.reg_sp_store dest v (Obj.magic env)))));
     697          (reg_sp_store dest v (Obj.magic env)))));
    558698    Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
    559699    Joint_semantics.setup_call = (Obj.magic rtl_setup_call_separate);
     
    562702    (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
    563703    (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
    564     (Obj.magic List.Nil); Joint_semantics.read_result = (fun x x0 ->
    565     Obj.magic rtl_read_result); Joint_semantics.eval_ext_seq = (fun x x0 ->
    566     Obj.magic eval_rtl_seq); Joint_semantics.pop_frame = (fun x x0 x1 ->
    567     Obj.magic rtl_pop_frame_separate) }) }
     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 **)
     714let 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 }
    568754
    569755(** val rTL_semantics_unique : SemanticsUtils.sem_graph_params **)
     
    574760    rTL_state_params; Joint_semantics.acca_store_ =
    575761    (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
    576     (Obj.magic SemanticsUtils.reg_sp_retrieve);
    577     Joint_semantics.acca_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
    578     Joint_semantics.accb_store_ = (Obj.magic reg_res_store);
    579     Joint_semantics.accb_retrieve_ =
    580     (Obj.magic SemanticsUtils.reg_sp_retrieve);
    581     Joint_semantics.accb_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
    582     Joint_semantics.dpl_store_ = (Obj.magic reg_res_store);
    583     Joint_semantics.dpl_retrieve_ =
    584     (Obj.magic SemanticsUtils.reg_sp_retrieve);
    585     Joint_semantics.dpl_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
    586     Joint_semantics.dph_store_ = (Obj.magic reg_res_store);
    587     Joint_semantics.dph_retrieve_ =
    588     (Obj.magic SemanticsUtils.reg_sp_retrieve);
    589     Joint_semantics.dph_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
    590     Joint_semantics.snd_arg_retrieve_ = (Obj.magic rtl_arg_retrieve);
    591     Joint_semantics.pair_reg_move_ = (fun env p ->
     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 ->
    592775    let { Types.fst = dest; Types.snd = src } = Obj.magic p in
    593776    Obj.magic
     
    595778        (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
    596779        Monad.m_return0 (Monad.max_def Errors.res0)
    597           (SemanticsUtils.reg_sp_store dest v (Obj.magic env)))));
     780          (reg_sp_store dest v (Obj.magic env)))));
    598781    Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
    599782    Joint_semantics.setup_call = (Obj.magic rtl_setup_call_unique);
     
    602785    (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
    603786    (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
    604     (Obj.magic List.Nil); Joint_semantics.read_result = (fun x x0 ->
    605     Obj.magic rtl_read_result); Joint_semantics.eval_ext_seq = (fun x x0 ->
    606     Obj.magic eval_rtl_seq); Joint_semantics.pop_frame = (fun x x0 x1 ->
    607     Obj.magic rtl_pop_frame_unique) }) }
    608 
     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
Note: See TracChangeset for help on using the changeset viewer.