Skip to content

Commit d97caa1

Browse files
xavierleroyxavierleroy
committed
Revise the declaration of __compcert_* helper functions
Don't put them in the C environment used for elaboration. Instead, add them directly to the generated CompCert C at the end of the C2C translation.
1 parent a0ad5ff commit d97caa1

File tree

1 file changed

+79
-82
lines changed

1 file changed

+79
-82
lines changed

‎cfrontend/C2C.ml‎

Lines changed: 79 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -253,88 +253,11 @@ let builtins_generic = {
253253
(TVoid [],
254254
[TPtr(TVoid [], [])],
255255
false);
256-
"__compcert_va_int32",
257-
(TInt(IUInt, []),
258-
[TPtr(TVoid [], [])],
259-
false);
260-
"__compcert_va_int64",
261-
(TInt(IULongLong, []),
262-
[TPtr(TVoid [], [])],
263-
false);
264-
"__compcert_va_float64",
265-
(TFloat(FDouble, []),
266-
[TPtr(TVoid [], [])],
267-
false);
268-
"__compcert_va_composite",
269-
(TPtr(TVoid [], []),
270-
[TPtr(TVoid [], []); TInt(IULong, [])],
271-
false);
272256
(* Optimization hints *)
273257
"__builtin_unreachable",
274258
(TVoid [], [], false);
275259
"__builtin_expect",
276-
(TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false);
277-
(* Helper functions for int64 arithmetic *)
278-
"__compcert_i64_dtos",
279-
(TInt(ILongLong, []),
280-
[TFloat(FDouble, [])],
281-
false);
282-
"__compcert_i64_dtou",
283-
(TInt(IULongLong, []),
284-
[TFloat(FDouble, [])],
285-
false);
286-
"__compcert_i64_stod",
287-
(TFloat(FDouble, []),
288-
[TInt(ILongLong, [])],
289-
false);
290-
"__compcert_i64_utod",
291-
(TFloat(FDouble, []),
292-
[TInt(IULongLong, [])],
293-
false);
294-
"__compcert_i64_stof",
295-
(TFloat(FFloat, []),
296-
[TInt(ILongLong, [])],
297-
false);
298-
"__compcert_i64_utof",
299-
(TFloat(FFloat, []),
300-
[TInt(IULongLong, [])],
301-
false);
302-
"__compcert_i64_sdiv",
303-
(TInt(ILongLong, []),
304-
[TInt(ILongLong, []); TInt(ILongLong, [])],
305-
false);
306-
"__compcert_i64_udiv",
307-
(TInt(IULongLong, []),
308-
[TInt(IULongLong, []); TInt(IULongLong, [])],
309-
false);
310-
"__compcert_i64_smod",
311-
(TInt(ILongLong, []),
312-
[TInt(ILongLong, []); TInt(ILongLong, [])],
313-
false);
314-
"__compcert_i64_umod",
315-
(TInt(IULongLong, []),
316-
[TInt(IULongLong, []); TInt(IULongLong, [])],
317-
false);
318-
"__compcert_i64_shl",
319-
(TInt(ILongLong, []),
320-
[TInt(ILongLong, []); TInt(IInt, [])],
321-
false);
322-
"__compcert_i64_shr",
323-
(TInt(IULongLong, []),
324-
[TInt(IULongLong, []); TInt(IInt, [])],
325-
false);
326-
"__compcert_i64_sar",
327-
(TInt(ILongLong, []),
328-
[TInt(ILongLong, []); TInt(IInt, [])],
329-
false);
330-
"__compcert_i64_smulh",
331-
(TInt(ILongLong, []),
332-
[TInt(ILongLong, []); TInt(ILongLong, [])],
333-
false);
334-
"__compcert_i64_umulh",
335-
(TInt(IULongLong, []),
336-
[TInt(IULongLong, []); TInt(IULongLong, [])],
337-
false)
260+
(TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false)
338261
]
339262
}
340263

@@ -1280,7 +1203,6 @@ let convertFundef loc env fd =
12801203
(** External function declaration *)
12811204

12821205
let re_builtin = Str.regexp "__builtin_"
1283-
let re_runtime = Str.regexp "__compcert_i64_"
12841206

12851207
let convertFundecl env (sto, id, ty, optinit) =
12861208
let (args, res, cconv) =
@@ -1293,7 +1215,6 @@ let convertFundecl env (sto, id, ty, optinit) =
12931215
let ef =
12941216
if id.name = "malloc" then AST.EF_malloc else
12951217
if id.name = "free" then AST.EF_free else
1296-
if Str.string_match re_runtime id.name 0 then AST.EF_runtime(id'', sg) else
12971218
if Str.string_match re_builtin id.name 0
12981219
&& List.mem_assoc id.name builtins.builtin_functions
12991220
then AST.EF_builtin(id'', sg)
@@ -1415,6 +1336,81 @@ let rec convertCompositedefs env res gl =
14151336
| _ ->
14161337
convertCompositedefs env res gl'
14171338

1339+
(** Add declarations for the helper functions
1340+
(for varargs and for int64 arithmetic) *)
1341+
1342+
let helper_functions () = [
1343+
"__compcert_va_int32",
1344+
Tint(I32, Unsigned, noattr),
1345+
[Tpointer(Tvoid, noattr)];
1346+
"__compcert_va_int64",
1347+
Tlong(Unsigned, noattr),
1348+
[Tpointer(Tvoid, noattr)];
1349+
"__compcert_va_float64",
1350+
Tfloat(F64, noattr),
1351+
[Tpointer(Tvoid, noattr)];
1352+
"__compcert_va_composite",
1353+
Tpointer(Tvoid, noattr),
1354+
[Tpointer(Tvoid, noattr); convertIkind (Cutil.size_t_ikind()) noattr];
1355+
"__compcert_i64_dtos",
1356+
Tlong(Signed, noattr),
1357+
[Tfloat(F64, noattr)];
1358+
"__compcert_i64_dtou",
1359+
Tlong(Unsigned, noattr),
1360+
[Tfloat(F64, noattr)];
1361+
"__compcert_i64_stod",
1362+
Tfloat(F64, noattr),
1363+
[Tlong(Signed, noattr)];
1364+
"__compcert_i64_utod",
1365+
Tfloat(F64, noattr),
1366+
[Tlong(Unsigned, noattr)];
1367+
"__compcert_i64_stof",
1368+
Tfloat(F32, noattr),
1369+
[Tlong(Signed, noattr)];
1370+
"__compcert_i64_utof",
1371+
Tfloat(F32, noattr),
1372+
[Tlong(Unsigned, noattr)];
1373+
"__compcert_i64_sdiv",
1374+
Tlong(Signed, noattr),
1375+
[Tlong(Signed, noattr); Tlong(Signed, noattr)];
1376+
"__compcert_i64_udiv",
1377+
Tlong(Unsigned, noattr),
1378+
[Tlong(Unsigned, noattr); Tlong(Unsigned, noattr)];
1379+
"__compcert_i64_smod",
1380+
Tlong(Signed, noattr),
1381+
[Tlong(Signed, noattr); Tlong(Signed, noattr)];
1382+
"__compcert_i64_umod",
1383+
Tlong(Unsigned, noattr),
1384+
[Tlong(Unsigned, noattr); Tlong(Unsigned, noattr)];
1385+
"__compcert_i64_shl",
1386+
Tlong(Signed, noattr),
1387+
[Tlong(Signed, noattr); Tint(I32, Signed, noattr)];
1388+
"__compcert_i64_shr",
1389+
Tlong(Unsigned, noattr),
1390+
[Tlong(Unsigned, noattr); Tint(I32, Signed, noattr)];
1391+
"__compcert_i64_sar",
1392+
Tlong(Signed, noattr),
1393+
[Tlong(Signed, noattr); Tint(I32, Signed, noattr)];
1394+
"__compcert_i64_smulh",
1395+
Tlong(Signed, noattr),
1396+
[Tlong(Signed, noattr); Tlong(Signed, noattr)];
1397+
"__compcert_i64_umulh",
1398+
Tlong(Unsigned, noattr),
1399+
[Tlong(Unsigned, noattr); Tlong(Unsigned, noattr)]
1400+
]
1401+
1402+
let helper_function_declaration (name, tyres, tyargs) =
1403+
let tyargs =
1404+
List.fold_right (fun t tl -> Tcons(t, tl)) tyargs Tnil in
1405+
let ef =
1406+
AST.EF_runtime(coqstring_of_camlstring name,
1407+
signature_of_type tyargs tyres AST.cc_default) in
1408+
(intern_string name,
1409+
AST.Gfun (Ctypes.External(ef, tyargs, tyres, AST.cc_default)))
1410+
1411+
let add_helper_functions globs =
1412+
List.map helper_function_declaration (helper_functions()) @ globs
1413+
14181414
(** Build environment of typedefs, structs, unions and enums *)
14191415

14201416
let rec translEnv env = function
@@ -1512,10 +1508,11 @@ let convertProgram p =
15121508
comp_env := ce;
15131509
let gl1 = convertGlobdecls env [] p in
15141510
let gl2 = globals_for_strings gl1 in
1511+
let gl3 = add_helper_functions gl2 in
15151512
comp_env := Maps.PTree.empty;
15161513
let p' =
1517-
{ prog_defs = gl2;
1518-
prog_public = public_globals gl2;
1514+
{ prog_defs = gl3;
1515+
prog_public = public_globals gl3;
15191516
prog_main = intern_string !Clflags.main_function_name;
15201517
prog_types = typs;
15211518
prog_comp_env = ce } in

0 commit comments

Comments
 (0)