Chess changes breakout for upstream

Dockerfile

@@ -7,7 +7,14 @@ LABEL dockerfile_maintenance=trailofbits
 
 ENV LANG C.UTF-8
 
-RUN apt-get -y update && DEBIAN_FRONTEND=noninteractive apt-get -y install python3.7 python3.7-dev python3-pip git wget
+RUN export DEBIAN_FRONTEND="noninteractive" && \
+    apt-get update && \
+    apt-get install -y \
+        gpg wget && \
+      wget -O - https://apt.kitware.com/keys/kitware-archive-latest.asc 2>/dev/null | gpg --dearmor - | tee /usr/share/keyrings/kitware-archive-keyring.gpg >/dev/null && \
+      echo 'deb [signed-by=/usr/share/keyrings/kitware-archive-keyring.gpg] https://apt.kitware.com/ubuntu/ bionic main' | tee /etc/apt/sources.list.d/kitware.list >/dev/null && \
+      apt-get update && \
+      apt-get -y install python3.7 python3.7-dev python3-pip git wget cmake build-essential pkg-config
 
 # Install solc 0.4.25 and validate it
 RUN wget https://github.com/ethereum/solidity/releases/download/v0.4.25/solc-static-linux \

manticore/__main__.py

@@ -29,6 +29,9 @@ def main() -> None:
     """
     Dispatches execution into one of Manticore's engines: evm or native.
     """
+    # Only print with Manticore's logger
+    logging.getLogger().handlers = []
+    log.init_logging()
     args = parse_arguments()
 
     if args.no_colors:
@@ -101,13 +104,13 @@ def positive(value):
         help=("A folder name for temporaries and results." "(default mcore_?????)"),
     )
 
-    current_version = pkg_resources.get_distribution("manticore").version
-    parser.add_argument(
-        "--version",
-        action="version",
-        version=f"Manticore {current_version}",
-        help="Show program version information",
-    )
+    # current_version = pkg_resources.get_distribution("manticore").version
+    # parser.add_argument(
+    #    "--version",
+    #    action="version",
+    #    version=f"Manticore {current_version}",
+    #    help="Show program version information",
+    # )
     parser.add_argument(
         "--config",
         type=str,

manticore/core/smtlib/visitors.py

@@ -503,13 +503,31 @@ def visit_BoolAnd(self, expression, *operands):
                         ) == BitVecExtract(operand=value1, offset=beg, size=end - beg + 1)
 
     def visit_BoolNot(self, expression, *operands):
+        """
+        !!a -> a
+        !(a&&b) -> !a || !b
+        !(a||b) -> !a && !b
+        """
         if isinstance(operands[0], BoolNot):
             return operands[0].operands[0]
 
+        if isinstance(operands[0], BoolAnd):
+            return BoolOr(
+                a=BoolNot(value=operands[0].operands[0]), b=BoolNot(value=operands[0].operands[1])
+            )
+
+        if isinstance(operands[0], BoolOr):
+            return BoolAnd(
+                a=BoolNot(value=operands[0].operands[0]), b=BoolNot(value=operands[0].operands[1])
+            )
+
     def visit_BoolEqual(self, expression, *operands):
         """(EQ, ITE(cond, constant1, constant2), constant1) -> cond
         (EQ, ITE(cond, constant1, constant2), constant2) -> NOT cond
         (EQ (extract a, b, c) (extract a, b, c))
+
+        EQ (a) True -> a
+        EQ (a) False -> !a
         """
         if isinstance(operands[0], BitVecITE) and isinstance(operands[1], Constant):
             if isinstance(operands[0].operands[1], Constant) and isinstance(
@@ -537,6 +555,9 @@ def visit_BoolEqual(self, expression, *operands):
 
                 return BoolConstant(value=True, taint=expression.taint)
 
+        if isinstance(operands[1], BoolConstant):
+            return operands[0] if operands[1].value else BoolNot(value=operands[0])
+
     def visit_BoolOr(self, expression, a, b):
         if isinstance(a, Constant):
             if a.value == False:
@@ -715,6 +736,18 @@ def visit_BitVecAdd(self, expression, *operands):
             if left.value == 0:
                 return right
 
+    def visit_BitVecMul(self, expression, *operands):
+        """
+        a * 1  ==> a
+        1 * a  ==> a
+        """
+        left = operands[0]
+        right = operands[1]
+        if isinstance(right, BitVecConstant) and right.value == 1:
+            return left
+        if isinstance(left, BitVecConstant) and left.value == 1:
+            return right
+
     def visit_BitVecSub(self, expression, *operands):
         """a - 0 ==> a
         (a + b) - b  ==> a

manticore/native/cpu/x86.py

@@ -249,13 +249,6 @@ class AMD64RegFile(RegisterFile):
         "TOP": Regspec("FPSW", int, 11, 3, False),
         "FPTAG": Regspec("FPTAG", int, 0, 16, False),
         "FPCW": Regspec("FPCW", int, 0, 16, False),
-        "FOP": Regspec("FOP", int, 0, 11, False),
-        "FIP": Regspec("FIP", int, 0, 64, False),
-        "FCS": Regspec("FCS", int, 0, 16, False),
-        "FDP": Regspec("FDP", int, 0, 64, False),
-        "FDS": Regspec("FDS", int, 0, 16, False),
-        "MXCSR": Regspec("MXCSR", int, 0, 32, False),
-        "MXCSR_MASK": Regspec("MXCSR_MASK", int, 0, 32, False),
         "CF": Regspec("CF", bool, 0, 1, False),
         "PF": Regspec("PF", bool, 0, 1, False),
         "AF": Regspec("AF", bool, 0, 1, False),
@@ -363,13 +356,6 @@ class AMD64RegFile(RegisterFile):
         "TOP": ("FPSW",),
         "FPCW": (),
         "FPTAG": (),
-        "FOP": (),
-        "FIP": (),
-        "FCS": (),
-        "FDP": (),
-        "FDS": (),
-        "MXCSR": (),
-        "MXCSR_MASK": (),
         "FP0": (),
         "FP1": (),
         "FP2": (),
@@ -510,13 +496,6 @@ class AMD64RegFile(RegisterFile):
         "FPSW",
         "FPCW",
         "FPTAG",
-        "FOP",
-        "FIP",
-        "FCS",
-        "FDP",
-        "FDS",
-        "MXCSR",
-        "MXCSR_MASK",
     )
 
     def __init__(self, *args, **kwargs):
@@ -576,18 +555,7 @@ def __init__(self, *args, **kwargs):
         for reg in ("FP0", "FP1", "FP2", "FP3", "FP4", "FP5", "FP6", "FP7"):
             self._registers[reg] = (0, 0)
 
-        for reg in (
-            "FPSW",
-            "FPTAG",
-            "FPCW",
-            "FOP",
-            "FIP",
-            "FCS",
-            "FDP",
-            "FDS",
-            "MXCSR",
-            "MXCSR_MASK",
-        ):
+        for reg in ("FPSW", "FPTAG", "FPCW"):
             self._registers[reg] = 0
 
         self._cache = {}
@@ -659,14 +627,7 @@ def _get_flag(self, register_id, register_size, offset, size):
     def _set_float(self, register_id, register_size, offset, size, reset, value):
         assert size == 80
         assert offset == 0
-        # Translate int bitfield into a floating point value according
-        # to IEEE 754 standard, 80-bit double extended precision
-        if isinstance(value, int):
-            value &= 0xFFFFFFFFFFFFFFFFFFFF  # 80-bit mask
-            exponent = value >> 64  # Exponent is the 16 higher bits
-            mantissa = value & 0xFFFFFFFFFFFFFFFF  # Mantissa is the lower 64 bits
-            value = (mantissa, exponent)
-        elif not isinstance(value, tuple):
+        if not isinstance(value, tuple):  # Add decimal here?
             raise TypeError
         self._registers[register_id] = value
         return value
@@ -939,23 +900,6 @@ def canonicalize_instruction_name(self, instruction):
         name = OP_NAME_MAP.get(name, name)
         return name
 
-    def read_register_as_bitfield(self, name):
-        """Read a register and return its value as a bitfield.
-        - if the register holds a bitvector, the bitvector object is returned.
-        - if the register holds a concrete value (int/float) it is returned as
-        a bitfield matching its representation in memory
-
-        This is mainly used to be able to write floating point registers to
-        memory.
-        """
-        value = self.read_register(name)
-        if isinstance(value, tuple):
-            # Convert floating point to bitfield according to IEEE 754
-            # (16-bits exponent).(64-bits mantissa)
-            mantissa, exponent = value
-            value = mantissa + (exponent << 64)
-        return value
-
     #
     # Instruction Implementations
     #
@@ -5748,37 +5692,6 @@ def sem_SYSCALL(cpu):
         cpu.R11 = cpu.RFLAGS
         raise Syscall()
 
-    def generic_FXSAVE(cpu, dest, reg_layout):
-        """
-        Saves the current state of the x87 FPU, MMX technology, XMM, and
-        MXCSR registers to a 512-byte memory location specified in the
-        destination operand.
-
-        The content layout of the 512 byte region depends
-        on whether the processor is operating in non-64-bit operating modes
-        or 64-bit sub-mode of IA-32e mode
-        """
-        addr = dest.address()
-        for offset, reg, size in reg_layout:
-            cpu.write_int(addr + offset, cpu.read_register_as_bitfield(reg), size)
-
-    def generic_FXRSTOR(cpu, dest, reg_layout):
-        """
-        Reloads the x87 FPU, MMX technology, XMM, and MXCSR registers from
-        the 512-byte memory image specified in the source operand. This data should
-        have been written to memory previously using the FXSAVE instruction, and in
-        the same format as required by the operating modes. The first byte of the data
-        should be located on a 16-byte boundary.
-
-        There are three distinct layouts of the FXSAVE state map:
-        one for legacy and compatibility mode, a second
-        format for 64-bit mode FXSAVE/FXRSTOR with REX.W=0, and the third format is for
-        64-bit mode with FXSAVE64/FXRSTOR64
-        """
-        addr = dest.address()
-        for offset, reg, size in reg_layout:
-            cpu.write_register(reg, cpu.read_int(addr + offset, size))
-
     @instruction
     def SYSCALL(cpu):
         """
@@ -6646,44 +6559,6 @@ class AMD64Cpu(X86Cpu):
     arch = cs.CS_ARCH_X86
     mode = cs.CS_MODE_64
 
-    # CPU specific instruction behaviour
-    FXSAVE_layout = [
-        (0, "FPCW", 16),
-        (2, "FPSW", 16),
-        (4, "FPTAG", 8),
-        (6, "FOP", 16),
-        (8, "FIP", 32),
-        (12, "FCS", 16),
-        (16, "FDP", 32),
-        (20, "FDS", 16),
-        (24, "MXCSR", 32),
-        (28, "MXCSR_MASK", 32),
-        (32, "FP0", 80),
-        (48, "FP1", 80),
-        (64, "FP2", 80),
-        (80, "FP3", 80),
-        (96, "FP4", 80),
-        (112, "FP5", 80),
-        (128, "FP6", 80),
-        (144, "FP7", 80),
-        (160, "XMM0", 128),
-        (176, "XMM1", 128),
-        (192, "XMM2", 128),
-        (208, "XMM3", 128),
-        (224, "XMM4", 128),
-        (240, "XMM5", 128),
-        (256, "XMM6", 128),
-        (272, "XMM7", 128),
-        (288, "XMM8", 128),
-        (304, "XMM9", 128),
-        (320, "XMM10", 128),
-        (336, "XMM11", 128),
-        (352, "XMM12", 128),
-        (368, "XMM13", 128),
-        (384, "XMM14", 128),
-        (400, "XMM15", 128),
-    ]
-
     def __init__(self, memory: Memory, *args, **kwargs):
         """
         Builds a CPU model.
@@ -6799,14 +6674,6 @@ def XLATB(cpu):
         """
         cpu.AL = cpu.read_int(cpu.RBX + Operators.ZEXTEND(cpu.AL, 64), 8)
 
-    @instruction
-    def FXSAVE(cpu, dest):
-        return cpu.generic_FXSAVE(dest, AMD64Cpu.FXSAVE_layout)
-
-    @instruction
-    def FXRSTOR(cpu, src):
-        return cpu.generic_FXRSTOR(src, AMD64Cpu.FXSAVE_layout)
-
 
 class I386Cpu(X86Cpu):
     # Config
@@ -6816,36 +6683,6 @@ class I386Cpu(X86Cpu):
     arch = cs.CS_ARCH_X86
     mode = cs.CS_MODE_32
 
-    # CPU specific instruction behaviour
-    FXSAVE_layout = [
-        (0, "FPCW", 16),
-        (2, "FPSW", 16),
-        (4, "FPTAG", 8),
-        (6, "FOP", 16),
-        (8, "FIP", 32),
-        (12, "FCS", 16),
-        (16, "FDP", 32),
-        (20, "FDS", 16),
-        (24, "MXCSR", 32),
-        (28, "MXCSR_MASK", 32),
-        (32, "FP0", 80),
-        (48, "FP1", 80),
-        (64, "FP2", 80),
-        (80, "FP3", 80),
-        (96, "FP4", 80),
-        (112, "FP5", 80),
-        (128, "FP6", 80),
-        (144, "FP7", 80),
-        (160, "XMM0", 128),
-        (176, "XMM1", 128),
-        (192, "XMM2", 128),
-        (208, "XMM3", 128),
-        (224, "XMM4", 128),
-        (240, "XMM5", 128),
-        (256, "XMM6", 128),
-        (272, "XMM7", 128),
-    ]
-
     def __init__(self, memory: Memory, *args, **kwargs):
         """
         Builds a CPU model.
@@ -6912,26 +6749,7 @@ def canonical_registers(self):
         regs = ["EAX", "ECX", "EDX", "EBX", "ESP", "EBP", "ESI", "EDI", "EIP"]
         regs.extend(["CS", "DS", "ES", "SS", "FS", "GS"])
         regs.extend(
-            [
-                "FP0",
-                "FP1",
-                "FP2",
-                "FP3",
-                "FP4",
-                "FP5",
-                "FP6",
-                "FP7",
-                "FPCW",
-                "FPSW",
-                "FPTAG",
-                "FOP",
-                "FIP",
-                "FCS",
-                "FDP",
-                "FDS",
-                "MXCSR",
-                "MXCSR_MASK",
-            ]
+            ["FP0", "FP1", "FP2", "FP3", "FP4", "FP5", "FP6", "FP7", "FPCW", "FPSW", "FPTAG"]
         )
         regs.extend(
             [
@@ -6983,11 +6801,3 @@ def XLATB(cpu):
         :param dest: destination operand.
         """
         cpu.AL = cpu.read_int(cpu.EBX + Operators.ZEXTEND(cpu.AL, 32), 8)
-
-    @instruction
-    def FXSAVE(cpu, dest):
-        return cpu.generic_FXSAVE(dest, I386Cpu.FXSAVE_layout)
-
-    @instruction
-    def FXRSTOR(cpu, src):
-        return cpu.generic_FXRSTOR(src, I386Cpu.FXSAVE_layout)