Skip to content

Invertibility for unchecked pointers #1127

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 5 commits into from
Jul 20, 2021
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Fix typo
  • Loading branch information
kakje committed Jul 14, 2021
commit f0b11319b8cd08e3d5920561875d0055e45aa2e0
3 changes: 0 additions & 3 deletions clang/include/clang/AST/ExprUtils.h
Original file line number Diff line number Diff line change
Expand Up @@ -129,9 +129,6 @@ class ExprUtil {
static bool EqualValue(ASTContext &Ctx, Expr *E1, Expr *E2,
EquivExprSets *EquivExprs);

// EqualTypes returns true if T1 and T2 are lexicographically equivalent.
static bool EqualTypes(ASTContext &Ctx, QualType T1, QualType T2);

// CheckIsNonModifying suppresses diagnostics while checking
// whether e is a non-modifying expression.
static bool CheckIsNonModifying(Sema &S, Expr *E);
Expand Down
5 changes: 0 additions & 5 deletions clang/lib/AST/ExprUtils.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -251,11 +251,6 @@ bool ExprUtil::EqualValue(ASTContext &Ctx, Expr *E1, Expr *E2,
return R == Lexicographic::Result::Equal;
}

bool ExprUtil::EqualTypes(ASTContext &Ctx, QualType T1, QualType T2) {
Lexicographic::Result R = Lexicographic(Ctx, nullptr).CompareType(T1, T2);
return R == Lexicographic::Result::Equal;
}

bool ExprUtil::CheckIsNonModifying(Sema &S, Expr *E) {
return S.CheckIsNonModifying(E, Sema::NonModifyingContext::NMC_Unknown,
Sema::NonModifyingMessage::NMM_None);
Expand Down
77 changes: 10 additions & 67 deletions clang/lib/Sema/SemaBounds.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -932,10 +932,9 @@ namespace {
// The proof system is incomplete, so there are will be statements that
// cannot be proved true or false. That's why "maybe" is a result.
enum class ProofResult {
True, // Definitely provable.
False, // Definitely false (an error)
Maybe, // We're not sure yet.
IncompleteTypes // Unable to prove due to incomplete referent types.
True, // Definitely provable.
False, // Definitely false (an error)
Maybe // We're not sure yet.
};

// The kind of statement that we are trying to prove true or false.
Expand Down Expand Up @@ -1038,7 +1037,6 @@ namespace {
enum Kind {
ConstantSized,
VariableSized,
IncompleteConstantSized,
Invalid
};

Expand All @@ -1049,31 +1047,24 @@ namespace {
llvm::APSInt UpperOffsetConstant;
Expr *LowerOffsetVariable;
Expr *UpperOffsetVariable;
// HasIncompleteConstant tracks whether either the lower or upper
// constant offset is based on an expression with an incomplete
// referent type.
bool HasIncompleteConstant;

public:
BaseRange(Sema &S) : S(S), Base(nullptr), LowerOffsetConstant(1, true),
UpperOffsetConstant(1, true), LowerOffsetVariable(nullptr), UpperOffsetVariable(nullptr),
HasIncompleteConstant(false) {
UpperOffsetConstant(1, true), LowerOffsetVariable(nullptr), UpperOffsetVariable(nullptr) {
}

BaseRange(Sema &S, Expr *Base,
llvm::APSInt &LowerOffsetConstant,
llvm::APSInt &UpperOffsetConstant) :
S(S), Base(Base), LowerOffsetConstant(LowerOffsetConstant), UpperOffsetConstant(UpperOffsetConstant),
LowerOffsetVariable(nullptr), UpperOffsetVariable(nullptr),
HasIncompleteConstant(false) {
LowerOffsetVariable(nullptr), UpperOffsetVariable(nullptr) {
}

BaseRange(Sema &S, Expr *Base,
Expr *LowerOffsetVariable,
Expr *UpperOffsetVariable) :
S(S), Base(Base), LowerOffsetConstant(1, true), UpperOffsetConstant(1, true),
LowerOffsetVariable(LowerOffsetVariable), UpperOffsetVariable(UpperOffsetVariable),
HasIncompleteConstant(false) {
LowerOffsetVariable(LowerOffsetVariable), UpperOffsetVariable(UpperOffsetVariable) {
}

private:
Expand Down Expand Up @@ -1259,11 +1250,6 @@ namespace {
return ProofResult::Maybe;
}

// Check whether we are allowed to continue with the proof, based on
// whether this and R involve incomplete referent types.
if (!CheckIncompleteConstants(R))
return ProofResult::IncompleteTypes;

if (ExprUtil::EqualValue(S.Context, Base, R.Base, EquivExprs)) {
ProofResult LowerBoundsResult = CompareLowerOffsetsImpl(R, Cause, EquivExprs, Facts);
ProofResult UpperBoundsResult = CompareUpperOffsetsImpl(R, Cause, EquivExprs, Facts);
Expand Down Expand Up @@ -1313,11 +1299,6 @@ namespace {
return ProofResult::Maybe;
}

// Check whether we are allowed to continue with the proof, based on
// whether this and R involve incomplete referent types.
if (!CheckIncompleteConstants(R))
return ProofResult::IncompleteTypes;

FreeVariablePosition BasePos = CombineFreeVariablePosition(
FreeVariablePosition::Lower, FreeVariablePosition::Upper);
FreeVariablePosition DeclaredBasePos = CombineFreeVariablePosition(
Expand Down Expand Up @@ -1346,30 +1327,6 @@ namespace {
return ProofResult::Maybe;
}

// This function checks whether it is possible to compare this and R,
// based on whether this and R have at least one offset that was derived
// from a base expression with an incomplete referent type.
//
// If both this and R have an offset based on types T1 and T2 with
// incomplete referent types, then the offsets should have been
// multiplied by sizeof(T1) and sizeof(T2), where the sizes of T1 and
// T2 could not be determined. In this case, we require that T1 and
// T2 are equivalent types. Otherwise, we cannot continue to compare
// this and R.
//
// If only one of this and R is based on an incomplete referent type,
// then we cannot continue to compare them.
bool CheckIncompleteConstants(BaseRange &R) {
if (HasIncompleteConstant) {
if (!R.HasIncompleteConstant)
return false;
if (!ExprUtil::EqualTypes(S.Context, Base->getType(), R.Base->getType()))
return false;
} else if (R.HasIncompleteConstant)
return false;
return true;
}

// This function proves whether this.LowerOffset <= R.LowerOffset.
// Depending on whether these lower offsets are ConstantSized or VariableSized, various cases should be checked:
// - If `this` and `R` both have constant lower offsets (i.e., if the following condition holds:
Expand Down Expand Up @@ -1779,10 +1736,6 @@ namespace {
UpperOffsetVariable = Upper;
}

void SetHasIncompleteConstant(bool Incomplete) {
HasIncompleteConstant = Incomplete;
}

void Dump(raw_ostream &OS) {
OS << "Range:\n";
OS << "Base: ";
Expand Down Expand Up @@ -1872,7 +1825,7 @@ namespace {
}
llvm::APSInt ElemSize;
if (!ExprUtil::getReferentSizeInChars(S.Context, Base->getType(), ElemSize))
return BaseRange::Kind::IncompleteConstantSized;
goto exit;
OffsetConstant = OffsetConstant.smul_ov(ElemSize, Overflow);
if (Overflow)
goto exit;
Expand All @@ -1890,12 +1843,6 @@ namespace {
Base = E->IgnoreParens();
OffsetConstant = llvm::APSInt(PointerWidth, false);
OffsetVariable = nullptr;
// If the base expression has an incomplete referent type, we consider
// the range to be incomplete constant-sized. This means that, if Base
// has an incomplete referent type, B and B + 0 will both be incomplete
// constant-sized ranges.
if (Base->getType()->getPointeeOrArrayElementType()->isIncompleteType())
return BaseRange::Kind::IncompleteConstantSized;
return BaseRange::Kind::ConstantSized;
}

Expand Down Expand Up @@ -2084,11 +2031,11 @@ namespace {
Expr *Upper = RB->getUpperExpr();
Expr *LowerBase, *UpperBase;
llvm::APSInt LowerOffsetConstant(1, true);
llvm::APSInt UpperOffsetConstant(1, true);
llvm::APSInt UpperOffsetConstant(1, true);
Expr *LowerOffsetVariable = nullptr;
Expr *UpperOffsetVariable = nullptr;
BaseRange::Kind LowerKind = SplitIntoBaseAndOffset(Lower, LowerBase, LowerOffsetConstant, LowerOffsetVariable);
BaseRange::Kind UpperKind = SplitIntoBaseAndOffset(Upper, UpperBase, UpperOffsetConstant, UpperOffsetVariable);
SplitIntoBaseAndOffset(Lower, LowerBase, LowerOffsetConstant, LowerOffsetVariable);
SplitIntoBaseAndOffset(Upper, UpperBase, UpperOffsetConstant, UpperOffsetVariable);

// If both of the offsets are constants, the range is considered constant-sized.
// Otherwise, it is a variable-sized range.
Expand All @@ -2098,8 +2045,6 @@ namespace {
R->SetLowerVariable(LowerOffsetVariable);
R->SetUpperConstant(UpperOffsetConstant);
R->SetUpperVariable(UpperOffsetVariable);
R->SetHasIncompleteConstant(LowerKind == BaseRange::Kind::IncompleteConstantSized ||
UpperKind == BaseRange::Kind::IncompleteConstantSized);
return true;
}
}
Expand Down Expand Up @@ -2162,8 +2107,6 @@ namespace {
DeclaredRange, Cause, EquivExprs, Facts, FreeVariables);
if (R == ProofResult::True)
return R;
if (R == ProofResult::IncompleteTypes)
return ProofResult::Maybe;
if (R == ProofResult::False || R == ProofResult::Maybe) {
if (R == ProofResult::False && SrcRange.IsEmpty())
Cause = CombineFailures(Cause, ProofFailure::SrcEmpty);
Expand Down
2 changes: 1 addition & 1 deletion clang/test/CheckedC/inferred-bounds/equiv-expr-sets.c
Original file line number Diff line number Diff line change
Expand Up @@ -1448,7 +1448,7 @@ void original_value19(array_ptr<int> *x, array_ptr<int> *i) {
// CHECK-NEXT: }

// Original value of i in i - 1: i + 1
// Updated EquivExprs: { { i + 1, i } }, Updated SameValue: { i + 1 }
// Updated EquivExprs: { { i + 1, x } }, Updated SameValue: { i + 1 }
i--;
// CHECK: Statement S:
// CHECK-NEXT: UnaryOperator {{.*}} postfix '--'
Expand Down
37 changes: 6 additions & 31 deletions clang/test/CheckedC/static-checking/bounds-decl-checking.c
Original file line number Diff line number Diff line change
Expand Up @@ -276,9 +276,7 @@ void test_addition_commutativity(void) {
// Test uses of incomplete types

struct S;
struct R;
extern void test_f30(_Array_ptr<const void> p_ptr : byte_count(1));
extern void test_f31(_Array_ptr<struct S> p : count(0));

int f30(_Ptr<struct S> p) {
// TODO: Github Checked C repo issue #422: Extend constant-sized ranges to cover Ptr to an incomplete type
Expand All @@ -288,41 +286,18 @@ int f30(_Ptr<struct S> p) {
return 0;
}

int f31(_Array_ptr<struct S> p : count(1), _Array_ptr<struct R> q : count(1)) { // expected-note {{(expanded) declared bounds are 'bounds(p, p + 1)'}}
// We cannot compare unequal incomplete referent types 'struct S' and 'struct R' of p and q.
p = (_Array_ptr<struct S>)q; // expected-warning {{cannot prove declared bounds for 'p' are valid after assignment}} \
// expected-note {{(expanded) inferred bounds are 'bounds(q, q + 1)'}}
}

int f32(_Array_ptr<struct S> p : count(0), _Array_ptr<struct S> q : count(1)) {
// p and q have the same incomplete referent type 'struct S'.
p = q;
}

int f33(_Ptr<struct S> p) {
test_f31(p);
return 0;
}

int f34(_Array_ptr<struct S> p : bounds(p, p), _Array_ptr<struct S> q : count(0)) {
p = q;
return 0;
}

int f35(_Array_ptr<struct S> p : count(i), _Array_ptr<struct S> q : count(i + 1), int i) { // expected-note {{(expanded) declared bounds are 'bounds(p, p + i)'}}
p = q; // expected-warning {{cannot prove declared bounds for 'p' are valid after assignment}} \
// expected-note {{(expanded) inferred bounds are 'bounds(q, q + i + 1)'}}
return 0;
}

int f36(_Ptr<void> p) {
int f31(_Ptr<void> p) {
test_f30(p);
return 0;
}

// The warning is not directly related to issue #599
// It is related to incomplete types.
_Array_ptr<struct S> f37_i(unsigned num) : count(num) {
_Array_ptr<struct S> q : count(num) = 0;
_Array_ptr<struct S> p : count(0) = q;
_Array_ptr<struct S> p : count(0) = q; // expected-warning {{cannot prove declared bounds for 'p' are valid after initialization}} \
// expected-note {{(expanded) declared bounds are 'bounds(p, p + 0)'}} \
// expected-note {{(expanded) inferred bounds are 'bounds(q, q + num)'}}
return p;
}

Expand Down
You are viewing a condensed version of this merge commit. You can view the full changes here.