From 24707fb6b8143d3f969c0fe5c6c3be936813ea31 Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Tue, 14 Mar 2023 18:17:56 +0100 Subject: [PATCH] [machdep] add missing POSIX macros --- share/machdeps/machdep-schema.yaml | 18 ++++++++++++++++++ share/machdeps/machdep_avr_16.yaml | 3 +++ share/machdeps/machdep_gcc_x86_16.yaml | 3 +++ share/machdeps/machdep_gcc_x86_32.yaml | 3 +++ share/machdeps/machdep_gcc_x86_64.yaml | 3 +++ share/machdeps/machdep_msvc_x86_64.yaml | 3 +++ share/machdeps/machdep_ppc_32.yaml | 3 +++ share/machdeps/machdep_x86_16.yaml | 3 +++ share/machdeps/machdep_x86_32.yaml | 3 +++ share/machdeps/machdep_x86_64.yaml | 3 +++ share/machdeps/make_machdep/limits_macros.c | 5 +++++ share/machdeps/make_machdep/make_machdep.py | 1 + src/kernel_internals/runtime/machdep.ml | 3 +++ src/kernel_services/ast_data/cil_types.ml | 3 +++ .../ast_queries/cil_datatype.ml | 3 +++ src/kernel_services/ast_queries/file.ml | 3 +++ .../oracle/realloc_multiple.0.res.oracle | 14 +++++++------- .../oracle/realloc_multiple.1.res.oracle | 18 +++++++++--------- tests/builtins/oracle/strnlen.res.oracle | 2 +- tests/misc/custom_machdep.ml | 3 +++ tests/misc/custom_machdep.yaml | 3 +++ tests/syntax/machdep_char_unsigned.ml | 3 +++ 22 files changed, 89 insertions(+), 17 deletions(-) create mode 100644 share/machdeps/make_machdep/limits_macros.c diff --git a/share/machdeps/machdep-schema.yaml b/share/machdeps/machdep-schema.yaml index 38d83deb099..b4d47f81ac0 100644 --- a/share/machdeps/machdep-schema.yaml +++ b/share/machdeps/machdep-schema.yaml @@ -136,6 +136,12 @@ has__builtin_va_list: type: boolean +host_name_max: + + description: expansion of 'HOST_NAME_MAX' POSIX macro + + type: string + int_fast8_t: description: definition of 'int_fast8_t' @@ -197,6 +203,12 @@ nsig: type: string +path_max: + + description: expansion of 'PATH_MAX' POSIX macro + + type: string + posix_version: description: | value of the macro '_POSIX_VERSION' @@ -304,6 +316,12 @@ tmp_max: type: string +tty_name_max: + + description: value of 'TTY_NAME_MAX' POSIX macro + + type: string + uint_fast8_t: description: definition of 'uint_fast8_t' diff --git a/share/machdeps/machdep_avr_16.yaml b/share/machdeps/machdep_avr_16.yaml index 9d27004bf79..31f2b2ee060 100644 --- a/share/machdeps/machdep_avr_16.yaml +++ b/share/machdeps/machdep_avr_16.yaml @@ -141,6 +141,7 @@ errno: filename_max: '4096' fopen_max: '16' has__builtin_va_list: true +host_name_max: '64' int_fast16_t: int int_fast32_t: int int_fast64_t: long long @@ -151,6 +152,7 @@ little_endian: true machdep_name: machdep_avr_16 mb_cur_max: ((size_t)16) nsig: (64 + 1) +path_max: '4096' posix_version: 200809L ptrdiff_t: int rand_max: '2147483647' @@ -169,6 +171,7 @@ sizeof_void: 1 ssize_t: int time_t: long tmp_max: '238328' +tty_name_max: '32' uint_fast16_t: unsigned int uint_fast32_t: unsigned int uint_fast64_t: unsigned long long diff --git a/share/machdeps/machdep_gcc_x86_16.yaml b/share/machdeps/machdep_gcc_x86_16.yaml index 999181ba2de..49022b0b99b 100644 --- a/share/machdeps/machdep_gcc_x86_16.yaml +++ b/share/machdeps/machdep_gcc_x86_16.yaml @@ -172,6 +172,9 @@ bufsiz: '8192' eof: '(-1)' fopen_max: '16' filename_max: '2048' +path_max: '256' +host_name_max: '64' +tty_name_max: '32' l_tmpnam: '2048' tmp_max: '0xFFFFFFFF' rand_max: '32767' diff --git a/share/machdeps/machdep_gcc_x86_32.yaml b/share/machdeps/machdep_gcc_x86_32.yaml index 53620c5a55d..d474ec51725 100644 --- a/share/machdeps/machdep_gcc_x86_32.yaml +++ b/share/machdeps/machdep_gcc_x86_32.yaml @@ -139,6 +139,7 @@ errno: filename_max: '4096' fopen_max: '16' has__builtin_va_list: true +host_name_max: '64' int_fast16_t: int int_fast32_t: int int_fast64_t: long long @@ -149,6 +150,7 @@ little_endian: true machdep_name: machdep_gcc_x86_32 mb_cur_max: ((size_t) 16 ) nsig: (64 + 1) +path_max: '4096' posix_version: 200809L ptrdiff_t: int rand_max: '2147483647' @@ -167,6 +169,7 @@ sizeof_void: 1 ssize_t: int time_t: long tmp_max: '238328' +tty_name_max: '32' uint_fast16_t: unsigned int uint_fast32_t: unsigned int uint_fast64_t: unsigned long long diff --git a/share/machdeps/machdep_gcc_x86_64.yaml b/share/machdeps/machdep_gcc_x86_64.yaml index 762187987d1..10ba75b7f13 100644 --- a/share/machdeps/machdep_gcc_x86_64.yaml +++ b/share/machdeps/machdep_gcc_x86_64.yaml @@ -139,6 +139,7 @@ errno: filename_max: '4096' fopen_max: '16' has__builtin_va_list: true +host_name_max: '64' int_fast16_t: long int_fast32_t: long int_fast64_t: long @@ -149,6 +150,7 @@ little_endian: true machdep_name: machdep_gcc_x86_64 mb_cur_max: ((size_t) 16 ) nsig: (64 + 1) +path_max: '4096' posix_version: 200809L ptrdiff_t: long rand_max: '2147483647' @@ -167,6 +169,7 @@ sizeof_void: 1 ssize_t: long time_t: long tmp_max: '238328' +tty_name_max: '32' uint_fast16_t: unsigned long uint_fast32_t: unsigned long uint_fast64_t: unsigned long diff --git a/share/machdeps/machdep_msvc_x86_64.yaml b/share/machdeps/machdep_msvc_x86_64.yaml index 39aaae34bab..fd6b2580120 100644 --- a/share/machdeps/machdep_msvc_x86_64.yaml +++ b/share/machdeps/machdep_msvc_x86_64.yaml @@ -134,6 +134,9 @@ posix_version: '' bufsiz: '8192' eof: '(-1)' fopen_max: '16' +host_name_max: '255' +path_max: '256' +tty_name_max: '32' filename_max: '2048' l_tmpnam: '20' tmp_max: '0xFFFFFFFF' diff --git a/share/machdeps/machdep_ppc_32.yaml b/share/machdeps/machdep_ppc_32.yaml index 57d62e62f9b..a9dfce1010a 100644 --- a/share/machdeps/machdep_ppc_32.yaml +++ b/share/machdeps/machdep_ppc_32.yaml @@ -141,6 +141,7 @@ errno: filename_max: '4096' fopen_max: '16' has__builtin_va_list: true +host_name_max: '64' int_fast16_t: int int_fast32_t: int int_fast64_t: long long @@ -151,6 +152,7 @@ little_endian: false machdep_name: machdep_ppc_32 mb_cur_max: ((size_t)16) nsig: (64 + 1) +path_max: '4096' posix_version: 200809L ptrdiff_t: int rand_max: '2147483647' @@ -169,6 +171,7 @@ sizeof_void: 1 ssize_t: int time_t: long tmp_max: '238328' +tty_name_max: '32' uint_fast16_t: unsigned int uint_fast32_t: unsigned int uint_fast64_t: unsigned long long diff --git a/share/machdeps/machdep_x86_16.yaml b/share/machdeps/machdep_x86_16.yaml index 5f90098938e..00cd07f7ebf 100644 --- a/share/machdeps/machdep_x86_16.yaml +++ b/share/machdeps/machdep_x86_16.yaml @@ -172,6 +172,9 @@ bufsiz: '8192' eof: '(-1)' fopen_max: '16' filename_max: '2048' +path_max: '256' +host_name_max: '64' +tty_name_max: '32' l_tmpnam: '2048' tmp_max: '0xFFFFFFFF' rand_max: '32767' diff --git a/share/machdeps/machdep_x86_32.yaml b/share/machdeps/machdep_x86_32.yaml index 63513825a26..d06c7f607bb 100644 --- a/share/machdeps/machdep_x86_32.yaml +++ b/share/machdeps/machdep_x86_32.yaml @@ -139,6 +139,7 @@ errno: filename_max: '4096' fopen_max: '16' has__builtin_va_list: true +host_name_max: '64' int_fast16_t: int int_fast32_t: int int_fast64_t: long long @@ -149,6 +150,7 @@ little_endian: true machdep_name: machdep_x86_32 mb_cur_max: ((size_t) 16 ) nsig: (64 + 1) +path_max: '4096' posix_version: 200809L ptrdiff_t: int rand_max: '2147483647' @@ -167,6 +169,7 @@ sizeof_void: -1 ssize_t: int time_t: long tmp_max: '238328' +tty_name_max: '32' uint_fast16_t: unsigned int uint_fast32_t: unsigned int uint_fast64_t: unsigned long long diff --git a/share/machdeps/machdep_x86_64.yaml b/share/machdeps/machdep_x86_64.yaml index 7852eb877a8..049407efe1b 100644 --- a/share/machdeps/machdep_x86_64.yaml +++ b/share/machdeps/machdep_x86_64.yaml @@ -139,6 +139,7 @@ errno: filename_max: '4096' fopen_max: '16' has__builtin_va_list: true +host_name_max: '64' int_fast16_t: long int_fast32_t: long int_fast64_t: long @@ -149,6 +150,7 @@ little_endian: true machdep_name: machdep_x86_64 mb_cur_max: ((size_t) 16 ) nsig: (64 + 1) +path_max: '4096' posix_version: 200809L ptrdiff_t: long rand_max: '2147483647' @@ -167,6 +169,7 @@ sizeof_void: -1 ssize_t: long time_t: long tmp_max: '238328' +tty_name_max: '32' uint_fast16_t: unsigned long uint_fast32_t: unsigned long uint_fast64_t: unsigned long diff --git a/share/machdeps/make_machdep/limits_macros.c b/share/machdeps/make_machdep/limits_macros.c new file mode 100644 index 00000000000..fdef911d18e --- /dev/null +++ b/share/machdeps/make_machdep/limits_macros.c @@ -0,0 +1,5 @@ +#include <limits.h> + +int path_max_is = PATH_MAX; +int tty_name_max_is = TTY_NAME_MAX; +int host_name_max_is = HOST_NAME_MAX; diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py index 8c49b8e495b..9f8dd0b3f7b 100755 --- a/share/machdeps/make_machdep/make_machdep.py +++ b/share/machdeps/make_machdep/make_machdep.py @@ -203,6 +203,7 @@ source_files = [ ("weof.c", "macro"), ("wordsize.c", "macro"), ("posix_version.c", "macro"), + ("limits_macros.c", "macro"), ("stdio_macros.c", "macro"), ("stdlib_macros.c", "macro"), ("nsig.c", "macro"), diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml index 127f612a11e..8b6a81c693d 100644 --- a/src/kernel_internals/runtime/machdep.ml +++ b/src/kernel_internals/runtime/machdep.ml @@ -272,6 +272,9 @@ let gen_all_defines fmt mach = gen_define_macro fmt "__FC_TMP_MAX" mach.tmp_max; gen_define_macro fmt "__FC_RAND_MAX" mach.rand_max; gen_define_macro fmt "__FC_MB_CUR_MAX" mach.mb_cur_max; + gen_define_macro fmt "__FC_PATH_MAX" mach.path_max; + gen_define_macro fmt "__FC_HOST_NAME_MAX" mach.host_name_max; + gen_define_macro fmt "__FC_TTY_NAME_MAX" mach.tty_name_max; List.iter (gen_define_errno_macro fmt) mach.errno; gen_define_macro fmt "__FC_TIME_T" mach.time_t; gen_define_macro fmt "__FC_NSIG" mach.nsig; diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml index 55986d1421a..e1c9e7270e8 100644 --- a/src/kernel_services/ast_data/cil_types.ml +++ b/src/kernel_services/ast_data/cil_types.ml @@ -1918,7 +1918,10 @@ type mach = { eof: string; (* expansion of EOF macro *) fopen_max: string; (* expansion of FOPEN_MAX macro *) filename_max: string; (* expansion of FILENAME_MAX macro *) + host_name_max: string; (* expansion of HOST_NAME_MAX macro *) + tty_name_max: string; (* expansion of TTY_NAME_MAX macro *) l_tmpnam: string; (* expansion of L_tmpnam macro *) + path_max: string; (* expansion of PATH_MAX macro *) tmp_max: string; (* expansion of TMP_MAX macro *) rand_max: string; (* expansion of RAND_MAX macro *) mb_cur_max: string; (* expansion of MB_CUR_MAX macro *) diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml index 80698e87233..35810382a30 100644 --- a/src/kernel_services/ast_queries/cil_datatype.ml +++ b/src/kernel_services/ast_queries/cil_datatype.ml @@ -2680,6 +2680,9 @@ let dummy_machdep = eof = "(-1)"; fopen_max = "255"; filename_max = "4095"; + path_max = "256"; + tty_name_max = "255"; + host_name_max = "255"; l_tmpnam = "63"; tmp_max = "1024"; rand_max = "0xFFFFFFFE"; diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml index 3f8d916dac7..e9d681ce0af 100644 --- a/src/kernel_services/ast_queries/file.ml +++ b/src/kernel_services/ast_queries/file.ml @@ -398,7 +398,10 @@ type mach = Cil_types.mach = { eof: string; fopen_max: string; filename_max: string; + host_name_max: string; + tty_name_max: string; l_tmpnam: string; + path_max: string; tmp_max: string; rand_max: string; mb_cur_max: string; diff --git a/tests/builtins/oracle/realloc_multiple.0.res.oracle b/tests/builtins/oracle/realloc_multiple.0.res.oracle index 90a945812a6..5908db2b9e5 100644 --- a/tests/builtins/oracle/realloc_multiple.0.res.oracle +++ b/tests/builtins/oracle/realloc_multiple.0.res.oracle @@ -21,7 +21,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -56,7 +56,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -105,7 +105,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -142,7 +142,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -196,7 +196,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -238,7 +238,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -280,7 +280,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} diff --git a/tests/builtins/oracle/realloc_multiple.1.res.oracle b/tests/builtins/oracle/realloc_multiple.1.res.oracle index 831c3434213..052f0f273fa 100644 --- a/tests/builtins/oracle/realloc_multiple.1.res.oracle +++ b/tests/builtins/oracle/realloc_multiple.1.res.oracle @@ -29,7 +29,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -64,7 +64,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -95,7 +95,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -150,7 +150,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -187,7 +187,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -222,7 +222,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -280,7 +280,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -326,7 +326,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -368,7 +368,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} diff --git a/tests/builtins/oracle/strnlen.res.oracle b/tests/builtins/oracle/strnlen.res.oracle index 0853c554d16..06fce1695a9 100644 --- a/tests/builtins/oracle/strnlen.res.oracle +++ b/tests/builtins/oracle/strnlen.res.oracle @@ -37,7 +37,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} diff --git a/tests/misc/custom_machdep.ml b/tests/misc/custom_machdep.ml index 974683a3127..5997c0388e3 100644 --- a/tests/misc/custom_machdep.ml +++ b/tests/misc/custom_machdep.ml @@ -53,6 +53,9 @@ let mach = eof = "(-1)"; fopen_max = "128"; filename_max = "1023"; + path_max = "255"; + tty_name_max = "255"; + host_name_max = "255"; l_tmpnam = "255"; tmp_max = "4095"; rand_max = "0xFFFFFFFE"; diff --git a/tests/misc/custom_machdep.yaml b/tests/misc/custom_machdep.yaml index 1fe7b404a43..1f6ef8d4b4e 100644 --- a/tests/misc/custom_machdep.yaml +++ b/tests/misc/custom_machdep.yaml @@ -49,6 +49,9 @@ fopen_max: '128' filename_max: '1023' l_tmpnam: '255' tmp_max: '255' +tty_name_max: '255' +host_name_max: '255' +path_max: '255' rand_max: '0xFFFFFE' mb_cur_max: '16' sig_atomic_t: int diff --git a/tests/syntax/machdep_char_unsigned.ml b/tests/syntax/machdep_char_unsigned.ml index 66f8c989e2a..98030ed4398 100644 --- a/tests/syntax/machdep_char_unsigned.ml +++ b/tests/syntax/machdep_char_unsigned.ml @@ -51,6 +51,9 @@ let md = { bufsiz = "8192"; eof = "(-1)"; fopen_max = "16"; + host_name_max = "255"; + tty_name_max = "255"; + path_max = "255"; filename_max = "2048"; l_tmpnam = "2048"; tmp_max = "0xFFFFFFFF"; -- GitLab