extracted/policyFront.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 Status
  32
  33 open BitVectorTrie
  34
  35 open String
  36
  37 open Integers
  38
  39 open AST
  40
  41 open LabelledObjects
  42
  43 open Proper
  44
  45 open PositiveMap
  46
  47 open Deqsets
  48
  49 open ErrorMessages
  50
  51 open PreIdentifiers
  52
  53 open Errors
  54
  55 open Lists
  56
  57 open Positive
  58
  59 open Identifiers
  60
  61 open CostLabel
  62
  63 open ASM
  64
  65 open Exp
  66
  67 open Setoids
  68
  69 open Monad
  70
  71 open Option
  72
  73 open Extranat
  74
  75 open Vector
  76
  77 open FoldStuff
  78
  79 open BitVector
  80
  81 open Arithmetic
  82
  83 open Fetch
  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