source: driver/extracted/linearise.ml @ 3106

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 10.9 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open GenMem
12
13open FrontEndMem
14
15open Globalenvs
16
17open String
18
19open Sets
20
21open Listb
22
23open LabelledObjects
24
25open BitVectorTrie
26
27open Graphs
28
29open I8051
30
31open Order
32
33open Registers
34
35open CostLabel
36
37open Hide
38
39open Proper
40
41open PositiveMap
42
43open Deqsets
44
45open ErrorMessages
46
47open PreIdentifiers
48
49open Errors
50
51open Extralib
52
53open Lists
54
55open Identifiers
56
57open Integers
58
59open AST
60
61open Division
62
63open Exp
64
65open Arithmetic
66
67open Setoids
68
69open Monad
70
71open Option
72
73open Extranat
74
75open Vector
76
77open Div_and_mod
78
79open Jmeq
80
81open Russell
82
83open List
84
85open Util
86
87open FoldStuff
88
89open BitVector
90
91open Types
92
93open Bool
94
95open Relations
96
97open Nat
98
99open Hints_declaration
100
101open Core_notation
102
103open Pts
104
105open Logic
106
107open Positive
108
109open Z
110
111open BitVectorZ
112
113open Pointers
114
115open ByteValues
116
117open BackEndOps
118
119open Joint
120
121(** val graph_to_lin_statement :
122    Joint.uns_params -> AST.ident List.list -> 'a1 Identifiers.identifier_map
123    -> Joint.joint_statement -> Joint.joint_statement **)
124let graph_to_lin_statement p globals visited = function
125| Joint.Sequential (c, nxt) ->
126  (match c with
127   | Joint.COST_LABEL x -> Joint.Sequential (c, (Obj.magic Types.It))
128   | Joint.CALL (x, x0, x1) -> Joint.Sequential (c, (Obj.magic Types.It))
129   | Joint.COND (a, ltrue) ->
130     (match Identifiers.member PreIdentifiers.LabelTag visited
131              (Obj.magic nxt) with
132      | Bool.True -> Joint.FCOND (a, ltrue, (Obj.magic nxt))
133      | Bool.False -> Joint.Sequential (c, (Obj.magic Types.It)))
134   | Joint.Step_seq x -> Joint.Sequential (c, (Obj.magic Types.It)))
135| Joint.Final c -> Joint.Final c
136| Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
137
138(** val chop :
139    ('a1 -> Bool.bool) -> 'a1 List.list -> ('a1, 'a1 List.list) Types.prod
140    Types.option **)
141let rec chop test = function
142| List.Nil -> Types.None
143| List.Cons (x, l') ->
144  (match test x with
145   | Bool.True -> chop test l'
146   | Bool.False ->
147     Obj.magic
148       (Monad.m_return0 (Monad.max_def Option.option) { Types.fst = x;
149         Types.snd = l' }))
150
151type graph_visit_ret_type =
152  ((Nat.nat Identifiers.identifier_map, Identifiers.identifier_set)
153  Types.prod, __) Types.prod Types.sig0
154
155(** val graph_visit :
156    Joint.uns_params -> AST.ident List.list -> __ ->
157    Identifiers.identifier_set -> Nat.nat Identifiers.identifier_map -> __ ->
158    Graphs.label List.list -> Nat.nat -> Nat.nat -> Graphs.label ->
159    graph_visit_ret_type **)
160let rec graph_visit p globals g required visited generated visiting gen_length n entry =
161  (match chop (fun x -> Identifiers.member PreIdentifiers.LabelTag visited x)
162           visiting with
163   | Types.None ->
164     (fun _ -> { Types.fst = { Types.fst = visited; Types.snd = required };
165       Types.snd = generated })
166   | Types.Some pr ->
167     (fun _ ->
168       let vis_hd = pr.Types.fst in
169       let vis_tl = pr.Types.snd in
170       (match n with
171        | Nat.O -> (fun _ -> assert false (* absurd case *))
172        | Nat.S n' ->
173          (fun _ ->
174            let visited' =
175              Identifiers.add PreIdentifiers.LabelTag visited vis_hd
176                gen_length
177            in
178            let statement =
179              Identifiers.lookup_safe PreIdentifiers.LabelTag (Obj.magic g)
180                vis_hd
181            in
182            let translated_statement =
183              graph_to_lin_statement p globals visited' statement
184            in
185            let generated' = List.Cons ({ Types.fst = (Types.Some vis_hd);
186              Types.snd = translated_statement }, (Obj.magic generated))
187            in
188            let required' =
189              Identifiers.union_set PreIdentifiers.LabelTag
190                (Identifiers.set_from_list PreIdentifiers.LabelTag
191                  (Joint.stmt_explicit_labels (Joint.lp_to_p__o__stmt_pars p)
192                    globals translated_statement)) required
193            in
194            let visiting' =
195              List.append
196                (Joint.stmt_labels { Joint.uns_pars = (Joint.g_u_pars p);
197                  Joint.succ_label = (Obj.magic (fun x -> Types.Some x));
198                  Joint.has_fcond = Bool.False } globals statement) vis_tl
199            in
200            let add_req_gen =
201              match statement with
202              | Joint.Sequential (s, nxt) ->
203                (match s with
204                 | Joint.COST_LABEL x ->
205                   (match Identifiers.member PreIdentifiers.LabelTag visited'
206                            (Obj.magic nxt) with
207                    | Bool.True ->
208                      { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
209                        (Identifiers.add_set PreIdentifiers.LabelTag
210                          (Identifiers.empty_set PreIdentifiers.LabelTag)
211                          (Obj.magic nxt)) }; Types.snd = (List.Cons
212                        ({ Types.fst = Types.None; Types.snd =
213                        (let x0 = Joint.Final (Joint.GOTO (Obj.magic nxt)) in
214                        x0) }, List.Nil)) }
215                    | Bool.False ->
216                      { Types.fst = { Types.fst = Nat.O; Types.snd =
217                        (Identifiers.empty_set PreIdentifiers.LabelTag) };
218                        Types.snd = List.Nil })
219                 | Joint.CALL (x, x0, x1) ->
220                   (match Identifiers.member PreIdentifiers.LabelTag visited'
221                            (Obj.magic nxt) with
222                    | Bool.True ->
223                      { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
224                        (Identifiers.add_set PreIdentifiers.LabelTag
225                          (Identifiers.empty_set PreIdentifiers.LabelTag)
226                          (Obj.magic nxt)) }; Types.snd = (List.Cons
227                        ({ Types.fst = Types.None; Types.snd =
228                        (let x2 = Joint.Final (Joint.GOTO (Obj.magic nxt)) in
229                        x2) }, List.Nil)) }
230                    | Bool.False ->
231                      { Types.fst = { Types.fst = Nat.O; Types.snd =
232                        (Identifiers.empty_set PreIdentifiers.LabelTag) };
233                        Types.snd = List.Nil })
234                 | Joint.COND (x, x0) ->
235                   { Types.fst = { Types.fst = Nat.O; Types.snd =
236                     (Identifiers.empty_set PreIdentifiers.LabelTag) };
237                     Types.snd = List.Nil }
238                 | Joint.Step_seq x ->
239                   (match Identifiers.member PreIdentifiers.LabelTag visited'
240                            (Obj.magic nxt) with
241                    | Bool.True ->
242                      { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
243                        (Identifiers.add_set PreIdentifiers.LabelTag
244                          (Identifiers.empty_set PreIdentifiers.LabelTag)
245                          (Obj.magic nxt)) }; Types.snd = (List.Cons
246                        ({ Types.fst = Types.None; Types.snd =
247                        (let x0 = Joint.Final (Joint.GOTO (Obj.magic nxt)) in
248                        x0) }, List.Nil)) }
249                    | Bool.False ->
250                      { Types.fst = { Types.fst = Nat.O; Types.snd =
251                        (Identifiers.empty_set PreIdentifiers.LabelTag) };
252                        Types.snd = List.Nil }))
253              | Joint.Final x ->
254                { Types.fst = { Types.fst = Nat.O; Types.snd =
255                  (Identifiers.empty_set PreIdentifiers.LabelTag) };
256                  Types.snd = List.Nil }
257              | Joint.FCOND (x0, x1, x2) ->
258                { Types.fst = { Types.fst = Nat.O; Types.snd =
259                  (Identifiers.empty_set PreIdentifiers.LabelTag) };
260                  Types.snd = List.Nil }
261            in
262            graph_visit p globals g
263              (Identifiers.union_set PreIdentifiers.LabelTag
264                add_req_gen.Types.fst.Types.snd required') visited'
265              (Obj.magic (List.append add_req_gen.Types.snd generated'))
266              visiting'
267              (Nat.plus add_req_gen.Types.fst.Types.fst (Nat.S gen_length))
268              n' entry)) __)) __
269
270(** val branch_compress :
271    Joint.graph_params -> AST.ident List.list -> __ -> Graphs.label
272    Types.sig0 -> __ **)
273let branch_compress p globals g entry =
274  g
275
276(** val filter_labels :
277    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> Bool.bool)
278    -> 'a1 LabelledObjects.labelled_obj List.list -> (__, 'a1) Types.prod
279    List.list **)
280let filter_labels tag test c =
281  List.map (fun s ->
282    let { Types.fst = l_opt; Types.snd = x } = s in
283    { Types.fst =
284    (Monad.m_bind0 (Monad.max_def Option.option) l_opt (fun l ->
285      match test l with
286      | Bool.True -> Monad.m_return0 (Monad.max_def Option.option) l
287      | Bool.False -> Obj.magic Types.None)); Types.snd = x }) (Obj.magic c)
288
289(** val linearise_code :
290    Joint.uns_params -> AST.ident List.list -> __ -> Graphs.label Types.sig0
291    -> (__, Graphs.label -> Nat.nat Types.option) Types.prod Types.sig0 **)
292let linearise_code p globals g entry_sig =
293  let g0 = branch_compress p globals g entry_sig in
294  let triple =
295    graph_visit p globals g0 (Identifiers.empty_set PreIdentifiers.LabelTag)
296      (Identifiers.empty_map PreIdentifiers.LabelTag) (Obj.magic List.Nil)
297      (List.Cons ((Types.pi1 entry_sig), List.Nil)) Nat.O
298      (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic g0))
299      (Types.pi1 entry_sig)
300  in
301  let sigma = triple.Types.fst.Types.fst in
302  let required = triple.Types.fst.Types.snd in
303  let crev = triple.Types.snd in
304  let lbld_code = Util.rev (Obj.magic crev) in
305  { Types.fst =
306  (Obj.magic
307    (filter_labels PreIdentifiers.LabelTag (fun l ->
308      Identifiers.member PreIdentifiers.LabelTag required l) lbld_code));
309  Types.snd = (Identifiers.lookup PreIdentifiers.LabelTag sigma) }
310
311(** val linearise_int_fun :
312    Joint.uns_params -> AST.ident List.list ->
313    Joint.joint_closed_internal_function ->
314    (Joint.joint_closed_internal_function, Graphs.label -> Nat.nat
315    Types.option) Types.prod Types.sig0 **)
316let linearise_int_fun p globals f_sig =
317  let code_sigma =
318    linearise_code p globals (Types.pi1 f_sig).Joint.joint_if_code
319      (Obj.magic (Types.pi1 f_sig).Joint.joint_if_entry)
320  in
321  let code = (Types.pi1 code_sigma).Types.fst in
322  let sigma = (Types.pi1 code_sigma).Types.snd in
323  { Types.fst = { Joint.joint_if_luniverse =
324  (Types.pi1 f_sig).Joint.joint_if_luniverse; Joint.joint_if_runiverse =
325  (Types.pi1 f_sig).Joint.joint_if_runiverse; Joint.joint_if_result =
326  (Types.pi1 f_sig).Joint.joint_if_result; Joint.joint_if_params =
327  (Types.pi1 f_sig).Joint.joint_if_params; Joint.joint_if_stacksize =
328  (Types.pi1 f_sig).Joint.joint_if_stacksize;
329  Joint.joint_if_local_stacksize =
330  (Types.pi1 f_sig).Joint.joint_if_local_stacksize; Joint.joint_if_code =
331  code; Joint.joint_if_entry = (Obj.magic Nat.O) }; Types.snd = sigma }
332
333(** val linearise :
334    Joint.uns_params -> Joint.joint_program -> Joint.joint_program **)
335let linearise p pr =
336  Joint.transform_joint_program (Joint.graph_params_to_params p)
337    (Joint.lin_params_to_params p) (fun globals f_in ->
338    (Types.pi1 (linearise_int_fun p globals f_in)).Types.fst) pr
339
Note: See TracBrowser for help on using the repository browser.