source: extracted/initialisation.ml @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 8 years ago

...

File size: 5.5 KB
Line 
1open Preamble
2
3open CostLabel
4
5open FrontEndVal
6
7open Hide
8
9open ByteValues
10
11open GenMem
12
13open FrontEndMem
14
15open Proper
16
17open PositiveMap
18
19open Deqsets
20
21open Extralib
22
23open Lists
24
25open Identifiers
26
27open Integers
28
29open AST
30
31open Division
32
33open Arithmetic
34
35open Extranat
36
37open Vector
38
39open FoldStuff
40
41open BitVector
42
43open Z
44
45open BitVectorZ
46
47open Pointers
48
49open ErrorMessages
50
51open Option
52
53open Setoids
54
55open Monad
56
57open Positive
58
59open PreIdentifiers
60
61open Errors
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open Util
70
71open Bool
72
73open Relations
74
75open Nat
76
77open List
78
79open Hints_declaration
80
81open Core_notation
82
83open Pts
84
85open Logic
86
87open Types
88
89open Coqlib
90
91open Values
92
93open FrontEndOps
94
95open Cminor_syntax
96
97open Extra_bool
98
99open Globalenvs
100
101(** val init_expr :
102    AST.init_data -> (AST.typ, Cminor_syntax.expr) Types.dPair Types.option **)
103let init_expr = function
104| AST.Init_int8 i ->
105  Types.Some { Types.dpi1 = (AST.ASTint (AST.I8, AST.Unsigned)); Types.dpi2 =
106    (Cminor_syntax.Cst ((AST.ASTint (AST.I8, AST.Unsigned)),
107    (FrontEndOps.Ointconst (AST.I8, AST.Unsigned, i)))) }
108| AST.Init_int16 i ->
109  Types.Some { Types.dpi1 = (AST.ASTint (AST.I16, AST.Unsigned));
110    Types.dpi2 = (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Unsigned)),
111    (FrontEndOps.Ointconst (AST.I16, AST.Unsigned, i)))) }
112| AST.Init_int32 i ->
113  Types.Some { Types.dpi1 = (AST.ASTint (AST.I32, AST.Unsigned));
114    Types.dpi2 = (Cminor_syntax.Cst ((AST.ASTint (AST.I32, AST.Unsigned)),
115    (FrontEndOps.Ointconst (AST.I32, AST.Unsigned, i)))) }
116| AST.Init_space n -> Types.None
117| AST.Init_null ->
118  Types.Some { Types.dpi1 = AST.ASTptr; Types.dpi2 = (Cminor_syntax.Op1
119    ((AST.ASTint (AST.I8, AST.Unsigned)), AST.ASTptr, (FrontEndOps.Optrofint
120    (AST.I8, AST.Unsigned)), (Cminor_syntax.Cst ((AST.ASTint (AST.I8,
121    AST.Unsigned)), (FrontEndOps.Ointconst (AST.I8, AST.Unsigned,
122    (BitVector.zero (AST.bitsize_of_intsize AST.I8)))))))) }
123| AST.Init_addrof (id, off) ->
124  Types.Some { Types.dpi1 = AST.ASTptr; Types.dpi2 = (Cminor_syntax.Cst
125    (AST.ASTptr, (FrontEndOps.Oaddrsymbol (id, off)))) }
126
127(** val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __ **)
128let option_jmdiscr x y =
129  Logic.eq_rect_Type2 x
130    (match x with
131     | Types.None -> Obj.magic (fun _ dH -> dH)
132     | Types.Some a0 -> Obj.magic (fun _ dH -> dH __)) y
133
134(** val dPair_jmdiscr :
135    ('a1, 'a2) Types.dPair -> ('a1, 'a2) Types.dPair -> __ **)
136let dPair_jmdiscr x y =
137  Logic.eq_rect_Type2 x
138    (let { Types.dpi1 = a0; Types.dpi2 = a10 } = x in
139    Obj.magic (fun _ dH -> dH __ __)) y
140
141(** val init_datum :
142    AST.ident -> AST.region -> AST.init_data -> Nat.nat -> Cminor_syntax.stmt
143    Types.sig0 **)
144let init_datum id r init off =
145  (match init_expr init with
146   | Types.None -> (fun _ -> Cminor_syntax.St_skip)
147   | Types.Some x ->
148     (fun _ ->
149       (let { Types.dpi1 = t; Types.dpi2 = e0 } = x in
150       (fun _ -> Cminor_syntax.St_store (t, (Cminor_syntax.Cst (AST.ASTptr,
151       (FrontEndOps.Oaddrsymbol (id, off)))), e0))) __)) __
152
153(** val init_var :
154    AST.ident -> AST.region -> AST.init_data List.list -> Cminor_syntax.stmt
155    Types.sig0 **)
156let init_var id r init =
157  (List.foldr (fun datum os ->
158    let { Types.fst = off; Types.snd = s } = os in
159    { Types.fst = (Nat.plus off (Globalenvs.size_init_data datum));
160    Types.snd = (Cminor_syntax.St_seq
161    ((Types.pi1 (init_datum id r datum off)), s)) }) { Types.fst = Nat.O;
162    Types.snd = (Types.pi1 Cminor_syntax.St_skip) } init).Types.snd
163
164(** val init_vars :
165    ((AST.ident, AST.region) Types.prod, AST.init_data List.list) Types.prod
166    List.list -> Cminor_syntax.stmt Types.sig0 **)
167let init_vars vars =
168  List.foldr (fun var s -> Cminor_syntax.St_seq ((Types.pi1 s),
169    (Types.pi1
170      (init_var var.Types.fst.Types.fst var.Types.fst.Types.snd
171        var.Types.snd)))) Cminor_syntax.St_skip vars
172
173(** val add_statement :
174    CostLabel.costlabel -> AST.ident -> Cminor_syntax.stmt Types.sig0 ->
175    (AST.ident, Cminor_syntax.internal_function AST.fundef) Types.prod
176    List.list -> (AST.ident, Cminor_syntax.internal_function AST.fundef)
177    Types.prod List.list **)
178let add_statement cost id s =
179  let s0 = s in
180  List.map (fun idf ->
181    let { Types.fst = id'; Types.snd = f' } = idf in
182    (match AST.ident_eq id id' with
183     | Types.Inl _ ->
184       (match f' with
185        | AST.Internal f ->
186          { Types.fst = id; Types.snd = (AST.Internal
187            { Cminor_syntax.f_return = f.Cminor_syntax.f_return;
188            Cminor_syntax.f_params = f.Cminor_syntax.f_params;
189            Cminor_syntax.f_vars = f.Cminor_syntax.f_vars;
190            Cminor_syntax.f_stacksize = f.Cminor_syntax.f_stacksize;
191            Cminor_syntax.f_body = (Cminor_syntax.St_cost (cost,
192            (Cminor_syntax.St_seq (s0, f.Cminor_syntax.f_body)))) }) }
193        | AST.External f -> { Types.fst = id; Types.snd = (AST.External f) })
194     | Types.Inr _ -> { Types.fst = id'; Types.snd = f' }))
195
196(** val empty_vars :
197    ((AST.ident, AST.region) Types.prod, AST.init_data List.list) Types.prod
198    List.list -> ((AST.ident, AST.region) Types.prod, Nat.nat) Types.prod
199    List.list **)
200let empty_vars =
201  List.map (fun v -> { Types.fst = { Types.fst = v.Types.fst.Types.fst;
202    Types.snd = v.Types.fst.Types.snd }; Types.snd =
203    (Globalenvs.size_init_data_list v.Types.snd) })
204
205(** val replace_init :
206    CostLabel.costlabel -> Cminor_syntax.cminor_program ->
207    Cminor_syntax.cminor_noinit_program **)
208let replace_init cost p =
209  { AST.prog_vars = (empty_vars p.AST.prog_vars); AST.prog_funct =
210    (add_statement cost p.AST.prog_main (init_vars p.AST.prog_vars)
211      p.AST.prog_funct); AST.prog_main = p.AST.prog_main }
212
Note: See TracBrowser for help on using the repository browser.