source: extracted/policy.ml @ 3069

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

New extraction.

File size: 4.7 KB
RevLine 
[2717]1open Preamble
2
3open Assembly
4
5open Status
6
7open Fetch
8
[2773]9open BitVectorTrie
10
[2717]11open String
12
13open Exp
14
15open Arithmetic
16
[2773]17open Vector
18
19open FoldStuff
20
21open BitVector
22
23open Extranat
24
[2717]25open Integers
26
27open AST
28
[2773]29open LabelledObjects
[2717]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
[2773]57open Util
[2717]58
59open List
60
[2773]61open Lists
[2717]62
63open Bool
64
[2773]65open Relations
66
67open Nat
68
69open Positive
70
[2717]71open Hints_declaration
72
73open Core_notation
74
75open Pts
76
77open Logic
78
[2773]79open Types
[2717]80
[2773]81open Identifiers
[2717]82
[2773]83open CostLabel
[2717]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 **)
[2773]94let rec jump_expansion_internal program n =
95  let labels = PolicyFront.create_label_map (Types.pi1 program) in
[3001]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(*
[2717]116  (match n with
117   | Nat.O ->
118     (fun _ -> { Types.fst = Bool.False; Types.snd =
119       (Types.pi1
[2773]120         (PolicyFront.jump_expansion_start program (Types.pi1 labels))) })
[2717]121   | Nat.S m ->
122     (fun _ ->
[2773]123       let res = Types.pi1 (jump_expansion_internal program m) in
124       (let { Types.fst = no_ch; Types.snd = z } = res in
[2717]125       (fun _ ->
126       (match z with
127        | Types.None ->
128          (fun _ -> { Types.fst = Bool.False; Types.snd = Types.None })
[2773]129        | Types.Some op ->
[2717]130          (fun _ ->
131            match no_ch with
[2773]132            | Bool.True -> res
[2717]133            | Bool.False ->
134              Types.pi1
[2773]135                (PolicyStep.jump_expansion_step program (Types.pi1 labels)
[3001]136                  op))) __)) __)) __*)
[2717]137
138(** val measure_int :
139    ASM.labelled_instruction List.list -> PolicyFront.ppc_pc_map -> Nat.nat
140    -> Nat.nat **)
[2773]141let rec measure_int program policy acc =
142  match program with
[2717]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 **)
[2773]162let je_fixpoint program =
[2717]163  (Types.pi1
[2773]164    (jump_expansion_internal program (Nat.S
165      (Nat.times (Nat.S (Nat.S Nat.O)) (List.length (Types.pi1 program)))))).Types.snd
[2717]166
167(** val jump_expansion' :
[2773]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
[2717]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.