Add docs and cli input check

mythril/analysis/symbolic.py

@@ -3,7 +3,6 @@ purposes."""
 
 import copy
 
-from ast import literal_eval
 from mythril.analysis.security import get_detection_module_hooks, get_detection_modules
 from mythril.laser.ethereum import svm
 from mythril.laser.ethereum.state.account import Account
@@ -76,8 +75,6 @@ class SymExecWrapper:
         )
         self.accounts = {address: account}
 
-        if transaction_sequences:
-            transaction_sequences = literal_eval(str(transaction_sequences))
         self.laser = svm.LaserEVM(
             self.accounts,
             dynamic_loader=dynloader,

mythril/interfaces/cli.py

@@ -13,6 +13,7 @@ import sys
 
 import coloredlogs
 import traceback
+from ast import literal_eval
 
 import mythril.support.signatures as sigs
 from mythril.exceptions import AddressNotFoundError, CriticalError
@@ -320,6 +321,18 @@ def validate_args(parser: argparse.ArgumentParser, args: argparse.Namespace):
                 args.outform,
                 "--enable-iprof must be used with one of -g, --graph, -x, --fire-lasers, -j and --statespace-json",
             )
+    if args.transaction_sequences:
+        try:
+            args.transaction_sequences = literal_eval(str(args.transaction_sequences))
+        except ValueError:
+            exit_with_error(
+                args.outform,
+                "The transaction sequence is in incorrect format, It should be "
+                "[list if possible function hashes in 1st transaction, "
+                "list of possible func hashes in 2nd tx, ..]",
+            )
+        if len(args.transaction_sequences) != args.transaction_count:
+            args.transaction_count = len(args.transaction_sequences)
 
 
 def quick_commands(args: argparse.Namespace):

mythril/laser/ethereum/transaction/symbolic.py

@@ -20,7 +20,13 @@ CREATOR_ADDRESS = 0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE
 ATTACKER_ADDRESS = 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF
 
 
-def generate_function_constraints(calldata: SymbolicCalldata, func_hashes: List[int]):
+def generate_function_constraints(calldata: SymbolicCalldata, func_hashes: List[List[int]]) -> List[Bool]:
+    """
+    This will generate constraints for fixing the function call part of calldata
+    :param calldata: Calldata
+    :param func_hashes: The list of function hashes allowed for this transaction
+    :return: Constraints List
+    """
     constraints = []
     for i in range(4):
         constraint = Bool(False)
@@ -35,8 +41,9 @@ def generate_function_constraints(calldata: SymbolicCalldata, func_hashes: List[
 def execute_message_call(laser_evm, callee_address: str, function_hashes=None) -> None:
     """Executes a message call transaction from all open states.
 
-    :param laser_evm:
-    :param callee_address:
+    :param laser_evm: The laser evm object
+    :param callee_address: The address of the callee
+    :param function_hashes: The function calls to be constrained for the message call
     """
     # TODO: Resolve circular import between .transaction and ..svm to import LaserEVM here
     open_states = laser_evm.open_states[:]

tests/laser/transaction/symbolic_test.py

@@ -13,7 +13,7 @@ import unittest.mock as mock
 from unittest.mock import MagicMock
 
 
-def _is_message_call(_, transaction):
+def _is_message_call(_, transaction, func_hashes):
     assert isinstance(transaction, MessageCallTransaction)