Skip to content

jefremof/AgdaCSA

BranchesTags

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

22 Commits
.github/workflows
.github/workflows
 
 
src
src
 
 
tests
tests
 
 
AgdaCSA.agda-lib
AgdaCSA.agda-lib
 
 
README.md
README.md
 
 

Repository files navigation

Roadmap

Прямо сейчас модуль с трансляцией представляет собой полный бардак, и нуждается в исправлении Следующая версия внесёт изменения:

  • Более компактный парсинг, с использованием всех преимуществ зависимой типизации
  • Inline-тесты, которые выполняются на этапе контроля типов
  • Косметические улучшения: исправленный нейминг, соблюдение рекомендованного кодстайла
  • Улучшенный cli
  • Парсинг JSON с помощью комбинаторного парсера

Brainfuck. Транслятор и модель

  • Ефремов Марк Андреевич, P3234
  • bf_lang -> bf_asm | bf_isa | harv | hw | instr | struct | stream | port | - | - | -
  • Базовый вариант.

Реализация примера на Agda.

Язык программирования

program ::= term

term ::= symbol
       | comment
       | term term
       | "[" term "]"

symbol ::= ">" | "<" | "+" | "-" | "." | ","

comment ::= <any symbols except: "><+-.,[]">

Код выполняется последовательно. Операции:

  • + -- увеличить значение в текущей ячейке на 1
  • - -- уменьшить значение в текущей ячейке на 1
  • > -- перейти к следующей ячейке
  • < -- перейти к предыдущей ячейке
  • . -- напечатать значение из текущей ячейки (символ)
  • , -- ввести извне значение и сохранить в текущей ячейке (символ)
  • [ -- если значение текущей ячейки ноль, перейти вперёд по тексту программы на символ, следующий за соответствующей ] (с учётом вложенности)
  • ] -- если значение текущей ячейки не ноль, перейти назад по тексту программы на символ [ (с учётом вложенности)

Любые другие символы трактуются как комментарии.

Память выделяется статически, при запуске модели. Видимость данных -- глобальная. Поддержка литералов -- отсутствует.

Организация памяти

Модель памяти процессора (приведено списком, так как тривиальна):

  1. Память команд. Машинное слово -- не определено. Реализуется списком словарей, описывающих инструкции (одно слово -- одна ячейка).
  2. Память данных. Машинное слово -- 8 бит, знаковое. Линейное адресное пространство. Реализуется списком чисел.

В связи с отсутствием на уровне языка переменных, констант, литералов и т.д., описание механизмов работы с ними -- отсутствует. Содержание раздела -- смотри в задании.

Система команд

Особенности процессора:

  • Машинное слово -- 8 бит, знаковое.
  • Доступ к памяти данных осуществляется по адресу, хранящемуся в специальном регистре data_address. Установка адреса осуществляется путём инкрементирования или декрементирования инструкциями < и >.
  • Обработка данных осуществляется по текущему адресу операциями + и -, а также через ввод/вывод.
  • Поток управления:
    • инкремент PC после каждой инструкции;
    • условный (jz) и безусловный (jmp) переходы (использование см. в разделе транслятор).

Набор инструкций

Язык Инструкция Кол-во тактов Описание
+ increment 2 увеличить значение в текущей ячейке на 1
- decrement 2 уменьшить значение в текущей ячейке на 1
< left 1 перейти к следующей ячейке
> right 1 перейти к предыдущей ячейке
. print 2 напечатать значение из текущей ячейки (символ)
, input 2 ввести извне значение и сохранить в текущей ячейке (символ)
jmp <addr> 1 безусловный переход
jz <addr> 2 переход, если в текущей ячейке 0
halt 0 остановка
  • <addr> -- исключительно непосредственная адресация памяти команд.

Кодирование инструкций

  • Машинный код сериализуется в список JSON.
  • Один элемент списка -- одна инструкция.
  • Индекс списка -- адрес инструкции. Используется для команд перехода.

Пример:

[
    {
        "opcode": "jz",
        "arg": 5,
        "term": [
            1,
            5,
            "]"
        ]
    }
]

где:

  • opcode -- строка с кодом операции;
  • arg -- аргумент (может отсутствовать);
  • term -- информация о связанном месте в исходном коде (если есть).

Типы данных в модуле isa, где:

  • Opcode -- перечисление кодов операций;

  • Term -- структура для описания значимого фрагмента кода исходной программы.

  • Instr n -- внутреннее представление для инструкций. n - количество инструкций в программе, операции перехода, вроде jmp или jz принимают в качестве аргумента значение типа Fin n. Это позволяет ещё на этапе компиляции убедиться, что jmp и jz действительно совершают переход только в рамках программы.

Транслятор

Интерфейс командной строки: translatorMain <input_file> <target_file>

Реализовано в модуле: translatorMain

Этапы трансляции (функция translate):

  1. Трансформирование текста в последовательность значимых термов.
  2. Проверка корректности программы (парность квадратных скобок).
  3. Генерация машинного кода.

Правила генерации машинного кода:

  • один символ языка -- одна инструкция;

  • для команд, однозначно соответствующих инструкциям, -- прямое отображение;

  • для циклов с соблюдением парности (многоточие -- произвольный код):

    Номер команды/инструкции Программа Машинный код
    n [ JZ (k+1)
    ... ... ...
    k ] JMP n
    k+1 ... ...

Примечание: вопросы отображения переменных на регистры опущены из-за отсутствия оных.

Модель процессора

Интерфейс командной строки: machineMain <machine_code_file> <input_file> [DEBUG|INFO|WARNING]

Реализовано в модуле: machineMain.

DataPath

     latch --------->+--------------+  addr   +--------+
     data            | data-address |---+---->|  data- |
     addr      +---->+--------------+   |     | memory |
               |                        |     |        |
           +-------+                    |     |        |
    sel -->|  MUX  |         +----------+     |        |
           +-------+         |                |        |
            ^     ^          |                |        |
            |     |          |       data_in  |        | data_out
            |     +---(+1)---+          +---->|        |-----+
            |                |          |     |        |     |
            +---------(-1)---+          |  oe |        |     |
                                        | --->|        |     |
                                        |     |        |     |
                                        |  wr |        |     |
                                        | --->|        |     |
                                        |     +--------+     |
                                        |                    v
                                    +--------+  latch_acc +-----+
                          sel ----> |  MUX   |  --------->| acc |
                                    +--------+            +-----+
                                     ^   ^  ^                |
                                     |   |  |                +---(==0)---> flag-zero
                                     |   |  |                |
                                     |   |  +---(+1)---------+
                                     |   |                   |
                                     |   +------(-1)---------+
                                     |                       |
            input -------------------+                       +---------> output

Реализован в record DataPath.

data-memory-size -- размер памяти. data-memory -- однопортовая память, поэтому либо читаем, либо пишем.

data-address -- адрес выбранной ячейки памяти. Предоставлен типом Fin data-memory-size для гарантии того, что индекс находится в рамках размера памяти.

Сигналы (обрабатываются за один такт, реализованы в виде функций):

  • latch-data-addr -- защёлкнуть выбранное значение в data-address;
  • latch-acc -- защёлкнуть в аккумулятор выход памяти данных;
  • signal-wr -- записать выбранное значение в память:
    • инкрементированное;
    • декрементированное;
    • с порта ввода input (обработка на Agda):
      • извлечь из входного буфера значение и записать в память;
      • если буфер пуст -- функция завершается неудачей и возвращает nothing;
  • output -- записать аккумулятор в порт вывода (обработка на Agda).

Флаги:

  • zero-flag -- отражает наличие нулевого значения в аккумуляторе.

ControlUnit

   +------------------(+1)-------+
   |                             |
   |    latch_program_counter    |
   |                  |          |
   |   +-----+        v          |
   +-->|     |     +---------+   |    +---------+
       | MUX |---->| program |---+--->| program |
   +-->|     |     | counter |        | memory  |
   |   +-----+     +---------+        +---------+
   |      ^                               |
   |      | sel_next                      | current instruction
   |      |                               |
   +---------------(select-arg)-----------+
          |                               |      +---------+
          |                               |      |  step   |
          |                               |  +---| counter |
          |                               |  |   +---------+
          |                               v  v        ^
          |                       +-------------+     |
          +-----------------------| instruction |-----+
                                  |   decoder   |
                                  |             |<-------+
                                  +-------------+        |
                                          |              |
                                          | signals      |
                                          v              |
                                    +----------+  zero   |
                                    |          |---------+
                                    | DataPath |
                     input -------->|          |----------> output
                                    +----------+

Реализован в классе ControlUnit.

  • Hardwired (реализовано полностью на Agda).
  • Метод executeStep моделирует выполнение полного цикла инструкции (1-2 такта процессора).
  • step_counter необходим для многотактовых инструкций;

Сигнал:

  • latch-program-counter -- сигнал для обновления счётчика команд в ControlUnit.

Особенности работы модели:

  • Цикл симуляции осуществляется в функции runsteps.
  • Шаг моделирования соответствует одной инструкции с выводом состояния в журнал.
  • Для журнала состояний процессора используется собственная реализация Logging.
  • Количество инструкций для моделирования лимитировано.
  • Остановка моделирования осуществляется при:
    • превышении лимита количества выполняемых инструкций;
    • если нет данных для чтения из порта ввода;
    • если выполнена инструкция halt.

Тестирование

Тестирование выполняется при помощи golden test-ов.

  1. Тесты для языка bf реализованы в: goldentest.

Запустить тесты: goldentest <testing root dir> <translator> <machine> В директории <testing root dir> должен хранится файл tests.txt, в котором на каждой строке указано название теста. В директории <testing root dir>/<test name>/ должно храниться три файла:

  • source.txt (программа на bf)
  • input.txt (пользовательский ввод)
  • expected.txt (эталонн работы)

Обновить конфигурацию golden tests: goldentest <testing root dir> <translator> <machine> DEBUG TRUE

CI при помощи Github Action:

name: basic
on:
  push:
    branches: ['main']
jobs:
  check:
    name: Check hello-world-dep.agda
    runs-on: ubuntu-latest # or macOS-latest, or windows-latest
    steps:
      - uses: actions/checkout@v3

      - uses: wenkokke/setup-agda@v2
        with:
          agda-version: '2.6.4.3'
          agda-stdlib-version: '2.0'

      # Check hello-world-dep.agda, which you can find in tests/agda-stdlib:
      - run: |
          agda --compile-dir=build/ -c src/goldentest.agda
          agda --compile-dir=build/ -c src/machineMain.agda
          agda --compile-dir=build/ -c src/translatorMain.agda
        working-directory: .
      - run: ./build/goldentest ./tests/ ./build/translatorMain ./build/machineMain
        working-directory: .

На данный момент для Agda не существует линтеров, но есть набор рекоммендаций к оформлению кода.

Пример использования и журнал работы процессора на примере cat: Тест - cat

Исходный код - ,[.,] Транслировался в 6 инструкций, где [ заменилась на {"opcode": "jz", "arg": 5, "term": [0,1,'[']}, а ] на {"opcode": "jmp", "arg": 1, "term": [0,4,']']}.

Результат - содержимое файла input.txt - foo.

$ cat tests/cat/input.txt
foo
$ cat tests/cat/source.txt
,[.,]
$ ./build/translatorMain tests/cat/source.txt tests/cat/temp.txt
$ cat tests/cat/temp.txt
[{"opcode": "input", "term": [0,0,',']},{"opcode": "jz", "arg": 5, "term": [0,1,'[']},{"opcode": "print", "term": [0,2,'.']},{"opcode": "input", "term": [0,3,',']},{"opcode": "jmp", "arg": 1, "term": [0,4,']']},{"opcode": "halt"}]⏎
$ ./build/machineMain tests/cat/temp.txt tests/cat/input.txt
DEBUG   input: 'f'
DEBUG   TICK:   2  PC:    1  ADDR:    0  MEM_OUT:  102  ACC:  0          jz  [0,1,'[']
DEBUG   TICK:   4  PC:    2  ADDR:    0  MEM_OUT:  102  ACC:  102        print  [0,2,'.']
DEBUG   output: '' << 'f'
DEBUG   TICK:   6  PC:    3  ADDR:    0  MEM_OUT:  102  ACC:  102        input  [0,3,',']
DEBUG   input: 'o'
DEBUG   TICK:   8  PC:    4  ADDR:    0  MEM_OUT:  111  ACC:  102        jmp  [0,4,']']
DEBUG   TICK:   9  PC:    1  ADDR:    0  MEM_OUT:  111  ACC:  102        jz  [0,1,'[']
DEBUG   TICK:   11  PC:    2  ADDR:    0  MEM_OUT:  111  ACC:  111       print  [0,2,'.']
DEBUG   output: 'f' << 'o'
DEBUG   TICK:   13  PC:    3  ADDR:    0  MEM_OUT:  111  ACC:  111       input  [0,3,',']
DEBUG   input: 'o'
DEBUG   TICK:   15  PC:    4  ADDR:    0  MEM_OUT:  111  ACC:  111       jmp  [0,4,']']
DEBUG   TICK:   16  PC:    1  ADDR:    0  MEM_OUT:  111  ACC:  111       jz  [0,1,'[']
DEBUG   TICK:   18  PC:    2  ADDR:    0  MEM_OUT:  111  ACC:  111       print  [0,2,'.']
DEBUG   output: 'fo' << 'o'
DEBUG   TICK:   20  PC:    3  ADDR:    0  MEM_OUT:  111  ACC:  111       input  [0,3,',']
WARNING   Input buffer is empty!
INFO   output-buffer 'foo'
$ cat tests/cat/input.txt
foo
$ cat tests/cat/source.txt
,[.,]
$ ./build/translatorMain tests/cat/source.txt tests/cat/temp.txt
$ cat tests/cat/temp.txt
[{"opcode": "input", "term": [0,0,',']},{"opcode": "jz", "arg": 5, "term": [0,1,'[']},{"opcode": "print", "term": [0,2,'.']},{"opcode": "input", "term": [0,3,',']},{"opcode": "jmp", "arg": 1, "term": [0,4,']']},{"opcode": "halt"}]⏎
$ ./build/machineMain tests/cat/temp.txt tests/cat/input.txt INFO
WARNING   Input buffer is empty!
INFO   output-buffer 'foo'

Пример проверки исходного кода:

$ .\goldentest tests\ ".\translatorMain" ".\machineMain"
Test 1 cat
SUCCESS

Test 2 hello
SUCCESS
| ФИО                            | алг   | LoC | code байт | code инстр. | инстр. | такт. | вариант |
| Ефремов Марк Андреевич         | hello | 43  | -         | 131         | 131    | 1532  | bf_lang -> bf_asm | bf_isa | harv | hw | instr | struct | stream | port | - | - | -     |
| Ефремов Марк Андреевич         | cat   | 1   | -         | 6           | 11     | 21    | bf_lang -> bf_asm | bf_isa | harv | hw | instr | struct | stream | port | - | - | -     |

About

No description, website, or topics provided.

Resources

Readme
Activity

Stars

0 stars

Watchers

1 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published

Languages