Equivalent expressions: assignments [3/n] #802

kkjeer · 2020-03-04T18:56:38Z

This PR updates the sets UEQ and G of equivalent expressions while checking expressions that involve assignments. This is done with the following changes:

Update UEQ and G from CheckVarDecl (for declarations with initializers), CheckBinaryOperator (for assignments and compound assignments), and CheckUnaryOperator (for increment/decrement operators).
Add a GetIncomingBlockState method that gets the state that is true at the beginning of a CFG block by getting the intersection of the UEQ sets of the block's predecessors.
Add an UpdateAfterAssignment method that updates UEQ and G after an assignment to a variable V.
Add a GetOriginalValue method that gets the original value of a variable in an expression. Helper methods IsInvertible and Inverse are used to get the original value.
Add helpers PruneVariableReferences and VariableOccurrenceCount to help with getting the inverse of an expression.
Add utility classes VariableUtil and ExprCreatorUtil to help with detecting and comparing variables and creating certain kinds of expressions.
Modify asserts and diagnostic behavior in CanonBounds, TreeTransform, and SemaExpr to reflect the greater variety of expressions that can be lexicographically compared and transformed.

Testing:

Changed the behavior of the -fdump-checking-state flag to only dump the checking state after checking a top-level CFG statement, rather than after every expression. The equiv-exprs.c test has been modified to reflect this change.
Added a test equiv-expr-sets.c to test that the set UEQ of sets of equivalent expressions is properly updated while checking assignments. This file also tests that the incoming UEQ set is properly determined for CFG blocks in functions with if statements.
Passed manual testing on Windows.
Passed automated testing on Windows/Linux.

…tions of predecessor block states

…reExpr

… the variable

…signment to a non-variable

dtarditi

I have suggestions for comment improvements and some issues to address in follow-up pull requests.

dtarditi · 2020-04-02T04:10:10Z

clang/lib/Sema/SemaBounds.cpp

+          // Create the RHS of the implied assignment `e1 = e1 @ e2`.
+          Src = ExprCreatorUtil::CreateBinaryOperator(S, Target, RHS, Op);
+
+          // Update the set of expressions that produce the same value as `e1`.


I think this comment could be clarified to explain why we are doing this. Given that the compound assignment modifies e1, we need to choose an expression equal to the value of e1 before the assignment.

dtarditi · 2020-04-02T04:12:29Z

clang/lib/Sema/SemaBounds.cpp

+          SubExprGs[Src] = State.G;
+        }
+
+        // Update UEQ and G for assignments to a variable `e1`.


In the comment, I think you should change variable to expression.

dtarditi · 2020-04-02T04:33:24Z

clang/lib/Sema/SemaBounds.cpp

+          // Update State.G using the the target of the inc/dec operator for
+          // expressions where the integer constant 1 could not be constructed
+          // (e.g. floating point expressions). State.UEQ remains unchanged.
+          if (CheckIsNonModifying(Target) && CanBeInEqualExprSet(Target))


This doesn't seem right. What if the expression is a pre-increment expression, such as ++e1? Target is not the correct value of the entire expression ++e1. I think in case where the increment/decrement literal does not have an integer type, it is fine to set G to the empty set.

dtarditi · 2020-04-02T04:40:03Z

clang/lib/Sema/SemaBounds.cpp

@@ -3238,6 +3520,71 @@ namespace {
        RValueBounds = Check(E, CSS, State);
    }

+  // Methods to update sets of equivalent expressions.


The indentation is off.

clang/lib/Sema/SemaBounds.cpp

dtarditi · 2020-04-02T04:54:46Z

clang/lib/Sema/SemaBounds.cpp

+      return EqualValue(S.Context, V, Var, nullptr);
+    }
+
+    // CanBeInEqualExprSet returns true if the expression e can be added to


I think this method name is confusing. It should either be more descriptive, or also exclude non-modifying expressions.

dtarditi · 2020-04-02T05:11:30Z

clang/lib/Sema/SemaBounds.cpp

@@ -2327,8 +2518,50 @@ namespace {
        }
      }

+      // Update State.UEQ and State.G.


I didn't see this comment addressed in your most recent change. It would have been helpful to have a clarifying response here about why it wasn't addressed.

I looked into this and see that UpdateG is screening out non-modifying expressions in the S_i. I am pretty concerned about this. Expression equivalence checking assumes that expressions are non-modifying expressions and may produce incorrect results if they are modifying expressions.

For this reason, I think we should have an invariant that none of the subexpressions G_i containy modifying expression. This change is already large and I'd rather land it now, then have it continune onward. @kkjeer could you file an issue about this, and follow-up in a subsequent check-in.

dtarditi · 2020-04-02T05:22:43Z

clang/test/CheckedC/inferred-bounds/equiv-expr-sets.c

+// BinaryOperator: compound assignment to a variable
+void f3(unsigned i) {
+  // Updated UEQ: { { (i - 2) + 2, i } }
+  i += 2;


This equality implied by the UEQ set is a tautology. (i-2)+2 is equivalent to i (ignoring overflow). So we are saying i == i. When updating UEQ information, we should screen out equality facts implied by assignments to variables where the variable also appears on the right-hand side of the assignments. It's fine to flag this as a follow-up issue. This is already a large pull request.

I created issue #814 to track this work.

…c operators

dtarditi

Overall, looks great.

I have one last change regarding pre/post-increment expressions. We are trying to compute the non-modifying expression that is equivalent to the value produced by the pre/post-increment expression in the program state after the pre/post-increment expression has executed. The logic that you have reversed. In the state after executing ++x, x produces a value equivalent to the value produced by ++x.

dtarditi · 2020-04-04T01:23:25Z

clang/lib/Sema/SemaBounds.cpp

+
+        // Update the set G of expressions that produce the same value as e.
+        if (RHS) {
+          // For post-inc/dec operators, use the rvalue for `e1` to update G.


This logic is reversed. In the state after the expression ++x has executed, the non-modifying expression equivalent to the value produced by ++x is x. For x++, the non-modifying expression is x - 1..

…into equiv-exprs-assignments

dtarditi

Looks good! Thank you for the effort that you put into this change!

kakje added 30 commits February 26, 2020 18:19

Add VariableUtil class

bb1a569

Add ExprCreatorUtil

fbbc6f5

Add PruneVariableReferences

5a4152d

Add VariableOccurrenceCount

755758b

Add IncludeAllMemberExprs parameter to ReadsMemoryViaPointer

364bcab

Add helper methods to search equality sets

17487fd

Add IntersectUEQ and IntersectG methods

3535348

Add SplitByVarCount helper method

98d960b

Fix SplitByVarCount comment

a9c3922

Add Inverse methods

09c7e9c

Add IsInvertible methods

a1d51b8

Add GetOriginalValue method

f0c7bf8

Add UpdateAfterAssignment method

7433053

Update state after initializers in CheckVarDecl

95523a2

Update checking state for assignments in CheckBinaryOperator

c97e303

Update checking state for inc/dec operators in CheckUnaryOperator

e09d109

Set the incoming checking state for a CFG block by using the intersec…

9f17e5e

…tions of predecessor block states

Only dump checking state after checking top-level statements

f92b11f

Add initial equiv-expr-sets test with VarDecl initializer test

199534f

Add BinaryOperator assignment tests

1b71577

Add UnaryOperator inc/dec operator tests

ee40a16

Add tests for multiple assignments

4a4b26e

Add tests for original values

550ddd6

Add tests for control flow

fc23804

Remove unexpected expression kind unreachable from CanonBounds::Compa…

792db05

…reExpr

Fix ExprCreatorUtil::CreateBinaryOperator to handle compond assignments

237b117

Modify PruneVariableReferences to only transform expressions that use…

fc23bfd

… the variable

Don't add unary operators to possible derefs if diagnostics are disabled

2014368

Change TreeTransform BlockExpr assert to compare CaptureMap counts

b4d3e35

Avoid adding duplicate expressions to UEQ and G

d0e9a6b

kakje added 9 commits March 12, 2020 16:47

Clean up set intersection methods

43f8b90

Explicitly handle getting lvalue and rvalue variables

e585d00

Add non-modifying expression check to the target of a non-compound as…

995fc71

…signment to a non-variable

Handle integer constant creation for unary inc/dec operators

7358af7

Check that the bit with and int size are equal in CreateIntegerLiteral

e967646

Avoid adding non-comparable expressions to UEQ and G

1ea75e4

Prevent StringLiterals from being added to UEQ and G

7ee9ef5

Allow conditional operators in equivalent expression sets

2bd6d6e

Update CanBeInEqualExprSet comment

135410d

dtarditi reviewed Apr 2, 2020

View reviewed changes

kakje added 13 commits April 2, 2020 13:02

Update CheckBinaryOperator and CheckUnaryOperator comments

a8d2bd1

Set G to empty for non-integer inc/dec operators

94f7676

Fix indentation

c1cbae2

Update CheckVarDecl comments

7b94476

Rename CanBeInEqualExprSet to CreatesNewObject

b247b71

Update GetEqualExprSetContainingVariable comment

58db814

Update comments and variable names for UpdateG

d13f8dc

Remove unnecessary SubExprGs updates in CheckBinaryOperator

c1b5d6b

Clear G for assignments to non-variables

16db44b

Add nonmodifying checks to CheckCastExpr before modifying G

a47e887

Prevent UEQ from containing contradictions and tautologies for inc/de…

62d8b2e

…c operators

Remove debug code

ac9e617

Add null check to IsInvertible

5844f66

dtarditi reviewed Apr 4, 2020

View reviewed changes

kakje added 2 commits April 3, 2020 21:54

Merge branch 'master' of https://github.com/Microsoft/checkedc-clang …

b334667

…into equiv-exprs-assignments

Fix logic to update G for inc/dec operators

89909a8

dtarditi approved these changes Apr 4, 2020

View reviewed changes

kkjeer merged commit cfefa2d into master Apr 6, 2020

kkjeer deleted the equiv-exprs-assignments branch April 11, 2020 07:25

secure-sw-dev-bot mentioned this pull request Jan 16, 2022

Equivalent expressions: assignments [3/n] checkedc/checkedc-llvm-project#798

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Equivalent expressions: assignments [3/n] #802

Equivalent expressions: assignments [3/n] #802

Uh oh!

kkjeer commented Mar 4, 2020

Uh oh!

dtarditi left a comment •

edited

Loading

Uh oh!

dtarditi Apr 2, 2020

Uh oh!

dtarditi Apr 2, 2020

Uh oh!

dtarditi Apr 2, 2020

Uh oh!

dtarditi Apr 2, 2020

Uh oh!

Uh oh!

Uh oh!

dtarditi Apr 2, 2020

Uh oh!

dtarditi Apr 2, 2020

Uh oh!

dtarditi Apr 2, 2020 •

edited

Loading

Uh oh!

kkjeer Apr 2, 2020

Uh oh!

dtarditi left a comment

Uh oh!

dtarditi Apr 4, 2020

Uh oh!

dtarditi left a comment

Uh oh!

Uh oh!

Equivalent expressions: assignments [3/n] #802

Equivalent expressions: assignments [3/n] #802

Uh oh!

Conversation

kkjeer commented Mar 4, 2020

Uh oh!

dtarditi left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dtarditi Apr 2, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dtarditi left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dtarditi left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

dtarditi left a comment •

edited

Loading

dtarditi Apr 2, 2020 •

edited

Loading