Clangの静的解析コードであるCheckerのひとつ、ArrayBoundCheckerV2を試し てみる。
1. Checkerの実行方法
$ clang -cc1 -analyzer-checker=alpha.security.ArrayBoundV2 \ -analyze <target>.c
2. 実装
Locationを継承し、checkLocationを実装している。
class ArrayBoundCheckerV2 :
public Checker<check::Location> {
<snip>
public:
void checkLocation(SVal l, bool isLoad, const Stmt*S,
CheckerContext &C) const;
};
checkLocationの説明は以下。
/// rief Called on a load from and a store to a location.
///
/// The method will be called each time a location (pointer) value is
/// accessed.
/// \param Loc The value of the location (pointer).
/// \param IsLoad The flag specifying if the location is a store or a load.
/// \param S The load is performed while processing the statement.
///
/// check::Location
void checkLocation(SVal Loc, bool IsLoad, const Stmt *S,
CheckerContext &) const {}
私が試した単純なソースコードだと、LocはSValの派生クラスである loc::MemRegionValが設定されていた。配列かmallocかで、MemRegionが持つ SuperRegionに違いが出てくる。
2.1. SVal
特にcheckLocationの場合、SValにアクセスすることで、配列のベースアドレ スや配列のオフセット値を取得することができる。加えて、SValBuilderを用 いることで任意の算術演算を施したSValも扱うことができる。
2.2. MemRegion
SValがloc::MemRegionValの場合はMemRegionを持つ。特にarray[1]や*p等のオ フセットを伴うSValの場合はElementRegionとなり、SuperRegionに配列のベー スアドレスを示すMemRegionを持つ。ただし、pがmallocで得た領域を指す場合 はSuperRegionにSymbolicRegionを持つようだ。
3. SValCheckerの作成
SValの内容、特にオフセット値を確認する為にcheckLocationを用いたChecker を作成する。
3.1. Checkerの内容
namespace {
class SValChecker : public Checker<check::Location> {
public:
void checkLocation(SVal Loc, bool IsLoad, const Stmt *S,
CheckerContext &ctx) const;
};
}
<snip>
void SValChecker::checkLocation(SVal Loc, bool IsLoad, const Stmt *S,
CheckerContext &ctx) const {
# Stmtの内容を表示、Locの範囲を~で表示
debug_stmt(S, ctx.getSourceManager());
# IsLoadの内容を表示
debug(IsLoad);
# Locの内容を表示
debug_sval(&Loc);
# ArrayBoundCheckerV2のcomputeOffset相当の処理でオフセットを算出して
# 表示
SVal offset = get_offset(Loc, ctx);
debug_sval(&offset);
}
void ento::registerSValChecker(CheckerManager &mgr) {
mgr.registerChecker<SValChecker>();
}
SVal表示関数は以下の通り。BaseKindとClassの種類を表示し、 nonloc::ConcreteIntの場合はオフセット値を表示する。MemRegionを持つ場合 はMemRegionのClassを表示する。そのMemRegionのSuperRegionを再帰的に表示 する。
static void __debug_region(const SubRegion *region, unsigned indent);
static void __debug_region(const MemRegion *region, unsigned indent = 0)
{
for (unsigned i = 0; i < indent; ++i)
llvm::errs() << ' ';
# 派生クラスとgetString()の内容を表示する。
llvm::errs() << "Class = " << getClass(region) << ", "
<< "String = " << region->getString() << "\n";
__debug_region(dyn_cast<SubRegion>(region), indent);
}
static void __debug_region(const SubRegion *region, unsigned indent = 0)
{
# SuperRegionの内容を再帰的に表示する。
if (region)
__debug_region(region->getSuperRegion(), indent + 2);
}
static void __debug_sval(const nonloc::ConcreteInt *sval)
{
# nonlocl::ConcreteIntの場合はオフセット値を表示する
llvm::errs() << "Offset = ";
if (sval->getValue().isUnsigned())
llvm::errs() << sval->getValue().getZExtValue();
else
llvm::errs() << sval->getValue().getSExtValue();
llvm::errs() << "\n";
}
static void __debug_sval(const SVal *sval)
{
# BaseKindと派生クラスの内容を表示する。
llvm::errs() << "BaseKind = " << getBaseKind(sval) << ", "
<< "Class = " << getClass(sval) << "\n";
if (sval->getAs<nonloc::ConcreteInt>() != None)
{
const nonloc::ConcreteInt __sval = (*sval).castAs<nonloc::ConcreteInt>();
__debug_sval(&__sval);
}
# MemRegionを表示する。
if (sval->getAsRegion())
__debug_region(sval->getAsRegion());
}
3.2. llvm/tools/clang/lib/StaticAnalyzer/Checkers/Checkers.td
$ svn diff Checkers.td Index: Checkers.td =================================================================== --- Checkers.td (revision 201037) +++ Checkers.td (working copy) @@ -255,6 +255,10 @@ HelpText<"Warn about buffer overflows (newer checker)">, DescFile<"ArrayBoundCheckerV2.cpp">; +def SValChecker : Checker<"SValChecker">, + HelpText<"SValChecker">, + DescFile<"SValChecker.cpp">; + def ReturnPointerRangeChecker : Checker<"ReturnPtrRange">, HelpText<"Check for an out-of-bound pointer being returned to callers">, DescFile<"ReturnPointerRangeChecker.cpp">;
3.3. llvm/tools/clang/lib/StaticAnalyzer/Checkers/CMakeLists.txt
$ svn diff CMakeLists.txt Index: CMakeLists.txt =================================================================== --- CMakeLists.txt (revision 201037) +++ CMakeLists.txt (working copy) @@ -12,6 +12,7 @@ AnalyzerStatsChecker.cpp ArrayBoundChecker.cpp ArrayBoundCheckerV2.cpp + SValChecker.cpp BasicObjCFoundationChecks.cpp BoolAssignmentChecker.cpp BuiltinFunctionChecker.cpp
4. SValCheckerの実行結果
4.1. 対象コード（一次元配列）
以下のコードに対してCheckerを実行する。
$ cat array1.c
#include <stdio.h>
int main(void)
{
char array1[] = {1, 2, 3, 4, 5};
char array2[] = {-1, -2, -3, -4, -5};
char *arrays[] = { array1, array2 };
char **p;
char *q;
p = arrays;
q = &p[0][2];
*q++ = 0;
*q = 0;
return 0;
}
4.2. 実行結果（一次元配列）
pを示すSValを補足。MemRegionのClassはVarRegion。オフセット値は0。
checkLocation(253): p = arrays; ~ checkLocation(254): IsLoad = 0 checkLocation(255): &Loc BaseKind = SVal::LocKind, Class = loc::MemRegionVal Class = VarRegion, String = p Class = StackLocalsSpaceRegion, String = StackLocalsSpaceRegion checkLocation(257): &offset BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt Offset = 0
pを示すSvalを補足。MemRegionのClassはVarRegion。オフセット値は0。
checkLocation(253):
q = &p[0][4];
~
checkLocation(254): IsLoad = 1
checkLocation(255): &Loc
BaseKind = SVal::LocKind, Class = loc::MemRegionVal
Class = VarRegion, String = p
Class = StackLocalsSpaceRegion, String = StackLocalsSpaceRegion
checkLocation(257): &offset
BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt
Offset = 0
p[]を示すSValを補足。Clang/LLVMのExpressionの評価順が見えて興味深い。 MemRegionのClassはElementRegion。オフセット値は0。
checkLocation(253):
q = &p[0][4];
~~~~
checkLocation(254): IsLoad = 1
checkLocation(255): &Loc
BaseKind = SVal::LocKind, Class = loc::MemRegionVal
Class = ElementRegion, String = element{arrays,0 S32b,char *}
Class = VarRegion, String = arrays
Class = StackLocalsSpaceRegion, String = StackLocalsSpaceRegion
checkLocation(257): &offset
BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt
Offset = 0
qを示すSValを補足。
checkLocation(253): q = &p[0][4]; ~ checkLocation(254): IsLoad = 0 checkLocation(255): &Loc BaseKind = SVal::LocKind, Class = loc::MemRegionVal Class = VarRegion, String = q Class = StackLocalsSpaceRegion, String = StackLocalsSpaceRegion checkLocation(257): &offset BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt Offset = 0
qを示すSValを補足。
checkLocation(253): *q++ = 0; ~ checkLocation(254): IsLoad = 1 checkLocation(255): &Loc BaseKind = SVal::LocKind, Class = loc::MemRegionVal Class = VarRegion, String = q Class = StackLocalsSpaceRegion, String = StackLocalsSpaceRegion checkLocation(257): &offset BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt Offset = 0
*qを示すSValを補足。ここでオフセット値が2になっていない（不思議）。
checkLocation(253): *q++ = 0; ~~ checkLocation(254): IsLoad = 0 checkLocation(255): &Loc BaseKind = SVal::LocKind, Class = loc::MemRegionVal Class = VarRegion, String = q Class = StackLocalsSpaceRegion, String = StackLocalsSpaceRegion checkLocation(257): &offset BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt Offset = 0
*q++を示すSValを補足。ここでようやくオフセット値が4になっている。また、 SuperRegionはarray1を指していることが分かる。
checkLocation(253):
*q++ = 0;
~~~
checkLocation(254): IsLoad = 0
checkLocation(255): &Loc
BaseKind = SVal::LocKind, Class = loc::MemRegionVal
Class = ElementRegion, String = element{array1,4 S32b,char}
Class = VarRegion, String = array1
Class = StackLocalsSpaceRegion, String = StackLocalsSpaceRegion
checkLocation(257): &offset
BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt
Offset = 4
qを示すSValを補足。
checkLocation(253): *q = 0; ~ checkLocation(254): IsLoad = 1 checkLocation(255): &Loc BaseKind = SVal::LocKind, Class = loc::MemRegionVal Class = VarRegion, String = q Class = StackLocalsSpaceRegion, String = StackLocalsSpaceRegion checkLocation(257): &offset BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt Offset = 0
*qを示すSValを補足。*q++の場合と異なり、*qの段階でオフセット値は5になっ ている。
checkLocation(253):
*q = 0;
~~
checkLocation(254): IsLoad = 0
checkLocation(255): &Loc
BaseKind = SVal::LocKind, Class = loc::MemRegionVal
Class = ElementRegion, String = element{array1,5 S32b,char}
Class = VarRegion, String = array1
Class = StackLocalsSpaceRegion, String = StackLocalsSpaceRegion
checkLocation(257): &offset
BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt
Offset = 5
4.3. 対象コード（二次元配列）
$ cat array2.c
#include <stdio.h>
int main(void)
{
char arrays[][3] = { {1, 2, 3}, {-1, -2, -3} };
char *p;
p = &arrays[1][3];
*p = 0;
return 0;
}
4.4. 実行結果（二次元配列）
オフセット値はきちんと算出できている。
checkLocation(253):
p = &arrays[1][3];
~
checkLocation(254): IsLoad = 0
checkLocation(255): &Loc
BaseKind = SVal::LocKind, Class = loc::MemRegionVal
Class = VarRegion, String = p
Class = StackLocalsSpaceRegion, String = StackLocalsSpaceRegion
checkLocation(257): &offset
BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt
Offset = 0
checkLocation(253):
*p = 0;
~
checkLocation(254): IsLoad = 1
checkLocation(255): &Loc
BaseKind = SVal::LocKind, Class = loc::MemRegionVal
Class = VarRegion, String = p
Class = StackLocalsSpaceRegion, String = StackLocalsSpaceRegion
checkLocation(257): &offset
BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt
Offset = 0
checkLocation(253):
*p = 0;
~~
checkLocation(254): IsLoad = 0
checkLocation(255): &Loc
BaseKind = SVal::LocKind, Class = loc::MemRegionVal
Class = ElementRegion, String = element{element{arrays,1 S32b,char [3]},3 S32b,char}
Class = ElementRegion, String = element{arrays,1 S32b,char [3]}
Class = VarRegion, String = arrays
Class = StackLocalsSpaceRegion, String = StackLocalsSpaceRegion
checkLocation(257): &offset
BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt
Offset = 6
4.5. 対象コード（malloc）
mallocを使用した場合も確認する。
$ cat malloc.c
#include <stdio.h>
#include <stdlib.h>
int main(void)
{
char *buffer = malloc(3);
char *p;
if (!buffer)
return 1;
p = &buffer[3];
*p = 0;
free(buffer);
return 0;
}
4.6. 実行結果（malloc）
Offset = 3と表示され、オフセット値を算出できていることが確認できる。 mallocで確保した領域がSymbolicRegionとなっている。
checkLocation(253):
if (!buffer)
~
checkLocation(254): IsLoad = 1
checkLocation(255): &Loc
BaseKind = SVal::LocKind, Class = loc::MemRegionVal
Class = VarRegion, String = buffer
Class = StackLocalsSpaceRegion, String = StackLocalsSpaceRegion
checkLocation(257): &offset
BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt
Offset = 0
checkLocation(253):
p = &buffer[3];
~
checkLocation(254): IsLoad = 1
checkLocation(255): &Loc
BaseKind = SVal::LocKind, Class = loc::MemRegionVal
Class = VarRegion, String = buffer
Class = StackLocalsSpaceRegion, String = StackLocalsSpaceRegion
checkLocation(257): &offset
BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt
Offset = 0
checkLocation(253):
p = &buffer[3];
~
checkLocation(254): IsLoad = 0
checkLocation(255): &Loc
BaseKind = SVal::LocKind, Class = loc::MemRegionVal
Class = VarRegion, String = p
Class = StackLocalsSpaceRegion, String = StackLocalsSpaceRegion
checkLocation(257): &offset
BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt
Offset = 0
checkLocation(253):
*p = 0;
~
checkLocation(254): IsLoad = 1
checkLocation(255): &Loc
BaseKind = SVal::LocKind, Class = loc::MemRegionVal
Class = VarRegion, String = p
Class = StackLocalsSpaceRegion, String = StackLocalsSpaceRegion
checkLocation(257): &offset
BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt
Offset = 0
checkLocation(253):
*p = 0;
~~
checkLocation(254): IsLoad = 0
checkLocation(255): &Loc
BaseKind = SVal::LocKind, Class = loc::MemRegionVal
Class = ElementRegion, String = element{SymRegion{conj_$1{void *}},3 S32b,char}
Class = SymbolicRegion, String = SymRegion{conj_$1{void *}}
Class = NULL, String = UnknownSpaceRegion
checkLocation(257): &offset
BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt
Offset = 3
checkLocation(253):
free(buffer);
~
checkLocation(254): IsLoad = 1
checkLocation(255): &Loc
BaseKind = SVal::LocKind, Class = loc::MemRegionVal
Class = VarRegion, String = buffer
Class = StackLocalsSpaceRegion, String = StackLocalsSpaceRegion
checkLocation(257): &offset
BaseKind = SVal::NonLocKind, Class = nonloc::ConcreteInt
Offset = 0
5. ArrayBoundCheckerV2の内容
ArrayBoundCheckerV2の概要を#でコメント記述する。
5.1. RegionRawOffsetV2
大元となる変数のアドレスとオフセット値を管理するクラス。
class RegionRawOffsetV2 {
private:
# baseRegionに大元となる変数のアドレスが設定され、byteOffsetに
# オフセット値が設定される。array[3]の場合、baseRegionにarray、
# byteOffsetに[3]のオフセット値を表すSValが設定される。
const SubRegion *baseRegion;
SVal byteOffset;
RegionRawOffsetV2()
: baseRegion(0), byteOffset(UnknownVal()) {}
public:
# 予めcomputeOffset等でbaseRegionとbyteOffsetを計算しておく。
RegionRawOffsetV2(const SubRegion* base, SVal offset)
: baseRegion(base), byteOffset(offset) {}
NonLoc getByteOffset() const { return byteOffset.castAs<NonLoc>(); }
const SubRegion *getRegion() const { return baseRegion; }
static RegionRawOffsetV2 computeOffset(ProgramStateRef state,
SValBuilder &svalBuilder,
SVal location);
<snip>
};
}
5.2. SValBuilder
SValBuilderを用いることで二項演算結果を施したSVal等を作成する。以下の scaleValueではSValBuilderを用いて型サイズを考慮したオフセット値を持つ SValを返す。char array[5]ならbaseValに5、scalingにsizeof(char)が設定さ れて本メソッドが呼ばれる。
// Scale a base value by a scaling factor, and return the scaled
// value as an SVal. Used by 'computeOffset'.
static inline SVal scaleValue(ProgramStateRef state,
NonLoc baseVal, CharUnits scaling,
SValBuilder &sb) {
# makeArrayIndexでscaling.getQuantity()のサイズを持つSValを生成する。
# evalBinOpNNでbaseValとmakeArrayIndexで生成したSvalを掛けた結果の
# SValを生成する。
return sb.evalBinOpNN(state, BO_Mul, baseVal,
sb.makeArrayIndex(scaling.getQuantity()),
sb.getArrayIndexType());
}
5.3. computeOffset
オフセット値を算出するメソッド。ElementRegionの場合にgetIndex()メソッ ドでオフセット値のSValを取得し、SValBuilderを用いてsizeof(char)のかけ 算と、それまでに割り出したオフセット値計算との足し算を実行している。
RegionRawOffsetV2 RegionRawOffsetV2::computeOffset(ProgramStateRef state,
SValBuilder &svalBuilder,
SVal location)
{
const MemRegion *region = location.getAsRegion();
SVal offset = UndefinedVal();
while (region) {
switch (region->getKind()) {
default: {
# baseRegionにregion、byteOffsetにoffsetをセットした
# RegionRawOffsetV2を返す。
<snip>
}
case MemRegion::ElementRegionKind: {
# array[5]等はここにくる。sizeof(char) * 5をoffsetにセットする。
# getSuperRegion()でarrayを取得し、regionにセットする。
<snip>
}
}
}
return RegionRawOffsetV2();
}
5.4. checkLocation
下限値、上限値、オフセット値をSValで扱い、その比較結果もSValで扱う。比 較結果のSValをProgramStateのassumeメソッドで評価し、下限を下回る場合、 あるいは上限を上回る場合にwarning出力する。オフセット値がtaintedな値の 場合にもwarningを出力する。
void ArrayBoundCheckerV2::checkLocation(SVal location, bool isLoad,
const Stmt* LoadS,
CheckerContext &checkerContext) const {
<snip>
ProgramStateRef state = checkerContext.getState();
ProgramStateRef originalState = state;
SValBuilder &svalBuilder = checkerContext.getSValBuilder();
const RegionRawOffsetV2 &rawOffset =
RegionRawOffsetV2::computeOffset(state, svalBuilder, location);
<snip>
# array[1]のarrayを表すSValを設定する。
SVal extentBegin = computeExtentBegin(svalBuilder, rawOffset.getRegion());
if (Optional<NonLoc> NV = extentBegin.getAs<NonLoc>()) {
# （オフセット値 < array）を計算した結果を持つSValを設定する
SVal lowerBound =
svalBuilder.evalBinOpNN(state, BO_LT, rawOffset.getByteOffset(), *NV,
svalBuilder.getConditionType());
Optional<NonLoc> lowerBoundToCheck = lowerBound.getAs<NonLoc>();
if (!lowerBoundToCheck)
return;
# 先ほど計算したSValが真の場合（オフセット値がarrayより前を指して
# いる）と偽の場合（オフセット値がarrayより後を指している）の
# ProgramStateRefを生成する。
ProgramStateRef state_precedesLowerBound, state_withinLowerBound;
llvm::tie(state_precedesLowerBound, state_withinLowerBound) =
state->assume(*lowerBoundToCheck);
# 真の場合のProgramStateRefが有効な場合はreportOOBでwarning出力する。
// Are we constrained enough to definitely precede the lower bound?
if (state_precedesLowerBound && !state_withinLowerBound) {
reportOOB(checkerContext, state_precedesLowerBound, OOB_Precedes);
return;
}
// Otherwise, assume the constraint of the lower bound.
assert(state_withinLowerBound);
state = state_withinLowerBound;
}
do {
// CHECK UPPER BOUND: Is byteOffset >= extent(baseRegion)? If so,
// we are doing a load/store after the last valid offset.
# arrayの定義であるchar array[5]のオフセット上限値を持つSValを設定する。
DefinedOrUnknownSVal extentVal =
rawOffset.getRegion()->getExtent(svalBuilder);
if (!extentVal.getAs<NonLoc>())
break;
# （オフセット値 >= オフセット上限値）の結果を持つSValを生成する。
SVal upperbound
= svalBuilder.evalBinOpNN(state, BO_GE, rawOffset.getByteOffset(),
extentVal.castAs<NonLoc>(),
svalBuilder.getConditionType());
Optional<NonLoc> upperboundToCheck = upperbound.getAs<NonLoc>();
if (!upperboundToCheck)
break;
# 先ほど計算したSValが真の場合と偽の場合のProgramStateRefを生成する。
ProgramStateRef state_exceedsUpperBound, state_withinUpperBound;
llvm::tie(state_exceedsUpperBound, state_withinUpperBound) =
state->assume(*upperboundToCheck);
# オフセット値が不定な場合に真偽が両方成り立ち、reportOOBでwarning出力する。
// If we are under constrained and the index variables are tainted, report.
if (state_exceedsUpperBound && state_withinUpperBound) {
if (state->isTainted(rawOffset.getByteOffset()))
reportOOB(checkerContext, state_exceedsUpperBound, OOB_Tainted);
return;
}
# 真の場合はreportOOBでwarning出力する。
// If we are constrained enough to definitely exceed the upper bound, report.
if (state_exceedsUpperBound) {
assert(!state_withinUpperBound);
reportOOB(checkerContext, state_exceedsUpperBound, OOB_Excedes);
return;
}
assert(state_withinUpperBound);
state = state_withinUpperBound;
}
while (false);
<snip>
}
6. ArrayBoundCheckerV2の実行結果
先ほどの３種類の対象コードに対してArrayBoundCheckerV2を実行する。
6.1. 対象コード（一次元配列）の実行結果
SuperRegionはarray1を指しており、array1の上限値5とオフセット値5が等し くなっている。その結果、warningが出力される。
array1.c:14:6: warning: Out of bound memory access (access exceeds upper limit of memory block) *q = 0; ~~~^~~ 1 warning generated.
6.2. 対象コード（二次元配列）の実行結果
SuperRegionはarraysを指しており、array2の上限値6とオフセット値6が等し くなっている。その結果、warningが出力される。
array2.c:9:6: warning: Out of bound memory access (access exceeds upper limit of memory block) *p = 0; ~~~^~~ 1 warning generated.
p = &arrays[0][3]にした場合はwarning出力されない。
6.3. 対象コード（malloc）の実行結果
オフセット値は3と算出されているが、warningが出力されない。 SymbolicRegionの場合は上限値と下限値が上手く評価されないようだ。
*pを補足した際、下記の下限値を判別するif文がfalseになる。
if (Optional<NonLoc> NV = extentBegin.getAs<NonLoc>()) {
*pを補足した際、上限値を判別処理中のassumeの結果が両方ともNULLになる。 upperboundToCheckが真偽値として成立していないということだろうか？
ProgramStateRef state_exceedsUpperBound, state_withinUpperBound;
llvm::tie(state_exceedsUpperBound, state_withinUpperBound) =
state->assume(*upperboundToCheck);
7. まとめ
SValでオフセット値、配列の上限値と下限値、真偽値を扱えることが確認でき た。malloc領域を指すSymbolicRegionの上限値と下限値を扱う場合は特別なケ アが必要となるようだ。
