Skip to content

Add support for C++ classes and dynamic memory allocation via new and delete - #68

Open
Plastpase123 wants to merge 5 commits into
uuverifiers:masterfrom
Plastpase123:cpp-class-transformations
Open

Add support for C++ classes and dynamic memory allocation via new and delete#68
Plastpase123 wants to merge 5 commits into
uuverifiers:masterfrom
Plastpase123:cpp-class-transformations

Conversation

@Plastpase123

@Plastpase123 Plastpase123 commented Jun 21, 2026

Copy link
Copy Markdown

What has been implemented

  • Parser can now parse class definitions, which act like extended C-structs that may contain function definitions, as well as expressions using new and delete
  • Classes are transformed into C-style structs, and member functions are transformed to operate on struct pointers
  • Usage of new for primitive types are encoded directly as CHCs, and translated into helper functions for class types
  • Usage of delete is translated to free for primitive types, and helper function calls for class types

Limitations

  • User must define a constructor and destructor for each defined class
  • User must invoke destructor explicitly to ensure that an object is properly destroyed
  • Using new to create pointer-to-pointers might be buggy

Not implemented (A non-exhaustive list)

  • Other special member functions (move/copy constructors etc)
  • Inheritance
  • Dynamic dispatch
  • Friend functions
  • Function overloading

Examples

For classes, the following program:

class C {
  public:
    int x;
    C(int val) {
      x = val;
    }
    ~C() {}
};

int main() {
    C obj = C(1);
    return 0;
}

Gets translated to:

struct C {
  int x;
};
// Constructor
void C::ctor(struct *this, int val) {
  this->x = val;
}
// Destructor
void C::dtor() {}

struct *C __create_C(int val) {
  struct C obj;
  C::ctor(&obj, val);
  return obj;
}

int main() {
  struct C obj = __create_C(1);
  return 0;
}

For new and delete:

int main() {
  int *int_ptr = new int(5);
  delete int_ptr;

  C *obj_ptr = new C(...)
  delete obj_ptr;
  return 0;
}

Gets turned into:

struct C* __new_C(...) {
  struct C* obj = malloc(sizeof(struct C*));
  C::ctor(obj, ...);
  return obj;
}

void __delete_C(struct *C this) {
  C::dtor(this);
  free(this);
}

int main() {
  int *int_ptr = new int(5); // Encoded as a call to `alloc` from the heap model
  free(int_ptr)

  C *obj_ptr = __new_C(...)
  __delete_C(obj_ptr);
  return 0;
}

Plastpase123 and others added 5 commits June 14, 2026 22:42
This enables verification of C++ classes by transforming them into C-style structs.

High-level description of transformation pipeline:
  1. Preprocess with C++-specific tri-pp
  2. Collect class definitions, mapping fully qualified class names with their
     member function definitions and C-struct valid declarations
  3. Create new global struct definitions from collected classes
  4. Add global member function definitions with and added `struct ClassName *this` argument
  5. Transform member function call-sites and object declarations to match
  6. Run remaining TriCera pipeline on resulting C-program

Besides class transformations, this commit also adds a check for the TriCeraPreProcessor,
which uses a specific version of tri-pp depending on the type of the file currently being read.
This adds support for dynamic memory allocation via `new` and `delete`.

This allows one to declare pointers of primitive- and class types with `new`,
and deallocate them via `delete`.

Class type pointers are transformed into calls to helper functions that both
allocate and construct the object via the constructor, whereas `new` is directly
encoded as CHCs for primitives.

NOTE: Constructing pointers to pointers with such as `new T*(new ...)` is still a bit iffy.
There are also some issues in regards to classes.
@Plastpase123 Plastpase123 reopened this Jun 21, 2026
@Plastpase123 Plastpase123 changed the title Cpp class transformations Add support for C++ classes and dynamic memory allocation via new and delete Jun 21, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant