From e7986efec631fe998a9219e95dbfe55c4ed74caa Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 28 Feb 2023 14:40:45 +0100
Subject: [PATCH] [machdep] generate all __fc_machdep.h that can be handled by
current YAML schema
---
src/kernel_internals/runtime/machdep.ml | 141 +++++++++++++++++++++++-
1 file changed, 138 insertions(+), 3 deletions(-)
diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml
index 98f5833119b..e2daa153cec 100644
--- a/src/kernel_internals/runtime/machdep.ml
+++ b/src/kernel_internals/runtime/machdep.ml
@@ -3,13 +3,25 @@ open Cil_types
let gen_define fmt macro pp def =
Format.fprintf fmt "#define %s %a@\n" macro pp def
+let gen_undef fmt macro = Format.fprintf fmt "#undef %s@\n" macro
+
let gen_define_string fmt macro def =
gen_define fmt macro Format.pp_print_string def
+let gen_define_literal_string fmt macro def =
+ gen_define fmt macro Format.pp_print_string ("\"" ^ def ^ "\"")
+
+let gen_define_int fmt macro def = gen_define fmt macro Format.pp_print_int def
+
let gen_byte_order fmt mach =
gen_define_string fmt "__FC_BYTE_ORDER"
(if mach.little_endian then "__LITTLE_ENDIAN" else "__BIG_ENDIAN")
+let no_signedness s =
+ let s = Option.value ~default:s (Extlib.string_del_prefix "signed" s) in
+ let s = Option.value ~default:s (Extlib.string_del_prefix "unsigned" s) in
+ if s = "" then "int" else s
+
let suff_of_kind =
[ "char", "";
"short", "";
@@ -23,7 +35,7 @@ let pp_of_kind =
"short", "h";
"int", "";
"long", "l";
- "long long", "ll";
+ "long long", "ll"
]
let max_val bitsize is_signed kind =
@@ -47,11 +59,21 @@ let gen_define_max_stype fmt name bitsize kind =
let gen_define_max_utype fmt name bitsize kind =
gen_define_string fmt ("__UINT" ^ name ^ "_MAX") (max_val bitsize false kind)
+let gen_std_signed fmt name bitsize kind =
+ gen_define_string fmt ("__FC_" ^ name ^ "_MIN") (min_val bitsize kind);
+ gen_define_string fmt ("__FC_" ^ name ^ "_MAX") (max_val bitsize true kind)
+
+let gen_std_unsigned fmt name bitsize kind =
+ gen_define_string fmt ("__FC_" ^ name ^ "_MAX") (max_val bitsize false kind)
+
let gen_define_printing_prefix fmt name kind =
- gen_define_string fmt
+ gen_define_literal_string fmt
("__PRI" ^ name ^ "_PREFIX")
(List.assoc kind pp_of_kind)
+let gen_sizeof fmt name size =
+ gen_define_int fmt ("__SIZEOF_" ^ name) size
+
let existing_int_size mach =
[ 1, "char";
mach.sizeof_short, "short";
@@ -59,6 +81,24 @@ let existing_int_size mach =
mach.sizeof_long, "long";
mach.sizeof_longlong, "long long"]
+let std_type_name mach =
+ [ "char", if mach.char_is_unsigned then ("UCHAR", false) else ("SCHAR", true);
+ "signed char", ("SCHAR", true);
+ "unsigned char", ("UCHAR", false);
+ "short", ("SHRT", true);
+ "signed short", ("SHRT", true);
+ "unsigned short", ("USHRT", false);
+ "int", ("INT", true);
+ "signed", ("INT", true);
+ "signed int", ("INT", true);
+ "unsigned", ("UINT", false);
+ "unsigned int", ("UINT", false);
+ "long", ("LONG", true);
+ "unsigned long", ("ULONG", false);
+ "long long", ("LLONG", true);
+ "unsigned long long", ("ULLONG", false)
+ ]
+
let gen_int_type_family fmt name bitsize kind =
gen_define_stype fmt name kind;
gen_define_utype fmt name kind;
@@ -82,16 +122,111 @@ let gen_fixed_size_family fmt bitsize mach =
let gen_max_size_int fmt mach =
gen_int_type_family fmt "MAX" (8 * mach.sizeof_longlong) "long long"
+let gen_std_min_max fmt mach =
+ gen_std_signed fmt "SCHAR" 8 "char";
+ gen_std_unsigned fmt "UCHAR" 8 "char";
+ gen_std_signed fmt "SHRT" (8*mach.sizeof_short) "short";
+ gen_std_unsigned fmt "USHRT" (8*mach.sizeof_short) "short";
+ gen_std_signed fmt "INT" (8*mach.sizeof_int) "int";
+ gen_std_unsigned fmt "UINT" (8*mach.sizeof_int) "int";
+ gen_std_signed fmt "LONG" (8*mach.sizeof_long) "long";
+ gen_std_unsigned fmt "ULONG" (8*mach.sizeof_long) "long";
+ gen_std_signed fmt "LLONG" (8*mach.sizeof_longlong) "long long";
+ gen_std_unsigned fmt "ULLONG" (8*mach.sizeof_longlong) "long long"
+
+let gen_va_list_repr fmt mach =
+ let repr =
+ if mach.has__builtin_va_list then "__builtin_va_list" else "char*"
+ in
+ gen_define_string fmt "__FC_VA_LIST_T" repr
+
+let gen_char_unsigned_flag fmt mach =
+ let macro = "__CHAR_UNSIGNED__" in
+ if mach.char_is_unsigned then gen_undef fmt macro
+ else gen_define_string fmt macro "1"
+
+let gen_sizeof_std fmt mach =
+ gen_sizeof fmt "SHORT" mach.sizeof_short;
+ gen_sizeof fmt "INT" mach.sizeof_int;
+ gen_sizeof fmt "LONG" mach.sizeof_long;
+ gen_sizeof fmt "LONGLONG" mach.sizeof_longlong
+
+let gen_intlike_min fmt name repr mach =
+ let macro = name ^ "_MIN" in
+ let repr_name, is_signed = List.assoc repr (std_type_name mach) in
+ if is_signed then gen_define_string fmt macro ("__FC_" ^ repr_name ^ "_MIN")
+ else gen_define_int fmt macro 0
+
+let gen_intlike_max fmt name repr mach =
+ let macro = name ^ "_MAX" in
+ let repr_name, _ = List.assoc repr (std_type_name mach) in
+ gen_define_string fmt macro ("__FC_" ^ repr_name ^ "_MAX")
+
+(* assuming all archs have an 8-bit char. In any case, if we end up dealing
+ with something else at some point, machdep will not be the only place were
+ changes will be required. *)
+let gen_char_bit fmt _mach =
+ gen_define_int fmt "__CHAR_BIT" 8
+
let gen_all_defines fmt mach =
Format.fprintf fmt "/* Machdep-specific info for Frama-C's libc */@\n";
Format.fprintf fmt "#ifndef __FC_MACHDEP@\n#define __FC_MACHDEP@\n";
gen_byte_order fmt mach;
- (* TODO: __FC_POSIX_VERSION *)
gen_fixed_size_family fmt 8 mach;
gen_fixed_size_family fmt 16 mach;
gen_fixed_size_family fmt 32 mach;
gen_fixed_size_family fmt 64 mach;
gen_max_size_int fmt mach;
+ gen_std_min_max fmt mach;
+ gen_va_list_repr fmt mach;
+ gen_char_unsigned_flag fmt mach;
+ gen_sizeof_std fmt mach;
+ gen_char_bit fmt mach;
+ gen_define_string fmt "__PTRDIFF_T" mach.ptrdiff_t;
+ gen_define_string fmt "__SIZE_T" mach.size_t;
+ gen_define_string fmt "__WCHAR_T" mach.wchar_t;
+ gen_define_string fmt "__INTPTR_T" mach.intptr_t;
+ gen_define_string fmt "__UINTPTR_T" mach.uintptr_t;
+ gen_define_string fmt "__PTRDIFF_T" mach.ptrdiff_t;
+ gen_define_string fmt "__WINT_T" mach.wint_t;
+ (* gen_define_string fmt "__SSIZE_T" mach.ssize_t; *)
+ gen_intlike_max fmt "__FC_SIZE" mach.size_t mach;
+ gen_intlike_min fmt "__FC_INTPTR" mach.intptr_t mach;
+ gen_intlike_max fmt "__FC_INTPTR" mach.intptr_t mach;
+ gen_intlike_max fmt "__FC_UINTPTR" mach.uintptr_t mach;
+ gen_intlike_min fmt "__FC_WCHAR" mach.wchar_t mach;
+ gen_intlike_max fmt "__FC_WCHAR" mach.wchar_t mach;
+ (* TODO: __SSIZE_MAX *)
+ gen_intlike_min fmt "__FC_PTRDIFF" mach.ptrdiff_t mach;
+ gen_intlike_max fmt "__FC_PTRDIFF" mach.ptrdiff_t mach;
+ gen_intlike_min fmt "__FC_WINT" mach.wint_t mach;
+ gen_intlike_max fmt "__FC_WINT" mach.wint_t mach;
+ (* TODO: __FC_WEOF *)
+ (* NB: Frama-C's inttypes.h is assuming that intptr_t and uintptr_t have the
+ same rank when it comes to define PRI.?PTR macros. *)
+ gen_define_literal_string fmt "__PRIPTR_PREFIX"
+ (List.assoc (no_signedness mach.intptr_t) pp_of_kind);
+
+ (* TODO: __FC_POSIX_VERSION *)
+ (* TODO: __FC_HOST_NAME_MAX *)
+ (* TODO: __FC_TTY_NAME_MAX *)
+ (* TODO: __FC_SIG_ATOMIC_MIN *)
+ (* TODO: __FC_SIG_ATOMIC_MAX *)
+ (* TODO: __FC_BUFSIZ *)
+ (* TODO: __FC_EOF *)
+ (* TODO: __FC_FOPEN_MAX *)
+ (* TODO: __FC_FILENAME_MAX *)
+ (* TODO: __FC_L_tmpnam *)
+ (* TODO: __FC_TMP_MAX *)
+ (* TODO: __FC_RAND_MAX *)
+ (* TODO: __FC_MB_CUR_MAX *)
+ (* TODO: __FC_E*, errno enumeration *)
+ (* TODO: __FC_TIME_T *)
+ (* TODO: __FC_NSIG *)
+ (* TODO: __FC__NSIG *)
+ (* TODO: __WORDSIZE *)
+ (* TODO: gcc builtins *)
+
Format.fprintf fmt "#endif // __FC_MACHDEP@\n"
let generate_machdep_header mach =
--
GitLab