open Preamble

open Div_and_mod

open Jmeq

open Russell

open Util

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Extralib

open Status

open BitVectorTrie

open String

open Integers

open AST

open LabelledObjects

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Lists

open Positive

open Identifiers

open CostLabel

open ASM

open Exp

open Setoids

open Monad

open Option

open Extranat

open Vector

open FoldStuff

open BitVector

open Arithmetic

open Fetch

open Assembly

type ppc_pc_map =
  (Nat.nat, (Nat.nat, Assembly.jump_length) Types.prod
  BitVectorTrie.bitVectorTrie) Types.prod

val jmpeqb : Assembly.jump_length -> Assembly.jump_length -> Bool.bool

val expand_relative_jump_internal_unsafe :
  Assembly.jump_length -> (ASM.subaddressing_mode -> ASM.subaddressing_mode
  ASM.preinstruction) -> ASM.instruction List.list

val strip_target :
  ASM.identifier ASM.preinstruction -> (ASM.subaddressing_mode ->
  ASM.subaddressing_mode ASM.preinstruction, ASM.instruction) Types.sum

val expand_relative_jump_unsafe :
  Assembly.jump_length -> ASM.identifier ASM.preinstruction ->
  ASM.instruction List.list

val expand_pseudo_instruction_unsafe :
  Assembly.jump_length -> ASM.pseudo_instruction -> ASM.instruction List.list

val instruction_size_jmplen :
  Assembly.jump_length -> ASM.pseudo_instruction -> Nat.nat

val max_length :
  Assembly.jump_length -> Assembly.jump_length -> Assembly.jump_length

val dec_jmple :
  Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum

val dec_eq_jump_length :
  Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum

val create_label_map :
  ASM.labelled_instruction List.list -> Fetch.label_map Types.sig0

val select_reljump_length :
  Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier ->
  Nat.nat -> Assembly.jump_length

val select_call_length :
  Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier ->
  Assembly.jump_length

val select_jump_length :
  Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier ->
  Assembly.jump_length

val destination_of :
  ASM.identifier ASM.preinstruction -> ASM.identifier Types.option

val length_of : ASM.identifier ASM.preinstruction -> Nat.nat

val jump_expansion_step_instruction :
  Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
  ASM.preinstruction -> Assembly.jump_length Types.option

val jump_expansion_start :
  ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map ->
  ppc_pc_map Types.option Types.sig0