source: extracted/linearise.ml @ 2797

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

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

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