extracted/policyFront.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 Jmeq
  48
  49 open Russell
  50
  51 open Util
  52
  53 open List
  54
  55 open Lists
  56
  57 open Bool
  58
  59 open Relations
  60
  61 open Nat
  62
  63 open Positive
  64
  65 open Hints_declaration
  66
  67 open Core_notation
  68
  69 open Pts
  70
  71 open Logic
  72
  73 open Types
  74
  75 open Identifiers
  76
  77 open CostLabel
  78
  79 open ASM
  80
  81 open Fetch
  82
  83 open Status
  84
  85 open Assembly
  86
  87 type ppc_pc_map =
  88   (Nat.nat, (Nat.nat, Assembly.jump_length) Types.prod
  89   BitVectorTrie.bitVectorTrie) Types.prod
  90
  91 val jmpeqb : Assembly.jump_length -> Assembly.jump_length -> Bool.bool
  92
  93 val expand_relative_jump_internal_unsafe :
  94   Assembly.jump_length -> (ASM.subaddressing_mode -> ASM.subaddressing_mode
  95   ASM.preinstruction) -> ASM.instruction List.list
  96
  97 val strip_target :
  98   ASM.identifier ASM.preinstruction -> (ASM.subaddressing_mode ->
  99   ASM.subaddressing_mode ASM.preinstruction, ASM.instruction) Types.sum
 100
 101 val expand_relative_jump_unsafe :
 102   Assembly.jump_length -> ASM.identifier ASM.preinstruction ->
 103   ASM.instruction List.list
 104
 105 val expand_pseudo_instruction_unsafe :
 106   Assembly.jump_length -> ASM.pseudo_instruction -> ASM.instruction List.list
 107
 108 val instruction_size_jmplen :
 109   Assembly.jump_length -> ASM.pseudo_instruction -> Nat.nat
 110
 111 val max_length :
 112   Assembly.jump_length -> Assembly.jump_length -> Assembly.jump_length
 113
 114 val dec_jmple :
 115   Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum
 116
 117 val dec_eq_jump_length :
 118   Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum
 119
 120 val create_label_map :
 121   ASM.labelled_instruction List.list -> Fetch.label_map Types.sig0
 122
 123 val select_reljump_length :
 124   Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier ->
 125   Nat.nat -> Assembly.jump_length
 126
 127 val select_call_length :
 128   Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier ->
 129   Assembly.jump_length
 130
 131 val select_jump_length :
 132   Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier ->
 133   Assembly.jump_length
 134
 135 val destination_of :
 136   ASM.identifier ASM.preinstruction -> ASM.identifier Types.option
 137
 138 val length_of : ASM.identifier ASM.preinstruction -> Nat.nat
 139
 140 val jump_expansion_step_instruction :
 141   Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
 142   ASM.preinstruction -> Assembly.jump_length Types.option
 143
 144 val jump_expansion_start :
 145   ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map ->
 146   ppc_pc_map Types.option Types.sig0
 147