CBMC Harness Generation and Checker

This system is a VScode extension for C developers, which generates a memory safety verification report from running CBMC (C-bounded model checker) on a harness generated by LLMs. Both the CBMC report and the LLM generated harness are returned to the user. The user only has to open a directory within VScode's workspace folder, specify a function within the current active .c file on screen then run the extension to receive the complete report.

Table of Contents

1. Prerequisites
2. Project Structure
3. Set Up Project
4. Quickstart
5. Additional Information

Prerequisites

Ensure you have the following installed on your system:

• node I have v20.6.1 on my environment
• npmI have version 9.8.1
• python You'll need pip
• cbmc Environmental variables have to be set up, has to be able to work from terminal

Project Structure

The project consists of 3 main directories:

• harness (VS code extension Frontend)
• backend (Django Backend)
• cbmc (C code to run tests on)

Setting Up Project

If you haven't already done so, clone the repository

1. Install all necessary packages for JS (frontend)

Navigate into the harness directory then run:

npm i

2. Test out VScode extension

Navigate over to the extension.js file and then open it so it is your current active file in VScode, then press f5. If you're asked to choose runtime, use Extension Development. Once you have the second (user) window opened, press ctrl + shift + P (or Cmd + shift + P on Mac) then type in:

helloworld

Pressing enter should show an information box indicating successful set up

3. Getting Django running

Navigate over to backend then run:

python3 -m venv venv
source venv/bin/activate  # (Windows: venv\Scripts\activate)
pip install -r requirements.txt
# Then navigate into extension_backend/
python manage.py migrate (if needed)
python manage.py runserver # this will start the Django server

Now send a curl request or any API GET request over to http://localhost:8000 the response you receive should indicate that Django is up and running

Quickstart

Make sure your backend server is running (python manage.py runserver) and activate extension through pressing f5 with current active file in window being extension.js. Navigate your VS code workspace so that it opens the cbmc folder containing the sample C code. Open up the main.c file then ctrl + shift + P. Type generate within the dialogue box and then enter the main function. Upon waiting around 15 seconds you should receive the report relayed back from the backend system and opened up in VScode.

*Note that the function name being entered has to be an exact match to a function within the current active C file on your screen

Additional Information

You'll also need to put the .env file containing the keys into the same folder as CBMC_LLM_Harness_Generation/backend