[Machine]

	* IMachine: Add an abstract method `is_true` to evaluate an
		expression.
	* StackBasedMachine:
		* `is_true` implementation;
		* `__init__` takes a program in input;
		* `push_onto_stack`: enforce that any element in
		  memory is a `z3.BitVec` element.

symbolic_execution/machines/interfaces.py

@@ -24,6 +24,11 @@ class IMachine(ABC):
         """Alters the program counter."""
         pass
 
+    @abstractmethod
+    def is_true(self, expr) -> bool:
+        """Evaluate an expression and return a boolean."""
+        pass
+
 
 class IStackBasedMachine(IMachine):
     """Abstract class to represent a stack based machine."""

symbolic_execution/machines/stack_based.py

 """Implementation of a stack-based machine able to run Bitcoin scripts."""
-from typing import Any
-from z3 import BitVec, Int
+from typing import Any, Dict
+from symbolic_execution.instruction.interfaces import IInstruction
+from z3 import BitVec, Int, is_bv, BitVecVal, simplify, is_true, is_false
 
 from .interfaces import IStackBasedMachine
 
+# Btc script supports byte vectors up to 520 bytes
+BTC_MAX_VALUE_SIZE = 520 * 8
+
+
+class SymbolicConditionError(Exception):
+    """A symbolic condition couldn't be evaluated.
+
+    Raised by the machine when a symbolic expression can't be evaluated
+    to True or False.
+    """
+
+    pass
+
 
 class StackBasedMachine(IStackBasedMachine):
     """Class to represent a Bitcoin machine able to run a script."""
 
-    def __init__(self, symbol_generation=True):
+    def __init__(self,
+                 program: Dict[int, IInstruction],
+                 symbol_generation=True):
         """Initialize the virtual Bitcoin machine.
 
         Set {symbol_generation} to True to allow the machine to generate
@@ -32,37 +48,57 @@ class StackBasedMachine(IStackBasedMachine):
         # Symbols created by the machine.
         self._symbols = []
 
-        # Programm being run
-        self._program = None
+        # Program being run
+        self._program = program
+
+        # Program counter
+        self._pc = 0
 
     # ################ #
     # IMachine Methods #
     # ################ #
-    # TODO to rework
     @property
     def program(self):
         """The program being run."""
-        pass
+        return self._program
 
-    # TODO to rework
     @property
     def pc(self) -> int:
         """The program counter."""
         return self._pc
 
-    # TODO to rework
     @pc.setter
     def pc(self, new_pc: int) -> int:
         """Alters the program counter."""
         self._pc = new_pc
 
+    def is_true(self, expr) -> bool:
+        """Evaluate an expression and return a boolean."""
+        # In btc, False is represented by 0
+        expr = simplify(expr != 0)
+
+        true, false = is_true(expr), is_false(expr)
+
+        if not true and not false:
+            raise SymbolicConditionError(f"""This expression can't be evaluated
+                to True nor False: {expr}""")
+        elif true and false:
+            # This case should never happen
+            raise SymbolicConditionError(f"""This expression is evaluated
+                to True and False: {expr}""")
+
+        return true
+
     # ########################## #
     # IStackBasedMachine Methods #
     # ########################## #
 
     def push_onto_stack(self, element: Any):
         """Put an element onto the stack."""
-        self._stack.append(element)
+        if is_bv(element):
+            self._stack.append(simplify(element))
+        else:
+            self._stack.append(BitVecVal(element, BTC_MAX_VALUE_SIZE))
 
     def pop_from_stack(self) -> Any:
         """Pop and return an element from the stack.
@@ -75,7 +111,8 @@ class StackBasedMachine(IStackBasedMachine):
         except IndexError as e:
             if self._symbol_generation:
                 sym_cnt = len(self._symbols)
-                self._symbols.append(BitVec(f"sym_{sym_cnt}", 32))
+                self._symbols.append(
+                    BitVec(f"sym_{sym_cnt}", BTC_MAX_VALUE_SIZE))
                 return self._symbols[sym_cnt]
             else:
                 raise e