chore: add explicit message when we find a library placeholder (#158)

a16z · Aug 3, 2023 · fc61d2f · fc61d2f
1 parent eb6e4a1
commit fc61d2f
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 2 deletions.
diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
@@ -22,7 +22,7 @@
     hexify,
 )
 from .cheatcodes import halmos_cheat_code, hevm_cheat_code, console, Prank
-from .warnings import warn, UNSUPPORTED_OPCODE
+from .warnings import warn, UNSUPPORTED_OPCODE, LIBRARY_PLACEHOLDER
 
 Word = Any  # z3 expression (including constants)
 Byte = Any  # z3 expression (including constants)
@@ -501,7 +501,13 @@ def from_hexcode(hexcode: str):
         if hexcode.startswith("0x"):
             hexcode = hexcode[2:]
 
-        return Contract(bytes.fromhex(hexcode))
+        if "__" in hexcode:
+            warn(LIBRARY_PLACEHOLDER, f"contract hexcode contains library placeholder")
+
+        try:
+            return Contract(bytes.fromhex(hexcode))
+        except ValueError as e:
+            raise ValueError(f"{e} (hexcode={hexcode})")
 
     def decode_instruction(self, pc: int) -> Instruction:
         opcode = int_of(self[pc])

diff --git a/src/halmos/warnings.py b/src/halmos/warnings.py
@@ -22,6 +22,7 @@ def url(self) -> str:
 COUNTEREXAMPLE_UNKNOWN = ErrorCode("counterexample-unknown")
 INTERNAL_ERROR = ErrorCode("internal-error")
 UNSUPPORTED_OPCODE = ErrorCode("unsupported-opcode")
+LIBRARY_PLACEHOLDER = ErrorCode("library-placeholder")
 
 LOOP_BOUND = ErrorCode("loop-bound")