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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
|
(* *********************************************************************)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
(* Expand assignments between structs and between unions *)
(* Assumes: simplified code.
Preserves: simplified code, unblocked code *)
open C
open Machine
open Cutil
open Env
open Errors
let maxsize = ref 8
let memcpy_decl = ref (None : ident option)
let memcpy_type =
TFun(TPtr(TVoid [], []),
Some [(Env.fresh_ident "", TPtr(TVoid [], []));
(Env.fresh_ident "", TPtr(TVoid [AConst], []));
(Env.fresh_ident "", TInt(size_t_ikind, []))],
false, [])
let lookup_function env name =
match Env.lookup_ident env name with
| (id, II_ident(sto, ty)) -> (id, ty)
| (id, II_enum _) -> raise (Env.Error(Env.Unbound_identifier name))
let memcpy_ident env =
try lookup_function env "__builtin_memcpy"
with Env.Error _ ->
try lookup_function env "memcpy"
with Env.Error _ ->
match !memcpy_decl with
| Some id ->
(id, memcpy_type)
| None ->
let id = Env.fresh_ident "memcpy" in
memcpy_decl := Some id;
(id, memcpy_type)
let memcpy_words_ident env =
try lookup_function env "__builtin_memcpy_words"
with Env.Error _ -> memcpy_ident env
let transf_assign env loc lhs rhs =
let num_assign = ref 0 in
let assign l r =
incr num_assign;
if !num_assign > !maxsize
then raise Exit
else sassign loc l r in
let rec transf l r =
match unroll env l.etyp with
| TStruct(id, attr) ->
let ci = Env.find_struct env id in
if ci.ci_sizeof = None then
error "%a: Error: incomplete struct '%s'" formatloc loc id.name;
transf_struct l r ci.ci_members
| TUnion(id, attr) ->
raise Exit
| TArray(ty_elt, Some sz, attr) ->
transf_array l r ty_elt 0L sz
| TArray(ty_elt, None, attr) ->
error "%a: Error: array of unknown size" formatloc loc;
sskip (* will be ignored later *)
| _ ->
assign l r
and transf_struct l r = function
| [] -> sskip
| f :: fl ->
sseq loc (transf {edesc = EUnop(Odot f.fld_name, l); etyp = f.fld_typ}
{edesc = EUnop(Odot f.fld_name, r); etyp = f.fld_typ})
(transf_struct l r fl)
and transf_array l r ty idx sz =
if idx >= sz then sskip else begin
let e = intconst idx size_t_ikind in
sseq loc (transf {edesc = EBinop(Oindex, l, e, ty); etyp = ty}
{edesc = EBinop(Oindex, r, e, ty); etyp = ty})
(transf_array l r ty (Int64.add idx 1L) sz)
end
in
try
transf lhs rhs
with Exit ->
let by_words =
match Cutil.sizeof env lhs.etyp with
| Some n -> n mod !config.sizeof_ptr = 0
| None -> false in
let (ident, ty) =
if by_words
then memcpy_words_ident env
else memcpy_ident env in
let memcpy = {edesc = EVar(ident); etyp = ty} in
let e_lhs = {edesc = EUnop(Oaddrof, lhs); etyp = TPtr(lhs.etyp, [])} in
let e_rhs = {edesc = EUnop(Oaddrof, rhs); etyp = TPtr(rhs.etyp, [])} in
let e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, [])} in
{sdesc = Sdo {edesc = ECall(memcpy, [e_lhs; e_rhs; e_size]);
etyp = TVoid[]};
sloc = loc}
let rec transf_stmt env s =
match s.sdesc with
| Sskip -> s
| Sdo {edesc = EBinop(Oassign, lhs, rhs, _)}
when is_composite_type env lhs.etyp ->
transf_assign env s.sloc lhs rhs
| Sdo _ -> s
| Sseq(s1, s2) ->
{s with sdesc = Sseq(transf_stmt env s1, transf_stmt env s2)}
| Sif(e, s1, s2) ->
{s with sdesc = Sif(e, transf_stmt env s1, transf_stmt env s2)}
| Swhile(e, s1) ->
{s with sdesc = Swhile(e, transf_stmt env s1)}
| Sdowhile(s1, e) ->
{s with sdesc = Sdowhile(transf_stmt env s1, e)}
| Sfor(s1, e, s2, s3) ->
{s with sdesc = Sfor(transf_stmt env s1, e,
transf_stmt env s2, transf_stmt env s3)}
| Sbreak -> s
| Scontinue -> s
| Sswitch(e, s1) ->
{s with sdesc = Sswitch(e, transf_stmt env s1)}
| Slabeled(lbl, s1) ->
{s with sdesc = Slabeled(lbl, transf_stmt env s1)}
| Sgoto lbl -> s
| Sreturn _ -> s
| Sblock sl ->
{s with sdesc = Sblock(List.map (transf_stmt env) sl)}
| Sdecl d -> s
let transf_fundef env fd =
{fd with fd_body = transf_stmt env fd.fd_body}
let program p =
memcpy_decl := None;
let p' = Transform.program ~fundef:transf_fundef p in
match !memcpy_decl with
| None -> p'
| Some id ->
{gdesc = Gdecl(Storage_extern, id, memcpy_type, None); gloc = no_loc}
:: p'
|
