2015-05-22

C言語(標準)にM_PIは無い

C言語で円周率πを使うには M_PI を使う、と経験で知っている人は多いが、あれは実はC言語の規格には含まれていない。むしろ、処理系がM_PIを定義してはいけない事情(c - Using M_PI with C89 standard - Stack Overflow)がある。

ここでは、C言語の最新規格であるC11と等価なN1570 (http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf) を参考にする。これより古いC言語の規格でも同様だと思われる。

C言語の規格では、まず「標準に準拠したプログラム」は何かということを定義し、続いて「標準に準拠した処理系」は何かということを定義する、という手順を踏んでいる。

Strictly conforming program

Strictly conforming programとは、最も移植性が高いプログラムである。あるプログラムがstrictly conformingであるかどうかは、この規格書の中で厳密に定義されている。大まかに言うと、

出力が不定動作に依存してはいけない。
出力が未定義動作に依存してはいけない。
出力が処理系定義の動作に依存してはいけない。
出力がminimum implementation limitsを超過してはいけない。(例えば、intは-32767以上32767以下の数値を表現できることは仮定してよいが、それよりも大きいとは仮定してはいけない。)

「不定動作」「未定義動作」「処理系定義の動作」「implementation limitとその最小値」なども、それぞれ厳密に定義されている。

Strictly conforming programの例

#include <stdio.h>

int main(int argc, char *argv[]) {
    printf("Hello, world!\n");
    return 0;
}

Strictly conformingではない例(mainの引数が非標準、GCC拡張であるStatements and Declarations in Expressionsを使っている)

#include <stdio.h>

int main(int argc, char *argv[], char *envp[]) {
    printf(({"Hello, world!\n";}));
    return 0;
}

(参考: N1570 p.8)

Conforming implementation

Conforming implementationとは、全てのstrictly conforming programを正しく動作させる処理系のことである。(その他、#errorでエラーになることや__cplusplusをマクロで定義しないことなど、いくつかの制約がある)

したがって、conforming implementationは、strictly conformingでないプログラムに関してはどう料理してもよい。

Conformingだと思われる処理系の例 : gcc -std=c11 (いくつかのGCC拡張は有効だが、C標準と矛盾する機能は無効化される)
- ただし、GCCで未実装のC11機能があるので、その点ではconformingではなさそう
Conformingではない処理系の例 : gcc -std=gnu11

(参考: N1570 p.8)

Conforming program

あるConforming implementationが受理するプログラムはConforming programと呼ばれる。この意味では、上記のCプログラムも「正しい」Cプログラムだが、移植性は保証されない。

(参考: N1570 p.8)

識別子

次のような識別子は予約されている:

アンダースコア+大文字、またはアンダースコア2個、で始まる識別子
アンダースコアで始まる識別子 (ファイルスコープ、通常の名前空間とタグ名前空間のみ制限)
規格書内で定義されているマクロ名
規格書内で定義されている外部リンク名とerrno (外部リンク名としての使用のみ制限)
規格書内で定義されているファイルスコープの名前 (関連するヘッダーがインクルードされている場合のみ、マクロ名としておよび同一名前空間でのファイルスコープでの使用のみ制限)

つまり、

Strictly conforming programは、予約されている識別子を独自に定義・宣言・undefしてはいけない。
Strictly conforming programは、予約されていない識別子は自由に使ってよい。
Conforming implementationは、予約されていない識別子を独自に定義・宣言してはいけない。 (strictly conforming programの挙動が邪魔されるので)
Conforming implementationは、予約されている識別子をある程度自由に使える。

例えば、ヘッダーによくある

#ifndef _HOGE_INCLUDED
#define _HOGE_INCLUDED

some_declarations

#endif

は、

ユーザー側のプログラムとしては: アンダースコアで始まっているので、strictly conformingではない。
ライブラリとしては: strictly conforming programが使える空間を汚していないので良い。むしろ、そうしないとstrictly conforming programの使える名前空間を汚していることになる。

(参考: N1570 p.182)

math.h

math.hは、規格で存在が要請されているヘッダーの一つである。

規格では、math.hで宣言されているべき識別子の一覧も指定されている。

例えば、

型 : float_t, double_t が定義されている。
マクロ : HUGE_VAL, INFINITY, NAN(NaNが使える場合だけ), ... などが定義されている。
関数マクロ : fpclassifyなどのマクロが定義されている。
関数 : cos, sin, log, ...などの関数が宣言されている。

したがって、これらの識別子は予約されていることになる。つまり、strictly conforming programは、

cos, sin, logなどを外部リンク名として独自に定義してはいけない。
math.hをインクルードしている場合は、logやHUGE_VALなどの識別子を独自にマクロ名やファイルスコープでの名前として使ってはいけない。

一方、問題のM_PIはここでは言及されていない。したがってこの識別子は予約されていない。

したがって、以下のようなプログラムはstrictly conformingではない。(存在しないはずのM_PIを使っているので)

#include <math.h>
#include <stdio.h>

int main(int argc, char *argv[]) {
    printf("PI = %f\n", M_PI);
    return 0;
}

一方、以下のようなプログラムはstrictly conformingである。

#include <math.h>
#include <stdio.h>

int M_PI = 3;

int main(int argc, char *argv[]) {
    printf("PI = %d\n", M_PI);
    return 0;
}

(参考: N1570 p.231)

M_PIを定義してはいけない理由

もし、conforming implementationがmath.hでM_PIを定義していたとすると、上記のStrictly conforming program

#include <math.h>
#include <stdio.h>

int M_PI = 3;

int main(int argc, char *argv[]) {
    printf("PI = %d\n", M_PI);
    return 0;
}

が正しく動作しなければいけないという制約に反する。

したがって、conforming implementationではM_PIを定義してはいけない。

実際のコンパイラー

gccは-std=c11のもとではM_PIを定義しない。
gccは-std=gnu11のもとではM_PIを定義する。 (つまりこのgccはconforming implementationではない)
VC++はM_PIを定義しないらしい。

gccについては、gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2で確認した。(参考
math.h の M_PI などは仕様外だった - Gust Notch? Diary)

_USE_MATH_DEFINES

処理系によっては、

#include <math.h>
#include <stdio.h>

int main(int argc, char *argv[]) {
    printf("PI = %f\n", M_PI);
    return 0;
}

はコンパイルできないが、

#define _USE_MATH_DEFINES
#include <math.h>
#include <stdio.h>

int main(int argc, char *argv[]) {
    printf("PI = %f\n", M_PI);
    return 0;
}

のように_USE_MATH_DEFINESを指定すると、正しく動作することがある。

これは、予約された識別子を定義している

#define _USE_MATH_DEFINES

の一行によって、このプログラムがStrictly conforming programではなくなることに由来している。したがって、

#define _USE_MATH_DEFINES
#include <math.h>
#include <stdio.h>

int M_PI = 3;

int main(int argc, char *argv[]) {
    printf("PI = %d\n", M_PI);
    return 0;
}

のように、わざわざM_PIを独自に定義して使おうという危なげなプログラムがあったとしても、これは最初の1行のせいでStrictly conformingではなくなり、処理系はこれを正しく動かす義務がなくなる。

まとめ

厳密には、処理系はM_PIを定義してはいけない。コンパイラーは実際にそれを上手に守っている。
困る

2015-02-05

GW-450DやWN-AC433UKをRaspberry Piで使う

planexのありがたい記事を参考に作業。

環境としてはRaspbian wheezyを仮定。

おおまかな流れ : まず、下準備としてカーネルモジュールのビルドに必要な道具を揃える(既に揃えてある人はスルーしてよい)。続いて、ドライバのソースコードを取得し、必要な変更を加えてからビルド、インストールする。

前提知識

記事執筆時点ではGW-450DやWN-AC433UKはRaspberry Piではそのままでは動作せず、ドライバを自分で導入してやる必要がある。

GW-450DやWN-AC433UKはMediaTekのMT-7610Uというチップセットを用いているので、中身は基本的に同じである。ただし、USBのベンダーIDとプロダクトIDは変更されているので、これをドライバ中に記述してやる必要がある。

下準備1: カーネルビルドに用いられたGCCのバージョンを調べる

ここでは、raspberry piのデフォルトのカーネルを使う場合の下準備の例を示す。Raspbianがaptで提供しているカーネルを使用する場合はこの限りではなく、単にapt-getでヘッダーファイルが含まれるパッケージを取得すればよい。

$ cat /proc/version
Linux version 3.18.5+ (dc4@dc4-XPS3-9333) (gcc version 4.8.3 20140303 (prerelease) (crosstool-NG linaro-1.13.1+bzr2650) - Linaro GCC 2014.03) ) #746 PREEMPT Mon Feb 2 13:57:16 GMT 2015

で、gcc4.8.3が使われていることがわかったので、gcc4.8系列を使う。

ただし、Linux ARMにとってgcc4.8.0から4.8.2までは "too buggy" で、Linuxを正しくビルドできないとされている(これらのバージョンを使おうとすると、あるヘッダでエラーが出て弾かれるようになっている)ので、これは避ける必要がある。

したがって、この記事の執筆時点では、gcc-4.8.3を用いるのが正解ということになる。

下準備2: gccを入れる

本来であれば、

$ sudo apt-get install gcc-4.8

で目的のバージョンが入るのが望ましい。試しに

$ gcc-4.8 -v

で、所望のバージョンが得られていれば、この節はスキップしてよい。

gcc 4.8 on Raspberry Pi Wheezy | some wide open space を参考に、新しいバージョンを入れる。

/etc/apt/sources.listを編集する。nanoと書かれている部分は適宜別のエディタ(vim等)に置き換えてよい。

$ sudo nano /etc/apt/sources.list

debで始まっている行を下にコピペし、wheezyと書いてある行をjessieに直す(←これらはDebianのバージョン)

例えば、

deb http://mirrordirector.raspbian.org/raspbian/ wheezy main contrib non-free rpi
deb http://mirrordirector.raspbian.org/raspbian/ jessie main contrib non-free rpi

のように、wheezyの行とjessieの行が共存した状態にする。

続いて、優先度を設定する。

$ sudo nano /etc/apt/preferences

まだこのファイルが無ければ、新しく作成してよい。以下のように編集する。

Package: *
Pin: release n=wheezy
Pin-Priority: 900

Package: *
Pin: release n=jessie
Pin-Priority: 300

Package: *
Pin: release o=Raspbian
Pin-Priority: -10

これで、原則としてwheezyを使うが、必要に応じてjessieを使うという状態になった。

aptのデータベースを更新する。

$ sudo apt-get update

jessieに入っているほうのgcc-4.8をインストールする。

$ sudo apt-get install gcc-4.8/jessie

とすれば良さそうだが、依存関係が壊れると言われるので、必要な依存関係を全て明示してinstallする。例えば、

$ sudo apt-get install gcc-4.8/jessie libmpfr4/jessie cpp-4.8/jessie libgcc-4.8-dev/jessie libgcc1/jessie libc6-dev/jessie libc-dev-bin/jessie libc6/jessie

とする。

念のため、gcc-4.8の依存関係のために書いたやつは自動でインストールしたとマークしておく。

$ sudo apt-mark auto libmpfr4 cpp-4.8 libgcc-4.8-dev libgcc1 libc6-dev libc-dev-bin libc6

下準備3: gccの特定バージョンをデフォルトにする

gccはalternativesに入っていないので、自分で追加する。

例えば、gcc-4.6, gcc-4.8が入っているときは、

$ sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-4.6 20
$ sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-4.8 50

のようにする。すると、gcc-4.8が優先度50で最大なのでデフォルトになる。

優先度に関わらず特定のバージョンをデフォルトにしたいときは、

$ sudo update-alternatives --config gcc

で所望のものを選択する。

$ gcc -v

で、所望のバージョン(記事執筆時点では4.8.3)が得られているかどうかを確認する。

下準備4: Linuxのソースコードを取得し、ビルドする

rpi-source を使って、Raspberry Pi用のLinuxのソースコードを取得する。

$ sudo wget https://raw.githubusercontent.com/notro/rpi-source/master/rpi-source -O /usr/bin/rpi-source && sudo chmod +x /usr/bin/rpi-source && /usr/bin/rpi-source -q --tag-update

ncurses-devを入れておく。

$ sudo apt-get install ncurses-dev

rpi-sourceを実行する。

$ rpi-source

rpi-sourceはカーネルソースを取得して必要な部分をビルドしてくれる。

成功すると、ホームディレクトリにlinuxというフォルダができる。/lib/modulesからここへのシンボリックリンクが貼られるので、これでカーネルモジュール作成の準備が整った。

ソースコードを取得する

mt7610u_wifi_sta_v3002_dpo_20130916.tar.bz2 というファイルを取得する。

MediaTekのサイトから、Linux用のMT7610U USBドライバーを取得するか、PlanexのサイトからLinux用のGW-450Dドライバーを取得する。どちらも同じものである。

これを解凍する。

$ tar jxvf mt7610u_wifi_sta_v3002_dpo_20130916.tar.bz2
$ cd mt7610u_wifi_sta_v3002_dpo_20130916

ドライバに必要な変更を加える

パッチを用意したのでこれを当ててもよい。手動で編集するはら以下のとおり。

linuxバージョンの差異への対応

include/os/rt_linux.hの

typedef struct _OS_FS_INFO_
{
	int				fsuid;
	int				fsuid;
	mm_segment_t	fs;
} OS_FS_INFO;

を、

typedef struct _OS_FS_INFO_
{
	kuid_t				fsuid;
	kgid_t				fsuid;
	mm_segment_t	fs;
} OS_FS_INFO;

と書き換える。

ベンダーID, プロダクトIDの追加

common/rtusb_dev_id.cの

USB_DEVICE_ID rtusb_dev_id[] = {
#ifdef MT76x0
	{USB_DEVICE(0x148F,0x7610)}, /* MT7610U */
	{USB_DEVICE(0x0E8D,0x7610)}, /* MT7610U */

となっている部分に、

USB_DEVICE_ID rtusb_dev_id[] = {
#ifdef MT76x0
	{USB_DEVICE(0x2019,0xAB31)}, /* GW-450D */
	{USB_DEVICE(0x04BB,0x0951)}, /* WN-AC433UK */
	{USB_DEVICE(0x148F,0x7610)}, /* MT7610U */
	{USB_DEVICE(0x0E8D,0x7610)}, /* MT7610U */

と追記する。

WPA Supplicantの設定

os/linux/config.mkの

# Support Wpa_Supplicant
# i.e. wpa_supplicant -Dralink
HAS_WPA_SUPPLICANT=n


# Support Native WpaSupplicant for Network Manager
# i.e. wpa_supplicant -Dwext
HAS_NATIVE_WPA_SUPPLICANT_SUPPORT=n

を、

# Support Wpa_Supplicant
# i.e. wpa_supplicant -Dralink
HAS_WPA_SUPPLICANT=y


# Support Native WpaSupplicant for Network Manager
# i.e. wpa_supplicant -Dwext
HAS_NATIVE_WPA_SUPPLICANT_SUPPORT=y

に変更する。

設定の変更

conf/RT2870STA.datの

SSID=11n-AP

を

SSID=

に変更する。また、

AuthMode=OPEN
EncrypType=NONE

を

AuthMode=WPA2PSK
EncrypType=AES

に変更する。(WPA2PSK/AESを使わない場合にどうすればよいかは未調査)

なぜか、デフォルトではconf/RT2870STA.datではなくconf/RT2860STA.datをインストールするようになってしまっているので、os/linux/config.mkの640行目あたりにある

ifneq ($(or $(findstring mt7650u,$(CHIPSET)),$(findstring mt7630u,$(CHIPSET)),$(findstring mt7610u,$(CHIPSET))),)
WFLAGS += -DMT76x0 -DRT65xx -DRLT_MAC -DRLT_RF -DRTMP_MAC_USB -DRTMP_USB_SUPPORT -DRTMP_TIMER_TASK_SUPPORT -DA_BAND_SUPPORT -DRTMP_EFUSE_SUPPORT -DNEW_MBSSID_MODE -DCONFIG_ANDES_SUPPORT
#-DRTMP_FREQ_CALIBRATION_SUPPORT
#-DRX_DMA_SCATTER
ifneq ($(findstring mt7650u,$(CHIPSET)),)
WFLAGS += -DMT7650
endif

ifneq ($(findstring mt7630u,$(CHIPSET)),)
WFLAGS += -DMT7630
endif

ifneq ($(findstring mt7610u,$(CHIPSET)),)
WFLAGS += -DMT7610
endif

ifneq ($(findstring $(RT28xx_MODE),AP),)
#WFLAGS += -DSPECIFIC_BCN_BUF_SUPPORT
endif

ifeq ($(HAS_CSO_SUPPORT), y)
WFLAGS += -DCONFIG_CSO_SUPPORT -DCONFIG_TSO_SUPPORT
endif

CHIPSET_DAT = 2860
endif

を見つけ(mt7610uと書いてあるのがポイント)、この末尾の

CHIPSET_DAT = 2860

を

CHIPSET_DAT = 2870

に変更する。

ビルド＆インストール

$ make
$ sudo make install

これでインストールされる。

あとは通常の無線LANドングルと同様に使用できる。

アップデートへの対応

rpi-updateでアップデートした場合、新しいカーネルが入ってくることがある。この場合、rpi-sourceを実行して対応するヘッダーファイル等を作成し、ドライバを再度ビルド＆インストールすればよい。

2014-09-30

Coqの新機能、Primitive Projectionについて

Coqリポジトリのtrunkを見ると、次の2つの機能が入っていることがわかります。

Universe Polymorphism
Primitive Projection

Universe Polymorphismは、グローバル定義をUniverseのレベルについて量化した形で定義することができる機能で、型に飾り付けをしたい場合(Homotopy n-typeやCategoryなどを定義したい場合)に宇宙ごとに異なる定義をする必要がなくなるという利点があります。

というのはさておき、この記事ではPrimitive Projectionを紹介します。

Primitive Projectionは、レコード型を定義したときにできる射影関数がプリミティブになるという機能です。Coqの内部で、普通の関数とは異なる特別な値として扱われるようです。

利点は次の2点のようです。

型検査の効率Up
η変換ができる

ここでは後者の点についてサンプルコードを示します。

(* 従来のレコード型 *)
Record Foo := Build_Foo {
  foo : unit
}.

Set Primitive Projections.

(* Primitive Projectionを有効にしたレコード型 (Primitive Recordと呼ぶ) *)
Record Bar := Build_Bar {
  bar : unit
}.

(* 従来のレコード型では、η変換はできない *)
Goal forall f : Foo, f = Build_Foo (foo f).
Proof.
  Fail reflexivity.
Abort.

(* Primitive Projectionを有効にしたレコード型では、η変換ができる *)
Goal forall b : Bar, b = Build_Bar (bar b).
Proof.
  reflexivity.
Qed.


(* どうやら、射影関数を自分で定義しても、同じ結果になるらしい？ *)

Definition foo2(f:Foo) : unit :=
  let (foo2) := f in foo2.

Goal forall f : Foo, f = Build_Foo (foo2 f).
Proof.
  Fail reflexivity.
Abort.

Definition bar2(b:Bar) : unit :=
  let (bar2) := b in bar2.

Goal forall b : Bar, b = Build_Bar (bar2 b).
Proof.
  reflexivity.
Qed.

補足

そもそも、関数に関するη変換が入ったのが最近 (Coq 8.4以降) です。サンプルコードを示します。

Goal (fun (f:nat->nat) (n:nat) => f n) = (fun (f:nat->nat) => f).
Proof.
  reflexivity.
Qed.

面倒なので確かめていませんが、このような証明は以前は成立しなかったはずです。

2014-04-22

よく使う Coq.Logic の公理

Coq.Logic にはCoqの集合論モデルにおいて正しい公理や、それらの間の関係が記述されている。

ここではその一部を取り上げて、意味を説明する。

前提知識

公理を仮定しない状態では、

Coqの論理は直観主義論理である。
ある2つが「等しい」という命題が証明できる場合は限定される。
証明の文脈(Prop)における「AまたはB」と、値の文脈(Set/Type)における「AまたはB」は区別される。前者から情報を取り出すことはできないようになっている(マッチングの型検査で弾かれる。)

以下、公理の説明

古典論理 (classical logic)

場所: Coq.Logic.Classical

古典論理で証明できることは、例えば以下の内容がある。

排中律 ( P or not P )
二重否定除去および背理法 ( if not not P, then P )

決定性の値の取り出し (description)

場所: Coq.Logic.Description

「条件を満たすものが唯一存在する」という命題から、具体的にその値を取り出す。

これによって証明できることは、例えば以下の内容がある。

二項関係であって関数としての条件を満たしているものから、関数を取り出す。

決定性の古典論理

場所: Coq.Logic.ClassicalDescription

名前どおり、Classical と Description を組み合わせたものである。

これによって証明できることは、例えば以下の内容がある。

ある命題が正しいかどうかによる条件分岐を、関数中に書くことができる。

ジョン・メジャーの等式 (John Major's equality)

場所: Coq.Logic.JMeq

「型Aとその値の対」について、「型も等しいし、その値も等しい」という関係を考える。

「型Aと値x」と「型Aと値y」がこの意味で等しいとき、 x = y である。しかしこれはCoqでは公理なしでは導けない。これを仮定するのが JMeq である。

関数外延性 (functional extensionality)

場所: Coq.Logic.FunctionalExtensionality

二つの関数が等しいとは、どの値を入れても等しいことである。しかしこれはCoqでは公理なしでは導けない。これを仮定するのが FunctionalExtensionality である。

命題外延性 (propositional extensionality)

二つの命題が同値(A <-> B, 互いから互いを導ける)ならば、二つの命題は等しい(A = B)とみなしてよい。これにちょうど対応する公理はなぜか Coq の標準ライブラリにはない。次を参照のこと。

部分集合についての集合外延性 (extensionality of ensembles)

場所: Coq.Sets.Ensembles

Aの部分集合を、所属関係を表す関数 A -> Prop で表すことにする。二つの部分集合が等しいとは、互いに包含していることとして定義される。

Ensembles に定義されている集合外延性 Extensionality_Ensembles は、関数外延性+命題外延性よりは弱く、関数外延性よりは強い。

非決定性の値の取り出し (indefinite description)

場所: Coq.Logic.IndefiniteDescription

「条件Pを満たす値が存在する」という命題から、具体的に値を取り出す。(一意性は要求されない。)これは明らかにDescriptionより強い公理である。

IndefiniteDescriptionで言えることは、集合論における「選択公理」から導けることとほぼ同じだと思ってよい。

2014-04-12

WindowsでCoqIDEの見た目をWindows風にする方法

%COQ%\share\themes\MS-Windows\gtk-2.0\gtkrc を %COQ%\etc\gtk-2.0 の下にコピーする。

ただし、%COQ%はCoqのインストールディレクトリのことを指すとする。たとえば %COQ% = C:\Program Files (x86)\Coq

f:id:qnighy:20140412221345p:plain

2014-04-02

C++で多倍長整数ライブラリGMPを使う

目的

GCJなど一部のプログラミングコンテストでは既存のライブラリを使用することが認められている。

特にC++であれば多倍長整数ライブラリとしてGMPを使うのが妥当であると考えられる。GMPを直接叩くのもよいが、GMPのC++バインディングを使うのが簡単であると考えた。

GMPのインストール

Cygwinの場合は、インストーラーから libgmp-devel とその依存関係をインストールすればよい。

Ubuntuの場合は、aptでlibgmp-devをインストールすればよい。

他の場合は未調査。

コンパイル

例えば、次のようにしてコンパイルする。(他のオプションは適宜補う)

g++ main.cpp -lgmpxx -lgmp

このとき、引数の順番に注意すること。
例えば、ライブラリ指定をコンパイル対象より前に置いてしまうと、次のようなエラーメッセージが出る。(ライブラリ指定を忘れた場合も同様)

/tmp/cco0O7Yl.o: In function `__gmp_binary_plus::eval(__mpz_struct*, __mpz_struct const*, __mpz_struct const*)':
main.cpp:(.text._ZN17__gmp_binary_plus4evalEP12__mpz_structPKS0_S3_[_ZN17__gmp_binary_plus4evalEP12__mpz_structPKS0_S3_]+0x27): undefined reference to `__gmpz_add'
/tmp/cco0O7Yl.o: In function `__gmp_binary_multiplies::eval(__mpz_struct*, __mpz_struct const*, __mpz_struct const*)':
main.cpp:(.text._ZN23__gmp_binary_multiplies4evalEP12__mpz_structPKS0_S3_[_ZN23__gmp_binary_multiplies4evalEP12__mpz_structPKS0_S3_]+0x27): undefined reference to `__gmpz_mul'
/tmp/cco0O7Yl.o: In function `__gmp_binary_multiplies::eval(__mpz_struct*, __mpz_struct const*, long)':
main.cpp:(.text._ZN23__gmp_binary_multiplies4evalEP12__mpz_structPKS0_l[_ZN23__gmp_binary_multiplies4evalEP12__mpz_structPKS0_l]+0x27): undefined reference to `__gmpz_mul_si'
/tmp/cco0O7Yl.o: In function `__gmp_expr<__mpz_struct [1], __mpz_struct [1]>::__gmp_expr()':
main.cpp:(.text._ZN10__gmp_exprIA1_12__mpz_structS1_EC2Ev[_ZN10__gmp_exprIA1_12__mpz_structS1_EC5Ev]+0x14): undefined reference to `__gmpz_init'
/tmp/cco0O7Yl.o: In function `__gmp_expr<__mpz_struct [1], __mpz_struct [1]>::__gmp_expr(int)':
main.cpp:(.text._ZN10__gmp_exprIA1_12__mpz_structS1_EC2Ei[_ZN10__gmp_exprIA1_12__mpz_structS1_EC5Ei]+0x20): undefined reference to `__gmpz_init_set_si'
/tmp/cco0O7Yl.o: In function `__gmp_expr<__mpz_struct [1], __mpz_struct [1]>::~__gmp_expr()':
main.cpp:(.text._ZN10__gmp_exprIA1_12__mpz_structS1_ED2Ev[_ZN10__gmp_exprIA1_12__mpz_structS1_ED5Ev]+0x14): undefined reference to `__gmpz_clear'
/tmp/cco0O7Yl.o: In function `std::ostream& operator<< <__mpz_struct [1], __mpz_struct [1]>(std::ostream&, __gmp_expr<__mpz_struct [1], __mpz_struct [1]> const&)':
main.cpp:(.text._ZlsIA1_12__mpz_structS1_ERSoS2_RK10__gmp_exprIT_T0_E[_ZlsIA1_12__mpz_structS1_ERSoS2_RK10__gmp_exprIT_T0_E]+0x32): undefined reference to `operator<<(std::ostream&, __mpz_struct const*)'
/tmp/cco0O7Yl.o: In function `__gmp_expr<__mpz_struct [1], __mpz_struct [1]>::__gmp_expr<__gmp_binary_expr<__gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_plus> >(__gmp_expr<__mpz_struct [1], __gmp_binary_expr<__gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_plus> > const&)':
main.cpp:(.text._ZN10__gmp_exprIA1_12__mpz_structS1_EC2I17__gmp_binary_exprIS2_S2_17__gmp_binary_plusEEERKS_IS1_T_E[_ZN10__gmp_exprIA1_12__mpz_structS1_EC5I17__gmp_binary_exprIS2_S2_17__gmp_binary_plusEEERKS_IS1_T_E]+0x18): undefined reference to `__gmpz_init'
/tmp/cco0O7Yl.o: In function `__gmp_expr<__mpz_struct [1], __mpz_struct [1]>::__gmp_expr<__gmp_binary_expr<__gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_multiplies> >(__gmp_expr<__mpz_struct [1], __gmp_binary_expr<__gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_multiplies> > const&)':
main.cpp:(.text._ZN10__gmp_exprIA1_12__mpz_structS1_EC2I17__gmp_binary_exprIS2_S2_23__gmp_binary_multipliesEEERKS_IS1_T_E[_ZN10__gmp_exprIA1_12__mpz_structS1_EC5I17__gmp_binary_exprIS2_S2_23__gmp_binary_multipliesEEERKS_IS1_T_E]+0x18): undefined reference to `__gmpz_init'
/tmp/cco0O7Yl.o: In function `__gmp_expr<__mpz_struct [1], __mpz_struct [1]>::__gmp_expr<__gmp_binary_expr<__gmp_expr<__mpz_struct [1], __gmp_binary_expr<long, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_multiplies> >, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_plus> >(__gmp_expr<__mpz_struct [1], __gmp_binary_expr<__gmp_expr<__mpz_struct [1], __gmp_binary_expr<long, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_multiplies> >, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_plus> > const&)':
main.cpp:(.text._ZN10__gmp_exprIA1_12__mpz_structS1_EC2I17__gmp_binary_exprIS_IS1_S4_IlS2_23__gmp_binary_multipliesEES2_17__gmp_binary_plusEEERKS_IS1_T_E[_ZN10__gmp_exprIA1_12__mpz_structS1_EC5I17__gmp_binary_exprIS_IS1_S4_IlS2_23__gmp_binary_multipliesEES2_17__gmp_binary_plusEEERKS_IS1_T_E]+0x18): undefined reference to `__gmpz_init'
/tmp/cco0O7Yl.o: In function `__gmp_expr<__mpz_struct [1], __mpz_struct [1]>::__gmp_expr<__gmp_binary_expr<long, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_multiplies> >(__gmp_expr<__mpz_struct [1], __gmp_binary_expr<long, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_multiplies> > const&)':
main.cpp:(.text._ZN10__gmp_exprIA1_12__mpz_structS1_EC2I17__gmp_binary_exprIlS2_23__gmp_binary_multipliesEEERKS_IS1_T_E[_ZN10__gmp_exprIA1_12__mpz_structS1_EC5I17__gmp_binary_exprIlS2_23__gmp_binary_multipliesEEERKS_IS1_T_E]+0x18): undefined reference to `__gmpz_init'
collect2: error: ld returned 1 exit status

サンプル

整数nとmを入力すると、フィボナッチ数列のn番目を計算するプログラム。

m = 1 のとき、再帰による計算を行う。(四則演算の回数は指数オーダー)
m = 2 のとき、動的計画法による計算を行う。(四則演算の回数は線形)
m = 3 のとき、行列累乗による計算を行う。(四則演算の回数は対数オーダー)

#include <iostream>
#include <gmpxx.h>

mpz_class fib1(int), fib2(int), fib3(int);

int main() {
  int n, m;
  std::cin >> n >> m;
  if(m == 1) {
    std::cout << fib1(n) << std::endl;
  } else if(m == 2) {
    std::cout << fib2(n) << std::endl;
  } else if(m == 3) {
    std::cout << fib3(n) << std::endl;
  }
  return 0;
}

mpz_class fib1(int n) {
  if(n <= 1) return n;
  else return fib1(n - 1) + fib1(n - 2);
}

mpz_class fib2(int n) {
  mpz_class a = 1, b = 0;
  for(int i = 0; i < n; ++i) {
    swap(a, b);
    b += a;
  }
  return b;
}

mpz_class fib3(int n) {
  mpz_class a = 1, b = 0, c, d;
  for(int i = 30; i >= 0; --i) {
    c = a * a + b * b;
    d = b * (2 * a + b);
    if((n >> i) & 1) {
      b = c + d;
      swap(a, d);
    } else {
      swap(a, c);
      swap(b, d);
    }
  }
  return b;
}

解説

mpz_classは、GMPの多倍長整数のC++によるラッパークラスである。これはintとほぼ同じように取り扱うことができる。

四則演算はほぼ通常通り使える。
iostreamを用いる場合は、intと同様に読み書きできる。
intからの自動キャストがある。

mpz_classは通常の整数型とは違い、生成コストやコピーコストに気を使ったほうがよい場面がある。vectorと同様、mpz_classには高速なswapが定義されているので、それを用いるのがよい(気がする)。

最近のGMPのC++バインディングにはムーブコンストラクタが定義されている。C++11を使うとコピーコストが低くなる場面があるかもしれない。(未検証)

2014-01-18

PowerPC64アセンブリ開発環境の整備

目的

PowerPC64アセンブリの演習のための環境を手元で構築する．

前提

Ubuntu 13.10 (x86_64) を利用していると仮定する．

crosstool-ngの導入

必要なパッケージの準備

$ sudo apt-get install build-essential gperf texinfo gawk libtool automake libncurses5-dev

ソースコードを入手してビルド

$ wget http://crosstool-ng.org/download/crosstool-ng/crosstool-ng-1.19.0.tar.bz2
$ tar jxvf crosstool-ng-1.19.0.tar.bz2
$ cd crosstool-ng-1.19.0
$ ./configure
$ make
$ sudo make install

bash用の補完プラグインを入れる

入れなくても良い

sudo cp ct-ng.comp /etc/bash_completion.d/

PowerPC64用クロスコンパイラのビルド

必要なパッケージを入れる

これらはcross-gdbのビルドに必要(入れていないとビルドの最後のほうで失敗して泣く)

$ sudo apt-get install libexpat1-dev python2.7-dev

ソースを補完するディレクトリを掘る

デフォルトだとホームの下のsrcに設定されている．ディレクトリがないと保存されないので掘っておく

$ mkdir ~/src

作業ディレクトリを掘る

$ mkdir ppc64-toolchain
$ cd ppc64-toolchain

powerpc64-unknown-linux-gnu用に設定する

$ ct-ng powerpc64-unknown-linux-gnu

設定をいじる

$ ct-ng menuconfig

設定画面の使い方

上下: 選択肢の移動
スペース: 選択肢の選択
左右: <Select> / <Exit> / <Help> の間を移動
Enter: <Select> / <Exit> / <Help> のうち選択されているものを実行

推奨の設定: FortranとJavaを外す

上下キーで C compiler ---> に移動，スペースで中に入る
上下キーで [*] Fortran に移動，スペースでチェックを消す
上下キーで [*] Java に移動，スペースでチェックを消す
左右キーで < Exit > を選択，Enterで実行→外に出る
左右キーで < Exit > を選択，Enterで実行→設定終了

終了時に設定を保存するか聞かれるのでYesと答える

ビルド実行

$ ct-ng build

あとはひたすら待つと勝手にビルドとインストールを実行してくれる

インストール先はデフォルトでは次のような構成

~/x-tools
~/x-tools/powerpc64-unknown-linux-gnu
~/x-tools/powerpc64-unknown-linux-gnu/bin
~/x-tools/powerpc64-unknown-linux-gnu/include
~/x-tools/powerpc64-unknown-linux-gnu/lib
~/x-tools/powerpc64-unknown-linux-gnu/libexec
~/x-tools/powerpc64-unknown-linux-gnu/powerpc64-unknown-linux-gnu
~/x-tools/powerpc64-unknown-linux-gnu/share

例えば，binの中身は次のようになっている

powerpc64-unknown-linux-gnu-addr2line
powerpc64-unknown-linux-gnu-ar
powerpc64-unknown-linux-gnu-as
powerpc64-unknown-linux-gnu-c++
powerpc64-unknown-linux-gnu-cc
powerpc64-unknown-linux-gnu-c++filt
powerpc64-unknown-linux-gnu-cpp
powerpc64-unknown-linux-gnu-ct-ng.config
powerpc64-unknown-linux-gnu-embedspu
powerpc64-unknown-linux-gnu-g++
powerpc64-unknown-linux-gnu-gcc
powerpc64-unknown-linux-gnu-gcc-4.5.2
powerpc64-unknown-linux-gnu-gccbug
powerpc64-unknown-linux-gnu-gcov
powerpc64-unknown-linux-gnu-gdb
powerpc64-unknown-linux-gnu-gdbtui
powerpc64-unknown-linux-gnu-gprof
powerpc64-unknown-linux-gnu-ld
powerpc64-unknown-linux-gnu-ldd
powerpc64-unknown-linux-gnu-nm
powerpc64-unknown-linux-gnu-objcopy
powerpc64-unknown-linux-gnu-objdump
powerpc64-unknown-linux-gnu-populate
powerpc64-unknown-linux-gnu-ranlib
powerpc64-unknown-linux-gnu-readelf
powerpc64-unknown-linux-gnu-size
powerpc64-unknown-linux-gnu-strings
powerpc64-unknown-linux-gnu-strip

コンパイルする

PATHの追加

環境変数PATHを追加する．

$ export PATH=$HOME/x-tools/powerpc64-unknown-linux-gnu/bin:$PATH

これを毎回実行するのは面倒なので，~/.bashrcに追記する．

$ echo 'export PATH=$HOME/x-tools/powerpc64-unknown-linux-gnu/bin:$PATH' >> ~/.bashrc

サンプルソースコード

次のようなCソースコードをhello.cという名前で作成する．

#include <stdio.h>

int main() {
  puts("Hello, world!");
  return 0;
}

コンパイル

コンパイルする

$ powerpc64-unknown-linux-gnu-gcc hello.c
$ file a.out
a.out: ELF 64-bit MSB executable, 64-bit PowerPC or cisco 7500, version 1 (SYSV), dynamically linked (uses shared libs), for GNU/Linux 2.6.31, not stripped

確かにPowerPC64用のバイナリである．

アセンブリソースの出力

アセンブリのソースを出力してみる

$ powerpc64-unknown-linux-gnu-gcc -S hello.c
$ cat hello.s
	.file	"hello.c"
	.section	".toc","aw"
	.section	".text"
	.section	.rodata
	.align 3
.LC0:
	.string	"Hello, world!"
	.section	".toc","aw"
.LC1:
	.tc .LC0[TC],.LC0
	.section	".text"
	.align 2
	.globl main
	.section	".opd","aw"
	.align 3
main:
	.quad	.L.main,.TOC.@tocbase,0
	.previous
	.type	main, @function
.L.main:
	mflr 0
	std 0,16(1)
	std 31,-8(1)
	stdu 1,-128(1)
	mr 31,1
	ld 3,.LC1@toc(2)
	bl puts
	nop
	li 0,0
	mr 3,0
	addi 1,31,128
	ld 0,16(1)
	mtlr 0
	ld 31,-8(1)
	blr
	.long 0
	.byte 0,0,0,1,128,1,0,1
	.size	main,.-.L.main
	.ident	"GCC: (crosstool-NG 1.19.0) 4.5.2"

確かにPowerPC64のアセンブリコードが出力されている．

実行

生成されたバイナリはPowerPC64用なのでそのままでは実行できない．

$ ./a.out
bash: ./a.out: cannot execute binary file

そこで，エミュレーター QEMUのユーザーモードエミュレーション機能を用いる．

qemu-userのインストール

$ sudo apt-get install qemu-user

QEMU_LD_PREFIXの設定

このままでは先ほどのa.outを実行できない．というのも，依存しているライブラリがあり，QEMUがその場所を把握していないからである．

QEMU_LD_PREFIX環境変数を設定

$ export QEMU_LD_PREFIX=$HOME/x-tools/powerpc64-unknown-linux-gnu/powerpc64-unknown-linux-gnu/

これも毎回実行するのは面倒なので，~/.bashrcに追記しておく．

$ echo 'export QEMU_LD_PREFIX=$HOME/x-tools/powerpc64-unknown-linux-gnu/powerpc64-unknown-linux-gnu/' >> ~/.bashrc

a.outを実行してみる

$ qemu-ppc64 ./a.out
Hello, world!

無事実行できた！

デバッガの利用

powerpc64-unknwon-linux-gnu-gdb自体はPowerPC64コードを実行する機能をもたないようなので，qemu-ppc64で実行しているものを遠隔操作する方法を用いる．(リモートデバッグという)

デバッグオプションをつけてコンパイル

デバッガを使う上で-gをつけないと余りに不便．

$ powerpc64-unknown-linux-gnu-gcc -g hello.c

プログラムを実行

12345のところはポート番号なので，他の数字でもよい．このポートにgdbから接続する．

$ qemu-ppc64 -g 12345 ./a.out

こうすると，qemu-ppc64は待機状態になる．

デバッガを起動

別の端末を開いて，gdbを起動する．

$ powerpc64-unknwon-linux-gnu-gdb a.out

実行中のqemu-ppc64に接続する．

(gdb) target remote localhost:12345

これでデバッグの準備が整った．

デバッガを使う

ブレークポイントを設定してみる

(gdb) b main
Breakpoint 1 at 0x1000051c: file hello.c, line 4.

実行してみる

(gdb) c
Continuing.

Breakpoint 1, main () at hello.c:4
4	  puts("Hello, world!");

r (run) ではなくc (continue) であることに注意！

もう一回continueするとputsが実行されて終了する．このとき，qemu-ppc64を実行している端末でHello, world!が出力されるので確認すること．

(gdb) c
Continuing.
[Inferior 1 (Remote target) exited normally]

gdbを終了する．

(gdb) q

Strictly conforming program

Conforming implementation

Conforming program

識別子

math.h

M_PIを定義してはいけない理由

実際のコンパイラー

_USE_MATH_DEFINES

まとめ

前提知識

下準備1: カーネルビルドに用いられたGCCのバージョンを調べる

下準備2: gccを入れる

下準備3: gccの特定バージョンをデフォルトにする

下準備4: Linuxのソースコードを取得し、ビルドする

ソースコードを取得する

ドライバに必要な変更を加える

linuxバージョンの差異への対応

ベンダーID, プロダクトIDの追加

WPA Supplicantの設定

設定の変更

ビルド＆インストール

アップデートへの対応

補足

前提知識

古典論理 (classical logic)

決定性の値の取り出し (description)

決定性の古典論理

ジョン・メジャーの等式 (John Major's equality)

関数外延性 (functional extensionality)

命題外延性 (propositional extensionality)

部分集合についての集合外延性 (extensionality of ensembles)

非決定性の値の取り出し (indefinite description)

目的

GMPのインストール

サンプル

解説

目的

最新情報へのリンク

前提

crosstool-ngの導入

必要なパッケージの準備

ソースコードを入手してビルド

bash用の補完プラグインを入れる

PowerPC64用クロスコンパイラのビルド

必要なパッケージを入れる

ソースを補完するディレクトリを掘る

作業ディレクトリを掘る

powerpc64-unknown-linux-gnu用に設定する

設定をいじる

ビルド実行

コンパイルする

PATHの追加

サンプルソースコード

アセンブリソースの出力

実行

qemu-userのインストール

QEMU_LD_PREFIXの設定

a.outを実行してみる

デバッガの利用

デバッグオプションをつけてコンパイル

プログラムを実行

デバッガを起動

デバッガを使う