extracted/policyStep.ml

   1 open Preamble
   2
   3 open Assembly
   4
   5 open Status
   6
   7 open Fetch
   8
   9 open BitVectorTrie
  10
  11 open String
  12
  13 open Exp
  14
  15 open Arithmetic
  16
  17 open Vector
  18
  19 open FoldStuff
  20
  21 open BitVector
  22
  23 open Extranat
  24
  25 open Integers
  26
  27 open AST
  28
  29 open LabelledObjects
  30
  31 open Proper
  32
  33 open PositiveMap
  34
  35 open Deqsets
  36
  37 open ErrorMessages
  38
  39 open PreIdentifiers
  40
  41 open Errors
  42
  43 open Extralib
  44
  45 open Setoids
  46
  47 open Monad
  48
  49 open Option
  50
  51 open Div_and_mod
  52
  53 open Jmeq
  54
  55 open Russell
  56
  57 open Util
  58
  59 open List
  60
  61 open Lists
  62
  63 open Bool
  64
  65 open Relations
  66
  67 open Nat
  68
  69 open Positive
  70
  71 open Hints_declaration
  72
  73 open Core_notation
  74
  75 open Pts
  76
  77 open Logic
  78
  79 open Types
  80
  81 open Identifiers
  82
  83 open CostLabel
  84
  85 open ASM
  86
  87 open PolicyFront
  88
  89 (** val jump_expansion_step :
  90     ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map
  91     Types.sig0 -> PolicyFront.ppc_pc_map Types.sig0 -> (Bool.bool,
  92     PolicyFront.ppc_pc_map Types.option) Types.prod Types.sig0 **)
  93 let jump_expansion_step program labels old_sigma =
  94   (let { Types.fst = final_added; Types.snd = final_policy } =
  95      Types.pi1
  96        (FoldStuff.foldl_strong (Types.pi1 program) (fun prefix x tl _ acc ->
  97          (let { Types.fst = inc_added; Types.snd = inc_pc_sigma } =
  98             Types.pi1 acc
  99           in
 100          (fun _ ->
 101          (let { Types.fst = label; Types.snd = instr } = x in
 102          (fun _ ->
 103          let add_instr =
 104            match instr with
 105            | ASM.Instruction i ->
 106              PolicyFront.jump_expansion_step_instruction (Types.pi1 labels)
 107                (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) i
 108            | ASM.Comment x0 -> Types.None
 109            | ASM.Cost x0 -> Types.None
 110            | ASM.Jmp j ->
 111              Types.Some
 112                (PolicyFront.select_jump_length (Types.pi1 labels)
 113                  (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) j)
 114            | ASM.Jnz (x0, x1, x2) -> Types.None
 115            | ASM.Call c ->
 116              Types.Some
 117                (PolicyFront.select_call_length (Types.pi1 labels)
 118                  (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) c)
 119            | ASM.Mov (x0, x1, x2) -> Types.None
 120          in
 121          let { Types.fst = inc_pc; Types.snd = inc_sigma } = inc_pc_sigma in
 122          let old_length =
 123            (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 124              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 125              (Nat.S Nat.O))))))))))))))))
 126              (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 127                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 128                (Nat.S (Nat.S Nat.O)))))))))))))))) (List.length prefix))
 129              (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
 130              Assembly.Short_jump }).Types.snd
 131          in
 132          let old_size = PolicyFront.instruction_size_jmplen old_length instr
 133          in
 134          let { Types.fst = new_length; Types.snd = isize } =
 135            match add_instr with
 136            | Types.None ->
 137              { Types.fst = Assembly.Short_jump; Types.snd =
 138                (PolicyFront.instruction_size_jmplen Assembly.Short_jump
 139                  instr) }
 140            | Types.Some pl ->
 141              { Types.fst = (PolicyFront.max_length old_length pl);
 142                Types.snd =
 143                (PolicyFront.instruction_size_jmplen
 144                  (PolicyFront.max_length old_length pl) instr) }
 145          in
 146          let new_added =
 147            match add_instr with
 148            | Types.None -> inc_added
 149            | Types.Some x0 -> Nat.plus inc_added (Nat.minus isize old_size)
 150          in
 151          let old_Slength =
 152            (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 153              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 154              (Nat.S Nat.O))))))))))))))))
 155              (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 156                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 157                (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S
 158                (List.length prefix))) (Types.pi1 old_sigma).Types.snd
 159              { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.snd
 160          in
 161          let updated_sigma =
 162            BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 163              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 164              (Nat.S Nat.O))))))))))))))))
 165              (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 166                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 167                (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S
 168                (List.length prefix))) { Types.fst = (Nat.plus inc_pc isize);
 169              Types.snd = old_Slength }
 170              (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 171                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 172                (Nat.S Nat.O))))))))))))))))
 173                (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
 174                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 175                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
 176                  (List.length prefix)) { Types.fst = inc_pc; Types.snd =
 177                new_length } inc_sigma)
 178          in
 179          { Types.fst = new_added; Types.snd = { Types.fst =
 180          (Nat.plus inc_pc isize); Types.snd = updated_sigma } })) __)) __)
 181          { Types.fst = Nat.O; Types.snd = { Types.fst = Nat.O; Types.snd =
 182          (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 183            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 184            (Nat.S Nat.O))))))))))))))))
 185            (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 186              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 187              (Nat.S (Nat.S Nat.O)))))))))))))))) Nat.O) { Types.fst = Nat.O;
 188            Types.snd =
 189            (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 190              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 191              (Nat.S Nat.O))))))))))))))))
 192              (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 193                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 194                (Nat.S (Nat.S Nat.O)))))))))))))))) Nat.O)
 195              (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
 196              Assembly.Short_jump }).Types.snd } (BitVectorTrie.Stub (Nat.S
 197            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 198            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } })
 199    in
 200   (fun _ ->
 201   (match Util.gtb final_policy.Types.fst
 202            (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 203              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 204              (Nat.S (Nat.S Nat.O))))))))))))))))) with
 205    | Bool.True ->
 206      (fun _ -> { Types.fst = (Nat.eqb final_added Nat.O); Types.snd =
 207        Types.None })
 208    | Bool.False ->
 209      (fun _ -> { Types.fst = (Nat.eqb final_added Nat.O); Types.snd =
 210        (Types.Some final_policy) })) __)) __
 211