source: extracted/policy.ml @ 2746

Last change on this file since 2746 was 2746, checked in by sacerdot, 7 years ago
  1. debugging code in glue
  2. updated version
File size: 4.2 KB
Line 
1open Preamble
2
3open Assembly
4
5open Status
6
7open Fetch
8
9open String
10
11open LabelledObjects
12
13open BitVectorTrie
14
15open Exp
16
17open Arithmetic
18
19open Integers
20
21open AST
22
23open CostLabel
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Setoids
40
41open Monad
42
43open Option
44
45open Lists
46
47open Positive
48
49open Identifiers
50
51open Extranat
52
53open Vector
54
55open Div_and_mod
56
57open Jmeq
58
59open Russell
60
61open Types
62
63open List
64
65open Util
66
67open FoldStuff
68
69open Bool
70
71open Hints_declaration
72
73open Core_notation
74
75open Pts
76
77open Logic
78
79open Relations
80
81open Nat
82
83open BitVector
84
85open ASM
86
87open PolicyFront
88
89open 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 **)
94let rec jump_expansion_internal program0 n =
95  let labels = PolicyFront.create_label_map (Types.pi1 program0) in
96  (match n with
97   | Nat.O ->
98     (fun _ -> { Types.fst = Bool.False; Types.snd =
99       (Types.pi1
100         (PolicyFront.jump_expansion_start program0 (Types.pi1 labels))) })
101   | Nat.S m ->
102     (fun _ ->
103       let res1 = Types.pi1 (jump_expansion_internal program0 m) in
104       (let { Types.fst = no_ch; Types.snd = z } = res1 in
105       (fun _ ->
106       (match z with
107        | Types.None ->
108          (fun _ -> { Types.fst = Bool.False; Types.snd = Types.None })
109        | Types.Some op0 ->
110          (fun _ ->
111            match no_ch with
112            | Bool.True -> res1
113            | Bool.False ->
114              Types.pi1
115                (PolicyStep.jump_expansion_step program0 (Types.pi1 labels)
116                  op0))) __)) __)) __
117
118(** val measure_int :
119    ASM.labelled_instruction List.list -> PolicyFront.ppc_pc_map -> Nat.nat
120    -> Nat.nat **)
121let rec measure_int program0 policy acc =
122  match program0 with
123  | List.Nil -> acc
124  | List.Cons (h, t) ->
125    (match (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
126             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
127             (Nat.S Nat.O))))))))))))))))
128             (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
129               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
130               (Nat.S (Nat.S Nat.O)))))))))))))))) (List.length t))
131             policy.Types.snd { Types.fst = Nat.O; Types.snd =
132             Assembly.Short_jump }).Types.snd with
133     | Assembly.Short_jump -> measure_int t policy acc
134     | Assembly.Absolute_jump ->
135       measure_int t policy (Nat.plus acc (Nat.S Nat.O))
136     | Assembly.Long_jump ->
137       measure_int t policy (Nat.plus acc (Nat.S (Nat.S Nat.O))))
138
139(** val je_fixpoint :
140    ASM.labelled_instruction List.list Types.sig0 -> PolicyFront.ppc_pc_map
141    Types.option Types.sig0 **)
142let je_fixpoint program0 =
143  (Types.pi1
144    (jump_expansion_internal program0 (Nat.S
145      (Nat.times (Nat.S (Nat.S Nat.O)) (List.length (Types.pi1 program0)))))).Types.snd
146
147(** val jump_expansion' :
148    (ASM.preamble, ASM.labelled_instruction List.list Types.sig0) Types.prod
149    -> (BitVector.word -> BitVector.word, BitVector.word -> Bool.bool)
150    Types.prod Types.sig0 Types.option **)
151let jump_expansion' program0 =
152  let f = Types.pi1 (je_fixpoint program0.Types.snd) in
153  (match f with
154   | Types.None -> (fun _ -> Types.None)
155   | Types.Some x ->
156     (fun _ -> Types.Some { Types.fst = (fun ppc ->
157       let pc =
158         (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
159           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
160           (Nat.S Nat.O)))))))))))))))) ppc x.Types.snd { Types.fst = Nat.O;
161           Types.snd = Assembly.Short_jump }).Types.fst
162       in
163       Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
164         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
165         (Nat.S Nat.O)))))))))))))))) pc); Types.snd = (fun ppc ->
166       let jl =
167         (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
168           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
169           (Nat.S Nat.O)))))))))))))))) ppc x.Types.snd { Types.fst = Nat.O;
170           Types.snd = Assembly.Short_jump }).Types.snd
171       in
172       PolicyFront.jmpeqb jl Assembly.Long_jump) })) __
173
Note: See TracBrowser for help on using the repository browser.