Project

General

Profile

Actions
Copy link

Bug #10014

closed

mir некорректно интерпретирует побитовое отрицание (~)

Added by Alexander Protsenko almost 5 years ago. Updated almost 5 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Artem Kotsynyak
Category:
nML Translator
Target version:
2.5
Start date:
12/25/2019
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:
2.5.0-beta-191226

Description

В примерах ниже были убраны "~" из кода, после этого mir логировался до строки 2 531 777, до этого до 750 000.

Пример 1 (armv8.nml line: 2800+-):

    MemLoadSingle(shifted_addr<60..0>, 8, acctype, 0).action;
    temp_dword = memLoadSingleValue;
-->    mask_dword = ~((coerce(card(65), 1) << size_op * 8) - coerce(card(65), 1));
    mask_dword = mask_dword << (8 * coerce(BYTE, address<2..0>));
    temp_dword = temp_dword & coerce(DWORD, mask_dword);
    temp_dword = temp_dword | (wdata << (8 * coerce(BYTE, address<2..0>)));
    MemStoreSingle(shifted_addr<60..0>, size_op, acctype, 0, temp_dword).action;
    trace("MemStore (atomic): address=0x%x (shifted_addr=0x%x), size=%d, written data=0x%x", address, shifted_addr, size_op, temp_dword);

Пример 2:

    assert(size_op > 1, "assert size > 1");
    // TODO ConstrainUnpredictable()
    MemLoadSingle(shifted_addr<60..0>, 8, acctype, 0).action;
    temp_qword<63..0> = memLoadSingleValue;
    MemLoadSingle(shifted_addr<60..0> + 1, 8, acctype, 0).action;
    temp_qword<127..64> = memLoadSingleValue;
-->    mask_qword = ~((coerce(card(129), 1) << size_op * 8) - coerce(card(129), 1));
    temp_qword = temp_qword & coerce(QWORD, mask_qword << (8 * coerce(BYTE, address<2..0>)));
    temp_qword = temp_qword | (coerce(QWORD, wdata) << (8 * coerce(BYTE, address<2..0>)));
    MemStoreSingle(shifted_addr<60..0>, size_op, acctype, 0, temp_qword<63..0>).action;
    MemStoreSingle(shifted_addr<60..0> + 1, size_op, acctype, 0, temp_qword<127..64>).action;
    trace("MemStore (not atomic or size-16): address=0x%x (shifted_addr=0x%x), size=%d, written data=0x%x", address, shifted_addr, size_op, temp_qword);

Логи ошибок при не убранных "~".

Пример лога 1 mir (строка 750 530):

EVAL: %1626 = load i64, i64 shifted_addr
EVAL: %1627 = Extract i61 of i64 %1626 <60, 0>
EVAL: store i8 8, i8 SIZE
EVAL: store i4 %9, i4 ACCTYPE
EVAL: store i138 0, i138 AddrDesc
EVAL: %2715 = load i64, [2305843009213693952, i64] M[%1627]
EVAL: store i64 %2715, i64 memLoadSingleValue
EVAL: %2716 = load i138, i138 AddrDesc
EVAL: %2717 = Extract i5 of i138 %2716 <4, 0>
EVAL: %2718 = i1 Ne i5 %2717, 0
EVAL: br i1 %2718, label %null, label %null
EVAL: br label %null
EVAL: br label %null
EVAL: %1628 = load i64, i64 memLoadSingleValue
EVAL: store i64 %1628, i64 temp_dword
EVAL: %1629 = i8 Mul i8 %59, 8
EVAL: %1630 = i65 Shl i65 1, %1629
EVAL: %1631 = i65 Sub i65 %1630, 1
EVAL: %1632 = i65 Xor i65 %1631, -1
********************************************************************************
ATTENTION! An unexpected error has occurred:
java.lang.IllegalArgumentException: Bit vector sizes do not match: 65 != 64.

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: 65 != 64.
    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.xor(BitVectorMath.java:364)
    at ru.ispras.microtesk.translator.mir.BvOpcode$8.evalBitVector(Instruction.java:462)
    at ru.ispras.microtesk.translator.mir.BvOpcode.evalConst(Instruction.java:512)
    at ru.ispras.microtesk.translator.mir.EvalContext.visit(EvalContext.java:77)
    at ru.ispras.microtesk.translator.mir.Instruction$Assignment.accept(Instruction.java:30)
    at ru.ispras.microtesk.translator.mir.EvalContext.eval(EvalContext.java:62)
    at ru.ispras.microtesk.translator.mir.EvalContext.evalInternal(EvalContext.java:44)
    at ru.ispras.microtesk.translator.mir.EvalContext.eval(EvalContext.java:31)
    at ru.ispras.microtesk.translator.mir.InsnRewriter.rewrite(InsnRewriter.java:22)
    at ru.ispras.microtesk.translator.mir.ForwardPass.apply(ForwardPass.java:21)
    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:73)
    at ru.ispras.microtesk.translator.mir.MirTransHandler.processIr(MirTransHandler.java:31)
    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)

Пример фрагмента лога 2 mir (строка 750 470):

EVAL: %1591 = load i64, i64 memLoadSingleValue
EVAL: %1593 = load i128, i128 temp_qword
EVAL: %1594 = Zext i64 %1591 to i128
EVAL: %1595 = i128 And i128 %1593, 18446744073709551615
EVAL: %1596 = i128 Shl i128 %1594, 64
EVAL: %1592 = i128 Or i128 %1595, %1596
EVAL: store i128 %1592, i128 temp_qword
EVAL: %1597 = i8 Mul i8 %59, 8
EVAL: %1598 = i129 Shl i129 1, %1597
EVAL: %1599 = i129 Sub i129 %1598, 1
EVAL: %1600 = i129 Xor i129 %1599, -1
********************************************************************************
ATTENTION! An unexpected error has occurred:
java.lang.IllegalArgumentException: Bit vector sizes do not match: 129 != 64.

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: 129 != 64.
    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.xor(BitVectorMath.java:364)
    at ru.ispras.microtesk.translator.mir.BvOpcode$8.evalBitVector(Instruction.java:462)
    at ru.ispras.microtesk.translator.mir.BvOpcode.evalConst(Instruction.java:512)
    at ru.ispras.microtesk.translator.mir.EvalContext.visit(EvalContext.java:77)
    at ru.ispras.microtesk.translator.mir.Instruction$Assignment.accept(Instruction.java:30)
    at ru.ispras.microtesk.translator.mir.EvalContext.eval(EvalContext.java:62)
    at ru.ispras.microtesk.translator.mir.EvalContext.evalInternal(EvalContext.java:44)
    at ru.ispras.microtesk.translator.mir.EvalContext.eval(EvalContext.java:31)
    at ru.ispras.microtesk.translator.mir.InsnRewriter.rewrite(InsnRewriter.java:22)
    at ru.ispras.microtesk.translator.mir.ForwardPass.apply(ForwardPass.java:21)
    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:73)
    at ru.ispras.microtesk.translator.mir.MirTransHandler.processIr(MirTransHandler.java:31)
    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)

Actions
Copy link

Also available in: Atom PDF