Open-Source Projects: Issueshttps://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692023-03-06T15:03:36ZOpen-Source Projects
Redmine MicroTESK - Bug #12223 (New): Конфликт инструкций с разными модификаторами (op, internal op) и с ...https://forge.ispras.ru/issues/122232023-03-06T15:03:36ZAlexander Protsenkoprotsenko@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 -> CVC5https://forge.ispras.ru/issues/120272022-11-02T10:34:51ZAlexander Protsenkoprotsenko@ispras.ru
<p>Обновить используемый в инструменте MicroTESK SMT Solvers CVC4 до CVC5.</p> MicroTESK - Bug #11695 (New): error: cannot find symbol (зависимость mode от op)https://forge.ispras.ru/issues/116952022-06-28T10:27:08ZAlexander Protsenkoprotsenko@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): Загрузка данных в память через modehttps://forge.ispras.ru/issues/116612022-06-15T08:15:03ZAlexander Protsenkoprotsenko@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/116542022-06-14T14:03:59ZAlexander Protsenkoprotsenko@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 typeshttps://forge.ispras.ru/issues/108322021-05-06T19:07:40ZAlexander Protsenkoprotsenko@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/107642021-03-23T13:17:44ZPavel Putropavel.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): Отсутствует поддержка тернарного оператора в mirhttps://forge.ispras.ru/issues/105662020-11-10T09:06:12ZPavel Putropavel.putro@ispras.ru
<p>Наличие тернарного оператора в NML модели приводит к падению при выполнении команды symexecute.</p> MicroTESK - Task #10193 (New): Cache instances configurationhttps://forge.ispras.ru/issues/101932020-04-01T07:23:10ZAlexander Kamkinaskamkin@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 expectedhttps://forge.ispras.ru/issues/101772020-03-24T08:49:09ZAlexander Kamkinaskamkin@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 #10011 (New): Необходима возможность преобразования конструкции if-then-else в mi...https://forge.ispras.ru/issues/100112019-12-24T17:00:39ZAlexander Protsenkoprotsenko@ispras.ru
<p>Пример:<br /><pre>
inline calls
PASS: inline 'general_rev_op_32.action'
PASS: inline call 'REG_32.read'
PASS: inline call 'general_rev.action'
********************************************************************************
ATTENTION! An unexpected error has occurred:
java.lang.IllegalArgumentException: Bit vector sizes do not match: 1 != 6.
The program will be terminated. Please contact us at:
microtesk-support@ispras.ru
We are sorry for the inconvenience.
Exception stack:
java.lang.IllegalArgumentException: Bit vector sizes do not match: 1 != 6.
at ru.ispras.fortress.data.types.bitvector.BitVectorMath.checkEqualSize(BitVectorMath.java:926)
at ru.ispras.fortress.data.types.bitvector.BitVectorMath.transform(BitVectorMath.java:902)
at ru.ispras.fortress.data.types.bitvector.BitVectorMath.add(BitVectorMath.java:682)
at ru.ispras.microtesk.translator.mir.BvOpcode$1.evalBitVector(Instruction.java:412)
at ru.ispras.microtesk.translator.mir.BvOpcode.evalConst(Instruction.java:512)
at ru.ispras.microtesk.translator.mir.EvalContext.visit(EvalContext.java:74)
at ru.ispras.microtesk.translator.mir.Instruction$Assignment.accept(Instruction.java:30)
at ru.ispras.microtesk.translator.mir.EvalContext.eval(EvalContext.java:59)
at ru.ispras.microtesk.translator.mir.InlinePass.apply(InlinePass.java:28)
at ru.ispras.microtesk.translator.mir.MirPassDriver.apply(MirPassDriver.java:46)
at ru.ispras.microtesk.translator.mir.MirPassDriver.run(MirPassDriver.java:56)
at ru.ispras.microtesk.translator.mir.MirTransHandler.processIr(MirTransHandler.java:72)
at ru.ispras.microtesk.translator.mir.MirTransHandler.processIr(MirTransHandler.java:30)
at ru.ispras.microtesk.translator.Translator.processIr(Translator.java:84)
at ru.ispras.microtesk.translator.nml.NmlTranslator.start(NmlTranslator.java:133)
at ru.ispras.microtesk.translator.Translator.translate(Translator.java:201)
at ru.ispras.microtesk.MicroTESK.translate(MicroTESK.java:168)
at ru.ispras.microtesk.MicroTESK.runTask(MicroTESK.java:141)
at ru.ispras.microtesk.MicroTESK.main(MicroTESK.java:79)
</pre><br /><pre>
var V_var[card(6)]
internal op general_rev (x: DWORD, rev_op: card(2), size: BIT)
action = {
if rev_op == RevOp_REV16 then V_var = 0b001000;
elif rev_op == RevOp_REV32 then V_var = 0b011000;
elif rev_op == RevOp_REV64 then V_var = 0b111000;
elif rev_op == RevOp_RBIT then
---> V_var = if size == 0 then coerce(card(6), 0b111111) else coerce(card(6), 0b011111) endif;
endif;
</pre></p> MicroTESK - Developer Request #9472 (Open): Неочевидные преобразования типов при вычислении выраж...https://forge.ispras.ru/issues/94722019-02-05T09:25:55ZAlexander Protsenkoprotsenko@ispras.ru
<pre>
trace("store_global: MEM_WORD 1");
tmp_qword = MEM[mem_index + 1]::MEM[mem_index];
trace("store_global: MEM_WORD 2 tmp_bit_offset = 0x%x", tmp_bit_offset);
tmp_qword<tmp_bit_offset + 31..0+tmp_bit_offset> = rs2_op<31..0>;
trace("store_global: MEM_WORD 3");
MEM[mem_index + 1]::MEM[mem_index] = tmp_qword;
trace("store_global: MEM_WORD 4");
</pre>
<pre>
Mmu.PreTranslateAddress: satp.mode=0. No translation or protection.
PreTranslateAddress
PreTranslateAddress: read 2
PreTranslateAddress: read 3
store_global: MEM_WORD 2 tmp_bit_offset = 0x28
********************************************************************************
ATTENTION! An unexpected error has occurred:
java.lang.IllegalArgumentException: Assigning 32-bit data to 34-bit location is not allowed.
The program will be terminated. Please contact us at:
microtesk-support@ispras.ru
We are sorry for the inconvenience.
Exception stack:
java.lang.IllegalArgumentException: Assigning 32-bit data to 34-bit location is not allowed.
at ru.ispras.microtesk.model.memory.Location.store(ru/ispras/microtesk/model/memory/Location.java:131)
at ru.ispras.microtesk.model.riscv.op.store_global.action(ru/ispras/microtesk/model/riscv/op/store_global.java:99)
at ru.ispras.microtesk.model.IsaPrimitive.execute(ru/ispras/microtesk/model/IsaPrimitive.java:183)
at ru.ispras.microtesk.model.riscv.op.store_rvi.action(ru/ispras/microtesk/model/riscv/op/store_rvi.java:74)
at ru.ispras.microtesk.model.IsaPrimitive.execute(ru/ispras/microtesk/model/IsaPrimitive.java:183)
at ru.ispras.microtesk.model.riscv.op.sw.action(ru/ispras/microtesk/model/riscv/op/sw.java:118)
at ru.ispras.microtesk.model.IsaPrimitive.execute(ru/ispras/microtesk/model/IsaPrimitive.java:183)
at ru.ispras.microtesk.model.riscv.op.instruction.action(ru/ispras/microtesk/model/riscv/op/instruction.java:77)
at ru.ispras.microtesk.model.IsaPrimitive.execute(ru/ispras/microtesk/model/IsaPrimitive.java:183)
at ru.ispras.microtesk.model.InstructionCall.execute(ru/ispras/microtesk/model/InstructionCall.java:68)
at ru.ispras.microtesk.test.template.ConcreteCall.execute(ru/ispras/microtesk/test/template/ConcreteCall.java:155)
at ru.ispras.microtesk.test.Executor.executeCall(ru/ispras/microtesk/test/Executor.java:455)
at ru.ispras.microtesk.test.Executor.executeToBreak(ru/ispras/microtesk/test/Executor.java:348)
at ru.ispras.microtesk.test.Executor.execute(ru/ispras/microtesk/test/Executor.java:276)
at ru.ispras.microtesk.test.TemplateProcessor.runExecution(ru/ispras/microtesk/test/TemplateProcessor.java:707)
at ru.ispras.microtesk.test.TemplateProcessor.runExecutionFromStart(ru/ispras/microtesk/test/TemplateProcessor.java:723)
at ru.ispras.microtesk.test.TemplateProcessor.finish(ru/ispras/microtesk/test/TemplateProcessor.java:193)
at ru.ispras.microtesk.test.template.Template.endMainSection(ru/ispras/microtesk/test/template/Template.java:213)
at jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at RUBY.generate(C:/!microtesk/MicroTESK-RISC-V/microtesk-riscv/microtesk-riscv/build/target/lib/ruby/template.rb:1066)
at RUBY.main(C:\!microtesk\MicroTESK-RISC-V\microtesk-riscv\microtesk-riscv\build\target\lib\ruby\microtesk.rb:33)
at org.jruby.RubyHash.each(org/jruby/RubyHash.java:1342)
at RUBY.main(C:\!microtesk\MicroTESK-RISC-V\microtesk-riscv\microtesk-riscv\build\target\lib\ruby\microtesk.rb:29)
at RUBY.(root)(C:\!microtesk\MicroTESK-RISC-V\microtesk-riscv\microtesk-riscv\build\target\lib\ruby\microtesk.rb:52)
at ru.ispras.microtesk.RubyRunner.run(ru/ispras/microtesk/RubyRunner.java:62)
at ru.ispras.microtesk.ScriptRunner.run(ru/ispras/microtesk/ScriptRunner.java:43)
at ru.ispras.microtesk.test.TestEngine.generate(ru/ispras/microtesk/test/TestEngine.java:172)
at ru.ispras.microtesk.MicroTESK.generate(ru/ispras/microtesk/MicroTESK.java:284)
at ru.ispras.microtesk.MicroTESK.runTask(ru/ispras/microtesk/MicroTESK.java:131)
at ru.ispras.microtesk.MicroTESK.main(ru/ispras/microtesk/MicroTESK.java:79)
********************************************************************************
</pre>
<p>Возможно стоит выводить больше информации, например имена переменных.</p> Fortress - Task #5211 (Open): Unit-тесты для трансформеров и калькулятораhttps://forge.ispras.ru/issues/52112014-08-21T06:38:22ZAlexander Kamkinaskamkin@gmail.com
<ol>
<li>Необходима база (массив, список) разнообразных выражений (разные константы, разные операции, связывание переменных и т.п.).</li>
<li>Необходимы тесты для всех трансформаторов (хотя бы проверка типа падает/не падает).</li>
</ol> Fortress - Task #4713 (New): SMT-LIB structureshttps://forge.ispras.ru/issues/47132014-03-17T06:59:53ZSergey Smolovsmolov@ispras.ru
<p>Реализовать поддержку структур (record) как типа данных языка SMT-LIB.</p> Fortress - Task #4523 (New): Implementing a solver for simple constraintshttps://forge.ispras.ru/issues/45232013-10-03T04:32:56ZAlexander Kamkinaskamkin@gmail.com
<p>Цель - генерация рандомизированных данных, удовлетворяющих несложным ограничениям (constrained random generation).</p>
<ol>
<li>Определить и описать в Wiki класс рассматриваемых ограничений.</li>
<li>Реализовать солвер (постараться добиться равномерного распределение данных, удовлетворяющих ограничениям).</li>
<li>Протестировать солвер (не берется за сложные ограничения, решает простые ограничения, решает их правильно, распределение данных близко к равномерному).</li>
</ol>