Skip to content
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

Don't record temporary equality between expression such as x and x + 1 in TargetSrcEquality #1162

Merged
merged 3 commits into from Aug 20, 2021

Conversation

kkjeer
Copy link
Contributor

@kkjeer kkjeer commented Aug 18, 2021

This PR fixes a bug with the way equivalent expressions were being recorded in RecordEqualityWithTarget.

In an assignment such as x++, x += 1, x = x + 1, etc., SameValue is empty after calling UpdateSameValueAfterAssignment (since the RHS x + 1 of the assignment uses the value of the LHS x). This meant that SrcAllowedInEquivExprs was false in RecordEqualityWithTarget, so the mapping x => x + 1 was added to TargetSrcEquality. The information in TargetSrcEquality is added to EquivExprs in ValidateBoundsContext, so EquivExprs would contain a set that contained both x and x + 1 only while checking bounds after the current top-level statement.

This PR adds an AllowTempEquality argument to RecordEqualityWithTarget that controls whether the mapping Target => Src is permitted to be added to TargetSrcEquality. UpdateSameValueAfterAssignment now returns true if State.SameValue was unchanged by the assignment (if the RHS of the assignment uses the value of the LHS, then at least one expression will be removed from State.SameValue if State.SameValue was initially nonempty). If State.SameValue was unchanged by the assignment, then temporary equality is allowed to be recorded between Target and Src.

@@ -4710,25 +4721,38 @@ namespace {
if (AdjustedE && !EqualExprsContainsExpr(State.SameValue, AdjustedE))
State.SameValue.push_back(AdjustedE);
}
return State.SameValue.size() == PrevSameValue.size();
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it sufficient to check that State.SameValue.size() == PrevSameValue.size() to be sure that no expressions in SameValue use the value of LValue? What if the number of elements in SameValue remain the same but one or more of these elements are modified?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If the original value uses the value of LValue, then the value used to replace uses of LValue in SameValue will be null, which means that any expressions in SameValue that use the value of LValue will be removed from SameValue.

I think this could be clearer in the code; I'll work on cleaning up the solution.

Copy link
Contributor

@sulekhark sulekhark left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM! Thank you!

@kkjeer kkjeer merged commit c88ca51 into master Aug 20, 2021
@kkjeer kkjeer deleted the fix-equiv-exprs branch August 20, 2021 22:05
arbipher added a commit that referenced this pull request Aug 26, 2021
* Revert "[BoundsWidening] Determine checked scope specifier per statement (#1139)" (#1141)

This reverts commit 980321d.

* Determine checked scopes per statement (#1142)

We introduce a 2-bit field called CheckedScopeSpecifier in the Stmt class.
During parsing when a compound statement is created we iterate the elements
(statements) of the compound statement and set the checked scope specifier for
each element to the checked scope specifier of the compound statement.

We can get the checked scope specifier for a statement by calling the
getCheckedScopeSpecifier method on the statement.

* Update the instructions for upgrade of LLVM/Clang. (#1146)

* Updated the instructions for upgrade of LLVM/Clang.
Also added a new file LLVM-Upgrade-Notes.md to track important
information related to upgrades.

* Fixed typos.

* Addressed review comments.

* Fixed an inadvertent deletion.

* Addressed review comments.

* Incorporated review comments.

* Fixed minor typos.

* Fixed typos.

* Add new flags for available facts analysis

* Add the analysis into the build script and the sema bounds

* Add utility functions to check whether a var is used in a Expr and a BoundsExpr

* Add AbstractFact as a basic available fact;
Add InferredFact and adjust WhereClauseFact to be a subclass of AbstractFact

* Add data structures used in the analysis

* Add print and dump functions

* Add utility functions which are also used by BoundsWideningAnalysis.

* Add other utility functions.

`IsSwitchCaseBlock`: use `dyn_cast_or_null` to cover the null pointer
case.

`ConditionOnEdge`: do not test if there is no edge between
pred to curr since it will only be called if there is an edge.

`GetModifiedVars`: use `TranspareCasts` to bypass some casting.
The feature to deal with membership access and the array indexing is
still TODO.

* Add fact comparision and fact-realted set oerations (contains TODO).

* Add testscases (one covers basic features and the other is converted
from the previous available facts analysis)

* Dataflow analysis: Add statement-based Gen/Kill.

* Dataflow analysis: Add block-edge-based Gen set.

* Dataflow analysis: Add function to compute In and Out set.

* Dataflow analysis: Addworklist algorithm.

* Add desctrutors to release the memory

* Fix: modify the Gen/Kill rules to match the design doc;
It also fixes a bug to visit dead blocks.

* Cleanup comments

* Fix: use the exisiting functions to find a `VarDecl` in an expr

* Change the equal check on fact collections to equal size check

* Update the testcases with the updated Gen/Kill

* Remove debug flag for available facts.

* Use lexco-compare for `EqualityOpFact` and `InferredFact`.

* Add a map to store the comparision results of facts.

* Change the source location of a fact to its near expr.

* Use a dedicated list to collect created facts and clean them finally.

* Verify if an expr contains errors before checking invertibility  (#1154)

The community has introduced a new annotation called "contains-errors" on AST
nodes that contain semantic errors. As a result, after the upgrade of Checked C
sources to LLVM 12 we need to check if an expr contains errors before operating
on the expr. One such place is in InverseUtil::IsInvertible where we need to
check if the input modifying expr contains errors.

* Added containsErrors checks to InverUtil::Inverse

* [BoundsWidening] Handle complex conditionals in bounds widening (#1149)

Support bounds widening in presence of complex conditionals like:
  "if (*p != 0)", "if ((c = *p) == 'a')", etc.

* Don't record temporary equality between expressions such as x and x + 1 in TargetSrcEquality (#1162)

* Add AllowTempEquality parameter to RecordEqualityWithTarget

* Use a ModifiedSameValue variable to determine the return value for UpdateSameValueAfterAssignment

* Rename ModifiedSameValue to RemovedAnyExprs and clean up comments

* Treat address-of array subscripts the same way as address-of dereferences (#1163)

* In CheckAddressOfOperand, add case for address-of array subscripts to C99-specific logic

* Move address-of array subscript check after other checks such as taking the address of an lvalue

* Adjust expected AST output to account for different types of address-of array subscripts

* Restore deleted comment about checking for array subscript expressions

* Add comment explaining the placement of the address-of array subscript logic

* Put &e1[e2] typing rules under a Checked C flag

* Update the available facts analysis.

Co-authored-by: Mandeep Singh Grang <magrang@microsoft.com>
Co-authored-by: Sulekha Kulkarni <Sulekha.Kulkarni@microsoft.com>
Co-authored-by: Katherine Kjeer <6687333+kkjeer@users.noreply.github.com>
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.

None yet

2 participants