Open-Source Projects: Issueshttps://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692015-04-09T13:18:19ZOpen-Source Projects
Redmine Fortress - Task #5819 (Closed): Calculator for bit vectorshttps://forge.ispras.ru/issues/58192015-04-09T13:18:19ZAndrei Tatarnikovandrewt@ispras.ru
<p>Subj. must be implemented.</p> Fortress - Bug #5775 (Closed): BitVector.longValue returns incorrect valueshttps://forge.ispras.ru/issues/57752015-03-27T09:00:32ZAndrei Tatarnikovandrewt@ispras.ru
<p>Subject. The code blow fails:</p>
<pre><code class="java syntaxhl" data-language="java"><span class="kd">final</span> <span class="nc">BitVector</span> <span class="n">bv1</span> <span class="o">=</span> <span class="nc">BitVector</span><span class="o">.</span><span class="na">valueOf</span><span class="o">(</span><span class="mh">0x00000000000A0000</span><span class="no">L</span><span class="o">,</span> <span class="mi">64</span><span class="o">);</span>
<span class="nc">System</span><span class="o">.</span><span class="na">out</span><span class="o">.</span><span class="na">println</span><span class="o">(</span><span class="n">bv1</span><span class="o">.</span><span class="na">toHexString</span><span class="o">());</span>
<span class="nc">System</span><span class="o">.</span><span class="na">out</span><span class="o">.</span><span class="na">println</span><span class="o">(</span><span class="nc">Long</span><span class="o">.</span><span class="na">toHexString</span><span class="o">(</span><span class="n">bv1</span><span class="o">.</span><span class="na">longValue</span><span class="o">()));</span>
<span class="n">assertEquals</span><span class="o">(</span><span class="mh">0x00000000000A0000</span><span class="no">L</span><span class="o">,</span> <span class="n">bv1</span><span class="o">.</span><span class="na">longValue</span><span class="o">());</span>
<span class="kd">final</span> <span class="nc">BitVector</span> <span class="n">bv2</span> <span class="o">=</span> <span class="nc">BitVector</span><span class="o">.</span><span class="na">valueOf</span><span class="o">(</span><span class="mh">0xFFFFFFFFFFF5FFFF</span><span class="no">L</span><span class="o">,</span> <span class="mi">64</span><span class="o">);</span>
<span class="nc">System</span><span class="o">.</span><span class="na">out</span><span class="o">.</span><span class="na">println</span><span class="o">(</span><span class="n">bv2</span><span class="o">.</span><span class="na">toHexString</span><span class="o">());</span>
<span class="nc">System</span><span class="o">.</span><span class="na">out</span><span class="o">.</span><span class="na">println</span><span class="o">(</span><span class="nc">Long</span><span class="o">.</span><span class="na">toHexString</span><span class="o">(</span><span class="n">bv2</span><span class="o">.</span><span class="na">longValue</span><span class="o">()));</span>
<span class="n">assertEquals</span><span class="o">(</span><span class="mh">0xFFFFFFFFFFF5FFFF</span><span class="no">L</span><span class="o">,</span> <span class="n">bv2</span><span class="o">.</span><span class="na">longValue</span><span class="o">());</span>
<span class="kd">final</span> <span class="nc">BitVector</span> <span class="n">bv3</span> <span class="o">=</span> <span class="nc">BitVector</span><span class="o">.</span><span class="na">valueOf</span><span class="o">(</span><span class="mh">0xDEADBEEFBAADF00D</span><span class="no">L</span><span class="o">,</span> <span class="mi">64</span><span class="o">);</span>
<span class="nc">System</span><span class="o">.</span><span class="na">out</span><span class="o">.</span><span class="na">println</span><span class="o">(</span><span class="n">bv3</span><span class="o">.</span><span class="na">toHexString</span><span class="o">());</span>
<span class="nc">System</span><span class="o">.</span><span class="na">out</span><span class="o">.</span><span class="na">println</span><span class="o">(</span><span class="nc">Long</span><span class="o">.</span><span class="na">toHexString</span><span class="o">(</span><span class="n">bv3</span><span class="o">.</span><span class="na">longValue</span><span class="o">()));</span>
<span class="n">assertEquals</span><span class="o">(</span><span class="mh">0xDEADBEEFBAADF00D</span><span class="no">L</span><span class="o">,</span> <span class="n">bv3</span><span class="o">.</span><span class="na">longValue</span><span class="o">());</span>
</code></pre> Fortress - Task #5665 (Closed): Support for CVC4https://forge.ispras.ru/issues/56652015-03-03T07:30:20ZAndrei Tatarnikovandrewt@ispras.ru
<p>Implement support for CVC4, a SMT solver that has no limits on its use (see <a class="external" href="http://cvc4.cs.nyu.edu/web/copyright/">http://cvc4.cs.nyu.edu/web/copyright/</a>).</p> Fortress - Bug #5463 (Closed): [S-expr] JavaDoc comments are neededhttps://forge.ispras.ru/issues/54632014-12-04T07:05:12ZAndrei Tatarnikovandrewt@ispras.ru
<p>The ru.ispras.fortress.esexpr package added in revisions r709 и r710 does not contain any description. It is not obvious what purpose it is supposed to serve. Corresponding JavaDoc comments should be included in the source code (including headers with the ISP RAS copyright).</p> Fortress - Bug #5460 (Closed): [project] Get rid of warningshttps://forge.ispras.ru/issues/54602014-12-04T06:55:25ZAndrei Tatarnikovandrewt@ispras.ru
<p>После коммитов r709 и r710 появилась куча Warning'ов. Нужно от них избавиться.</p>
<pre>
Description Resource Path Location Type
The import java.io.IOException is never used ESExpr.java /fortress/src/main/java/ru/ispras/fortress/esexpr line 3 Java Problem
The import java.io.Reader is never used ESExpr.java /fortress/src/main/java/ru/ispras/fortress/esexpr line 4 Java Problem
The import java.io.StreamTokenizer is never used ESExpr.java /fortress/src/main/java/ru/ispras/fortress/esexpr line 5 Java Problem
The import java.io.StringReader is never used ESExpr.java /fortress/src/main/java/ru/ispras/fortress/esexpr line 6 Java Problem
The import java.util.ArrayList is never used Z3TextSolver.java /fortress/src/main/java/ru/ispras/fortress/solver/engine/z3 line 28 Java Problem
The import java.util.List is never used Z3TextSolver.java /fortress/src/main/java/ru/ispras/fortress/solver/engine/z3 line 27 Java Problem
The method tryToParseError(String, SolverResultBuilder) from the type Z3TextSolver is never used locally Z3TextSolver.java /fortress/src/main/java/ru/ispras/fortress/solver/engine/z3 line 245 Java Problem
The method tryToParseStatus(String, SolverResultBuilder) from the type Z3TextSolver is never used locally Z3TextSolver.java /fortress/src/main/java/ru/ispras/fortress/solver/engine/z3 line 227 Java Problem
The method tryToParseVariable(String, Variable, SolverResultBuilder, Map<String,Variable>) from the type Z3TextSolver is never used locally Z3TextSolver.java /fortress/src/main/java/ru/ispras/fortress/solver/engine/z3 line 302 Java Problem
The value of the local variable vi is not used Z3TextSolver.java /fortress/src/main/java/ru/ispras/fortress/solver/engine/z3 line 123 Java Problem
</pre> Fortress - Bug #5217 (Closed): [expression] NodeBinding: hashCode and equals must be implementedhttps://forge.ispras.ru/issues/52172014-08-23T09:15:42ZAndrei Tatarnikovandrewt@ispras.ru
<p>У класса NodeBinding должны быть определены методы hashCode и equals, как это сделано в других классах Node.</p> Fortress - Task #5177 (Closed): [solver] Implement function templateshttps://forge.ispras.ru/issues/51772014-07-31T07:44:00ZAndrei Tatarnikovandrewt@ispras.ru
<p>Реализовать возможность расширять фонкциональность солвера операциями, основанными на шаблонах функций (Описывают семейство похожих функций, опрерирующих разными типами данных. Например, битовыми векторами разной длины). Солвер должен генерировать нужную функцию из семейства, описанного шаблоном, в зависимости от типа операндов.</p> Fortress - Task #5176 (Closed): [expression] Possibility to calculate the expression typehttps://forge.ispras.ru/issues/51762014-07-31T07:35:32ZAndrei Tatarnikovandrewt@ispras.ru
<p>Необходимо реализовать во всех подклассах Node метод getDataType для вычисления типа данных подвыражения:</p>
<pre>
public DataType getDataType()
</pre> Fortress - Task #4693 (Closed): [data] Реализации операций над битовыми векторами (BitVector)https://forge.ispras.ru/issues/46932014-02-13T11:58:00ZAndrei Tatarnikovandrewt@ispras.ru
<p>Необходима реализация стандартного набора операций над битовыми векторами (BitVector) включая побитовые операции, логические операции и часто используемые арифметические операции. Подобная реализация существует в виде наброска в Model API MicroTESK. Ещё нужно перенести в Fortress, унифицировать, расширить и создать для неё модульные тесты.</p> MicroTESK - Task #4061 (New): Support for endiannesshttps://forge.ispras.ru/issues/40612013-04-03T09:36:03ZAndrei Tatarnikovandrewt@ispras.ru
<p>Сейчас порядок байт не учитывается при моделировании. Он принимается за little-endian по умолчанию.</p>
<p>В моделях, предоставленных IIT Kanpur порядок байт задаётся ключом byte_order. Это выглядит так:</p>
<p>let byte_order = "little" <br />let byte_order = "big"</p>
<p>Нам тоже нужно учитывать порядок байт при моделировании модели.</p> MicroTESK - Bug #4015 (Closed): [translator] Shift and Rotate operations: negative distancehttps://forge.ispras.ru/issues/40152013-03-17T15:00:02ZAndrei Tatarnikovandrewt@ispras.ru
<p>Для данных, моделируемых через RawData, не будут работать операторы сдвига и поворота, если второй операнд (на сколько сдвигаем/поворачиваем) будет отрицательным.</p> MicroTESK - Bug #4014 (Closed): Concatenation in left hand side expressionshttps://forge.ispras.ru/issues/40142013-03-17T14:41:39ZAndrei Tatarnikovandrewt@ispras.ru
<p>Логика выражений типа M [0] :: M [1] = R [4] некорректна. Она должна означать:</p>
<p>M [0] = R [4];<br />M [1] = R [4]</p>
<p>Вот что написано в драфте Фредерикса:</p>
<p><<<<<<<<<<<<<<<<<<<<<<<br />4.10 Concatenation of Values</p>
<p>The :: operator allows the concatenation of arbitrary expressions; it is de ned on the left side of<br />assignments, too (if the expressions denote memory locations only, of course). For example,<br />M [0] :: M [1] = R [4]<br />assigns the value of R [4] to the locations M [0] and M [1]. The order is the same as used in sequences<br />of locations, i.e., essentially unde ned.</p>
<blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote><blockquote>
</blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote>
<p>Нужно найти решение.</p> MicroTESK - Bug #3996 (Closed): [translator] Support for long types (64-bit) in expressionshttps://forge.ispras.ru/issues/39962013-03-11T09:47:24ZAndrei Tatarnikovandrewt@ispras.ru
<p>Сейчас не поддерживаются числа больше 32-х бит (int). При трансляции встречаются выражения, использующие 64-битные константы и транслирующиеся напрямую в Java код (без упаковки в классы Data/RawData). Такие выражения мы не можем оттраслировать т.к. не используем тип long при трансляции в Java. Нужно его использовать.</p>
<p>if (sum < 0xffffffff80000001) then <br /> GPR[rd] = 0x80000001;<br /> CPSR<27..27> = 1;<br />else<br /> GPR[rd] = op1 - op2;<br />endif;</p> MicroTESK - Bug #3995 (Closed): [translator] Support for bitfields using non-constant expressionshttps://forge.ispras.ru/issues/39952013-03-11T09:39:51ZAndrei Tatarnikovandrewt@ispras.ru
<p>Для правильной индентификации типов при обращении к битовым полям вычисляется размер поля (на этапе трансляции).<br />Индексные выражения, как правило, - статически вычисляемые константные выражения. Однако, возможны следующие варианты:</p>
<p>shifter_carry_out = GPR[r]<amount-1..amount-1>;</p>
<p>Такой код не будет транслироваться т.к. amount - не константа. Однако, размер поля можно посчтитать и видно, что он будет равен 1.<br />В модели ARM встречается несколько подобных симметричных конструкций. Для них можно и НУЖНО вычислять размер поля.</p> MicroTESK - Task #3988 (Rejected): Support for forward definitions in the nML translatorhttps://forge.ispras.ru/issues/39882013-03-04T09:18:49ZAndrei Tatarnikovandrewt@ispras.ru
<p>Сейчас forward definitions не поддерживаются в Sim-nML трансляторе. Т.е. если код ссылается на какой-либо внешний элемент,<br />то он должен быть определён ранее в коде. Например, следующий код не будет транслироваться т.к. OR-rule setU ссылается на элементы setUon и setUoff, которые ещё не определены:</p>
<p>mode setU = setUon | setUoff</p>
<p>mode setUon() = 0b1<br /> syntax = "+" <br /> image = "1" <br /> action = {<br /> }</p>
<p>mode setUoff() = 0b0<br /> syntax = "-" <br /> image = "0" <br /> action = {<br /> }</p>