[Question] Can goto-cc be used with an ESP-IDF project easily

[jdbaptista]

Firstly, I apologize for anything that doesn't make sense here because I am both trying to wrap my head around what I can do and how I can potentially do it. I am interested in testing some portions of my esp32s3 project (built with ESP-IDF) with formal verification. An example of what I mean is:

/**
 * Specifies that a greater major version outputs UPDATE_MAJOR.
 */
void spec1(void)
{
    VersionInfo in;
    UpdateType out;

    __CPROVER_assume(in.hardwareVer == OTA_HARDWARE_VERSION);
    __CPROVER_assume(in.revisionVer == OTA_REVISION_VERSION);
    __CPROVER_assume(in.majorVer > OTA_MAJOR_VERSION);

    out = compareVersions(in);

    assert(out == UPDATE_MAJOR);
}

I would typically write some unit tests for this, however these types of CBMC tests seem more robust and quicker to create. I was able to test compareVersions by copying it out of the source file it is in and manually copying dependencies. I would like to avoid the overhead of copying and manually mocking dependencies. The issue I am facing is that my source files tend to include a large number of ESP-IDF header files:

#include "esp_crt_bundle.h"
#include "esp_err.h"
#include "esp_http_client.h"
#include "esp_https_ota.h"
#include "esp_log.h"
#include "esp_system.h"
#include "freertos/FreeRTOS.h"
#include "freertos/portmacro.h"
#include "freertos/projdefs.h"
#include "freertos/task.h"
#include "sdkconfig.h"

This means that I need to use goto-cc with effectively every header file and source file necessary for my project, down to hardware specific files. I believe the correct solution would be to decouple my business logic from hardware files, however even then including something like esp_err.h requires inclusion of various ESP-IDF internal source and header files. I have tried to get around this issue by including every source and header file in the project in my call to goto-cc with some custom CMake, however I always seem to be missing some files.

One question I had was whether it is possible to have goto-cc drop-in as a replacement for the xtensa-esp32s3-elf-gcc cross-compiler. If that is not possible, I suppose it is a lost cause to try to track down all the machine-specific source files that my project depends on. Overall, I would like to know if anyone has used CBMC or other formal verification tools alongside ESP-IDF for an ESP32 and how I can go about doing that without refactoring my entire project. Thank you!