Removed use of global solver from Memory

[ggrieco-tob]

The Memory class had a global solver hard-coded that resulted in z3 (or the solver the user has installed) always used when a native binary was executed. This PR should fix that.

[ekilmer]

global solver hard-coded that resulted in z3

I just run the following locally with yices installed through my system and SelectedSolver.instance() returns YicesSolver

$ python
Python 3.6.13 (default, Feb 22 2021, 12:20:57)
[GCC 10.2.1 20201125 (Red Hat 10.2.1-9)] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> from manticore.core.smtlib import SelectedSolver
>>> solver = SelectedSolver.instance()
>>> solver
<manticore.core.smtlib.solver.YicesSolver object at 0x7f51d999ee48>

I also tried inspecting the global solver itself and still got YicesSolver

$ python
Python 3.6.13 (default, Feb 22 2021, 12:20:57)
[GCC 10.2.1 20201125 (Red Hat 10.2.1-9)] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> from manticore.native.memory import solver
>>> solver
<manticore.core.smtlib.solver.YicesSolver object at 0x7fa727dbc780>

Am I missing something?

[ggrieco-tob]

If you apply this patch:

diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py
index 7e61217..208cfd3 100644
--- a/manticore/core/smtlib/solver.py
+++ b/manticore/core/smtlib/solver.py
@@ -761,4 +761,5 @@ class SelectedSolver:
             cls.choice = consts.solver
 
         SelectedSolver = {"cvc4": CVC4Solver, "yices": YicesSolver, "z3": Z3Solver}[cls.choice.name]
+        print("Calling instance() with cls.choice =", cls.choice)
         return SelectedSolver.instance()

you can see that running anything using the manticore cli will print Calling instance() with cls.choice = SolverType.z3 then it will use any other solver you specify (for instance, using --smt.solver cvc4 will still print that line).

[ekilmer]

Ahh, okay, yes I see that now.

I think there's a bigger issue with the CLI options not getting parsed correctly. I'm currently looking into it.

Edit: Maybe not.

[ekilmer]

Okay! I think I finally understand what's going on here...

The global solver instance is initialized incorrectly because it calls SelectedSolver.instance() before we've parsed the command line flags, due to execution upon import, and so if someone chooses to use a particular solver, it will be ignored for these global instances.

Thank you!

[ekilmer]

LGTM!!

[ggrieco-tob]

This looks ready to merge, but again I can't do it since one check (CI / upload) was skipped. Can you merge it @ekilmer ?