MacOS: fails to recognize installed Z3 solver #1488
Comments
|
Some additional information that would be helpful for debugging this:
|
|
$ uname -a
Darwin 549725-mitll 21.6.0 Darwin Kernel Version 21.6.0: Sun Nov 6 23:31:16 PST 2022; root:xnu-8020.240.14~1/RELEASE_X86_64 x86_64
$ z3 --version
Z3 version 4.8.17 - 64 bit
$ z3 ../mult_dist.smt2
unsat
$ |
|
Interesting. I can't reproduce this with Z3 4.8.17 on Linux, so perhaps there really is something macOS-specific about this issue. I won't have access to a Mac machine to debug this myself for a couple of weeks, however. In the meantime, one thing that you could to do to help debug this further is to run a test case with higher debug settings. Namely, can you apply this patch: diff --git a/tests/constraint-guards/constant.icry b/tests/constraint-guards/constant.icry
index b7557b19..8323aa1d 100644
--- a/tests/constraint-guards/constant.icry
+++ b/tests/constraint-guards/constant.icry
@@ -1,3 +1,4 @@
+:set tcDebug=2
:l constant.cry
:check
\ No newline at end of fileAnd then run the Doing so should print out the sequence of commands send to and received from Z3, which might help reveal what the issue is. |
Apparently, we need something different to print out the communications with Z3. |
|
Huh, that is very strange. Does the same thing happen on the Cryptol REPL? That is, if you run: And then type in the following at the REPL: For me, that produces lots of output starting with: |
Can you get me a patch that makes printing out SMT communications a default? So that I could recompile Cryptol, try to run it, and get the output? BTW: |
|
Ah, that's helpful to know: the failure is happening during the initial SMT solver setup, rather than when running any Cryptol code.
Good idea. Try this patch: diff --git a/src/Cryptol/TypeCheck/Solver/SMT.hs b/src/Cryptol/TypeCheck/Solver/SMT.hs
index 8da61e34..e80b9433 100644
--- a/src/Cryptol/TypeCheck/Solver/SMT.hs
+++ b/src/Cryptol/TypeCheck/Solver/SMT.hs
@@ -77,10 +77,8 @@ setupSolver s cfg = do
-- | Start a fresh solver instance
startSolver :: IO () -> SolverConfig -> IO Solver
startSolver onExit sCfg =
- do logger <- if (solverVerbose sCfg) > 0 then SMT.newLogger 0
-
- else return quietLogger
- let smtDbg = if (solverVerbose sCfg) > 1 then Just logger else Nothing
+ do logger <- SMT.newLogger 0
+ let smtDbg = Just logger
solver <- SMT.newSolverNotify
(solverPath sCfg) (solverArgs sCfg) smtDbg (Just (const onExit))
let sol = Solver solver loggerAfter applying this patch, I get solver output right after starting Cryptol: |
|
|
I'd like to see a different kind of debug messages, at a much lower level:
The current verbose output tells me that when Cryptol "thinks" it "sent" something to the SMT process, something somehow (
|
|
Thanks! Interestingly, the (set-option :print-success true )
(set-option :produce-models true )
(set-option :global-decls false )
(push 1 )And run it through For me, that produces: It's possible that this may not be enough to trigger your issue, however. The way that Cryptol actually invokes Z3 is through an interactive process, like so: And then it redirects the commands to the Z3 process via standard input. For instance, I can run the sequence of commands in Where I typed each command, hit Enter, and then received |
|
I did not see your comment at #1488 (comment) until after submitting #1488 (comment), but to answer your questions:
Cryptol is managing its Z3 subprocess through the cryptol/src/Cryptol/TypeCheck/Solver/SMT.hs Lines 84 to 85 in 8cca245 And we are using the default values of cryptol/src/Cryptol/TypeCheck/InferTypes.hs Lines 51 to 61 in 8cca245 So the subprocess is being invoked as
It is quitting after that message. This is because the cryptol/src/Cryptol/TypeCheck/Solver/SMT.hs Lines 193 to 208 in 8cca245 And the cryptol/src/Cryptol/ModuleSystem/Base.hs Lines 232 to 247 in 31d30c1
Setting The cryptol/src/Cryptol/TypeCheck/Solver/SMT.hs Lines 201 to 202 in 8cca245 |
|
If you want to see the commands flowing to and from z3, you can use First, rename Then you can |
|
Funny - here's what I got: and crash report: Submitted a bug report at Macports: https://trac.macports.org/ticket/66676#ticket Working on getting a working Z3 from other sources. |
|
For me, on macos, z3 builds out-of-the-box after pulling the source from github and running |
|
Building and installing Z3 v4.11.2 from sources, majority of the tests pass: |
|
Thanks! As far as the 7 test case failures are concerned:
|
|
It sounds like installing Z3 from a source besides MacPorts has resolved the issue, so I'll go ahead and close this. If you encounter other issues, please do not hesitate to open a separate issue. Thanks for your patience and help in debugging this, @mouse07410! |
This is interesting - So, how do I tell Cryptol to look for the "extras" (C headers and libraries) in Or do you want me to open a new issue for this? |
|
Feel free to file a new issue if you believe there is another Cryptol issue lurking here. That being said, I don't think the issue is necessarily on Cryptol's side. The FFI-related tests first build a foreign library using this I think you can resolve the issue by extending |
The reason being - it's not a system location (like That means these locations must be explicitly given to
How can I do it with Cryptol, where the build details are "under the hood"? I think it needs a way to intake these. |
|
I think extending |
You are correct, thank you!
|
MacOS Monterey 12.6.2, Xcode-14.2, GHC-9.2.5, Cabal-3.8.1.0, current Cryptol built form sources.
Apparent error:
Missing response from solver.The text was updated successfully, but these errors were encountered: