更改代码以在Solaris上构建z3

我需要在Solaris 8上构建z3 building。我查看了文件scoped_timer.cpp，它是唯一使用-D_LINUX_的地方，并且我可以获得正确的代码在Solaris中使用-D_SOLARIS_来保护它。另外，需要更改src/util/hwf.cpp以提供fma（）和nearbyint（）的定义，这些定义在Solaris 8上未定义。也可以通过定义fma（x，y，z ）是x * y + z，但是接下来会有两次舍入，而不是一次，这是IEEE 754要求的。这对于z3的目的会造成问题吗？我还需要更改mk_util.py来为Solaris设置编译和链接选项。由于我们在Solaris上使用g ++，这也看起来相当可行，所以编译选项会类似。链接选项可能需要额外的库。我愿意做一些工作，但我可能需要帮助。任何人都愿意和我一起工作，这是否会受到欢迎？更改代码以在Solaris上构建z3

来源

2015-10-13 Tom Kacvinsky

什么是您的硬件？ x86还是SPARC？较旧的硬件往往不具备真正的FMA指令 - SPARC在2007年获得了它，x86不是直到2011年才用于AMD，而是2013年用于英特尔。另外，如果您可以为您的硬件获得Solaris Studio的副本。查看安装目录的.../prod/lib目录下的所有'math.il'文件。这些文件是内联数学例程的汇编指令。在我安装Solaris Studio 12.3的x86安装中有一个'nearbyint（）'实现。 –

当我尝试在OpenBSD/SPARC上编译Z3时遇到了以下情况：从某些旧版本开始，内存管理器可能错误地认为，由于您没有使用AMD64，所以您的处理器是32位，因此内存分配器可以使用4-字节对齐一切。在SPARC64上，情况并非如此，需要8字节对齐。小心。 – mtrberzi

我们使用SPARC Solaris 8构建32位应用程序。我厌倦了Sun Studio 11的构建，因为版本12在Solaris上不受支持，但有很多编译器错误。我确实可以访问Solaris 10和Sun Studio 12，所以我可以尝试一下，但是我不愿意这样做，因为我们的一些用户仍然是儿子Solaris 8. –

这会是一个受欢迎的补充吗？

我想我们可以在准备就绪时（并且不会遮挡其他设置）进行拉取请求，并且至少有两个用户。通常的条件适用于取得请求https://github.com/Z3Prover/z3/wiki/Contribution-Guidelines。当然，您可以拥有自己的分支而不需要合并变更。

另一个问题可能是您的计算机上的字节序和内存对齐方面的限制可能会暴露更多的可移植性问题。您应该能够通过在z3test存储库下运行回归测试（以及单元测试）来查找问题。我们最近修复了ARM/PowerPC的一些排序相关问题。

来源

2015-10-14 00:01:30

好的，请牢记这一点。现在，我只是高举了FreeBSD配置，但我会清理一些事情，以便Solaris有特定的配置/代码更改。 –

我有一个堆栈跟踪是什么或者排序问题，但我认为我将不得不做一个新的帖子，因为堆栈跟踪花了很长时间来发表评论。 –

更改代码以在Solaris上构建z3

回答

相关问题