source: extracted/policy.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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 { Types.fst = no_ch; Types.snd = z } =
104          Types.pi1 (jump_expansion_internal program0 m)
105        in
106       (fun _ ->
107       (match z with
108        | Types.None ->
109          (fun _ -> { Types.fst = Bool.False; Types.snd = Types.None })
110        | Types.Some op0 ->
111          (fun _ ->
112            match no_ch with
113            | Bool.True -> Types.pi1 (jump_expansion_internal program0 m)
114            | Bool.False ->
115              Types.pi1
116                (PolicyStep.jump_expansion_step program0 (Types.pi1 labels)
117                  op0))) __)) __)) __
118
119(** val measure_int :
120    ASM.labelled_instruction List.list -> PolicyFront.ppc_pc_map -> Nat.nat
121    -> Nat.nat **)
122let rec measure_int program0 policy acc =
123  match program0 with
124  | List.Nil -> acc
125  | List.Cons (h, t) ->
126    (match (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
127             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
128             (Nat.S Nat.O))))))))))))))))
129             (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
130               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
131               (Nat.S (Nat.S Nat.O)))))))))))))))) (List.length t))
132             policy.Types.snd { Types.fst = Nat.O; Types.snd =
133             Assembly.Short_jump }).Types.snd with
134     | Assembly.Short_jump -> measure_int t policy acc
135     | Assembly.Absolute_jump ->
136       measure_int t policy (Nat.plus acc (Nat.S Nat.O))
137     | Assembly.Long_jump ->
138       measure_int t policy (Nat.plus acc (Nat.S (Nat.S Nat.O))))
139
140(** val je_fixpoint :
141    ASM.labelled_instruction List.list Types.sig0 -> PolicyFront.ppc_pc_map
142    Types.option Types.sig0 **)
143let je_fixpoint program0 =
144  (Types.pi1
145    (jump_expansion_internal program0 (Nat.S
146      (Nat.times (Nat.S (Nat.S Nat.O)) (List.length (Types.pi1 program0)))))).Types.snd
147
148(** val jump_expansion' :
149    (ASM.preamble, ASM.labelled_instruction List.list Types.sig0) Types.prod
150    -> (BitVector.word -> BitVector.word, BitVector.word -> Bool.bool)
151    Types.prod Types.sig0 Types.option **)
152let jump_expansion' program0 =
153  let f = Types.pi1 (je_fixpoint program0.Types.snd) in
154  (match f with
155   | Types.None -> (fun _ -> Types.None)
156   | Types.Some x ->
157     (fun _ -> Types.Some { Types.fst = (fun ppc ->
158       let pc =
159         (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
160           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
161           (Nat.S Nat.O)))))))))))))))) ppc x.Types.snd { Types.fst = Nat.O;
162           Types.snd = Assembly.Short_jump }).Types.fst
163       in
164       Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
165         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
166         (Nat.S Nat.O)))))))))))))))) pc); Types.snd = (fun ppc ->
167       let jl =
168         (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
169           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
170           (Nat.S Nat.O)))))))))))))))) ppc x.Types.snd { Types.fst = Nat.O;
171           Types.snd = Assembly.Short_jump }).Types.snd
172       in
173       PolicyFront.jmpeqb jl Assembly.Long_jump) })) __
174
Note: See TracBrowser for help on using the repository browser.