Open-Source Projects: Issueshttps://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692017-04-13T10:48:57ZOpen-Source Projects
Redmine MicroTESK - Bug #8060 (New): Attributes image and syntax and static instanceshttps://forge.ispras.ru/issues/80602017-04-13T10:48:57ZAndrei Tatarnikovandrewt@ispras.ru
<p>The following construct is illegal:<br /><pre>image = slt(rd, X(0), rs).image</pre><br />nML translator forces to write it like this:<br /><pre>image = format("%s", slt(rd, X(0), rs).image)</pre><br />This is inconvenient and redundant.</p>
<p>Constructs like in the first example must be supported.</p> MicroTESK - Bug #7251 (Rejected): A warning or error is needed when a value is truncatedhttps://forge.ispras.ru/issues/72512016-05-25T10:30:24ZAndrei Tatarnikovandrewt@ispras.ru
<p>Constant expressions are cast to nML types depending of the context. For example, in expressions of kind "<code>VARIABLE operator CONSTANT</code>", CONSTANT is cast to the type of VARIABLE. If CONSTANT is larger than can be represented by the type, its higher bits are truncated. This can lead to unexpected results. For this reason, in such situations a warning or an error must be generated.</p>
<p>Example:</p>
<code>In "x + 32" where x has type card(5), 32 gets truncated to 0.</code> MicroTESK - Bug #6380 (New): Possibility to specify initial values for registershttps://forge.ispras.ru/issues/63802015-10-29T12:24:31ZAndrei Tatarnikovandrewt@ispras.ru
<p>Possibility to specify initial values for registers must be provided in nML:</p>
<pre>reg R[1, card(32)] initial = 100</pre> 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> MicroTESK - Bug #5708 (Closed): MicroTESK build fails: SsaAssembler - symbol Changes is not definedhttps://forge.ispras.ru/issues/57082015-03-13T11:06:24ZAndrei Tatarnikovandrewt@ispras.ru
<p>Artem, please add the Changes class to the SVN source code base. Now the build fails:</p>
<pre>
javac.core:
[mkdir] Created dir: /srv/hudson/jobs/MicroTESK/workspace/bin/microtesk
[javac] Compiling 272 source files to /srv/hudson/jobs/MicroTESK/workspace/bin/microtesk
[javac] /srv/hudson/jobs/MicroTESK/workspace/src/main/java/core/ru/ispras/microtesk/translator/simnml/coverage/ssa/SsaAssembler.java:42: error: cannot find symbol
[javac] Deque<Changes> changesStack;
[javac] ^
[javac] symbol: class Changes
[javac] location: class SsaAssembler
[javac] /srv/hudson/jobs/MicroTESK/workspace/src/main/java/core/ru/ispras/microtesk/translator/simnml/coverage/ssa/SsaAssembler.java:43: error: cannot find symbol
[javac] Changes changes;
[javac] ^
[javac] symbol: class Changes
[javac] location: class SsaAssembler
[javac] /srv/hudson/jobs/MicroTESK/workspace/src/main/java/core/ru/ispras/microtesk/translator/simnml/coverage/ssa/SsaAssembler.java:169: error: cannot find symbol
[javac] private static void join(Changes repo, Collection<GuardedBlock> blocks, Collection<Changes> containers, NodeTransformer xform) {
[javac] ^
[javac] symbol: class Changes
[javac] location: class SsaAssembler
[javac] /srv/hudson/jobs/MicroTESK/workspace/src/main/java/core/ru/ispras/microtesk/translator/simnml/coverage/ssa/SsaAssembler.java:169: error: cannot find symbol
[javac] private static void join(Changes repo, Collection<GuardedBlock> blocks, Collection<Changes> containers, NodeTransformer xform) {
[javac] ^
[javac] symbol: class Changes
[javac] location: class SsaAssembler
[javac] /srv/hudson/jobs/MicroTESK/workspace/src/main/java/core/ru/ispras/microtesk/translator/simnml/coverage/ssa/SsaAssembler.java:185: error: cannot find symbol
[javac] private static Node getJointFallback(String name, Changes master, Changes branch) {
[javac] ^
[javac] symbol: class Changes
[javac] location: class SsaAssembler
[javac] /srv/hudson/jobs/MicroTESK/workspace/src/main/java/core/ru/ispras/microtesk/translator/simnml/coverage/ssa/SsaAssembler.java:185: error: cannot find symbol
[javac] private static Node getJointFallback(String name, Changes master, Changes branch) {
[javac] ^
[javac] symbol: class Changes
[javac] location: class SsaAssembler
[javac] /srv/hudson/jobs/MicroTESK/workspace/src/main/java/core/ru/ispras/microtesk/translator/simnml/coverage/ssa/SsaAssembler.java:62: error: unexpected type
[javac] this.changesStack = new ArrayDeque<>();
[javac] ^
[javac] required: class
[javac] found: <E>ArrayDeque<E>
[javac] where E is a type-variable:
[javac] E extends Object declared in class ArrayDeque
[javac] /srv/hudson/jobs/MicroTESK/workspace/src/main/java/core/ru/ispras/microtesk/translator/simnml/coverage/ssa/SsaAssembler.java:65: error: cannot find symbol
[javac] this.changes = new Changes(changesStore, changesStore);
[javac] ^
[javac] symbol: class Changes
[javac] location: class SsaAssembler
[javac] /srv/hudson/jobs/MicroTESK/workspace/src/main/java/core/ru/ispras/microtesk/translator/simnml/coverage/ssa/SsaAssembler.java:130: error: cannot find symbol
[javac] final Collection<Changes> containers = changes.fork(size);
[javac] ^
[javac] symbol: class Changes
[javac] location: class SsaAssembler
[javac] /srv/hudson/jobs/MicroTESK/workspace/src/main/java/core/ru/ispras/microtesk/translator/simnml/coverage/ssa/SsaAssembler.java:131: error: cannot find symbol
[javac] final Iterator<Changes> rebasers = containers.iterator();
[javac] ^
[javac] symbol: class Changes
[javac] location: class SsaAssembler
[javac] /srv/hudson/jobs/MicroTESK/workspace/src/main/java/core/ru/ispras/microtesk/translator/simnml/coverage/ssa/SsaAssembler.java:172: error: cannot find symbol
[javac] for (Changes diff : containers) {
[javac] ^
[javac] symbol: class Changes
[javac] location: class SsaAssembler
[javac] Note: /srv/hudson/jobs/MicroTESK/workspace/src/main/java/core/ru/ispras/microtesk/translator/simnml/coverage/ssa/SsaAssembler.java uses unchecked or unsafe operations.
[javac] Note: Recompile with -Xlint:unchecked for details.
[javac] 11 errors
BUILD FAILED
/srv/hudson/jobs/MicroTESK/workspace/build.xml:217: Compile failed; see the compiler error output for details.
Total time: 18 seconds
[WARNINGS] Skipping publisher since build result is FAILURE
Recording test results
Finished: FAILURE
</pre> MicroTESK - Task #5678 (Closed): Support for named branches in ISA specificationshttps://forge.ispras.ru/issues/56782015-03-03T10:46:59ZAndrei Tatarnikovandrewt@ispras.ru
<p>Named branches in ISA specifications must be supported:</p>
<ol>
<li>Support the construct "<code>branch("BranchName");</code>" in the nML translator;</li>
<li>Support situations for named branches in the coverage extractor.</li>
</ol> MicroTESK - Task #5676 (Closed): [generator] Random generation - weighting / biasing distribution https://forge.ispras.ru/issues/56762015-03-03T09:20:51ZAndrei Tatarnikovandrewt@ispras.ru
<p>Subj. must be implemented.</p>
<p>Discussion about the randomisation/seeding/biasing/buckets point (Randomisation and seeding / Biasing – not just :min, :max , but buckets):</p>
<blockquote>
<p>we were thinking about something available in languages with support for constrained-random activity, like Specman 'e' and SystemVerilog.</p>
<p>For instance this is a SystemVerilog example taken from <a class="external" href="http://www.asic-world.com/systemverilog/random_constraint7.html">http://www.asic-world.com/systemverilog/random_constraint7.html</a> :<br /><pre>
constraint src {
src_port dist {
0 := 1,
1 := 1,
2 := 5,
4 := 1
};
}
constraint des {
des_port dist {
[0 : 5 ] :/ 5,
[6 : 100 ] := 1,
[101 : 200 ] := 1,
[201 : 255 ] := 1
};
}
</pre><br />Basically the "dist" construct allows a "distribution" of probability to be specified.</p>
<p>For instance the value of "src_port" can have values 0,1,2,4, where values 0,1,4 all have the same weight whereas value 2 has five times the weight of the others.</p>
<p>As the total sum of all the weights is 8, values 0,1,4 will be extracted 1/8 of the time each (i.e. 12.5%), whereas value 2 will have a probability of 5/8 (i.e. 62.5%).</p>
<p>The second example for "dst_port" is a bit more complex (you can find an explanation of the operators here: <a class="external" href="http://www.testbench.in/CR_15_CONSTRAINT_EXPRESSION.html">http://www.testbench.in/CR_15_CONSTRAINT_EXPRESSION.html</a> ).</p>
<p>Basically all the values comprised for instance in the second range [6:100] will all have a weight of 1 each; whereas those in the first range will share the same weight of 5 (so the six numbers will have a weight of 5/6 each).</p>
<p>Each of these ranges can be considered a "bucket" (but we usually refer to this as "distributions" at the time of generation and "bucketing" at the time of collecting coverage).</p>
<p>In addition of getting generating values match the desired distribution across multiple generated tests, it is desirable to be able to generate exactly the same test again if the generator is invoked with the same randomization seed (typically from the command line).</p>
<p>Please note that the probability distribution doesn't necessarily have to only work with numbers, for instance something like this could be envisaged for load instructions:<br /><pre>
constraint c_LD_instr {
LD_instr dist {
LDR := 1,
LDRB := 1,
LDRH := 5,
LDUR := 1
};
}
</pre></p>
</blockquote> MicroTESK - Task #5672 (Closed): Support for UNPREDICTED and UNDEFINEDhttps://forge.ispras.ru/issues/56722015-03-03T08:35:05ZAndrei Tatarnikovandrewt@ispras.ru
<p>Support for handling branches of instruction logic marked as UNPREDICTED and UNDEFINED:</p>
<ol>
<li>In the nML translator (keywords UNPREDICTED or UNDEFINED);</li>
<li>In the coverage extractor (corresponding constraints)</li>
</ol> 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> TestBase - Task #5312 (Closed): TestBase.executeQuery should return some status descriptionhttps://forge.ispras.ru/issues/53122014-10-05T15:05:36ZAndrei Tatarnikovandrewt@ispras.ru
<p>Метод TestBase.executeQuery сейчас возвращает объект типа TestDataProvider. Клиенту этой информации не совсем достаточно.<br />Если запрос будет успешно выполнен, то мы получим нужные данные. А если нет? Вернётся null или пустой TestDataProvider? А как мы узнаем, почему наш запрос не выполнился (мне нужно вывести соответствующее сообщение)? Будет кидаться исключение?</p>
<p>Наверное, нужно возвращать какой-то статус. Например, как в Solver (Fortress), есть класс SolverResult, который хранит следующие атрибуты:</p>
<p>1. Статус (enum: OK, ERROR, UNSAT и т.д.).<br />2. Результат (в нашем случае TestDataProvider).<br />3. Список ошибок (List<String>).</p> 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> MicroTESK - Bug #4996 (Closed): [translator] It should be possible to define the "instruction" op...https://forge.ispras.ru/issues/49962014-06-18T11:42:22ZAndrei Tatarnikovandrewt@ispras.ru
<p>The current version has an unreasonable limitation: the "instruction" operation (root) can be defined as an AND rule only. This should be changed. It should be allowed to define the "instruction" operation as an OR rule.</p> MicroTESK - Task #4283 (Closed): [translator] Support for custom attributes in operations and add...https://forge.ispras.ru/issues/42832013-07-01T10:24:28ZAndrei Tatarnikovandrewt@ispras.ru
<p>Транслятор и модель должны поддерживатить использование <strong>кастомных аттрибутов</strong>. Например, в приведённом ниже куске используется аттрибут loop, который организует цикл путём рекурсии. Для трансляции модели MIPS требуется эта возможность.</p>
<pre>
op CLZ(rd : index, rs : REG_IND_ZERO)
syntax = format ("CLZ %d,%s", rd, rs.syntax)
image = format ("011100%s%5b%5b00000100000", rs.image, rd, rd)
action = {
tmp_signed_byte = 31;
GPR [rd] = 32;
loop;
}
loop = {
if tmp_signed_byte >= 0 then
if ( rs < tmp_signed_byte..tmp_signed_byte > == 0 ) then
tmp_signed_byte = tmp_signed_byte - 1;
else
GPR [ rd ] = 31 - tmp_signed_byte;
tmp_signed_byte = -1;
endif;
loop;
endif;
}
</pre>