macaw-symbolic: Simplify doPtrEq

[langston-barrett]

doPtrEq is defined like so:

doPtrEq :: PtrOp sym w (RegValue sym BoolType)
doPtrEq = ptrOp $ \bak _mem w xPtr xBits yPtr yBits x y ->
  do let sym = backendGetSym bak
     both_bits <- andPred sym xBits yBits
     both_ptrs <- andPred sym xPtr  yPtr
     xNull <- isNullPtr sym w x
     yNull <- isNullPtr sym w y
     both_null <- andPred sym xNull yNull
     undef <- mkUndefinedBool sym "ptr_eq"
     let nw = M.addrWidthNatRepr w
     cases bak (binOpLabel "ptr_eq" x y) itePred (Just undef)
       [ both_bits ~> endCase =<< bvEq sym (asBits x) (asBits y)
       , both_ptrs ~> endCase =<< ptrEq sym nw x y
       , both_null ~> endCase (truePred sym)
       , xNull ~> endCase (falsePred sym)
       , yNull ~> endCase (falsePred sym)
       ]

Here are the definitions of {x,y}Ptr and {x,y}Bits:

xBits <- natEq sym (ptrBase x) zero
xPtr <- notPred sym xBits

yBits <- natEq sym (ptrBase y) zero
yPtr <- notPred sym yBits

To me, the cases read:

1. If both block numbers are zero, compare the offsets for equality.
2. If both block numbers are nonzero, compare both block numbers and pointers for equality.
3. If both block numbers are zero and offsets are zero, return true.
4. If only one of the pointers is null, return false.
5. If none of this is true, return an "undefined" pointer.

First of all, case (3) seems subsumed entirely by case (1).

Secondly, it seems that this could more easily be written as the following three cases:

1. If x is a pointer and y is not, return undef.
2. If y is a pointer and x is not, return undef.
3. Otherwise, compare block numbers and offsets for equality.

[Ptival]

I did a small Coq proof and found a small subtlety:

From Coq Require Import ssreflect.
From mathcomp Require Import ssreflect.eqtype.
From mathcomp Require Import ssreflect.ssrnat.

Definition old (v1 v2 : (nat * nat)) :=
  let '(b1, o1) := v1 in
  let '(b2, o2) := v2 in
  if (b1 == 0) && (b2 == 0) then Some (o1 == o2)%bool
  else if (b1 != 0) && (b2 != 0) then Some ((b1 == b2) && (o1 == o2))%bool
  else if (b1 == 0) && (o1 == 0) && (b2 == 0) && (o2 == 0) then Some true
  else if (b1 == 0) && (o1 == 0) then Some false
  else if (b2 == 0) && (o2 == 0) then Some false
  else None (* undef *)
.

Definition new (v1 v2 : (nat * nat)) :=
  let '(b1, o1) := v1 in
  let '(b2, o2) := v2 in
  if (b1 == 0) && (b2 != 0) then (if (o1 == 0) then Some false else None)
  else if (b1 != 0) && (b2 == 0) then (if (o2 == 0) then Some false else None)
  else Some ((b1 == b2) && (o1 == o2))%bool.

Theorem old_same_as_new : forall v1 v2, old v1 v2 = new v1 v2.
Proof.
  move => [b1 o1] [b2 o2].
  rewrite /old /new.
  case B1 : (b1 == 0)%bool => //=.
  {
    case B2 : (b2 == 0)%bool => //=.
    {
      move : B1 B2.
      elim : b1 => //= _.
      elim : b2 => //= _.
    }
    {
      case O1 : (o1 == 0)%bool => //=.
    }
  }
  {
    case B2 : (b2 == 0)%bool => //=.
  }
Qed.

Namely, when one is a pointer and the other is not, the old code returns undef only when the pointer is non-null, otherwise it returns false.