extracted/policyFront.ml

   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 :
  92     Assembly.jump_length -> Assembly.jump_length -> Bool.bool **)
  93 let jmpeqb j1 j2 =
  94   match j1 with
  95   | Assembly.Short_jump ->
  96     (match j2 with
  97      | Assembly.Short_jump -> Bool.True
  98      | Assembly.Absolute_jump -> Bool.False
  99      | Assembly.Long_jump -> Bool.False)
 100   | Assembly.Absolute_jump ->
 101     (match j2 with
 102      | Assembly.Short_jump -> Bool.False
 103      | Assembly.Absolute_jump -> Bool.True
 104      | Assembly.Long_jump -> Bool.False)
 105   | Assembly.Long_jump ->
 106     (match j2 with
 107      | Assembly.Short_jump -> Bool.False
 108      | Assembly.Absolute_jump -> Bool.False
 109      | Assembly.Long_jump -> Bool.True)
 110
 111 (** val expand_relative_jump_internal_unsafe :
 112     Assembly.jump_length -> (ASM.subaddressing_mode -> ASM.subaddressing_mode
 113     ASM.preinstruction) -> ASM.instruction List.list **)
 114 let expand_relative_jump_internal_unsafe jmp_len i =
 115   match jmp_len with
 116   | Assembly.Short_jump ->
 117     List.Cons ((ASM.RealInstruction
 118       (i (ASM.RELATIVE
 119         (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 120           (Nat.S Nat.O)))))))))))), List.Nil)
 121   | Assembly.Absolute_jump -> List.Nil
 122   | Assembly.Long_jump ->
 123     List.Cons ((ASM.RealInstruction
 124       (i (ASM.RELATIVE
 125         (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 126           (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S Nat.O)))))),
 127       (List.Cons ((ASM.SJMP (ASM.RELATIVE
 128       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 129         (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S Nat.O)))))),
 130       (List.Cons ((ASM.LJMP (ASM.ADDR16
 131       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 132         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 133         Nat.O))))))))))))))))))), List.Nil)))))
 134
 135 (** val strip_target :
 136     ASM.identifier ASM.preinstruction -> (ASM.subaddressing_mode ->
 137     ASM.subaddressing_mode ASM.preinstruction, ASM.instruction) Types.sum **)
 138 let strip_target = function
 139 | ASM.ADD (arg1, arg2) ->
 140   Types.Inr (ASM.RealInstruction (ASM.ADD (arg1, arg2)))
 141 | ASM.ADDC (arg1, arg2) ->
 142   Types.Inr (ASM.RealInstruction (ASM.ADDC (arg1, arg2)))
 143 | ASM.SUBB (arg1, arg2) ->
 144   Types.Inr (ASM.RealInstruction (ASM.SUBB (arg1, arg2)))
 145 | ASM.INC arg -> Types.Inr (ASM.RealInstruction (ASM.INC arg))
 146 | ASM.DEC arg -> Types.Inr (ASM.RealInstruction (ASM.DEC arg))
 147 | ASM.MUL (arg1, arg2) ->
 148   Types.Inr (ASM.RealInstruction (ASM.MUL (arg1, arg2)))
 149 | ASM.DIV (arg1, arg2) ->
 150   Types.Inr (ASM.RealInstruction (ASM.DIV (arg1, arg2)))
 151 | ASM.DA arg -> Types.Inr (ASM.RealInstruction (ASM.DA arg))
 152 | ASM.JC x -> Types.Inl (fun x0 -> ASM.JC x0)
 153 | ASM.JNC x -> Types.Inl (fun x0 -> ASM.JNC x0)
 154 | ASM.JB (baddr, x) -> Types.Inl (fun x0 -> ASM.JB (baddr, x0))
 155 | ASM.JNB (baddr, x) -> Types.Inl (fun x0 -> ASM.JNB (baddr, x0))
 156 | ASM.JBC (baddr, x) -> Types.Inl (fun x0 -> ASM.JBC (baddr, x0))
 157 | ASM.JZ x -> Types.Inl (fun x0 -> ASM.JZ x0)
 158 | ASM.JNZ x -> Types.Inl (fun x0 -> ASM.JNZ x0)
 159 | ASM.CJNE (addr, x) -> Types.Inl (fun x0 -> ASM.CJNE (addr, x0))
 160 | ASM.DJNZ (addr, x) -> Types.Inl (fun x0 -> ASM.DJNZ (addr, x0))
 161 | ASM.ANL arg -> Types.Inr (ASM.RealInstruction (ASM.ANL arg))
 162 | ASM.ORL arg -> Types.Inr (ASM.RealInstruction (ASM.ORL arg))
 163 | ASM.XRL arg -> Types.Inr (ASM.RealInstruction (ASM.XRL arg))
 164 | ASM.CLR arg -> Types.Inr (ASM.RealInstruction (ASM.CLR arg))
 165 | ASM.CPL arg -> Types.Inr (ASM.RealInstruction (ASM.CPL arg))
 166 | ASM.RL arg -> Types.Inr (ASM.RealInstruction (ASM.RL arg))
 167 | ASM.RLC arg -> Types.Inr (ASM.RealInstruction (ASM.RLC arg))
 168 | ASM.RR arg -> Types.Inr (ASM.RealInstruction (ASM.RR arg))
 169 | ASM.RRC arg -> Types.Inr (ASM.RealInstruction (ASM.RRC arg))
 170 | ASM.SWAP arg -> Types.Inr (ASM.RealInstruction (ASM.SWAP arg))
 171 | ASM.MOV arg -> Types.Inr (ASM.RealInstruction (ASM.MOV arg))
 172 | ASM.MOVX arg -> Types.Inr (ASM.RealInstruction (ASM.MOVX arg))
 173 | ASM.SETB arg -> Types.Inr (ASM.RealInstruction (ASM.SETB arg))
 174 | ASM.PUSH arg -> Types.Inr (ASM.RealInstruction (ASM.PUSH arg))
 175 | ASM.POP arg -> Types.Inr (ASM.RealInstruction (ASM.POP arg))
 176 | ASM.XCH (arg1, arg2) ->
 177   Types.Inr (ASM.RealInstruction (ASM.XCH (arg1, arg2)))
 178 | ASM.XCHD (arg1, arg2) ->
 179   Types.Inr (ASM.RealInstruction (ASM.XCHD (arg1, arg2)))
 180 | ASM.RET -> Types.Inr (ASM.RealInstruction ASM.RET)
 181 | ASM.RETI -> Types.Inr (ASM.RealInstruction ASM.RETI)
 182 | ASM.NOP -> Types.Inr (ASM.RealInstruction ASM.NOP)
 183 | ASM.JMP dst -> Types.Inr (ASM.RealInstruction (ASM.JMP dst))
 184
 185 (** val expand_relative_jump_unsafe :
 186     Assembly.jump_length -> ASM.identifier ASM.preinstruction ->
 187     ASM.instruction List.list **)
 188 let expand_relative_jump_unsafe jmp_len i =
 189   match strip_target i with
 190   | Types.Inl jmp -> expand_relative_jump_internal_unsafe jmp_len jmp
 191   | Types.Inr instr -> List.Cons (instr, List.Nil)
 192
 193 (** val expand_pseudo_instruction_unsafe :
 194     Assembly.jump_length -> ASM.pseudo_instruction -> ASM.instruction
 195     List.list **)
 196 let expand_pseudo_instruction_unsafe jmp_len = function
 197 | ASM.Instruction instr -> expand_relative_jump_unsafe jmp_len instr
 198 | ASM.Comment comment -> List.Nil
 199 | ASM.Cost cost -> List.Cons ((ASM.RealInstruction ASM.NOP), List.Nil)
 200 | ASM.Jmp jmp ->
 201   (match jmp_len with
 202    | Assembly.Short_jump ->
 203      List.Cons ((ASM.SJMP (ASM.RELATIVE
 204        (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 205          (Nat.S Nat.O))))))))))), List.Nil)
 206    | Assembly.Absolute_jump ->
 207      List.Cons ((ASM.AJMP (ASM.ADDR11
 208        (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 209          (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))), List.Nil)
 210    | Assembly.Long_jump ->
 211      List.Cons ((ASM.LJMP (ASM.ADDR16
 212        (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 213          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 214          Nat.O))))))))))))))))))), List.Nil))
 215 | ASM.Jnz (acc, dst1, dst2) ->
 216   List.Cons ((ASM.RealInstruction (ASM.JNZ (ASM.RELATIVE
 217     (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 218       (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S Nat.O))))))),
 219     (List.Cons ((ASM.LJMP (ASM.ADDR16
 220     (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 221       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 222       Nat.O))))))))))))))))))), (List.Cons ((ASM.LJMP (ASM.ADDR16
 223     (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 224       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 225       Nat.O))))))))))))))))))), List.Nil)))))
 226 | ASM.Call call ->
 227   (match jmp_len with
 228    | Assembly.Short_jump -> List.Nil
 229    | Assembly.Absolute_jump ->
 230      List.Cons ((ASM.ACALL (ASM.ADDR11
 231        (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 232          (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))), List.Nil)
 233    | Assembly.Long_jump ->
 234      List.Cons ((ASM.LCALL (ASM.ADDR16
 235        (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 236          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 237          Nat.O))))))))))))))))))), List.Nil))
 238 | ASM.Mov (d, trgt, off) ->
 239   (match d with
 240    | Types.Inl x ->
 241      let address = ASM.DATA16
 242        (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 243          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 244          Nat.O)))))))))))))))))
 245      in
 246      List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
 247      (Types.Inr { Types.fst = ASM.DPTR; Types.snd = address }))))), List.Nil)
 248    | Types.Inr pr ->
 249      let v = ASM.DATA
 250        (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 251          (Nat.S Nat.O)))))))))
 252      in
 253      (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
 254               ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S
 255               Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr,
 256               Vector.VEmpty)))))) pr.Types.fst with
 257       | ASM.DIRECT b1 ->
 258         (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
 259           (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b1);
 260           Types.snd = v })))))), List.Nil))
 261       | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
 262       | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
 263       | ASM.REGISTER r ->
 264         (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
 265           (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst =
 266           (ASM.REGISTER r); Types.snd = v }))))))), List.Nil))
 267       | ASM.ACC_A ->
 268         (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
 269           (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst =
 270           ASM.ACC_A; Types.snd = v }))))))), List.Nil))
 271       | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 272       | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 273       | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
 274       | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
 275       | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 276       | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 277       | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 278       | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 279       | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 280       | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 281       | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 282       | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
 283       | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
 284       | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
 285
 286 (** val instruction_size_jmplen :
 287     Assembly.jump_length -> ASM.pseudo_instruction -> Nat.nat **)
 288 let instruction_size_jmplen jmp_len i =
 289   let mapped =
 290     List.map Assembly.assembly1 (expand_pseudo_instruction_unsafe jmp_len i)
 291   in
 292   let flattened = List.flatten mapped in
 293   let pc_len = List.length flattened in pc_len
 294
 295 (** val max_length :
 296     Assembly.jump_length -> Assembly.jump_length -> Assembly.jump_length **)
 297 let max_length j1 j2 =
 298   match j1 with
 299   | Assembly.Short_jump ->
 300     (match j2 with
 301      | Assembly.Short_jump -> Assembly.Short_jump
 302      | Assembly.Absolute_jump -> Assembly.Long_jump
 303      | Assembly.Long_jump -> Assembly.Long_jump)
 304   | Assembly.Absolute_jump ->
 305     (match j2 with
 306      | Assembly.Short_jump -> Assembly.Long_jump
 307      | Assembly.Absolute_jump -> Assembly.Absolute_jump
 308      | Assembly.Long_jump -> Assembly.Long_jump)
 309   | Assembly.Long_jump -> Assembly.Long_jump
 310
 311 (** val dec_jmple :
 312     Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum **)
 313 let dec_jmple x y =
 314   match x with
 315   | Assembly.Short_jump ->
 316     (match y with
 317      | Assembly.Short_jump -> Types.Inr __
 318      | Assembly.Absolute_jump -> Types.Inl __
 319      | Assembly.Long_jump -> Types.Inl __)
 320   | Assembly.Absolute_jump ->
 321     (match y with
 322      | Assembly.Short_jump -> Types.Inr __
 323      | Assembly.Absolute_jump -> Types.Inr __
 324      | Assembly.Long_jump -> Types.Inl __)
 325   | Assembly.Long_jump ->
 326     (match y with
 327      | Assembly.Short_jump -> Types.Inr __
 328      | Assembly.Absolute_jump -> Types.Inr __
 329      | Assembly.Long_jump -> Types.Inr __)
 330
 331 (** val dec_eq_jump_length :
 332     Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum **)
 333 let dec_eq_jump_length a b =
 334   match a with
 335   | Assembly.Short_jump ->
 336     (match b with
 337      | Assembly.Short_jump -> Types.Inl __
 338      | Assembly.Absolute_jump -> Types.Inr __
 339      | Assembly.Long_jump -> Types.Inr __)
 340   | Assembly.Absolute_jump ->
 341     (match b with
 342      | Assembly.Short_jump -> Types.Inr __
 343      | Assembly.Absolute_jump -> Types.Inl __
 344      | Assembly.Long_jump -> Types.Inr __)
 345   | Assembly.Long_jump ->
 346     (match b with
 347      | Assembly.Short_jump -> Types.Inr __
 348      | Assembly.Absolute_jump -> Types.Inr __
 349      | Assembly.Long_jump -> Types.Inl __)
 350
 351 (** val create_label_map :
 352     ASM.labelled_instruction List.list -> Fetch.label_map Types.sig0 **)
 353 let create_label_map program =
 354   (Fetch.create_label_cost_map program).Types.fst
 355
 356 (** val select_reljump_length :
 357     Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
 358     -> Nat.nat -> Assembly.jump_length **)
 359 let select_reljump_length labels old_sigma inc_sigma ppc lbl ins_len =
 360   let paddr = Identifiers.lookup_def PreIdentifiers.ASMTag labels lbl Nat.O
 361   in
 362   let { Types.fst = src; Types.snd = dest } =
 363     match Nat.leb paddr ppc with
 364     | Bool.True ->
 365       let pc = inc_sigma.Types.fst in
 366       let addr =
 367         (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 368           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 369           (Nat.S Nat.O))))))))))))))))
 370           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 371             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 372             (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) inc_sigma.Types.snd
 373           { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
 374       in
 375       { Types.fst =
 376       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 377         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 378         Nat.O)))))))))))))))) (Nat.plus pc ins_len)); Types.snd =
 379       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 380         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 381         Nat.O)))))))))))))))) addr) }
 382     | Bool.False ->
 383       let pc =
 384         (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 385           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 386           (Nat.S Nat.O))))))))))))))))
 387           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 388             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 389             (Nat.S (Nat.S Nat.O)))))))))))))))) ppc) old_sigma.Types.snd
 390           { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
 391       in
 392       let addr =
 393         (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 394           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 395           (Nat.S Nat.O))))))))))))))))
 396           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 397             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 398             (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) old_sigma.Types.snd
 399           { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
 400       in
 401       { Types.fst =
 402       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 403         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 404         Nat.O)))))))))))))))) (Nat.plus pc ins_len)); Types.snd =
 405       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 406         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 407         Nat.O)))))))))))))))) addr) }
 408   in
 409   let { Types.fst = sj_possible; Types.snd = disp } =
 410     Assembly.short_jump_cond src dest
 411   in
 412   (match sj_possible with
 413    | Bool.True -> Assembly.Short_jump
 414    | Bool.False -> Assembly.Long_jump)
 415
 416 (** val select_call_length :
 417     Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
 418     -> Assembly.jump_length **)
 419 let select_call_length labels old_sigma inc_sigma ppc lbl =
 420   let paddr = Identifiers.lookup_def PreIdentifiers.ASMTag labels lbl Nat.O
 421   in
 422   let { Types.fst = src; Types.snd = dest } =
 423     match Nat.leb paddr ppc with
 424     | Bool.True ->
 425       let pc = inc_sigma.Types.fst in
 426       let addr =
 427         (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 428           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 429           (Nat.S Nat.O))))))))))))))))
 430           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 431             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 432             (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) inc_sigma.Types.snd
 433           { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
 434       in
 435       { Types.fst =
 436       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 437         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 438         Nat.O)))))))))))))))) (Nat.plus pc (Nat.S (Nat.S Nat.O))));
 439       Types.snd =
 440       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 441         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 442         Nat.O)))))))))))))))) addr) }
 443     | Bool.False ->
 444       let pc =
 445         (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 446           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 447           (Nat.S Nat.O))))))))))))))))
 448           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 449             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 450             (Nat.S (Nat.S Nat.O)))))))))))))))) ppc) old_sigma.Types.snd
 451           { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
 452       in
 453       let addr =
 454         (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 455           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 456           (Nat.S Nat.O))))))))))))))))
 457           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 458             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 459             (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) old_sigma.Types.snd
 460           { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
 461       in
 462       { Types.fst =
 463       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 464         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 465         Nat.O)))))))))))))))) (Nat.plus pc (Nat.S (Nat.S Nat.O))));
 466       Types.snd =
 467       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 468         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 469         Nat.O)))))))))))))))) addr) }
 470   in
 471   let { Types.fst = aj_possible; Types.snd = disp } =
 472     Assembly.absolute_jump_cond src dest
 473   in
 474   (match aj_possible with
 475    | Bool.True -> Assembly.Absolute_jump
 476    | Bool.False -> Assembly.Long_jump)
 477
 478 (** val select_jump_length :
 479     Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
 480     -> Assembly.jump_length **)
 481 let select_jump_length labels old_sigma inc_sigma ppc lbl =
 482   let paddr = Identifiers.lookup_def PreIdentifiers.ASMTag labels lbl Nat.O
 483   in
 484   let { Types.fst = src; Types.snd = dest } =
 485     match Nat.leb paddr ppc with
 486     | Bool.True ->
 487       let pc = inc_sigma.Types.fst in
 488       let addr =
 489         (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 490           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 491           (Nat.S Nat.O))))))))))))))))
 492           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 493             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 494             (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) inc_sigma.Types.snd
 495           { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
 496       in
 497       { Types.fst =
 498       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 499         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 500         Nat.O)))))))))))))))) (Nat.plus pc (Nat.S (Nat.S Nat.O))));
 501       Types.snd =
 502       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 503         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 504         Nat.O)))))))))))))))) addr) }
 505     | Bool.False ->
 506       let pc =
 507         (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 508           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 509           (Nat.S Nat.O))))))))))))))))
 510           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 511             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 512             (Nat.S (Nat.S Nat.O)))))))))))))))) ppc) old_sigma.Types.snd
 513           { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
 514       in
 515       let addr =
 516         (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 517           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 518           (Nat.S Nat.O))))))))))))))))
 519           (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 520             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 521             (Nat.S (Nat.S Nat.O)))))))))))))))) paddr) old_sigma.Types.snd
 522           { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.fst
 523       in
 524       { Types.fst =
 525       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 526         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 527         Nat.O)))))))))))))))) (Nat.plus pc (Nat.S (Nat.S Nat.O))));
 528       Types.snd =
 529       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 530         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 531         Nat.O)))))))))))))))) addr) }
 532   in
 533   let { Types.fst = sj_possible; Types.snd = disp } =
 534     Assembly.short_jump_cond src dest
 535   in
 536   (match sj_possible with
 537    | Bool.True -> Assembly.Short_jump
 538    | Bool.False -> select_call_length labels old_sigma inc_sigma ppc lbl)
 539
 540 (** val destination_of :
 541     ASM.identifier ASM.preinstruction -> ASM.identifier Types.option **)
 542 let destination_of = function
 543 | ASM.ADD (x, x0) -> Types.None
 544 | ASM.ADDC (x, x0) -> Types.None
 545 | ASM.SUBB (x, x0) -> Types.None
 546 | ASM.INC x -> Types.None
 547 | ASM.DEC x -> Types.None
 548 | ASM.MUL (x, x0) -> Types.None
 549 | ASM.DIV (x, x0) -> Types.None
 550 | ASM.DA x -> Types.None
 551 | ASM.JC j -> Types.Some j
 552 | ASM.JNC j -> Types.Some j
 553 | ASM.JB (x, j) -> Types.Some j
 554 | ASM.JNB (x, j) -> Types.Some j
 555 | ASM.JBC (x, j) -> Types.Some j
 556 | ASM.JZ j -> Types.Some j
 557 | ASM.JNZ j -> Types.Some j
 558 | ASM.CJNE (x, j) -> Types.Some j
 559 | ASM.DJNZ (x, j) -> Types.Some j
 560 | ASM.ANL x -> Types.None
 561 | ASM.ORL x -> Types.None
 562 | ASM.XRL x -> Types.None
 563 | ASM.CLR x -> Types.None
 564 | ASM.CPL x -> Types.None
 565 | ASM.RL x -> Types.None
 566 | ASM.RLC x -> Types.None
 567 | ASM.RR x -> Types.None
 568 | ASM.RRC x -> Types.None
 569 | ASM.SWAP x -> Types.None
 570 | ASM.MOV x -> Types.None
 571 | ASM.MOVX x -> Types.None
 572 | ASM.SETB x -> Types.None
 573 | ASM.PUSH x -> Types.None
 574 | ASM.POP x -> Types.None
 575 | ASM.XCH (x, x0) -> Types.None
 576 | ASM.XCHD (x, x0) -> Types.None
 577 | ASM.RET -> Types.None
 578 | ASM.RETI -> Types.None
 579 | ASM.NOP -> Types.None
 580 | ASM.JMP x -> Types.None
 581
 582 (** val length_of : ASM.identifier ASM.preinstruction -> Nat.nat **)
 583 let length_of = function
 584 | ASM.ADD (x, x0) -> Nat.O
 585 | ASM.ADDC (x, x0) -> Nat.O
 586 | ASM.SUBB (x, x0) -> Nat.O
 587 | ASM.INC x -> Nat.O
 588 | ASM.DEC x -> Nat.O
 589 | ASM.MUL (x, x0) -> Nat.O
 590 | ASM.DIV (x, x0) -> Nat.O
 591 | ASM.DA x -> Nat.O
 592 | ASM.JC j -> Nat.S (Nat.S Nat.O)
 593 | ASM.JNC j -> Nat.S (Nat.S Nat.O)
 594 | ASM.JB (x, j) -> Nat.S (Nat.S (Nat.S Nat.O))
 595 | ASM.JNB (x, j) -> Nat.S (Nat.S (Nat.S Nat.O))
 596 | ASM.JBC (x, j) -> Nat.S (Nat.S (Nat.S Nat.O))
 597 | ASM.JZ j -> Nat.S (Nat.S Nat.O)
 598 | ASM.JNZ j -> Nat.S (Nat.S Nat.O)
 599 | ASM.CJNE (x, j) -> Nat.S (Nat.S (Nat.S Nat.O))
 600 | ASM.DJNZ (x, j) ->
 601   (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
 602            ASM.Registr, (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)))) x with
 603    | ASM.DIRECT x0 -> Nat.S (Nat.S (Nat.S Nat.O))
 604    | ASM.INDIRECT x0 -> Nat.S (Nat.S (Nat.S Nat.O))
 605    | ASM.EXT_INDIRECT x0 -> Nat.S (Nat.S (Nat.S Nat.O))
 606    | ASM.REGISTER x0 -> Nat.S (Nat.S Nat.O)
 607    | ASM.ACC_A -> Nat.S (Nat.S (Nat.S Nat.O))
 608    | ASM.ACC_B -> Nat.S (Nat.S (Nat.S Nat.O))
 609    | ASM.DPTR -> Nat.S (Nat.S (Nat.S Nat.O))
 610    | ASM.DATA x0 -> Nat.S (Nat.S (Nat.S Nat.O))
 611    | ASM.DATA16 x0 -> Nat.S (Nat.S (Nat.S Nat.O))
 612    | ASM.ACC_DPTR -> Nat.S (Nat.S (Nat.S Nat.O))
 613    | ASM.ACC_PC -> Nat.S (Nat.S (Nat.S Nat.O))
 614    | ASM.EXT_INDIRECT_DPTR -> Nat.S (Nat.S (Nat.S Nat.O))
 615    | ASM.INDIRECT_DPTR -> Nat.S (Nat.S (Nat.S Nat.O))
 616    | ASM.CARRY -> Nat.S (Nat.S (Nat.S Nat.O))
 617    | ASM.BIT_ADDR x0 -> Nat.S (Nat.S (Nat.S Nat.O))
 618    | ASM.N_BIT_ADDR x0 -> Nat.S (Nat.S (Nat.S Nat.O))
 619    | ASM.RELATIVE x0 -> Nat.S (Nat.S (Nat.S Nat.O))
 620    | ASM.ADDR11 x0 -> Nat.S (Nat.S (Nat.S Nat.O))
 621    | ASM.ADDR16 x0 -> Nat.S (Nat.S (Nat.S Nat.O)))
 622 | ASM.ANL x -> Nat.O
 623 | ASM.ORL x -> Nat.O
 624 | ASM.XRL x -> Nat.O
 625 | ASM.CLR x -> Nat.O
 626 | ASM.CPL x -> Nat.O
 627 | ASM.RL x -> Nat.O
 628 | ASM.RLC x -> Nat.O
 629 | ASM.RR x -> Nat.O
 630 | ASM.RRC x -> Nat.O
 631 | ASM.SWAP x -> Nat.O
 632 | ASM.MOV x -> Nat.O
 633 | ASM.MOVX x -> Nat.O
 634 | ASM.SETB x -> Nat.O
 635 | ASM.PUSH x -> Nat.O
 636 | ASM.POP x -> Nat.O
 637 | ASM.XCH (x, x0) -> Nat.O
 638 | ASM.XCHD (x, x0) -> Nat.O
 639 | ASM.RET -> Nat.O
 640 | ASM.RETI -> Nat.O
 641 | ASM.NOP -> Nat.O
 642 | ASM.JMP x -> Nat.O
 643
 644 (** val jump_expansion_step_instruction :
 645     Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
 646     ASM.preinstruction -> Assembly.jump_length Types.option **)
 647 let jump_expansion_step_instruction labels old_sigma inc_sigma ppc i =
 648   let ins_len = length_of i in
 649   (match destination_of i with
 650    | Types.None -> Types.None
 651    | Types.Some j ->
 652      Types.Some
 653        (select_reljump_length labels old_sigma inc_sigma ppc j ins_len))
 654
 655 (** val jump_expansion_start :
 656     ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map ->
 657     ppc_pc_map Types.option Types.sig0 **)
 658 let jump_expansion_start program labels =
 659   let final_policy =
 660     FoldStuff.foldl_strong (Types.pi1 program) (fun prefix x tl _ p ->
 661       let { Types.fst = pc; Types.snd = sigma } = Types.pi1 p in
 662       let { Types.fst = label; Types.snd = instr } = x in
 663       let isize = instruction_size_jmplen Assembly.Short_jump instr in
 664       { Types.fst = (Nat.plus pc isize); Types.snd =
 665       (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 666         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 667         Nat.O))))))))))))))))
 668         (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 669           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 670           (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S (List.length prefix)))
 671         { Types.fst = (Nat.plus pc isize); Types.snd = Assembly.Short_jump }
 672         sigma) }) { Types.fst = Nat.O; Types.snd =
 673       (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 674         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 675         Nat.O))))))))))))))))
 676         (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 677           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 678           (Nat.S (Nat.S Nat.O)))))))))))))))) Nat.O) { Types.fst = Nat.O;
 679         Types.snd = Assembly.Short_jump } (BitVectorTrie.Stub (Nat.S (Nat.S
 680         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 681         (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) }
 682   in
 683   (match Util.gtb (Types.pi1 final_policy).Types.fst
 684            (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 685              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 686              (Nat.S (Nat.S Nat.O))))))))))))))))) with
 687    | Bool.True -> (fun _ -> Types.None)
 688    | Bool.False -> (fun _ -> Types.Some (Types.pi1 final_policy))) __
 689