Axioms



The memory Mem is defined only for addresses that have been allocated to the program by the C runtime. The C runtime provides primitive operations for accessing memory: accessMem, storeMem, umalloc, ufree, function frame allocation ucreateFrame and function frame deallocation udestroyFrame. Rather than committing to a particular implementation of these primitives, our formalism axiomatizes properties that any reasonable implementation should satisfy.
The axioms of accessMem and storeMem state simple properties like ``reading a location after storing to it returns the value that was stored'', and ``storing to a location does not affect any other location.'' accessMem and storeMem fail if they try to access unallocated memory.
Axiom validAccessMem__validStoreMem : forall m l v,
  (exists v, accessMem m l = Some v) <-> (exists m', storeMem m l v = Some m').

Axiom storeMem__accessMem : forall M loc v M',
  storeMem M loc v = Some M' ->
  accessMem M' loc = Some v /\
  (forall l v,
    l <> loc ->
    accessMem M l = Some v ->
    accessMem M' l = Some v
  ) /\
  (forall l,
    accessMem M l = None ->
    accessMem M' l = None
  )
  .

Axiom storeMem_uniqBehavior : forall v m l v',
  ((exists m', storeMem m l v = Some m') -> (exists m', storeMem m l v' = Some m')) /\
  (storeMem m l v = None -> storeMem m l v' = None).

An allocated key in the lock table must be zero.
Axiom getFreshRentry__inversion : forall RI ri,
  getFreshRentry RI = Some ri ->
  RI ri = 0.

The axioms of umalloc and ufree enforce properties like ``malloc returns a pointer to a region of memory that was previously unallocated, and stores this region in AllocMemBlock'', ``free only deallocates a memory region stored at AllocMemBlock, and removes this region from AllocMemBlock'', and ``malloc and free do not alter the contents of irrelevant locations.'' malloc fails if there is not enough space; ufree fails if it tries to deallocate a memory region that is not at AllocMemBlock.
Axiom umalloc__inversion : forall uE n uM' uAMB' uG' uS' loc,
  umalloc uE n = Some ((MkuEnv uM' uAMB' uG' uS'), loc) ->
  exists uM, exists uAMB,
  uE = MkuEnv uM uAMB uG' uS' /\
  (baseAddress<=loc /\ loc+ n <= uE.(ustack).(utop) /\ n > 0) /\
  (forall l v,
    accessMem uM l = Some v -> accessMem uM' l = Some v
  ) /\
  (forall l,
    l < loc \/ l >= loc + n ->
    accessMem uM l = None -> accessMem uM' l = None
    ) /\
  (forall l,
    loc <= l < loc + n -> accessMem uM l = None
  ) /\
  (forall l,
    loc <= l < loc + n ->
    accessMem uM' l = Some 0
  ) /\
  uAMB' = addAllocMemBlock uAMB loc (loc+n)
  .

Axiom ufree__inversion : forall uE uM' uAMB' uG' uS' loc,
  ufree uE loc = Some (MkuEnv uM' uAMB' uG' uS') ->
  exists uM, exists uAMB,
  exists b, exists e,
  uE = MkuEnv uM uAMB uG' uS' /\
  accessMem uM loc = Some b /\ uAMB b = Some e /\
  (forall l a,
    l < b \/ l >= e ->
    accessMem uM l = a -> accessMem uM' l = a
  ) /\
  (forall l,
    b <= l < e -> exists v, accessMem uM l = Some v
  ) /\
  (forall l,
    b <= l < e -> accessMem uM' l = None
  ) /\
  e <= uE.(ustack).(utop) /\
  b >= baseAddress /\
  uAMB' = removeAllocMemBlock uAMB b
  .

ucreateFrame allocates a new frame on the top of the Stack without changing allocated memory. udestroyFrame simply removes the latest frame from the stack. ucreateFrame fails if there is not enough space; udestroyFrame fails if the runtime removes a frame from an empty stack.
Axiom ucreateFrame__inversion : forall uE f uE',
  ucreateFrame uE f = Some uE' ->
  exists uF,
  f = uStack2frame (uE'.(ustack)) /\
  uE.(uglobal) = uE'.(uglobal) /\
  uE.(uamb) = uE'.(uamb) /\
  head (uE'.(ustack).(uframes)) = Some uF /\
  uF.(uto) = uE.(ustack).(utop) /\
  uF.(ufrom) = uE'.(ustack).(utop) /\
  baseAddress < uE'.(ustack).(utop) < uE.(ustack).(utop) /\
  tail (uE'.(ustack).(uframes)) = uE.(ustack).(uframes) /\
  (forall v t,
      f v = Some t ->
     exists l,
        lookUpuStack uE'.(ustack) v = Some (l, t) /\
        uF.(ufrom) <= l < uF.(uto)
  ) /\
  (forall l v,
     accessMem uE.(umem) l = Some v -> accessMem uE'.(umem) l = Some v
  ) /\
  (forall l,
    l < uF.(ufrom) \/ l >= uF.(uto) ->
    accessMem uE.(umem) l = None -> accessMem uE'.(umem) l = None
    ) /\
  (forall l,
      uF.(ufrom) <= l < uF.(uto) ->
      accessMem uE.(umem) l = None
  ) /\
  (forall l,
      uF.(ufrom) <= l < uF.(uto) ->
      accessMem uE'.(umem) l = Some 0
  ) /\
  wfuFrameNoOverlapped uF
  .

Axiom udestroyFrame__inversion : forall uE uE',
  udestroyFrame uE = Some uE' ->
  exists uF,
  uE.(uglobal) = uE'.(uglobal) /\
  uE.(uamb) = uE'.(uamb) /\
  head (uE.(ustack).(uframes)) = Some uF /\
  uE'.(ustack).(utop) = uF.(uto) /\
  uE'.(ustack).(uframes) = tail (uE.(ustack).(uframes)) /\
  (forall l a,
    l < uF.(ufrom) \/ l >= uF.(uto) ->
    accessMem (umem uE) l = a -> accessMem (umem uE') l = a
  ) /\
  (forall l,
    uF.(ufrom) <= l < uF.(uto) -> exists v, accessMem (umem uE) l = Some v
  ) /\
  (forall l,
    uF.(ufrom) <= l < uF.(uto) -> accessMem (umem uE') l = None
  )
  .