Блог

Я работаю над проектом обратного проектирования, в котором меня просят выполнить обратное срезание кода сборки. для данного регистра кода сборки в данной функции кода сборки я хотел бы обнаружить все инструкции внутри функции сборки, которые выполняют операцию, обновляющую этот регистр. Короче говоря, я представляю операции этих инструкций, например, в виде выражений z3

 sub r2 r2 10
add r1 r2 3 
 

регистр r1 представлен в виде (bvadd #x0000000d r2)) . однако в случае инструкции ldr, такой как

 ldr r2,[r2, #13]
add r1 r2 3
 

Я хочу представить память в виде карты, которая содержит выражения z3 в качестве ключей и значений, поэтому инструкция ldr должна быть выражением формы z3 (z3_ctx.select(mem, i)) только теперь мне нужна карта, а не массив в z3

итак, мой вопрос в том, как я могу построить карту в z3, ключи и значения которой являются выражениями z3, поскольку я хочу представить операции загрузки с этой карты в виде выражений z3, аналогичных (z3_ctx.select(mem, i)) в случае массива z3, только теперь сам i является выражением z3 (bvadd #x0000000d r2)

Массив SMTLib от битовых векторов до битовых векторов будет отлично работать для этого. С точки зрения API, нет никакой разницы между a map и an array в решении SMT: вы решаете его с помощью битовых векторов, как и то, что вы хотели сделать.

Ваше сообщение предполагает, что вы беспокоитесь, что не сможете «адресовать» массив с помощью выражения z3? Это неправда. Массив из битовых векторов в битовые векторы может быть адресован произвольными выражениями z3 правильного типа битового вектора.

Если вы попытались выполнить описанное выше и столкнулись с проблемами, опубликуйте код, который выдал вам ошибки. В противном случае, это должно работать просто отлично. (Сказав это, это не значит, что он будет «эффективным». Воспоминания, как правило, являются слабыми местами для решателей с точки зрения производительности; но это совсем другая тема.)