angr: добавить ограничение на адрес загрузки в состояние

Question

Этот вопрос относится к платформе символического исполнения. angr. В частности, хочу задать два вопроса:

1. Как найти символьное выражение для адресного операнда инструкции загрузки?
2. Как добавить ограничение в состояние, когда вышеупомянутый адрес является известным значением?

Чтобы дать больше информации, я использую Simulation Manager, где в любой момент есть список состояний в stashes. Рассмотрим любое конкретное состояниеst0. Это состояние сохраняет символическое состояние в соответствии с последовательностью инструкций, ведущих к последней инструкции, например, загрузкаmov (rdx), rax. Теперь внешняя информация (котораяangr не имеет) сообщил мне, что доступ к адресу на самом деле 0xdeadbeef.

Поэтому я считаю, что мне нужно сделать следующие шаги:

1. Из s0.addr, определите инструкцию и ее адресный операнд. Отсюда я получаю символический битовый вектор дляs0.regs._rax. Вопрос в основном в том, как мне выяснить, что адрес, используемый загрузкой, былrax?
2. Добавьте ограничение, которое rax == 0xdeadbeef. К счастью,angr у государства хороший add_constraintфункция. Вопрос в том, как мне выразить свое ограничение в коде?