Open-Source Projects: Issues
https://forge.ispras.ru/
https://forge.ispras.ru/favicon.ico?1649012669
2023-03-06T15:03:36Z
Open-Source Projects
Redmine
MicroTESK - Bug #12223 (New): Конфликт инструкций с разными модификаторами (op, internal op) и с ...
https://forge.ispras.ru/issues/12223
2023-03-06T15:03:36Z
Alexander Protsenko
protsenko@ispras.ru
<p>Пример:<br /><pre>
op ands_bitmask (rd: REG, rn: REG, N: BIT, imms: card(6), immr: card(6))
internal op ands_bitmask_32n (rd: REG_32, rn: REG_32, N: BIT, imms: card(6), immr: card(6))
init = {}
syntax = format("ands %s, %s, %s", rd.syntax, rn.syntax, lsx(sf_53, wmask).syntax)
image = format("%22s%5s%5s", lix(sf_53, N, imms, immr, opc_53).image, rn.image, rd.image)
action = {}
</pre><br />Спецификация собирается, но инструкция ands_bitmask не доступна в шаблонах.</p>
MicroTESK - Task #12027 (New): SMT Solvers: CVC4 -> CVC5
https://forge.ispras.ru/issues/12027
2022-11-02T10:34:51Z
Alexander Protsenko
protsenko@ispras.ru
<p>Обновить используемый в инструменте MicroTESK SMT Solvers CVC4 до CVC5.</p>
MicroTESK - Bug #11695 (New): error: cannot find symbol (зависимость mode от op)
https://forge.ispras.ru/issues/11695
2022-06-28T10:27:08Z
Alexander Protsenko
protsenko@ispras.ru
<p>Описание ошибки:<br /><pre>
internal op imm4_syntax_i32(imm: imm4)
init = {}
syntax = format("0x%x", sign_extend(i32, imm))
mode BRANCH_IMM4(imm: int(4)) = imm
init = {
jump_imm4 = imm;
}
syntax = format("%s", imm4_syntax_i32(imm).syntax)
image = format("%s", imm)
</pre></p>
<p>Ошибка:<br /><pre>
mode\BRANCH_IMM4.java:72: error: cannot find symbol
return String.format("%s", new imm4_syntax_i32(imm).text(vars__));
^
symbol: class imm4_syntax_i32
location: class BRANCH_IMM4
</pre></p>
<p>В BRANCH_IMM4.java отсутствует импорт imm4_syntax_i32.</p>
MicroTESK - Developer Request #11661 (New): Загрузка данных в память через mode
https://forge.ispras.ru/issues/11661
2022-06-15T08:15:03Z
Alexander Protsenko
protsenko@ispras.ru
<p>Это будет полезно для спецификации виртуальных машин и позволит заменить загрузку данных через псевдо операции.</p>
<p>Например:<br /><pre>
mode F(i: card(4), a: card(4), b: card(4), c: card(4)) = FMEM[i..i+2]
</pre></p>
<p>Возможно, стоит это сделать с использованием структур:<br /><pre>
struct f_structure (
i: card(4),
a: card(4),
b: card(4),
c: card(4)
)
mode F(v: f_structure): {FMEM[f_structure.i] = f_structure}
</pre></p>
<p>Нужно понять, возможно ли добавить это в инструмент.</p>
MicroTESK - Bug #11654 (New): Или правило для регистров может вызывать ошибку "error: incompatibl...
https://forge.ispras.ru/issues/11654
2022-06-14T14:03:59Z
Alexander Protsenko
protsenko@ispras.ru
<p>Ниже приведен код для модели minimips для воссоздания ошибки:<br />Регистр:<br /><pre>
mode REG (i: INDEX) = GPR[i]
init = { tmp = i; }
// This is just to demonstrate the decode attribute
decode = { i = tmp; }
syntax = format("$%d", tmp)
image = format("%s", tmp)
mode REG_SHIFT (i: INDEX, shift: BIT) = GPR[i]
init = { tmp = i; }
// This is just to demonstrate the decode attribute
decode = { i = tmp; }
syntax = format("%s", if shift == 0
then "shift0"
else "shift1" endif)
image = format("%s", tmp)
mode REGA = REG_SHIFT | REG
</pre></p>
<p>Инструкция:<br /><pre>
internal op op_rega_rega_rega(rd: REGA, rs: REGA, rt: REGA)
image = format("%s%s%s", rs.image, rt.image, rd.image)
op addB (rd: REG, rs: REGA, rt: REGA)
syntax = format("add %s, %s, %s", rd.syntax, rs.syntax, rt.syntax)
image = format("000000%s00000100000", op_rega_rega_rega(rd, rs, rt).image)
action = {
temp = rs<31>::rs + rt<31>::rt;
if temp<32> != temp<31> then
mark("overflow");
COP0_R[14] = CIA;
exception("IntegerOverflow");
else
mark("normal");
rd = temp<31..0>;
endif;
}
</pre></p>
<p>Ошибка:<br /><pre>
D:\WorkProjects\MicroTESK\microtesk\build\generated-src\models\src\java\ru\ispras\microtesk\model\minimips\decoder\DecoderAddB.java:75: error: incompatible types: IsaPrimitive cannot be converted to REG
rd = op_rega_rega_rega_instance.rd;
</pre></p>
MicroTESK - Bug #10832 (New): Parser allows bit vector extraction of array types
https://forge.ispras.ru/issues/10832
2021-05-06T19:07:40Z
Alexander Protsenko
protsenko@ispras.ru
<p>Ошибка:<br /><pre>
Translating to MIR...
********************************************************************************
ATTENTION! An unexpected error has occurred:
java.lang.UnsupportedOperationException: null
The program will be terminated. Please contact us at:
microtesk-support@ispras.ru
We are sorry for the inconvenience.
Exception stack:
java.lang.UnsupportedOperationException
at ru.ispras.microtesk.translator.mir.MirArray.getSize(MirTy.java:213)
at ru.ispras.microtesk.translator.mir.NmlIrTrans$WriteAccess.shiftLeft(NmlIrTrans.java:902)
at ru.ispras.microtesk.translator.mir.NmlIrTrans$WriteAccess.write(NmlIrTrans.java:887)
at ru.ispras.microtesk.translator.mir.NmlIrTrans$WriteAccess.accessMemory(NmlIrTrans.java:873)
at ru.ispras.microtesk.translator.mir.NmlIrTrans.translateAccess(NmlIrTrans.java:696)
at ru.ispras.microtesk.translator.mir.NmlIrTrans.translateWrite(NmlIrTrans.java:666)
at ru.ispras.microtesk.translator.mir.NmlIrTrans.translateAssignment(NmlIrTrans.java:321)
at ru.ispras.microtesk.translator.mir.NmlIrTrans.translate(NmlIrTrans.java:314)
at ru.ispras.microtesk.translator.mir.NmlIrTrans.translate(NmlIrTrans.java:194)
at ru.ispras.microtesk.translator.mir.NmlIrTrans.translate(NmlIrTrans.java:117)
at ru.ispras.microtesk.translator.mir.NmlIrTrans.translate(NmlIrTrans.java:74)
at ru.ispras.microtesk.translator.mir.MirTransHandler.translateIr(MirTransHandler.java:106)
at ru.ispras.microtesk.translator.mir.MirTransHandler.processIr(MirTransHandler.java:69)
at ru.ispras.microtesk.translator.mir.MirTransHandler.processIr(MirTransHandler.java:52)
at ru.ispras.microtesk.translator.Translator.processIr(Translator.java:84)
at ru.ispras.microtesk.translator.nml.NmlTranslator.start(NmlTranslator.java:131)
at ru.ispras.microtesk.translator.Translator.translate(Translator.java:201)
at ru.ispras.microtesk.MicroTESK.translate(MicroTESK.java:150)
at ru.ispras.microtesk.MicroTESK.runTask(MicroTESK.java:142)
at ru.ispras.microtesk.MicroTESK.main(MicroTESK.java:80)
********************************************************************************
</pre></p>
<p>Ошибка возникает на спецификации ВМ от 2021.05.06.</p>
MicroTESK - Task #10764 (New): Поддержка алтернативного формата вывода SMT-LIB представления маши...
https://forge.ispras.ru/issues/10764
2021-03-23T13:17:44Z
Pavel Putro
pavel.putro@ispras.ru
Для использования в рамках задачи SyGuS необходима поддержка формата вывода базовых блоков машинного кода в виде единых функций. Данные функции должны принимать на вход и возвращать единственный параметр типа State, представляющий текущее состояние машины (регистры + память). Тип State должен вычисляться путём анализа NML модели и иметь единый формат для всех базовых блоков.<br />Тип State должен включать:
<ol>
<li>регистры общего назначения</li>
<li>массив памяти</li>
<li>регистры специального назначения</li>
<li>Флаги (если не встроены в регистры специального назначения)</li>
<li>Отдельный булевый параметр - условие перехода.</li>
</ol>
Тип State не должен включать
<ol>
<li>временные переменные типа tmp_dword и т. п.</li>
<li>безымянные промежуточные значения типа %123</li>
</ol>
<p>Пример определения типа State на SMT-LIB:<br /><pre>
(declare-datatypes ((State 0))
(((cons (XREG (Array (_ BitVec 5) (_ BitVec 32))) (MEM (Array (_ BitVec 32) (_ BitVec 8))) (zf Bool) (sf Bool) (jc Bool)))))
</pre><br />Для удобства использования типа State и сокращения объёма генерируемого кода желательно определить аксессоры для записи и чтения данных:</p>
<pre>
(define-fun get_reg ((s State) (r (_ BitVec 5))) (_ BitVec 32) (select (XREG s) r))
(define-fun set_reg ((s State) (r (_ BitVec 5)) (v (_ BitVec 32))) State (cons (store (XREG s) r v) (MEM s) (zf s) (sf s) (jc s)))
(define-fun get_mem ((s State) (r (_ BitVec 5))) (_ BitVec 8) (select (MEM s) (get_reg s r)))
(define-fun set_mem ((s State) (r (_ BitVec 5)) (v (_ BitVec 8))) State (cons (XREG s) (store (MEM s) (get_reg s r) v) (zf s) (sf s) (jc s)))
</pre>
<p>Сама функция в таком случае может быть реализована через цепочку let-выражений в виде:<br /><pre>
(define-fun memset-O1_block_2 ((s State)) State
(let ((s1 (set_mem s (_ bv10 5) ((_ extract 7 0) (get_reg s (_ bv11 5))))))
(let ((s2 (set_reg s1 (_ bv12 5) (bvsub (get_reg s1 (_ bv12 5)) (_ bv1 32)))))
(let ((s3 (set_reg s2 (_ bv14 5) (bvadd (get_reg s2 (_ bv14 5)) (_ bv1 32)))))
s3))))
</pre><br />Стоит также заметить, что в формате генерации функции по базовому блоку, а не по каждой конкретной инструкции отдельно, остаётся возможным применять оптимизации, используемые в текущем представлении модели.</p>
MicroTESK - Bug #10566 (New): Отсутствует поддержка тернарного оператора в mir
https://forge.ispras.ru/issues/10566
2020-11-10T09:06:12Z
Pavel Putro
pavel.putro@ispras.ru
<p>Наличие тернарного оператора в NML модели приводит к падению при выполнении команды symexecute.</p>
MicroTESK - Task #10193 (New): Cache instances configuration
https://forge.ispras.ru/issues/10193
2020-04-01T07:23:10Z
Alexander Kamkin
askamkin@gmail.com
<p>MMU specifications look like they are written for a single core. That's OK and, I think, it should be so. However, it is unclear how to instantiate the caches and connects them with the cores, the main memory and each other in multi-core settings. There should be a kind of configuration.</p>
<p>The modeling library provides the following mechanisms.</p>
<p><code>CacheUnit</code>'s constructor has the <code>next</code> parameter, which is a reference to the next-level cache instance or the main memory (<code>null</code> if the <code>next</code> attribute is not specified):</p>
<pre><code class="java syntaxhl" data-language="java"><span class="kd">public</span> <span class="nf">CacheUnit</span><span class="o">(...,</span> <span class="kd">final</span> <span class="nc">Buffer</span><span class="o"><?</span> <span class="kd">extends</span> <span class="nc">Struct</span><span class="o"><?>,</span> <span class="no">A</span><span class="o">></span> <span class="n">next</span><span class="o">)</span>
</code></pre>
<p>Also, <code>CacheUnit</code> implements the <code>addNeighbor</code> method that links the cache instance with the same-level ones:</p>
<pre><code class="java syntaxhl" data-language="java"><span class="kd">public</span> <span class="kt">void</span> <span class="nf">addNeighbor</span><span class="o">(</span><span class="kd">final</span> <span class="nc">CacheUnit</span><span class="o"><?,</span> <span class="no">A</span><span class="o">></span> <span class="n">other</span><span class="o">)</span>
</code></pre>
Fortress - Bug #10177 (Feedback): TreeVisitor's SKIP status does not work as expected
https://forge.ispras.ru/issues/10177
2020-03-24T08:49:09Z
Alexander Kamkin
askamkin@gmail.com
<p>When I call <code>setStatus(Status.SKIP)</code> in <code>onOperationBegin(node)</code>, I expect the visitor will not visit the node's children but will visit the node's neighbors.<br />However, the call skips visiting the neighbors.</p>
MicroTESK - Bug #10064 (New): Support FP instructions in MIR
https://forge.ispras.ru/issues/10064
2020-01-24T07:54:30Z
Alexander Protsenko
protsenko@ispras.ru
<pre>
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<31..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<31..0>)'
Warning: missing opcode mapping: ADD in '(ADD (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 fs<63..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 ft<63..0>)'
Warning: missing opcode mapping: ADD in '(ADD (INT_TO_FLOAT 64 fs<63..0>) (INT_TO_FLOAT 64 ft<63..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 64 temp_fp_d)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<31..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<31..0>)'
Warning: missing opcode mapping: ADD in '(ADD (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<63..32>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<63..32>)'
Warning: missing opcode mapping: ADD in '(ADD (INT_TO_FLOAT 32 fs<63..32>) (INT_TO_FLOAT 32 ft<63..32>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: DIV in '(DIV fs<31..0> ft<31..0>)'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 fs)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 ft)'
Warning: missing opcode mapping: DIV in '(DIV (INT_TO_FLOAT 64 fs) (INT_TO_FLOAT 64 ft))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 64 temp_fp_d)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<31..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<31..0>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>))'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fr<31..0>)'
Warning: missing opcode mapping: ADD in '(ADD (MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>)) (INT_TO_FLOAT 32 fr<31..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 fs<63..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 ft<63..0>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 64 fs<63..0>) (INT_TO_FLOAT 64 ft<63..0>))'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 fr<63..0>)'
Warning: missing opcode mapping: ADD in '(ADD (MUL (INT_TO_FLOAT 64 fs<63..0>) (INT_TO_FLOAT 64 ft<63..0>)) (INT_TO_FLOAT 64 fr<63..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 64 temp_fp_d)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<31..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<31..0>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>))'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fr<31..0>)'
Warning: missing opcode mapping: ADD in '(ADD (MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>)) (INT_TO_FLOAT 32 fr<31..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<63..32>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<63..32>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 32 fs<63..32>) (INT_TO_FLOAT 32 ft<63..32>))'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fr<63..32>)'
Warning: missing opcode mapping: ADD in '(ADD (MUL (INT_TO_FLOAT 32 fs<63..32>) (INT_TO_FLOAT 32 ft<63..32>)) (INT_TO_FLOAT 32 fr<63..32>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<31..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<31..0>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>))'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fr<31..0>)'
Warning: missing opcode mapping: SUB in '(SUB (MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>)) (INT_TO_FLOAT 32 fr<31..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 fs<63..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 ft<63..0>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 64 fs<63..0>) (INT_TO_FLOAT 64 ft<63..0>))'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 fr<63..0>)'
Warning: missing opcode mapping: SUB in '(SUB (MUL (INT_TO_FLOAT 64 fs<63..0>) (INT_TO_FLOAT 64 ft<63..0>)) (INT_TO_FLOAT 64 fr<63..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 64 temp_fp_d)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<31..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<31..0>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>))'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fr<31..0>)'
Warning: missing opcode mapping: SUB in '(SUB (MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>)) (INT_TO_FLOAT 32 fr<31..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<63..32>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<63..32>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 32 fs<63..32>) (INT_TO_FLOAT 32 ft<63..32>))'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fr<63..32>)'
Warning: missing opcode mapping: SUB in '(SUB (MUL (INT_TO_FLOAT 32 fs<63..32>) (INT_TO_FLOAT 32 ft<63..32>)) (INT_TO_FLOAT 32 fr<63..32>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<31..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<31..0>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 fs)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 ft)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 64 fs) (INT_TO_FLOAT 64 ft))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 64 temp_fp_d)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<31..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<31..0>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<63..32>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<63..32>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 32 fs<63..32>) (INT_TO_FLOAT 32 ft<63..32>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<31..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<31..0>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>))'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fr<31..0>)'
Warning: missing opcode mapping: ADD in '(ADD (MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>)) (INT_TO_FLOAT 32 fr<31..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 fs<63..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 ft<63..0>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 64 fs<63..0>) (INT_TO_FLOAT 64 ft<63..0>))'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 fr<63..0>)'
Warning: missing opcode mapping: ADD in '(ADD (MUL (INT_TO_FLOAT 64 fs<63..0>) (INT_TO_FLOAT 64 ft<63..0>)) (INT_TO_FLOAT 64 fr<63..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 64 temp_fp_d)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<31..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<31..0>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>))'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fr<31..0>)'
Warning: missing opcode mapping: ADD in '(ADD (MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>)) (INT_TO_FLOAT 32 fr<31..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<63..32>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<63..32>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 32 fs<63..32>) (INT_TO_FLOAT 32 ft<63..32>))'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fr<63..32>)'
Warning: missing opcode mapping: ADD in '(ADD (MUL (INT_TO_FLOAT 32 fs<63..32>) (INT_TO_FLOAT 32 ft<63..32>)) (INT_TO_FLOAT 32 fr<63..32>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<31..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<31..0>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>))'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fr<31..0>)'
Warning: missing opcode mapping: SUB in '(SUB (MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>)) (INT_TO_FLOAT 32 fr<31..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 fs<63..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 ft<63..0>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 64 fs<63..0>) (INT_TO_FLOAT 64 ft<63..0>))'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 fr<63..0>)'
Warning: missing opcode mapping: SUB in '(SUB (MUL (INT_TO_FLOAT 64 fs<63..0>) (INT_TO_FLOAT 64 ft<63..0>)) (INT_TO_FLOAT 64 fr<63..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 64 temp_fp_d)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<31..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<31..0>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>))'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fr<31..0>)'
Warning: missing opcode mapping: SUB in '(SUB (MUL (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>)) (INT_TO_FLOAT 32 fr<31..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<63..32>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<63..32>)'
Warning: missing opcode mapping: MUL in '(MUL (INT_TO_FLOAT 32 fs<63..32>) (INT_TO_FLOAT 32 ft<63..32>))'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fr<63..32>)'
Warning: missing opcode mapping: SUB in '(SUB (MUL (INT_TO_FLOAT 32 fs<63..32>) (INT_TO_FLOAT 32 ft<63..32>)) (INT_TO_FLOAT 32 fr<63..32>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 temp)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<31..0>)'
Warning: missing opcode mapping: DIV in '(DIV (INT_TO_FLOAT 32 temp) (INT_TO_FLOAT 32 fs<31..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 temp)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 fs<63..0>)'
Warning: missing opcode mapping: DIV in '(DIV (INT_TO_FLOAT 64 temp) (INT_TO_FLOAT 64 fs<63..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 64 temp_fp_d)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 temp)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<31..0>)'
Warning: missing opcode mapping: SQRT in '(SQRT (INT_TO_FLOAT 32 fs<31..0>))'
Warning: missing opcode mapping: DIV in '(DIV (INT_TO_FLOAT 32 temp) (SQRT (INT_TO_FLOAT 32 fs<31..0>)))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 temp)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 fs<63..0>)'
Warning: missing opcode mapping: SQRT in '(SQRT (INT_TO_FLOAT 64 fs<63..0>))'
Warning: missing opcode mapping: DIV in '(DIV (INT_TO_FLOAT 64 temp) (SQRT (INT_TO_FLOAT 64 fs<63..0>)))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 64 temp_fp_d)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<31..0>)'
Warning: missing opcode mapping: SQRT in '(SQRT (INT_TO_FLOAT 32 fs<31..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 fs<63..0>)'
Warning: missing opcode mapping: SQRT in '(SQRT (INT_TO_FLOAT 64 fs<63..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 64 temp_fp_d)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<31..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<31..0>)'
Warning: missing opcode mapping: SUB in '(SUB (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 fs<63..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 ft<63..0>)'
Warning: missing opcode mapping: SUB in '(SUB (INT_TO_FLOAT 64 fs<63..0>) (INT_TO_FLOAT 64 ft<63..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 64 temp_fp_d)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<31..0>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<31..0>)'
Warning: missing opcode mapping: SUB in '(SUB (INT_TO_FLOAT 32 fs<31..0>) (INT_TO_FLOAT 32 ft<31..0>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 fs<63..32>)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 ft<63..32>)'
Warning: missing opcode mapping: SUB in '(SUB (INT_TO_FLOAT 32 fs<63..32>) (INT_TO_FLOAT 32 ft<63..32>))'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
Warning: missing opcode mapping: IS_NAN in '(IS_NAN temp_fp_d)'
Warning: missing opcode mapping: IS_NAN in '(IS_NAN temp_fp_d2)'
Warning: missing opcode mapping: IS_SIGN_NAN in '(IS_SIGN_NAN temp_fp_d)'
Warning: missing opcode mapping: IS_SIGN_NAN in '(IS_SIGN_NAN temp_fp_d2)'
Warning: missing opcode mapping: IS_SIGN_NAN in '(IS_SIGN_NAN temp_fp_d)'
Warning: missing opcode mapping: IS_SIGN_NAN in '(IS_SIGN_NAN temp_fp_d2)'
Warning: missing opcode mapping: IS_NAN in '(IS_NAN temp_fp_d)'
Warning: missing opcode mapping: IS_NAN in '(IS_NAN temp_fp_d2)'
Warning: missing opcode mapping: FLOAT_TO_FLOAT in '(FLOAT_TO_FLOAT 64 temp_fp_s)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 tempI)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 64 temp64)'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 64 temp_fp_s)'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 64 temp_fp_d)'
Warning: missing opcode mapping: FLOAT_TO_FLOAT in '(FLOAT_TO_FLOAT 32 temp_fp_d)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 tempI)'
Warning: missing opcode mapping: INT_TO_FLOAT in '(INT_TO_FLOAT 32 temp64)'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_d)'
Warning: missing opcode mapping: FLOAT_TO_INT in '(FLOAT_TO_INT 32 temp_fp_s)'
</pre>
<p>INT_TO_FLOAT и пр. библиотечные операции, добавленные в проект тут: ru.ispras.microtesk.model.data.floatx<br />Это внутренние операции, у них нет и не должно быть "opcode";</p>
Fortress - Feature #5451 (New): Support external rules in TransformerRule interface
https://forge.ispras.ru/issues/5451
2014-11-26T12:58:41Z
Artem Kotsynyak
<p>TransformerRules are dedicated for use in NodeTransformer with other rules, but interface implementations has no information about other rules, therefore it may introduce inconsistencies in transformed expressions accordingly to entire set as a whole. Since given transforms are considered local, i.e. should match and replace only limited (and small) subgraph, it is reasonable to support external rules in interface instead of multiple transformation runs. Consider using abstract class in place of interface to enforce respecting external rules.</p>
Fortress - Task #5211 (Open): Unit-тесты для трансформеров и калькулятора
https://forge.ispras.ru/issues/5211
2014-08-21T06:38:22Z
Alexander Kamkin
askamkin@gmail.com
<ol>
<li>Необходима база (массив, список) разнообразных выражений (разные константы, разные операции, связывание переменных и т.п.).</li>
<li>Необходимы тесты для всех трансформаторов (хотя бы проверка типа падает/не падает).</li>
</ol>
Fortress - Task #4713 (New): SMT-LIB structures
https://forge.ispras.ru/issues/4713
2014-03-17T06:59:53Z
Sergey Smolov
smolov@ispras.ru
<p>Реализовать поддержку структур (record) как типа данных языка SMT-LIB.</p>
Fortress - Task #4523 (New): Implementing a solver for simple constraints
https://forge.ispras.ru/issues/4523
2013-10-03T04:32:56Z
Alexander Kamkin
askamkin@gmail.com
<p>Цель - генерация рандомизированных данных, удовлетворяющих несложным ограничениям (constrained random generation).</p>
<ol>
<li>Определить и описать в Wiki класс рассматриваемых ограничений.</li>
<li>Реализовать солвер (постараться добиться равномерного распределение данных, удовлетворяющих ограничениям).</li>
<li>Протестировать солвер (не берется за сложные ограничения, решает простые ограничения, решает их правильно, распределение данных близко к равномерному).</li>
</ol>