分段故障哈斯克爾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

回答

相關問題