Ignore:
Timestamp:
Mar 26, 2013, 4:51:40 PM (7 years ago)
Author:
sacerdot
Message:

New extraction, it diverges in RTL execution now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/semanticsUtils.ml

    r2951 r2960  
    168168    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    169169    -> hw_register_env -> 'a1 **)
    170 let rec hw_register_env_rect_Type4 h_mk_hw_register_env x_5847 =
    171   let { reg_env = reg_env0; other_bit = other_bit0 } = x_5847 in
     170let rec hw_register_env_rect_Type4 h_mk_hw_register_env x_432 =
     171  let { reg_env = reg_env0; other_bit = other_bit0 } = x_432 in
    172172  h_mk_hw_register_env reg_env0 other_bit0
    173173
     
    175175    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    176176    -> hw_register_env -> 'a1 **)
    177 let rec hw_register_env_rect_Type5 h_mk_hw_register_env x_5849 =
    178   let { reg_env = reg_env0; other_bit = other_bit0 } = x_5849 in
     177let rec hw_register_env_rect_Type5 h_mk_hw_register_env x_434 =
     178  let { reg_env = reg_env0; other_bit = other_bit0 } = x_434 in
    179179  h_mk_hw_register_env reg_env0 other_bit0
    180180
     
    182182    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    183183    -> hw_register_env -> 'a1 **)
    184 let rec hw_register_env_rect_Type3 h_mk_hw_register_env x_5851 =
    185   let { reg_env = reg_env0; other_bit = other_bit0 } = x_5851 in
     184let rec hw_register_env_rect_Type3 h_mk_hw_register_env x_436 =
     185  let { reg_env = reg_env0; other_bit = other_bit0 } = x_436 in
    186186  h_mk_hw_register_env reg_env0 other_bit0
    187187
     
    189189    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    190190    -> hw_register_env -> 'a1 **)
    191 let rec hw_register_env_rect_Type2 h_mk_hw_register_env x_5853 =
    192   let { reg_env = reg_env0; other_bit = other_bit0 } = x_5853 in
     191let rec hw_register_env_rect_Type2 h_mk_hw_register_env x_438 =
     192  let { reg_env = reg_env0; other_bit = other_bit0 } = x_438 in
    193193  h_mk_hw_register_env reg_env0 other_bit0
    194194
     
    196196    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    197197    -> hw_register_env -> 'a1 **)
    198 let rec hw_register_env_rect_Type1 h_mk_hw_register_env x_5855 =
    199   let { reg_env = reg_env0; other_bit = other_bit0 } = x_5855 in
     198let rec hw_register_env_rect_Type1 h_mk_hw_register_env x_440 =
     199  let { reg_env = reg_env0; other_bit = other_bit0 } = x_440 in
    200200  h_mk_hw_register_env reg_env0 other_bit0
    201201
     
    203203    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    204204    -> hw_register_env -> 'a1 **)
    205 let rec hw_register_env_rect_Type0 h_mk_hw_register_env x_5857 =
    206   let { reg_env = reg_env0; other_bit = other_bit0 } = x_5857 in
     205let rec hw_register_env_rect_Type0 h_mk_hw_register_env x_442 =
     206  let { reg_env = reg_env0; other_bit = other_bit0 } = x_442 in
    207207  h_mk_hw_register_env reg_env0 other_bit0
    208208
     
    319319    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    320320    -> sem_graph_params -> 'a1 **)
    321 let rec sem_graph_params_rect_Type4 h_mk_sem_graph_params x_5873 =
     321let rec sem_graph_params_rect_Type4 h_mk_sem_graph_params x_458 =
    322322  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    323     graph_pre_main_generator0 } = x_5873
     323    graph_pre_main_generator0 } = x_458
    324324  in
    325325  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    329329    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    330330    -> sem_graph_params -> 'a1 **)
    331 let rec sem_graph_params_rect_Type5 h_mk_sem_graph_params x_5875 =
     331let rec sem_graph_params_rect_Type5 h_mk_sem_graph_params x_460 =
    332332  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    333     graph_pre_main_generator0 } = x_5875
     333    graph_pre_main_generator0 } = x_460
    334334  in
    335335  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    339339    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    340340    -> sem_graph_params -> 'a1 **)
    341 let rec sem_graph_params_rect_Type3 h_mk_sem_graph_params x_5877 =
     341let rec sem_graph_params_rect_Type3 h_mk_sem_graph_params x_462 =
    342342  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    343     graph_pre_main_generator0 } = x_5877
     343    graph_pre_main_generator0 } = x_462
    344344  in
    345345  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    349349    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    350350    -> sem_graph_params -> 'a1 **)
    351 let rec sem_graph_params_rect_Type2 h_mk_sem_graph_params x_5879 =
     351let rec sem_graph_params_rect_Type2 h_mk_sem_graph_params x_464 =
    352352  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    353     graph_pre_main_generator0 } = x_5879
     353    graph_pre_main_generator0 } = x_464
    354354  in
    355355  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    359359    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    360360    -> sem_graph_params -> 'a1 **)
    361 let rec sem_graph_params_rect_Type1 h_mk_sem_graph_params x_5881 =
     361let rec sem_graph_params_rect_Type1 h_mk_sem_graph_params x_466 =
    362362  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    363     graph_pre_main_generator0 } = x_5881
     363    graph_pre_main_generator0 } = x_466
    364364  in
    365365  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    369369    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    370370    -> sem_graph_params -> 'a1 **)
    371 let rec sem_graph_params_rect_Type0 h_mk_sem_graph_params x_5883 =
     371let rec sem_graph_params_rect_Type0 h_mk_sem_graph_params x_468 =
    372372  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    373     graph_pre_main_generator0 } = x_5883
     373    graph_pre_main_generator0 } = x_468
    374374  in
    375375  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    501501    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    502502    -> sem_lin_params -> 'a1 **)
    503 let rec sem_lin_params_rect_Type4 h_mk_sem_lin_params x_5900 =
     503let rec sem_lin_params_rect_Type4 h_mk_sem_lin_params x_485 =
    504504  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    505     lin_pre_main_generator0 } = x_5900
     505    lin_pre_main_generator0 } = x_485
    506506  in
    507507  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
     
    511511    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    512512    -> sem_lin_params -> 'a1 **)
    513 let rec sem_lin_params_rect_Type5 h_mk_sem_lin_params x_5902 =
     513let rec sem_lin_params_rect_Type5 h_mk_sem_lin_params x_487 =
    514514  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    515     lin_pre_main_generator0 } = x_5902
     515    lin_pre_main_generator0 } = x_487
    516516  in
    517517  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
     
    521521    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    522522    -> sem_lin_params -> 'a1 **)
    523 let rec sem_lin_params_rect_Type3 h_mk_sem_lin_params x_5904 =
     523let rec sem_lin_params_rect_Type3 h_mk_sem_lin_params x_489 =
    524524  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    525     lin_pre_main_generator0 } = x_5904
     525    lin_pre_main_generator0 } = x_489
    526526  in
    527527  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
     
    531531    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    532532    -> sem_lin_params -> 'a1 **)
    533 let rec sem_lin_params_rect_Type2 h_mk_sem_lin_params x_5906 =
     533let rec sem_lin_params_rect_Type2 h_mk_sem_lin_params x_491 =
    534534  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    535     lin_pre_main_generator0 } = x_5906
     535    lin_pre_main_generator0 } = x_491
    536536  in
    537537  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
     
    541541    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    542542    -> sem_lin_params -> 'a1 **)
    543 let rec sem_lin_params_rect_Type1 h_mk_sem_lin_params x_5908 =
     543let rec sem_lin_params_rect_Type1 h_mk_sem_lin_params x_493 =
    544544  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    545     lin_pre_main_generator0 } = x_5908
     545    lin_pre_main_generator0 } = x_493
    546546  in
    547547  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
     
    551551    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    552552    -> sem_lin_params -> 'a1 **)
    553 let rec sem_lin_params_rect_Type0 h_mk_sem_lin_params x_5910 =
     553let rec sem_lin_params_rect_Type0 h_mk_sem_lin_params x_495 =
    554554  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    555     lin_pre_main_generator0 } = x_5910
     555    lin_pre_main_generator0 } = x_495
    556556  in
    557557  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
     
    669669    (sem_lin_params_to_sem_params x0)
    670670
    671 (** val pre_main_id : AST.ident **)
    672 let pre_main_id =
    673   Positive.One
    674 
    675 (** val joint_globalenv :
    676     Joint_semantics.sem_params -> Joint.joint_program ->
    677     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
    678 let joint_globalenv pars prog =
    679   let genv =
    680     Globalenvs.drop_fn pre_main_id
    681       (Globalenvs.globalenv (fun x -> x) prog.Joint.joint_prog)
    682   in
    683   { Globalenvs.functions =
    684   (PositiveMap.insert Positive.One (AST.Internal
    685     (pars.Joint_semantics.pre_main_generator prog))
    686     genv.Globalenvs.functions); Globalenvs.nextfunction =
    687   genv.Globalenvs.nextfunction; Globalenvs.symbols =
    688   (Identifiers.add PreIdentifiers.SymbolTag genv.Globalenvs.symbols
    689     pre_main_id (Z.zopp (Z.z_of_nat (Nat.S Nat.O)))) }
    690 
    691671(** val match_genv_t_rect_Type4 :
    692672    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
     
    767747  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
    768748
     749(** val joint_globalenv :
     750    Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
     751    Nat.nat Types.option) -> Joint_semantics.genv **)
     752let joint_globalenv p prog stacksizes =
     753  let genv = Globalenvs.globalenv (fun x -> x) prog.Joint.joint_prog in
     754  let pc_from_lbl = fun bl fn lbl ->
     755    Monad.m_bind0 (Monad.max_def Option.option)
     756      (Obj.magic
     757        ((Joint_semantics.spp'__o__spp p).Joint.point_of_label
     758          (AST.prog_var_names prog.Joint.joint_prog)
     759          (Types.pi1 fn).Joint.joint_if_code lbl)) (fun pt ->
     760      Monad.m_return0 (Monad.max_def Option.option) { ByteValues.pc_block =
     761        bl; ByteValues.pc_offset =
     762        (p.Joint_semantics.spp'.Joint_semantics.offset_of_point pt) })
     763  in
     764  { Joint_semantics.ge = genv; Joint_semantics.stack_sizes = stacksizes;
     765  Joint_semantics.premain = (p.Joint_semantics.pre_main_generator prog);
     766  Joint_semantics.pc_from_label = (Obj.magic pc_from_lbl) }
     767
Note: See TracChangeset for help on using the changeset viewer.