extracted/interpret.mli

   1 open Preamble
   2
   3 open BitVectorTrie
   4
   5 open String
   6
   7 open Exp
   8
   9 open Arithmetic
  10
  11 open Vector
  12
  13 open FoldStuff
  14
  15 open BitVector
  16
  17 open Extranat
  18
  19 open Integers
  20
  21 open AST
  22
  23 open LabelledObjects
  24
  25 open Proper
  26
  27 open PositiveMap
  28
  29 open Deqsets
  30
  31 open ErrorMessages
  32
  33 open PreIdentifiers
  34
  35 open Errors
  36
  37 open Extralib
  38
  39 open Setoids
  40
  41 open Monad
  42
  43 open Option
  44
  45 open Div_and_mod
  46
  47 open Util
  48
  49 open List
  50
  51 open Lists
  52
  53 open Bool
  54
  55 open Relations
  56
  57 open Nat
  58
  59 open Positive
  60
  61 open Identifiers
  62
  63 open CostLabel
  64
  65 open ASM
  66
  67 open Types
  68
  69 open Hints_declaration
  70
  71 open Core_notation
  72
  73 open Pts
  74
  75 open Logic
  76
  77 open Jmeq
  78
  79 open Russell
  80
  81 open Status
  82
  83 open StatusProofs
  84
  85 open Fetch
  86
  87 open Hide
  88
  89 open Division
  90
  91 open Z
  92
  93 open BitVectorZ
  94
  95 open Pointers
  96
  97 open Coqlib
  98
  99 open Values
 100
 101 open Events
 102
 103 open IOMonad
 104
 105 open IO
 106
 107 open Sets
 108
 109 open Listb
 110
 111 open StructuredTraces
 112
 113 open AbstractStatus
 114
 115 val execute_1_preinstruction :
 116   (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
 117   BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
 118   Status.preStatus
 119
 120 val execute_1_preinstruction_ok' :
 121   (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
 122   BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
 123   Status.preStatus Types.sig0
 124
 125 val compute_target_of_unconditional_jump :
 126   BitVector.word -> ASM.instruction -> BitVector.word
 127
 128 val is_unconditional_jump : ASM.instruction -> Bool.bool
 129
 130 val program_counter_after_other :
 131   BitVector.word -> ASM.instruction -> BitVector.word
 132
 133 val addr_of_relative :
 134   'a1 -> ASM.subaddressing_mode -> 'a1 Status.preStatus -> BitVector.word
 135
 136 val execute_1_0 :
 137   BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
 138   ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod ->
 139   Status.status Types.sig0
 140
 141 val current_instruction_cost :
 142   BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status -> Nat.nat
 143
 144 val execute_1' :
 145   BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
 146   Status.status Types.sig0
 147
 148 val execute_1 :
 149   BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
 150   Status.status
 151
 152 val execute_1_pseudo_instruction0 :
 153   (Nat.nat, Nat.nat) Types.prod -> ASM.pseudo_assembly_program ->
 154   (ASM.identifier -> BitVector.word) -> (ASM.identifier -> BitVector.word) ->
 155   Status.pseudoStatus -> ASM.pseudo_instruction -> BitVector.word ->
 156   Status.pseudoStatus
 157
 158 val execute_1_pseudo_instruction :
 159   ASM.pseudo_assembly_program -> (BitVector.word -> __ -> (Nat.nat, Nat.nat)
 160   Types.prod) -> (ASM.identifier -> BitVector.word) -> (ASM.identifier ->
 161   BitVector.word) -> Status.pseudoStatus -> Status.pseudoStatus
 162
 163 val execute :
 164   Nat.nat -> BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
 165   Status.status
 166