From 31bb794fff1ef6f81cec4b1a9234aa83358ba8d0 Mon Sep 17 00:00:00 2001
From: karmacoma <karma@coma.lol>
Date: Mon, 29 Jul 2024 13:30:27 -0700
Subject: [PATCH] handle solidity files with no contracts (#333)

---
 src/halmos/__main__.py | 49 ++++++++++++++++++++++++++----------------
 1 file changed, 30 insertions(+), 19 deletions(-)

diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py
index d538a2a9..b7dd1ab6 100644
--- a/src/halmos/__main__.py
+++ b/src/halmos/__main__.py
@@ -1300,6 +1300,19 @@ def mk_arrlen(args: HalmosConfig) -> Dict[str, int]:
     return arrlen
 
 
+def get_contract_type(
+    ast_nodes: Dict, contract_name: str
+) -> Tuple[str | None, str | None]:
+    for node in ast_nodes:
+        if node["nodeType"] == "ContractDefinition" and node["name"] == contract_name:
+            abstract = "abstract " if node.get("abstract") else ""
+            contract_type = abstract + node["contractKind"]
+            natspec = node.get("documentation")
+            return contract_type, natspec
+
+    return None, None
+
+
 def parse_build_out(args: HalmosConfig) -> Dict:
     result = {}  # compiler version -> source filename -> contract name -> (json, type)
 
@@ -1328,28 +1341,25 @@ def parse_build_out(args: HalmosConfig) -> Dict:
                 with open(json_path, encoding="utf8") as f:
                     json_out = json.load(f)
 
-                compiler_version = json_out["metadata"]["compiler"]["version"]
-                if compiler_version not in result:
-                    result[compiler_version] = {}
-                if sol_dirname not in result[compiler_version]:
-                    result[compiler_version][sol_dirname] = {}
-                contract_map = result[compiler_version][sol_dirname]
-
                 # cut off compiler version number as well
                 contract_name = json_filename.split(".")[0]
-
-                contract_type = None
-                for node in json_out["ast"]["nodes"]:
-                    if (
-                        node["nodeType"] == "ContractDefinition"
-                        and node["name"] == contract_name
-                    ):
-                        abstract = "abstract " if node.get("abstract") else ""
-                        contract_type = abstract + node["contractKind"]
-                        natspec = node.get("documentation")
-                        break
+                ast_nodes = json_out["ast"]["nodes"]
+                contract_type, natspec = get_contract_type(ast_nodes, contract_name)
+
+                # can happen to solidity files for multiple reasons:
+                # - import only (like console2.log)
+                # - defines only structs or enums
+                # - defines only free functions
+                # - ...
                 if contract_type is None:
-                    raise ValueError("no contract type", contract_name)
+                    if args.debug:
+                        debug(f"Skipped {json_filename}, no contract definition found")
+                    continue
+
+                compiler_version = json_out["metadata"]["compiler"]["version"]
+                result.setdefault(compiler_version, {})
+                result[compiler_version].setdefault(sol_dirname, {})
+                contract_map = result[compiler_version][sol_dirname]
 
                 if contract_name in contract_map:
                     raise ValueError(
@@ -1357,6 +1367,7 @@ def parse_build_out(args: HalmosConfig) -> Dict:
                         contract_name,
                         sol_dirname,
                     )
+
                 contract_map[contract_name] = (json_out, contract_type, natspec)
 
                 try: