cpp-to-dafny-translator

C/C++ to Dafny Translator

Translate C/C++ programs into equivalent, verifiable Dafny code while preserving program semantics and ensuring memory safety.

Overview

This skill provides systematic guidance for translating C/C++ code to Dafny, handling memory management, pointer semantics, type conversions, and ensuring well-typed, verifiable output with appropriate specifications.

Translation Workflow

C/C++ Input → Analyze Structure → Map Types & Memory → Translate → Add Specifications → Verify
    ├─ Identify types, pointers, memory patterns
    ├─ Map C/C++ constructs to Dafny equivalents
    ├─ Handle memory safety and ownership
    ├─ Add preconditions, postconditions, invariants
    └─ Validate executability and verification

Core Translation Principles

1. Memory Safety First

Dafny enforces memory safety. Every translation must:

• Replace raw pointers with safe references or arrays
• Make memory bounds explicit
• Ensure no null pointer dereferences
• Handle dynamic memory with sequences or arrays

2. Preserve Semantics

The translated code must maintain the same computational behavior, preserve function contracts, keep algorithmic complexity, and handle all edge cases including error conditions.

3. Enable Verification

Generated Dafny code must include specifications (preconditions, postconditions, invariants), be verifiable by Dafny's verifier, compile and execute correctly, and follow Dafny idioms.

Type Mapping Reference

Basic Types

| C/C++ Type | Dafny Type | Notes | |-----------|-----------|-------| | int, long | int | Unbounded integers in Dafny | | unsigned int | nat | Natural numbers (≥ 0) | | char | char | Single character | | bool | bool | Direct mapping | | float, double | real | Exact rationals in Dafny | | void | () | Unit type | | NULL | Use Option or bounds checks | No null pointers |

Composite Types

| C/C++ Type | Dafny Type | Notes | |-----------|-----------|-------| | int arr[] | array<int> | Fixed-size arrays | | int* ptr | array<int> or seq<int> | Depends on usage | | struct | class or datatype | Mutable vs immutable | | enum | datatype | Algebraic data types | | union | datatype with variants | Tagged unions |

For detailed mappings, see [references/type_mappings.md](references/type_mappings.md).

Translation Patterns

Functions

Simple C function:

int add(int a, int b) {
    return a + b;
}

Dafny:

function add(a: int, b: int): int
{
    a + b
}

Function with side effects:

void increment(int* x) {
    (*x)++;
}

Dafny (using method):

method increment(x: array<int>, index: nat)
    requires index < x.Length
    modifies x
    ensures x[index] == old(x[index]) + 1
{
    x[index] := x[index] + 1;
}

Pointers and Arrays

C array access:

int sum_array(int* arr, int n) {
    int sum = 0;
    for (int i = 0; i < n; i++) {
        sum += arr[i];
    }
    return sum;
}

Dafny:

method sumArray(arr: array<int>) returns (sum: int)
    ensures sum == arraySum(arr[..])
{
    sum := 0;
    var i := 0;
    while i < arr.Length
        invariant 0 <= i <= arr.Length
        invariant sum == arraySum(arr[..i])
    {
        sum := sum + arr[i];
        i := i + 1;
    }
}

function arraySum(s: seq<int>): int
{
    if |s| == 0 then 0 else s[0] + arraySum(s[1..])
}

Structs and Classes

C struct:

struct Point {
    int x;
    int y;
};

int distance_squared(struct Point* p) {
    return p->x * p->x + p->y * p->y;
}

Dafny:

class Point {
    var x: int
    var y: int

    constructor(x0: int, y0: int)
        ensures x == x0 && y == y0
    {
        x := x0;
        y := y0;
    }
}

function distanceSquared(p: Point): int
    reads p
{
    p.x * p.x + p.y * p.y
}

Control Flow

If-else:

int max(int a, int b) {
    if (a > b) return a;
    else return b;
}

Dafny:

function max(a: int, b: int): int
{
    if a > b then a else b
}

Loops with invariants:

int factorial(int n) {
    int result = 1;
    for (int i = 1; i <= n; i++) {
        result *= i;
    }
    return result;
}

Dafny:

method factorial(n: nat) returns (result: nat)
    ensures result == fact(n)
{
    result := 1;
    var i := 1;
    while i <= n
        invariant 1 <= i <= n + 1
        invariant result == fact(i - 1)
    {
        result := result * i;
        i := i + 1;
    }
}

function fact(n: nat): nat
{
    if n == 0 then 1 else n * fact(n - 1)
}

Handling Common Challenges

1. Pointer Arithmetic

Challenge: C allows pointer arithmetic; Dafny doesn't.

Solution: Use array indices instead:

// C
int* ptr = arr + 5;
*ptr = 10;

// Dafny
arr[5] := 10;

2. Dynamic Memory Allocation

Challenge: C uses malloc/free; Dafny has automatic memory management.

Solution: Use arrays or sequences:

// C
int* arr = (int*)malloc(n * sizeof(int));
// ... use arr ...
free(arr);

// Dafny
var arr := new int[n];
// ... use arr ...
// No explicit free needed

3. Null Pointers

Challenge: C allows NULL; Dafny doesn't have null references.

Solution: Use Option types or ensure non-null:

// C
int* find(int* arr, int n, int target) {
    for (int i = 0; i < n; i++) {
        if (arr[i] == target) return &arr[i];
    }
    return NULL;
}

// Dafny
method find(arr: array<int>, target: int) returns (index: int)
    ensures index == -1 || (0 <= index < arr.Length && arr[index] == target)
{
    var i := 0;
    while i < arr.Length
        invariant 0 <= i <= arr.Length
    {
        if arr[i] == target {
            return i;
        }
        i := i + 1;
    }
    return -1;
}

4. Mutable vs Immutable

Challenge: C has mutable everything; Dafny distinguishes functions (pure) from methods (with side effects).

Solution:

• Use function for pure computations
• Use method for operations with side effects
• Add reads clauses for functions that read object fields
• Add modifies clauses for methods that modify state

5. Verification Annotations

Challenge: Dafny requires specifications for verification.

Solution: Add preconditions, postconditions, and loop invariants:

method binarySearch(arr: array<int>, target: int) returns (index: int)
    requires forall i, j :: 0 <= i < j < arr.Length ==> arr[i] <= arr[j]  // sorted
    ensures index == -1 || (0 <= index < arr.Length && arr[index] == target)
{
    var low := 0;
    var high := arr.Length;
    while low < high
        invariant 0 <= low <= high <= arr.Length
        invariant forall i :: 0 <= i < low ==> arr[i] < target
        invariant forall i :: high <= i < arr.Length ==> arr[i] > target
    {
        var mid := (low + high) / 2;
        if arr[mid] < target {
            low := mid + 1;
        } else if arr[mid] > target {
            high := mid;
        } else {
            return mid;
        }
    }
    return -1;
}

Translation Process

Step 1: Analyze C/C++ Code

Identify all functions, structs, and global variables. Analyze pointer usage and memory patterns. Identify side effects and state modifications. Note any unsafe operations.

Step 2: Plan Type and Memory Mappings

Map C/C++ types to Dafny types. Decide how to handle pointers (arrays, sequences, or references). Plan struct translations (class vs datatype). Identify what needs specifications.

Step 3: Translate Constructs

Start with data structures (structs → classes/datatypes). Translate pure functions first. Convert functions with side effects to methods. Add memory safety checks. Include necessary specifications.

Step 4: Add Verification Annotations

Add preconditions (requires). Add postconditions (ensures). Add loop invariants. Add frame conditions (reads, modifies). Add termination measures (decreases).