*Add a paragraph describing bounds declarations for integer-typed variables. These are needed when a pointer is cast to an integer that is then assigned to a variable. This brings the specification into agreement with the clang Checked C implementation, which already allows this. This address issue #79.
Also fix some typos in the interoperation section and clarify some wording.
Adjust the tag in the example to only be one-bit wide. There are some additional complications with handling multi-bit tags. See GitHub issue #89 for details. To avoid these complications, we just change the example to use a 1-bit tag.
Fix a bad LaTeX page break for an example by removing a line from an example, There was a single line on one page with the bad page break.
- Add a definition of structure type compatibility across compilation units. This addresses Github issue #74. This is mostly of theoretical interest because C compilers do not typically check compatibility of structure types across C compilation units.
- Update the text to match changes made to variable bounds declaration for typing rules and bounds-safe interface types.
- Be more precise with terminology, differentiating between member bounds and member bounds declarations.
This updates the checking of bounds declaration to handle lexically-hidden variables. This address issues GitHub issue #75. Block-scoped variables that hide other variables need to be renamed before checking. This change also fixes a few typos in that section.
This adds tests for:
- variables with unchecked pointer type or unchecked array type and bounds-safe interfaces.
- variables with checked pointer type or checked array and bounds declarations.
- locally-scoped variables that hide global variables.
- locally-scoped extern variable declaration.
For now, we require that bounds expressions be identically syntactically when they need to match. This will be generalized later.
The clang error message for bounds mismatches when functions were redeclared was "mismatched type", which was not helpful. We've updated the Checked C version of clang to produce better error messages for mismatched bound. This updates the error messages in the tests. Also rename some functions from to begin with f instead of fn.
This change adds tests of redeclarations of functions with bounds declarations. This matches a corresponding change for the Checked C clang implementation. The tests check that functions can be redeclared with identical bounds declarations on parameters and returns. They also check that error messages are produced when the bounds declarations are not identical. This change also checks redeclarations of functions with bounds-safe interfaces. For now, the bounds declaration must be syntactically identical modulo parameter names. Later this will be changed to require that the bounds declaration be provably semantically identical.
To further test redeclarations of functions, this change also adds header files that redeclare functions in the C standard library with bounds-safe interfaces, when the functions can have a bounds-safe interfaces. This exercise shows three things, two of which were known and one that is new:
- There needs to be type system support for null-terminated arrays.
- That there is not a way to specify a bounds-safe interface to variable argument functions.
- That bounds declaration may need refer to parameters in an enclosing parameter list (bsearch and qsort demonstrate the need for this). The Checked C clang implementation does not account for this.
This change also improves the testing of typechecking of bounds on parameters and return types, including bounds and returns of function types.
This change corresponds to an update to the Checked C clang implementation to do better checking of bounds declarations and bounds-safe inferface type annotations for function pointer types.
This change fixes errors in existing tests found by the improved checking:
- Fix an error in parsing\return_bounds.c where there is a count bounds expression used with a function return type of `int`.
- Fix errors in typechecking\interop_type_annotations.c where lack of parentheses led interface types being declared for the wrong return types.
For example, the annotation type declared here:
int (*g80)(int *, int *) : itype(ptr<int(int *, int *)>)`
is the interface type for the return value of `g80`, which has type `int', not the interface type for g80 as intended. Add parentheses to fix this issue:
int ((*g80)(int *, int *)) : itype(ptr<int(int *, int *)>);
The change also updates the existing error messages involving bounds declarations and return types because those error messages have changed.
It adds the following tests:
- More tests of function pointer parameters and returns with bounds declarations and bounds-safe interfaces.
- Tests for unnamed parameters with bounds declarations.
- Tests that bounds-safe interface types are not allowed for local variables.
This change reworks the bounds-safe interface section. It adds a description of bounds-safe interface types and brings the section up-to-date with the clang implementation. This addresses issue #60.
The text for the section needed to be revised substantially so that it accurately describes that programmers can use bounds declarations or bounds-safe interface types, depending on what needs to be described. While I was doing that, I improved the writing and organization of the section. I shortened up some descriptions. I moved sections on type checking and checking of bounds declarations that are primarily for language designers and compiler writers to the end of the section. I also added a description of the organization of the section.
This changes updates the Checked C specification to describe how function types are extended with bounds information. This addresses issue #69.
- It adds a section to Chapter 3 (bounds for variables) that describes how function types and function pointer types include bounds information. The section includes a description of how type compatibility changes for function types.
- It updates the rules for casts in Chapter 5 (interoperation) to include function pointers.
- It adds a section to bound-safe interfaces in Chapter 5 that describes how function types with bounds-safe interfaces are compatible with function types without bounds information. This is crucial for allowing redeclarations of existing library functions with bounds information.
For now, we have simple rules for function pointer casts. We require that bounds declarations on parameters and return values be syntactically identical (after canonicalization). We do not allow weaker preconditions or stronger post-conditions for function pointer casts, even though we could. This would make the system more complex and it is not clear that more general rules are needed in practice. Add a section to the design alternatives chapter that discusses this decision.
There are a few other changes folded into this change:
- Revamp the rules around lexical hiding of variables. We drop the prohibition on lexical hiding of variables used in bounds declarations. It could cause backward-compatibility issues and was unnecessarily restrictive. We now allow lexical hiding of variables used in bounds declarations. We point out that it may make it impossible to update other variables used in a bounds declaration. There may be no way to do updates that make the bounds declaration be valid.
- Simplify the static checking rules for C-style casts. The rules were fairly long and adding rules for function only made them even longer. I compensated for this by reworking the rules to be simpler and shorter.
- Shorten the motivation section for bounds-safe interfaces. The text was longer than it needed to be.
Update the title of Chapter 4 to be clearer. The terminology
"check bounds" is ambiguous and could be misconstrued to be about
runtime bounds checks. The chapter is really about checking bounds
declarations.
Update the title of "Extent of dataflow-sensitive bounds declarations"
to be "Extent of bounds declared at statements". The terminology "dataflow"
is specific to compilers, so avoid it.
Rearrange the order in which material is presented in Chapter 3 (bounds for variables) to flow more logically.
- Present the important concepts that programmers will need to know in earlier sections.
- Move the more advanced technical material to later sections. This includes additional requirements on bounds declarations that programmers may need to consult rarely . It also includes support for non-relatively aligned pointers and detailed technical descriptions of concepts such as flow-sensitive bounds declarations.
- Update the description of bundled blocks to be more succinct and direct. Discuss the somewhat esoteric differences between e1, e2 and e1; e2 in Checked C at the end of the section.
This change addresses issue #53. To avoid backward-compatibility problems when using the
Checked C extension with existing C programs, we are changing the keywords for the
extension to start with an underscore followed by a capital letter.
The updated keywords are:
_Array_ptr _Checked _Dynamic_check _Ptr _Span _Where _Unchecked
This change adds a description of these keywords to the specification. We use a header file
that provides all-lowercase versions of the keywords. The text and examples in the
specification continue to use the all-lowercase versions because that is the way extension is
intended to be used.
This change also clarifies that the syntax for bounds expressions uses specific identifiers,
not keywords. This reduces the number of new keywords that need to be introduced.
The places where the specific identifiers occur in bounds expressions are not places where
general-purpose identifiers can also appear. This means there is no need to turn the specific
identifiers into keywords to disambiguate a possible overlap during parsing. This technique
has been used in C++ and C# to avoid introducing new keywords for names that have special
meaning only in specific syntactic contexts.
Calls to no-prototype functions are not type checked according to the C Specification (Section 6.5.2.2 of the C11 specification). Because of this, the Checked C extension does not allow no-prototype functions to be redeclared to take or return checked types. The lack of type checking at calls enables checking of bounds to be bypassed. Section 5.5 of the Checked C extension specification describes the restrictions. In the terminology of the C Specification, no-prototype function types are incompatible with function types that take arguments or return values that have checked types, contain values with checked types embedded within them, or are recursively pointers to function types that take or return checked types or checked values.
This change adds feature tests that check that redeclarations of no-prototype functions to use checked types are not allowed. The tests are in typechecking/no_prototype_functions.c.
It also fixes accidental declarations in existing tests of no-prototype functions. All these functions actually take no arguments. In C, a prototype for a function that takes no arguments has to be declared with an argument list that is the `void` keyword. For example, `int f(void);` declares a function that takes no arguments and returns an integer.
Update the specification to add some draft rules for declarations of
functions without prototypes. These are C functions declared without their
arguments. Informally,
- In checked scopes, it is an error to declare or use functions without
prototypes.
- Outside of checked scopes, it is an error to pass a checked type or
return a checked type from a function without a prototype.
The change adds a new section to interoperation that contains examples
and detailed rules. The draft rules need to be reviewed with other people
working on Checked C.
The change removes functions without prototypes from the list of work
to be addressed in Chapter 10.2. It also updates the section on checked
scopes to say that functions without prototypes are not allowed there.
This change updates some examples with empty parameter lists to
use void to properly describe the empty parameter lists.
This change adds feature tests for type checking of bounds-safe interface type annotations. It matches Checked C pull request [https://github.com/Microsoft/checkedc-clang/pull/74](https://github.com/Microsoft/checkedc-clang/pull/74).
The are 4 groups of tests: tests for parameter types, tests for global variable types, tests for function returns, and tests for structure members. For each group of tests, there are tests for types that can't appear as bounds-safe interface types, types that can't have bounds-safe interface type annotation, tests of valid annotations, tests of annotations where the interface type and the declared type are mismatched (not compatible types when the checked property on pointer and array types is disregarded), and tests of annotations where the interface type loses checking relative to the declared type.
The tests are customized for each area of functionality. For example, for parameters, we need to test combinations of array types and pointer types. Array types that appear as types for parameters are automatically converted to pointer types, so there is a fairly large number of combinations possible. For function return, array types can't be returned, so we need to test that interface types are not array types. We don't need to worry about return types that are array types.
Return bounds declarations are only allowed for functions with return types that are integer or pointer types. The clang error messages for this situation suggested an array type as a possibility. Functions cannot return arrays, so we've updated the clang error message. Update the corresponding Checked C tests too.
Add tests of misplaced return bounds expressions in complex declarators.
The tests also check the resulting error messages from the clang Checked C
implementation. These tests are for Checked C clang repo issue 66.
This also fixes some cases where const type qualifiers were omitted in
bound-safe interface type annotations.
This change adds feature tests for implicit type conversions at bounds-safe interfaces. It includes three sets of tests, corresponding to each language construct that can have a bounds-safe interface: a set for parameters with bounds-safe interfaces, a set for non-locally scoped variables with bounds-safe interfaces, and a set for members with bounds-safe interfaces. These tests match corresponding compiler changes for Checked C clang repo issue 31.
For each set of tests, there are
- tests for assigning (or passing) checked pointers to unchecked pointers with bounds-safe interfaces (where the referent types match)
- tests for assigning or passing checked pointers to void * pointers with bounds-safe interfaces
- tests for passing checked void pointers to non void * pointers with bounds-safe interfaces. These tests are expected to cause errors.
- There are also tests for types involving type qualifiers, making sure that the qualifier restrictions are enforced (a pointer to non-const type can be assigned to a pointer to a const-type, but not the reverse).
There are additional tests for parameters with array types. During type checking, the array types are adjusted to be pointer types. For Checked C, the bounds-safe interface types are checked array types and they are adjusted during type checking to be checked pointer types. For multi-dimensional arrays, this ends up being a little subtle. The multi-dimensional array has a bounds-safe interface type that is a checked multi-dimensional array. The checkedness propagates to the nested array types.
When the checked multi-dimensional array type is adjusted to be a pointer, the result is a "checked pointer to a checked array type."
There are tests for both 1-dimensional and 2-dimensional array parameters. The 2-dimensional array parameter tests check the subtleties of multi-dimensional arrays. Each multi-dimensional argument is typed as a "checked pointer to a checked array type", so if the appropriate adjustments did not happen for the bounds-safe interface type for the parameter, a type mismatch would occur.
This change adds tests for parsing of bounds-safe interface type annotations. It matches a corresponding change for the checked-clang repo.
The type annotations are a generalization of the `int * x : ptr` annotation described in the specification. That annotation does not provide a way to represent information for pointers with multiple levels of indirection (`int **x` for example). Instead of just using `ptr`, we now allow a type annotation to be specified. The annotation has the form `type` `(` _type name_ `)`. For example, a variable declaration `int **x` could be annotated as `int ** x : type(_Ptr<_Ptr<int>>)`. This richer form allows us to represent bounds-safe interfaces where pointers are passed by reference, for example.
Bounds-safe interfaces are allowed for parameters, global variables, and members. This change adds tests for type annotations involving `_Ptr`, `_Array_ptr`, typedef'ed names, and types with type modifiers.
I updated some clang error messages to use the new type names `_Ptr` and `_Array_ptr` during the code review yesterday. This caused some of the tests to break. Update the tests..
We're updating the clang implementation so that Checked C keywords start with an underscore and a capital letter. This avoids conflicts with existing C identifiers.
The keyword change follows the rules in the C Standard: all identifiers beginning with an underscore followed by a capital letter or underscore are reserved for implementation use. This allows them to be used for language extensions without conflicting with existing identifiers. Of course, some programs do not follow the standard and use these identifiers.
This change adds a header file stdchecked.h that has macros that maps the existing non-prefix, lower case keywords to the new keywords. It updates the tests to include that header file.
Testing:
- Updated version of clang passes these new tests.
This change adds tests for type checking bounds expression of the form bounds(e1, e2). It tests both positive cases (that should type check) and negative cases (that should fail to type check). This change matches a corresponding change in the checkedc-clang repo. It addresses checkedc-clang repo issue 14.
It includes tests of cases such as using expressions whose types are given by typedef'ed type names, using an expression with an array type as a bound, and using pointers that point to the same object type but have different modifiers.
This change add tests for checking the type requirements of bounds declarations. It matches a corresponding compiler change in the checked-clang repo.
This commit include both positive tests (that are supposed to work) and negative tests that should fail with an error message. We have added the expected error message from the clang implementation for the negative tests, so that the tests can be used in the clang test infrastructure. This commit also fixes issues in existing tests that the checking uncovered.
This change adds feature tests that the dimensions of a multi-dimensional array are either all checked or unchecked. The Checked C spec requires this for multi-dimensional arrays. It removes feature tests where individual dimensions could be declared as unchecked using the `unchecked` keyword. These feature tests were for an experimental feature in the clang implementation of Checked C. We have decided to stick with the existing wording in the spec.
This change also adds tests for parenthesized array declarators. The checked property is supposed to propagate from the outer dimension of a multi-dimensional array to the inner dimension: `int a checked[10][10]` declares a checked array of checked arrays This propagation wasn't happening when the declarator for the outer dimension was parenthesized: `int (a checked[10])[10].`
- Clarify that the checked property of an array declarator is only propagated
to nested array declarators. It is not propagated to typedef bodies.
- It is an error if there is a mismatch in checked properties between an array
type and an element type that is an array type.
- Improve the organization and wording of the text for checked
multi-dimensional arrays.
This addresses issue #20 by expanding the implicit conversions for pointers to arrays. We now allow conversions from pointers to unchecked arrays to pointers to checked arrays. This is needed to support passing unchecked multi-dimensional arrays to functions that have checked array parameters.
This change adds a notion of assignment compatibility. Compatibility of types in C is similar to equality and is not directional. We need a directional conversion, where source and destination matter. Informally, we allow a type A to be converted to another type B if A and B are the same except that B has more checking.
I considered defining a recursive notion of assignment compatibility for referent types that are pointers, but decided not to do that now. It requires other changes to the specification that go beyond what is needed for issue #20, so I'm putting that work off.
I also reworked some of the examples for casts and conversions and added non-examples of code that will fail to check.
This finishes up addressing issue #11. When we switched to the terminology of
checked and unchecked pointers, there was feedback that we should be very
clear about what is being checked. Specifically, checked pointers check
bounds, but do not check memory lifetime. This adds a paragraph to the
description of checked pointers making to clear that memory lifetime is
not checked.
This change adds feature tests for parsing member bounds. This accompanies pull request 23 for the checked-clang repo. It include tests for parsing member bounds on structures and unions.
This change adds tests for parsing return bounds expressions in function
declarators and function types.
- The tests for function declarators that return array_ptr types are
straightforward. array_ptr types avoid the problems of the
infix C type declarator syntax, at least for pointer types.
- There are additional tests for parsing return bounds expressions for
more complicated types, such as pointers to function types, function
types that return pointers to function types, and function declarations
that return pointers to function types.
- There are variants of these additional tests for unchecked pointer types
with bounds declared for them. The interoperation support in Checked C
may lead to these types of bounds declarations. The tests cover return
bounds expressions for unchecked pointer types to function types and
so on.
- There are tests for both function declarations and function definitions.
- Also added tests of parsing bounds expressions with omitted arguments.
This change adds tests for parsing return bounds expressions in function
declarators and function types.
- The tests for function declarators that return array_ptr types are
straightforward. array_ptr types avoid the problems of the
infix C type declarator syntax, at least for pointer types.
- There are additional tests for parsing return bounds expressions for
more complicated types, such as pointers to function types, function types
that return pointers to function types, and function declarations that return
pointers to function types.
- There are variants of these tests for unchecked pointer types to
function types and so on. These may arise from the interoperation support
in Checked C.
- Also added tests parsing bounds and count expressions with omitted arguments.
This change adds:
- Feature tests for parsing variable declarations with bounds
declarations. Most of the tests are for local variable declarations,
with the assumption that parsing of bounds declarations themselves will
be similar for variables with different linkage and storage classes.
The tests also include tests for the other storage classes and linkage
combinations that C allows.
- Feature tests for parsing function pointers where there are bounds on
function parameters.
It also moves files to subdirectories so that tests will be easier to find.
The subdirectories are named after the functionality that is being tested
(parsing and typechecking, so far). With the prior naming scheme,
functionality was included at the end of the file name, making it harder to find
tests.
Bounds expressions for parameters can use parameters variables declared
at any point in the parameter list. This means that bounds expressions must
be checked in a scope that contains all the parameters for the
parameter list.
- This change adds tests for that, by having bounds expressions for parameters use parameters declared later in the parameter list.
- It also adds tests that subexpressions of bounds expressions can be parenthesized expressions.
- Finally, this change adds tests that have misspelled contextual keywords in bounds expressions. These expressions should be rejected by a compiler. These tests can be used also to test error messages and error recovery in compilers for that situation.
This change adds feature tests for parsing bounds expressions in function parameter lists. These tests are for the checkedc-clang pull request "Extend clang IR with bounds expressions and parse bounds expressions for parameters"
Add tests for parsing and typechecking new checked types.
This adds feature tests for parsing and type checking the new checked types. The test code illustrates how the new types can and cannot be used. Tests that are supposed to fail are annotated with part of an expected error or warning message that clang/LLVM will produce. Code that is not annotated with an error or warning message is expected to pass. clang produces detailed error messages, so to avoid cluttering the test code, we usually only include part of the error or warning message.
Fix lost highlighting of code and fix typos.
The addresses issue #3, where highlighting of text was lost when the Word document was converted to LaTex This adds back the missing highlighting to the LaTex document. This also fixes some typos.
The highlighting was used in code examples. The code examples used the verbatim environment. To be able to highlight the code, we need to be able to use LaTex commands, which are not allowed by the verbatim environment. Switching to the alltt environment does not work because the LaTex highlighting package that we are using does not work well with alltt. The solution is to just switch to teletype font and handle line breaking and spacing manually where necessary. This works well with the highlighting package.