Language Support

The BRiCk program logic is aimed to be a formalization of pragmatic C++. Its feature set is guided by the requirements of low-level program verification and also some pragmatic considerations.

Limitations of BRiCk

BRiCk does not cover the full feature set of C++. Some features that are explicitly not supported are:

  • The BRiCk program logic assumes that the abstract syntax tree is well-typed and uses this assumption to avoid performing type checking within the semantics. If you are using cpp2v to generate the AST, then Clang will ensure that the syntax tree is well typed.

  • BRiCk is based on the Clang front-end IR. We believe that this is a reasonable proxy for source-level C++.

  • Exceptions. In addition to not supporting throw and try, BRiCk additionally assumes that function calls do not throw exceptions.

  • virtual inheritance.

  • Floating point values and operations

  • Labeled statements and goto are not supported.

  • switch statements have restricted semantics when mixed with control flow.

  • Bitfields

  • [packed] data structures.

While not supported right now, some features are on our road map.

  • Translation unit initialization (i.e. initialization of globals)

  • template code can only be reasoned about after instantiating it to specific arguments.

  • Weak memory accesses. BRiCk currently requires that all atomic accesses are sequentially consistent 1.

  • Member pointers (and associated operators, i.e. .* and ->*)

  • Member functions, constructors, and destructors are modeled by translating them to functions. This is unsound but requires reinterpret_cast to exploit.

  • The semantics currently ignores volatile qualifiers.

  • We rely on the semantics of defaulted functions (e.g. default constructors, assignment operators, etc) generated by Clang. If your compiler generates different code (but still semantically correct code), this may invalidate your proof. We recommend using Clang with exactly the same build parameters as those used in your build for the best compatibility.

  • Transparent replacement.

  • Verification of variadic functions (e.g. printf) is not supported, but calling variadic functions is supported.

Deviations from the Standard

In certain instances, BRiCk’s semantics deviates from the C++ standard.

  • BRiCk’s semantics do not currently permit “pointer zapping”. See Assumptions beyond the standard.

  • BRiCk uses Tnum sz sgn to represent all integer types rather than the standard types char, short, int, long, long long.

Known Issues

There are several known issues with the current BRiCk semantics; we are working to support these.

  • BRiCk semantics does not currently support flexible array members. These are not officially supported by the standard but are frequently used in C++ programs.

Extensions to the Standard

BRiCk also extends the C++ standard in limited ways to make low-level program verification possible. For example, inter-operation with assembly (see Assembly Interoperation), sharing data across address spaces, etc. We believe that our extensions are conservative and characterize the way that low-level programmers rely on compilers to work.

1

We plan to support weak memory C++ in the future based on other work in Iris.