Cソースで静的に動作する（半）自動検証ソフトウェア（CBMC （リンク） ）を使用する必要があります。浮動小数点はサポートされていますが、すべての数学関数の定義はありません。それを使って数値計算ソフトウェアをチェックできるかどうかをチェックしようとしています。
だから私はこれらの機能が必要です。コプロセッサを使用しない定義を探していmath.hます(例: sqrt、pow、剰余、tan; int/ float/ double)。
いくつかの Linux ディストリビューション (おそらく今は eglibc) に同梱されている libc でそれを探したとき、たとえばハードウェアの sqrt 関数を意味するプロセッサ組み込み関数がいくつかあるポイントに常に到達しました。
パート 1: ソフトウェア実装の検索
私が必要としているのは、次の特性を持つ数学関数をサポートするライブラリです。
- IEEE 浮動小数点がサポートされていますが、純粋に整数で動作するライブラリも素晴らしいでしょう。
- 正確さは重要な要素です。(一部の情報源に隠されている特殊なケースの既知のバグはそれほどクールではありません)。結果は、IEEE-754 に関しても正しいはずです (例: sqrt のルール)。
- コプロセッサ呼び出しを使用しません。純粋なソフトウェア。C が推奨されますが、asm でもかまいません。
これまで、さまざまな libc 実装、特に組み込みシステムに関するものを少し探してきました。これらのライブラリのほとんどは、コンパイルされたプログラムの移植性とサイズをターゲットにしていると思いますが、プロセッサ固有の命令を使用しているかどうかを判断するのは困難です。
- ** fdlibmは、一見、純粋なソフトウェア定義をいくつか持っているように見えます。これをさらに検査します。ただし、ソースにはいくつかのバグが記載されています (コードは標準ではありません)。
- ** newlibは同じ定義を持っているようです (Sun Microsystems のコードに基づく)。しかし、これらのソフトウェア バージョンが常に使用されているかどうかは、現時点でははっきりとは言えません。そのため、現時点では見られないコプロセッサ コールがいくつかある可能性があります (パート 2 を参照)。
- ** uClibcは newlibと特徴を共有しているようです。
パート 2: これらの実装の構造を理解する
これらの数学ライブラリの構造を簡単に紹介してくれませんか。さまざまなバージョン (特定のコプロセッサなど) はどのようにディスパッチされますか?
そして、ファイル名のこれらの異なる接頭辞の意味は何ですか.
e_sqrt.c、k_sin、s_sin?
私にとって有用なライブラリについて教えていただければ幸いです。私はライブラリをそのまま使用することを好みますが、必要な場合は、いくつかの単一関数の実装を探して、小さなライブラリを構築することもできます。math.h で定義されているすべての関数を使用するわけではありません。
thisおよびthis SO-posts は、Java Math 実装がfdlibmに基づいている/だったと言っています。これは、このライブラリが進むべき道であるように聞こえます。私が知っておくべきこのライブラリについてもっと情報を持っている人はいますか?
次の2つを含む多くの可能性があるようです：
- glibc を使用し、ソフトウェア モードでコンパイルします。問題は、(configure で) 自動システム チェック ツールを使用できないことです。すべての情報を手動で提供する必要があります。fp コプロセッサーの使用を禁止し、simd 操作を禁止するフラグはありますか? fp-without から始める必要があり、コンパイルするとソフトフロートも使用されます。コンパイルプロセスは、多かれ少なかれホストの特定の決定に依存していると思います（アームなど）。
- fdlibm を使用します(現時点では推奨)。問題: プログラムをリンクするにはどうすればよいですか? assert のような非 libm 関数が必要ですが、インストールされている system-libm ではなく、私の fdlibm に対してリンクしたい (したがって、-nodefaultlibs は assert の使用を禁止します)。