Project

General

Profile

Actions

Bug #9395

closed

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

Added by Pavel Putro over 5 years ago. Updated about 4 years ago.

Status:
Closed
Priority:
Normal
Category:
nML Translator
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")

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


Files

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

Updated by Alexander Kamkin over 5 years ago

  • Status changed from New to Open
Actions #2

Updated by Alexander Kamkin over 5 years ago

  • Assignee set to Artem Kotsynyak
Actions #3

Updated by Alexander Kamkin over 5 years ago

  • Assignee changed from Artem Kotsynyak to Alexander Protsenko

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

Actions #4

Updated by Alexander Protsenko over 5 years ago

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

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

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

Actions #5

Updated by Pavel Putro over 5 years ago

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

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

Actions #6

Updated by Alexander Kamkin over 5 years ago

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

Actions #7

Updated by Alexander Kamkin over 4 years ago

  • Category set to nML Translator
  • Target version set to 2.4
Actions #8

Updated by Alexander Kamkin about 4 years ago

  • Status changed from Open to Closed

Есть отдельная задача #9472.
Закрываем.

Actions

Also available in: Atom PDF