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:**
```c
int add(int a, int b) {
    return a + b;
}
```

**Dafny:**
```dafny
function add(a: int, b: int): int
{
    a + b
}
```

**Function with side effects:**
```c
void increment(int* x) {
    (*x)++;
}
```

**Dafny (using method):**
```dafny
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:**
```c
int sum_array(int* arr, int n) {
    int sum = 0;
    for (int i = 0; i < n; i++) {
        sum += arr[i];
    }
    return sum;
}
```

**Dafny:**
```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:**
```c
struct Point {
    int x;
    int y;
};

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

**Dafny:**
```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:**
```c
int max(int a, int b) {
    if (a > b) return a;
    else return b;
}
```

**Dafny:**
```dafny
function max(a: int, b: int): int
{
    if a > b then a else b
}
```

**Loops with invariants:**
```c
int factorial(int n) {
    int result = 1;
    for (int i = 1; i <= n; i++) {
        result *= i;
    }
    return result;
}
```

**Dafny:**
```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
// C
int* ptr = arr + 5;
*ptr = 10;
```

```dafny
// Dafny
arr[5] := 10;
```

### 2. Dynamic Memory Allocation

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

**Solution:** Use arrays or sequences:
```c
// C
int* arr = (int*)malloc(n * sizeof(int));
// ... use arr ...
free(arr);
```

```dafny
// 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
// 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
// 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