Skip to content

Commit

Permalink
[clang][dataflow] Unsoundly treat "Unknown" as "Equivalent" in widening.
Browse files Browse the repository at this point in the history
This change makes widening act the same as equivalence checking. When the
analysis does not provide an answer regarding the equivalence of two distinct
values, the framework treats them as equivalent. This is an unsound choice that
enables convergence.

Differential Revision: https://reviews.llvm.org/D159355
  • Loading branch information
ymand committed Sep 7, 2023
1 parent 9ff0a44 commit 80f0dc3
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 24 deletions.
35 changes: 19 additions & 16 deletions clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -22,10 +22,8 @@
#include "llvm/ADT/DenseSet.h"
#include "llvm/ADT/MapVector.h"
#include "llvm/ADT/STLExtras.h"
#include "llvm/Support/Casting.h"
#include "llvm/Support/ErrorHandling.h"
#include <cassert>
#include <memory>
#include <utility>

namespace clang {
Expand All @@ -50,6 +48,23 @@ llvm::DenseMap<K, V> intersectDenseMaps(const llvm::DenseMap<K, V> &Map1,
return Result;
}

// Whether to consider equivalent two values with an unknown relation.
//
// FIXME: this function is a hack enabling unsoundness to support
// convergence. Once we have widening support for the reference/pointer and
// struct built-in models, this should be unconditionally `false` (and inlined
// as such at its call sites).
static bool equateUnknownValues(Value::Kind K) {
switch (K) {
case Value::Kind::Integer:
case Value::Kind::Pointer:
case Value::Kind::Record:
return true;
default:
return false;
}
}

static bool compareDistinctValues(QualType Type, Value &Val1,
const Environment &Env1, Value &Val2,
const Environment &Env2,
Expand All @@ -66,18 +81,7 @@ static bool compareDistinctValues(QualType Type, Value &Val1,
case ComparisonResult::Different:
return false;
case ComparisonResult::Unknown:
switch (Val1.getKind()) {
case Value::Kind::Integer:
case Value::Kind::Pointer:
case Value::Kind::Record:
// FIXME: this choice intentionally introduces unsoundness to allow
// for convergence. Once we have widening support for the
// reference/pointer and struct built-in models, this should be
// `false`.
return true;
default:
return false;
}
return equateUnknownValues(Val1.getKind());
}
llvm_unreachable("All cases covered in switch");
}
Expand Down Expand Up @@ -167,8 +171,7 @@ static Value &widenDistinctValues(QualType Type, Value &Prev,
if (auto *W = Model.widen(Type, Prev, PrevEnv, Current, CurrentEnv))
return *W;

// Default of widening is a no-op: leave the current value unchanged.
return Current;
return equateUnknownValues(Prev.getKind()) ? Prev : Current;
}

// Returns whether the values in `Map1` and `Map2` compare equal for those
Expand Down
10 changes: 2 additions & 8 deletions clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -3964,10 +3964,7 @@ TEST(TransferTest, LoopDereferencingChangingPointerConverges) {
}
}
)cc";
// FIXME: Implement pointer value widening to make analysis converge.
ASSERT_THAT_ERROR(
checkDataflowWithNoopAnalysis(Code),
llvm::FailedWithMessage("maximum number of iterations reached"));
ASSERT_THAT_ERROR(checkDataflowWithNoopAnalysis(Code), llvm::Succeeded());
}

TEST(TransferTest, LoopDereferencingChangingRecordPointerConverges) {
Expand All @@ -3989,10 +3986,7 @@ TEST(TransferTest, LoopDereferencingChangingRecordPointerConverges) {
}
}
)cc";
// FIXME: Implement pointer value widening to make analysis converge.
ASSERT_THAT_ERROR(
checkDataflowWithNoopAnalysis(Code),
llvm::FailedWithMessage("maximum number of iterations reached"));
ASSERT_THAT_ERROR(checkDataflowWithNoopAnalysis(Code), llvm::Succeeded());
}

TEST(TransferTest, DoesNotCrashOnUnionThisExpr) {
Expand Down

0 comments on commit 80f0dc3

Please sign in to comment.