Cosmetic changes & README sr/plugin

4 files changed, 56 insertions, 54 deletions

diff --git a/src/focaccia/arch/aarch64.py b/src/focaccia/arch/aarch64.py
index af173e3..0e7d98c 100644
--- a/src/focaccia/arch/aarch64.py
+++ b/src/focaccia/arch/aarch64.py
@@ -7,37 +7,37 @@ from .arch import Arch, RegisterDescription as _Reg
 archname = 'aarch64'
 
 registers = [
-    _Reg(('R0',  0, 64), ('X0',  0, 64), ('W0',  0, 32)),
-    _Reg(('R1',  0, 64), ('X1',  0, 64), ('W1',  0, 32)),
-    _Reg(('R2',  0, 64), ('X2',  0, 64), ('W2',  0, 32)),
-    _Reg(('R3',  0, 64), ('X3',  0, 64), ('W3',  0, 32)),
-    _Reg(('R4',  0, 64), ('X4',  0, 64), ('W4',  0, 32)),
-    _Reg(('R5',  0, 64), ('X5',  0, 64), ('W5',  0, 32)),
-    _Reg(('R6',  0, 64), ('X6',  0, 64), ('W6',  0, 32)),
-    _Reg(('R7',  0, 64), ('X7',  0, 64), ('W7',  0, 32)),
-    _Reg(('R8',  0, 64), ('X8',  0, 64), ('W8',  0, 32)),
-    _Reg(('R9',  0, 64), ('X9',  0, 64), ('W9',  0, 32)),
-    _Reg(('R10', 0, 64), ('X10', 0, 64), ('W10', 0, 32)),
-    _Reg(('R11', 0, 64), ('X11', 0, 64), ('W11', 0, 32)),
-    _Reg(('R12', 0, 64), ('X12', 0, 64), ('W12', 0, 32)),
-    _Reg(('R13', 0, 64), ('X13', 0, 64), ('W13', 0, 32)),
-    _Reg(('R14', 0, 64), ('X14', 0, 64), ('W14', 0, 32)),
-    _Reg(('R15', 0, 64), ('X15', 0, 64), ('W15', 0, 32)),
-    _Reg(('R16', 0, 64), ('X16', 0, 64), ('W16', 0, 32)),
-    _Reg(('R17', 0, 64), ('X17', 0, 64), ('W17', 0, 32)),
-    _Reg(('R18', 0, 64), ('X18', 0, 64), ('W18', 0, 32)),
-    _Reg(('R19', 0, 64), ('X19', 0, 64), ('W19', 0, 32)),
-    _Reg(('R20', 0, 64), ('X20', 0, 64), ('W20', 0, 32)),
-    _Reg(('R21', 0, 64), ('X21', 0, 64), ('W21', 0, 32)),
-    _Reg(('R22', 0, 64), ('X22', 0, 64), ('W22', 0, 32)),
-    _Reg(('R23', 0, 64), ('X23', 0, 64), ('W23', 0, 32)),
-    _Reg(('R24', 0, 64), ('X24', 0, 64), ('W24', 0, 32)),
-    _Reg(('R25', 0, 64), ('X25', 0, 64), ('W25', 0, 32)),
-    _Reg(('R26', 0, 64), ('X26', 0, 64), ('W26', 0, 32)),
-    _Reg(('R27', 0, 64), ('X27', 0, 64), ('W27', 0, 32)),
-    _Reg(('R28', 0, 64), ('X28', 0, 64), ('W28', 0, 32)),
-    _Reg(('R29', 0, 64), ('X29', 0, 64), ('W29', 0, 32)),
-    _Reg(('R30', 0, 64), ('X30', 0, 64), ('W30', 0, 32), ('LR', 0, 64)),
+    _Reg(('X0',  0, 64), ('W0',  0, 32)),
+    _Reg(('X1',  0, 64), ('W1',  0, 32)),
+    _Reg(('X2',  0, 64), ('W2',  0, 32)),
+    _Reg(('X3',  0, 64), ('W3',  0, 32)),
+    _Reg(('X4',  0, 64), ('W4',  0, 32)),
+    _Reg(('X5',  0, 64), ('W5',  0, 32)),
+    _Reg(('X6',  0, 64), ('W6',  0, 32)),
+    _Reg(('X7',  0, 64), ('W7',  0, 32)),
+    _Reg(('X8',  0, 64), ('W8',  0, 32)),
+    _Reg(('X9',  0, 64), ('W9',  0, 32)),
+    _Reg(('X10', 0, 64), ('W10', 0, 32)),
+    _Reg(('X11', 0, 64), ('W11', 0, 32)),
+    _Reg(('X12', 0, 64), ('W12', 0, 32)),
+    _Reg(('X13', 0, 64), ('W13', 0, 32)),
+    _Reg(('X14', 0, 64), ('W14', 0, 32)),
+    _Reg(('X15', 0, 64), ('W15', 0, 32)),
+    _Reg(('X16', 0, 64), ('W16', 0, 32)),
+    _Reg(('X17', 0, 64), ('W17', 0, 32)),
+    _Reg(('X18', 0, 64), ('W18', 0, 32)),
+    _Reg(('X19', 0, 64), ('W19', 0, 32)),
+    _Reg(('X20', 0, 64), ('W20', 0, 32)),
+    _Reg(('X21', 0, 64), ('W21', 0, 32)),
+    _Reg(('X22', 0, 64), ('W22', 0, 32)),
+    _Reg(('X23', 0, 64), ('W23', 0, 32)),
+    _Reg(('X24', 0, 64), ('W24', 0, 32)),
+    _Reg(('X25', 0, 64), ('W25', 0, 32)),
+    _Reg(('X26', 0, 64), ('W26', 0, 32)),
+    _Reg(('X27', 0, 64), ('W27', 0, 32)),
+    _Reg(('X28', 0, 64), ('W28', 0, 32)),
+    _Reg(('X29', 0, 64), ('W29', 0, 32)),
+    _Reg(('X30', 0, 64), ('W30', 0, 32), ('LR', 0, 64)),
 
     _Reg(('RZR', 0, 64), ('XZR', 0, 64), ('WZR', 0, 32)),
     _Reg(('SP', 0, 64), ('RSP', 0, 64)),
@@ -179,4 +179,3 @@ class ArchAArch64(Arch):
             from . import aarch64_dczid as dczid
             return dczid.read
         return None
-
diff --git a/src/focaccia/snapshot.py b/src/focaccia/snapshot.py
index 294afb1..03a03cd 100644
--- a/src/focaccia/snapshot.py
+++ b/src/focaccia/snapshot.py
@@ -90,6 +90,7 @@ class ReadableProgramState:
     """Interface for read-only program states."""
     def __init__(self, arch: Arch):
         self.arch = arch
+        self.strict = True
 
     def read_register(self, reg: str) -> int:
         """Read a register's value.
diff --git a/src/focaccia/symbolic.py b/src/focaccia/symbolic.py
index 3925a06..7b6098e 100644
--- a/src/focaccia/symbolic.py
+++ b/src/focaccia/symbolic.py
@@ -338,7 +338,7 @@ class SymbolicTransform:
         """
         res = {}
         for regname, expr in self.changed_regs.items():
-            if regname.upper() in self.arch.ignored_regs:
+            if not conc_state.strict and regname.upper() in self.arch.ignored_regs:
                 continue
             res[regname] = eval_symbol(expr, conc_state)
         return res
diff --git a/src/focaccia/tools/validation_server.py b/src/focaccia/tools/validation_server.py
index 6a62fa3..b87048a 100755
--- a/src/focaccia/tools/validation_server.py
+++ b/src/focaccia/tools/validation_server.py
@@ -26,7 +26,7 @@ def endian_fmt(endianness: str) -> str:
     else:
         return '>'
 
-def mkCommand(cmd: str, endianness: str, reg: str="", addr: int=0, size: int=0) -> bytes:
+def mk_command(cmd: str, endianness: str, reg: str="", addr: int=0, size: int=0) -> bytes:
     # char[16]:regname | long long:addr long long:size | long long:unused
     # READ REG         | READ MEM                      | STEP ONE
 
@@ -41,7 +41,7 @@ def mkCommand(cmd: str, endianness: str, reg: str="", addr: int=0, size: int=0)
         return struct.pack(fmt, 0, 0, "STEP ONE".encode('utf-8'))
     else:
         raise ValueError(f'Unknown command {cmd}')
-def unmkMemory(msg: bytes, endianness: str) -> tuple:
+def unmk_memory(msg: bytes, endianness: str) -> tuple:
     # packed!
     # unsigned long long: addr
     # unsigned long: length
@@ -50,7 +50,7 @@ def unmkMemory(msg: bytes, endianness: str) -> tuple:
 
     return addr, length
 
-def unmkRegister(msg: bytes, endianness: str) -> tuple:
+def unmk_register(msg: bytes, endianness: str) -> tuple:
     # packed!
     # char[108]:regname | unsigned long:bytes | char[64]:value
     fmt = f'{endian_fmt(endianness)}108sQ64s'
@@ -62,9 +62,7 @@ def unmkRegister(msg: bytes, endianness: str) -> tuple:
                                   f'[QEMU Plugin] Unable to access register {reg_name}.')
 
     val = val[:size]
-
     val = int.from_bytes(val, endianness)
-
     return val, size
 
 class PluginProgramState(ProgramState):
@@ -88,7 +86,7 @@ class PluginProgramState(ProgramState):
 
     def __init__(self, arch: Arch):
         super().__init__(arch)
-        self.curr_pc = -1
+        self.strict = False
 
     def read_register(self, reg: str, no_cached: bool=False) -> int:
         global CONN
@@ -100,11 +98,16 @@ class PluginProgramState(ProgramState):
         if reg in flags and self.arch.archname in self.flag_register_names:
             reg_name = self.flag_register_names[self.arch.archname]
         else:
-            reg_name = reg
+            reg_name = self.arch.to_regname(reg)
+
+        if reg_name is None:
+            raise RegisterAccessError(reg, f'Not a register name: {reg}')
 
-        reg_name = reg_name.lower()
-        reg_name = self.arch.to_regname(reg_name)
-        reg_name = reg_name.lower()
+        reg_acc = self.arch.get_reg_accessor(reg_name)
+        if reg_acc is None:
+            raise RegisterAccessError(reg, f'Not a enclosing register name: {reg}')
+            exit(-1)
+        reg_name = reg_acc.base_reg.lower()
 
         val = None
         from_cache = False
@@ -112,7 +115,7 @@ class PluginProgramState(ProgramState):
             val = super().read_register(reg_name)
             from_cache = True
         else:
-            msg = mkCommand("read register", self.arch.endianness, reg=reg_name)
+            msg = mk_command("read register", self.arch.endianness, reg=reg_name)
             CONN.send(msg)
 
             try:
@@ -125,8 +128,7 @@ class PluginProgramState(ProgramState):
                 print(f'Response: {resp}')
                 return 0
 
-
-            val, size = unmkRegister(resp, self.arch.endianness)
+            val, size = unmk_register(resp, self.arch.endianness)
 
         # Try to access the flags register with `reg` as a logical flag name
         if reg in flags and self.arch.archname in self.flag_register_names:
@@ -140,7 +142,7 @@ class PluginProgramState(ProgramState):
 
         if not from_cache:
             self.set_register(reg, val)
-        return val
+        return val & reg_acc.mask >> reg_acc.start
 
     def read_memory(self, addr: int, size: int) -> bytes:
         global CONN
@@ -150,14 +152,14 @@ class PluginProgramState(ProgramState):
 
         # print(f'Reading memory at {addr:x}, size={size}')
 
-        msg = mkCommand("read memory", self.arch.endianness, addr=addr, size=size)
+        msg = mk_command("read memory", self.arch.endianness, addr=addr, size=size)
         CONN.send(msg)
 
         try:
             resp = CONN.recv(16)
         except ConnectionResetError:
             raise StopIteration
-        _addr, length = unmkMemory(resp, self.arch.endianness)
+        _addr, length = unmk_memory(resp, self.arch.endianness)
 
         if _addr != addr or length == 0:
             raise MemoryAccessError(
@@ -180,7 +182,7 @@ class PluginProgramState(ProgramState):
         global CONN
 
         self._flush_caches()
-        msg = mkCommand("step", self.arch.endianness)
+        msg = mk_command("step", self.arch.endianness)
         CONN.send(msg)
 
 
@@ -264,7 +266,7 @@ def record_minimal_snapshot(prev_state: ProgramState,
     assert(cur_state.read_register('pc') == cur_transform.addr)
     assert(prev_transform.arch == cur_transform.arch)
 
-    def get_written_addresses(t: SymbolicTransform):
+    def get_written_addresses(t: SymbolicTransform) -> Iterable[ExprMem]:
         """Get all output memory accesses of a symbolic transformation."""
         return [ExprMem(a, v.size) for a, v in t.changed_mem.items()]
 
@@ -297,9 +299,7 @@ def record_minimal_snapshot(prev_state: ProgramState,
     set_values(prev_transform.changed_regs.keys(),
                get_written_addresses(prev_transform),
                cur_state,
-               prev_state,  # Evaluate memory addresses based on previous
-                            # state because they are that state's output
-                            # addresses.
+               prev_state,
                state)
     set_values(cur_transform.get_used_registers(),
                cur_transform.get_used_memory_addresses(),
@@ -398,6 +398,7 @@ def main():
     sock_path = args.use_socket
 
     qemu = PluginStateIterator(sock_path, arch)
+
     # Use symbolic trace to collect concrete trace from QEMU
     conc_states, matched_transforms = collect_conc_trace(
         qemu,
@@ -415,3 +416,4 @@ def main():
 
 if __name__ == "__main__":
     main()
+