Allocating and Deallocating Memory

At the moment, CN does not understand the malloc and free functions. They are a bit tricky because they rely on a bit of polymorphism and a typecast between char* -- the result type of malloc and argument type of free -- and the actual type of the object being allocated or deallocated.

However, for any given type, we can define a type-specific function that allocates heap storage with exactly that type. The implementation of this function cannot be checked by CN, but we can give just the spec, together with a promise to link against an external C library providing a correct (but not verified!) implementation:

exercises/malloc.h

extern int *mallocInt ();
/*@ spec mallocInt();
    requires true;
    ensures take R = Block<int>(return);
@*/

extern unsigned int *mallocUnsignedInt ();
/*@ spec mallocUnsignedInt();
    requires true;
    ensures take R = Block<unsigned int>(return);
@*/

(Alternatively we can include an implementation written in arbitrary C inside a CN file by marking it with the keyword trusted at the top of its CN specification.)

Similarly:

exercises/free.h

extern void freeInt (int *p);
/*@ spec freeInt(pointer p);
    requires take P = Block<int>(p);
    ensures true;
@*/


extern void freeUnsignedInt (unsigned int *p);
/*@ spec freeUnsignedInt(pointer p);
    requires take P = Block<unsigned int>(p);
    ensures true;
@*/

Now we can write code that allocates and frees memory:

exercises/slf17_get_and_free.c

#include "free.h"

unsigned int get_and_free (unsigned int *p)
/*@ requires take P = Owned(p);
    ensures return == P; 
@*/
{
  unsigned int v = *p;
  freeUnsignedInt (p);
  return v;
}

We can also define a "safer", ML-style version of malloc that handles both allocation and initialization:

exercises/ref.h

extern unsigned int *refUnsignedInt (unsigned int v);
/*@ spec refUnsignedInt(u32 v);
    requires true;
    ensures take R = Owned(return);
            R == v;
@*/

extern int *refInt (int v);
/*@ spec refInt(i32 v);
    requires true;
    ensures take R = Owned(return);
            R == v;
@*/

exercises/slf16_basic_succ_using_incr.c

#include "free.h"
#include "ref.h"
#include "slf0_basic_incr.c"

unsigned int succ_using_incr (unsigned int n)
/*@ ensures return == n + 1u32; @*/
{
  unsigned int *p = refUnsignedInt(n);
  incr(p);
  unsigned int x = *p;
  freeUnsignedInt(p);
  return x;
}

Exercises

Prove a specification for the following program that reveals only that it returns a pointer to a number that is greater than the number pointed to by its argument.

exercises/slf_ref_greater.c

#include "malloc.h"

unsigned int *ref_greater_abstract (unsigned int *p)
{
  unsigned int* q = mallocUnsignedInt();
  *q = *p + 1;
  return q;
}

Side note

Here is another syntax for external / unknown functions, together with an example of a loose specification:

exercises/slf18_two_dice.c

unsigned int val_rand (unsigned int n);
/*@ spec val_rand(u32 n);
    requires n > 0u32;
    ensures 0u32 <= return && return < n;
@*/

unsigned int two_dice ()
/*@ ensures 2u32 <= return && return <= 12u32; @*/
{
  unsigned int n1 = val_rand (6);
  unsigned int n2 = val_rand (6);
  unsigned int s = n1 + n2;
  return s + 2;
}