Project

General

Profile

Task #10764

Поддержка алтернативного формата вывода SMT-LIB представления машинного кода

Added by Pavel Putro about 2 months ago.

Status:
New
Priority:
Normal
Category:
-
Target version:
-
Start date:
03/23/2021
Due date:
% Done:

0%

Estimated time:
Detected in build:
git
Published in build:

Description

Для использования в рамках задачи 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))))

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

No data to display

Also available in: Atom PDF