CODEWITHSUNDEEP
verifiable-c
schoppenhauer
schoppenhauer

Reputation: 421

Proving correctness of Xor-Swapping

Update: Now I have the following program swap.c:

void swap (int* a, int* b) {
  int ta = *a;             
  int tb = *b;            
  ta = ta ^ tb;
  tb = ta ^ tb;
  ta = ta ^ tb;
  *a = ta;
  *b = tb;                           
}

My specification is

Require Import floyd.proofauto.
Require Import floyd.entailer.
Require Import veric.SeparationLogic.

Require Import swap.

Local Open Scope logic.
Local Open Scope Z.

Definition swap_spec :=
  DECLARE _swap
   WITH sh : share, aptr : val, a : int, bptr : val, b : int
     PRE [ _a OF (tptr tint), _b OF (tptr tint)]
       PROP ()
       LOCAL (`(eq aptr) (eval_id _a);
              `(eq bptr) (eval_id _b))
       SEP (` (mapsto sh tint aptr (Vint a));
            ` (mapsto sh tint bptr (Vint b)))
       POST [tint] (`(mapsto sh tint aptr (Vint b)) *
                    `(mapsto sh tint bptr (Vint a))).

Definition Vprog : varspecs := nil.
Definition Gprog : funspecs := swap_spec :: nil.

Lemma body_swap : semax_body Vprog Gprog f_swap swap_spec.
Proof.
  start_function.
  forward.
  forward.
  forward.
  forward.
  forward.  
  eapply semax_seq.
  eapply semax_seq.

Now I am stuck: I can unfold eval_binop, and try to proceed unfolding, but it doesn't really converge to anything that I can work with. Furthermore, I am not sure how to use the `eq properties to actually rewrite anything.

Upvotes: 1

Views: 214

Answers (1)

Andrew Appel
Andrew Appel

Reputation: 548

Your specification looks correct.

In Verifiable C's standard Separation Logic, you can reason about only one load or store per C statement, so you will have to rewrite the code as,

ta = *a; tb = *b; *a = ta^tb;
ta = *a; tb = *b; *b = ta^tb;
ta = *a; tb = *b; *a = ta^tb;

Upvotes: 1

Related Questions