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.
120 lines
3.4 KiB
120 lines
3.4 KiB
#!/usr/bin/env python3
|
|
"""
|
|
Demo code generator for CBMC SpecGen web interface
|
|
This creates a demonstration of CBMC assertion generation without API calls
|
|
"""
|
|
|
|
import os
|
|
import sys
|
|
import re
|
|
from datetime import datetime
|
|
|
|
def add_cbmc_assertions(code):
|
|
"""Add CBMC assertions to C code (demo version)"""
|
|
|
|
# Simple patterns for common functions
|
|
patterns = {
|
|
r'int\s+(\w+)\s*\([^)]*\)\s*\{': [
|
|
' // Preconditions\n',
|
|
' // Function body\n'
|
|
],
|
|
r'for\s*\([^)]+\)\s*\{': [
|
|
' // Loop invariant\n',
|
|
' // Bounds checking\n'
|
|
],
|
|
r'if\s*\([^)]+\)\s*\{': [
|
|
' // Condition check\n'
|
|
],
|
|
r'int\s+\w+\s*\[\s*(\w+)\s*\]': [
|
|
' // Array bounds checking\n'
|
|
],
|
|
r'return\s+\w+;': [
|
|
' // Postcondition check\n'
|
|
]
|
|
}
|
|
|
|
# Add basic assertions
|
|
result = code
|
|
|
|
# Add includes
|
|
if '#include <stdio.h>' in result:
|
|
result = result.replace('#include <stdio.h>', '#include <stdio.h>\n// CBMC assertions\n#include <assert.h>\n')
|
|
|
|
# Add some basic assertions for demo
|
|
if 'main()' in result:
|
|
result = result.replace('int main() {', 'int main() {\n // Entry point assertion\n assert(1 == 1); // Basic sanity check')
|
|
|
|
if 'printf' in result:
|
|
result = result.replace('printf(', '// Output operation\n printf(')
|
|
|
|
return result
|
|
|
|
def create_demo_verification_result():
|
|
"""Create a demo CBMC verification result"""
|
|
return """CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
|
|
Parsing demo.c
|
|
Converting
|
|
Type-checking demo
|
|
Generating GOTO Program
|
|
Adding CPROVER library (x86_64)
|
|
Removal of function pointers and virtual functions
|
|
Generic Property Instrumentation
|
|
Running with 8 object bits, 56 offset bits (default)
|
|
Starting Bounded Model Checking
|
|
|
|
** Results:
|
|
demo.c function main
|
|
[main.assertion.1] line 8 main: basic sanity check: SUCCESS
|
|
[main.assertion.2] line 15 main: valid computation: SUCCESS
|
|
|
|
** 0 of 2 failed (1 iterations)
|
|
VERIFICATION SUCCESSFUL
|
|
**** WARNING: Use --unwinding-assertions to obtain sound verification results"""
|
|
|
|
def generate_demo_result(input_code):
|
|
"""Generate a complete demo result"""
|
|
|
|
# Generate assertions
|
|
generated_code = add_cbmc_assertions(input_code)
|
|
|
|
# Create verification result
|
|
verification_result = create_demo_verification_result()
|
|
|
|
# Count assertions (simple count)
|
|
assertion_count = generated_code.count('assert') + generated_code.count('__CPROVER_')
|
|
|
|
return {
|
|
'generated_code': generated_code,
|
|
'verification_result': {
|
|
'success': True,
|
|
'output': verification_result,
|
|
'assertion_count': assertion_count,
|
|
'failed_count': 0
|
|
},
|
|
'summary': {
|
|
'total_assertions': assertion_count,
|
|
'passed_assertions': assertion_count,
|
|
'failed_assertions': 0,
|
|
'verification_success': True
|
|
}
|
|
}
|
|
|
|
if __name__ == "__main__":
|
|
# Test the demo generator
|
|
test_code = '''#include <stdio.h>
|
|
|
|
int add(int a, int b) {
|
|
return a + b;
|
|
}
|
|
|
|
int main() {
|
|
int result = add(3, 4);
|
|
printf("Result: %d\\n", result);
|
|
return 0;
|
|
}'''
|
|
|
|
result = generate_demo_result(test_code)
|
|
print("Generated Code:")
|
|
print(result['generated_code'])
|
|
print("\nVerification Result:")
|
|
print(result['verification_result']['output']) |