Неожиданный результат от z3 при оценке выражения - PullRequest
Новая
       26

Неожиданный результат от z3 при оценке выражения

0 голосов
/ 08 апреля 2019

Итак, я пытался работать с решателями ограничений claripy и z3, чтобы найти диапазон возможных решений для данного выражения. К сожалению, claripy не хочет работать с выражением, если оно задано как строковый тип, но z3 может. Выражение таково:

(((((rax+((rax>>>0x1f)>>0x1e))&0x3)-((rax>>>0x1f)>>0x1e))<<0x3)+6295648)

Чтобы было легче читать, я заменил LShR (логическое смещение вправо) на >>>, но в коде он правильно введен.

При работе с claripy, уравнение может быть оценено с помощью 11 различных возможных решений, но при попытке вычислить то же выражение с помощью z3, оно дает неожиданный (и неверный результат). Я попытался просмотреть примеры z3 в Интернете, а также некоторые примеры z3python, но ничто из того, что объясняется, не относится к моей проблеме или описывает результаты, которые я получаю.

Код с использованием z3 (python 2.7) 

from z3 import *

rax = BitVec('rax', 64)
expr = 'UGE((((((rax+((LShR(rax,31))>>30))&3)-((LShR(rax,31))>>30)<<3)+6295648),6295648)'
F = eval(expr)
solve(F)

Код с использованием claripy (python3) 

import claripy

rax = claripy.BVS('rax', 64)
s = claripy.Solver()
soln_list = s.eval((((((rax+(claripy.LShR(rax,0x1f)>>0x1e))&0x3)-(claripy.LShR(rax,0x1f)>>0x1e))<<0x3)+6295648), 2**64)

Результат приведенного выше кода равен rax == 2, но ожидаемый результат должен быть rax == 0, так как замена 0 на rax приведет к 6295648>=6295648, что верно.

Что-то не так с форматом выражения, используемого для оценки? При жестком кодировании выражения для ясности для оценки, результаты гораздо больше похожи на то, что я ожидаю увидеть, список всех возможных результатов для уравнения, учитывая общее число возможностей, которыми может быть rax (2 * * 64).

Самым простым решением, вероятно, было бы использование claripy поверх z3python, но claripy работает только с кодом python3, в то время как программа, которая создает выражение, запускает python2.7. Другая проблема заключается в том, что claripy не хочет оценивать выражение, когда оно является строковым типом, что может выполнить z3, хотя оно дает неверные результаты.

TL: DR Попытка работать с z3 для вычисления выражения, чтобы найти минимальное значение, которое вызывает выражение для удовлетворения. Как только это станет известно, я хотел бы просмотреть диапазон значений, начиная с минимума, чтобы найти то, к чему будет относиться выражение. Проблемы с z3 приводят к неожиданным / неправильным оценкам исходного выражения.

...