extracted/policy.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 open PolicyStep
  90
  91 (** val jump_expansion_internal :
  92     ASM.labelled_instruction List.list Types.sig0 -> Nat.nat -> (Bool.bool,
  93     PolicyFront.ppc_pc_map Types.option) Types.prod Types.sig0 **)
  94 let rec jump_expansion_internal program n =
  95   let labels = PolicyFront.create_label_map (Types.pi1 program) in
  96   let rec aux res =
  97 prerr_endline "JEI";
  98    let { Types.fst = no_ch; Types.snd = z } = res in
  99     match z with
 100      | Types.None ->
 101        { Types.fst = Bool.False; Types.snd = Types.None }
 102      | Types.Some op ->
 103          match no_ch with
 104          | Bool.True -> res
 105          | Bool.False ->
 106            aux
 107             (Types.pi1
 108              (PolicyStep.jump_expansion_step program (Types.pi1 labels)
 109                op))
 110   in
 111 prerr_endline "JES";
 112 let init =(PolicyFront.jump_expansion_start program (Types.pi1 labels)) in
 113    aux
 114     { Types.fst = Bool.False; Types.snd =
 115        (Types.pi1 init) }
 116 (*
 117   (match n with
 118    | Nat.O ->
 119      (fun _ -> { Types.fst = Bool.False; Types.snd =
 120        (Types.pi1
 121          (PolicyFront.jump_expansion_start program (Types.pi1 labels))) })
 122    | Nat.S m ->
 123      (fun _ ->
 124        let res = Types.pi1 (jump_expansion_internal program m) in
 125        (let { Types.fst = no_ch; Types.snd = z } = res in
 126        (fun _ ->
 127        (match z with
 128         | Types.None ->
 129           (fun _ -> { Types.fst = Bool.False; Types.snd = Types.None })
 130         | Types.Some op ->
 131           (fun _ ->
 132             match no_ch with
 133             | Bool.True -> res
 134             | Bool.False ->
 135               Types.pi1
 136                 (PolicyStep.jump_expansion_step program (Types.pi1 labels)
 137                   op))) __)) __)) __*)
 138
 139 (** val measure_int :
 140     ASM.labelled_instruction List.list -> PolicyFront.ppc_pc_map -> Nat.nat
 141     -> Nat.nat **)
 142 let rec measure_int program policy acc =
 143   match program with
 144   | List.Nil -> acc
 145   | List.Cons (h, t) ->
 146     (match (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 147              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 148              (Nat.S Nat.O))))))))))))))))
 149              (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 150                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 151                (Nat.S (Nat.S Nat.O)))))))))))))))) (List.length t))
 152              policy.Types.snd { Types.fst = Nat.O; Types.snd =
 153              Assembly.Short_jump }).Types.snd with
 154      | Assembly.Short_jump -> measure_int t policy acc
 155      | Assembly.Absolute_jump ->
 156        measure_int t policy (Nat.plus acc (Nat.S Nat.O))
 157      | Assembly.Long_jump ->
 158        measure_int t policy (Nat.plus acc (Nat.S (Nat.S Nat.O))))
 159
 160 (** val je_fixpoint :
 161     ASM.labelled_instruction List.list Types.sig0 -> PolicyFront.ppc_pc_map
 162     Types.option Types.sig0 **)
 163 let je_fixpoint program =
 164   (Types.pi1
 165     (jump_expansion_internal program (Nat.S
 166       (Nat.times (Nat.S (Nat.S Nat.O)) (List.length (Types.pi1 program)))))).Types.snd
 167
 168 (** val jump_expansion' :
 169     ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word,
 170     BitVector.word -> Bool.bool) Types.prod Types.sig0 Types.option **)
 171 let jump_expansion' program =
 172   let program' = program.ASM.code in
 173   let f = Types.pi1 (je_fixpoint program') in
 174   (match f with
 175    | Types.None -> (fun _ -> Types.None)
 176    | Types.Some x ->
 177      (fun _ -> Types.Some { Types.fst = (fun ppc ->
 178        let pc =
 179          (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 180            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 181            (Nat.S Nat.O)))))))))))))))) ppc x.Types.snd { Types.fst = Nat.O;
 182            Types.snd = Assembly.Short_jump }).Types.fst
 183        in
 184 (*prerr_endline "Z3";*)
 185        Arithmetic.bitvector_of_nat (Nat.S (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.O)))))))))))))))) pc); Types.snd = (fun ppc ->
 188        let jl =
 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)))))))))))))))) ppc x.Types.snd { Types.fst = Nat.O;
 192            Types.snd = Assembly.Short_jump }).Types.snd
 193        in
 194        PolicyFront.jmpeqb jl Assembly.Long_jump) })) __
 195