Project

General

Profile

Feature #5190

[solver] Поддержка целочисленного переполнения

Added by Igor Melnichenko about 6 years ago. Updated almost 6 years ago.

Status:
Closed
Priority:
High
Assignee:
Andrei Tatarnikov
Category:
-
Target version:
Start date:
08/02/2014
Due date:
% Done:

100%

Estimated time:
Published in build:
141226

Description

При генерации тестов потребовалось выполнить выражение (ADD -1487988057 -1487988057) для типа данных INTEGER. Вылетело следующее исключение:

java.lang.NumberFormatException: For input string: "-2975976114"
at java.lang.NumberFormatException.forInputString(Unknown Source)
at java.lang.Integer.parseInt(Unknown Source)
at java.lang.Integer.valueOf(Unknown Source)
at ru.ispras.fortress.data.DataTypeId$3.valueOf(DataTypeId.java:125)
at ru.ispras.fortress.data.DataType.valueOf(DataType.java:197)
at ru.ispras.fortress.solver.engine.z3.Z3TextSolver.parseVariable(Z3TextSolver.java:212)
at ru.ispras.fortress.solver.engine.z3.Z3TextSolver.tryToParseVariable(Z3TextSolver.java:238)
at ru.ispras.fortress.solver.engine.z3.Z3TextSolver.solve(Z3TextSolver.java:144)
...

History

#1

Updated by Igor Melnichenko about 6 years ago

  • Priority changed from Normal to High
#2

Updated by Andrei Tatarnikov about 6 years ago

А пример кода для воспроизведения можно прислать?

#3

Updated by Igor Melnichenko about 6 years ago

Каюсь, неправильно сформулировал: проблема возникает не на этапе сложения, а на этапе выполнения операции (EQ INTEGER -2975976114)

ConstraintBuilder builder = new ConstraintBuilder();

builder.setName("Arithmetic");
builder.setKind(ConstraintKind.FORMULA_BASED);
builder.setDescription("Arithmetic constraint");

NodeVariable a = new NodeVariable(builder.addVariable("a", DataType.INTEGER));
NodeValue value = new NodeValue(DataType.INTEGER.valueOf("-1487988057", 10));
NodeExpr sum = new NodeExpr(StandardOperation.ADD, value, value);

builder.setInnerRep(new Formulas(new NodeExpr(StandardOperation.EQ, a, sum)));
onstraint c = builder.build();
c.getKind().getDefaultSolverId().getSolver().solve(c);

#4

Updated by Andrei Tatarnikov about 6 years ago

Ошибка происходит при попытке распарсить результат Z3 - число -2975976114. Оно не вмещается в тип Java int, который используется в Fortress для реализации типа SMT-LIB Int.

int x1 = -1487988057;
int y1 = -2975976114; // Не скомпилируется

int x2 = Integer.valueOf("-1487988057");
int y2 = Integer.valueOf("-2975976114"); // Сгенерирует исключение

Чтобы поддерживать числа, выходящие за пределы Java int, нужно менять внутреннюю реализацию DataTypeId.LOGIC_INTEGER (перейти на long или BigInteger). Должен заметить, что тип SMT-LIB Int - безразмерный и не будет переполняться, какие бы числа не складывалить. Если нужно работать с данными фиксированного размера, то нужно использовать битовые вектора.

#5

Updated by Igor Melnichenko about 6 years ago

Мне кажется, имеет смысл добавить переполняемый знаковый целочисленный тип данных, соответствующий int'у из Java и integer'у из Verilog'а, для которого будет выполняться равенство -1487988057 - 1487988057 = 1318991182.

#6

Updated by Andrei Tatarnikov about 6 years ago

В SMT-LIB есть только один тип Int и он работает так:

Код, сгенерированый Fortress:

(declare-const a Int)
(assert  (= a (+ (- 1487988057) (- 1487988057))))
(check-sat)
(get-value ( a))
(get-model)
(exit)

Результат работы Z3:
sat
((a (- 2975976114)))
(model 
  (define-fun a () Int
    (- 2975976114))
)

Int фиксированный длины нужно будет реализовывать как обёртку вокруг BIT_VECTOR. Т.е., что бы для данного ограничения генерировался код

(declare-const a (_ BitVec 32))
(assert  (= a (bvadd (bvneg (_ bv1487988057 32)) (bvneg (_ bv1487988057 32)))))
(check-sat)
(get-value ( a))
(get-model)
(exit)

который даст результат:

sat
((a #x4e9e354e))
(model 
  (define-fun a () (_ BitVec 32)
    #x4e9e354e)
)

#x4e9e354e - это 1318991182

Такое ограничение можно написать самостоятельно. Методы преобразования int в битововый вектор и обратно в классе BitVector есть. Нужно ли это автоматизировать пусть решает Саша.

#7

Updated by Alexander Kamkin about 6 years ago

  • Subject changed from Поддержка целочисленного переполнения to [solver] Поддержка целочисленного переполнения
  1. Игорю предлагаю использовать битовые вектора. Безразмерные целые типы в описании аппаратуры - это странность.
  2. Андрею предлагаю подумать над возможностью использования BigInteger.
#8

Updated by Andrei Tatarnikov about 6 years ago

  • Priority changed from High to Normal

Андрею предлагаю подумать над возможностью использования BigInteger.

Сделаю, по чуть попозже.

#9

Updated by Sergey Smolov almost 6 years ago

  • Priority changed from Normal to High
#10

Updated by Alexander Kamkin almost 6 years ago

Андрей, "чуть попозже" длится 2 месяца.

#11

Updated by Andrei Tatarnikov almost 6 years ago

  • Status changed from New to Resolved
  • % Done changed from 0 to 100

Сделано. См. r645 и r646.

#12

Updated by Andrei Tatarnikov almost 6 years ago

  • Status changed from Resolved to Closed
  • Published in build set to 141226

Also available in: Atom PDF