checkedc/checkedc-clang CheckedC-Clang-12.0.1-rel2 on GitHub

Summary

This is a release build of the Checked C Clang compiler for Windows 32-bit and 64-bit platforms. It is for use by developers who want to experiment with the Checked C language extensions to guarantee the type safety of their C code. It is based on the Checked C specification version 0.9, which is also one of the released artifacts.

Release Date and Tag

3rd August 2021 CheckedC-Clang-12.0.1-rel2

Installation Notes

Clang expects an existing C/C++ compiler before running the installer. If installing on a fresh machine, first install the C/C++ compiler. We recommend Visual Studio 2019, which has a free Community version available. Use Visual Studio 2019's installer to ensure a C/C++ compiler and runtime are present before installing Checked C Clang.

The binaries are installers for 32-bit and 64-bit Windows versions of the compiler
The compiler will be installed in a separate directory from your existing Clang install. If you are also using the production version of Clang, do not add the Checked C version to your path.

Using the Compiler

See the Checked C Clang users manual for directions on how to use the compiler.

There are now two ways to use the Checked C Clang compiler in Visual Studio. The LLVM project has created a Visual Studio extension. You can use a property page for your project to directly choose the Checked C Clang compiler binary.

Visual Studio 2019 also now directly supports Clang/LLVM. This blog post describes the support for CMake projects. This blog post describes support for MSBuild projects. If you installed the Checked C Clang compiler and added it to your PATH variable, Visual Studio should directly pick it up. Otherwise, you can follow the directions to use a custom installation of Clang.

Change Notes

Core features

PR #1136: Upgrade to LLVM/Clang 12.
PR #1127: Invertibility for unchecked pointers. For example, in a statement p = p + 1, the inverse of an unchecked pointer p is p - 1.

PR #1128: Simple normalizations for +1/-1 bounds scenarios. The bounds checker is able to validate bounds in examples such as:

void f(_Nt_array_ptr<char> p : count(len), unsigned int len) {
  if (*(p + len)) {
    // The inferred bounds of p are bounds(p, (p + (len - 1)) + 1).
    // The bounds checker recognizes that these are equivalent to
    // the declared bounds of bounds(p, p + len).
    ++len;
  }
}

PR #1117: Handle incomplete types in BaseRange. If p1 and p2 have the same incomplete type, and c1 and c2 are constants, and p1 is equal to p2, then bounds(p1, p1 + c1) implies bounds(p2, p2 + c2) if and only if c1 >= c2.

Bounds checking for member expressions

The static checking for bounds declarations has been extended to check the bounds of pointers stored in struct members. For example, consider the following sample program involving variables:

void f(_Array_ptr<int> p : count(len), // note: (expanded) declared bounds are 'bounds(p, p + len)'
       _Array_ptr<int> q : bounds(unknown),
       unsigned int len) {
  // warning: cannot prove declared bounds for 'p' are valid after increment
  // note: (expanded) inferred bounds are 'bounds(p, p + len - 1U)'
  ++len;

  // error: inferred bounds for 'p' are unknown after assignment
  // note: assigned expression 'q' with unknown bounds to 'p'
  p = q;

  // no errors or warnings
  // inferred bounds of p after the statement are bounds(any)
  len = 1, p = 0;
}

The bounds checker exhibits similar behavior in an analogous program involving struct members:

struct S {
  _Array_ptr<int> p : count(len); // note: (expanded) declared bounds are 'bounds(s.p, s.p + len)'
  _Array_ptr<int> q : bounds(unknown);
  unsigned int len;
};

void f(struct S s) {
  // warning: cannot prove declared bounds for 's.p' are valid after increment
  // note: (expanded) inferred bounds are 'bounds(s.p, s.p + s.len - 1U)'
  ++s.len;

  // error: inferred bounds for 's.p' are unknown after assignment
  // note: assigned expression 's.q' with unknown bounds to 's.p'
  s.p = s.q;

  // no errors or warnings
  // inferred bounds of s.p are the statement are bounds(any)
  s.len = 1, s.p = 0;
}

PR #1122: Support bounds widening of null-terminated arrays in presence of Where clauses.

We have added support to widen the bounds of a null-terminated array in case its bounds are redeclared using a Where clause. This enables us to widen the bounds of a null-terminated array when its length is obtained using a call to strlen.

void foo(_Nt_array_ptr<char> p : count(n), unsigned n) {
  if (*(p + n)) { // bounds of p widened to bounds(p, p + n + 1)
    char x = *(p + n + 1); //valid access
  }

  int len = strlen(p) _Where p : bounds(p, p + len); // bounds of p redeclared to bounds(p, p + len)

  if (*(p + len)) { // bounds of p widened to bounds(p, p + len + 1)
    char x = *(p + len + 1); // valid access
  }
}

PR #1137: Use invertibility to support bounds widening of null-terminated arrays inside loops.

We have improved support to widen the bounds of a null-terminated array when the elements of the null-terminated array are iterated in a loop.

void foo(_Nt_array_ptr<char> p : count(len), unsigned len) {
  while (*(p + len)) { // bounds of p widened to bounds(p, p + len + 1)
    if (*(p + len + 1)) { // bounds of p widened to bounds(p, p + len + 2)
      len++; // bounds of p adjusted to bounds(p, p + len - 1 + 2)
      char x = *(p + len + 1); // valid access
    }
  }
}

Where clauses can be used to specify program invariants and pre/post conditions. In this release we have added the support for parsing Where clauses in Checked C as part of the ongoing design and implementation of the complete support for Where clauses.

We have added support to parse Where clauses on:

Expression statements

int a;
a = foo() _Where a > 0 _And a < 10;

Variable declarations
```
int a = b _Where a > 0 _And a < 10;
```

Parameter declarations

void foo(int a _Where a > 0, int b, int c _Where c < 0);
void bar(_Nt_array_ptr<char> p _Where p: bounds(p, p + len), unsigned len);
void baz(int *p : itype(_Ptr<int>) _Where p != 0);

Null statements

void foo(_Nt_array_ptr<char> p, unsigned len) {
  _Where p : bounds(p, p + len);
  ...
}

Bug fixes

Issue #974: Wrong error from #903 when passing _Assume_bounds_cast directly to function with itype (fixed by PR #978).
Issue #1084: Crash while compilation (fixed by PR #1090).
Issue #1120: An nt_checked array with an empty initializer list should be an error (fixed by PR #1121).

Extension Features Implemented

See the implementation roadmap and status page. Some runtime checks and some static checking is not implemented yet.

checkedc/checkedc-clang CheckedC-Clang-12.0.1-rel2 2021-08-03 Release of the Checked C Clang compiler on GitHub