Changeset 2999


Ignore:
Timestamp:
Mar 28, 2013, 12:47:55 PM (4 years ago)
Author:
sacerdot
Message:

code_memory added to labelled_object_code to avoid recomputing it every time.
This gives a major speed up in the semantics of the extracted code.

Files:
21 edited

Legend:

Unmodified
Added
Removed
  • driver/ASMPrinter.ml

    r2778 r2999  
    33
    44let print_program p =
    5   let code_memory = Extracted.Fetch.load_code_memory p in
    6   let intel_hex = IntelHex.pack_exported_code_memory 16 65535 code_memory in
     5  let intel_hex =
     6   IntelHex.pack_exported_code_memory 16 65535 p.Extracted.ASM.cm in
    77  IntelHex.string_of_intel_hex_format intel_hex
  • driver/ASMPrinter.mli

    r2778 r2999  
    22(** This module provides a function to print [ASM] programs. *)
    33
    4 val print_program : Extracted.ASM.object_code -> string
     4val print_program : Extracted.ASM.labelled_object_code -> string
  • driver/cerco.ml

    r2993 r2999  
    3434
    3535let argv1 = Sys.argv.(1) in
    36 let do_exec,filename,style =
     36let do_exec,filename =
    3737 if argv1 = "-exec" then
    38   true,Sys.argv.(2),(try Sys.argv.(3) with _ -> "instrumented")
     38  true,Sys.argv.(2)
    3939 else
    40   false,argv1,(try Sys.argv.(2) with _ -> "instrumented") in
     40  false,argv1 in
    4141let cl = ClightParser.process filename in
    4242let observe =
    4343 let rec infinity = Extracted.Nat.S infinity in
    4444 (fun pass prog ->
    45    if do_exec || pass = Extracted.Compiler.Clight_label_pass ||
    46       pass = Extracted.Compiler.Object_code_pass then
     45   if do_exec || pass = Extracted.Compiler.Object_code_pass then
    4746    Printer.print_program filename pass prog;
    4847   if do_exec then
     
    6766let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
    6867let s_costmap = output.Extracted.Compiler.c_stack_cost in
    69 let style =
    70   match style with
    71   | "plain" -> Cost_plain
    72   | "numbered" -> Cost_numbered (l_costmap,s_costmap)
    73   | "instrumented" -> Cost_instrumented (l_costmap,s_costmap)
    74   | x -> failwith ("I have no idea what " ^ x ^ " means")
    75 in
    76 print_endline (ClightPrinter.print_program style labelled);
    77 print_newline (); flush stdout;
    78 print_endline (ASMPrinter.print_program (Extracted.ASM.oc (Extracted.Compiler.c_labelled_object_code output)));
     68let style = Cost_instrumented (l_costmap,s_costmap) in
     69let instrumented = ClightPrinter.print_program style labelled in
     70let filename = Filename.chop_extension filename ^ "-instrumented.c" in
     71let och = open_out filename in
     72output_string och instrumented;
     73close_out och
  • driver/printer.ml

    r2993 r2999  
    266266       (Extracted.LIN_printer.print_LIN_program joint_LTL_LIN_printing_params)
    267267   | Extracted.Compiler.Object_code_pass ->
    268       ASMPrinter.print_program (Extracted.ASM.oc (Obj.magic program))
     268      ASMPrinter.print_program (Obj.magic program)
    269269   | _ -> ""
    270270 in
  • extracted/aSM.ml

    r2997 r2999  
    113113    -> 'a1) -> addressing_mode -> 'a1 **)
    114114let rec addressing_mode_rect_Type4 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    115 | DIRECT x_1001 -> h_DIRECT x_1001
    116 | INDIRECT x_1002 -> h_INDIRECT x_1002
    117 | EXT_INDIRECT x_1003 -> h_EXT_INDIRECT x_1003
    118 | REGISTER x_1004 -> h_REGISTER x_1004
     115| DIRECT x_33 -> h_DIRECT x_33
     116| INDIRECT x_34 -> h_INDIRECT x_34
     117| EXT_INDIRECT x_35 -> h_EXT_INDIRECT x_35
     118| REGISTER x_36 -> h_REGISTER x_36
    119119| ACC_A -> h_ACC_A
    120120| ACC_B -> h_ACC_B
    121121| DPTR -> h_DPTR
    122 | DATA x_1005 -> h_DATA x_1005
    123 | DATA16 x_1006 -> h_DATA16 x_1006
     122| DATA x_37 -> h_DATA x_37
     123| DATA16 x_38 -> h_DATA16 x_38
    124124| ACC_DPTR -> h_ACC_DPTR
    125125| ACC_PC -> h_ACC_PC
     
    127127| INDIRECT_DPTR -> h_INDIRECT_DPTR
    128128| CARRY -> h_CARRY
    129 | BIT_ADDR x_1007 -> h_BIT_ADDR x_1007
    130 | N_BIT_ADDR x_1008 -> h_N_BIT_ADDR x_1008
    131 | RELATIVE x_1009 -> h_RELATIVE x_1009
    132 | ADDR11 x_1010 -> h_ADDR11 x_1010
    133 | ADDR16 x_1011 -> h_ADDR16 x_1011
     129| BIT_ADDR x_39 -> h_BIT_ADDR x_39
     130| N_BIT_ADDR x_40 -> h_N_BIT_ADDR x_40
     131| RELATIVE x_41 -> h_RELATIVE x_41
     132| ADDR11 x_42 -> h_ADDR11 x_42
     133| ADDR16 x_43 -> h_ADDR16 x_43
    134134
    135135(** val addressing_mode_rect_Type5 :
     
    141141    -> 'a1) -> addressing_mode -> 'a1 **)
    142142let rec addressing_mode_rect_Type5 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    143 | DIRECT x_1032 -> h_DIRECT x_1032
    144 | INDIRECT x_1033 -> h_INDIRECT x_1033
    145 | EXT_INDIRECT x_1034 -> h_EXT_INDIRECT x_1034
    146 | REGISTER x_1035 -> h_REGISTER x_1035
     143| DIRECT x_64 -> h_DIRECT x_64
     144| INDIRECT x_65 -> h_INDIRECT x_65
     145| EXT_INDIRECT x_66 -> h_EXT_INDIRECT x_66
     146| REGISTER x_67 -> h_REGISTER x_67
    147147| ACC_A -> h_ACC_A
    148148| ACC_B -> h_ACC_B
    149149| DPTR -> h_DPTR
    150 | DATA x_1036 -> h_DATA x_1036
    151 | DATA16 x_1037 -> h_DATA16 x_1037
     150| DATA x_68 -> h_DATA x_68
     151| DATA16 x_69 -> h_DATA16 x_69
    152152| ACC_DPTR -> h_ACC_DPTR
    153153| ACC_PC -> h_ACC_PC
     
    155155| INDIRECT_DPTR -> h_INDIRECT_DPTR
    156156| CARRY -> h_CARRY
    157 | BIT_ADDR x_1038 -> h_BIT_ADDR x_1038
    158 | N_BIT_ADDR x_1039 -> h_N_BIT_ADDR x_1039
    159 | RELATIVE x_1040 -> h_RELATIVE x_1040
    160 | ADDR11 x_1041 -> h_ADDR11 x_1041
    161 | ADDR16 x_1042 -> h_ADDR16 x_1042
     157| BIT_ADDR x_70 -> h_BIT_ADDR x_70
     158| N_BIT_ADDR x_71 -> h_N_BIT_ADDR x_71
     159| RELATIVE x_72 -> h_RELATIVE x_72
     160| ADDR11 x_73 -> h_ADDR11 x_73
     161| ADDR16 x_74 -> h_ADDR16 x_74
    162162
    163163(** val addressing_mode_rect_Type3 :
     
    169169    -> 'a1) -> addressing_mode -> 'a1 **)
    170170let rec addressing_mode_rect_Type3 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    171 | DIRECT x_1063 -> h_DIRECT x_1063
    172 | INDIRECT x_1064 -> h_INDIRECT x_1064
    173 | EXT_INDIRECT x_1065 -> h_EXT_INDIRECT x_1065
    174 | REGISTER x_1066 -> h_REGISTER x_1066
     171| DIRECT x_95 -> h_DIRECT x_95
     172| INDIRECT x_96 -> h_INDIRECT x_96
     173| EXT_INDIRECT x_97 -> h_EXT_INDIRECT x_97
     174| REGISTER x_98 -> h_REGISTER x_98
    175175| ACC_A -> h_ACC_A
    176176| ACC_B -> h_ACC_B
    177177| DPTR -> h_DPTR
    178 | DATA x_1067 -> h_DATA x_1067
    179 | DATA16 x_1068 -> h_DATA16 x_1068
     178| DATA x_99 -> h_DATA x_99
     179| DATA16 x_100 -> h_DATA16 x_100
    180180| ACC_DPTR -> h_ACC_DPTR
    181181| ACC_PC -> h_ACC_PC
     
    183183| INDIRECT_DPTR -> h_INDIRECT_DPTR
    184184| CARRY -> h_CARRY
    185 | BIT_ADDR x_1069 -> h_BIT_ADDR x_1069
    186 | N_BIT_ADDR x_1070 -> h_N_BIT_ADDR x_1070
    187 | RELATIVE x_1071 -> h_RELATIVE x_1071
    188 | ADDR11 x_1072 -> h_ADDR11 x_1072
    189 | ADDR16 x_1073 -> h_ADDR16 x_1073
     185| BIT_ADDR x_101 -> h_BIT_ADDR x_101
     186| N_BIT_ADDR x_102 -> h_N_BIT_ADDR x_102
     187| RELATIVE x_103 -> h_RELATIVE x_103
     188| ADDR11 x_104 -> h_ADDR11 x_104
     189| ADDR16 x_105 -> h_ADDR16 x_105
    190190
    191191(** val addressing_mode_rect_Type2 :
     
    197197    -> 'a1) -> addressing_mode -> 'a1 **)
    198198let rec addressing_mode_rect_Type2 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    199 | DIRECT x_1094 -> h_DIRECT x_1094
    200 | INDIRECT x_1095 -> h_INDIRECT x_1095
    201 | EXT_INDIRECT x_1096 -> h_EXT_INDIRECT x_1096
    202 | REGISTER x_1097 -> h_REGISTER x_1097
     199| DIRECT x_126 -> h_DIRECT x_126
     200| INDIRECT x_127 -> h_INDIRECT x_127
     201| EXT_INDIRECT x_128 -> h_EXT_INDIRECT x_128
     202| REGISTER x_129 -> h_REGISTER x_129
    203203| ACC_A -> h_ACC_A
    204204| ACC_B -> h_ACC_B
    205205| DPTR -> h_DPTR
    206 | DATA x_1098 -> h_DATA x_1098
    207 | DATA16 x_1099 -> h_DATA16 x_1099
     206| DATA x_130 -> h_DATA x_130
     207| DATA16 x_131 -> h_DATA16 x_131
    208208| ACC_DPTR -> h_ACC_DPTR
    209209| ACC_PC -> h_ACC_PC
     
    211211| INDIRECT_DPTR -> h_INDIRECT_DPTR
    212212| CARRY -> h_CARRY
    213 | BIT_ADDR x_1100 -> h_BIT_ADDR x_1100
    214 | N_BIT_ADDR x_1101 -> h_N_BIT_ADDR x_1101
    215 | RELATIVE x_1102 -> h_RELATIVE x_1102
    216 | ADDR11 x_1103 -> h_ADDR11 x_1103
    217 | ADDR16 x_1104 -> h_ADDR16 x_1104
     213| BIT_ADDR x_132 -> h_BIT_ADDR x_132
     214| N_BIT_ADDR x_133 -> h_N_BIT_ADDR x_133
     215| RELATIVE x_134 -> h_RELATIVE x_134
     216| ADDR11 x_135 -> h_ADDR11 x_135
     217| ADDR16 x_136 -> h_ADDR16 x_136
    218218
    219219(** val addressing_mode_rect_Type1 :
     
    225225    -> 'a1) -> addressing_mode -> 'a1 **)
    226226let rec addressing_mode_rect_Type1 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    227 | DIRECT x_1125 -> h_DIRECT x_1125
    228 | INDIRECT x_1126 -> h_INDIRECT x_1126
    229 | EXT_INDIRECT x_1127 -> h_EXT_INDIRECT x_1127
    230 | REGISTER x_1128 -> h_REGISTER x_1128
     227| DIRECT x_157 -> h_DIRECT x_157
     228| INDIRECT x_158 -> h_INDIRECT x_158
     229| EXT_INDIRECT x_159 -> h_EXT_INDIRECT x_159
     230| REGISTER x_160 -> h_REGISTER x_160
    231231| ACC_A -> h_ACC_A
    232232| ACC_B -> h_ACC_B
    233233| DPTR -> h_DPTR
    234 | DATA x_1129 -> h_DATA x_1129
    235 | DATA16 x_1130 -> h_DATA16 x_1130
     234| DATA x_161 -> h_DATA x_161
     235| DATA16 x_162 -> h_DATA16 x_162
    236236| ACC_DPTR -> h_ACC_DPTR
    237237| ACC_PC -> h_ACC_PC
     
    239239| INDIRECT_DPTR -> h_INDIRECT_DPTR
    240240| CARRY -> h_CARRY
    241 | BIT_ADDR x_1131 -> h_BIT_ADDR x_1131
    242 | N_BIT_ADDR x_1132 -> h_N_BIT_ADDR x_1132
    243 | RELATIVE x_1133 -> h_RELATIVE x_1133
    244 | ADDR11 x_1134 -> h_ADDR11 x_1134
    245 | ADDR16 x_1135 -> h_ADDR16 x_1135
     241| BIT_ADDR x_163 -> h_BIT_ADDR x_163
     242| N_BIT_ADDR x_164 -> h_N_BIT_ADDR x_164
     243| RELATIVE x_165 -> h_RELATIVE x_165
     244| ADDR11 x_166 -> h_ADDR11 x_166
     245| ADDR16 x_167 -> h_ADDR16 x_167
    246246
    247247(** val addressing_mode_rect_Type0 :
     
    253253    -> 'a1) -> addressing_mode -> 'a1 **)
    254254let rec addressing_mode_rect_Type0 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    255 | DIRECT x_1156 -> h_DIRECT x_1156
    256 | INDIRECT x_1157 -> h_INDIRECT x_1157
    257 | EXT_INDIRECT x_1158 -> h_EXT_INDIRECT x_1158
    258 | REGISTER x_1159 -> h_REGISTER x_1159
     255| DIRECT x_188 -> h_DIRECT x_188
     256| INDIRECT x_189 -> h_INDIRECT x_189
     257| EXT_INDIRECT x_190 -> h_EXT_INDIRECT x_190
     258| REGISTER x_191 -> h_REGISTER x_191
    259259| ACC_A -> h_ACC_A
    260260| ACC_B -> h_ACC_B
    261261| DPTR -> h_DPTR
    262 | DATA x_1160 -> h_DATA x_1160
    263 | DATA16 x_1161 -> h_DATA16 x_1161
     262| DATA x_192 -> h_DATA x_192
     263| DATA16 x_193 -> h_DATA16 x_193
    264264| ACC_DPTR -> h_ACC_DPTR
    265265| ACC_PC -> h_ACC_PC
     
    267267| INDIRECT_DPTR -> h_INDIRECT_DPTR
    268268| CARRY -> h_CARRY
    269 | BIT_ADDR x_1162 -> h_BIT_ADDR x_1162
    270 | N_BIT_ADDR x_1163 -> h_N_BIT_ADDR x_1163
    271 | RELATIVE x_1164 -> h_RELATIVE x_1164
    272 | ADDR11 x_1165 -> h_ADDR11 x_1165
    273 | ADDR16 x_1166 -> h_ADDR16 x_1166
     269| BIT_ADDR x_194 -> h_BIT_ADDR x_194
     270| N_BIT_ADDR x_195 -> h_N_BIT_ADDR x_195
     271| RELATIVE x_196 -> h_RELATIVE x_196
     272| ADDR11 x_197 -> h_ADDR11 x_197
     273| ADDR16 x_198 -> h_ADDR16 x_198
    274274
    275275(** val addressing_mode_inv_rect_Type4 :
     
    19261926    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19271927    'a1) -> subaddressing_mode -> 'a1 **)
    1928 let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_1634 =
    1929   let subaddressing_modeel = x_1634 in
     1928let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_666 =
     1929  let subaddressing_modeel = x_666 in
    19301930  h_mk_subaddressing_mode subaddressing_modeel __
    19311931
     
    19331933    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19341934    'a1) -> subaddressing_mode -> 'a1 **)
    1935 let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_1636 =
    1936   let subaddressing_modeel = x_1636 in
     1935let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_668 =
     1936  let subaddressing_modeel = x_668 in
    19371937  h_mk_subaddressing_mode subaddressing_modeel __
    19381938
     
    19401940    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19411941    'a1) -> subaddressing_mode -> 'a1 **)
    1942 let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_1638 =
    1943   let subaddressing_modeel = x_1638 in
     1942let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_670 =
     1943  let subaddressing_modeel = x_670 in
    19441944  h_mk_subaddressing_mode subaddressing_modeel __
    19451945
     
    19471947    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19481948    'a1) -> subaddressing_mode -> 'a1 **)
    1949 let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_1640 =
    1950   let subaddressing_modeel = x_1640 in
     1949let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_672 =
     1950  let subaddressing_modeel = x_672 in
    19511951  h_mk_subaddressing_mode subaddressing_modeel __
    19521952
     
    19541954    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19551955    'a1) -> subaddressing_mode -> 'a1 **)
    1956 let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_1642 =
    1957   let subaddressing_modeel = x_1642 in
     1956let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_674 =
     1957  let subaddressing_modeel = x_674 in
    19581958  h_mk_subaddressing_mode subaddressing_modeel __
    19591959
     
    19611961    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19621962    'a1) -> subaddressing_mode -> 'a1 **)
    1963 let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_1644 =
    1964   let subaddressing_modeel = x_1644 in
     1963let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_676 =
     1964  let subaddressing_modeel = x_676 in
    19651965  h_mk_subaddressing_mode subaddressing_modeel __
    19661966
     
    22882288    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    22892289let rec preinstruction_rect_Type4 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
    2290 | ADD (x_1746, x_1745) -> h_ADD x_1746 x_1745
    2291 | ADDC (x_1748, x_1747) -> h_ADDC x_1748 x_1747
    2292 | SUBB (x_1750, x_1749) -> h_SUBB x_1750 x_1749
    2293 | INC x_1751 -> h_INC x_1751
    2294 | DEC x_1752 -> h_DEC x_1752
    2295 | MUL (x_1754, x_1753) -> h_MUL x_1754 x_1753
    2296 | DIV (x_1756, x_1755) -> h_DIV x_1756 x_1755
    2297 | DA x_1757 -> h_DA x_1757
    2298 | JC x_1758 -> h_JC x_1758
    2299 | JNC x_1759 -> h_JNC x_1759
    2300 | JB (x_1761, x_1760) -> h_JB x_1761 x_1760
    2301 | JNB (x_1763, x_1762) -> h_JNB x_1763 x_1762
    2302 | JBC (x_1765, x_1764) -> h_JBC x_1765 x_1764
    2303 | JZ x_1766 -> h_JZ x_1766
    2304 | JNZ x_1767 -> h_JNZ x_1767
    2305 | CJNE (x_1769, x_1768) -> h_CJNE x_1769 x_1768
    2306 | DJNZ (x_1771, x_1770) -> h_DJNZ x_1771 x_1770
    2307 | ANL x_1772 -> h_ANL x_1772
    2308 | ORL x_1773 -> h_ORL x_1773
    2309 | XRL x_1774 -> h_XRL x_1774
    2310 | CLR x_1775 -> h_CLR x_1775
    2311 | CPL x_1776 -> h_CPL x_1776
    2312 | RL x_1777 -> h_RL x_1777
    2313 | RLC x_1778 -> h_RLC x_1778
    2314 | RR x_1779 -> h_RR x_1779
    2315 | RRC x_1780 -> h_RRC x_1780
    2316 | SWAP x_1781 -> h_SWAP x_1781
    2317 | MOV x_1782 -> h_MOV x_1782
    2318 | MOVX x_1783 -> h_MOVX x_1783
    2319 | SETB x_1784 -> h_SETB x_1784
    2320 | PUSH x_1785 -> h_PUSH x_1785
    2321 | POP x_1786 -> h_POP x_1786
    2322 | XCH (x_1788, x_1787) -> h_XCH x_1788 x_1787
    2323 | XCHD (x_1790, x_1789) -> h_XCHD x_1790 x_1789
     2290| ADD (x_778, x_777) -> h_ADD x_778 x_777
     2291| ADDC (x_780, x_779) -> h_ADDC x_780 x_779
     2292| SUBB (x_782, x_781) -> h_SUBB x_782 x_781
     2293| INC x_783 -> h_INC x_783
     2294| DEC x_784 -> h_DEC x_784
     2295| MUL (x_786, x_785) -> h_MUL x_786 x_785
     2296| DIV (x_788, x_787) -> h_DIV x_788 x_787
     2297| DA x_789 -> h_DA x_789
     2298| JC x_790 -> h_JC x_790
     2299| JNC x_791 -> h_JNC x_791
     2300| JB (x_793, x_792) -> h_JB x_793 x_792
     2301| JNB (x_795, x_794) -> h_JNB x_795 x_794
     2302| JBC (x_797, x_796) -> h_JBC x_797 x_796
     2303| JZ x_798 -> h_JZ x_798
     2304| JNZ x_799 -> h_JNZ x_799
     2305| CJNE (x_801, x_800) -> h_CJNE x_801 x_800
     2306| DJNZ (x_803, x_802) -> h_DJNZ x_803 x_802
     2307| ANL x_804 -> h_ANL x_804
     2308| ORL x_805 -> h_ORL x_805
     2309| XRL x_806 -> h_XRL x_806
     2310| CLR x_807 -> h_CLR x_807
     2311| CPL x_808 -> h_CPL x_808
     2312| RL x_809 -> h_RL x_809
     2313| RLC x_810 -> h_RLC x_810
     2314| RR x_811 -> h_RR x_811
     2315| RRC x_812 -> h_RRC x_812
     2316| SWAP x_813 -> h_SWAP x_813
     2317| MOV x_814 -> h_MOV x_814
     2318| MOVX x_815 -> h_MOVX x_815
     2319| SETB x_816 -> h_SETB x_816
     2320| PUSH x_817 -> h_PUSH x_817
     2321| POP x_818 -> h_POP x_818
     2322| XCH (x_820, x_819) -> h_XCH x_820 x_819
     2323| XCHD (x_822, x_821) -> h_XCHD x_822 x_821
    23242324| RET -> h_RET
    23252325| RETI -> h_RETI
    23262326| NOP -> h_NOP
    2327 | JMP x_1791 -> h_JMP x_1791
     2327| JMP x_823 -> h_JMP x_823
    23282328
    23292329(** val preinstruction_rect_Type5 :
     
    23632363    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    23642364let rec preinstruction_rect_Type5 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
    2365 | ADD (x_1832, x_1831) -> h_ADD x_1832 x_1831
    2366 | ADDC (x_1834, x_1833) -> h_ADDC x_1834 x_1833
    2367 | SUBB (x_1836, x_1835) -> h_SUBB x_1836 x_1835
    2368 | INC x_1837 -> h_INC x_1837
    2369 | DEC x_1838 -> h_DEC x_1838
    2370 | MUL (x_1840, x_1839) -> h_MUL x_1840 x_1839
    2371 | DIV (x_1842, x_1841) -> h_DIV x_1842 x_1841
    2372 | DA x_1843 -> h_DA x_1843
    2373 | JC x_1844 -> h_JC x_1844
    2374 | JNC x_1845 -> h_JNC x_1845
    2375 | JB (x_1847, x_1846) -> h_JB x_1847 x_1846
    2376 | JNB (x_1849, x_1848) -> h_JNB x_1849 x_1848
    2377 | JBC (x_1851, x_1850) -> h_JBC x_1851 x_1850
    2378 | JZ x_1852 -> h_JZ x_1852
    2379 | JNZ x_1853 -> h_JNZ x_1853
    2380 | CJNE (x_1855, x_1854) -> h_CJNE x_1855 x_1854
    2381 | DJNZ (x_1857, x_1856) -> h_DJNZ x_1857 x_1856
    2382 | ANL x_1858 -> h_ANL x_1858
    2383 | ORL x_1859 -> h_ORL x_1859
    2384 | XRL x_1860 -> h_XRL x_1860
    2385 | CLR x_1861 -> h_CLR x_1861
    2386 | CPL x_1862 -> h_CPL x_1862
    2387 | RL x_1863 -> h_RL x_1863
    2388 | RLC x_1864 -> h_RLC x_1864
    2389 | RR x_1865 -> h_RR x_1865
    2390 | RRC x_1866 -> h_RRC x_1866
    2391 | SWAP x_1867 -> h_SWAP x_1867
    2392 | MOV x_1868 -> h_MOV x_1868
    2393 | MOVX x_1869 -> h_MOVX x_1869
    2394 | SETB x_1870 -> h_SETB x_1870
    2395 | PUSH x_1871 -> h_PUSH x_1871
    2396 | POP x_1872 -> h_POP x_1872
    2397 | XCH (x_1874, x_1873) -> h_XCH x_1874 x_1873
    2398 | XCHD (x_1876, x_1875) -> h_XCHD x_1876 x_1875
     2365| ADD (x_864, x_863) -> h_ADD x_864 x_863
     2366| ADDC (x_866, x_865) -> h_ADDC x_866 x_865
     2367| SUBB (x_868, x_867) -> h_SUBB x_868 x_867
     2368| INC x_869 -> h_INC x_869
     2369| DEC x_870 -> h_DEC x_870
     2370| MUL (x_872, x_871) -> h_MUL x_872 x_871
     2371| DIV (x_874, x_873) -> h_DIV x_874 x_873
     2372| DA x_875 -> h_DA x_875
     2373| JC x_876 -> h_JC x_876
     2374| JNC x_877 -> h_JNC x_877
     2375| JB (x_879, x_878) -> h_JB x_879 x_878
     2376| JNB (x_881, x_880) -> h_JNB x_881 x_880
     2377| JBC (x_883, x_882) -> h_JBC x_883 x_882
     2378| JZ x_884 -> h_JZ x_884
     2379| JNZ x_885 -> h_JNZ x_885
     2380| CJNE (x_887, x_886) -> h_CJNE x_887 x_886
     2381| DJNZ (x_889, x_888) -> h_DJNZ x_889 x_888
     2382| ANL x_890 -> h_ANL x_890
     2383| ORL x_891 -> h_ORL x_891
     2384| XRL x_892 -> h_XRL x_892
     2385| CLR x_893 -> h_CLR x_893
     2386| CPL x_894 -> h_CPL x_894
     2387| RL x_895 -> h_RL x_895
     2388| RLC x_896 -> h_RLC x_896
     2389| RR x_897 -> h_RR x_897
     2390| RRC x_898 -> h_RRC x_898
     2391| SWAP x_899 -> h_SWAP x_899
     2392| MOV x_900 -> h_MOV x_900
     2393| MOVX x_901 -> h_MOVX x_901
     2394| SETB x_902 -> h_SETB x_902
     2395| PUSH x_903 -> h_PUSH x_903
     2396| POP x_904 -> h_POP x_904
     2397| XCH (x_906, x_905) -> h_XCH x_906 x_905
     2398| XCHD (x_908, x_907) -> h_XCHD x_908 x_907
    23992399| RET -> h_RET
    24002400| RETI -> h_RETI
    24012401| NOP -> h_NOP
    2402 | JMP x_1877 -> h_JMP x_1877
     2402| JMP x_909 -> h_JMP x_909
    24032403
    24042404(** val preinstruction_rect_Type3 :
     
    24382438    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    24392439let rec preinstruction_rect_Type3 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
    2440 | ADD (x_1918, x_1917) -> h_ADD x_1918 x_1917
    2441 | ADDC (x_1920, x_1919) -> h_ADDC x_1920 x_1919
    2442 | SUBB (x_1922, x_1921) -> h_SUBB x_1922 x_1921
    2443 | INC x_1923 -> h_INC x_1923
    2444 | DEC x_1924 -> h_DEC x_1924
    2445 | MUL (x_1926, x_1925) -> h_MUL x_1926 x_1925
    2446 | DIV (x_1928, x_1927) -> h_DIV x_1928 x_1927
    2447 | DA x_1929 -> h_DA x_1929
    2448 | JC x_1930 -> h_JC x_1930
    2449 | JNC x_1931 -> h_JNC x_1931
    2450 | JB (x_1933, x_1932) -> h_JB x_1933 x_1932
    2451 | JNB (x_1935, x_1934) -> h_JNB x_1935 x_1934
    2452 | JBC (x_1937, x_1936) -> h_JBC x_1937 x_1936
    2453 | JZ x_1938 -> h_JZ x_1938
    2454 | JNZ x_1939 -> h_JNZ x_1939
    2455 | CJNE (x_1941, x_1940) -> h_CJNE x_1941 x_1940
    2456 | DJNZ (x_1943, x_1942) -> h_DJNZ x_1943 x_1942
    2457 | ANL x_1944 -> h_ANL x_1944
    2458 | ORL x_1945 -> h_ORL x_1945
    2459 | XRL x_1946 -> h_XRL x_1946
    2460 | CLR x_1947 -> h_CLR x_1947
    2461 | CPL x_1948 -> h_CPL x_1948
    2462 | RL x_1949 -> h_RL x_1949
    2463 | RLC x_1950 -> h_RLC x_1950
    2464 | RR x_1951 -> h_RR x_1951
    2465 | RRC x_1952 -> h_RRC x_1952
    2466 | SWAP x_1953 -> h_SWAP x_1953
    2467 | MOV x_1954 -> h_MOV x_1954
    2468 | MOVX x_1955 -> h_MOVX x_1955
    2469 | SETB x_1956 -> h_SETB x_1956
    2470 | PUSH x_1957 -> h_PUSH x_1957
    2471 | POP x_1958 -> h_POP x_1958
    2472 | XCH (x_1960, x_1959) -> h_XCH x_1960 x_1959
    2473 | XCHD (x_1962, x_1961) -> h_XCHD x_1962 x_1961
     2440| ADD (x_950, x_949) -> h_ADD x_950 x_949
     2441| ADDC (x_952, x_951) -> h_ADDC x_952 x_951
     2442| SUBB (x_954, x_953) -> h_SUBB x_954 x_953
     2443| INC x_955 -> h_INC x_955
     2444| DEC x_956 -> h_DEC x_956
     2445| MUL (x_958, x_957) -> h_MUL x_958 x_957
     2446| DIV (x_960, x_959) -> h_DIV x_960 x_959
     2447| DA x_961 -> h_DA x_961
     2448| JC x_962 -> h_JC x_962
     2449| JNC x_963 -> h_JNC x_963
     2450| JB (x_965, x_964) -> h_JB x_965 x_964
     2451| JNB (x_967, x_966) -> h_JNB x_967 x_966
     2452| JBC (x_969, x_968) -> h_JBC x_969 x_968
     2453| JZ x_970 -> h_JZ x_970
     2454| JNZ x_971 -> h_JNZ x_971
     2455| CJNE (x_973, x_972) -> h_CJNE x_973 x_972
     2456| DJNZ (x_975, x_974) -> h_DJNZ x_975 x_974
     2457| ANL x_976 -> h_ANL x_976
     2458| ORL x_977 -> h_ORL x_977
     2459| XRL x_978 -> h_XRL x_978
     2460| CLR x_979 -> h_CLR x_979
     2461| CPL x_980 -> h_CPL x_980
     2462| RL x_981 -> h_RL x_981
     2463| RLC x_982 -> h_RLC x_982
     2464| RR x_983 -> h_RR x_983
     2465| RRC x_984 -> h_RRC x_984
     2466| SWAP x_985 -> h_SWAP x_985
     2467| MOV x_986 -> h_MOV x_986
     2468| MOVX x_987 -> h_MOVX x_987
     2469| SETB x_988 -> h_SETB x_988
     2470| PUSH x_989 -> h_PUSH x_989
     2471| POP x_990 -> h_POP x_990
     2472| XCH (x_992, x_991) -> h_XCH x_992 x_991
     2473| XCHD (x_994, x_993) -> h_XCHD x_994 x_993
    24742474| RET -> h_RET
    24752475| RETI -> h_RETI
    24762476| NOP -> h_NOP
    2477 | JMP x_1963 -> h_JMP x_1963
     2477| JMP x_995 -> h_JMP x_995
    24782478
    24792479(** val preinstruction_rect_Type2 :
     
    25132513    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    25142514let rec preinstruction_rect_Type2 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
    2515 | ADD (x_2004, x_2003) -> h_ADD x_2004 x_2003
    2516 | ADDC (x_2006, x_2005) -> h_ADDC x_2006 x_2005
    2517 | SUBB (x_2008, x_2007) -> h_SUBB x_2008 x_2007
    2518 | INC x_2009 -> h_INC x_2009
    2519 | DEC x_2010 -> h_DEC x_2010
    2520 | MUL (x_2012, x_2011) -> h_MUL x_2012 x_2011
    2521 | DIV (x_2014, x_2013) -> h_DIV x_2014 x_2013
    2522 | DA x_2015 -> h_DA x_2015
    2523 | JC x_2016 -> h_JC x_2016
    2524 | JNC x_2017 -> h_JNC x_2017
    2525 | JB (x_2019, x_2018) -> h_JB x_2019 x_2018
    2526 | JNB (x_2021, x_2020) -> h_JNB x_2021 x_2020
    2527 | JBC (x_2023, x_2022) -> h_JBC x_2023 x_2022
    2528 | JZ x_2024 -> h_JZ x_2024
    2529 | JNZ x_2025 -> h_JNZ x_2025
    2530 | CJNE (x_2027, x_2026) -> h_CJNE x_2027 x_2026
    2531 | DJNZ (x_2029, x_2028) -> h_DJNZ x_2029 x_2028
    2532 | ANL x_2030 -> h_ANL x_2030
    2533 | ORL x_2031 -> h_ORL x_2031
    2534 | XRL x_2032 -> h_XRL x_2032
    2535 | CLR x_2033 -> h_CLR x_2033
    2536 | CPL x_2034 -> h_CPL x_2034
    2537 | RL x_2035 -> h_RL x_2035
    2538 | RLC x_2036 -> h_RLC x_2036
    2539 | RR x_2037 -> h_RR x_2037
    2540 | RRC x_2038 -> h_RRC x_2038
    2541 | SWAP x_2039 -> h_SWAP x_2039
    2542 | MOV x_2040 -> h_MOV x_2040
    2543 | MOVX x_2041 -> h_MOVX x_2041
    2544 | SETB x_2042 -> h_SETB x_2042
    2545 | PUSH x_2043 -> h_PUSH x_2043
    2546 | POP x_2044 -> h_POP x_2044
    2547 | XCH (x_2046, x_2045) -> h_XCH x_2046 x_2045
    2548 | XCHD (x_2048, x_2047) -> h_XCHD x_2048 x_2047
     2515| ADD (x_1036, x_1035) -> h_ADD x_1036 x_1035
     2516| ADDC (x_1038, x_1037) -> h_ADDC x_1038 x_1037
     2517| SUBB (x_1040, x_1039) -> h_SUBB x_1040 x_1039
     2518| INC x_1041 -> h_INC x_1041
     2519| DEC x_1042 -> h_DEC x_1042
     2520| MUL (x_1044, x_1043) -> h_MUL x_1044 x_1043
     2521| DIV (x_1046, x_1045) -> h_DIV x_1046 x_1045
     2522| DA x_1047 -> h_DA x_1047
     2523| JC x_1048 -> h_JC x_1048
     2524| JNC x_1049 -> h_JNC x_1049
     2525| JB (x_1051, x_1050) -> h_JB x_1051 x_1050
     2526| JNB (x_1053, x_1052) -> h_JNB x_1053 x_1052
     2527| JBC (x_1055, x_1054) -> h_JBC x_1055 x_1054
     2528| JZ x_1056 -> h_JZ x_1056
     2529| JNZ x_1057 -> h_JNZ x_1057
     2530| CJNE (x_1059, x_1058) -> h_CJNE x_1059 x_1058
     2531| DJNZ (x_1061, x_1060) -> h_DJNZ x_1061 x_1060
     2532| ANL x_1062 -> h_ANL x_1062
     2533| ORL x_1063 -> h_ORL x_1063
     2534| XRL x_1064 -> h_XRL x_1064
     2535| CLR x_1065 -> h_CLR x_1065
     2536| CPL x_1066 -> h_CPL x_1066
     2537| RL x_1067 -> h_RL x_1067
     2538| RLC x_1068 -> h_RLC x_1068
     2539| RR x_1069 -> h_RR x_1069
     2540| RRC x_1070 -> h_RRC x_1070
     2541| SWAP x_1071 -> h_SWAP x_1071
     2542| MOV x_1072 -> h_MOV x_1072
     2543| MOVX x_1073 -> h_MOVX x_1073
     2544| SETB x_1074 -> h_SETB x_1074
     2545| PUSH x_1075 -> h_PUSH x_1075
     2546| POP x_1076 -> h_POP x_1076
     2547| XCH (x_1078, x_1077) -> h_XCH x_1078 x_1077
     2548| XCHD (x_1080, x_1079) -> h_XCHD x_1080 x_1079
    25492549| RET -> h_RET
    25502550| RETI -> h_RETI
    25512551| NOP -> h_NOP
    2552 | JMP x_2049 -> h_JMP x_2049
     2552| JMP x_1081 -> h_JMP x_1081
    25532553
    25542554(** val preinstruction_rect_Type1 :
     
    25882588    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    25892589let rec preinstruction_rect_Type1 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
    2590 | ADD (x_2090, x_2089) -> h_ADD x_2090 x_2089
    2591 | ADDC (x_2092, x_2091) -> h_ADDC x_2092 x_2091
    2592 | SUBB (x_2094, x_2093) -> h_SUBB x_2094 x_2093
    2593 | INC x_2095 -> h_INC x_2095
    2594 | DEC x_2096 -> h_DEC x_2096
    2595 | MUL (x_2098, x_2097) -> h_MUL x_2098 x_2097
    2596 | DIV (x_2100, x_2099) -> h_DIV x_2100 x_2099
    2597 | DA x_2101 -> h_DA x_2101
    2598 | JC x_2102 -> h_JC x_2102
    2599 | JNC x_2103 -> h_JNC x_2103
    2600 | JB (x_2105, x_2104) -> h_JB x_2105 x_2104
    2601 | JNB (x_2107, x_2106) -> h_JNB x_2107 x_2106
    2602 | JBC (x_2109, x_2108) -> h_JBC x_2109 x_2108
    2603 | JZ x_2110 -> h_JZ x_2110
    2604 | JNZ x_2111 -> h_JNZ x_2111
    2605 | CJNE (x_2113, x_2112) -> h_CJNE x_2113 x_2112
    2606 | DJNZ (x_2115, x_2114) -> h_DJNZ x_2115 x_2114
    2607 | ANL x_2116 -> h_ANL x_2116
    2608 | ORL x_2117 -> h_ORL x_2117
    2609 | XRL x_2118 -> h_XRL x_2118
    2610 | CLR x_2119 -> h_CLR x_2119
    2611 | CPL x_2120 -> h_CPL x_2120
    2612 | RL x_2121 -> h_RL x_2121
    2613 | RLC x_2122 -> h_RLC x_2122
    2614 | RR x_2123 -> h_RR x_2123
    2615 | RRC x_2124 -> h_RRC x_2124
    2616 | SWAP x_2125 -> h_SWAP x_2125
    2617 | MOV x_2126 -> h_MOV x_2126
    2618 | MOVX x_2127 -> h_MOVX x_2127
    2619 | SETB x_2128 -> h_SETB x_2128
    2620 | PUSH x_2129 -> h_PUSH x_2129
    2621 | POP x_2130 -> h_POP x_2130
    2622 | XCH (x_2132, x_2131) -> h_XCH x_2132 x_2131
    2623 | XCHD (x_2134, x_2133) -> h_XCHD x_2134 x_2133
     2590| ADD (x_1122, x_1121) -> h_ADD x_1122 x_1121
     2591| ADDC (x_1124, x_1123) -> h_ADDC x_1124 x_1123
     2592| SUBB (x_1126, x_1125) -> h_SUBB x_1126 x_1125
     2593| INC x_1127 -> h_INC x_1127
     2594| DEC x_1128 -> h_DEC x_1128
     2595| MUL (x_1130, x_1129) -> h_MUL x_1130 x_1129
     2596| DIV (x_1132, x_1131) -> h_DIV x_1132 x_1131
     2597| DA x_1133 -> h_DA x_1133
     2598| JC x_1134 -> h_JC x_1134
     2599| JNC x_1135 -> h_JNC x_1135
     2600| JB (x_1137, x_1136) -> h_JB x_1137 x_1136
     2601| JNB (x_1139, x_1138) -> h_JNB x_1139 x_1138
     2602| JBC (x_1141, x_1140) -> h_JBC x_1141 x_1140
     2603| JZ x_1142 -> h_JZ x_1142
     2604| JNZ x_1143 -> h_JNZ x_1143
     2605| CJNE (x_1145, x_1144) -> h_CJNE x_1145 x_1144
     2606| DJNZ (x_1147, x_1146) -> h_DJNZ x_1147 x_1146
     2607| ANL x_1148 -> h_ANL x_1148
     2608| ORL x_1149 -> h_ORL x_1149
     2609| XRL x_1150 -> h_XRL x_1150
     2610| CLR x_1151 -> h_CLR x_1151
     2611| CPL x_1152 -> h_CPL x_1152
     2612| RL x_1153 -> h_RL x_1153
     2613| RLC x_1154 -> h_RLC x_1154
     2614| RR x_1155 -> h_RR x_1155
     2615| RRC x_1156 -> h_RRC x_1156
     2616| SWAP x_1157 -> h_SWAP x_1157
     2617| MOV x_1158 -> h_MOV x_1158
     2618| MOVX x_1159 -> h_MOVX x_1159
     2619| SETB x_1160 -> h_SETB x_1160
     2620| PUSH x_1161 -> h_PUSH x_1161
     2621| POP x_1162 -> h_POP x_1162
     2622| XCH (x_1164, x_1163) -> h_XCH x_1164 x_1163
     2623| XCHD (x_1166, x_1165) -> h_XCHD x_1166 x_1165
    26242624| RET -> h_RET
    26252625| RETI -> h_RETI
    26262626| NOP -> h_NOP
    2627 | JMP x_2135 -> h_JMP x_2135
     2627| JMP x_1167 -> h_JMP x_1167
    26282628
    26292629(** val preinstruction_rect_Type0 :
     
    26632663    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    26642664let rec preinstruction_rect_Type0 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
    2665 | ADD (x_2176, x_2175) -> h_ADD x_2176 x_2175
    2666 | ADDC (x_2178, x_2177) -> h_ADDC x_2178 x_2177
    2667 | SUBB (x_2180, x_2179) -> h_SUBB x_2180 x_2179
    2668 | INC x_2181 -> h_INC x_2181
    2669 | DEC x_2182 -> h_DEC x_2182
    2670 | MUL (x_2184, x_2183) -> h_MUL x_2184 x_2183
    2671 | DIV (x_2186, x_2185) -> h_DIV x_2186 x_2185
    2672 | DA x_2187 -> h_DA x_2187
    2673 | JC x_2188 -> h_JC x_2188
    2674 | JNC x_2189 -> h_JNC x_2189
    2675 | JB (x_2191, x_2190) -> h_JB x_2191 x_2190
    2676 | JNB (x_2193, x_2192) -> h_JNB x_2193 x_2192
    2677 | JBC (x_2195, x_2194) -> h_JBC x_2195 x_2194
    2678 | JZ x_2196 -> h_JZ x_2196
    2679 | JNZ x_2197 -> h_JNZ x_2197
    2680 | CJNE (x_2199, x_2198) -> h_CJNE x_2199 x_2198
    2681 | DJNZ (x_2201, x_2200) -> h_DJNZ x_2201 x_2200
    2682 | ANL x_2202 -> h_ANL x_2202
    2683 | ORL x_2203 -> h_ORL x_2203
    2684 | XRL x_2204 -> h_XRL x_2204
    2685 | CLR x_2205 -> h_CLR x_2205
    2686 | CPL x_2206 -> h_CPL x_2206
    2687 | RL x_2207 -> h_RL x_2207
    2688 | RLC x_2208 -> h_RLC x_2208
    2689 | RR x_2209 -> h_RR x_2209
    2690 | RRC x_2210 -> h_RRC x_2210
    2691 | SWAP x_2211 -> h_SWAP x_2211
    2692 | MOV x_2212 -> h_MOV x_2212
    2693 | MOVX x_2213 -> h_MOVX x_2213
    2694 | SETB x_2214 -> h_SETB x_2214
    2695 | PUSH x_2215 -> h_PUSH x_2215
    2696 | POP x_2216 -> h_POP x_2216
    2697 | XCH (x_2218, x_2217) -> h_XCH x_2218 x_2217
    2698 | XCHD (x_2220, x_2219) -> h_XCHD x_2220 x_2219
     2665| ADD (x_1208, x_1207) -> h_ADD x_1208 x_1207
     2666| ADDC (x_1210, x_1209) -> h_ADDC x_1210 x_1209
     2667| SUBB (x_1212, x_1211) -> h_SUBB x_1212 x_1211
     2668| INC x_1213 -> h_INC x_1213
     2669| DEC x_1214 -> h_DEC x_1214
     2670| MUL (x_1216, x_1215) -> h_MUL x_1216 x_1215
     2671| DIV (x_1218, x_1217) -> h_DIV x_1218 x_1217
     2672| DA x_1219 -> h_DA x_1219
     2673| JC x_1220 -> h_JC x_1220
     2674| JNC x_1221 -> h_JNC x_1221
     2675| JB (x_1223, x_1222) -> h_JB x_1223 x_1222
     2676| JNB (x_1225, x_1224) -> h_JNB x_1225 x_1224
     2677| JBC (x_1227, x_1226) -> h_JBC x_1227 x_1226
     2678| JZ x_1228 -> h_JZ x_1228
     2679| JNZ x_1229 -> h_JNZ x_1229
     2680| CJNE (x_1231, x_1230) -> h_CJNE x_1231 x_1230
     2681| DJNZ (x_1233, x_1232) -> h_DJNZ x_1233 x_1232
     2682| ANL x_1234 -> h_ANL x_1234
     2683| ORL x_1235 -> h_ORL x_1235
     2684| XRL x_1236 -> h_XRL x_1236
     2685| CLR x_1237 -> h_CLR x_1237
     2686| CPL x_1238 -> h_CPL x_1238
     2687| RL x_1239 -> h_RL x_1239
     2688| RLC x_1240 -> h_RLC x_1240
     2689| RR x_1241 -> h_RR x_1241
     2690| RRC x_1242 -> h_RRC x_1242
     2691| SWAP x_1243 -> h_SWAP x_1243
     2692| MOV x_1244 -> h_MOV x_1244
     2693| MOVX x_1245 -> h_MOVX x_1245
     2694| SETB x_1246 -> h_SETB x_1246
     2695| PUSH x_1247 -> h_PUSH x_1247
     2696| POP x_1248 -> h_POP x_1248
     2697| XCH (x_1250, x_1249) -> h_XCH x_1250 x_1249
     2698| XCHD (x_1252, x_1251) -> h_XCHD x_1252 x_1251
    26992699| RET -> h_RET
    27002700| RETI -> h_RETI
    27012701| NOP -> h_NOP
    2702 | JMP x_2221 -> h_JMP x_2221
     2702| JMP x_1253 -> h_JMP x_1253
    27032703
    27042704(** val preinstruction_inv_rect_Type4 :
     
    51045104    'a1 **)
    51055105let rec instruction_rect_Type4 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5106 | ACALL x_2793 -> h_ACALL x_2793
    5107 | LCALL x_2794 -> h_LCALL x_2794
    5108 | AJMP x_2795 -> h_AJMP x_2795
    5109 | LJMP x_2796 -> h_LJMP x_2796
    5110 | SJMP x_2797 -> h_SJMP x_2797
    5111 | MOVC (x_2799, x_2798) -> h_MOVC x_2799 x_2798
    5112 | RealInstruction x_2800 -> h_RealInstruction x_2800
     5106| ACALL x_1825 -> h_ACALL x_1825
     5107| LCALL x_1826 -> h_LCALL x_1826
     5108| AJMP x_1827 -> h_AJMP x_1827
     5109| LJMP x_1828 -> h_LJMP x_1828
     5110| SJMP x_1829 -> h_SJMP x_1829
     5111| MOVC (x_1831, x_1830) -> h_MOVC x_1831 x_1830
     5112| RealInstruction x_1832 -> h_RealInstruction x_1832
    51135113
    51145114(** val instruction_rect_Type5 :
     
    51195119    'a1 **)
    51205120let rec instruction_rect_Type5 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5121 | ACALL x_2809 -> h_ACALL x_2809
    5122 | LCALL x_2810 -> h_LCALL x_2810
    5123 | AJMP x_2811 -> h_AJMP x_2811
    5124 | LJMP x_2812 -> h_LJMP x_2812
    5125 | SJMP x_2813 -> h_SJMP x_2813
    5126 | MOVC (x_2815, x_2814) -> h_MOVC x_2815 x_2814
    5127 | RealInstruction x_2816 -> h_RealInstruction x_2816
     5121| ACALL x_1841 -> h_ACALL x_1841
     5122| LCALL x_1842 -> h_LCALL x_1842
     5123| AJMP x_1843 -> h_AJMP x_1843
     5124| LJMP x_1844 -> h_LJMP x_1844
     5125| SJMP x_1845 -> h_SJMP x_1845
     5126| MOVC (x_1847, x_1846) -> h_MOVC x_1847 x_1846
     5127| RealInstruction x_1848 -> h_RealInstruction x_1848
    51285128
    51295129(** val instruction_rect_Type3 :
     
    51345134    'a1 **)
    51355135let rec instruction_rect_Type3 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5136 | ACALL x_2825 -> h_ACALL x_2825
    5137 | LCALL x_2826 -> h_LCALL x_2826
    5138 | AJMP x_2827 -> h_AJMP x_2827
    5139 | LJMP x_2828 -> h_LJMP x_2828
    5140 | SJMP x_2829 -> h_SJMP x_2829
    5141 | MOVC (x_2831, x_2830) -> h_MOVC x_2831 x_2830
    5142 | RealInstruction x_2832 -> h_RealInstruction x_2832
     5136| ACALL x_1857 -> h_ACALL x_1857
     5137| LCALL x_1858 -> h_LCALL x_1858
     5138| AJMP x_1859 -> h_AJMP x_1859
     5139| LJMP x_1860 -> h_LJMP x_1860
     5140| SJMP x_1861 -> h_SJMP x_1861
     5141| MOVC (x_1863, x_1862) -> h_MOVC x_1863 x_1862
     5142| RealInstruction x_1864 -> h_RealInstruction x_1864
    51435143
    51445144(** val instruction_rect_Type2 :
     
    51495149    'a1 **)
    51505150let rec instruction_rect_Type2 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5151 | ACALL x_2841 -> h_ACALL x_2841
    5152 | LCALL x_2842 -> h_LCALL x_2842
    5153 | AJMP x_2843 -> h_AJMP x_2843
    5154 | LJMP x_2844 -> h_LJMP x_2844
    5155 | SJMP x_2845 -> h_SJMP x_2845
    5156 | MOVC (x_2847, x_2846) -> h_MOVC x_2847 x_2846
    5157 | RealInstruction x_2848 -> h_RealInstruction x_2848
     5151| ACALL x_1873 -> h_ACALL x_1873
     5152| LCALL x_1874 -> h_LCALL x_1874
     5153| AJMP x_1875 -> h_AJMP x_1875
     5154| LJMP x_1876 -> h_LJMP x_1876
     5155| SJMP x_1877 -> h_SJMP x_1877
     5156| MOVC (x_1879, x_1878) -> h_MOVC x_1879 x_1878
     5157| RealInstruction x_1880 -> h_RealInstruction x_1880
    51585158
    51595159(** val instruction_rect_Type1 :
     
    51645164    'a1 **)
    51655165let rec instruction_rect_Type1 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5166 | ACALL x_2857 -> h_ACALL x_2857
    5167 | LCALL x_2858 -> h_LCALL x_2858
    5168 | AJMP x_2859 -> h_AJMP x_2859
    5169 | LJMP x_2860 -> h_LJMP x_2860
    5170 | SJMP x_2861 -> h_SJMP x_2861
    5171 | MOVC (x_2863, x_2862) -> h_MOVC x_2863 x_2862
    5172 | RealInstruction x_2864 -> h_RealInstruction x_2864
     5166| ACALL x_1889 -> h_ACALL x_1889
     5167| LCALL x_1890 -> h_LCALL x_1890
     5168| AJMP x_1891 -> h_AJMP x_1891
     5169| LJMP x_1892 -> h_LJMP x_1892
     5170| SJMP x_1893 -> h_SJMP x_1893
     5171| MOVC (x_1895, x_1894) -> h_MOVC x_1895 x_1894
     5172| RealInstruction x_1896 -> h_RealInstruction x_1896
    51735173
    51745174(** val instruction_rect_Type0 :
     
    51795179    'a1 **)
    51805180let rec instruction_rect_Type0 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5181 | ACALL x_2873 -> h_ACALL x_2873
    5182 | LCALL x_2874 -> h_LCALL x_2874
    5183 | AJMP x_2875 -> h_AJMP x_2875
    5184 | LJMP x_2876 -> h_LJMP x_2876
    5185 | SJMP x_2877 -> h_SJMP x_2877
    5186 | MOVC (x_2879, x_2878) -> h_MOVC x_2879 x_2878
    5187 | RealInstruction x_2880 -> h_RealInstruction x_2880
     5181| ACALL x_1905 -> h_ACALL x_1905
     5182| LCALL x_1906 -> h_LCALL x_1906
     5183| AJMP x_1907 -> h_AJMP x_1907
     5184| LJMP x_1908 -> h_LJMP x_1908
     5185| SJMP x_1909 -> h_SJMP x_1909
     5186| MOVC (x_1911, x_1910) -> h_MOVC x_1911 x_1910
     5187| RealInstruction x_1912 -> h_RealInstruction x_1912
    51885188
    51895189(** val instruction_inv_rect_Type4 :
     
    54765476    -> 'a1 **)
    54775477let rec pseudo_instruction_rect_Type4 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5478 | Instruction x_3046 -> h_Instruction x_3046
    5479 | Comment x_3047 -> h_Comment x_3047
    5480 | Cost x_3048 -> h_Cost x_3048
    5481 | Jmp x_3049 -> h_Jmp x_3049
    5482 | Jnz (x_3052, x_3051, x_3050) -> h_Jnz x_3052 x_3051 x_3050
    5483 | MovSuccessor (x_3055, x_3054, x_3053) ->
    5484   h_MovSuccessor x_3055 x_3054 x_3053
    5485 | Call x_3056 -> h_Call x_3056
    5486 | Mov (x_3058, x_3057) -> h_Mov x_3058 x_3057
     5478| Instruction x_2078 -> h_Instruction x_2078
     5479| Comment x_2079 -> h_Comment x_2079
     5480| Cost x_2080 -> h_Cost x_2080
     5481| Jmp x_2081 -> h_Jmp x_2081
     5482| Jnz (x_2084, x_2083, x_2082) -> h_Jnz x_2084 x_2083 x_2082
     5483| MovSuccessor (x_2087, x_2086, x_2085) ->
     5484  h_MovSuccessor x_2087 x_2086 x_2085
     5485| Call x_2088 -> h_Call x_2088
     5486| Mov (x_2090, x_2089) -> h_Mov x_2090 x_2089
    54875487
    54885488(** val pseudo_instruction_rect_Type5 :
     
    54945494    -> 'a1 **)
    54955495let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5496 | Instruction x_3068 -> h_Instruction x_3068
    5497 | Comment x_3069 -> h_Comment x_3069
    5498 | Cost x_3070 -> h_Cost x_3070
    5499 | Jmp x_3071 -> h_Jmp x_3071
    5500 | Jnz (x_3074, x_3073, x_3072) -> h_Jnz x_3074 x_3073 x_3072
    5501 | MovSuccessor (x_3077, x_3076, x_3075) ->
    5502   h_MovSuccessor x_3077 x_3076 x_3075
    5503 | Call x_3078 -> h_Call x_3078
    5504 | Mov (x_3080, x_3079) -> h_Mov x_3080 x_3079
     5496| Instruction x_2100 -> h_Instruction x_2100
     5497| Comment x_2101 -> h_Comment x_2101
     5498| Cost x_2102 -> h_Cost x_2102
     5499| Jmp x_2103 -> h_Jmp x_2103
     5500| Jnz (x_2106, x_2105, x_2104) -> h_Jnz x_2106 x_2105 x_2104
     5501| MovSuccessor (x_2109, x_2108, x_2107) ->
     5502  h_MovSuccessor x_2109 x_2108 x_2107
     5503| Call x_2110 -> h_Call x_2110
     5504| Mov (x_2112, x_2111) -> h_Mov x_2112 x_2111
    55055505
    55065506(** val pseudo_instruction_rect_Type3 :
     
    55125512    -> 'a1 **)
    55135513let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5514 | Instruction x_3090 -> h_Instruction x_3090
    5515 | Comment x_3091 -> h_Comment x_3091
    5516 | Cost x_3092 -> h_Cost x_3092
    5517 | Jmp x_3093 -> h_Jmp x_3093
    5518 | Jnz (x_3096, x_3095, x_3094) -> h_Jnz x_3096 x_3095 x_3094
    5519 | MovSuccessor (x_3099, x_3098, x_3097) ->
    5520   h_MovSuccessor x_3099 x_3098 x_3097
    5521 | Call x_3100 -> h_Call x_3100
    5522 | Mov (x_3102, x_3101) -> h_Mov x_3102 x_3101
     5514| Instruction x_2122 -> h_Instruction x_2122
     5515| Comment x_2123 -> h_Comment x_2123
     5516| Cost x_2124 -> h_Cost x_2124
     5517| Jmp x_2125 -> h_Jmp x_2125
     5518| Jnz (x_2128, x_2127, x_2126) -> h_Jnz x_2128 x_2127 x_2126
     5519| MovSuccessor (x_2131, x_2130, x_2129) ->
     5520  h_MovSuccessor x_2131 x_2130 x_2129
     5521| Call x_2132 -> h_Call x_2132
     5522| Mov (x_2134, x_2133) -> h_Mov x_2134 x_2133
    55235523
    55245524(** val pseudo_instruction_rect_Type2 :
     
    55305530    -> 'a1 **)
    55315531let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5532 | Instruction x_3112 -> h_Instruction x_3112
    5533 | Comment x_3113 -> h_Comment x_3113
    5534 | Cost x_3114 -> h_Cost x_3114
    5535 | Jmp x_3115 -> h_Jmp x_3115
    5536 | Jnz (x_3118, x_3117, x_3116) -> h_Jnz x_3118 x_3117 x_3116
    5537 | MovSuccessor (x_3121, x_3120, x_3119) ->
    5538   h_MovSuccessor x_3121 x_3120 x_3119
    5539 | Call x_3122 -> h_Call x_3122
    5540 | Mov (x_3124, x_3123) -> h_Mov x_3124 x_3123
     5532| Instruction x_2144 -> h_Instruction x_2144
     5533| Comment x_2145 -> h_Comment x_2145
     5534| Cost x_2146 -> h_Cost x_2146
     5535| Jmp x_2147 -> h_Jmp x_2147
     5536| Jnz (x_2150, x_2149, x_2148) -> h_Jnz x_2150 x_2149 x_2148
     5537| MovSuccessor (x_2153, x_2152, x_2151) ->
     5538  h_MovSuccessor x_2153 x_2152 x_2151
     5539| Call x_2154 -> h_Call x_2154
     5540| Mov (x_2156, x_2155) -> h_Mov x_2156 x_2155
    55415541
    55425542(** val pseudo_instruction_rect_Type1 :
     
    55485548    -> 'a1 **)
    55495549let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5550 | Instruction x_3134 -> h_Instruction x_3134
    5551 | Comment x_3135 -> h_Comment x_3135
    5552 | Cost x_3136 -> h_Cost x_3136
    5553 | Jmp x_3137 -> h_Jmp x_3137
    5554 | Jnz (x_3140, x_3139, x_3138) -> h_Jnz x_3140 x_3139 x_3138
    5555 | MovSuccessor (x_3143, x_3142, x_3141) ->
    5556   h_MovSuccessor x_3143 x_3142 x_3141
    5557 | Call x_3144 -> h_Call x_3144
    5558 | Mov (x_3146, x_3145) -> h_Mov x_3146 x_3145
     5550| Instruction x_2166 -> h_Instruction x_2166
     5551| Comment x_2167 -> h_Comment x_2167
     5552| Cost x_2168 -> h_Cost x_2168
     5553| Jmp x_2169 -> h_Jmp x_2169
     5554| Jnz (x_2172, x_2171, x_2170) -> h_Jnz x_2172 x_2171 x_2170
     5555| MovSuccessor (x_2175, x_2174, x_2173) ->
     5556  h_MovSuccessor x_2175 x_2174 x_2173
     5557| Call x_2176 -> h_Call x_2176
     5558| Mov (x_2178, x_2177) -> h_Mov x_2178 x_2177
    55595559
    55605560(** val pseudo_instruction_rect_Type0 :
     
    55665566    -> 'a1 **)
    55675567let rec pseudo_instruction_rect_Type0 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5568 | Instruction x_3156 -> h_Instruction x_3156
    5569 | Comment x_3157 -> h_Comment x_3157
    5570 | Cost x_3158 -> h_Cost x_3158
    5571 | Jmp x_3159 -> h_Jmp x_3159
    5572 | Jnz (x_3162, x_3161, x_3160) -> h_Jnz x_3162 x_3161 x_3160
    5573 | MovSuccessor (x_3165, x_3164, x_3163) ->
    5574   h_MovSuccessor x_3165 x_3164 x_3163
    5575 | Call x_3166 -> h_Call x_3166
    5576 | Mov (x_3168, x_3167) -> h_Mov x_3168 x_3167
     5568| Instruction x_2188 -> h_Instruction x_2188
     5569| Comment x_2189 -> h_Comment x_2189
     5570| Cost x_2190 -> h_Cost x_2190
     5571| Jmp x_2191 -> h_Jmp x_2191
     5572| Jnz (x_2194, x_2193, x_2192) -> h_Jnz x_2194 x_2193 x_2192
     5573| MovSuccessor (x_2197, x_2196, x_2195) ->
     5574  h_MovSuccessor x_2197 x_2196 x_2195
     5575| Call x_2198 -> h_Call x_2198
     5576| Mov (x_2200, x_2199) -> h_Mov x_2200 x_2199
    55775577
    55785578(** val pseudo_instruction_inv_rect_Type4 :
     
    57965796    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    57975797    pseudo_assembly_program -> 'a1 **)
    5798 let rec pseudo_assembly_program_rect_Type4 h_mk_pseudo_assembly_program x_3311 =
     5798let rec pseudo_assembly_program_rect_Type4 h_mk_pseudo_assembly_program x_2343 =
    57995799  let { preamble = preamble0; code = code0; renamed_symbols =
    5800     renamed_symbols0; final_label = final_label0 } = x_3311
     5800    renamed_symbols0; final_label = final_label0 } = x_2343
    58015801  in
    58025802  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    58085808    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    58095809    pseudo_assembly_program -> 'a1 **)
    5810 let rec pseudo_assembly_program_rect_Type5 h_mk_pseudo_assembly_program x_3313 =
     5810let rec pseudo_assembly_program_rect_Type5 h_mk_pseudo_assembly_program x_2345 =
    58115811  let { preamble = preamble0; code = code0; renamed_symbols =
    5812     renamed_symbols0; final_label = final_label0 } = x_3313
     5812    renamed_symbols0; final_label = final_label0 } = x_2345
    58135813  in
    58145814  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    58205820    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    58215821    pseudo_assembly_program -> 'a1 **)
    5822 let rec pseudo_assembly_program_rect_Type3 h_mk_pseudo_assembly_program x_3315 =
     5822let rec pseudo_assembly_program_rect_Type3 h_mk_pseudo_assembly_program x_2347 =
    58235823  let { preamble = preamble0; code = code0; renamed_symbols =
    5824     renamed_symbols0; final_label = final_label0 } = x_3315
     5824    renamed_symbols0; final_label = final_label0 } = x_2347
    58255825  in
    58265826  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    58325832    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    58335833    pseudo_assembly_program -> 'a1 **)
    5834 let rec pseudo_assembly_program_rect_Type2 h_mk_pseudo_assembly_program x_3317 =
     5834let rec pseudo_assembly_program_rect_Type2 h_mk_pseudo_assembly_program x_2349 =
    58355835  let { preamble = preamble0; code = code0; renamed_symbols =
    5836     renamed_symbols0; final_label = final_label0 } = x_3317
     5836    renamed_symbols0; final_label = final_label0 } = x_2349
    58375837  in
    58385838  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    58445844    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    58455845    pseudo_assembly_program -> 'a1 **)
    5846 let rec pseudo_assembly_program_rect_Type1 h_mk_pseudo_assembly_program x_3319 =
     5846let rec pseudo_assembly_program_rect_Type1 h_mk_pseudo_assembly_program x_2351 =
    58475847  let { preamble = preamble0; code = code0; renamed_symbols =
    5848     renamed_symbols0; final_label = final_label0 } = x_3319
     5848    renamed_symbols0; final_label = final_label0 } = x_2351
    58495849  in
    58505850  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    58565856    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
    58575857    pseudo_assembly_program -> 'a1 **)
    5858 let rec pseudo_assembly_program_rect_Type0 h_mk_pseudo_assembly_program x_3321 =
     5858let rec pseudo_assembly_program_rect_Type0 h_mk_pseudo_assembly_program x_2353 =
    58595859  let { preamble = preamble0; code = code0; renamed_symbols =
    5860     renamed_symbols0; final_label = final_label0 } = x_3321
     5860    renamed_symbols0; final_label = final_label0 } = x_2353
    58615861  in
    58625862  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     
    59335933type object_code = BitVector.byte List.list
    59345934
     5935(** val next :
     5936    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
     5937    (BitVector.word, BitVector.byte) Types.prod **)
     5938let next pmem pc =
     5939  { Types.fst =
     5940    (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5941      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5942      Nat.O)))))))))))))))) pc
     5943      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5944        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5945        Nat.O)))))))))))))))) (Nat.S Nat.O))); Types.snd =
     5946    (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5947      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5948      Nat.O)))))))))))))))) pc pmem
     5949      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5950        Nat.O)))))))))) }
     5951
     5952(** val load_code_memory0 :
     5953    object_code -> BitVector.byte BitVectorTrie.bitVectorTrie Types.sig0 **)
     5954let load_code_memory0 program =
     5955  (Types.pi1
     5956    (FoldStuff.foldl_strong program (fun prefix v tl _ i_mem ->
     5957      (let { Types.fst = i; Types.snd = mem } = Types.pi1 i_mem in
     5958      (fun _ -> { Types.fst = (Nat.S i); Types.snd =
     5959      (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5960        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5961        Nat.O))))))))))))))))
     5962        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5963          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5964          (Nat.S (Nat.S Nat.O)))))))))))))))) i) v mem) })) __) { Types.fst =
     5965      Nat.O; Types.snd = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S
     5966      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5967      (Nat.S (Nat.S Nat.O))))))))))))))))) })).Types.snd
     5968
     5969(** val load_code_memory :
     5970    object_code -> BitVector.byte BitVectorTrie.bitVectorTrie **)
     5971let load_code_memory program =
     5972  Types.pi1 (load_code_memory0 program)
     5973
    59355974type costlabel_map = CostLabel.costlabel BitVectorTrie.bitVectorTrie
    59365975
    59375976type symboltable_type = AST.ident BitVectorTrie.bitVectorTrie
    59385977
    5939 type labelled_object_code = { oc : object_code; costlabels : costlabel_map;
     5978type labelled_object_code = { oc : object_code;
     5979                              cm : BitVector.byte BitVectorTrie.bitVectorTrie;
     5980                              costlabels : costlabel_map;
    59405981                              symboltable : symboltable_type;
    59415982                              final_pc : BitVector.word }
    59425983
    59435984(** val labelled_object_code_rect_Type4 :
    5944     (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    5945     -> 'a1) -> labelled_object_code -> 'a1 **)
    5946 let rec labelled_object_code_rect_Type4 h_mk_labelled_object_code x_3337 =
    5947   let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
    5948     final_pc = final_pc0 } = x_3337
     5985    (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     5986    costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     5987    labelled_object_code -> 'a1 **)
     5988let rec labelled_object_code_rect_Type4 h_mk_labelled_object_code x_2369 =
     5989  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
     5990    symboltable0; final_pc = final_pc0 } = x_2369
    59495991  in
    5950   h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     5992  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
    59515993
    59525994(** val labelled_object_code_rect_Type5 :
    5953     (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    5954     -> 'a1) -> labelled_object_code -> 'a1 **)
    5955 let rec labelled_object_code_rect_Type5 h_mk_labelled_object_code x_3339 =
    5956   let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
    5957     final_pc = final_pc0 } = x_3339
     5995    (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     5996    costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     5997    labelled_object_code -> 'a1 **)
     5998let rec labelled_object_code_rect_Type5 h_mk_labelled_object_code x_2371 =
     5999  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
     6000    symboltable0; final_pc = final_pc0 } = x_2371
    59586001  in
    5959   h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     6002  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
    59606003
    59616004(** val labelled_object_code_rect_Type3 :
    5962     (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    5963     -> 'a1) -> labelled_object_code -> 'a1 **)
    5964 let rec labelled_object_code_rect_Type3 h_mk_labelled_object_code x_3341 =
    5965   let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
    5966     final_pc = final_pc0 } = x_3341
     6005    (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     6006    costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     6007    labelled_object_code -> 'a1 **)
     6008let rec labelled_object_code_rect_Type3 h_mk_labelled_object_code x_2373 =
     6009  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
     6010    symboltable0; final_pc = final_pc0 } = x_2373
    59676011  in
    5968   h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     6012  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
    59696013
    59706014(** val labelled_object_code_rect_Type2 :
    5971     (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    5972     -> 'a1) -> labelled_object_code -> 'a1 **)
    5973 let rec labelled_object_code_rect_Type2 h_mk_labelled_object_code x_3343 =
    5974   let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
    5975     final_pc = final_pc0 } = x_3343
     6015    (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     6016    costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     6017    labelled_object_code -> 'a1 **)
     6018let rec labelled_object_code_rect_Type2 h_mk_labelled_object_code x_2375 =
     6019  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
     6020    symboltable0; final_pc = final_pc0 } = x_2375
    59766021  in
    5977   h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     6022  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
    59786023
    59796024(** val labelled_object_code_rect_Type1 :
    5980     (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    5981     -> 'a1) -> labelled_object_code -> 'a1 **)
    5982 let rec labelled_object_code_rect_Type1 h_mk_labelled_object_code x_3345 =
    5983   let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
    5984     final_pc = final_pc0 } = x_3345
     6025    (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     6026    costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     6027    labelled_object_code -> 'a1 **)
     6028let rec labelled_object_code_rect_Type1 h_mk_labelled_object_code x_2377 =
     6029  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
     6030    symboltable0; final_pc = final_pc0 } = x_2377
    59856031  in
    5986   h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     6032  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
    59876033
    59886034(** val labelled_object_code_rect_Type0 :
    5989     (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    5990     -> 'a1) -> labelled_object_code -> 'a1 **)
    5991 let rec labelled_object_code_rect_Type0 h_mk_labelled_object_code x_3347 =
    5992   let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
    5993     final_pc = final_pc0 } = x_3347
     6035    (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     6036    costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     6037    labelled_object_code -> 'a1 **)
     6038let rec labelled_object_code_rect_Type0 h_mk_labelled_object_code x_2379 =
     6039  let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable =
     6040    symboltable0; final_pc = final_pc0 } = x_2379
    59946041  in
    5995   h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     6042  h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __
    59966043
    59976044(** val oc : labelled_object_code -> object_code **)
     
    59996046  xxx.oc
    60006047
     6048(** val cm :
     6049    labelled_object_code -> BitVector.byte BitVectorTrie.bitVectorTrie **)
     6050let rec cm xxx =
     6051  xxx.cm
     6052
    60016053(** val costlabels : labelled_object_code -> costlabel_map **)
    60026054let rec costlabels xxx =
     
    60126064
    60136065(** val labelled_object_code_inv_rect_Type4 :
    6014     labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
    6015     -> BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
     6066    labelled_object_code -> (object_code -> BitVector.byte
     6067    BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
     6068    BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
    60166069let labelled_object_code_inv_rect_Type4 hterm h1 =
    60176070  let hcut = labelled_object_code_rect_Type4 h1 hterm in hcut __
    60186071
    60196072(** val labelled_object_code_inv_rect_Type3 :
    6020     labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
    6021     -> BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
     6073    labelled_object_code -> (object_code -> BitVector.byte
     6074    BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
     6075    BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
    60226076let labelled_object_code_inv_rect_Type3 hterm h1 =
    60236077  let hcut = labelled_object_code_rect_Type3 h1 hterm in hcut __
    60246078
    60256079(** val labelled_object_code_inv_rect_Type2 :
    6026     labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
    6027     -> BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
     6080    labelled_object_code -> (object_code -> BitVector.byte
     6081    BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
     6082    BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
    60286083let labelled_object_code_inv_rect_Type2 hterm h1 =
    60296084  let hcut = labelled_object_code_rect_Type2 h1 hterm in hcut __
    60306085
    60316086(** val labelled_object_code_inv_rect_Type1 :
    6032     labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
    6033     -> BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
     6087    labelled_object_code -> (object_code -> BitVector.byte
     6088    BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
     6089    BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
    60346090let labelled_object_code_inv_rect_Type1 hterm h1 =
    60356091  let hcut = labelled_object_code_rect_Type1 h1 hterm in hcut __
    60366092
    60376093(** val labelled_object_code_inv_rect_Type0 :
    6038     labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
    6039     -> BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
     6094    labelled_object_code -> (object_code -> BitVector.byte
     6095    BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
     6096    BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
    60406097let labelled_object_code_inv_rect_Type0 hterm h1 =
    60416098  let hcut = labelled_object_code_rect_Type0 h1 hterm in hcut __
    6042 
    6043 (** val labelled_object_code_discr :
    6044     labelled_object_code -> labelled_object_code -> __ **)
    6045 let labelled_object_code_discr x y =
    6046   Logic.eq_rect_Type2 x
    6047     (let { oc = a0; costlabels = a1; symboltable = a2; final_pc = a3 } = x in
    6048     Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
    60496099
    60506100(** val labelled_object_code_jmdiscr :
     
    60526102let labelled_object_code_jmdiscr x y =
    60536103  Logic.eq_rect_Type2 x
    6054     (let { oc = a0; costlabels = a1; symboltable = a2; final_pc = a3 } = x in
    6055     Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
    6056 
     6104    (let { oc = a0; cm = a1; costlabels = a3; symboltable = a4; final_pc =
     6105       a5 } = x
     6106     in
     6107    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
     6108
  • extracted/aSM.mli

    r2773 r2999  
    12881288type object_code = BitVector.byte List.list
    12891289
     1290val next :
     1291  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
     1292  (BitVector.word, BitVector.byte) Types.prod
     1293
     1294val load_code_memory0 :
     1295  object_code -> BitVector.byte BitVectorTrie.bitVectorTrie Types.sig0
     1296
     1297val load_code_memory :
     1298  object_code -> BitVector.byte BitVectorTrie.bitVectorTrie
     1299
    12901300type costlabel_map = CostLabel.costlabel BitVectorTrie.bitVectorTrie
    12911301
    12921302type symboltable_type = AST.ident BitVectorTrie.bitVectorTrie
    12931303
    1294 type labelled_object_code = { oc : object_code; costlabels : costlabel_map;
     1304type labelled_object_code = { oc : object_code;
     1305                              cm : BitVector.byte BitVectorTrie.bitVectorTrie;
     1306                              costlabels : costlabel_map;
    12951307                              symboltable : symboltable_type;
    12961308                              final_pc : BitVector.word }
    12971309
    12981310val labelled_object_code_rect_Type4 :
    1299   (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    1300   -> 'a1) -> labelled_object_code -> 'a1
     1311  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     1312  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     1313  labelled_object_code -> 'a1
    13011314
    13021315val labelled_object_code_rect_Type5 :
    1303   (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    1304   -> 'a1) -> labelled_object_code -> 'a1
     1316  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     1317  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     1318  labelled_object_code -> 'a1
    13051319
    13061320val labelled_object_code_rect_Type3 :
    1307   (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    1308   -> 'a1) -> labelled_object_code -> 'a1
     1321  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     1322  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     1323  labelled_object_code -> 'a1
    13091324
    13101325val labelled_object_code_rect_Type2 :
    1311   (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    1312   -> 'a1) -> labelled_object_code -> 'a1
     1326  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     1327  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     1328  labelled_object_code -> 'a1
    13131329
    13141330val labelled_object_code_rect_Type1 :
    1315   (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    1316   -> 'a1) -> labelled_object_code -> 'a1
     1331  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     1332  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     1333  labelled_object_code -> 'a1
    13171334
    13181335val labelled_object_code_rect_Type0 :
    1319   (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
    1320   -> 'a1) -> labelled_object_code -> 'a1
     1336  (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
     1337  costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
     1338  labelled_object_code -> 'a1
    13211339
    13221340val oc : labelled_object_code -> object_code
    13231341
     1342val cm : labelled_object_code -> BitVector.byte BitVectorTrie.bitVectorTrie
     1343
    13241344val costlabels : labelled_object_code -> costlabel_map
    13251345
     
    13291349
    13301350val labelled_object_code_inv_rect_Type4 :
    1331   labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
    1332   -> BitVector.word -> __ -> __ -> 'a1) -> 'a1
     1351  labelled_object_code -> (object_code -> BitVector.byte
     1352  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
     1353  BitVector.word -> __ -> __ -> 'a1) -> 'a1
    13331354
    13341355val labelled_object_code_inv_rect_Type3 :
    1335   labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
    1336   -> BitVector.word -> __ -> __ -> 'a1) -> 'a1
     1356  labelled_object_code -> (object_code -> BitVector.byte
     1357  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
     1358  BitVector.word -> __ -> __ -> 'a1) -> 'a1
    13371359
    13381360val labelled_object_code_inv_rect_Type2 :
    1339   labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
    1340   -> BitVector.word -> __ -> __ -> 'a1) -> 'a1
     1361  labelled_object_code -> (object_code -> BitVector.byte
     1362  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
     1363  BitVector.word -> __ -> __ -> 'a1) -> 'a1
    13411364
    13421365val labelled_object_code_inv_rect_Type1 :
    1343   labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
    1344   -> BitVector.word -> __ -> __ -> 'a1) -> 'a1
     1366  labelled_object_code -> (object_code -> BitVector.byte
     1367  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
     1368  BitVector.word -> __ -> __ -> 'a1) -> 'a1
    13451369
    13461370val labelled_object_code_inv_rect_Type0 :
    1347   labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
    1348   -> BitVector.word -> __ -> __ -> 'a1) -> 'a1
    1349 
    1350 val labelled_object_code_discr :
    1351   labelled_object_code -> labelled_object_code -> __
     1371  labelled_object_code -> (object_code -> BitVector.byte
     1372  BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
     1373  BitVector.word -> __ -> __ -> 'a1) -> 'a1
    13521374
    13531375val labelled_object_code_jmdiscr :
  • extracted/aSMCosts.ml

    r2993 r2999  
    225225    ASM.labelled_object_code -> StructuredTraces.abstract_status **)
    226226let oC_abstract_status prog =
    227   let code_memory = Fetch.load_code_memory prog.ASM.oc in
    228227  { StructuredTraces.as_pc = AbstractStatus.word_deqset;
    229   StructuredTraces.as_pc_of =
    230   (Obj.magic (Status.program_counter code_memory));
    231   StructuredTraces.as_classify =
    232   (Obj.magic (AbstractStatus.oC_classify code_memory));
    233   StructuredTraces.as_label_of_pc = (fun pc ->
    234   BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    235     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    236     Nat.O)))))))))))))))) (Obj.magic pc) prog.ASM.costlabels);
    237   StructuredTraces.as_result = (fun st ->
    238   as_result_of_finaladdr code_memory (Obj.magic st) prog.ASM.final_pc);
    239   StructuredTraces.as_call_ident =
    240   (Obj.magic (oC_as_call_ident prog code_memory));
    241   StructuredTraces.as_tailcall_ident = (fun clearme ->
    242   let st = clearme in
    243   (match AbstractStatus.current_instruction code_memory (Obj.magic st) with
    244    | ASM.ACALL x ->
    245      (fun _ ->
    246        Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_call
    247          StructuredTraces.Cl_tailcall __)
    248    | ASM.LCALL x ->
    249      (fun _ ->
    250        Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_call
    251          StructuredTraces.Cl_tailcall __)
    252    | ASM.AJMP x ->
    253      (fun _ ->
    254        Obj.magic StructuredTraces.status_class_discr
    255          StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    256    | ASM.LJMP x ->
    257      (fun _ ->
    258        Obj.magic StructuredTraces.status_class_discr
    259          StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    260    | ASM.SJMP x ->
    261      (fun _ ->
    262        Obj.magic StructuredTraces.status_class_discr
    263          StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    264    | ASM.MOVC (x, y) ->
    265      (fun _ ->
    266        Obj.magic StructuredTraces.status_class_discr
    267          StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    268    | ASM.RealInstruction clearme0 ->
    269      (match clearme0 with
    270       | ASM.ADD (x, y) ->
    271         (fun _ ->
    272           Obj.magic StructuredTraces.status_class_discr
    273             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    274       | ASM.ADDC (x, y) ->
    275         (fun _ ->
    276           Obj.magic StructuredTraces.status_class_discr
    277             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    278       | ASM.SUBB (x, y) ->
    279         (fun _ ->
    280           Obj.magic StructuredTraces.status_class_discr
    281             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    282       | ASM.INC x ->
    283         (fun _ ->
    284           Obj.magic StructuredTraces.status_class_discr
    285             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    286       | ASM.DEC x ->
    287         (fun _ ->
    288           Obj.magic StructuredTraces.status_class_discr
    289             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    290       | ASM.MUL (x, y) ->
    291         (fun _ ->
    292           Obj.magic StructuredTraces.status_class_discr
    293             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    294       | ASM.DIV (x, y) ->
    295         (fun _ ->
    296           Obj.magic StructuredTraces.status_class_discr
    297             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    298       | ASM.DA x ->
    299         (fun _ ->
    300           Obj.magic StructuredTraces.status_class_discr
    301             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    302       | ASM.JC x ->
    303         (fun _ ->
    304           Obj.magic StructuredTraces.status_class_discr
    305             StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
    306       | ASM.JNC x ->
    307         (fun _ ->
    308           Obj.magic StructuredTraces.status_class_discr
    309             StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
    310       | ASM.JB (x, y) ->
    311         (fun _ ->
    312           Obj.magic StructuredTraces.status_class_discr
    313             StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
    314       | ASM.JNB (x, y) ->
    315         (fun _ ->
    316           Obj.magic StructuredTraces.status_class_discr
    317             StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
    318       | ASM.JBC (x, y) ->
    319         (fun _ ->
    320           Obj.magic StructuredTraces.status_class_discr
    321             StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
    322       | ASM.JZ x ->
    323         (fun _ ->
    324           Obj.magic StructuredTraces.status_class_discr
    325             StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
    326       | ASM.JNZ x ->
    327         (fun _ ->
    328           Obj.magic StructuredTraces.status_class_discr
    329             StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
    330       | ASM.CJNE (x, y) ->
    331         (fun _ ->
    332           Obj.magic StructuredTraces.status_class_discr
    333             StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
    334       | ASM.DJNZ (x, y) ->
    335         (fun _ ->
    336           Obj.magic StructuredTraces.status_class_discr
    337             StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
    338       | ASM.ANL x ->
    339         (fun _ ->
    340           Obj.magic StructuredTraces.status_class_discr
    341             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    342       | ASM.ORL x ->
    343         (fun _ ->
    344           Obj.magic StructuredTraces.status_class_discr
    345             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    346       | ASM.XRL x ->
    347         (fun _ ->
    348           Obj.magic StructuredTraces.status_class_discr
    349             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    350       | ASM.CLR x ->
    351         (fun _ ->
    352           Obj.magic StructuredTraces.status_class_discr
    353             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    354       | ASM.CPL x ->
    355         (fun _ ->
    356           Obj.magic StructuredTraces.status_class_discr
    357             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    358       | ASM.RL x ->
    359         (fun _ ->
    360           Obj.magic StructuredTraces.status_class_discr
    361             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    362       | ASM.RLC x ->
    363         (fun _ ->
    364           Obj.magic StructuredTraces.status_class_discr
    365             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    366       | ASM.RR x ->
    367         (fun _ ->
    368           Obj.magic StructuredTraces.status_class_discr
    369             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    370       | ASM.RRC x ->
    371         (fun _ ->
    372           Obj.magic StructuredTraces.status_class_discr
    373             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    374       | ASM.SWAP x ->
    375         (fun _ ->
    376           Obj.magic StructuredTraces.status_class_discr
    377             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    378       | ASM.MOV x ->
    379         (fun _ ->
    380           Obj.magic StructuredTraces.status_class_discr
    381             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    382       | ASM.MOVX x ->
    383         (fun _ ->
    384           Obj.magic StructuredTraces.status_class_discr
    385             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    386       | ASM.SETB x ->
    387         (fun _ ->
    388           Obj.magic StructuredTraces.status_class_discr
    389             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    390       | ASM.PUSH x ->
    391         (fun _ ->
    392           Obj.magic StructuredTraces.status_class_discr
    393             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    394       | ASM.POP x ->
    395         (fun _ ->
    396           Obj.magic StructuredTraces.status_class_discr
    397             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    398       | ASM.XCH (x, y) ->
    399         (fun _ ->
    400           Obj.magic StructuredTraces.status_class_discr
    401             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    402       | ASM.XCHD (x, y) ->
    403         (fun _ ->
    404           Obj.magic StructuredTraces.status_class_discr
    405             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    406       | ASM.RET ->
    407         (fun _ ->
    408           Obj.magic StructuredTraces.status_class_discr
    409             StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
    410       | ASM.RETI ->
    411         (fun _ ->
    412           Obj.magic StructuredTraces.status_class_discr
    413             StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
    414       | ASM.NOP ->
    415         (fun _ ->
    416           Obj.magic StructuredTraces.status_class_discr
    417             StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
    418       | ASM.JMP x ->
    419         (fun _ ->
    420           Obj.magic StructuredTraces.status_class_discr
    421             StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __))) __) }
     228    StructuredTraces.as_pc_of =
     229    (Obj.magic (Status.program_counter prog.ASM.cm));
     230    StructuredTraces.as_classify =
     231    (Obj.magic (AbstractStatus.oC_classify prog.ASM.cm));
     232    StructuredTraces.as_label_of_pc = (fun pc ->
     233    BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     234      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     235      Nat.O)))))))))))))))) (Obj.magic pc) prog.ASM.costlabels);
     236    StructuredTraces.as_result = (fun st ->
     237    as_result_of_finaladdr prog.ASM.cm (Obj.magic st) prog.ASM.final_pc);
     238    StructuredTraces.as_call_ident =
     239    (Obj.magic (oC_as_call_ident prog prog.ASM.cm));
     240    StructuredTraces.as_tailcall_ident = (fun clearme ->
     241    let st = clearme in
     242    (match AbstractStatus.current_instruction prog.ASM.cm (Obj.magic st) with
     243     | ASM.ACALL x ->
     244       (fun _ ->
     245         Obj.magic StructuredTraces.status_class_discr
     246           StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __)
     247     | ASM.LCALL x ->
     248       (fun _ ->
     249         Obj.magic StructuredTraces.status_class_discr
     250           StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __)
     251     | ASM.AJMP x ->
     252       (fun _ ->
     253         Obj.magic StructuredTraces.status_class_discr
     254           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     255     | ASM.LJMP x ->
     256       (fun _ ->
     257         Obj.magic StructuredTraces.status_class_discr
     258           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     259     | ASM.SJMP x ->
     260       (fun _ ->
     261         Obj.magic StructuredTraces.status_class_discr
     262           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     263     | ASM.MOVC (x, y) ->
     264       (fun _ ->
     265         Obj.magic StructuredTraces.status_class_discr
     266           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     267     | ASM.RealInstruction clearme0 ->
     268       (match clearme0 with
     269        | ASM.ADD (x, y) ->
     270          (fun _ ->
     271            Obj.magic StructuredTraces.status_class_discr
     272              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     273        | ASM.ADDC (x, y) ->
     274          (fun _ ->
     275            Obj.magic StructuredTraces.status_class_discr
     276              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     277        | ASM.SUBB (x, y) ->
     278          (fun _ ->
     279            Obj.magic StructuredTraces.status_class_discr
     280              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     281        | ASM.INC x ->
     282          (fun _ ->
     283            Obj.magic StructuredTraces.status_class_discr
     284              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     285        | ASM.DEC x ->
     286          (fun _ ->
     287            Obj.magic StructuredTraces.status_class_discr
     288              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     289        | ASM.MUL (x, y) ->
     290          (fun _ ->
     291            Obj.magic StructuredTraces.status_class_discr
     292              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     293        | ASM.DIV (x, y) ->
     294          (fun _ ->
     295            Obj.magic StructuredTraces.status_class_discr
     296              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     297        | ASM.DA x ->
     298          (fun _ ->
     299            Obj.magic StructuredTraces.status_class_discr
     300              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     301        | ASM.JC x ->
     302          (fun _ ->
     303            Obj.magic StructuredTraces.status_class_discr
     304              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     305        | ASM.JNC x ->
     306          (fun _ ->
     307            Obj.magic StructuredTraces.status_class_discr
     308              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     309        | ASM.JB (x, y) ->
     310          (fun _ ->
     311            Obj.magic StructuredTraces.status_class_discr
     312              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     313        | ASM.JNB (x, y) ->
     314          (fun _ ->
     315            Obj.magic StructuredTraces.status_class_discr
     316              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     317        | ASM.JBC (x, y) ->
     318          (fun _ ->
     319            Obj.magic StructuredTraces.status_class_discr
     320              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     321        | ASM.JZ x ->
     322          (fun _ ->
     323            Obj.magic StructuredTraces.status_class_discr
     324              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     325        | ASM.JNZ x ->
     326          (fun _ ->
     327            Obj.magic StructuredTraces.status_class_discr
     328              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     329        | ASM.CJNE (x, y) ->
     330          (fun _ ->
     331            Obj.magic StructuredTraces.status_class_discr
     332              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     333        | ASM.DJNZ (x, y) ->
     334          (fun _ ->
     335            Obj.magic StructuredTraces.status_class_discr
     336              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     337        | ASM.ANL x ->
     338          (fun _ ->
     339            Obj.magic StructuredTraces.status_class_discr
     340              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     341        | ASM.ORL x ->
     342          (fun _ ->
     343            Obj.magic StructuredTraces.status_class_discr
     344              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     345        | ASM.XRL x ->
     346          (fun _ ->
     347            Obj.magic StructuredTraces.status_class_discr
     348              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     349        | ASM.CLR x ->
     350          (fun _ ->
     351            Obj.magic StructuredTraces.status_class_discr
     352              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     353        | ASM.CPL x ->
     354          (fun _ ->
     355            Obj.magic StructuredTraces.status_class_discr
     356              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     357        | ASM.RL x ->
     358          (fun _ ->
     359            Obj.magic StructuredTraces.status_class_discr
     360              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     361        | ASM.RLC x ->
     362          (fun _ ->
     363            Obj.magic StructuredTraces.status_class_discr
     364              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     365        | ASM.RR x ->
     366          (fun _ ->
     367            Obj.magic StructuredTraces.status_class_discr
     368              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     369        | ASM.RRC x ->
     370          (fun _ ->
     371            Obj.magic StructuredTraces.status_class_discr
     372              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     373        | ASM.SWAP x ->
     374          (fun _ ->
     375            Obj.magic StructuredTraces.status_class_discr
     376              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     377        | ASM.MOV x ->
     378          (fun _ ->
     379            Obj.magic StructuredTraces.status_class_discr
     380              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     381        | ASM.MOVX x ->
     382          (fun _ ->
     383            Obj.magic StructuredTraces.status_class_discr
     384              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     385        | ASM.SETB x ->
     386          (fun _ ->
     387            Obj.magic StructuredTraces.status_class_discr
     388              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     389        | ASM.PUSH x ->
     390          (fun _ ->
     391            Obj.magic StructuredTraces.status_class_discr
     392              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     393        | ASM.POP x ->
     394          (fun _ ->
     395            Obj.magic StructuredTraces.status_class_discr
     396              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     397        | ASM.XCH (x, y) ->
     398          (fun _ ->
     399            Obj.magic StructuredTraces.status_class_discr
     400              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     401        | ASM.XCHD (x, y) ->
     402          (fun _ ->
     403            Obj.magic StructuredTraces.status_class_discr
     404              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     405        | ASM.RET ->
     406          (fun _ ->
     407            Obj.magic StructuredTraces.status_class_discr
     408              StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
     409        | ASM.RETI ->
     410          (fun _ ->
     411            Obj.magic StructuredTraces.status_class_discr
     412              StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
     413        | ASM.NOP ->
     414          (fun _ ->
     415            Obj.magic StructuredTraces.status_class_discr
     416              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     417        | ASM.JMP x ->
     418          (fun _ ->
     419            Obj.magic StructuredTraces.status_class_discr
     420              StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __))) __) }
    422421
    423422(** val trace_any_label_length :
     
    425424    Status.status -> Status.status -> StructuredTraces.trace_any_label ->
    426425    Nat.nat **)
    427 let trace_any_label_length prog =
    428   let code_memory = Fetch.load_code_memory prog.ASM.oc in
    429   (fun trace_ends_flag start_status final_status the_trace ->
     426let trace_any_label_length prog trace_ends_flag start_status final_status the_trace =
    430427  StructuredTraces.as_trace_any_label_length' (oC_abstract_status prog)
    431428    trace_ends_flag (Obj.magic start_status) (Obj.magic final_status)
    432     the_trace)
     429    the_trace
    433430
    434431(** val all_program_counter_list :
     
    448445let rec compute_paid_trace_any_label prog trace_ends_flag start_status final_status = function
    449446| StructuredTraces.Tal_base_not_return (the_status, x) ->
    450   Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
    451     (Obj.magic the_status)
     447  Interpret.current_instruction_cost prog.ASM.cm (Obj.magic the_status)
    452448| StructuredTraces.Tal_base_return (the_status, x) ->
    453   Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
    454     (Obj.magic the_status)
     449  Interpret.current_instruction_cost prog.ASM.cm (Obj.magic the_status)
    455450| StructuredTraces.Tal_base_call (pre_fun_call, start_fun_call, final, x2) ->
    456   Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
    457     (Obj.magic pre_fun_call)
     451  Interpret.current_instruction_cost prog.ASM.cm (Obj.magic pre_fun_call)
    458452| StructuredTraces.Tal_base_tailcall
    459453    (pre_fun_call, start_fun_call, final, x1) ->
    460   Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
    461     (Obj.magic pre_fun_call)
     454  Interpret.current_instruction_cost prog.ASM.cm (Obj.magic pre_fun_call)
    462455| StructuredTraces.Tal_step_call
    463456    (end_flag, pre_fun_call, start_fun_call, after_fun_call, final,
    464457     call_trace, final_trace) ->
    465458  let current_instruction_cost =
    466     Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
    467       (Obj.magic pre_fun_call)
     459    Interpret.current_instruction_cost prog.ASM.cm (Obj.magic pre_fun_call)
    468460  in
    469461  let final_trace_cost =
     
    475467    (end_flag, status_pre, status_init, status_end, tail_trace) ->
    476468  let current_instruction_cost =
    477     Interpret.current_instruction_cost (Fetch.load_code_memory prog.ASM.oc)
    478       (Obj.magic status_pre)
     469    Interpret.current_instruction_cost prog.ASM.cm (Obj.magic status_pre)
    479470  in
    480471  let tail_trace_cost =
     
    488479    Status.status -> Status.status -> StructuredTraces.trace_label_label ->
    489480    Nat.nat **)
    490 let compute_paid_trace_label_label prog =
    491   let code_memory = Fetch.load_code_memory prog.ASM.oc in
    492   (fun trace_ends_flag start_status final_status the_trace ->
    493   let StructuredTraces.Tll_base (ends_flag, initial, final, given_trace) =
    494     the_trace
    495   in
     481let compute_paid_trace_label_label prog trace_ends_flag start_status final_status = function
     482| StructuredTraces.Tll_base (ends_flag, initial, final, given_trace) ->
    496483  compute_paid_trace_any_label prog ends_flag (Obj.magic initial)
    497     (Obj.magic final) given_trace)
     484    (Obj.magic final) given_trace
    498485
    499486(** val block_cost' :
     
    501488    Nat.nat Types.sig0 **)
    502489let rec block_cost' prog program_counter' program_size first_time_around =
    503   let code_memory' = Fetch.load_code_memory prog.ASM.oc in
    504490  (match program_size with
    505491   | Nat.O -> (fun _ -> Nat.O)
    506492   | Nat.S program_size' ->
    507493     (fun _ ->
    508        (let { Types.fst = eta16; Types.snd = ticks } =
    509           Fetch.fetch (Fetch.load_code_memory prog.ASM.oc) program_counter'
     494       (let { Types.fst = eta24755; Types.snd = ticks } =
     495          Fetch.fetch prog.ASM.cm program_counter'
    510496        in
    511        let { Types.fst = instruction; Types.snd = program_counter'' } = eta16
     497       let { Types.fst = instruction; Types.snd = program_counter'' } =
     498         eta24755
    512499       in
    513500       (fun _ ->
  • extracted/assembly.ml

    r2905 r2999  
    28322832           Nat.O))))))))))))))))); Types.snd = List.Nil })
    28332833   in
    2834   (fun _ -> { ASM.oc = (List.reverse revcode); ASM.costlabels =
     2834  (fun _ ->
     2835  let code = List.reverse revcode in
     2836  { ASM.oc = code; ASM.cm = (ASM.load_code_memory code); ASM.costlabels =
    28352837  (BitVectorTrie.fold (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    28362838    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    28552857let ticks_of_instruction i =
    28562858  let trivial_code_memory = assembly1 i in
    2857   let trivial_status = Fetch.load_code_memory trivial_code_memory in
     2859  let trivial_status = ASM.load_code_memory trivial_code_memory in
    28582860  (Fetch.fetch trivial_status
    28592861    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
  • extracted/fetch.ml

    r2997 r2999  
    9898  (Types.pi1
    9999    (FoldStuff.foldl_strong program (fun prefix x tl _ labels_costs_ppc ->
    100       (let { Types.fst = eta24856; Types.snd = ppc } =
     100      (let { Types.fst = eta24592; Types.snd = ppc } =
    101101         Types.pi1 labels_costs_ppc
    102102       in
    103103      (fun _ ->
    104       (let { Types.fst = labels; Types.snd = costs } = eta24856 in
     104      (let { Types.fst = labels; Types.snd = costs } = eta24592 in
    105105      (fun _ ->
    106106      (let { Types.fst = label; Types.snd = instr } = x in
     
    159159    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    160160    Nat.O))))))))))))))))
    161 
    162 (** val next :
    163     BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
    164     (BitVector.word, BitVector.byte) Types.prod **)
    165 let next pmem pc =
    166   { Types.fst =
    167     (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    168       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    169       Nat.O)))))))))))))))) pc
    170       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    171         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    172         Nat.O)))))))))))))))) (Nat.S Nat.O))); Types.snd =
    173     (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    174       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    175       Nat.O)))))))))))))))) pc pmem
    176       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    177         Nat.O)))))))))) }
    178 
    179 (** val load_code_memory0 :
    180     ASM.object_code -> BitVector.byte BitVectorTrie.bitVectorTrie Types.sig0 **)
    181 let load_code_memory0 program =
    182   (Types.pi1
    183     (FoldStuff.foldl_strong program (fun prefix v tl _ i_mem ->
    184       (let { Types.fst = i; Types.snd = mem } = Types.pi1 i_mem in
    185       (fun _ -> { Types.fst = (Nat.S i); Types.snd =
    186       (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    187         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    188         Nat.O))))))))))))))))
    189         (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    190           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    191           (Nat.S (Nat.S Nat.O)))))))))))))))) i) v mem) })) __) { Types.fst =
    192       Nat.O; Types.snd = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S
    193       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    194       (Nat.S (Nat.S Nat.O))))))))))))))))) })).Types.snd
    195 
    196 (** val load_code_memory :
    197     ASM.object_code -> BitVector.byte BitVectorTrie.bitVectorTrie **)
    198 let load_code_memory program =
    199   Types.pi1 (load_code_memory0 program)
    200161
    201162(** val prod_inv_rect_Type0 :
     
    264225                       (match b6 with
    265226                        | Bool.True ->
    266                           prod_inv_rect_Type0 (next pmem pc)
     227                          prod_inv_rect_Type0 (ASM.next pmem pc)
    267228                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    268229                            (ASM.RealInstruction (ASM.MOV (Types.Inl
     
    291252                       (match b6 with
    292253                        | Bool.True ->
    293                           prod_inv_rect_Type0 (next pmem pc)
     254                          prod_inv_rect_Type0 (ASM.next pmem pc)
    294255                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    295256                            (ASM.ACALL (ASM.ADDR11
     
    341302                       (match b6 with
    342303                        | Bool.True ->
    343                           prod_inv_rect_Type0 (next pmem pc)
     304                          prod_inv_rect_Type0 (ASM.next pmem pc)
    344305                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    345306                            (ASM.RealInstruction (ASM.MOV (Types.Inl
     
    369330                       (match b6 with
    370331                        | Bool.True ->
    371                           prod_inv_rect_Type0 (next pmem pc)
     332                          prod_inv_rect_Type0 (ASM.next pmem pc)
    372333                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    373334                            (ASM.AJMP (ASM.ADDR11
     
    397358              (match b3 with
    398359               | Bool.True ->
    399                  prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
     360                 prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ ->
    400361                   { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.DJNZ
    401362                   ((ASM.REGISTER v4), (ASM.RELATIVE b10)))); Types.snd =
     
    422383                       (match b6 with
    423384                        | Bool.True ->
    424                           prod_inv_rect_Type0 (next pmem pc)
     385                          prod_inv_rect_Type0 (ASM.next pmem pc)
    425386                            (fun pc0 b10 _ ->
    426                             prod_inv_rect_Type0 (next pmem pc0)
     387                            prod_inv_rect_Type0 (ASM.next pmem pc0)
    427388                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    428389                              (ASM.RealInstruction (ASM.DJNZ ((ASM.DIRECT
     
    448409                            Types.snd = (Nat.S Nat.O) }
    449410                        | Bool.False ->
    450                           prod_inv_rect_Type0 (next pmem pc)
     411                          prod_inv_rect_Type0 (ASM.next pmem pc)
    451412                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    452413                            (ASM.RealInstruction (ASM.SETB (ASM.BIT_ADDR
     
    459420                       (match b6 with
    460421                        | Bool.True ->
    461                           prod_inv_rect_Type0 (next pmem pc)
     422                          prod_inv_rect_Type0 (ASM.next pmem pc)
    462423                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    463424                            (ASM.ACALL (ASM.ADDR11
     
    471432                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    472433                        | Bool.False ->
    473                           prod_inv_rect_Type0 (next pmem pc)
     434                          prod_inv_rect_Type0 (ASM.next pmem pc)
    474435                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    475436                            (ASM.RealInstruction (ASM.POP (ASM.DIRECT b10)));
     
    506467                       (match b6 with
    507468                        | Bool.True ->
    508                           prod_inv_rect_Type0 (next pmem pc)
     469                          prod_inv_rect_Type0 (ASM.next pmem pc)
    509470                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    510471                            (ASM.RealInstruction (ASM.XCH (ASM.ACC_A,
     
    530491                            Types.snd = (Nat.S Nat.O) }
    531492                        | Bool.False ->
    532                           prod_inv_rect_Type0 (next pmem pc)
     493                          prod_inv_rect_Type0 (ASM.next pmem pc)
    533494                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    534495                            (ASM.RealInstruction (ASM.CLR (ASM.BIT_ADDR
     
    541502                       (match b6 with
    542503                        | Bool.True ->
    543                           prod_inv_rect_Type0 (next pmem pc)
     504                          prod_inv_rect_Type0 (ASM.next pmem pc)
    544505                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    545506                            (ASM.AJMP (ASM.ADDR11
     
    553514                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    554515                        | Bool.False ->
    555                           prod_inv_rect_Type0 (next pmem pc)
     516                          prod_inv_rect_Type0 (ASM.next pmem pc)
    556517                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    557518                            (ASM.RealInstruction (ASM.PUSH (ASM.DIRECT
     
    574535              (match b3 with
    575536               | Bool.True ->
    576                  prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
    577                    prod_inv_rect_Type0 (next pmem pc0) (fun pc1 b20 _ ->
     537                 prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ ->
     538                   prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ ->
    578539                     { Types.fst = { Types.fst = (ASM.RealInstruction
    579540                     (ASM.CJNE ((Types.Inr { Types.fst = (ASM.REGISTER v4);
     
    591552                    (match b5 with
    592553                     | Bool.True ->
    593                        prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
    594                          prod_inv_rect_Type0 (next pmem pc0)
     554                       prod_inv_rect_Type0 (ASM.next pmem pc)
     555                         (fun pc0 b10 _ ->
     556                         prod_inv_rect_Type0 (ASM.next pmem pc0)
    595557                           (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    596558                           (ASM.RealInstruction (ASM.CJNE ((Types.Inr
     
    605567                       (match b6 with
    606568                        | Bool.True ->
    607                           prod_inv_rect_Type0 (next pmem pc)
     569                          prod_inv_rect_Type0 (ASM.next pmem pc)
    608570                            (fun pc0 b10 _ ->
    609                             prod_inv_rect_Type0 (next pmem pc0)
     571                            prod_inv_rect_Type0 (ASM.next pmem pc0)
    610572                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    611573                              (ASM.RealInstruction (ASM.CJNE ((Types.Inl
     
    615577                              Nat.O)) }))
    616578                        | Bool.False ->
    617                           prod_inv_rect_Type0 (next pmem pc)
     579                          prod_inv_rect_Type0 (ASM.next pmem pc)
    618580                            (fun pc0 b10 _ ->
    619                             prod_inv_rect_Type0 (next pmem pc0)
     581                            prod_inv_rect_Type0 (ASM.next pmem pc0)
    620582                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    621583                              (ASM.RealInstruction (ASM.CJNE ((Types.Inl
     
    638600                            Types.snd = (Nat.S Nat.O) }
    639601                        | Bool.False ->
    640                           prod_inv_rect_Type0 (next pmem pc)
     602                          prod_inv_rect_Type0 (ASM.next pmem pc)
    641603                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    642604                            (ASM.RealInstruction (ASM.CPL (ASM.BIT_ADDR
     
    649611                       (match b6 with
    650612                        | Bool.True ->
    651                           prod_inv_rect_Type0 (next pmem pc)
     613                          prod_inv_rect_Type0 (ASM.next pmem pc)
    652614                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    653615                            (ASM.ACALL (ASM.ADDR11
     
    661623                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    662624                        | Bool.False ->
    663                           prod_inv_rect_Type0 (next pmem pc)
     625                          prod_inv_rect_Type0 (ASM.next pmem pc)
    664626                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    665627                            (ASM.RealInstruction (ASM.ANL (Types.Inr
     
    673635              (match b3 with
    674636               | Bool.True ->
    675                  prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
     637                 prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ ->
    676638                   { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
    677639                   (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr
     
    690652                    (match b5 with
    691653                     | Bool.True ->
    692                        prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
    693                          { Types.fst = { Types.fst = (ASM.RealInstruction
    694                          (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl
    695                          (Types.Inr { Types.fst = (ASM.INDIRECT
    696                          (Vector.from_singl v6)); Types.snd = (ASM.DIRECT
    697                          b10) }))))))); Types.snd = pc0 }; Types.snd = (Nat.S
    698                          (Nat.S Nat.O)) })
     654                       prod_inv_rect_Type0 (ASM.next pmem pc)
     655                         (fun pc0 b10 _ -> { Types.fst = { Types.fst =
     656                         (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
     657                         (Types.Inl (Types.Inl (Types.Inr { Types.fst =
     658                         (ASM.INDIRECT (Vector.from_singl v6)); Types.snd =
     659                         (ASM.DIRECT b10) }))))))); Types.snd = pc0 };
     660                         Types.snd = (Nat.S (Nat.S Nat.O)) })
    699661                     | Bool.False ->
    700662                       { Types.fst = { Types.fst = (ASM.RealInstruction
     
    716678                            Types.snd = (Nat.S (Nat.S Nat.O)) }
    717679                        | Bool.False ->
    718                           prod_inv_rect_Type0 (next pmem pc)
     680                          prod_inv_rect_Type0 (ASM.next pmem pc)
    719681                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    720682                            (ASM.RealInstruction (ASM.MOV (Types.Inl
     
    728690                       (match b6 with
    729691                        | Bool.True ->
    730                           prod_inv_rect_Type0 (next pmem pc)
     692                          prod_inv_rect_Type0 (ASM.next pmem pc)
    731693                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    732694                            (ASM.AJMP (ASM.ADDR11
     
    740702                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    741703                        | Bool.False ->
    742                           prod_inv_rect_Type0 (next pmem pc)
     704                          prod_inv_rect_Type0 (ASM.next pmem pc)
    743705                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    744706                            (ASM.RealInstruction (ASM.ORL (Types.Inr
     
    781743                       (match b6 with
    782744                        | Bool.True ->
    783                           prod_inv_rect_Type0 (next pmem pc)
     745                          prod_inv_rect_Type0 (ASM.next pmem pc)
    784746                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    785747                            (ASM.RealInstruction (ASM.SUBB (ASM.ACC_A,
     
    787749                            Types.snd = (Nat.S Nat.O) })
    788750                        | Bool.False ->
    789                           prod_inv_rect_Type0 (next pmem pc)
     751                          prod_inv_rect_Type0 (ASM.next pmem pc)
    790752                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    791753                            (ASM.RealInstruction (ASM.SUBB (ASM.ACC_A,
     
    807769                            (Nat.S (Nat.S Nat.O)) }
    808770                        | Bool.False ->
    809                           prod_inv_rect_Type0 (next pmem pc)
     771                          prod_inv_rect_Type0 (ASM.next pmem pc)
    810772                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    811773                            (ASM.RealInstruction (ASM.MOV (Types.Inr
     
    819781                       (match b6 with
    820782                        | Bool.True ->
    821                           prod_inv_rect_Type0 (next pmem pc)
     783                          prod_inv_rect_Type0 (ASM.next pmem pc)
    822784                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    823785                            (ASM.ACALL (ASM.ADDR11
     
    831793                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    832794                        | Bool.False ->
    833                           prod_inv_rect_Type0 (next pmem pc)
     795                          prod_inv_rect_Type0 (ASM.next pmem pc)
    834796                            (fun pc0 b10 _ ->
    835                             prod_inv_rect_Type0 (next pmem pc0)
     797                            prod_inv_rect_Type0 (ASM.next pmem pc0)
    836798                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    837799                              (ASM.RealInstruction (ASM.MOV (Types.Inl
     
    850812              (match b3 with
    851813               | Bool.True ->
    852                  prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
     814                 prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ ->
    853815                   { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
    854816                   (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst =
     
    866828                    (match b5 with
    867829                     | Bool.True ->
    868                        prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
    869                          { Types.fst = { Types.fst = (ASM.RealInstruction
    870                          (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inr
    871                          { Types.fst = (ASM.DIRECT b10); Types.snd =
    872                          (ASM.INDIRECT (Vector.from_singl v6)) }))))));
    873                          Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S
    874                          Nat.O)) })
    875                      | Bool.False ->
    876                        let { Types.fst = b6; Types.snd = v7 } =
    877                          Vector.head Nat.O v6
    878                        in
    879                        (match b6 with
    880                         | Bool.True ->
    881                           prod_inv_rect_Type0 (next pmem pc)
     830                       prod_inv_rect_Type0 (ASM.next pmem pc)
     831                         (fun pc0 b10 _ -> { Types.fst = { Types.fst =
     832                         (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
     833                         (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT
     834                         b10); Types.snd = (ASM.INDIRECT
     835                         (Vector.from_singl v6)) })))))); Types.snd = pc0 };
     836                         Types.snd = (Nat.S (Nat.S Nat.O)) })
     837                     | Bool.False ->
     838                       let { Types.fst = b6; Types.snd = v7 } =
     839                         Vector.head Nat.O v6
     840                       in
     841                       (match b6 with
     842                        | Bool.True ->
     843                          prod_inv_rect_Type0 (ASM.next pmem pc)
    882844                            (fun pc0 b10 _ ->
    883                             prod_inv_rect_Type0 (next pmem pc0)
     845                            prod_inv_rect_Type0 (ASM.next pmem pc0)
    884846                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    885847                              (ASM.RealInstruction (ASM.MOV (Types.Inl
     
    908870                            (Nat.S (Nat.S Nat.O)) }
    909871                        | Bool.False ->
    910                           prod_inv_rect_Type0 (next pmem pc)
     872                          prod_inv_rect_Type0 (ASM.next pmem pc)
    911873                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    912874                            (ASM.RealInstruction (ASM.ANL (Types.Inr
     
    920882                       (match b6 with
    921883                        | Bool.True ->
    922                           prod_inv_rect_Type0 (next pmem pc)
     884                          prod_inv_rect_Type0 (ASM.next pmem pc)
    923885                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    924886                            (ASM.AJMP (ASM.ADDR11
     
    932894                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    933895                        | Bool.False ->
    934                           prod_inv_rect_Type0 (next pmem pc)
     896                          prod_inv_rect_Type0 (ASM.next pmem pc)
    935897                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    936898                            (ASM.SJMP (ASM.RELATIVE b10)); Types.snd = pc0 };
     
    957919              (match b3 with
    958920               | Bool.True ->
    959                  prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
     921                 prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ ->
    960922                   { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
    961923                   (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr
     
    974936                    (match b5 with
    975937                     | Bool.True ->
    976                        prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
    977                          { Types.fst = { Types.fst = (ASM.RealInstruction
    978                          (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl
    979                          (Types.Inr { Types.fst = (ASM.INDIRECT
    980                          (Vector.from_singl v6)); Types.snd = (ASM.DATA
    981                          b10) }))))))); Types.snd = pc0 }; Types.snd = (Nat.S
    982                          Nat.O) })
    983                      | Bool.False ->
    984                        let { Types.fst = b6; Types.snd = v7 } =
    985                          Vector.head Nat.O v6
    986                        in
    987                        (match b6 with
    988                         | Bool.True ->
    989                           prod_inv_rect_Type0 (next pmem pc)
     938                       prod_inv_rect_Type0 (ASM.next pmem pc)
     939                         (fun pc0 b10 _ -> { Types.fst = { Types.fst =
     940                         (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
     941                         (Types.Inl (Types.Inl (Types.Inr { Types.fst =
     942                         (ASM.INDIRECT (Vector.from_singl v6)); Types.snd =
     943                         (ASM.DATA b10) }))))))); Types.snd = pc0 };
     944                         Types.snd = (Nat.S Nat.O) })
     945                     | Bool.False ->
     946                       let { Types.fst = b6; Types.snd = v7 } =
     947                         Vector.head Nat.O v6
     948                       in
     949                       (match b6 with
     950                        | Bool.True ->
     951                          prod_inv_rect_Type0 (ASM.next pmem pc)
    990952                            (fun pc0 b10 _ ->
    991                             prod_inv_rect_Type0 (next pmem pc0)
     953                            prod_inv_rect_Type0 (ASM.next pmem pc0)
    992954                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    993955                              (ASM.RealInstruction (ASM.MOV (Types.Inl
     
    997959                              (Nat.S (Nat.S (Nat.S Nat.O))) }))
    998960                        | Bool.False ->
    999                           prod_inv_rect_Type0 (next pmem pc)
     961                          prod_inv_rect_Type0 (ASM.next pmem pc)
    1000962                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    1001963                            (ASM.RealInstruction (ASM.MOV (Types.Inl
     
    1019981                            Types.snd = (Nat.S (Nat.S Nat.O)) }
    1020982                        | Bool.False ->
    1021                           prod_inv_rect_Type0 (next pmem pc)
     983                          prod_inv_rect_Type0 (ASM.next pmem pc)
    1022984                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    1023985                            (ASM.RealInstruction (ASM.ORL (Types.Inr
     
    1031993                       (match b6 with
    1032994                        | Bool.True ->
    1033                           prod_inv_rect_Type0 (next pmem pc)
     995                          prod_inv_rect_Type0 (ASM.next pmem pc)
    1034996                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    1035997                            (ASM.ACALL (ASM.ADDR11
     
    10431005                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    10441006                        | Bool.False ->
    1045                           prod_inv_rect_Type0 (next pmem pc)
     1007                          prod_inv_rect_Type0 (ASM.next pmem pc)
    10461008                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    10471009                            (ASM.RealInstruction (ASM.JNZ (ASM.RELATIVE
     
    10801042                       (match b6 with
    10811043                        | Bool.True ->
    1082                           prod_inv_rect_Type0 (next pmem pc)
     1044                          prod_inv_rect_Type0 (ASM.next pmem pc)
    10831045                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    10841046                            (ASM.RealInstruction (ASM.XRL (Types.Inl
     
    10871049                            Nat.O) })
    10881050                        | Bool.False ->
    1089                           prod_inv_rect_Type0 (next pmem pc)
     1051                          prod_inv_rect_Type0 (ASM.next pmem pc)
    10901052                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    10911053                            (ASM.RealInstruction (ASM.XRL (Types.Inl
     
    11041066                       (match b6 with
    11051067                        | Bool.True ->
    1106                           prod_inv_rect_Type0 (next pmem pc)
     1068                          prod_inv_rect_Type0 (ASM.next pmem pc)
    11071069                            (fun pc0 b10 _ ->
    1108                             prod_inv_rect_Type0 (next pmem pc0)
     1070                            prod_inv_rect_Type0 (ASM.next pmem pc0)
    11091071                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    11101072                              (ASM.RealInstruction (ASM.XRL (Types.Inr
     
    11131075                              Types.snd = (Nat.S (Nat.S Nat.O)) }))
    11141076                        | Bool.False ->
    1115                           prod_inv_rect_Type0 (next pmem pc)
     1077                          prod_inv_rect_Type0 (ASM.next pmem pc)
    11161078                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    11171079                            (ASM.RealInstruction (ASM.XRL (Types.Inr
     
    11251087                       (match b6 with
    11261088                        | Bool.True ->
    1127                           prod_inv_rect_Type0 (next pmem pc)
     1089                          prod_inv_rect_Type0 (ASM.next pmem pc)
    11281090                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    11291091                            (ASM.AJMP (ASM.ADDR11
     
    11371099                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    11381100                        | Bool.False ->
    1139                           prod_inv_rect_Type0 (next pmem pc)
     1101                          prod_inv_rect_Type0 (ASM.next pmem pc)
    11401102                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    11411103                            (ASM.RealInstruction (ASM.JZ (ASM.RELATIVE
     
    11791141                       (match b6 with
    11801142                        | Bool.True ->
    1181                           prod_inv_rect_Type0 (next pmem pc)
     1143                          prod_inv_rect_Type0 (ASM.next pmem pc)
    11821144                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    11831145                            (ASM.RealInstruction (ASM.ANL (Types.Inl
     
    11861148                            Types.snd = (Nat.S Nat.O) })
    11871149                        | Bool.False ->
    1188                           prod_inv_rect_Type0 (next pmem pc)
     1150                          prod_inv_rect_Type0 (ASM.next pmem pc)
    11891151                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    11901152                            (ASM.RealInstruction (ASM.ANL (Types.Inl
     
    12031165                       (match b6 with
    12041166                        | Bool.True ->
    1205                           prod_inv_rect_Type0 (next pmem pc)
     1167                          prod_inv_rect_Type0 (ASM.next pmem pc)
    12061168                            (fun pc0 b10 _ ->
    1207                             prod_inv_rect_Type0 (next pmem pc0)
     1169                            prod_inv_rect_Type0 (ASM.next pmem pc0)
    12081170                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    12091171                              (ASM.RealInstruction (ASM.ANL (Types.Inl
     
    12121174                              pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))
    12131175                        | Bool.False ->
    1214                           prod_inv_rect_Type0 (next pmem pc)
     1176                          prod_inv_rect_Type0 (ASM.next pmem pc)
    12151177                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    12161178                            (ASM.RealInstruction (ASM.ANL (Types.Inl
     
    12241186                       (match b6 with
    12251187                        | Bool.True ->
    1226                           prod_inv_rect_Type0 (next pmem pc)
     1188                          prod_inv_rect_Type0 (ASM.next pmem pc)
    12271189                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    12281190                            (ASM.ACALL (ASM.ADDR11
     
    12361198                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    12371199                        | Bool.False ->
    1238                           prod_inv_rect_Type0 (next pmem pc)
     1200                          prod_inv_rect_Type0 (ASM.next pmem pc)
    12391201                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    12401202                            (ASM.RealInstruction (ASM.JNC (ASM.RELATIVE
     
    12731235                       (match b6 with
    12741236                        | Bool.True ->
    1275                           prod_inv_rect_Type0 (next pmem pc)
     1237                          prod_inv_rect_Type0 (ASM.next pmem pc)
    12761238                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    12771239                            (ASM.RealInstruction (ASM.ORL (Types.Inl
     
    12801242                            Types.snd = (Nat.S Nat.O) })
    12811243                        | Bool.False ->
    1282                           prod_inv_rect_Type0 (next pmem pc)
     1244                          prod_inv_rect_Type0 (ASM.next pmem pc)
    12831245                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    12841246                            (ASM.RealInstruction (ASM.ORL (Types.Inl
     
    12971259                       (match b6 with
    12981260                        | Bool.True ->
    1299                           prod_inv_rect_Type0 (next pmem pc)
     1261                          prod_inv_rect_Type0 (ASM.next pmem pc)
    13001262                            (fun pc0 b10 _ ->
    1301                             prod_inv_rect_Type0 (next pmem pc0)
     1263                            prod_inv_rect_Type0 (ASM.next pmem pc0)
    13021264                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    13031265                              (ASM.RealInstruction (ASM.ORL (Types.Inl
     
    13061268                              pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))
    13071269                        | Bool.False ->
    1308                           prod_inv_rect_Type0 (next pmem pc)
     1270                          prod_inv_rect_Type0 (ASM.next pmem pc)
    13091271                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    13101272                            (ASM.RealInstruction (ASM.ORL (Types.Inl
     
    13181280                       (match b6 with
    13191281                        | Bool.True ->
    1320                           prod_inv_rect_Type0 (next pmem pc)
     1282                          prod_inv_rect_Type0 (ASM.next pmem pc)
    13211283                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    13221284                            (ASM.AJMP (ASM.ADDR11
     
    13301292                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    13311293                        | Bool.False ->
    1332                           prod_inv_rect_Type0 (next pmem pc)
     1294                          prod_inv_rect_Type0 (ASM.next pmem pc)
    13331295                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    13341296                            (ASM.RealInstruction (ASM.JC (ASM.RELATIVE
     
    13751337                       (match b6 with
    13761338                        | Bool.True ->
    1377                           prod_inv_rect_Type0 (next pmem pc)
     1339                          prod_inv_rect_Type0 (ASM.next pmem pc)
    13781340                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    13791341                            (ASM.RealInstruction (ASM.ADDC (ASM.ACC_A,
     
    13811343                            Types.snd = (Nat.S Nat.O) })
    13821344                        | Bool.False ->
    1383                           prod_inv_rect_Type0 (next pmem pc)
     1345                          prod_inv_rect_Type0 (ASM.next pmem pc)
    13841346                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    13851347                            (ASM.RealInstruction (ASM.ADDC (ASM.ACC_A,
     
    14101372                       (match b6 with
    14111373                        | Bool.True ->
    1412                           prod_inv_rect_Type0 (next pmem pc)
     1374                          prod_inv_rect_Type0 (ASM.next pmem pc)
    14131375                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    14141376                            (ASM.ACALL (ASM.ADDR11
     
    14221384                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    14231385                        | Bool.False ->
    1424                           prod_inv_rect_Type0 (next pmem pc)
     1386                          prod_inv_rect_Type0 (ASM.next pmem pc)
    14251387                            (fun pc0 b10 _ ->
    1426                             prod_inv_rect_Type0 (next pmem pc0)
     1388                            prod_inv_rect_Type0 (ASM.next pmem pc0)
    14271389                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    14281390                              (ASM.RealInstruction (ASM.JNB ((ASM.BIT_ADDR
     
    14591421                       (match b6 with
    14601422                        | Bool.True ->
    1461                           prod_inv_rect_Type0 (next pmem pc)
     1423                          prod_inv_rect_Type0 (ASM.next pmem pc)
    14621424                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    14631425                            (ASM.RealInstruction (ASM.ADD (ASM.ACC_A,
     
    14651427                            Types.snd = (Nat.S Nat.O) })
    14661428                        | Bool.False ->
    1467                           prod_inv_rect_Type0 (next pmem pc)
     1429                          prod_inv_rect_Type0 (ASM.next pmem pc)
    14681430                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    14691431                            (ASM.RealInstruction (ASM.ADD (ASM.ACC_A,
     
    14941456                       (match b6 with
    14951457                        | Bool.True ->
    1496                           prod_inv_rect_Type0 (next pmem pc)
     1458                          prod_inv_rect_Type0 (ASM.next pmem pc)
    14971459                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    14981460                            (ASM.AJMP (ASM.ADDR11
     
    15061468                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    15071469                        | Bool.False ->
    1508                           prod_inv_rect_Type0 (next pmem pc)
     1470                          prod_inv_rect_Type0 (ASM.next pmem pc)
    15091471                            (fun pc0 b10 _ ->
    1510                             prod_inv_rect_Type0 (next pmem pc0)
     1472                            prod_inv_rect_Type0 (ASM.next pmem pc0)
    15111473                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    15121474                              (ASM.RealInstruction (ASM.JB ((ASM.BIT_ADDR
     
    15471509                       (match b6 with
    15481510                        | Bool.True ->
    1549                           prod_inv_rect_Type0 (next pmem pc)
     1511                          prod_inv_rect_Type0 (ASM.next pmem pc)
    15501512                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    15511513                            (ASM.RealInstruction (ASM.DEC (ASM.DIRECT b10)));
     
    15701532                            Types.snd = (Nat.S Nat.O) }
    15711533                        | Bool.False ->
    1572                           prod_inv_rect_Type0 (next pmem pc)
     1534                          prod_inv_rect_Type0 (ASM.next pmem pc)
    15731535                            (fun pc0 b10 _ ->
    1574                             prod_inv_rect_Type0 (next pmem pc0)
     1536                            prod_inv_rect_Type0 (ASM.next pmem pc0)
    15751537                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    15761538                              (ASM.LCALL (ASM.ADDR16
     
    15871549                       (match b6 with
    15881550                        | Bool.True ->
    1589                           prod_inv_rect_Type0 (next pmem pc)
     1551                          prod_inv_rect_Type0 (ASM.next pmem pc)
    15901552                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    15911553                            (ASM.ACALL (ASM.ADDR11
     
    15991561                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    16001562                        | Bool.False ->
    1601                           prod_inv_rect_Type0 (next pmem pc)
     1563                          prod_inv_rect_Type0 (ASM.next pmem pc)
    16021564                            (fun pc0 b10 _ ->
    1603                             prod_inv_rect_Type0 (next pmem pc0)
     1565                            prod_inv_rect_Type0 (ASM.next pmem pc0)
    16041566                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    16051567                              (ASM.RealInstruction (ASM.JBC ((ASM.BIT_ADDR
     
    16351597                       (match b6 with
    16361598                        | Bool.True ->
    1637                           prod_inv_rect_Type0 (next pmem pc)
     1599                          prod_inv_rect_Type0 (ASM.next pmem pc)
    16381600                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    16391601                            (ASM.RealInstruction (ASM.INC (ASM.DIRECT b10)));
     
    16581620                            Types.snd = (Nat.S Nat.O) }
    16591621                        | Bool.False ->
    1660                           prod_inv_rect_Type0 (next pmem pc)
     1622                          prod_inv_rect_Type0 (ASM.next pmem pc)
    16611623                            (fun pc0 b10 _ ->
    1662                             prod_inv_rect_Type0 (next pmem pc0)
     1624                            prod_inv_rect_Type0 (ASM.next pmem pc0)
    16631625                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    16641626                              (ASM.LJMP (ASM.ADDR16
     
    16751637                       (match b6 with
    16761638                        | Bool.True ->
    1677                           prod_inv_rect_Type0 (next pmem pc)
     1639                          prod_inv_rect_Type0 (ASM.next pmem pc)
    16781640                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    16791641                            (ASM.AJMP (ASM.ADDR11
     
    16951657    ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod **)
    16961658let fetch pmem pc =
    1697   let { Types.fst = word; Types.snd = byte } = next pmem pc in
     1659  let { Types.fst = word; Types.snd = byte } = ASM.next pmem pc in
    16981660  fetch0 pmem word byte
    16991661
  • extracted/fetch.mli

    r2773 r2999  
    9999val code_memory_size : Nat.nat
    100100
    101 val next :
    102   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
    103   (BitVector.word, BitVector.byte) Types.prod
    104 
    105 val load_code_memory0 :
    106   ASM.object_code -> BitVector.byte BitVectorTrie.bitVectorTrie Types.sig0
    107 
    108 val load_code_memory :
    109   ASM.object_code -> BitVector.byte BitVectorTrie.bitVectorTrie
    110 
    111101val prod_inv_rect_Type0 :
    112102  ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
  • extracted/interpret2.ml

    r2997 r2999  
    129129    (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
    130130let mk_trans_system_of_abstract_status s as_eval =
    131   { SmallstepExec.is_final = (fun x -> s.StructuredTraces.as_result);
     131  { SmallstepExec.is_final = (fun x -> StructuredTraces.as_result s);
    132132    SmallstepExec.step = (fun x status ->
    133133    let tr =
     
    158158    Measurable.pcs_labelled = (fun x st ->
    159159    Bool.notb (PositiveMap.is_none (StructuredTraces.as_label s st)));
    160     Measurable.pcs_classify = (fun x -> s.StructuredTraces.as_classify);
     160    Measurable.pcs_classify = (fun x -> StructuredTraces.as_classify s);
    161161    Measurable.pcs_callee = (fun x st _ ->
    162     s.StructuredTraces.as_call_ident st) }
     162    StructuredTraces.as_call_ident s st) }
    163163
    164164(** val oC_preclassified_system :
    165165    ASM.labelled_object_code -> Measurable.preclassified_system **)
    166166let oC_preclassified_system c =
    167   let lcm = Fetch.load_code_memory c.ASM.oc in
    168167  mk_preclassified_system_of_abstract_status (ASMCosts.oC_abstract_status c)
    169168    (fun st ->
    170169    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
    171       (Interpret.execute_1 lcm (Obj.magic st)))
    172     (Obj.magic (Status.initialise_status (Fetch.load_code_memory c.ASM.oc)))
     170      (Interpret.execute_1 c.ASM.cm (Obj.magic st)))
     171    (Obj.magic (Status.initialise_status c.ASM.cm))
    173172
    174173open Assembly
  • extracted/policy.ml

    r2962 r2999  
    9494let rec jump_expansion_internal program n =
    9595  let labels = PolicyFront.create_label_map (Types.pi1 program) in
    96   let rec aux res =
    97 prerr_endline "JEI_start";
    98    let { Types.fst = no_ch; Types.snd = z } = res in
    99     match z with
    100      | Types.None ->
    101        { Types.fst = Bool.False; Types.snd = Types.None }
    102      | Types.Some op ->
    103          match no_ch with
    104          | Bool.True -> res
    105          | Bool.False ->
    106            aux
    107             (Types.pi1
    108              (PolicyStep.jump_expansion_step program (Types.pi1 labels)
    109                op))
    110   in
    111    aux
    112     { Types.fst = Bool.False; Types.snd =
    113        (Types.pi1
    114          (PolicyFront.jump_expansion_start program (Types.pi1 labels))) }
    115 (*
    11696  (match n with
    11797   | Nat.O ->
     
    134114              Types.pi1
    135115                (PolicyStep.jump_expansion_step program (Types.pi1 labels)
    136                   op))) __)) __)) __*)
     116                  op))) __)) __)) __
    137117
    138118(** val measure_int :
  • extracted/status.ml

    r2997 r2999  
    8989    serialBufferType -> 'a1 **)
    9090let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
    91 | Eight x_3368 -> h_Eight x_3368
    92 | Nine (x_3370, x_3369) -> h_Nine x_3370 x_3369
     91| Eight x_2400 -> h_Eight x_2400
     92| Nine (x_2402, x_2401) -> h_Nine x_2402 x_2401
    9393
    9494(** val serialBufferType_rect_Type5 :
     
    9696    serialBufferType -> 'a1 **)
    9797let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
    98 | Eight x_3374 -> h_Eight x_3374
    99 | Nine (x_3376, x_3375) -> h_Nine x_3376 x_3375
     98| Eight x_2406 -> h_Eight x_2406
     99| Nine (x_2408, x_2407) -> h_Nine x_2408 x_2407
    100100
    101101(** val serialBufferType_rect_Type3 :
     
    103103    serialBufferType -> 'a1 **)
    104104let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
    105 | Eight x_3380 -> h_Eight x_3380
    106 | Nine (x_3382, x_3381) -> h_Nine x_3382 x_3381
     105| Eight x_2412 -> h_Eight x_2412
     106| Nine (x_2414, x_2413) -> h_Nine x_2414 x_2413
    107107
    108108(** val serialBufferType_rect_Type2 :
     
    110110    serialBufferType -> 'a1 **)
    111111let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
    112 | Eight x_3386 -> h_Eight x_3386
    113 | Nine (x_3388, x_3387) -> h_Nine x_3388 x_3387
     112| Eight x_2418 -> h_Eight x_2418
     113| Nine (x_2420, x_2419) -> h_Nine x_2420 x_2419
    114114
    115115(** val serialBufferType_rect_Type1 :
     
    117117    serialBufferType -> 'a1 **)
    118118let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
    119 | Eight x_3392 -> h_Eight x_3392
    120 | Nine (x_3394, x_3393) -> h_Nine x_3394 x_3393
     119| Eight x_2424 -> h_Eight x_2424
     120| Nine (x_2426, x_2425) -> h_Nine x_2426 x_2425
    121121
    122122(** val serialBufferType_rect_Type0 :
     
    124124    serialBufferType -> 'a1 **)
    125125let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
    126 | Eight x_3398 -> h_Eight x_3398
    127 | Nine (x_3400, x_3399) -> h_Nine x_3400 x_3399
     126| Eight x_2430 -> h_Eight x_2430
     127| Nine (x_2432, x_2431) -> h_Nine x_2432 x_2431
    128128
    129129(** val serialBufferType_inv_rect_Type4 :
     
    182182    -> 'a1) -> lineType -> 'a1 **)
    183183let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
    184 | P1 x_3447 -> h_P1 x_3447
    185 | P3 x_3448 -> h_P3 x_3448
    186 | SerialBuffer x_3449 -> h_SerialBuffer x_3449
     184| P1 x_2479 -> h_P1 x_2479
     185| P3 x_2480 -> h_P3 x_2480
     186| SerialBuffer x_2481 -> h_SerialBuffer x_2481
    187187
    188188(** val lineType_rect_Type5 :
     
    190190    -> 'a1) -> lineType -> 'a1 **)
    191191let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function
    192 | P1 x_3454 -> h_P1 x_3454
    193 | P3 x_3455 -> h_P3 x_3455
    194 | SerialBuffer x_3456 -> h_SerialBuffer x_3456
     192| P1 x_2486 -> h_P1 x_2486
     193| P3 x_2487 -> h_P3 x_2487
     194| SerialBuffer x_2488 -> h_SerialBuffer x_2488
    195195
    196196(** val lineType_rect_Type3 :
     
    198198    -> 'a1) -> lineType -> 'a1 **)
    199199let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function
    200 | P1 x_3461 -> h_P1 x_3461
    201 | P3 x_3462 -> h_P3 x_3462
    202 | SerialBuffer x_3463 -> h_SerialBuffer x_3463
     200| P1 x_2493 -> h_P1 x_2493
     201| P3 x_2494 -> h_P3 x_2494
     202| SerialBuffer x_2495 -> h_SerialBuffer x_2495
    203203
    204204(** val lineType_rect_Type2 :
     
    206206    -> 'a1) -> lineType -> 'a1 **)
    207207let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function
    208 | P1 x_3468 -> h_P1 x_3468
    209 | P3 x_3469 -> h_P3 x_3469
    210 | SerialBuffer x_3470 -> h_SerialBuffer x_3470
     208| P1 x_2500 -> h_P1 x_2500
     209| P3 x_2501 -> h_P3 x_2501
     210| SerialBuffer x_2502 -> h_SerialBuffer x_2502
    211211
    212212(** val lineType_rect_Type1 :
     
    214214    -> 'a1) -> lineType -> 'a1 **)
    215215let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function
    216 | P1 x_3475 -> h_P1 x_3475
    217 | P3 x_3476 -> h_P3 x_3476
    218 | SerialBuffer x_3477 -> h_SerialBuffer x_3477
     216| P1 x_2507 -> h_P1 x_2507
     217| P3 x_2508 -> h_P3 x_2508
     218| SerialBuffer x_2509 -> h_SerialBuffer x_2509
    219219
    220220(** val lineType_rect_Type0 :
     
    222222    -> 'a1) -> lineType -> 'a1 **)
    223223let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function
    224 | P1 x_3482 -> h_P1 x_3482
    225 | P3 x_3483 -> h_P3 x_3483
    226 | SerialBuffer x_3484 -> h_SerialBuffer x_3484
     224| P1 x_2514 -> h_P1 x_2514
     225| P3 x_2515 -> h_P3 x_2515
     226| SerialBuffer x_2516 -> h_SerialBuffer x_2516
    227227
    228228(** val lineType_inv_rect_Type4 :
     
    731731    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    732732    preStatus -> 'a2 **)
    733 let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_3870 =
     733let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_2902 =
    734734  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    735735    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    737737    special_function_registers_8053; special_function_registers_8052 =
    738738    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    739     p3_latch0; clock = clock0 } = x_3870
     739    p3_latch0; clock = clock0 } = x_2902
    740740  in
    741741  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    749749    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    750750    preStatus -> 'a2 **)
    751 let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_3872 =
     751let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_2904 =
    752752  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    753753    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    755755    special_function_registers_8053; special_function_registers_8052 =
    756756    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    757     p3_latch0; clock = clock0 } = x_3872
     757    p3_latch0; clock = clock0 } = x_2904
    758758  in
    759759  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    767767    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    768768    preStatus -> 'a2 **)
    769 let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_3874 =
     769let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_2906 =
    770770  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    771771    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    773773    special_function_registers_8053; special_function_registers_8052 =
    774774    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    775     p3_latch0; clock = clock0 } = x_3874
     775    p3_latch0; clock = clock0 } = x_2906
    776776  in
    777777  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    785785    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    786786    preStatus -> 'a2 **)
    787 let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_3876 =
     787let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_2908 =
    788788  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    789789    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    791791    special_function_registers_8053; special_function_registers_8052 =
    792792    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    793     p3_latch0; clock = clock0 } = x_3876
     793    p3_latch0; clock = clock0 } = x_2908
    794794  in
    795795  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    803803    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    804804    preStatus -> 'a2 **)
    805 let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_3878 =
     805let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_2910 =
    806806  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    807807    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    809809    special_function_registers_8053; special_function_registers_8052 =
    810810    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    811     p3_latch0; clock = clock0 } = x_3878
     811    p3_latch0; clock = clock0 } = x_2910
    812812  in
    813813  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    821821    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    822822    preStatus -> 'a2 **)
    823 let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_3880 =
     823let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_2912 =
    824824  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    825825    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    827827    special_function_registers_8053; special_function_registers_8052 =
    828828    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    829     p3_latch0; clock = clock0 } = x_3880
     829    p3_latch0; clock = clock0 } = x_2912
    830830  in
    831831  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
  • src/ASM/ASM.ma

    r2767 r2999  
    11561156}.
    11571157
    1158 definition object_code ≝ list Byte.
     1158definition object_code ≝ list Byte.
     1159
     1160include alias "ASM/BitVectorTrie.ma".
     1161include alias "ASM/Arithmetic.ma".
     1162
     1163definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝
     1164  λpmem: BitVectorTrie Byte 16.
     1165  λpc: Word.
     1166    〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
     1167
     1168definition load_code_memory0:
     1169 ∀program: object_code. Σres: BitVectorTrie Byte 16.
     1170  let program_size ≝ |program| in
     1171   program_size ≤ 2^16 →
     1172    ∀pc. ∀pc_ok: pc < program_size.
     1173     nth_safe ? pc program pc_ok = \snd (next res (bitvector_of_nat … pc))
     1174
     1175 λprogram. \snd
     1176  (foldl_strong ?
     1177   (λprefix.
     1178     Σres: nat × (BitVectorTrie Byte 16).
     1179      let 〈i,mem〉 ≝ res in
     1180      i = |prefix| ∧
     1181      (i ≤ 2^16 →
     1182        ∀pc. ∀pc_ok: pc < |prefix|.
     1183         nth_safe ? pc prefix pc_ok = \snd (next mem (bitvector_of_nat … pc))))
     1184   program
     1185   (λprefix,v,tl,prf,i_mem.
     1186     let 〈i,mem〉 ≝ i_mem in
     1187      〈S i,insert … (bitvector_of_nat … i) v mem〉)
     1188  〈0,Stub Byte 16〉).
     1189[3: cases (foldl_strong ? (λprefix.Σres.?) ???) * #i #mem * #H1 >H1 #H2 @H2
     1190| % // #_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))
     1191| cases i_mem in p; * #i' #mem' #H #EQ destruct(EQ) cases H -H #H1 #H2 %
     1192  [ >length_append >H1 normalize //
     1193  | #LE #pc #pc_ok
     1194    cases (le_to_or_lt_eq … pc_ok)
     1195    [2: #EQ_Spc >(?: pc = |prefix| + 0) in pc_ok;
     1196      [2: >length_append in EQ_Spc; normalize #EQ @injective_S >EQ //]
     1197      #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?);
     1198      <H1 <plus_n_O whd in ⊢ (???%); //
     1199    | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix [2: /2/]
     1200      >H2 [2: @(transitive_le … LE) //]
     1201      cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ
     1202      whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false %
     1203      #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption
     1204      @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]]
     1205qed.
     1206
     1207definition load_code_memory: object_code → BitVectorTrie Byte 16 ≝
     1208 λprogram.load_code_memory0 program.
     1209
     1210lemma load_code_memory_ok:
     1211 ∀program: object_code.
     1212  let program_size ≝ |program| in
     1213   program_size ≤ 2^16 →
     1214    ∀pc. ∀pc_ok: pc < program_size.
     1215     nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
     1216whd in match load_code_memory; normalize nodelta #program @pi2
     1217qed.
     1218
     1219
    11591220definition costlabel_map ≝ BitVectorTrie costlabel 16. (* XXX *)
    11601221definition symboltable_type ≝ BitVectorTrie ident 16.  (* XXX *)
    11611222record labelled_object_code : Type[0] ≝
    11621223{ oc : object_code
     1224; cm: BitVectorTrie Byte 16
     1225; cm_def: cm = load_code_memory oc
    11631226; costlabels : costlabel_map
    11641227; symboltable : symboltable_type
     
    11681231  partial_injection … (λpc.lookup_opt … pc costlabels)
    11691232}.
    1170 
    1171 
    1172 
  • src/ASM/ASMCosts.ma

    r2993 r2999  
    3737definition OC_abstract_status: labelled_object_code → abstract_status ≝
    3838 λprog.
    39   let code_memory ≝ load_code_memory (oc prog) in
    4039    mk_abstract_status
    41       (Status code_memory)
     40      (Status (cm prog))
    4241      (λs1,s2. execute_1 … s1 = s2)
    4342      word_deqset
    44       (program_counter … code_memory)
    45       (OC_classify code_memory)
     43      (program_counter …)
     44      (OC_classify )
    4645      (λpc.lookup_opt … pc (costlabels prog))
    47       (next_instruction_properly_relates_program_counters code_memory)
    48       (λst. as_result_of_finaladdr … code_memory … st (final_pc prog))
    49       (OC_as_call_ident prog code_memory)
     46      (next_instruction_properly_relates_program_counters )
     47      (λst. as_result_of_finaladdr … st (final_pc prog))
     48      (OC_as_call_ident prog )
    5049      ?.
    5150 * #st whd in ⊢ (??%? → ?); cases current_instruction [7: *] normalize
     
    5554definition trace_any_label_length ≝
    5655  λprog: labelled_object_code.
    57   let code_memory ≝ load_code_memory (oc prog) in
    5856  λtrace_ends_flag: trace_ends_with_ret.
    59   λstart_status: Status code_memory.
    60   λfinal_status: Status code_memory.
     57  λstart_status: Status (cm prog).
     58  λfinal_status: Status (cm prog).
    6159  λthe_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    6260    as_trace_any_label_length' … the_trace.
     
    178176lemma execute_1_and_program_counter_after_other_in_lockstep:
    179177  ∀prog: labelled_object_code.
    180   let code_memory ≝ load_code_memory (oc prog) in
    181   ∀start_status: Status code_memory.
     178  ∀start_status: Status (cm prog).
    182179    as_classifier (OC_abstract_status prog) start_status cl_other →
    183       let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
     180      let 〈instruction, pc, ticks〉 ≝ fetch (cm prog) (program_counter … start_status) in
    184181        program_counter ? ? (execute_1 … start_status) =
    185182          program_counter_after_other pc instruction.
     
    192189lemma sublist_tal_pc_list_all_program_counter_list:
    193190  ∀prog: labelled_object_code.
    194   let code_memory ≝ load_code_memory (oc prog) in
    195   ∀start, final: Status code_memory.
     191  ∀start, final: Status (cm prog).
    196192  ∀trace_ends_flag.
    197193  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final.
     
    205201corollary tal_pc_list_length_leq_total_program_size:
    206202  ∀prog: labelled_object_code.
    207   let code_memory ≝ load_code_memory (oc prog) in
    208   ∀start, final: Status code_memory.
     203  ∀start, final: Status (cm prog).
    209204  ∀trace_ends_flag.
    210205  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final.
     
    225220let rec compute_paid_trace_any_label
    226221  (prog: labelled_object_code) (trace_ends_flag: trace_ends_with_ret)
    227    (start_status: Status (load_code_memory (oc prog)))
    228    (final_status: Status (load_code_memory (oc prog)))
     222   (start_status: Status (cm prog))
     223   (final_status: Status (cm prog))
    229224        (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    230225       on the_trace: nat ≝
     
    250245definition compute_paid_trace_label_label ≝
    251246  λprog: labelled_object_code.
    252   let code_memory ≝ load_code_memory (oc prog) in
    253247  λtrace_ends_flag: trace_ends_with_ret.
    254   λstart_status: Status code_memory.
    255   λfinal_status: Status code_memory.
     248  λstart_status: Status (cm prog).
     249  λfinal_status: Status (cm prog).
    256250  λthe_trace: (trace_label_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
    257251  match the_trace with
     
    262256lemma trace_compute_paid_trace_cl_other:
    263257  ∀prog : labelled_object_code.
    264   let code_memory' ≝ load_code_memory (oc prog) in
    265258  ∀program_counter' : Word.
    266259  ∀program_size' : ℕ.
     
    268261  ∀instruction : instruction.
    269262  ∀program_counter'' : Word.
    270   ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
     263  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter').
    271264  let program_counter''' ≝ program_counter_after_other program_counter'' instruction in
    272   ∀start_status : (Status code_memory').
    273   ∀final_status : (Status code_memory').
     265  ∀start_status : (Status (cm prog)).
     266  ∀final_status : (Status (cm prog)).
    274267  ∀trace_ends_flag : trace_ends_with_ret.
    275268  ∀the_trace : (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
     
    283276         ] 
    284277    then
    285       ∀start_status0:Status code_memory'.
    286       ∀final_status0:Status code_memory'.
     278      ∀start_status0:Status (cm prog).
     279      ∀final_status0:Status (cm prog).
    287280      ∀trace_ends_flag0:trace_ends_with_ret.
    288281      ∀the_trace0:trace_any_label (OC_abstract_status prog) trace_ends_flag0 start_status0 final_status0.
     
    341334          end_flag trace_any_label ? ?) try (>rewrite_assm %)
    342335        whd in match (current_instruction_cost … status_pre);
    343         cut(ticks = \snd (fetch (load_code_memory (oc prog))
    344            (program_counter … status_pre)))
     336        cut(ticks = \snd (fetch (cm prog) (program_counter … status_pre)))
    345337        [1,3:
    346338          <FETCH %
     
    384376          #Some_lookup_opt_assm <Some_lookup_opt_assm
    385377          normalize nodelta #new_recursive_assm >new_recursive_assm
    386           cut(ticks = \snd (fetch (load_code_memory (oc prog))
    387              (program_counter … status_start)))
     378          cut(ticks = \snd (fetch (cm prog) (program_counter … status_start)))
    388379          [1:
    389380            <FETCH %
     
    420411lemma trace_compute_paid_trace_cl_jump:
    421412  ∀prog: labelled_object_code.
    422   let code_memory' ≝ load_code_memory (oc prog) in
    423413  ∀program_counter': Word.
    424414  ∀first_time_around: bool.
     
    427417  ∀instruction: instruction.
    428418  ∀program_counter'': Word.
    429   ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'.
    430   ∀start_status: (Status code_memory').
    431   ∀final_status: (Status code_memory').
     419  ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch (cm prog) program_counter'.
     420  ∀start_status: (Status (cm prog)).
     421  ∀final_status: (Status (cm prog)).
    432422  ∀trace_ends_flag: trace_ends_with_ret.
    433423  ∀the_trace: (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
     
    436426    ticks
    437427     =compute_paid_trace_any_label … the_trace.
    438   #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #first_time_around
     428  #prog #program_counter' #first_time_around
    439429  #program_size' #ticks #instruction #program_counter'' #FETCH
    440430  #start_status #final_status
     
    479469lemma trace_compute_paid_trace_cl_call:
    480470  ∀prog: labelled_object_code.
    481   let code_memory' ≝ load_code_memory (oc prog) in
    482471  ∀program_counter' : Word.
    483472  ∀program_size' : ℕ.
     
    485474  ∀instruction : instruction.
    486475  ∀program_counter'' : Word.
    487   ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
    488   ∀start_status : (Status code_memory').
    489   ∀final_status : (Status code_memory').
     476  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter').
     477  ∀start_status : (Status (cm prog)).
     478  ∀final_status : (Status (cm prog)).
    490479  ∀trace_ends_flag : trace_ends_with_ret.
    491480  ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
     
    496485  .if match lookup_opt costlabel 16 program_counter'' (costlabels prog) with 
    497486      [None ⇒ true | Some _ ⇒ false] 
    498    then (∀start_status0:Status code_memory'
    499              .∀final_status0:Status code_memory'
     487   then (∀start_status0:Status (cm prog)
     488             .∀final_status0:Status (cm prog)
    500489              .∀trace_ends_flag0:trace_ends_with_ret
    501490               .∀the_trace0:trace_any_label
     
    511500   → ticks+pi1
    512501     =compute_paid_trace_any_label … the_trace).
    513   #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #program_size'
     502  #prog #program_counter' #program_size'
    514503  #ticks #instruction #program_counter'' #FETCH
    515504  #start_status #final_status #trace_ends_flag
     
    555544        #program_counter_assm >program_counter_assm <Some_lookup_opt
    556545        normalize nodelta #new_recursive_assm >new_recursive_assm
    557         cut(ticks = \snd (fetch code_memory' (program_counter … status_pre_fun_call)))
     546        cut(ticks = \snd (fetch (cm prog) (program_counter … status_pre_fun_call)))
    558547        [1:
    559548          <FETCH %
     
    618607lemma trace_compute_paid_trace_cl_return:
    619608  ∀prog: labelled_object_code.
    620   let code_memory' ≝ load_code_memory (oc prog) in
    621609  ∀program_counter' : Word.
    622610  ∀program_size' : ℕ.
     
    624612  ∀instruction : instruction.
    625613  ∀program_counter'' : Word.
    626   ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
    627   ∀start_status : (Status code_memory').
    628   ∀final_status : (Status code_memory').
     614  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter').
     615  ∀start_status : (Status (cm prog)).
     616  ∀final_status : (Status (cm prog)).
    629617  ∀trace_ends_flag : trace_ends_with_ret.
    630618  ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
     
    633621    ticks
    634622     =compute_paid_trace_any_label … the_trace.
    635   #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #program_size'
     623  #prog #program_counter' #program_size'
    636624  #ticks #instruction #program_counter'' #FETCH
    637625  #start_status #final_status #trace_ends_flag
     
    686674lemma trace_any_label_length_leq_0_to_False:
    687675  ∀prog: labelled_object_code.
    688   let code_memory ≝ load_code_memory (oc prog) in
    689676  ∀trace_ends_flag: trace_ends_with_ret.
    690   ∀start_status: Status code_memory.
    691   ∀final_status: Status code_memory.
     677  ∀start_status: Status (cm prog).
     678  ∀final_status: Status (cm prog).
    692679  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    693680   trace_any_label_length … the_trace ≤ 0 → False.
     
    703690          Σcost_of_block: nat.
    704691          if (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) then
    705             ∀start_status,final_status: Status (load_code_memory (oc prog)).
     692            ∀start_status,final_status: Status (cm prog).
    706693            ∀trace_ends_flag.
    707694            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
     
    711698          else
    712699            (cost_of_block = 0) ≝
    713   let code_memory' ≝ load_code_memory (oc prog) in
    714700  match program_size return λx. x = program_size → ? with
    715701  [ O ⇒ λbase_case. 0 (* XXX: dummy to be inserted here *)
    716702  | S program_size' ⇒ λstep_case.
    717     let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch (load_code_memory (oc prog)) program_counter' in
     703    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch (cm prog) program_counter' in
    718704    let to_continue ≝
    719705      match lookup_opt … program_counter' (costlabels prog) with
     
    727713          match real_instruction return λx. x = real_instruction →
    728714          Σcost_of_block: nat.
    729             ∀start_status,final_status: Status code_memory'.
     715            ∀start_status,final_status: Status (cm prog).
    730716            ∀trace_ends_flag.
    731717            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
     
    770756          match (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) with
    771757          [ true ⇒
    772             ∀start_status: Status code_memory'.
    773             ∀final_status: Status code_memory'.
     758            ∀start_status: Status (cm prog).
     759            ∀final_status: Status (cm prog).
    774760            ∀trace_ends_flag.
    775761            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
     
    832818    ∀program_counter': Word.
    833819      Σcost_of_block: nat.
    834         ∀start_status: Status (load_code_memory (oc prog)).
    835         ∀final_status: Status (load_code_memory (oc prog)).
     820        ∀start_status: Status (cm prog).
     821        ∀final_status: Status (cm prog).
    836822        ∀trace_ends_flag.
    837823        ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
  • src/ASM/ASMCostsSplit.ma

    r2907 r2999  
    316316definition ASM_cost_map :
    317317  ∀p: labelled_object_code.
    318   let code_memory ≝ load_code_memory (oc p) in
    319318  let a_s ≝ OC_abstract_status p in
    320319  as_cost_map a_s ≝
  • src/ASM/Assembly.ma

    r2899 r2999  
    872872      〈(zero ?), [ ]〉)
    873873    in
     874     let code ≝ reverse … revcode in
    874875     mk_labelled_object_code
    875      (reverse … revcode)
     876     code (load_code_memory code) (refl …)
    876877     (fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??))
    877878     (foldl ??
  • src/ASM/CostsProof.ma

    r2907 r2999  
    1111  (prog: labelled_object_code)
    1212   (trace_ends_flag: trace_ends_with_ret)
    13     (start_status: Status (load_code_memory (oc prog)))
    14     (final_status: Status (load_code_memory (oc prog)))
     13    (start_status: Status (cm prog))
     14    (final_status: Status (cm prog))
    1515      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    1616        start_status final_status) on the_trace: nat ≝
     
    2222  (prog: labelled_object_code)
    2323  (trace_ends_flag: trace_ends_with_ret)
    24    (start_status: Status (load_code_memory (oc prog)))
    25    (final_status: Status (load_code_memory (oc prog)))
     24   (start_status: Status (cm prog))
     25   (final_status: Status (cm prog))
    2626     (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    2727       on the_trace: nat ≝
     
    5353and compute_max_trace_label_return_cost
    5454  (prog: labelled_object_code)
    55   (start_status: Status (load_code_memory (oc prog)))
    56   (final_status: Status (load_code_memory (oc prog)))
     55  (start_status: Status (cm prog))
     56  (final_status: Status (cm prog))
    5757    (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
    5858      on the_trace: nat ≝
     
    7070  (prog: labelled_object_code)
    7171   (trace_ends_flag: trace_ends_with_ret)
    72     (start_status: Status (load_code_memory (oc prog)))
    73     (final_status: Status (load_code_memory (oc prog)))
     72    (start_status: Status (cm prog))
     73    (final_status: Status (cm prog))
    7474      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    7575        start_status final_status) on the_trace:
    76           clock … (load_code_memory (oc prog)) … final_status = (compute_max_trace_label_label_cost prog trace_ends_flag start_status final_status the_trace) + (clock … (load_code_memory (oc prog)) … start_status) ≝ ?
     76          clock … (cm prog) … final_status = (compute_max_trace_label_label_cost prog trace_ends_flag start_status final_status the_trace) + (clock … (cm prog) … start_status) ≝ ?
    7777and compute_max_trace_any_label_cost_is_ok
    7878  (prog: labelled_object_code)
    7979  (trace_ends_flag: trace_ends_with_ret)
    80     (start_status: Status (load_code_memory (oc prog)))
    81     (final_status: Status (load_code_memory (oc prog)))
     80    (start_status: Status (cm prog))
     81    (final_status: Status (cm prog))
    8282     (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    8383       on the_trace:
    84          clock … (load_code_memory (oc prog)) … final_status = (compute_max_trace_any_label_cost prog trace_ends_flag start_status final_status the_trace) + (clock … (load_code_memory (oc prog)) … start_status) ≝ ?
     84         clock … (cm prog) … final_status = (compute_max_trace_any_label_cost prog trace_ends_flag start_status final_status the_trace) + (clock … (cm prog) … start_status) ≝ ?
    8585and compute_max_trace_label_return_cost_is_ok
    8686  (prog: labelled_object_code)
    87     (start_status: Status (load_code_memory (oc prog)))
    88     (final_status: Status (load_code_memory (oc prog)))
     87    (start_status: Status (cm prog))
     88    (final_status: Status (cm prog))
    8989    (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
    9090      on the_trace:
    91         clock … (load_code_memory (oc prog)) … final_status = (compute_max_trace_label_return_cost prog start_status final_status the_trace) + clock … (load_code_memory (oc prog)) … start_status ≝ ?.
     91        clock … (cm prog) … final_status = (compute_max_trace_label_return_cost prog start_status final_status the_trace) + clock … (cm prog) … start_status ≝ ?.
    9292  [1:
    9393    cases the_trace
     
    127127      >(compute_max_trace_label_return_cost_is_ok prog status_start_fun_call
    128128        status_after_fun_call call_trace)
    129       cases(is_next) in match (clock … (load_code_memory (oc prog)) status_start_fun_call);
     129      cases(is_next) in match (clock … (cm prog) status_start_fun_call);
    130130      >(execute_1_ok_clock … status_pre_fun_call)
    131131      <associative_plus in ⊢ (??%?);
     
    149149      >(compute_max_trace_any_label_cost_is_ok prog end_flag
    150150         status_init status_end trace_any_label)
    151       cases(is_next) in match (clock … (load_code_memory (oc prog)) status_init);
     151      cases(is_next) in match (clock … (cm prog) status_init);
    152152      >(execute_1_ok_clock … status_pre)
    153153      >commutative_plus >associative_plus >associative_plus @eq_f
     
    175175  (prog:labelled_object_code)
    176176   (trace_ends_flag: trace_ends_with_ret)
    177     (start_status: Status (load_code_memory (oc prog)))
    178     (final_status: Status (load_code_memory (oc prog)))
     177    (start_status: Status (cm prog))
     178    (final_status: Status (cm prog))
    179179      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    180180        start_status final_status) on the_trace: nat ≝
     
    187187  (prog:labelled_object_code)
    188188  (trace_ends_flag: trace_ends_with_ret)
    189     (start_status: Status (load_code_memory (oc prog)))
    190     (final_status: Status (load_code_memory (oc prog)))
     189    (start_status: Status (cm prog))
     190    (final_status: Status (cm prog))
    191191     (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    192192       on the_trace: nat ≝
     
    209209and compute_trace_label_return_cost_using_paid
    210210  (prog:labelled_object_code)
    211     (start_status: Status (load_code_memory (oc prog)))
    212     (final_status: Status (load_code_memory (oc prog)))
     211    (start_status: Status (cm prog))
     212    (final_status: Status (cm prog))
    213213    (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
    214214      on the_trace: nat ≝
     
    224224  (prog:labelled_object_code)
    225225   (trace_ends_flag: trace_ends_with_ret)
    226     (start_status: Status (load_code_memory (oc prog)))
    227     (final_status: Status (load_code_memory (oc prog)))
     226    (start_status: Status (cm prog))
     227    (final_status: Status (cm prog))
    228228      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    229229        start_status final_status) on the_trace:
     
    233233  (prog:labelled_object_code)
    234234  (trace_ends_flag: trace_ends_with_ret)
    235     (start_status: Status (load_code_memory (oc prog)))
    236     (final_status: Status (load_code_memory (oc prog)))
     235    (start_status: Status (cm prog))
     236    (final_status: Status (cm prog))
    237237     (the_trace: trace_any_label (OC_abstract_status prog)
    238238      trace_ends_flag start_status final_status) on the_trace:     
     
    242242and compute_trace_label_return_cost_using_paid_ok
    243243  (prog:labelled_object_code)
    244     (start_status: Status (load_code_memory (oc prog)))
    245     (final_status: Status (load_code_memory (oc prog)))
     244    (start_status: Status (cm prog))
     245    (final_status: Status (cm prog))
    246246    (the_trace: trace_label_return (OC_abstract_status prog)
    247247     start_status final_status) on the_trace:
     
    454454 (prog: labelled_object_code)
    455455 (cost_map: identifier_map CostTag nat)
    456  (initial: Status (load_code_memory (oc prog)))
    457  (final: Status (load_code_memory (oc prog)))
     456 (initial: Status (cm prog))
     457 (final: Status (cm prog))
    458458 (trace: trace_label_return (OC_abstract_status prog) initial final)
    459459 (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k))
     
    470470 (trace_ends_flag: trace_ends_with_ret)
    471471 (cost_map: identifier_map CostTag nat)
    472  (initial: Status (load_code_memory (oc prog)))
    473  (final: Status (load_code_memory (oc prog)))
     472 (initial: Status (cm prog))
     473 (final: Status (cm prog))
    474474 (trace: trace_any_label (OC_abstract_status prog) trace_ends_flag initial final)
    475475 (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k))
     
    486486 (trace_ends_flag: trace_ends_with_ret)
    487487 (cost_map: identifier_map CostTag nat)
    488  (initial: Status (load_code_memory (oc prog)))
    489  (final: Status (load_code_memory (oc prog)))
     488 (initial: Status (cm prog))
     489 (final: Status (cm prog))
    490490 (trace: trace_label_label (OC_abstract_status prog) trace_ends_flag initial final)
    491491 (unrepeating_witness: tll_unrepeating … trace)
     
    630630  ∀prog: labelled_object_code.
    631631  ∀cost_map: identifier_map CostTag nat.
    632   ∀initial: Status (load_code_memory (oc prog)).
    633   ∀final: Status (load_code_memory (oc prog)).
     632  ∀initial: Status (cm prog).
     633  ∀final: Status (cm prog).
    634634  ∀trace: trace_label_return (OC_abstract_status prog) initial final.
    635635  ∀unrepeating_witness: tlr_unrepeating … trace.
     
    638638      pi1 … (block_cost prog pc) = lookup_present … k_pres).
    639639        let ctrace ≝ flatten_trace_label_return … trace in
    640           clock … (load_code_memory (oc prog)) … final =
    641             clock … (load_code_memory (oc prog)) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i)).
     640          clock … (cm prog) … final =
     641            clock … (cm prog) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i)).
    642642  #prog #cost_map
    643643  #initial #final #trace #unrepeating_witness #codom_dom #dom_codom normalize nodelta
     
    648648theorem compute_max_trace_label_return_cost_ok_with_trace:
    649649  ∀prog: labelled_object_code.
    650   ∀initial: Status (load_code_memory (oc prog)).
    651   ∀final: Status (load_code_memory (oc prog)).
     650  ∀initial: Status (cm prog).
     651  ∀final: Status (cm prog).
    652652  ∀trace: trace_label_return (OC_abstract_status prog) initial final.
    653653  ∀unrepeating_witness: tlr_unrepeating … trace.
    654654    let cost_map ≝ traverse_code prog in
    655655    let ctrace ≝ flatten_trace_label_return … trace in
    656       clock … (load_code_memory (oc prog)) … final = clock … (load_code_memory (oc prog)) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map ? ctrace i)).
     656      clock … (cm prog) … final = clock … (cm prog) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map ? ctrace i)).
    657657  [1:
    658658    #prog #initial #final #trace #unrepeating_witness
  • src/ASM/Fetch.ma

    r2770 r2999  
    173173definition code_memory_size ≝ bitvector_max_nat 16.
    174174
    175 include alias "ASM/BitVectorTrie.ma".
    176 include alias "ASM/Arithmetic.ma".
    177 
    178 definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝
    179   λpmem: BitVectorTrie Byte 16.
    180   λpc: Word.
    181     〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
    182 
    183 definition load_code_memory0:
    184  ∀program: object_code. Σres: BitVectorTrie Byte 16.
    185   let program_size ≝ |program| in
    186    program_size ≤ 2^16 →
    187     ∀pc. ∀pc_ok: pc < program_size.
    188      nth_safe ? pc program pc_ok = \snd (next res (bitvector_of_nat … pc))
    189 
    190  λprogram. \snd
    191   (foldl_strong ?
    192    (λprefix.
    193      Σres: nat × (BitVectorTrie Byte 16).
    194       let 〈i,mem〉 ≝ res in
    195       i = |prefix| ∧
    196       (i ≤ 2^16 →
    197         ∀pc. ∀pc_ok: pc < |prefix|.
    198          nth_safe ? pc prefix pc_ok = \snd (next mem (bitvector_of_nat … pc))))
    199    program
    200    (λprefix,v,tl,prf,i_mem.
    201      let 〈i,mem〉 ≝ i_mem in
    202       〈S i,insert … (bitvector_of_nat … i) v mem〉)
    203   〈0,Stub Byte 16〉).
    204 [3: cases (foldl_strong ? (λprefix.Σres.?) ???) * #i #mem * #H1 >H1 #H2 @H2
    205 | % // #_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))
    206 | cases i_mem in p; * #i' #mem' #H #EQ destruct(EQ) cases H -H #H1 #H2 %
    207   [ >length_append >H1 normalize //
    208   | #LE #pc #pc_ok
    209     cases (le_to_or_lt_eq … pc_ok)
    210     [2: #EQ_Spc >(?: pc = |prefix| + 0) in pc_ok;
    211       [2: >length_append in EQ_Spc; normalize #EQ @injective_S >EQ //]
    212       #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?);
    213       <H1 <plus_n_O whd in ⊢ (???%); //
    214     | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix [2: /2/]
    215       >H2 [2: @(transitive_le … LE) //]
    216       cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ
    217       whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false %
    218       #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption
    219       @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]]
    220 qed.
    221 
    222 definition load_code_memory: object_code → BitVectorTrie Byte 16 ≝
    223  λprogram.load_code_memory0 program.
    224 
    225 lemma load_code_memory_ok:
    226  ∀program: object_code.
    227   let program_size ≝ |program| in
    228    program_size ≤ 2^16 →
    229     ∀pc. ∀pc_ok: pc < program_size.
    230      nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
    231 whd in match load_code_memory; normalize nodelta #program @pi2
    232 qed.
    233 
    234175lemma Prod_inv_rect_Type0:
    235176 ∀A,B. ∀P: A × B → Type[0].∀ab.
  • src/ASM/Interpret2.ma

    r2993 r2999  
    3939definition OC_preclassified_system: labelled_object_code → preclassified_system ≝
    4040 λc:labelled_object_code.
    41   let lcm ≝ load_code_memory … (oc c) in
    4241  mk_preclassified_system_of_abstract_status
    4342   labelled_object_code
    4443   (OC_abstract_status c)
    45    (λst. return (execute_1 lcm … st))
    46    (initialise_status … (load_code_memory (oc c))).
     44   (λst. return (execute_1 (cm c) … st))
     45   (initialise_status … (cm c)).
    4746
    4847(* Pre-classified system for ASM *)
  • src/correctness.ma

    r2928 r2999  
    100100definition simulates ≝
    101101  λp: compiler_output.
    102   let initial_status ≝ initialise_status … (load_code_memory (oc (c_labelled_object_code … p))) in
     102  let initial_status ≝ initialise_status … (cm c_labelled_object_code … p) in
    103103  ∀m1,m2.
    104104   measurable Clight_pcs (c_labelled_clight … p) m1 m2
Note: See TracChangeset for help on using the changeset viewer.