Project

General

Profile

Bug #9395

Symexecute не учитывает неявные преобразования типов в nml моделях

Added by Pavel Putro 22 days ago. Updated 21 days ago.

Status:
Open
Priority:
Normal
Category:
-
Target version:
-
Start date:
11/22/2018
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

В модели RISC-V в массив памяти с 62-х битным индексом производится запись по индексу размерностью 64 бит, что обрабатывается MicroTESK при компиляции и генерации модели, однако Symexecute не учитывает то, что smt-lib таких неявных преобразований не позволяет. Пример из файла riscv_rv32i.nml (строка 350).

tmp_index = tmp_address >> 2;

if tmp_address<1..0> == 0 then // Word-aligned address
tmp_word = MEM[tmp_index];

Генерация smt по данному коду приводит к ошибке солвера:
(error "array select not indexed with correct type for array")

На всякий случай прикладываю бинарный код.

abs_1.bin (68 Bytes) abs_1.bin Машинный код risc-v Pavel Putro, 11/22/2018 02:34 PM

History

#1 Updated by Alexander Kamkin 21 days ago

  • Status changed from New to Open

#2 Updated by Alexander Kamkin 21 days ago

  • Assignee set to Artem Kotsynyak

#3 Updated by Alexander Kamkin 21 days ago

  • Assignee changed from Artem Kotsynyak to Alexander Protsenko

Нужно поправить спецификации. Неявные преобразования нежелательны.

#4 Updated by Alexander Protsenko 21 days ago

  • Assignee changed from Alexander Protsenko to Pavel Putro
  • Status changed from Open to Feedback

Обновил спецификации RISC-V
https://forge.ispras.ru/projects/microtesk-riscv/repository/revisions/cc0c1b9fb06cfc3efe13b9b4bb43146554b3fdb7

Теперь все индексы, при обращении к MEM[], являются 62-битными (точнее card(XLEN - 2), для 32-х битной сборки, это будут 30-битные индексы).

#5 Updated by Pavel Putro 21 days ago

  • Assignee changed from Pavel Putro to Alexander Kamkin
  • Status changed from Feedback to Open

Раз неявные преобразования нежелательны, то возможно их стоит запретить на уровне инструмента, чтобы такая ситуация не повторилась в будущем. Ну или всё-таки добавить поддержку в symexecute.

#6 Updated by Alexander Kamkin 21 days ago

Согласен: нужно запретить на уровне парсера. Задачу пока не закрываем.

Also available in: Atom PDF