avoid solver race conditions with a lock (#569)

Author: 0xkarmacoma

src/halmos/solvers.py

@@ -16,7 +16,7 @@
 
 from halmos.logs import debug, error
 from halmos.ui import ui
-from halmos.utils import format_size
+from halmos.utils import format_size, synchronized
 
 # not defaulting to latest because of https://github.com/a16z/halmos/issues/492
 DEFAULT_YICES_VERSION = "2.6.4"
@@ -475,6 +475,7 @@ def find_solver_binary(solver: SolverInfo) -> Path | None:
     return None
 
 
+@synchronized()
 def ensure_solver_available(solver: SolverInfo) -> Path:
     """
     Ensures the specified solver is available, downloading it if necessary.

src/halmos/utils.py

@@ -4,8 +4,9 @@
 
 import math
 import re
+import threading
 import uuid
-from functools import partial
+from functools import partial, wraps
 from timeit import default_timer as timer
 from typing import TYPE_CHECKING, Any, TypeAlias, Union
 
@@ -1243,6 +1244,23 @@ def wrapper(*args, **kwargs):
     return decorator
 
 
+def synchronized(lock=None):
+    """Decorator that synchronizes access to a method or function"""
+
+    def decorator(func):
+        # Create a lock for this specific function if none provided
+        func_lock = lock or threading.RLock()
+
+        @wraps(func)
+        def wrapper(*args, **kwargs):
+            with func_lock:
+                return func(*args, **kwargs)
+
+        return wrapper
+
+    return decorator
+
+
 dict_of_unsupported_cheatcodes = {
     0x23361207: "expectCall(address,uint256,uint64,bytes)",
     0x97624631: "assertEq(bytes,bytes)",