Skip to content

[BoundsWidening] Update observed bounds with widened bounds#1108

Closed
mgrang wants to merge 1 commit into
bounds_widening_dev5from
update_observed_bounds5
Closed

[BoundsWidening] Update observed bounds with widened bounds#1108
mgrang wants to merge 1 commit into
bounds_widening_dev5from
update_observed_bounds5

Conversation

@mgrang

@mgrang mgrang commented Jun 25, 2021

Copy link
Copy Markdown

For each statement update the observed bounds in the BlockState with the
widened bounds as computed by the updated bounds widening analysis. The bounds
of variables whose bounds are killed are reset to the declared bounds. This PR
also updates the method GetBoundsWidenedAndNotKilled that returns the bounds
widened in a block before a given statement and not killed by that statement.

This PR also deletes the old bounds widening analysis files
BoundsAnalysis(.h,.cpp).

For each statement update the observed bounds in the BlockState with the
widened bounds as computed by the updated bounds widening analysis. The bounds
of variables whose bounds are killed are reset to the declared bounds. This PR
also updates the method GetBoundsWidenedAndNotKilled that returns the bounds
widened in a block before a given statement and not killed by that statement.

This PR also deletes the old bounds widening analysis files
BoundsAnalysis(.h,.cpp).
@mgrang mgrang requested review from arbipher, kkjeer and sulekhark and removed request for sulekhark June 25, 2021 02:19

// If a variable does not exist in WidenedBounds but exists in
// State.ObservedBounds it means that the bounds of the variable got
// killed before the current statement. So we reset the bounds of the

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

This comment could be made more precise:
If a variable does not exist in WidenedBounds but exists in State.ObservedBounds, it may not be an _Nt_array_ptr or it is no longer a candidate for widening.

continue;

// BoundsWideningAnalysis currently uses VarDecls as keys in the widened
// bounds data structure, so we create an AbstractSet for each VarDecl

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Minor correction but will help clarify things for a reader unfamiliar with all the details: ..... so we get the AbstractSet for each VarDecl .....

int f();
// Test where clauses on variable declarations inside a function.
void valid_cases_decl(_Nt_array_ptr<char> p, _Nt_array_ptr<char> q) {
void valid_cases_decl(_Nt_array_ptr<char> p, _Nt_array_ptr<char> q) { // expected-error {{it is not possible to prove that the inferred bounds of 'p' imply the declared bounds of 'p' after initialization}} expected-error {{it is not possible to prove that the inferred bounds of 'p' imply the declared bounds of 'p' after initialization}} expected-error {{it is not possible to prove that the inferred bounds of 'p' imply the declared bounds of 'p' after initialization}} expected-error {{it is not possible to prove that the inferred bounds of 'q' imply the declared bounds of 'q' after initialization}}

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Could we please discuss what exactly is happening here and analyze the compiler error messages?

for (auto I = State.ObservedBounds.begin(),
E = State.ObservedBounds.end(); I != E; ++I) {
const AbstractSet *A = I->first;
const VarDecl *V = A->GetVarDecl();

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

On master, AbstractSet no longer has a GetVarDecl method. It has a GetDecl method that returns a NamedDecl *.

// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'p'
// CHECK-NEXT: IntegerLiteral {{.*}} 0
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Since it looks like the widened bounds of p are bounds(p, p + 1) instead of bounds(p, p + 0 + 1), can the comment on line 2012 be updated?

// bounds data structure, so we create an AbstractSet for each
// VarDecl in the killed bounds. TODO: use AbstractSets as keys
// in BoundsAnalysis (checkedc-clang issue #1015).
// Update State.ObservedBounds with the WidenedBounds before the current

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Could this logic be moved into the pass over State.ObservedBounds?

@mgrang

mgrang commented Jul 9, 2021

Copy link
Copy Markdown
Author

Superseded by #1122

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.

3 participants