diff --git a/bin/frama-c-script b/bin/frama-c-script index 669573f5394d1bcd7cae750123a17f013204fbc8..3e2bfc9335f779c6637a22db14df6c23ffad0c30 100755 --- a/bin/frama-c-script +++ b/bin/frama-c-script @@ -279,6 +279,11 @@ case "$command" in shift; ${FRAMAC_LIB}/analysis-scripts/creduce.sh "$@"; ;; + "make-machdep") + shift; + ${FRAMAC_LIB}/make_machdep/make_machdep.py \ + --machdep-schema ${FRAMAC_SHARE}/machdeps/machdep-schema.yaml "$@" + ;; *) echo "error: unrecognized command: $command"; exit 1 diff --git a/nix/frama-c.nix b/nix/frama-c.nix index aa1ac64409e8b8a22e4b2629e12f0b6568856d11..c9fb61365d1b771b01e787a7db34ab9dee375770 100644 --- a/nix/frama-c.nix +++ b/nix/frama-c.nix @@ -43,6 +43,8 @@ , dos2unix , doxygen , python3 +, python3Packages +, yq , release_mode ? false }: @@ -101,6 +103,8 @@ stdenvNoCC.mkDerivation rec { dos2unix doxygen python3 + python3Packages.pyaml + yq ]; outputs = [ "out" "build_dir" ]; diff --git a/nix/internal-tests.nix b/nix/internal-tests.nix index 4bbf098618c4190ee55bcdfb908355c15c3fafc2..cef5cbba337a9b5f1d41c865eed47bb8ec894a61 100644 --- a/nix/internal-tests.nix +++ b/nix/internal-tests.nix @@ -47,6 +47,8 @@ , perl , pkgs , python3 +, python3Packages +, yq , swiProlog , time , wp-cache @@ -107,6 +109,8 @@ stdenvNoCC.mkDerivation rec { perl pkgs.getopt python3 + python3Packages.pyaml + yq swiProlog time ]; diff --git a/share/dune b/share/dune index 77f771002d1b2e413dd411f13512b51fbf62f5b9..f00d3b92a5ed96459a035d8ca93acd082c366e9c 100644 --- a/share/dune +++ b/share/dune @@ -339,7 +339,9 @@ (machdeps/machdep_gcc_x86_32.yaml as share/machdeps/machdep_gcc_x86_32.yaml) (machdeps/machdep_gcc_x86_64.yaml as share/machdeps/machdep_gcc_x86_64.yaml) (machdeps/machdep_msvc_x86_64.yaml as share/machdeps/machdep_msvc_x86_64.yaml) - (machdeps/machdep_ppc_32.yaml as share/machdeps/machdep_ppc_32.yaml)) + (machdeps/machdep_ppc_32.yaml as share/machdeps/machdep_ppc_32.yaml) + (machdeps/machdep-schema.yaml as share/machdeps/machdep-schema.yaml) + ) ) ; machdep generation script @@ -368,9 +370,21 @@ (machdeps/make_machdep/alignof_str.c as lib/make_machdep/alignof_str.c) (machdeps/make_machdep/char_is_unsigned.c as lib/make_machdep/char_is_unsigned.c) (machdeps/make_machdep/const_string_literals.c as lib/make_machdep/const_string_literals.c) + (machdeps/make_machdep/errno.c as lib/make_machdep/errno.c) (machdeps/make_machdep/has__builtin_va_list.c as lib/make_machdep/has__builtin_va_list.c) + (machdeps/make_machdep/int_fast16_t.c as lib/make_machdep/int_fast16_t.c) + (machdeps/make_machdep/int_fast32_t.c as lib/make_machdep/int_fast32_t.c) + (machdeps/make_machdep/int_fast64_t.c as lib/make_machdep/int_fast64_t.c) + (machdeps/make_machdep/int_fast8_t.c as lib/make_machdep/int_fast8_t.c) + (machdeps/make_machdep/intptr_t.c as lib/make_machdep/intptr_t.c) + (machdeps/make_machdep/limits_macros.c as lib/make_machdep/limits_macros.c) (machdeps/make_machdep/little_endian.c as lib/make_machdep/little_endian.c) + (machdeps/make_machdep/make_machdep_common.h as lib/make_machdep/make_machdep_common.h) + (machdeps/make_machdep/nsig.c as lib/make_machdep/nsig.c) + (machdeps/make_machdep/posix_version.c as lib/make_machdep/posix_version.c) (machdeps/make_machdep/ptrdiff_t.c as lib/make_machdep/ptrdiff_t.c) + (machdeps/make_machdep/sanity_check.c as lib/make_machdep/sanity_check.c) + (machdeps/make_machdep/sig_atomic_t.c as lib/make_machdep/sig_atomic_t.c) (machdeps/make_machdep/sizeof_double.c as lib/make_machdep/sizeof_double.c) (machdeps/make_machdep/sizeof_float.c as lib/make_machdep/sizeof_float.c) (machdeps/make_machdep/sizeof_fun.c as lib/make_machdep/sizeof_fun.c) @@ -382,6 +396,17 @@ (machdeps/make_machdep/sizeof_short.c as lib/make_machdep/sizeof_short.c) (machdeps/make_machdep/sizeof_void.c as lib/make_machdep/sizeof_void.c) (machdeps/make_machdep/size_t.c as lib/make_machdep/size_t.c) + (machdeps/make_machdep/ssize_t.c as lib/make_machdep/ssize_t.c) + (machdeps/make_machdep/stdio_macros.c as lib/make_machdep/stdio_macros.c) + (machdeps/make_machdep/stdlib_macros.c as lib/make_machdep/stdlib_macros.c) + (machdeps/make_machdep/time_t.c as lib/make_machdep/time_t.c) + (machdeps/make_machdep/uint_fast16_t.c as lib/make_machdep/uint_fast16_t.c) + (machdeps/make_machdep/uint_fast32_t.c as lib/make_machdep/uint_fast32_t.c) + (machdeps/make_machdep/uint_fast64_t.c as lib/make_machdep/uint_fast64_t.c) + (machdeps/make_machdep/uint_fast8_t.c as lib/make_machdep/uint_fast8_t.c) + (machdeps/make_machdep/uintptr_t.c as lib/make_machdep/uintptr_t.c) (machdeps/make_machdep/wchar_t.c as lib/make_machdep/wchar_t.c) - (machdeps/make_machdep/make_machdep_common.h as lib/make_machdep/make_machdep_common.h) + (machdeps/make_machdep/weof.c as lib/make_machdep/weof.c) + (machdeps/make_machdep/wint_t.c as lib/make_machdep/wint_t.c) + (machdeps/make_machdep/wordsize.c as lib/make_machdep/wordsize.c) )) diff --git a/share/machdeps/machdep_avr_16.yaml b/share/machdeps/machdep_avr_16.yaml index f5ee3f6c8487f9c21f3de15a75d7255d4ff617d8..055d78e85c3d33563175e3c2c5f2e8d3c2508b8a 100644 --- a/share/machdeps/machdep_avr_16.yaml +++ b/share/machdeps/machdep_avr_16.yaml @@ -16,6 +16,7 @@ cpp_arch_flags: - -target - avr - -m16 +- -mmcu=atmega16 custom_defs: | #undef AVR #define AVR 1 @@ -33,6 +34,8 @@ custom_defs: | #define __ATOMIC_SEQ_CST 5 #undef __AVR #define __AVR 1 + #undef __AVR_ATmega16__ + #define __AVR_ATmega16__ 1 #undef __AVR__ #define __AVR__ 1 #undef __BIGGEST_ALIGNMENT__ @@ -645,6 +648,8 @@ custom_defs: | #define __clang_version__ "15.0.7 " #undef __clang_wide_literal_encoding__ #define __clang_wide_literal_encoding__ "UTF-16" + #undef __flash + #define __flash __attribute__((address_space(1))) #undef __llvm__ #define __llvm__ 1 eof: (-1) diff --git a/share/machdeps/machdep_avr_8.yaml b/share/machdeps/machdep_avr_8.yaml index 9a9268a4d5590425281b29da80561ab9d037b8cd..cbaeb67bbd3b9626e1cba28f416efded67c9cd79 100644 --- a/share/machdeps/machdep_avr_8.yaml +++ b/share/machdeps/machdep_avr_8.yaml @@ -15,6 +15,7 @@ compiler: clang cpp_arch_flags: - -target - avr +- -mmcu=atmega8 custom_defs: | #undef AVR #define AVR 1 @@ -32,6 +33,8 @@ custom_defs: | #define __ATOMIC_SEQ_CST 5 #undef __AVR #define __AVR 1 + #undef __AVR_ATmega8__ + #define __AVR_ATmega8__ 1 #undef __AVR__ #define __AVR__ 1 #undef __BIGGEST_ALIGNMENT__ @@ -644,6 +647,8 @@ custom_defs: | #define __clang_version__ "15.0.7 " #undef __clang_wide_literal_encoding__ #define __clang_wide_literal_encoding__ "UTF-16" + #undef __flash + #define __flash __attribute__((address_space(1))) #undef __llvm__ #define __llvm__ 1 eof: (-1) diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py index bd0b6cefa82eeebfdbf575326681d26122018c34..c6045ab856a81cc991fbda527d32ca5648914719 100755 --- a/share/machdeps/make_machdep/make_machdep.py +++ b/share/machdeps/make_machdep/make_machdep.py @@ -49,8 +49,6 @@ from yaml.representer import Representer my_path = Path(sys.argv[0]).parent -logging.basicConfig(format="%(levelname)s: %(message)s") - parser = argparse.ArgumentParser(prog="make_machdep") parser.add_argument("-v", "--verbose", action="store_true") parser.add_argument("-o", type=argparse.FileType("w"), dest="dest_file") @@ -61,6 +59,12 @@ parser.add_argument( help="option to pass to the compiler to obtain its version; default is --version", ) +parser.add_argument( + "--machdep-schema", + default="machdep-schema.yaml", + help="location of the schema file describing a machdep; default is 'machdep-schema.yaml'", +) + parser.add_argument( "--from-file", help="reads compiler and arch flags from existing yaml file. Use -i to update it in place", @@ -98,6 +102,11 @@ parser.add_argument( args, other_args = parser.parse_known_args() +if args.verbose: + logging.basicConfig(format="%(levelname)s: %(message)s", level=logging.INFO) +else: + logging.basicConfig(format="%(levelname)s: %(message)s") + if not args.compiler_flags: args.compiler_flags = ["-c"] @@ -106,8 +115,7 @@ if not args.cpp_arch_flags: def make_schema(): - schema_filename = my_path.parent / "machdep-schema.yaml" - with open(schema_filename, "r") as schema: + with open(args.machdep_schema, "r") as schema: return yaml.safe_load(schema) @@ -275,11 +283,9 @@ def find_value(name, typ, output): machdep[name] = value else: logging.warning( - f"cannot find value of field '{name}', using default value: '{default}'" + f"cannot find value of field '{name}', using default value: '{default}'\ncompiler output is:\n{output}" ) machdep[name] = default - if args.verbose: - print(f"compiler output is:{output}") else: logging.warning(f"unexpected symbol '{name}', ignoring") @@ -331,9 +337,9 @@ for f, typ in source_files: continue if typ == "macro": if proc.returncode != 0: - logging.warning(f"error in preprocessing value '{p}', some values won't be filled") - if args.verbose: - print(f"compiler output is:{proc.stderr.decode()}") + logging.warning( + f"error in preprocessing value '{p}', some values won't be filled\ncompiler output is:\n{proc.stderr.decode()}" + ) name = p.stem if name in machdep: machdep[name] = "" @@ -343,9 +349,9 @@ for f, typ in source_files: if typ == "macrolist": name = p.stem if proc.returncode != 0: - logging.warning(f"error in preprocessing value '{p}', some value might not be filled") - if args.verbose: - print(f"compiler output is:{proc.stderr.decode()}") + logging.warning( + f"error in preprocessing value '{p}', some values might not be filled\ncompiler output is:{proc.stderr.decode()}" + ) if name in machdep: machdep[name] = {} continue @@ -416,9 +422,7 @@ if proc.returncode == 0: lines += f"{line.strip()}\n" machdep["custom_defs"] = custom_defs(lines) else: - logging.warning("could not determine predefined macros") - if args.verbose: - print(f"compiler output is:{proc.stderr}") + logging.warning(f"could not determine predefined macros. compiler output is:\n{proc.stderr}") if args.from_file and args.in_place: machdep["machdep_name"] = Path(args.from_file).stem diff --git a/tests/fc_script/oracle/custom_machdep.yaml b/tests/fc_script/oracle/custom_machdep.yaml new file mode 100644 index 0000000000000000000000000000000000000000..24f472d19e21723c8f7bf328c8ff0a0bea41a373 --- /dev/null +++ b/tests/fc_script/oracle/custom_machdep.yaml @@ -0,0 +1,183 @@ +alignof_aligned: 16 +alignof_double: 8 +alignof_float: 4 +alignof_fun: 4 +alignof_int: 4 +alignof_long: 8 +alignof_longdouble: 16 +alignof_longlong: 8 +alignof_ptr: 8 +alignof_short: 2 +alignof_str: 1 +bufsiz: '8192' +char_is_unsigned: false +compiler: clang +cpp_arch_flags: + - --target=x86_64 +eof: (-1) +errno: + e2big: '7' + eacces: '13' + eaddrinuse: '98' + eaddrnotavail: '99' + eafnosupport: '97' + eagain: '11' + ealready: '114' + ebade: '52' + ebadf: '9' + ebadfd: '77' + ebadmsg: '74' + ebadr: '53' + ebadrqc: '56' + ebadslt: '57' + ebusy: '16' + ecanceled: '125' + echild: '10' + echrng: '44' + ecomm: '70' + econnaborted: '103' + econnrefused: '111' + econnreset: '104' + edeadlk: '35' + edeadlock: '35' + edestaddrreq: '89' + edom: '33' + edquot: '122' + eexist: '17' + efault: '14' + efbig: '27' + ehostdown: '112' + ehostunreach: '113' + eidrm: '43' + eilseq: '84' + einprogress: '115' + eintr: '4' + einval: '22' + eio: '5' + eisconn: '106' + eisdir: '21' + eisnam: '120' + ekeyexpired: '127' + ekeyrejected: '129' + ekeyrevoked: '128' + el2hlt: '51' + el2nsync: '45' + el3hlt: '46' + el3rst: '47' + elibacc: '79' + elibbad: '80' + elibexec: '83' + elibmax: '82' + elibscn: '81' + eloop: '40' + emediumtype: '124' + emfile: '24' + emlink: '31' + emsgsize: '90' + emultihop: '72' + enametoolong: '36' + enetdown: '100' + enetreset: '102' + enetunreach: '101' + enfile: '23' + enobufs: '105' + enodata: '61' + enodev: '19' + enoent: '2' + enoexec: '8' + enokey: '126' + enolck: '37' + enolink: '67' + enomedium: '123' + enomem: '12' + enomsg: '42' + enonet: '64' + enopkg: '65' + enoprotoopt: '92' + enospc: '28' + enosr: '63' + enostr: '60' + enosys: '38' + enotblk: '15' + enotconn: '107' + enotdir: '20' + enotempty: '39' + enotrecoverable: '131' + enotsock: '88' + enotsup: '95' + enotty: '25' + enotuniq: '76' + enxio: '6' + eopnotsupp: '95' + eoverflow: '75' + eownerdead: '130' + eperm: '1' + epfnosupport: '96' + epipe: '32' + eproto: '71' + eprotonosupport: '93' + eprototype: '91' + erange: '34' + eremchg: '78' + eremote: '66' + eremoteio: '121' + erestart: '85' + erofs: '30' + eshutdown: '108' + esocktnosupport: '94' + espipe: '29' + esrch: '3' + estale: '116' + estrpipe: '86' + etime: '62' + etimedout: '110' + etxtbsy: '26' + euclean: '117' + eunatch: '49' + eusers: '87' + ewouldblock: '11' + exdev: '18' + exfull: '54' +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 +int_fast8_t: signed char +intptr_t: long +l_tmpnam: '20' +little_endian: true +machdep_name: anonymous_machdep +mb_cur_max: ((size_t)16) +nsig: (64 + 1) +path_max: '4096' +posix_version: 200809L +ptrdiff_t: long +rand_max: '2147483647' +sig_atomic_t: int +size_t: unsigned long +sizeof_double: 8 +sizeof_float: 4 +sizeof_fun: 1 +sizeof_int: 4 +sizeof_long: 8 +sizeof_longdouble: 16 +sizeof_longlong: 8 +sizeof_ptr: 8 +sizeof_short: 2 +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 +uint_fast8_t: unsigned char +uintptr_t: unsigned long +wchar_t: int +weof: (0xffffffffu) +wint_t: int +wordsize: '64' diff --git a/tests/fc_script/oracle/find_fun1.res b/tests/fc_script/oracle/find_fun1.res index 58bf804e3c123e33f21c6761b63dcefa26e2e129..71eea9bdef1d36da92d821b392155e03e811c21e 100644 --- a/tests/fc_script/oracle/find_fun1.res +++ b/tests/fc_script/oracle/find_fun1.res @@ -1,4 +1,4 @@ -Looking for 'main2' inside 15 file(s)... +Looking for 'main2' inside 16 file(s)... Possible declarations for function 'main2' in the following file(s): for-find-fun.c Possible definitions for function 'main2' in the following file(s): diff --git a/tests/fc_script/oracle/find_fun2.res b/tests/fc_script/oracle/find_fun2.res index d868795ee4e11b8858e75185cfd91d68ea8a24e7..5c9b9b69b9d58907335997f8db1b440930ca63ef 100644 --- a/tests/fc_script/oracle/find_fun2.res +++ b/tests/fc_script/oracle/find_fun2.res @@ -1,4 +1,4 @@ -Looking for 'main3' inside 15 file(s)... +Looking for 'main3' inside 16 file(s)... Possible declarations for function 'main3' in the following file(s): for-find-fun2.c Possible definitions for function 'main3' in the following file(s): diff --git a/tests/fc_script/oracle/find_fun3.res b/tests/fc_script/oracle/find_fun3.res index 00f4bbc10eab9c20620426e670d9d0cf6b715762..67c26fc2681fd115eaca995ff472d4419c48248a 100644 --- a/tests/fc_script/oracle/find_fun3.res +++ b/tests/fc_script/oracle/find_fun3.res @@ -1,2 +1,2 @@ -Looking for 'false_positive' inside 15 file(s)... +Looking for 'false_positive' inside 16 file(s)... No declaration/definition found for function 'false_positive' diff --git a/tests/fc_script/oracle/make_machdep.err.log b/tests/fc_script/oracle/make_machdep.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/tests/fc_script/test_machdep.i b/tests/fc_script/test_machdep.i new file mode 100644 index 0000000000000000000000000000000000000000..923485dde8e59c0631db3e506d95a6c23cf4699b --- /dev/null +++ b/tests/fc_script/test_machdep.i @@ -0,0 +1,12 @@ +/* run.config + NOFRAMAC: Just test the generation of a custom machdep with the installed script. + COMMENT: No C code gets analyzed there. File is empty on purpose + COMMENT: be sure to keep the first EXECNOW: it ensures + COMMENT: that dune will copy the file regardless of the environment + COMMENT: so that other tests whose oracles depend on the number of file in + COMMENT: the directory will be stable. + EXECNOW: LOG empty.res touch empty.res + ENABLED_IF: (and %{bin-available:clang} %{bin-available:yq}) + FILTER: sed -e '/^version:/d' + EXECNOW: LOG custom_machdep.yaml LOG make_machdep.err.log PTESTS_TESTING=1 %{bin:frama-c-script} make-machdep --compiler clang --cpp-arch-flags='--target=x86_64' | yq -Y 'del(.version)|del(.custom_defs)' > custom_machdep.yaml 2> make_machdep.err.log +*/ diff --git a/tools/ptests/ptests.ml b/tools/ptests/ptests.ml index 6c8432958909130fa6008dfdc82d090f29ceb864..afe8a2c8e94690afd588450faf03723d2da514d6 100644 --- a/tools/ptests/ptests.ml +++ b/tools/ptests/ptests.ml @@ -1977,11 +1977,15 @@ let warn_if_not_enabled = let dune_cond_regexp = Str.regexp "^(\\(.*\\))" in let doublequote_regexp = Str.regexp "\"" in let dune_var_regexp = Str.regexp "%{" in + let paren_regexp = Str.regexp "[()]" in let dune_cond_item s = Str.global_replace dune_cond_regexp "\\1" s in let escaped_cond s = let s = Str.global_replace dune_var_regexp "\\%{" s in Str.global_replace doublequote_regexp "\\\"" s in + let safe_cond s = + Str.global_replace paren_regexp "\"\\0\"" s + in fun ~env ~suite fmt enabled_if -> if not (StringSet.is_empty enabled_if) then begin Format.fprintf fmt @@ -2000,7 +2004,7 @@ let warn_if_not_enabled = let pp_enabled fmt cond = let cond = dune_cond_item cond in Format.fprintf fmt " (echo \"- %s: \" %s \"\\n\")\n " - (escaped_cond cond) cond + (escaped_cond cond) (safe_cond cond) in let conds = StringSet.elements enabled_if in Format.fprintf fmt diff --git a/tools/ptests/wtests.ml b/tools/ptests/wtests.ml index 9d4d84f9e74d96532ac1f6bc62d9aebbd8aaab5d..6c68edae0becccf09ef34ad4a4bcba4f69a66901 100644 --- a/tools/ptests/wtests.ml +++ b/tools/ptests/wtests.ml @@ -211,7 +211,8 @@ let wrapper json test = let error = ret_code <> test.ret_code in if error || !verbosity > 0 then begin if test.out <> "" then print_file test.dir (if test.tmpout = "" then test.out else test.tmpout) ; - if test.err <> "" then print_file test.dir (if test.tmperr = "" then test.err else test.tmperr) + if test.err <> "" then print_file test.dir (if test.tmperr = "" then test.err else test.tmperr) ; + List.iter (print_file test.dir) test.log end; if error then begin Format.printf "%a: return code (%d) differs from the requested code (%d) for the command:%s@."