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 **)
let jmpeqb j1 j2 =
  match j1 with
  | Assembly.Short_jump ->
    (match j2 with
     | Assembly.Short_jump -> Bool.True
     | Assembly.Absolute_jump -> Bool.False
     | Assembly.Long_jump -> Bool.False)
  | Assembly.Absolute_jump ->
    (match j2 with
     | Assembly.Short_jump -> Bool.False
     | Assembly.Absolute_jump -> Bool.True
     | Assembly.Long_jump -> Bool.False)
  | Assembly.Long_jump ->
    (match j2 with
     | Assembly.Short_jump -> Bool.False
     | Assembly.Absolute_jump -> Bool.False
     | Assembly.Long_jump -> Bool.True)

(** val expand_relative_jump_internal_unsafe :
    Assembly.jump_length -> (ASM.subaddressing_mode -> ASM.subaddressing_mode
    ASM.preinstruction) -> ASM.instruction List.list **)
let expand_relative_jump_internal_unsafe jmp_len i =
  match jmp_len with
  | Assembly.Short_jump ->
    List.Cons ((ASM.RealInstruction
      (i (ASM.RELATIVE
        (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S Nat.O)))))))))))), List.Nil)
  | Assembly.Absolute_jump -> List.Nil
  | Assembly.Long_jump ->
    List.Cons ((ASM.RealInstruction
      (i (ASM.RELATIVE
        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S Nat.O)))))),
      (List.Cons ((ASM.SJMP (ASM.RELATIVE
      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S Nat.O)))))),
      (List.Cons ((ASM.LJMP (ASM.ADDR16
      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O))))))))))))))))))), List.Nil)))))

(** val strip_target :
    ASM.identifier ASM.preinstruction -> (ASM.subaddressing_mode ->
    ASM.subaddressing_mode ASM.preinstruction, ASM.instruction) Types.sum **)
let strip_target = function
| ASM.ADD (arg1, arg2) ->
  Types.Inr (ASM.RealInstruction (ASM.ADD (arg1, arg2)))
| ASM.ADDC (arg1, arg2) ->
  Types.Inr (ASM.RealInstruction (ASM.ADDC (arg1, arg2)))
| ASM.SUBB (arg1, arg2) ->
  Types.Inr (ASM.RealInstruction (ASM.SUBB (arg1, arg2)))
| ASM.INC arg -> Types.Inr (ASM.RealInstruction (ASM.INC arg))
| ASM.DEC arg -> Types.Inr (ASM.RealInstruction (ASM.DEC arg))
| ASM.MUL (arg1, arg2) ->
  Types.Inr (ASM.RealInstruction (ASM.MUL (arg1, arg2)))
| ASM.DIV (arg1, arg2) ->
  Types.Inr (ASM.RealInstruction (ASM.DIV (arg1, arg2)))
| ASM.DA arg -> Types.Inr (ASM.RealInstruction (ASM.DA arg))
| ASM.JC x -> Types.Inl (fun x0 -> ASM.JC x0)
| ASM.JNC x -> Types.Inl (fun x0 -> ASM.JNC x0)
| ASM.JB (baddr, x) -> Types.Inl (fun x0 -> ASM.JB (baddr, x0))
| ASM.JNB (baddr, x) -> Types.Inl (fun x0 -> ASM.JNB (baddr, x0))
| ASM.JBC (baddr, x) -> Types.Inl (fun x0 -> ASM.JBC (baddr, x0))
| ASM.JZ x -> Types.Inl (fun x0 -> ASM.JZ x0)
| ASM.JNZ x -> Types.Inl (fun x0 -> ASM.JNZ x0)
| ASM.CJNE (addr, x) -> Types.Inl (fun x0 -> ASM.CJNE (addr, x0))
| ASM.DJNZ (addr, x) -> Types.Inl (fun x0 -> ASM.DJNZ (addr, x0))
| ASM.ANL arg -> Types.Inr (ASM.RealInstruction (ASM.ANL arg))
| ASM.ORL arg -> Types.Inr (ASM.RealInstruction (ASM.ORL arg))
| ASM.XRL arg -> Types.Inr (ASM.RealInstruction (ASM.XRL arg))
| ASM.CLR arg -> Types.Inr (ASM.RealInstruction (ASM.CLR arg))
| ASM.CPL arg -> Types.Inr (ASM.RealInstruction (ASM.CPL arg))
| ASM.RL arg -> Types.Inr (ASM.RealInstruction (ASM.RL arg))
| ASM.RLC arg -> Types.Inr (ASM.RealInstruction (ASM.RLC arg))
| ASM.RR arg -> Types.Inr (ASM.RealInstruction (ASM.RR arg))
| ASM.RRC arg -> Types.Inr (ASM.RealInstruction (ASM.RRC arg))
| ASM.SWAP arg -> Types.Inr (ASM.RealInstruction (ASM.SWAP arg))
| ASM.MOV arg -> Types.Inr (ASM.RealInstruction (ASM.MOV arg))
| ASM.MOVX arg -> Types.Inr (ASM.RealInstruction (ASM.MOVX arg))
| ASM.SETB arg -> Types.Inr (ASM.RealInstruction (ASM.SETB arg))
| ASM.PUSH arg -> Types.Inr (ASM.RealInstruction (ASM.PUSH arg))
| ASM.POP arg -> Types.Inr (ASM.RealInstruction (ASM.POP arg))
| ASM.XCH (arg1, arg2) ->
  Types.Inr (ASM.RealInstruction (ASM.XCH (arg1, arg2)))
| ASM.XCHD (arg1, arg2) ->
  Types.Inr (ASM.RealInstruction (ASM.XCHD (arg1, arg2)))
| ASM.RET -> Types.Inr (ASM.RealInstruction ASM.RET)
| ASM.RETI -> Types.Inr (ASM.RealInstruction ASM.RETI)
| ASM.NOP -> Types.Inr (ASM.RealInstruction ASM.NOP)
| ASM.JMP dst -> Types.Inr (ASM.RealInstruction (ASM.JMP dst))

(** val expand_relative_jump_unsafe :
    Assembly.jump_length -> ASM.identifier ASM.preinstruction ->
    ASM.instruction List.list **)
let expand_relative_jump_unsafe jmp_len i =
  match strip_target i with
  | Types.Inl jmp -> expand_relative_jump_internal_unsafe jmp_len jmp
  | Types.Inr instr -> List.Cons (instr, List.Nil)

(** val expand_pseudo_instruction_unsafe :
    Assembly.jump_length -> ASM.pseudo_instruction -> ASM.instruction
    List.list **)
let expand_pseudo_instruction_unsafe jmp_len = function
| ASM.Instruction instr -> expand_relative_jump_unsafe jmp_len instr
| ASM.Comment comment -> List.Nil
| ASM.Cost cost -> List.Cons ((ASM.RealInstruction ASM.NOP), List.Nil)
| ASM.Jmp jmp ->
  (match jmp_len with
   | Assembly.Short_jump ->
     List.Cons ((ASM.SJMP (ASM.RELATIVE
       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S Nat.O))))))))))), List.Nil)
   | Assembly.Absolute_jump ->
     List.Cons ((ASM.AJMP (ASM.ADDR11
       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))), List.Nil)
   | Assembly.Long_jump ->
     List.Cons ((ASM.LJMP (ASM.ADDR16
       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         Nat.O))))))))))))))))))), List.Nil))
| ASM.Jnz (acc, dst1, dst2) ->
  List.Cons ((ASM.RealInstruction (ASM.JNZ (ASM.RELATIVE
    (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S Nat.O))))))),
    (List.Cons ((ASM.LJMP (ASM.ADDR16
    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O))))))))))))))))))), (List.Cons ((ASM.LJMP (ASM.ADDR16
    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O))))))))))))))))))), List.Nil)))))
| ASM.Call call ->
  (match jmp_len with
   | Assembly.Short_jump -> List.Nil
   | Assembly.Absolute_jump ->
     List.Cons ((ASM.ACALL (ASM.ADDR11
       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))), List.Nil)
   | Assembly.Long_jump ->
     List.Cons ((ASM.LCALL (ASM.ADDR16
       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         Nat.O))))))))))))))))))), List.Nil))
| ASM.Mov (d, trgt, off) ->
  (match d with
   | Types.Inl x ->
     let address = ASM.DATA16
       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         Nat.O)))))))))))))))))
     in
     List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
     (Types.Inr { Types.fst = ASM.DPTR; Types.snd = address }))))), List.Nil)
   | Types.Inr pr ->
     let v = ASM.DATA
       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S Nat.O)))))))))
     in
     (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
              ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S
              Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr,
              Vector.VEmpty)))))) pr.Types.fst with
      | ASM.DIRECT b1 ->
        (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
          (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b1);
          Types.snd = v })))))), List.Nil))
      | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
      | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
      | ASM.REGISTER r ->
        (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
          (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst =
          (ASM.REGISTER r); Types.snd = v }))))))), List.Nil))
      | ASM.ACC_A ->
        (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
          (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst =
          ASM.ACC_A; Types.snd = v }))))))), List.Nil))
      | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
      | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
      | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
      | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
      | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
      | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
      | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
      | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
      | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
      | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
      | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
      | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
      | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
      | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)

(** val instruction_size_jmplen :
    Assembly.jump_length -> ASM.pseudo_instruction -> Nat.nat **)
let instruction_size_jmplen jmp_len i =
  let mapped =
    List.map Assembly.assembly1 (expand_pseudo_instruction_unsafe jmp_len i)
  in
  let flattened = List.flatten mapped in
  let pc_len = List.length flattened in pc_len

(** val max_length :
    Assembly.jump_length -> Assembly.jump_length -> Assembly.jump_length **)
let max_length j1 j2 =
  match j1 with
  | Assembly.Short_jump ->
    (match j2 with
     | Assembly.Short_jump -> Assembly.Short_jump
     | Assembly.Absolute_jump -> Assembly.Long_jump
     | Assembly.Long_jump -> Assembly.Long_jump)
  | Assembly.Absolute_jump ->
    (match j2 with
     | Assembly.Short_jump -> Assembly.Long_jump
     | Assembly.Absolute_jump -> Assembly.Absolute_jump
     | Assembly.Long_jump -> Assembly.Long_jump)
  | Assembly.Long_jump -> Assembly.Long_jump

(** val dec_jmple :
    Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum **)
let dec_jmple x y =
  match x with
  | Assembly.Short_jump ->
    (match y with
     | Assembly.Short_jump -> Types.Inr __
     | Assembly.Absolute_jump -> Types.Inl __
     | Assembly.Long_jump -> Types.Inl __)
  | Assembly.Absolute_jump ->
    (match y with
     | Assembly.Short_jump -> Types.Inr __
     | Assembly.Absolute_jump -> Types.Inr __
     | Assembly.Long_jump -> Types.Inl __)
  | Assembly.Long_jump ->
    (match y with
     | Assembly.Short_jump -> Types.Inr __
     | Assembly.Absolute_jump -> Types.Inr __
     | Assembly.Long_jump -> Types.Inr __)

(** val dec_eq_jump_length :
    Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum **)
let dec_eq_jump_length a b =
  match a with
  | Assembly.Short_jump ->
    (match b with
     | Assembly.Short_jump -> Types.Inl __
     | Assembly.Absolute_jump -> Types.Inr __
     | Assembly.Long_jump -> Types.Inr __)
  | Assembly.Absolute_jump ->
    (match b with
     | Assembly.Short_jump -> Types.Inr __
     | Assembly.Absolute_jump -> Types.Inl __
     | Assembly.Long_jump -> Types.Inr __)
  | Assembly.Long_jump ->
    (match b with
     | Assembly.Short_jump -> Types.Inr __
     | Assembly.Absolute_jump -> Types.Inr __
     | Assembly.Long_jump -> Types.Inl __)

(** val create_label_map :
    ASM.labelled_instruction List.list -> Fetch.label_map Types.sig0 **)
let create_label_map program =
  (Fetch.create_label_cost_map program).Types.fst

(** val select_reljump_length :
    Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
    -> Nat.nat -> Assembly.jump_length **)
let select_reljump_length labels old_sigma inc_sigma ppc lbl ins_len =
  let paddr = Identifiers.lookup_def PreIdentifiers.ASMTag labels lbl Nat.O
  in
  let { Types.fst = src; Types.snd = dest } =
    match Nat.leb paddr ppc with
    | Bool.True ->
      let pc = inc_sigma.Types.fst in
      let addr =
        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S Nat.O))))))))))))))))
          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) inc_sigma.Types.snd
          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
      in
      { Types.fst =
      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))))))))) (Nat.plus pc ins_len)); Types.snd =
      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))))))))) addr) }
    | Bool.False ->
      let pc =
        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S Nat.O))))))))))))))))
          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S Nat.O)))))))))))))))) ppc) old_sigma.Types.snd
          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
      in
      let addr =
        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S Nat.O))))))))))))))))
          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) old_sigma.Types.snd
          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
      in
      { Types.fst =
      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))))))))) (Nat.plus pc ins_len)); Types.snd =
      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))))))))) addr) }
  in
  let { Types.fst = sj_possible; Types.snd = disp } =
    Assembly.short_jump_cond src dest
  in
  (match sj_possible with
   | Bool.True -> Assembly.Short_jump
   | Bool.False -> Assembly.Long_jump)

(** val select_call_length :
    Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
    -> Assembly.jump_length **)
let select_call_length labels old_sigma inc_sigma ppc lbl =
  let paddr = Identifiers.lookup_def PreIdentifiers.ASMTag labels lbl Nat.O
  in
  let { Types.fst = src; Types.snd = dest } =
    match Nat.leb paddr ppc with
    | Bool.True ->
      let pc = inc_sigma.Types.fst in
      let addr =
        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S Nat.O))))))))))))))))
          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) inc_sigma.Types.snd
          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
      in
      { Types.fst =
      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))))))))) (Nat.plus pc (Nat.S (Nat.S Nat.O))));
      Types.snd =
      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))))))))) addr) }
    | Bool.False ->
      let pc =
        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S Nat.O))))))))))))))))
          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S Nat.O)))))))))))))))) ppc) old_sigma.Types.snd
          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
      in
      let addr =
        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S Nat.O))))))))))))))))
          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) old_sigma.Types.snd
          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
      in
      { Types.fst =
      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))))))))) (Nat.plus pc (Nat.S (Nat.S Nat.O))));
      Types.snd =
      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))))))))) addr) }
  in
  let { Types.fst = aj_possible; Types.snd = disp } =
    Assembly.absolute_jump_cond src dest
  in
  (match aj_possible with
   | Bool.True -> Assembly.Absolute_jump
   | Bool.False -> Assembly.Long_jump)

(** val select_jump_length :
    Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
    -> Assembly.jump_length **)
let select_jump_length labels old_sigma inc_sigma ppc lbl =
  let paddr = Identifiers.lookup_def PreIdentifiers.ASMTag labels lbl Nat.O
  in
  let { Types.fst = src; Types.snd = dest } =
    match Nat.leb paddr ppc with
    | Bool.True ->
      let pc = inc_sigma.Types.fst in
      let addr =
        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S Nat.O))))))))))))))))
          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) inc_sigma.Types.snd
          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
      in
      { Types.fst =
      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))))))))) (Nat.plus pc (Nat.S (Nat.S Nat.O))));
      Types.snd =
      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))))))))) addr) }
    | Bool.False ->
      let pc =
        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S Nat.O))))))))))))))))
          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S Nat.O)))))))))))))))) ppc) old_sigma.Types.snd
          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
      in
      let addr =
        (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S Nat.O))))))))))))))))
          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) old_sigma.Types.snd
          { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
      in
      { Types.fst =
      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))))))))) (Nat.plus pc (Nat.S (Nat.S Nat.O))));
      Types.snd =
      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))))))))))) addr) }
  in
  let { Types.fst = sj_possible; Types.snd = disp } =
    Assembly.short_jump_cond src dest
  in
  (match sj_possible with
   | Bool.True -> Assembly.Short_jump
   | Bool.False -> select_call_length labels old_sigma inc_sigma ppc lbl)

(** val destination_of :
    ASM.identifier ASM.preinstruction -> ASM.identifier Types.option **)
let destination_of = function
| ASM.ADD (x, x0) -> Types.None
| ASM.ADDC (x, x0) -> Types.None
| ASM.SUBB (x, x0) -> Types.None
| ASM.INC x -> Types.None
| ASM.DEC x -> Types.None
| ASM.MUL (x, x0) -> Types.None
| ASM.DIV (x, x0) -> Types.None
| ASM.DA x -> Types.None
| ASM.JC j -> Types.Some j
| ASM.JNC j -> Types.Some j
| ASM.JB (x, j) -> Types.Some j
| ASM.JNB (x, j) -> Types.Some j
| ASM.JBC (x, j) -> Types.Some j
| ASM.JZ j -> Types.Some j
| ASM.JNZ j -> Types.Some j
| ASM.CJNE (x, j) -> Types.Some j
| ASM.DJNZ (x, j) -> Types.Some j
| ASM.ANL x -> Types.None
| ASM.ORL x -> Types.None
| ASM.XRL x -> Types.None
| ASM.CLR x -> Types.None
| ASM.CPL x -> Types.None
| ASM.RL x -> Types.None
| ASM.RLC x -> Types.None
| ASM.RR x -> Types.None
| ASM.RRC x -> Types.None
| ASM.SWAP x -> Types.None
| ASM.MOV x -> Types.None
| ASM.MOVX x -> Types.None
| ASM.SETB x -> Types.None
| ASM.PUSH x -> Types.None
| ASM.POP x -> Types.None
| ASM.XCH (x, x0) -> Types.None
| ASM.XCHD (x, x0) -> Types.None
| ASM.RET -> Types.None
| ASM.RETI -> Types.None
| ASM.NOP -> Types.None
| ASM.JMP x -> Types.None

(** val length_of : ASM.identifier ASM.preinstruction -> Nat.nat **)
let length_of = function
| ASM.ADD (x, x0) -> Nat.O
| ASM.ADDC (x, x0) -> Nat.O
| ASM.SUBB (x, x0) -> Nat.O
| ASM.INC x -> Nat.O
| ASM.DEC x -> Nat.O
| ASM.MUL (x, x0) -> Nat.O
| ASM.DIV (x, x0) -> Nat.O
| ASM.DA x -> Nat.O
| ASM.JC j -> Nat.S (Nat.S Nat.O)
| ASM.JNC j -> Nat.S (Nat.S Nat.O)
| ASM.JB (x, j) -> Nat.S (Nat.S (Nat.S Nat.O))
| ASM.JNB (x, j) -> Nat.S (Nat.S (Nat.S Nat.O))
| ASM.JBC (x, j) -> Nat.S (Nat.S (Nat.S Nat.O))
| ASM.JZ j -> Nat.S (Nat.S Nat.O)
| ASM.JNZ j -> Nat.S (Nat.S Nat.O)
| ASM.CJNE (x, j) -> Nat.S (Nat.S (Nat.S Nat.O))
| ASM.DJNZ (x, j) ->
  (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
           ASM.Registr, (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)))) x with
   | ASM.DIRECT x0 -> Nat.S (Nat.S (Nat.S Nat.O))
   | ASM.INDIRECT x0 -> Nat.S (Nat.S (Nat.S Nat.O))
   | ASM.EXT_INDIRECT x0 -> Nat.S (Nat.S (Nat.S Nat.O))
   | ASM.REGISTER x0 -> Nat.S (Nat.S Nat.O)
   | ASM.ACC_A -> Nat.S (Nat.S (Nat.S Nat.O))
   | ASM.ACC_B -> Nat.S (Nat.S (Nat.S Nat.O))
   | ASM.DPTR -> Nat.S (Nat.S (Nat.S Nat.O))
   | ASM.DATA x0 -> Nat.S (Nat.S (Nat.S Nat.O))
   | ASM.DATA16 x0 -> Nat.S (Nat.S (Nat.S Nat.O))
   | ASM.ACC_DPTR -> Nat.S (Nat.S (Nat.S Nat.O))
   | ASM.ACC_PC -> Nat.S (Nat.S (Nat.S Nat.O))
   | ASM.EXT_INDIRECT_DPTR -> Nat.S (Nat.S (Nat.S Nat.O))
   | ASM.INDIRECT_DPTR -> Nat.S (Nat.S (Nat.S Nat.O))
   | ASM.CARRY -> Nat.S (Nat.S (Nat.S Nat.O))
   | ASM.BIT_ADDR x0 -> Nat.S (Nat.S (Nat.S Nat.O))
   | ASM.N_BIT_ADDR x0 -> Nat.S (Nat.S (Nat.S Nat.O))
   | ASM.RELATIVE x0 -> Nat.S (Nat.S (Nat.S Nat.O))
   | ASM.ADDR11 x0 -> Nat.S (Nat.S (Nat.S Nat.O))
   | ASM.ADDR16 x0 -> Nat.S (Nat.S (Nat.S Nat.O)))
| ASM.ANL x -> Nat.O
| ASM.ORL x -> Nat.O
| ASM.XRL x -> Nat.O
| ASM.CLR x -> Nat.O
| ASM.CPL x -> Nat.O
| ASM.RL x -> Nat.O
| ASM.RLC x -> Nat.O
| ASM.RR x -> Nat.O
| ASM.RRC x -> Nat.O
| ASM.SWAP x -> Nat.O
| ASM.MOV x -> Nat.O
| ASM.MOVX x -> Nat.O
| ASM.SETB x -> Nat.O
| ASM.PUSH x -> Nat.O
| ASM.POP x -> Nat.O
| ASM.XCH (x, x0) -> Nat.O
| ASM.XCHD (x, x0) -> Nat.O
| ASM.RET -> Nat.O
| ASM.RETI -> Nat.O
| ASM.NOP -> Nat.O
| ASM.JMP x -> Nat.O

(** 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 **)
let jump_expansion_step_instruction labels old_sigma inc_sigma ppc i =
  let ins_len = length_of i in
  (match destination_of i with
   | Types.None -> Types.None
   | Types.Some j ->
     Types.Some
       (select_reljump_length labels old_sigma inc_sigma ppc j ins_len))

(** val jump_expansion_start :
    ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map ->
    ppc_pc_map Types.option Types.sig0 **)
let jump_expansion_start program labels =
  (let { Types.fst = ignore; Types.snd = final_policy } =
     Types.pi1
       (FoldStuff.foldl_strong (Types.pi1 program)
         (fun prefix x tl _ acc_pol ->
         (let { Types.fst = acc; Types.snd = p } = Types.pi1 acc_pol in
         (fun _ ->
         let { Types.fst = pc; Types.snd = sigma } = p in
         let { Types.fst = label; Types.snd = instr } = x in
         let isize = instruction_size_jmplen Assembly.Short_jump instr in
         let sacc =
           Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
             (Nat.S Nat.O)))))))))))))))) acc
         in
         { Types.fst = sacc; Types.snd = { Types.fst = (Nat.plus pc isize);
         Types.snd =
         (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S Nat.O)))))))))))))))) sacc { Types.fst =
           (Nat.plus pc isize); Types.snd = Assembly.Short_jump } sigma) } }))
           __) { Types.fst =
         (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           Nat.O))))))))))))))))); Types.snd = { Types.fst = Nat.O;
         Types.snd =
         (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S Nat.O))))))))))))))))
           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
             (Nat.S (Nat.S Nat.O)))))))))))))))) Nat.O) { Types.fst = Nat.O;
           Types.snd = Assembly.Short_jump } (BitVectorTrie.Stub (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } })
   in
  (fun _ ->
  (match Util.gtb final_policy.Types.fst
           (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
             (Nat.S (Nat.S Nat.O))))))))))))))))) with
   | Bool.True -> (fun _ -> Types.None)
   | Bool.False -> (fun _ -> Types.Some final_policy)) __)) __