extracted/assembly.mli

   1 open Preamble
   2
   3 open Div_and_mod
   4
   5 open Jmeq
   6
   7 open Russell
   8
   9 open Util
  10
  11 open Bool
  12
  13 open Relations
  14
  15 open Nat
  16
  17 open List
  18
  19 open Hints_declaration
  20
  21 open Core_notation
  22
  23 open Pts
  24
  25 open Logic
  26
  27 open Types
  28
  29 open Extralib
  30
  31 open BitVectorTrie
  32
  33 open String
  34
  35 open Integers
  36
  37 open AST
  38
  39 open LabelledObjects
  40
  41 open Proper
  42
  43 open PositiveMap
  44
  45 open Deqsets
  46
  47 open ErrorMessages
  48
  49 open PreIdentifiers
  50
  51 open Errors
  52
  53 open Lists
  54
  55 open Positive
  56
  57 open Identifiers
  58
  59 open CostLabel
  60
  61 open ASM
  62
  63 open Exp
  64
  65 open Setoids
  66
  67 open Monad
  68
  69 open Option
  70
  71 open Extranat
  72
  73 open Vector
  74
  75 open FoldStuff
  76
  77 open BitVector
  78
  79 open Arithmetic
  80
  81 open Fetch
  82
  83 open Status
  84
  85 type jump_length =
  86 | Short_jump
  87 | Absolute_jump
  88 | Long_jump
  89
  90 val jump_length_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
  91
  92 val jump_length_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
  93
  94 val jump_length_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
  95
  96 val jump_length_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
  97
  98 val jump_length_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
  99
 100 val jump_length_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
 101
 102 val jump_length_inv_rect_Type4 :
 103   jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 104
 105 val jump_length_inv_rect_Type3 :
 106   jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 107
 108 val jump_length_inv_rect_Type2 :
 109   jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 110
 111 val jump_length_inv_rect_Type1 :
 112   jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 113
 114 val jump_length_inv_rect_Type0 :
 115   jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 116
 117 val jump_length_discr : jump_length -> jump_length -> __
 118
 119 val jump_length_jmdiscr : jump_length -> jump_length -> __
 120
 121 val short_jump_cond :
 122   BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector)
 123   Types.prod
 124
 125 val absolute_jump_cond :
 126   BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector)
 127   Types.prod
 128
 129 val assembly_preinstruction :
 130   ('a1 -> BitVector.byte) -> 'a1 ASM.preinstruction -> Bool.bool
 131   Vector.vector List.list
 132
 133 val assembly1 : ASM.instruction -> Bool.bool Vector.vector List.list
 134
 135 val expand_relative_jump_internal :
 136   (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
 137   (BitVector.word -> Bool.bool) -> ASM.identifier -> BitVector.word ->
 138   (ASM.subaddressing_mode -> ASM.subaddressing_mode ASM.preinstruction) ->
 139   ASM.instruction List.list
 140
 141 val expand_relative_jump :
 142   (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
 143   (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.identifier
 144   ASM.preinstruction -> ASM.instruction List.list
 145
 146 val is_code : AST.region -> Bool.bool
 147
 148 val expand_pseudo_instruction :
 149   (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
 150   (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
 151   (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
 152   ASM.instruction List.list
 153
 154 val assembly_1_pseudoinstruction :
 155   (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
 156   (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
 157   (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
 158   (Nat.nat, Bool.bool Vector.vector List.list) Types.prod
 159
 160 val instruction_size :
 161   (ASM.identifier -> BitVector.word) -> (ASM.identifier -> (AST.region,
 162   BitVector.word) Types.prod) -> (BitVector.word -> BitVector.word) ->
 163   (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.pseudo_instruction
 164   -> Nat.nat
 165
 166 val assembly :
 167   ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
 168   (BitVector.word -> Bool.bool) -> ASM.labelled_object_code Types.sig0
 169
 170 val ticks_of_instruction : ASM.instruction -> Nat.nat
 171
 172 val ticks_of0 :
 173   ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
 174   (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
 175   BitVector.word -> ASM.pseudo_instruction -> (Nat.nat, Nat.nat) Types.prod
 176
 177 val ticks_of :
 178   ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
 179   (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
 180   BitVector.word -> (Nat.nat, Nat.nat) Types.prod
 181