source: extracted/policy.ml @ 3001

Last change on this file since 3001 was 3001, checked in by sacerdot, 7 years ago

New extraction.

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