Changeset 2773


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
Files:
2 added
4 deleted
228 edited

Legend:

Unmodified
Added
Removed
  • driver/clightFromC.ml

    r2758 r2773  
    388388        | C.Oshr -> Oshr
    389389        | C.Oeq  -> Oeq
    390         | C.One  -> One0
     390        | C.One  -> One
    391391        | C.Olt  -> Olt
    392392        | C.Ogt  -> Ogt
  • driver/clightPrinter.ml

    r2759 r2773  
    7676  | Oshr -> ">>"
    7777  | Oeq  -> "=="
    78   | One0  -> "!="
     78  | One  -> "!="
    7979  | Olt  -> "<"
    8080  | Ogt  -> ">"
     
    176176      begin match op with
    177177      | Oand | Oor | Oxor -> 75
    178       | Oeq | One0 | Olt | Ogt | Ole | Oge -> 70
     178      | Oeq | One | Olt | Ogt | Ole | Oge -> 70
    179179      | Oadd | Osub | Oshl | Oshr -> 60
    180180      | Omul | Odiv | Omod -> 40
  • driver/error.ml

    r2729 r2773  
    33
    44let error_to_string = function
     5| AssemblyTooLarge -> "AssemblyTooLarge"
    56| MISSING -> "MISSING"
    67| EXTERNAL -> "EXTERNAL"
  • driver/exec.ml

    r2721 r2773  
    22
    33let rec run g s =
    4   (match Extracted.Cexec.is_final0 s with
     4  (match Extracted.Cexec.is_final s with
    55  | Extracted.Types.None ->
    66    (match Extracted.Cexec.exec_step g s with
     
    2525let OK mid = Extracted.Compiler.front_end cl in
    2626let rtlabs = Extracted.Types.snd mid in
    27 let g = Extracted.Cexec.make_global0 cl in
    28 let OK s0 = Extracted.Cexec.make_initial_state0 cl in
     27let g = Extracted.Cexec.make_global cl in
     28let OK s0 = Extracted.Cexec.make_initial_state cl in
    2929let r = run g s0 in
    3030exit (bv_to_int r)
  • driver/frontend.ml

    r2721 r2773  
    2525let OK mid = Extracted.Compiler.front_end cl in
    2626let rtlabs = Extracted.Types.snd mid in
    27 let g = Extracted.RTLabs_semantics.make_global0 rtlabs in
    28 let OK s0 = Extracted.RTLabs_semantics.make_initial_state0 rtlabs in
     27let g = Extracted.RTLabs_semantics.make_global rtlabs in
     28let OK s0 = Extracted.RTLabs_semantics.make_initial_state rtlabs in
    2929let r = run g s0 in
    3030exit (bv_to_int r)
  • extracted/PROBLEMS

    r2743 r2773  
    1 ================
    2 EXTRACTION BUGS:
    3 ================
    4 
    5 1. In some situations the types implemented with = __ in the .mli
    6    are less general than those in the .ml
    7 
    81=========================
    92AXIOMS TO BE IMPLEMENTED:
     
    136intervention:
    147
    15 a) compiler.ml
    16 b) set_adt needs to be removed to favour the untrusted implementation
     8a) compiler.ml: the two failwith must be replaced with calls to the
     9   untrusted code
     10b) the build script removed set_adt to favour the untrusted implementation
  • extracted/aSM.ml

    r2743 r2773  
    11open Preamble
    22
     3open Proper
     4
     5open PositiveMap
     6
     7open Deqsets
     8
     9open ErrorMessages
     10
     11open PreIdentifiers
     12
     13open Errors
     14
     15open Extralib
     16
     17open Setoids
     18
     19open Monad
     20
     21open Option
     22
     23open Div_and_mod
     24
     25open Jmeq
     26
     27open Russell
     28
     29open Util
     30
     31open List
     32
     33open Lists
     34
     35open Bool
     36
     37open Relations
     38
     39open Nat
     40
     41open Positive
     42
     43open Hints_declaration
     44
     45open Core_notation
     46
     47open Pts
     48
     49open Logic
     50
     51open Types
     52
     53open Identifiers
     54
     55open CostLabel
     56
     57open LabelledObjects
     58
     59open Exp
     60
     61open Arithmetic
     62
     63open Vector
     64
     65open FoldStuff
     66
     67open BitVector
     68
    369open Extranat
    470
    5 open Vector
    6 
    7 open Div_and_mod
    8 
    9 open Jmeq
    10 
    11 open Russell
    12 
    13 open Types
    14 
    15 open List
    16 
    17 open Util
    18 
    19 open FoldStuff
    20 
    21 open Bool
    22 
    23 open Hints_declaration
    24 
    25 open Core_notation
    26 
    27 open Pts
    28 
    29 open Logic
    30 
    31 open Relations
    32 
    33 open Nat
    34 
    35 open BitVector
    36 
    37 open Proper
    38 
    39 open PositiveMap
    40 
    41 open Deqsets
    42 
    43 open ErrorMessages
    44 
    45 open PreIdentifiers
    46 
    47 open Errors
    48 
    49 open Extralib
    50 
    51 open Setoids
    52 
    53 open Monad
    54 
    55 open Option
    56 
    57 open Lists
    58 
    59 open Positive
    60 
    61 open Identifiers
     71open Integers
     72
     73open AST
     74
     75open String
    6276
    6377open BitVectorTrie
    6478
    65 open Exp
    66 
    67 open Arithmetic
    68 
    69 open Integers
    70 
    71 open AST
    72 
    73 open CostLabel
    74 
    75 open LabelledObjects
    76 
    77 open String
    78 
    79 type identifier0 = PreIdentifiers.identifier
     79type identifier = PreIdentifiers.identifier
    8080
    8181(** val toASM_ident :
    82     PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier0 **)
     82    PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier **)
    8383let toASM_ident t i =
    8484  let id = i in id
     
    113113    -> 'a1) -> addressing_mode -> 'a1 **)
    114114let rec addressing_mode_rect_Type4 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    115 | DIRECT x_21796 -> h_DIRECT x_21796
    116 | INDIRECT x_21797 -> h_INDIRECT x_21797
    117 | EXT_INDIRECT x_21798 -> h_EXT_INDIRECT x_21798
    118 | REGISTER x_21799 -> h_REGISTER x_21799
     115| DIRECT x_17106 -> h_DIRECT x_17106
     116| INDIRECT x_17107 -> h_INDIRECT x_17107
     117| EXT_INDIRECT x_17108 -> h_EXT_INDIRECT x_17108
     118| REGISTER x_17109 -> h_REGISTER x_17109
    119119| ACC_A -> h_ACC_A
    120120| ACC_B -> h_ACC_B
    121121| DPTR -> h_DPTR
    122 | DATA x_21800 -> h_DATA x_21800
    123 | DATA16 x_21801 -> h_DATA16 x_21801
     122| DATA x_17110 -> h_DATA x_17110
     123| DATA16 x_17111 -> h_DATA16 x_17111
    124124| ACC_DPTR -> h_ACC_DPTR
    125125| ACC_PC -> h_ACC_PC
     
    127127| INDIRECT_DPTR -> h_INDIRECT_DPTR
    128128| CARRY -> h_CARRY
    129 | BIT_ADDR x_21802 -> h_BIT_ADDR x_21802
    130 | N_BIT_ADDR x_21803 -> h_N_BIT_ADDR x_21803
    131 | RELATIVE x_21804 -> h_RELATIVE x_21804
    132 | ADDR11 x_21805 -> h_ADDR11 x_21805
    133 | ADDR16 x_21806 -> h_ADDR16 x_21806
     129| BIT_ADDR x_17112 -> h_BIT_ADDR x_17112
     130| N_BIT_ADDR x_17113 -> h_N_BIT_ADDR x_17113
     131| RELATIVE x_17114 -> h_RELATIVE x_17114
     132| ADDR11 x_17115 -> h_ADDR11 x_17115
     133| ADDR16 x_17116 -> h_ADDR16 x_17116
    134134
    135135(** val addressing_mode_rect_Type5 :
     
    141141    -> 'a1) -> addressing_mode -> 'a1 **)
    142142let rec addressing_mode_rect_Type5 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    143 | DIRECT x_21827 -> h_DIRECT x_21827
    144 | INDIRECT x_21828 -> h_INDIRECT x_21828
    145 | EXT_INDIRECT x_21829 -> h_EXT_INDIRECT x_21829
    146 | REGISTER x_21830 -> h_REGISTER x_21830
     143| DIRECT x_17137 -> h_DIRECT x_17137
     144| INDIRECT x_17138 -> h_INDIRECT x_17138
     145| EXT_INDIRECT x_17139 -> h_EXT_INDIRECT x_17139
     146| REGISTER x_17140 -> h_REGISTER x_17140
    147147| ACC_A -> h_ACC_A
    148148| ACC_B -> h_ACC_B
    149149| DPTR -> h_DPTR
    150 | DATA x_21831 -> h_DATA x_21831
    151 | DATA16 x_21832 -> h_DATA16 x_21832
     150| DATA x_17141 -> h_DATA x_17141
     151| DATA16 x_17142 -> h_DATA16 x_17142
    152152| ACC_DPTR -> h_ACC_DPTR
    153153| ACC_PC -> h_ACC_PC
     
    155155| INDIRECT_DPTR -> h_INDIRECT_DPTR
    156156| CARRY -> h_CARRY
    157 | BIT_ADDR x_21833 -> h_BIT_ADDR x_21833
    158 | N_BIT_ADDR x_21834 -> h_N_BIT_ADDR x_21834
    159 | RELATIVE x_21835 -> h_RELATIVE x_21835
    160 | ADDR11 x_21836 -> h_ADDR11 x_21836
    161 | ADDR16 x_21837 -> h_ADDR16 x_21837
     157| BIT_ADDR x_17143 -> h_BIT_ADDR x_17143
     158| N_BIT_ADDR x_17144 -> h_N_BIT_ADDR x_17144
     159| RELATIVE x_17145 -> h_RELATIVE x_17145
     160| ADDR11 x_17146 -> h_ADDR11 x_17146
     161| ADDR16 x_17147 -> h_ADDR16 x_17147
    162162
    163163(** val addressing_mode_rect_Type3 :
     
    169169    -> 'a1) -> addressing_mode -> 'a1 **)
    170170let rec addressing_mode_rect_Type3 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    171 | DIRECT x_21858 -> h_DIRECT x_21858
    172 | INDIRECT x_21859 -> h_INDIRECT x_21859
    173 | EXT_INDIRECT x_21860 -> h_EXT_INDIRECT x_21860
    174 | REGISTER x_21861 -> h_REGISTER x_21861
     171| DIRECT x_17168 -> h_DIRECT x_17168
     172| INDIRECT x_17169 -> h_INDIRECT x_17169
     173| EXT_INDIRECT x_17170 -> h_EXT_INDIRECT x_17170
     174| REGISTER x_17171 -> h_REGISTER x_17171
    175175| ACC_A -> h_ACC_A
    176176| ACC_B -> h_ACC_B
    177177| DPTR -> h_DPTR
    178 | DATA x_21862 -> h_DATA x_21862
    179 | DATA16 x_21863 -> h_DATA16 x_21863
     178| DATA x_17172 -> h_DATA x_17172
     179| DATA16 x_17173 -> h_DATA16 x_17173
    180180| ACC_DPTR -> h_ACC_DPTR
    181181| ACC_PC -> h_ACC_PC
     
    183183| INDIRECT_DPTR -> h_INDIRECT_DPTR
    184184| CARRY -> h_CARRY
    185 | BIT_ADDR x_21864 -> h_BIT_ADDR x_21864
    186 | N_BIT_ADDR x_21865 -> h_N_BIT_ADDR x_21865
    187 | RELATIVE x_21866 -> h_RELATIVE x_21866
    188 | ADDR11 x_21867 -> h_ADDR11 x_21867
    189 | ADDR16 x_21868 -> h_ADDR16 x_21868
     185| BIT_ADDR x_17174 -> h_BIT_ADDR x_17174
     186| N_BIT_ADDR x_17175 -> h_N_BIT_ADDR x_17175
     187| RELATIVE x_17176 -> h_RELATIVE x_17176
     188| ADDR11 x_17177 -> h_ADDR11 x_17177
     189| ADDR16 x_17178 -> h_ADDR16 x_17178
    190190
    191191(** val addressing_mode_rect_Type2 :
     
    197197    -> 'a1) -> addressing_mode -> 'a1 **)
    198198let rec addressing_mode_rect_Type2 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    199 | DIRECT x_21889 -> h_DIRECT x_21889
    200 | INDIRECT x_21890 -> h_INDIRECT x_21890
    201 | EXT_INDIRECT x_21891 -> h_EXT_INDIRECT x_21891
    202 | REGISTER x_21892 -> h_REGISTER x_21892
     199| DIRECT x_17199 -> h_DIRECT x_17199
     200| INDIRECT x_17200 -> h_INDIRECT x_17200
     201| EXT_INDIRECT x_17201 -> h_EXT_INDIRECT x_17201
     202| REGISTER x_17202 -> h_REGISTER x_17202
    203203| ACC_A -> h_ACC_A
    204204| ACC_B -> h_ACC_B
    205205| DPTR -> h_DPTR
    206 | DATA x_21893 -> h_DATA x_21893
    207 | DATA16 x_21894 -> h_DATA16 x_21894
     206| DATA x_17203 -> h_DATA x_17203
     207| DATA16 x_17204 -> h_DATA16 x_17204
    208208| ACC_DPTR -> h_ACC_DPTR
    209209| ACC_PC -> h_ACC_PC
     
    211211| INDIRECT_DPTR -> h_INDIRECT_DPTR
    212212| CARRY -> h_CARRY
    213 | BIT_ADDR x_21895 -> h_BIT_ADDR x_21895
    214 | N_BIT_ADDR x_21896 -> h_N_BIT_ADDR x_21896
    215 | RELATIVE x_21897 -> h_RELATIVE x_21897
    216 | ADDR11 x_21898 -> h_ADDR11 x_21898
    217 | ADDR16 x_21899 -> h_ADDR16 x_21899
     213| BIT_ADDR x_17205 -> h_BIT_ADDR x_17205
     214| N_BIT_ADDR x_17206 -> h_N_BIT_ADDR x_17206
     215| RELATIVE x_17207 -> h_RELATIVE x_17207
     216| ADDR11 x_17208 -> h_ADDR11 x_17208
     217| ADDR16 x_17209 -> h_ADDR16 x_17209
    218218
    219219(** val addressing_mode_rect_Type1 :
     
    225225    -> 'a1) -> addressing_mode -> 'a1 **)
    226226let rec addressing_mode_rect_Type1 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    227 | DIRECT x_21920 -> h_DIRECT x_21920
    228 | INDIRECT x_21921 -> h_INDIRECT x_21921
    229 | EXT_INDIRECT x_21922 -> h_EXT_INDIRECT x_21922
    230 | REGISTER x_21923 -> h_REGISTER x_21923
     227| DIRECT x_17230 -> h_DIRECT x_17230
     228| INDIRECT x_17231 -> h_INDIRECT x_17231
     229| EXT_INDIRECT x_17232 -> h_EXT_INDIRECT x_17232
     230| REGISTER x_17233 -> h_REGISTER x_17233
    231231| ACC_A -> h_ACC_A
    232232| ACC_B -> h_ACC_B
    233233| DPTR -> h_DPTR
    234 | DATA x_21924 -> h_DATA x_21924
    235 | DATA16 x_21925 -> h_DATA16 x_21925
     234| DATA x_17234 -> h_DATA x_17234
     235| DATA16 x_17235 -> h_DATA16 x_17235
    236236| ACC_DPTR -> h_ACC_DPTR
    237237| ACC_PC -> h_ACC_PC
     
    239239| INDIRECT_DPTR -> h_INDIRECT_DPTR
    240240| CARRY -> h_CARRY
    241 | BIT_ADDR x_21926 -> h_BIT_ADDR x_21926
    242 | N_BIT_ADDR x_21927 -> h_N_BIT_ADDR x_21927
    243 | RELATIVE x_21928 -> h_RELATIVE x_21928
    244 | ADDR11 x_21929 -> h_ADDR11 x_21929
    245 | ADDR16 x_21930 -> h_ADDR16 x_21930
     241| BIT_ADDR x_17236 -> h_BIT_ADDR x_17236
     242| N_BIT_ADDR x_17237 -> h_N_BIT_ADDR x_17237
     243| RELATIVE x_17238 -> h_RELATIVE x_17238
     244| ADDR11 x_17239 -> h_ADDR11 x_17239
     245| ADDR16 x_17240 -> h_ADDR16 x_17240
    246246
    247247(** val addressing_mode_rect_Type0 :
     
    253253    -> 'a1) -> addressing_mode -> 'a1 **)
    254254let rec addressing_mode_rect_Type0 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    255 | DIRECT x_21951 -> h_DIRECT x_21951
    256 | INDIRECT x_21952 -> h_INDIRECT x_21952
    257 | EXT_INDIRECT x_21953 -> h_EXT_INDIRECT x_21953
    258 | REGISTER x_21954 -> h_REGISTER x_21954
     255| DIRECT x_17261 -> h_DIRECT x_17261
     256| INDIRECT x_17262 -> h_INDIRECT x_17262
     257| EXT_INDIRECT x_17263 -> h_EXT_INDIRECT x_17263
     258| REGISTER x_17264 -> h_REGISTER x_17264
    259259| ACC_A -> h_ACC_A
    260260| ACC_B -> h_ACC_B
    261261| DPTR -> h_DPTR
    262 | DATA x_21955 -> h_DATA x_21955
    263 | DATA16 x_21956 -> h_DATA16 x_21956
     262| DATA x_17265 -> h_DATA x_17265
     263| DATA16 x_17266 -> h_DATA16 x_17266
    264264| ACC_DPTR -> h_ACC_DPTR
    265265| ACC_PC -> h_ACC_PC
     
    267267| INDIRECT_DPTR -> h_INDIRECT_DPTR
    268268| CARRY -> h_CARRY
    269 | BIT_ADDR x_21957 -> h_BIT_ADDR x_21957
    270 | N_BIT_ADDR x_21958 -> h_N_BIT_ADDR x_21958
    271 | RELATIVE x_21959 -> h_RELATIVE x_21959
    272 | ADDR11 x_21960 -> h_ADDR11 x_21960
    273 | ADDR16 x_21961 -> h_ADDR16 x_21961
     269| BIT_ADDR x_17267 -> h_BIT_ADDR x_17267
     270| N_BIT_ADDR x_17268 -> h_N_BIT_ADDR x_17268
     271| RELATIVE x_17269 -> h_RELATIVE x_17269
     272| ADDR11 x_17270 -> h_ADDR11 x_17270
     273| ADDR16 x_17271 -> h_ADDR16 x_17271
    274274
    275275(** val addressing_mode_inv_rect_Type4 :
     
    403403  | DIRECT d ->
    404404    (match b with
    405      | DIRECT e0 ->
     405     | DIRECT e ->
    406406       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    407          (Nat.S Nat.O)))))))) d e0
     407         (Nat.S Nat.O)))))))) d e
    408408     | INDIRECT x -> Bool.False
    409409     | EXT_INDIRECT x -> Bool.False
     
    427427    (match b with
    428428     | DIRECT x -> Bool.False
    429      | INDIRECT e0 -> BitVector.eq_b b' e0
     429     | INDIRECT e -> BitVector.eq_b b' e
    430430     | EXT_INDIRECT x -> Bool.False
    431431     | REGISTER x -> Bool.False
     
    449449     | DIRECT x -> Bool.False
    450450     | INDIRECT x -> Bool.False
    451      | EXT_INDIRECT e0 -> BitVector.eq_b b' e0
     451     | EXT_INDIRECT e -> BitVector.eq_b b' e
    452452     | REGISTER x -> Bool.False
    453453     | ACC_A -> Bool.False
     
    559559     | ACC_B -> Bool.False
    560560     | DPTR -> Bool.False
    561      | DATA e0 ->
     561     | DATA e ->
    562562       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    563          (Nat.S Nat.O)))))))) b' e0
     563         (Nat.S Nat.O)))))))) b' e
    564564     | DATA16 x -> Bool.False
    565565     | ACC_DPTR -> Bool.False
     
    583583     | DPTR -> Bool.False
    584584     | DATA x -> Bool.False
    585      | DATA16 e0 ->
     585     | DATA16 e ->
    586586       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    587587         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    588          Nat.O)))))))))))))))) w e0
     588         Nat.O)))))))))))))))) w e
    589589     | ACC_DPTR -> Bool.False
    590590     | ACC_PC -> Bool.False
     
    718718     | INDIRECT_DPTR -> Bool.False
    719719     | CARRY -> Bool.False
    720      | BIT_ADDR e0 ->
     720     | BIT_ADDR e ->
    721721       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    722          (Nat.S Nat.O)))))))) b' e0
     722         (Nat.S Nat.O)))))))) b' e
    723723     | N_BIT_ADDR x -> Bool.False
    724724     | RELATIVE x -> Bool.False
     
    742742     | CARRY -> Bool.False
    743743     | BIT_ADDR x -> Bool.False
    744      | N_BIT_ADDR e0 ->
     744     | N_BIT_ADDR e ->
    745745       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    746          (Nat.S Nat.O)))))))) b' e0
     746         (Nat.S Nat.O)))))))) b' e
    747747     | RELATIVE x -> Bool.False
    748748     | ADDR11 x -> Bool.False
     
    766766     | BIT_ADDR x -> Bool.False
    767767     | N_BIT_ADDR x -> Bool.False
    768      | RELATIVE e0 ->
     768     | RELATIVE e ->
    769769       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    770          (Nat.S Nat.O)))))))) n e0
     770         (Nat.S Nat.O)))))))) n e
    771771     | ADDR11 x -> Bool.False
    772772     | ADDR16 x -> Bool.False)
     
    790790     | N_BIT_ADDR x -> Bool.False
    791791     | RELATIVE x -> Bool.False
    792      | ADDR11 e0 ->
     792     | ADDR11 e ->
    793793       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    794          (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))) w e0
     794         (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))) w e
    795795     | ADDR16 x -> Bool.False)
    796796  | ADDR16 w ->
     
    814814     | RELATIVE x -> Bool.False
    815815     | ADDR11 x -> Bool.False
    816      | ADDR16 e0 ->
     816     | ADDR16 e ->
    817817       BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    818818         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    819          Nat.O)))))))))))))))) w e0)
     819         Nat.O)))))))))))))))) w e)
    820820
    821821type addressing_mode_tag =
     
    15081508     | Addr16 -> Bool.True)
    15091509
    1510 type member_addressing_mode_tag = __
    1511 
    15121510(** val is_a : addressing_mode_tag -> addressing_mode -> Bool.bool **)
    15131511let rec is_a d a =
     
    19281926    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19291927    'a1) -> subaddressing_mode -> 'a1 **)
    1930 let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_22429 =
    1931   let subaddressing_modeel = x_22429 in
     1928let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_17739 =
     1929  let subaddressing_modeel = x_17739 in
    19321930  h_mk_subaddressing_mode subaddressing_modeel __
    19331931
     
    19351933    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19361934    'a1) -> subaddressing_mode -> 'a1 **)
    1937 let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_22431 =
    1938   let subaddressing_modeel = x_22431 in
     1935let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_17741 =
     1936  let subaddressing_modeel = x_17741 in
    19391937  h_mk_subaddressing_mode subaddressing_modeel __
    19401938
     
    19421940    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19431941    'a1) -> subaddressing_mode -> 'a1 **)
    1944 let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_22433 =
    1945   let subaddressing_modeel = x_22433 in
     1942let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_17743 =
     1943  let subaddressing_modeel = x_17743 in
    19461944  h_mk_subaddressing_mode subaddressing_modeel __
    19471945
     
    19491947    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19501948    'a1) -> subaddressing_mode -> 'a1 **)
    1951 let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_22435 =
    1952   let subaddressing_modeel = x_22435 in
     1949let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_17745 =
     1950  let subaddressing_modeel = x_17745 in
    19531951  h_mk_subaddressing_mode subaddressing_modeel __
    19541952
     
    19561954    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19571955    'a1) -> subaddressing_mode -> 'a1 **)
    1958 let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_22437 =
    1959   let subaddressing_modeel = x_22437 in
     1956let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_17747 =
     1957  let subaddressing_modeel = x_17747 in
    19601958  h_mk_subaddressing_mode subaddressing_modeel __
    19611959
     
    19631961    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19641962    'a1) -> subaddressing_mode -> 'a1 **)
    1965 let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_22439 =
    1966   let subaddressing_modeel = x_22439 in
     1963let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_17749 =
     1964  let subaddressing_modeel = x_17749 in
    19671965  h_mk_subaddressing_mode subaddressing_modeel __
    19681966
     
    22002198let eject__o__mk_subaddressing_mode x1 x2 x3 =
    22012199  Types.pi1 x2
    2202 
    2203 type subaddressing_mode_elim_type = __
    22042200
    22052201type 'a preinstruction =
     
    22922288    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    22932289let 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
    2294 | ADD (x_22541, x_22540) -> h_ADD x_22541 x_22540
    2295 | ADDC (x_22543, x_22542) -> h_ADDC x_22543 x_22542
    2296 | SUBB (x_22545, x_22544) -> h_SUBB x_22545 x_22544
    2297 | INC x_22546 -> h_INC x_22546
    2298 | DEC x_22547 -> h_DEC x_22547
    2299 | MUL (x_22549, x_22548) -> h_MUL x_22549 x_22548
    2300 | DIV (x_22551, x_22550) -> h_DIV x_22551 x_22550
    2301 | DA x_22552 -> h_DA x_22552
    2302 | JC x_22553 -> h_JC x_22553
    2303 | JNC x_22554 -> h_JNC x_22554
    2304 | JB (x_22556, x_22555) -> h_JB x_22556 x_22555
    2305 | JNB (x_22558, x_22557) -> h_JNB x_22558 x_22557
    2306 | JBC (x_22560, x_22559) -> h_JBC x_22560 x_22559
    2307 | JZ x_22561 -> h_JZ x_22561
    2308 | JNZ x_22562 -> h_JNZ x_22562
    2309 | CJNE (x_22564, x_22563) -> h_CJNE x_22564 x_22563
    2310 | DJNZ (x_22566, x_22565) -> h_DJNZ x_22566 x_22565
    2311 | ANL x_22567 -> h_ANL x_22567
    2312 | ORL x_22568 -> h_ORL x_22568
    2313 | XRL x_22569 -> h_XRL x_22569
    2314 | CLR x_22570 -> h_CLR x_22570
    2315 | CPL x_22571 -> h_CPL x_22571
    2316 | RL x_22572 -> h_RL x_22572
    2317 | RLC x_22573 -> h_RLC x_22573
    2318 | RR x_22574 -> h_RR x_22574
    2319 | RRC x_22575 -> h_RRC x_22575
    2320 | SWAP x_22576 -> h_SWAP x_22576
    2321 | MOV x_22577 -> h_MOV x_22577
    2322 | MOVX x_22578 -> h_MOVX x_22578
    2323 | SETB x_22579 -> h_SETB x_22579
    2324 | PUSH x_22580 -> h_PUSH x_22580
    2325 | POP x_22581 -> h_POP x_22581
    2326 | XCH (x_22583, x_22582) -> h_XCH x_22583 x_22582
    2327 | XCHD (x_22585, x_22584) -> h_XCHD x_22585 x_22584
     2290| ADD (x_17851, x_17850) -> h_ADD x_17851 x_17850
     2291| ADDC (x_17853, x_17852) -> h_ADDC x_17853 x_17852
     2292| SUBB (x_17855, x_17854) -> h_SUBB x_17855 x_17854
     2293| INC x_17856 -> h_INC x_17856
     2294| DEC x_17857 -> h_DEC x_17857
     2295| MUL (x_17859, x_17858) -> h_MUL x_17859 x_17858
     2296| DIV (x_17861, x_17860) -> h_DIV x_17861 x_17860
     2297| DA x_17862 -> h_DA x_17862
     2298| JC x_17863 -> h_JC x_17863
     2299| JNC x_17864 -> h_JNC x_17864
     2300| JB (x_17866, x_17865) -> h_JB x_17866 x_17865
     2301| JNB (x_17868, x_17867) -> h_JNB x_17868 x_17867
     2302| JBC (x_17870, x_17869) -> h_JBC x_17870 x_17869
     2303| JZ x_17871 -> h_JZ x_17871
     2304| JNZ x_17872 -> h_JNZ x_17872
     2305| CJNE (x_17874, x_17873) -> h_CJNE x_17874 x_17873
     2306| DJNZ (x_17876, x_17875) -> h_DJNZ x_17876 x_17875
     2307| ANL x_17877 -> h_ANL x_17877
     2308| ORL x_17878 -> h_ORL x_17878
     2309| XRL x_17879 -> h_XRL x_17879
     2310| CLR x_17880 -> h_CLR x_17880
     2311| CPL x_17881 -> h_CPL x_17881
     2312| RL x_17882 -> h_RL x_17882
     2313| RLC x_17883 -> h_RLC x_17883
     2314| RR x_17884 -> h_RR x_17884
     2315| RRC x_17885 -> h_RRC x_17885
     2316| SWAP x_17886 -> h_SWAP x_17886
     2317| MOV x_17887 -> h_MOV x_17887
     2318| MOVX x_17888 -> h_MOVX x_17888
     2319| SETB x_17889 -> h_SETB x_17889
     2320| PUSH x_17890 -> h_PUSH x_17890
     2321| POP x_17891 -> h_POP x_17891
     2322| XCH (x_17893, x_17892) -> h_XCH x_17893 x_17892
     2323| XCHD (x_17895, x_17894) -> h_XCHD x_17895 x_17894
    23282324| RET -> h_RET
    23292325| RETI -> h_RETI
    23302326| NOP -> h_NOP
    2331 | JMP x_22586 -> h_JMP x_22586
     2327| JMP x_17896 -> h_JMP x_17896
    23322328
    23332329(** val preinstruction_rect_Type5 :
     
    23672363    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    23682364let 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
    2369 | ADD (x_22627, x_22626) -> h_ADD x_22627 x_22626
    2370 | ADDC (x_22629, x_22628) -> h_ADDC x_22629 x_22628
    2371 | SUBB (x_22631, x_22630) -> h_SUBB x_22631 x_22630
    2372 | INC x_22632 -> h_INC x_22632
    2373 | DEC x_22633 -> h_DEC x_22633
    2374 | MUL (x_22635, x_22634) -> h_MUL x_22635 x_22634
    2375 | DIV (x_22637, x_22636) -> h_DIV x_22637 x_22636
    2376 | DA x_22638 -> h_DA x_22638
    2377 | JC x_22639 -> h_JC x_22639
    2378 | JNC x_22640 -> h_JNC x_22640
    2379 | JB (x_22642, x_22641) -> h_JB x_22642 x_22641
    2380 | JNB (x_22644, x_22643) -> h_JNB x_22644 x_22643
    2381 | JBC (x_22646, x_22645) -> h_JBC x_22646 x_22645
    2382 | JZ x_22647 -> h_JZ x_22647
    2383 | JNZ x_22648 -> h_JNZ x_22648
    2384 | CJNE (x_22650, x_22649) -> h_CJNE x_22650 x_22649
    2385 | DJNZ (x_22652, x_22651) -> h_DJNZ x_22652 x_22651
    2386 | ANL x_22653 -> h_ANL x_22653
    2387 | ORL x_22654 -> h_ORL x_22654
    2388 | XRL x_22655 -> h_XRL x_22655
    2389 | CLR x_22656 -> h_CLR x_22656
    2390 | CPL x_22657 -> h_CPL x_22657
    2391 | RL x_22658 -> h_RL x_22658
    2392 | RLC x_22659 -> h_RLC x_22659
    2393 | RR x_22660 -> h_RR x_22660
    2394 | RRC x_22661 -> h_RRC x_22661
    2395 | SWAP x_22662 -> h_SWAP x_22662
    2396 | MOV x_22663 -> h_MOV x_22663
    2397 | MOVX x_22664 -> h_MOVX x_22664
    2398 | SETB x_22665 -> h_SETB x_22665
    2399 | PUSH x_22666 -> h_PUSH x_22666
    2400 | POP x_22667 -> h_POP x_22667
    2401 | XCH (x_22669, x_22668) -> h_XCH x_22669 x_22668
    2402 | XCHD (x_22671, x_22670) -> h_XCHD x_22671 x_22670
     2365| ADD (x_17937, x_17936) -> h_ADD x_17937 x_17936
     2366| ADDC (x_17939, x_17938) -> h_ADDC x_17939 x_17938
     2367| SUBB (x_17941, x_17940) -> h_SUBB x_17941 x_17940
     2368| INC x_17942 -> h_INC x_17942
     2369| DEC x_17943 -> h_DEC x_17943
     2370| MUL (x_17945, x_17944) -> h_MUL x_17945 x_17944
     2371| DIV (x_17947, x_17946) -> h_DIV x_17947 x_17946
     2372| DA x_17948 -> h_DA x_17948
     2373| JC x_17949 -> h_JC x_17949
     2374| JNC x_17950 -> h_JNC x_17950
     2375| JB (x_17952, x_17951) -> h_JB x_17952 x_17951
     2376| JNB (x_17954, x_17953) -> h_JNB x_17954 x_17953
     2377| JBC (x_17956, x_17955) -> h_JBC x_17956 x_17955
     2378| JZ x_17957 -> h_JZ x_17957
     2379| JNZ x_17958 -> h_JNZ x_17958
     2380| CJNE (x_17960, x_17959) -> h_CJNE x_17960 x_17959
     2381| DJNZ (x_17962, x_17961) -> h_DJNZ x_17962 x_17961
     2382| ANL x_17963 -> h_ANL x_17963
     2383| ORL x_17964 -> h_ORL x_17964
     2384| XRL x_17965 -> h_XRL x_17965
     2385| CLR x_17966 -> h_CLR x_17966
     2386| CPL x_17967 -> h_CPL x_17967
     2387| RL x_17968 -> h_RL x_17968
     2388| RLC x_17969 -> h_RLC x_17969
     2389| RR x_17970 -> h_RR x_17970
     2390| RRC x_17971 -> h_RRC x_17971
     2391| SWAP x_17972 -> h_SWAP x_17972
     2392| MOV x_17973 -> h_MOV x_17973
     2393| MOVX x_17974 -> h_MOVX x_17974
     2394| SETB x_17975 -> h_SETB x_17975
     2395| PUSH x_17976 -> h_PUSH x_17976
     2396| POP x_17977 -> h_POP x_17977
     2397| XCH (x_17979, x_17978) -> h_XCH x_17979 x_17978
     2398| XCHD (x_17981, x_17980) -> h_XCHD x_17981 x_17980
    24032399| RET -> h_RET
    24042400| RETI -> h_RETI
    24052401| NOP -> h_NOP
    2406 | JMP x_22672 -> h_JMP x_22672
     2402| JMP x_17982 -> h_JMP x_17982
    24072403
    24082404(** val preinstruction_rect_Type3 :
     
    24422438    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    24432439let 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
    2444 | ADD (x_22713, x_22712) -> h_ADD x_22713 x_22712
    2445 | ADDC (x_22715, x_22714) -> h_ADDC x_22715 x_22714
    2446 | SUBB (x_22717, x_22716) -> h_SUBB x_22717 x_22716
    2447 | INC x_22718 -> h_INC x_22718
    2448 | DEC x_22719 -> h_DEC x_22719
    2449 | MUL (x_22721, x_22720) -> h_MUL x_22721 x_22720
    2450 | DIV (x_22723, x_22722) -> h_DIV x_22723 x_22722
    2451 | DA x_22724 -> h_DA x_22724
    2452 | JC x_22725 -> h_JC x_22725
    2453 | JNC x_22726 -> h_JNC x_22726
    2454 | JB (x_22728, x_22727) -> h_JB x_22728 x_22727
    2455 | JNB (x_22730, x_22729) -> h_JNB x_22730 x_22729
    2456 | JBC (x_22732, x_22731) -> h_JBC x_22732 x_22731
    2457 | JZ x_22733 -> h_JZ x_22733
    2458 | JNZ x_22734 -> h_JNZ x_22734
    2459 | CJNE (x_22736, x_22735) -> h_CJNE x_22736 x_22735
    2460 | DJNZ (x_22738, x_22737) -> h_DJNZ x_22738 x_22737
    2461 | ANL x_22739 -> h_ANL x_22739
    2462 | ORL x_22740 -> h_ORL x_22740
    2463 | XRL x_22741 -> h_XRL x_22741
    2464 | CLR x_22742 -> h_CLR x_22742
    2465 | CPL x_22743 -> h_CPL x_22743
    2466 | RL x_22744 -> h_RL x_22744
    2467 | RLC x_22745 -> h_RLC x_22745
    2468 | RR x_22746 -> h_RR x_22746
    2469 | RRC x_22747 -> h_RRC x_22747
    2470 | SWAP x_22748 -> h_SWAP x_22748
    2471 | MOV x_22749 -> h_MOV x_22749
    2472 | MOVX x_22750 -> h_MOVX x_22750
    2473 | SETB x_22751 -> h_SETB x_22751
    2474 | PUSH x_22752 -> h_PUSH x_22752
    2475 | POP x_22753 -> h_POP x_22753
    2476 | XCH (x_22755, x_22754) -> h_XCH x_22755 x_22754
    2477 | XCHD (x_22757, x_22756) -> h_XCHD x_22757 x_22756
     2440| ADD (x_18023, x_18022) -> h_ADD x_18023 x_18022
     2441| ADDC (x_18025, x_18024) -> h_ADDC x_18025 x_18024
     2442| SUBB (x_18027, x_18026) -> h_SUBB x_18027 x_18026
     2443| INC x_18028 -> h_INC x_18028
     2444| DEC x_18029 -> h_DEC x_18029
     2445| MUL (x_18031, x_18030) -> h_MUL x_18031 x_18030
     2446| DIV (x_18033, x_18032) -> h_DIV x_18033 x_18032
     2447| DA x_18034 -> h_DA x_18034
     2448| JC x_18035 -> h_JC x_18035
     2449| JNC x_18036 -> h_JNC x_18036
     2450| JB (x_18038, x_18037) -> h_JB x_18038 x_18037
     2451| JNB (x_18040, x_18039) -> h_JNB x_18040 x_18039
     2452| JBC (x_18042, x_18041) -> h_JBC x_18042 x_18041
     2453| JZ x_18043 -> h_JZ x_18043
     2454| JNZ x_18044 -> h_JNZ x_18044
     2455| CJNE (x_18046, x_18045) -> h_CJNE x_18046 x_18045
     2456| DJNZ (x_18048, x_18047) -> h_DJNZ x_18048 x_18047
     2457| ANL x_18049 -> h_ANL x_18049
     2458| ORL x_18050 -> h_ORL x_18050
     2459| XRL x_18051 -> h_XRL x_18051
     2460| CLR x_18052 -> h_CLR x_18052
     2461| CPL x_18053 -> h_CPL x_18053
     2462| RL x_18054 -> h_RL x_18054
     2463| RLC x_18055 -> h_RLC x_18055
     2464| RR x_18056 -> h_RR x_18056
     2465| RRC x_18057 -> h_RRC x_18057
     2466| SWAP x_18058 -> h_SWAP x_18058
     2467| MOV x_18059 -> h_MOV x_18059
     2468| MOVX x_18060 -> h_MOVX x_18060
     2469| SETB x_18061 -> h_SETB x_18061
     2470| PUSH x_18062 -> h_PUSH x_18062
     2471| POP x_18063 -> h_POP x_18063
     2472| XCH (x_18065, x_18064) -> h_XCH x_18065 x_18064
     2473| XCHD (x_18067, x_18066) -> h_XCHD x_18067 x_18066
    24782474| RET -> h_RET
    24792475| RETI -> h_RETI
    24802476| NOP -> h_NOP
    2481 | JMP x_22758 -> h_JMP x_22758
     2477| JMP x_18068 -> h_JMP x_18068
    24822478
    24832479(** val preinstruction_rect_Type2 :
     
    25172513    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    25182514let 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
    2519 | ADD (x_22799, x_22798) -> h_ADD x_22799 x_22798
    2520 | ADDC (x_22801, x_22800) -> h_ADDC x_22801 x_22800
    2521 | SUBB (x_22803, x_22802) -> h_SUBB x_22803 x_22802
    2522 | INC x_22804 -> h_INC x_22804
    2523 | DEC x_22805 -> h_DEC x_22805
    2524 | MUL (x_22807, x_22806) -> h_MUL x_22807 x_22806
    2525 | DIV (x_22809, x_22808) -> h_DIV x_22809 x_22808
    2526 | DA x_22810 -> h_DA x_22810
    2527 | JC x_22811 -> h_JC x_22811
    2528 | JNC x_22812 -> h_JNC x_22812
    2529 | JB (x_22814, x_22813) -> h_JB x_22814 x_22813
    2530 | JNB (x_22816, x_22815) -> h_JNB x_22816 x_22815
    2531 | JBC (x_22818, x_22817) -> h_JBC x_22818 x_22817
    2532 | JZ x_22819 -> h_JZ x_22819
    2533 | JNZ x_22820 -> h_JNZ x_22820
    2534 | CJNE (x_22822, x_22821) -> h_CJNE x_22822 x_22821
    2535 | DJNZ (x_22824, x_22823) -> h_DJNZ x_22824 x_22823
    2536 | ANL x_22825 -> h_ANL x_22825
    2537 | ORL x_22826 -> h_ORL x_22826
    2538 | XRL x_22827 -> h_XRL x_22827
    2539 | CLR x_22828 -> h_CLR x_22828
    2540 | CPL x_22829 -> h_CPL x_22829
    2541 | RL x_22830 -> h_RL x_22830
    2542 | RLC x_22831 -> h_RLC x_22831
    2543 | RR x_22832 -> h_RR x_22832
    2544 | RRC x_22833 -> h_RRC x_22833
    2545 | SWAP x_22834 -> h_SWAP x_22834
    2546 | MOV x_22835 -> h_MOV x_22835
    2547 | MOVX x_22836 -> h_MOVX x_22836
    2548 | SETB x_22837 -> h_SETB x_22837
    2549 | PUSH x_22838 -> h_PUSH x_22838
    2550 | POP x_22839 -> h_POP x_22839
    2551 | XCH (x_22841, x_22840) -> h_XCH x_22841 x_22840
    2552 | XCHD (x_22843, x_22842) -> h_XCHD x_22843 x_22842
     2515| ADD (x_18109, x_18108) -> h_ADD x_18109 x_18108
     2516| ADDC (x_18111, x_18110) -> h_ADDC x_18111 x_18110
     2517| SUBB (x_18113, x_18112) -> h_SUBB x_18113 x_18112
     2518| INC x_18114 -> h_INC x_18114
     2519| DEC x_18115 -> h_DEC x_18115
     2520| MUL (x_18117, x_18116) -> h_MUL x_18117 x_18116
     2521| DIV (x_18119, x_18118) -> h_DIV x_18119 x_18118
     2522| DA x_18120 -> h_DA x_18120
     2523| JC x_18121 -> h_JC x_18121
     2524| JNC x_18122 -> h_JNC x_18122
     2525| JB (x_18124, x_18123) -> h_JB x_18124 x_18123
     2526| JNB (x_18126, x_18125) -> h_JNB x_18126 x_18125
     2527| JBC (x_18128, x_18127) -> h_JBC x_18128 x_18127
     2528| JZ x_18129 -> h_JZ x_18129
     2529| JNZ x_18130 -> h_JNZ x_18130
     2530| CJNE (x_18132, x_18131) -> h_CJNE x_18132 x_18131
     2531| DJNZ (x_18134, x_18133) -> h_DJNZ x_18134 x_18133
     2532| ANL x_18135 -> h_ANL x_18135
     2533| ORL x_18136 -> h_ORL x_18136
     2534| XRL x_18137 -> h_XRL x_18137
     2535| CLR x_18138 -> h_CLR x_18138
     2536| CPL x_18139 -> h_CPL x_18139
     2537| RL x_18140 -> h_RL x_18140
     2538| RLC x_18141 -> h_RLC x_18141
     2539| RR x_18142 -> h_RR x_18142
     2540| RRC x_18143 -> h_RRC x_18143
     2541| SWAP x_18144 -> h_SWAP x_18144
     2542| MOV x_18145 -> h_MOV x_18145
     2543| MOVX x_18146 -> h_MOVX x_18146
     2544| SETB x_18147 -> h_SETB x_18147
     2545| PUSH x_18148 -> h_PUSH x_18148
     2546| POP x_18149 -> h_POP x_18149
     2547| XCH (x_18151, x_18150) -> h_XCH x_18151 x_18150
     2548| XCHD (x_18153, x_18152) -> h_XCHD x_18153 x_18152
    25532549| RET -> h_RET
    25542550| RETI -> h_RETI
    25552551| NOP -> h_NOP
    2556 | JMP x_22844 -> h_JMP x_22844
     2552| JMP x_18154 -> h_JMP x_18154
    25572553
    25582554(** val preinstruction_rect_Type1 :
     
    25922588    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    25932589let 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
    2594 | ADD (x_22885, x_22884) -> h_ADD x_22885 x_22884
    2595 | ADDC (x_22887, x_22886) -> h_ADDC x_22887 x_22886
    2596 | SUBB (x_22889, x_22888) -> h_SUBB x_22889 x_22888
    2597 | INC x_22890 -> h_INC x_22890
    2598 | DEC x_22891 -> h_DEC x_22891
    2599 | MUL (x_22893, x_22892) -> h_MUL x_22893 x_22892
    2600 | DIV (x_22895, x_22894) -> h_DIV x_22895 x_22894
    2601 | DA x_22896 -> h_DA x_22896
    2602 | JC x_22897 -> h_JC x_22897
    2603 | JNC x_22898 -> h_JNC x_22898
    2604 | JB (x_22900, x_22899) -> h_JB x_22900 x_22899
    2605 | JNB (x_22902, x_22901) -> h_JNB x_22902 x_22901
    2606 | JBC (x_22904, x_22903) -> h_JBC x_22904 x_22903
    2607 | JZ x_22905 -> h_JZ x_22905
    2608 | JNZ x_22906 -> h_JNZ x_22906
    2609 | CJNE (x_22908, x_22907) -> h_CJNE x_22908 x_22907
    2610 | DJNZ (x_22910, x_22909) -> h_DJNZ x_22910 x_22909
    2611 | ANL x_22911 -> h_ANL x_22911
    2612 | ORL x_22912 -> h_ORL x_22912
    2613 | XRL x_22913 -> h_XRL x_22913
    2614 | CLR x_22914 -> h_CLR x_22914
    2615 | CPL x_22915 -> h_CPL x_22915
    2616 | RL x_22916 -> h_RL x_22916
    2617 | RLC x_22917 -> h_RLC x_22917
    2618 | RR x_22918 -> h_RR x_22918
    2619 | RRC x_22919 -> h_RRC x_22919
    2620 | SWAP x_22920 -> h_SWAP x_22920
    2621 | MOV x_22921 -> h_MOV x_22921
    2622 | MOVX x_22922 -> h_MOVX x_22922
    2623 | SETB x_22923 -> h_SETB x_22923
    2624 | PUSH x_22924 -> h_PUSH x_22924
    2625 | POP x_22925 -> h_POP x_22925
    2626 | XCH (x_22927, x_22926) -> h_XCH x_22927 x_22926
    2627 | XCHD (x_22929, x_22928) -> h_XCHD x_22929 x_22928
     2590| ADD (x_18195, x_18194) -> h_ADD x_18195 x_18194
     2591| ADDC (x_18197, x_18196) -> h_ADDC x_18197 x_18196
     2592| SUBB (x_18199, x_18198) -> h_SUBB x_18199 x_18198
     2593| INC x_18200 -> h_INC x_18200
     2594| DEC x_18201 -> h_DEC x_18201
     2595| MUL (x_18203, x_18202) -> h_MUL x_18203 x_18202
     2596| DIV (x_18205, x_18204) -> h_DIV x_18205 x_18204
     2597| DA x_18206 -> h_DA x_18206
     2598| JC x_18207 -> h_JC x_18207
     2599| JNC x_18208 -> h_JNC x_18208
     2600| JB (x_18210, x_18209) -> h_JB x_18210 x_18209
     2601| JNB (x_18212, x_18211) -> h_JNB x_18212 x_18211
     2602| JBC (x_18214, x_18213) -> h_JBC x_18214 x_18213
     2603| JZ x_18215 -> h_JZ x_18215
     2604| JNZ x_18216 -> h_JNZ x_18216
     2605| CJNE (x_18218, x_18217) -> h_CJNE x_18218 x_18217
     2606| DJNZ (x_18220, x_18219) -> h_DJNZ x_18220 x_18219
     2607| ANL x_18221 -> h_ANL x_18221
     2608| ORL x_18222 -> h_ORL x_18222
     2609| XRL x_18223 -> h_XRL x_18223
     2610| CLR x_18224 -> h_CLR x_18224
     2611| CPL x_18225 -> h_CPL x_18225
     2612| RL x_18226 -> h_RL x_18226
     2613| RLC x_18227 -> h_RLC x_18227
     2614| RR x_18228 -> h_RR x_18228
     2615| RRC x_18229 -> h_RRC x_18229
     2616| SWAP x_18230 -> h_SWAP x_18230
     2617| MOV x_18231 -> h_MOV x_18231
     2618| MOVX x_18232 -> h_MOVX x_18232
     2619| SETB x_18233 -> h_SETB x_18233
     2620| PUSH x_18234 -> h_PUSH x_18234
     2621| POP x_18235 -> h_POP x_18235
     2622| XCH (x_18237, x_18236) -> h_XCH x_18237 x_18236
     2623| XCHD (x_18239, x_18238) -> h_XCHD x_18239 x_18238
    26282624| RET -> h_RET
    26292625| RETI -> h_RETI
    26302626| NOP -> h_NOP
    2631 | JMP x_22930 -> h_JMP x_22930
     2627| JMP x_18240 -> h_JMP x_18240
    26322628
    26332629(** val preinstruction_rect_Type0 :
     
    26672663    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    26682664let 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
    2669 | ADD (x_22971, x_22970) -> h_ADD x_22971 x_22970
    2670 | ADDC (x_22973, x_22972) -> h_ADDC x_22973 x_22972
    2671 | SUBB (x_22975, x_22974) -> h_SUBB x_22975 x_22974
    2672 | INC x_22976 -> h_INC x_22976
    2673 | DEC x_22977 -> h_DEC x_22977
    2674 | MUL (x_22979, x_22978) -> h_MUL x_22979 x_22978
    2675 | DIV (x_22981, x_22980) -> h_DIV x_22981 x_22980
    2676 | DA x_22982 -> h_DA x_22982
    2677 | JC x_22983 -> h_JC x_22983
    2678 | JNC x_22984 -> h_JNC x_22984
    2679 | JB (x_22986, x_22985) -> h_JB x_22986 x_22985
    2680 | JNB (x_22988, x_22987) -> h_JNB x_22988 x_22987
    2681 | JBC (x_22990, x_22989) -> h_JBC x_22990 x_22989
    2682 | JZ x_22991 -> h_JZ x_22991
    2683 | JNZ x_22992 -> h_JNZ x_22992
    2684 | CJNE (x_22994, x_22993) -> h_CJNE x_22994 x_22993
    2685 | DJNZ (x_22996, x_22995) -> h_DJNZ x_22996 x_22995
    2686 | ANL x_22997 -> h_ANL x_22997
    2687 | ORL x_22998 -> h_ORL x_22998
    2688 | XRL x_22999 -> h_XRL x_22999
    2689 | CLR x_23000 -> h_CLR x_23000
    2690 | CPL x_23001 -> h_CPL x_23001
    2691 | RL x_23002 -> h_RL x_23002
    2692 | RLC x_23003 -> h_RLC x_23003
    2693 | RR x_23004 -> h_RR x_23004
    2694 | RRC x_23005 -> h_RRC x_23005
    2695 | SWAP x_23006 -> h_SWAP x_23006
    2696 | MOV x_23007 -> h_MOV x_23007
    2697 | MOVX x_23008 -> h_MOVX x_23008
    2698 | SETB x_23009 -> h_SETB x_23009
    2699 | PUSH x_23010 -> h_PUSH x_23010
    2700 | POP x_23011 -> h_POP x_23011
    2701 | XCH (x_23013, x_23012) -> h_XCH x_23013 x_23012
    2702 | XCHD (x_23015, x_23014) -> h_XCHD x_23015 x_23014
     2665| ADD (x_18281, x_18280) -> h_ADD x_18281 x_18280
     2666| ADDC (x_18283, x_18282) -> h_ADDC x_18283 x_18282
     2667| SUBB (x_18285, x_18284) -> h_SUBB x_18285 x_18284
     2668| INC x_18286 -> h_INC x_18286
     2669| DEC x_18287 -> h_DEC x_18287
     2670| MUL (x_18289, x_18288) -> h_MUL x_18289 x_18288
     2671| DIV (x_18291, x_18290) -> h_DIV x_18291 x_18290
     2672| DA x_18292 -> h_DA x_18292
     2673| JC x_18293 -> h_JC x_18293
     2674| JNC x_18294 -> h_JNC x_18294
     2675| JB (x_18296, x_18295) -> h_JB x_18296 x_18295
     2676| JNB (x_18298, x_18297) -> h_JNB x_18298 x_18297
     2677| JBC (x_18300, x_18299) -> h_JBC x_18300 x_18299
     2678| JZ x_18301 -> h_JZ x_18301
     2679| JNZ x_18302 -> h_JNZ x_18302
     2680| CJNE (x_18304, x_18303) -> h_CJNE x_18304 x_18303
     2681| DJNZ (x_18306, x_18305) -> h_DJNZ x_18306 x_18305
     2682| ANL x_18307 -> h_ANL x_18307
     2683| ORL x_18308 -> h_ORL x_18308
     2684| XRL x_18309 -> h_XRL x_18309
     2685| CLR x_18310 -> h_CLR x_18310
     2686| CPL x_18311 -> h_CPL x_18311
     2687| RL x_18312 -> h_RL x_18312
     2688| RLC x_18313 -> h_RLC x_18313
     2689| RR x_18314 -> h_RR x_18314
     2690| RRC x_18315 -> h_RRC x_18315
     2691| SWAP x_18316 -> h_SWAP x_18316
     2692| MOV x_18317 -> h_MOV x_18317
     2693| MOVX x_18318 -> h_MOVX x_18318
     2694| SETB x_18319 -> h_SETB x_18319
     2695| PUSH x_18320 -> h_PUSH x_18320
     2696| POP x_18321 -> h_POP x_18321
     2697| XCH (x_18323, x_18322) -> h_XCH x_18323 x_18322
     2698| XCHD (x_18325, x_18324) -> h_XCHD x_18325 x_18324
    27032699| RET -> h_RET
    27042700| RETI -> h_RETI
    27052701| NOP -> h_NOP
    2706 | JMP x_23016 -> h_JMP x_23016
     2702| JMP x_18326 -> h_JMP x_18326
    27072703
    27082704(** val preinstruction_inv_rect_Type4 :
     
    51085104    'a1 **)
    51095105let rec instruction_rect_Type4 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5110 | ACALL x_23588 -> h_ACALL x_23588
    5111 | LCALL x_23589 -> h_LCALL x_23589
    5112 | AJMP x_23590 -> h_AJMP x_23590
    5113 | LJMP x_23591 -> h_LJMP x_23591
    5114 | SJMP x_23592 -> h_SJMP x_23592
    5115 | MOVC (x_23594, x_23593) -> h_MOVC x_23594 x_23593
    5116 | RealInstruction x_23595 -> h_RealInstruction x_23595
     5106| ACALL x_18898 -> h_ACALL x_18898
     5107| LCALL x_18899 -> h_LCALL x_18899
     5108| AJMP x_18900 -> h_AJMP x_18900
     5109| LJMP x_18901 -> h_LJMP x_18901
     5110| SJMP x_18902 -> h_SJMP x_18902
     5111| MOVC (x_18904, x_18903) -> h_MOVC x_18904 x_18903
     5112| RealInstruction x_18905 -> h_RealInstruction x_18905
    51175113
    51185114(** val instruction_rect_Type5 :
     
    51235119    'a1 **)
    51245120let rec instruction_rect_Type5 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5125 | ACALL x_23604 -> h_ACALL x_23604
    5126 | LCALL x_23605 -> h_LCALL x_23605
    5127 | AJMP x_23606 -> h_AJMP x_23606
    5128 | LJMP x_23607 -> h_LJMP x_23607
    5129 | SJMP x_23608 -> h_SJMP x_23608
    5130 | MOVC (x_23610, x_23609) -> h_MOVC x_23610 x_23609
    5131 | RealInstruction x_23611 -> h_RealInstruction x_23611
     5121| ACALL x_18914 -> h_ACALL x_18914
     5122| LCALL x_18915 -> h_LCALL x_18915
     5123| AJMP x_18916 -> h_AJMP x_18916
     5124| LJMP x_18917 -> h_LJMP x_18917
     5125| SJMP x_18918 -> h_SJMP x_18918
     5126| MOVC (x_18920, x_18919) -> h_MOVC x_18920 x_18919
     5127| RealInstruction x_18921 -> h_RealInstruction x_18921
    51325128
    51335129(** val instruction_rect_Type3 :
     
    51385134    'a1 **)
    51395135let rec instruction_rect_Type3 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5140 | ACALL x_23620 -> h_ACALL x_23620
    5141 | LCALL x_23621 -> h_LCALL x_23621
    5142 | AJMP x_23622 -> h_AJMP x_23622
    5143 | LJMP x_23623 -> h_LJMP x_23623
    5144 | SJMP x_23624 -> h_SJMP x_23624
    5145 | MOVC (x_23626, x_23625) -> h_MOVC x_23626 x_23625
    5146 | RealInstruction x_23627 -> h_RealInstruction x_23627
     5136| ACALL x_18930 -> h_ACALL x_18930
     5137| LCALL x_18931 -> h_LCALL x_18931
     5138| AJMP x_18932 -> h_AJMP x_18932
     5139| LJMP x_18933 -> h_LJMP x_18933
     5140| SJMP x_18934 -> h_SJMP x_18934
     5141| MOVC (x_18936, x_18935) -> h_MOVC x_18936 x_18935
     5142| RealInstruction x_18937 -> h_RealInstruction x_18937
    51475143
    51485144(** val instruction_rect_Type2 :
     
    51535149    'a1 **)
    51545150let rec instruction_rect_Type2 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5155 | ACALL x_23636 -> h_ACALL x_23636
    5156 | LCALL x_23637 -> h_LCALL x_23637
    5157 | AJMP x_23638 -> h_AJMP x_23638
    5158 | LJMP x_23639 -> h_LJMP x_23639
    5159 | SJMP x_23640 -> h_SJMP x_23640
    5160 | MOVC (x_23642, x_23641) -> h_MOVC x_23642 x_23641
    5161 | RealInstruction x_23643 -> h_RealInstruction x_23643
     5151| ACALL x_18946 -> h_ACALL x_18946
     5152| LCALL x_18947 -> h_LCALL x_18947
     5153| AJMP x_18948 -> h_AJMP x_18948
     5154| LJMP x_18949 -> h_LJMP x_18949
     5155| SJMP x_18950 -> h_SJMP x_18950
     5156| MOVC (x_18952, x_18951) -> h_MOVC x_18952 x_18951
     5157| RealInstruction x_18953 -> h_RealInstruction x_18953
    51625158
    51635159(** val instruction_rect_Type1 :
     
    51685164    'a1 **)
    51695165let rec instruction_rect_Type1 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5170 | ACALL x_23652 -> h_ACALL x_23652
    5171 | LCALL x_23653 -> h_LCALL x_23653
    5172 | AJMP x_23654 -> h_AJMP x_23654
    5173 | LJMP x_23655 -> h_LJMP x_23655
    5174 | SJMP x_23656 -> h_SJMP x_23656
    5175 | MOVC (x_23658, x_23657) -> h_MOVC x_23658 x_23657
    5176 | RealInstruction x_23659 -> h_RealInstruction x_23659
     5166| ACALL x_18962 -> h_ACALL x_18962
     5167| LCALL x_18963 -> h_LCALL x_18963
     5168| AJMP x_18964 -> h_AJMP x_18964
     5169| LJMP x_18965 -> h_LJMP x_18965
     5170| SJMP x_18966 -> h_SJMP x_18966
     5171| MOVC (x_18968, x_18967) -> h_MOVC x_18968 x_18967
     5172| RealInstruction x_18969 -> h_RealInstruction x_18969
    51775173
    51785174(** val instruction_rect_Type0 :
     
    51835179    'a1 **)
    51845180let rec instruction_rect_Type0 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5185 | ACALL x_23668 -> h_ACALL x_23668
    5186 | LCALL x_23669 -> h_LCALL x_23669
    5187 | AJMP x_23670 -> h_AJMP x_23670
    5188 | LJMP x_23671 -> h_LJMP x_23671
    5189 | SJMP x_23672 -> h_SJMP x_23672
    5190 | MOVC (x_23674, x_23673) -> h_MOVC x_23674 x_23673
    5191 | RealInstruction x_23675 -> h_RealInstruction x_23675
     5181| ACALL x_18978 -> h_ACALL x_18978
     5182| LCALL x_18979 -> h_LCALL x_18979
     5183| AJMP x_18980 -> h_AJMP x_18980
     5184| LJMP x_18981 -> h_LJMP x_18981
     5185| SJMP x_18982 -> h_SJMP x_18982
     5186| MOVC (x_18984, x_18983) -> h_MOVC x_18984 x_18983
     5187| RealInstruction x_18985 -> h_RealInstruction x_18985
    51925188
    51935189(** val instruction_inv_rect_Type4 :
     
    54635459
    54645460type pseudo_instruction =
    5465 | Instruction of identifier0 preinstruction
     5461| Instruction of identifier preinstruction
    54665462| Comment of String.string
    54675463| Cost of CostLabel.costlabel
    5468 | Jmp of identifier0
    5469 | Jnz of subaddressing_mode * identifier0 * identifier0
    5470 | MovSuccessor of subaddressing_mode * word_side * identifier0
    5471 | Call of identifier0
    5472 | Mov of subaddressing_mode * identifier0
     5464| Jmp of identifier
     5465| Jnz of subaddressing_mode * identifier * identifier
     5466| MovSuccessor of subaddressing_mode * word_side * identifier
     5467| Call of identifier
     5468| Mov of subaddressing_mode * identifier
    54735469
    54745470(** val pseudo_instruction_rect_Type4 :
    5475     (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5476     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
    5477     (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
    5478     (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
    5479     -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
    5480     pseudo_instruction -> 'a1 **)
     5471    (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     5472    (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) ->
     5473    (subaddressing_mode -> identifier -> identifier -> 'a1) ->
     5474    (subaddressing_mode -> word_side -> identifier -> 'a1) -> (identifier ->
     5475    'a1) -> (subaddressing_mode -> identifier -> 'a1) -> pseudo_instruction
     5476    -> 'a1 **)
    54815477let rec pseudo_instruction_rect_Type4 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5482 | Instruction x_23841 -> h_Instruction x_23841
    5483 | Comment x_23842 -> h_Comment x_23842
    5484 | Cost x_23843 -> h_Cost x_23843
    5485 | Jmp x_23844 -> h_Jmp x_23844
    5486 | Jnz (x_23847, x_23846, x_23845) -> h_Jnz x_23847 x_23846 x_23845
    5487 | MovSuccessor (x_23850, x_23849, x_23848) ->
    5488   h_MovSuccessor x_23850 x_23849 x_23848
    5489 | Call x_23851 -> h_Call x_23851
    5490 | Mov (x_23853, x_23852) -> h_Mov x_23853 x_23852
     5478| Instruction x_19151 -> h_Instruction x_19151
     5479| Comment x_19152 -> h_Comment x_19152
     5480| Cost x_19153 -> h_Cost x_19153
     5481| Jmp x_19154 -> h_Jmp x_19154
     5482| Jnz (x_19157, x_19156, x_19155) -> h_Jnz x_19157 x_19156 x_19155
     5483| MovSuccessor (x_19160, x_19159, x_19158) ->
     5484  h_MovSuccessor x_19160 x_19159 x_19158
     5485| Call x_19161 -> h_Call x_19161
     5486| Mov (x_19163, x_19162) -> h_Mov x_19163 x_19162
    54915487
    54925488(** val pseudo_instruction_rect_Type5 :
    5493     (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5494     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
    5495     (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
    5496     (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
    5497     -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
    5498     pseudo_instruction -> 'a1 **)
     5489    (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     5490    (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) ->
     5491    (subaddressing_mode -> identifier -> identifier -> 'a1) ->
     5492    (subaddressing_mode -> word_side -> identifier -> 'a1) -> (identifier ->
     5493    'a1) -> (subaddressing_mode -> identifier -> 'a1) -> pseudo_instruction
     5494    -> 'a1 **)
    54995495let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5500 | Instruction x_23863 -> h_Instruction x_23863
    5501 | Comment x_23864 -> h_Comment x_23864
    5502 | Cost x_23865 -> h_Cost x_23865
    5503 | Jmp x_23866 -> h_Jmp x_23866
    5504 | Jnz (x_23869, x_23868, x_23867) -> h_Jnz x_23869 x_23868 x_23867
    5505 | MovSuccessor (x_23872, x_23871, x_23870) ->
    5506   h_MovSuccessor x_23872 x_23871 x_23870
    5507 | Call x_23873 -> h_Call x_23873
    5508 | Mov (x_23875, x_23874) -> h_Mov x_23875 x_23874
     5496| Instruction x_19173 -> h_Instruction x_19173
     5497| Comment x_19174 -> h_Comment x_19174
     5498| Cost x_19175 -> h_Cost x_19175
     5499| Jmp x_19176 -> h_Jmp x_19176
     5500| Jnz (x_19179, x_19178, x_19177) -> h_Jnz x_19179 x_19178 x_19177
     5501| MovSuccessor (x_19182, x_19181, x_19180) ->
     5502  h_MovSuccessor x_19182 x_19181 x_19180
     5503| Call x_19183 -> h_Call x_19183
     5504| Mov (x_19185, x_19184) -> h_Mov x_19185 x_19184
    55095505
    55105506(** val pseudo_instruction_rect_Type3 :
    5511     (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5512     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
    5513     (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
    5514     (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
    5515     -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
    5516     pseudo_instruction -> 'a1 **)
     5507    (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     5508    (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) ->
     5509    (subaddressing_mode -> identifier -> identifier -> 'a1) ->
     5510    (subaddressing_mode -> word_side -> identifier -> 'a1) -> (identifier ->
     5511    'a1) -> (subaddressing_mode -> identifier -> 'a1) -> pseudo_instruction
     5512    -> 'a1 **)
    55175513let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5518 | Instruction x_23885 -> h_Instruction x_23885
    5519 | Comment x_23886 -> h_Comment x_23886
    5520 | Cost x_23887 -> h_Cost x_23887
    5521 | Jmp x_23888 -> h_Jmp x_23888
    5522 | Jnz (x_23891, x_23890, x_23889) -> h_Jnz x_23891 x_23890 x_23889
    5523 | MovSuccessor (x_23894, x_23893, x_23892) ->
    5524   h_MovSuccessor x_23894 x_23893 x_23892
    5525 | Call x_23895 -> h_Call x_23895
    5526 | Mov (x_23897, x_23896) -> h_Mov x_23897 x_23896
     5514| Instruction x_19195 -> h_Instruction x_19195
     5515| Comment x_19196 -> h_Comment x_19196
     5516| Cost x_19197 -> h_Cost x_19197
     5517| Jmp x_19198 -> h_Jmp x_19198
     5518| Jnz (x_19201, x_19200, x_19199) -> h_Jnz x_19201 x_19200 x_19199
     5519| MovSuccessor (x_19204, x_19203, x_19202) ->
     5520  h_MovSuccessor x_19204 x_19203 x_19202
     5521| Call x_19205 -> h_Call x_19205
     5522| Mov (x_19207, x_19206) -> h_Mov x_19207 x_19206
    55275523
    55285524(** val pseudo_instruction_rect_Type2 :
    5529     (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5530     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
    5531     (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
    5532     (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
    5533     -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
    5534     pseudo_instruction -> 'a1 **)
     5525    (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     5526    (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) ->
     5527    (subaddressing_mode -> identifier -> identifier -> 'a1) ->
     5528    (subaddressing_mode -> word_side -> identifier -> 'a1) -> (identifier ->
     5529    'a1) -> (subaddressing_mode -> identifier -> 'a1) -> pseudo_instruction
     5530    -> 'a1 **)
    55355531let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5536 | Instruction x_23907 -> h_Instruction x_23907
    5537 | Comment x_23908 -> h_Comment x_23908
    5538 | Cost x_23909 -> h_Cost x_23909
    5539 | Jmp x_23910 -> h_Jmp x_23910
    5540 | Jnz (x_23913, x_23912, x_23911) -> h_Jnz x_23913 x_23912 x_23911
    5541 | MovSuccessor (x_23916, x_23915, x_23914) ->
    5542   h_MovSuccessor x_23916 x_23915 x_23914
    5543 | Call x_23917 -> h_Call x_23917
    5544 | Mov (x_23919, x_23918) -> h_Mov x_23919 x_23918
     5532| Instruction x_19217 -> h_Instruction x_19217
     5533| Comment x_19218 -> h_Comment x_19218
     5534| Cost x_19219 -> h_Cost x_19219
     5535| Jmp x_19220 -> h_Jmp x_19220
     5536| Jnz (x_19223, x_19222, x_19221) -> h_Jnz x_19223 x_19222 x_19221
     5537| MovSuccessor (x_19226, x_19225, x_19224) ->
     5538  h_MovSuccessor x_19226 x_19225 x_19224
     5539| Call x_19227 -> h_Call x_19227
     5540| Mov (x_19229, x_19228) -> h_Mov x_19229 x_19228
    55455541
    55465542(** val pseudo_instruction_rect_Type1 :
    5547     (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5548     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
    5549     (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
    5550     (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
    5551     -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
    5552     pseudo_instruction -> 'a1 **)
     5543    (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     5544    (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) ->
     5545    (subaddressing_mode -> identifier -> identifier -> 'a1) ->
     5546    (subaddressing_mode -> word_side -> identifier -> 'a1) -> (identifier ->
     5547    'a1) -> (subaddressing_mode -> identifier -> 'a1) -> pseudo_instruction
     5548    -> 'a1 **)
    55535549let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5554 | Instruction x_23929 -> h_Instruction x_23929
    5555 | Comment x_23930 -> h_Comment x_23930
    5556 | Cost x_23931 -> h_Cost x_23931
    5557 | Jmp x_23932 -> h_Jmp x_23932
    5558 | Jnz (x_23935, x_23934, x_23933) -> h_Jnz x_23935 x_23934 x_23933
    5559 | MovSuccessor (x_23938, x_23937, x_23936) ->
    5560   h_MovSuccessor x_23938 x_23937 x_23936
    5561 | Call x_23939 -> h_Call x_23939
    5562 | Mov (x_23941, x_23940) -> h_Mov x_23941 x_23940
     5550| Instruction x_19239 -> h_Instruction x_19239
     5551| Comment x_19240 -> h_Comment x_19240
     5552| Cost x_19241 -> h_Cost x_19241
     5553| Jmp x_19242 -> h_Jmp x_19242
     5554| Jnz (x_19245, x_19244, x_19243) -> h_Jnz x_19245 x_19244 x_19243
     5555| MovSuccessor (x_19248, x_19247, x_19246) ->
     5556  h_MovSuccessor x_19248 x_19247 x_19246
     5557| Call x_19249 -> h_Call x_19249
     5558| Mov (x_19251, x_19250) -> h_Mov x_19251 x_19250
    55635559
    55645560(** val pseudo_instruction_rect_Type0 :
    5565     (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    5566     (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) ->
    5567     (subaddressing_mode -> identifier0 -> identifier0 -> 'a1) ->
    5568     (subaddressing_mode -> word_side -> identifier0 -> 'a1) -> (identifier0
    5569     -> 'a1) -> (subaddressing_mode -> identifier0 -> 'a1) ->
    5570     pseudo_instruction -> 'a1 **)
     5561    (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     5562    (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) ->
     5563    (subaddressing_mode -> identifier -> identifier -> 'a1) ->
     5564    (subaddressing_mode -> word_side -> identifier -> 'a1) -> (identifier ->
     5565    'a1) -> (subaddressing_mode -> identifier -> 'a1) -> pseudo_instruction
     5566    -> 'a1 **)
    55715567let rec pseudo_instruction_rect_Type0 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5572 | Instruction x_23951 -> h_Instruction x_23951
    5573 | Comment x_23952 -> h_Comment x_23952
    5574 | Cost x_23953 -> h_Cost x_23953
    5575 | Jmp x_23954 -> h_Jmp x_23954
    5576 | Jnz (x_23957, x_23956, x_23955) -> h_Jnz x_23957 x_23956 x_23955
    5577 | MovSuccessor (x_23960, x_23959, x_23958) ->
    5578   h_MovSuccessor x_23960 x_23959 x_23958
    5579 | Call x_23961 -> h_Call x_23961
    5580 | Mov (x_23963, x_23962) -> h_Mov x_23963 x_23962
     5568| Instruction x_19261 -> h_Instruction x_19261
     5569| Comment x_19262 -> h_Comment x_19262
     5570| Cost x_19263 -> h_Cost x_19263
     5571| Jmp x_19264 -> h_Jmp x_19264
     5572| Jnz (x_19267, x_19266, x_19265) -> h_Jnz x_19267 x_19266 x_19265
     5573| MovSuccessor (x_19270, x_19269, x_19268) ->
     5574  h_MovSuccessor x_19270 x_19269 x_19268
     5575| Call x_19271 -> h_Call x_19271
     5576| Mov (x_19273, x_19272) -> h_Mov x_19273 x_19272
    55815577
    55825578(** val pseudo_instruction_inv_rect_Type4 :
    5583     pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
     5579    pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
    55845580    (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    5585     (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
    5586     identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
    5587     identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    5588     (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1 **)
     5581    (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
     5582    identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     5583    identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
     5584    (subaddressing_mode -> identifier -> __ -> 'a1) -> 'a1 **)
    55895585let pseudo_instruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    55905586  let hcut = pseudo_instruction_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 hterm in
     
    55925588
    55935589(** val pseudo_instruction_inv_rect_Type3 :
    5594     pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
     5590    pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
    55955591    (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    5596     (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
    5597     identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
    5598     identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    5599     (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1 **)
     5592    (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
     5593    identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     5594    identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
     5595    (subaddressing_mode -> identifier -> __ -> 'a1) -> 'a1 **)
    56005596let pseudo_instruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    56015597  let hcut = pseudo_instruction_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 hterm in
     
    56035599
    56045600(** val pseudo_instruction_inv_rect_Type2 :
    5605     pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
     5601    pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
    56065602    (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    5607     (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
    5608     identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
    5609     identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    5610     (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1 **)
     5603    (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
     5604    identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     5605    identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
     5606    (subaddressing_mode -> identifier -> __ -> 'a1) -> 'a1 **)
    56115607let pseudo_instruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    56125608  let hcut = pseudo_instruction_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 hterm in
     
    56145610
    56155611(** val pseudo_instruction_inv_rect_Type1 :
    5616     pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
     5612    pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
    56175613    (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    5618     (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
    5619     identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
    5620     identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    5621     (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1 **)
     5614    (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
     5615    identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     5616    identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
     5617    (subaddressing_mode -> identifier -> __ -> 'a1) -> 'a1 **)
    56225618let pseudo_instruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    56235619  let hcut = pseudo_instruction_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 hterm in
     
    56255621
    56265622(** val pseudo_instruction_inv_rect_Type0 :
    5627     pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
     5623    pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
    56285624    (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    5629     (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
    5630     identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
    5631     identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    5632     (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1 **)
     5625    (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
     5626    identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     5627    identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
     5628    (subaddressing_mode -> identifier -> __ -> 'a1) -> 'a1 **)
    56335629let pseudo_instruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    56345630  let hcut = pseudo_instruction_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 hterm in
     
    56655661type labelled_instruction = pseudo_instruction LabelledObjects.labelled_obj
    56665662
    5667 type preamble = (identifier0, BitVector.word) Types.prod List.list
    5668 
    56695663type assembly_program = instruction List.list
    56705664
    5671 type pseudo_assembly_program =
    5672   (preamble, labelled_instruction List.list) Types.prod
    5673 
    5674 (** val is_jump' : identifier0 preinstruction -> Bool.bool **)
     5665(** val fetch_pseudo_instruction :
     5666    labelled_instruction List.list -> BitVector.word -> (pseudo_instruction,
     5667    BitVector.word) Types.prod **)
     5668let fetch_pseudo_instruction code_mem pc =
     5669  let { Types.fst = lbl; Types.snd = instr } =
     5670    Util.nth_safe
     5671      (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5672        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5673        Nat.O)))))))))))))))) pc) code_mem
     5674  in
     5675  let new_pc =
     5676    Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5677      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5678      Nat.O)))))))))))))))) pc
     5679      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5680        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5681        Nat.O)))))))))))))))) (Nat.S Nat.O))
     5682  in
     5683  { Types.fst = instr; Types.snd = new_pc }
     5684
     5685(** val is_jump' : identifier preinstruction -> Bool.bool **)
    56755686let is_jump' = function
    56765687| ADD (x0, x1) -> Bool.False
     
    57465757| Mov (x, x0) -> Bool.False
    57475758
     5759(** val asm_cost_label :
     5760    labelled_instruction List.list -> BitVector.word Types.sig0 ->
     5761    CostLabel.costlabel Types.option **)
     5762let asm_cost_label mem w_prf =
     5763  match (fetch_pseudo_instruction mem (Types.pi1 w_prf)).Types.fst with
     5764  | Instruction x -> Types.None
     5765  | Comment x -> Types.None
     5766  | Cost c -> Types.Some c
     5767  | Jmp x -> Types.None
     5768  | Jnz (x, x0, x1) -> Types.None
     5769  | MovSuccessor (x, x0, x1) -> Types.None
     5770  | Call x -> Types.None
     5771  | Mov (x, x0) -> Types.None
     5772
     5773(** val aDDRESS_WIDTH : Nat.nat **)
     5774let aDDRESS_WIDTH =
     5775  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     5776    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))
     5777
     5778(** val mAX_CODE_SIZE : Nat.nat **)
     5779let mAX_CODE_SIZE =
     5780  Exp.exp (Nat.S (Nat.S Nat.O)) aDDRESS_WIDTH
     5781
     5782(** val code_size_opt : labelled_instruction List.list -> __ Types.option **)
     5783let code_size_opt code =
     5784  Extranat.nat_bound_opt mAX_CODE_SIZE (Nat.S (List.length code))
     5785
     5786type pseudo_assembly_program = { preamble : (identifier, BitVector.word)
     5787                                            Types.prod List.list;
     5788                                 code : labelled_instruction List.list;
     5789                                 renamed_symbols : (identifier, AST.ident)
     5790                                                   Types.prod List.list;
     5791                                 final_label : identifier }
     5792
     5793(** val pseudo_assembly_program_rect_Type4 :
     5794    ((identifier, BitVector.word) Types.prod List.list ->
     5795    labelled_instruction List.list -> __ -> (identifier, AST.ident)
     5796    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     5797    pseudo_assembly_program -> 'a1 **)
     5798let rec pseudo_assembly_program_rect_Type4 h_mk_pseudo_assembly_program x_19416 =
     5799  let { preamble = preamble0; code = code0; renamed_symbols =
     5800    renamed_symbols0; final_label = final_label0 } = x_19416
     5801  in
     5802  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     5803    final_label0 __ __
     5804
     5805(** val pseudo_assembly_program_rect_Type5 :
     5806    ((identifier, BitVector.word) Types.prod List.list ->
     5807    labelled_instruction List.list -> __ -> (identifier, AST.ident)
     5808    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     5809    pseudo_assembly_program -> 'a1 **)
     5810let rec pseudo_assembly_program_rect_Type5 h_mk_pseudo_assembly_program x_19418 =
     5811  let { preamble = preamble0; code = code0; renamed_symbols =
     5812    renamed_symbols0; final_label = final_label0 } = x_19418
     5813  in
     5814  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     5815    final_label0 __ __
     5816
     5817(** val pseudo_assembly_program_rect_Type3 :
     5818    ((identifier, BitVector.word) Types.prod List.list ->
     5819    labelled_instruction List.list -> __ -> (identifier, AST.ident)
     5820    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     5821    pseudo_assembly_program -> 'a1 **)
     5822let rec pseudo_assembly_program_rect_Type3 h_mk_pseudo_assembly_program x_19420 =
     5823  let { preamble = preamble0; code = code0; renamed_symbols =
     5824    renamed_symbols0; final_label = final_label0 } = x_19420
     5825  in
     5826  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     5827    final_label0 __ __
     5828
     5829(** val pseudo_assembly_program_rect_Type2 :
     5830    ((identifier, BitVector.word) Types.prod List.list ->
     5831    labelled_instruction List.list -> __ -> (identifier, AST.ident)
     5832    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     5833    pseudo_assembly_program -> 'a1 **)
     5834let rec pseudo_assembly_program_rect_Type2 h_mk_pseudo_assembly_program x_19422 =
     5835  let { preamble = preamble0; code = code0; renamed_symbols =
     5836    renamed_symbols0; final_label = final_label0 } = x_19422
     5837  in
     5838  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     5839    final_label0 __ __
     5840
     5841(** val pseudo_assembly_program_rect_Type1 :
     5842    ((identifier, BitVector.word) Types.prod List.list ->
     5843    labelled_instruction List.list -> __ -> (identifier, AST.ident)
     5844    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     5845    pseudo_assembly_program -> 'a1 **)
     5846let rec pseudo_assembly_program_rect_Type1 h_mk_pseudo_assembly_program x_19424 =
     5847  let { preamble = preamble0; code = code0; renamed_symbols =
     5848    renamed_symbols0; final_label = final_label0 } = x_19424
     5849  in
     5850  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     5851    final_label0 __ __
     5852
     5853(** val pseudo_assembly_program_rect_Type0 :
     5854    ((identifier, BitVector.word) Types.prod List.list ->
     5855    labelled_instruction List.list -> __ -> (identifier, AST.ident)
     5856    Types.prod List.list -> identifier -> __ -> __ -> 'a1) ->
     5857    pseudo_assembly_program -> 'a1 **)
     5858let rec pseudo_assembly_program_rect_Type0 h_mk_pseudo_assembly_program x_19426 =
     5859  let { preamble = preamble0; code = code0; renamed_symbols =
     5860    renamed_symbols0; final_label = final_label0 } = x_19426
     5861  in
     5862  h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0
     5863    final_label0 __ __
     5864
     5865(** val preamble :
     5866    pseudo_assembly_program -> (identifier, BitVector.word) Types.prod
     5867    List.list **)
     5868let rec preamble xxx =
     5869  xxx.preamble
     5870
     5871(** val code : pseudo_assembly_program -> labelled_instruction List.list **)
     5872let rec code xxx =
     5873  xxx.code
     5874
     5875(** val renamed_symbols :
     5876    pseudo_assembly_program -> (identifier, AST.ident) Types.prod List.list **)
     5877let rec renamed_symbols xxx =
     5878  xxx.renamed_symbols
     5879
     5880(** val final_label : pseudo_assembly_program -> identifier **)
     5881let rec final_label xxx =
     5882  xxx.final_label
     5883
     5884(** val pseudo_assembly_program_inv_rect_Type4 :
     5885    pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
     5886    List.list -> labelled_instruction List.list -> __ -> (identifier,
     5887    AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1)
     5888    -> 'a1 **)
     5889let pseudo_assembly_program_inv_rect_Type4 hterm h1 =
     5890  let hcut = pseudo_assembly_program_rect_Type4 h1 hterm in hcut __
     5891
     5892(** val pseudo_assembly_program_inv_rect_Type3 :
     5893    pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
     5894    List.list -> labelled_instruction List.list -> __ -> (identifier,
     5895    AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1)
     5896    -> 'a1 **)
     5897let pseudo_assembly_program_inv_rect_Type3 hterm h1 =
     5898  let hcut = pseudo_assembly_program_rect_Type3 h1 hterm in hcut __
     5899
     5900(** val pseudo_assembly_program_inv_rect_Type2 :
     5901    pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
     5902    List.list -> labelled_instruction List.list -> __ -> (identifier,
     5903    AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1)
     5904    -> 'a1 **)
     5905let pseudo_assembly_program_inv_rect_Type2 hterm h1 =
     5906  let hcut = pseudo_assembly_program_rect_Type2 h1 hterm in hcut __
     5907
     5908(** val pseudo_assembly_program_inv_rect_Type1 :
     5909    pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
     5910    List.list -> labelled_instruction List.list -> __ -> (identifier,
     5911    AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1)
     5912    -> 'a1 **)
     5913let pseudo_assembly_program_inv_rect_Type1 hterm h1 =
     5914  let hcut = pseudo_assembly_program_rect_Type1 h1 hterm in hcut __
     5915
     5916(** val pseudo_assembly_program_inv_rect_Type0 :
     5917    pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
     5918    List.list -> labelled_instruction List.list -> __ -> (identifier,
     5919    AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1)
     5920    -> 'a1 **)
     5921let pseudo_assembly_program_inv_rect_Type0 hterm h1 =
     5922  let hcut = pseudo_assembly_program_rect_Type0 h1 hterm in hcut __
     5923
     5924(** val pseudo_assembly_program_jmdiscr :
     5925    pseudo_assembly_program -> pseudo_assembly_program -> __ **)
     5926let pseudo_assembly_program_jmdiscr x y =
     5927  Logic.eq_rect_Type2 x
     5928    (let { preamble = a0; code = a1; renamed_symbols = a3; final_label =
     5929       a4 } = x
     5930     in
     5931    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
     5932
     5933type object_code = BitVector.byte List.list
     5934
     5935type costlabel_map = CostLabel.costlabel BitVectorTrie.bitVectorTrie
     5936
     5937type symboltable_type = AST.ident BitVectorTrie.bitVectorTrie
     5938
     5939type labelled_object_code = { oc : object_code; costlabels : costlabel_map;
     5940                              symboltable : symboltable_type;
     5941                              final_pc : BitVector.word }
     5942
     5943(** val labelled_object_code_rect_Type4 :
     5944    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     5945    -> 'a1) -> labelled_object_code -> 'a1 **)
     5946let rec labelled_object_code_rect_Type4 h_mk_labelled_object_code x_19442 =
     5947  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
     5948    final_pc = final_pc0 } = x_19442
     5949  in
     5950  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     5951
     5952(** val labelled_object_code_rect_Type5 :
     5953    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     5954    -> 'a1) -> labelled_object_code -> 'a1 **)
     5955let rec labelled_object_code_rect_Type5 h_mk_labelled_object_code x_19444 =
     5956  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
     5957    final_pc = final_pc0 } = x_19444
     5958  in
     5959  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     5960
     5961(** val labelled_object_code_rect_Type3 :
     5962    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     5963    -> 'a1) -> labelled_object_code -> 'a1 **)
     5964let rec labelled_object_code_rect_Type3 h_mk_labelled_object_code x_19446 =
     5965  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
     5966    final_pc = final_pc0 } = x_19446
     5967  in
     5968  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     5969
     5970(** val labelled_object_code_rect_Type2 :
     5971    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     5972    -> 'a1) -> labelled_object_code -> 'a1 **)
     5973let rec labelled_object_code_rect_Type2 h_mk_labelled_object_code x_19448 =
     5974  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
     5975    final_pc = final_pc0 } = x_19448
     5976  in
     5977  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     5978
     5979(** val labelled_object_code_rect_Type1 :
     5980    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     5981    -> 'a1) -> labelled_object_code -> 'a1 **)
     5982let rec labelled_object_code_rect_Type1 h_mk_labelled_object_code x_19450 =
     5983  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
     5984    final_pc = final_pc0 } = x_19450
     5985  in
     5986  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     5987
     5988(** val labelled_object_code_rect_Type0 :
     5989    (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     5990    -> 'a1) -> labelled_object_code -> 'a1 **)
     5991let rec labelled_object_code_rect_Type0 h_mk_labelled_object_code x_19452 =
     5992  let { oc = oc0; costlabels = costlabels0; symboltable = symboltable0;
     5993    final_pc = final_pc0 } = x_19452
     5994  in
     5995  h_mk_labelled_object_code oc0 costlabels0 symboltable0 final_pc0 __
     5996
     5997(** val oc : labelled_object_code -> object_code **)
     5998let rec oc xxx =
     5999  xxx.oc
     6000
     6001(** val costlabels : labelled_object_code -> costlabel_map **)
     6002let rec costlabels xxx =
     6003  xxx.costlabels
     6004
     6005(** val symboltable : labelled_object_code -> symboltable_type **)
     6006let rec symboltable xxx =
     6007  xxx.symboltable
     6008
     6009(** val final_pc : labelled_object_code -> BitVector.word **)
     6010let rec final_pc xxx =
     6011  xxx.final_pc
     6012
     6013(** val labelled_object_code_inv_rect_Type4 :
     6014    labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
     6015    -> BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
     6016let labelled_object_code_inv_rect_Type4 hterm h1 =
     6017  let hcut = labelled_object_code_rect_Type4 h1 hterm in hcut __
     6018
     6019(** val labelled_object_code_inv_rect_Type3 :
     6020    labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
     6021    -> BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
     6022let labelled_object_code_inv_rect_Type3 hterm h1 =
     6023  let hcut = labelled_object_code_rect_Type3 h1 hterm in hcut __
     6024
     6025(** val labelled_object_code_inv_rect_Type2 :
     6026    labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
     6027    -> BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
     6028let labelled_object_code_inv_rect_Type2 hterm h1 =
     6029  let hcut = labelled_object_code_rect_Type2 h1 hterm in hcut __
     6030
     6031(** val labelled_object_code_inv_rect_Type1 :
     6032    labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
     6033    -> BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
     6034let labelled_object_code_inv_rect_Type1 hterm h1 =
     6035  let hcut = labelled_object_code_rect_Type1 h1 hterm in hcut __
     6036
     6037(** val labelled_object_code_inv_rect_Type0 :
     6038    labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
     6039    -> BitVector.word -> __ -> __ -> 'a1) -> 'a1 **)
     6040let labelled_object_code_inv_rect_Type0 hterm h1 =
     6041  let hcut = labelled_object_code_rect_Type0 h1 hterm in hcut __
     6042
     6043(** val labelled_object_code_discr :
     6044    labelled_object_code -> labelled_object_code -> __ **)
     6045let labelled_object_code_discr x y =
     6046  Logic.eq_rect_Type2 x
     6047    (let { oc = a0; costlabels = a1; symboltable = a2; final_pc = a3 } = x in
     6048    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
     6049
     6050(** val labelled_object_code_jmdiscr :
     6051    labelled_object_code -> labelled_object_code -> __ **)
     6052let labelled_object_code_jmdiscr x y =
     6053  Logic.eq_rect_Type2 x
     6054    (let { oc = a0; costlabels = a1; symboltable = a2; final_pc = a3 } = x in
     6055    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
     6056
  • extracted/aSM.mli

    r2743 r2773  
    11open Preamble
    22
     3open Proper
     4
     5open PositiveMap
     6
     7open Deqsets
     8
     9open ErrorMessages
     10
     11open PreIdentifiers
     12
     13open Errors
     14
     15open Extralib
     16
     17open Setoids
     18
     19open Monad
     20
     21open Option
     22
     23open Div_and_mod
     24
     25open Jmeq
     26
     27open Russell
     28
     29open Util
     30
     31open List
     32
     33open Lists
     34
     35open Bool
     36
     37open Relations
     38
     39open Nat
     40
     41open Positive
     42
     43open Hints_declaration
     44
     45open Core_notation
     46
     47open Pts
     48
     49open Logic
     50
     51open Types
     52
     53open Identifiers
     54
     55open CostLabel
     56
     57open LabelledObjects
     58
     59open Exp
     60
     61open Arithmetic
     62
     63open Vector
     64
     65open FoldStuff
     66
     67open BitVector
     68
    369open Extranat
    470
    5 open Vector
    6 
    7 open Div_and_mod
    8 
    9 open Jmeq
    10 
    11 open Russell
    12 
    13 open Types
    14 
    15 open List
    16 
    17 open Util
    18 
    19 open FoldStuff
    20 
    21 open Bool
    22 
    23 open Hints_declaration
    24 
    25 open Core_notation
    26 
    27 open Pts
    28 
    29 open Logic
    30 
    31 open Relations
    32 
    33 open Nat
    34 
    35 open BitVector
    36 
    37 open Proper
    38 
    39 open PositiveMap
    40 
    41 open Deqsets
    42 
    43 open ErrorMessages
    44 
    45 open PreIdentifiers
    46 
    47 open Errors
    48 
    49 open Extralib
    50 
    51 open Setoids
    52 
    53 open Monad
    54 
    55 open Option
    56 
    57 open Lists
    58 
    59 open Positive
    60 
    61 open Identifiers
     71open Integers
     72
     73open AST
     74
     75open String
    6276
    6377open BitVectorTrie
    6478
    65 open Exp
    66 
    67 open Arithmetic
    68 
    69 open Integers
    70 
    71 open AST
    72 
    73 open CostLabel
    74 
    75 open LabelledObjects
    76 
    77 open String
    78 
    79 type identifier0 = PreIdentifiers.identifier
     79type identifier = PreIdentifiers.identifier
    8080
    8181val toASM_ident :
    82   PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier0
     82  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier
    8383
    8484type addressing_mode =
     
    296296val eq_a : addressing_mode_tag -> addressing_mode_tag -> Bool.bool
    297297
    298 type member_addressing_mode_tag = __
    299 
    300298val is_a : addressing_mode_tag -> addressing_mode -> Bool.bool
    301299
     
    490488  Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
    491489  -> subaddressing_mode
    492 
    493 type subaddressing_mode_elim_type = __
    494490
    495491type 'a preinstruction =
     
    10871083
    10881084type pseudo_instruction =
    1089 | Instruction of identifier0 preinstruction
     1085| Instruction of identifier preinstruction
    10901086| Comment of String.string
    10911087| Cost of CostLabel.costlabel
    1092 | Jmp of identifier0
    1093 | Jnz of subaddressing_mode * identifier0 * identifier0
    1094 | MovSuccessor of subaddressing_mode * word_side * identifier0
    1095 | Call of identifier0
    1096 | Mov of subaddressing_mode * identifier0
     1088| Jmp of identifier
     1089| Jnz of subaddressing_mode * identifier * identifier
     1090| MovSuccessor of subaddressing_mode * word_side * identifier
     1091| Call of identifier
     1092| Mov of subaddressing_mode * identifier
    10971093
    10981094val pseudo_instruction_rect_Type4 :
    1099   (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    1100   (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
    1101   -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
    1102   -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
    1103   identifier0 -> 'a1) -> pseudo_instruction -> 'a1
     1095  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     1096  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
     1097  -> identifier -> identifier -> 'a1) -> (subaddressing_mode -> word_side ->
     1098  identifier -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode ->
     1099  identifier -> 'a1) -> pseudo_instruction -> 'a1
    11041100
    11051101val pseudo_instruction_rect_Type5 :
    1106   (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    1107   (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
    1108   -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
    1109   -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
    1110   identifier0 -> 'a1) -> pseudo_instruction -> 'a1
     1102  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     1103  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
     1104  -> identifier -> identifier -> 'a1) -> (subaddressing_mode -> word_side ->
     1105  identifier -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode ->
     1106  identifier -> 'a1) -> pseudo_instruction -> 'a1
    11111107
    11121108val pseudo_instruction_rect_Type3 :
    1113   (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    1114   (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
    1115   -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
    1116   -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
    1117   identifier0 -> 'a1) -> pseudo_instruction -> 'a1
     1109  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     1110  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
     1111  -> identifier -> identifier -> 'a1) -> (subaddressing_mode -> word_side ->
     1112  identifier -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode ->
     1113  identifier -> 'a1) -> pseudo_instruction -> 'a1
    11181114
    11191115val pseudo_instruction_rect_Type2 :
    1120   (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    1121   (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
    1122   -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
    1123   -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
    1124   identifier0 -> 'a1) -> pseudo_instruction -> 'a1
     1116  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     1117  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
     1118  -> identifier -> identifier -> 'a1) -> (subaddressing_mode -> word_side ->
     1119  identifier -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode ->
     1120  identifier -> 'a1) -> pseudo_instruction -> 'a1
    11251121
    11261122val pseudo_instruction_rect_Type1 :
    1127   (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    1128   (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
    1129   -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
    1130   -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
    1131   identifier0 -> 'a1) -> pseudo_instruction -> 'a1
     1123  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     1124  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
     1125  -> identifier -> identifier -> 'a1) -> (subaddressing_mode -> word_side ->
     1126  identifier -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode ->
     1127  identifier -> 'a1) -> pseudo_instruction -> 'a1
    11321128
    11331129val pseudo_instruction_rect_Type0 :
    1134   (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    1135   (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
    1136   -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
    1137   -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
    1138   identifier0 -> 'a1) -> pseudo_instruction -> 'a1
     1130  (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
     1131  (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
     1132  -> identifier -> identifier -> 'a1) -> (subaddressing_mode -> word_side ->
     1133  identifier -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode ->
     1134  identifier -> 'a1) -> pseudo_instruction -> 'a1
    11391135
    11401136val pseudo_instruction_inv_rect_Type4 :
    1141   pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
     1137  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
    11421138  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    1143   (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
    1144   identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
    1145   identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    1146   (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
     1139  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
     1140  identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side -> identifier
     1141  -> __ -> 'a1) -> (identifier -> __ -> 'a1) -> (subaddressing_mode ->
     1142  identifier -> __ -> 'a1) -> 'a1
    11471143
    11481144val pseudo_instruction_inv_rect_Type3 :
    1149   pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
     1145  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
    11501146  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    1151   (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
    1152   identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
    1153   identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    1154   (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
     1147  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
     1148  identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side -> identifier
     1149  -> __ -> 'a1) -> (identifier -> __ -> 'a1) -> (subaddressing_mode ->
     1150  identifier -> __ -> 'a1) -> 'a1
    11551151
    11561152val pseudo_instruction_inv_rect_Type2 :
    1157   pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
     1153  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
    11581154  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    1159   (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
    1160   identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
    1161   identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    1162   (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
     1155  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
     1156  identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side -> identifier
     1157  -> __ -> 'a1) -> (identifier -> __ -> 'a1) -> (subaddressing_mode ->
     1158  identifier -> __ -> 'a1) -> 'a1
    11631159
    11641160val pseudo_instruction_inv_rect_Type1 :
    1165   pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
     1161  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
    11661162  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    1167   (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
    1168   identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
    1169   identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    1170   (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
     1163  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
     1164  identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side -> identifier
     1165  -> __ -> 'a1) -> (identifier -> __ -> 'a1) -> (subaddressing_mode ->
     1166  identifier -> __ -> 'a1) -> 'a1
    11711167
    11721168val pseudo_instruction_inv_rect_Type0 :
    1173   pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
     1169  pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
    11741170  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    1175   (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
    1176   identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
    1177   identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    1178   (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
     1171  (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
     1172  identifier -> __ -> 'a1) -> (subaddressing_mode -> word_side -> identifier
     1173  -> __ -> 'a1) -> (identifier -> __ -> 'a1) -> (subaddressing_mode ->
     1174  identifier -> __ -> 'a1) -> 'a1
    11791175
    11801176val pseudo_instruction_discr : pseudo_instruction -> pseudo_instruction -> __
     
    11851181type labelled_instruction = pseudo_instruction LabelledObjects.labelled_obj
    11861182
    1187 type preamble = (identifier0, BitVector.word) Types.prod List.list
    1188 
    11891183type assembly_program = instruction List.list
    11901184
    1191 type pseudo_assembly_program =
    1192   (preamble, labelled_instruction List.list) Types.prod
    1193 
    1194 val is_jump' : identifier0 preinstruction -> Bool.bool
     1185val fetch_pseudo_instruction :
     1186  labelled_instruction List.list -> BitVector.word -> (pseudo_instruction,
     1187  BitVector.word) Types.prod
     1188
     1189val is_jump' : identifier preinstruction -> Bool.bool
    11951190
    11961191val is_relative_jump : pseudo_instruction -> Bool.bool
     
    12001195val is_call : pseudo_instruction -> Bool.bool
    12011196
     1197val asm_cost_label :
     1198  labelled_instruction List.list -> BitVector.word Types.sig0 ->
     1199  CostLabel.costlabel Types.option
     1200
     1201val aDDRESS_WIDTH : Nat.nat
     1202
     1203val mAX_CODE_SIZE : Nat.nat
     1204
     1205val code_size_opt : labelled_instruction List.list -> __ Types.option
     1206
     1207type pseudo_assembly_program = { preamble : (identifier, BitVector.word)
     1208                                            Types.prod List.list;
     1209                                 code : labelled_instruction List.list;
     1210                                 renamed_symbols : (identifier, AST.ident)
     1211                                                   Types.prod List.list;
     1212                                 final_label : identifier }
     1213
     1214val pseudo_assembly_program_rect_Type4 :
     1215  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
     1216  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
     1217  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
     1218
     1219val pseudo_assembly_program_rect_Type5 :
     1220  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
     1221  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
     1222  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
     1223
     1224val pseudo_assembly_program_rect_Type3 :
     1225  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
     1226  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
     1227  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
     1228
     1229val pseudo_assembly_program_rect_Type2 :
     1230  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
     1231  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
     1232  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
     1233
     1234val pseudo_assembly_program_rect_Type1 :
     1235  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
     1236  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
     1237  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
     1238
     1239val pseudo_assembly_program_rect_Type0 :
     1240  ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
     1241  List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
     1242  identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
     1243
     1244val preamble :
     1245  pseudo_assembly_program -> (identifier, BitVector.word) Types.prod
     1246  List.list
     1247
     1248val code : pseudo_assembly_program -> labelled_instruction List.list
     1249
     1250val renamed_symbols :
     1251  pseudo_assembly_program -> (identifier, AST.ident) Types.prod List.list
     1252
     1253val final_label : pseudo_assembly_program -> identifier
     1254
     1255val pseudo_assembly_program_inv_rect_Type4 :
     1256  pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
     1257  List.list -> labelled_instruction List.list -> __ -> (identifier,
     1258  AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
     1259  'a1
     1260
     1261val pseudo_assembly_program_inv_rect_Type3 :
     1262  pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
     1263  List.list -> labelled_instruction List.list -> __ -> (identifier,
     1264  AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
     1265  'a1
     1266
     1267val pseudo_assembly_program_inv_rect_Type2 :
     1268  pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
     1269  List.list -> labelled_instruction List.list -> __ -> (identifier,
     1270  AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
     1271  'a1
     1272
     1273val pseudo_assembly_program_inv_rect_Type1 :
     1274  pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
     1275  List.list -> labelled_instruction List.list -> __ -> (identifier,
     1276  AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
     1277  'a1
     1278
     1279val pseudo_assembly_program_inv_rect_Type0 :
     1280  pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
     1281  List.list -> labelled_instruction List.list -> __ -> (identifier,
     1282  AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
     1283  'a1
     1284
     1285val pseudo_assembly_program_jmdiscr :
     1286  pseudo_assembly_program -> pseudo_assembly_program -> __
     1287
     1288type object_code = BitVector.byte List.list
     1289
     1290type costlabel_map = CostLabel.costlabel BitVectorTrie.bitVectorTrie
     1291
     1292type symboltable_type = AST.ident BitVectorTrie.bitVectorTrie
     1293
     1294type labelled_object_code = { oc : object_code; costlabels : costlabel_map;
     1295                              symboltable : symboltable_type;
     1296                              final_pc : BitVector.word }
     1297
     1298val labelled_object_code_rect_Type4 :
     1299  (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     1300  -> 'a1) -> labelled_object_code -> 'a1
     1301
     1302val labelled_object_code_rect_Type5 :
     1303  (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     1304  -> 'a1) -> labelled_object_code -> 'a1
     1305
     1306val labelled_object_code_rect_Type3 :
     1307  (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     1308  -> 'a1) -> labelled_object_code -> 'a1
     1309
     1310val labelled_object_code_rect_Type2 :
     1311  (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     1312  -> 'a1) -> labelled_object_code -> 'a1
     1313
     1314val labelled_object_code_rect_Type1 :
     1315  (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     1316  -> 'a1) -> labelled_object_code -> 'a1
     1317
     1318val labelled_object_code_rect_Type0 :
     1319  (object_code -> costlabel_map -> symboltable_type -> BitVector.word -> __
     1320  -> 'a1) -> labelled_object_code -> 'a1
     1321
     1322val oc : labelled_object_code -> object_code
     1323
     1324val costlabels : labelled_object_code -> costlabel_map
     1325
     1326val symboltable : labelled_object_code -> symboltable_type
     1327
     1328val final_pc : labelled_object_code -> BitVector.word
     1329
     1330val labelled_object_code_inv_rect_Type4 :
     1331  labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
     1332  -> BitVector.word -> __ -> __ -> 'a1) -> 'a1
     1333
     1334val labelled_object_code_inv_rect_Type3 :
     1335  labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
     1336  -> BitVector.word -> __ -> __ -> 'a1) -> 'a1
     1337
     1338val labelled_object_code_inv_rect_Type2 :
     1339  labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
     1340  -> BitVector.word -> __ -> __ -> 'a1) -> 'a1
     1341
     1342val labelled_object_code_inv_rect_Type1 :
     1343  labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
     1344  -> BitVector.word -> __ -> __ -> 'a1) -> 'a1
     1345
     1346val labelled_object_code_inv_rect_Type0 :
     1347  labelled_object_code -> (object_code -> costlabel_map -> symboltable_type
     1348  -> BitVector.word -> __ -> __ -> 'a1) -> 'a1
     1349
     1350val labelled_object_code_discr :
     1351  labelled_object_code -> labelled_object_code -> __
     1352
     1353val labelled_object_code_jmdiscr :
     1354  labelled_object_code -> labelled_object_code -> __
     1355
  • extracted/aSMCosts.ml

    r2759 r2773  
    11open Preamble
    22
     3open Fetch
     4
     5open Hide
     6
     7open Division
     8
     9open Z
     10
     11open BitVectorZ
     12
     13open Pointers
     14
     15open Coqlib
     16
     17open Values
     18
     19open Events
     20
     21open IOMonad
     22
     23open IO
     24
     25open Sets
     26
     27open Listb
     28
     29open StructuredTraces
     30
     31open AbstractStatus
     32
     33open BitVectorTrie
     34
    335open String
    436
     37open Exp
     38
     39open Arithmetic
     40
     41open Vector
     42
     43open FoldStuff
     44
     45open BitVector
     46
     47open Extranat
     48
     49open Integers
     50
     51open AST
     52
    553open LabelledObjects
    654
    7 open BitVectorTrie
    8 
    9 open Exp
    10 
    11 open Arithmetic
    12 
    13 open Integers
    14 
    15 open AST
     55open Proper
     56
     57open PositiveMap
     58
     59open Deqsets
     60
     61open ErrorMessages
     62
     63open PreIdentifiers
     64
     65open Errors
     66
     67open Extralib
     68
     69open Setoids
     70
     71open Monad
     72
     73open Option
     74
     75open Div_and_mod
     76
     77open Jmeq
     78
     79open Russell
     80
     81open Util
     82
     83open List
     84
     85open Lists
     86
     87open Bool
     88
     89open Relations
     90
     91open Nat
     92
     93open Positive
     94
     95open Hints_declaration
     96
     97open Core_notation
     98
     99open Pts
     100
     101open Logic
     102
     103open Types
     104
     105open Identifiers
    16106
    17107open CostLabel
    18108
    19 open Proper
    20 
    21 open PositiveMap
    22 
    23 open Deqsets
    24 
    25 open ErrorMessages
    26 
    27 open PreIdentifiers
    28 
    29 open Errors
    30 
    31 open Extralib
    32 
    33 open Setoids
    34 
    35 open Monad
    36 
    37 open Option
    38 
    39 open Lists
    40 
    41 open Positive
    42 
    43 open Identifiers
    44 
    45 open Extranat
    46 
    47 open Vector
    48 
    49 open Div_and_mod
    50 
    51 open Jmeq
    52 
    53 open Russell
    54 
    55 open Types
    56 
    57 open List
    58 
    59 open Util
    60 
    61 open FoldStuff
    62 
    63 open Bool
    64 
    65 open Hints_declaration
    66 
    67 open Core_notation
    68 
    69 open Pts
    70 
    71 open Logic
    72 
    73 open Relations
    74 
    75 open Nat
    76 
    77 open BitVector
    78 
    79109open ASM
    80110
    81 open Fetch
    82 
    83 open StructuredTraces
    84 
    85 open AbstractStatus
    86 
    87111open Status
    88112
    89113open StatusProofs
    90 
    91 open Sets
    92 
    93 open Listb
    94114
    95115open Interpret
     
    102122    StructuredTraces.as_pc_of =
    103123    (Obj.magic (Status.program_counter code_memory));
    104     StructuredTraces.as_classify = (fun s -> Types.Some
    105     (AbstractStatus.aSM_classify code_memory (Obj.magic s)));
     124    StructuredTraces.as_classify =
     125    (Obj.magic (AbstractStatus.aSM_classify code_memory));
    106126    StructuredTraces.as_label_of_pc = (fun pc ->
    107127    BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    108128      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    109129      Nat.O)))))))))))))))) (Obj.magic pc) cost_labels);
     130    StructuredTraces.as_result = (fun _ -> assert false (* absurd case *));
    110131    StructuredTraces.as_call_ident = (fun _ -> assert false (* absurd case *));
    111132    StructuredTraces.as_tailcall_ident = (fun _ -> assert false (* absurd case *)) }
     
    149170    (end_flag, pre_fun_call, start_fun_call, after_fun_call, final,
    150171     call_trace, final_trace) ->
    151   let current_instruction_cost0 =
     172  let current_instruction_cost =
    152173    Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call)
    153174  in
     
    156177      (Obj.magic after_fun_call) (Obj.magic final) final_trace
    157178  in
    158   Nat.plus current_instruction_cost0 final_trace_cost
     179  Nat.plus current_instruction_cost final_trace_cost
    159180| StructuredTraces.Tal_step_default
    160181    (end_flag, status_pre, status_init, status_end, tail_trace) ->
    161   let current_instruction_cost0 =
     182  let current_instruction_cost =
    162183    Interpret.current_instruction_cost code_memory (Obj.magic status_pre)
    163184  in
     
    166187      (Obj.magic status_init) (Obj.magic status_end) tail_trace
    167188  in
    168   Nat.plus current_instruction_cost0 tail_trace_cost
     189  Nat.plus current_instruction_cost tail_trace_cost
    169190
    170191(** val compute_paid_trace_label_label :
     
    187208   | Nat.S program_size' ->
    188209     (fun _ ->
    189        (let { Types.fst = eta31746; Types.snd = ticks } =
     210       (let { Types.fst = eta30542; Types.snd = ticks } =
    190211          Fetch.fetch code_memory' program_counter'
    191212        in
    192        let { Types.fst = instruction0; Types.snd = program_counter'' } =
    193          eta31746
     213       let { Types.fst = instruction; Types.snd = program_counter'' } =
     214         eta30542
    194215       in
    195216       (fun _ ->
     
    207228            (fun _ ->
    208229              Types.pi1
    209                 ((match instruction0 with
     230                ((match instruction with
    210231                  | ASM.ACALL addr ->
    211232                    (fun _ ->
     
    224245                      let jump_target =
    225246                        Interpret.compute_target_of_unconditional_jump
    226                           program_counter'' instruction0
     247                          program_counter'' instruction
    227248                      in
    228249                      Nat.plus ticks
     
    234255                      let jump_target =
    235256                        Interpret.compute_target_of_unconditional_jump
    236                           program_counter'' instruction0
     257                          program_counter'' instruction
    237258                      in
    238259                      Nat.plus ticks
     
    244265                      let jump_target =
    245266                        Interpret.compute_target_of_unconditional_jump
    246                           program_counter'' instruction0
     267                          program_counter'' instruction
    247268                      in
    248269                      Nat.plus ticks
     
    440461    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
    441462    CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Nat.nat Types.sig0 **)
    442 let block_cost code_memory program_counter0 cost_labels =
     463let block_cost code_memory program_counter cost_labels =
    443464  let cost_of_block =
    444     block_cost' code_memory program_counter0
     465    block_cost' code_memory program_counter
    445466      (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    446467        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
  • extracted/aSMCosts.mli

    r2717 r2773  
    11open Preamble
    22
    3 open String
     3open Fetch
    44
    5 open LabelledObjects
     5open Hide
     6
     7open Division
     8
     9open Z
     10
     11open BitVectorZ
     12
     13open Pointers
     14
     15open Coqlib
     16
     17open Values
     18
     19open Events
     20
     21open IOMonad
     22
     23open IO
     24
     25open Sets
     26
     27open Listb
     28
     29open StructuredTraces
     30
     31open AbstractStatus
    632
    733open BitVectorTrie
     34
     35open String
    836
    937open Exp
     
    1139open Arithmetic
    1240
     41open Vector
     42
     43open FoldStuff
     44
     45open BitVector
     46
     47open Extranat
     48
    1349open Integers
    1450
    1551open AST
    1652
    17 open CostLabel
     53open LabelledObjects
    1854
    1955open Proper
     
    3773open Option
    3874
    39 open Lists
    40 
    41 open Positive
    42 
    43 open Identifiers
    44 
    45 open Extranat
    46 
    47 open Vector
    48 
    4975open Div_and_mod
    5076
     
    5379open Russell
    5480
    55 open Types
     81open Util
    5682
    5783open List
    5884
    59 open Util
    60 
    61 open FoldStuff
     85open Lists
    6286
    6387open Bool
     88
     89open Relations
     90
     91open Nat
     92
     93open Positive
    6494
    6595open Hints_declaration
     
    71101open Logic
    72102
    73 open Relations
     103open Types
    74104
    75 open Nat
     105open Identifiers
    76106
    77 open BitVector
     107open CostLabel
    78108
    79109open ASM
    80 
    81 open Fetch
    82 
    83 open StructuredTraces
    84 
    85 open AbstractStatus
    86110
    87111open Status
    88112
    89113open StatusProofs
    90 
    91 open Sets
    92 
    93 open Listb
    94114
    95115open Interpret
  • extracted/aSMCostsSplit.ml

    r2717 r2773  
    11open Preamble
     2
     3open Fetch
     4
     5open Hide
     6
     7open Division
     8
     9open Z
     10
     11open BitVectorZ
     12
     13open Pointers
     14
     15open Coqlib
     16
     17open Values
     18
     19open Events
     20
     21open IOMonad
     22
     23open IO
     24
     25open Sets
     26
     27open Listb
    228
    329open StructuredTraces
     
    531open AbstractStatus
    632
    7 open Status
    8 
    9 open StatusProofs
    10 
    11 open Sets
    12 
    13 open Listb
    14 
    15 open Interpret
    16 
    17 open Fetch
     33open BitVectorTrie
    1834
    1935open String
    20 
    21 open LabelledObjects
    22 
    23 open BitVectorTrie
    2436
    2537open Exp
     
    2739open Arithmetic
    2840
     41open Vector
     42
     43open FoldStuff
     44
     45open BitVector
     46
     47open Extranat
     48
    2949open Integers
    3050
    3151open AST
    3252
    33 open CostLabel
     53open LabelledObjects
    3454
    3555open Proper
     
    5373open Option
    5474
    55 open Lists
    56 
    57 open Positive
    58 
    59 open Identifiers
    60 
    61 open Extranat
    62 
    63 open Vector
    64 
    6575open Div_and_mod
    6676
     
    6979open Russell
    7080
    71 open Types
     81open Util
    7282
    7383open List
    7484
    75 open Util
    76 
    77 open FoldStuff
     85open Lists
    7886
    7987open Bool
     88
     89open Relations
     90
     91open Nat
     92
     93open Positive
    8094
    8195open Hints_declaration
     
    87101open Logic
    88102
    89 open Relations
     103open Types
    90104
    91 open Nat
     105open Identifiers
    92106
    93 open BitVector
     107open CostLabel
    94108
    95109open ASM
     110
     111open Status
     112
     113open StatusProofs
     114
     115open Interpret
    96116
    97117open ASMCosts
     
    103123    BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat -> Nat.nat
    104124    Identifiers.identifier_map Types.sig0 **)
    105 let rec traverse_code_internal code_memory cost_labels program_counter0 program_size =
     125let rec traverse_code_internal code_memory cost_labels program_counter program_size =
    106126  (match program_size with
    107127   | Nat.O -> (fun _ -> Identifiers.empty_map PreIdentifiers.CostTag)
     
    115135             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    116136             (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O))
    117            program_counter0
     137           program_counter
    118138       in
    119139       let cost_mapping =
     
    123143       (match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    124144                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    125                 (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter0
     145                (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter
    126146                cost_labels with
    127147        | Types.None -> (fun _ -> Types.pi1 cost_mapping)
     
    129149          (fun _ ->
    130150            let cost =
    131               ASMCosts.block_cost code_memory program_counter0 cost_labels
     151              ASMCosts.block_cost code_memory program_counter cost_labels
    132152            in
    133153            Identifiers.add PreIdentifiers.CostTag (Types.pi1 cost_mapping)
     
    149169
    150170(** val compute_costs :
    151     BitVector.byte List.list -> CostLabel.costlabel
    152     BitVectorTrie.bitVectorTrie -> Nat.nat Identifiers.identifier_map
    153     Types.sig0 **)
    154 let compute_costs program0 cost_labels =
    155   let code_memory = Fetch.load_code_memory program0 in
     171    ASM.object_code -> CostLabel.costlabel BitVectorTrie.bitVectorTrie ->
     172    Nat.nat Identifiers.identifier_map Types.sig0 **)
     173let compute_costs program cost_labels =
     174  let code_memory = Fetch.load_code_memory program in
    156175  traverse_code code_memory cost_labels
    157176
    158177(** val aSM_cost_map :
    159     (BitVector.byte List.list, CostLabel.costlabel
    160     BitVectorTrie.bitVectorTrie) Types.prod -> StructuredTraces.as_cost_map **)
     178    ASM.labelled_object_code -> StructuredTraces.as_cost_map **)
    161179let aSM_cost_map p =
    162   let cost_map = compute_costs p.Types.fst p.Types.snd in
     180  let cost_map = compute_costs p.ASM.oc p.ASM.costlabels in
    163181  (fun l_sig ->
    164182  Identifiers.lookup_present PreIdentifiers.CostTag (Types.pi1 cost_map)
    165183    (StructuredTraces.as_cost_get_label
    166       (ASMCosts.aSM_abstract_status (Fetch.load_code_memory p.Types.fst)
    167         p.Types.snd) l_sig))
     184      (ASMCosts.aSM_abstract_status (Fetch.load_code_memory p.ASM.oc)
     185        p.ASM.costlabels) l_sig))
    168186
  • extracted/aSMCostsSplit.mli

    r2717 r2773  
    11open Preamble
     2
     3open Fetch
     4
     5open Hide
     6
     7open Division
     8
     9open Z
     10
     11open BitVectorZ
     12
     13open Pointers
     14
     15open Coqlib
     16
     17open Values
     18
     19open Events
     20
     21open IOMonad
     22
     23open IO
     24
     25open Sets
     26
     27open Listb
    228
    329open StructuredTraces
     
    531open AbstractStatus
    632
    7 open Status
    8 
    9 open StatusProofs
    10 
    11 open Sets
    12 
    13 open Listb
    14 
    15 open Interpret
    16 
    17 open Fetch
     33open BitVectorTrie
    1834
    1935open String
    20 
    21 open LabelledObjects
    22 
    23 open BitVectorTrie
    2436
    2537open Exp
     
    2739open Arithmetic
    2840
     41open Vector
     42
     43open FoldStuff
     44
     45open BitVector
     46
     47open Extranat
     48
    2949open Integers
    3050
    3151open AST
    3252
    33 open CostLabel
     53open LabelledObjects
    3454
    3555open Proper
     
    5373open Option
    5474
    55 open Lists
    56 
    57 open Positive
    58 
    59 open Identifiers
    60 
    61 open Extranat
    62 
    63 open Vector
    64 
    6575open Div_and_mod
    6676
     
    6979open Russell
    7080
    71 open Types
     81open Util
    7282
    7383open List
    7484
    75 open Util
    76 
    77 open FoldStuff
     85open Lists
    7886
    7987open Bool
     88
     89open Relations
     90
     91open Nat
     92
     93open Positive
    8094
    8195open Hints_declaration
     
    87101open Logic
    88102
    89 open Relations
     103open Types
    90104
    91 open Nat
     105open Identifiers
    92106
    93 open BitVector
     107open CostLabel
    94108
    95109open ASM
     110
     111open Status
     112
     113open StatusProofs
     114
     115open Interpret
    96116
    97117open ASMCosts
     
    110130
    111131val compute_costs :
    112   BitVector.byte List.list -> CostLabel.costlabel BitVectorTrie.bitVectorTrie
    113   -> Nat.nat Identifiers.identifier_map Types.sig0
     132  ASM.object_code -> CostLabel.costlabel BitVectorTrie.bitVectorTrie ->
     133  Nat.nat Identifiers.identifier_map Types.sig0
    114134
    115 val aSM_cost_map :
    116   (BitVector.byte List.list, CostLabel.costlabel BitVectorTrie.bitVectorTrie)
    117   Types.prod -> StructuredTraces.as_cost_map
     135val aSM_cost_map : ASM.labelled_object_code -> StructuredTraces.as_cost_map
    118136
  • extracted/aST.ml

    r2743 r2773  
    1919open Div_and_mod
    2020
     21open Util
     22
     23open FoldStuff
     24
     25open BitVector
     26
    2127open Jmeq
    2228
     
    2531open List
    2632
    27 open Util
    28 
    29 open FoldStuff
    30 
    31 open BitVector
     33open Setoids
     34
     35open Monad
     36
     37open Option
    3238
    3339open Extranat
     
    5460
    5561open Extralib
    56 
    57 open Setoids
    58 
    59 open Monad
    60 
    61 open Option
    6262
    6363open Lists
     
    151151
    152152(** val eq_region : region -> region -> Bool.bool **)
    153 let eq_region r5 r6 =
    154   match r5 with
     153let eq_region r1 r2 =
     154  match r1 with
    155155  | XData ->
    156     (match r6 with
     156    (match r2 with
    157157     | XData -> Bool.True
    158158     | Code -> Bool.False)
    159159  | Code ->
    160     (match r6 with
     160    (match r2 with
    161161     | XData -> Bool.False
    162162     | Code -> Bool.True)
     
    164164(** val eq_region_elim :
    165165    region -> region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
    166 let eq_region_elim r5 r6 =
    167   match r5 with
     166let eq_region_elim r1 r2 =
     167  match r1 with
    168168  | XData ->
    169     (match r6 with
     169    (match r2 with
    170170     | XData -> (fun ptrue pfalse -> ptrue __)
    171171     | Code -> (fun ptrue pfalse -> pfalse __))
    172172  | Code ->
    173     (match r6 with
     173    (match r2 with
    174174     | XData -> (fun ptrue pfalse -> pfalse __)
    175175     | Code -> (fun ptrue pfalse -> ptrue __))
    176176
    177177(** val eq_region_dec : region -> region -> (__, __) Types.sum **)
    178 let eq_region_dec r5 r6 =
    179   eq_region_elim r5 r6 (fun _ -> Types.Inl __) (fun _ -> Types.Inr __)
     178let eq_region_dec r1 r2 =
     179  eq_region_elim r1 r2 (fun _ -> Types.Inl __) (fun _ -> Types.Inr __)
    180180
    181181(** val size_pointer : Nat.nat **)
     
    418418    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    419419let rec typ_rect_Type4 h_ASTint h_ASTptr = function
    420 | ASTint (x_3506, x_3505) -> h_ASTint x_3506 x_3505
     420| ASTint (x_3766, x_3765) -> h_ASTint x_3766 x_3765
    421421| ASTptr -> h_ASTptr
    422422
     
    424424    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    425425let rec typ_rect_Type5 h_ASTint h_ASTptr = function
    426 | ASTint (x_3511, x_3510) -> h_ASTint x_3511 x_3510
     426| ASTint (x_3771, x_3770) -> h_ASTint x_3771 x_3770
    427427| ASTptr -> h_ASTptr
    428428
     
    430430    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    431431let rec typ_rect_Type3 h_ASTint h_ASTptr = function
    432 | ASTint (x_3516, x_3515) -> h_ASTint x_3516 x_3515
     432| ASTint (x_3776, x_3775) -> h_ASTint x_3776 x_3775
    433433| ASTptr -> h_ASTptr
    434434
     
    436436    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    437437let rec typ_rect_Type2 h_ASTint h_ASTptr = function
    438 | ASTint (x_3521, x_3520) -> h_ASTint x_3521 x_3520
     438| ASTint (x_3781, x_3780) -> h_ASTint x_3781 x_3780
    439439| ASTptr -> h_ASTptr
    440440
     
    442442    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    443443let rec typ_rect_Type1 h_ASTint h_ASTptr = function
    444 | ASTint (x_3526, x_3525) -> h_ASTint x_3526 x_3525
     444| ASTint (x_3786, x_3785) -> h_ASTint x_3786 x_3785
    445445| ASTptr -> h_ASTptr
    446446
     
    448448    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    449449let rec typ_rect_Type0 h_ASTint h_ASTptr = function
    450 | ASTint (x_3531, x_3530) -> h_ASTint x_3531 x_3530
     450| ASTint (x_3791, x_3790) -> h_ASTint x_3791 x_3790
    451451| ASTptr -> h_ASTptr
    452452
     
    666666type bvint = BitVector.bitVector
    667667
    668 (** val repr0 : intsize -> Nat.nat -> bvint **)
    669 let repr0 sz x =
     668(** val repr : intsize -> Nat.nat -> bvint **)
     669let repr sz x =
    670670  Arithmetic.bitvector_of_nat (bitsize_of_intsize sz) x
    671671
     
    877877(** val signature_rect_Type4 :
    878878    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    879 let rec signature_rect_Type4 h_mk_signature x_3566 =
    880   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3566 in
     879let rec signature_rect_Type4 h_mk_signature x_3826 =
     880  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3826 in
    881881  h_mk_signature sig_args0 sig_res0
    882882
    883883(** val signature_rect_Type5 :
    884884    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    885 let rec signature_rect_Type5 h_mk_signature x_3568 =
    886   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3568 in
     885let rec signature_rect_Type5 h_mk_signature x_3828 =
     886  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3828 in
    887887  h_mk_signature sig_args0 sig_res0
    888888
    889889(** val signature_rect_Type3 :
    890890    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    891 let rec signature_rect_Type3 h_mk_signature x_3570 =
    892   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3570 in
     891let rec signature_rect_Type3 h_mk_signature x_3830 =
     892  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3830 in
    893893  h_mk_signature sig_args0 sig_res0
    894894
    895895(** val signature_rect_Type2 :
    896896    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    897 let rec signature_rect_Type2 h_mk_signature x_3572 =
    898   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3572 in
     897let rec signature_rect_Type2 h_mk_signature x_3832 =
     898  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3832 in
    899899  h_mk_signature sig_args0 sig_res0
    900900
    901901(** val signature_rect_Type1 :
    902902    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    903 let rec signature_rect_Type1 h_mk_signature x_3574 =
    904   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3574 in
     903let rec signature_rect_Type1 h_mk_signature x_3834 =
     904  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3834 in
    905905  h_mk_signature sig_args0 sig_res0
    906906
    907907(** val signature_rect_Type0 :
    908908    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    909 let rec signature_rect_Type0 h_mk_signature x_3576 =
    910   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3576 in
     909let rec signature_rect_Type0 h_mk_signature x_3836 =
     910  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3836 in
    911911  h_mk_signature sig_args0 sig_res0
    912912
     
    984984    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    985985let rec init_data_rect_Type4 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    986 | Init_int8 x_3604 -> h_Init_int8 x_3604
    987 | Init_int16 x_3605 -> h_Init_int16 x_3605
    988 | Init_int32 x_3606 -> h_Init_int32 x_3606
    989 | Init_space x_3607 -> h_Init_space x_3607
     986| Init_int8 x_3864 -> h_Init_int8 x_3864
     987| Init_int16 x_3865 -> h_Init_int16 x_3865
     988| Init_int32 x_3866 -> h_Init_int32 x_3866
     989| Init_space x_3867 -> h_Init_space x_3867
    990990| Init_null -> h_Init_null
    991 | Init_addrof (x_3609, x_3608) -> h_Init_addrof x_3609 x_3608
     991| Init_addrof (x_3869, x_3868) -> h_Init_addrof x_3869 x_3868
    992992
    993993(** val init_data_rect_Type5 :
     
    995995    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    996996let rec init_data_rect_Type5 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    997 | Init_int8 x_3617 -> h_Init_int8 x_3617
    998 | Init_int16 x_3618 -> h_Init_int16 x_3618
    999 | Init_int32 x_3619 -> h_Init_int32 x_3619
    1000 | Init_space x_3620 -> h_Init_space x_3620
     997| Init_int8 x_3877 -> h_Init_int8 x_3877
     998| Init_int16 x_3878 -> h_Init_int16 x_3878
     999| Init_int32 x_3879 -> h_Init_int32 x_3879
     1000| Init_space x_3880 -> h_Init_space x_3880
    10011001| Init_null -> h_Init_null
    1002 | Init_addrof (x_3622, x_3621) -> h_Init_addrof x_3622 x_3621
     1002| Init_addrof (x_3882, x_3881) -> h_Init_addrof x_3882 x_3881
    10031003
    10041004(** val init_data_rect_Type3 :
     
    10061006    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10071007let rec init_data_rect_Type3 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    1008 | Init_int8 x_3630 -> h_Init_int8 x_3630
    1009 | Init_int16 x_3631 -> h_Init_int16 x_3631
    1010 | Init_int32 x_3632 -> h_Init_int32 x_3632
    1011 | Init_space x_3633 -> h_Init_space x_3633
     1008| Init_int8 x_3890 -> h_Init_int8 x_3890
     1009| Init_int16 x_3891 -> h_Init_int16 x_3891
     1010| Init_int32 x_3892 -> h_Init_int32 x_3892
     1011| Init_space x_3893 -> h_Init_space x_3893
    10121012| Init_null -> h_Init_null
    1013 | Init_addrof (x_3635, x_3634) -> h_Init_addrof x_3635 x_3634
     1013| Init_addrof (x_3895, x_3894) -> h_Init_addrof x_3895 x_3894
    10141014
    10151015(** val init_data_rect_Type2 :
     
    10171017    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10181018let rec init_data_rect_Type2 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    1019 | Init_int8 x_3643 -> h_Init_int8 x_3643
    1020 | Init_int16 x_3644 -> h_Init_int16 x_3644
    1021 | Init_int32 x_3645 -> h_Init_int32 x_3645
    1022 | Init_space x_3646 -> h_Init_space x_3646
     1019| Init_int8 x_3903 -> h_Init_int8 x_3903
     1020| Init_int16 x_3904 -> h_Init_int16 x_3904
     1021| Init_int32 x_3905 -> h_Init_int32 x_3905
     1022| Init_space x_3906 -> h_Init_space x_3906
    10231023| Init_null -> h_Init_null
    1024 | Init_addrof (x_3648, x_3647) -> h_Init_addrof x_3648 x_3647
     1024| Init_addrof (x_3908, x_3907) -> h_Init_addrof x_3908 x_3907
    10251025
    10261026(** val init_data_rect_Type1 :
     
    10281028    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10291029let rec init_data_rect_Type1 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    1030 | Init_int8 x_3656 -> h_Init_int8 x_3656
    1031 | Init_int16 x_3657 -> h_Init_int16 x_3657
    1032 | Init_int32 x_3658 -> h_Init_int32 x_3658
    1033 | Init_space x_3659 -> h_Init_space x_3659
     1030| Init_int8 x_3916 -> h_Init_int8 x_3916
     1031| Init_int16 x_3917 -> h_Init_int16 x_3917
     1032| Init_int32 x_3918 -> h_Init_int32 x_3918
     1033| Init_space x_3919 -> h_Init_space x_3919
    10341034| Init_null -> h_Init_null
    1035 | Init_addrof (x_3661, x_3660) -> h_Init_addrof x_3661 x_3660
     1035| Init_addrof (x_3921, x_3920) -> h_Init_addrof x_3921 x_3920
    10361036
    10371037(** val init_data_rect_Type0 :
     
    10391039    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10401040let rec init_data_rect_Type0 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_space h_Init_null h_Init_addrof = function
    1041 | Init_int8 x_3669 -> h_Init_int8 x_3669
    1042 | Init_int16 x_3670 -> h_Init_int16 x_3670
    1043 | Init_int32 x_3671 -> h_Init_int32 x_3671
    1044 | Init_space x_3672 -> h_Init_space x_3672
     1041| Init_int8 x_3929 -> h_Init_int8 x_3929
     1042| Init_int16 x_3930 -> h_Init_int16 x_3930
     1043| Init_int32 x_3931 -> h_Init_int32 x_3931
     1044| Init_space x_3932 -> h_Init_space x_3932
    10451045| Init_null -> h_Init_null
    1046 | Init_addrof (x_3674, x_3673) -> h_Init_addrof x_3674 x_3673
     1046| Init_addrof (x_3934, x_3933) -> h_Init_addrof x_3934 x_3933
    10471047
    10481048(** val init_data_inv_rect_Type4 :
     
    11111111    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11121112    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1113 let rec program_rect_Type4 h_mk_program x_3761 =
     1113let rec program_rect_Type4 h_mk_program x_4021 =
    11141114  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1115     prog_main0 } = x_3761
     1115    prog_main0 } = x_4021
    11161116  in
    11171117  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11201120    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11211121    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1122 let rec program_rect_Type5 h_mk_program x_3763 =
     1122let rec program_rect_Type5 h_mk_program x_4023 =
    11231123  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1124     prog_main0 } = x_3763
     1124    prog_main0 } = x_4023
    11251125  in
    11261126  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11291129    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11301130    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1131 let rec program_rect_Type3 h_mk_program x_3765 =
     1131let rec program_rect_Type3 h_mk_program x_4025 =
    11321132  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1133     prog_main0 } = x_3765
     1133    prog_main0 } = x_4025
    11341134  in
    11351135  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11381138    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11391139    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1140 let rec program_rect_Type2 h_mk_program x_3767 =
     1140let rec program_rect_Type2 h_mk_program x_4027 =
    11411141  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1142     prog_main0 } = x_3767
     1142    prog_main0 } = x_4027
    11431143  in
    11441144  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11471147    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11481148    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1149 let rec program_rect_Type1 h_mk_program x_3769 =
     1149let rec program_rect_Type1 h_mk_program x_4029 =
    11501150  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1151     prog_main0 } = x_3769
     1151    prog_main0 } = x_4029
    11521152  in
    11531153  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11561156    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11571157    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1158 let rec program_rect_Type0 h_mk_program x_3771 =
     1158let rec program_rect_Type0 h_mk_program x_4031 =
    11591159  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1160     prog_main0 } = x_3771
     1160    prog_main0 } = x_4031
    11611161  in
    11621162  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    13621362type m_W = __
    13631363
    1364 type match_fundef = __
    1365 
    1366 type match_varinfo = __
    1367 
    13681364(** val matching_inv_rect_Type4 :
    13691365    matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     
    13991395    matching -> ident List.list -> ident List.list -> __ -> __ **)
    14001396let mfe_cast_fn_type m vs vs' =
    1401   Extralib.eq_rect_Type0_r1 vs (fun m0 -> m0) vs'
     1397  Extralib.eq_rect_Type0_r vs (fun m0 -> m0) vs'
    14021398
    14031399(** val match_program_rect_Type4 :
    14041400    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
    14051401    'a1) -> 'a1 **)
    1406 let rec match_program_rect_Type4 m p3 p4 h_mk_match_program =
     1402let rec match_program_rect_Type4 m p1 p2 h_mk_match_program =
    14071403  h_mk_match_program __ __ __
    14081404
     
    14101406    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
    14111407    'a1) -> 'a1 **)
    1412 let rec match_program_rect_Type5 m p3 p4 h_mk_match_program =
     1408let rec match_program_rect_Type5 m p1 p2 h_mk_match_program =
    14131409  h_mk_match_program __ __ __
    14141410
     
    14161412    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
    14171413    'a1) -> 'a1 **)
    1418 let rec match_program_rect_Type3 m p3 p4 h_mk_match_program =
     1414let rec match_program_rect_Type3 m p1 p2 h_mk_match_program =
    14191415  h_mk_match_program __ __ __
    14201416
     
    14221418    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
    14231419    'a1) -> 'a1 **)
    1424 let rec match_program_rect_Type2 m p3 p4 h_mk_match_program =
     1420let rec match_program_rect_Type2 m p1 p2 h_mk_match_program =
    14251421  h_mk_match_program __ __ __
    14261422
     
    14281424    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
    14291425    'a1) -> 'a1 **)
    1430 let rec match_program_rect_Type1 m p3 p4 h_mk_match_program =
     1426let rec match_program_rect_Type1 m p1 p2 h_mk_match_program =
    14311427  h_mk_match_program __ __ __
    14321428
     
    14341430    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
    14351431    'a1) -> 'a1 **)
    1436 let rec match_program_rect_Type0 m p3 p4 h_mk_match_program =
     1432let rec match_program_rect_Type0 m p1 p2 h_mk_match_program =
    14371433  h_mk_match_program __ __ __
    14381434
     
    14811477(** val external_function_rect_Type4 :
    14821478    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1483 let rec external_function_rect_Type4 h_mk_external_function x_3975 =
    1484   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3975 in
     1479let rec external_function_rect_Type4 h_mk_external_function x_4235 =
     1480  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4235 in
    14851481  h_mk_external_function ef_id0 ef_sig0
    14861482
    14871483(** val external_function_rect_Type5 :
    14881484    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1489 let rec external_function_rect_Type5 h_mk_external_function x_3977 =
    1490   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3977 in
     1485let rec external_function_rect_Type5 h_mk_external_function x_4237 =
     1486  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4237 in
    14911487  h_mk_external_function ef_id0 ef_sig0
    14921488
    14931489(** val external_function_rect_Type3 :
    14941490    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1495 let rec external_function_rect_Type3 h_mk_external_function x_3979 =
    1496   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3979 in
     1491let rec external_function_rect_Type3 h_mk_external_function x_4239 =
     1492  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4239 in
    14971493  h_mk_external_function ef_id0 ef_sig0
    14981494
    14991495(** val external_function_rect_Type2 :
    15001496    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1501 let rec external_function_rect_Type2 h_mk_external_function x_3981 =
    1502   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3981 in
     1497let rec external_function_rect_Type2 h_mk_external_function x_4241 =
     1498  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4241 in
    15031499  h_mk_external_function ef_id0 ef_sig0
    15041500
    15051501(** val external_function_rect_Type1 :
    15061502    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1507 let rec external_function_rect_Type1 h_mk_external_function x_3983 =
    1508   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3983 in
     1503let rec external_function_rect_Type1 h_mk_external_function x_4243 =
     1504  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4243 in
    15091505  h_mk_external_function ef_id0 ef_sig0
    15101506
    15111507(** val external_function_rect_Type0 :
    15121508    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1513 let rec external_function_rect_Type0 h_mk_external_function x_3985 =
    1514   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3985 in
     1509let rec external_function_rect_Type0 h_mk_external_function x_4245 =
     1510  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4245 in
    15151511  h_mk_external_function ef_id0 ef_sig0
    15161512
     
    15791575    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15801576let rec fundef_rect_Type4 h_Internal h_External = function
    1581 | Internal x_4005 -> h_Internal x_4005
    1582 | External x_4006 -> h_External x_4006
     1577| Internal x_4265 -> h_Internal x_4265
     1578| External x_4266 -> h_External x_4266
    15831579
    15841580(** val fundef_rect_Type5 :
    15851581    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15861582let rec fundef_rect_Type5 h_Internal h_External = function
    1587 | Internal x_4010 -> h_Internal x_4010
    1588 | External x_4011 -> h_External x_4011
     1583| Internal x_4270 -> h_Internal x_4270
     1584| External x_4271 -> h_External x_4271
    15891585
    15901586(** val fundef_rect_Type3 :
    15911587    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15921588let rec fundef_rect_Type3 h_Internal h_External = function
    1593 | Internal x_4015 -> h_Internal x_4015
    1594 | External x_4016 -> h_External x_4016
     1589| Internal x_4275 -> h_Internal x_4275
     1590| External x_4276 -> h_External x_4276
    15951591
    15961592(** val fundef_rect_Type2 :
    15971593    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15981594let rec fundef_rect_Type2 h_Internal h_External = function
    1599 | Internal x_4020 -> h_Internal x_4020
    1600 | External x_4021 -> h_External x_4021
     1595| Internal x_4280 -> h_Internal x_4280
     1596| External x_4281 -> h_External x_4281
    16011597
    16021598(** val fundef_rect_Type1 :
    16031599    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16041600let rec fundef_rect_Type1 h_Internal h_External = function
    1605 | Internal x_4025 -> h_Internal x_4025
    1606 | External x_4026 -> h_External x_4026
     1601| Internal x_4285 -> h_Internal x_4285
     1602| External x_4286 -> h_External x_4286
    16071603
    16081604(** val fundef_rect_Type0 :
    16091605    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16101606let rec fundef_rect_Type0 h_Internal h_External = function
    1611 | Internal x_4030 -> h_Internal x_4030
    1612 | External x_4031 -> h_External x_4031
     1607| Internal x_4290 -> h_Internal x_4290
     1608| External x_4291 -> h_External x_4291
    16131609
    16141610(** val fundef_inv_rect_Type4 :
     
    16701666| External ef -> Errors.OK (External ef)
    16711667
    1672 type member1 = __
    1673 
  • extracted/aST.mli

    r2717 r2773  
    1919open Div_and_mod
    2020
     21open Util
     22
     23open FoldStuff
     24
     25open BitVector
     26
    2127open Jmeq
    2228
     
    2531open List
    2632
    27 open Util
    28 
    29 open FoldStuff
    30 
    31 open BitVector
     33open Setoids
     34
     35open Monad
     36
     37open Option
    3238
    3339open Extranat
     
    5460
    5561open Extralib
    56 
    57 open Setoids
    58 
    59 open Monad
    60 
    61 open Option
    6262
    6363open Lists
     
    278278type bvint = BitVector.bitVector
    279279
    280 val repr0 : intsize -> Nat.nat -> bvint
     280val repr : intsize -> Nat.nat -> bvint
    281281
    282282val size_floatsize : floatsize -> Nat.nat
     
    532532type m_W
    533533
    534 type match_fundef = __
    535 
    536 type match_varinfo = __
    537 
    538534val matching_inv_rect_Type4 :
    539535  matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
     
    701697  ('a1 -> 'a2 Errors.res) -> 'a1 fundef -> 'a2 fundef Errors.res
    702698
    703 type member1 = __
    704 
  • extracted/abstractStatus.ml

    r2717 r2773  
    11open Preamble
    22
    3 open String
     3open Hide
    44
    5 open LabelledObjects
     5open Integers
    66
    7 open BitVectorTrie
     7open AST
     8
     9open Division
    810
    911open Exp
     
    1113open Arithmetic
    1214
    13 open Integers
     15open Extranat
    1416
    15 open AST
     17open Vector
    1618
    17 open CostLabel
     19open FoldStuff
     20
     21open BitVector
     22
     23open Z
     24
     25open BitVectorZ
     26
     27open Pointers
     28
     29open Coqlib
     30
     31open Values
     32
     33open Events
     34
     35open IOMonad
     36
     37open IO
     38
     39open Sets
     40
     41open Listb
    1842
    1943open Proper
     
    3761open Option
    3862
     63open Div_and_mod
     64
     65open Russell
     66
     67open Util
     68
     69open List
     70
    3971open Lists
     72
     73open Nat
    4074
    4175open Positive
    4276
     77open Types
     78
    4379open Identifiers
    4480
    45 open Extranat
    46 
    47 open Vector
    48 
    49 open Div_and_mod
     81open CostLabel
    5082
    5183open Jmeq
    52 
    53 open Russell
    54 
    55 open Types
    56 
    57 open List
    58 
    59 open Util
    60 
    61 open FoldStuff
    62 
    63 open Bool
    6484
    6585open Hints_declaration
     
    7393open Relations
    7494
    75 open Nat
     95open Bool
    7696
    77 open BitVector
     97open StructuredTraces
     98
     99open BitVectorTrie
     100
     101open String
     102
     103open LabelledObjects
    78104
    79105open ASM
     
    82108
    83109open Fetch
    84 
    85 open Sets
    86 
    87 open Listb
    88 
    89 open StructuredTraces
    90110
    91111(** val aSM_classify00 :
     
    144164    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
    145165    ASM.instruction **)
    146 let current_instruction0 code_memory program_counter0 =
    147   (Fetch.fetch code_memory program_counter0).Types.fst.Types.fst
     166let current_instruction0 code_memory program_counter =
     167  (Fetch.fetch code_memory program_counter).Types.fst.Types.fst
    148168
    149169(** val current_instruction :
  • extracted/abstractStatus.mli

    r2717 r2773  
    11open Preamble
    22
    3 open String
     3open Hide
    44
    5 open LabelledObjects
     5open Integers
    66
    7 open BitVectorTrie
     7open AST
     8
     9open Division
    810
    911open Exp
     
    1113open Arithmetic
    1214
    13 open Integers
     15open Extranat
    1416
    15 open AST
     17open Vector
    1618
    17 open CostLabel
     19open FoldStuff
     20
     21open BitVector
     22
     23open Z
     24
     25open BitVectorZ
     26
     27open Pointers
     28
     29open Coqlib
     30
     31open Values
     32
     33open Events
     34
     35open IOMonad
     36
     37open IO
     38
     39open Sets
     40
     41open Listb
    1842
    1943open Proper
     
    3761open Option
    3862
     63open Div_and_mod
     64
     65open Russell
     66
     67open Util
     68
     69open List
     70
    3971open Lists
     72
     73open Nat
    4074
    4175open Positive
    4276
     77open Types
     78
    4379open Identifiers
    4480
    45 open Extranat
    46 
    47 open Vector
    48 
    49 open Div_and_mod
     81open CostLabel
    5082
    5183open Jmeq
    52 
    53 open Russell
    54 
    55 open Types
    56 
    57 open List
    58 
    59 open Util
    60 
    61 open FoldStuff
    62 
    63 open Bool
    6484
    6585open Hints_declaration
     
    7393open Relations
    7494
    75 open Nat
     95open Bool
    7696
    77 open BitVector
     97open StructuredTraces
     98
     99open BitVectorTrie
     100
     101open String
     102
     103open LabelledObjects
    78104
    79105open ASM
     
    82108
    83109open Fetch
    84 
    85 open Sets
    86 
    87 open Listb
    88 
    89 open StructuredTraces
    90110
    91111val aSM_classify00 : 'a1 ASM.preinstruction -> StructuredTraces.status_class
  • extracted/arithmetic.ml

    r2717 r2773  
    11open Preamble
     2
     3open Setoids
     4
     5open Monad
     6
     7open Option
    28
    39open Extranat
     
    6369  let p5 = Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) n2 Nat.O
    6470  in
    65   Vector.append0
     71  Vector.append
    6672    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S
    6773      (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    6874    (Nat.S Nat.O))))))))
    69     (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
    70       (Nat.S (Nat.S Nat.O)))) n1 (Vector.VCons ((Nat.S (Nat.S (Nat.S
    71       Nat.O))), p5, (Vector.VCons ((Nat.S (Nat.S Nat.O)), b1, (Vector.VCons
    72       ((Nat.S Nat.O), b2, (Vector.VCons (Nat.O, b3, Vector.VEmpty))))))))) b
     75    (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S
     76      (Nat.S Nat.O)))) n1 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), p5,
     77      (Vector.VCons ((Nat.S (Nat.S Nat.O)), b1, (Vector.VCons ((Nat.S Nat.O),
     78      b2, (Vector.VCons (Nat.O, b3, Vector.VEmpty))))))))) b
    7379
    7480(** val nat_of_bool : Bool.bool -> Nat.nat **)
     
    96102    (match last_carry with
    97103     | Bool.True ->
    98        let bit0 = Bool.xorb (Bool.xorb b c) Bool.True in
     104       let bit = Bool.xorb (Bool.xorb b c) Bool.True in
    99105       let carry = carry_of b c Bool.True in
    100        { Types.fst = (Vector.VCons (n0, bit0, lower_bits)); Types.snd =
     106       { Types.fst = (Vector.VCons (n0, bit, lower_bits)); Types.snd =
    101107       (Vector.VCons (n0, carry, carries)) }
    102108     | Bool.False ->
    103        let bit0 = Bool.xorb (Bool.xorb b c) Bool.False in
     109       let bit = Bool.xorb (Bool.xorb b c) Bool.False in
    104110       let carry = carry_of b c Bool.False in
    105        { Types.fst = (Vector.VCons (n0, bit0, lower_bits)); Types.snd =
     111       { Types.fst = (Vector.VCons (n0, bit, lower_bits)); Types.snd =
    106112       (Vector.VCons (n0, carry, carries)) })) { Types.fst = Vector.VEmpty;
    107113    Types.snd = Vector.VEmpty } n x y
     
    124130      | Vector.VCons (x0, bw, x1) -> bw
    125131    in
    126     let bit0 = Bool.xorb (Bool.xorb b c) last_borrow in
     132    let bit = Bool.xorb (Bool.xorb b c) last_borrow in
    127133    let borrow = borrow_of b c last_borrow in
    128     { Types.fst = (Vector.VCons (n0, bit0, lower_bits)); Types.snd =
     134    { Types.fst = (Vector.VCons (n0, bit, lower_bits)); Types.snd =
    129135    (Vector.VCons (n0, borrow, borrows)) }) { Types.fst = Vector.VEmpty;
    130136    Types.snd = Vector.VEmpty } n x y
     
    226232let rec nat_of_bitvector_aux n m = function
    227233| Vector.VEmpty -> m
    228 | Vector.VCons (n', hd0, tl) ->
     234| Vector.VCons (n', hd, tl) ->
    229235  nat_of_bitvector_aux n'
    230     (match hd0 with
     236    (match hd with
    231237     | Bool.True ->
    232238       Nat.plus (Nat.times (Nat.S (Nat.S Nat.O)) m) (Nat.S Nat.O)
     
    260266  match b with
    261267  | Vector.VEmpty -> acc
    262   | Vector.VCons (m', hd0, tl) ->
     268  | Vector.VCons (m', hd, tl) ->
    263269    let acc' =
    264       match hd0 with
     270      match hd with
    265271      | Bool.True -> addition_n (Nat.S n) c acc
    266272      | Bool.False -> acc
     
    291297(** val fbs_diff_rect_Type4 :
    292298    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    293 let rec fbs_diff_rect_Type4 h_fbs_diff' x_1137 = function
     299let rec fbs_diff_rect_Type4 h_fbs_diff' x_1836 = function
    294300| Fbs_diff' (n, m) -> h_fbs_diff' n m
    295301
    296302(** val fbs_diff_rect_Type5 :
    297303    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    298 let rec fbs_diff_rect_Type5 h_fbs_diff' x_1140 = function
     304let rec fbs_diff_rect_Type5 h_fbs_diff' x_1839 = function
    299305| Fbs_diff' (n, m) -> h_fbs_diff' n m
    300306
    301307(** val fbs_diff_rect_Type3 :
    302308    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    303 let rec fbs_diff_rect_Type3 h_fbs_diff' x_1143 = function
     309let rec fbs_diff_rect_Type3 h_fbs_diff' x_1842 = function
    304310| Fbs_diff' (n, m) -> h_fbs_diff' n m
    305311
    306312(** val fbs_diff_rect_Type2 :
    307313    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    308 let rec fbs_diff_rect_Type2 h_fbs_diff' x_1146 = function
     314let rec fbs_diff_rect_Type2 h_fbs_diff' x_1845 = function
    309315| Fbs_diff' (n, m) -> h_fbs_diff' n m
    310316
    311317(** val fbs_diff_rect_Type1 :
    312318    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    313 let rec fbs_diff_rect_Type1 h_fbs_diff' x_1149 = function
     319let rec fbs_diff_rect_Type1 h_fbs_diff' x_1848 = function
    314320| Fbs_diff' (n, m) -> h_fbs_diff' n m
    315321
    316322(** val fbs_diff_rect_Type0 :
    317323    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    318 let rec fbs_diff_rect_Type0 h_fbs_diff' x_1152 = function
     324let rec fbs_diff_rect_Type0 h_fbs_diff' x_1851 = function
    319325| Fbs_diff' (n, m) -> h_fbs_diff' n m
    320326
     
    378384        Bool.False
    379385    in
    380     let bit0 = Vector.head' n flags in
     386    let bit = Vector.head' n flags in
    381387    let q'' =
    382       match bit0 with
     388      match bit with
    383389      | Bool.True -> q'
    384390      | Bool.False -> q
     
    387393      divmod_u_aux n m' q'' (Vector.shift_right_1 n d Bool.False)
    388394    in
    389     { Types.fst = (Vector.VCons (m', bit0, tl)); Types.snd = md }
     395    { Types.fst = (Vector.VCons (m', bit, tl)); Types.snd = md }
    390396
    391397(** val divmod_u :
     
    668674       let xb = Vector.head' sz' b' in
    669675       let xc = Vector.head' sz' c' in
    670        let tlb = Vector.tail0 sz' b' in
    671        let tlc = Vector.tail0 sz' c' in
     676       let tlb = Vector.tail sz' b' in
     677       let tlc = Vector.tail sz' c' in
    672678       let { Types.fst = bits; Types.snd = last } =
    673679         canonical_add sz' tla tlb tlc init
    674680       in
    675        let { Types.fst = bit0; Types.snd = carry } =
     681       let { Types.fst = bit; Types.snd = carry } =
    676682         ternary_carry_of xa xb xc last
    677683       in
    678        { Types.fst = (Vector.VCons (sz', bit0, bits)); Types.snd = carry }))
    679     b c
     684       { Types.fst = (Vector.VCons (sz', bit, bits)); Types.snd = carry })) b
     685    c
    680686
    681687(** val carries_to_ternary : Bool.bool -> Bool.bool -> ternary **)
     
    756762      (Nat.S Nat.O)))))))) c (Nat.S Nat.O)
    757763  in
    758   Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     764  Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    759765    Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    760766    Nat.O)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
  • extracted/arithmetic.mli

    r2717 r2773  
    11open Preamble
     2
     3open Setoids
     4
     5open Monad
     6
     7open Option
    28
    39open Extranat
  • extracted/assembly.ml

    r2717 r2773  
    11open Preamble
    22
     3open BitVectorTrie
     4
    35open String
    46
     7open Exp
     8
     9open Arithmetic
     10
     11open Vector
     12
     13open FoldStuff
     14
     15open BitVector
     16
     17open Extranat
     18
     19open Integers
     20
     21open AST
     22
    523open LabelledObjects
    624
    7 open BitVectorTrie
    8 
    9 open Exp
    10 
    11 open Arithmetic
    12 
    13 open Integers
    14 
    15 open AST
     25open Proper
     26
     27open PositiveMap
     28
     29open Deqsets
     30
     31open ErrorMessages
     32
     33open PreIdentifiers
     34
     35open Errors
     36
     37open Extralib
     38
     39open Setoids
     40
     41open Monad
     42
     43open Option
     44
     45open Div_and_mod
     46
     47open Jmeq
     48
     49open Russell
     50
     51open Util
     52
     53open List
     54
     55open Lists
     56
     57open Bool
     58
     59open Relations
     60
     61open Nat
     62
     63open Positive
     64
     65open Hints_declaration
     66
     67open Core_notation
     68
     69open Pts
     70
     71open Logic
     72
     73open Types
     74
     75open Identifiers
    1676
    1777open CostLabel
    18 
    19 open Proper
    20 
    21 open PositiveMap
    22 
    23 open Deqsets
    24 
    25 open ErrorMessages
    26 
    27 open PreIdentifiers
    28 
    29 open Errors
    30 
    31 open Extralib
    32 
    33 open Setoids
    34 
    35 open Monad
    36 
    37 open Option
    38 
    39 open Lists
    40 
    41 open Positive
    42 
    43 open Identifiers
    44 
    45 open Extranat
    46 
    47 open Vector
    48 
    49 open Div_and_mod
    50 
    51 open Jmeq
    52 
    53 open Russell
    54 
    55 open Types
    56 
    57 open List
    58 
    59 open Util
    60 
    61 open FoldStuff
    62 
    63 open Bool
    64 
    65 open Hints_declaration
    66 
    67 open Core_notation
    68 
    69 open Pts
    70 
    71 open Logic
    72 
    73 open Relations
    74 
    75 open Nat
    76 
    77 open BitVector
    7878
    7979open ASM
     
    253253   | ASM.REGISTER r ->
    254254     (fun _ -> List.Cons
    255        ((Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
     255       ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
    256256          (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
    257257          Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
     
    312312   | ASM.REGISTER r ->
    313313     (fun _ -> List.Cons
    314        ((Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
     314       ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
    315315          (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
    316316          Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
     
    371371   | ASM.REGISTER r ->
    372372     (fun _ -> List.Cons
    373        ((Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
     373       ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
    374374          (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
    375375          Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
     
    431431   | ASM.REGISTER r ->
    432432     (fun _ -> List.Cons
    433        ((Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
     433       ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
    434434          (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
    435435          Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
     
    499499   | ASM.REGISTER r ->
    500500     (fun _ -> List.Cons
    501        ((Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
     501       ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
    502502          (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
    503503          Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
     
    785785      | ASM.REGISTER r ->
    786786        (fun _ -> List.Cons
    787           ((Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
     787          ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
    788788             (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
    789789             (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
     
    827827   | ASM.REGISTER r ->
    828828     (fun _ -> List.Cons
    829        ((Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
     829       ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
    830830          (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
    831831          Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
     
    884884         | ASM.REGISTER r ->
    885885           (fun _ -> List.Cons
    886              ((Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
     886             ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
    887887                (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
    888888                (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S
     
    10641064         | ASM.REGISTER r ->
    10651065           (fun _ -> List.Cons
    1066              ((Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
     1066             ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
    10671067                (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
    10681068                (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S
     
    12411241      | ASM.REGISTER r ->
    12421242        (fun _ -> List.Cons
    1243           ((Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
     1243          ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
    12441244             (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
    12451245             (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S
     
    15341534                  | ASM.REGISTER r ->
    15351535                    (fun _ -> List.Cons
    1536                       ((Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1536                      ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    15371537                         Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
    15381538                         (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
     
    16721672                       | ASM.DIRECT b1 ->
    16731673                         (fun _ -> List.Cons
    1674                            ((Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S
    1675                               (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
     1674                           ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1675                              Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
    16761676                              (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
    16771677                              Nat.O)))), Bool.True, (Vector.VCons ((Nat.S
     
    16901690                       | ASM.ACC_A ->
    16911691                         (fun _ -> List.Cons
    1692                            ((Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S
    1693                               (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
     1692                           ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1693                              Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
    16941694                              (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
    16951695                              Nat.O)))), Bool.True, (Vector.VCons ((Nat.S
     
    17051705                       | ASM.DATA b1 ->
    17061706                         (fun _ -> List.Cons
    1707                            ((Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S
    1708                               (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
     1707                           ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1708                              Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
    17091709                              (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
    17101710                              Nat.O)))), Bool.False, (Vector.VCons ((Nat.S
     
    18271827               | ASM.REGISTER r ->
    18281828                 (fun _ -> List.Cons
    1829                    ((Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1829                   ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    18301830                      Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
    18311831                      ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
     
    22032203   | ASM.REGISTER r ->
    22042204     (fun _ -> List.Cons
    2205        ((Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
     2205       ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
    22062206          (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
    22072207          Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
     
    23232323       let v2 = v1_v2.Types.snd in
    23242324       List.Cons
    2325        ((Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
     2325       ((Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
    23262326          (Nat.S (Nat.S Nat.O))))) v1 (Vector.VCons ((Nat.S (Nat.S (Nat.S
    23272327          (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
     
    23992399       let v2 = v1_v2.Types.snd in
    24002400       List.Cons
    2401        ((Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
     2401       ((Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
    24022402          (Nat.S (Nat.S Nat.O))))) v1 (Vector.VCons ((Nat.S (Nat.S (Nat.S
    24032403          (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
     
    25432543
    25442544(** val expand_relative_jump_internal :
    2545     (ASM.identifier0 -> BitVector.word) -> (BitVector.word -> BitVector.word)
    2546     -> (BitVector.word -> Bool.bool) -> ASM.identifier0 -> BitVector.word ->
     2545    (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
     2546    -> (BitVector.word -> Bool.bool) -> ASM.identifier -> BitVector.word ->
    25472547    (ASM.subaddressing_mode -> ASM.subaddressing_mode ASM.preinstruction) ->
    25482548    ASM.instruction List.list **)
    2549 let expand_relative_jump_internal lookup_labels sigma0 policy lbl ppc i =
    2550   let lookup_address = sigma0 (lookup_labels lbl) in
     2549let expand_relative_jump_internal lookup_labels sigma policy lbl ppc i =
     2550  let lookup_address = sigma (lookup_labels lbl) in
    25512551  let pc_plus_jmp_length =
    2552     sigma0
     2552    sigma
    25532553      (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    25542554        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    25762576
    25772577(** val expand_relative_jump :
    2578     (ASM.identifier0 -> BitVector.word) -> (BitVector.word -> BitVector.word)
    2579     -> (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.identifier0
     2578    (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
     2579    -> (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.identifier
    25802580    ASM.preinstruction -> ASM.instruction List.list **)
    2581 let expand_relative_jump lookup_labels sigma0 policy ppc = function
     2581let expand_relative_jump lookup_labels sigma policy ppc = function
    25822582| ASM.ADD (arg1, arg2) ->
    25832583  List.Cons ((ASM.RealInstruction (ASM.ADD (arg1, arg2))), List.Nil)
     
    25942594| ASM.DA arg -> List.Cons ((ASM.RealInstruction (ASM.DA arg)), List.Nil)
    25952595| ASM.JC jmp ->
    2596   expand_relative_jump_internal lookup_labels sigma0 policy jmp ppc (fun x ->
     2596  expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
    25972597    ASM.JC x)
    25982598| ASM.JNC jmp ->
    2599   expand_relative_jump_internal lookup_labels sigma0 policy jmp ppc (fun x ->
     2599  expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
    26002600    ASM.JNC x)
    26012601| ASM.JB (baddr, jmp) ->
    2602   expand_relative_jump_internal lookup_labels sigma0 policy jmp ppc (fun x ->
     2602  expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
    26032603    ASM.JB (baddr, x))
    26042604| ASM.JNB (baddr, jmp) ->
    2605   expand_relative_jump_internal lookup_labels sigma0 policy jmp ppc (fun x ->
     2605  expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
    26062606    ASM.JNB (baddr, x))
    26072607| ASM.JBC (baddr, jmp) ->
    2608   expand_relative_jump_internal lookup_labels sigma0 policy jmp ppc (fun x ->
     2608  expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
    26092609    ASM.JBC (baddr, x))
    26102610| ASM.JZ jmp ->
    2611   expand_relative_jump_internal lookup_labels sigma0 policy jmp ppc (fun x ->
     2611  expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
    26122612    ASM.JZ x)
    26132613| ASM.JNZ jmp ->
    2614   expand_relative_jump_internal lookup_labels sigma0 policy jmp ppc (fun x ->
     2614  expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
    26152615    ASM.JNZ x)
    26162616| ASM.CJNE (addr, jmp) ->
    2617   expand_relative_jump_internal lookup_labels sigma0 policy jmp ppc (fun x ->
     2617  expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
    26182618    ASM.CJNE (addr, x))
    26192619| ASM.DJNZ (addr, jmp) ->
    2620   expand_relative_jump_internal lookup_labels sigma0 policy jmp ppc (fun x ->
     2620  expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
    26212621    ASM.DJNZ (addr, x))
    26222622| ASM.ANL arg -> List.Cons ((ASM.RealInstruction (ASM.ANL arg)), List.Nil)
     
    26452645
    26462646(** val expand_pseudo_instruction :
    2647     (ASM.identifier0 -> BitVector.word) -> (BitVector.word -> BitVector.word)
    2648     -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier0 ->
     2647    (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
     2648    -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
    26492649    BitVector.word) -> ASM.pseudo_instruction -> ASM.instruction List.list **)
    2650 let expand_pseudo_instruction lookup_labels sigma0 policy ppc lookup_datalabels = function
     2650let expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels = function
    26512651| ASM.Instruction instr ->
    2652   expand_relative_jump lookup_labels sigma0 policy ppc instr
     2652  expand_relative_jump lookup_labels sigma policy ppc instr
    26532653| ASM.Comment comment -> List.Nil
    26542654| ASM.Cost cost -> List.Nil
    26552655| ASM.Jmp jmp ->
    26562656  let pc_plus_jmp_length =
    2657     sigma0
     2657    sigma
    26582658      (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    26592659        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    26642664  in
    26652665  let do_a_long = policy ppc in
    2666   let lookup_address = sigma0 (lookup_labels jmp) in
     2666  let lookup_address = sigma (lookup_labels jmp) in
    26672667  let { Types.fst = sj_possible; Types.snd = disp } =
    26682668    short_jump_cond pc_plus_jmp_length lookup_address
     
    26842684        List.Cons ((ASM.LJMP address), List.Nil)))
    26852685| ASM.Jnz (acc, tgt1, tgt2) ->
    2686   let lookup_address1 = sigma0 (lookup_labels tgt1) in
    2687   let lookup_address2 = sigma0 (lookup_labels tgt2) in
     2686  let lookup_address1 = sigma (lookup_labels tgt1) in
     2687  let lookup_address2 = sigma (lookup_labels tgt2) in
    26882688  List.Cons ((ASM.RealInstruction (ASM.JNZ (ASM.RELATIVE
    26892689  (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    27372737| ASM.Call call ->
    27382738  let pc_plus_jmp_length =
    2739     sigma0
     2739    sigma
    27402740      (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    27412741        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    27452745          (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
    27462746  in
    2747   let lookup_address = sigma0 (lookup_labels call) in
     2747  let lookup_address = sigma (lookup_labels call) in
    27482748  let { Types.fst = mj_possible; Types.snd = disp } =
    27492749    absolute_jump_cond pc_plus_jmp_length lookup_address
     
    27632763
    27642764(** val assembly_1_pseudoinstruction :
    2765     (ASM.identifier0 -> BitVector.word) -> (BitVector.word -> BitVector.word)
    2766     -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier0 ->
     2765    (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
     2766    -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
    27672767    BitVector.word) -> ASM.pseudo_instruction -> (Nat.nat, Bool.bool
    27682768    Vector.vector List.list) Types.prod **)
    2769 let assembly_1_pseudoinstruction lookup_labels sigma0 policy ppc lookup_datalabels i =
     2769let assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels i =
    27702770  let pseudos =
    2771     expand_pseudo_instruction lookup_labels sigma0 policy ppc
     2771    expand_pseudo_instruction lookup_labels sigma policy ppc
    27722772      lookup_datalabels i
    27732773  in
     
    27782778
    27792779(** val instruction_size :
    2780     (ASM.identifier0 -> BitVector.word) -> (ASM.identifier0 ->
    2781     BitVector.word) -> (BitVector.word -> BitVector.word) -> (BitVector.word
    2782     -> Bool.bool) -> BitVector.word -> ASM.pseudo_instruction -> Nat.nat **)
    2783 let instruction_size lookup_labels lookup_datalabels sigma0 policy ppc i =
    2784   (assembly_1_pseudoinstruction lookup_labels sigma0 policy ppc
     2780    (ASM.identifier -> BitVector.word) -> (ASM.identifier -> BitVector.word)
     2781    -> (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
     2782    BitVector.word -> ASM.pseudo_instruction -> Nat.nat **)
     2783let instruction_size lookup_labels lookup_datalabels sigma policy ppc i =
     2784  (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
    27852785    lookup_datalabels i).Types.fst
    27862786
    27872787(** val assembly :
    27882788    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
    2789     (BitVector.word -> Bool.bool) -> (BitVector.byte List.list,
    2790     CostLabel.costlabel BitVectorTrie.bitVectorTrie) Types.prod Types.sig0 **)
    2791 let assembly p sigma0 policy =
    2792   (let { Types.fst = preamble0; Types.snd = instr_list } = p in
    2793   (fun _ ->
     2789    (BitVector.word -> Bool.bool) -> ASM.labelled_object_code Types.sig0 **)
     2790let assembly p sigma policy =
    27942791  (let { Types.fst = labels_to_ppc; Types.snd = ppc_to_costs } =
    2795      Fetch.create_label_cost_map instr_list
     2792     Fetch.create_label_cost_map p.ASM.code
    27962793   in
    27972794  (fun _ ->
    2798   let datalabels = Status.construct_datalabels preamble0 in
     2795  let preamble = p.ASM.preamble in
     2796  let instr_list = p.ASM.code in
     2797  let datalabels = Status.construct_datalabels preamble in
    27992798  let lookup_labels = fun x ->
    28002799    Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    28112810  (let { Types.fst = next_pc; Types.snd = revcode } =
    28122811     Types.pi1
    2813        (FoldStuff.foldl_strong instr_list (fun prefix0 hd0 tl _ ppc_code ->
     2812       (FoldStuff.foldl_strong instr_list (fun prefix hd tl _ ppc_code ->
    28142813         (let { Types.fst = ppc; Types.snd = code } = Types.pi1 ppc_code in
    28152814         (fun _ ->
    2816          (let { Types.fst = pc_delta; Types.snd = program0 } =
    2817             assembly_1_pseudoinstruction lookup_labels sigma0 policy ppc
    2818               lookup_datalabels hd0.Types.snd
     2815         (let { Types.fst = pc_delta; Types.snd = program } =
     2816            assembly_1_pseudoinstruction lookup_labels sigma policy ppc
     2817              lookup_datalabels hd.Types.snd
    28192818          in
    28202819         (fun _ ->
     
    28282827         in
    28292828         { Types.fst = new_ppc; Types.snd =
    2830          (List.append (List.reverse program0) code) })) __)) __)
    2831          { Types.fst =
     2829         (List.append (List.reverse program) code) })) __)) __) { Types.fst =
    28322830         (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    28332831           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    28342832           Nat.O))))))))))))))))); Types.snd = List.Nil })
    28352833   in
    2836   (fun _ -> { Types.fst = (List.reverse revcode); Types.snd =
    2837   (BitVectorTrie.fold0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    2838     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2834  (fun _ -> { ASM.oc = (List.reverse revcode); ASM.costlabels =
     2835  (BitVectorTrie.fold (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2836    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    28392837    Nat.O)))))))))))))))) (fun ppc cost pc_to_costs ->
    28402838    BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    28412839      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    2842       Nat.O)))))))))))))))) (sigma0 ppc) cost pc_to_costs) ppc_to_costs
     2840      Nat.O)))))))))))))))) (sigma ppc) cost pc_to_costs) ppc_to_costs
    28432841    (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    28442842    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    2845     Nat.O)))))))))))))))))) })) __)) __)) __
    2846 
    2847 (** val assembly_unlabelled_program :
    2848     ASM.assembly_program -> (BitVector.byte List.list, ASM.identifier0
    2849     BitVectorTrie.bitVectorTrie) Types.prod Types.option **)
    2850 let assembly_unlabelled_program p =
    2851   Types.Some { Types.fst =
    2852     (List.foldr (fun i l -> List.append (assembly1 i) l) List.Nil p);
    2853     Types.snd = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2843    Nat.O)))))))))))))))))); ASM.symboltable =
     2844  (Util.foldl (fun symboltable newident_oldident ->
     2845    let ppc = lookup_labels newident_oldident.Types.fst in
     2846    BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2847      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     2848      Nat.O)))))))))))))))) (sigma ppc) newident_oldident.Types.snd
     2849      symboltable) (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    28542850    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    2855     Nat.O))))))))))))))))) }
    2856 
     2851    (Nat.S Nat.O))))))))))))))))) p.ASM.renamed_symbols); ASM.final_pc =
     2852  (assert false (* absurd case *)) })) __)) __
     2853
  • extracted/assembly.mli

    r2717 r2773  
    11open Preamble
    22
     3open BitVectorTrie
     4
    35open String
    4 
    5 open LabelledObjects
    6 
    7 open BitVectorTrie
    86
    97open Exp
     
    119open Arithmetic
    1210
     11open Vector
     12
     13open FoldStuff
     14
     15open BitVector
     16
     17open Extranat
     18
    1319open Integers
    1420
    1521open AST
    1622
    17 open CostLabel
     23open LabelledObjects
    1824
    1925open Proper
     
    3743open Option
    3844
    39 open Lists
    40 
    41 open Positive
    42 
    43 open Identifiers
    44 
    45 open Extranat
    46 
    47 open Vector
    48 
    4945open Div_and_mod
    5046
     
    5349open Russell
    5450
    55 open Types
     51open Util
    5652
    5753open List
    5854
    59 open Util
    60 
    61 open FoldStuff
     55open Lists
    6256
    6357open Bool
     58
     59open Relations
     60
     61open Nat
     62
     63open Positive
    6464
    6565open Hints_declaration
     
    7171open Logic
    7272
    73 open Relations
     73open Types
    7474
    75 open Nat
     75open Identifiers
    7676
    77 open BitVector
     77open CostLabel
    7878
    7979open ASM
     
    134134
    135135val expand_relative_jump_internal :
    136   (ASM.identifier0 -> BitVector.word) -> (BitVector.word -> BitVector.word)
    137   -> (BitVector.word -> Bool.bool) -> ASM.identifier0 -> BitVector.word ->
     136  (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
     137  (BitVector.word -> Bool.bool) -> ASM.identifier -> BitVector.word ->
    138138  (ASM.subaddressing_mode -> ASM.subaddressing_mode ASM.preinstruction) ->
    139139  ASM.instruction List.list
    140140
    141141val expand_relative_jump :
    142   (ASM.identifier0 -> BitVector.word) -> (BitVector.word -> BitVector.word)
    143   -> (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.identifier0
     142  (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
     143  (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.identifier
    144144  ASM.preinstruction -> ASM.instruction List.list
    145145
    146146val expand_pseudo_instruction :
    147   (ASM.identifier0 -> BitVector.word) -> (BitVector.word -> BitVector.word)
    148   -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier0 ->
     147  (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
     148  (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
    149149  BitVector.word) -> ASM.pseudo_instruction -> ASM.instruction List.list
    150150
    151151val assembly_1_pseudoinstruction :
    152   (ASM.identifier0 -> BitVector.word) -> (BitVector.word -> BitVector.word)
    153   -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier0 ->
     152  (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
     153  (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
    154154  BitVector.word) -> ASM.pseudo_instruction -> (Nat.nat, Bool.bool
    155155  Vector.vector List.list) Types.prod
    156156
    157157val instruction_size :
    158   (ASM.identifier0 -> BitVector.word) -> (ASM.identifier0 -> BitVector.word)
    159   -> (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
     158  (ASM.identifier -> BitVector.word) -> (ASM.identifier -> BitVector.word) ->
     159  (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
    160160  BitVector.word -> ASM.pseudo_instruction -> Nat.nat
    161161
    162162val assembly :
    163163  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
    164   (BitVector.word -> Bool.bool) -> (BitVector.byte List.list,
    165   CostLabel.costlabel BitVectorTrie.bitVectorTrie) Types.prod Types.sig0
     164  (BitVector.word -> Bool.bool) -> ASM.labelled_object_code Types.sig0
    166165
    167 val assembly_unlabelled_program :
    168   ASM.assembly_program -> (BitVector.byte List.list, ASM.identifier0
    169   BitVectorTrie.bitVectorTrie) Types.prod Types.option
    170 
  • extracted/assocList.ml

    r2717 r2773  
    3232let rec assoc_list_exists a eq = function
    3333| List.Nil -> Bool.False
    34 | List.Cons (hd0, tl) ->
    35   Bool.orb (eq hd0.Types.fst a) (assoc_list_exists a eq tl)
     34| List.Cons (hd, tl) ->
     35  Bool.orb (eq hd.Types.fst a) (assoc_list_exists a eq tl)
    3636
    3737(** val assoc_list_lookup :
     
    4040let rec assoc_list_lookup a eq = function
    4141| List.Nil -> Types.None
    42 | List.Cons (hd0, tl) ->
    43   (match eq hd0.Types.fst a with
    44    | Bool.True -> Types.Some hd0.Types.snd
     42| List.Cons (hd, tl) ->
     43  (match eq hd.Types.fst a with
     44   | Bool.True -> Types.Some hd.Types.snd
    4545   | Bool.False -> assoc_list_lookup a eq tl)
    4646
  • extracted/backEndOps.ml

    r2743 r2773  
    1717open Extralib
    1818
     19open Lists
     20
     21open Identifiers
     22
     23open Integers
     24
     25open AST
     26
     27open Division
     28
     29open Exp
     30
     31open Arithmetic
     32
    1933open Setoids
    2034
     
    2236
    2337open Option
    24 
    25 open Lists
    26 
    27 open Identifiers
    28 
    29 open Integers
    30 
    31 open AST
    32 
    33 open Division
    34 
    35 open Exp
    36 
    37 open Arithmetic
    3838
    3939open Extranat
     
    402402    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    403403    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    404 let rec eval_rect_Type4 h_mk_Eval x_18831 =
    405   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18831 in
     404let rec eval_rect_Type4 h_mk_Eval x_14141 =
     405  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14141 in
    406406  h_mk_Eval opaccs0 op4 op5
    407407
     
    411411    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    412412    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    413 let rec eval_rect_Type5 h_mk_Eval x_18833 =
    414   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18833 in
     413let rec eval_rect_Type5 h_mk_Eval x_14143 =
     414  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14143 in
    415415  h_mk_Eval opaccs0 op4 op5
    416416
     
    420420    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    421421    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    422 let rec eval_rect_Type3 h_mk_Eval x_18835 =
    423   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18835 in
     422let rec eval_rect_Type3 h_mk_Eval x_14145 =
     423  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14145 in
    424424  h_mk_Eval opaccs0 op4 op5
    425425
     
    429429    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    430430    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    431 let rec eval_rect_Type2 h_mk_Eval x_18837 =
    432   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18837 in
     431let rec eval_rect_Type2 h_mk_Eval x_14147 =
     432  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14147 in
    433433  h_mk_Eval opaccs0 op4 op5
    434434
     
    438438    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    439439    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    440 let rec eval_rect_Type1 h_mk_Eval x_18839 =
    441   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18839 in
     440let rec eval_rect_Type1 h_mk_Eval x_14149 =
     441  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14149 in
    442442  h_mk_Eval opaccs0 op4 op5
    443443
     
    447447    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    448448    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    449 let rec eval_rect_Type0 h_mk_Eval x_18841 =
    450   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18841 in
     449let rec eval_rect_Type0 h_mk_Eval x_14151 =
     450  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14151 in
    451451  h_mk_Eval opaccs0 op4 op5
    452452
     
    522522    opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
    523523    BitVector.byte) Types.prod **)
    524 let opaccs_implementation op4 by1 by2 =
     524let opaccs_implementation op by1 by2 =
    525525  let n1 =
    526526    BitVectorZ.z_of_unsigned_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    531531      (Nat.S (Nat.S (Nat.S Nat.O)))))))) by2
    532532  in
    533   (match op4 with
     533  (match op with
    534534   | Mul ->
    535      let prod0 =
     535     let prod =
    536536       Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    537537         Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    542542             (Nat.S Nat.O))))))))) (Z.z_times n1 n2))
    543543     in
    544      { Types.fst = prod0.Types.snd; Types.snd = prod0.Types.fst }
     544     { Types.fst = prod.Types.snd; Types.snd = prod.Types.fst }
    545545   | DivuModu ->
    546546     (match Z.eqZb n2 Z.OZ with
     
    555555
    556556(** val op1_implementation : op1 -> BitVector.byte -> BitVector.byte **)
    557 let op1_implementation op4 by =
    558   match op4 with
     557let op1_implementation op by =
     558  match op with
    559559  | Cmpl ->
    560560    BitVector.negation_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    572572    BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    573573    (BitVector.byte, BitVector.bit) Types.prod **)
    574 let op2_implementation carry op4 by1 by2 =
    575   match op4 with
     574let op2_implementation carry op by1 by2 =
     575  match op with
    576576  | Add ->
    577     let { Types.fst = res1; Types.snd = flags } =
     577    let { Types.fst = res; Types.snd = flags } =
    578578      Arithmetic.add_8_with_carry by1 by2 Bool.False
    579579    in
    580     { Types.fst = res1; Types.snd =
     580    { Types.fst = res; Types.snd =
    581581    (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
    582582  | Addc ->
    583     let { Types.fst = res1; Types.snd = flags } =
     583    let { Types.fst = res; Types.snd = flags } =
    584584      Arithmetic.add_8_with_carry by1 by2 carry
    585585    in
    586     { Types.fst = res1; Types.snd =
     586    { Types.fst = res; Types.snd =
    587587    (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
    588588  | Sub ->
    589     let { Types.fst = res1; Types.snd = flags } =
     589    let { Types.fst = res; Types.snd = flags } =
    590590      Arithmetic.sub_8_with_carry by1 by2 carry
    591591    in
    592     { Types.fst = res1; Types.snd =
     592    { Types.fst = res; Types.snd =
    593593    (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
    594594  | And ->
     
    613613    opAccs -> ByteValues.beval -> ByteValues.beval -> (ByteValues.beval,
    614614    ByteValues.beval) Types.prod Errors.res **)
    615 let be_opaccs op4 a b =
     615let be_opaccs op a b =
    616616  Obj.magic
    617617    (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    621621        (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp b))
    622622        (fun b' ->
    623         let { Types.fst = a''; Types.snd = b'' } = eval0.opaccs op4 a' b' in
     623        let { Types.fst = a''; Types.snd = b'' } = eval0.opaccs op a' b' in
    624624        Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    625625          (ByteValues.BVByte a''); Types.snd = (ByteValues.BVByte b'') })))
    626626
    627627(** val be_op1 : op1 -> ByteValues.beval -> ByteValues.beval Errors.res **)
    628 let be_op1 op4 a =
     628let be_op1 op a =
    629629  Obj.magic
    630630    (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    632632      (fun a' ->
    633633      Monad.m_return0 (Monad.max_def Errors.res0) (ByteValues.BVByte
    634         (eval0.op0 op4 a'))))
     634        (eval0.op0 op a'))))
    635635
    636636(** val op2_bytes :
     
    638638    BitVector.byte Vector.vector -> (BitVector.byte Vector.vector,
    639639    BitVector.bit) Types.prod **)
    640 let op2_bytes op4 n carry =
     640let op2_bytes op n carry =
    641641  let f = fun n0 b1 b2 pr ->
    642642    let { Types.fst = res_tl; Types.snd = carry0 } = pr in
    643643    let { Types.fst = res_hd; Types.snd = carry' } =
    644       eval0.op3 carry0 op4 b1 b2
     644      eval0.op3 carry0 op b1 b2
    645645    in
    646646    { Types.fst = (Vector.VCons (n0, res_hd, res_tl)); Types.snd = carry' }
     
    652652    (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res **)
    653653let be_add_sub_byte is_add carry a1 b2 =
    654   let op4 =
     654  let op =
    655655    match is_add with
    656656    | Bool.True -> Addc
     
    674674         (fun carry' ->
    675675         let { Types.fst = rslt; Types.snd = carry'' } =
    676            eval0.op3 carry' op4 b1 b2
     676           eval0.op3 carry' op b1 b2
    677677         in
    678678         Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     
    703703                 in
    704704                 let { Types.fst = rslt; Types.snd = carry0 } =
    705                    eval0.op3 Bool.False op4 b2 o1o0.Types.snd
     705                   eval0.op3 Bool.False op b2 o1o0.Types.snd
    706706                 in
    707707                 let p0 = Nat.O in
    708708                 let ptr' = { Pointers.pblock = ptr.Pointers.pblock;
    709709                   Pointers.poff =
    710                    (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     710                   (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    711711                     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
    712712                     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) o1o0.Types.fst
     
    750750                   in
    751751                   let { Types.fst = rslt; Types.snd = ignore } =
    752                      op2_bytes op4 (Nat.S (Nat.S Nat.O)) Bool.False o1o1
     752                     op2_bytes op (Nat.S (Nat.S Nat.O)) Bool.False o1o1
    753753                       (Vector.VCons ((Nat.S Nat.O), b2, (Vector.VCons
    754754                       (Nat.O, by'0, Vector.VEmpty))))
     
    763763                   Errors.OK { Types.fst = (ByteValues.BVptr (ptr'0, part1));
    764764                   Types.snd = (ByteValues.BBptrcarry (is_add, ptr'0, part1,
    765                    (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     765                   (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    766766                     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
    767767                     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) b2 by'0))) })
     
    798798    ('a1 -> 'a1 -> Bool.bool) -> 'a1 Types.option -> 'a1 Types.option ->
    799799    Bool.bool **)
    800 let eq_opt eq0 m n =
     800let eq_opt eq m n =
    801801  match m with
    802802  | Types.None ->
     
    807807    (match n with
    808808     | Types.None -> Bool.False
    809      | Types.Some b -> eq0 a b)
     809     | Types.Some b -> eq a b)
    810810
    811811(** val be_op2 :
    812812    ByteValues.bebit -> op2 -> ByteValues.beval -> ByteValues.beval ->
    813813    (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res **)
    814 let be_op2 carry op4 a1 a2 =
     814let be_op2 carry op a1 a2 =
    815815  match a1 with
    816816  | ByteValues.BVundef ->
     
    823823         List.Nil))
    824824     | ByteValues.BVnonzero ->
    825        (match op4 with
     825       (match op with
    826826        | Add ->
    827827          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    844844            List.Nil)))
    845845     | ByteValues.BVXor (x, x0, x1) ->
    846        (match op4 with
     846       (match op with
    847847        | Add ->
    848848          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    865865            List.Nil)))
    866866     | ByteValues.BVByte x ->
    867        (match op4 with
     867       (match op with
    868868        | Add ->
    869869          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    894894       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    895895         List.Nil)))
    896   | ByteValues.BVXor (ptr1_opt, ptr1_opt', p3) ->
     896  | ByteValues.BVXor (ptr1_opt, ptr1_opt', p1) ->
    897897    (match a2 with
    898898     | ByteValues.BVundef ->
     
    900900         List.Nil))
    901901     | ByteValues.BVnonzero ->
    902        (match op4 with
     902       (match op with
    903903        | Add ->
    904904          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    920920          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    921921            List.Nil)))
    922      | ByteValues.BVXor (ptr2_opt, ptr2_opt', p4) ->
    923        (match op4 with
     922     | ByteValues.BVXor (ptr2_opt, ptr2_opt', p2) ->
     923       (match op with
    924924        | Add ->
    925925          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    936936        | Or ->
    937937          (match Bool.orb
    938                    (Bool.andb (Nat.eqb (ByteValues.part_no p3) Nat.O)
    939                      (Nat.eqb (ByteValues.part_no p4) (Nat.S Nat.O)))
    940                    (Bool.andb (Nat.eqb (ByteValues.part_no p3) (Nat.S Nat.O))
    941                      (Nat.eqb (ByteValues.part_no p4) Nat.O)) with
     938                   (Bool.andb (Nat.eqb (ByteValues.part_no p1) Nat.O)
     939                     (Nat.eqb (ByteValues.part_no p2) (Nat.S Nat.O)))
     940                   (Bool.andb (Nat.eqb (ByteValues.part_no p1) (Nat.S Nat.O))
     941                     (Nat.eqb (ByteValues.part_no p2) Nat.O)) with
    942942           | Bool.True ->
    943943             let eq_at = fun p ptr1 ptr2 ->
     
    954954                     (ByteValues.part_no p)))
    955955             in
    956              (match Bool.andb (eq_opt (eq_at p3) ptr1_opt ptr1_opt')
    957                       (eq_opt (eq_at p4) ptr2_opt ptr2_opt') with
     956             (match Bool.andb (eq_opt (eq_at p1) ptr1_opt ptr1_opt')
     957                      (eq_opt (eq_at p2) ptr2_opt ptr2_opt') with
    958958              | Bool.True ->
    959959                Obj.magic
     
    973973            List.Nil)))
    974974     | ByteValues.BVByte b2 ->
    975        (match op4 with
     975       (match op with
    976976        | Add ->
    977977          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    10161016         List.Nil))
    10171017     | ByteValues.BVnonzero ->
    1018        (match op4 with
     1018       (match op with
    10191019        | Add ->
    10201020          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    10461046           (fun carry0 ->
    10471047           let { Types.fst = result; Types.snd = carry1 } =
    1048              eval0.op3 carry0 op4 b1 b2
     1048             eval0.op3 carry0 op b1 b2
    10491049           in
    10501050           Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     
    10551055         List.Nil))
    10561056     | ByteValues.BVptr (x, x0) ->
    1057        (match op4 with
     1057       (match op with
    10581058        | Add ->
    10591059          be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a2 b1
     
    10741074       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    10751075         List.Nil)))
    1076   | ByteValues.BVnull p3 ->
     1076  | ByteValues.BVnull p1 ->
    10771077    (match a2 with
    10781078     | ByteValues.BVundef ->
     
    10881088       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    10891089         List.Nil))
    1090      | ByteValues.BVnull p4 ->
    1091        (match op4 with
     1090     | ByteValues.BVnull p2 ->
     1091       (match op with
    10921092        | Add ->
    10931093          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    11061106            List.Nil))
    11071107        | Xor ->
    1108           (match Nat.eqb (ByteValues.part_no p3) (ByteValues.part_no p4) with
     1108          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
    11091109           | Bool.True ->
    11101110             Obj.magic
    11111111               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    1112                  (ByteValues.BVXor (Types.None, Types.None, p3)); Types.snd =
     1112                 (ByteValues.BVXor (Types.None, Types.None, p1)); Types.snd =
    11131113                 carry })
    11141114           | Bool.False ->
    11151115             Errors.Error (List.Cons ((Errors.MSG
    11161116               ErrorMessages.UnsupportedOp), List.Nil))))
    1117      | ByteValues.BVptr (ptr2, p4) ->
    1118        (match op4 with
     1117     | ByteValues.BVptr (ptr2, p2) ->
     1118       (match op with
    11191119        | Add ->
    11201120          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    11331133            List.Nil))
    11341134        | Xor ->
    1135           (match Nat.eqb (ByteValues.part_no p3) (ByteValues.part_no p4) with
     1135          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
    11361136           | Bool.True ->
    11371137             Obj.magic
    11381138               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    1139                  (ByteValues.BVXor (Types.None, (Types.Some ptr2), p3));
     1139                 (ByteValues.BVXor (Types.None, (Types.Some ptr2), p1));
    11401140                 Types.snd = carry })
    11411141           | Bool.False ->
     
    11451145       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    11461146         List.Nil)))
    1147   | ByteValues.BVptr (ptr1, p3) ->
     1147  | ByteValues.BVptr (ptr1, p1) ->
    11481148    (match a2 with
    11491149     | ByteValues.BVundef ->
     
    11571157         List.Nil))
    11581158     | ByteValues.BVByte b2 ->
    1159        (match op4 with
     1159       (match op with
    11601160        | Add ->
    11611161          be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a1 b2
     
    11711171          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    11721172            List.Nil)))
    1173      | ByteValues.BVnull p4 ->
    1174        (match op4 with
     1173     | ByteValues.BVnull p2 ->
     1174       (match op with
    11751175        | Add ->
    11761176          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    11891189            List.Nil))
    11901190        | Xor ->
    1191           (match Nat.eqb (ByteValues.part_no p3) (ByteValues.part_no p4) with
     1191          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
    11921192           | Bool.True ->
    11931193             Obj.magic
    11941194               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    1195                  (ByteValues.BVXor ((Types.Some ptr1), Types.None, p3));
     1195                 (ByteValues.BVXor ((Types.Some ptr1), Types.None, p1));
    11961196                 Types.snd = carry })
    11971197           | Bool.False ->
    11981198             Errors.Error (List.Cons ((Errors.MSG
    11991199               ErrorMessages.UnsupportedOp), List.Nil))))
    1200      | ByteValues.BVptr (ptr2, p4) ->
    1201        (match op4 with
     1200     | ByteValues.BVptr (ptr2, p2) ->
     1201       (match op with
    12021202        | Add ->
    12031203          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    12121212                      (Pointers.eq_block ptr1.Pointers.pblock
    12131213                        ptr2.Pointers.pblock)
    1214                       (Nat.eqb (ByteValues.part_no p3)
    1215                         (ByteValues.part_no p4)) with
     1214                      (Nat.eqb (ByteValues.part_no p1)
     1215                        (ByteValues.part_no p2)) with
    12161216              | Bool.True ->
    12171217                Obj.magic
     
    12231223                      byte_at AST.size_pointer
    12241224                        (Pointers.offv ptr1.Pointers.poff)
    1225                         (ByteValues.part_no p3)
     1225                        (ByteValues.part_no p1)
    12261226                    in
    12271227                    let by2 =
    12281228                      byte_at AST.size_pointer
    12291229                        (Pointers.offv ptr2.Pointers.poff)
    1230                         (ByteValues.part_no p3)
     1230                        (ByteValues.part_no p1)
    12311231                    in
    12321232                    let { Types.fst = result; Types.snd = carry1 } =
     
    12491249            List.Nil))
    12501250        | Xor ->
    1251           (match Nat.eqb (ByteValues.part_no p3) (ByteValues.part_no p4) with
     1251          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
    12521252           | Bool.True ->
    12531253             Obj.magic
    12541254               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    12551255                 (ByteValues.BVXor ((Types.Some ptr1), (Types.Some ptr2),
    1256                  p3)); Types.snd = carry })
     1256                 p1)); Types.snd = carry })
    12571257           | Bool.False ->
    12581258             Errors.Error (List.Cons ((Errors.MSG
  • extracted/backEndOps.mli

    r2730 r2773  
    1717open Extralib
    1818
     19open Lists
     20
     21open Identifiers
     22
     23open Integers
     24
     25open AST
     26
     27open Division
     28
     29open Exp
     30
     31open Arithmetic
     32
    1933open Setoids
    2034
     
    2236
    2337open Option
    24 
    25 open Lists
    26 
    27 open Identifiers
    28 
    29 open Integers
    30 
    31 open AST
    32 
    33 open Division
    34 
    35 open Exp
    36 
    37 open Arithmetic
    3838
    3939open Extranat
  • extracted/bindLists.ml

    r2743 r2773  
    6868      (Obj.magic x))
    6969
     70open Option
     71
    7072open Extranat
    7173
     
    7779
    7880(** val bcons : 'a2 -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list **)
    79 let bcons e0 =
     81let bcons e =
    8082  Obj.magic
    81     (Monad.m_map (Monad.max_def Bind_new.bindNew) (fun x -> List.Cons (e0,
     83    (Monad.m_map (Monad.max_def Bind_new.bindNew) (fun x -> List.Cons (e,
    8284      x)))
    83