Skip to content
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

Cryptol hangs on :r with some modules #1298

Open
brianhuffman opened this issue Oct 9, 2021 · 11 comments
Open

Cryptol hangs on :r with some modules #1298

brianhuffman opened this issue Oct 9, 2021 · 11 comments
Labels
low-hanging fruit For issues that should be easy to fix performance General performance related issues.

Comments

@brianhuffman
Copy link
Contributor

The problem seems to occur when reloading a file that contains at least two different "tricky" definitions that need solver support to type check. Here's a minimized example:

module Test where

pproduct1 : {u, v} (fin u, fin v) => [u][1 + v] -> [1 + u * v]
pproduct1 xs = if `u == 0 then 1 else pmult x0 (pproduct1 xs')
  where
    x0 = drop`{(1 - min 1 u) * v} (xs @ 0)
    xs' = drop`{min 1 u} xs

pproduct2 : {u, v} (fin u, fin v) => [u][1 + v] -> [1 + u * v]
pproduct2 xs = if `u == 0 then 1 else pmult x0 (pproduct2 xs')
  where
    x0 = drop`{(1 - min 1 u) * v} (xs @ 0)
    xs' = drop`{min 1 u} xs

Loading it with cryptol Test.cry works just fine, taking practically no time.

┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.11.0.99 (c013035, modified)
https://cryptol.net  :? for help

Loading module Cryptol
Loading module Test
Test> :r
Loading module Cryptol
Loading module Test

But then after typing :r, it prints the "Loading module" messages and then just hangs, with z3 running at 100% cpu.

The bug occurs with a recent master version (c013035) on MacOS. This seems to be a regression, as the bug does not occur with the earlier cryptol-2.11 release.

@brianhuffman
Copy link
Contributor Author

Bisection identifies 3114110 (#1128) as the first bad commit.

@robdockins
Copy link
Contributor

I wonder if this is essentially the same issue as #1250. That was fixed in #1258 by resetting the solver. Maybe we should do the same on :r

@brianhuffman
Copy link
Contributor Author

It does get unstuck if you interrupt it with ctrl-C (which resets the solver) and then do :r again. So yes, I think resetting the solver on every :r would do it.

@atomb atomb added performance General performance related issues. low-hanging fruit For issues that should be easy to fix labels Oct 22, 2021
@yav
Copy link
Member

yav commented Oct 28, 2021

I investigated what's happening here, and to me this looks like a z3 bug. Here is a trimmed down (not fully) smt-lib file that reproduces the problem directly with z3:
out.txt

@robdockins
Copy link
Contributor

This appears to be version specific as well. Z3 version 4.8.9 exhibits the hang, but a wide variety of other versions (that I happen to have lying around) from 4.8.1 to 4.8.11 do not.

@robdockins
Copy link
Contributor

#965 seems like it might be related too, it also seems specific to Z3 4.8.9.

@brianhuffman
Copy link
Contributor Author

I ran into a variation of this issue just now. Unlike before, it no longer requires a reload; it actually hangs when the module is first loaded. (The bug is triggered by exactly the same source file listed in the original post above.)

I did a bisection, and found that 3fabe4a (#1302) is the first bad commit. This commit only modifies the definition of sortBy in the cryptol prelude; apparently it does it in such a way that merely loading the prelude puts z3 into a buggy state.

I'm see the bug with z3-4.8.9. Switching to 4.8.10 seems to make it work. I guess we should just consider 4.8.9 to be deprecated?

@yav
Copy link
Member

yav commented Dec 29, 2021

Seems reasonable, although I am using z3-4.8.10 and it can't pass all the tests either, but at least it is hanging during :proof rather than just loading a module.

@brianhuffman
Copy link
Contributor Author

The cryptol README says, "Cryptol generally requires the most recent version of Z3, but you can see the specific version tested in CI by looking here." The link indicates z3 version 4.8.10, so I would hope that 4.8.10 actually works. Is that link actually right? Are we using 4.8.10 in CI?

@yav
Copy link
Member

yav commented Dec 29, 2021

We do appear to be using 4.8.10 indeed, so perhaps I am just not being patient enough. The two tests I am having trouble with are regression/negshift.icry and regression/primes.icry

@yav
Copy link
Member

yav commented Dec 29, 2021

It would appear that the problem with negshift is the 32-bit case. I run a bunch of tests with different sizes, here are the numbers, which are pretty odd:

Main> :set proverStats=yes
Main> :set prover=z3
Main> :prove negLeftShift`{8,Bit}
Q.E.D.
(Total Elapsed Time: 0.066s, using "Z3")
Main> :prove negLeftShift`{9,Bit}
Q.E.D.
(Total Elapsed Time: 0.097s, using "Z3")
Main> :prove negLeftShift`{10,Bit}
Q.E.D.
(Total Elapsed Time: 0.183s, using "Z3")
Main> :prove negLeftShift`{11,Bit}
Q.E.D.
(Total Elapsed Time: 0.342s, using "Z3")
Main> :prove negLeftShift`{12,Bit}
Q.E.D.
(Total Elapsed Time: 0.362s, using "Z3")
Main> :prove negLeftShift`{13,Bit}
Q.E.D.
(Total Elapsed Time: 1.092s, using "Z3")
Main> :prove negLeftShift`{14,Bit}
Q.E.D.
(Total Elapsed Time: 2.972s, using "Z3")
Main> :prove negLeftShift`{15,Bit}
Q.E.D.
(Total Elapsed Time: 4.085s, using "Z3")
Main> :prove negLeftShift`{16,Bit}
Q.E.D.
(Total Elapsed Time: 27.806s, using "Z3")
Main> :prove negLeftShift`{17,Bit}
Q.E.D.
(Total Elapsed Time: 0.138s, using "Z3")
Main> :prove negLeftShift`{18,Bit}
Q.E.D.
(Total Elapsed Time: 10m:5.245s, using "Z3")

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
low-hanging fruit For issues that should be easy to fix performance General performance related issues.
Projects
None yet
Development

No branches or pull requests

4 participants