MicroTESK

Для использования в рамках задачи SyGuS необходима поддержка формата вывода базовых блоков машинного кода в виде единых функций. Данные функции должны принимать на вход и возвращать единственный параметр типа State, представляющий текущее состояние машины (регистры + память). Тип State должен вычисляться путём анализа NML модели и иметь единый формат для всех базовых блоков.
Тип State должен включать:

1. регистры общего назначения
2. массив памяти
3. регистры специального назначения
4. Флаги (если не встроены в регистры специального назначения)
5. Отдельный булевый параметр - условие перехода.

Тип State не должен включать

1. временные переменные типа tmp_dword и т. п.
2. безымянные промежуточные значения типа %123

Пример определения типа State на SMT-LIB:

(declare-datatypes ((State 0))
  (((cons (XREG (Array (_ BitVec 5) (_ BitVec 32))) (MEM (Array (_ BitVec 32) (_ BitVec 8))) (zf Bool) (sf Bool) (jc Bool)))))

Для удобства использования типа State и сокращения объёма генерируемого кода желательно определить аксессоры для записи и чтения данных:

(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)))

Сама функция в таком случае может быть реализована через цепочку let-выражений в виде:

(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))))

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