Detect indirect relationships between variables #940

kkjeer · 2020-11-16T19:03:48Z

This PR modifies the definition of free variables so that, if:

x is a variable appearing in declared (or inferred) bounds, and:
y is a variable appearing in inferred (or declared) bounds, and:
e1 is an expression that uses the value of x, and:
e2 is an expression that uses the value of y, and:
EquivExprs contains a set that contains both e1 and e2

then x is not a free variable.

This change means that some bounds warnings that were converted to free variable errors are now back to being warnings. The free variable note messages are also reworded to mention expressions in declared/inferred bounds rather than variables.

Testing

Modified tests to reflect free variable errors which are now back to being bounds warnings.
Modified tests to reflect reworded free variable note messages.
Modified checkedc tests in checkedc/428.
Passed automated testing on Linux.

… between variables

…and IntegerLiterals

…le relationships

…n a free variable and expressions

mgrang · 2020-11-16T19:10:50Z

clang/lib/Sema/SemaBounds.cpp

@@ -1453,23 +1453,78 @@ namespace {

        // Gather free variables.
        for (const auto &SrcV : SrcVars) {
-          if (IsEqualToConstant(S, SrcV, EquivExprs))
+          DeclRefExpr *SrcVar = cast<DeclRefExpr>(SrcV);


What happens if SrcV is not a DeclRefExpr?

The list SrcVars should always be a list of DeclRefExprs since it is obtained by searching for all the DeclRefExprs that occur in a bounds expression. As a separate cleanup item, the type of SrcVars should be changed from EqualExprTy (set of Exprs) to a set of DeclRefExprs.

Created #941 to track this.

kkjeer · 2020-11-19T23:40:18Z

Some notes from the PR discussion:

A potential performance improvement is to construct a map of each expression in EquivExprs to the set of variables the expression uses. This prevents the need to repeatedly search each expression in EquivExprs for expressions that use SrcV or a variable in DstVars. This is a follow-up item to consider if further testing data indicates that performance improvements are necessary.
Which kinds of expressions can be used to find indirect relationships between variables?
The EquivExprs set (containing expressions that can be used to find variable relationships) can contain expressions that:

Are non-modifying (function calls, assignments, etc. cannot be in EquivExprs)
Do not read memory via a pointer (pointer dereferences, array subscripts, etc. cannot be in EquivExprs)
Create a new object (string literals, initializer lists, etc. cannot be in EquivExprs)
Some examples of expressions that can appear in EquivExprs are x, 3, y + 1, a && b, &p, etc.

How is EquivExprs modified?
EquivExprs is modified after assignments (x = y, x++, x += z, etc.) and initializers. For example, after checking the assignment x = y, EquivExprs will contain a set containing x and y (thus recording equality between x and y).
Which kinds of expressions do we use to emit free variable errors?
We only consider variables, i.e. DeclRefExprs to be free. For example, in declared bounds (p, p + s.len) and inferred bounds (p, p + 3), we do not consider s.len to be a "free expression". In declared bounds (p, p + x) and inferred bounds (p, p + 3), we can consider x to be a free variable.

…ree variable methods

mgrang

LGTM.

dtarditi

Looks great, thanks! I have some suggestions about comments.

dtarditi · 2021-01-12T05:40:03Z

clang/lib/Sema/SemaBounds.cpp

-      //   that contains both V and U.
+      //   1. V is not equal to an integer constant, i.e. there is no set in
+      //      EquivExprs that contains V and an IntegerLiteral expression, and:
+      //   2. For each variable U in DstVars, V is not equivlaent to U, i.e.


This is a typo in the spelling of equivalent.

dtarditi · 2021-01-12T05:56:43Z

clang/lib/Sema/SemaBounds.cpp

@@ -1432,111 +1432,170 @@ namespace {
        return ProofResult::Maybe;
      }

+      // CheckFreeVarInExprs returns true if there are any free variables in
+      // E1 w.r.t E2, or if there are any free variables in E2 w.r.t E1.
+      // Any free variables in E1 with position Pos1 and any free variables in


The comment is somewhat confusing in its explanation of the uses of the Pos1 and Pos2 arguments. I think it would better to expand the comment: Any free variables in E1 and any free variables in E2 are appended to FreeVars. Pos1 is the position of E1 and Pos2 is the position of E2. Free variables are appended with the position information of the expression in which they are free (free variables in E1 are appended with the position of E1, for example).

…lared bounds (#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 (#913) * Free variables: fix #909 and #911 by ignoring casts in EquivExprs (#919) * Fix issue #909 and #911 by ignoring casts in EquivExprs * Replace IgnoreCasts with IgnoreParenCasts and add test cases * Detect indirect relationships between variables (#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]>

Katherine Kjeer added 6 commits November 14, 2020 23:30

Change IsEqualToConstant to search for an rvalue cast of a variable

9cfa5b7

Add FindVarRelationship method to search for an indirect relationship…

d963c41

… between variables

Remove EquivVars set that filters out everything except DeclRefExprs …

4e97be6

…and IntegerLiterals

Remove expected free variables errors where there are indirect variab…

12588cf

…le relationships

Update note messages to mention lack of relational information betwee…

c720d6a

…n a free variable and expressions

Remove comma from expected notes

f723736

kkjeer requested review from dtarditi, mgrang and sulekhark November 16, 2020 19:03

kkjeer mentioned this pull request Nov 16, 2020

Detect indirect relationships between variables checkedc/checkedc#428

Merged

mgrang reviewed Nov 16, 2020

View reviewed changes

Katherine Kjeer added 3 commits November 19, 2020 15:47

Fix comments

3682ab8

Make free variable-related methods non-static

a6bd723

Move top-level free variable method CheckFreeVarInExprs above other f…

2934719

…ree variable methods

mgrang approved these changes Nov 20, 2020

View reviewed changes

dtarditi approved these changes Jan 12, 2021

View reviewed changes

Katherine Kjeer added 2 commits January 12, 2021 15:34

Fix comment typo

e7dbc18

Update CheckFreeVarsInExprs comment

f91c892

kkjeer merged commit 555a93c into non-equiv-exprs-in-bounds Jan 14, 2021

kkjeer deleted the free-vars-relationships branch January 14, 2021 23:51

This was referenced Jan 15, 2022

Detect indirect relationships between variables checkedc/checkedc-fork#427

Closed

Detect indirect relationships between variables checkedc/checkedc-llvm-project#936

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Detect indirect relationships between variables #940

Detect indirect relationships between variables #940

Uh oh!

kkjeer commented Nov 16, 2020 •

edited

Loading

Uh oh!

mgrang Nov 16, 2020

Uh oh!

kkjeer Nov 16, 2020

Uh oh!

kkjeer Nov 16, 2020

Uh oh!

kkjeer commented Nov 19, 2020

Uh oh!

mgrang left a comment

Uh oh!

dtarditi left a comment

Uh oh!

dtarditi Jan 12, 2021

Uh oh!

dtarditi Jan 12, 2021

Uh oh!

Uh oh!

Detect indirect relationships between variables #940

Detect indirect relationships between variables #940

Uh oh!

Conversation

kkjeer commented Nov 16, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Testing

Uh oh!

mgrang Nov 16, 2020

Choose a reason for hiding this comment

Uh oh!

kkjeer Nov 16, 2020

Choose a reason for hiding this comment

Uh oh!

kkjeer Nov 16, 2020

Choose a reason for hiding this comment

Uh oh!

kkjeer commented Nov 19, 2020

Uh oh!

mgrang left a comment

Choose a reason for hiding this comment

Uh oh!

dtarditi left a comment

Choose a reason for hiding this comment

Uh oh!

dtarditi Jan 12, 2021

Choose a reason for hiding this comment

Uh oh!

dtarditi Jan 12, 2021

Choose a reason for hiding this comment

Uh oh!

Uh oh!

kkjeer commented Nov 16, 2020 •

edited

Loading