Add support for the CompCert C Compiler

* Add preliminary support for the CompCert C Compiler

The intention is to use this with the picolibc, so some GCC flags are
automatically filtered. Since CompCert uses GCC is for linking, those
GCC-linker flags which are used by picolibc, are automatically prefixed
with '-WUl', so that they're passed to GCC.

Squashed commit of the following:

commit 4e0ad66dca9de301d2e41e74aea4142afbd1da7d
Author: Sebastian Meyer <meyer@absint.com>
Date:   Mon Aug 31 14:20:39 2020 +0200

    remove '-fall' from default arguments, also filter -ftls-model=.*

commit 41afa3ccc62ae72824eb319cb8b34b7e6693cb67
Author: Sebastian Meyer <meyer@absint.com>
Date:   Mon Aug 31 14:13:55 2020 +0200

    use regex for filtering ccomp args

commit d68d242d0ad22f8bf53923ce849da9b86b696a75
Author: Sebastian Meyer <meyer@absint.com>
Date:   Mon Aug 31 13:54:36 2020 +0200

    filter some gcc arguments

commit 982a01756266bddbbd211c54e8dbfa2f43dec38f
Author: Sebastian Meyer <meyer@absint.com>
Date:   Fri Aug 28 15:03:14 2020 +0200

    fix ccomp meson configuration

commit dce0bea00b1caa094b1ed0c6c77cf6c12f0f58d9
Author: Sebastian Meyer <meyer@absint.com>
Date:   Thu Aug 27 13:02:19 2020 +0200

    add CompCert to meson (does not fully work, yet)

* remove unused import and s/cls/self/

fixes the two obvious LGTM warnings

* CompCert: Do not ignore unsupported GCC flags

Some are safe to ignore, however, as per
https://github.com/mesonbuild/meson/pull/7674, they should not be
ignored by meson itself. Instead the meson.build should take care to
select only those which are actually supported by the compiler.

* remove unused variable

* Only add arguments once.

* Apply suggestions from code review

Co-authored-by: Dylan Baker <dylan@pnwbakers.com>

* Remove erroneous ' ' from '-o {}'.format()

As noticed by @dcbaker

* added release note snippet for compcert

* properly split parameters

As suggested by @dcbaker, these parameters should be properly split into multiple strings.

Co-authored-by: Dylan Baker <dylan@pnwbakers.com>

* Update add_compcert_compiler.md

Added a sentence about the state of the implementation (experimental); use proper markdown

* properly separate arguments

Co-authored-by: Dylan Baker <dylan@pnwbakers.com>

cross/ccomp-armv7a.txt

@@ -0,0 +1,13 @@
+[binaries]
+c = 'ccomp'
+ar = 'ccomp'
+strip = 'strip'
+
+[built-in options]
+c_args      = ['-target', 'armv7a-eabi', '-fall']
+
+[host_machine]
+system = 'bare metal'      # Update with your system name - bare metal/OS.
+cpu_family = 'arm'
+cpu = 'Cortex-A9'
+endian = 'little'

docs/markdown/Reference-tables.md

@@ -10,6 +10,7 @@ These are return values of the `get_id` (Compiler family) and
 | arm       | ARM compiler                     |                 |
 | armclang  | ARMCLANG compiler                |                 |
 | c2000     | Texas Instruments C2000 compiler |                 |
+| ccomp     | The CompCert formally-verified C compiler |        |
 | ccrx      | Renesas RX Family C/C++ compiler |                 |
 | clang     | The Clang compiler               | gcc             |
 | clang-cl  | The Clang compiler (MSVC compatible driver) | msvc |
@@ -56,6 +57,7 @@ These are return values of the `get_linker_id` method in a compiler object.
 | armlink    | The ARM linker (arm and armclang compilers) |
 | pgi        | Portland/Nvidia PGI                         |
 | nvlink     | Nvidia Linker used with cuda                |
+| ccomp      | CompCert used as the linker driver          |
 
 For languages that don't have separate dynamic linkers such as C# and Java, the
 `get_linker_id` will return the compiler name.

docs/markdown/snippets/add_compcert_compiler.md

@@ -0,0 +1,3 @@
+## Added CompCert C compiler
+
+Added experimental support for the [CompCert formally-verified C compiler](https://github.com/AbsInt/CompCert). The current state of the implementation is good enough to build the [picolibc project](https://github.com/picolibc/picolibc) with CompCert, but might still need additional adjustments for other projects.

mesonbuild/compilers/__init__.py

@@ -97,6 +97,7 @@ __all__ = [
     'CcrxCCompiler',
     'CcrxCPPCompiler',
     'Xc16CCompiler',
+    'CompCertCCompiler',
     'C2000CCompiler',
     'C2000CPPCompiler',
     'SunFortranCompiler',
@@ -145,6 +146,7 @@ from .c import (
     PGICCompiler,
     CcrxCCompiler,
     Xc16CCompiler,
+    CompCertCCompiler,
     C2000CCompiler,
     VisualStudioCCompiler,
 )

mesonbuild/compilers/c.py

@@ -22,6 +22,7 @@ from .c_function_attributes import C_FUNC_ATTRIBUTES
 from .mixins.clike import CLikeCompiler
 from .mixins.ccrx import CcrxCompiler
 from .mixins.xc16 import Xc16Compiler
+from .mixins.compcert import CompCertCompiler
 from .mixins.c2000 import C2000Compiler
 from .mixins.arm import ArmCompiler, ArmclangCompiler
 from .mixins.visualstudio import MSVCCompiler, ClangClCompiler
@@ -554,6 +555,36 @@ class Xc16CCompiler(Xc16Compiler, CCompiler):
             path = '.'
         return ['-I' + path]
 
+class CompCertCCompiler(CompCertCompiler, CCompiler):
+    def __init__(self, exelist, version, for_machine: MachineChoice,
+                 is_cross, info: 'MachineInfo', exe_wrapper=None, **kwargs):
+        CCompiler.__init__(self, exelist, version, for_machine, is_cross,
+                           info, exe_wrapper, **kwargs)
+        CompCertCompiler.__init__(self)
+
+    def get_options(self):
+        opts = CCompiler.get_options(self)
+        opts.update({'c_std': coredata.UserComboOption('C language standard to use',
+                                                       ['none', 'c89', 'c99'],
+                                                       'none')})
+        return opts
+
+    def get_option_compile_args(self, options):
+        return []
+
+    def get_no_optimization_args(self):
+        return ['-O0']
+
+    def get_output_args(self, target):
+        return ['-o{}'.format(target)]
+
+    def get_werror_args(self):
+        return ['-Werror']
+
+    def get_include_args(self, path, is_system):
+        if path == '':
+            path = '.'
+        return ['-I' + path]
 
 class C2000CCompiler(C2000Compiler, CCompiler):
     def __init__(self, exelist, version, for_machine: MachineChoice,

mesonbuild/compilers/mixins/compcert.py

@@ -0,0 +1,127 @@
+# Copyright 2012-2019 The Meson development team
+
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+
+#     http://www.apache.org/licenses/LICENSE-2.0
+
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+"""Representations specific to the CompCert C compiler family."""
+
+import os
+import re
+import typing as T
+
+if T.TYPE_CHECKING:
+    from ...environment import Environment
+
+ccomp_buildtype_args = {
+    'plain': [''],
+    'debug': ['-O0', '-g'],
+    'debugoptimized': ['-O0', '-g'],
+    'release': ['-03'],
+    'minsize': ['-Os'],
+    'custom': ['-Obranchless'],
+}  # type: T.Dict[str, T.List[str]]
+
+ccomp_optimization_args = {
+    '0': ['-O0'],
+    'g': ['-O0'],
+    '1': ['-O1'],
+    '2': ['-O2'],
+    '3': ['-O3'],
+    's': ['-Os']
+}  # type: T.Dict[str, T.List[str]]
+
+ccomp_debug_args = {
+    False: [],
+    True: ['-g']
+}  # type: T.Dict[bool, T.List[str]]
+
+# As of CompCert 20.04, these arguments should be passed to the underlying gcc linker (via -WUl,<arg>)
+# There are probably (many) more, but these are those used by picolibc
+ccomp_args_to_wul = [
+        r"^-ffreestanding$",
+        r"^-r$"
+] # type: T.List[str]
+
+class CompCertCompiler:
+    def __init__(self) -> None:
+        self.id = 'ccomp'
+        # Assembly
+        self.can_compile_suffixes.add('s')
+        default_warn_args = []  # type: T.List[str]
+        self.warn_args = {'0': [],
+                          '1': default_warn_args,
+                          '2': default_warn_args + [],
+                          '3': default_warn_args + []}
+
+    def get_always_args(self) -> T.List[str]:
+        return []
+
+    def get_pic_args(self) -> T.List[str]:
+        # As of now, CompCert does not support PIC
+        return []
+
+    def get_buildtype_args(self, buildtype: str) -> T.List[str]:
+        return ccomp_buildtype_args[buildtype]
+
+    def get_pch_suffix(self) -> str:
+        return 'pch'
+
+    def get_pch_use_args(self, pch_dir: str, header: str) -> T.List[str]:
+        return []
+
+    def unix_args_to_native(self, args):
+        "Always returns a copy that can be independently mutated"
+        patched_args = []
+        for arg in args:
+            added = 0
+            for ptrn in ccomp_args_to_wul:
+                if re.match(ptrn, arg):
+                    patched_args.append('-WUl,' + arg)
+                    added = 1
+            if not added:
+                patched_args.append(arg)
+        return patched_args
+
+    # Override CCompiler.get_dependency_gen_args
+    def get_dependency_gen_args(self, outtarget: str, outfile: str) -> T.List[str]:
+        return []
+
+    def thread_flags(self, env: 'Environment') -> T.List[str]:
+        return []
+
+    def get_preprocess_only_args(self) -> T.List[str]:
+        return ['-E']
+
+    def get_compile_only_args(self) -> T.List[str]:
+        return ['-c']
+
+    def get_coverage_args(self) -> T.List[str]:
+        return []
+
+    def get_no_stdinc_args(self) -> T.List[str]:
+        return ['-nostdinc']
+
+    def get_no_stdlib_link_args(self) -> T.List[str]:
+        return ['-nostdlib']
+
+    def get_optimization_args(self, optimization_level: str) -> T.List[str]:
+        return ccomp_optimization_args[optimization_level]
+
+    def get_debug_args(self, is_debug: bool) -> T.List[str]:
+        return ccomp_debug_args[is_debug]
+
+    def compute_parameters_with_absolute_paths(self, parameter_list: T.List[str], build_dir: str) -> T.List[str]:
+        for idx, i in enumerate(parameter_list):
+            if i[:9] == '-I':
+                parameter_list[idx] = i[:9] + os.path.normpath(os.path.join(build_dir, i[9:]))
+
+        return parameter_list

mesonbuild/environment.py

@@ -19,7 +19,7 @@ import typing as T
 import collections
 
 from . import coredata
-from .linkers import ArLinker, ArmarLinker, VisualStudioLinker, DLinker, CcrxLinker, Xc16Linker, C2000Linker, IntelVisualStudioLinker, AIXArLinker
+from .linkers import ArLinker, ArmarLinker, VisualStudioLinker, DLinker, CcrxLinker, Xc16Linker, CompCertLinker, C2000Linker, IntelVisualStudioLinker, AIXArLinker
 from . import mesonlib
 from .mesonlib import (
     MesonException, EnvironmentException, MachineChoice, Popen_safe,
@@ -49,6 +49,7 @@ from .linkers import (
     ArmDynamicLinker,
     CcrxDynamicLinker,
     Xc16DynamicLinker,
+    CompCertDynamicLinker,
     C2000DynamicLinker,
     ClangClDynamicLinker,
     DynamicLinker,
@@ -120,6 +121,7 @@ from .compilers import (
     CcrxCCompiler,
     CcrxCPPCompiler,
     Xc16CCompiler,
+    CompCertCCompiler,
     C2000CCompiler,
     C2000CPPCompiler,
     SunFortranCompiler,
@@ -1155,6 +1157,8 @@ class Environment:
                 arg = '-v'
             elif 'xc16' in compiler_name:
                 arg = '--version'
+            elif 'ccomp' in compiler_name:
+                arg = '-version'
             elif 'cl2000' in compiler_name:
                 arg = '-version'
             elif compiler_name in {'icl', 'icl.exe'}:
@@ -1365,6 +1369,14 @@ class Environment:
                     ccache + compiler, version, for_machine, is_cross, info,
                     exe_wrap, full_version=full_version, linker=linker)
 
+            if 'CompCert' in out:
+                cls = CompCertCCompiler
+                self.coredata.add_lang_args(cls.language, cls, for_machine, self)
+                linker = CompCertDynamicLinker(for_machine, version=version)
+                return cls(
+                    ccache + compiler, version, for_machine, is_cross, info,
+                    exe_wrap, full_version=full_version, linker=linker)
+
             if 'TMS320C2000 C/C++' in out:
                 cls = C2000CCompiler if lang == 'c' else C2000CPPCompiler
                 self.coredata.add_lang_args(cls.language, cls, for_machine, self)
@@ -1373,6 +1385,7 @@ class Environment:
                     ccache + compiler, version, for_machine, is_cross, info,
                     exe_wrap, full_version=full_version, linker=linker)
 
+
         self._handle_exceptions(popen_exceptions, compilers)
 
     def detect_c_compiler(self, for_machine):
@@ -1965,6 +1978,8 @@ class Environment:
                 return Xc16Linker(linker)
             if out.startswith('TMS320C2000') and ('ar2000' in linker or 'ar2000.exe' in linker):
                 return C2000Linker(linker)
+            if out.startswith('The CompCert'):
+                return CompCertLinker(linker)
             if p.returncode == 0:
                 return ArLinker(linker)
             if p.returncode == 1 and err.startswith('usage'): # OSX

mesonbuild/linkers.py

@@ -230,6 +230,18 @@ class Xc16Linker(StaticLinker):
     def get_linker_always_args(self) -> T.List[str]:
         return ['rcs']
 
+class CompCertLinker(StaticLinker):
+
+    def __init__(self, exelist: T.List[str]):
+        super().__init__(exelist)
+        self.id = 'ccomp'
+
+    def can_linker_accept_rsp(self) -> bool:
+        return False
+
+    def get_output_args(self, target: str) -> T.List[str]:
+        return ['-o{}'.format(target)]
+
 
 class C2000Linker(StaticLinker):
 
@@ -869,6 +881,47 @@ class Xc16DynamicLinker(DynamicLinker):
                          install_rpath: str) -> T.Tuple[T.List[str], T.Set[bytes]]:
         return ([], set())
 
+class CompCertDynamicLinker(DynamicLinker):
+
+    """Linker for CompCert C compiler."""
+
+    def __init__(self, for_machine: mesonlib.MachineChoice,
+                 *, version: str = 'unknown version'):
+        super().__init__('ccomp', ['ccomp'], for_machine, '', [],
+                         version=version)
+
+    def get_link_whole_for(self, args: T.List[str]) -> T.List[str]:
+        if not args:
+            return args
+        return self._apply_prefix('-WUl,--start-group') + args + self._apply_prefix('-WUl,--end-group')
+
+    def get_accepts_rsp(self) -> bool:
+        return False
+
+    def get_lib_prefix(self) -> str:
+        return '-l'
+
+    def get_std_shared_lib_args(self) -> T.List[str]:
+        return []
+
+    def get_output_args(self, outputname: str) -> T.List[str]:
+        return ['-o{}'.format(outputname)]
+
+    def get_search_args(self, dirname: str) -> T.List[str]:
+        return ['-L{}'.format(outputname)]
+
+    def get_allow_undefined_args(self) -> T.List[str]:
+        return []
+
+    def get_soname_args(self, env: 'Environment', prefix: str, shlib_name: str,
+                        suffix: str, soversion: str, darwin_versions: T.Tuple[str, str],
+                        is_shared_module: bool) -> T.List[str]:
+        raise mesonlib.MesonException('{} does not support shared libraries.'.format(self.id))
+
+    def build_rpath_args(self, env: 'Environment', build_dir: str, from_dir: str,
+                         rpath_paths: str, build_rpath: str,
+                         install_rpath: str) -> T.Tuple[T.List[str], T.Set[bytes]]:
+        return ([], set())
 
 class C2000DynamicLinker(DynamicLinker):