From a8a76b3da52c205197608da3303579a27a3cce47 Mon Sep 17 00:00:00 2001
From: e-ngo <52668908+e-ngo@users.noreply.github.com>
Date: Thu, 3 Oct 2019 10:00:20 -0700
Subject: [PATCH] Added returning global state to SIGNEXTEND opcode. (#1227)

* Added returning global state to SIGNEXTEND opcode.

* Add TODO statement.

* added new symbol instead

* hash s0
---
 mythril/laser/ethereum/instructions.py | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index 2f1c7f03..6434978c 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -619,23 +619,29 @@ class Instruction:
         :param global_state:
         :return:
         """
-        state = global_state.mstate
-        s0, s1 = state.stack.pop(), state.stack.pop()
+        mstate = global_state.mstate
+        s0, s1 = mstate.stack.pop(), mstate.stack.pop()
 
         try:
             s0 = util.get_concrete_int(s0)
             s1 = util.get_concrete_int(s1)
         except TypeError:
-            return []
+            log.debug("Unsupported symbolic argument for SIGNEXTEND")
+            mstate.stack.append(
+                global_state.new_bitvec(
+                    "SIGNEXTEND({},{})".format(hash(s0), hash(s1)), 256
+                )
+            )
+            return [global_state]
 
         if s0 <= 31:
             testbit = s0 * 8 + 7
             if s1 & (1 << testbit):
-                state.stack.append(s1 | (TT256 - (1 << testbit)))
+                mstate.stack.append(s1 | (TT256 - (1 << testbit)))
             else:
-                state.stack.append(s1 & ((1 << testbit) - 1))
+                mstate.stack.append(s1 & ((1 << testbit) - 1))
         else:
-            state.stack.append(s1)
+            mstate.stack.append(s1)
 
         return [global_state]