Symbolic interpreter

	* New value for the enum Satifiability: Satifiability

symbolic_execution/language/bitcoin/symbolic_interpreter.py

@@ -3,16 +3,31 @@
 from enum import Enum
 from multiprocessing import Manager, Process, Queue
 from symbolic_execution.hardware.interfaces import IMachine
-from symbolic_execution.hardware.machines.btc_machine import CHECK_SINGLE_SIG, BTCMachine, BTC_VECTOR_SIZE, HASH_FUNCTIONS
+from symbolic_execution.hardware.machines.btc_machine import (
+    CHECK_SINGLE_SIG,
+    BTCMachine,
+    BTC_VECTOR_SIZE,
+    HASH_FUNCTIONS,
+)
 from symbolic_execution.hardware.memory.ram import FullySymbolicRAM
 from symbolic_execution.language.bitcoin.parser import BitcoinParser
+from symbolic_execution.language.exceptions import (
+    IncompleteIfEndIfClause,
+    InvalidOpCode,
+)
 from symbolic_execution.program.executer.symbolic import SymbolicExecuter
+from symbolic_execution.program.instruction.exceptions import (
+    UnimplementedInstructionError,
+)
+from symbolic_execution.program.instruction.general import InstructionTag
 from z3 import *
 
-class Satifiability (Enum):
+
+class Satifiability(Enum):
     SATISFIABLE = 0
     UNSATISFIABLE = 1
     UNKNOWN = 2
+    UNSPENDABLE = 3
 
     @classmethod
     def z3_to_enum(cls, satisfiability):
@@ -33,29 +48,51 @@ def __find_unlocking_script_timed(hex_script, return_dict, verbose):
     m = ""
     satisfiability = unknown
 
-    btc_parser = BitcoinParser()
-    tokens = btc_parser.tokenize_code(hex_script)
-    if verbose:
-        print(tokens)
-    program = btc_parser.build_control_flow_graph(tokens)
+    try:
+        btc_parser = BitcoinParser()
+        tokens = btc_parser.tokenize_code(hex_script)
+        if verbose:
+            print(tokens)
+        program = btc_parser.build_control_flow_graph(tokens)
+
+        machine = BTCMachine(FullySymbolicRAM, BTC_VECTOR_SIZE, stack_count=2)
+
+        symbolic_executer = SymbolicExecuter()
+        final_machine = symbolic_executer.execute(program, machine)
+        top_elt = final_machine.pop_from_stack()
+
+        s = Solver()
+        s.add(top_elt.val != 0)
+        s.add(final_machine._constraints)
+        z3.set_param("model.compact", False)
+
+        satisfiability = s.check()
+        if satisfiability == sat:
+            m = s.model()
 
-    machine = BTCMachine(FullySymbolicRAM, BTC_VECTOR_SIZE, stack_count=2)
 
-    symbolic_executer = SymbolicExecuter()
-    final_machine = symbolic_executer.execute(program, machine)
-    top_elt = final_machine.pop_from_stack()
+        return_dict["satisfiability"] = Satifiability.z3_to_enum(satisfiability)
+        return_dict["model"] = str(m)
 
-    s = Solver()
-    s.add(top_elt.val != 0)
-    s.add(final_machine._constraints)
-    z3.set_param('model.compact', False)
+    except InvalidOpCode as e:
+        return_dict["satisfiability"] = Satifiability.UNSPENDABLE
+        return_dict["model"] = {}
 
-    satisfiability = s.check()
-    if satisfiability == sat:
-        m = s.model()
+    except IncompleteIfEndIfClause as e:
+        return_dict["satisfiability"] = Satifiability.UNSPENDABLE
+        return_dict["model"] = {}
+
+    except UnimplementedInstructionError as e:
+        if e.tag in [InstructionTag.RESERVED, InstructionTag.DISABLED]:
+            return_dict["satisfiability"] = Satifiability.UNSPENDABLE
+            return_dict["model"] = {}
+        else:
+            return_dict["satisfiability"] = Satifiability.UNKNOWN
+            return_dict["model"] = {}
+            raise e
 
-    return_dict["satisfiability"] = Satifiability.z3_to_enum(satisfiability)
-    return_dict["model"] = str(m)
+    except Exception as e:
+        raise e
 
 
 def find_unlocking_script(hex_script: str, timeout=None, verbose=False):
@@ -63,7 +100,9 @@ def find_unlocking_script(hex_script: str, timeout=None, verbose=False):
     manager = Manager()
     return_dict = manager.dict()
 
-    p1 = Process(target=__find_unlocking_script_timed, args=(hex_script, return_dict, verbose))
+    p1 = Process(
+        target=__find_unlocking_script_timed, args=(hex_script, return_dict, verbose)
+    )
     p1.start()
     p1.join(timeout=timeout)
     p1.terminate()