Skip to content

Merge from Microsoft 2021-01-27 #407

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 9 commits into from
Feb 13, 2021

Conversation

mattmccutchen-cci
Copy link
Member

Merging from Microsoft in preparation for submitting an omnibus PR. (When this PR is ready, I will normal-merge it from the command line, not squash-merge it in the GitHub UI. I'm filing a PR so we can discuss the test failures; I may perform subsequent merges without filing a PR.)

It seems Microsoft made bounds checking stricter (checkedc#903) and this is causing three of our regression tests to fail. Is anyone familiar with what to do about this? It would probably take a while for me to figure it out on my own.

mattmccutchen-cci and others added 6 commits December 30, 2020 09:35
…heckedc#962)

277d84a.

We first submitted them in PR checkedc#837, but Mandeep noticed
(checkedc#837 (review))
and the unintended changes were removed from that PR in
74bfcaf.  However, when the squash of
PR checkedc#837 was merged with the original commits in
cfc998e, the unintended changes were
incorrectly retained.  They got submitted again in the next 3C PR
(checkedc#891), and no one noticed that time.
…lared bounds (checkedc#903)

* Target error message at assignments

* Target subexpressions to blame on error messages for unknown inferred bounds

* Update tests to reflect fine-grained error messages

* Update comments

* Remove unused variable

* * Also add (V, E) to BlameAssignments if E modifies the bounds of V

* Simplify logic and improve comments

* Update tests to reflect the missing case

* Restore whitespace

* Restore whitespace

* Restore whitespace

* Restore whitespace

* Refactor and address the missing case; fix tests

* Clarify the logic in BlameAssignmentWithinStmt

* Reorder BoundsDeclarationCheck enum and update comments

* Gather proof failure cause and new error message

* Update diagnostic messages

* Convert offset constant to count

* Simplify error messages

* New error message

* Find free variables; use const modifier for some parameters

* Clean up and small fix

* Check equal variable

* Traverse ImplicitCastExpr instead of DeclRefExpr

* Revert changes

* Remove extra changes

* Add wrapper for ProofBoundsDeclValidity

* Add comments

* More comments

* Fix CollectVariableSet Helper

* Exclude variables that equal to a constant from free variables; consider declared bounds as well

* Code refactoring

* Detect free variables in bases and offsets separately

* Consider member accesses and filter out indirect accesses

* Handle expected argument bounds

* Fix tests

* Add comments

* Reformatting and fixing constant checking

* Update comments and reformat

* fix test

* Do not check free variables in static cast

* No free variable detection for static pointer casts and other cleanup

* Clean up

* Minor fix

* Add expected errors where the compiler is able to create a base range for the declared bounds (checkedc#913)

* Free variables: fix checkedc#909 and checkedc#911 by ignoring casts in EquivExprs (checkedc#919)

* Fix issue checkedc#909 and checkedc#911 by ignoring casts in EquivExprs

* Replace IgnoreCasts with IgnoreParenCasts and add test cases

* Detect indirect relationships between variables (checkedc#940)

* Change IsEqualToConstant to search for an rvalue cast of a variable

* Add FindVarRelationship method to search for an indirect relationship between variables

* Remove EquivVars set that filters out everything except DeclRefExprs and IntegerLiterals

* Remove expected free variables errors where there are indirect variable relationships

* Update note messages to mention lack of relational information between a free variable and expressions

* Remove comma from expected notes

* Fix comments

* Make free variable-related methods non-static

* Move top-level free variable method CheckFreeVarInExprs above other free variable methods

* Fix comment typo

* Update CheckFreeVarsInExprs comment

Co-authored-by: Katherine Kjeer <[email protected]>

* Add free-variables.c test to CheckedC/static-checking

This test was originally in the checkedc/tests/typechecking directory but was moved to checkedc-clang since it tests compiler implementation details (diagnostic messages).

* Update InRangeWithFreeVars comment

* Update more InRangeWithFreeVars comments

* Update EqualExprsContainsExpr comment

* Add TODO for quadratic algorithm in CollectVariableSetHelper

Co-authored-by: Yahui Sun <[email protected]>
Co-authored-by: Katherine Kjeer <[email protected]>
Co-authored-by: Katherine Kjeer <[email protected]>
* Add lvalue generalization doc

* Fix typos

* Move description of initial ObservedBounds to the end of the ResetKilledBounds section

* Replace details of checking state updating methods with a brief list of relevant methods

The details have been moved into the bounds checking doc in PR checkedc#945.

* Rephrase identical lvalue work description
* Pass IncludeAllMemberExprs argument through to ReadsMemoryViaPointer

* Skip checking free variables for expressions that are or contain any kind of member expressions

* Change expected struct-related free variables error to a warning

* Remove commented out lines in free-variables test

* Remove expected free variable errors from member-reference test

(cherry picked from commit 007ab6d)
@john-h-kastner
Copy link
Collaborator

PR microsoft#973 has been merged into Microsoft's master and resolves one of the failing tests

@mattmccutchen-cci mattmccutchen-cci force-pushed the merge-from-microsoft-20210127 branch from 762cd4c to 00db6f9 Compare February 4, 2021 14:51
@mattmccutchen-cci
Copy link
Member Author

Thanks John for the update and for getting one of the failures resolved! I decided to recheck where we stand.

I'm starting to look into the remaining failures:

  • manyprotos:
    int foo(_Array_ptr<int> x : count(y), int y);
    int bar(_Array_ptr<int> x : count(c), int c) { 
      return foo(x, 1) + 3;  // Checked C compile error
    }
    I think the Checked C compiler is right to reject our code. Without an assumption that c >= 1, there is no way to prove that the call foo(x, 1) is consistent with the signature of foo. @aaronjeline It looks like you added this test back in 1ebc2c1. Can you comment on what you were trying to test? Should we just change the call to be foo(x, c) or should we expect the error?
  • liberal_itype_ptrptr: This is a weird one. After one 3C pass with -alltypes, the relevant part of the code reads:
    void itype_defined_ptrptr(int **p : itype(_Ptr<_Ptr<int>>)) _Checked { }
    void itype_defined_caller() {
      _Ptr<int *> e = ((void *)0);
      itype_defined_ptrptr(_Assume_bounds_cast<_Ptr<_Ptr<int>>>(e));
    }
    With my limited knowledge of Checked C, I'd think that should be fine because we are casting e to the exact itype of the parameter. But the Checked C compiler gives this error message:
    liberal_itypes_ptrptr.checked.c:146:24: error: it is not possible to prove argument meets declared bounds for 1st parameter
      itype_defined_ptrptr(_Assume_bounds_cast<_Ptr<_Ptr<int>>>(e));
                           ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    liberal_itypes_ptrptr.checked.c:146:24: note: the expected argument bounds use the variable 'e' and there is no relational information involving 'e' and any of the expressions used by the inferred bounds
    liberal_itypes_ptrptr.checked.c:146:24: note: (expanded) expected argument bounds are 'bounds((_Array_ptr<_Ptr<int>>)_Assume_bounds_cast<_Ptr<_Ptr<int>>>e(count(1)), (_Array_ptr<_Ptr<int>>)_Assume_bounds_cast<_Ptr<_Ptr<int>>>e(count(1)) + 1)'
    liberal_itypes_ptrptr.checked.c:146:24: note: (expanded) inferred bounds are 'bounds((_Array_ptr<_Ptr<int>>)value of e, (_Array_ptr<_Ptr<int>>)value of e + 1)'
    
    It looks like the Checked C compiler is keeping the cast in the expression for the expected bounds but not the actual bounds, which leads to the mismatch and an error. Interestingly, if I change the definition of itype_defined_ptrptr to just void itype_defined_ptrptr(_Ptr<_Ptr<int>> p) _Checked { } rather than using an itype, then the error goes away. Or if I change the definition of itype_defined_caller to store the result of the cast in a local variable first:
    void itype_defined_caller() {
      _Ptr<int *> e = ((void *)0);
      _Ptr<_Ptr<int>> f = _Assume_bounds_cast<_Ptr<_Ptr<int>>>(e);
      itype_defined_ptrptr(f);
    }
    then the error also goes away. @john-h-kastner If you've already investigated this and learned anything, please let me know ASAP, otherwise I'll look into it a bit further and probably file an issue with Microsoft.

@john-h-kastner
Copy link
Collaborator

It's not clear to me when exactly CheckedC should emit a compile-time error for bounds rather than inserting runtime bounds checks, so I don't know for sure if the first test failure is legitimate. Since it's in an --alltypes test, this isn't too important for us. For this merge with Microsoft, I would be ok with either changing the function call to be foo(x, c) or passing the test -f3c-tool. I don't think the specifics of the function call are important to the test, so unless Aaron say otherwise, I think we should change the function call.

Another modification of the second test case that works is

void itype_defined_ptrptr(int **p : itype(_Ptr<_Ptr<int>>)) _Checked { }
void itype_defined_caller() {
  _Ptr<int *> e = ((void *)0);
  itype_defined_ptrptr((int**)e);
}

If we need to fix this in our code, changing the generated cast to (int**) should not be difficult. It does, however, seem wrong to me that CheckedC rejects the cast. Given that Microsoft has already fixed one issue in CheckedC that caused a failing test here, it's definitely worth asking them about this one.

@mattmccutchen-cci
Copy link
Member Author

mattmccutchen-cci commented Feb 4, 2021

I've tentatively added the manyprotos fix to this PR pending Aaron's approval (update: Aaron approved), so the only remaining failure is liberal_itype_ptrptr. Hopefully that will be fixed in checkedc#974 and then I can merge this PR.

@mattmccutchen-cci mattmccutchen-cci force-pushed the merge-from-microsoft-20210127 branch from 7007c6e to 6694a25 Compare February 12, 2021 17:04
@mattmccutchen-cci
Copy link
Member Author

Mike decided it was better to add an expected-error to the liberal_itype_ptrptr test than to wait longer for a fix from Microsoft, so I've done so and then rebased this PR.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants