Add summaries and additional bugfixes

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
@@ -236,11 +237,27 @@ 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) 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.
+    """
+    try:
+        # Attempt to decode as UTF-8 text
+        return item.decode("utf-8")
+    except UnicodeDecodeError:
+        # If it fails, encode as base64
+        return base64.b64encode(item).decode("utf-8")
+
+
 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",
@@ -784,10 +789,10 @@ def execute_command(
             print("Disassembly: \n" + disassembler.contracts[0].get_creation_easm())
 
     elif args.command == SAFE_FUNCTIONS_COMMAND:
-        args.unconstrained_storage = True
+        args.no_onchain_data = (
+            args.disable_dependency_pruning
+        ) = args.unconstrained_storage = True
         args.pruning_factor = 1
-        args.disable_dependency_pruning = True
-        args.no_onchain_data = True
         function_analyzer = MythrilAnalyzer(
             strategy=strategy, disassembler=disassembler, address=address, cmd_args=args
         )

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