TIS-Chiron

AI-powered driver generation for TrustInSoft Analyzer.

Overview

TIS-Chiron is a CLI tool that uses LLMs to automatically generate verification drivers for C functions. It integrates with TrustInSoft Analyzer to validate the generated drivers through a refinement loop.

Requirements

• Python 3.10+
• TrustInSoft Analyzer installed (locally or on a remote machine)
• OpenAI API key

Installation

1. Clone the repository

git clone <repository-url>
cd tis-chiron

2. Create a virtual environment (recommended)

python3 -m venv venv
source venv/bin/activate  # On Windows: venv\Scripts\activate

3. Install the package

pip install -e .

4. Configure environment variables

Create a .env file in the project root:

OPENAI_API_KEY=sk-your-openai-api-key

Security note: Never commit the .env file. Add it to .gitignore.

5. Verify installation

tischiron --help

Usage

Initialize a project

First, obtain a compile_commands.json from your C project (generated by CMake, Bear, or similar tools).

# Basic initialization
tischiron init compile_commands.json

# With custom project name
tischiron init compile_commands.json --name my-project -v

List projects and files

# List all projects
tischiron list

# List files in a project
tischiron list my-project

# Verbose output (shows paths and includes)
tischiron list my-project -v

Generate a driver

# Basic usage
tischiron gen <project> <filename> <function>

# Example
tischiron gen json-c json_object.c json_object_equal

# Full example with all options
tischiron gen json-c json_object.c json_object_equal \
  --with-logs \
  --context function \
  --output drivers/my_driver.c \
  --model gpt-4o-mini \
  --max-iterations 3 \
  -v

CLI Reference

tischiron init <compile_commands.json> [options]
  --name, -n          Project name (default: derived from directory)
  --verbose, -v       Verbose output

tischiron list [project] [options]
  project             Project name (omit to list all)
  --verbose, -v       Verbose output

tischiron gen <project> <filename> <function> [options]
  --output, -o        Output file path
  --model             LLM model (default: gpt-4o-mini)
  --max-iterations    Max refinement iterations (default: 5)
  --context           Context mode (default: function):
                        function  - extracted function only
                        source    - full source file
                        matching  - source + matching header
                        full      - all headers
                        ast       - use AST index for factory functions
  --log, -l           Path to log file for detailed workflow logging
  --with-logs         Enable structured logging to logs/log_<timestamp>/
  --ollama-url        Ollama server URL (default: http://localhost:11434)
  --verbose, -v       Verbose output

tischiron context <project> <function> [options]
  --verbose, -v       Show full context (debug command)

tischiron reindex <project>
  Rebuild AST index for a project

Supported models:
  OpenAI:  gpt-4o-mini, gpt-4o
  Ollama:  llama3.2, mistral, codellama, deepseek-coder, gemma, phi, qwen, etc.

  Models are auto-detected: names starting with llama, mistral, gemma, etc. use Ollama.

How It Works

1. Parse - Reads compile_commands.json to extract source files, include paths, and defines
2. Index - Builds AST index of function declarations to detect factory functions and types
3. Plan - Analyzes the target function and prepares generation context
4. Generate - Uses LLM to generate a TIS verification driver
5. Validate - Two-stage validation:
   • Stage 1: Local cc syntax check
   • Stage 2: TIS Analyzer compilation
6. Refine - If validation fails, feeds errors back to LLM for correction
7. Output - Writes the final validated driver to disk

Project Structure

After initialization, project data is stored in .tischiron/:

.tischiron/
└── projects/
    └── my-project/
        ├── project.json       # Project config
        └── files/
            ├── main.c.json    # File metadata
            └── utils.c.json

Troubleshooting

OpenAI API errors

• Verify OPENAI_API_KEY is set correctly
• Check API quota and billing status

Driver generation fails repeatedly

• Try increasing --max-iterations
• Use a more capable model: --model gpt-4o
• Check if the function has complex dependencies
• Use --with-logs to see detailed error information

---

Optional: Remote TIS via SSH

If TrustInSoft Analyzer is installed on a remote machine, you can configure SSH access.

SSH Environment Variables

Add these to your .env file:

OPENAI_API_KEY=sk-your-openai-api-key

# SSH configuration for remote TIS
SSH_HOST=192.168.1.100
SSH_USER=username
SSH_PASSWORD=your_ssh_password

# TIS environment setup command (run on remote before tis-analyzer)
TIS_ENV_SCRIPT="source /opt/tis/bin/tis-env --source && tis_choose main"

Initialize with SSH settings

tischiron init compile_commands.json \
  --ssh-host 192.168.1.100 \
  --ssh-user myuser \
  --tis-env-script "source /opt/tis/bin/tis-env --source && tis_choose main"

SSH CLI options

tischiron init <compile_commands.json> [options]
  --ssh-host          SSH host for remote TIS
  --ssh-user          SSH username
  --tis-env-script    Script to source TIS environment

Configuration Priority

SSH and TIS settings are resolved in this order (first match wins):

1. Project configuration (stored during init)
2. Environment variables (SSH_HOST, SSH_USER, SSH_PASSWORD, TIS_ENV_SCRIPT)

SSH Troubleshooting

SSH connection fails:

• Verify SSH credentials in .env or CLI arguments
• Ensure the remote host is reachable: ssh user@host
• Check firewall settings

TIS Analyzer not found:

• Ensure tis-env-script is correctly set to source the TIS environment
• Example: --tis-env-script "source /opt/tis/bin/tis-env --source && tis_choose main"

---

Optional: Shell Completion

The CLI supports tab completion for bash, zsh, and fish.

Bash (add to ~/.bashrc):

eval "$(register-python-argcomplete tischiron)"

Zsh (add to ~/.zshrc):

autoload -U bashcompinit
bashcompinit
eval "$(register-python-argcomplete tischiron)"

Fish:

register-python-argcomplete --shell fish tischiron | source

Global activation (all argcomplete-enabled scripts):

activate-global-python-argcomplete

After adding the line, restart your shell or run source ~/.bashrc (or ~/.zshrc).

Completion features:

• Project names: tischiron list <TAB>, tischiron gen <TAB>
• Filenames within project: tischiron gen myproject <TAB>
• Model names: tischiron gen proj file func --model <TAB>

---

Development

Install dev dependencies

pip install -e ".[dev]"

Run tests

pytest -v

Project layout

tis_driver_agent/
├── __init__.py
├── cli.py              # CLI entry point
├── config.py           # Configuration dataclasses
├── state.py            # LangGraph state schema
├── graph.py            # LangGraph workflow
├── cc.py               # Local C compiler validation
├── workflow_logger.py  # Detailed workflow logging
├── builtins.c          # TIS builtins implementation
├── nodes/              # LangGraph nodes
│   ├── planner.py
│   ├── skeleton.py     # TIS skeleton extraction
│   ├── router.py
│   ├── generator.py
│   ├── validator.py
│   └── refiner.py
├── models/             # LLM adapters
│   ├── openai_adapter.py
│   └── ollama_adapter.py
├── tis/                # TIS runner (local/remote)
│   ├── base.py
│   ├── local.py
│   └── remote.py
├── utils/              # Utilities
│   ├── compilation_db.py
│   ├── context_detector.py
│   └── project_manager.py
├── prompts/            # LLM prompt templates
│   └── templates.py
├── stubs/              # TIS header stubs
│   └── tis_builtin.h
└── context/            # AST indexing for context assembly
    ├── parser.py       # C function declaration parser
    ├── index.py        # AST index builder
    ├── lookup.py       # Factory function lookup
    ├── assembler.py    # Context assembly from index
    └── models.py       # Data models for index

License

[Add license information]