論文の概要: PTE: Axiomatic Semantics based Compiler Testing
- arxiv url: http://arxiv.org/abs/2401.01036v1
- Date: Tue, 2 Jan 2024 04:50:47 GMT
- ステータス: 処理完了
- システム内更新日: 2024-01-03 14:46:38.626449
- Title: PTE: Axiomatic Semantics based Compiler Testing
- Title(参考訳): PTE: Axiomatic Semantics ベースのコンパイラテスト
- Authors: Guoliang Dong, Jun Sun, Richard Schumi, Bo Wang, Xinyu Wang
- Abstract要約: 本稿では,PTEと呼ばれるコンパイラテストのための公理的セマンティクスに基づくアプローチを提案する。
その考え方は、emph(textbfprecondition, textbftransformation, textbfexpectation)という形で言語意味論の逸話を捉えた公理の集合を段階的に発展させることである。
- 参考スコア(独自算出の注目度): 7.203331838793759
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The correctness of a compiler affects the correctness of every program
written in the language, and thus must be thoroughly evaluated. Existing
automatic compiler testing methods however either rely on weak oracles (e.g., a
program behaves the same if only dead code is modified), or require substantial
initial effort (e.g., having a complete operational language semantics). While
the former prevents a comprehensive correctness evaluation, the latter makes
those methods irrelevant in practice. In this work, we propose an axiomatic
semantics based approach for testing compilers, called PTE. The idea is to
incrementally develop a set of ``axioms'' capturing anecdotes of the language
semantics in the form of \emph{(\textbf{p}recondition, \textbf{t}ransformation,
\textbf{e}xpectation) triples, which allows us to test the compiler
automatically.} Such axioms are written in the same language whose compiler is
under test, and can be developed either based on the language specification, or
by generalizing the bug reports. PTE has been applied to a newly developed
compiler (i.e., Cangjie) and a mature compiler (i.e., Java), and successfully
identified 42 implementation bugs and 9 potential language design issues.
- Abstract(参考訳): コンパイラの正しさは言語で書かれたすべてのプログラムの正しさに影響を与えるため、徹底的に評価する必要がある。
しかし、既存の自動コンパイラテストメソッドは弱いoracle(例えば、デッドコードだけが修正された場合、プログラムは同じように振る舞う)に依存するか、あるいはかなりの初期的労力(例えば、完全な運用言語セマンティクスを持つ)を必要とする。
前者は包括的正当性評価を阻止するが、後者は実際にはそれらの方法を無関係にする。
そこで本研究では,PTEと呼ばれるコンパイラテストのための公理的セマンティクスに基づくアプローチを提案する。
そのアイデアは、言語意味論の逸話を、emph{(\textbf{p}recondition, \textbf{t}ransformation, \textbf{e}xpectation)トリプルという形で段階的に発展させることで、コンパイラの自動テストを可能にします。
このような公理は、コンパイラがテスト中である同じ言語で書かれており、言語仕様に基づいて開発するか、バグレポートを一般化して開発することができる。
PTEは新しく開発されたコンパイラ(Cangjie)と成熟したコンパイラ(Java)に適用され、42の実装バグと9つの潜在的な言語設計問題を特定した。
関連論文リスト
- Developing a Modular Compiler for a Subset of a C-like Language [0.0]
本稿では,C型言語のサブセットに対するモジュール型コンパイラの開発について紹介する。
このモジュラーアプローチにより、開発者は必要に応じてサブセットを追加または削除することで言語を変更でき、最小限のメモリ効率のコンパイラが実現される。
論文 参考訳(メタデータ) (2025-01-08T13:42:54Z) - Finding Missed Code Size Optimizations in Compilers using LLMs [1.90019787465083]
我々は,大規模言語モデルと一連の差分テスト戦略を組み合わせた新しいテスト手法を開発した。
当社のアプローチでは,実装に150行未満のコードが必要です。
現在までに、本番コンパイラの24のバグが報告されている。
論文 参考訳(メタデータ) (2024-12-31T21:47:46Z) - Evolutionary Generative Fuzzing for Differential Testing of the Kotlin
Compiler [14.259471945857431]
JetBrainsが開発したKotlinコンパイラのバグ発見における差分テストの有効性について検討する。
そこで我々は,K1コンパイラとK2コンパイラの入力プログラムを生成するブラックボックス生成手法を提案する。
ケーススタディでは,提案手法がK1とK2のバグを効果的に検出している。
論文 参考訳(メタデータ) (2024-01-12T16:01:12Z) - Extended Paper: API-driven Program Synthesis for Testing Static Typing
Implementations [11.300829269111627]
本稿では,API駆動型プログラム合成の概念に基づいて静的型付けの実装をテストする新しい手法を提案する。
このアイデアは、既存のソフトウェアライブラリから派生したアプリケーションプログラミングインタフェース(API)を活用して組み合わせることで、型集約型だが小さく、十分に型付けされたプログラムを合成することである。
論文 参考訳(メタデータ) (2023-11-08T08:32:40Z) - Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。
確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。
Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
論文 参考訳(メタデータ) (2023-09-25T15:42:18Z) - Natural Language Embedded Programs for Hybrid Language Symbolic Reasoning [84.12154024070024]
本研究では,数学・記号的推論,自然言語理解,後続の課題に対処するための統合フレームワークとして,自然言語組み込みプログラム(NLEP)を提案する。
我々のアプローチは,構造化知識の自然言語表現を含むデータ構造上の関数を定義する完全なPythonプログラムを生成するよう,言語モデルに促す。
Pythonインタープリタが生成されたコードを実行し、出力をプリントする。
論文 参考訳(メタデータ) (2023-09-19T17:54:21Z) - A Static Evaluation of Code Completion by Large Language Models [65.18008807383816]
単純なプログラミング問題に対するモデル生成コードの機能的正当性を評価するために,実行ベースベンチマークが提案されている。
プログラムを実行せずにエラーを検出するlinterのような静的解析ツールは、コード生成モデルを評価するために十分に研究されていない。
抽象構文木を利用して,Pythonのコード補完における静的エラーを定量化する静的評価フレームワークを提案する。
論文 参考訳(メタデータ) (2023-06-05T19:23:34Z) - Effective Random Test Generation for Deep Learning Compilers [16.065653480978092]
Israはドメイン固有の制約解決ツールで、バックトラックなしでセマンティック仕様から制約を解決する。
我々は、TVM、Glow、およびSophGoという商用コンパイラを含む3つの人気のある現実世界のディープラーニングコンパイラに対して、我々のアプローチを実装し、適用する。
Israは、最先端のアプローチや、コンパイラーバグ検出のための有効なテストインプットを構築するためのベースラインアプローチよりも効果的である。
論文 参考訳(メタデータ) (2023-02-02T03:00:36Z) - Interactive Code Generation via Test-Driven User-Intent Formalization [60.90035204567797]
大きな言語モデル(LLM)は、非公式な自然言語(NL)の意図からコードを生成する。
自然言語は曖昧であり、形式的な意味論が欠けているため、正確性の概念を定義するのは難しい。
言語に依存しない抽象アルゴリズムと具体的な実装TiCoderについて述べる。
論文 参考訳(メタデータ) (2022-08-11T17:41:08Z) - Natural Language to Code Translation with Execution [82.52142893010563]
実行結果-プログラム選択のための最小ベイズリスク復号化。
そこで本研究では,自然言語からコードへのタスクにおいて,事前訓練されたコードモデルの性能を向上することを示す。
論文 参考訳(メタデータ) (2022-04-25T06:06:08Z) - Zero-Shot Cross-lingual Semantic Parsing [56.95036511882921]
7つのテスト言語に対する並列データを持たないゼロショット問題として,言語間セマンティックパーシングについて検討した。
英文論理形式ペアデータのみを用いて解析知識を付加言語に転送するマルチタスクエンコーダデコーダモデルを提案する。
このシステムは、ゼロショット解析を潜時空間アライメント問題としてフレーム化し、事前訓練されたモデルを改善し、最小のクロスリンガル転送ペナルティで論理形式を生成することができる。
論文 参考訳(メタデータ) (2021-04-15T16:08:43Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。