Add support for fallback() and receive() functions for prioritising tx sequences (#1723)

* Resstrict precommit

* Add support for fallback and receive

* Fix requirements

docs/source/tutorial.rst

@@ -505,3 +505,178 @@ relays it to the solc compiler.
 
 This can effectively execute the file since the Solidity compiler can locate `PRC20.sol`. For more information on remappings, you can
 refer to `Solc docs <https://docs.soliditylang.org/en/v0.8.14/using-the-compiler.html#base-path-and-import-remapping>`_.
+
+********************************************************
+Executing Mythril by Restricting Transaction Sequences
+********************************************************
+
+You can use Mythril to search certain transaction sequences. You can use ``--transaction-sequences`` argument to direct the search.
+An example usage is ``[[func_hash1,func_hash2], [func_hash2,func_hash3],[]]`` where the first transaction is constrained with ``func_hash1`` and ``func_hash2``, the second tx is constrained with ``func_hash2`` and ``func_hash3`` and the final transaction is unconstrained on any function.
+Use ``-1`` as a proxy for the hash of ``fallback()`` function and ``-2`` as a proxy for the hash of ``receive()`` function.
+
+Consider the following contract
+
+    .. code-block:: solidity
+
+        pragma solidity 0.5.0;
+
+
+        contract Rubixi {
+            //Declare variables for storage critical to contract
+            uint private balance = 0;
+            uint private collectedFees = 0;
+            uint private feePercent = 10;
+            uint private pyramidMultiplier = 300;
+            uint private payoutOrder = 0;
+
+            address payable private creator;
+
+            modifier onlyowner {
+                if (msg.sender == creator) _;
+            }
+
+            struct Participant {
+                address payable etherAddress;
+                uint payout;
+            }
+
+            //Fallback function
+            function() external payable {
+                init();
+            }
+
+            //Sets creator
+            function dynamicPyramid() public {
+                creator = msg.sender;
+            }
+
+            Participant[] private participants;
+
+            //Fee functions for creator
+            function collectAllFees() public onlyowner {
+                require(collectedFees > 0);
+                creator.transfer(collectedFees);
+                collectedFees = 0;
+            }
+
+            function collectFeesInEther(uint _amt) public onlyowner {
+                _amt *= 1 ether;
+                if (_amt > collectedFees) collectAllFees();
+
+                require(collectedFees > 0);
+
+                creator.transfer(_amt);
+                collectedFees -= _amt;
+            }
+
+            function collectPercentOfFees(uint _pcent) public onlyowner {
+                require(collectedFees > 0 && _pcent <= 100);
+
+                uint feesToCollect = collectedFees / 100 * _pcent;
+                creator.transfer(feesToCollect);
+                collectedFees -= feesToCollect;
+            }
+
+            //Functions for changing variables related to the contract
+            function changeOwner(address payable _owner) public onlyowner {
+                creator = _owner;
+            }
+
+            function changeMultiplier(uint _mult) public onlyowner {
+                require(_mult <= 300 &&  _mult >= 120);
+                pyramidMultiplier = _mult;
+            }
+
+            function changeFeePercentage(uint _fee) public onlyowner {
+                require(_fee <= 10);
+                feePercent = _fee;
+            }
+
+            //Functions to provide information to end-user using JSON interface or other interfaces
+            function currentMultiplier() public view returns (uint multiplier, string memory info) {
+                multiplier = pyramidMultiplier;
+                info = "This multiplier applies to you as soon as transaction is received, may be lowered to hasten payouts or increased if payouts are fast enough. Due to no float or decimals, multiplier is x100 for a fractional multiplier e.g. 250 is actually a 2.5x multiplier. Capped at 3x max and 1.2x min.";
+            }
+
+            function currentFeePercentage() public view returns (uint fee, string memory info) {
+                fee = feePercent;
+                info = "Shown in % form. Fee is halved(50%) for amounts equal or greater than 50 ethers. (Fee may change, but is capped to a maximum of 10%)";
+            }
+
+            function currentPyramidBalanceApproximately() public view returns (uint pyramidBalance, string memory info) {
+                pyramidBalance = balance / 1 ether;
+                info = "All balance values are measured in Ethers, note that due to no decimal placing, these values show up as integers only, within the contract itself you will get the exact decimal value you are supposed to";
+            }
+
+            function nextPayoutWhenPyramidBalanceTotalsApproximately() public view returns (uint balancePayout) {
+                balancePayout = participants[payoutOrder].payout / 1 ether;
+            }
+
+            function feesSeperateFromBalanceApproximately() public view returns (uint fees) {
+                fees = collectedFees / 1 ether;
+            }
+
+            function totalParticipants() public view returns (uint count) {
+                count = participants.length;
+            }
+
+            function numberOfParticipantsWaitingForPayout() public view returns (uint count) {
+                count = participants.length - payoutOrder;
+            }
+
+            function participantDetails(uint orderInPyramid) public view returns (address addr, uint payout) {
+                if (orderInPyramid <= participants.length) {
+                    addr = participants[orderInPyramid].etherAddress;
+                    payout = participants[orderInPyramid].payout / 1 ether;
+                }
+            }
+
+            //init function run on fallback
+            function init() private {
+                //Ensures only tx with value of 1 ether or greater are processed and added to pyramid
+                if (msg.value < 1 ether) {
+                    collectedFees += msg.value;
+                    return;
+                }
+
+                uint _fee = feePercent;
+                // 50% fee rebate on any ether value of 50 or greater
+                if (msg.value >= 50 ether) _fee /= 2;
+
+                addPayout(_fee);
+            }
+
+            //Function called for valid tx to the contract
+            function addPayout(uint _fee) private {
+                //Adds new address to participant array
+                participants.push(Participant(msg.sender, (msg.value * pyramidMultiplier) / 100));
+
+                // These statements ensure a quicker payout system to
+                // later pyramid entrants, so the pyramid has a longer lifespan
+                if (participants.length == 10) pyramidMultiplier = 200;
+                else if (participants.length == 25) pyramidMultiplier = 150;
+
+                // collect fees and update contract balance
+                balance += (msg.value * (100 - _fee)) / 100;
+                collectedFees += (msg.value * _fee) / 100;
+
+                //Pays earlier participiants if balance sufficient
+                while (balance > participants[payoutOrder].payout) {
+                    uint payoutToSend = participants[payoutOrder].payout;
+                    participants[payoutOrder].etherAddress.transfer(payoutToSend);
+
+                    balance -= participants[payoutOrder].payout;
+                    payoutOrder += 1;
+                }
+            }
+        }
+
+Since this contract has ``16`` functions, it is infeasible to execute uninteresting functions such as ``feesSeperateFromBalanceApproximately()``.
+To successfully explore useful transaction sequences we can use Mythril's ``--transaction-sequences`` argument.
+
+.. code-block:: bash
+
+    $ myth analyze rubixi.sol -t 3 --transaction-sequences [["0x89b8ae9b"],[-1],["0x686f2c90","0xb4022950","0x4229616d"]]
+
+The first transaction is constrained on ``fallback()`` function, the second transaction is constrained on ``dynamicPyramid`` function, and finally the third transaction is constrained on ``collectAllFees()``, ``collectFeesInEther(uint256)`` and, ``collectPercentOfFees(uint256)``.
+Make sure to use ``-t 3`` argument, since the length of the transaction sequence should match with the transaction count argument.

mythril/interfaces/cli.py

@@ -458,8 +458,8 @@ def add_analysis_args(options):
         type=str,
         default=None,
         help="The possible transaction sequences to be executed. "
-        "Like [[func_hash1, func_hash2], [func_hash2, func_hash3]] where for the first transaction is constrained "
-        "with func_hash1 and func_hash2, and the second tx is constrained with func_hash2 and func_hash3",
+        "Like [[func_hash1, func_hash2], [func_hash2, func_hash3]] where the first transaction is constrained "
+        "with func_hash1 and func_hash2, and the second tx is constrained with func_hash2 and func_hash3. Use -1 as a proxy for fallback() function and -2 for receive() function.",
     )
     options.add_argument(
         "--beam-search",
@@ -615,6 +615,10 @@ def validate_args(args: Namespace):
         exit_with_error("text", "Only a single arg is supported for using disassemble")
 
     if args.__dict__.get("transaction_sequences", None):
+        if args.__dict__.get("disable_dependency_pruning", False) is False:
+            log.warning(
+                "It is advised to disable dependency pruning (use the flag --disable-dependency-pruning) when specifying transaction sequences."
+            )
         try:
             args.transaction_sequences = literal_eval(str(args.transaction_sequences))
         except ValueError:
@@ -623,7 +627,8 @@ def validate_args(args: Namespace):
                 "The transaction sequence is in incorrect format, It should be "
                 "[list of possible function hashes in 1st transaction, "
                 "list of possible func hashes in 2nd tx, ...] "
-                "If any list is empty then all possible functions are considered for that transaction",
+                "If any list is empty then all possible functions are considered for that transaction."
+                "Use -1 as a proxy for fallback() and -2 for receive() function.",
             )
         if len(args.transaction_sequences) != args.transaction_count:
             args.transaction_count = len(args.transaction_sequences)

mythril/laser/ethereum/instructions.py

@@ -1571,6 +1571,7 @@ class Instruction:
             global_state.mstate.max_gas_used += max_gas
             return [global_state]
         # False case
+
         negated = (
             simplify(Not(condition)) if isinstance(condition, Bool) else condition == 0
         )

mythril/laser/ethereum/svm.py

@@ -240,6 +240,7 @@ class LaserEVM:
             if len(self.open_states) == 0:
                 break
             old_states_count = len(self.open_states)
+
             if self.use_reachability_check:
                 self.open_states = [
                     state
@@ -257,10 +258,14 @@ class LaserEVM:
             func_hashes = (
                 args.transaction_sequences[i] if args.transaction_sequences else None
             )
+
             if func_hashes:
-                func_hashes = [
-                    bytes.fromhex(hex(func_hash)[2:]) for func_hash in func_hashes
-                ]
+                for itr, func_hash in enumerate(func_hashes):
+                    if func_hash in (-1, -2):
+                        func_hashes[itr] = func_hash
+                    else:
+                        func_hashes[itr] = bytes.fromhex(hex(func_hash)[2:])
+
             for hook in self._start_sym_trans_hooks:
                 hook()
 
@@ -319,7 +324,6 @@ class LaserEVM:
                     for state in new_states
                     if state.world_state.constraints.is_possible()
                 ]
-
             self.manage_cfg(op_code, new_states)  # TODO: What about op_code is None?
             if new_states:
                 self.work_list += new_states

mythril/laser/ethereum/transaction/symbolic.py

@@ -89,6 +89,13 @@ def generate_function_constraints(
     for i in range(FUNCTION_HASH_BYTE_LENGTH):
         constraint = Bool(False)
         for func_hash in func_hashes:
+            if func_hash == -1:
+                # Fallback function without calldata
+                constraint = Or(constraint, calldata.size < 4)
+            elif func_hash == -2:
+                # Receive function
+                constraint = Or(constraint, calldata.size == 0)
+            else:
                 constraint = Or(
                     constraint, calldata[i] == symbol_factory.BitVecVal(func_hash[i], 8)
                 )

requirements.txt

@@ -5,7 +5,7 @@ cython
 cytoolz<0.12.0
 asn1crypto>=0.22.0
 configparser>=3.5.0
-coverage>6.0
+coverage<7.0,>6.0
 py_ecc<5.0.0,>=1.4.7
 eth_abi<3.0.0,>=2.0.0b4
 eth-account<0.6.0,>=0.5.6