| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2022-01-12 09:40 LLVM中間表現の意味論規則を表現する制約付き書換え規則について ○加藤拓洋・西田直樹・酒井正彦（名大）  MSS2021-47 SS2021-34 |
|
| 抄録 | （和） | 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 / / / / / | |
| 文献情報 | 信学技報, vol. 121, no. 318, SS2021-34, pp. 89-94, 2022年1月. | |
| 資料番号 | SS2021-34 | |
| 発行日 | 2022-01-04 (MSS, SS) | |
| ISSN | Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| 査読に ついて |
本技術報告は査読を経ていない技術報告であり，推敲を加えられていずれかの場に発表されることがあります． | |
| PDFダウンロード | MSS2021-47 SS2021-34 |
|
| 研究会情報 | |
| 研究会 | SS MSS |
| 開催期間 | 2022-01-11 - 2022-01-12 |
| 開催地（和） | 長崎県建設総合会館 |
| 開催地（英） | Nagasakiken-Kensetsu-Sogo-Kaikan Bldg. |
| テーマ（和） | システム数理と応用，ソフトウェアサイエンスおよび一般 |
| テーマ（英） | Mathematical Systems Science and its Applications, Software Science, etc. |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2022-01-SS-MSS |
| 本文の言語 | 日本語 |
| タイトル（和） | LLVM中間表現の意味論規則を表現する制約付き書換え規則について |
| サブタイトル（和） | |
| タイトル（英） | On Constrained Rewrite Rules Representing Semantics Rules of LLVM IR |
| サブタイトル（英） | |
| キーワード(1)（和/英） | プログラム変換 / program transformation |
| キーワード(2)（和/英） | 論理制約付き項書換え系 / logically constrained term rewrite systems |
| キーワード(3)（和/英） | ビットベクトル算術 / bit-vector arithmetic |
| キーワード(4)（和/英） | / |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 加藤 拓洋 / Takumi Kato / カトウ タクミ |
| 第1著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 西田 直樹 / Naoki Nishida / ニシダ ナオキ |
| 第2著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 酒井 正彦 / Masahiko Sakai / サカイ マサヒコ |
| 第3著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第4著者 氏名（和/英/ヨミ） | / / |
| 第4著者 所属（和/英） | (略称： ) (略称： ) |
| 第5著者 氏名（和/英/ヨミ） | / / |
| 第5著者 所属（和/英） | (略称： ) (略称： ) |
| 第6著者 氏名（和/英/ヨミ） | / / |
| 第6著者 所属（和/英） | (略称： ) (略称： ) |
| 第7著者 氏名（和/英/ヨミ） | / / |
| 第7著者 所属（和/英） | (略称： ) (略称： ) |
| 第8著者 氏名（和/英/ヨミ） | / / |
| 第8著者 所属（和/英） | (略称： ) (略称： ) |
| 第9著者 氏名（和/英/ヨミ） | / / |
| 第9著者 所属（和/英） | (略称： ) (略称： ) |
| 第10著者 氏名（和/英/ヨミ） | / / |
| 第10著者 所属（和/英） | (略称： ) (略称： ) |
| 第11著者 氏名（和/英/ヨミ） | / / |
| 第11著者 所属（和/英） | (略称： ) (略称： ) |
| 第12著者 氏名（和/英/ヨミ） | / / |
| 第12著者 所属（和/英） | (略称： ) (略称： ) |
| 第13著者 氏名（和/英/ヨミ） | / / |
| 第13著者 所属（和/英） | (略称： ) (略称： ) |
| 第14著者 氏名（和/英/ヨミ） | / / |
| 第14著者 所属（和/英） | (略称： ) (略称： ) |
| 第15著者 氏名（和/英/ヨミ） | / / |
| 第15著者 所属（和/英） | (略称： ) (略称： ) |
| 第16著者 氏名（和/英/ヨミ） | / / |
| 第16著者 所属（和/英） | (略称： ) (略称： ) |
| 第17著者 氏名（和/英/ヨミ） | / / |
| 第17著者 所属（和/英） | (略称： ) (略称： ) |
| 第18著者 氏名（和/英/ヨミ） | / / |
| 第18著者 所属（和/英） | (略称： ) (略称： ) |
| 講演者 | 第1著者 |
| 発表日時 | 2022-01-12 09:40:00 |
| 発表時間 | 25分 |
| 申込先研究会 | SS |
| 資料番号 | MSS2021-47, SS2021-34 |
| 巻番号（vol） | vol.121 |
| 号番号（no） | no.317(MSS), no.318(SS) |
| ページ範囲 | pp.89-94 |
| ページ数 | 6 |
| 発行日 | 2022-01-04 (MSS, SS) |
[研究会発表申込システムのトップページに戻る]