From d549e01e37d9b10e96f60e64a1814f5a9208e283 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 30 Apr 2013 18:58:09 +0200 Subject: [PATCH] Imported Upstream version 0.2 --- .build.swp | Bin 0 -> 12288 bytes extracted/aSM.ml | 813 ++++++++++++++++++----------------- extracted/aSMCosts.ml | 4 +- extracted/abstractStatus.ml | 13 +- extracted/abstractStatus.mli | 9 +- extracted/compiler.ml | 5 + extracted/compiler.mli | 4 +- extracted/fetch.ml | 76 ++-- extracted/fetch.mli | 44 +- extracted/globalenvs.ml | 8 +- extracted/interpret2.ml | 18 + extracted/interpret2.mli | 4 + extracted/joint_printer.ml | 104 ++--- extracted/lINToASM.ml | 56 +-- extracted/policy.ml | 8 +- extracted/policy.mli | 54 +-- extracted/policyFront.ml | 144 ++++--- extracted/policyFront.mli | 80 ++-- extracted/policyStep.ml | 127 +++--- extracted/policyStep.mli | 54 +-- extracted/semantics.ml | 32 +- extracted/semantics.mli | 4 +- extracted/simplifyCasts.ml | 36 +- extracted/status.ml | 84 ++-- extracted/switchRemoval.ml | 80 ++-- extracted/toCminor.ml | 4 +- extracted/toRTLabs.ml | 12 +- 27 files changed, 951 insertions(+), 926 deletions(-) create mode 100644 .build.swp diff --git a/.build.swp b/.build.swp new file mode 100644 index 0000000000000000000000000000000000000000..2f910a1f6b3f066caec641e3873d62f0ad4be6c9 GIT binary patch literal 12288 zcmeI2y>1gh5XU!E6bT?`C?`-Pp!m*qgq${sh2kPo00jz!(B0m|-sJ9fwY!Jn2A+XO zpo5Z*l81mtffi=hb}$rJNoQ$R`fEM2^L0O0r`x>!d~gW8WLwa>CB&Df2T#6!zAjep z3UR9HGadX3mT3%nzc})3ESSE~_RN_~V!Dr3>a?)x4catsR9P(O#K%m430#Rl<4;;U zYscH&PCMk^zqbx|ZXaK%6elqOCcp%k025#WOn?b60Vc4V1iV=h?`ZUE)A4Ui_mzM4 zsmU7?U;<2l2`~XBzyz286JP>NfC(@GCa{DAGWz8HZB>ZPH5#72|Ign4f8G@02k8^( zBk4VNfC(@GCcp%k025eZ0$OHODWN4B z=XC|GA+!dNBxxVZaCG(cJTxU; et}h@TgVR-<#?S=L+eZ4vVtDHHG*@-%M&dU;))t@u literal 0 HcmV?d00001 diff --git a/extracted/aSM.ml b/extracted/aSM.ml index e7665c5..79ec03a 100644 --- a/extracted/aSM.ml +++ b/extracted/aSM.ml @@ -112,25 +112,25 @@ type addressing_mode = (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) -> addressing_mode -> 'a1 **) 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 -| DIRECT x_19160 -> h_DIRECT x_19160 -| INDIRECT x_19161 -> h_INDIRECT x_19161 -| EXT_INDIRECT x_19162 -> h_EXT_INDIRECT x_19162 -| REGISTER x_19163 -> h_REGISTER x_19163 +| DIRECT x_33 -> h_DIRECT x_33 +| INDIRECT x_34 -> h_INDIRECT x_34 +| EXT_INDIRECT x_35 -> h_EXT_INDIRECT x_35 +| REGISTER x_36 -> h_REGISTER x_36 | ACC_A -> h_ACC_A | ACC_B -> h_ACC_B | DPTR -> h_DPTR -| DATA x_19164 -> h_DATA x_19164 -| DATA16 x_19165 -> h_DATA16 x_19165 +| DATA x_37 -> h_DATA x_37 +| DATA16 x_38 -> h_DATA16 x_38 | ACC_DPTR -> h_ACC_DPTR | ACC_PC -> h_ACC_PC | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR | INDIRECT_DPTR -> h_INDIRECT_DPTR | CARRY -> h_CARRY -| BIT_ADDR x_19166 -> h_BIT_ADDR x_19166 -| N_BIT_ADDR x_19167 -> h_N_BIT_ADDR x_19167 -| RELATIVE x_19168 -> h_RELATIVE x_19168 -| ADDR11 x_19169 -> h_ADDR11 x_19169 -| ADDR16 x_19170 -> h_ADDR16 x_19170 +| BIT_ADDR x_39 -> h_BIT_ADDR x_39 +| N_BIT_ADDR x_40 -> h_N_BIT_ADDR x_40 +| RELATIVE x_41 -> h_RELATIVE x_41 +| ADDR11 x_42 -> h_ADDR11 x_42 +| ADDR16 x_43 -> h_ADDR16 x_43 (** val addressing_mode_rect_Type5 : (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> @@ -140,25 +140,25 @@ let rec addressing_mode_rect_Type4 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) -> addressing_mode -> 'a1 **) 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 -| DIRECT x_19191 -> h_DIRECT x_19191 -| INDIRECT x_19192 -> h_INDIRECT x_19192 -| EXT_INDIRECT x_19193 -> h_EXT_INDIRECT x_19193 -| REGISTER x_19194 -> h_REGISTER x_19194 +| DIRECT x_64 -> h_DIRECT x_64 +| INDIRECT x_65 -> h_INDIRECT x_65 +| EXT_INDIRECT x_66 -> h_EXT_INDIRECT x_66 +| REGISTER x_67 -> h_REGISTER x_67 | ACC_A -> h_ACC_A | ACC_B -> h_ACC_B | DPTR -> h_DPTR -| DATA x_19195 -> h_DATA x_19195 -| DATA16 x_19196 -> h_DATA16 x_19196 +| DATA x_68 -> h_DATA x_68 +| DATA16 x_69 -> h_DATA16 x_69 | ACC_DPTR -> h_ACC_DPTR | ACC_PC -> h_ACC_PC | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR | INDIRECT_DPTR -> h_INDIRECT_DPTR | CARRY -> h_CARRY -| BIT_ADDR x_19197 -> h_BIT_ADDR x_19197 -| N_BIT_ADDR x_19198 -> h_N_BIT_ADDR x_19198 -| RELATIVE x_19199 -> h_RELATIVE x_19199 -| ADDR11 x_19200 -> h_ADDR11 x_19200 -| ADDR16 x_19201 -> h_ADDR16 x_19201 +| BIT_ADDR x_70 -> h_BIT_ADDR x_70 +| N_BIT_ADDR x_71 -> h_N_BIT_ADDR x_71 +| RELATIVE x_72 -> h_RELATIVE x_72 +| ADDR11 x_73 -> h_ADDR11 x_73 +| ADDR16 x_74 -> h_ADDR16 x_74 (** val addressing_mode_rect_Type3 : (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> @@ -168,25 +168,25 @@ let rec addressing_mode_rect_Type5 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) -> addressing_mode -> 'a1 **) 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 -| DIRECT x_19222 -> h_DIRECT x_19222 -| INDIRECT x_19223 -> h_INDIRECT x_19223 -| EXT_INDIRECT x_19224 -> h_EXT_INDIRECT x_19224 -| REGISTER x_19225 -> h_REGISTER x_19225 +| DIRECT x_95 -> h_DIRECT x_95 +| INDIRECT x_96 -> h_INDIRECT x_96 +| EXT_INDIRECT x_97 -> h_EXT_INDIRECT x_97 +| REGISTER x_98 -> h_REGISTER x_98 | ACC_A -> h_ACC_A | ACC_B -> h_ACC_B | DPTR -> h_DPTR -| DATA x_19226 -> h_DATA x_19226 -| DATA16 x_19227 -> h_DATA16 x_19227 +| DATA x_99 -> h_DATA x_99 +| DATA16 x_100 -> h_DATA16 x_100 | ACC_DPTR -> h_ACC_DPTR | ACC_PC -> h_ACC_PC | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR | INDIRECT_DPTR -> h_INDIRECT_DPTR | CARRY -> h_CARRY -| BIT_ADDR x_19228 -> h_BIT_ADDR x_19228 -| N_BIT_ADDR x_19229 -> h_N_BIT_ADDR x_19229 -| RELATIVE x_19230 -> h_RELATIVE x_19230 -| ADDR11 x_19231 -> h_ADDR11 x_19231 -| ADDR16 x_19232 -> h_ADDR16 x_19232 +| BIT_ADDR x_101 -> h_BIT_ADDR x_101 +| N_BIT_ADDR x_102 -> h_N_BIT_ADDR x_102 +| RELATIVE x_103 -> h_RELATIVE x_103 +| ADDR11 x_104 -> h_ADDR11 x_104 +| ADDR16 x_105 -> h_ADDR16 x_105 (** val addressing_mode_rect_Type2 : (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> @@ -196,25 +196,25 @@ let rec addressing_mode_rect_Type3 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) -> addressing_mode -> 'a1 **) 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 -| DIRECT x_19253 -> h_DIRECT x_19253 -| INDIRECT x_19254 -> h_INDIRECT x_19254 -| EXT_INDIRECT x_19255 -> h_EXT_INDIRECT x_19255 -| REGISTER x_19256 -> h_REGISTER x_19256 +| DIRECT x_126 -> h_DIRECT x_126 +| INDIRECT x_127 -> h_INDIRECT x_127 +| EXT_INDIRECT x_128 -> h_EXT_INDIRECT x_128 +| REGISTER x_129 -> h_REGISTER x_129 | ACC_A -> h_ACC_A | ACC_B -> h_ACC_B | DPTR -> h_DPTR -| DATA x_19257 -> h_DATA x_19257 -| DATA16 x_19258 -> h_DATA16 x_19258 +| DATA x_130 -> h_DATA x_130 +| DATA16 x_131 -> h_DATA16 x_131 | ACC_DPTR -> h_ACC_DPTR | ACC_PC -> h_ACC_PC | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR | INDIRECT_DPTR -> h_INDIRECT_DPTR | CARRY -> h_CARRY -| BIT_ADDR x_19259 -> h_BIT_ADDR x_19259 -| N_BIT_ADDR x_19260 -> h_N_BIT_ADDR x_19260 -| RELATIVE x_19261 -> h_RELATIVE x_19261 -| ADDR11 x_19262 -> h_ADDR11 x_19262 -| ADDR16 x_19263 -> h_ADDR16 x_19263 +| BIT_ADDR x_132 -> h_BIT_ADDR x_132 +| N_BIT_ADDR x_133 -> h_N_BIT_ADDR x_133 +| RELATIVE x_134 -> h_RELATIVE x_134 +| ADDR11 x_135 -> h_ADDR11 x_135 +| ADDR16 x_136 -> h_ADDR16 x_136 (** val addressing_mode_rect_Type1 : (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> @@ -224,25 +224,25 @@ let rec addressing_mode_rect_Type2 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) -> addressing_mode -> 'a1 **) 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 -| DIRECT x_19284 -> h_DIRECT x_19284 -| INDIRECT x_19285 -> h_INDIRECT x_19285 -| EXT_INDIRECT x_19286 -> h_EXT_INDIRECT x_19286 -| REGISTER x_19287 -> h_REGISTER x_19287 +| DIRECT x_157 -> h_DIRECT x_157 +| INDIRECT x_158 -> h_INDIRECT x_158 +| EXT_INDIRECT x_159 -> h_EXT_INDIRECT x_159 +| REGISTER x_160 -> h_REGISTER x_160 | ACC_A -> h_ACC_A | ACC_B -> h_ACC_B | DPTR -> h_DPTR -| DATA x_19288 -> h_DATA x_19288 -| DATA16 x_19289 -> h_DATA16 x_19289 +| DATA x_161 -> h_DATA x_161 +| DATA16 x_162 -> h_DATA16 x_162 | ACC_DPTR -> h_ACC_DPTR | ACC_PC -> h_ACC_PC | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR | INDIRECT_DPTR -> h_INDIRECT_DPTR | CARRY -> h_CARRY -| BIT_ADDR x_19290 -> h_BIT_ADDR x_19290 -| N_BIT_ADDR x_19291 -> h_N_BIT_ADDR x_19291 -| RELATIVE x_19292 -> h_RELATIVE x_19292 -| ADDR11 x_19293 -> h_ADDR11 x_19293 -| ADDR16 x_19294 -> h_ADDR16 x_19294 +| BIT_ADDR x_163 -> h_BIT_ADDR x_163 +| N_BIT_ADDR x_164 -> h_N_BIT_ADDR x_164 +| RELATIVE x_165 -> h_RELATIVE x_165 +| ADDR11 x_166 -> h_ADDR11 x_166 +| ADDR16 x_167 -> h_ADDR16 x_167 (** val addressing_mode_rect_Type0 : (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> @@ -252,25 +252,25 @@ let rec addressing_mode_rect_Type1 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) -> addressing_mode -> 'a1 **) 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 -| DIRECT x_19315 -> h_DIRECT x_19315 -| INDIRECT x_19316 -> h_INDIRECT x_19316 -| EXT_INDIRECT x_19317 -> h_EXT_INDIRECT x_19317 -| REGISTER x_19318 -> h_REGISTER x_19318 +| DIRECT x_188 -> h_DIRECT x_188 +| INDIRECT x_189 -> h_INDIRECT x_189 +| EXT_INDIRECT x_190 -> h_EXT_INDIRECT x_190 +| REGISTER x_191 -> h_REGISTER x_191 | ACC_A -> h_ACC_A | ACC_B -> h_ACC_B | DPTR -> h_DPTR -| DATA x_19319 -> h_DATA x_19319 -| DATA16 x_19320 -> h_DATA16 x_19320 +| DATA x_192 -> h_DATA x_192 +| DATA16 x_193 -> h_DATA16 x_193 | ACC_DPTR -> h_ACC_DPTR | ACC_PC -> h_ACC_PC | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR | INDIRECT_DPTR -> h_INDIRECT_DPTR | CARRY -> h_CARRY -| BIT_ADDR x_19321 -> h_BIT_ADDR x_19321 -| N_BIT_ADDR x_19322 -> h_N_BIT_ADDR x_19322 -| RELATIVE x_19323 -> h_RELATIVE x_19323 -| ADDR11 x_19324 -> h_ADDR11 x_19324 -| ADDR16 x_19325 -> h_ADDR16 x_19325 +| BIT_ADDR x_194 -> h_BIT_ADDR x_194 +| N_BIT_ADDR x_195 -> h_N_BIT_ADDR x_195 +| RELATIVE x_196 -> h_RELATIVE x_196 +| ADDR11 x_197 -> h_ADDR11 x_197 +| ADDR16 x_198 -> h_ADDR16 x_198 (** val addressing_mode_inv_rect_Type4 : addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ @@ -1925,43 +1925,43 @@ type subaddressing_mode = (** val subaddressing_mode_rect_Type4 : Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> 'a1) -> subaddressing_mode -> 'a1 **) -let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_19793 = - let subaddressing_modeel = x_19793 in +let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_666 = + let subaddressing_modeel = x_666 in h_mk_subaddressing_mode subaddressing_modeel __ (** val subaddressing_mode_rect_Type5 : Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> 'a1) -> subaddressing_mode -> 'a1 **) -let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_19795 = - let subaddressing_modeel = x_19795 in +let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_668 = + let subaddressing_modeel = x_668 in h_mk_subaddressing_mode subaddressing_modeel __ (** val subaddressing_mode_rect_Type3 : Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> 'a1) -> subaddressing_mode -> 'a1 **) -let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_19797 = - let subaddressing_modeel = x_19797 in +let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_670 = + let subaddressing_modeel = x_670 in h_mk_subaddressing_mode subaddressing_modeel __ (** val subaddressing_mode_rect_Type2 : Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> 'a1) -> subaddressing_mode -> 'a1 **) -let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_19799 = - let subaddressing_modeel = x_19799 in +let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_672 = + let subaddressing_modeel = x_672 in h_mk_subaddressing_mode subaddressing_modeel __ (** val subaddressing_mode_rect_Type1 : Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> 'a1) -> subaddressing_mode -> 'a1 **) -let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_19801 = - let subaddressing_modeel = x_19801 in +let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_674 = + let subaddressing_modeel = x_674 in h_mk_subaddressing_mode subaddressing_modeel __ (** val subaddressing_mode_rect_Type0 : Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> 'a1) -> subaddressing_mode -> 'a1 **) -let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_19803 = - let subaddressing_modeel = x_19803 in +let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_676 = + let subaddressing_modeel = x_676 in h_mk_subaddressing_mode subaddressing_modeel __ (** val subaddressing_modeel : @@ -2287,44 +2287,44 @@ type 'a preinstruction = -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) 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 -| ADD (x_19905, x_19904) -> h_ADD x_19905 x_19904 -| ADDC (x_19907, x_19906) -> h_ADDC x_19907 x_19906 -| SUBB (x_19909, x_19908) -> h_SUBB x_19909 x_19908 -| INC x_19910 -> h_INC x_19910 -| DEC x_19911 -> h_DEC x_19911 -| MUL (x_19913, x_19912) -> h_MUL x_19913 x_19912 -| DIV (x_19915, x_19914) -> h_DIV x_19915 x_19914 -| DA x_19916 -> h_DA x_19916 -| JC x_19917 -> h_JC x_19917 -| JNC x_19918 -> h_JNC x_19918 -| JB (x_19920, x_19919) -> h_JB x_19920 x_19919 -| JNB (x_19922, x_19921) -> h_JNB x_19922 x_19921 -| JBC (x_19924, x_19923) -> h_JBC x_19924 x_19923 -| JZ x_19925 -> h_JZ x_19925 -| JNZ x_19926 -> h_JNZ x_19926 -| CJNE (x_19928, x_19927) -> h_CJNE x_19928 x_19927 -| DJNZ (x_19930, x_19929) -> h_DJNZ x_19930 x_19929 -| ANL x_19931 -> h_ANL x_19931 -| ORL x_19932 -> h_ORL x_19932 -| XRL x_19933 -> h_XRL x_19933 -| CLR x_19934 -> h_CLR x_19934 -| CPL x_19935 -> h_CPL x_19935 -| RL x_19936 -> h_RL x_19936 -| RLC x_19937 -> h_RLC x_19937 -| RR x_19938 -> h_RR x_19938 -| RRC x_19939 -> h_RRC x_19939 -| SWAP x_19940 -> h_SWAP x_19940 -| MOV x_19941 -> h_MOV x_19941 -| MOVX x_19942 -> h_MOVX x_19942 -| SETB x_19943 -> h_SETB x_19943 -| PUSH x_19944 -> h_PUSH x_19944 -| POP x_19945 -> h_POP x_19945 -| XCH (x_19947, x_19946) -> h_XCH x_19947 x_19946 -| XCHD (x_19949, x_19948) -> h_XCHD x_19949 x_19948 +| ADD (x_778, x_777) -> h_ADD x_778 x_777 +| ADDC (x_780, x_779) -> h_ADDC x_780 x_779 +| SUBB (x_782, x_781) -> h_SUBB x_782 x_781 +| INC x_783 -> h_INC x_783 +| DEC x_784 -> h_DEC x_784 +| MUL (x_786, x_785) -> h_MUL x_786 x_785 +| DIV (x_788, x_787) -> h_DIV x_788 x_787 +| DA x_789 -> h_DA x_789 +| JC x_790 -> h_JC x_790 +| JNC x_791 -> h_JNC x_791 +| JB (x_793, x_792) -> h_JB x_793 x_792 +| JNB (x_795, x_794) -> h_JNB x_795 x_794 +| JBC (x_797, x_796) -> h_JBC x_797 x_796 +| JZ x_798 -> h_JZ x_798 +| JNZ x_799 -> h_JNZ x_799 +| CJNE (x_801, x_800) -> h_CJNE x_801 x_800 +| DJNZ (x_803, x_802) -> h_DJNZ x_803 x_802 +| ANL x_804 -> h_ANL x_804 +| ORL x_805 -> h_ORL x_805 +| XRL x_806 -> h_XRL x_806 +| CLR x_807 -> h_CLR x_807 +| CPL x_808 -> h_CPL x_808 +| RL x_809 -> h_RL x_809 +| RLC x_810 -> h_RLC x_810 +| RR x_811 -> h_RR x_811 +| RRC x_812 -> h_RRC x_812 +| SWAP x_813 -> h_SWAP x_813 +| MOV x_814 -> h_MOV x_814 +| MOVX x_815 -> h_MOVX x_815 +| SETB x_816 -> h_SETB x_816 +| PUSH x_817 -> h_PUSH x_817 +| POP x_818 -> h_POP x_818 +| XCH (x_820, x_819) -> h_XCH x_820 x_819 +| XCHD (x_822, x_821) -> h_XCHD x_822 x_821 | RET -> h_RET | RETI -> h_RETI | NOP -> h_NOP -| JMP x_19950 -> h_JMP x_19950 +| JMP x_823 -> h_JMP x_823 (** val preinstruction_rect_Type5 : (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode @@ -2362,44 +2362,44 @@ let rec preinstruction_rect_Type4 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_ -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) 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 -| ADD (x_19991, x_19990) -> h_ADD x_19991 x_19990 -| ADDC (x_19993, x_19992) -> h_ADDC x_19993 x_19992 -| SUBB (x_19995, x_19994) -> h_SUBB x_19995 x_19994 -| INC x_19996 -> h_INC x_19996 -| DEC x_19997 -> h_DEC x_19997 -| MUL (x_19999, x_19998) -> h_MUL x_19999 x_19998 -| DIV (x_20001, x_20000) -> h_DIV x_20001 x_20000 -| DA x_20002 -> h_DA x_20002 -| JC x_20003 -> h_JC x_20003 -| JNC x_20004 -> h_JNC x_20004 -| JB (x_20006, x_20005) -> h_JB x_20006 x_20005 -| JNB (x_20008, x_20007) -> h_JNB x_20008 x_20007 -| JBC (x_20010, x_20009) -> h_JBC x_20010 x_20009 -| JZ x_20011 -> h_JZ x_20011 -| JNZ x_20012 -> h_JNZ x_20012 -| CJNE (x_20014, x_20013) -> h_CJNE x_20014 x_20013 -| DJNZ (x_20016, x_20015) -> h_DJNZ x_20016 x_20015 -| ANL x_20017 -> h_ANL x_20017 -| ORL x_20018 -> h_ORL x_20018 -| XRL x_20019 -> h_XRL x_20019 -| CLR x_20020 -> h_CLR x_20020 -| CPL x_20021 -> h_CPL x_20021 -| RL x_20022 -> h_RL x_20022 -| RLC x_20023 -> h_RLC x_20023 -| RR x_20024 -> h_RR x_20024 -| RRC x_20025 -> h_RRC x_20025 -| SWAP x_20026 -> h_SWAP x_20026 -| MOV x_20027 -> h_MOV x_20027 -| MOVX x_20028 -> h_MOVX x_20028 -| SETB x_20029 -> h_SETB x_20029 -| PUSH x_20030 -> h_PUSH x_20030 -| POP x_20031 -> h_POP x_20031 -| XCH (x_20033, x_20032) -> h_XCH x_20033 x_20032 -| XCHD (x_20035, x_20034) -> h_XCHD x_20035 x_20034 +| ADD (x_864, x_863) -> h_ADD x_864 x_863 +| ADDC (x_866, x_865) -> h_ADDC x_866 x_865 +| SUBB (x_868, x_867) -> h_SUBB x_868 x_867 +| INC x_869 -> h_INC x_869 +| DEC x_870 -> h_DEC x_870 +| MUL (x_872, x_871) -> h_MUL x_872 x_871 +| DIV (x_874, x_873) -> h_DIV x_874 x_873 +| DA x_875 -> h_DA x_875 +| JC x_876 -> h_JC x_876 +| JNC x_877 -> h_JNC x_877 +| JB (x_879, x_878) -> h_JB x_879 x_878 +| JNB (x_881, x_880) -> h_JNB x_881 x_880 +| JBC (x_883, x_882) -> h_JBC x_883 x_882 +| JZ x_884 -> h_JZ x_884 +| JNZ x_885 -> h_JNZ x_885 +| CJNE (x_887, x_886) -> h_CJNE x_887 x_886 +| DJNZ (x_889, x_888) -> h_DJNZ x_889 x_888 +| ANL x_890 -> h_ANL x_890 +| ORL x_891 -> h_ORL x_891 +| XRL x_892 -> h_XRL x_892 +| CLR x_893 -> h_CLR x_893 +| CPL x_894 -> h_CPL x_894 +| RL x_895 -> h_RL x_895 +| RLC x_896 -> h_RLC x_896 +| RR x_897 -> h_RR x_897 +| RRC x_898 -> h_RRC x_898 +| SWAP x_899 -> h_SWAP x_899 +| MOV x_900 -> h_MOV x_900 +| MOVX x_901 -> h_MOVX x_901 +| SETB x_902 -> h_SETB x_902 +| PUSH x_903 -> h_PUSH x_903 +| POP x_904 -> h_POP x_904 +| XCH (x_906, x_905) -> h_XCH x_906 x_905 +| XCHD (x_908, x_907) -> h_XCHD x_908 x_907 | RET -> h_RET | RETI -> h_RETI | NOP -> h_NOP -| JMP x_20036 -> h_JMP x_20036 +| JMP x_909 -> h_JMP x_909 (** val preinstruction_rect_Type3 : (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode @@ -2437,44 +2437,44 @@ let rec preinstruction_rect_Type5 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_ -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) 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 -| ADD (x_20077, x_20076) -> h_ADD x_20077 x_20076 -| ADDC (x_20079, x_20078) -> h_ADDC x_20079 x_20078 -| SUBB (x_20081, x_20080) -> h_SUBB x_20081 x_20080 -| INC x_20082 -> h_INC x_20082 -| DEC x_20083 -> h_DEC x_20083 -| MUL (x_20085, x_20084) -> h_MUL x_20085 x_20084 -| DIV (x_20087, x_20086) -> h_DIV x_20087 x_20086 -| DA x_20088 -> h_DA x_20088 -| JC x_20089 -> h_JC x_20089 -| JNC x_20090 -> h_JNC x_20090 -| JB (x_20092, x_20091) -> h_JB x_20092 x_20091 -| JNB (x_20094, x_20093) -> h_JNB x_20094 x_20093 -| JBC (x_20096, x_20095) -> h_JBC x_20096 x_20095 -| JZ x_20097 -> h_JZ x_20097 -| JNZ x_20098 -> h_JNZ x_20098 -| CJNE (x_20100, x_20099) -> h_CJNE x_20100 x_20099 -| DJNZ (x_20102, x_20101) -> h_DJNZ x_20102 x_20101 -| ANL x_20103 -> h_ANL x_20103 -| ORL x_20104 -> h_ORL x_20104 -| XRL x_20105 -> h_XRL x_20105 -| CLR x_20106 -> h_CLR x_20106 -| CPL x_20107 -> h_CPL x_20107 -| RL x_20108 -> h_RL x_20108 -| RLC x_20109 -> h_RLC x_20109 -| RR x_20110 -> h_RR x_20110 -| RRC x_20111 -> h_RRC x_20111 -| SWAP x_20112 -> h_SWAP x_20112 -| MOV x_20113 -> h_MOV x_20113 -| MOVX x_20114 -> h_MOVX x_20114 -| SETB x_20115 -> h_SETB x_20115 -| PUSH x_20116 -> h_PUSH x_20116 -| POP x_20117 -> h_POP x_20117 -| XCH (x_20119, x_20118) -> h_XCH x_20119 x_20118 -| XCHD (x_20121, x_20120) -> h_XCHD x_20121 x_20120 +| ADD (x_950, x_949) -> h_ADD x_950 x_949 +| ADDC (x_952, x_951) -> h_ADDC x_952 x_951 +| SUBB (x_954, x_953) -> h_SUBB x_954 x_953 +| INC x_955 -> h_INC x_955 +| DEC x_956 -> h_DEC x_956 +| MUL (x_958, x_957) -> h_MUL x_958 x_957 +| DIV (x_960, x_959) -> h_DIV x_960 x_959 +| DA x_961 -> h_DA x_961 +| JC x_962 -> h_JC x_962 +| JNC x_963 -> h_JNC x_963 +| JB (x_965, x_964) -> h_JB x_965 x_964 +| JNB (x_967, x_966) -> h_JNB x_967 x_966 +| JBC (x_969, x_968) -> h_JBC x_969 x_968 +| JZ x_970 -> h_JZ x_970 +| JNZ x_971 -> h_JNZ x_971 +| CJNE (x_973, x_972) -> h_CJNE x_973 x_972 +| DJNZ (x_975, x_974) -> h_DJNZ x_975 x_974 +| ANL x_976 -> h_ANL x_976 +| ORL x_977 -> h_ORL x_977 +| XRL x_978 -> h_XRL x_978 +| CLR x_979 -> h_CLR x_979 +| CPL x_980 -> h_CPL x_980 +| RL x_981 -> h_RL x_981 +| RLC x_982 -> h_RLC x_982 +| RR x_983 -> h_RR x_983 +| RRC x_984 -> h_RRC x_984 +| SWAP x_985 -> h_SWAP x_985 +| MOV x_986 -> h_MOV x_986 +| MOVX x_987 -> h_MOVX x_987 +| SETB x_988 -> h_SETB x_988 +| PUSH x_989 -> h_PUSH x_989 +| POP x_990 -> h_POP x_990 +| XCH (x_992, x_991) -> h_XCH x_992 x_991 +| XCHD (x_994, x_993) -> h_XCHD x_994 x_993 | RET -> h_RET | RETI -> h_RETI | NOP -> h_NOP -| JMP x_20122 -> h_JMP x_20122 +| JMP x_995 -> h_JMP x_995 (** val preinstruction_rect_Type2 : (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode @@ -2512,44 +2512,44 @@ let rec preinstruction_rect_Type3 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_ -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) 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 -| ADD (x_20163, x_20162) -> h_ADD x_20163 x_20162 -| ADDC (x_20165, x_20164) -> h_ADDC x_20165 x_20164 -| SUBB (x_20167, x_20166) -> h_SUBB x_20167 x_20166 -| INC x_20168 -> h_INC x_20168 -| DEC x_20169 -> h_DEC x_20169 -| MUL (x_20171, x_20170) -> h_MUL x_20171 x_20170 -| DIV (x_20173, x_20172) -> h_DIV x_20173 x_20172 -| DA x_20174 -> h_DA x_20174 -| JC x_20175 -> h_JC x_20175 -| JNC x_20176 -> h_JNC x_20176 -| JB (x_20178, x_20177) -> h_JB x_20178 x_20177 -| JNB (x_20180, x_20179) -> h_JNB x_20180 x_20179 -| JBC (x_20182, x_20181) -> h_JBC x_20182 x_20181 -| JZ x_20183 -> h_JZ x_20183 -| JNZ x_20184 -> h_JNZ x_20184 -| CJNE (x_20186, x_20185) -> h_CJNE x_20186 x_20185 -| DJNZ (x_20188, x_20187) -> h_DJNZ x_20188 x_20187 -| ANL x_20189 -> h_ANL x_20189 -| ORL x_20190 -> h_ORL x_20190 -| XRL x_20191 -> h_XRL x_20191 -| CLR x_20192 -> h_CLR x_20192 -| CPL x_20193 -> h_CPL x_20193 -| RL x_20194 -> h_RL x_20194 -| RLC x_20195 -> h_RLC x_20195 -| RR x_20196 -> h_RR x_20196 -| RRC x_20197 -> h_RRC x_20197 -| SWAP x_20198 -> h_SWAP x_20198 -| MOV x_20199 -> h_MOV x_20199 -| MOVX x_20200 -> h_MOVX x_20200 -| SETB x_20201 -> h_SETB x_20201 -| PUSH x_20202 -> h_PUSH x_20202 -| POP x_20203 -> h_POP x_20203 -| XCH (x_20205, x_20204) -> h_XCH x_20205 x_20204 -| XCHD (x_20207, x_20206) -> h_XCHD x_20207 x_20206 +| ADD (x_1036, x_1035) -> h_ADD x_1036 x_1035 +| ADDC (x_1038, x_1037) -> h_ADDC x_1038 x_1037 +| SUBB (x_1040, x_1039) -> h_SUBB x_1040 x_1039 +| INC x_1041 -> h_INC x_1041 +| DEC x_1042 -> h_DEC x_1042 +| MUL (x_1044, x_1043) -> h_MUL x_1044 x_1043 +| DIV (x_1046, x_1045) -> h_DIV x_1046 x_1045 +| DA x_1047 -> h_DA x_1047 +| JC x_1048 -> h_JC x_1048 +| JNC x_1049 -> h_JNC x_1049 +| JB (x_1051, x_1050) -> h_JB x_1051 x_1050 +| JNB (x_1053, x_1052) -> h_JNB x_1053 x_1052 +| JBC (x_1055, x_1054) -> h_JBC x_1055 x_1054 +| JZ x_1056 -> h_JZ x_1056 +| JNZ x_1057 -> h_JNZ x_1057 +| CJNE (x_1059, x_1058) -> h_CJNE x_1059 x_1058 +| DJNZ (x_1061, x_1060) -> h_DJNZ x_1061 x_1060 +| ANL x_1062 -> h_ANL x_1062 +| ORL x_1063 -> h_ORL x_1063 +| XRL x_1064 -> h_XRL x_1064 +| CLR x_1065 -> h_CLR x_1065 +| CPL x_1066 -> h_CPL x_1066 +| RL x_1067 -> h_RL x_1067 +| RLC x_1068 -> h_RLC x_1068 +| RR x_1069 -> h_RR x_1069 +| RRC x_1070 -> h_RRC x_1070 +| SWAP x_1071 -> h_SWAP x_1071 +| MOV x_1072 -> h_MOV x_1072 +| MOVX x_1073 -> h_MOVX x_1073 +| SETB x_1074 -> h_SETB x_1074 +| PUSH x_1075 -> h_PUSH x_1075 +| POP x_1076 -> h_POP x_1076 +| XCH (x_1078, x_1077) -> h_XCH x_1078 x_1077 +| XCHD (x_1080, x_1079) -> h_XCHD x_1080 x_1079 | RET -> h_RET | RETI -> h_RETI | NOP -> h_NOP -| JMP x_20208 -> h_JMP x_20208 +| JMP x_1081 -> h_JMP x_1081 (** val preinstruction_rect_Type1 : (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode @@ -2587,44 +2587,44 @@ let rec preinstruction_rect_Type2 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_ -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) 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 -| ADD (x_20249, x_20248) -> h_ADD x_20249 x_20248 -| ADDC (x_20251, x_20250) -> h_ADDC x_20251 x_20250 -| SUBB (x_20253, x_20252) -> h_SUBB x_20253 x_20252 -| INC x_20254 -> h_INC x_20254 -| DEC x_20255 -> h_DEC x_20255 -| MUL (x_20257, x_20256) -> h_MUL x_20257 x_20256 -| DIV (x_20259, x_20258) -> h_DIV x_20259 x_20258 -| DA x_20260 -> h_DA x_20260 -| JC x_20261 -> h_JC x_20261 -| JNC x_20262 -> h_JNC x_20262 -| JB (x_20264, x_20263) -> h_JB x_20264 x_20263 -| JNB (x_20266, x_20265) -> h_JNB x_20266 x_20265 -| JBC (x_20268, x_20267) -> h_JBC x_20268 x_20267 -| JZ x_20269 -> h_JZ x_20269 -| JNZ x_20270 -> h_JNZ x_20270 -| CJNE (x_20272, x_20271) -> h_CJNE x_20272 x_20271 -| DJNZ (x_20274, x_20273) -> h_DJNZ x_20274 x_20273 -| ANL x_20275 -> h_ANL x_20275 -| ORL x_20276 -> h_ORL x_20276 -| XRL x_20277 -> h_XRL x_20277 -| CLR x_20278 -> h_CLR x_20278 -| CPL x_20279 -> h_CPL x_20279 -| RL x_20280 -> h_RL x_20280 -| RLC x_20281 -> h_RLC x_20281 -| RR x_20282 -> h_RR x_20282 -| RRC x_20283 -> h_RRC x_20283 -| SWAP x_20284 -> h_SWAP x_20284 -| MOV x_20285 -> h_MOV x_20285 -| MOVX x_20286 -> h_MOVX x_20286 -| SETB x_20287 -> h_SETB x_20287 -| PUSH x_20288 -> h_PUSH x_20288 -| POP x_20289 -> h_POP x_20289 -| XCH (x_20291, x_20290) -> h_XCH x_20291 x_20290 -| XCHD (x_20293, x_20292) -> h_XCHD x_20293 x_20292 +| ADD (x_1122, x_1121) -> h_ADD x_1122 x_1121 +| ADDC (x_1124, x_1123) -> h_ADDC x_1124 x_1123 +| SUBB (x_1126, x_1125) -> h_SUBB x_1126 x_1125 +| INC x_1127 -> h_INC x_1127 +| DEC x_1128 -> h_DEC x_1128 +| MUL (x_1130, x_1129) -> h_MUL x_1130 x_1129 +| DIV (x_1132, x_1131) -> h_DIV x_1132 x_1131 +| DA x_1133 -> h_DA x_1133 +| JC x_1134 -> h_JC x_1134 +| JNC x_1135 -> h_JNC x_1135 +| JB (x_1137, x_1136) -> h_JB x_1137 x_1136 +| JNB (x_1139, x_1138) -> h_JNB x_1139 x_1138 +| JBC (x_1141, x_1140) -> h_JBC x_1141 x_1140 +| JZ x_1142 -> h_JZ x_1142 +| JNZ x_1143 -> h_JNZ x_1143 +| CJNE (x_1145, x_1144) -> h_CJNE x_1145 x_1144 +| DJNZ (x_1147, x_1146) -> h_DJNZ x_1147 x_1146 +| ANL x_1148 -> h_ANL x_1148 +| ORL x_1149 -> h_ORL x_1149 +| XRL x_1150 -> h_XRL x_1150 +| CLR x_1151 -> h_CLR x_1151 +| CPL x_1152 -> h_CPL x_1152 +| RL x_1153 -> h_RL x_1153 +| RLC x_1154 -> h_RLC x_1154 +| RR x_1155 -> h_RR x_1155 +| RRC x_1156 -> h_RRC x_1156 +| SWAP x_1157 -> h_SWAP x_1157 +| MOV x_1158 -> h_MOV x_1158 +| MOVX x_1159 -> h_MOVX x_1159 +| SETB x_1160 -> h_SETB x_1160 +| PUSH x_1161 -> h_PUSH x_1161 +| POP x_1162 -> h_POP x_1162 +| XCH (x_1164, x_1163) -> h_XCH x_1164 x_1163 +| XCHD (x_1166, x_1165) -> h_XCHD x_1166 x_1165 | RET -> h_RET | RETI -> h_RETI | NOP -> h_NOP -| JMP x_20294 -> h_JMP x_20294 +| JMP x_1167 -> h_JMP x_1167 (** val preinstruction_rect_Type0 : (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode @@ -2662,44 +2662,44 @@ let rec preinstruction_rect_Type1 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_ -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) 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 -| ADD (x_20335, x_20334) -> h_ADD x_20335 x_20334 -| ADDC (x_20337, x_20336) -> h_ADDC x_20337 x_20336 -| SUBB (x_20339, x_20338) -> h_SUBB x_20339 x_20338 -| INC x_20340 -> h_INC x_20340 -| DEC x_20341 -> h_DEC x_20341 -| MUL (x_20343, x_20342) -> h_MUL x_20343 x_20342 -| DIV (x_20345, x_20344) -> h_DIV x_20345 x_20344 -| DA x_20346 -> h_DA x_20346 -| JC x_20347 -> h_JC x_20347 -| JNC x_20348 -> h_JNC x_20348 -| JB (x_20350, x_20349) -> h_JB x_20350 x_20349 -| JNB (x_20352, x_20351) -> h_JNB x_20352 x_20351 -| JBC (x_20354, x_20353) -> h_JBC x_20354 x_20353 -| JZ x_20355 -> h_JZ x_20355 -| JNZ x_20356 -> h_JNZ x_20356 -| CJNE (x_20358, x_20357) -> h_CJNE x_20358 x_20357 -| DJNZ (x_20360, x_20359) -> h_DJNZ x_20360 x_20359 -| ANL x_20361 -> h_ANL x_20361 -| ORL x_20362 -> h_ORL x_20362 -| XRL x_20363 -> h_XRL x_20363 -| CLR x_20364 -> h_CLR x_20364 -| CPL x_20365 -> h_CPL x_20365 -| RL x_20366 -> h_RL x_20366 -| RLC x_20367 -> h_RLC x_20367 -| RR x_20368 -> h_RR x_20368 -| RRC x_20369 -> h_RRC x_20369 -| SWAP x_20370 -> h_SWAP x_20370 -| MOV x_20371 -> h_MOV x_20371 -| MOVX x_20372 -> h_MOVX x_20372 -| SETB x_20373 -> h_SETB x_20373 -| PUSH x_20374 -> h_PUSH x_20374 -| POP x_20375 -> h_POP x_20375 -| XCH (x_20377, x_20376) -> h_XCH x_20377 x_20376 -| XCHD (x_20379, x_20378) -> h_XCHD x_20379 x_20378 +| ADD (x_1208, x_1207) -> h_ADD x_1208 x_1207 +| ADDC (x_1210, x_1209) -> h_ADDC x_1210 x_1209 +| SUBB (x_1212, x_1211) -> h_SUBB x_1212 x_1211 +| INC x_1213 -> h_INC x_1213 +| DEC x_1214 -> h_DEC x_1214 +| MUL (x_1216, x_1215) -> h_MUL x_1216 x_1215 +| DIV (x_1218, x_1217) -> h_DIV x_1218 x_1217 +| DA x_1219 -> h_DA x_1219 +| JC x_1220 -> h_JC x_1220 +| JNC x_1221 -> h_JNC x_1221 +| JB (x_1223, x_1222) -> h_JB x_1223 x_1222 +| JNB (x_1225, x_1224) -> h_JNB x_1225 x_1224 +| JBC (x_1227, x_1226) -> h_JBC x_1227 x_1226 +| JZ x_1228 -> h_JZ x_1228 +| JNZ x_1229 -> h_JNZ x_1229 +| CJNE (x_1231, x_1230) -> h_CJNE x_1231 x_1230 +| DJNZ (x_1233, x_1232) -> h_DJNZ x_1233 x_1232 +| ANL x_1234 -> h_ANL x_1234 +| ORL x_1235 -> h_ORL x_1235 +| XRL x_1236 -> h_XRL x_1236 +| CLR x_1237 -> h_CLR x_1237 +| CPL x_1238 -> h_CPL x_1238 +| RL x_1239 -> h_RL x_1239 +| RLC x_1240 -> h_RLC x_1240 +| RR x_1241 -> h_RR x_1241 +| RRC x_1242 -> h_RRC x_1242 +| SWAP x_1243 -> h_SWAP x_1243 +| MOV x_1244 -> h_MOV x_1244 +| MOVX x_1245 -> h_MOVX x_1245 +| SETB x_1246 -> h_SETB x_1246 +| PUSH x_1247 -> h_PUSH x_1247 +| POP x_1248 -> h_POP x_1248 +| XCH (x_1250, x_1249) -> h_XCH x_1250 x_1249 +| XCHD (x_1252, x_1251) -> h_XCHD x_1252 x_1251 | RET -> h_RET | RETI -> h_RETI | NOP -> h_NOP -| JMP x_20380 -> h_JMP x_20380 +| JMP x_1253 -> h_JMP x_1253 (** val preinstruction_inv_rect_Type4 : 'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ -> @@ -5103,13 +5103,13 @@ type instruction = -> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1 **) let rec instruction_rect_Type4 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function -| ACALL x_20952 -> h_ACALL x_20952 -| LCALL x_20953 -> h_LCALL x_20953 -| AJMP x_20954 -> h_AJMP x_20954 -| LJMP x_20955 -> h_LJMP x_20955 -| SJMP x_20956 -> h_SJMP x_20956 -| MOVC (x_20958, x_20957) -> h_MOVC x_20958 x_20957 -| RealInstruction x_20959 -> h_RealInstruction x_20959 +| ACALL x_1825 -> h_ACALL x_1825 +| LCALL x_1826 -> h_LCALL x_1826 +| AJMP x_1827 -> h_AJMP x_1827 +| LJMP x_1828 -> h_LJMP x_1828 +| SJMP x_1829 -> h_SJMP x_1829 +| MOVC (x_1831, x_1830) -> h_MOVC x_1831 x_1830 +| RealInstruction x_1832 -> h_RealInstruction x_1832 (** val instruction_rect_Type5 : (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) -> @@ -5118,13 +5118,13 @@ let rec instruction_rect_Type4 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_Rea -> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1 **) let rec instruction_rect_Type5 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function -| ACALL x_20968 -> h_ACALL x_20968 -| LCALL x_20969 -> h_LCALL x_20969 -| AJMP x_20970 -> h_AJMP x_20970 -| LJMP x_20971 -> h_LJMP x_20971 -| SJMP x_20972 -> h_SJMP x_20972 -| MOVC (x_20974, x_20973) -> h_MOVC x_20974 x_20973 -| RealInstruction x_20975 -> h_RealInstruction x_20975 +| ACALL x_1841 -> h_ACALL x_1841 +| LCALL x_1842 -> h_LCALL x_1842 +| AJMP x_1843 -> h_AJMP x_1843 +| LJMP x_1844 -> h_LJMP x_1844 +| SJMP x_1845 -> h_SJMP x_1845 +| MOVC (x_1847, x_1846) -> h_MOVC x_1847 x_1846 +| RealInstruction x_1848 -> h_RealInstruction x_1848 (** val instruction_rect_Type3 : (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) -> @@ -5133,13 +5133,13 @@ let rec instruction_rect_Type5 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_Rea -> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1 **) let rec instruction_rect_Type3 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function -| ACALL x_20984 -> h_ACALL x_20984 -| LCALL x_20985 -> h_LCALL x_20985 -| AJMP x_20986 -> h_AJMP x_20986 -| LJMP x_20987 -> h_LJMP x_20987 -| SJMP x_20988 -> h_SJMP x_20988 -| MOVC (x_20990, x_20989) -> h_MOVC x_20990 x_20989 -| RealInstruction x_20991 -> h_RealInstruction x_20991 +| ACALL x_1857 -> h_ACALL x_1857 +| LCALL x_1858 -> h_LCALL x_1858 +| AJMP x_1859 -> h_AJMP x_1859 +| LJMP x_1860 -> h_LJMP x_1860 +| SJMP x_1861 -> h_SJMP x_1861 +| MOVC (x_1863, x_1862) -> h_MOVC x_1863 x_1862 +| RealInstruction x_1864 -> h_RealInstruction x_1864 (** val instruction_rect_Type2 : (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) -> @@ -5148,13 +5148,13 @@ let rec instruction_rect_Type3 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_Rea -> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1 **) let rec instruction_rect_Type2 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function -| ACALL x_21000 -> h_ACALL x_21000 -| LCALL x_21001 -> h_LCALL x_21001 -| AJMP x_21002 -> h_AJMP x_21002 -| LJMP x_21003 -> h_LJMP x_21003 -| SJMP x_21004 -> h_SJMP x_21004 -| MOVC (x_21006, x_21005) -> h_MOVC x_21006 x_21005 -| RealInstruction x_21007 -> h_RealInstruction x_21007 +| ACALL x_1873 -> h_ACALL x_1873 +| LCALL x_1874 -> h_LCALL x_1874 +| AJMP x_1875 -> h_AJMP x_1875 +| LJMP x_1876 -> h_LJMP x_1876 +| SJMP x_1877 -> h_SJMP x_1877 +| MOVC (x_1879, x_1878) -> h_MOVC x_1879 x_1878 +| RealInstruction x_1880 -> h_RealInstruction x_1880 (** val instruction_rect_Type1 : (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) -> @@ -5163,13 +5163,13 @@ let rec instruction_rect_Type2 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_Rea -> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1 **) let rec instruction_rect_Type1 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function -| ACALL x_21016 -> h_ACALL x_21016 -| LCALL x_21017 -> h_LCALL x_21017 -| AJMP x_21018 -> h_AJMP x_21018 -| LJMP x_21019 -> h_LJMP x_21019 -| SJMP x_21020 -> h_SJMP x_21020 -| MOVC (x_21022, x_21021) -> h_MOVC x_21022 x_21021 -| RealInstruction x_21023 -> h_RealInstruction x_21023 +| ACALL x_1889 -> h_ACALL x_1889 +| LCALL x_1890 -> h_LCALL x_1890 +| AJMP x_1891 -> h_AJMP x_1891 +| LJMP x_1892 -> h_LJMP x_1892 +| SJMP x_1893 -> h_SJMP x_1893 +| MOVC (x_1895, x_1894) -> h_MOVC x_1895 x_1894 +| RealInstruction x_1896 -> h_RealInstruction x_1896 (** val instruction_rect_Type0 : (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) -> @@ -5178,13 +5178,13 @@ let rec instruction_rect_Type1 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_Rea -> 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1 **) let rec instruction_rect_Type0 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function -| ACALL x_21032 -> h_ACALL x_21032 -| LCALL x_21033 -> h_LCALL x_21033 -| AJMP x_21034 -> h_AJMP x_21034 -| LJMP x_21035 -> h_LJMP x_21035 -| SJMP x_21036 -> h_SJMP x_21036 -| MOVC (x_21038, x_21037) -> h_MOVC x_21038 x_21037 -| RealInstruction x_21039 -> h_RealInstruction x_21039 +| ACALL x_1905 -> h_ACALL x_1905 +| LCALL x_1906 -> h_LCALL x_1906 +| AJMP x_1907 -> h_AJMP x_1907 +| LJMP x_1908 -> h_LJMP x_1908 +| SJMP x_1909 -> h_SJMP x_1909 +| MOVC (x_1911, x_1910) -> h_MOVC x_1911 x_1910 +| RealInstruction x_1912 -> h_RealInstruction x_1912 (** val instruction_inv_rect_Type4 : instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode @@ -5475,13 +5475,13 @@ type pseudo_instruction = Types.sum -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1 **) let rec pseudo_instruction_rect_Type4 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function -| Instruction x_21202 -> h_Instruction x_21202 -| Comment x_21203 -> h_Comment x_21203 -| Cost x_21204 -> h_Cost x_21204 -| Jmp x_21205 -> h_Jmp x_21205 -| Jnz (x_21208, x_21207, x_21206) -> h_Jnz x_21208 x_21207 x_21206 -| Call x_21209 -> h_Call x_21209 -| Mov (x_21212, x_21211, x_21210) -> h_Mov x_21212 x_21211 x_21210 +| Instruction x_2075 -> h_Instruction x_2075 +| Comment x_2076 -> h_Comment x_2076 +| Cost x_2077 -> h_Cost x_2077 +| Jmp x_2078 -> h_Jmp x_2078 +| Jnz (x_2081, x_2080, x_2079) -> h_Jnz x_2081 x_2080 x_2079 +| Call x_2082 -> h_Call x_2082 +| Mov (x_2085, x_2084, x_2083) -> h_Mov x_2085 x_2084 x_2083 (** val pseudo_instruction_rect_Type5 : (identifier preinstruction -> 'a1) -> (String.string -> 'a1) -> @@ -5491,13 +5491,13 @@ let rec pseudo_instruction_rect_Type4 h_Instruction h_Comment h_Cost h_Jmp h_Jnz Types.sum -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1 **) let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function -| Instruction x_21221 -> h_Instruction x_21221 -| Comment x_21222 -> h_Comment x_21222 -| Cost x_21223 -> h_Cost x_21223 -| Jmp x_21224 -> h_Jmp x_21224 -| Jnz (x_21227, x_21226, x_21225) -> h_Jnz x_21227 x_21226 x_21225 -| Call x_21228 -> h_Call x_21228 -| Mov (x_21231, x_21230, x_21229) -> h_Mov x_21231 x_21230 x_21229 +| Instruction x_2094 -> h_Instruction x_2094 +| Comment x_2095 -> h_Comment x_2095 +| Cost x_2096 -> h_Cost x_2096 +| Jmp x_2097 -> h_Jmp x_2097 +| Jnz (x_2100, x_2099, x_2098) -> h_Jnz x_2100 x_2099 x_2098 +| Call x_2101 -> h_Call x_2101 +| Mov (x_2104, x_2103, x_2102) -> h_Mov x_2104 x_2103 x_2102 (** val pseudo_instruction_rect_Type3 : (identifier preinstruction -> 'a1) -> (String.string -> 'a1) -> @@ -5507,13 +5507,13 @@ let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Jnz Types.sum -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1 **) let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function -| Instruction x_21240 -> h_Instruction x_21240 -| Comment x_21241 -> h_Comment x_21241 -| Cost x_21242 -> h_Cost x_21242 -| Jmp x_21243 -> h_Jmp x_21243 -| Jnz (x_21246, x_21245, x_21244) -> h_Jnz x_21246 x_21245 x_21244 -| Call x_21247 -> h_Call x_21247 -| Mov (x_21250, x_21249, x_21248) -> h_Mov x_21250 x_21249 x_21248 +| Instruction x_2113 -> h_Instruction x_2113 +| Comment x_2114 -> h_Comment x_2114 +| Cost x_2115 -> h_Cost x_2115 +| Jmp x_2116 -> h_Jmp x_2116 +| Jnz (x_2119, x_2118, x_2117) -> h_Jnz x_2119 x_2118 x_2117 +| Call x_2120 -> h_Call x_2120 +| Mov (x_2123, x_2122, x_2121) -> h_Mov x_2123 x_2122 x_2121 (** val pseudo_instruction_rect_Type2 : (identifier preinstruction -> 'a1) -> (String.string -> 'a1) -> @@ -5523,13 +5523,13 @@ let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Jnz Types.sum -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1 **) let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function -| Instruction x_21259 -> h_Instruction x_21259 -| Comment x_21260 -> h_Comment x_21260 -| Cost x_21261 -> h_Cost x_21261 -| Jmp x_21262 -> h_Jmp x_21262 -| Jnz (x_21265, x_21264, x_21263) -> h_Jnz x_21265 x_21264 x_21263 -| Call x_21266 -> h_Call x_21266 -| Mov (x_21269, x_21268, x_21267) -> h_Mov x_21269 x_21268 x_21267 +| Instruction x_2132 -> h_Instruction x_2132 +| Comment x_2133 -> h_Comment x_2133 +| Cost x_2134 -> h_Cost x_2134 +| Jmp x_2135 -> h_Jmp x_2135 +| Jnz (x_2138, x_2137, x_2136) -> h_Jnz x_2138 x_2137 x_2136 +| Call x_2139 -> h_Call x_2139 +| Mov (x_2142, x_2141, x_2140) -> h_Mov x_2142 x_2141 x_2140 (** val pseudo_instruction_rect_Type1 : (identifier preinstruction -> 'a1) -> (String.string -> 'a1) -> @@ -5539,13 +5539,13 @@ let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Jnz Types.sum -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1 **) let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function -| Instruction x_21278 -> h_Instruction x_21278 -| Comment x_21279 -> h_Comment x_21279 -| Cost x_21280 -> h_Cost x_21280 -| Jmp x_21281 -> h_Jmp x_21281 -| Jnz (x_21284, x_21283, x_21282) -> h_Jnz x_21284 x_21283 x_21282 -| Call x_21285 -> h_Call x_21285 -| Mov (x_21288, x_21287, x_21286) -> h_Mov x_21288 x_21287 x_21286 +| Instruction x_2151 -> h_Instruction x_2151 +| Comment x_2152 -> h_Comment x_2152 +| Cost x_2153 -> h_Cost x_2153 +| Jmp x_2154 -> h_Jmp x_2154 +| Jnz (x_2157, x_2156, x_2155) -> h_Jnz x_2157 x_2156 x_2155 +| Call x_2158 -> h_Call x_2158 +| Mov (x_2161, x_2160, x_2159) -> h_Mov x_2161 x_2160 x_2159 (** val pseudo_instruction_rect_Type0 : (identifier preinstruction -> 'a1) -> (String.string -> 'a1) -> @@ -5555,13 +5555,13 @@ let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Jnz Types.sum -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1 **) let rec pseudo_instruction_rect_Type0 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function -| Instruction x_21297 -> h_Instruction x_21297 -| Comment x_21298 -> h_Comment x_21298 -| Cost x_21299 -> h_Cost x_21299 -| Jmp x_21300 -> h_Jmp x_21300 -| Jnz (x_21303, x_21302, x_21301) -> h_Jnz x_21303 x_21302 x_21301 -| Call x_21304 -> h_Call x_21304 -| Mov (x_21307, x_21306, x_21305) -> h_Mov x_21307 x_21306 x_21305 +| Instruction x_2170 -> h_Instruction x_2170 +| Comment x_2171 -> h_Comment x_2171 +| Cost x_2172 -> h_Cost x_2172 +| Jmp x_2173 -> h_Jmp x_2173 +| Jnz (x_2176, x_2175, x_2174) -> h_Jnz x_2176 x_2175 x_2174 +| Call x_2177 -> h_Call x_2177 +| Mov (x_2180, x_2179, x_2178) -> h_Mov x_2180 x_2179 x_2178 (** val pseudo_instruction_inv_rect_Type4 : pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) -> @@ -5777,9 +5777,9 @@ type pseudo_assembly_program = { preamble : (identifier, BitVector.word) labelled_instruction List.list -> __ -> (identifier, AST.ident) Types.prod List.list -> identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1 **) -let rec pseudo_assembly_program_rect_Type4 h_mk_pseudo_assembly_program x_21431 = +let rec pseudo_assembly_program_rect_Type4 h_mk_pseudo_assembly_program x_2304 = let { preamble = preamble0; code = code0; renamed_symbols = - renamed_symbols0; final_label = final_label0 } = x_21431 + renamed_symbols0; final_label = final_label0 } = x_2304 in h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0 final_label0 __ __ @@ -5789,9 +5789,9 @@ let rec pseudo_assembly_program_rect_Type4 h_mk_pseudo_assembly_program x_21431 labelled_instruction List.list -> __ -> (identifier, AST.ident) Types.prod List.list -> identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1 **) -let rec pseudo_assembly_program_rect_Type5 h_mk_pseudo_assembly_program x_21433 = +let rec pseudo_assembly_program_rect_Type5 h_mk_pseudo_assembly_program x_2306 = let { preamble = preamble0; code = code0; renamed_symbols = - renamed_symbols0; final_label = final_label0 } = x_21433 + renamed_symbols0; final_label = final_label0 } = x_2306 in h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0 final_label0 __ __ @@ -5801,9 +5801,9 @@ let rec pseudo_assembly_program_rect_Type5 h_mk_pseudo_assembly_program x_21433 labelled_instruction List.list -> __ -> (identifier, AST.ident) Types.prod List.list -> identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1 **) -let rec pseudo_assembly_program_rect_Type3 h_mk_pseudo_assembly_program x_21435 = +let rec pseudo_assembly_program_rect_Type3 h_mk_pseudo_assembly_program x_2308 = let { preamble = preamble0; code = code0; renamed_symbols = - renamed_symbols0; final_label = final_label0 } = x_21435 + renamed_symbols0; final_label = final_label0 } = x_2308 in h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0 final_label0 __ __ @@ -5813,9 +5813,9 @@ let rec pseudo_assembly_program_rect_Type3 h_mk_pseudo_assembly_program x_21435 labelled_instruction List.list -> __ -> (identifier, AST.ident) Types.prod List.list -> identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1 **) -let rec pseudo_assembly_program_rect_Type2 h_mk_pseudo_assembly_program x_21437 = +let rec pseudo_assembly_program_rect_Type2 h_mk_pseudo_assembly_program x_2310 = let { preamble = preamble0; code = code0; renamed_symbols = - renamed_symbols0; final_label = final_label0 } = x_21437 + renamed_symbols0; final_label = final_label0 } = x_2310 in h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0 final_label0 __ __ @@ -5825,9 +5825,9 @@ let rec pseudo_assembly_program_rect_Type2 h_mk_pseudo_assembly_program x_21437 labelled_instruction List.list -> __ -> (identifier, AST.ident) Types.prod List.list -> identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1 **) -let rec pseudo_assembly_program_rect_Type1 h_mk_pseudo_assembly_program x_21439 = +let rec pseudo_assembly_program_rect_Type1 h_mk_pseudo_assembly_program x_2312 = let { preamble = preamble0; code = code0; renamed_symbols = - renamed_symbols0; final_label = final_label0 } = x_21439 + renamed_symbols0; final_label = final_label0 } = x_2312 in h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0 final_label0 __ __ @@ -5837,9 +5837,9 @@ let rec pseudo_assembly_program_rect_Type1 h_mk_pseudo_assembly_program x_21439 labelled_instruction List.list -> __ -> (identifier, AST.ident) Types.prod List.list -> identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1 **) -let rec pseudo_assembly_program_rect_Type0 h_mk_pseudo_assembly_program x_21441 = +let rec pseudo_assembly_program_rect_Type0 h_mk_pseudo_assembly_program x_2314 = let { preamble = preamble0; code = code0; renamed_symbols = - renamed_symbols0; final_label = final_label0 } = x_21441 + renamed_symbols0; final_label = final_label0 } = x_2314 in h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0 final_label0 __ __ @@ -5936,17 +5936,22 @@ let next pmem pc = let load_code_memory0 program = (Types.pi1 (FoldStuff.foldl_strong program (fun prefix v tl _ i_mem -> - (let { Types.fst = i; Types.snd = mem } = Types.pi1 i_mem in - (fun _ -> { Types.fst = (Nat.S i); Types.snd = + (let { Types.fst = eta24568; Types.snd = mem } = Types.pi1 i_mem in + (fun _ -> + (let { Types.fst = i; Types.snd = bvi } = eta24568 in + (fun _ -> { Types.fst = { Types.fst = (Nat.S i); Types.snd = + (Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + Nat.O)))))))))))))))) bvi) }; Types.snd = (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - Nat.O)))))))))))))))) - (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S Nat.O)))))))))))))))) i) v mem) })) __) { Types.fst = - Nat.O; Types.snd = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S + Nat.O)))))))))))))))) bvi v mem) })) __)) __) { Types.fst = + { Types.fst = Nat.O; Types.snd = + (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + Nat.O))))))))))))))))) }; Types.snd = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S Nat.O))))))))))))))))) })).Types.snd + (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))) })).Types.snd (** val load_code_memory : object_code -> BitVector.byte BitVectorTrie.bitVectorTrie **) @@ -5967,9 +5972,9 @@ type labelled_object_code = { oc : object_code; (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) -> labelled_object_code -> 'a1 **) -let rec labelled_object_code_rect_Type4 h_mk_labelled_object_code x_21457 = +let rec labelled_object_code_rect_Type4 h_mk_labelled_object_code x_2330 = let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable = - symboltable0; final_pc = final_pc0 } = x_21457 + symboltable0; final_pc = final_pc0 } = x_2330 in h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __ @@ -5977,9 +5982,9 @@ let rec labelled_object_code_rect_Type4 h_mk_labelled_object_code x_21457 = (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) -> labelled_object_code -> 'a1 **) -let rec labelled_object_code_rect_Type5 h_mk_labelled_object_code x_21459 = +let rec labelled_object_code_rect_Type5 h_mk_labelled_object_code x_2332 = let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable = - symboltable0; final_pc = final_pc0 } = x_21459 + symboltable0; final_pc = final_pc0 } = x_2332 in h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __ @@ -5987,9 +5992,9 @@ let rec labelled_object_code_rect_Type5 h_mk_labelled_object_code x_21459 = (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) -> labelled_object_code -> 'a1 **) -let rec labelled_object_code_rect_Type3 h_mk_labelled_object_code x_21461 = +let rec labelled_object_code_rect_Type3 h_mk_labelled_object_code x_2334 = let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable = - symboltable0; final_pc = final_pc0 } = x_21461 + symboltable0; final_pc = final_pc0 } = x_2334 in h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __ @@ -5997,9 +6002,9 @@ let rec labelled_object_code_rect_Type3 h_mk_labelled_object_code x_21461 = (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) -> labelled_object_code -> 'a1 **) -let rec labelled_object_code_rect_Type2 h_mk_labelled_object_code x_21463 = +let rec labelled_object_code_rect_Type2 h_mk_labelled_object_code x_2336 = let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable = - symboltable0; final_pc = final_pc0 } = x_21463 + symboltable0; final_pc = final_pc0 } = x_2336 in h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __ @@ -6007,9 +6012,9 @@ let rec labelled_object_code_rect_Type2 h_mk_labelled_object_code x_21463 = (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) -> labelled_object_code -> 'a1 **) -let rec labelled_object_code_rect_Type1 h_mk_labelled_object_code x_21465 = +let rec labelled_object_code_rect_Type1 h_mk_labelled_object_code x_2338 = let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable = - symboltable0; final_pc = final_pc0 } = x_21465 + symboltable0; final_pc = final_pc0 } = x_2338 in h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __ @@ -6017,9 +6022,9 @@ let rec labelled_object_code_rect_Type1 h_mk_labelled_object_code x_21465 = (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) -> labelled_object_code -> 'a1 **) -let rec labelled_object_code_rect_Type0 h_mk_labelled_object_code x_21467 = +let rec labelled_object_code_rect_Type0 h_mk_labelled_object_code x_2340 = let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable = - symboltable0; final_pc = final_pc0 } = x_21467 + symboltable0; final_pc = final_pc0 } = x_2340 in h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __ diff --git a/extracted/aSMCosts.ml b/extracted/aSMCosts.ml index 41ba9f9..52d1276 100644 --- a/extracted/aSMCosts.ml +++ b/extracted/aSMCosts.ml @@ -501,11 +501,11 @@ let rec block_cost' prog program_counter' program_size first_time_around = | Nat.O -> (fun _ -> Nat.O) | Nat.S program_size' -> (fun _ -> - (let { Types.fst = eta31588; Types.snd = ticks } = + (let { Types.fst = eta302; Types.snd = ticks } = Fetch.fetch prog.ASM.cm program_counter' in let { Types.fst = instruction; Types.snd = program_counter'' } = - eta31588 + eta302 in (fun _ -> let to_continue = diff --git a/extracted/abstractStatus.ml b/extracted/abstractStatus.ml index 61faf8d..bc6bf1c 100644 --- a/extracted/abstractStatus.ml +++ b/extracted/abstractStatus.ml @@ -160,22 +160,15 @@ let aSM_classify0 = function | ASM.MOVC (x, x0) -> StructuredTraces.Cl_other | ASM.RealInstruction pre -> aSM_classify00 pre -(** val current_instruction0 : - BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word -> - ASM.instruction **) -let current_instruction0 code_memory program_counter = - (Fetch.fetch code_memory program_counter).Types.fst.Types.fst - (** val current_instruction : BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status -> ASM.instruction **) let current_instruction code_memory s = - current_instruction0 code_memory s.Status.program_counter + (Fetch.fetch code_memory s.Status.program_counter).Types.fst.Types.fst (** val current_instruction_label : - BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel - BitVectorTrie.bitVectorTrie -> Status.status -> CostLabel.costlabel - Types.option **) + BitVector.byte BitVectorTrie.bitVectorTrie -> ASM.costlabel_map -> + Status.status -> CostLabel.costlabel Types.option **) let current_instruction_label code_memory cost_labels s = let pc = s.Status.program_counter in BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S diff --git a/extracted/abstractStatus.mli b/extracted/abstractStatus.mli index fe82c6a..118b5cb 100644 --- a/extracted/abstractStatus.mli +++ b/extracted/abstractStatus.mli @@ -112,18 +112,13 @@ val aSM_classify00 : 'a1 ASM.preinstruction -> StructuredTraces.status_class val aSM_classify0 : ASM.instruction -> StructuredTraces.status_class -val current_instruction0 : - BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word -> - ASM.instruction - val current_instruction : BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status -> ASM.instruction val current_instruction_label : - BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel - BitVectorTrie.bitVectorTrie -> Status.status -> CostLabel.costlabel - Types.option + BitVector.byte BitVectorTrie.bitVectorTrie -> ASM.costlabel_map -> + Status.status -> CostLabel.costlabel Types.option val word_deqset : Deqsets.deqSet diff --git a/extracted/compiler.ml b/extracted/compiler.ml index f2c456d..eaae3c4 100644 --- a/extracted/compiler.ml +++ b/extracted/compiler.ml @@ -530,19 +530,24 @@ open Policy observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code Errors.res **) let assembler observe p = +prerr_endline "Y1"; Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed) (Policy.jump_expansion' p))) (fun sigma_pol -> +prerr_endline "Y2"; let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in let i = Obj.magic observe Assembly_pass { Types.fst = { Types.fst = p; Types.snd = sigma }; Types.snd = pol } in +prerr_endline "Y3"; let p0 = Assembly.assembly p sigma pol in +prerr_endline "Y4"; let i0 = Obj.magic observe Object_code_pass (Types.pi1 p0) in +prerr_endline "Y5"; Obj.magic (Errors.OK (Types.pi1 p0)))) open StructuredTraces diff --git a/extracted/compiler.mli b/extracted/compiler.mli index 26bd574..a2d8be9 100644 --- a/extracted/compiler.mli +++ b/extracted/compiler.mli @@ -322,12 +322,12 @@ val back_end : (((ASM.pseudo_assembly_program, CostLabel.costlabel) Types.prod, Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res -open Assembly - open Status open Fetch +open Assembly + open PolicyFront open PolicyStep diff --git a/extracted/fetch.ml b/extracted/fetch.ml index 4ad7b4f..0932432 100644 --- a/extracted/fetch.ml +++ b/extracted/fetch.ml @@ -1,5 +1,19 @@ open Preamble +open Types + +open Hints_declaration + +open Core_notation + +open Pts + +open Logic + +open Jmeq + +open Russell + open Exp open Setoids @@ -14,12 +28,6 @@ open Vector open Div_and_mod -open Jmeq - -open Russell - -open Types - open List open Util @@ -28,14 +36,6 @@ open FoldStuff open Bool -open Hints_declaration - -open Core_notation - -open Pts - -open Logic - open Relations open Nat @@ -78,30 +78,26 @@ open CostLabel open ASM -(** val inefficient_address_of_word_labels_code_mem : - ASM.labelled_instruction List.list -> ASM.identifier -> - BitVector.bitVector **) -let inefficient_address_of_word_labels_code_mem code_mem id = - Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - Nat.O)))))))))))))))) - (LabelledObjects.index_of - (LabelledObjects.instruction_matches_identifier PreIdentifiers.ASMTag - id) code_mem) +(** val inefficient_address_of_label : + ASM.labelled_instruction List.list -> ASM.identifier -> Nat.nat **) +let inefficient_address_of_label instr_list id = + LabelledObjects.index_of + (LabelledObjects.instruction_matches_identifier PreIdentifiers.ASMTag id) + instr_list type label_map = Nat.nat Identifiers.identifier_map (** val create_label_cost_map0 : - ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel - BitVectorTrie.bitVectorTrie) Types.prod Types.sig0 **) + ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map) + Types.prod Types.sig0 **) let create_label_cost_map0 program = (Types.pi1 (FoldStuff.foldl_strong program (fun prefix x tl _ labels_costs_ppc -> - (let { Types.fst = eta28695; Types.snd = ppc } = + (let { Types.fst = eta19; Types.snd = ppc } = Types.pi1 labels_costs_ppc in (fun _ -> - (let { Types.fst = labels; Types.snd = costs } = eta28695 in + (let { Types.fst = labels; Types.snd = costs } = eta19 in (fun _ -> (let { Types.fst = label; Types.snd = instr } = x in (fun _ -> @@ -134,29 +130,21 @@ let create_label_cost_map0 program = Nat.O))))))))))))))))) }; Types.snd = Nat.O })).Types.fst (** val create_label_cost_map : - ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel - BitVectorTrie.bitVectorTrie) Types.prod **) + ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map) + Types.prod **) let create_label_cost_map program = Types.pi1 (create_label_cost_map0 program) (** val address_of_word_labels : ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word **) -let address_of_word_labels code_mem id = - let labels = (create_label_cost_map code_mem).Types.fst in +let address_of_word_labels program id = + let labels = (create_label_cost_map program).Types.fst in + let address_of_label = fun l -> + Identifiers.lookup_def PreIdentifiers.ASMTag labels l Nat.O + in Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - Nat.O)))))))))))))))) - (Identifiers.lookup_def PreIdentifiers.ASMTag labels id Nat.O) - -(** val bitvector_max_nat : Nat.nat -> Nat.nat **) -let bitvector_max_nat length = - Exp.exp (Nat.S (Nat.S Nat.O)) length - -(** val code_memory_size : Nat.nat **) -let code_memory_size = - bitvector_max_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - Nat.O)))))))))))))))) + Nat.O)))))))))))))))) (address_of_label id) (** val prod_inv_rect_Type0 : ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **) diff --git a/extracted/fetch.mli b/extracted/fetch.mli index bad649d..283dc7f 100644 --- a/extracted/fetch.mli +++ b/extracted/fetch.mli @@ -1,5 +1,19 @@ open Preamble +open Types + +open Hints_declaration + +open Core_notation + +open Pts + +open Logic + +open Jmeq + +open Russell + open Exp open Setoids @@ -14,12 +28,6 @@ open Vector open Div_and_mod -open Jmeq - -open Russell - -open Types - open List open Util @@ -28,14 +36,6 @@ open FoldStuff open Bool -open Hints_declaration - -open Core_notation - -open Pts - -open Logic - open Relations open Nat @@ -78,26 +78,22 @@ open CostLabel open ASM -val inefficient_address_of_word_labels_code_mem : - ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.bitVector +val inefficient_address_of_label : + ASM.labelled_instruction List.list -> ASM.identifier -> Nat.nat type label_map = Nat.nat Identifiers.identifier_map val create_label_cost_map0 : - ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel - BitVectorTrie.bitVectorTrie) Types.prod Types.sig0 + ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map) + Types.prod Types.sig0 val create_label_cost_map : - ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel - BitVectorTrie.bitVectorTrie) Types.prod + ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map) + Types.prod val address_of_word_labels : ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word -val bitvector_max_nat : Nat.nat -> Nat.nat - -val code_memory_size : Nat.nat - val prod_inv_rect_Type0 : ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 diff --git a/extracted/globalenvs.ml b/extracted/globalenvs.ml index 1ae2aa3..3e52b9c 100644 --- a/extracted/globalenvs.ml +++ b/extracted/globalenvs.ml @@ -313,8 +313,8 @@ let size_init_data_list i_data = genv_t, GenMem.mem) Types.prod **) let add_globals extract_init init_env vars = Util.foldl (fun g_st id_init -> - let { Types.fst = eta1345; Types.snd = init_info } = id_init in - let { Types.fst = id; Types.snd = r } = eta1345 in + let { Types.fst = eta1367; Types.snd = init_info } = id_init in + let { Types.fst = id; Types.snd = r } = eta1367 in let init = extract_init init_info in let { Types.fst = g; Types.snd = st } = g_st in let { Types.fst = st'; Types.snd = b } = @@ -329,8 +329,8 @@ let add_globals extract_init init_env vars = GenMem.mem Errors.res **) let init_globals extract_init g m vars = Util.foldl (fun st id_init -> - let { Types.fst = eta1346; Types.snd = init_info } = id_init in - let { Types.fst = id; Types.snd = r } = eta1346 in + let { Types.fst = eta1368; Types.snd = init_info } = id_init in + let { Types.fst = id; Types.snd = r } = eta1368 in let init = extract_init init_info in Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic st) (fun st0 -> diff --git a/extracted/interpret2.ml b/extracted/interpret2.ml index 530ad61..e4b89e4 100644 --- a/extracted/interpret2.ml +++ b/extracted/interpret2.ml @@ -467,3 +467,21 @@ let aSM_preclassified_system c sigma policy = (execute_1_pseudo_instruction' c addr_of_label addr_of_symbol sigma policy (Obj.magic st))) (Obj.magic (Status.initialise_status c)) +(** val aSM_status : + ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) -> + (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status **) +let aSM_status c sigma policy = + let label_map = (Fetch.create_label_cost_map c.ASM.code).Types.fst in + let symbol_map = Status.construct_datalabels c.ASM.preamble in + let addr_of_label = fun x -> + Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + Nat.O)))))))))))))))) + (Identifiers.lookup_def PreIdentifiers.ASMTag label_map x Nat.O) + in + let addr_of_symbol = fun x -> + Identifiers.lookup_def PreIdentifiers.ASMTag symbol_map x + (addr_of_label x) + in + aSM_abstract_status c addr_of_label addr_of_symbol sigma policy + diff --git a/extracted/interpret2.mli b/extracted/interpret2.mli index 2858287..0490034 100644 --- a/extracted/interpret2.mli +++ b/extracted/interpret2.mli @@ -178,3 +178,7 @@ val aSM_preclassified_system : ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) -> Measurable.preclassified_system +val aSM_status : + ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) -> + (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status + diff --git a/extracted/joint_printer.ml b/extracted/joint_printer.ml index f463f2c..ce4472b 100644 --- a/extracted/joint_printer.ml +++ b/extracted/joint_printer.ml @@ -432,13 +432,13 @@ type 'string printing_pass_independent_params = { print_String : (String.string (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params -> 'a2 **) -let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independent_params x_263 = +let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independent_params x_25506 = let { print_String = print_String0; print_keyword = print_keyword0; print_concat = print_concat0; print_empty = print_empty0; print_ident = print_ident0; print_costlabel = print_costlabel0; print_label = print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3; print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector = - print_bitvector0 } = x_263 + print_bitvector0 } = x_25506 in h_mk_printing_pass_independent_params print_String0 print_keyword0 print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0 @@ -451,13 +451,13 @@ let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independe (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params -> 'a2 **) -let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independent_params x_265 = +let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independent_params x_25508 = let { print_String = print_String0; print_keyword = print_keyword0; print_concat = print_concat0; print_empty = print_empty0; print_ident = print_ident0; print_costlabel = print_costlabel0; print_label = print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3; print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector = - print_bitvector0 } = x_265 + print_bitvector0 } = x_25508 in h_mk_printing_pass_independent_params print_String0 print_keyword0 print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0 @@ -470,13 +470,13 @@ let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independe (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params -> 'a2 **) -let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independent_params x_267 = +let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independent_params x_25510 = let { print_String = print_String0; print_keyword = print_keyword0; print_concat = print_concat0; print_empty = print_empty0; print_ident = print_ident0; print_costlabel = print_costlabel0; print_label = print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3; print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector = - print_bitvector0 } = x_267 + print_bitvector0 } = x_25510 in h_mk_printing_pass_independent_params print_String0 print_keyword0 print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0 @@ -489,13 +489,13 @@ let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independe (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params -> 'a2 **) -let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independent_params x_269 = +let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independent_params x_25512 = let { print_String = print_String0; print_keyword = print_keyword0; print_concat = print_concat0; print_empty = print_empty0; print_ident = print_ident0; print_costlabel = print_costlabel0; print_label = print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3; print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector = - print_bitvector0 } = x_269 + print_bitvector0 } = x_25512 in h_mk_printing_pass_independent_params print_String0 print_keyword0 print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0 @@ -508,13 +508,13 @@ let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independe (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params -> 'a2 **) -let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independent_params x_271 = +let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independent_params x_25514 = let { print_String = print_String0; print_keyword = print_keyword0; print_concat = print_concat0; print_empty = print_empty0; print_ident = print_ident0; print_costlabel = print_costlabel0; print_label = print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3; print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector = - print_bitvector0 } = x_271 + print_bitvector0 } = x_25514 in h_mk_printing_pass_independent_params print_String0 print_keyword0 print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0 @@ -527,13 +527,13 @@ let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independe (BackEndOps.op2 -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> BitVector.bitVector -> 'a1) -> 'a2) -> 'a1 printing_pass_independent_params -> 'a2 **) -let rec printing_pass_independent_params_rect_Type0 h_mk_printing_pass_independent_params x_273 = +let rec printing_pass_independent_params_rect_Type0 h_mk_printing_pass_independent_params x_25516 = let { print_String = print_String0; print_keyword = print_keyword0; print_concat = print_concat0; print_empty = print_empty0; print_ident = print_ident0; print_costlabel = print_costlabel0; print_label = print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3; print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector = - print_bitvector0 } = x_273 + print_bitvector0 } = x_25516 in h_mk_printing_pass_independent_params print_String0 print_keyword0 print_concat0 print_empty0 print_ident0 print_costlabel0 print_label0 @@ -683,7 +683,7 @@ type 'string printing_params = { print_pass_ind : 'string (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2 **) -let rec printing_params_rect_Type4 p h_mk_printing_params x_301 = +let rec printing_params_rect_Type4 p h_mk_printing_params x_25544 = let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0; print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0; print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0; @@ -691,7 +691,7 @@ let rec printing_params_rect_Type4 p h_mk_printing_params x_301 = print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0; print_pair_move = print_pair_move0; print_call_args = print_call_args0; print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } = - x_301 + x_25544 in h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0 print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0 @@ -704,7 +704,7 @@ let rec printing_params_rect_Type4 p h_mk_printing_params x_301 = (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2 **) -let rec printing_params_rect_Type5 p h_mk_printing_params x_303 = +let rec printing_params_rect_Type5 p h_mk_printing_params x_25546 = let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0; print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0; print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0; @@ -712,7 +712,7 @@ let rec printing_params_rect_Type5 p h_mk_printing_params x_303 = print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0; print_pair_move = print_pair_move0; print_call_args = print_call_args0; print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } = - x_303 + x_25546 in h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0 print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0 @@ -725,7 +725,7 @@ let rec printing_params_rect_Type5 p h_mk_printing_params x_303 = (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2 **) -let rec printing_params_rect_Type3 p h_mk_printing_params x_305 = +let rec printing_params_rect_Type3 p h_mk_printing_params x_25548 = let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0; print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0; print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0; @@ -733,7 +733,7 @@ let rec printing_params_rect_Type3 p h_mk_printing_params x_305 = print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0; print_pair_move = print_pair_move0; print_call_args = print_call_args0; print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } = - x_305 + x_25548 in h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0 print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0 @@ -746,7 +746,7 @@ let rec printing_params_rect_Type3 p h_mk_printing_params x_305 = (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2 **) -let rec printing_params_rect_Type2 p h_mk_printing_params x_307 = +let rec printing_params_rect_Type2 p h_mk_printing_params x_25550 = let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0; print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0; print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0; @@ -754,7 +754,7 @@ let rec printing_params_rect_Type2 p h_mk_printing_params x_307 = print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0; print_pair_move = print_pair_move0; print_call_args = print_call_args0; print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } = - x_307 + x_25550 in h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0 print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0 @@ -767,7 +767,7 @@ let rec printing_params_rect_Type2 p h_mk_printing_params x_307 = (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2 **) -let rec printing_params_rect_Type1 p h_mk_printing_params x_309 = +let rec printing_params_rect_Type1 p h_mk_printing_params x_25552 = let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0; print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0; print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0; @@ -775,7 +775,7 @@ let rec printing_params_rect_Type1 p h_mk_printing_params x_309 = print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0; print_pair_move = print_pair_move0; print_call_args = print_call_args0; print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } = - x_309 + x_25552 in h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0 print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0 @@ -788,7 +788,7 @@ let rec printing_params_rect_Type1 p h_mk_printing_params x_309 = (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 printing_params -> 'a2 **) -let rec printing_params_rect_Type0 p h_mk_printing_params x_311 = +let rec printing_params_rect_Type0 p h_mk_printing_params x_25554 = let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0; print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0; print_acc_b_arg = print_acc_b_arg0; print_dpl_reg = print_dpl_reg0; @@ -796,7 +796,7 @@ let rec printing_params_rect_Type0 p h_mk_printing_params x_311 = print_dph_arg = print_dph_arg0; print_snd_arg = print_snd_arg0; print_pair_move = print_pair_move0; print_call_args = print_call_args0; print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } = - x_311 + x_25554 in h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0 print_acc_a_arg0 print_acc_b_arg0 print_dpl_reg0 print_dph_reg0 @@ -969,54 +969,54 @@ type 'string print_serialization_params = { print_succ : (__ -> 'string); (** val print_serialization_params_rect_Type4 : Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 print_serialization_params -> 'a2 **) -let rec print_serialization_params_rect_Type4 p h_mk_print_serialization_params x_340 = +let rec print_serialization_params_rect_Type4 p h_mk_print_serialization_params x_25583 = let { print_succ = print_succ0; print_code_point = print_code_point0 } = - x_340 + x_25583 in h_mk_print_serialization_params print_succ0 print_code_point0 (** val print_serialization_params_rect_Type5 : Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 print_serialization_params -> 'a2 **) -let rec print_serialization_params_rect_Type5 p h_mk_print_serialization_params x_342 = +let rec print_serialization_params_rect_Type5 p h_mk_print_serialization_params x_25585 = let { print_succ = print_succ0; print_code_point = print_code_point0 } = - x_342 + x_25585 in h_mk_print_serialization_params print_succ0 print_code_point0 (** val print_serialization_params_rect_Type3 : Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 print_serialization_params -> 'a2 **) -let rec print_serialization_params_rect_Type3 p h_mk_print_serialization_params x_344 = +let rec print_serialization_params_rect_Type3 p h_mk_print_serialization_params x_25587 = let { print_succ = print_succ0; print_code_point = print_code_point0 } = - x_344 + x_25587 in h_mk_print_serialization_params print_succ0 print_code_point0 (** val print_serialization_params_rect_Type2 : Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 print_serialization_params -> 'a2 **) -let rec print_serialization_params_rect_Type2 p h_mk_print_serialization_params x_346 = +let rec print_serialization_params_rect_Type2 p h_mk_print_serialization_params x_25589 = let { print_succ = print_succ0; print_code_point = print_code_point0 } = - x_346 + x_25589 in h_mk_print_serialization_params print_succ0 print_code_point0 (** val print_serialization_params_rect_Type1 : Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 print_serialization_params -> 'a2 **) -let rec print_serialization_params_rect_Type1 p h_mk_print_serialization_params x_348 = +let rec print_serialization_params_rect_Type1 p h_mk_print_serialization_params x_25591 = let { print_succ = print_succ0; print_code_point = print_code_point0 } = - x_348 + x_25591 in h_mk_print_serialization_params print_succ0 print_code_point0 (** val print_serialization_params_rect_Type0 : Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1 print_serialization_params -> 'a2 **) -let rec print_serialization_params_rect_Type0 p h_mk_print_serialization_params x_350 = +let rec print_serialization_params_rect_Type0 p h_mk_print_serialization_params x_25593 = let { print_succ = print_succ0; print_code_point = print_code_point0 } = - x_350 + x_25593 in h_mk_print_serialization_params print_succ0 print_code_point0 @@ -1094,9 +1094,9 @@ type ('string, 'statementT) code_iteration_params = { cip_print_serialization_pa Joint.params -> AST.ident List.list -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **) -let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_368 = +let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_25611 = let { cip_print_serialization_params = cip_print_serialization_params0; - fold_code = fold_code0; print_statementT = print_statementT0 } = x_368 + fold_code = fold_code0; print_statementT = print_statementT0 } = x_25611 in h_mk_code_iteration_params cip_print_serialization_params0 fold_code0 print_statementT0 @@ -1105,9 +1105,9 @@ let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_ Joint.params -> AST.ident List.list -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **) -let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_370 = +let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_25613 = let { cip_print_serialization_params = cip_print_serialization_params0; - fold_code = fold_code0; print_statementT = print_statementT0 } = x_370 + fold_code = fold_code0; print_statementT = print_statementT0 } = x_25613 in h_mk_code_iteration_params cip_print_serialization_params0 fold_code0 print_statementT0 @@ -1116,9 +1116,9 @@ let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_ Joint.params -> AST.ident List.list -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **) -let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_372 = +let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_25615 = let { cip_print_serialization_params = cip_print_serialization_params0; - fold_code = fold_code0; print_statementT = print_statementT0 } = x_372 + fold_code = fold_code0; print_statementT = print_statementT0 } = x_25615 in h_mk_code_iteration_params cip_print_serialization_params0 fold_code0 print_statementT0 @@ -1127,9 +1127,9 @@ let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_ Joint.params -> AST.ident List.list -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **) -let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_374 = +let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_25617 = let { cip_print_serialization_params = cip_print_serialization_params0; - fold_code = fold_code0; print_statementT = print_statementT0 } = x_374 + fold_code = fold_code0; print_statementT = print_statementT0 } = x_25617 in h_mk_code_iteration_params cip_print_serialization_params0 fold_code0 print_statementT0 @@ -1138,9 +1138,9 @@ let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_ Joint.params -> AST.ident List.list -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **) -let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_376 = +let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_25619 = let { cip_print_serialization_params = cip_print_serialization_params0; - fold_code = fold_code0; print_statementT = print_statementT0 } = x_376 + fold_code = fold_code0; print_statementT = print_statementT0 } = x_25619 in h_mk_code_iteration_params cip_print_serialization_params0 fold_code0 print_statementT0 @@ -1149,9 +1149,9 @@ let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_ Joint.params -> AST.ident List.list -> ('a1 print_serialization_params -> (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1) -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **) -let rec code_iteration_params_rect_Type0 p globals h_mk_code_iteration_params x_378 = +let rec code_iteration_params_rect_Type0 p globals h_mk_code_iteration_params x_25621 = let { cip_print_serialization_params = cip_print_serialization_params0; - fold_code = fold_code0; print_statementT = print_statementT0 } = x_378 + fold_code = fold_code0; print_statementT = print_statementT0 } = x_25621 in h_mk_code_iteration_params cip_print_serialization_params0 fold_code0 print_statementT0 @@ -1165,11 +1165,11 @@ let rec cip_print_serialization_params p globals xxx = (** val fold_code0 : Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params -> (__ -> 'a2 -> 'a3 -> 'a3) -> __ -> __ -> 'a3 -> 'a3 **) -let rec fold_code0 p globals xxx x_393 x_394 x_395 x_396 = +let rec fold_code0 p globals xxx x_25636 x_25637 x_25638 x_25639 = (let { cip_print_serialization_params = x; fold_code = yyy; print_statementT = x0 } = xxx in - Obj.magic yyy) __ x_393 x_394 x_395 x_396 + Obj.magic yyy) __ x_25636 x_25637 x_25638 x_25639 (** val print_statementT : Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params @@ -1246,8 +1246,8 @@ let rec visit_graph next f b n m = function (match pm_choose_with_pref m n with | Types.None -> b | Types.Some res -> - let { Types.fst = eta2; Types.snd = m' } = res in - let { Types.fst = pos; Types.snd = a } = eta2 in + let { Types.fst = eta32074; Types.snd = m' } = res in + let { Types.fst = pos; Types.snd = a } = eta32074 in visit_graph next f (f pos a b) (next a) m' y) (** val print_list : diff --git a/extracted/lINToASM.ml b/extracted/lINToASM.ml index 770789a..dc2b40b 100644 --- a/extracted/lINToASM.ml +++ b/extracted/lINToASM.ml @@ -139,10 +139,10 @@ type aSM_universe = { id_univ : Identifiers.universe; (Identifiers.universe -> AST.ident -> ASM.identifier Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **) -let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_21483 = +let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_588 = let { id_univ = id_univ0; current_funct = current_funct0; ident_map = ident_map0; label_map = label_map0; fresh_cost_label = - fresh_cost_label0 } = x_21483 + fresh_cost_label0 } = x_588 in h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 fresh_cost_label0 @@ -151,10 +151,10 @@ let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_21483 = (Identifiers.universe -> AST.ident -> ASM.identifier Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **) -let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_21485 = +let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_590 = let { id_univ = id_univ0; current_funct = current_funct0; ident_map = ident_map0; label_map = label_map0; fresh_cost_label = - fresh_cost_label0 } = x_21485 + fresh_cost_label0 } = x_590 in h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 fresh_cost_label0 @@ -163,10 +163,10 @@ let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_21485 = (Identifiers.universe -> AST.ident -> ASM.identifier Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **) -let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_21487 = +let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_592 = let { id_univ = id_univ0; current_funct = current_funct0; ident_map = ident_map0; label_map = label_map0; fresh_cost_label = - fresh_cost_label0 } = x_21487 + fresh_cost_label0 } = x_592 in h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 fresh_cost_label0 @@ -175,10 +175,10 @@ let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_21487 = (Identifiers.universe -> AST.ident -> ASM.identifier Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **) -let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_21489 = +let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_594 = let { id_univ = id_univ0; current_funct = current_funct0; ident_map = ident_map0; label_map = label_map0; fresh_cost_label = - fresh_cost_label0 } = x_21489 + fresh_cost_label0 } = x_594 in h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 fresh_cost_label0 @@ -187,10 +187,10 @@ let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_21489 = (Identifiers.universe -> AST.ident -> ASM.identifier Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **) -let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_21491 = +let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_596 = let { id_univ = id_univ0; current_funct = current_funct0; ident_map = ident_map0; label_map = label_map0; fresh_cost_label = - fresh_cost_label0 } = x_21491 + fresh_cost_label0 } = x_596 in h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 fresh_cost_label0 @@ -199,10 +199,10 @@ let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_21491 = (Identifiers.universe -> AST.ident -> ASM.identifier Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **) -let rec aSM_universe_rect_Type0 h_mk_ASM_universe x_21493 = +let rec aSM_universe_rect_Type0 h_mk_ASM_universe x_598 = let { id_univ = id_univ0; current_funct = current_funct0; ident_map = ident_map0; label_map = label_map0; fresh_cost_label = - fresh_cost_label0 } = x_21493 + fresh_cost_label0 } = x_598 in h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 fresh_cost_label0 @@ -302,7 +302,7 @@ let identifier_of_label l = Identifiers.lookup_def PreIdentifiers.SymbolTag u.label_map current (Identifiers.empty_map PreIdentifiers.LabelTag) in - let { Types.fst = eta28616; Types.snd = lmap0 } = + let { Types.fst = eta2825; Types.snd = lmap0 } = match Identifiers.lookup PreIdentifiers.LabelTag lmap l with | Types.None -> let { Types.fst = id; Types.snd = univ } = @@ -314,7 +314,7 @@ let identifier_of_label l = { Types.fst = { Types.fst = id; Types.snd = u.id_univ }; Types.snd = lmap } in - let { Types.fst = id; Types.snd = univ } = eta28616 in + let { Types.fst = id; Types.snd = univ } = eta2825 in { Types.fst = { id_univ = univ; current_funct = current; ident_map = u.ident_map; label_map = (Identifiers.add PreIdentifiers.SymbolTag u.label_map current lmap0); @@ -1050,9 +1050,9 @@ type init_mutable = { virtual_dptr : (ASM.identifier, Z.z) Types.prod; ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod -> ASM.labelled_instruction List.list List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **) -let rec init_mutable_rect_Type4 h_mk_init_mutable x_21509 = +let rec init_mutable_rect_Type4 h_mk_init_mutable x_614 = let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; - built_code = built_code0; built_preamble = built_preamble0 } = x_21509 + built_code = built_code0; built_preamble = built_preamble0 } = x_614 in h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 @@ -1060,9 +1060,9 @@ let rec init_mutable_rect_Type4 h_mk_init_mutable x_21509 = ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod -> ASM.labelled_instruction List.list List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **) -let rec init_mutable_rect_Type5 h_mk_init_mutable x_21511 = +let rec init_mutable_rect_Type5 h_mk_init_mutable x_616 = let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; - built_code = built_code0; built_preamble = built_preamble0 } = x_21511 + built_code = built_code0; built_preamble = built_preamble0 } = x_616 in h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 @@ -1070,9 +1070,9 @@ let rec init_mutable_rect_Type5 h_mk_init_mutable x_21511 = ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod -> ASM.labelled_instruction List.list List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **) -let rec init_mutable_rect_Type3 h_mk_init_mutable x_21513 = +let rec init_mutable_rect_Type3 h_mk_init_mutable x_618 = let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; - built_code = built_code0; built_preamble = built_preamble0 } = x_21513 + built_code = built_code0; built_preamble = built_preamble0 } = x_618 in h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 @@ -1080,9 +1080,9 @@ let rec init_mutable_rect_Type3 h_mk_init_mutable x_21513 = ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod -> ASM.labelled_instruction List.list List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **) -let rec init_mutable_rect_Type2 h_mk_init_mutable x_21515 = +let rec init_mutable_rect_Type2 h_mk_init_mutable x_620 = let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; - built_code = built_code0; built_preamble = built_preamble0 } = x_21515 + built_code = built_code0; built_preamble = built_preamble0 } = x_620 in h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 @@ -1090,9 +1090,9 @@ let rec init_mutable_rect_Type2 h_mk_init_mutable x_21515 = ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod -> ASM.labelled_instruction List.list List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **) -let rec init_mutable_rect_Type1 h_mk_init_mutable x_21517 = +let rec init_mutable_rect_Type1 h_mk_init_mutable x_622 = let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; - built_code = built_code0; built_preamble = built_preamble0 } = x_21517 + built_code = built_code0; built_preamble = built_preamble0 } = x_622 in h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 @@ -1100,9 +1100,9 @@ let rec init_mutable_rect_Type1 h_mk_init_mutable x_21517 = ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod -> ASM.labelled_instruction List.list List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **) -let rec init_mutable_rect_Type0 h_mk_init_mutable x_21519 = +let rec init_mutable_rect_Type0 h_mk_init_mutable x_624 = let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; - built_code = built_code0; built_preamble = built_preamble0 } = x_21519 + built_code = built_code0; built_preamble = built_preamble0 } = x_624 in h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 @@ -1303,8 +1303,8 @@ let do_store_init_data m_mut data = Monad.smax_def__o__monad **) let do_store_global m_mut id_reg_data = Monad.m_bind0 (Monad.smax_def State.state_monad) m_mut (fun mut -> - let { Types.fst = eta28633; Types.snd = data } = id_reg_data in - let { Types.fst = id; Types.snd = reg } = eta28633 in + let { Types.fst = eta2842; Types.snd = data } = id_reg_data in + let { Types.fst = id; Types.snd = reg } = eta2842 in Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_ident id) (fun id0 -> let mut0 = { virtual_dptr = { Types.fst = id0; Types.snd = Z.OZ }; diff --git a/extracted/policy.ml b/extracted/policy.ml index 194fc73..e13f645 100644 --- a/extracted/policy.ml +++ b/extracted/policy.ml @@ -94,7 +94,7 @@ open PolicyStep let rec jump_expansion_internal program n = let labels = PolicyFront.create_label_map (Types.pi1 program) in let rec aux res = -prerr_endline "JEI_start"; +prerr_endline "JEI"; let { Types.fst = no_ch; Types.snd = z } = res in match z with | Types.None -> @@ -108,10 +108,11 @@ prerr_endline "JEI_start"; (PolicyStep.jump_expansion_step program (Types.pi1 labels) op)) in +prerr_endline "JES"; +let init =(PolicyFront.jump_expansion_start program (Types.pi1 labels)) in aux { Types.fst = Bool.False; Types.snd = - (Types.pi1 - (PolicyFront.jump_expansion_start program (Types.pi1 labels))) } + (Types.pi1 init) } (* (match n with | Nat.O -> @@ -180,6 +181,7 @@ let jump_expansion' program = (Nat.S Nat.O)))))))))))))))) ppc x.Types.snd { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst in +(*prerr_endline "Z3";*) Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) pc); Types.snd = (fun ppc -> diff --git a/extracted/policy.mli b/extracted/policy.mli index 3d8eb7f..6794a52 100644 --- a/extracted/policy.mli +++ b/extracted/policy.mli @@ -1,27 +1,11 @@ open Preamble -open Assembly - open Status -open Fetch - open BitVectorTrie open String -open Exp - -open Arithmetic - -open Vector - -open FoldStuff - -open BitVector - -open Extranat - open Integers open AST @@ -40,7 +24,17 @@ open PreIdentifiers open Errors -open Extralib +open Lists + +open Positive + +open Identifiers + +open CostLabel + +open ASM + +open Exp open Setoids @@ -48,6 +42,20 @@ open Monad open Option +open Extranat + +open Vector + +open FoldStuff + +open BitVector + +open Arithmetic + +open Fetch + +open Assembly + open Div_and_mod open Jmeq @@ -56,17 +64,13 @@ open Russell open Util -open List - -open Lists - open Bool open Relations open Nat -open Positive +open List open Hints_declaration @@ -78,11 +82,7 @@ open Logic open Types -open Identifiers - -open CostLabel - -open ASM +open Extralib open PolicyFront diff --git a/extracted/policyFront.ml b/extracted/policyFront.ml index 1b8ccc5..66d8985 100644 --- a/extracted/policyFront.ml +++ b/extracted/policyFront.ml @@ -1,86 +1,86 @@ open Preamble -open BitVectorTrie +open Div_and_mod -open String +open Jmeq -open Exp +open Russell -open Arithmetic +open Util -open Vector +open Bool -open FoldStuff +open Relations -open BitVector +open Nat -open Extranat +open List -open Integers +open Hints_declaration -open AST +open Core_notation -open LabelledObjects +open Pts -open Proper +open Logic -open PositiveMap +open Types -open Deqsets +open Extralib -open ErrorMessages +open Status -open PreIdentifiers +open BitVectorTrie -open Errors +open String -open Extralib +open Integers -open Setoids +open AST -open Monad +open LabelledObjects -open Option +open Proper -open Div_and_mod +open PositiveMap -open Jmeq +open Deqsets -open Russell +open ErrorMessages -open Util +open PreIdentifiers -open List +open Errors open Lists -open Bool +open Positive -open Relations +open Identifiers -open Nat +open CostLabel -open Positive +open ASM -open Hints_declaration +open Exp -open Core_notation +open Setoids -open Pts +open Monad -open Logic +open Option -open Types +open Extranat -open Identifiers +open Vector -open CostLabel +open FoldStuff -open ASM +open BitVector -open Fetch +open Arithmetic -open Status +open Fetch open Assembly @@ -656,34 +656,46 @@ let jump_expansion_step_instruction labels old_sigma inc_sigma ppc i = ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map -> ppc_pc_map Types.option Types.sig0 **) let jump_expansion_start program labels = - let final_policy = - FoldStuff.foldl_strong (Types.pi1 program) (fun prefix x tl _ p -> - let { Types.fst = pc; Types.snd = sigma } = Types.pi1 p in - let { Types.fst = label; Types.snd = instr } = x in - let isize = instruction_size_jmplen Assembly.Short_jump instr in - { Types.fst = (Nat.plus pc isize); Types.snd = - (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - Nat.O)))))))))))))))) - (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S (List.length prefix))) - { Types.fst = (Nat.plus pc isize); Types.snd = Assembly.Short_jump } - sigma) }) { Types.fst = Nat.O; Types.snd = - (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - Nat.O)))))))))))))))) - (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S Nat.O)))))))))))))))) Nat.O) { Types.fst = Nat.O; - Types.snd = Assembly.Short_jump } (BitVectorTrie.Stub (Nat.S (Nat.S - (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } - in - (match Util.gtb (Types.pi1 final_policy).Types.fst + (let { Types.fst = ignore; Types.snd = final_policy } = + Types.pi1 + (FoldStuff.foldl_strong (Types.pi1 program) + (fun prefix x tl _ acc_pol -> + (let { Types.fst = acc; Types.snd = p } = Types.pi1 acc_pol in + (fun _ -> + let { Types.fst = pc; Types.snd = sigma } = p in + let { Types.fst = label; Types.snd = instr } = x in + let isize = instruction_size_jmplen Assembly.Short_jump instr in + let sacc = + Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S Nat.O)))))))))))))))) acc + in + { Types.fst = sacc; Types.snd = { Types.fst = (Nat.plus pc isize); + Types.snd = + (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S Nat.O)))))))))))))))) sacc { Types.fst = + (Nat.plus pc isize); Types.snd = Assembly.Short_jump } sigma) } })) + __) { Types.fst = + (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + Nat.O))))))))))))))))); Types.snd = { Types.fst = Nat.O; + Types.snd = + (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S Nat.O)))))))))))))))) + (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S (Nat.S Nat.O)))))))))))))))) Nat.O) { Types.fst = Nat.O; + Types.snd = Assembly.Short_jump } (BitVectorTrie.Stub (Nat.S + (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } }) + in + (fun _ -> + (match Util.gtb final_policy.Types.fst (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))) with | Bool.True -> (fun _ -> Types.None) - | Bool.False -> (fun _ -> Types.Some (Types.pi1 final_policy))) __ + | Bool.False -> (fun _ -> Types.Some final_policy)) __)) __ diff --git a/extracted/policyFront.mli b/extracted/policyFront.mli index d2a2c58..814f985 100644 --- a/extracted/policyFront.mli +++ b/extracted/policyFront.mli @@ -1,86 +1,86 @@ open Preamble -open BitVectorTrie +open Div_and_mod -open String +open Jmeq -open Exp +open Russell -open Arithmetic +open Util -open Vector +open Bool -open FoldStuff +open Relations -open BitVector +open Nat -open Extranat +open List -open Integers +open Hints_declaration -open AST +open Core_notation -open LabelledObjects +open Pts -open Proper +open Logic -open PositiveMap +open Types -open Deqsets +open Extralib -open ErrorMessages +open Status -open PreIdentifiers +open BitVectorTrie -open Errors +open String -open Extralib +open Integers -open Setoids +open AST -open Monad +open LabelledObjects -open Option +open Proper -open Div_and_mod +open PositiveMap -open Jmeq +open Deqsets -open Russell +open ErrorMessages -open Util +open PreIdentifiers -open List +open Errors open Lists -open Bool +open Positive -open Relations +open Identifiers -open Nat +open CostLabel -open Positive +open ASM -open Hints_declaration +open Exp -open Core_notation +open Setoids -open Pts +open Monad -open Logic +open Option -open Types +open Extranat -open Identifiers +open Vector -open CostLabel +open FoldStuff -open ASM +open BitVector -open Fetch +open Arithmetic -open Status +open Fetch open Assembly diff --git a/extracted/policyStep.ml b/extracted/policyStep.ml index ddc45e9..3d66283 100644 --- a/extracted/policyStep.ml +++ b/extracted/policyStep.ml @@ -1,27 +1,11 @@ open Preamble -open Assembly - open Status -open Fetch - open BitVectorTrie open String -open Exp - -open Arithmetic - -open Vector - -open FoldStuff - -open BitVector - -open Extranat - open Integers open AST @@ -40,7 +24,17 @@ open PreIdentifiers open Errors -open Extralib +open Lists + +open Positive + +open Identifiers + +open CostLabel + +open ASM + +open Exp open Setoids @@ -48,6 +42,20 @@ open Monad open Option +open Extranat + +open Vector + +open FoldStuff + +open BitVector + +open Arithmetic + +open Fetch + +open Assembly + open Div_and_mod open Jmeq @@ -56,17 +64,13 @@ open Russell open Util -open List - -open Lists - open Bool open Relations open Nat -open Positive +open List open Hints_declaration @@ -78,11 +82,7 @@ open Logic open Types -open Identifiers - -open CostLabel - -open ASM +open Extralib open PolicyFront @@ -91,41 +91,49 @@ open PolicyFront Types.sig0 -> PolicyFront.ppc_pc_map Types.sig0 -> (Bool.bool, PolicyFront.ppc_pc_map Types.option) Types.prod Types.sig0 **) let jump_expansion_step program labels old_sigma = - (let { Types.fst = final_added; Types.snd = final_policy } = + (let { Types.fst = ignore; Types.snd = res } = Types.pi1 - (FoldStuff.foldl_strong (Types.pi1 program) (fun prefix x tl _ acc -> - (let { Types.fst = inc_added; Types.snd = inc_pc_sigma } = - Types.pi1 acc + (FoldStuff.foldl_strong (Types.pi1 program) + (fun prefix x tl _ prefixlens_acc -> + (let { Types.fst = prefixlens; Types.snd = acc } = + Types.pi1 prefixlens_acc + in + (fun _ -> + (let { Types.fst = prefixlen; Types.snd = bvprefixlen } = prefixlens in (fun _ -> + let bvSprefixlen = + Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S Nat.O)))))))))))))))) bvprefixlen + in + (let { Types.fst = inc_added; Types.snd = inc_pc_sigma } = acc in + (fun _ -> (let { Types.fst = label; Types.snd = instr } = x in (fun _ -> let add_instr = match instr with | ASM.Instruction i -> PolicyFront.jump_expansion_step_instruction (Types.pi1 labels) - (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) i + (Types.pi1 old_sigma) inc_pc_sigma prefixlen i | ASM.Comment x0 -> Types.None | ASM.Cost x0 -> Types.None | ASM.Jmp j -> Types.Some (PolicyFront.select_jump_length (Types.pi1 labels) - (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) j) + (Types.pi1 old_sigma) inc_pc_sigma prefixlen j) | ASM.Jnz (x0, x1, x2) -> Types.None | ASM.Call c -> Types.Some (PolicyFront.select_call_length (Types.pi1 labels) - (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) c) + (Types.pi1 old_sigma) inc_pc_sigma prefixlen c) | ASM.Mov (x0, x1, x2) -> Types.None in let { Types.fst = inc_pc; Types.snd = inc_sigma } = inc_pc_sigma in let old_length = (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S Nat.O)))))))))))))))) - (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S Nat.O)))))))))))))))) (List.length prefix)) + (Nat.S Nat.O)))))))))))))))) bvprefixlen (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.snd in @@ -151,34 +159,31 @@ let jump_expansion_step program labels old_sigma = let old_Slength = (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S Nat.O)))))))))))))))) - (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S - (List.length prefix))) (Types.pi1 old_sigma).Types.snd - { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.snd + (Nat.S Nat.O)))))))))))))))) bvSprefixlen + (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd = + Assembly.Short_jump }).Types.snd in let updated_sigma = BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S Nat.O)))))))))))))))) - (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S - (List.length prefix))) { Types.fst = (Nat.plus inc_pc isize); - Types.snd = old_Slength } + (Nat.S Nat.O)))))))))))))))) bvSprefixlen { Types.fst = + (Nat.plus inc_pc isize); Types.snd = old_Slength } (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S Nat.O)))))))))))))))) - (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) - (List.length prefix)) { Types.fst = inc_pc; Types.snd = - new_length } inc_sigma) + (Nat.S Nat.O)))))))))))))))) bvprefixlen { Types.fst = inc_pc; + Types.snd = new_length } inc_sigma) in + { Types.fst = { Types.fst = (Nat.S prefixlen); Types.snd = + (Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S Nat.O)))))))))))))))) bvprefixlen) }; Types.snd = { Types.fst = new_added; Types.snd = { Types.fst = - (Nat.plus inc_pc isize); Types.snd = updated_sigma } })) __)) __) - { Types.fst = Nat.O; Types.snd = { Types.fst = Nat.O; Types.snd = + (Nat.plus inc_pc isize); Types.snd = updated_sigma } } })) __)) __)) + __)) __) { Types.fst = { Types.fst = Nat.O; Types.snd = + (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S + Nat.O))))))))))))))))) }; Types.snd = { Types.fst = Nat.O; + Types.snd = { Types.fst = Nat.O; Types.snd = (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) @@ -195,9 +200,11 @@ let jump_expansion_step program labels old_sigma = (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.snd } (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S - (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } }) + (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } } }) in (fun _ -> + (let { Types.fst = final_added; Types.snd = final_policy } = res in + (fun _ -> (match Util.gtb final_policy.Types.fst (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S @@ -207,5 +214,5 @@ let jump_expansion_step program labels old_sigma = Types.None }) | Bool.False -> (fun _ -> { Types.fst = (Nat.eqb final_added Nat.O); Types.snd = - (Types.Some final_policy) })) __)) __ + (Types.Some final_policy) })) __)) __)) __ diff --git a/extracted/policyStep.mli b/extracted/policyStep.mli index 1e23bab..6f3ef49 100644 --- a/extracted/policyStep.mli +++ b/extracted/policyStep.mli @@ -1,27 +1,11 @@ open Preamble -open Assembly - open Status -open Fetch - open BitVectorTrie open String -open Exp - -open Arithmetic - -open Vector - -open FoldStuff - -open BitVector - -open Extranat - open Integers open AST @@ -40,7 +24,17 @@ open PreIdentifiers open Errors -open Extralib +open Lists + +open Positive + +open Identifiers + +open CostLabel + +open ASM + +open Exp open Setoids @@ -48,6 +42,20 @@ open Monad open Option +open Extranat + +open Vector + +open FoldStuff + +open BitVector + +open Arithmetic + +open Fetch + +open Assembly + open Div_and_mod open Jmeq @@ -56,17 +64,13 @@ open Russell open Util -open List - -open Lists - open Bool open Relations open Nat -open Positive +open List open Hints_declaration @@ -78,11 +82,7 @@ open Logic open Types -open Identifiers - -open CostLabel - -open ASM +open Extralib open PolicyFront diff --git a/extracted/semantics.ml b/extracted/semantics.ml index 221a22e..c49e25f 100644 --- a/extracted/semantics.ml +++ b/extracted/semantics.ml @@ -14,12 +14,12 @@ open Interpret open ASMCosts -open Assembly - open Status open Fetch +open Assembly + open PolicyFront open PolicyStep @@ -315,38 +315,38 @@ type preclassified_system_pass = (** val preclassified_system_pass_rect_Type4 : Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) -> preclassified_system_pass -> 'a1 **) -let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_25220 = - let pcs_pcs = x_25220 in h_mk_preclassified_system_pass pcs_pcs __ +let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_3 = + let pcs_pcs = x_3 in h_mk_preclassified_system_pass pcs_pcs __ (** val preclassified_system_pass_rect_Type5 : Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) -> preclassified_system_pass -> 'a1 **) -let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_25222 = - let pcs_pcs = x_25222 in h_mk_preclassified_system_pass pcs_pcs __ +let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_5 = + let pcs_pcs = x_5 in h_mk_preclassified_system_pass pcs_pcs __ (** val preclassified_system_pass_rect_Type3 : Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) -> preclassified_system_pass -> 'a1 **) -let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_25224 = - let pcs_pcs = x_25224 in h_mk_preclassified_system_pass pcs_pcs __ +let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_7 = + let pcs_pcs = x_7 in h_mk_preclassified_system_pass pcs_pcs __ (** val preclassified_system_pass_rect_Type2 : Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) -> preclassified_system_pass -> 'a1 **) -let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_25226 = - let pcs_pcs = x_25226 in h_mk_preclassified_system_pass pcs_pcs __ +let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_9 = + let pcs_pcs = x_9 in h_mk_preclassified_system_pass pcs_pcs __ (** val preclassified_system_pass_rect_Type1 : Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) -> preclassified_system_pass -> 'a1 **) -let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_25228 = - let pcs_pcs = x_25228 in h_mk_preclassified_system_pass pcs_pcs __ +let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_11 = + let pcs_pcs = x_11 in h_mk_preclassified_system_pass pcs_pcs __ (** val preclassified_system_pass_rect_Type0 : Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) -> preclassified_system_pass -> 'a1 **) -let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_25230 = - let pcs_pcs = x_25230 in h_mk_preclassified_system_pass pcs_pcs __ +let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_13 = + let pcs_pcs = x_13 in h_mk_preclassified_system_pass pcs_pcs __ (** val pcs_pcs : Compiler.pass -> preclassified_system_pass -> @@ -433,8 +433,8 @@ let preclassified_system_of_pass = function Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics) | Compiler.Assembly_pass -> (fun prog -> - let { Types.fst = eta32049; Types.snd = policy } = Obj.magic prog in - let { Types.fst = code; Types.snd = sigma } = eta32049 in + let { Types.fst = eta4; Types.snd = policy } = Obj.magic prog in + let { Types.fst = code; Types.snd = sigma } = eta4 in Interpret2.aSM_preclassified_system code sigma policy) | Compiler.Object_code_pass -> (fun prog -> Interpret2.oC_preclassified_system (Obj.magic prog)) diff --git a/extracted/semantics.mli b/extracted/semantics.mli index 68973c5..5957a12 100644 --- a/extracted/semantics.mli +++ b/extracted/semantics.mli @@ -14,12 +14,12 @@ open Interpret open ASMCosts -open Assembly - open Status open Fetch +open Assembly + open PolicyFront open PolicyStep diff --git a/extracted/simplifyCasts.ml b/extracted/simplifyCasts.ml index dd7afae..dc6f2bc 100644 --- a/extracted/simplifyCasts.ml +++ b/extracted/simplifyCasts.ml @@ -356,16 +356,16 @@ let rec simplify_expr e target_sz target_sg = (match TypeComparison.assert_type_eq (Csyntax.typeof lhs) (Csyntax.typeof rhs) with | Errors.OK _ -> - (let eta2011 = simplify_expr lhs target_sz target_sg in + (let eta2033 = simplify_expr lhs target_sz target_sg in (fun _ -> (let { Types.fst = desired_type_lhs; Types.snd = lhs1 } = - eta2011 + eta2033 in (fun _ -> - (let eta2010 = simplify_expr rhs target_sz target_sg in + (let eta2032 = simplify_expr rhs target_sz target_sg in (fun _ -> (let { Types.fst = desired_type_rhs; Types.snd = - rhs1 } = eta2010 + rhs1 } = eta2032 in (fun _ -> (match Bool.andb desired_type_lhs desired_type_rhs with @@ -418,10 +418,10 @@ let rec simplify_expr e target_sz target_sg = (match necessary_conditions cast_sz cast_sg target_sz target_sg with | Bool.True -> (fun _ -> - (let eta2013 = simplify_expr castee target_sz target_sg in + (let eta2035 = simplify_expr castee target_sz target_sg in (fun _ -> (let { Types.fst = desired_type; Types.snd = castee1 } = - eta2013 + eta2035 in (fun _ -> (match desired_type with @@ -430,11 +430,11 @@ let rec simplify_expr e target_sz target_sg = castee1 }) | Bool.False -> (fun _ -> - (let eta2012 = simplify_expr castee cast_sz cast_sg + (let eta2034 = simplify_expr castee cast_sz cast_sg in (fun _ -> (let { Types.fst = desired_type2; Types.snd = - castee2 } = eta2012 + castee2 } = eta2034 in (fun _ -> (match desired_type2 with @@ -448,10 +448,10 @@ let rec simplify_expr e target_sz target_sg = __)) __)) __) | Bool.False -> (fun _ -> - (let eta2014 = simplify_expr castee cast_sz cast_sg in + (let eta2036 = simplify_expr castee cast_sz cast_sg in (fun _ -> (let { Types.fst = desired_type2; Types.snd = - castee2 } = eta2014 + castee2 } = eta2036 in (fun _ -> (match desired_type2 with @@ -505,16 +505,16 @@ let rec simplify_expr e target_sz target_sg = (match TypeComparison.assert_type_eq (Csyntax.typeof iftrue) (Csyntax.typeof iffalse) with | Errors.OK _ -> - (let eta2016 = simplify_expr iftrue target_sz target_sg in + (let eta2038 = simplify_expr iftrue target_sz target_sg in (fun _ -> (let { Types.fst = desired_true; Types.snd = iftrue1 } = - eta2016 + eta2038 in (fun _ -> - (let eta2015 = simplify_expr iffalse target_sz target_sg in + (let eta2037 = simplify_expr iffalse target_sz target_sg in (fun _ -> (let { Types.fst = desired_false; Types.snd = iffalse1 } = - eta2015 + eta2037 in (fun _ -> (match Bool.andb desired_true desired_false with @@ -572,9 +572,9 @@ let rec simplify_expr e target_sz target_sg = (fun _ -> match TypeComparison.type_eq_dec ty (Csyntax.typeof e1) with | Types.Inl _ -> - (let eta2017 = simplify_expr e1 target_sz target_sg in + (let eta2039 = simplify_expr e1 target_sz target_sg in (fun _ -> - (let { Types.fst = desired_type; Types.snd = e2 } = eta2017 in + (let { Types.fst = desired_type; Types.snd = e2 } = eta2039 in (fun _ -> { Types.fst = desired_type; Types.snd = (Csyntax.Expr ((Csyntax.Ecost (l, e2)), (Csyntax.typeof e2))) })) __)) __ | Types.Inr _ -> @@ -615,9 +615,9 @@ and simplify_inside e = | Csyntax.Tvoid -> (fun _ -> e) | Csyntax.Tint (cast_sz, cast_sg) -> (fun _ -> - (let eta2018 = simplify_expr castee cast_sz cast_sg in + (let eta2040 = simplify_expr castee cast_sz cast_sg in (fun _ -> - (let { Types.fst = success; Types.snd = castee1 } = eta2018 + (let { Types.fst = success; Types.snd = castee1 } = eta2040 in (fun _ -> (match success with diff --git a/extracted/status.ml b/extracted/status.ml index 7a08f70..2abe567 100644 --- a/extracted/status.ml +++ b/extracted/status.ml @@ -88,43 +88,43 @@ type serialBufferType = (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) -> serialBufferType -> 'a1 **) let rec serialBufferType_rect_Type4 h_Eight h_Nine = function -| Eight x_21722 -> h_Eight x_21722 -| Nine (x_21724, x_21723) -> h_Nine x_21724 x_21723 +| Eight x_8 -> h_Eight x_8 +| Nine (x_10, x_9) -> h_Nine x_10 x_9 (** val serialBufferType_rect_Type5 : (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) -> serialBufferType -> 'a1 **) let rec serialBufferType_rect_Type5 h_Eight h_Nine = function -| Eight x_21728 -> h_Eight x_21728 -| Nine (x_21730, x_21729) -> h_Nine x_21730 x_21729 +| Eight x_14 -> h_Eight x_14 +| Nine (x_16, x_15) -> h_Nine x_16 x_15 (** val serialBufferType_rect_Type3 : (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) -> serialBufferType -> 'a1 **) let rec serialBufferType_rect_Type3 h_Eight h_Nine = function -| Eight x_21734 -> h_Eight x_21734 -| Nine (x_21736, x_21735) -> h_Nine x_21736 x_21735 +| Eight x_20 -> h_Eight x_20 +| Nine (x_22, x_21) -> h_Nine x_22 x_21 (** val serialBufferType_rect_Type2 : (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) -> serialBufferType -> 'a1 **) let rec serialBufferType_rect_Type2 h_Eight h_Nine = function -| Eight x_21740 -> h_Eight x_21740 -| Nine (x_21742, x_21741) -> h_Nine x_21742 x_21741 +| Eight x_26 -> h_Eight x_26 +| Nine (x_28, x_27) -> h_Nine x_28 x_27 (** val serialBufferType_rect_Type1 : (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) -> serialBufferType -> 'a1 **) let rec serialBufferType_rect_Type1 h_Eight h_Nine = function -| Eight x_21746 -> h_Eight x_21746 -| Nine (x_21748, x_21747) -> h_Nine x_21748 x_21747 +| Eight x_32 -> h_Eight x_32 +| Nine (x_34, x_33) -> h_Nine x_34 x_33 (** val serialBufferType_rect_Type0 : (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) -> serialBufferType -> 'a1 **) let rec serialBufferType_rect_Type0 h_Eight h_Nine = function -| Eight x_21752 -> h_Eight x_21752 -| Nine (x_21754, x_21753) -> h_Nine x_21754 x_21753 +| Eight x_38 -> h_Eight x_38 +| Nine (x_40, x_39) -> h_Nine x_40 x_39 (** val serialBufferType_inv_rect_Type4 : serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> @@ -181,49 +181,49 @@ type lineType = (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType -> 'a1) -> lineType -> 'a1 **) let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function -| P1 x_21801 -> h_P1 x_21801 -| P3 x_21802 -> h_P3 x_21802 -| SerialBuffer x_21803 -> h_SerialBuffer x_21803 +| P1 x_87 -> h_P1 x_87 +| P3 x_88 -> h_P3 x_88 +| SerialBuffer x_89 -> h_SerialBuffer x_89 (** val lineType_rect_Type5 : (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType -> 'a1) -> lineType -> 'a1 **) let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function -| P1 x_21808 -> h_P1 x_21808 -| P3 x_21809 -> h_P3 x_21809 -| SerialBuffer x_21810 -> h_SerialBuffer x_21810 +| P1 x_94 -> h_P1 x_94 +| P3 x_95 -> h_P3 x_95 +| SerialBuffer x_96 -> h_SerialBuffer x_96 (** val lineType_rect_Type3 : (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType -> 'a1) -> lineType -> 'a1 **) let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function -| P1 x_21815 -> h_P1 x_21815 -| P3 x_21816 -> h_P3 x_21816 -| SerialBuffer x_21817 -> h_SerialBuffer x_21817 +| P1 x_101 -> h_P1 x_101 +| P3 x_102 -> h_P3 x_102 +| SerialBuffer x_103 -> h_SerialBuffer x_103 (** val lineType_rect_Type2 : (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType -> 'a1) -> lineType -> 'a1 **) let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function -| P1 x_21822 -> h_P1 x_21822 -| P3 x_21823 -> h_P3 x_21823 -| SerialBuffer x_21824 -> h_SerialBuffer x_21824 +| P1 x_108 -> h_P1 x_108 +| P3 x_109 -> h_P3 x_109 +| SerialBuffer x_110 -> h_SerialBuffer x_110 (** val lineType_rect_Type1 : (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType -> 'a1) -> lineType -> 'a1 **) let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function -| P1 x_21829 -> h_P1 x_21829 -| P3 x_21830 -> h_P3 x_21830 -| SerialBuffer x_21831 -> h_SerialBuffer x_21831 +| P1 x_115 -> h_P1 x_115 +| P3 x_116 -> h_P3 x_116 +| SerialBuffer x_117 -> h_SerialBuffer x_117 (** val lineType_rect_Type0 : (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType -> 'a1) -> lineType -> 'a1 **) let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function -| P1 x_21836 -> h_P1 x_21836 -| P3 x_21837 -> h_P3 x_21837 -| SerialBuffer x_21838 -> h_SerialBuffer x_21838 +| P1 x_122 -> h_P1 x_122 +| P3 x_123 -> h_P3 x_123 +| SerialBuffer x_124 -> h_SerialBuffer x_124 (** val lineType_inv_rect_Type4 : lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> @@ -730,13 +730,13 @@ type 'm preStatus = { low_internal_ram : BitVector.byte -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1 preStatus -> 'a2 **) -let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_22224 = +let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_510 = let { low_internal_ram = low_internal_ram0; high_internal_ram = high_internal_ram0; external_ram = external_ram0; program_counter = program_counter0; special_function_registers_8051 = special_function_registers_8053; special_function_registers_8052 = special_function_registers_8054; p1_latch = p1_latch0; p3_latch = - p3_latch0; clock = clock0 } = x_22224 + p3_latch0; clock = clock0 } = x_510 in h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 program_counter0 special_function_registers_8053 @@ -748,13 +748,13 @@ let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_22224 = -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1 preStatus -> 'a2 **) -let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_22226 = +let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_512 = let { low_internal_ram = low_internal_ram0; high_internal_ram = high_internal_ram0; external_ram = external_ram0; program_counter = program_counter0; special_function_registers_8051 = special_function_registers_8053; special_function_registers_8052 = special_function_registers_8054; p1_latch = p1_latch0; p3_latch = - p3_latch0; clock = clock0 } = x_22226 + p3_latch0; clock = clock0 } = x_512 in h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 program_counter0 special_function_registers_8053 @@ -766,13 +766,13 @@ let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_22226 = -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1 preStatus -> 'a2 **) -let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_22228 = +let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_514 = let { low_internal_ram = low_internal_ram0; high_internal_ram = high_internal_ram0; external_ram = external_ram0; program_counter = program_counter0; special_function_registers_8051 = special_function_registers_8053; special_function_registers_8052 = special_function_registers_8054; p1_latch = p1_latch0; p3_latch = - p3_latch0; clock = clock0 } = x_22228 + p3_latch0; clock = clock0 } = x_514 in h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 program_counter0 special_function_registers_8053 @@ -784,13 +784,13 @@ let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_22228 = -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1 preStatus -> 'a2 **) -let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_22230 = +let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_516 = let { low_internal_ram = low_internal_ram0; high_internal_ram = high_internal_ram0; external_ram = external_ram0; program_counter = program_counter0; special_function_registers_8051 = special_function_registers_8053; special_function_registers_8052 = special_function_registers_8054; p1_latch = p1_latch0; p3_latch = - p3_latch0; clock = clock0 } = x_22230 + p3_latch0; clock = clock0 } = x_516 in h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 program_counter0 special_function_registers_8053 @@ -802,13 +802,13 @@ let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_22230 = -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1 preStatus -> 'a2 **) -let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_22232 = +let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_518 = let { low_internal_ram = low_internal_ram0; high_internal_ram = high_internal_ram0; external_ram = external_ram0; program_counter = program_counter0; special_function_registers_8051 = special_function_registers_8053; special_function_registers_8052 = special_function_registers_8054; p1_latch = p1_latch0; p3_latch = - p3_latch0; clock = clock0 } = x_22232 + p3_latch0; clock = clock0 } = x_518 in h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 program_counter0 special_function_registers_8053 @@ -820,13 +820,13 @@ let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_22232 = -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1 preStatus -> 'a2 **) -let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_22234 = +let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_520 = let { low_internal_ram = low_internal_ram0; high_internal_ram = high_internal_ram0; external_ram = external_ram0; program_counter = program_counter0; special_function_registers_8051 = special_function_registers_8053; special_function_registers_8052 = special_function_registers_8054; p1_latch = p1_latch0; p3_latch = - p3_latch0; clock = clock0 } = x_22234 + p3_latch0; clock = clock0 } = x_520 in h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0 program_counter0 special_function_registers_8053 diff --git a/extracted/switchRemoval.ml b/extracted/switchRemoval.ml index 3a873f7..c018da2 100644 --- a/extracted/switchRemoval.ml +++ b/extracted/switchRemoval.ml @@ -173,10 +173,10 @@ let rec produce_cond e switch_cases u exit = { Types.fst = { Types.fst = (Csyntax.Slabel (lab, st')); Types.snd = lab }; Types.snd = u1 } | Csyntax.LScase (sz, tag, st, other_cases) -> - let { Types.fst = eta2108; Types.snd = u1 } = + let { Types.fst = eta2130; Types.snd = u1 } = produce_cond e other_cases u exit in - let { Types.fst = sub_statements; Types.snd = sub_label } = eta2108 in + let { Types.fst = sub_statements; Types.snd = sub_label } = eta2130 in let st' = convert_break_to_goto st exit in let { Types.fst = lab; Types.snd = u2 } = Identifiers.fresh PreIdentifiers.SymbolTag u1 @@ -198,10 +198,10 @@ let simplify_switch e switch_cases uv = let { Types.fst = exit_label; Types.snd = uv1 } = Identifiers.fresh PreIdentifiers.SymbolTag uv in - let { Types.fst = eta2109; Types.snd = uv2 } = + let { Types.fst = eta2131; Types.snd = uv2 } = produce_cond e switch_cases uv1 exit_label in - let { Types.fst = result; Types.snd = useless_label } = eta2109 in + let { Types.fst = result; Types.snd = useless_label } = eta2131 in { Types.fst = (Csyntax.Ssequence (result, (Csyntax.Slabel (exit_label, Csyntax.Sskip)))); Types.snd = uv2 } @@ -218,36 +218,36 @@ let rec switch_removal st u = | Csyntax.Scall (x, x0, x1) -> { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u } | Csyntax.Ssequence (s1, s2) -> - let { Types.fst = eta2123; Types.snd = u' } = switch_removal s1 u in - let { Types.fst = s1'; Types.snd = acc1 } = eta2123 in - let { Types.fst = eta2122; Types.snd = u'' } = switch_removal s2 u' in - let { Types.fst = s2'; Types.snd = acc2 } = eta2122 in + let { Types.fst = eta2145; Types.snd = u' } = switch_removal s1 u in + let { Types.fst = s1'; Types.snd = acc1 } = eta2145 in + let { Types.fst = eta2144; Types.snd = u'' } = switch_removal s2 u' in + let { Types.fst = s2'; Types.snd = acc2 } = eta2144 in { Types.fst = { Types.fst = (Csyntax.Ssequence (s1', s2')); Types.snd = (List.append acc1 acc2) }; Types.snd = u'' } | Csyntax.Sifthenelse (e, s1, s2) -> - let { Types.fst = eta2125; Types.snd = u' } = switch_removal s1 u in - let { Types.fst = s1'; Types.snd = acc1 } = eta2125 in - let { Types.fst = eta2124; Types.snd = u'' } = switch_removal s2 u' in - let { Types.fst = s2'; Types.snd = acc2 } = eta2124 in + let { Types.fst = eta2147; Types.snd = u' } = switch_removal s1 u in + let { Types.fst = s1'; Types.snd = acc1 } = eta2147 in + let { Types.fst = eta2146; Types.snd = u'' } = switch_removal s2 u' in + let { Types.fst = s2'; Types.snd = acc2 } = eta2146 in { Types.fst = { Types.fst = (Csyntax.Sifthenelse (e, s1', s2')); Types.snd = (List.append acc1 acc2) }; Types.snd = u'' } | Csyntax.Swhile (e, body) -> - let { Types.fst = eta2126; Types.snd = u' } = switch_removal body u in - let { Types.fst = body'; Types.snd = acc } = eta2126 in + let { Types.fst = eta2148; Types.snd = u' } = switch_removal body u in + let { Types.fst = body'; Types.snd = acc } = eta2148 in { Types.fst = { Types.fst = (Csyntax.Swhile (e, body')); Types.snd = acc }; Types.snd = u' } | Csyntax.Sdowhile (e, body) -> - let { Types.fst = eta2127; Types.snd = u' } = switch_removal body u in - let { Types.fst = body'; Types.snd = acc } = eta2127 in + let { Types.fst = eta2149; Types.snd = u' } = switch_removal body u in + let { Types.fst = body'; Types.snd = acc } = eta2149 in { Types.fst = { Types.fst = (Csyntax.Sdowhile (e, body')); Types.snd = acc }; Types.snd = u' } | Csyntax.Sfor (s1, e, s2, s3) -> - let { Types.fst = eta2130; Types.snd = u' } = switch_removal s1 u in - let { Types.fst = s1'; Types.snd = acc1 } = eta2130 in - let { Types.fst = eta2129; Types.snd = u'' } = switch_removal s2 u' in - let { Types.fst = s2'; Types.snd = acc2 } = eta2129 in - let { Types.fst = eta2128; Types.snd = u''' } = switch_removal s3 u'' in - let { Types.fst = s3'; Types.snd = acc3 } = eta2128 in + let { Types.fst = eta2152; Types.snd = u' } = switch_removal s1 u in + let { Types.fst = s1'; Types.snd = acc1 } = eta2152 in + let { Types.fst = eta2151; Types.snd = u'' } = switch_removal s2 u' in + let { Types.fst = s2'; Types.snd = acc2 } = eta2151 in + let { Types.fst = eta2150; Types.snd = u''' } = switch_removal s3 u'' in + let { Types.fst = s3'; Types.snd = acc3 } = eta2150 in { Types.fst = { Types.fst = (Csyntax.Sfor (s1', e, s2', s3')); Types.snd = (List.append acc1 (List.append acc2 acc3)) }; Types.snd = u''' } @@ -258,10 +258,10 @@ let rec switch_removal st u = | Csyntax.Sreturn x -> { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u } | Csyntax.Sswitch (e, branches) -> - let { Types.fst = eta2131; Types.snd = u' } = + let { Types.fst = eta2153; Types.snd = u' } = switch_removal_branches branches u in - let { Types.fst = sf_branches; Types.snd = acc } = eta2131 in + let { Types.fst = sf_branches; Types.snd = acc } = eta2153 in let { Types.fst = switch_tmp; Types.snd = u'' } = Identifiers.fresh PreIdentifiers.SymbolTag u' in @@ -275,15 +275,15 @@ let rec switch_removal st u = Types.snd = (List.Cons ({ Types.fst = switch_tmp; Types.snd = (Csyntax.typeof e) }, acc)) }; Types.snd = u''' } | Csyntax.Slabel (label, body) -> - let { Types.fst = eta2132; Types.snd = u' } = switch_removal body u in - let { Types.fst = body'; Types.snd = acc } = eta2132 in + let { Types.fst = eta2154; Types.snd = u' } = switch_removal body u in + let { Types.fst = body'; Types.snd = acc } = eta2154 in { Types.fst = { Types.fst = (Csyntax.Slabel (label, body')); Types.snd = acc }; Types.snd = u' } | Csyntax.Sgoto x -> { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u } | Csyntax.Scost (cost, body) -> - let { Types.fst = eta2133; Types.snd = u' } = switch_removal body u in - let { Types.fst = body'; Types.snd = acc } = eta2133 in + let { Types.fst = eta2155; Types.snd = u' } = switch_removal body u in + let { Types.fst = body'; Types.snd = acc } = eta2155 in { Types.fst = { Types.fst = (Csyntax.Scost (cost, body')); Types.snd = acc }; Types.snd = u' } (** val switch_removal_branches : @@ -293,17 +293,17 @@ let rec switch_removal st u = and switch_removal_branches l u = match l with | Csyntax.LSdefault st -> - let { Types.fst = eta2134; Types.snd = u' } = switch_removal st u in - let { Types.fst = st'; Types.snd = acc1 } = eta2134 in + let { Types.fst = eta2156; Types.snd = u' } = switch_removal st u in + let { Types.fst = st'; Types.snd = acc1 } = eta2156 in { Types.fst = { Types.fst = (Csyntax.LSdefault st'); Types.snd = acc1 }; Types.snd = u' } | Csyntax.LScase (sz, int, st, tl) -> - let { Types.fst = eta2136; Types.snd = u' } = + let { Types.fst = eta2158; Types.snd = u' } = switch_removal_branches tl u in - let { Types.fst = tl_result; Types.snd = acc1 } = eta2136 in - let { Types.fst = eta2135; Types.snd = u'' } = switch_removal st u' in - let { Types.fst = st'; Types.snd = acc2 } = eta2135 in + let { Types.fst = tl_result; Types.snd = acc1 } = eta2158 in + let { Types.fst = eta2157; Types.snd = u'' } = switch_removal st u' in + let { Types.fst = st'; Types.snd = acc2 } = eta2157 in { Types.fst = { Types.fst = (Csyntax.LScase (sz, int, st', tl_result)); Types.snd = (List.append acc1 acc2) }; Types.snd = u'' } @@ -311,21 +311,21 @@ and switch_removal_branches l u = (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod, Identifiers.universe) Types.prod -> 'a1 **) let ret_st x = - let { Types.fst = eta2137; Types.snd = u } = x in eta2137.Types.fst + let { Types.fst = eta2159; Types.snd = u } = x in eta2159.Types.fst (** val ret_vars : (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod, Identifiers.universe) Types.prod -> (AST.ident, Csyntax.type0) Types.prod List.list **) let ret_vars x = - let { Types.fst = eta2138; Types.snd = u } = x in eta2138.Types.snd + let { Types.fst = eta2160; Types.snd = u } = x in eta2160.Types.snd (** val ret_u : (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod, Identifiers.universe) Types.prod -> Identifiers.universe **) let ret_u x = - let { Types.fst = eta2139; Types.snd = u } = x in - let { Types.fst = s; Types.snd = vars } = eta2139 in u + let { Types.fst = eta2161; Types.snd = u } = x in + let { Types.fst = s; Types.snd = vars } = eta2161 in u (** val least_identifier : PreIdentifiers.identifier **) let least_identifier = @@ -405,10 +405,10 @@ let max_id_of_function f = Types.prod List.list) Types.prod **) let function_switch_removal f = let u = Fresh.universe_of_max (max_id_of_function f) in - let { Types.fst = eta2140; Types.snd = u' } = + let { Types.fst = eta2162; Types.snd = u' } = switch_removal f.Csyntax.fn_body u in - let { Types.fst = st; Types.snd = vars } = eta2140 in + let { Types.fst = st; Types.snd = vars } = eta2162 in let result = { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params = f.Csyntax.fn_params; Csyntax.fn_vars = (List.append vars f.Csyntax.fn_vars); Csyntax.fn_body = st } diff --git a/extracted/toCminor.ml b/extracted/toCminor.ml index 4131f6c..8e12b74 100644 --- a/extracted/toCminor.ml +++ b/extracted/toCminor.ml @@ -2062,8 +2062,8 @@ let alloc_params_main vars lbls statement uv ul rettyp params s = let { Types.fst = id; Types.snd = ty } = it in Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su) - (fun eta2356 -> - let result = eta2356 in + (fun eta2378 -> + let result = eta2378 in (let { Types.fst = fgens1; Types.snd = s0 } = result in (fun _ -> Obj.magic diff --git a/extracted/toRTLabs.ml b/extracted/toRTLabs.ml index c33d803..b5ca972 100644 --- a/extracted/toRTLabs.ml +++ b/extracted/toRTLabs.ml @@ -120,8 +120,8 @@ type env = let populate_env en gen = List.foldr (fun idt rsengen -> let { Types.fst = id; Types.snd = ty } = idt in - let { Types.fst = eta2859; Types.snd = gen0 } = rsengen in - let { Types.fst = rs; Types.snd = en0 } = eta2859 in + let { Types.fst = eta2881; Types.snd = gen0 } = rsengen in + let { Types.fst = rs; Types.snd = en0 } = eta2881 in let { Types.fst = r; Types.snd = gen' } = Identifiers.fresh PreIdentifiers.RegisterTag gen0 in @@ -1344,16 +1344,16 @@ let c2ra_function f = let labgen0 = Identifiers.new_universe PreIdentifiers.LabelTag in let reggen0 = Identifiers.new_universe PreIdentifiers.RegisterTag in let cminor_labels = Cminor_syntax.labels_of f.Cminor_syntax.f_body in - (let { Types.fst = eta3086; Types.snd = reggen1 } = + (let { Types.fst = eta3108; Types.snd = reggen1 } = populate_env (Identifiers.empty_map PreIdentifiers.SymbolTag) reggen0 f.Cminor_syntax.f_params in - let { Types.fst = params; Types.snd = env1 } = eta3086 in + let { Types.fst = params; Types.snd = env1 } = eta3108 in (fun _ -> - (let { Types.fst = eta3085; Types.snd = reggen2 } = + (let { Types.fst = eta3107; Types.snd = reggen2 } = populate_env env1 reggen1 f.Cminor_syntax.f_vars in - let { Types.fst = locals0; Types.snd = env0 } = eta3085 in + let { Types.fst = locals0; Types.snd = env0 } = eta3107 in (fun _ -> (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } = match f.Cminor_syntax.f_return with -- 2.39.2