https://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692014-08-05T12:45:36ZOpen-Source ProjectsFortress - Feature #5190: [solver] Поддержка целочисленного переполненияhttps://forge.ispras.ru/issues/5190?journal_id=203552014-08-05T12:45:36ZIgor Melnichenkosuomi-47@ya.ru
<ul><li><strong>Priority</strong> changed from <i>Normal</i> to <i>High</i></li></ul> Fortress - Feature #5190: [solver] Поддержка целочисленного переполненияhttps://forge.ispras.ru/issues/5190?journal_id=203562014-08-05T12:47:51ZAndrei Tatarnikovandrewt@ispras.ru
<ul></ul><p>А пример кода для воспроизведения можно прислать?</p> Fortress - Feature #5190: [solver] Поддержка целочисленного переполненияhttps://forge.ispras.ru/issues/5190?journal_id=203572014-08-05T12:57:19ZIgor Melnichenkosuomi-47@ya.ru
<ul></ul><p>Каюсь, неправильно сформулировал: проблема возникает не на этапе сложения, а на этапе выполнения операции (EQ INTEGER -2975976114)</p>
<p>ConstraintBuilder builder = new ConstraintBuilder();</p>
<p>builder.setName("Arithmetic");<br />builder.setKind(ConstraintKind.FORMULA_BASED);<br />builder.setDescription("Arithmetic constraint");</p>
<p>NodeVariable a = new NodeVariable(builder.addVariable("a", DataType.INTEGER));<br />NodeValue value = new NodeValue(DataType.INTEGER.valueOf("-1487988057", 10));<br />NodeExpr sum = new NodeExpr(StandardOperation.ADD, value, value);</p>
<p>builder.setInnerRep(new Formulas(new NodeExpr(StandardOperation.EQ, a, sum)));<br />onstraint c = builder.build();<br />c.getKind().getDefaultSolverId().getSolver().solve(c);</p> Fortress - Feature #5190: [solver] Поддержка целочисленного переполненияhttps://forge.ispras.ru/issues/5190?journal_id=203582014-08-05T13:26:02ZAndrei Tatarnikovandrewt@ispras.ru
<ul></ul><p>Ошибка происходит при попытке распарсить результат Z3 - число -2975976114. Оно не вмещается в тип Java int, который используется в Fortress для реализации типа SMT-LIB Int.</p>
<pre><code class="java syntaxhl" data-language="java"><span class="kt">int</span> <span class="n">x1</span> <span class="o">=</span> <span class="o">-</span><span class="mi">1487988057</span><span class="o">;</span>
<span class="kt">int</span> <span class="n">y1</span> <span class="o">=</span> <span class="o">-</span><span class="mi">2975976114</span><span class="o">;</span> <span class="c1">// Не скомпилируется</span>
<span class="kt">int</span> <span class="n">x2</span> <span class="o">=</span> <span class="nc">Integer</span><span class="o">.</span><span class="na">valueOf</span><span class="o">(</span><span class="s">"-1487988057"</span><span class="o">);</span>
<span class="kt">int</span> <span class="n">y2</span> <span class="o">=</span> <span class="nc">Integer</span><span class="o">.</span><span class="na">valueOf</span><span class="o">(</span><span class="s">"-2975976114"</span><span class="o">);</span> <span class="c1">// Сгенерирует исключение</span>
</pre></code>
<p>Чтобы поддерживать числа, выходящие за пределы Java int, нужно менять внутреннюю реализацию DataTypeId.LOGIC_INTEGER (перейти на long или BigInteger). Должен заметить, что тип SMT-LIB Int - безразмерный и не будет переполняться, какие бы числа не складывалить. Если нужно работать с данными фиксированного размера, то нужно использовать битовые вектора.</p></pre> Fortress - Feature #5190: [solver] Поддержка целочисленного переполненияhttps://forge.ispras.ru/issues/5190?journal_id=203592014-08-05T13:46:50ZIgor Melnichenkosuomi-47@ya.ru
<ul></ul><p>Мне кажется, имеет смысл добавить переполняемый знаковый целочисленный тип данных, соответствующий int'у из Java и integer'у из Verilog'а, для которого будет выполняться равенство -1487988057 - 1487988057 = 1318991182.</p> Fortress - Feature #5190: [solver] Поддержка целочисленного переполненияhttps://forge.ispras.ru/issues/5190?journal_id=203602014-08-05T14:11:37ZAndrei Tatarnikovandrewt@ispras.ru
<ul></ul><p>В SMT-LIB есть только один тип Int и он работает так:</p>
<p>Код, сгенерированый Fortress:<br /><pre><code>(declare-const a Int)
(assert (= a (+ (- 1487988057) (- 1487988057))))
(check-sat)
(get-value ( a))
(get-model)
(exit)</code></pre><br />Результат работы Z3:<br /><pre><code>sat
((a (- 2975976114)))
(model
(define-fun a () Int
(- 2975976114))
)</code></pre></p>
<p>Int фиксированный длины нужно будет реализовывать как обёртку вокруг BIT_VECTOR. Т.е., что бы для данного ограничения генерировался код</p>
<pre><code>(declare-const a (_ BitVec 32))
(assert (= a (bvadd (bvneg (_ bv1487988057 32)) (bvneg (_ bv1487988057 32)))))
(check-sat)
(get-value ( a))
(get-model)
(exit)</code></pre>
<p>который даст результат:<br /><pre><code>sat
((a #x4e9e354e))
(model
(define-fun a () (_ BitVec 32)
#x4e9e354e)
)
</code></pre></p>
<p>#x4e9e354e - это 1318991182</p>
<p>Такое ограничение можно написать самостоятельно. Методы преобразования int в битововый вектор и обратно в классе BitVector есть. Нужно ли это автоматизировать пусть решает Саша.</p> Fortress - Feature #5190: [solver] Поддержка целочисленного переполненияhttps://forge.ispras.ru/issues/5190?journal_id=204142014-08-21T06:27:25ZAlexander Kamkinaskamkin@gmail.com
<ul><li><strong>Subject</strong> changed from <i>Поддержка целочисленного переполнения</i> to <i>[solver] Поддержка целочисленного переполнения</i></li></ul><ol>
<li>Игорю предлагаю использовать битовые вектора. Безразмерные целые типы в описании аппаратуры - это странность.</li>
<li>Андрею предлагаю подумать над возможностью использования <code>BigInteger</code>.</li>
</ol> Fortress - Feature #5190: [solver] Поддержка целочисленного переполненияhttps://forge.ispras.ru/issues/5190?journal_id=204522014-08-25T11:34:52ZAndrei Tatarnikovandrewt@ispras.ru
<ul><li><strong>Priority</strong> changed from <i>High</i> to <i>Normal</i></li></ul><blockquote>
<p>Андрею предлагаю подумать над возможностью использования BigInteger.</p>
</blockquote>
<p>Сделаю, по чуть попозже.</p> Fortress - Feature #5190: [solver] Поддержка целочисленного переполненияhttps://forge.ispras.ru/issues/5190?journal_id=210132014-10-31T14:54:08ZSergey Smolovsmolov@ispras.ru
<ul><li><strong>Priority</strong> changed from <i>Normal</i> to <i>High</i></li></ul> Fortress - Feature #5190: [solver] Поддержка целочисленного переполненияhttps://forge.ispras.ru/issues/5190?journal_id=210172014-11-01T18:31:26ZAlexander Kamkinaskamkin@gmail.com
<ul></ul><p>Андрей, "чуть попозже" длится 2 месяца.</p> Fortress - Feature #5190: [solver] Поддержка целочисленного переполненияhttps://forge.ispras.ru/issues/5190?journal_id=210222014-11-05T14:51:57ZAndrei Tatarnikovandrewt@ispras.ru
<ul><li><strong>Status</strong> changed from <i>New</i> to <i>Resolved</i></li><li><strong>% Done</strong> changed from <i>0</i> to <i>100</i></li></ul><p>Сделано. См. r645 и r646.</p> Fortress - Feature #5190: [solver] Поддержка целочисленного переполненияhttps://forge.ispras.ru/issues/5190?journal_id=216042014-12-26T16:23:21ZAndrei Tatarnikovandrewt@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Resolved</i> to <i>Closed</i></li><li><strong>Published in build</strong> set to <i>141226</i></li></ul>