読者です 読者をやめる 読者になる 読者になる

combine: マクロのいらないRustのパーサーコンビネーター

はじめに

Rustには有名なnomというパーサーコンビネーターライブラリがあるが、せっかく高級な型システムと最適化があるのにマクロで何とかしようとするのは勿体無いと思うので、マクロに深く依存しないcombineを使ってみた。

combineの主な特徴

  • parsec リスペクトのパーサーコンビネータ
  • コンビネーターはマクロではなく、 Parser traitを実装する値で表す
  • バイトストリーム、文字(Unicodeコードポイント)ストリーム、トークンストリームの全てに対応
  • メモリ上の文字列だけではなく、入力ストリームからの直接のパースにも対応

まだ計測はしていないが、 Box を多用していたりはしないので、速度的に大きく遅れをとるようなことはないのではないかと思う。

以下、parsecについて知っていたほうが読みやすい構成になっているので、必要ならparsecの資料を探して読むといいかもしれない。大雑把に言うと、1つの構文要素を1つの関数(現在位置を受け取って、成功/失敗と次の位置を返す)であらわす再帰下降パーサーというのがベースになっている。その構文解析関数を自力で書かなくても、既存の高階関数を組み合わせて手軽に書けるようにしたのがパーサーコンビネーターである。

基本的な使い方

Cargo.toml の中身

[dependencies]
combine = "2.2.2"
# これは必要なければ削除してもよい
combine-language = "2.0.0"

src/main.rs の中身

extern crate combine;

use combine::{Parser, many1};
use combine::char::digit;

fn main() {
    let mut parser = many1::<Vec<_>, _>(digit());
    println!("{:?}", parser.parse("123"));
    println!("{:?}", parser.parse("123ABC"));
    println!("{:?}", parser.parse("ABC123"));
}

実行結果

Ok((['1', '2', '3'], ""))
Ok((['1', '2', '3'], "ABC"))
Err(ParseError { position: 94191262981061, errors: [Unexpected(Token('A')), Expected(Borrowed("digit"))] })

成功した場合は、パース結果と、残り文字列が返される。

ポイント

次のようにしてパーサーを生成する。これは名前からわかるように数字の1個以上の並びを取得する。

let mut parser = many1(digit());

ここで、 digit() は関数呼び出しだが、ここではパーサーの生成が行われているだけで、この時点でパーサーが実行されているわけではない。

many1 は任意の FromIterator に変換できる。ここでは Vec<_> を使うため、それを明示している。

parsermut でないといけない。これは勿論 parse(&mut self, ... だからだが、これは突き詰めればステートフルなパーサーを書くためだと思われる。

色々組み合わせる

parsecの (>>=)return はそれぞれ .thenvalue という名前になっている。

// 何も読まずに1を返す
let mut parser = value(1);
assert_eq!(parser.parse("123"), Ok((1, "123")));
// 同じ文字2つの並びを読む
let mut parser = letter().then(|c| token(c));
assert_eq!(parser.parse("aa"), Ok(('a', "")));
assert!(parser.parse("11").is_err());
assert!(parser.parse("ab").is_err());

単に、パースした結果を変換したい場合は、 .map を使う。(parsecでいうところの fmap, (<$>))

// 数字の1つ以上の並びをパースして、数値として返す
let mut parser = many1::<String, _>(digit()).map(|s| s.parse::<u32>().unwrap());
assert_eq!(parser.parse("123"), Ok((123, "")));

左を試して、失敗したら右を試すには、.or を使う。 (parsecの (<|>) と同様、左で1文字以上消費して失敗したら右は試さない。)

// 整数をパース
let mut parser =
    token('-')
    .with(many1::<String, _>(digit()).map(|s| -s.parse::<i32>().unwrap()))
    .or(many1::<String, _>(digit()).map(|s| s.parse::<i32>().unwrap()));
assert_eq!(parser.parse("123"), Ok((123, "")));
assert_eq!(parser.parse("-123"), Ok((-123, "")));

上で使われている .with は左の結果を捨てて続けて右を読む (parsecの (*>) ) 。逆に、右の結果を捨てる (parsecの (<*)) ときは .skip を使う。使い方はほぼ同じ。

ポイント

汎用のコンビネーターは combine::combinator にある。また、文字用と後述するバイト用のコンビネーターはそれぞれ combine::charcombine::byte にある。

combine::combinator にあるコンビネーターは以下の方法でも利用できる。

  • combine の直下に同じものがuseされていることがある。
  • combine::Parser にメソッドとして実装されていることがある。メソッドチェーンとして書くのにも使える。

combineのコンビネーターはparsecと同じような感覚で使えるようになっているが、大きな違いが1つある。parsecのパーサー ParsecT s u m a は型コンストラクタである。したがって、例えば「 [Char] を読んで Int を返すパーサー」なら、中身によらず同じ型 Parsec [Char] () Int をもつ。

一方、combineのパーサー Parser はtrait(型クラスのようなもの)である。同じ「 &str を読んで i32 を返すパーサー」でも、パーサーの実装ごとに異なる型をもつ。

異なる実装のパーサーを同じように扱いたいということがもしあるならば、trait objectを使って Box<Parser<Input=&'a str, Output=i32>> のように書くことは可能である。

再利用と再帰

再利用可能なパーサーを書くときは、慣習的には以下の手順を踏む。

  1. そのパーサーをあらわす型を struct で作る。
  2. その実装を impl で書く。
  3. そのパーサーを生成する関数を fn で書く。

例えば、先ほど作成した非負整数パーサーは以下のように書く。

// 非負整数パーサーをあらわす型
struct Unsigned<I>(PhantomData<fn(I) -> I>);

// 非負整数パーサーの実装
impl<I> Parser for Unsigned<I> where I: Stream<Item=char> {
    type Input = I;
    type Output = u32;
    #[inline]
    fn parse_stream(&mut self, input: I) -> ParseResult<Self::Output, Self::Input> {
        // 基本的な書き方: ラップしたいパーサーをその場で生成し、parse_streamを移譲するだけ。
        let mut parser = many1::<String, _>(digit()).map(|s| s.parse::<u32>().unwrap());
        parser.parse_stream(input)
    }
}

// 非負整数パーサーを返す関数
fn unsigned<I>() -> Unsigned<I> where I: Stream<Item=char> {
    Unsigned(PhantomData)
}

これを使うと以下のように整数パーサーを書ける。

// 整数をパース
let mut parser =
    token('-').with(unsigned()).map(|x| -(x as i32))
    .or(unsigned().map(|x| x as i32));
assert_eq!(parser.parse("123"), Ok((123, "")));
assert_eq!(parser.parse("-123"), Ok((-123, "")));

上のような方法を使えば、再帰的なパーサーを書くこともできる。ただし、単に再帰的なパーサーがほしいだけなら、より簡単な方法がある。

parser 関数を使うと、関数やクロージャをパーサーに変換できる。これを使えば、例えば括弧の対応がとれている文字列をパースする以下のようなパーサーが書ける。

// 括弧の対応
fn paren<I>(input: I) -> ParseResult<(), I> where I: Stream<Item=char> {
    let mut parser =
        token('(').with(parser(paren::<I>)).skip(token(')'))
        .or(token('[').with(parser(paren::<I>)).skip(token(']')))
        .or(value(()));
    parser.parse_stream(input)
}

これは以下のように使える。

let mut parser = parser(paren);
assert_eq!(parser.parse("[()]"), Ok(((), "")));
assert!(parser.parse("[(])").is_err());

エラー処理

combineはparsecと似たバックトラック規則を採用している。つまり、

  • 1文字も消費せずに失敗したら、バックトラックする。
  • 1文字以上消費して失敗したら、バックトラックをせずに全体も失敗とする。

したがって以下は失敗する。

// 2AHのような16進数か、20Dのような十進数を受理しようとしている
let mut parser =
    many1::<String, _>(hex_digit()).skip(char('H'))
    .or(many1::<String, _>(digit()).skip(char('D')));
// バックトラックしないため、マッチしない
println!("{:?}", parser.parse("123D"));
Err(ParseError { position: 94623997271456, errors: [Unexpected(Borrowed("end of input")), Expected(Token('H'))] })

この規則の例外が必要な場合は、 try を使う。 try で包まれたパーサーは失敗した場合は1文字も消費しなかったことになる。

// 2AHのような16進数か、20Dのような十進数を受理する
let mut parser =
    try(many1::<String, _>(hex_digit()).skip(char('H')))
    .or(try(many1::<String, _>(digit()).skip(char('D'))));
println!("{:?}", parser.parse("123D"));
Ok(("123", ""))

.expected を使うと、バックトラック時に “Expected …” という形のエラーメッセージを付与できる。しばしば try と併用される (と思われる。)

// 2AHのような16進数か、20Dのような十進数を受理する
let mut parser =
    try(many1::<String, _>(hex_digit()).skip(char('H'))).expected("hexadecimal number")
    .or(try(many1::<String, _>(digit()).skip(char('D'))).expected("decimal number"));
println!("{:?}", parser.parse("123"));
Err(ParseError { position: 94647351694019, errors: [Unexpected(Borrowed("end of input")), Expected(Token('H')), Expected(Token('D')), Unexpected(Token('1')), Expected(Borrowed("hexadecimal number")), Expected(Borrowed("decimal number"))] })

当たり前だが try を増やせばバックトラックが増えるのでパフォーマンスが落ちる可能性がある。あくまで、できるだけ先読みのいらない形でパースするのが望ましいだろう。 try の典型的な利用方法の1つは、字句解析と構文解析がわかれているような言語における「字句」のパーサーであると考えられる。

バイトパーサー

ここまでは、Unicodeのコードポイントごとに処理をするパーサーを扱った。combineでは、文字に限らず、何かが並んでいればそれをパースすることができる。何かの並びは Stream というtraitであらわされる。文字の並びは Stream<Item=char>, バイトの並びは Stream<Item=u8> である。

例えば以下のように &[u8] に対して構文解析を実行できる。

let mut parser =
    many1::<Vec<_>, _>(combine::byte::digit());
assert_eq!(parser.parse(&b"123ABC"[..]), Ok((vec![49, 50, 51], &[65, 66, 67][..])));

ストリームパーサー

combineでは&[u8]&strのように既に全体がメモリ上に読み込まれているもの以外にも、特定の入力ストリームから必要に応じてトークンを読み込むようなパーサーを書くことができる。それには Stream を実装する他の型を使えばよい。

例えば、標準入力のように Read を実装するものに対してバイト単位で構文解析をするには、from_readBufferedStream を使うことができる。

let stdin = std::io::stdin();
let stdin = stdin.lock();
// 先読み10文字
let stdin_stream = BufferedStream::new(from_read(stdin), 10);
let stdin_stream = stdin_stream.as_stream();

// 英数字と空白以外がくるまで読み続ける
let mut parser = many1::<Vec<_>, _>(combine::byte::alpha_num().or(combine::byte::space()));
println!("{:?}", parser.parse(stdin_stream));

実行すると、英数字と空白(改行を含む)がくる間はストリームから読み続ける。それ以外の文字が来た時点で読み込みが停止される。

ポイント

Stream 自体は簡単で、インターフェースを見れば一目瞭然である。しかし実際のストリームパーサーの実装はもう少し複雑である。

まず、 Stream が単に StreamOnce + Clone であることに注意する。また StreamOnceIterator に位置記憶機能がついたものに過ぎない。

StreamOnceRead をラップする (from_read) ことで簡単に実現できる。しかしこれでは Clone が足りない。 Clone が必要なのはもちろん、バックトラックのためである。

そのために、StreamOnce をラップして Stream を作成する一般的な仕組みが提供されている。それが BufferedStream である。

ストリーム本体はもちろん複製できないので、 BufferedStream はストリーム本体の特定位置を参照するだけの簡単なデータ構造としてふるまう。例えば、3つの BufferedStream が同じストリームの位置50, 位置80, 位置110を参照するといったことが考えられる。このとき、ストリーム本体は位置110まで読み込み済みの状態である。

このとき位置50のストリームから読み直したいということがありえる。そのために、ストリーム本体から読み出したデータは共有の先読みバッファに保存される。先読みバッファの自動解放をするにはより複雑な仕組みが必要なので、ここでは固定サイズのバッファを確保しておき、先読みバッファから溢れた部分を読み出そうとした場合はエラーとなる。

Read を使ってバイトストリームではなく文字ストリーム Stream<Item=char> を得るのは少し面倒そうだ。 Read::chars() を参考に自分で実装してしまうほうが楽かもしれない。

トークンパーサー

parsec同様、あまり真面目にサポートされているかというと微妙だが、一度字句解析器がトークン列を生成し、その後で構文解析器がトークン列を解析する、というような実装も可能である。

これも実装方法によって難易度が異なる。「トークン列を一度メモリ上に全部展開する」「位置情報を保持しない」という条件ならそれほど難しくない。

extern crate combine;

use combine::char::{char, digit, spaces};
use combine::{many, many1, Parser, eof, sep_by1, satisfy_map};

#[derive(Debug, Copy, Clone, PartialEq, Eq)]
enum Token {
    Number(u32),
    Plus,
}

fn lex(s: &str) -> Vec<Token> {
    let number = many1::<String, _>(digit()).map(|s| Token::Number(s.parse::<u32>().unwrap()));
    let plus = char('+').map(|_| Token::Plus);
    let mut parser =
        spaces().with(many(number.or(plus).skip(spaces()))).skip(eof());
    parser.parse(s).map(|x| x.0).unwrap()
}

fn eval(s: &str) -> u32 {
    let tokens = lex(s);

    let number = satisfy_map(|t| match t {
        Token::Number(x) => Some(x),
        _ => None,
    });
    let plus = satisfy_map(|t| match t {
        Token::Plus => Some(()),
        _ => None,
    });
    let mut parser = sep_by1::<Vec<_>, _, _>(number, plus).map(|v| v.iter().sum());
    parser.parse(&tokens[..]).unwrap().0
}

fn main() {
    println!("{:?}", lex("1"));
    println!("{:?}", lex(" 1 + 2 "));
    println!("{:?}", lex("100    +    200+323"));
    println!("{:?}", eval("1"));
    println!("{:?}", eval(" 1 + 2 "));
    println!("{:?}", eval("100    +    200+323"));
}

combine-language

combine-languageを使うと、典型的なプログラミング言語のlexerを自動で生成できる。これもparsecのText.Parsec.Tokenと似た機能を提供するものである。

combine-languageを使って簡易的な電卓プログラム(四則演算パーサー)を書くと以下のようになる。

extern crate combine;
extern crate combine_language;

use combine::char::{string, letter, alpha_num};
use combine::{Parser, satisfy, Stream, ParseResult, parser, chainl1};
use combine_language::{LanguageEnv, LanguageDef, Identifier};

#[derive(Debug, Clone, PartialEq, Eq)]
enum Expr {
    Number(i64),
    Plus(Box<Expr>, Box<Expr>),
    Minus(Box<Expr>, Box<Expr>),
    Times(Box<Expr>, Box<Expr>),
    Divides(Box<Expr>, Box<Expr>),
}

fn calc_env<'a, I>() -> LanguageEnv<'a, I> where I: Stream<Item=char>, I: 'a {
    LanguageEnv::new(LanguageDef {
        ident: Identifier {
            start: letter(),
            rest: alpha_num(),
            reserved: ["if", "then", "else", "let", "in", "type"].iter()
                                                                 .map(|x| (*x).into())
                                                                 .collect(),
        },
        op: Identifier {
            start: satisfy(|c| "+-*/".chars().any(|x| x == c)),
            rest: satisfy(|c| "+-*/".chars().any(|x| x == c)),
            reserved: ["+", "-", "*", "/"].iter().map(|x| (*x).into()).collect()
        },
        comment_start: string("/*").map(|_| ()),
        comment_end: string("*/").map(|_| ()),
        comment_line: string("//").map(|_| ()),
    })
}

// 整数または括弧で括られた式
fn factor<I>(input: I) -> ParseResult<Box<Expr>, I> where I: Stream<Item=char> {
    let env = calc_env();
    let number = env.integer().map(|x| Box::new(Expr::Number(x)));
    let parenthesized = env.parens(parser(expr));
    number.or(parenthesized).parse_stream(input)
}

// 掛け算・割り算またはfactor
fn term<I>(input: I) -> ParseResult<Box<Expr>, I> where I: Stream<Item=char> {
    let env = calc_env();
    let op = env.reserved_op("*").or(env.reserved_op("/"))
        .map(|op| move |lhs, rhs| {
        if op == "*" {
            Box::new(Expr::Times(lhs, rhs))
        } else if op == "/" {
            Box::new(Expr::Divides(lhs, rhs))
        } else { unreachable!() }
    });
    chainl1(parser(factor), op)
        .parse_stream(input)
}

// 全ての式
fn expr<I>(input: I) -> ParseResult<Box<Expr>, I> where I: Stream<Item=char> {
    let env = calc_env();
    let op = env.reserved_op("+").or(env.reserved_op("-"))
        .map(|op| move |lhs, rhs| {
        if op == "+" {
            Box::new(Expr::Plus(lhs, rhs))
        } else if op == "-" {
            Box::new(Expr::Minus(lhs, rhs))
        } else { unreachable!() }
    });
    chainl1(parser(term), op)
        .parse_stream(input)
}

fn main() {
    let mut parser = parser(expr);
    println!("{:?}", parser.parse("1 + 2 * 3"));
}

行番号と列番号

行番号や列番号を取得するには、ステートフルな字句解析器を用意するという方法が考えられる。その他に、以下のようにして Stream に1枚噛ませても実装できる。

extern crate combine;

use combine::char::{string, letter, alpha_num, space};
use combine::{Parser, satisfy, Stream, ParseResult, parser, chainl1, StreamOnce, many1, eof};

#[derive(Debug, Clone)]
pub struct CRStream<I> {
    inner: I,
    rownum: usize,
    rowpos: usize,
}

impl<I> CRStream<I> where I: Stream<Item=char, Position=usize> {
    pub fn new(inner: I) -> Self {
        let rowpos = inner.position();
        CRStream {
            inner: inner,
            rownum: 0,
            rowpos: rowpos,
        }
    }
}

impl<I> StreamOnce for CRStream<I> where I: Stream<Item=char, Position=usize> {
    type Item = I::Item;
    type Range = I::Range;
    type Position = (usize, usize);
    fn uncons(&mut self) -> Result<Self::Item, combine::primitives::Error<Self::Item, Self::Range>> {
        let c = try!(self.inner.uncons());
        if c == '\n' {
            self.rownum += 1;
            self.rowpos = self.inner.position();
        }
        Ok(c)
    }
    fn position(&self) -> Self::Position {
        (self.rownum, self.inner.position() - self.rowpos)
    }
}

fn main() {
    // 英数字と空白のみからなる文字列を受理する
    let mut parser = many1::<Vec<_>, _>(alpha_num().or(space())).skip(eof());
    println!("{:?}", parser.parse("hoge"));
    println!("{:?}", parser.parse("hoge+fuga"));
    println!("{:?}", parser.parse("h\nge+fuga"));

    // 英数字と空白のみからなる文字列を受理する
    let mut parser = many1::<Vec<_>, _>(alpha_num().or(space())).skip(eof());
    println!("{:?}", parser.parse(CRStream::new("hoge")));
    println!("{:?}", parser.parse(CRStream::new("hoge+fuga")));
    println!("{:?}", parser.parse(CRStream::new("h\nge+fuga")));
}

PositionOrd を実装することに注意すること。ここでは (row, column) を返しているが、タプルの順序は辞書順であるため、この Ord 構造は構文解析の向きと整合している。

まとめ

combineは、parsecのような利便性・汎用性と、Rustのライブラリに求められるゼロ抽象化を両立しようとしている。Rustの強力な型システムをうまく活用することで、これらは十分に実現できているように思う。

一方で、parsecに比べて不便な点や、現時点で必要なインターフェースが不足している点も感じられた。また、型エラーの解決は決して簡単ではない。Rustの型システムに慣れていなければなおさら躓きやすいかもしれない。

個人的には、マクロを駆使している nom よりも好印象であった。

OCamlのformat (型安全なprintf/scanf) の仕組み

OCamlPervasives (デフォルトでopenされるモジュール) には、Printf/Format/Scanfで使うための format という型がある。

OCamlの特殊機能として、型推論時に文字列リテラルstringではなくformatという型がつくことがある。

$ ocaml
        OCaml version 4.04.0+dev2-2016-04-27

# "%d";;
- : string = "%d"
# ("%d" : _ format);;
- : (int -> 'a, 'b, 'a) format =
CamlinternalFormatBasics.Format
 (CamlinternalFormatBasics.Int (CamlinternalFormatBasics.Int_d,
   CamlinternalFormatBasics.No_padding,
   CamlinternalFormatBasics.No_precision,
   CamlinternalFormatBasics.End_of_format),
 "%d")

内部表現はさておき、これには (int -> 'a, 'b, 'a) format という型がついている。このような型がつく条件は文脈からこれがformatだとわかる場合で、上記のように明示した場合、Pervasives.format_of_stringを使った場合*1、そしてPrintf.printfなど実際にフォーマットを使う関数の引数に置いた場合などである。

format についている3つの型引数がポイントで、これの組み合わせにより、型安全なprintf/scanfを実現している。

3引数のformat (型安全なフォーマット入出力のための基本的な枠組み)

3引数の format は次のような形をしている。

('a, 'b, 'c) format

この 'a, 'b, 'c が型変数であり、使われる場面に応じて様々な型が入る。

この中で説明が最も簡単なのは 'b である。ここには入出力先のチャンネルを表すための型が入る。例えば、

  • Printf.fprintf の場合、 out_channel (出力先チャンネル)
  • Format.fprintf の場合、 Format.formatter (フォーマッタ)
  • Printf.sprintfFormat.sprintf の場合、 unit (特に出力先はない)
  • Printf.bprintfFormat.bprintf の場合、 Buffer.t (バッファ)

などとなる。

いっぽう、 'a'c は連携して仕事をこなす。'aは(Curry化された)多引数関数で、その戻り値が'cと一致するように設定する。'aの引数の個数は%フォーマットが必要とする引数の個数に他ならない。例えば、

"Hello" : ('a, 'b, 'a) format
"Number: %d" : (int -> 'a, 'b, 'a) format
"%d (%s)" : (int -> string -> 'a, 'b, 'a) format

上記のように、各文字列リテラルの型は、('a, 'b, 'c)の一部が埋められているが、一部に変更の余地が残されている。第1引数と第3引数に共通の 'a という型変数が使われているので、第1引数と第3引数の型も連動して変化する。

この仕組みにより、「フォーマットの個数だけの引数を受け取る関数」というのをうまく書くことができる。例えば、

val Printf.fprintf : out_channel -> ('a, out_channel, unit) format -> 'a
val Printf.sprintf : ('a, unit, string) format -> 'a

の2つを考える。ここで、Printf.fprintf stdout "%d %s"の型はどうなるか。

  • Printf.fprintf の第2引数の型は ('a, out_channel, unit) format である。
  • "%d %s" の型は (int -> string -> 'c, 'b, 'c) format である。(変数名は適当に付け替えた)
  • 上記の2つにunificationを行うと、
    • 'aint -> string -> 'cである。
    • 'bout_channelである。
    • 'cunitである。
  • したがって、Printf.fprintf stdout "%d %s"の型は 'a つまり int -> string -> unitである。

一方、Printf.sprintf "%d %s"の型はどうなるか。

  • Printf.sprintf の第1引数の型は ('a, unit, string) format である。
  • "%d %s" の型は (int -> string -> 'c, 'b, 'c) format である。(変数名は適当に付け替えた)
  • 上記の2つにunificationを行うと、
    • 'aint -> string -> 'cである。
    • 'bunitである。
    • 'cstringである。
  • したがって、Printf.sprintf "%d %s"の型は 'a つまり int -> string -> stringである。

また、フォーマットのフォーマット指定子を変えると、その文字列リテラルの型が変化し、全体としては引数の個数が変化する。

%aフォーマット指定子

OCamlには%aというフォーマット指定子がある。これはユーザー定義オブジェクトを出力するための仕組みである。(%tという亜種もある)

mytypeの値を出力するために、ユーザーはあらかじめ次のような関数を定義しておく。

val print_mytype : out_channel -> mytype -> unit

そして、Printf.fprintfを次のように呼び出す。

Printf.fprintf stdout "%a" print_mytype myval

"%a"の型は(('b -> 'd -> 'a) -> 'd -> 'a, 'b, 'a) formatだから、Printf.fprintf stdout "%a"の型は(out_channel -> 'd -> unit) -> 'd -> unitとなる。この関数は"%a"に差し掛かったら、myvalprint_mytypeに渡すことで出力する。

この仕組みの問題点は、ユーザー定義出力関数をPrintf.fprintfPrintf.sprintfの種別ごとに別々に用意しなければならないことである。Printfモジュールではこれは本質的に解決が難しいが、Formatモジュールでは解決策が用意されている。それはFormat.asprintf関数である。

val Format.asprintf : ('a, formatter, unit, string) format4 -> 'a

このように、Format.asprintfformat4というより一般的な型を使っている。

フォーマットの結合

フォーマット文字列は(^^)によって結合できる。例えば、

Printf.fprintf stdout ("[%d]" ^^ "[%s]") 1 "Foo";;

しかし、このような(^^)formatの範囲内では実現できない。次のように、format4というより一般的な型を使う必要がある。(後述するように、実際にはさらに一般的な型をもつ。)

val (^^) : ('a, 'b, 'c, 'd) format4 ->
       ('d, 'b, 'c, 'e) format4 ->
       ('a, 'b, 'c, 'e) format4

4引数のformat4 (型安全なフォーマット入出力において継続渡しをするための枠組み)

4引数のformat4は、formatの一般化である。正確には、formatformat4の特別な場合として以下のように定義されている。

type ('a, 'b, 'c) format = ('a, 'b, 'c, 'c) format4

したがってformat4には2種類の異なる「戻り値型」の概念があることになる。

この理由は、フォーマット入出力関数を実行後に、その結果を使って何か別のことをするという処理を一般的に書くためである。このような処理は、フォーマットが決まっていれば ;let ... in ...を使って簡単に書ける。しかし、任意のフォーマットに対して動作しようとすると、そのままでは上手くいかない。

OCamlでは、各種フォーマット入出力関数の継続渡し形式バージョンを用意することでこれを解決している。例えば以下のような関数である。

val Printf.kfprintf : (out_channel -> 'd) ->
       out_channel ->
       ('a, out_channel, unit, 'd) format4 -> 'a
val Printf.ksprintf : (string -> 'd) -> ('a, unit, string, 'd) format4 -> 'a
val Format.kfprintf : (formatter -> 'a) ->
       formatter -> ('b, formatter, unit, 'a) format4 -> 'b
val Format.kasprintf : (string -> 'a) -> ('b, formatter, unit, 'a) format4 -> 'b

これらの特徴は、第1引数として継続 (continuation)を取っている点である。実際、何もしない継続を第1引数に入れることで、普通のフォーマット入出力関数が得られる。

さて、これらの継続渡し形式では、「フォーマット入出力処理の結果」と、「それを継続に渡して得られた最終的な結果という2種類の結果の概念があることがわかるだろう。これが、('a, 'b, 'c, 'd) format4における'c'dの区別に他ならない。

これを踏まえると、先ほど説明した2つの機能がformat4に依存している理由も説明できる。

  • Format.asprintfは次のような関数である: 「文字列バッファに出力するformatterを作成し、Format.fprintfを呼び出す。その後、出力された文字列バッファから文字列を取り出して返却する。」内部的にはFormat.fprintfが呼ばれているため、ユーザー定義出力関数は共通のものを使い回せる。そして、この処理ではFormat.fprintfの実行後に続けて処理をしたいので、実際には継続渡し形式(Format.kfprintf)を使う必要がある。
  • (^^)はフォーマットを結合する関数である。フォーマットの結合は言い換えると、「フォーマット1を出力後、フォーマット2を出力するようなフォーマット」となる。したがってフォーマット1にとっては後続する処理が継続となる。

scanf系関数

scanf系関数でも同じformat4を使うことができる。これは単純化すると以下のような型をもつ。

val Scanf.bscanf : Scanf.Scanning.in_channel -> ('a, Scanf.Scanning.in_channel, 'a -> 'd, 'd) format4 -> 'a -> 'd

例えば、Scanf.scanf "%d %s"には以下のように型がつく。

# Scanf.scanf "%d %s";;
- : (int -> string -> '_a) -> '_a = <fun>

したがって、例えば、以下のように書ける。

let (i, s) = Scanf.scanf "%d %s" (fun i s -> (i, s)) in
Printf.printf "i=%d, s=%s\n" i s

%rフォーマット指定子

出力用の%aと同様に、OCamlにはユーザー定義オブジェクトを入力するための%rというフォーマット指定子がある。

mytypeの値を入力するために、ユーザーはあらかじめ次のような関数を定義しておく。

val read_mytype : Scanf.Scanning.in_channel -> mytype

そして、Scanf.bscanfを次のように呼び出す。

Scanf.scanf "%r" read_mytype (fun myval -> myval)

ここで、フォーマット文字列の直後にユーザー定義入出力関数がくることに注意。これは%rの個数だけ必要である。

6引数のformat6

%rを含むフォーマットには、より一般的なformat6という型がつく。format4format6の関係は以下の通り。

type ('a, 'b, 'c, 'd) format4 = ('a, 'b, 'c, 'c, 'c, 'd) format6

ここで、4番目と5番目の引数は、1番目と最後の引数の関係に近い。上記のように、%rがないときは同じ型がつくが、%rが入ると次のように型が変化する。

# ("" : _ format6);;
- : ('a, 'b, 'c, 'd, 'd, 'a) format6 =
# ("%r" : _ format6);;
- : ('a -> 'b, 'c, 'd, ('c -> 'a) -> 'e, 'e, 'b) format6 =
# ("%r%r" : _ format6);;
- : ('a -> 'b -> 'c, 'd, 'e, ('d -> 'a) -> ('d -> 'b) -> 'f, 'f, 'c) format6

4番目と5番目の引数をうまくunifyすることで、必要な数だけユーザー定義入力関数をとるような関数が作れる。

フォーマットを連結する関数の型も、以下のように一般化される。

val (^^) : ('a, 'b, 'c, 'd, 'e, 'f) format6 ->
       ('f, 'b, 'c, 'e, 'g, 'h) format6 ->
       ('a, 'b, 'c, 'd, 'g, 'h) format6

まとめ

OCamlでは、型安全なprintf/scanfを実現するために、コンパイラ側でフォーマット文字列を解析して特殊な型をつけた上で、一般的な型推論のunificationの仕組みを活用したライブラリを提供している。本稿ではその仕組みを、歴史的にこの型が複雑化してきた順に解説した。

*1:ちなみにこの関数は実は、型を強制するだけの単なる恒等関数である。

C言語で部分適用したい!(実は、できるアーキテクチャがあるんです)

通常、C言語の関数ポインタは、クロージャではない。したがって、関数を部分適用したり、カリー化したり、ローカル変数をキャプチャーした関数ポインタを返したりすることはできない。しかし、実際にC言語が動作する環境のなかには、そのようなことが実現できるものがある。PowerPC64 System V ABIは、そのひとつである。

PowerPC64 System V ABIは、Linux等において高級言語のコードをPowerPC64機械語に翻訳するさいの取り決めである。

多くのABIでは、関数ポインタは関数の最初の命令のアドレスに翻訳されるが、PowerPC64 System V ABIはそれとは異なる定義をしている。具体的には、関数ポインタは以下のような構造体

struct Funptr {
  void *jump_target; /* ジャンプ先 */
  void *initial_r2; /* TOCベース。ジャンプ前に %r2 レジスタに代入される値 */
  void *initial_r11; /* 環境ポインタ。ジャンプ前に %r11 レジスタに代入される値 */
};

へのポインタ (すなわち struct Funptr*) である。

この3番目の要素はプログラミング言語の要請に応じて使ってよい。C言語自体は環境ポインタを使わないが、関数ポインタを呼ぶさいは環境ポインタが考慮される。

そのため、アセンブリを用いて以下のようなコードを書くことができる。以下は、乗算演算子を部分適用する multiply 関数を用いてかけ算九九を出力するコードである。

#include <stdio.h>
#include <stdlib.h>

int (*multiply(int x))(int);

int main() {
  int (*f[10])(int);
  for(int x = 0; x < 10; ++x) {
    f[x] = multiply(x);
  }
  for(int x = 0; x < 10; ++x) {
    for(int y = 0; y < 10; ++y) {
      printf("%d * %d = %d\n", x, y, f[x](y));
    }
  }
  for(int x = 0; x < 10; ++x) {
    free(f[x]);
  }
  return 0;
}

この multiplyアセンブリで以下のように書ける。

	.globl multiply
multiply:
	mflr %r0
	std %r0, 16(%r1)
	stdu %r1, -96(%r1)
	std %r3, 88(%r1)
	li %r3, 24
	bl malloc
	nop
	ld %r5, 88(%r1)
	addis %r4, %r2, multiply2@toc@ha
	addi %r4, %r4, multiply2@toc@l
	std %r4, 0(%r3)
	std %r2, 8(%r3)
	std %r5, 16(%r3)
	addi %r1, %r1, 96
	ld %r0, 16(%r1)
	mtlr %r0
	blr
multiply2:
	mulld %r3, %r3, %r11
	blr

これを実行すると、以下のようになる。

$ powerpc64-linux-gnu-gcc -std=c99 -static main.c multiply.s
$ qemu-ppc64 ./a.out
0 * 0 = 0
0 * 1 = 0
0 * 2 = 0
0 * 3 = 0
0 * 4 = 0
0 * 5 = 0
0 * 6 = 0
0 * 7 = 0
0 * 8 = 0
0 * 9 = 0
1 * 0 = 0
1 * 1 = 1
1 * 2 = 2
1 * 3 = 3
1 * 4 = 4
1 * 5 = 5
1 * 6 = 6
1 * 7 = 7
1 * 8 = 8
1 * 9 = 9
2 * 0 = 0
2 * 1 = 2
2 * 2 = 4
2 * 3 = 6
2 * 4 = 8
2 * 5 = 10
2 * 6 = 12
2 * 7 = 14
2 * 8 = 16
2 * 9 = 18
3 * 0 = 0
3 * 1 = 3
3 * 2 = 6
3 * 3 = 9
3 * 4 = 12
3 * 5 = 15
3 * 6 = 18
3 * 7 = 21
3 * 8 = 24
3 * 9 = 27
4 * 0 = 0
4 * 1 = 4
4 * 2 = 8
4 * 3 = 12
4 * 4 = 16
4 * 5 = 20
4 * 6 = 24
4 * 7 = 28
4 * 8 = 32
4 * 9 = 36
5 * 0 = 0
5 * 1 = 5
5 * 2 = 10
5 * 3 = 15
5 * 4 = 20
5 * 5 = 25
5 * 6 = 30
5 * 7 = 35
5 * 8 = 40
5 * 9 = 45
6 * 0 = 0
6 * 1 = 6
6 * 2 = 12
6 * 3 = 18
6 * 4 = 24
6 * 5 = 30
6 * 6 = 36
6 * 7 = 42
6 * 8 = 48
6 * 9 = 54
7 * 0 = 0
7 * 1 = 7
7 * 2 = 14
7 * 3 = 21
7 * 4 = 28
7 * 5 = 35
7 * 6 = 42
7 * 7 = 49
7 * 8 = 56
7 * 9 = 63
8 * 0 = 0
8 * 1 = 8
8 * 2 = 16
8 * 3 = 24
8 * 4 = 32
8 * 5 = 40
8 * 6 = 48
8 * 7 = 56
8 * 8 = 64
8 * 9 = 72
9 * 0 = 0
9 * 1 = 9
9 * 2 = 18
9 * 3 = 27
9 * 4 = 36
9 * 5 = 45
9 * 6 = 54
9 * 7 = 63
9 * 8 = 72
9 * 9 = 81

FAQ

Q. つまりPowerPC64がすごいということか?

A. そうではない。これは「C言語のコードを機械語にどのように翻訳するか」という決まり事、すなわちABIに関する話である。LinuxのPowerPC64版においてたまたま上記のようであったというだけであり、この特徴はPowerPC64というCPUアーキテクチャ自身の性質とは関係ない。したがって、同様にPowerPC64のCPU上で動作するシステムであっても、上で述べたようなことが成り立たない可能性もある。

Q. 関数ポインタをそのような特殊な形で実装してしまって、非互換性は生じないのか。

A. 少なくともC言語(ISO C)の定める範囲では、関数ポインタの中身に関しての規定はほぼない。それどころか、関数ポインタとオブジェクトへのポインタは明確に区別され、バイト数が異なっていてもよい。(16bitのx86には実際にそのようなメモリモデルがある)

Q. これはどう見ても関数ポインタではなくてクロージャなのではないか。

A. もちろん誰がどう見てもクロージャだが、C言語からは完璧に関数ポインタとして見えている。

巻き舌できるようになった(たぶん)

これまで巻き舌ができなかったが、今日ふと試したらできるようになった。巻き舌といっても、舌を変な形にするほうではなく、Rの音を出すほう。

あんまり参考にならないかもしれないけど、一応どんな風にやったか書いておく

舌を意図的に動かす

ロシア語やイタリア語ではRを巻き舌にするのが普通(全員ができるわけではないので必須ではない)のようで、巻き舌ができなかった僕は次のように巻き舌を真似していた。

  • 巻き舌では舌は上の歯か歯茎あたりに触れる。このとき左右の側面で触れる方法と、舌の先で触れる方法がある。この2つの状態を切り替えるときにはじくような音が出る。
  • 声を出さずにやると、ボイスパーカッションみたいな感じになるので、これを繰り返すとルタルタルタルタルタルタ……という感じになる。
  • これに声を入れると、ルルルルルルルル……という感じになるので、これを高速に行うとそれっぽくなる。

気流で舌を動かす

上のように舌を動かす動作を、舌の筋肉ではなくて気流でやることを考える。

  • 舌と上の歯茎を完全に接触させると、口から空気を出せなくなる。その状態でさらに圧力を加えると、どこかに強制的に隙間があく。この時に、上記と同様にはじくような音が出る。
  • 気流を維持したまま、舌の筋肉を使って舌をもとの位置(舌と上の歯茎を完全に接触させた状態)に戻そうとする。うまくやると、上の動作が繰り返し起こる。
  • 先ほどと同様に、そのまま声を入れる。
  • この時、側面で触れている状態と、舌の先端で触れている状態を行ったり来たりするように意識する。
  • 気流だけで舌がうまく動くようにする。そのためには、それなりに勢いが必要である。気持ちとしては、Rの音をいきなり出すのではなく、予備動作として適当な母音(uとか)をちょっと入れて、そこから一気に息を吹きこみつつ舌を動かす感じでやるとうまくいくことがある。
  • うまくいくと巻き舌のRっぽくなる

ランサムウェアを作ってみた(シェルスクリプトで)

ランサムウェアの暗号化部分についての実証コードを書いてみた。暗号の計算にはOpenSSLのコマンドが使えるので、シェルスクリプトを使って書いた。

github.com

注意

  • このコードを試して起こった損害について作者は責任を追わない。基本的にdocuments/以下にあるテストファイルのみが操作対象だが、シェルスクリプトがザルなので空白を含むファイルなどが混ざっていると少し危いかもしれない。
  • このコードはランサムウェアの暗号化の動作を実証することを目的としたものであり、実際にランサムウェアなどのマルウェアに「応用」することを意図したものではない。もちろん、実際に身代金目的のランサムウェアを作って配布することは違法である可能性が高い。そもそも、このコードは暗号化部分の最低限の実装しかしていないので、実際にランサムウェアを作るにあたって役に立つことはほとんどないだろう。

はじめに

ランサムウェアは起動するとコンピューター内のファイルを暗号化し、復号を見返りに身代金を要求するマルウェアである。支払い後に実際に復号するものとそうではないものがあるらしいが、ここでは実際に復号能力があるものを考える。

ランサムウェアが作者の意図通りに動作するには、以下の条件を満たしてほしいだろう。

  • ランサムウェアの存在が発覚したあとは、そのランサムウェアは解析の対象となるが、それによって身代金なしにファイルを復号されてしまっては困る。
  • ランサムウェアの被害者ごとに、それぞれ身代金を支払ってほしい。
  • 復号時のクライアントとサーバーの通信は最小限に留めたい。

複数の暗号を組み合わせることでこれを実現できる。今回はそれを実証するコードを書いてみた。

仕組み

まず、ランサムウェアの作者は秘密鍵と公開鍵の鍵ペアを作成し、ランサムウェアには公開鍵のみを同梱する。この方法であれば、ランサムウェアが解析されても秘密鍵は復元できない。

この公開鍵を作ってファイルを暗号化することも可能だが、これには次の問題がある。

  • そもそも、公開鍵を使って大きなファイルを暗号化するのはコストが高くつく。
  • また、身代金が支払われたあとの復号の方法が問題になる。仮に秘密鍵を送るとすると、このランサムウェアは被害者1人が身代金を支払うだけで終わってしまう。
  • かといって、サーバー側でファイルを復号すると大量の通信が必要になる。

そこで、次のようにする。

  • ランサムウェアは起動したらまず新規に共通鍵を生成する。
  • 共通鍵を公開鍵で暗号化し、保存する。
  • メモリ上にある共通鍵を使って、ファイルを暗号化する。全ての暗号化が終わったら、共通鍵は捨てる。

被害者は身代金を支払う際に暗号化された共通鍵を添付する。ランサムウェアの作者はこれを手元の秘密鍵で復号して送り返す。ファイルの復号は手元で行うことができる。

使い方

RSAやAES-CBCなどの暗号はOpenSSLのコマンドとして用意されているため、このデモはシェルとOpenSSLがあれば動かすことができる。

まず、デモコードを取得する。

~$ git clone https://github.com/qnighy/ransomware-demo.git
~$ cd ransomware-demo
マスター鍵対を作成する
~/ransomware-demo$ ./genmaster.sh

これによってRSA鍵対が作成される。秘密鍵ランサムウェアの作者が保有し、公開鍵はランサムウェアに埋め込まれる。

ランサムウェアを実行する

ランサムウェアが配布され、被害者のコンピューター上で実行されたとする。

~/ransomware-demo$ cd client
~/ransomware-demo/client$ find documents
documents
documents/lipsum.txt
documents/hello.txt
~/ransomware-demo/client$ cat documents/hello.txt
Hello, world!
~/ransomware-demo/client$ ./encrypt.sh
~/ransomware-demo/client$ find documents
documents
documents/hello.txt.enc
documents/hello.txt.iv
documents/hello.txt.sha256
documents/lipsum.txt.enc
documents/lipsum.txt.iv
documents/lipsum.txt.sha256

この ./encrypt.shランサムウェアによる暗号化である。ここでは3つのことが起こっている。

  • バイスごとの共通鍵が作成される。
  • この共通鍵を使ってファイルが暗号化される。
  • 共通鍵はマスター鍵を使って暗号化される。
支払いとデバイス鍵の復元

ファイルを復号するためには、まずランサムウェアの作者に身代金を払ってデバイス鍵を復元する必要がある。

~/ransomware-demo/client$ ./decrypt.sh
device_key.dat not found. First pay for us!
~/ransomware-demo/client$ cp device_key_encrypted.dat ../server/
~/ransomware-demo/client$ mv ../server/
~/ransomware-demo/server$ ./decrypt-key.sh
~/ransomware-demo/server$ cp device_key.dat ../client/
~/ransomware-demo/server$ mv ../client/
復号

バイス鍵を復号したら、これを使ってファイルを復号できる。

~/ransomware-demo/client$ ./decrypt.sh
~/ransomware-demo/client$ find documents
documents
documents/lipsum.txt
documents/hello.txt
~/ransomware-demo/client$ cat documents/hello.txt
Hello, world!

まとめ

ランサムウェアにおけるファイルの暗号化は決して複雑ではないが、複数の暗号を組み合わせて実現されている。この記事では暗号化のOpenSSLのコマンドを使って、ランサムウェアがどのように暗号を組み合わせているかを示すデモを作成した。

とある偽シャッフルアルゴリズムとその分布

次のようなシャッフルアルゴリズムを考える(簡単のためrand()%Nと表記したが、この部分で0以上N-1未満の一様な整数乱数が生成されると仮定して議論する)。出力されるものは 0, ..., 255 を並び換えたもの(置換)である。

std::vector<int> a(N);
for(int i = 0; i < N; ++i) {
  a[i] = i;
}
for(int i = 0; i < N; ++i) {
  std::swap(a[i], a[rand()%N]);
}

このアルゴリズムは均一ではない。a[i]==jとなる確率は、 i < jのときに高くなり、j <= iのときに低くなる。グラフにすると以下のようになる。

f:id:qnighy:20160605175316p:plain

定理

上のシャッフルアルゴリズムで得られる aについて、 a[i]==jとなる確率は、

{
\begin{cases}
\frac{1}{N}\left(1-\frac{1}{N}\right)^{N-1-i} + \frac{1}{N}\left(1-\frac{1}{N}\right)^j - \frac{1}{N}\left(1-\frac{1}{N}\right)^{N-1-i+j} & j \leq i \\
\frac{1}{N}\left(1-\frac{1}{N}\right)^{N-1-i} + \frac{1}{N}\left(1-\frac{1}{N}\right)^j & i < j
\end{cases}
}

となる。

証明

2個目のループの本体が {t}{(0 \leq t \leq N)} 実行された時点で a[i]==j となる確率を {p_{t,i,j}} とおく。プログラムをジッと睨むと、以下の式を得る:

{
p_{0,i,j} = \begin{cases}
  1 & i = j \\
  0 & i \neq j
\end{cases}
}

{
p_{t+1,i,j} = \begin{cases}
  \frac{1}{N} \sum_{k=0}^{N-1} p_{t,k,j} & i = t \\
  \left(1-\frac{1}{N}\right)p_{t,i,j} + \frac{1}{N}p_{t,t,j} & i \neq t
\end{cases}
}

さらに、不変条件 {\sum_{k=0}^{N-1} p_{t,k,j} = 1} に注目すると、後者の式は

{
p_{t+1,i,j} = \begin{cases}
  \frac{1}{N} & i = t \\
  \left(1-\frac{1}{N}\right)p_{t,i,j} + \frac{1}{N}p_{t,t,j} & i \neq t
\end{cases}
}

となる。このとき、以下が成り立つことを示す。 {t=N} の場合が定理の主張に他ならない。

{
p_{t,i,j} = \begin{cases}
  \frac{1}{N}\left(1-\frac{1}{N}\right)^{t-1-i} + \frac{1}{N}\left(1-\frac{1}{N}\right)^j - \frac{1}{N}\left(1-\frac{1}{N}\right)^{t-1-i+j} & j \leq i < t \\
  \frac{1}{N}\left(1-\frac{1}{N}\right)^{t-1-i} + \frac{1}{N}\left(1-\frac{1}{N}\right)^j & i < j < t \\
  \frac{1}{N}\left(1-\frac{1}{N}\right)^j & j < t \leq i \\
  \frac{1}{N}\left(1-\frac{1}{N}\right)^{t-1-i} & i < t \leq j \\
  \left(1-\frac{1}{N}\right)^t & t \leq i = j \\
  0 & t \leq i, t \leq j, i \neq j
\end{cases}
}

{t} に関する帰納法で示す。まず、 {p_{0,i,j}} が上記を満たすことはすぐにわかる。

{i,j} について {p_{t,i,j}} が上記を満たすと仮定する。このとき、各 {i,j} について {p_{t+1,i,j}} も上記を満たすことを示す。そのために以下のように場合分けをする。

  • {j \leq i < t} のとき。
  • {j \leq i = t} のとき。
  • {i < j < t} のとき。
  • {i < j = t} のとき。
  • {i < t < j} のとき。
  • {i = t < j} のとき。
  • {j < t < i} のとき。
  • {j = t < i} のとき。
  • {t < i = j} のとき。
  • {t < i, t < j, i \neq j} のとき。

各場合分けは簡単な式変形で示せる。

正しいアルゴリズム

例えば、以下のようにする。(別途、rand()%(i+1)の部分をより適切な擬似乱数に置き換える必要がある。)

std::vector<int> a(N);
for(int i = 0; i < N; ++i) {
  a[i] = i;
}
for(int i = 0; i < N; ++i) {
  std::swap(a[i], a[rand()%(i+1)]);
}

この方法の場合、2個目のループ本体が {t} 回実行された時点で a[0], ..., a[t-1] が一様にランダムな置換になっていることが保証できる。

このアルゴリズムKnuth shuffleとかFisher-Yates shuffleと呼ばれている。

相関に関する補足

この記事では偽シャッフルアルゴリズムについて、要素ごとの確率分布に注目して解析したが、これだけでは不十分な場合もある。例えば、以下のアルゴリズムは明らかに正しくないシャッフルアルゴリズムだが、要素ごとの確率分布は一様である。

std::vector<int> a(N);
int s = rand()%N;
for(int i = 0; i < N; ++i) {
  a[i] = (i+s)%N;
}

C/C++の静的解析ツール・事例まとめ

C/C++の静的解析は、どう考えても大変なんだけどどう考えても需要が高いので、やはり色々なソフトウェアや事例があるようだ。まとまった情報が欲しいけど見つからなかったので自分の調べた範囲でまとめることにした。

他にも耳寄りな情報があったら教えてほしい。

静的解析を行うことができるソフトウェア

調べてみると結構たくさんある。それぞれの特徴とかあまりよくわからない。

(個人的には、とりわけ網羅的な形式的検証ができるツールの性能に興味があるので、それを中心に集めていたが、やはり網羅的とは限らないで探すともっとたくさん見つかるようだ。もちろん網羅性にはトレードオフがある)

  • Frama-C …… C言語に形式手法を適用するための汎用のフレームワークで、静的検証のためのプラグインも多数(WPとかValueとか)存在する。網羅的な検証から発見的な手法、動的な手法まで様々ある。研究で使うのに便利そう
  • Astrée Runtime Error Analyzer …… 飛行機などミッションクリティカル環境を主に想定した網羅的な静的分析器のようだ。昔のページ→The Astrée Static Analyzerを見ると、再帰と動的メモリ確保のないプログラムを対象としていたようだが、現在は再帰のないプログラムなら動的メモリ確保があっても検査できるようだ。フランスのINRIAとかその辺が関わっていそうな雰囲気がある
  • VCC …… 名前に "concurrent" が含まれていたり、並行性が何かとプッシュされているように見える。codeplexに置いてあるしMSRかな
  • SLAyer …… 最近MSが出したらしい。これも分離論理でメモリ安全性を調べるパターン(なので網羅性あるのかな)。
  • VeriFast …… これもCのプログラムが検証できるらしい。
  • Escher C/C++ Verifier …… 説明を見る限り、網羅的な検査をすると言っているように読める。C++も検証できると主張しているので強そう。会社概要を見る限り、これが主力商品のようだ
  • Infer …… Facebookが買収したことで有名。分離論理使うくらいだから何らかの意味で網羅的なんだろうか。一般的なC/C++プログラムを検証できそうな雰囲気
  • CBMC …… 有界モデル検査をするツールのようだ
  • CodeSonar …… Z3使うらしい(ということはwhite-box testingとかかな)。網羅的とは書いていないように見えるので発見的な手法かな
  • Coverity …… これも静的解析ツールとしては強いらしい。網羅性はパッと見では確認できなかった ← grafiさんが紹介してくれた記事にunsoundと書いてあった
  • QAC …… これも網羅性は確認できなかった

余裕があれば上記のソフトウェアを以下のような観点から整理したい。

  • 標準準拠 …… 言語仕様である ISO C, ISO C++. POSIXの仕様であるSUSやThe Open Group Specification. コーディング標準であるCWE, CERT C, MISRA-C. 安全性の規格であるDO-178B level A, ISO 26262, IEC 61508. ……などがあるらしいので、それぞれへの対応度を調べる。
  • 網羅性 …… 一部の静的解析ツールは、ある種の問題(例えば実行時エラー)がないことを保証できる場合がある。例えばAstréeのページにはsound(健全)という言葉があるが、これはこの網羅性をあらわしている。
  • 精度と再現率 …… 実際の問題に適用したときには、見つけられなかったバグの数や誤検出された問題の数が重要になると考えられる。
  • 適用可能なプログラムの範囲 …… Astréeは再帰のないプログラムに限定して検証すると書かれている。このように、適用対象を絞ることで高性能な静的解析を提供している場合があるようだ。
  • 適用可能なアサーションの表現力 …… プログラムにコメントでアサーションを入れるタイプの静的解析ツールでは、そのアサーションの表現力に違いがあるかもしれないので、その辺りを調べる。また、そうでない静的解析ツールでは、発見できるバグの種類がこれに相当すると考えられる。

検証済みコンパイラ

コンパイラ自体が(主に最適化まわりで)バグってることはたまにあるので、ミッションクリティカルな用途ではコンパイラ自体の正しさも気になるという事情があるようだ。

  • CompCert …… Astréeと同じあたりが作ってるやつ。

プログラミング言語の形式仕様

C言語のプログラムやコンパイラに関して正確に論証したいとなるとそもそも仕様が必要になるが、ここで紹介しているのがまさにそれだ。

  • Verifiable C …… Coqで書かれたC言語の仕様。便利そう。CompCertの正しさはこの仕様と照らしあわせて検証されている。

動的検査するやつ

静的解析ではないような気がするけど。

更新履歴