about summary refs log tree commit diff stats
path: root/tools/_qemu_tool.py (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Implement online verification of symbolic backend ta/developTheofilos Augoustis2024-10-141-1/+6
| | | | | Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
* Add support for aarch64Theofilos Augoustis2024-07-121-23/+58
| | | | | | | | | | | | | | | | | | - Implement an architecture description for aarch64 - Add endianness information to the `Arch` class. - Move conversion from flags register to logical flag values from the calling code to the concrete targets (LLDB and GDB), which is the only point where we (have to) deal in flags registers. - Handle assembly/disassembly errors in serialization of SymbolicTransform - Move ProgramState's `arch` attribute into ReadableProgramState. Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>
* Make symbolic equations more symbolicTheofilos Augoustis2024-02-191-74/+84
| | | | | | Reduce the impact of concrete guidance on the process of calculating an instruction's symbolic equation. The resulting equations will contain less assumptions about the concrete state and thus be more generic.
* Store instructions in SymbolicTransformationTheofilos Augoustis2024-02-081-5/+18
|
* Verify QEMU by abstracting over inconsistencies in trace logs via matching ↵Theofilos Augoustis2024-01-301-0/+251
algorithm Co-authored-by: Theofilos Augoustis <theofilos.augoustis@gmail.com> Co-authored-by: Nicola Crivellin <nicola.crivellin98@gmail.com>