source: driver/extracted/initialisation.ml @ 3106

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