Formal verification of XOR swap in C

run.sh

#! /usr/bin/env nix-shell
#! nix-shell -i bash -p coq_8_13 coqPackages.VST compcert
#! nix-shell -I nixpkgs=https://github.com/NixOS/nixpkgs/archive/432fc2d9a67f92e05438dff5fdc2b39d33f77997.tar.gz
# Run this file with NIXPKGS_ALLOW_UNFREE=1 ./run.sh
set -uex

clightgen -normalize xor_swap.c
coqc xor_swap.v
coqc Verif_xor_swap.v

Verif_xor_swap.v

Require Import VST.floyd.proofauto.
Require Import VST.floyd.library.
Require Import xor_swap.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs.  mk_varspecs prog. Defined.

(* Specification of xor swap. In words:

   Let a and b be unsigned int pointers to values n and m
   respectively, with respective writable shares sh1 and sh2, and
   a ≠ b.

   Then the postcondition of XorSwap states that a and b will point to
   m and n respectively.
*)
Definition XorSwap_spec : ident * funspec :=
DECLARE _XorSwap
 WITH a : val, b : val, sh1 : share, sh2 : share, n : Z, m : Z
 PRE [ tptr tuint, tptr tuint ]
  PROP  (writable_share sh1; writable_share sh2; a <> b)
  PARAMS (a; b)
  SEP   (data_at sh1 tuint (Vint (Int.repr n)) a;
         data_at sh2 tuint (Vint (Int.repr m)) b)
 POST [ tvoid ]
  PROP (writable_share sh1; writable_share sh2)
  RETURN ()
  SEP (data_at sh1 tuint (Vint (Int.repr m)) a;
       data_at sh2 tuint (Vint (Int.repr n)) b).

(* We also give a spec for the main function *)
Definition main_spec :=
 DECLARE _main
 WITH gv: globals
 PRE [ ] main_pre prog tt gv
 POST [ tint ]
   PROP ()
   RETURN (Vint (Int.repr 2))
   SEP (TT).

Definition Gprog : funspecs :=
  ltac:(with_library prog [ XorSwap_spec; main_spec ]).

Lemma body_XorSwap: semax_body Vprog Gprog f_XorSwap XorSwap_spec.
Proof.
  start_function.
  forward_if.
  - forward. forward. forward. forward. forward. forward. forward. forward.
    forward. entailer!. remember (Int.repr n) as n'. remember (Int.repr m) as m'.
    rewrite Int.xor_commut, (Int.xor_assoc m' (Int.xor n' m') _), Int.xor_idem, Int.xor_zero.
    rewrite Int.xor_commut, Int.xor_assoc, Int.xor_idem, Int.xor_zero. auto.
  - forward. entailer!. autorewrite with norm in H0.
    now destruct (eq_dec a b).
Qed.


Lemma body_main:  semax_body Vprog Gprog f_main main_spec.
Proof.
  start_function.
  forward. forward.
  (* stack allocated variables must be separate *)
  assert_PROP (v_a <> v_b) by entailer!.
  forward_call. forward. forward. forward. entailer!.
Qed.

(* Use a trivial external specification since we don't do any external
   I/O. *)
Existing Instance NullExtension.Espec.

(* Prove that the whole program prog is correct. *)
Lemma prog_correct: semax_prog prog tt Vprog Gprog.
Proof.
  prove_semax_prog.

  semax_func_cons body_XorSwap.
  semax_func_cons body_main.
Qed.

xor_swap.c

#include <stddef.h>

void XorSwap(unsigned int *x, unsigned int *y)
{
  if (x != y)
  {
    *x ^= *y;
    *y ^= *x;
    *x ^= *y;
  }
}

int main() {
  unsigned int a = 3;
  unsigned int b = 5;
  XorSwap(&a, &b);
  return (int) (a - b);
}