‹ XCSG解説集

XCSG解説集 — 制御フロー

制御フローを表す XCSG スキーマの部分です。対象は、文、条件、ループ、およびそれらを使うクエリです。

解説集の索引はこちらをご覧下さい。

この記事では、制御フローに関連する XCSG スキーマの部分を取り上げます。

Atlas が、Xinu/sys/dswrite.c の文 dskenq(drptr, devptr->dvioblk) に XCSG.ControlFlow_Node、XCSG.Language.C、XCSG.ModelElement、XCSG.Node のタグを付けて表示している詳細です。
  • XCSG.ControlFlow_Node: コード中の実行可能な文を表すノードです。Atlas は、基本ブロックを 1 つのノードとするのではなく、個々の文をノードとして表すことを選び、制御フロー解析をより細かい粒度で行えるようにしています。
  • XCSG.ControlFlow_Edge: Frances Allen が定義した後続関係を表すエッジです。2 つの XCSG.ControlFlow_Node を a->b で結びます。ある実行の振る舞いにおいて、b は a の後に実行されます。
  • XCSG.controlFlowRoot: 関数内で最初に実行される文を表す XCSG.ControlFlow_Node です。すべての関数は、一意の XCSG.controlFlowRoot ノードを持ちます。
  • XCSG.controlFlowExit: 関数内の return 文の 1 つを表す XCSG.ControlFlow_Node です。

クエリの例:

var cfg = <function>.contained().nodes(XCSG.ControlFlow_Node).induce(universe.edges(XCSG.ControlFlow_Edge))

このクエリは、関数 '<function>' の制御フローグラフ(CFG)を計算します。

条件文のタグと属性を見ていきます。

  • XCSG.ControlFlowCondition: 条件文を表す XCSG.ControlFlow_Node です。
  • XCSG.ControlFlowIfCondition: IF 文を表す XCSG.ControlFlowCondition ノードです。
  • XCSG.ControlFlowSwitchCondition: Switch 文を表す XCSG.ControlFlowCondition ノードです。
  • XCSG.conditionValue: XCSG.ControlFlowCondition ノードの出エッジを表す XCSG.ControlFlow_Edge が持つ属性です。名前が示すとおり、この属性は、実行時にそのエッジが選ばれるときに XCSG.ControlFlowCondition ノードが捕捉した条件の値を表します。IF 文からの出エッジでは、値は true または false のいずれかです。switch 文では、出エッジのヘッドが表す文の case 値を表します。

クエリの例:

var num_conditions = <cfg>.nodes(XCSG.ControlFlowCondition).eval().nodes().size()

このクエリは、与えられた cfg に含まれる条件文の数を数えます。IF 文だけ、または Switch 文だけを数えるには、XCSG.ControlFlowCondition を XCSG.ControlFlowIfCondition または XCSG.ControlFlowSwitchCondition に置き換えることができます。

var trueEdges = <condition>.out().selectEdge(XCSG.conditionValue,"true")

このクエリは、与えられた '<condition>' について、「true」のエッジだけを表すエッジの集合を返します。この集合を使うと、条件が true であることに対応する特定の実行パスだけをシミュレートできます。用途に応じて、パスセンシティブな解析器を書くためにも使えます。

ループ関連のタグを見ていきます。

  • XCSG.Loop: ループヘッダを表す XCSG.ControlFlow_Node です。そのループが while ループまたは for ループである場合は、XCSG.ControlFlowCondition ノードでもあります。
  • XCSG.DoWhileLoop: do-while ループを表す XCSG.Loop ノードです。while 文には、XCSG.ControlFlowCondition のタグが付きます。
  • XCSG.LoopChild: XCSG.Loop ノードと XCSG.ControlFlow_Node とを結ぶエッジ a->b です。b は a のループ本体の一部です。b も XCSG.Loop ノードである場合、このエッジはループの入れ子関係を捉えます。

クエリの例:

var nested_loops = <cfg>.nodes(XCSG.Loop).induce(universe.edges(XCSG.LoopChild))

このクエリは、与えられた '<cfg>' 内のループの入れ子構造を捉えた部分グラフを返します。

制御フロー文の特別な種類を見ていきます。

  • XCSG.GotoStatement: Goto 文を表す XCSG.ControlFlow_Node です。
  • XCSG.Break: break 文を表す XCSG.ControlFlow_Node です。
  • XCSG.Continue: continue 文を表す XCSG.ControlFlow_Node です。

クエリの例:

var num_gotos = universe.nodes(XCSG.GotoStatement).eval().nodes().size()

このクエリは、インデックスされたコードベース全体に含まれる goto 文の数を数えます。数え上げの対象を特定のファイルまたは関数に限る場合は、universe を、そのファイルまたは関数を表すノードに置き換えてください。

これで、XCSG スキーマにおける制御フロー関連の概念の簡潔な概要は終わりです。

ご質問、または修正のご希望はありますか?

どのようなご用件ですか?