0

Z3 (2012-12-21 git バージョン、最新の「マスター」リリース) を使用してツールの移植性を確認していたので、Sparc64 で Z3 をコンパイルしてみました。src/util/hwf.cppIA64だけでなく、Sparc64をSIMD組み込み関数とemmintrin.h. コンパイルは成功しました。

残念ながら、結果として得られる実行可能ファイルは、起動時にバス エラーでクラッシュしますprime_generator::prime_generator()。理由がわかりません。

Program received signal SIGBUS, Bus error.
0x009b1dac in global constructors keyed to _ZN15prime_generatorC2Ev ()
(gdb) bt
#0  0x009b1dac in global constructors keyed to _ZN15prime_generatorC2Ev ()

これは私にとってはあまり重要ではありませんが (私たちのマシンは x86 または x86-64 です)、一部の組み込みアプリケーションには関係があるかもしれません。

4

1 に答える 1

1

x86 以外のマシンで Z3 を実行することに関心があったとは思わないので、いくつかの問題が見つかる可能性が高いでしょう。

特に SPARC では、x86 のようにアラインされていないメモリ アクセスは許可されません。ざっと見てみると、不整合が発生する可能性のあるいくつかのポイントがわかりました。たとえば、memory::allocate() は、malloc によって返されたポインターを sizeof(size_t) だけデアラインします。それが 64 ビットでない場合、クラッシュします (svector データのため)。次に、svector の割り当ても、データの前に 2*sizeof(unsigned) を予約します。2*sizeof(unsigned) が sizeof(uint64) の倍数でない場合、クラッシュが発生します。

等々。重要なのは、それ以上の情報がなければ、あなたを助けることは不可能だということです. -g を指定してコンパイルする必要があります。必要に応じて、クラッシュしているアセンブリ コードを出力して、正確な場所を特定するのに役立ててください。

また、 master ブランチは使用しないでください。それはとても古いです。不安定なブランチの使用を検討してください (名前が聞こえるかもしれませんが、それほど悪くはありません:)

于 2014-02-12T10:56:13.873 に答える