A complete pipeline for LLM-based code generation with security analysis using CodeQL and symbolic execution with KLEE - all without requiring administrator privileges.
- LLM Code Generation: DeepSeek/HuggingFace models with automatic caching and cleanup
- CodeQL Security Analysis: Static security analysis with GitHub's CodeQL
- KLEE Symbolic Execution: Comprehensive path exploration and test case generation
- User-Space Installation: No sudo/admin privileges required - username auto-detected
- Unified Pipeline: Single command runs complete generation β analysis workflow
- Smart Code Cleaning: Removes LLM artifacts, comments, and duplicate statements
- Disk Quota Friendly: Uses
/scratchspace and cleans up automatically
- Python 3.11 (system-wide installation)
- CUDA 12.4 (for GPU-accelerated LLM inference)
- Git and basic build tools (gcc, make)
- Internet connection (for downloading dependencies)
git clone <repository-url>
cd basic-rl-feedback-workflowNote: Your username is automatically detected - no manual configuration needed!
chmod +x prerequisites-setup.sh
./prerequisites-setup.shThis will install and build:
- Python 3.11 virtual environment with PyTorch, Transformers, llama-cpp-python
- CodeQL static analysis engine
- CMake, Ninja, LLVM 14.0 (user-space)
- SQLite 3.43.2 (built from source)
- Z3 4.8.15 SMT solver (built from source)
- KLEE symbolic execution engine (built from source)
β±οΈ Installation time: ~30-45 minutes (depending on your system)
# Run the complete pipeline (LLM generation + analysis)
./run_pipeline.sh
# OR run analysis only on existing code
./analyze_only.shComplete Pipeline (run_pipeline.sh):
- Generate C code using LLM (DeepSeek model)
- Clean and process code (remove markdown, duplicates)
- Run CodeQL security analysis to detect vulnerabilities
- Generate LLVM bitcode for symbolic execution
- Execute KLEE analysis with 30-second timeout, generating test cases
./run_pipeline.sh- Generates new C code with LLM
- Analyzes with CodeQL and KLEE
- Everything in one command
./analyze_only.sh- Re-analyzes existing generated code
- Faster - skips LLM generation
- Useful for testing different analysis parameters
Generate Code Only:
python run_llm.py- Output:
generated_code/generated_code.c
View Results:
# View generated code
cat generated_code/generated_code.c
# View KLEE test cases
ls -la klee_output/
/scratch/$(whoami)/klee/build/bin/ktest-tool klee_output/test*.ktest
# View analysis statistics
cat klee_output/infobasic-rl-feedback-workflow/
βββ prerequisites-setup.sh # Complete setup script (auto-detects username)
βββ run_pipeline.sh # Complete LLM + analysis pipeline
βββ analyze_only.sh # Analysis-only pipeline
βββ run_llm.py # LLM code generation
βββ run_codeql.py # CodeQL security analysis
βββ config.json # LLM model and prompt configuration
βββ gpu_requirements.txt # Python dependencies
βββ klee_requirements.txt # System dependencies reference
βββ generated_code/ # All generated and processed code
β βββ generated_code.c # Raw LLM output
β βββ clean_code.c # Cleaned C source
β βββ clean_code.bc # LLVM bitcode
β βββ clean_code.out # Compiled executable
β βββ Makefile # Build configuration
βββ klee_output/ # KLEE symbolic execution results
β βββ test*.ktest # Generated test cases
β βββ info # Execution statistics
β βββ *.err # Error traces (if any)
βββ feedback/ # Analysis feedback and reports
{
"MODEL_PATH": "deepseek-ai/deepseek-coder-1.3b-base",
"max_new_tokens": 512,
"num_return_sequences": 1,
"PROMPT": "write a calculator in C"
}Supported models:
deepseek-ai/deepseek-coder-1.3b-base(default)microsoft/DialoGPT-small- Any HuggingFace model compatible with transformers
All components install to /scratch/your_username/:
- Python Environment:
/scratch/your_username/klee-venv/ - LLVM/Clang:
/scratch/your_username/llvm-14/ - Z3 Solver:
/scratch/your_username/z3-build/ - SQLite:
/scratch/your_username/sqlite/ - KLEE:
/scratch/your_username/klee/build/bin/klee - CodeQL:
/scratch/your_username/codeql/
- Success: Security vulnerabilities found and reported
- No issues: Code passes security analysis
- Build errors: C code compilation issues
- Test Cases:
test*.ktestfiles contain concrete input values - Coverage: Paths explored during symbolic execution
- Errors:
*.errfiles contain error traces and bug reports - Statistics: Execution time, paths explored, queries generated
β KLEE analysis complete: klee_output/
Generated test cases:
Test files: 3
Error files: 1
KLEE Statistics:
Elapsed: 00:00:30
KLEE: done: explored paths = 3
KLEE: done: generated tests = 3
-
Python 3.11 not found
# Install Python 3.11 system-wide (ask admin) sudo yum install python3.11 -
CUDA not available
- Check:
nvidia-smiandnvcc --version - LLM will fall back to CPU mode (slower)
- Check:
-
Build failures during setup
- Check internet connection
- Ensure sufficient disk space (~10GB)
- Re-run setup script (it's resumable)
-
KLEE timeout/no results
- Code may have infinite loops
- External function calls (printf, scanf) limit exploration
- Increase timeout in
analysis.sh
# Test Python environment
source /scratch/$(whoami)/klee-venv/bin/activate
python -c "import torch; print('PyTorch:', torch.__version__)"
python -c "import transformers; print('Transformers:', transformers.__version__)"
# Test KLEE
/scratch/$(whoami)/klee/build/bin/klee --version
# Test CodeQL
/scratch/$(whoami)/codeql/codeql version
# Test complete pipeline
./run_pipeline.shThis tool combines three powerful techniques:
- Large Language Models (LLMs): Generate code from natural language descriptions
- Static Analysis (CodeQL): Find security vulnerabilities without execution
- Symbolic Execution (KLEE): Explore all possible program paths systematically
The goal is to create a secure-by-construction code generation pipeline that:
- Generates functional code with LLMs
- Identifies security issues with static analysis
- Validates correctness with comprehensive testing
The complete secure code generation pipeline is now operational with proper CodeQL security analysis:
- β LLM Generation: DeepSeek models generate C code successfully
- β CodeQL Security Analysis: Full cpp-security-and-quality.qls query suite
- β KLEE Symbolic Execution: Comprehensive path exploration and test generation
- β Unified Pipeline: Single command runs complete workflow
- β Disk Quota Management: Automatic cache cleanup in /scratch/ space
Recent pipeline run generated a calculator program and found 17 security findings:
CodeQL Security Analysis Results
================================
Analyzed with: cpp-security-and-quality.qls
Database: /scratch/user/workflow/codeql_db
Findings (17 total):
[NOTE] cpp/missing-check-scanf: Variables read without proper scanf return value checks
DeepSeek LLM β C Calculator Code β CodeQL Analysis β 17 Security Issues Found β KLEE Test Generation
All components work together seamlessly to provide actionable security feedback for LLM-generated code.
[Your License Here]
[Contribution Guidelines Here] Example RL feedback chain for training LLM. Incorporates feedback from compiler, KLEE, and CodeQL in form of text files accessible by the training program.
-
Setup Environment:
./prerequisites-setup.sh
-
Activate Virtual Environment:
source /scratch/{YOUR_USER_ID}/klee-venv/bin/activate -
Configure Prompt (edit
config.json):{ "PROMPT": "Write a secure C function that safely handles user input" } -
Run Complete Pipeline:
./run_pipeline.sh
Or generate code only:
python run_llm.py
For detailed setup instructions, see SETUP_INSTRUCTIONS.md.
- Python 3.11 + Virtual Environment: Clean, isolated environment
- CUDA Support: GPU-accelerated PyTorch and llama-cpp-python
- Modern Libraries: Updated transformers library (4.57.0+)
- Automated Setup: Single script handles all dependencies