---
# System prepended metadata

title: ToDo List for TermCOMP 2025

---

# ToDo List for TermCOMP 2025
- [x] 参加登録
  - [x] termcompのホームページで情報収集
      - 逐一確認
  - [x] メーリングリストの過去のメールを読む
  - [x] Docker Hubへイメージをプッシュする
  - [x] [このレポジトリ](https://github.com/TermCOMP/registration)にPRを送る
      - [こちら](https://termination-portal.org/wiki/Termination_Competition_2025_technical_details)を参照
- [x] ベンチマーク実行の準備
  - [x] ベンチマークを入手する
      - 既にサブモジュールへ追加済みの[リポジトリ](https://github.com/TermCOMP/TPDB)からpull
  - [x] 過去のベンチマーク用スクリプトの再利用
      - 2020用のスクリプトらしきものは存在を確認済み
      - 2022, 2024用もどこかに存在？
      - [x] [このDockerfile](https://bitbucket.org/uhiro/fptprove/src/develop/cav21ae_dt/Dockerfile?at=develop)の修正
          - [x] z3とllvm2KITTeLのC++互換性問題
          - [x] libsvmのビルドエラー
  - [x] 今年の大会に合わせた実行環境を整える
      - [ホームページの案内](https://termination-portal.org/wiki/Termination_Competition_2025_technical_details)に従って環境構築
          - [x] apptainerの動作確認
              - [x] AWSでは動作せず
          - [x] コンテナ内で`solver`コマンドを呼び出せるようにする
              - [x] `--name`、`--timeout`引数の処理
              - [x] `--category`引数の処理
                  - [x] `--category=C`が未対応
      - 去年のStarExecからRWTH HPC clusterへ移行

- [ ] ソルバの改良・修正
    - [ ] llvm2kittelのバグ修正(門馬)
      - [ ] 一部入力に対して出力されない
      - [ ] 無限ループ + mallocでOut of Memory→visitBBで無限ループ？
      - [ ] segmentation faultの原因調査
    - [x] 再帰関数のサポート(植原)
        - [x] 前処理でLLVM IR上のtail callをbrに置き換える
            - tail callのうち再帰呼び出しのものを検出する
            - 関数のentry blockにはbrできない→ループヘッダの作成、一部命令の移動
            - 再帰呼出し時に引数を上書き→定数（レジスタ）から変数（メモリ）への移行
        - [ ] 複数のtail call/returnが存在する場合にループ展開しきれない
            - 現状は最初の1つのtail callのみをループ展開する
            - 発見した末尾再帰のtail callを一旦vectorに集め、ループでまとめて処理する
        - [ ] `opt -tailcallelim`で末尾再帰でないものもtail callになる？
            - `-tailcallelim`の仕様を調査する必要
            - tail callの検出も自前で実装した方が良い？
        - [ ] 可読性/保守性向上のためのリファクタリング
            - 1つの大きい関数から複数の小さい関数へ分割する
            - main.cppへの直書きから独立したファイルへ移動
    - [ ] C言語のundefined behaviorのサポート
        - [ ] 運営の最初の実行を待ってから対策を考える
- [x] ベンチマーク実行
    - [x] C
    - [x] Integer transition
- [ ] 他分野への検討
- [ ] 性能向上