You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
844 lines
37 KiB
844 lines
37 KiB
<!DOCTYPE html>
|
|
<html lang="zh-CN">
|
|
<head>
|
|
<meta charset="UTF-8">
|
|
<meta name="viewport" content="width=device-width, initial-scale=1.0">
|
|
<title>CBMC SpecGen - 智能代码验证平台</title>
|
|
<link href="https://cdn.jsdelivr.net/npm/tailwindcss@2.2.19/dist/tailwind.min.css" rel="stylesheet">
|
|
<link href="https://cdnjs.cloudflare.com/ajax/libs/prism/1.29.0/themes/prism-tomorrow.min.css" rel="stylesheet">
|
|
<style>
|
|
.gradient-bg {
|
|
background: linear-gradient(135deg, #667eea 0%, #764ba2 100%);
|
|
}
|
|
.code-editor {
|
|
font-family: 'Monaco', 'Menlo', 'Ubuntu Mono', monospace;
|
|
tab-size: 4;
|
|
}
|
|
.status-running {
|
|
animation: pulse 2s infinite;
|
|
}
|
|
@keyframes pulse {
|
|
0%, 100% { opacity: 1; }
|
|
50% { opacity: 0.7; }
|
|
}
|
|
.result-card {
|
|
max-height: 400px;
|
|
overflow-y: auto;
|
|
}
|
|
pre[class*="language-"] {
|
|
background: #2d2d2d;
|
|
margin: 0;
|
|
padding: 1em;
|
|
border-radius: 0.5em;
|
|
}
|
|
.file-upload-area {
|
|
border: 2px dashed #cbd5e0;
|
|
border-radius: 0.5rem;
|
|
transition: all 0.3s ease;
|
|
background: linear-gradient(135deg, #f8fafc 0%, #f1f5f9 100%);
|
|
}
|
|
.file-upload-area:hover {
|
|
border-color: #4299e1;
|
|
background: linear-gradient(135deg, #ebf8ff 0%, #dbeafe 100%);
|
|
transform: translateY(-1px);
|
|
box-shadow: 0 4px 12px rgba(0, 0, 0, 0.1);
|
|
}
|
|
.file-upload-area.dragover {
|
|
border-color: #3182ce;
|
|
background: linear-gradient(135deg, #bee3f8 0%, #90cdf4 100%);
|
|
transform: scale(1.02);
|
|
box-shadow: 0 8px 25px rgba(59, 130, 246, 0.15);
|
|
}
|
|
.file-input-hidden {
|
|
display: none;
|
|
}
|
|
.upload-icon {
|
|
animation: float 3s ease-in-out infinite;
|
|
}
|
|
@keyframes float {
|
|
0%, 100% { transform: translateY(0px); }
|
|
50% { transform: translateY(-10px); }
|
|
}
|
|
.file-info-card {
|
|
background: linear-gradient(135deg, #e0f2fe 0%, #bae6fd 100%);
|
|
border-left: 4px solid #0ea5e9;
|
|
}
|
|
</style>
|
|
</head>
|
|
<body class="bg-gray-50">
|
|
<!-- Header -->
|
|
<header class="gradient-bg text-white shadow-lg">
|
|
<div class="container mx-auto px-4 py-6">
|
|
<div class="flex items-center justify-between">
|
|
<div>
|
|
<h1 class="text-3xl font-bold">CBMC SpecGen</h1>
|
|
<p class="text-blue-100 mt-2">基于大语言模型的C/C++智能代码验证平台</p>
|
|
</div>
|
|
<div class="flex items-center space-x-4">
|
|
<button onclick="loadSystemInfo()" class="bg-white text-purple-600 px-4 py-2 rounded-lg hover:bg-blue-50 transition">
|
|
🔄 系统状态
|
|
</button>
|
|
</div>
|
|
</div>
|
|
</div>
|
|
</header>
|
|
|
|
<!-- Main Content -->
|
|
<main class="container mx-auto px-4 py-8">
|
|
<!-- System Info Card -->
|
|
<div id="systemInfo" class="bg-white rounded-lg shadow-md p-6 mb-8 hidden">
|
|
<h2 class="text-xl font-bold mb-4">系统信息</h2>
|
|
<div class="grid grid-cols-1 md:grid-cols-3 gap-4">
|
|
<div class="text-center">
|
|
<div class="text-3xl font-bold text-blue-600" id="cbmcVersion">-</div>
|
|
<div class="text-gray-600">CBMC版本</div>
|
|
</div>
|
|
<div class="text-center">
|
|
<div class="text-3xl font-bold text-green-600" id="activeTasks">0</div>
|
|
<div class="text-gray-600">活跃任务</div>
|
|
</div>
|
|
<div class="text-center">
|
|
<div class="text-3xl font-bold text-purple-600" id="completedTasks">0</div>
|
|
<div class="text-gray-600">完成任务</div>
|
|
</div>
|
|
</div>
|
|
</div>
|
|
|
|
<!-- Input Section -->
|
|
<div class="bg-white rounded-lg shadow-md p-6 mb-8">
|
|
<div class="flex items-center justify-between mb-4">
|
|
<h2 class="text-xl font-bold">📝 代码输入</h2>
|
|
<div class="flex space-x-2">
|
|
<button onclick="loadDemo()" class="bg-gray-600 text-white px-4 py-2 rounded hover:bg-gray-700 transition">
|
|
📋 加载示例
|
|
</button>
|
|
<button onclick="clearInput()" class="bg-red-600 text-white px-4 py-2 rounded hover:bg-red-700 transition">
|
|
🗑️ 清空
|
|
</button>
|
|
</div>
|
|
</div>
|
|
|
|
<div class="mb-4">
|
|
<label class="block text-gray-700 text-sm font-bold mb-2">
|
|
C/C++ 代码:
|
|
</label>
|
|
|
|
<!-- 文件上传区域 -->
|
|
<div id="fileUploadArea" class="file-upload-area p-6 mb-4 text-center cursor-pointer">
|
|
<div class="flex flex-col items-center">
|
|
<svg class="upload-icon w-12 h-12 text-blue-500 mb-3" fill="none" stroke="currentColor" viewBox="0 0 24 24">
|
|
<path stroke-linecap="round" stroke-linejoin="round" stroke-width="2" d="M7 16a4 4 0 01-.88-7.903A5 5 0 1115.9 6L16 6a5 5 0 011 9.9M15 13l-3-3m0 0l-3 3m3-3v12"></path>
|
|
</svg>
|
|
<p class="text-gray-700 font-medium mb-2">点击或拖拽C/C++文件到此处上传</p>
|
|
<p class="text-sm text-gray-500">支持 .c, .cpp, .h, .hpp, .cc, .cxx 文件 (最大5MB)</p>
|
|
</div>
|
|
<input type="file" id="fileInput" class="file-input-hidden" accept=".c,.cpp,.h,.hpp,.cc,.cxx" multiple>
|
|
</div>
|
|
|
|
<!-- 上传的文件信息 -->
|
|
<div id="uploadedFiles" class="hidden mb-4">
|
|
<div class="file-info-card border border-blue-200 rounded-lg p-4">
|
|
<div class="flex items-center justify-between">
|
|
<div class="flex items-center">
|
|
<span class="text-blue-600 mr-3 text-lg">📄</span>
|
|
<div>
|
|
<span id="fileName" class="text-sm font-medium text-blue-900 block"></span>
|
|
<span id="fileSize" class="text-xs text-blue-700"></span>
|
|
</div>
|
|
</div>
|
|
<button onclick="removeUploadedFile()" class="bg-red-500 hover:bg-red-600 text-white px-3 py-1 rounded-md text-sm transition-colors duration-200">
|
|
✕ 移除
|
|
</button>
|
|
</div>
|
|
</div>
|
|
</div>
|
|
|
|
<textarea
|
|
id="inputCode"
|
|
class="code-editor w-full h-64 px-3 py-2 border border-gray-300 rounded-lg focus:outline-none focus:ring-2 focus:ring-blue-500"
|
|
placeholder="在此输入您的C/C++代码，或通过上方文件上传..."
|
|
spellcheck="false"
|
|
></textarea>
|
|
</div>
|
|
|
|
<div class="flex items-center justify-between">
|
|
<div class="text-sm text-gray-600">
|
|
<span id="charCount">0</span> 字符
|
|
</div>
|
|
<button
|
|
onclick="submitTask()"
|
|
id="submitBtn"
|
|
class="bg-blue-600 text-white px-6 py-3 rounded-lg hover:bg-blue-700 transition font-semibold disabled:bg-gray-400 disabled:cursor-not-allowed"
|
|
>
|
|
🚀 开始验证
|
|
</button>
|
|
</div>
|
|
</div>
|
|
|
|
<!-- Task Status -->
|
|
<div id="taskStatus" class="bg-white rounded-lg shadow-md p-6 mb-8 hidden">
|
|
<h2 class="text-xl font-bold mb-4">📊 任务状态</h2>
|
|
<div class="mb-4">
|
|
<div class="flex justify-between text-sm mb-2">
|
|
<span id="taskStatusText">准备中...</span>
|
|
<span id="taskProgress">0%</span>
|
|
</div>
|
|
<div class="w-full bg-gray-200 rounded-full h-3">
|
|
<div id="progressBar" class="bg-blue-600 h-3 rounded-full transition-all duration-300" style="width: 0%"></div>
|
|
</div>
|
|
</div>
|
|
<div class="text-sm text-gray-600">
|
|
任务ID: <code id="taskId" class="bg-gray-100 px-2 py-1 rounded">-</code>
|
|
</div>
|
|
</div>
|
|
|
|
<!-- Results Section -->
|
|
<div id="results" class="hidden">
|
|
<div class="grid grid-cols-1 lg:grid-cols-2 gap-8 mb-8">
|
|
<!-- Generated Code -->
|
|
<div class="bg-white rounded-lg shadow-md p-6">
|
|
<h3 class="text-lg font-bold mb-4">✨ 生成的验证代码</h3>
|
|
<div class="result-card">
|
|
<pre><code id="generatedCode" class="language-c"></code></pre>
|
|
</div>
|
|
<button onclick="copyToClipboard('generatedCode')" class="mt-4 bg-green-600 text-white px-4 py-2 rounded hover:bg-green-700 transition">
|
|
📋 复制代码
|
|
</button>
|
|
</div>
|
|
|
|
<!-- Verification Results -->
|
|
<div class="bg-white rounded-lg shadow-md p-6">
|
|
<h3 class="text-lg font-bold mb-4">✅ CBMC验证结果</h3>
|
|
<div id="verificationSummary" class="mb-4"></div>
|
|
<div class="result-card">
|
|
<pre><code id="verificationOutput" class="language-text"></code></pre>
|
|
</div>
|
|
</div>
|
|
|
|
<!-- AI Analysis Report -->
|
|
<div id="analysisReportSection" class="bg-white rounded-lg shadow-md p-6 hidden">
|
|
<div class="flex items-center justify-between mb-4">
|
|
<h3 class="text-lg font-bold">🤖 AI智能分析报告</h3>
|
|
<div class="flex items-center space-x-2">
|
|
<span id="analysisStatus" class="px-3 py-1 rounded-full text-sm font-medium bg-blue-100 text-blue-800">
|
|
生成中...
|
|
</span>
|
|
<button onclick="refreshAnalysisReport()" class="text-blue-600 hover:text-blue-900" title="刷新分析报告">
|
|
🔄
|
|
</button>
|
|
</div>
|
|
</div>
|
|
<div id="analysisReportContent" class="prose prose-sm max-w-none">
|
|
<!-- AI分析报告内容将在这里显示 -->
|
|
</div>
|
|
</div>
|
|
</div>
|
|
|
|
<!-- Task History -->
|
|
<div class="bg-white rounded-lg shadow-md p-6">
|
|
<h3 class="text-lg font-bold mb-4">📜 任务历史</h3>
|
|
<div id="taskHistory" class="overflow-x-auto">
|
|
<table class="min-w-full divide-y divide-gray-200">
|
|
<thead class="bg-gray-50">
|
|
<tr>
|
|
<th class="px-6 py-3 text-left text-xs font-medium text-gray-500 uppercase tracking-wider">任务ID</th>
|
|
<th class="px-6 py-3 text-left text-xs font-medium text-gray-500 uppercase tracking-wider">状态</th>
|
|
<th class="px-6 py-3 text-left text-xs font-medium text-gray-500 uppercase tracking-wider">断言数</th>
|
|
<th class="px-6 py-3 text-left text-xs font-medium text-gray-500 uppercase tracking-wider">通过率</th>
|
|
<th class="px-6 py-3 text-left text-xs font-medium text-gray-500 uppercase tracking-wider">完成时间</th>
|
|
<th class="px-6 py-3 text-left text-xs font-medium text-gray-500 uppercase tracking-wider">操作</th>
|
|
</tr>
|
|
</thead>
|
|
<tbody id="taskHistoryBody" class="bg-white divide-y divide-gray-200">
|
|
</tbody>
|
|
</table>
|
|
</div>
|
|
</div>
|
|
</div>
|
|
</main>
|
|
|
|
<!-- Footer -->
|
|
<footer class="bg-gray-800 text-white py-6 mt-12">
|
|
<div class="container mx-auto px-4 text-center">
|
|
<p>© 2024 CBMC SpecGen - 智能代码验证平台</p>
|
|
<p class="text-gray-400 mt-2">基于DeepSeek API和CBMC的形式化验证工具</p>
|
|
</div>
|
|
</footer>
|
|
|
|
<!-- Scripts -->
|
|
<script src="https://cdnjs.cloudflare.com/ajax/libs/prism/1.29.0/prism.min.js"></script>
|
|
<script src="https://cdnjs.cloudflare.com/ajax/libs/prism/1.29.0/components/prism-c.min.js"></script>
|
|
<script>
|
|
const API_BASE = 'http://localhost:8080/api';
|
|
let currentTaskId = null;
|
|
let statusCheckInterval = null;
|
|
|
|
// 初始化
|
|
document.addEventListener('DOMContentLoaded', function() {
|
|
const inputCode = document.getElementById('inputCode');
|
|
inputCode.addEventListener('input', updateCharCount);
|
|
|
|
// 初始化文件上传功能
|
|
initFileUpload();
|
|
|
|
loadTaskHistory();
|
|
loadSystemInfo();
|
|
});
|
|
|
|
// 初始化文件上传功能
|
|
function initFileUpload() {
|
|
const fileUploadArea = document.getElementById('fileUploadArea');
|
|
const fileInput = document.getElementById('fileInput');
|
|
|
|
// 点击上传区域触发文件选择
|
|
fileUploadArea.addEventListener('click', () => {
|
|
fileInput.click();
|
|
});
|
|
|
|
// 文件选择事件
|
|
fileInput.addEventListener('change', handleFileSelect);
|
|
|
|
// 拖拽事件
|
|
fileUploadArea.addEventListener('dragover', handleDragOver);
|
|
fileUploadArea.addEventListener('dragleave', handleDragLeave);
|
|
fileUploadArea.addEventListener('drop', handleFileDrop);
|
|
}
|
|
|
|
// 处理文件选择
|
|
function handleFileSelect(event) {
|
|
const files = event.target.files;
|
|
if (files.length > 0) {
|
|
processFile(files[0]);
|
|
}
|
|
}
|
|
|
|
// 处理拖拽悬停
|
|
function handleDragOver(event) {
|
|
event.preventDefault();
|
|
event.stopPropagation();
|
|
document.getElementById('fileUploadArea').classList.add('dragover');
|
|
}
|
|
|
|
// 处理拖拽离开
|
|
function handleDragLeave(event) {
|
|
event.preventDefault();
|
|
event.stopPropagation();
|
|
document.getElementById('fileUploadArea').classList.remove('dragover');
|
|
}
|
|
|
|
// 处理文件拖拽放下
|
|
function handleFileDrop(event) {
|
|
event.preventDefault();
|
|
event.stopPropagation();
|
|
document.getElementById('fileUploadArea').classList.remove('dragover');
|
|
|
|
const files = event.dataTransfer.files;
|
|
if (files.length > 0) {
|
|
processFile(files[0]);
|
|
}
|
|
}
|
|
|
|
// 处理文件读取
|
|
async function processFile(file) {
|
|
// 验证文件类型
|
|
const validExtensions = ['.c', '.cpp', '.h', '.hpp', '.cc', '.cxx'];
|
|
const fileName = file.name.toLowerCase();
|
|
const isValidFile = validExtensions.some(ext => fileName.endsWith(ext));
|
|
|
|
if (!isValidFile) {
|
|
showToast('请选择有效的C/C++文件 (.c, .cpp, .h, .hpp)', 'error');
|
|
return;
|
|
}
|
|
|
|
// 验证文件大小 (限制为5MB)
|
|
const maxSize = 5 * 1024 * 1024; // 5MB
|
|
if (file.size > maxSize) {
|
|
showToast('文件大小不能超过5MB', 'error');
|
|
return;
|
|
}
|
|
|
|
try {
|
|
const content = await readFileContent(file);
|
|
|
|
// 将文件内容填入代码编辑器
|
|
document.getElementById('inputCode').value = content;
|
|
updateCharCount();
|
|
|
|
// 显示文件信息
|
|
showUploadedFileInfo(file);
|
|
|
|
showToast(`文件 "${file.name}" 上传成功`, 'success');
|
|
} catch (error) {
|
|
showToast('文件读取失败: ' + error.message, 'error');
|
|
}
|
|
}
|
|
|
|
// 读取文件内容
|
|
function readFileContent(file) {
|
|
return new Promise((resolve, reject) => {
|
|
const reader = new FileReader();
|
|
|
|
reader.onload = (event) => {
|
|
resolve(event.target.result);
|
|
};
|
|
|
|
reader.onerror = () => {
|
|
reject(new Error('文件读取失败'));
|
|
};
|
|
|
|
reader.readAsText(file, 'UTF-8');
|
|
});
|
|
}
|
|
|
|
// 显示上传的文件信息
|
|
function showUploadedFileInfo(file) {
|
|
const uploadedFilesDiv = document.getElementById('uploadedFiles');
|
|
const fileNameSpan = document.getElementById('fileName');
|
|
const fileSizeSpan = document.getElementById('fileSize');
|
|
|
|
fileNameSpan.textContent = file.name;
|
|
fileSizeSpan.textContent = `(${formatFileSize(file.size)})`;
|
|
|
|
uploadedFilesDiv.classList.remove('hidden');
|
|
}
|
|
|
|
// 移除上传的文件
|
|
function removeUploadedFile() {
|
|
document.getElementById('uploadedFiles').classList.add('hidden');
|
|
document.getElementById('fileInput').value = '';
|
|
document.getElementById('inputCode').value = '';
|
|
updateCharCount();
|
|
showToast('文件已移除', 'info');
|
|
}
|
|
|
|
// 格式化文件大小
|
|
function formatFileSize(bytes) {
|
|
if (bytes === 0) return '0 Bytes';
|
|
|
|
const k = 1024;
|
|
const sizes = ['Bytes', 'KB', 'MB', 'GB'];
|
|
const i = Math.floor(Math.log(bytes) / Math.log(k));
|
|
|
|
return parseFloat((bytes / Math.pow(k, i)).toFixed(2)) + ' ' + sizes[i];
|
|
}
|
|
|
|
// 更新字符计数
|
|
function updateCharCount() {
|
|
const code = document.getElementById('inputCode').value;
|
|
document.getElementById('charCount').textContent = code.length;
|
|
}
|
|
|
|
// 加载示例代码
|
|
async function loadDemo() {
|
|
try {
|
|
const response = await fetch(`${API_BASE}/demo/sample`);
|
|
const data = await response.json();
|
|
document.getElementById('inputCode').value = data.sample_code;
|
|
updateCharCount();
|
|
showToast('示例代码已加载', 'success');
|
|
} catch (error) {
|
|
showToast('加载示例失败', 'error');
|
|
}
|
|
}
|
|
|
|
// 清空输入
|
|
function clearInput() {
|
|
document.getElementById('inputCode').value = '';
|
|
document.getElementById('uploadedFiles').classList.add('hidden');
|
|
document.getElementById('fileInput').value = '';
|
|
updateCharCount();
|
|
}
|
|
|
|
// 提交任务
|
|
async function submitTask() {
|
|
const inputCode = document.getElementById('inputCode').value.trim();
|
|
|
|
if (!inputCode) {
|
|
showToast('请输入代码', 'error');
|
|
return;
|
|
}
|
|
|
|
const submitBtn = document.getElementById('submitBtn');
|
|
submitBtn.disabled = true;
|
|
submitBtn.textContent = '⏳ 提交中...';
|
|
|
|
try {
|
|
const response = await fetch(`${API_BASE}/tasks`, {
|
|
method: 'POST',
|
|
headers: {
|
|
'Content-Type': 'application/json',
|
|
},
|
|
body: JSON.stringify({
|
|
input_code: inputCode,
|
|
options: {}
|
|
})
|
|
});
|
|
|
|
const data = await response.json();
|
|
|
|
if (response.ok) {
|
|
currentTaskId = data.task_id;
|
|
showTaskStatus();
|
|
startStatusCheck();
|
|
showToast('任务提交成功', 'success');
|
|
} else {
|
|
showToast(data.error || '提交失败', 'error');
|
|
}
|
|
} catch (error) {
|
|
showToast('网络错误', 'error');
|
|
} finally {
|
|
submitBtn.disabled = false;
|
|
submitBtn.textContent = '🚀 开始验证';
|
|
}
|
|
}
|
|
|
|
// 显示任务状态
|
|
function showTaskStatus() {
|
|
document.getElementById('taskStatus').classList.remove('hidden');
|
|
document.getElementById('taskId').textContent = currentTaskId;
|
|
}
|
|
|
|
// 开始状态检查
|
|
function startStatusCheck() {
|
|
if (statusCheckInterval) {
|
|
clearInterval(statusCheckInterval);
|
|
}
|
|
|
|
statusCheckInterval = setInterval(async () => {
|
|
try {
|
|
const response = await fetch(`${API_BASE}/tasks/${currentTaskId}`);
|
|
const task = await response.json();
|
|
|
|
updateTaskStatus(task);
|
|
|
|
if (task.status === 'completed') {
|
|
clearInterval(statusCheckInterval);
|
|
loadTaskResult(task.task_id);
|
|
showToast('验证完成', 'success');
|
|
} else if (task.status === 'failed') {
|
|
clearInterval(statusCheckInterval);
|
|
showToast('验证失败: ' + (task.error || '未知错误'), 'error');
|
|
}
|
|
} catch (error) {
|
|
console.error('检查状态失败:', error);
|
|
}
|
|
}, 2000);
|
|
}
|
|
|
|
// 更新任务状态显示
|
|
function updateTaskStatus(task) {
|
|
const statusText = document.getElementById('taskStatusText');
|
|
const progressBar = document.getElementById('progressBar');
|
|
const progressText = document.getElementById('taskProgress');
|
|
|
|
const statusMap = {
|
|
'pending': '⏳ 等待中...',
|
|
'running': '🔄 处理中...',
|
|
'completed': '✅ 已完成',
|
|
'failed': '❌ 失败'
|
|
};
|
|
|
|
statusText.textContent = statusMap[task.status] || task.status;
|
|
progressBar.style.width = `${task.progress}%`;
|
|
progressText.textContent = `${task.progress}%`;
|
|
|
|
if (task.status === 'running') {
|
|
progressBar.classList.add('status-running');
|
|
} else {
|
|
progressBar.classList.remove('status-running');
|
|
}
|
|
}
|
|
|
|
// 加载任务结果
|
|
async function loadTaskResult(taskId) {
|
|
try {
|
|
const response = await fetch(`${API_BASE}/tasks/${taskId}/result`);
|
|
const result = await response.json();
|
|
|
|
displayResults(result);
|
|
loadTaskHistory();
|
|
} catch (error) {
|
|
showToast('加载结果失败', 'error');
|
|
}
|
|
}
|
|
|
|
// 显示结果
|
|
function displayResults(result) {
|
|
document.getElementById('results').classList.remove('hidden');
|
|
|
|
// 显示生成的代码
|
|
document.getElementById('generatedCode').textContent = result.generated_code;
|
|
Prism.highlightElement(document.getElementById('generatedCode'));
|
|
|
|
// 显示验证摘要
|
|
const summary = result.summary;
|
|
const summaryHtml = `
|
|
<div class="grid grid-cols-2 gap-4">
|
|
<div class="text-center">
|
|
<div class="text-2xl font-bold ${summary.verification_success ? 'text-green-600' : 'text-red-600'}">
|
|
${summary.verification_success ? '✅ 通过' : '❌ 失败'}
|
|
</div>
|
|
<div class="text-sm text-gray-600">验证状态</div>
|
|
</div>
|
|
<div class="text-center">
|
|
<div class="text-2xl font-bold text-blue-600">${summary.total_assertions}</div>
|
|
<div class="text-sm text-gray-600">总断言数</div>
|
|
</div>
|
|
<div class="text-center">
|
|
<div class="text-2xl font-bold text-green-600">${summary.passed_assertions}</div>
|
|
<div class="text-sm text-gray-600">通过断言</div>
|
|
</div>
|
|
<div class="text-center">
|
|
<div class="text-2xl font-bold text-red-600">${summary.failed_assertions}</div>
|
|
<div class="text-sm text-gray-600">失败断言</div>
|
|
</div>
|
|
</div>
|
|
`;
|
|
document.getElementById('verificationSummary').innerHTML = summaryHtml;
|
|
|
|
// 显示验证输出
|
|
document.getElementById('verificationOutput').textContent = result.verification_result.output;
|
|
|
|
// 显示AI分析报告
|
|
displayAnalysisReport(result);
|
|
}
|
|
|
|
// 加载任务历史
|
|
async function loadTaskHistory() {
|
|
try {
|
|
const response = await fetch(`${API_BASE}/tasks`);
|
|
const tasks = await response.json();
|
|
|
|
const tbody = document.getElementById('taskHistoryBody');
|
|
tbody.innerHTML = '';
|
|
|
|
tasks.slice(0, 10).forEach(task => {
|
|
const row = document.createElement('tr');
|
|
const statusClass = task.status === 'completed' ? 'text-green-600' :
|
|
task.status === 'failed' ? 'text-red-600' : 'text-yellow-600';
|
|
|
|
const statusText = task.status === 'completed' ? '✅ 完成' :
|
|
task.status === 'failed' ? '❌ 失败' : '⏳ 运行中';
|
|
|
|
row.innerHTML = `
|
|
<td class="px-6 py-4 whitespace-nowrap text-sm text-gray-900">
|
|
<code class="bg-gray-100 px-2 py-1 rounded">${task.task_id.substring(0, 8)}</code>
|
|
</td>
|
|
<td class="px-6 py-4 whitespace-nowrap text-sm ${statusClass} font-medium">
|
|
${statusText}
|
|
</td>
|
|
<td class="px-6 py-4 whitespace-nowrap text-sm text-gray-900">
|
|
${task.result?.summary?.total_assertions || '-'}
|
|
</td>
|
|
<td class="px-6 py-4 whitespace-nowrap text-sm text-gray-900">
|
|
${task.result?.summary?.total_assertions ?
|
|
Math.round((task.result.summary.passed_assertions / task.result.summary.total_assertions) * 100) + '%' : '-'}
|
|
</td>
|
|
<td class="px-6 py-4 whitespace-nowrap text-sm text-gray-500">
|
|
${task.completed_at ? new Date(task.completed_at).toLocaleString() : '-'}
|
|
</td>
|
|
<td class="px-6 py-4 whitespace-nowrap text-sm font-medium">
|
|
${task.status === 'completed' ?
|
|
`<button onclick="viewResult('${task.task_id}')" class="text-blue-600 hover:text-blue-900">查看</button>` : '-'}
|
|
</td>
|
|
`;
|
|
tbody.appendChild(row);
|
|
});
|
|
|
|
if (tasks.length === 0) {
|
|
tbody.innerHTML = '<tr><td colspan="6" class="px-6 py-4 text-center text-gray-500">暂无任务记录</td></tr>';
|
|
}
|
|
} catch (error) {
|
|
console.error('加载任务历史失败:', error);
|
|
}
|
|
}
|
|
|
|
// 查看结果
|
|
async function viewResult(taskId) {
|
|
try {
|
|
const response = await fetch(`${API_BASE}/tasks/${taskId}/result`);
|
|
const result = await response.json();
|
|
displayResults(result);
|
|
document.getElementById('results').scrollIntoView({ behavior: 'smooth' });
|
|
} catch (error) {
|
|
showToast('加载结果失败', 'error');
|
|
}
|
|
}
|
|
|
|
// 加载系统信息
|
|
async function loadSystemInfo() {
|
|
try {
|
|
const response = await fetch(`${API_BASE}/system/info`);
|
|
const info = await response.json();
|
|
|
|
document.getElementById('cbmcVersion').textContent = info.cbmc_version.split('\n')[0];
|
|
document.getElementById('activeTasks').textContent = info.active_tasks;
|
|
document.getElementById('completedTasks').textContent = info.completed_tasks;
|
|
|
|
document.getElementById('systemInfo').classList.remove('hidden');
|
|
} catch (error) {
|
|
console.error('加载系统信息失败:', error);
|
|
}
|
|
}
|
|
|
|
// 复制到剪贴板
|
|
function copyToClipboard(elementId) {
|
|
const element = document.getElementById(elementId);
|
|
const textArea = document.createElement('textarea');
|
|
textArea.value = element.textContent;
|
|
document.body.appendChild(textArea);
|
|
textArea.select();
|
|
document.execCommand('copy');
|
|
document.body.removeChild(textArea);
|
|
showToast('已复制到剪贴板', 'success');
|
|
}
|
|
|
|
// 显示AI分析报告
|
|
function displayAnalysisReport(result) {
|
|
const reportSection = document.getElementById('analysisReportSection');
|
|
const reportContent = document.getElementById('analysisReportContent');
|
|
const analysisStatus = document.getElementById('analysisStatus');
|
|
|
|
if (result.analysis_generated && result.analysis_report) {
|
|
// 显示生成的分析报告
|
|
reportSection.classList.remove('hidden');
|
|
analysisStatus.textContent = 'AI分析完成';
|
|
analysisStatus.className = 'px-3 py-1 rounded-full text-sm font-medium bg-green-100 text-green-800';
|
|
|
|
// 将Markdown报告转换为HTML并显示
|
|
const htmlContent = markdownToHtml(result.analysis_report);
|
|
reportContent.innerHTML = htmlContent;
|
|
|
|
// 添加一些样式增强
|
|
enhanceReportStyles();
|
|
} else if (result.analysis_error) {
|
|
// 显示分析错误
|
|
reportSection.classList.remove('hidden');
|
|
analysisStatus.textContent = '分析失败';
|
|
analysisStatus.className = 'px-3 py-1 rounded-full text-sm font-medium bg-red-100 text-red-800';
|
|
reportContent.innerHTML = `
|
|
<div class="bg-red-50 border border-red-200 rounded-lg p-4">
|
|
<div class="flex items-center">
|
|
<span class="text-red-600 mr-2">❌</span>
|
|
<div>
|
|
<h4 class="text-red-800 font-medium">分析报告生成失败</h4>
|
|
<p class="text-red-600 text-sm mt-1">${result.analysis_error}</p>
|
|
</div>
|
|
</div>
|
|
</div>
|
|
`;
|
|
} else {
|
|
// 分析报告不可用
|
|
reportSection.classList.add('hidden');
|
|
}
|
|
}
|
|
|
|
// 刷新分析报告
|
|
async function refreshAnalysisReport() {
|
|
if (!currentTaskId) return;
|
|
|
|
const analysisStatus = document.getElementById('analysisStatus');
|
|
const reportContent = document.getElementById('analysisReportContent');
|
|
|
|
try {
|
|
analysisStatus.textContent = '刷新中...';
|
|
analysisStatus.className = 'px-3 py-1 rounded-full text-sm font-medium bg-blue-100 text-blue-800';
|
|
|
|
const response = await fetch(`${API_BASE}/tasks/${currentTaskId}/analysis`);
|
|
const data = await response.json();
|
|
|
|
if (data.analysis_report) {
|
|
const htmlContent = markdownToHtml(data.analysis_report);
|
|
reportContent.innerHTML = htmlContent;
|
|
enhanceReportStyles();
|
|
analysisStatus.textContent = 'AI分析完成';
|
|
analysisStatus.className = 'px-3 py-1 rounded-full text-sm font-medium bg-green-100 text-green-800';
|
|
showToast('分析报告已刷新', 'success');
|
|
} else {
|
|
throw new Error(data.analysis_error || '分析报告不可用');
|
|
}
|
|
|
|
} catch (error) {
|
|
analysisStatus.textContent = '刷新失败';
|
|
analysisStatus.className = 'px-3 py-1 rounded-full text-sm font-medium bg-red-100 text-red-800';
|
|
showToast('刷新分析报告失败: ' + error.message, 'error');
|
|
}
|
|
}
|
|
|
|
// 简单的Markdown转HTML转换器
|
|
function markdownToHtml(markdown) {
|
|
if (!markdown) return '';
|
|
|
|
return markdown
|
|
// 标题
|
|
.replace(/^# (.*$)/gim, '<h1 class="text-2xl font-bold text-gray-900 mb-4 mt-6">$1</h1>')
|
|
.replace(/^## (.*$)/gim, '<h2 class="text-xl font-bold text-gray-800 mb-3 mt-5">$1</h2>')
|
|
.replace(/^### (.*$)/gim, '<h3 class="text-lg font-bold text-gray-700 mb-2 mt-4">$1</h3>')
|
|
// 粗体和斜体
|
|
.replace(/\*\*(.*?)\*\*/g, '<strong>$1</strong>')
|
|
.replace(/\*(.*?)\*/g, '<em>$1</em>')
|
|
// 列表
|
|
.replace(/^- (.*$)/gim, '<li class="ml-4">• $1</li>')
|
|
.replace(/(<li.*<\/li>)/s, '<ul class="list-disc ml-6 mb-3">$1</ul>')
|
|
// 链接
|
|
.replace(/\[([^\]]+)\]\(([^)]+)\)/g, '<a href="$2" class="text-blue-600 hover:text-blue-800 underline" target="_blank">$1</a>')
|
|
// 代码块
|
|
.replace(/```([^`]+)```/g, '<pre class="bg-gray-100 p-3 rounded-md overflow-x-auto my-3"><code>$1</code></pre>')
|
|
// 行内代码
|
|
.replace(/`([^`]+)`/g, '<code class="bg-gray-100 px-2 py-1 rounded text-sm">$1</code>')
|
|
// 段落
|
|
.replace(/\n\n/g, '</p><p class="mb-4">')
|
|
.replace(/^/, '<p class="mb-4">')
|
|
.replace(/$/, '</p>');
|
|
}
|
|
|
|
// 增强报告样式
|
|
function enhanceReportStyles() {
|
|
// 为表格添加样式
|
|
const tables = document.querySelectorAll('#analysisReportContent table');
|
|
tables.forEach(table => {
|
|
table.className = 'min-w-full divide-y divide-gray-200 border border-gray-300 rounded-lg overflow-hidden my-4';
|
|
|
|
const headers = table.querySelectorAll('th');
|
|
headers.forEach(header => {
|
|
header.className = 'px-6 py-3 bg-gray-50 text-left text-xs font-medium text-gray-500 uppercase tracking-wider border-b border-gray-200';
|
|
});
|
|
|
|
const cells = table.querySelectorAll('td');
|
|
cells.forEach(cell => {
|
|
cell.className = 'px-6 py-4 whitespace-nowrap text-sm text-gray-900 border-b border-gray-100';
|
|
});
|
|
});
|
|
|
|
// 为状态指示器添加样式
|
|
const statusIndicators = document.querySelectorAll('#analysisReportContent .text-green-600, #analysisReportContent .text-red-600, #analysisReportContent .text-yellow-600');
|
|
statusIndicators.forEach(indicator => {
|
|
if (indicator.textContent.includes('✅') || indicator.textContent.includes('🟢')) {
|
|
indicator.className = 'inline-flex items-center px-2 py-1 rounded-full text-xs font-medium bg-green-100 text-green-800';
|
|
} else if (indicator.textContent.includes('❌') || indicator.textContent.includes('🔴')) {
|
|
indicator.className = 'inline-flex items-center px-2 py-1 rounded-full text-xs font-medium bg-red-100 text-red-800';
|
|
} else if (indicator.textContent.includes('⚠️') || indicator.textContent.includes('🟡')) {
|
|
indicator.className = 'inline-flex items-center px-2 py-1 rounded-full text-xs font-medium bg-yellow-100 text-yellow-800';
|
|
}
|
|
});
|
|
}
|
|
|
|
// Toast 提示
|
|
function showToast(message, type = 'info') {
|
|
const toast = document.createElement('div');
|
|
const bgColor = type === 'success' ? 'bg-green-500' :
|
|
type === 'error' ? 'bg-red-500' : 'bg-blue-500';
|
|
|
|
toast.className = `fixed top-4 right-4 ${bgColor} text-white px-6 py-3 rounded-lg shadow-lg z-50 transition-opacity duration-300`;
|
|
toast.textContent = message;
|
|
|
|
document.body.appendChild(toast);
|
|
|
|
setTimeout(() => {
|
|
toast.style.opacity = '0';
|
|
setTimeout(() => document.body.removeChild(toast), 300);
|
|
}, 3000);
|
|
}
|
|
</script>
|
|
</body>
|
|
</html> |