Changeset 3029


Ignore:
Timestamp:
Mar 29, 2013, 9:47:49 AM (4 years ago)
Author:
sacerdot
Message:

New extraction after DPH/DPL bug fixing.

Location:
extracted
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • extracted/aSMCosts.ml

    r2999 r3029  
    127127      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    128128      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    129       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    130       Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
     129      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     130      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     131      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     132      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     133      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     134      (Nat.S (Nat.S (Nat.S (Nat.S
     135      Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
    131136    (List.Cons ((ASM.DIRECT
    132137    (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    139144      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    140145      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    141       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    142       Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
     146      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     147      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     148      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     149      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     150      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     151      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     152      Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
    143153    (List.Cons ((ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)),
    144154    Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
     
    492502   | Nat.S program_size' ->
    493503     (fun _ ->
    494        (let { Types.fst = eta24755; Types.snd = ticks } =
     504       (let { Types.fst = eta83; Types.snd = ticks } =
    495505          Fetch.fetch prog.ASM.cm program_counter'
    496506        in
    497        let { Types.fst = instruction; Types.snd = program_counter'' } =
    498          eta24755
     507       let { Types.fst = instruction; Types.snd = program_counter'' } = eta83
    499508       in
    500509       (fun _ ->
  • extracted/lINToASM.ml

    r3023 r3029  
    143143    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    144144    -> 'a1 **)
    145 let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_263 =
     145let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_3 =
    146146  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    147147    ident_map0; label_map = label_map0; address_map = address_map0;
    148     fresh_cost_label = fresh_cost_label0 } = x_263
     148    fresh_cost_label = fresh_cost_label0 } = x_3
    149149  in
    150150  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    157157    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    158158    -> 'a1 **)
    159 let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_265 =
     159let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_5 =
    160160  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    161161    ident_map0; label_map = label_map0; address_map = address_map0;
    162     fresh_cost_label = fresh_cost_label0 } = x_265
     162    fresh_cost_label = fresh_cost_label0 } = x_5
    163163  in
    164164  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    171171    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    172172    -> 'a1 **)
    173 let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_267 =
     173let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_7 =
    174174  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    175175    ident_map0; label_map = label_map0; address_map = address_map0;
    176     fresh_cost_label = fresh_cost_label0 } = x_267
     176    fresh_cost_label = fresh_cost_label0 } = x_7
    177177  in
    178178  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    185185    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    186186    -> 'a1 **)
    187 let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_269 =
     187let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_9 =
    188188  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    189189    ident_map0; label_map = label_map0; address_map = address_map0;
    190     fresh_cost_label = fresh_cost_label0 } = x_269
     190    fresh_cost_label = fresh_cost_label0 } = x_9
    191191  in
    192192  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    199199    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    200200    -> 'a1 **)
    201 let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_271 =
     201let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_11 =
    202202  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    203203    ident_map0; label_map = label_map0; address_map = address_map0;
    204     fresh_cost_label = fresh_cost_label0 } = x_271
     204    fresh_cost_label = fresh_cost_label0 } = x_11
    205205  in
    206206  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    213213    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    214214    -> 'a1 **)
    215 let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_273 =
     215let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_13 =
    216216  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    217217    ident_map0; label_map = label_map0; address_map = address_map0;
    218     fresh_cost_label = fresh_cost_label0 } = x_273
     218    fresh_cost_label = fresh_cost_label0 } = x_13
    219219  in
    220220  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    320320  let globals_addr_internal = fun res_offset x_size ->
    321321    let { Types.fst = res; Types.snd = offset } = res_offset in
    322     let { Types.fst = eta11; Types.snd = data } = x_size in
    323     let { Types.fst = x; Types.snd = region } = eta11 in
     322    let { Types.fst = eta6; Types.snd = data } = x_size in
     323    let { Types.fst = x; Types.snd = region } = eta6 in
    324324    { Types.fst =
    325325    (Identifiers.add PreIdentifiers.SymbolTag res x
     
    352352        (Identifiers.empty_map PreIdentifiers.LabelTag)
    353353    in
    354     let { Types.fst = eta12; Types.snd = lmap0 } =
     354    let { Types.fst = eta7; Types.snd = lmap0 } =
    355355      match Identifiers.lookup PreIdentifiers.LabelTag lmap l with
    356356      | Types.None ->
     
    364364          lmap }
    365365    in
    366     let { Types.fst = id; Types.snd = univ } = eta12 in
     366    let { Types.fst = id; Types.snd = univ } = eta7 in
    367367    { Types.fst = { id_univ = univ; current_funct = current; ident_map =
    368368    u.ident_map; label_map =
     
    377377  Obj.magic (fun u ->
    378378    let imap = u.ident_map in
    379     let { Types.fst = eta13; Types.snd = imap0 } =
     379    let { Types.fst = eta8; Types.snd = imap0 } =
    380380      match Identifiers.lookup PreIdentifiers.SymbolTag imap i with
    381381      | Types.None ->
     
    389389          imap }
    390390    in
    391     let { Types.fst = id; Types.snd = univ } = eta13 in
     391    let { Types.fst = id; Types.snd = univ } = eta8 in
    392392    { Types.fst = { id_univ = univ; current_funct = u.current_funct;
    393393    ident_map = imap0; label_map = u.label_map; address_map = u.address_map;
     
    597597         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    598598         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    599          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    600          Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
     599         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     600         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     601         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     602         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     603         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     604         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     605         Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
    601606   | I8051.RegisterDPH ->
    602607     (fun _ -> ASM.DIRECT
     
    611616         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    612617         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    613          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    614          Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
     618         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     619         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     620         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     621         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     622         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     623         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     624         Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
    615625   | I8051.RegisterCarry ->
    616626     (fun _ -> ASM.DIRECT
     
    10081018       (identifier_of_label globals lbl) (fun lbl' ->
    10091019       Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Jmp
    1010          (ASM.toASM_ident PreIdentifiers.LabelTag lbl')))
     1020         (ASM.toASM_ident PreIdentifiers.ASMTag lbl')))
    10111021   | Joint.RETURN ->
    10121022     Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
     
    10781088    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    10791089    -> 'a1 **)
    1080 let rec init_mutable_rect_Type4 h_mk_init_mutable x_290 =
     1090let rec init_mutable_rect_Type4 h_mk_init_mutable x_30 =
    10811091  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1082     built0 } = x_290
     1092    built0 } = x_30
    10831093  in
    10841094  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
     
    10871097    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    10881098    -> 'a1 **)
    1089 let rec init_mutable_rect_Type5 h_mk_init_mutable x_292 =
     1099let rec init_mutable_rect_Type5 h_mk_init_mutable x_32 =
    10901100  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1091     built0 } = x_292
     1101    built0 } = x_32
    10921102  in
    10931103  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
     
    10961106    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    10971107    -> 'a1 **)
    1098 let rec init_mutable_rect_Type3 h_mk_init_mutable x_294 =
     1108let rec init_mutable_rect_Type3 h_mk_init_mutable x_34 =
    10991109  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1100     built0 } = x_294
     1110    built0 } = x_34
    11011111  in
    11021112  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
     
    11051115    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    11061116    -> 'a1 **)
    1107 let rec init_mutable_rect_Type2 h_mk_init_mutable x_296 =
     1117let rec init_mutable_rect_Type2 h_mk_init_mutable x_36 =
    11081118  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1109     built0 } = x_296
     1119    built0 } = x_36
    11101120  in
    11111121  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
     
    11141124    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    11151125    -> 'a1 **)
    1116 let rec init_mutable_rect_Type1 h_mk_init_mutable x_298 =
     1126let rec init_mutable_rect_Type1 h_mk_init_mutable x_38 =
    11171127  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1118     built0 } = x_298
     1128    built0 } = x_38
    11191129  in
    11201130  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
     
    11231133    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    11241134    -> 'a1 **)
    1125 let rec init_mutable_rect_Type0 h_mk_init_mutable x_300 =
     1135let rec init_mutable_rect_Type0 h_mk_init_mutable x_40 =
    11261136  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1127     built0 } = x_300
     1137    built0 } = x_40
    11281138  in
    11291139  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
Note: See TracChangeset for help on using the changeset viewer.