-
Notifications
You must be signed in to change notification settings - Fork 33
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Using cvc5
on Windows goes into an infinite loop
#644
Comments
If I put the SMT2 interaction into its own file: ; diagnostic.smt2
(set-option :print-success true)
(set-option :global-declarations true)
(set-option :diagnostic-output-channel "stdout") And then run
The fact that it is trying to open a file named |
It is surprising we fail to catch that indeed. Alas, I don't have a Windows machine to try it on. Definitely needs debugging. I wonder if the cvc5 process dies before we get access to the output. To be honest, while "happy path" is tested on Windows, the failure paths are almost never tested on anything but a Mac. If anyone has access to a windows machine and can do some debugging, it'd be much appreciated. |
I can help with this. Where should I start? |
Let's first try to figure out if CVC5 has to be involved. I'd start with creating a fake solver script:
You'll have to create the equivalent of that that works on Windows; like a
The above is on a Mac, and is the desired/expected behavior. If this loops forever too on Windows, then we can start looking into SBV itself. If it works well, then I suppose CVC5 is somehow involved and we have to look at if it's crashing and leaving the handle open still. (I'm guessing the latter, but the above is a quick way to see it's not a pure "SBV on Windows" problem. |
@RyanGlScott Looks like CVC5 folks actually fixed the issue with the filenames; so if you're looking for a workaround, simply upgrading your CVC5 to their latest might do the trick. I still would like to fix this issue from an SBV perspective, of course. So, please keep the ticket open in either case. |
I wrote a Haskell program that does the same thing as your module Main where
main :: IO ()
main = do
_ <- getLine
putStrLn "(error \"Error in option parsing: Cannot open file: `\"\"stdout\"\"': unknown reason\")" And then compiled it to
|
Ah, I think I see what's going on here. The good news is that this isn't a Windows or CVC5 issue. And here's how to replicate on any platform: module Main where
import System.IO
main :: IO ()
main = do
_ <- getLine
putStrLn "success"
hFlush stdout
_ <- getLine
putStrLn "success"
hFlush stdout
_ <- getLine
putStrLn "success"
hFlush stdout
_ <- getLine
hPutStrLn stderr "(error \"Error in option parsing: Cannot open file: `\"\"stdout\"\"': unknown reason\")"
hFlush stdout
_ <- getLine
pure () Note that this program puts the error message to Shouldn't be too hard to fix, let me see what I can do.. |
@RyanGlScott Just committed 8b226c3, which should resolve this issue, I think. (It'll still fail of course, but won't hang and will print something useful to the user.) Can you give this a try on your Windows machine to see how it goes? |
Hm, I think there is still something not quite right. If I run the program in #644 (comment) in GHCi using commit 8b226c3, then it still goes into an infinite loop:
Very strangely, however, if I first compile the program and then run the resulting executable, then it does terminate. However, it's far from instant, as it takes about five seconds to get unstuck:
I'm not quite sure what to make of this. |
@RyanGlScott I had another go to clean-up the code, there was some extra blocking. Note that SBV always does a 5-second wait in case something goes wrong. This allows the solver to spit out as much as it can, so we can grab it from stdout/stderr and not kill the process prematurely. Perhaps this wait is way too long. But since this should be a rare occurrence (assuming there are no bugs), perhaps it's not too terrible. So, do expect a wait at the end for a little bit. But I'm hoping ba7178e will work as expected. Can you give that a try? |
Bummer.. Can you test it by faking cvc with the following program: module Main where
import System.IO
main :: IO ()
main = do
_ <- getLine
putStrLn "success"
hFlush stdout
_ <- getLine
putStrLn "success"
hFlush stdout
_ <- getLine
hPutStrLn stderr "(error \"Error in option parsing: Cannot open file: `\"\"stdout\"\"': unknown reason\")"
hFlush stdout
_ <- getLine
pure () On my Mac, it works with this "fake" solver. I'd like to know what the behavior is on Windows. |
After setting
At this point, I have to kill the process to make it stop. A similar hang happens in GHCi, except that I am able to Ctrl-C it successfully after the hang. |
Just to make sure I'm not imagining things, if you could try the same experiment on a Linux/Mac machine, that'd be great. That way we can focus on this being a Windows only problem. If that's the case (i.e., if you also get it working fine on Mac/Linux), then I'd suspect something fishy is going on with: Line 769 in ba7178e
when run on Windows. We will need to put a print statement around there to see what's going on I guess. If you can experiment with that, it'd be really nice. Otherwise, I'll need to figure out how to acquire a windows machine to debug, perhaps you have one that can grant me remote access somehow? |
Indeed, I can confirm that the fake solver does in fact terminate on Linux:
I'll add some debug printing around the call to |
Great! So, this is a Windows problem only, and has really nothing to do with CVC5. Could have something to do with buffering, we might have to explicitly set buffering options. I thought the Posix layer made programs work in exactly the same way on different OSs, but I suppose that's not true. Note that, at this point, it should also be possible to create a failing test case that has nothing to do with SBV. Establish a pipe, and do a timeout based read from a channel that the corresponding process writes something to. (Or along those lines.) This way it might be easier to debug, and also report to GHC folks if it ends up being something they need to take a look at. |
Your mention of POSIX made me remember that GHC on Windows actually has two IO managers: there is
And with
(That output is rather weird, but one problem at a time.) So the bug is about diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs
index 4c109d05..f98bc8e7 100644
--- a/Data/SBV/SMT/SMT.hs
+++ b/Data/SBV/SMT/SMT.hs
@@ -766,7 +766,16 @@ runSolver cfg ctx execPath opts pgm continuation
-- Carefully grab things as they are ready. But don't block!
collectH handle = reverse <$> coll ""
- where coll sofar = do b <- hReady handle
+ where coll sofar = do putStrLn $ unlines
+ [ "RGS coll 1"
+ , show handle
+ , sofar
+ ]
+ b <- hReady handle
+ putStrLn $ unlines
+ [ "RGS coll 2"
+ , show b
+ ]
if b
then hGetChar handle >>= \c -> coll (c:sofar)
else pure sofar
And here is what I get when running with
At which point the program hangs. I get the same output regardless of whether I use the real |
Great sleuthing! At this point, your knowledge of this problem is beyond mine.. I'll assign this ticket to you and feel free to submit a PR if anything needs to change on the SBV side.. Thanks! |
Do you think you could help me distill down a small, channel-based example (like the one you refer to in #644 (comment)) that does the same inter-process communication that SBV does? I could try to do this myself, but since I am not familiar with the code in SBV, it would probably take me much longer to minimize the issue. |
Sure.. I'll give it a shot; sometime next week I hope. |
Thanks! |
Maybe something like this? $ cat Producer.hs
module Main where
import System.IO
main :: IO ()
main = do
s <- getLine
putStrLn $ "Responding to: " ++ s
hFlush stdout
_ <- getLine
pure ()
$ cat Consumer.hs
module Main (main) where
import Control.Concurrent
import System.Environment
import System.Process
import System.IO
main :: IO ()
main = do
args <- getArgs
pgm <- case args of
[p] -> pure p
_ -> error "Pass the path to the producer executable"
(inp, out, _, _) <- runInteractiveProcess pgm [] Nothing Nothing
hPutStrLn inp "Hello"
hFlush inp
threadDelay 1000000
let collect = reverse <$> go ""
go sofar = do isReady <- hReady out
if isReady
then do c <- hGetChar out
go (c : sofar)
else pure sofar
s <- collect
putStrLn $ "Producer says: " ++ s
$ cat test
ghc -o Producer Producer.hs
ghc -o Consumer Consumer.hs
./Consumer ./Producer Then:
I wonder how this behaves on Windows with both io-managers. If the native one terminates but posix doesn't, I think you'd have a smoking gun. |
Thanks for the minimal example!
(I used GHC 9.2.7 above, but I get the same results with 9.4.4 and 9.6.1-alpha3 as well.) That being said,
That's not a hang: it just prints out " |
It is bizarre indeed. I'm not sure if the cure to this will cure SBV; whose communication is a bit more involved. (It uses both stdout and stderr, maybe that plays a role. Also a call to timeout..) But let's see what the GHC guys have to say about this; perhaps whatever they propose can be adopted to SBV. |
The
And
The latter in particular is quite strange. I wonder if I can reproduce this independently of SBV by spawning a |
Oh, this sounds real bad.. Definitely needs debugging! |
Interestingly, removing the use of the diff --git a/Data/SBV/Provers/CVC5.hs b/Data/SBV/Provers/CVC5.hs
index c26af933..759e053c 100644
--- a/Data/SBV/Provers/CVC5.hs
+++ b/Data/SBV/Provers/CVC5.hs
@@ -28,7 +28,7 @@ cvc5 = SMTSolver {
name = CVC5
, executable = "cvc5"
, preprocess = clean
- , options = const ["--lang", "smt", "--incremental", "--no-interactive", "--nl-cov"]
+ , options = const ["--lang", "smt", "--incremental", {-"--no-interactive",-} "--nl-cov"]
, engine = standardEngine "SBV_CVC5" "SBV_CVC5_OPTIONS"
, capabilities = SolverCapabilities {
supportsQuantifiers = True
|
Interesting. Does it actually work without that setting? If memory serves, without that setting cvc printed a lot of headers and stuff. That’d certainly throw SBV off, I think. Doesn’t it? |
I ran all of the SBV test cases that mention
I didn't see this when testing
Very strangely, this doesn't happen if I run the same |
Fantastic! Great sleuthing. And I was able to get a clean test-suite run on my Mac after removing the Everything is committed to SBV head, if you want to do some testing with that. |
Great! I am now able to run all of the SBV test cases involving |
Awesome. I think we can close this ticket now though? I don't think there's much left for SBV to do regarding this problem. |
This simple SBV program that uses CVC5 works fine on Linux:
However, it goes into an infinite loop on Windows. Here is all the output that it produces before looping:
At this point, I have to kill the GHC process. I'm unclear if this is an SBV issue or a CVC5 one, but it does seem odd that SBV wouldn't catch the failure and proceed. In case it's relevant, I'm using SBV 9.2 and:
The text was updated successfully, but these errors were encountered: