LeavaTailの日記

LeavaTailの日記

Linuxエンジニアを目指した技術者の備忘録

Linuxカーネルに対して静的解析ツールSparseの実行方法

Linux Linux/Sparse

概要

本記事では、Ubuntu 22.04でSparseをビルドし、Linux kernel v6.3 に実行する手順を確認した。

はじめに

Linuxカーネルは、主にC言語とアセンブリ言語によって記述された巨大なオープンソースソフトウェアのプロジェクトの一つである。 そのソースコードの行数は2000万行を超えており、大勢のエンジニアが開発に携わっている。

こういったこともあり、人力でソースコードの品質を担保することが非常に難しい。
そこでLinuxカーネルでは、開発ツールを多くサポートしている。

www.kernel.org

本稿では、この中から静的解析ツール Sparse に注目して、実行時間を比較してみる。

実験環境

本記事で使用した開発用PC (Host PC)の構成は次の通りとなっている。

環境 概要
CPU AMD Ryzen 3 3300X
RAM DDR4-2666 16GB ×2
Storage WDS500G2B0B
Target kernel v6.3
Kconfig x86_64_defconfig
Docker image Ubuntu 22.04

インストール

Sparse は C言語プログラムの軽量かつシンプルな静的解析ツールの一つである。
Sparse では、型チェックやロックチェック、値の範囲チェックといった検査をする。

sparse.docs.kernel.org

Sparseのソースコードはgitで管理されているため、Sparseの最新バージョンをビルドし、インストールする。

  1. 必要なパッケージをインストールする。

     leava@sparse:/work/# apt install gcc make libsqlite3-dev libxml2-dev libgtk-3-dev llvm g++ pkg-config

  2. Sparseのソースコードを手元にダウンロードする。

     leava@sparse:/work/$ git clone git://git.kernel.org/pub/scm/devel/sparse/sparse.git

  3. Sparseをビルドする。

     leava@sparse:/work/# cd sparse
 leava@sparse:/work/sparse/# make

  4. Sparseを/usr/local/bin以下にインストールする。

     leava@sparse:/work/sparse/# PREFIX=/usr/local make install

実行方法

Linuxカーネルでは、sparseを実行できるようにMakefileが修正されている。 ここでは、このフレームワークを利用してSparseを実行する。

    leava@sparse:/work/sparse/# cd ../linux
    leava@sparse:/work/linux/# make C=1 CHECK="/usr/local/bin/sparse" -j"$(nproc)" 2> sparse.log

Sparseでは、問題がありそうな箇所をファイル名と行番号と共に出力する。

    leava@sparse:/work/linux/# grep fs/ext4 check.log
    leava@sparse:/work/linux/# fs/ext4/mballoc.c:2942:13: warning: context imbalance in 'ext4_mb_seq_structs_summary_start' - wrong count at exit
注意

False Posittiveの可能性もあるため、内容は確認しておくこと。

また C=2とすることで、再コンパイルが必要かどうか関係なく sparseによるチェックをする。

    leava@sparse:/work/linux/# make C=2 CHECK="/usr/local/bin/sparse" -j"$(nproc)" 2> sparse2.log

実験結果

GNU timeコマンドを利用して、実行時間を同様ツールの Smatch と比較する。

    leava@sparse:/work/linux/# usr/bin/time -v make C=2 CHECK="/usr/local/bin/sparse" > /dev/null
    leava@sparse:/work/linux/# usr/bin/time -v make C=2 CHECK="/usr/local/bin/smatch -p=kernel" > /dev/null

それぞれ、ジョブ数 (-j) を 1, 4,8 にしたときの実行時間は次の通りとなった。

Sparse と Smatch の実行時間の比較

ここで、赤線はカーネルをビルドするときにかかった時間を参考として示している。

おわりに

本稿では、Sparseを実行する手順について確認した。

SparseはLinux kernel のパッチ投稿チェックリストにも記載されており、また同様のツールSmatchと比較しても軽量であるので、一度使ってみるのもよいと思う。

変更履歴

  • 2023/5/3: 記事公開

参考文献