Changeset 2717 for extracted/aSM.ml
 Timestamp:
 Feb 23, 2013, 1:16:55 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/aSM.ml
r2649 r2717 60 60 61 61 open Identifiers 62 63 open BitVectorTrie 64 65 open Exp 62 66 63 67 open Arithmetic … … 109 113 > 'a1) > addressing_mode > 'a1 **) 110 114 let 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 111  DIRECT x_ 59 > h_DIRECT x_59112  INDIRECT x_ 60 > h_INDIRECT x_60113  EXT_INDIRECT x_ 61 > h_EXT_INDIRECT x_61114  REGISTER x_ 62 > h_REGISTER x_62115  DIRECT x_18716 > h_DIRECT x_18716 116  INDIRECT x_18717 > h_INDIRECT x_18717 117  EXT_INDIRECT x_18718 > h_EXT_INDIRECT x_18718 118  REGISTER x_18719 > h_REGISTER x_18719 115 119  ACC_A > h_ACC_A 116 120  ACC_B > h_ACC_B 117 121  DPTR > h_DPTR 118  DATA x_ 63 > h_DATA x_63119  DATA16 x_ 64 > h_DATA16 x_64122  DATA x_18720 > h_DATA x_18720 123  DATA16 x_18721 > h_DATA16 x_18721 120 124  ACC_DPTR > h_ACC_DPTR 121 125  ACC_PC > h_ACC_PC … … 123 127  INDIRECT_DPTR > h_INDIRECT_DPTR 124 128  CARRY > h_CARRY 125  BIT_ADDR x_ 65 > h_BIT_ADDR x_65126  N_BIT_ADDR x_ 66 > h_N_BIT_ADDR x_66127  RELATIVE x_ 67 > h_RELATIVE x_67128  ADDR11 x_ 68 > h_ADDR11 x_68129  ADDR16 x_ 69 > h_ADDR16 x_69129  BIT_ADDR x_18722 > h_BIT_ADDR x_18722 130  N_BIT_ADDR x_18723 > h_N_BIT_ADDR x_18723 131  RELATIVE x_18724 > h_RELATIVE x_18724 132  ADDR11 x_18725 > h_ADDR11 x_18725 133  ADDR16 x_18726 > h_ADDR16 x_18726 130 134 131 135 (** val addressing_mode_rect_Type5 : … … 137 141 > 'a1) > addressing_mode > 'a1 **) 138 142 let 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 139  DIRECT x_ 90 > h_DIRECT x_90140  INDIRECT x_ 91 > h_INDIRECT x_91141  EXT_INDIRECT x_ 92 > h_EXT_INDIRECT x_92142  REGISTER x_ 93 > h_REGISTER x_93143  DIRECT x_18747 > h_DIRECT x_18747 144  INDIRECT x_18748 > h_INDIRECT x_18748 145  EXT_INDIRECT x_18749 > h_EXT_INDIRECT x_18749 146  REGISTER x_18750 > h_REGISTER x_18750 143 147  ACC_A > h_ACC_A 144 148  ACC_B > h_ACC_B 145 149  DPTR > h_DPTR 146  DATA x_ 94 > h_DATA x_94147  DATA16 x_ 95 > h_DATA16 x_95150  DATA x_18751 > h_DATA x_18751 151  DATA16 x_18752 > h_DATA16 x_18752 148 152  ACC_DPTR > h_ACC_DPTR 149 153  ACC_PC > h_ACC_PC … … 151 155  INDIRECT_DPTR > h_INDIRECT_DPTR 152 156  CARRY > h_CARRY 153  BIT_ADDR x_ 96 > h_BIT_ADDR x_96154  N_BIT_ADDR x_ 97 > h_N_BIT_ADDR x_97155  RELATIVE x_ 98 > h_RELATIVE x_98156  ADDR11 x_ 99 > h_ADDR11 x_99157  ADDR16 x_1 00 > h_ADDR16 x_100157  BIT_ADDR x_18753 > h_BIT_ADDR x_18753 158  N_BIT_ADDR x_18754 > h_N_BIT_ADDR x_18754 159  RELATIVE x_18755 > h_RELATIVE x_18755 160  ADDR11 x_18756 > h_ADDR11 x_18756 161  ADDR16 x_18757 > h_ADDR16 x_18757 158 162 159 163 (** val addressing_mode_rect_Type3 : … … 165 169 > 'a1) > addressing_mode > 'a1 **) 166 170 let 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 167  DIRECT x_1 21 > h_DIRECT x_121168  INDIRECT x_1 22 > h_INDIRECT x_122169  EXT_INDIRECT x_1 23 > h_EXT_INDIRECT x_123170  REGISTER x_1 24 > h_REGISTER x_124171  DIRECT x_18778 > h_DIRECT x_18778 172  INDIRECT x_18779 > h_INDIRECT x_18779 173  EXT_INDIRECT x_18780 > h_EXT_INDIRECT x_18780 174  REGISTER x_18781 > h_REGISTER x_18781 171 175  ACC_A > h_ACC_A 172 176  ACC_B > h_ACC_B 173 177  DPTR > h_DPTR 174  DATA x_1 25 > h_DATA x_125175  DATA16 x_1 26 > h_DATA16 x_126178  DATA x_18782 > h_DATA x_18782 179  DATA16 x_18783 > h_DATA16 x_18783 176 180  ACC_DPTR > h_ACC_DPTR 177 181  ACC_PC > h_ACC_PC … … 179 183  INDIRECT_DPTR > h_INDIRECT_DPTR 180 184  CARRY > h_CARRY 181  BIT_ADDR x_1 27 > h_BIT_ADDR x_127182  N_BIT_ADDR x_1 28 > h_N_BIT_ADDR x_128183  RELATIVE x_1 29 > h_RELATIVE x_129184  ADDR11 x_1 30 > h_ADDR11 x_130185  ADDR16 x_1 31 > h_ADDR16 x_131185  BIT_ADDR x_18784 > h_BIT_ADDR x_18784 186  N_BIT_ADDR x_18785 > h_N_BIT_ADDR x_18785 187  RELATIVE x_18786 > h_RELATIVE x_18786 188  ADDR11 x_18787 > h_ADDR11 x_18787 189  ADDR16 x_18788 > h_ADDR16 x_18788 186 190 187 191 (** val addressing_mode_rect_Type2 : … … 193 197 > 'a1) > addressing_mode > 'a1 **) 194 198 let 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 195  DIRECT x_1 52 > h_DIRECT x_152196  INDIRECT x_1 53 > h_INDIRECT x_153197  EXT_INDIRECT x_1 54 > h_EXT_INDIRECT x_154198  REGISTER x_1 55 > h_REGISTER x_155199  DIRECT x_18809 > h_DIRECT x_18809 200  INDIRECT x_18810 > h_INDIRECT x_18810 201  EXT_INDIRECT x_18811 > h_EXT_INDIRECT x_18811 202  REGISTER x_18812 > h_REGISTER x_18812 199 203  ACC_A > h_ACC_A 200 204  ACC_B > h_ACC_B 201 205  DPTR > h_DPTR 202  DATA x_1 56 > h_DATA x_156203  DATA16 x_1 57 > h_DATA16 x_157206  DATA x_18813 > h_DATA x_18813 207  DATA16 x_18814 > h_DATA16 x_18814 204 208  ACC_DPTR > h_ACC_DPTR 205 209  ACC_PC > h_ACC_PC … … 207 211  INDIRECT_DPTR > h_INDIRECT_DPTR 208 212  CARRY > h_CARRY 209  BIT_ADDR x_1 58 > h_BIT_ADDR x_158210  N_BIT_ADDR x_1 59 > h_N_BIT_ADDR x_159211  RELATIVE x_1 60 > h_RELATIVE x_160212  ADDR11 x_1 61 > h_ADDR11 x_161213  ADDR16 x_1 62 > h_ADDR16 x_162213  BIT_ADDR x_18815 > h_BIT_ADDR x_18815 214  N_BIT_ADDR x_18816 > h_N_BIT_ADDR x_18816 215  RELATIVE x_18817 > h_RELATIVE x_18817 216  ADDR11 x_18818 > h_ADDR11 x_18818 217  ADDR16 x_18819 > h_ADDR16 x_18819 214 218 215 219 (** val addressing_mode_rect_Type1 : … … 221 225 > 'a1) > addressing_mode > 'a1 **) 222 226 let 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 223  DIRECT x_18 3 > h_DIRECT x_183224  INDIRECT x_18 4 > h_INDIRECT x_184225  EXT_INDIRECT x_18 5 > h_EXT_INDIRECT x_185226  REGISTER x_18 6 > h_REGISTER x_186227  DIRECT x_18840 > h_DIRECT x_18840 228  INDIRECT x_18841 > h_INDIRECT x_18841 229  EXT_INDIRECT x_18842 > h_EXT_INDIRECT x_18842 230  REGISTER x_18843 > h_REGISTER x_18843 227 231  ACC_A > h_ACC_A 228 232  ACC_B > h_ACC_B 229 233  DPTR > h_DPTR 230  DATA x_18 7 > h_DATA x_187231  DATA16 x_188 > h_DATA16 x_188234  DATA x_18844 > h_DATA x_18844 235  DATA16 x_18845 > h_DATA16 x_18845 232 236  ACC_DPTR > h_ACC_DPTR 233 237  ACC_PC > h_ACC_PC … … 235 239  INDIRECT_DPTR > h_INDIRECT_DPTR 236 240  CARRY > h_CARRY 237  BIT_ADDR x_18 9 > h_BIT_ADDR x_189238  N_BIT_ADDR x_1 90 > h_N_BIT_ADDR x_190239  RELATIVE x_1 91 > h_RELATIVE x_191240  ADDR11 x_1 92 > h_ADDR11 x_192241  ADDR16 x_1 93 > h_ADDR16 x_193241  BIT_ADDR x_18846 > h_BIT_ADDR x_18846 242  N_BIT_ADDR x_18847 > h_N_BIT_ADDR x_18847 243  RELATIVE x_18848 > h_RELATIVE x_18848 244  ADDR11 x_18849 > h_ADDR11 x_18849 245  ADDR16 x_18850 > h_ADDR16 x_18850 242 246 243 247 (** val addressing_mode_rect_Type0 : … … 249 253 > 'a1) > addressing_mode > 'a1 **) 250 254 let 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 251  DIRECT x_ 214 > h_DIRECT x_214252  INDIRECT x_ 215 > h_INDIRECT x_215253  EXT_INDIRECT x_ 216 > h_EXT_INDIRECT x_216254  REGISTER x_ 217 > h_REGISTER x_217255  DIRECT x_18871 > h_DIRECT x_18871 256  INDIRECT x_18872 > h_INDIRECT x_18872 257  EXT_INDIRECT x_18873 > h_EXT_INDIRECT x_18873 258  REGISTER x_18874 > h_REGISTER x_18874 255 259  ACC_A > h_ACC_A 256 260  ACC_B > h_ACC_B 257 261  DPTR > h_DPTR 258  DATA x_ 218 > h_DATA x_218259  DATA16 x_ 219 > h_DATA16 x_219262  DATA x_18875 > h_DATA x_18875 263  DATA16 x_18876 > h_DATA16 x_18876 260 264  ACC_DPTR > h_ACC_DPTR 261 265  ACC_PC > h_ACC_PC … … 263 267  INDIRECT_DPTR > h_INDIRECT_DPTR 264 268  CARRY > h_CARRY 265  BIT_ADDR x_ 220 > h_BIT_ADDR x_220266  N_BIT_ADDR x_ 221 > h_N_BIT_ADDR x_221267  RELATIVE x_ 222 > h_RELATIVE x_222268  ADDR11 x_ 223 > h_ADDR11 x_223269  ADDR16 x_ 224 > h_ADDR16 x_224269  BIT_ADDR x_18877 > h_BIT_ADDR x_18877 270  N_BIT_ADDR x_18878 > h_N_BIT_ADDR x_18878 271  RELATIVE x_18879 > h_RELATIVE x_18879 272  ADDR11 x_18880 > h_ADDR11 x_18880 273  ADDR16 x_18881 > h_ADDR16 x_18881 270 274 271 275 (** val addressing_mode_inv_rect_Type4 : … … 1924 1928 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1925 1929 'a1) > subaddressing_mode > 'a1 **) 1926 let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_ 692=1927 let subaddressing_modeel = x_ 692in1930 let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_19349 = 1931 let subaddressing_modeel = x_19349 in 1928 1932 h_mk_subaddressing_mode subaddressing_modeel __ 1929 1933 … … 1931 1935 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1932 1936 'a1) > subaddressing_mode > 'a1 **) 1933 let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_ 694=1934 let subaddressing_modeel = x_ 694in1937 let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_19351 = 1938 let subaddressing_modeel = x_19351 in 1935 1939 h_mk_subaddressing_mode subaddressing_modeel __ 1936 1940 … … 1938 1942 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1939 1943 'a1) > subaddressing_mode > 'a1 **) 1940 let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_ 696=1941 let subaddressing_modeel = x_ 696in1944 let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_19353 = 1945 let subaddressing_modeel = x_19353 in 1942 1946 h_mk_subaddressing_mode subaddressing_modeel __ 1943 1947 … … 1945 1949 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1946 1950 'a1) > subaddressing_mode > 'a1 **) 1947 let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_ 698=1948 let subaddressing_modeel = x_ 698in1951 let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_19355 = 1952 let subaddressing_modeel = x_19355 in 1949 1953 h_mk_subaddressing_mode subaddressing_modeel __ 1950 1954 … … 1952 1956 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1953 1957 'a1) > subaddressing_mode > 'a1 **) 1954 let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_ 700=1955 let subaddressing_modeel = x_ 700in1958 let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_19357 = 1959 let subaddressing_modeel = x_19357 in 1956 1960 h_mk_subaddressing_mode subaddressing_modeel __ 1957 1961 … … 1959 1963 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1960 1964 'a1) > subaddressing_mode > 'a1 **) 1961 let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_ 702=1962 let subaddressing_modeel = x_ 702in1965 let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_19359 = 1966 let subaddressing_modeel = x_19359 in 1963 1967 h_mk_subaddressing_mode subaddressing_modeel __ 1964 1968 … … 2094 2098  RETI 2095 2099  NOP 2100  JMP of subaddressing_mode 2096 2101 2097 2102 (** val preinstruction_rect_Type4 : … … 2129 2134 (subaddressing_mode > 'a2) > (subaddressing_mode > subaddressing_mode 2130 2135 > 'a2) > (subaddressing_mode > subaddressing_mode > 'a2) > 'a2 > 2131 'a2 > 'a2 > 'a1 preinstruction > 'a2 **)2132 let 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 = function2133  ADD (x_ 802, x_801) > h_ADD x_802 x_8012134  ADDC (x_ 804, x_803) > h_ADDC x_804 x_8032135  SUBB (x_ 806, x_805) > h_SUBB x_806 x_8052136  INC x_ 807 > h_INC x_8072137  DEC x_ 808 > h_DEC x_8082138  MUL (x_ 810, x_809) > h_MUL x_810 x_8092139  DIV (x_ 812, x_811) > h_DIV x_812 x_8112140  DA x_ 813 > h_DA x_8132141  JC x_ 814 > h_JC x_8142142  JNC x_ 815 > h_JNC x_8152143  JB (x_ 817, x_816) > h_JB x_817 x_8162144  JNB (x_ 819, x_818) > h_JNB x_819 x_8182145  JBC (x_ 821, x_820) > h_JBC x_821 x_8202146  JZ x_ 822 > h_JZ x_8222147  JNZ x_ 823 > h_JNZ x_8232148  CJNE (x_ 825, x_824) > h_CJNE x_825 x_8242149  DJNZ (x_ 827, x_826) > h_DJNZ x_827 x_8262150  ANL x_ 828 > h_ANL x_8282151  ORL x_ 829 > h_ORL x_8292152  XRL x_ 830 > h_XRL x_8302153  CLR x_ 831 > h_CLR x_8312154  CPL x_ 832 > h_CPL x_8322155  RL x_ 833 > h_RL x_8332156  RLC x_ 834 > h_RLC x_8342157  RR x_ 835 > h_RR x_8352158  RRC x_ 836 > h_RRC x_8362159  SWAP x_ 837 > h_SWAP x_8372160  MOV x_ 838 > h_MOV x_8382161  MOVX x_ 839 > h_MOVX x_8392162  SETB x_ 840 > h_SETB x_8402163  PUSH x_ 841 > h_PUSH x_8412164  POP x_ 842 > h_POP x_8422165  XCH (x_ 844, x_843) > h_XCH x_844 x_8432166  XCHD (x_ 846, x_845) > h_XCHD x_846 x_8452136 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2137 let 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 2138  ADD (x_19461, x_19460) > h_ADD x_19461 x_19460 2139  ADDC (x_19463, x_19462) > h_ADDC x_19463 x_19462 2140  SUBB (x_19465, x_19464) > h_SUBB x_19465 x_19464 2141  INC x_19466 > h_INC x_19466 2142  DEC x_19467 > h_DEC x_19467 2143  MUL (x_19469, x_19468) > h_MUL x_19469 x_19468 2144  DIV (x_19471, x_19470) > h_DIV x_19471 x_19470 2145  DA x_19472 > h_DA x_19472 2146  JC x_19473 > h_JC x_19473 2147  JNC x_19474 > h_JNC x_19474 2148  JB (x_19476, x_19475) > h_JB x_19476 x_19475 2149  JNB (x_19478, x_19477) > h_JNB x_19478 x_19477 2150  JBC (x_19480, x_19479) > h_JBC x_19480 x_19479 2151  JZ x_19481 > h_JZ x_19481 2152  JNZ x_19482 > h_JNZ x_19482 2153  CJNE (x_19484, x_19483) > h_CJNE x_19484 x_19483 2154  DJNZ (x_19486, x_19485) > h_DJNZ x_19486 x_19485 2155  ANL x_19487 > h_ANL x_19487 2156  ORL x_19488 > h_ORL x_19488 2157  XRL x_19489 > h_XRL x_19489 2158  CLR x_19490 > h_CLR x_19490 2159  CPL x_19491 > h_CPL x_19491 2160  RL x_19492 > h_RL x_19492 2161  RLC x_19493 > h_RLC x_19493 2162  RR x_19494 > h_RR x_19494 2163  RRC x_19495 > h_RRC x_19495 2164  SWAP x_19496 > h_SWAP x_19496 2165  MOV x_19497 > h_MOV x_19497 2166  MOVX x_19498 > h_MOVX x_19498 2167  SETB x_19499 > h_SETB x_19499 2168  PUSH x_19500 > h_PUSH x_19500 2169  POP x_19501 > h_POP x_19501 2170  XCH (x_19503, x_19502) > h_XCH x_19503 x_19502 2171  XCHD (x_19505, x_19504) > h_XCHD x_19505 x_19504 2167 2172  RET > h_RET 2168 2173  RETI > h_RETI 2169 2174  NOP > h_NOP 2175  JMP x_19506 > h_JMP x_19506 2170 2176 2171 2177 (** val preinstruction_rect_Type5 : … … 2203 2209 (subaddressing_mode > 'a2) > (subaddressing_mode > subaddressing_mode 2204 2210 > 'a2) > (subaddressing_mode > subaddressing_mode > 'a2) > 'a2 > 2205 'a2 > 'a2 > 'a1 preinstruction > 'a2 **)2206 let 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 = function2207  ADD (x_ 886, x_885) > h_ADD x_886 x_8852208  ADDC (x_ 888, x_887) > h_ADDC x_888 x_8872209  SUBB (x_ 890, x_889) > h_SUBB x_890 x_8892210  INC x_ 891 > h_INC x_8912211  DEC x_ 892 > h_DEC x_8922212  MUL (x_ 894, x_893) > h_MUL x_894 x_8932213  DIV (x_ 896, x_895) > h_DIV x_896 x_8952214  DA x_ 897 > h_DA x_8972215  JC x_ 898 > h_JC x_8982216  JNC x_ 899 > h_JNC x_8992217  JB (x_ 901, x_900) > h_JB x_901 x_9002218  JNB (x_ 903, x_902) > h_JNB x_903 x_9022219  JBC (x_ 905, x_904) > h_JBC x_905 x_9042220  JZ x_ 906 > h_JZ x_9062221  JNZ x_ 907 > h_JNZ x_9072222  CJNE (x_ 909, x_908) > h_CJNE x_909 x_9082223  DJNZ (x_ 911, x_910) > h_DJNZ x_911 x_9102224  ANL x_ 912 > h_ANL x_9122225  ORL x_ 913 > h_ORL x_9132226  XRL x_ 914 > h_XRL x_9142227  CLR x_ 915 > h_CLR x_9152228  CPL x_ 916 > h_CPL x_9162229  RL x_ 917 > h_RL x_9172230  RLC x_ 918 > h_RLC x_9182231  RR x_ 919 > h_RR x_9192232  RRC x_ 920 > h_RRC x_9202233  SWAP x_ 921 > h_SWAP x_9212234  MOV x_ 922 > h_MOV x_9222235  MOVX x_ 923 > h_MOVX x_9232236  SETB x_ 924 > h_SETB x_9242237  PUSH x_ 925 > h_PUSH x_9252238  POP x_ 926 > h_POP x_9262239  XCH (x_ 928, x_927) > h_XCH x_928 x_9272240  XCHD (x_ 930, x_929) > h_XCHD x_930 x_9292211 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2212 let 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 2213  ADD (x_19547, x_19546) > h_ADD x_19547 x_19546 2214  ADDC (x_19549, x_19548) > h_ADDC x_19549 x_19548 2215  SUBB (x_19551, x_19550) > h_SUBB x_19551 x_19550 2216  INC x_19552 > h_INC x_19552 2217  DEC x_19553 > h_DEC x_19553 2218  MUL (x_19555, x_19554) > h_MUL x_19555 x_19554 2219  DIV (x_19557, x_19556) > h_DIV x_19557 x_19556 2220  DA x_19558 > h_DA x_19558 2221  JC x_19559 > h_JC x_19559 2222  JNC x_19560 > h_JNC x_19560 2223  JB (x_19562, x_19561) > h_JB x_19562 x_19561 2224  JNB (x_19564, x_19563) > h_JNB x_19564 x_19563 2225  JBC (x_19566, x_19565) > h_JBC x_19566 x_19565 2226  JZ x_19567 > h_JZ x_19567 2227  JNZ x_19568 > h_JNZ x_19568 2228  CJNE (x_19570, x_19569) > h_CJNE x_19570 x_19569 2229  DJNZ (x_19572, x_19571) > h_DJNZ x_19572 x_19571 2230  ANL x_19573 > h_ANL x_19573 2231  ORL x_19574 > h_ORL x_19574 2232  XRL x_19575 > h_XRL x_19575 2233  CLR x_19576 > h_CLR x_19576 2234  CPL x_19577 > h_CPL x_19577 2235  RL x_19578 > h_RL x_19578 2236  RLC x_19579 > h_RLC x_19579 2237  RR x_19580 > h_RR x_19580 2238  RRC x_19581 > h_RRC x_19581 2239  SWAP x_19582 > h_SWAP x_19582 2240  MOV x_19583 > h_MOV x_19583 2241  MOVX x_19584 > h_MOVX x_19584 2242  SETB x_19585 > h_SETB x_19585 2243  PUSH x_19586 > h_PUSH x_19586 2244  POP x_19587 > h_POP x_19587 2245  XCH (x_19589, x_19588) > h_XCH x_19589 x_19588 2246  XCHD (x_19591, x_19590) > h_XCHD x_19591 x_19590 2241 2247  RET > h_RET 2242 2248  RETI > h_RETI 2243 2249  NOP > h_NOP 2250  JMP x_19592 > h_JMP x_19592 2244 2251 2245 2252 (** val preinstruction_rect_Type3 : … … 2277 2284 (subaddressing_mode > 'a2) > (subaddressing_mode > subaddressing_mode 2278 2285 > 'a2) > (subaddressing_mode > subaddressing_mode > 'a2) > 'a2 > 2279 'a2 > 'a2 > 'a1 preinstruction > 'a2 **)2280 let 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 = function2281  ADD (x_ 970, x_969) > h_ADD x_970 x_9692282  ADDC (x_ 972, x_971) > h_ADDC x_972 x_9712283  SUBB (x_ 974, x_973) > h_SUBB x_974 x_9732284  INC x_ 975 > h_INC x_9752285  DEC x_ 976 > h_DEC x_9762286  MUL (x_ 978, x_977) > h_MUL x_978 x_9772287  DIV (x_ 980, x_979) > h_DIV x_980 x_9792288  DA x_ 981 > h_DA x_9812289  JC x_ 982 > h_JC x_9822290  JNC x_ 983 > h_JNC x_9832291  JB (x_ 985, x_984) > h_JB x_985 x_9842292  JNB (x_ 987, x_986) > h_JNB x_987 x_9862293  JBC (x_ 989, x_988) > h_JBC x_989 x_9882294  JZ x_ 990 > h_JZ x_9902295  JNZ x_ 991 > h_JNZ x_9912296  CJNE (x_ 993, x_992) > h_CJNE x_993 x_9922297  DJNZ (x_ 995, x_994) > h_DJNZ x_995 x_9942298  ANL x_ 996 > h_ANL x_9962299  ORL x_ 997 > h_ORL x_9972300  XRL x_ 998 > h_XRL x_9982301  CLR x_ 999 > h_CLR x_9992302  CPL x_1 000 > h_CPL x_10002303  RL x_1 001 > h_RL x_10012304  RLC x_1 002 > h_RLC x_10022305  RR x_1 003 > h_RR x_10032306  RRC x_1 004 > h_RRC x_10042307  SWAP x_1 005 > h_SWAP x_10052308  MOV x_1 006 > h_MOV x_10062309  MOVX x_1 007 > h_MOVX x_10072310  SETB x_1 008 > h_SETB x_10082311  PUSH x_1 009 > h_PUSH x_10092312  POP x_1 010 > h_POP x_10102313  XCH (x_1 012, x_1011) > h_XCH x_1012 x_10112314  XCHD (x_1 014, x_1013) > h_XCHD x_1014 x_10132286 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2287 let 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 2288  ADD (x_19633, x_19632) > h_ADD x_19633 x_19632 2289  ADDC (x_19635, x_19634) > h_ADDC x_19635 x_19634 2290  SUBB (x_19637, x_19636) > h_SUBB x_19637 x_19636 2291  INC x_19638 > h_INC x_19638 2292  DEC x_19639 > h_DEC x_19639 2293  MUL (x_19641, x_19640) > h_MUL x_19641 x_19640 2294  DIV (x_19643, x_19642) > h_DIV x_19643 x_19642 2295  DA x_19644 > h_DA x_19644 2296  JC x_19645 > h_JC x_19645 2297  JNC x_19646 > h_JNC x_19646 2298  JB (x_19648, x_19647) > h_JB x_19648 x_19647 2299  JNB (x_19650, x_19649) > h_JNB x_19650 x_19649 2300  JBC (x_19652, x_19651) > h_JBC x_19652 x_19651 2301  JZ x_19653 > h_JZ x_19653 2302  JNZ x_19654 > h_JNZ x_19654 2303  CJNE (x_19656, x_19655) > h_CJNE x_19656 x_19655 2304  DJNZ (x_19658, x_19657) > h_DJNZ x_19658 x_19657 2305  ANL x_19659 > h_ANL x_19659 2306  ORL x_19660 > h_ORL x_19660 2307  XRL x_19661 > h_XRL x_19661 2308  CLR x_19662 > h_CLR x_19662 2309  CPL x_19663 > h_CPL x_19663 2310  RL x_19664 > h_RL x_19664 2311  RLC x_19665 > h_RLC x_19665 2312  RR x_19666 > h_RR x_19666 2313  RRC x_19667 > h_RRC x_19667 2314  SWAP x_19668 > h_SWAP x_19668 2315  MOV x_19669 > h_MOV x_19669 2316  MOVX x_19670 > h_MOVX x_19670 2317  SETB x_19671 > h_SETB x_19671 2318  PUSH x_19672 > h_PUSH x_19672 2319  POP x_19673 > h_POP x_19673 2320  XCH (x_19675, x_19674) > h_XCH x_19675 x_19674 2321  XCHD (x_19677, x_19676) > h_XCHD x_19677 x_19676 2315 2322  RET > h_RET 2316 2323  RETI > h_RETI 2317 2324  NOP > h_NOP 2325  JMP x_19678 > h_JMP x_19678 2318 2326 2319 2327 (** val preinstruction_rect_Type2 : … … 2351 2359 (subaddressing_mode > 'a2) > (subaddressing_mode > subaddressing_mode 2352 2360 > 'a2) > (subaddressing_mode > subaddressing_mode > 'a2) > 'a2 > 2353 'a2 > 'a2 > 'a1 preinstruction > 'a2 **)2354 let 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 = function2355  ADD (x_1 054, x_1053) > h_ADD x_1054 x_10532356  ADDC (x_1 056, x_1055) > h_ADDC x_1056 x_10552357  SUBB (x_1 058, x_1057) > h_SUBB x_1058 x_10572358  INC x_1 059 > h_INC x_10592359  DEC x_1 060 > h_DEC x_10602360  MUL (x_1 062, x_1061) > h_MUL x_1062 x_10612361  DIV (x_1 064, x_1063) > h_DIV x_1064 x_10632362  DA x_1 065 > h_DA x_10652363  JC x_1 066 > h_JC x_10662364  JNC x_1 067 > h_JNC x_10672365  JB (x_1 069, x_1068) > h_JB x_1069 x_10682366  JNB (x_1 071, x_1070) > h_JNB x_1071 x_10702367  JBC (x_1 073, x_1072) > h_JBC x_1073 x_10722368  JZ x_1 074 > h_JZ x_10742369  JNZ x_1 075 > h_JNZ x_10752370  CJNE (x_1 077, x_1076) > h_CJNE x_1077 x_10762371  DJNZ (x_1 079, x_1078) > h_DJNZ x_1079 x_10782372  ANL x_1 080 > h_ANL x_10802373  ORL x_1 081 > h_ORL x_10812374  XRL x_1 082 > h_XRL x_10822375  CLR x_1 083 > h_CLR x_10832376  CPL x_1 084 > h_CPL x_10842377  RL x_1 085 > h_RL x_10852378  RLC x_1 086 > h_RLC x_10862379  RR x_1 087 > h_RR x_10872380  RRC x_1 088 > h_RRC x_10882381  SWAP x_1 089 > h_SWAP x_10892382  MOV x_1 090 > h_MOV x_10902383  MOVX x_1 091 > h_MOVX x_10912384  SETB x_1 092 > h_SETB x_10922385  PUSH x_1 093 > h_PUSH x_10932386  POP x_1 094 > h_POP x_10942387  XCH (x_1 096, x_1095) > h_XCH x_1096 x_10952388  XCHD (x_1 098, x_1097) > h_XCHD x_1098 x_10972361 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2362 let 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 2363  ADD (x_19719, x_19718) > h_ADD x_19719 x_19718 2364  ADDC (x_19721, x_19720) > h_ADDC x_19721 x_19720 2365  SUBB (x_19723, x_19722) > h_SUBB x_19723 x_19722 2366  INC x_19724 > h_INC x_19724 2367  DEC x_19725 > h_DEC x_19725 2368  MUL (x_19727, x_19726) > h_MUL x_19727 x_19726 2369  DIV (x_19729, x_19728) > h_DIV x_19729 x_19728 2370  DA x_19730 > h_DA x_19730 2371  JC x_19731 > h_JC x_19731 2372  JNC x_19732 > h_JNC x_19732 2373  JB (x_19734, x_19733) > h_JB x_19734 x_19733 2374  JNB (x_19736, x_19735) > h_JNB x_19736 x_19735 2375  JBC (x_19738, x_19737) > h_JBC x_19738 x_19737 2376  JZ x_19739 > h_JZ x_19739 2377  JNZ x_19740 > h_JNZ x_19740 2378  CJNE (x_19742, x_19741) > h_CJNE x_19742 x_19741 2379  DJNZ (x_19744, x_19743) > h_DJNZ x_19744 x_19743 2380  ANL x_19745 > h_ANL x_19745 2381  ORL x_19746 > h_ORL x_19746 2382  XRL x_19747 > h_XRL x_19747 2383  CLR x_19748 > h_CLR x_19748 2384  CPL x_19749 > h_CPL x_19749 2385  RL x_19750 > h_RL x_19750 2386  RLC x_19751 > h_RLC x_19751 2387  RR x_19752 > h_RR x_19752 2388  RRC x_19753 > h_RRC x_19753 2389  SWAP x_19754 > h_SWAP x_19754 2390  MOV x_19755 > h_MOV x_19755 2391  MOVX x_19756 > h_MOVX x_19756 2392  SETB x_19757 > h_SETB x_19757 2393  PUSH x_19758 > h_PUSH x_19758 2394  POP x_19759 > h_POP x_19759 2395  XCH (x_19761, x_19760) > h_XCH x_19761 x_19760 2396  XCHD (x_19763, x_19762) > h_XCHD x_19763 x_19762 2389 2397  RET > h_RET 2390 2398  RETI > h_RETI 2391 2399  NOP > h_NOP 2400  JMP x_19764 > h_JMP x_19764 2392 2401 2393 2402 (** val preinstruction_rect_Type1 : … … 2425 2434 (subaddressing_mode > 'a2) > (subaddressing_mode > subaddressing_mode 2426 2435 > 'a2) > (subaddressing_mode > subaddressing_mode > 'a2) > 'a2 > 2427 'a2 > 'a2 > 'a1 preinstruction > 'a2 **)2428 let 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 = function2429  ADD (x_1 138, x_1137) > h_ADD x_1138 x_11372430  ADDC (x_1 140, x_1139) > h_ADDC x_1140 x_11392431  SUBB (x_1 142, x_1141) > h_SUBB x_1142 x_11412432  INC x_1 143 > h_INC x_11432433  DEC x_1 144 > h_DEC x_11442434  MUL (x_1 146, x_1145) > h_MUL x_1146 x_11452435  DIV (x_1 148, x_1147) > h_DIV x_1148 x_11472436  DA x_1 149 > h_DA x_11492437  JC x_1 150 > h_JC x_11502438  JNC x_1 151 > h_JNC x_11512439  JB (x_1 153, x_1152) > h_JB x_1153 x_11522440  JNB (x_1 155, x_1154) > h_JNB x_1155 x_11542441  JBC (x_1 157, x_1156) > h_JBC x_1157 x_11562442  JZ x_1 158 > h_JZ x_11582443  JNZ x_1 159 > h_JNZ x_11592444  CJNE (x_1 161, x_1160) > h_CJNE x_1161 x_11602445  DJNZ (x_1 163, x_1162) > h_DJNZ x_1163 x_11622446  ANL x_1 164 > h_ANL x_11642447  ORL x_1 165 > h_ORL x_11652448  XRL x_1 166 > h_XRL x_11662449  CLR x_1 167 > h_CLR x_11672450  CPL x_1 168 > h_CPL x_11682451  RL x_1 169 > h_RL x_11692452  RLC x_1 170 > h_RLC x_11702453  RR x_1 171 > h_RR x_11712454  RRC x_1 172 > h_RRC x_11722455  SWAP x_1 173 > h_SWAP x_11732456  MOV x_1 174 > h_MOV x_11742457  MOVX x_1 175 > h_MOVX x_11752458  SETB x_1 176 > h_SETB x_11762459  PUSH x_1 177 > h_PUSH x_11772460  POP x_1 178 > h_POP x_11782461  XCH (x_1 180, x_1179) > h_XCH x_1180 x_11792462  XCHD (x_1 182, x_1181) > h_XCHD x_1182 x_11812436 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2437 let 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 2438  ADD (x_19805, x_19804) > h_ADD x_19805 x_19804 2439  ADDC (x_19807, x_19806) > h_ADDC x_19807 x_19806 2440  SUBB (x_19809, x_19808) > h_SUBB x_19809 x_19808 2441  INC x_19810 > h_INC x_19810 2442  DEC x_19811 > h_DEC x_19811 2443  MUL (x_19813, x_19812) > h_MUL x_19813 x_19812 2444  DIV (x_19815, x_19814) > h_DIV x_19815 x_19814 2445  DA x_19816 > h_DA x_19816 2446  JC x_19817 > h_JC x_19817 2447  JNC x_19818 > h_JNC x_19818 2448  JB (x_19820, x_19819) > h_JB x_19820 x_19819 2449  JNB (x_19822, x_19821) > h_JNB x_19822 x_19821 2450  JBC (x_19824, x_19823) > h_JBC x_19824 x_19823 2451  JZ x_19825 > h_JZ x_19825 2452  JNZ x_19826 > h_JNZ x_19826 2453  CJNE (x_19828, x_19827) > h_CJNE x_19828 x_19827 2454  DJNZ (x_19830, x_19829) > h_DJNZ x_19830 x_19829 2455  ANL x_19831 > h_ANL x_19831 2456  ORL x_19832 > h_ORL x_19832 2457  XRL x_19833 > h_XRL x_19833 2458  CLR x_19834 > h_CLR x_19834 2459  CPL x_19835 > h_CPL x_19835 2460  RL x_19836 > h_RL x_19836 2461  RLC x_19837 > h_RLC x_19837 2462  RR x_19838 > h_RR x_19838 2463  RRC x_19839 > h_RRC x_19839 2464  SWAP x_19840 > h_SWAP x_19840 2465  MOV x_19841 > h_MOV x_19841 2466  MOVX x_19842 > h_MOVX x_19842 2467  SETB x_19843 > h_SETB x_19843 2468  PUSH x_19844 > h_PUSH x_19844 2469  POP x_19845 > h_POP x_19845 2470  XCH (x_19847, x_19846) > h_XCH x_19847 x_19846 2471  XCHD (x_19849, x_19848) > h_XCHD x_19849 x_19848 2463 2472  RET > h_RET 2464 2473  RETI > h_RETI 2465 2474  NOP > h_NOP 2475  JMP x_19850 > h_JMP x_19850 2466 2476 2467 2477 (** val preinstruction_rect_Type0 : … … 2499 2509 (subaddressing_mode > 'a2) > (subaddressing_mode > subaddressing_mode 2500 2510 > 'a2) > (subaddressing_mode > subaddressing_mode > 'a2) > 'a2 > 2501 'a2 > 'a2 > 'a1 preinstruction > 'a2 **)2502 let 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 = function2503  ADD (x_1 222, x_1221) > h_ADD x_1222 x_12212504  ADDC (x_1 224, x_1223) > h_ADDC x_1224 x_12232505  SUBB (x_1 226, x_1225) > h_SUBB x_1226 x_12252506  INC x_1 227 > h_INC x_12272507  DEC x_1 228 > h_DEC x_12282508  MUL (x_1 230, x_1229) > h_MUL x_1230 x_12292509  DIV (x_1 232, x_1231) > h_DIV x_1232 x_12312510  DA x_1 233 > h_DA x_12332511  JC x_1 234 > h_JC x_12342512  JNC x_1 235 > h_JNC x_12352513  JB (x_1 237, x_1236) > h_JB x_1237 x_12362514  JNB (x_1 239, x_1238) > h_JNB x_1239 x_12382515  JBC (x_1 241, x_1240) > h_JBC x_1241 x_12402516  JZ x_1 242 > h_JZ x_12422517  JNZ x_1 243 > h_JNZ x_12432518  CJNE (x_1 245, x_1244) > h_CJNE x_1245 x_12442519  DJNZ (x_1 247, x_1246) > h_DJNZ x_1247 x_12462520  ANL x_1 248 > h_ANL x_12482521  ORL x_1 249 > h_ORL x_12492522  XRL x_1 250 > h_XRL x_12502523  CLR x_1 251 > h_CLR x_12512524  CPL x_1 252 > h_CPL x_12522525  RL x_1 253 > h_RL x_12532526  RLC x_1 254 > h_RLC x_12542527  RR x_1 255 > h_RR x_12552528  RRC x_1 256 > h_RRC x_12562529  SWAP x_1 257 > h_SWAP x_12572530  MOV x_1 258 > h_MOV x_12582531  MOVX x_1 259 > h_MOVX x_12592532  SETB x_1 260 > h_SETB x_12602533  PUSH x_1 261 > h_PUSH x_12612534  POP x_1 262 > h_POP x_12622535  XCH (x_1 264, x_1263) > h_XCH x_1264 x_12632536  XCHD (x_1 266, x_1265) > h_XCHD x_1266 x_12652511 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2512 let 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 2513  ADD (x_19891, x_19890) > h_ADD x_19891 x_19890 2514  ADDC (x_19893, x_19892) > h_ADDC x_19893 x_19892 2515  SUBB (x_19895, x_19894) > h_SUBB x_19895 x_19894 2516  INC x_19896 > h_INC x_19896 2517  DEC x_19897 > h_DEC x_19897 2518  MUL (x_19899, x_19898) > h_MUL x_19899 x_19898 2519  DIV (x_19901, x_19900) > h_DIV x_19901 x_19900 2520  DA x_19902 > h_DA x_19902 2521  JC x_19903 > h_JC x_19903 2522  JNC x_19904 > h_JNC x_19904 2523  JB (x_19906, x_19905) > h_JB x_19906 x_19905 2524  JNB (x_19908, x_19907) > h_JNB x_19908 x_19907 2525  JBC (x_19910, x_19909) > h_JBC x_19910 x_19909 2526  JZ x_19911 > h_JZ x_19911 2527  JNZ x_19912 > h_JNZ x_19912 2528  CJNE (x_19914, x_19913) > h_CJNE x_19914 x_19913 2529  DJNZ (x_19916, x_19915) > h_DJNZ x_19916 x_19915 2530  ANL x_19917 > h_ANL x_19917 2531  ORL x_19918 > h_ORL x_19918 2532  XRL x_19919 > h_XRL x_19919 2533  CLR x_19920 > h_CLR x_19920 2534  CPL x_19921 > h_CPL x_19921 2535  RL x_19922 > h_RL x_19922 2536  RLC x_19923 > h_RLC x_19923 2537  RR x_19924 > h_RR x_19924 2538  RRC x_19925 > h_RRC x_19925 2539  SWAP x_19926 > h_SWAP x_19926 2540  MOV x_19927 > h_MOV x_19927 2541  MOVX x_19928 > h_MOVX x_19928 2542  SETB x_19929 > h_SETB x_19929 2543  PUSH x_19930 > h_PUSH x_19930 2544  POP x_19931 > h_POP x_19931 2545  XCH (x_19933, x_19932) > h_XCH x_19933 x_19932 2546  XCHD (x_19935, x_19934) > h_XCHD x_19935 x_19934 2537 2547  RET > h_RET 2538 2548  RETI > h_RETI 2539 2549  NOP > h_NOP 2550  JMP x_19936 > h_JMP x_19936 2540 2551 2541 2552 (** val preinstruction_inv_rect_Type4 : … … 2575 2586 > (subaddressing_mode > subaddressing_mode > __ > 'a2) > 2576 2587 (subaddressing_mode > subaddressing_mode > __ > 'a2) > (__ > 'a2) > 2577 (__ > 'a2) > (__ > 'a2) > 'a2 **)2578 let preinstruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =2588 (__ > 'a2) > (__ > 'a2) > (subaddressing_mode > __ > 'a2) > 'a2 **) 2589 let preinstruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 = 2579 2590 let hcut = 2580 2591 preinstruction_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 2581 2592 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 2582 h33 h34 h35 h36 h37 h term2593 h33 h34 h35 h36 h37 h38 hterm 2583 2594 in 2584 2595 hcut __ … … 2620 2631 > (subaddressing_mode > subaddressing_mode > __ > 'a2) > 2621 2632 (subaddressing_mode > subaddressing_mode > __ > 'a2) > (__ > 'a2) > 2622 (__ > 'a2) > (__ > 'a2) > 'a2 **)2623 let preinstruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =2633 (__ > 'a2) > (__ > 'a2) > (subaddressing_mode > __ > 'a2) > 'a2 **) 2634 let preinstruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 = 2624 2635 let hcut = 2625 2636 preinstruction_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 2626 2637 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 2627 h33 h34 h35 h36 h37 h term2638 h33 h34 h35 h36 h37 h38 hterm 2628 2639 in 2629 2640 hcut __ … … 2665 2676 > (subaddressing_mode > subaddressing_mode > __ > 'a2) > 2666 2677 (subaddressing_mode > subaddressing_mode > __ > 'a2) > (__ > 'a2) > 2667 (__ > 'a2) > (__ > 'a2) > 'a2 **)2668 let preinstruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =2678 (__ > 'a2) > (__ > 'a2) > (subaddressing_mode > __ > 'a2) > 'a2 **) 2679 let preinstruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 = 2669 2680 let hcut = 2670 2681 preinstruction_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 2671 2682 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 2672 h33 h34 h35 h36 h37 h term2683 h33 h34 h35 h36 h37 h38 hterm 2673 2684 in 2674 2685 hcut __ … … 2710 2721 > (subaddressing_mode > subaddressing_mode > __ > 'a2) > 2711 2722 (subaddressing_mode > subaddressing_mode > __ > 'a2) > (__ > 'a2) > 2712 (__ > 'a2) > (__ > 'a2) > 'a2 **)2713 let preinstruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =2723 (__ > 'a2) > (__ > 'a2) > (subaddressing_mode > __ > 'a2) > 'a2 **) 2724 let preinstruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 = 2714 2725 let hcut = 2715 2726 preinstruction_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 2716 2727 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 2717 h33 h34 h35 h36 h37 h term2728 h33 h34 h35 h36 h37 h38 hterm 2718 2729 in 2719 2730 hcut __ … … 2755 2766 > (subaddressing_mode > subaddressing_mode > __ > 'a2) > 2756 2767 (subaddressing_mode > subaddressing_mode > __ > 'a2) > (__ > 'a2) > 2757 (__ > 'a2) > (__ > 'a2) > 'a2 **)2758 let preinstruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 =2768 (__ > 'a2) > (__ > 'a2) > (subaddressing_mode > __ > 'a2) > 'a2 **) 2769 let preinstruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 = 2759 2770 let hcut = 2760 2771 preinstruction_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 2761 2772 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 2762 h33 h34 h35 h36 h37 h term2773 h33 h34 h35 h36 h37 h38 hterm 2763 2774 in 2764 2775 hcut __ … … 2805 2816  RET > Obj.magic (fun _ dH > dH) 2806 2817  RETI > Obj.magic (fun _ dH > dH) 2807  NOP > Obj.magic (fun _ dH > dH)) y 2818  NOP > Obj.magic (fun _ dH > dH) 2819  JMP a0 > Obj.magic (fun _ dH > dH __)) y 2808 2820 2809 2821 (** val preinstruction_jmdiscr : … … 2848 2860  RET > Obj.magic (fun _ dH > dH) 2849 2861  RETI > Obj.magic (fun _ dH > dH) 2850  NOP > Obj.magic (fun _ dH > dH)) y 2862  NOP > Obj.magic (fun _ dH > dH) 2863  JMP a0 > Obj.magic (fun _ dH > dH __)) y 2851 2864 2852 2865 (** val eq_preinstruction : … … 2908 2921  RET > Bool.False 2909 2922  RETI > Bool.False 2910  NOP > Bool.False) 2923  NOP > Bool.False 2924  JMP x > Bool.False) 2911 2925  ADDC (arg1, arg2) > 2912 2926 (match j with … … 2962 2976  RET > Bool.False 2963 2977  RETI > Bool.False 2964  NOP > Bool.False) 2978  NOP > Bool.False 2979  JMP x > Bool.False) 2965 2980  SUBB (arg1, arg2) > 2966 2981 (match j with … … 3016 3031  RET > Bool.False 3017 3032  RETI > Bool.False 3018  NOP > Bool.False) 3033  NOP > Bool.False 3034  JMP x > Bool.False) 3019 3035  INC arg > 3020 3036 (match j with … … 3068 3084  RET > Bool.False 3069 3085  RETI > Bool.False 3070  NOP > Bool.False) 3086  NOP > Bool.False 3087  JMP x > Bool.False) 3071 3088  DEC arg > 3072 3089 (match j with … … 3116 3133  RET > Bool.False 3117 3134  RETI > Bool.False 3118  NOP > Bool.False) 3135  NOP > Bool.False 3136  JMP x > Bool.False) 3119 3137  MUL (arg1, arg2) > 3120 3138 (match j with … … 3166 3184  RET > Bool.False 3167 3185  RETI > Bool.False 3168  NOP > Bool.False) 3186  NOP > Bool.False 3187  JMP x > Bool.False) 3169 3188  DIV (arg1, arg2) > 3170 3189 (match j with … … 3216 3235  RET > Bool.False 3217 3236  RETI > Bool.False 3218  NOP > Bool.False) 3237  NOP > Bool.False 3238  JMP x > Bool.False) 3219 3239  DA arg > 3220 3240 (match j with … … 3260 3280  RET > Bool.False 3261 3281  RETI > Bool.False 3262  NOP > Bool.False) 3282  NOP > Bool.False 3283  JMP x > Bool.False) 3263 3284  JC arg > 3264 3285 (match j with … … 3304 3325  RET > Bool.False 3305 3326  RETI > Bool.False 3306  NOP > Bool.False) 3327  NOP > Bool.False 3328  JMP x > Bool.False) 3307 3329  JNC arg > 3308 3330 (match j with … … 3348 3370  RET > Bool.False 3349 3371  RETI > Bool.False 3350  NOP > Bool.False) 3372  NOP > Bool.False 3373  JMP x > Bool.False) 3351 3374  JB (arg1, arg2) > 3352 3375 (match j with … … 3398 3421  RET > Bool.False 3399 3422  RETI > Bool.False 3400  NOP > Bool.False) 3423  NOP > Bool.False 3424  JMP x > Bool.False) 3401 3425  JNB (arg1, arg2) > 3402 3426 (match j with … … 3448 3472  RET > Bool.False 3449 3473  RETI > Bool.False 3450  NOP > Bool.False) 3474  NOP > Bool.False 3475  JMP x > Bool.False) 3451 3476  JBC (arg1, arg2) > 3452 3477 (match j with … … 3498 3523  RET > Bool.False 3499 3524  RETI > Bool.False 3500  NOP > Bool.False) 3525  NOP > Bool.False 3526  JMP x > Bool.False) 3501 3527  JZ arg > 3502 3528 (match j with … … 3542 3568  RET > Bool.False 3543 3569  RETI > Bool.False 3544  NOP > Bool.False) 3570  NOP > Bool.False 3571  JMP x > Bool.False) 3545 3572  JNZ arg > 3546 3573 (match j with … … 3586 3613  RET > Bool.False 3587 3614  RETI > Bool.False 3588  NOP > Bool.False) 3615  NOP > Bool.False 3616  JMP x > Bool.False) 3589 3617  CJNE (arg1, arg2) > 3590 3618 (match j with … … 3662 3690  RET > Bool.False 3663 3691  RETI > Bool.False 3664  NOP > Bool.False) 3692  NOP > Bool.False 3693  JMP x > Bool.False) 3665 3694  DJNZ (arg1, arg2) > 3666 3695 (match j with … … 3712 3741  RET > Bool.False 3713 3742  RETI > Bool.False 3714  NOP > Bool.False) 3743  NOP > Bool.False 3744  JMP x > Bool.False) 3715 3745  ANL arg > 3716 3746 (match j with … … 3802 3832  RET > Bool.False 3803 3833  RETI > Bool.False 3804  NOP > Bool.False) 3834  NOP > Bool.False 3835  JMP x > Bool.False) 3805 3836  ORL arg > 3806 3837 (match j with … … 3892 3923  RET > Bool.False 3893 3924  RETI > Bool.False 3894  NOP > Bool.False) 3925  NOP > Bool.False 3926  JMP x > Bool.False) 3895 3927  XRL arg > 3896 3928 (match j with … … 3966 3998  RET > Bool.False 3967 3999  RETI > Bool.False 3968  NOP > Bool.False) 4000  NOP > Bool.False 4001  JMP x > Bool.False) 3969 4002  CLR arg > 3970 4003 (match j with … … 4012 4045  RET > Bool.False 4013 4046  RETI > Bool.False 4014  NOP > Bool.False) 4047  NOP > Bool.False 4048  JMP x > Bool.False) 4015 4049  CPL arg > 4016 4050 (match j with … … 4058 4092  RET > Bool.False 4059 4093  RETI > Bool.False 4060  NOP > Bool.False) 4094  NOP > Bool.False 4095  JMP x > Bool.False) 4061 4096  RL arg > 4062 4097 (match j with … … 4102 4137  RET > Bool.False 4103 4138  RETI > Bool.False 4104  NOP > Bool.False) 4139  NOP > Bool.False 4140  JMP x > Bool.False) 4105 4141  RLC arg > 4106 4142 (match j with … … 4146 4182  RET > Bool.False 4147 4183  RETI > Bool.False 4148  NOP > Bool.False) 4184  NOP > Bool.False 4185  JMP x > Bool.False) 4149 4186  RR arg > 4150 4187 (match j with … … 4190 4227  RET > Bool.False 4191 4228  RETI > Bool.False 4192  NOP > Bool.False) 4229  NOP > Bool.False 4230  JMP x > Bool.False) 4193 4231  RRC arg > 4194 4232 (match j with … … 4234 4272  RET > Bool.False 4235 4273  RETI > Bool.False 4236  NOP > Bool.False) 4274  NOP > Bool.False 4275  JMP x > Bool.False) 4237 4276  SWAP arg > 4238 4277 (match j with … … 4278 4317  RET > Bool.False 4279 4318  RETI > Bool.False 4280  NOP > Bool.False) 4319  NOP > Bool.False 4320  JMP x > Bool.False) 4281 4321  MOV arg > 4282 4322 (match j with … … 4418 4458  RET > Bool.False 4419 4459  RETI > Bool.False 4420  NOP > Bool.False) 4460  NOP > Bool.False 4461  JMP x > Bool.False) 4421 4462  MOVX arg > 4422 4463 (match j with … … 4488 4529  RET > Bool.False 4489 4530  RETI > Bool.False 4490  NOP > Bool.False) 4531  NOP > Bool.False 4532  JMP x > Bool.False) 4491 4533  SETB arg > 4492 4534 (match j with … … 4532 4574  RET > Bool.False 4533 4575  RETI > Bool.False 4534  NOP > Bool.False) 4576  NOP > Bool.False 4577  JMP x > Bool.False) 4535 4578  PUSH arg > 4536 4579 (match j with … … 4576 4619  RET > Bool.False 4577 4620  RETI > Bool.False 4578  NOP > Bool.False) 4621  NOP > Bool.False 4622  JMP x > Bool.False) 4579 4623  POP arg > 4580 4624 (match j with … … 4620 4664  RET > Bool.False 4621 4665  RETI > Bool.False 4622  NOP > Bool.False) 4666  NOP > Bool.False 4667  JMP x > Bool.False) 4623 4668  XCH (arg1, arg2) > 4624 4669 (match j with … … 4672 4717  RET > Bool.False 4673 4718  RETI > Bool.False 4674  NOP > Bool.False) 4719  NOP > Bool.False 4720  JMP x > Bool.False) 4675 4721  XCHD (arg1, arg2) > 4676 4722 (match j with … … 4722 4768  RET > Bool.False 4723 4769  RETI > Bool.False 4724  NOP > Bool.False) 4770  NOP > Bool.False 4771  JMP x > Bool.False) 4725 4772  RET > 4726 4773 (match j with … … 4761 4808  RET > Bool.True 4762 4809  RETI > Bool.False 4763  NOP > Bool.False) 4810  NOP > Bool.False 4811  JMP x > Bool.False) 4764 4812  RETI > 4765 4813 (match j with … … 4800 4848  RET > Bool.False 4801 4849  RETI > Bool.True 4802  NOP > Bool.False) 4850  NOP > Bool.False 4851  JMP x > Bool.False) 4803 4852  NOP > 4804 4853 (match j with … … 4839 4888  RET > Bool.False 4840 4889  RETI > Bool.False 4841  NOP > Bool.True) 4890  NOP > Bool.True 4891  JMP x > Bool.False) 4892  JMP arg > 4893 (match j with 4894  ADD (x, x0) > Bool.False 4895  ADDC (x, x0) > Bool.False 4896  SUBB (x, x0) > Bool.False 4897  INC x > Bool.False 4898  DEC x > Bool.False 4899  MUL (x, x0) > Bool.False 4900  DIV (x, x0) > Bool.False 4901  DA x > Bool.False 4902  JC x > Bool.False 4903  JNC x > Bool.False 4904  JB (x, x0) > Bool.False 4905  JNB (x, x0) > Bool.False 4906  JBC (x, x0) > Bool.False 4907  JZ x > Bool.False 4908  JNZ x > Bool.False 4909  CJNE (x, x0) > Bool.False 4910  DJNZ (x, x0) > Bool.False 4911  ANL x > Bool.False 4912  ORL x > Bool.False 4913  XRL x > Bool.False 4914  CLR x > Bool.False 4915  CPL x > Bool.False 4916  RL x > Bool.False 4917  RLC x > Bool.False 4918  RR x > Bool.False 4919  RRC x > Bool.False 4920  SWAP x > Bool.False 4921  MOV x > Bool.False 4922  MOVX x > Bool.False 4923  SETB x > Bool.False 4924  PUSH x > Bool.False 4925  POP x > Bool.False 4926  XCH (x, x0) > Bool.False 4927  XCHD (x, x0) > Bool.False 4928  RET > Bool.False 4929  RETI > Bool.False 4930  NOP > Bool.False 4931  JMP arg' > 4932 eq_addressing_mode 4933 (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Indirect_dptr, 4934 Vector.VEmpty)) arg) 4935 (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Indirect_dptr, 4936 Vector.VEmpty)) arg')) 4842 4937 4843 4938 type instruction = … … 4847 4942  LJMP of subaddressing_mode 4848 4943  SJMP of subaddressing_mode 4849  JMP of subaddressing_mode4850 4944  MOVC of subaddressing_mode * subaddressing_mode 4851 4945  RealInstruction of subaddressing_mode preinstruction … … 4854 4948 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4855 4949 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4856 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4857 (subaddressing_mode > subaddressing_mode > 'a1) > (subaddressing_mode 4858 preinstruction > 'a1) > instruction > 'a1 **) 4859 let rec instruction_rect_Type4 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function 4860  ACALL x_1827 > h_ACALL x_1827 4861  LCALL x_1828 > h_LCALL x_1828 4862  AJMP x_1829 > h_AJMP x_1829 4863  LJMP x_1830 > h_LJMP x_1830 4864  SJMP x_1831 > h_SJMP x_1831 4865  JMP x_1832 > h_JMP x_1832 4866  MOVC (x_1834, x_1833) > h_MOVC x_1834 x_1833 4867  RealInstruction x_1835 > h_RealInstruction x_1835 4950 (subaddressing_mode > 'a1) > (subaddressing_mode > subaddressing_mode 4951 > 'a1) > (subaddressing_mode preinstruction > 'a1) > instruction > 4952 'a1 **) 4953 let rec instruction_rect_Type4 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function 4954  ACALL x_20508 > h_ACALL x_20508 4955  LCALL x_20509 > h_LCALL x_20509 4956  AJMP x_20510 > h_AJMP x_20510 4957  LJMP x_20511 > h_LJMP x_20511 4958  SJMP x_20512 > h_SJMP x_20512 4959  MOVC (x_20514, x_20513) > h_MOVC x_20514 x_20513 4960  RealInstruction x_20515 > h_RealInstruction x_20515 4868 4961 4869 4962 (** val instruction_rect_Type5 : 4870 4963 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4871 4964 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4872 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4873 (subaddressing_mode > subaddressing_mode > 'a1) > (subaddressing_mode 4874 preinstruction > 'a1) > instruction > 'a1 **) 4875 let rec instruction_rect_Type5 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function 4876  ACALL x_1845 > h_ACALL x_1845 4877  LCALL x_1846 > h_LCALL x_1846 4878  AJMP x_1847 > h_AJMP x_1847 4879  LJMP x_1848 > h_LJMP x_1848 4880  SJMP x_1849 > h_SJMP x_1849 4881  JMP x_1850 > h_JMP x_1850 4882  MOVC (x_1852, x_1851) > h_MOVC x_1852 x_1851 4883  RealInstruction x_1853 > h_RealInstruction x_1853 4965 (subaddressing_mode > 'a1) > (subaddressing_mode > subaddressing_mode 4966 > 'a1) > (subaddressing_mode preinstruction > 'a1) > instruction > 4967 'a1 **) 4968 let rec instruction_rect_Type5 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function 4969  ACALL x_20524 > h_ACALL x_20524 4970  LCALL x_20525 > h_LCALL x_20525 4971  AJMP x_20526 > h_AJMP x_20526 4972  LJMP x_20527 > h_LJMP x_20527 4973  SJMP x_20528 > h_SJMP x_20528 4974  MOVC (x_20530, x_20529) > h_MOVC x_20530 x_20529 4975  RealInstruction x_20531 > h_RealInstruction x_20531 4884 4976 4885 4977 (** val instruction_rect_Type3 : 4886 4978 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4887 4979 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4888 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4889 (subaddressing_mode > subaddressing_mode > 'a1) > (subaddressing_mode 4890 preinstruction > 'a1) > instruction > 'a1 **) 4891 let rec instruction_rect_Type3 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function 4892  ACALL x_1863 > h_ACALL x_1863 4893  LCALL x_1864 > h_LCALL x_1864 4894  AJMP x_1865 > h_AJMP x_1865 4895  LJMP x_1866 > h_LJMP x_1866 4896  SJMP x_1867 > h_SJMP x_1867 4897  JMP x_1868 > h_JMP x_1868 4898  MOVC (x_1870, x_1869) > h_MOVC x_1870 x_1869 4899  RealInstruction x_1871 > h_RealInstruction x_1871 4980 (subaddressing_mode > 'a1) > (subaddressing_mode > subaddressing_mode 4981 > 'a1) > (subaddressing_mode preinstruction > 'a1) > instruction > 4982 'a1 **) 4983 let rec instruction_rect_Type3 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function 4984  ACALL x_20540 > h_ACALL x_20540 4985  LCALL x_20541 > h_LCALL x_20541 4986  AJMP x_20542 > h_AJMP x_20542 4987  LJMP x_20543 > h_LJMP x_20543 4988  SJMP x_20544 > h_SJMP x_20544 4989  MOVC (x_20546, x_20545) > h_MOVC x_20546 x_20545 4990  RealInstruction x_20547 > h_RealInstruction x_20547 4900 4991 4901 4992 (** val instruction_rect_Type2 : 4902 4993 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4903 4994 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4904 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4905 (subaddressing_mode > subaddressing_mode > 'a1) > (subaddressing_mode 4906 preinstruction > 'a1) > instruction > 'a1 **) 4907 let rec instruction_rect_Type2 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function 4908  ACALL x_1881 > h_ACALL x_1881 4909  LCALL x_1882 > h_LCALL x_1882 4910  AJMP x_1883 > h_AJMP x_1883 4911  LJMP x_1884 > h_LJMP x_1884 4912  SJMP x_1885 > h_SJMP x_1885 4913  JMP x_1886 > h_JMP x_1886 4914  MOVC (x_1888, x_1887) > h_MOVC x_1888 x_1887 4915  RealInstruction x_1889 > h_RealInstruction x_1889 4995 (subaddressing_mode > 'a1) > (subaddressing_mode > subaddressing_mode 4996 > 'a1) > (subaddressing_mode preinstruction > 'a1) > instruction > 4997 'a1 **) 4998 let rec instruction_rect_Type2 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function 4999  ACALL x_20556 > h_ACALL x_20556 5000  LCALL x_20557 > h_LCALL x_20557 5001  AJMP x_20558 > h_AJMP x_20558 5002  LJMP x_20559 > h_LJMP x_20559 5003  SJMP x_20560 > h_SJMP x_20560 5004  MOVC (x_20562, x_20561) > h_MOVC x_20562 x_20561 5005  RealInstruction x_20563 > h_RealInstruction x_20563 4916 5006 4917 5007 (** val instruction_rect_Type1 : 4918 5008 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4919 5009 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4920 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4921 (subaddressing_mode > subaddressing_mode > 'a1) > (subaddressing_mode 4922 preinstruction > 'a1) > instruction > 'a1 **) 4923 let rec instruction_rect_Type1 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function 4924  ACALL x_1899 > h_ACALL x_1899 4925  LCALL x_1900 > h_LCALL x_1900 4926  AJMP x_1901 > h_AJMP x_1901 4927  LJMP x_1902 > h_LJMP x_1902 4928  SJMP x_1903 > h_SJMP x_1903 4929  JMP x_1904 > h_JMP x_1904 4930  MOVC (x_1906, x_1905) > h_MOVC x_1906 x_1905 4931  RealInstruction x_1907 > h_RealInstruction x_1907 5010 (subaddressing_mode > 'a1) > (subaddressing_mode > subaddressing_mode 5011 > 'a1) > (subaddressing_mode preinstruction > 'a1) > instruction > 5012 'a1 **) 5013 let rec instruction_rect_Type1 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function 5014  ACALL x_20572 > h_ACALL x_20572 5015  LCALL x_20573 > h_LCALL x_20573 5016  AJMP x_20574 > h_AJMP x_20574 5017  LJMP x_20575 > h_LJMP x_20575 5018  SJMP x_20576 > h_SJMP x_20576 5019  MOVC (x_20578, x_20577) > h_MOVC x_20578 x_20577 5020  RealInstruction x_20579 > h_RealInstruction x_20579 4932 5021 4933 5022 (** val instruction_rect_Type0 : 4934 5023 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4935 5024 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4936 (subaddressing_mode > 'a1) > (subaddressing_mode > 'a1) > 4937 (subaddressing_mode > subaddressing_mode > 'a1) > (subaddressing_mode 4938 preinstruction > 'a1) > instruction > 'a1 **) 4939 let rec instruction_rect_Type0 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_JMP h_MOVC h_RealInstruction = function 4940  ACALL x_1917 > h_ACALL x_1917 4941  LCALL x_1918 > h_LCALL x_1918 4942  AJMP x_1919 > h_AJMP x_1919 4943  LJMP x_1920 > h_LJMP x_1920 4944  SJMP x_1921 > h_SJMP x_1921 4945  JMP x_1922 > h_JMP x_1922 4946  MOVC (x_1924, x_1923) > h_MOVC x_1924 x_1923 4947  RealInstruction x_1925 > h_RealInstruction x_1925 5025 (subaddressing_mode > 'a1) > (subaddressing_mode > subaddressing_mode 5026 > 'a1) > (subaddressing_mode preinstruction > 'a1) > instruction > 5027 'a1 **) 5028 let rec instruction_rect_Type0 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function 5029  ACALL x_20588 > h_ACALL x_20588 5030  LCALL x_20589 > h_LCALL x_20589 5031  AJMP x_20590 > h_AJMP x_20590 5032  LJMP x_20591 > h_LJMP x_20591 5033  SJMP x_20592 > h_SJMP x_20592 5034  MOVC (x_20594, x_20593) > h_MOVC x_20594 x_20593 5035  RealInstruction x_20595 > h_RealInstruction x_20595 4948 5036 4949 5037 (** val instruction_inv_rect_Type4 : … … 4951 5039 > __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode 4952 5040 > __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode 4953 > __ > 'a1) > (subaddressing_mode > subaddressing_mode > __ > 'a1)4954 > (subaddressing_mode preinstruction >__ > 'a1) > 'a1 **)4955 let instruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8=4956 let hcut = instruction_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h 8 hterm in hcut __5041 > subaddressing_mode > __ > 'a1) > (subaddressing_mode preinstruction 5042 > __ > 'a1) > 'a1 **) 5043 let instruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 = 5044 let hcut = instruction_rect_Type4 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __ 4957 5045 4958 5046 (** val instruction_inv_rect_Type3 : … … 4960 5048 > __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode 4961 5049 > __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode 4962 > __ > 'a1) > (subaddressing_mode > subaddressing_mode > __ > 'a1)4963 > (subaddressing_mode preinstruction >__ > 'a1) > 'a1 **)4964 let instruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8=4965 let hcut = instruction_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h 8 hterm in hcut __5050 > subaddressing_mode > __ > 'a1) > (subaddressing_mode preinstruction 5051 > __ > 'a1) > 'a1 **) 5052 let instruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 = 5053 let hcut = instruction_rect_Type3 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __ 4966 5054 4967 5055 (** val instruction_inv_rect_Type2 : … … 4969 5057 > __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode 4970 5058 > __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode 4971 > __ > 'a1) > (subaddressing_mode > subaddressing_mode > __ > 'a1)4972 > (subaddressing_mode preinstruction >__ > 'a1) > 'a1 **)4973 let instruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8=4974 let hcut = instruction_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h 8 hterm in hcut __5059 > subaddressing_mode > __ > 'a1) > (subaddressing_mode preinstruction 5060 > __ > 'a1) > 'a1 **) 5061 let instruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 = 5062 let hcut = instruction_rect_Type2 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __ 4975 5063 4976 5064 (** val instruction_inv_rect_Type1 : … … 4978 5066 > __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode 4979 5067 > __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode 4980 > __ > 'a1) > (subaddressing_mode > subaddressing_mode > __ > 'a1)4981 > (subaddressing_mode preinstruction >__ > 'a1) > 'a1 **)4982 let instruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8=4983 let hcut = instruction_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h 8 hterm in hcut __5068 > subaddressing_mode > __ > 'a1) > (subaddressing_mode preinstruction 5069 > __ > 'a1) > 'a1 **) 5070 let instruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 = 5071 let hcut = instruction_rect_Type1 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __ 4984 5072 4985 5073 (** val instruction_inv_rect_Type0 : … … 4987 5075 > __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode 4988 5076 > __ > 'a1) > (subaddressing_mode > __ > 'a1) > (subaddressing_mode 4989 > __ > 'a1) > (subaddressing_mode > subaddressing_mode > __ > 'a1)4990 > (subaddressing_mode preinstruction >__ > 'a1) > 'a1 **)4991 let instruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8=4992 let hcut = instruction_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h 8 hterm in hcut __5077 > subaddressing_mode > __ > 'a1) > (subaddressing_mode preinstruction 5078 > __ > 'a1) > 'a1 **) 5079 let instruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 = 5080 let hcut = instruction_rect_Type0 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __ 4993 5081 4994 5082 (** val instruction_discr : instruction > instruction > __ **) … … 5001 5089  LJMP a0 > Obj.magic (fun _ dH > dH __) 5002 5090  SJMP a0 > Obj.magic (fun _ dH > dH __) 5003  JMP a0 > Obj.magic (fun _ dH > dH __)5004 5091  MOVC (a0, a1) > Obj.magic (fun _ dH > dH __ __) 5005 5092  RealInstruction a0 > Obj.magic (fun _ dH > dH __)) y … … 5014 5101  LJMP a0 > Obj.magic (fun _ dH > dH __) 5015 5102  SJMP a0 > Obj.magic (fun _ dH > dH __) 5016  JMP a0 > Obj.magic (fun _ dH > dH __)5017 5103  MOVC (a0, a1) > Obj.magic (fun _ dH > dH __ __) 5018 5104  RealInstruction a0 > Obj.magic (fun _ dH > dH __)) y … … 5033 5119  LJMP x > Bool.False 5034 5120  SJMP x > Bool.False 5035  JMP x > Bool.False5036 5121  MOVC (x, x0) > Bool.False 5037 5122  RealInstruction x > Bool.False) … … 5048 5133  LJMP x > Bool.False 5049 5134  SJMP x > Bool.False 5050  JMP x > Bool.False5051 5135  MOVC (x, x0) > Bool.False 5052 5136  RealInstruction x > Bool.False) … … 5063 5147  LJMP x > Bool.False 5064 5148  SJMP x > Bool.False 5065  JMP x > Bool.False5066 5149  MOVC (x, x0) > Bool.False 5067 5150  RealInstruction x > Bool.False) … … 5078 5161 Vector.VEmpty)) arg') 5079 5162  SJMP x > Bool.False 5080  JMP x > Bool.False5081 5163  MOVC (x, x0) > Bool.False 5082 5164  RealInstruction x > Bool.False) … … 5093 5175 (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Relative, 5094 5176 Vector.VEmpty)) arg') 5095  JMP x > Bool.False5096  MOVC (x, x0) > Bool.False5097  RealInstruction x > Bool.False)5098  JMP arg >5099 (match j with5100  ACALL x > Bool.False5101  LCALL x > Bool.False5102  AJMP x > Bool.False5103  LJMP x > Bool.False5104  SJMP x > Bool.False5105  JMP arg' >5106 eq_addressing_mode5107 (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Indirect_dptr,5108 Vector.VEmpty)) arg)5109 (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Indirect_dptr,5110 Vector.VEmpty)) arg')5111 5177  MOVC (x, x0) > Bool.False 5112 5178  RealInstruction x > Bool.False) … … 5118 5184  LJMP x > Bool.False 5119 5185  SJMP x > Bool.False 5120  JMP x > Bool.False5121 5186  MOVC (arg1', arg2') > 5122 5187 Bool.andb … … 5139 5204  LJMP x > Bool.False 5140 5205  SJMP x > Bool.False 5141  JMP x > Bool.False5142 5206  MOVC (x, x0) > Bool.False 5143 5207  RealInstruction instr' > eq_preinstruction instr instr') 5208 5209 type word_side = 5210  HIGH 5211  LOW 5212 5213 (** val word_side_rect_Type4 : 'a1 > 'a1 > word_side > 'a1 **) 5214 let rec word_side_rect_Type4 h_HIGH h_LOW = function 5215  HIGH > h_HIGH 5216  LOW > h_LOW 5217 5218 (** val word_side_rect_Type5 : 'a1 > 'a1 > word_side > 'a1 **) 5219 let rec word_side_rect_Type5 h_HIGH h_LOW = function 5220  HIGH > h_HIGH 5221  LOW > h_LOW 5222 5223 (** val word_side_rect_Type3 : 'a1 > 'a1 > word_side > 'a1 **) 5224 let rec word_side_rect_Type3 h_HIGH h_LOW = function 5225  HIGH > h_HIGH 5226  LOW > h_LOW 5227 5228 (** val word_side_rect_Type2 : 'a1 > 'a1 > word_side > 'a1 **) 5229 let rec word_side_rect_Type2 h_HIGH h_LOW = function 5230  HIGH > h_HIGH 5231  LOW > h_LOW 5232 5233 (** val word_side_rect_Type1 : 'a1 > 'a1 > word_side > 'a1 **) 5234 let rec word_side_rect_Type1 h_HIGH h_LOW = function 5235  HIGH > h_HIGH 5236  LOW > h_LOW 5237 5238 (** val word_side_rect_Type0 : 'a1 > 'a1 > word_side > 'a1 **) 5239 let rec word_side_rect_Type0 h_HIGH h_LOW = function 5240  HIGH > h_HIGH 5241  LOW > h_LOW 5242 5243 (** val word_side_inv_rect_Type4 : 5244 word_side > (__ > 'a1) > (__ > 'a1) > 'a1 **) 5245 let word_side_inv_rect_Type4 hterm h1 h2 = 5246 let hcut = word_side_rect_Type4 h1 h2 hterm in hcut __ 5247 5248 (** val word_side_inv_rect_Type3 : 5249 word_side > (__ > 'a1) > (__ > 'a1) > 'a1 **) 5250 let word_side_inv_rect_Type3 hterm h1 h2 = 5251 let hcut = word_side_rect_Type3 h1 h2 hterm in hcut __ 5252 5253 (** val word_side_inv_rect_Type2 : 5254 word_side > (__ > 'a1) > (__ > 'a1) > 'a1 **) 5255 let word_side_inv_rect_Type2 hterm h1 h2 = 5256 let hcut = word_side_rect_Type2 h1 h2 hterm in hcut __ 5257 5258 (** val word_side_inv_rect_Type1 : 5259 word_side > (__ > 'a1) > (__ > 'a1) > 'a1 **) 5260 let word_side_inv_rect_Type1 hterm h1 h2 = 5261 let hcut = word_side_rect_Type1 h1 h2 hterm in hcut __ 5262 5263 (** val word_side_inv_rect_Type0 : 5264 word_side > (__ > 'a1) > (__ > 'a1) > 'a1 **) 5265 let word_side_inv_rect_Type0 hterm h1 h2 = 5266 let hcut = word_side_rect_Type0 h1 h2 hterm in hcut __ 5267 5268 (** val word_side_discr : word_side > word_side > __ **) 5269 let word_side_discr x y = 5270 Logic.eq_rect_Type2 x 5271 (match x with 5272  HIGH > Obj.magic (fun _ dH > dH) 5273  LOW > Obj.magic (fun _ dH > dH)) y 5274 5275 (** val word_side_jmdiscr : word_side > word_side > __ **) 5276 let word_side_jmdiscr x y = 5277 Logic.eq_rect_Type2 x 5278 (match x with 5279  HIGH > Obj.magic (fun _ dH > dH) 5280  LOW > Obj.magic (fun _ dH > dH)) y 5144 5281 5145 5282 type pseudo_instruction = … … 5148 5285  Cost of CostLabel.costlabel 5149 5286  Jmp of identifier0 5287  Jnz of subaddressing_mode * identifier0 * identifier0 5288  MovSuccessor of subaddressing_mode * word_side * identifier0 5150 5289  Call of identifier0 5151 5290  Mov of subaddressing_mode * identifier0 … … 5153 5292 (** val pseudo_instruction_rect_Type4 : 5154 5293 (identifier0 preinstruction > 'a1) > (String.string > 'a1) > 5155 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (identifier0 > 5156 'a1) > (subaddressing_mode > identifier0 > 'a1) > pseudo_instruction 5157 > 'a1 **) 5158 let rec pseudo_instruction_rect_Type4 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function 5159  Instruction x_2057 > h_Instruction x_2057 5160  Comment x_2058 > h_Comment x_2058 5161  Cost x_2059 > h_Cost x_2059 5162  Jmp x_2060 > h_Jmp x_2060 5163  Call x_2061 > h_Call x_2061 5164  Mov (x_2063, x_2062) > h_Mov x_2063 x_2062 5294 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > 5295 (subaddressing_mode > identifier0 > identifier0 > 'a1) > 5296 (subaddressing_mode > word_side > identifier0 > 'a1) > (identifier0 5297 > 'a1) > (subaddressing_mode > identifier0 > 'a1) > 5298 pseudo_instruction > 'a1 **) 5299 let rec pseudo_instruction_rect_Type4 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function 5300  Instruction x_20761 > h_Instruction x_20761 5301  Comment x_20762 > h_Comment x_20762 5302  Cost x_20763 > h_Cost x_20763 5303  Jmp x_20764 > h_Jmp x_20764 5304  Jnz (x_20767, x_20766, x_20765) > h_Jnz x_20767 x_20766 x_20765 5305  MovSuccessor (x_20770, x_20769, x_20768) > 5306 h_MovSuccessor x_20770 x_20769 x_20768 5307  Call x_20771 > h_Call x_20771 5308  Mov (x_20773, x_20772) > h_Mov x_20773 x_20772 5165 5309 5166 5310 (** val pseudo_instruction_rect_Type5 : 5167 5311 (identifier0 preinstruction > 'a1) > (String.string > 'a1) > 5168 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (identifier0 > 5169 'a1) > (subaddressing_mode > identifier0 > 'a1) > pseudo_instruction 5170 > 'a1 **) 5171 let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function 5172  Instruction x_2071 > h_Instruction x_2071 5173  Comment x_2072 > h_Comment x_2072 5174  Cost x_2073 > h_Cost x_2073 5175  Jmp x_2074 > h_Jmp x_2074 5176  Call x_2075 > h_Call x_2075 5177  Mov (x_2077, x_2076) > h_Mov x_2077 x_2076 5312 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > 5313 (subaddressing_mode > identifier0 > identifier0 > 'a1) > 5314 (subaddressing_mode > word_side > identifier0 > 'a1) > (identifier0 5315 > 'a1) > (subaddressing_mode > identifier0 > 'a1) > 5316 pseudo_instruction > 'a1 **) 5317 let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function 5318  Instruction x_20783 > h_Instruction x_20783 5319  Comment x_20784 > h_Comment x_20784 5320  Cost x_20785 > h_Cost x_20785 5321  Jmp x_20786 > h_Jmp x_20786 5322  Jnz (x_20789, x_20788, x_20787) > h_Jnz x_20789 x_20788 x_20787 5323  MovSuccessor (x_20792, x_20791, x_20790) > 5324 h_MovSuccessor x_20792 x_20791 x_20790 5325  Call x_20793 > h_Call x_20793 5326  Mov (x_20795, x_20794) > h_Mov x_20795 x_20794 5178 5327 5179 5328 (** val pseudo_instruction_rect_Type3 : 5180 5329 (identifier0 preinstruction > 'a1) > (String.string > 'a1) > 5181 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (identifier0 > 5182 'a1) > (subaddressing_mode > identifier0 > 'a1) > pseudo_instruction 5183 > 'a1 **) 5184 let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function 5185  Instruction x_2085 > h_Instruction x_2085 5186  Comment x_2086 > h_Comment x_2086 5187  Cost x_2087 > h_Cost x_2087 5188  Jmp x_2088 > h_Jmp x_2088 5189  Call x_2089 > h_Call x_2089 5190  Mov (x_2091, x_2090) > h_Mov x_2091 x_2090 5330 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > 5331 (subaddressing_mode > identifier0 > identifier0 > 'a1) > 5332 (subaddressing_mode > word_side > identifier0 > 'a1) > (identifier0 5333 > 'a1) > (subaddressing_mode > identifier0 > 'a1) > 5334 pseudo_instruction > 'a1 **) 5335 let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function 5336  Instruction x_20805 > h_Instruction x_20805 5337  Comment x_20806 > h_Comment x_20806 5338  Cost x_20807 > h_Cost x_20807 5339  Jmp x_20808 > h_Jmp x_20808 5340  Jnz (x_20811, x_20810, x_20809) > h_Jnz x_20811 x_20810 x_20809 5341  MovSuccessor (x_20814, x_20813, x_20812) > 5342 h_MovSuccessor x_20814 x_20813 x_20812 5343  Call x_20815 > h_Call x_20815 5344  Mov (x_20817, x_20816) > h_Mov x_20817 x_20816 5191 5345 5192 5346 (** val pseudo_instruction_rect_Type2 : 5193 5347 (identifier0 preinstruction > 'a1) > (String.string > 'a1) > 5194 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (identifier0 > 5195 'a1) > (subaddressing_mode > identifier0 > 'a1) > pseudo_instruction 5196 > 'a1 **) 5197 let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function 5198  Instruction x_2099 > h_Instruction x_2099 5199  Comment x_2100 > h_Comment x_2100 5200  Cost x_2101 > h_Cost x_2101 5201  Jmp x_2102 > h_Jmp x_2102 5202  Call x_2103 > h_Call x_2103 5203  Mov (x_2105, x_2104) > h_Mov x_2105 x_2104 5348 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > 5349 (subaddressing_mode > identifier0 > identifier0 > 'a1) > 5350 (subaddressing_mode > word_side > identifier0 > 'a1) > (identifier0 5351 > 'a1) > (subaddressing_mode > identifier0 > 'a1) > 5352 pseudo_instruction > 'a1 **) 5353 let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function 5354  Instruction x_20827 > h_Instruction x_20827 5355  Comment x_20828 > h_Comment x_20828 5356  Cost x_20829 > h_Cost x_20829 5357  Jmp x_20830 > h_Jmp x_20830 5358  Jnz (x_20833, x_20832, x_20831) > h_Jnz x_20833 x_20832 x_20831 5359  MovSuccessor (x_20836, x_20835, x_20834) > 5360 h_MovSuccessor x_20836 x_20835 x_20834 5361  Call x_20837 > h_Call x_20837 5362  Mov (x_20839, x_20838) > h_Mov x_20839 x_20838 5204 5363 5205 5364 (** val pseudo_instruction_rect_Type1 : 5206 5365 (identifier0 preinstruction > 'a1) > (String.string > 'a1) > 5207 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (identifier0 > 5208 'a1) > (subaddressing_mode > identifier0 > 'a1) > pseudo_instruction 5209 > 'a1 **) 5210 let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function 5211  Instruction x_2113 > h_Instruction x_2113 5212  Comment x_2114 > h_Comment x_2114 5213  Cost x_2115 > h_Cost x_2115 5214  Jmp x_2116 > h_Jmp x_2116 5215  Call x_2117 > h_Call x_2117 5216  Mov (x_2119, x_2118) > h_Mov x_2119 x_2118 5366 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > 5367 (subaddressing_mode > identifier0 > identifier0 > 'a1) > 5368 (subaddressing_mode > word_side > identifier0 > 'a1) > (identifier0 5369 > 'a1) > (subaddressing_mode > identifier0 > 'a1) > 5370 pseudo_instruction > 'a1 **) 5371 let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function 5372  Instruction x_20849 > h_Instruction x_20849 5373  Comment x_20850 > h_Comment x_20850 5374  Cost x_20851 > h_Cost x_20851 5375  Jmp x_20852 > h_Jmp x_20852 5376  Jnz (x_20855, x_20854, x_20853) > h_Jnz x_20855 x_20854 x_20853 5377  MovSuccessor (x_20858, x_20857, x_20856) > 5378 h_MovSuccessor x_20858 x_20857 x_20856 5379  Call x_20859 > h_Call x_20859 5380  Mov (x_20861, x_20860) > h_Mov x_20861 x_20860 5217 5381 5218 5382 (** val pseudo_instruction_rect_Type0 : 5219 5383 (identifier0 preinstruction > 'a1) > (String.string > 'a1) > 5220 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > (identifier0 > 5221 'a1) > (subaddressing_mode > identifier0 > 'a1) > pseudo_instruction 5222 > 'a1 **) 5223 let rec pseudo_instruction_rect_Type0 h_Instruction h_Comment h_Cost h_Jmp h_Call h_Mov = function 5224  Instruction x_2127 > h_Instruction x_2127 5225  Comment x_2128 > h_Comment x_2128 5226  Cost x_2129 > h_Cost x_2129 5227  Jmp x_2130 > h_Jmp x_2130 5228  Call x_2131 > h_Call x_2131 5229  Mov (x_2133, x_2132) > h_Mov x_2133 x_2132 5384 (CostLabel.costlabel > 'a1) > (identifier0 > 'a1) > 5385 (subaddressing_mode > identifier0 > identifier0 > 'a1) > 5386 (subaddressing_mode > word_side > identifier0 > 'a1) > (identifier0 5387 > 'a1) > (subaddressing_mode > identifier0 > 'a1) > 5388 pseudo_instruction > 'a1 **) 5389 let rec pseudo_instruction_rect_Type0 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function 5390  Instruction x_20871 > h_Instruction x_20871 5391  Comment x_20872 > h_Comment x_20872 5392  Cost x_20873 > h_Cost x_20873 5393  Jmp x_20874 > h_Jmp x_20874 5394  Jnz (x_20877, x_20876, x_20875) > h_Jnz x_20877 x_20876 x_20875 5395  MovSuccessor (x_20880, x_20879, x_20878) > 5396 h_MovSuccessor x_20880 x_20879 x_20878 5397  Call x_20881 > h_Call x_20881 5398  Mov (x_20883, x_20882) > h_Mov x_20883 x_20882 5230 5399 5231 5400 (** val pseudo_instruction_inv_rect_Type4 : 5232 5401 pseudo_instruction > (identifier0 preinstruction > __ > 'a1) > 5233 5402 (String.string > __ > 'a1) > (CostLabel.costlabel > __ > 'a1) > 5234 (identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 5403 (identifier0 > __ > 'a1) > (subaddressing_mode > identifier0 > 5404 identifier0 > __ > 'a1) > (subaddressing_mode > word_side > 5405 identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 5235 5406 (subaddressing_mode > identifier0 > __ > 'a1) > 'a1 **) 5236 let pseudo_instruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 = 5237 let hcut = pseudo_instruction_rect_Type4 h1 h2 h3 h4 h5 h6 hterm in hcut __ 5407 let pseudo_instruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 = 5408 let hcut = pseudo_instruction_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 hterm in 5409 hcut __ 5238 5410 5239 5411 (** val pseudo_instruction_inv_rect_Type3 : 5240 5412 pseudo_instruction > (identifier0 preinstruction > __ > 'a1) > 5241 5413 (String.string > __ > 'a1) > (CostLabel.costlabel > __ > 'a1) > 5242 (identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 5414 (identifier0 > __ > 'a1) > (subaddressing_mode > identifier0 > 5415 identifier0 > __ > 'a1) > (subaddressing_mode > word_side > 5416 identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 5243 5417 (subaddressing_mode > identifier0 > __ > 'a1) > 'a1 **) 5244 let pseudo_instruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 = 5245 let hcut = pseudo_instruction_rect_Type3 h1 h2 h3 h4 h5 h6 hterm in hcut __ 5418 let pseudo_instruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 = 5419 let hcut = pseudo_instruction_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 hterm in 5420 hcut __ 5246 5421 5247 5422 (** val pseudo_instruction_inv_rect_Type2 : 5248 5423 pseudo_instruction > (identifier0 preinstruction > __ > 'a1) > 5249 5424 (String.string > __ > 'a1) > (CostLabel.costlabel > __ > 'a1) > 5250 (identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 5425 (identifier0 > __ > 'a1) > (subaddressing_mode > identifier0 > 5426 identifier0 > __ > 'a1) > (subaddressing_mode > word_side > 5427 identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 5251 5428 (subaddressing_mode > identifier0 > __ > 'a1) > 'a1 **) 5252 let pseudo_instruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 = 5253 let hcut = pseudo_instruction_rect_Type2 h1 h2 h3 h4 h5 h6 hterm in hcut __ 5429 let pseudo_instruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 = 5430 let hcut = pseudo_instruction_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 hterm in 5431 hcut __ 5254 5432 5255 5433 (** val pseudo_instruction_inv_rect_Type1 : 5256 5434 pseudo_instruction > (identifier0 preinstruction > __ > 'a1) > 5257 5435 (String.string > __ > 'a1) > (CostLabel.costlabel > __ > 'a1) > 5258 (identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 5436 (identifier0 > __ > 'a1) > (subaddressing_mode > identifier0 > 5437 identifier0 > __ > 'a1) > (subaddressing_mode > word_side > 5438 identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 5259 5439 (subaddressing_mode > identifier0 > __ > 'a1) > 'a1 **) 5260 let pseudo_instruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 = 5261 let hcut = pseudo_instruction_rect_Type1 h1 h2 h3 h4 h5 h6 hterm in hcut __ 5440 let pseudo_instruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 = 5441 let hcut = pseudo_instruction_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 hterm in 5442 hcut __ 5262 5443 5263 5444 (** val pseudo_instruction_inv_rect_Type0 : 5264 5445 pseudo_instruction > (identifier0 preinstruction > __ > 'a1) > 5265 5446 (String.string > __ > 'a1) > (CostLabel.costlabel > __ > 'a1) > 5266 (identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 5447 (identifier0 > __ > 'a1) > (subaddressing_mode > identifier0 > 5448 identifier0 > __ > 'a1) > (subaddressing_mode > word_side > 5449 identifier0 > __ > 'a1) > (identifier0 > __ > 'a1) > 5267 5450 (subaddressing_mode > identifier0 > __ > 'a1) > 'a1 **) 5268 let pseudo_instruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 = 5269 let hcut = pseudo_instruction_rect_Type0 h1 h2 h3 h4 h5 h6 hterm in hcut __ 5451 let pseudo_instruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 = 5452 let hcut = pseudo_instruction_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 hterm in 5453 hcut __ 5270 5454 5271 5455 (** val pseudo_instruction_discr : … … 5278 5462  Cost a0 > Obj.magic (fun _ dH > dH __) 5279 5463  Jmp a0 > Obj.magic (fun _ dH > dH __) 5464  Jnz (a0, a1, a2) > Obj.magic (fun _ dH > dH __ __ __) 5465  MovSuccessor (a0, a1, a2) > Obj.magic (fun _ dH > dH __ __ __) 5280 5466  Call a0 > Obj.magic (fun _ dH > dH __) 5281 5467  Mov (a0, a1) > Obj.magic (fun _ dH > dH __ __)) y … … 5290 5476  Cost a0 > Obj.magic (fun _ dH > dH __) 5291 5477  Jmp a0 > Obj.magic (fun _ dH > dH __) 5478  Jnz (a0, a1, a2) > Obj.magic (fun _ dH > dH __ __ __) 5479  MovSuccessor (a0, a1, a2) > Obj.magic (fun _ dH > dH __ __ __) 5292 5480  Call a0 > Obj.magic (fun _ dH > dH __) 5293 5481  Mov (a0, a1) > Obj.magic (fun _ dH > dH __ __)) y … … 5295 5483 type labelled_instruction = pseudo_instruction LabelledObjects.labelled_obj 5296 5484 5297 type preamble = 5298 (Nat.nat Identifiers.identifier_map, (identifier0, BitVector.word) 5299 Types.prod List.list) Types.prod 5485 type preamble = (identifier0, BitVector.word) Types.prod List.list 5300 5486 5301 5487 type assembly_program = instruction List.list … … 5343 5529  RETI > Bool.False 5344 5530  NOP > Bool.False 5531  JMP x0 > Bool.False 5345 5532 5346 5533 (** val is_relative_jump : pseudo_instruction > Bool.bool **) … … 5350 5537  Cost x > Bool.False 5351 5538  Jmp x > Bool.False 5539  Jnz (x, x0, x1) > Bool.False 5540  MovSuccessor (x, x0, x1) > Bool.False 5352 5541  Call x > Bool.False 5353 5542  Mov (x, x0) > Bool.False … … 5359 5548  Cost x > Bool.False 5360 5549  Jmp x > Bool.True 5550  Jnz (x, x0, x1) > Bool.False 5551  MovSuccessor (x, x0, x1) > Bool.False 5361 5552  Call x > Bool.True 5362 5553  Mov (x, x0) > Bool.False … … 5368 5559  Cost x > Bool.False 5369 5560  Jmp x > Bool.False 5561  Jnz (x, x0, x1) > Bool.False 5562  MovSuccessor (x, x0, x1) > Bool.False 5370 5563  Call x > Bool.True 5371 5564  Mov (x, x0) > Bool.False
Note: See TracChangeset
for help on using the changeset viewer.