fix(rpc): reset TC solver on file/module load

[pnwamk]

Some difficult to reproduce bugs regarding the RPC server hanging
(#1250) seemed to be
related to the type checker solver (Z3) hanging after periods of
extended use. I.e., a module would load/error quickly normally,
but if preceded by enough prior solver/server activity, Z3
would consistently hang. To avoid this, we can simply reset the
solver and reload the type checker prelude when the server is asked
to load a file or module. This solves the Z3 hang issues in observed
cases and requires no additional forking (which we're trying to
minimize when possible).

[robdockins]

Interesting... do you find that the Z3 version matters?

Either way, I wonder if this is worth trying to reduce to an issue we can file upstream?

[pnwamk]

It was with Z3 version 4.8.8 inside the docker container produced by this Dockerfile. The steps in this issue reproduce it: #1250 (comment)

I can try bumping the version of Z3 in the Dockerfile to see if that impacts things and we can go from there w.r.t. a future issue.

[robdockins]

Yeah, I'd see if, e.g., Z3 4.8.11 makes a difference.

[weaversa]

We tried 4.8.13 today and it resolved our observable issues. It's possible that upgrading just stalls the problem. That is, imagine that the problem is that some series of push/pop is leaving too much in the z3 state, and when z3 is presented with a new type-checking problem, it becomes bogged down by previous state. Perhaps newer versions of z3 are simply faster, but may get bogged down in the future as the state continues to grow. The reset problem would fix any such leakage, if it exists.

Of course, it could simply be a bug in and old z3 and the new version just fixes it. I don't know.

[robdockins]

Interesting. I know they have been doing a lot of work on a new real/integer arithmetic solver over the last several versions, so that might be related.

I feel like it's a bit of a shame to reset the solver so often because then we have to reload the type-checking prelude... but if it prevents problems, perhaps it is worth it.

[pnwamk]

Chatted briefly with @atomb and I think these changes all things considered are worth merging: we're still miles ahead of where we used to be---i.e., we used to reinvoke the solver from scratch constantly and now use a single instance, thanks @robdockins!---, and so while this is a slight step back in performance for some queries, it seems unlikely to be a bottle neck given that we're just doing it when a new module/file is loaded explicitly by an RPC client, and that's going to potentially invoke quite a bit of cryptol/server computation anyway.