source: driver/extracted/policy.ml @ 3106

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

Pretty printing changed.
There is still an inefficiency left: activate the commented out prerr_endline
to understand it.

File size: 4.8 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";
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
111prerr_endline "JES";
112let 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 **)
142let 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 **)
163let 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 **)
171let 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
Note: See TracBrowser for help on using the repository browser.