Skip to content

Create stand-alone tool for checking Checked C programs compiled with regular C compilers.  #498

@dtarditi

Description

@dtarditi

People interested in Checked C may not be willing to switch to the Checked C clang compiler.

  • They may be working on an existing project that does not use clang.
  • They may be compiling for a computer architecture not supported by clang, such as a specialized embedded processor.
  • They may not want to take a critical dependency on a research compiler or a non-standard version of clang.

For this scenario, we would like to create a "Checked C Static Checker" (name suggestions are welcome). This tool will check that no runtime checks are needed to enforce Checked C semantics (that is, all checks that would be inserted by the Checked C compiler are redundant to existing checks in the programs).

Programmers could then use this checker to check programs written using the erasable Checked C syntax. For their production compiler, the syntax would automatically be erased.

One question to address: can we identify some people who will use Checked C if such a tool exists? One concern is how faithfully the tool models the semantics of C as implemented by the production compiler they use. We will base this tool on the current Checked C clang implementation. At the very least, we need to make primitive type sizes line up and to look at known ambiguities in the C language specification. It will be good to work through those issues with a a concrete production compiler in mind.

UEFI developers are a good target for this tool. They primarily use GCC to compile UEFI, although the code also compiles with clang. Clang matches GCC's C semantics well. This will simplify the initial implementation of the tool.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions