| Presentation | 2022-01-12 On Constrained Rewrite Rules Representing Semantics Rules of LLVM IR Takumi Kato, Naoki Nishida, Masahiko Sakai, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | 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. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | program transformation / logically constrained term rewrite systems / bit-vector arithmetic |
| Paper # | MSS2021-47,SS2021-34 |
| Date of Issue | 2022-01-04 (MSS, SS) |
| Conference Information | |
| Committee | SS / MSS |
|---|---|
| Conference Date | 2022/1/11(2days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | Nagasakiken-Kensetsu-Sogo-Kaikan Bldg. |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | Mathematical Systems Science and its Applications, Software Science, etc. |
| Chair | Takashi Kobayashi(Tokyo Inst. of Tech.) / Atsuo Ozaki(Osaka Inst. of Tech.) |
| Vice Chair | Kozo Okano(Shinshu Univ.) / Shingo Yamaguchi(Yamaguchi Univ.) |
| Secretary | Kozo Okano(Hiroshima City Univ.) / Shingo Yamaguchi(Tokyo Inst. of Tech.) |
| Assistant | Shinpei Ogata(Shinshu Univ.) / Masato Shirai(Shimane Univ.) |
| Paper Information | |
| Registration To | Technical Committee on Software Science / Technical Committee on Mathematical Systems Science and its Applications |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | On Constrained Rewrite Rules Representing Semantics Rules of LLVM IR |
| Sub Title (in English) | |
| Keyword(1) | program transformation |
| Keyword(2) | logically constrained term rewrite systems |
| Keyword(3) | bit-vector arithmetic |
| 1st Author's Name | Takumi Kato |
| 1st Author's Affiliation | Nagoya University(Nagoya Univ.) |
| 2nd Author's Name | Naoki Nishida |
| 2nd Author's Affiliation | Nagoya University(Nagoya Univ.) |
| 3rd Author's Name | Masahiko Sakai |
| 3rd Author's Affiliation | Nagoya University(Nagoya Univ.) |
| Date | 2022-01-12 |
| Paper # | MSS2021-47,SS2021-34 |
| Volume (vol) | vol.121 |
| Number (no) | MSS-317,SS-318 |
| Page | pp.pp.89-94(MSS), pp.89-94(SS), |
| #Pages | 6 |
| Date of Issue | 2022-01-04 (MSS, SS) |