нужно решить уравнение либо сбрутить (но быстрее чем простой перебор)
a xor x - b xor x = c
где a,b,c,x - dwords

| Сообщение посчитали полезным:

Введи свою задачу в Z3, пусть решает, для него это должно быть ерундой.
https://rise4fun.com/Z3

| Сообщение посчитали полезным: Isaev

srm60171
Мне ещё и a,b надо брутить

| Сообщение посчитали полезным:

а там не важно, что назначишь переменными, то и будет искать.
Это же SMT солвер, ты ему условия обозначаешь, а он пытается подобрать входные данные для их удовлетворения.

| Сообщение посчитали полезным:

8 секунд занимает весь перебор под VMware на i5:



Добавлено спустя 19 минут
srm60171

Это не аналоговая функция, её нельзя сократить поксорив её компоненты. Так что солвер ваш это решить не может в принципе. Вам и тс идти назад в 5-й класс школы учить алгебру.

r99

> Мне ещё и a,b надо брутить

Тогда уравнения не существует, обратитесь к доктору, он вам подскажет как это решается.

-----
vx

| Сообщение посчитали полезным:

r99 пишет:
a xor x - b xor x = c
А чем Вас не устраивает случай, когда:
a = 0, b = 0, c = 0? (равны между собой)
просто не совсем понятно, зачем брутить, если такое большое количество неизвестных.

| Сообщение посчитали полезным:

c<>0

| Сообщение посчитали полезным:

как и предлагалось Z3



выхлоп
A = 0x0
B = 0x80000000L
X = 0x80000000L
C = 0x80000000L
OK!

При B == X всегда B^X == 0 и C == A^X

Если добавить условия A != B, A != X, B != X
s.add(A != B)
s.add(A != X)
s.add(B != X)
то выхлоп будет например

A = 0x1546aa96L
B = 0x1546aa93L
X = 0x1546aa90L
C = 3L
OK!

Т.е. A, B, X должны быть примерно равны и маскированием X оставляем младший ниббл, разность которых легко получить.

-----
127.0.0.1, sweet 127.0.0.1

| Сообщение посчитали полезным:

OKOB

Тоесть вы использовали умножение на ноль - одинаковую константу с парой изменённых младших бит, что бы при ксоре образовался ноль и выражение сошлось, вот так сейчас решаются задачи, главное сделать видимость, солвер как никак

Может быть для моего примера покажите вычисления ?

A = 1234
B = 123
C = 1127

Добавлено спустя 45 минут
Так как есть заблуждение на счёт функций - можно резолвить булевые и аналоговые, но никак не их комбинации, то для наглядности собрал простейшую диаграмку.



Y есть функция X через ксор с линейно изменяющимся значением(аналог ШИМ). Красивая диаграмка.

Это без ввода аналоговой компоненты в функцию.


bf55_31.12.2017_EXELAB.rU.tgz - xor.png

Добавлено спустя 1 час 3 минуты
Немного изменил функцию цветовую для наглядности.

6d22_31.12.2017_EXELAB.rU.tgz - xor2.png

На 3-м скрине N = 16.

Добавлено спустя 1 час 8 минут
..

9508_31.12.2017_EXELAB.rU.tgz - xor3.png

-----
vx

| Сообщение посчитали полезным:

difexacaw div 2018 = null

| Сообщение посчитали полезным:

difexacaw
тебе человек пример использования солвера показал, ты как обычно * не понял, желаю тебе мозгов в 2018м!!!
От модератора: крепких нервов вам в новом году! )

| Сообщение посчитали полезным:

>>> Может быть для моего примера покажите вычисления ?

>>> A = 1234
>>> B = 123
>>> C = 1127

A = 0x4d2
B = 0x7b
X = 0x80a
C = 0x467

в X старшие биты кроме задействованных в получении значения С могут быть любыми, т.к. Х используется в маскировании и уменьшаемого и вычитаемого.

-----
127.0.0.1, sweet 127.0.0.1

| Сообщение посчитали полезным:

OKOB

Ну и что это за цифры ?

Это аналого-цифровое выражение, я не знаю мат способа его как то изменить. Это значит что оно может быть решено только перебором. Для одного аргумента это заняло несколько секунд. Удивительно другое, вроде бы как простейшая ксор функция выдаёт столь сложный график, возможна ли по не нему какая то свёртка - сомневаюсь. Даже для элементарной функции задача свёртки становится слишком сложной. Что весьма печально, так как в принципе эта задача может быть решена алгоритмически, но нет основ, не известно с чего начать. Есть только один способ - использовать нейросеть, но это примитивная система, она не резолвит задачу, она находит зависимости. Это значит что такие темы провальные, нет мат модели а вероятные решения через какие то нс невозможны.
На данный момент положение дел такое. Есть сложные задачи, решение которых требует автоматики. В общем случае решения нет, есть локальные костыли и нет даже принципа, на основе которого можно строить механизм.
Думаю даже что наступил технологический коллапс. Так как задачи чётко формулированы и решение их в принципе возможно, но на данном этапе развития решение не может быть найдено к сожалению.

-----
vx

| Сообщение посчитали полезным:

difexacaw пишет: Это значит что оно может быть решено только перебором

То есть тебя не смущает, что солверы чаще всего описывают в функциональном стиле, в том самом в котором все вертится вокруг циклов и рекурсии?

difexacaw пишет: Думаю даже что наступил технологический коллапс

Не о том думаешь, нужно думать о задаче и условиях которые неполные. Под уравнение попадает больше одного решения, а тут возникает вот такая проблема https://ru.wikipedia.org/wiki/Проблема_остановки
и в данной задаче проще делать атаку на данные, если там какой то примитивный шифр и известно примерное содержание данных. Проблема в ТЗ, а не в солверах, некорректный подход к решению задачи, одни сплошные неизвестные и без перебора, ну пиздец, а как проверять выполнение условия. Солвер лишь маскирует брут, а не избавляет от него. В коем веке соглашусь с тобой, ТС нужно начинать с учебника алгебры.

| Сообщение посчитали полезным:

Временно уточним задачу. Допустим, у нас заданы a,b,c и мы ищем x.

Решение можно ускорить существенно, т.к. решения для младших бит не зависят от старших, а на старшие биты влияет лишь перенос разряда при вычитании.
Можно, например, перебрать 16 младших бит и 16 старших бит (с переносом и без), а потом комбинировать из них 32-битные решения.
Сложность 2^16 + 2*2^16 вместо 2^32.
Можно еще круче ускорить, если разбивать биты более, чем на две части.

Проблема в другом.
Данная формулировка задачи потенциально имеет такое количество решений, что вывод их всех эквивалентен брутфорсу.
Например, если a-b=c, то x{i} (i-ый бит числа x) может принимать любое значение при a{i}=b{i}.
То есть, берем a=1,b=0,c=1 и получаем 2^31 решений x.

А у вас, кроме всего прочего, a и b не фиксированы. Это вообще трындец.
Короче, переформулируйте задачу. Или не ебите всем мозги и выкладывайте исходную задачу.

Добавлено спустя 6 часов 39 минут
Чуть расширю мысль.
Если у вас есть некие a,b,c и x такие, что (a xor x) - (b xor x) = c, то вы можете изменять значения тех x{i}, для которых a{i}=b{i}, и получать новые решения x для данных a,b,c.
Короче, там будет реально дохрена решений.
В среднем, 2^16 для случайных a,b,c, имеющих хоть одно решение x.

| Сообщение посчитали полезным: difexacaw

всем спасибо - особенно за z3 ( не знал про такое).
все решилось брутом - (нашел ограничение для 2-х двордов размерами экзешника.) за 2 часа.

difexacaw пишет:
Вам и тс идти назад в 5-й класс школы учить алгебру.

какая алгебра в 5-классе?
школу так опустили , что в 6-классе еще дроби делят

| Сообщение посчитали полезным:

r99

Можно ваш брут код посмотреть ?

-----
vx

| Сообщение посчитали полезным:

там ничего интересного (из экзекриптора).
два дворда гоняются в пределах от min1=$401000 до max1=$58c100
в результате вылезает много решений из которых с помощью дополнительного условия отбирается всего
одно(!) годное.

| Сообщение посчитали полезным:

r99

Ищется указатель в кодовую секцию ?

Опишите плз исходную задачу, интересно.

-----
vx

| Сообщение посчитали полезным:

x60,x64,x74,x78,x7c,x94,xa0:dword; <---- неизвестные
x88=$2B30B554;
a0=$D5FA0D83; b0=$B268D4F0; a1=$677836C3; b1=$0311A5BE; a2=$1DB1154F; b2=$18F33EE0; a3=$5546FE86; b3=$3C1634EC;
a4=$6D16321A; b4=$464673F8; a5=$8D0A19F3; b5=$85D39CB9; a6=$89DFBF8B; b6=$7D13365F;
a7=$6D16321A : b7=$464673F8

здесь xor60 означает xor x60 и тд
x60 в диапазоне ($00401000-$EA008CE8 ..... 0058c100-$EA008CE8)
x74 в диапазоне ($00401000-$D6F6A087 ..... 0058c100-$D6F6A087)

(((a0 xor x60) ror 9) xor x74) add x78 =b0
(((a1 xor x60) rol $11) xor x74) add x78 =b1
a2 - x64 + x74 = b2
((a3 - x64) xor x74) add x78 = b3
((a4-x7c) xor x88) xor x94=b4
(((a5 xor x7c) xor x88) xor x94) -xa0 = b5
(a6-x94) xor xa0 = b6
((a7 - x7c) xor x88) xor x94 = b7

| Сообщение посчитали полезным:

Задача как раз для SMT солвера

Хотелось бы в системе уравнений увидеть скобки.
В 6м уравнении a5 xor7c xor88 xor94 -a0 = b5 последняя разность вероятно - ха0.
Да и другие константы 64, 74, 94 вероятно тоже имелось в виду х64, х74, х94.

в таком вот виде
s.add(((((0xD5FA0D83 ^ x60) >> 9) | (((0xD5FA0D83 ^ x60) & 0x1ff) << 23)) ^ x74) + x78 == 0xB268D4F0)
s.add(((((0x677836C3 ^ x60) >> 21) | (((0x677836C3 ^ x60) & 0x1fffff) << 11)) ^ x74) + x78 == 0x0311A5BE)
s.add((0x1DB1154F - x64) + x74 == 0x18F33EE0)
s.add(((0x5546FE86 - x64) ^ x74) + x78 == 0x3C1634EC)
s.add(((0x6D16321A - x7c) ^ x88) ^ x94 == 0x464673F8)
s.add((((0x8D0A19F3 ^ x7c) ^ x88) ^ x94) - xa0 == 0x85D39CB9)
s.add((0x89DFBF8B - x94) ^ xa0 == 0x7D13365F)
s.add(((0x6D16321A - x7c) ^ x88) ^ x94 == 0x464673F8)

система решения не имеет.

-----
127.0.0.1, sweet 127.0.0.1

| Сообщение посчитали полезным:

Порядок действий - последовательный слева направо

| Сообщение посчитали полезным:

Последние четыре уравнения решаются
при зафиксированном по заданию x88=$2B30B554;

x7c = 0x2c09c132
x88 = 0x2b30b554
x94 = 0x2c7ab644
xa0 = 0x20763f18

или при свободном
x7c = 0x8142580c
x88 = 0x8553eb8a
x94 = 0x28c6427c
xa0 = 0x1c0a4b50

первые четыре значения не находит, возможно из за трактовки знаковое/беззнаковое.

-----
127.0.0.1, sweet 127.0.0.1

| Сообщение посчитали полезным:

x60= 164048D8 x74= 2956AAE9 x78= 2DB15D25 x64= 2E148158
x7c ....xa0 - такие же

а вот это непонятно-
s.add(((((0xD5FA0D83 ^ x60) >> 9) | (((0xD5FA0D83 ^ x60) & 0x1ff) << 23)) ^ x74) + x78 == 0xB268D4F0)
s.add(((((0x677836C3 ^ x60) >> 21) | (((0x677836C3 ^ x60) & 0x1fffff) << 11)) ^ x74) + x78 == 0x0311A5BE)

| Сообщение посчитали полезным:

>>> а вот это непонятно-

через сдвиги реализовано ROR, ROL (bits = 32)
ROR -> (x >> n) | ((x & ((2L**n) - 1)) << (bits - n))
ROL -> (x >> (bits - n)) | ((x & ((2L**(bits - n)) - 1)) << n)

переписал эти 2 уравнения
s.add((RotateRight(0xD5FA0D83 ^ x60, 9L) ^ x74) + x78 == 0xB268D4F0)
s.add((RotateLeft(0x677836C3 ^ x60, 11L) ^ x74) + x78 == 0x0311A5BE)

нашло решение
x60 = 0xc32eec49
x64 = 0xe56e340a
x74 = 0xe0b05d9b
x78 = 0xacad9d05
x7c = 0x2c09c132
x88 = 0x2b30b554
x94 = 0x2c7ab644
xa0 = 0x20763f18

или
x60 = 0xaaa734d0
x64 = 0x3239eff6
x74 = 0x2d7c1987
x78 = 0x2da51dd5
x7c = 0x2c09c132
x88 = 0x2b30b554
x94 = 0x2c7ab644
xa0 = 0x20763f18

или
x60 = 0x888516f2
x64 = 0x1f2adf05
x74 = 0x1a6d0896
x78 = 0xfa51dd5
x7c = 0x2c09c132
x88 = 0x2b30b554
x94 = 0x2c7ab644
xa0 = 0x20763f18

-----
127.0.0.1, sweet 127.0.0.1

| Сообщение посчитали полезным: