分段故障哈斯克尔Z3 API

我使用的Haskell这个Z3包，密切镜（和利用的，通过Haskell的外部函数接口）的C API：https://hackage.haskell.org/package/z3 分段故障哈斯克尔Z3 API

我得到一个分段错误，并设法将其降低到以下几点：

mainx = do 
    print =<< intCheck [0..70] 

intCheck :: [Int] -> IO [Int] 
intCheck [] = return [] 
intCheck (x:xs) = 
    do 
     checking <- evalZ3 $ checkImpact x 
     print checking 
     return =<< intCheck xs 

checkImpact :: Int -> Z3 Result 
checkImpact r = do 
    reset 

    xSymb <- mkStringSymbol "x" 
    x <- mkConst xSymb =<< mkIntSort 
    trace ("asserting = " ++ show r) assert =<< mkEq x x 

    solverCheck

输出是：

asserting = 0 
Sat 
asserting = 1 
Sat 
asserting = 2 
Sat 
...[omitted] 
asserting = 45 
Sat 
asserting = 46 
Segmentation fault: 11

通常情况下，最后断言大约是46的地方，BU它的执行情况各不相同。我最好的猜测是内存没有被正确释放（我无法弄清楚为什么它会在稍微不同的地方停下来），但我不确定这是递归问题（在intCheck中），还是与z3 API。

在此先感谢您的帮助！

来源

2016-09-06 Bill

我会在haskell软件包中打开一个bug报告，如果出现问题，让他们处理上游问题 – jberryman

我已经完成了tha t： https://bitbucket.org/iago/z3-haskell/issues/12/possible-error-in-package 如果iago在那里回复，而不是在这里，我会发布更新。 – Bill

我看到你粘贴的代码中有一个间距问题（对齐do）。请确保这是否是导致您的问题的代码。

我无法重现您的问题：

% ghc so.hs -fforce-recomp && ./so 2>&1 | tail ; ghc --version ; z3 -version 
[1 of 1] Compiling Main    (so.hs, so.o) 
Linking so ... 
Sat 
Sat 
Sat 
Sat 
Sat 
Sat 
Sat 
Sat 
Sat 
[] 
The Glorious Glasgow Haskell Compilation System, version 7.10.3 
Z3 version 4.4.1

哦，还有：

% ghc-pkg list z3 
    z3-4.1.0

编辑：匹配GHC和Z3的版本，我仍然无法重现该问题：

% LD_LIBRARY_PATH=$HOME/lib ghc so.hs -fforce-recomp && LD_LIBRARY_PATH=$HOME/lib ./so 2>&1 | tail ; ghc --version ; z3 -version 
[1 of 1] Compiling Main    (so.hs, so.o) 
Linking so ... 
Sat 
Sat 
Sat 
Sat 
Sat 
Sat 
Sat 
Sat 
Sat 
[] 
The Glorious Glasgow Haskell Compilation System, version 8.0.1 
Z3 version 4.3.2

来源

2016-09-06 20:05:34

对不起，关于这个错误 - 我不得不重新将所有东西都复制粘贴到SO后面，并搞砸了那个部分（现在已经修复了）。我们有不同版本的ghc（我在8.0.1上）和z3（I '对4.4.2。）虽然相同版本的z3 haskell包。你是否用0到70（或其他更大的数字）运行它，并减少你的输出？当我仅使用[0..9]时，我不会收到段错误错误。 – Bill

我跑0..70，只是你的代码与固定的缩进。 –

好的，非常感谢您无论如何看待它。我倾向于怀疑它与ghc有关，但我会看看是否可以用7.10.3来实现，以防万一。 – Bill

分段故障哈斯克尔Z3 API

回答

相关问题