1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 2 of the License, or *)
(* (at your option) any later version. This file is also distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(* Generic program transformation *)
open C
open Cutil
open Env
(* Recording fresh temporaries *)
let temporaries = ref ([]: decl list)
let reset_temps () =
temporaries := []
let new_temp_var ?(name = "t") ty =
let id = Env.fresh_ident name in
temporaries := (Storage_default, id, ty, None) :: !temporaries;
id
let new_temp ?(name = "t") ty =
let id = new_temp_var ~name ty in
{ edesc = EVar id; etyp = ty }
let get_temps () =
let temps = !temporaries in
temporaries := [];
List.rev temps
(* Generic transformation *)
let program
?(decl = fun env d -> d)
?(fundef = fun env fd -> fd)
?(composite = fun env su id attr fl -> (attr, fl))
?(typedef = fun env id ty -> ty)
?(enum = fun env id members -> members)
?(pragma = fun env s -> s)
p =
let rec transf_globdecls env accu = function
| [] -> List.rev accu
| g :: gl ->
let (desc', env') =
match g.gdesc with
| Gdecl((sto, id, ty, init) as d) ->
(Gdecl(decl env d), Env.add_ident env id sto ty)
| Gfundef f ->
(Gfundef(fundef env f),
Env.add_ident env f.fd_name f.fd_storage (fundef_typ f))
| Gcompositedecl(su, id, attr) ->
(Gcompositedecl(su, id, attr),
Env.add_composite env id (composite_info_decl env su attr))
| Gcompositedef(su, id, attr, fl) ->
let (attr', fl') = composite env su id attr fl in
(Gcompositedef(su, id, attr', fl'),
Env.add_composite env id (composite_info_def env su attr fl))
| Gtypedef(id, ty) ->
(Gtypedef(id, typedef env id ty), Env.add_typedef env id ty)
| Genumdef(id, members) ->
(Genumdef(id, enum env id members), env)
| Gpragma s ->
(Gpragma(pragma env s), env)
in
transf_globdecls env' ({g with gdesc = desc'} :: accu) gl
in transf_globdecls (Builtins.environment()) [] p
|
