| 講演名 | 2022-01-12 LLVM中間表現の意味論規則を表現する制約付き書換え規則について 加藤 拓洋(名大), 西田 直樹(名大), 酒井 正彦(名大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | C言語に沿った簡易プログラミング言語を論理制約付き項書換え系（LCTRS）に変換し，元のプログラムの性質をLCTRSの性質に帰着して検証する手法が研究されている．本稿では，LCTRSへ変換できるプログラミング言語を増やすことをめざし，LLVM中間表現からLCTRSへの変換を提案する．一般に，LLVM中間表現の意味論ではメモリ及び変数への割当てが写像として計算状態に含まれる．一方，写像をデータとして扱わないLCTRSへの既存の変換では写像の値域を関数記号の引数として保持させることになり正当性証明を複雑にする．本稿ではメモリ及び割当てに相当する写像をデータとして扱うLCTRSを用いることで，変換とその正当性証明を簡潔にする．具体的には，プログラムの計算状態から項への単射関数を定義し，LLVM中間表現の各命令とそれに適用可能な各意味論規則に対して，1つの制約付き書換え規則を生成する． |
| 抄録(英) | A method to verify programs written in a simple C-like language via logically constrained term rewrite systems (LCTRS, for short) has been investigated. The method transforms a program into an LCTRS, and reduces properties of the program to those of the transformed LCTRS. In this article, we propose a transformation of LLVM IRs into LCTRSs, aiming at expanding the scope of the method. In the semantics of LLVM IRs, a configuration includes a memory and an assignment as mappings in general. On the other hand, LCTRSs used in the existing work do not deal with such mappings as built-in data, and thus, function symbols keep ranges of memories and assignments as arguments, making the transformation and its correctness proof more complicated. For this reason, we employ LCTRSs that deal with memories and assignments as built-in data, as LLVM IRs do. This makes a correctness proof of our transformation clear. More precisely, we define an injective mapping from configurations to terms. Using the mapping, we propose a transformation that generates a rewrite rule for each instruction in an LLVM IR by instantiating each inference rule of the LLVM-IR semantics which is applicable to the instruction. |
| キーワード(和) | プログラム変換 / 論理制約付き項書換え系 / ビットベクトル算術 |
| キーワード(英) | program transformation / logically constrained term rewrite systems / bit-vector arithmetic |
| 資料番号 | MSS2021-47,SS2021-34 |
| 発行日 | 2022-01-04 (MSS, SS) |
| 研究会情報 | |
| 研究会 | SS / MSS |
|---|---|
| 開催期間 | 2022/1/11(から2日開催) |
| 開催地（和） | 長崎県建設総合会館 |
| 開催地（英） | Nagasakiken-Kensetsu-Sogo-Kaikan Bldg. |
| テーマ（和） | システム数理と応用，ソフトウェアサイエンスおよび一般 |
| テーマ（英） | Mathematical Systems Science and its Applications, Software Science, etc. |
| 委員長氏名（和） | 小林 隆志(東工大) / 尾崎 敦夫(阪工大) |
| 委員長氏名（英） | Takashi Kobayashi(Tokyo Inst. of Tech.) / Atsuo Ozaki(Osaka Inst. of Tech.) |
| 副委員長氏名（和） | 岡野 浩三(信州大) / 山口 真悟(山口大) |
| 副委員長氏名（英） | Kozo Okano(Shinshu Univ.) / Shingo Yamaguchi(Yamaguchi Univ.) |
| 幹事氏名（和） | 島 和之(広島市大) / 林 晋平(東工大) / 小林 孝一(北大) / 劉 健全(NEC) |
| 幹事氏名（英） | Kazuyuki Shima(Hiroshima City Univ.) / Shinpei Hayashi(Tokyo Inst. of Tech.) / Koichi Kobayashi(Hokkaido Univ.) / Jianquan Liui(NEC) |
| 幹事補佐氏名（和） | 小形 真平(信州大) / 白井 匡人(島根大) |
| 幹事補佐氏名（英） | Shinpei Ogata(Shinshu Univ.) / Masato Shirai(Shimane Univ.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Software Science / Technical Committee on Mathematical Systems Science and its Applications |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | LLVM中間表現の意味論規則を表現する制約付き書換え規則について |
| サブタイトル（和） | |
| タイトル（英） | On Constrained Rewrite Rules Representing Semantics Rules of LLVM IR |
| サブタイトル（和） | |
| キーワード(1)（和/英） | プログラム変換 / program transformation |
| キーワード(2)（和/英） | 論理制約付き項書換え系 / logically constrained term rewrite systems |
| キーワード(3)（和/英） | ビットベクトル算術 / bit-vector arithmetic |
| 第 1 著者 氏名（和/英） | 加藤 拓洋 / Takumi Kato |
| 第 1 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 第 2 著者 氏名（和/英） | 西田 直樹 / Naoki Nishida |
| 第 2 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 第 3 著者 氏名（和/英） | 酒井 正彦 / Masahiko Sakai |
| 第 3 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 発表年月日 | 2022-01-12 |
| 資料番号 | MSS2021-47,SS2021-34 |
| 巻番号（vol） | vol.121 |
| 号番号（no） | MSS-317,SS-318 |
| ページ範囲 | pp.89-94(MSS), pp.89-94(SS), |
| ページ数 | 6 |
| 発行日 | 2022-01-04 (MSS, SS) |