Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

手続き間制御フローグラフ(ICFG)

可能であれば、パターンによってバグのカテゴリを排除することは、静的な保証にとって理想的です。 これは、第4章第2節でスタック安全性と MISRA C 17.21(「再帰なし」)を調べたときに見ました。

再帰は、より一般的なケース、つまり任意の静的解析および/または検証ツールにどのような影響を与えるのでしょうか?

技術的には、場合によります。 現実的には、多くの有用なツールは静的な**手続き間制御フローグラフ(ICFG)**を構築する必要があります。 これは、一般的な解析アルゴリズムがその上で実行される「バックボーン」だからです。 また、可能なすべての呼び出しシーケンスを理解することで、可能なすべての実行について判断できることが多いからです。

複雑さが増していく 3 つの ICFG を考えてみます。 まず、第4.2章の MISRA C 17.2 互換の反復プログラムです。

反復プログラムの ICFG - 有向非巡回グラフ(DAG)

  • これは**有向非巡回グラフ(DAG)**です。解析の作者にとって、このグラフは特定のアルゴリズムや可能性を有効にします。

    • 例: トポロジカルソート2。これはタスクの有効なシーケンスを表すために使用できますが、DAG を必要とします。

次に、最初の再帰版(これも 4.2 から)です。

再帰プログラムの ICFG - 有向グラフ(DG)

  • これは**有向グラフ(DG)**です。一部の解析の作者にとっては、問題が難しくなったということです。過剰近似(偽陽性を許容)を強いられたり、保証を緩和したり(より弱い解析)する必要があるかもしれません。

    • 例: プログラムの最悪時スタック使用量の静的計算。

相互再帰もあります。これは、2 つ以上の関数が互いを呼び出すものです。 ここでは、先ほどの再帰版のさらに望ましくないバリエーションと考えることにします。

相互再帰プログラムの ICFG - 有向グラフ(DG)のバリエーション。

DAG と DG の比較は、意図的に曖昧にしています。静的アナライザー全体について何らかの主張を行うことは実際にはできません。おそらく、数百のユースケースに対応する数千もの静的アナライザーが存在します。 しかし、直感を養う助けにはなります。 これらのグラフを走査するロジックを書くことを想像してみてください。DAG は例外的なケースを回避します。

要点

再帰は、実行時のメモリ枯渇だけの問題ではありません。 再帰はプログラムの手続き間制御フローグラフ(ICFG)に影響を与え、一般的に静的解析を妨げます。


  1. MISRA C: 2012 Guidelines for the use of the C language in critical systems (3rd edition). MISRA (2019).

  2. トポロジカルソート. Wikipedia(2023年アクセス)。