Add summaries and additional bugfixes (#1830)

* Add summaries and additional bugfixes

* Update test w.r.t bugfixes

* Update namespace

* Disable sonar

Author: norhh

.circleci/config.yml

@@ -72,15 +72,15 @@ jobs:
           command: python3 -m build
           working_directory: /home/mythril
 
-      - run:
-          name: Sonar analysis
-          command: if [ -z "$CIRCLE_PR_NUMBER" ]; then if [ -z "$CIRCLE_TAG" ]; then
-            sonar-scanner -Dsonar.projectKey=$SONAR_PROJECT_KEY
-            -Dsonar.organization=$SONAR_ORGANIZATION
-            -Dsonar.branch.name=$CIRCLE_BRANCH
-            -Dsonar.projectBaseDir=/home/mythril -Dsonar.sources=mythril
-            -Dsonar.host.url=$SONAR_HOST_URL -Dsonar.tests=/home/mythril/tests
-            -Dsonar.login=$SONAR_LOGIN; fi; fi
+      #- run:
+      #    name: Sonar analysis
+      #    command: if [ -z "$CIRCLE_PR_NUMBER" ]; then if [ -z "$CIRCLE_TAG" ]; then
+      #      sonar-scanner -Dsonar.projectKey=$SONAR_PROJECT_KEY
+      #      -Dsonar.organization=$SONAR_ORGANIZATION
+      #      -Dsonar.branch.name=$CIRCLE_BRANCH
+      #      -Dsonar.projectBaseDir=/home/mythril -Dsonar.sources=mythril
+      #      -Dsonar.host.url=$SONAR_HOST_URL -Dsonar.tests=/home/mythril/tests
+      #      -Dsonar.login=$SONAR_LOGIN; fi; fi
       # - run:
       #     name: Integration tests
       #     command: if [ -z "$CIRCLE_PR_NUMBER" ]; then ./run-integration-tests.sh; fi

mythril/analysis/report.py

@@ -1,4 +1,5 @@
 """This module provides classes that make up an issue report."""
+import base64
 import logging
 import re
 import json
@@ -10,7 +11,7 @@
     from eth_abi import decode_abi as decode
 
 from jinja2 import PackageLoader, Environment
-from typing import Dict, List, Any, Optional
+from typing import Dict, Iterable, List, Any, Optional
 import hashlib
 
 from mythril.laser.execution_info import ExecutionInfo
@@ -236,11 +237,28 @@ def resolve_input(data, function_name):
             data += "0" * (64 - len(data) % 64)
         try:
             decoded_output = decode(type_info, bytes.fromhex(data))
+            decoded_output = tuple(
+                convert_bytes(item) if isinstance(item, (bytes, Iterable)) else item
+                for item in decoded_output
+            )
             return decoded_output
         except Exception as e:
             return None
 
 
+def convert_bytes(item):
+    """
+    Converts bytes to a serializable format. Handles nested iterables.
+    """
+    if isinstance(item, bytes):
+        return item.hex()
+    elif isinstance(item, Iterable) and not isinstance(item, (str, bytes)):
+        # Recursively apply convert_bytes to each item in the iterable
+        return type(item)(convert_bytes(subitem) for subitem in item)
+    else:
+        return item
+
+
 class Report:
     """A report containing the content of multiple issues."""
 

mythril/analysis/symbolic.py

@@ -26,6 +26,7 @@
     CoveragePluginBuilder,
     CallDepthLimitBuilder,
     InstructionProfilerBuilder,
+    SymbolicSummaryPluginBuilder,
 )
 from mythril.laser.ethereum.strategy.extensions.bounded_loops import (
     BoundedLoopsStrategy,
@@ -148,6 +149,8 @@ def __init__(
             plugin_loader.load(MutationPrunerBuilder())
         if not args.disable_iprof:
             plugin_loader.load(InstructionProfilerBuilder())
+        if args.enable_summaries:
+            plugin_loader.load(SymbolicSummaryPluginBuilder())
 
         plugin_loader.load(CallDepthLimitBuilder())
         plugin_loader.add_args(

mythril/interfaces/cli.py

@@ -572,6 +572,11 @@ def add_analysis_args(options):
         action="store_true",
         help="Disable mutation pruner",
     )
+    options.add_argument(
+        "--enable-summaries",
+        action="store_true",
+        help="Enable using symbolic summaries",
+    )
     options.add_argument(
         "--custom-modules-directory",
         help="Designates a separate directory to search for custom analysis modules",

mythril/laser/plugin/plugins/__init__.py

@@ -11,3 +11,4 @@
 from mythril.laser.plugin.plugins.mutation_pruner import MutationPrunerBuilder
 from mythril.laser.plugin.plugins.call_depth_limiter import CallDepthLimitBuilder
 from mythril.laser.plugin.plugins.instruction_profiler import InstructionProfilerBuilder
+from mythril.laser.plugin.plugins.summary import SymbolicSummaryPluginBuilder

mythril/laser/plugin/plugins/summary/__init__.py

@@ -0,0 +1 @@
+from .core import SymbolicSummaryPluginBuilder

mythril/laser/plugin/plugins/summary/annotations.py

@@ -0,0 +1,44 @@
+from mythril.laser.ethereum.state.annotation import StateAnnotation
+from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.state.environment import Environment
+from mythril.laser.smt import Bool, BaseArray
+from typing import List, Tuple
+
+from copy import deepcopy, copy
+
+
+class SummaryTrackingAnnotation(StateAnnotation):
+    """SummaryTrackingAnnotation
+    This annotation is used by the symbolic summary plugin to keep track of data related to a summary that
+    will be computed during the future exploration of the annotated world state.
+    """
+
+    def __init__(
+        self,
+        entry: GlobalState,
+        storage_pairs: List[Tuple[BaseArray, BaseArray]],
+        storage_constraints: List[Bool],
+        environment_pair: Tuple[Environment, Environment],
+        balance_pair: Tuple[BaseArray, BaseArray],
+        code: str,
+    ):
+        self.entry = entry
+        self.trace = []
+        self.storage_pairs = storage_pairs
+        self.storage_constraints = storage_constraints
+        self.environment_pair = environment_pair
+        self.balance_pair = balance_pair
+        self.code = code
+
+    def __copy__(self):
+
+        annotation = SummaryTrackingAnnotation(
+            entry=self.entry,
+            storage_pairs=deepcopy(self.storage_pairs),
+            storage_constraints=deepcopy(self.storage_constraints),
+            environment_pair=deepcopy(self.environment_pair),
+            balance_pair=deepcopy(self.balance_pair),
+            code=self.code,
+        )
+        annotation.trace = self.trace
+        return annotation