Open-Source Projects: Issueshttps://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692020-06-08T13:56:16ZOpen-Source Projects
Redmine Fortress - Bug #10370 (Closed): class ru.ispras.fortress.solver.constraint.Formulas cannot be ca...https://forge.ispras.ru/issues/103702020-06-08T13:56:16ZSergey Smolovsmolov@ispras.ru
<p>68 test cases fall with the stack trace:<br /><pre>
java.lang.ClassCastException: class ru.ispras.fortress.solver.constraint.Formulas cannot be cast to class ru.ispras.fortress.solver.constraint.Sat4jFormula (ru.ispras.fortress.solver.constraint.Formulas and ru.ispras.fortress.solver.constraint.Sat4jFormula are in unnamed module of loader 'app')
at ru.ispras.fortress.solver.engine.sat.Sat4jSolver.solve(Sat4jSolver.java:74)
at ru.ispras.fortress.solver.constraint.GenericSolverTestBase.solveAndCheckResult(GenericSolverTestBase.java:167)
at ru.ispras.fortress.solver.constraint.GenericSolverTestBase.runSolverTests(GenericSolverTestBase.java:115)
</pre></p> Fortress - Bug #8573 (Closed): missing javadochttps://forge.ispras.ru/issues/85732017-11-14T12:59:32ZSergey Smolovsmolov@ispras.ru
<p>When running "./gradlew assemble" I've got the following:</p>
<pre>
/home/ssedai/projects/fortress.git/src/main/java/ru/ispras/fortress/expression/ExprUtils.java:101: warning - Tag @link: can't find Kind in ru.ispras.fortress.expression.Node
/home/ssedai/projects/fortress.git/src/main/java/ru/ispras/fortress/expression/Node.java:41: warning - Tag @link: can't find Kind in ru.ispras.fortress.expression.Node
/home/ssedai/projects/fortress.git/src/main/java/ru/ispras/fortress/transformer/Reducer.java:172: warning - @param argument "engine" is not a parameter name.
/home/ssedai/projects/fortress.git/src/main/java/ru/ispras/fortress/transformer/ValueProvider.java:34: warning - @param argument "variableName" is not a parameter name.
</pre> Fortress - Bug #7557 (Closed): ConstCastTestCase: java.lang.AssertionError: Calculator failed to ...https://forge.ispras.ru/issues/75572016-09-07T16:54:35ZSergey Smolovsmolov@ispras.ru
<p>Probable bug in calculator, because ConstCastTestCase falls upon calling it.</p>
<pre>
Calculator failed to substitute result:
(AND (EQ (POWER y 3) z))
-> (LET () (AND (EQ (POWER y 3) z)))
-> (AND (EQ (POWER y 3) z))
-> (AND (EQ (POWER y 3) z))
java.lang.AssertionError: Calculator failed to substitute result:
(AND (EQ (POWER y 3) z))
-> (LET () (AND (EQ (POWER y 3) z)))
-> (AND (EQ (POWER y 3) z))
-> (AND (EQ (POWER y 3) z))
at org.junit.Assert.fail(Assert.java:88)
at org.junit.Assert.assertTrue(Assert.java:41)
at ru.ispras.fortress.solver.constraint.GenericSolverTestBase.checkResult(GenericSolverTestBase.java:210)
at ru.ispras.fortress.solver.constraint.GenericSolverTestBase.solveAndCheckResult(GenericSolverTestBase.java:174)
at ru.ispras.fortress.solver.constraint.GenericSolverTestBase.runSolverTests(GenericSolverTestBase.java:110)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
</pre> Fortress - Bug #7555 (Closed): unable to create constraint-related jUnit tests including unused v...https://forge.ispras.ru/issues/75552016-09-07T14:50:33ZSergey Smolovsmolov@ispras.ru
<p>When creating a jUnit constraint-related test case I've found that the test fails because of unused variable inside my constraint.</p>
<p>More precisely, the problem is in this code fragment of <code>GenericSolverTestBase</code> class:</p>
<pre><code class="java syntaxhl" data-language="java"> <span class="kd">private</span> <span class="kd">static</span> <span class="kt">void</span> <span class="nf">checkResult</span><span class="o">(</span><span class="nc">CalculatorEngine</span> <span class="n">calculator</span><span class="o">,</span> <span class="nc">Constraint</span> <span class="n">constraint</span><span class="o">,</span> <span class="nc">SolverResult</span> <span class="n">result</span><span class="o">)</span> <span class="o">{</span>
<span class="kd">final</span> <span class="nc">Formulas</span> <span class="n">formulas</span> <span class="o">=</span> <span class="o">(</span><span class="nc">Formulas</span><span class="o">)</span> <span class="n">constraint</span><span class="o">.</span><span class="na">getInnerRep</span><span class="o">();</span>
<span class="kd">final</span> <span class="nc">Collection</span><span class="o"><</span><span class="nc">NodeVariable</span><span class="o">></span> <span class="n">variables</span> <span class="o">=</span>
<span class="nc">ExprUtils</span><span class="o">.</span><span class="na">getVariables</span><span class="o">(</span><span class="n">formulas</span><span class="o">.</span><span class="na">exprs</span><span class="o">());</span>
<span class="kd">final</span> <span class="nc">Map</span><span class="o"><</span><span class="nc">String</span><span class="o">,</span> <span class="nc">NodeVariable</span><span class="o">></span> <span class="n">variableMap</span> <span class="o">=</span> <span class="k">new</span> <span class="nc">HashMap</span><span class="o"><>(</span><span class="n">variables</span><span class="o">.</span><span class="na">size</span><span class="o">());</span>
<span class="k">for</span> <span class="o">(</span><span class="nc">NodeVariable</span> <span class="n">node</span> <span class="o">:</span> <span class="n">variables</span><span class="o">)</span> <span class="o">{</span>
<span class="n">variableMap</span><span class="o">.</span><span class="na">put</span><span class="o">(</span><span class="n">node</span><span class="o">.</span><span class="na">getName</span><span class="o">(),</span> <span class="n">node</span><span class="o">);</span>
<span class="o">}</span>
<span class="kd">final</span> <span class="nc">List</span><span class="o"><</span><span class="nc">NodeBinding</span><span class="o">.</span><span class="na">BoundVariable</span><span class="o">></span> <span class="n">bindings</span> <span class="o">=</span>
<span class="k">new</span> <span class="nc">ArrayList</span><span class="o"><>(</span><span class="n">result</span><span class="o">.</span><span class="na">getVariables</span><span class="o">().</span><span class="na">size</span><span class="o">());</span>
<span class="k">for</span> <span class="o">(</span><span class="nc">Variable</span> <span class="kt">var</span> <span class="o">:</span> <span class="n">result</span><span class="o">.</span><span class="na">getVariables</span><span class="o">())</span> <span class="o">{</span>
<span class="kd">final</span> <span class="nc">NodeVariable</span> <span class="n">node</span> <span class="o">=</span> <span class="n">variableMap</span><span class="o">.</span><span class="na">get</span><span class="o">(</span><span class="kt">var</span><span class="o">.</span><span class="na">getName</span><span class="o">());</span>
<span class="kd">final</span> <span class="nc">NodeValue</span> <span class="n">value</span> <span class="o">=</span> <span class="k">new</span> <span class="nc">NodeValue</span><span class="o">(</span><span class="kt">var</span><span class="o">.</span><span class="na">getData</span><span class="o">());</span>
<span class="n">bindings</span><span class="o">.</span><span class="na">add</span><span class="o">(</span><span class="nc">NodeBinding</span><span class="o">.</span><span class="na">bindVariable</span><span class="o">(</span><span class="n">node</span><span class="o">,</span> <span class="n">value</span><span class="o">));</span>
<span class="o">}</span>
</code></pre>
<p>Sizes of <code>variables</code> and <code>bindings</code> seem to be different.</p>
<p>I've also implemented a small test case called <code>UnusedVariableTestCase</code> that illustrates the problem (r1298).</p> Fortress - Bug #6352 (Closed): Transformer.standardize returns 'false' on (AND (EQ a 00) (NOT(EQ ...https://forge.ispras.ru/issues/63522015-10-15T15:10:10ZSergey Smolovsmolov@ispras.ru
<p>The <code>Transformer.standardize</code> method works incorrectly: on (AND (EQ a 00) (NOT (EQ a b 00))) constraint (where a and b are BIT_VECTOR(2)) it returns 'false'.</p>
<p>Use the <code>equalNotEqual</code> test at Transformer jUnit testcase to check that this bug is fixed.</p> Fortress - Bug #5461 (Closed): [arrays] Insufficient arrays supporthttps://forge.ispras.ru/issues/54612014-12-04T06:57:34ZSergey Smolovsmolov@ispras.ru
<p>Реализованная в проекте поддержка массивов имеет два существенных ограничения.</p>
<p>1) radix элементов массива должен совпадать с radix индексов;</p>
<p>2) метод getTypeRadix для MAP всегда возвращает 10.</p>
<p>Эти ограничения, в частности, не позволяют создавать массивы битовых векторов (очень распространенный объект в HDL-описаниях), а также получить для них radix элементов массива.</p>
<p>Проблема 1) частично решена ревизией r715 (теперь все массивы имеют radix=10 для индексов - см. блок TODO), что позволяет успешно обрабатывать код HDL-описаний. Если решение устраивает - можно блок TODO удалить. Если есть необходимость создавать массивы, у которых radix индексов не всегда равен 10, то нужно эту возможность учитывать.</p> Fortress - Bug #5453 (Closed): [arrays] Unexpected solver output: " (INSTQUEUE ((as const (Array ...https://forge.ispras.ru/issues/54532014-11-27T15:46:10ZSergey Smolovsmolov@ispras.ru
<p>При анализе HDL-описаний инструментом Retrascope иногда возникает ошибка со следующим логом:</p>
<p>[log]</p>
<p>java.lang.AssertionError: Unexpected solver output: " (INSTQUEUE ((as const (Array Int Int)) 0))" <br /> at ru.ispras.fortress.solver.engine.z3.Z3TextSolver.solve(Z3TextSolver.java:136)<br /> at ru.ispras.fortress.solver.constraint.ConstraintUtils.solve(ConstraintUtils.java:69)<br /> at ru.ispras.fortress.expression.ExprUtils.isSAT(ExprUtils.java:303)<br /> at ru.ispras.fortress.expression.ExprUtils.areCompatible(ExprUtils.java:288)</p>
<p>[/log]</p>
<p>Ошибка плавающая, т.е. пока не удалось так подобрать аргументы программы, чтобы сделать её воспроизводимой.</p> Fortress - Bug #5425 (Closed): [expression] java.lang.IllegalArgumentException: Expression is not...https://forge.ispras.ru/issues/54252014-11-12T20:29:04ZSergey Smolovsmolov@ispras.ru
<p>Дано: объект NodeOperation вида (BVEXTRACT D_IN 0 0), где D_IN - объект NodeVariable типа BIT_VECTOR (длины 9).</p>
<p>При попытке создать из него и прочих NodeOperation конъюнкцию с помощью метода ExprUtils.getConjunction возникает ошибка:</p>
<p>2014.11.12 23:21:04.076. ERROR: The exception has been encountered: java.lang.IllegalArgumentException: Expression is not a condition: (BVEXTRACT D_IN 0 0)<br /> at ru.ispras.fortress.expression.ExprUtils.checkAllConditions(ExprUtils.java:378)<br /> at ru.ispras.fortress.expression.ExprUtils.getConjunction(ExprUtils.java:189)<br />...</p>
<p>Причина ошибки состоит в том, что для данного выражения метод getDataType() возвращает UNKNOWN, хотя тут чистой воды BOOLEAN.</p> Fortress - Bug #5401 (Closed): error at ru/ispras/fortress/solver/constraint/ArrayTestCase.javahttps://forge.ispras.ru/issues/54012014-10-30T14:05:07ZSergey Smolovsmolov@ispras.ru
<p>Приведенный в тесте ru/ispras/fortress/solver/constraint/ArrayTestCase.java пример на языке SMT-LIB не выполняется решателем Z3:</p>
<p>[log]</p>
<p><abbr title="5, 13">Z3</abbr>: ERROR: unexpected character sat ((a (_ as-array k!1))) ((v (_ as-array k!0))) (model (define-fun v () (Array Int Int) (_ as-array k!0)) (define-fun a () (Array Int Int) (_ as-array k!1)) (define-fun k!0 ((x!1 Int)) Int 0) (define-fun k!1 ((x!1 Int)) Int (ite (= x!1 37) 37 0)) )</p>
<p>[/log]</p>
<p>Код на SMT-LIB:</p>
<p>[code]</p>
<p>(define-sort ARRAY_TYPE () (Array Int Int))<br />(declare-fun a () ARRAY_TYPE)<br />(declare-fun v () ARRAY_TYPE)<br />(assert (= a (store v 37 37)))<br />(assert (= a '((37 37))))<br />(check-sat)<br />(get-value (a))<br />(get-value (v))<br />(get-model)<br />(exit)</p>
<p>[/code]</p> Fortress - Bug #5162 (Closed): [solver] ReductionCustomOperationsTestCase -> java.lang.AssertionE...https://forge.ispras.ru/issues/51622014-07-28T12:15:03ZSergey Smolovsmolov@ispras.ru
<p>Запускаю тест ReductionCustomOperationsTestCase, падает с ошибкой. Лог следующий:</p>
<p><code>java.lang.AssertionError<br /> at ru.ispras.fortress.solver.engine.z3.FunctionDefinitionBuilders.beginCallTree(SMTTextBuilder.java:308)<br /> at ru.ispras.fortress.solver.engine.z3.SMTTextBuilder.addFunctionDefinition(SMTTextBuilder.java:163)<br /> at ru.ispras.fortress.solver.engine.z3.SMTTextBuilder.onExprBegin(SMTTextBuilder.java:203)<br /> at ru.ispras.fortress.expression.ExprTreeWalker.visitExpr(ExprTreeWalker.java:136)<br /> at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:122)<br /> at ru.ispras.fortress.expression.ExprTreeWalker.visitExpr(ExprTreeWalker.java:142)<br /> at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:122)<br /> at ru.ispras.fortress.expression.ExprTreeWalker.visit(ExprTreeWalker.java:93)<br /> at ru.ispras.fortress.expression.ExprTreeWalker.visit(ExprTreeWalker.java:72)<br /> at ru.ispras.fortress.solver.engine.z3.Z3TextSolver.solve(Z3TextSolver.java:119)<br /> at ru.ispras.fortress.solver.GenericSolverTestBase.runSolverTests(GenericSolverTestBase.java:87)</code></p> C++TESK Testing ToolKit - Bug #4005 (Rejected): удалить пустой READMEhttps://forge.ispras.ru/issues/40052013-03-15T14:17:10ZSergey Smolovsmolov@ispras.ru
<p>Что делает пустой файл README в trunk основного проекта?</p> C++TESK Testing ToolKit - Bug #4004 (Closed): Из build'а пропал скрипт install-eclipse-plugin.shhttps://forge.ispras.ru/issues/40042013-03-14T17:36:57ZSergey Smolovsmolov@ispras.ru
<p>Т.е. в trunk проекта он есть, а в сборке не присутствует. <br />Без данного скрипта пропадает возможность установить C++TesK Eclipse plug-in из командной строки.</p>
<p>Просьба починить.</p> C++TESK Testing ToolKit - Bug #3805 (Closed): Ошибка в QuickReferencehttps://forge.ispras.ru/issues/38052012-12-18T08:19:48ZSergey Smolovsmolov@ispras.ru
<p>Файл C++TESK.QuickReference.ru.pdf, страница 10:</p>
<p>"CPPTESK_CONT_CAST_MESSAGE(класс_сообщения)."</p>
<p>Видимо, нужно исправить на</p>
<p>"CPPTESK_CONST_CAST_MESSAGE(класс_сообщения)."</p> C++TESK Testing ToolKit - Bug #3590 (Closed): C++TesK installation fails on OpenSUSE 12.2 x64https://forge.ispras.ru/issues/35902012-10-15T11:18:40ZSergey Smolovsmolov@ispras.ru
<p>Попробовал установить subj на OpenSUSE 12.2 x64. Системные требования были удовлетворены (в соответствии с C++TESK.InstallationGuide.ru.pdf), скрипт установки запускался с опцией --force-install-veritool (Veritool и Icarus Verilog предварительно установлены не были, подключение к сети, естественно, есть).</p>
<p>По-видимому, Icarus Verilog установился корректно, а Veritool - нет.</p>
<p>Лог установочного скрипта в аттаче.</p> CTESK - Bug #2494 (New): warning at build loghttps://forge.ispras.ru/issues/24942012-02-24T06:40:28ZSergey Smolovsmolov@ispras.ru
<p>При сборке возникает следующее предупреждение:</p>
<p>gcc -I. -g -ggdb -O0 -fno-inline -D_GLIBCXX_DEBUG -O -DATL_CLONE_DISABLE -DUSE_FOPEN64 -c c_tracer/c_tracer.c -o c_tracer/c_tracer.o<br />c_tracer/c_tracer.c: In function ‘addTraceToFile’:<br />c_tracer/c_tracer.c:117:7: warning: assignment makes pointer from integer without a cast</p>
<p>Сборка завершается корректно, так что это скорее небольшой досадный недочет.</p>