Fix wrapped pointer arithmetic and comparisons

lib/smack/Prelude.cpp

@@ -1205,23 +1205,28 @@ void PtrOpGen::generatePtrNumConvs(std::stringstream &s) const {
 void PtrOpGen::generatePreds(std::stringstream &s) const {
   describe("Pointer predicates", s);
 
-  using PredInfo = std::pair<std::string, BinExpr::Binary>;
+  // Wrapped non-bitvector pointer-producing operations use signed-canonical
+  // values. Only unsigned ordering needs the unsigned representation.
+  using PredInfo = std::tuple<std::string, BinExpr::Binary, bool>;
   const std::vector<PredInfo> predicates{
-      {"$eq", BinExpr::Eq},   {"$ne", BinExpr::Neq},  {"$ugt", BinExpr::Gt},
-      {"$uge", BinExpr::Gte}, {"$ult", BinExpr::Lt},  {"$ule", BinExpr::Lte},
-      {"$sgt", BinExpr::Gt},  {"$sge", BinExpr::Gte}, {"$slt", BinExpr::Lt},
-      {"$sle", BinExpr::Lte}};
+      {"$eq", BinExpr::Eq, false},  {"$ne", BinExpr::Neq, false},
+      {"$ugt", BinExpr::Gt, true},  {"$uge", BinExpr::Gte, true},
+      {"$ult", BinExpr::Lt, true},  {"$ule", BinExpr::Lte, true},
+      {"$sgt", BinExpr::Gt, false}, {"$sge", BinExpr::Gte, false},
+      {"$slt", BinExpr::Lt, false}, {"$sle", BinExpr::Lte, false}};
 
   // e.g., function {:inline} $eq.ref(p1: ref, p2: ref)
   // returns (i1) { (if $eq.i64.bool(p1, p2) then 1 else 0) }
   for (auto info : predicates) {
-    auto predName = info.first;
-    auto binPred = info.second;
+    auto predName = std::get<0>(info);
+    auto binPred = std::get<1>(info);
+    auto isUnsigned = std::get<2>(info);
     auto condExpr = Expr::fn(
         indexedName(predName, {prelude.rep.pointerType(), Naming::BOOL_TYPE}),
         {makePtrVarExpr(1), makePtrVarExpr(2)});
     const Expr *predExpr =
-        SmackOptions::BitPrecisePointers
+        SmackOptions::BitPrecisePointers ||
+                (SmackOptions::WrappedIntegerEncoding && isUnsigned)
             ? condExpr
             : new BinExpr(binPred, makePtrVarExpr(1), makePtrVarExpr(2));
 
@@ -1251,15 +1256,21 @@ void PtrOpGen::generateArithOps(std::stringstream &s) const {
 
   const std::vector<std::string> operations = {"$add", "$sub", "$mul"};
 
-  // e.g., function {:inline} $add.ref(p1: ref, p2: ref) returns (ref) {
-  // $add.i64(p1, p2) }
+  // Under wrapped integer encoding, for example:
+  // function {:inline} $add.ref(p1: ref, p2: ref) returns (ref) {
+  //   $tos.i64($add.i64(p1, p2))
+  // }
   for (auto op : operations) {
+    const Expr *arithExpr =
+        Expr::fn(indexedName(op, {prelude.rep.pointerType()}),
+                 {Expr::id("p1"), Expr::id("p2")});
+    if (!SmackOptions::BitPrecisePointers)
+      arithExpr = IntOpGen::IntArithOp::wrappedExpr(prelude.rep.ptrSizeInBits,
+                                                    arithExpr, false);
+
     s << Decl::function(indexedName(op, {Naming::PTR_TYPE}),
                         {{"p1", Naming::PTR_TYPE}, {"p2", Naming::PTR_TYPE}},
-                        Naming::PTR_TYPE,
-                        Expr::fn(indexedName(op, {prelude.rep.pointerType()}),
-                                 {Expr::id("p1"), Expr::id("p2")}),
-                        {makeInlineAttr()})
+                        Naming::PTR_TYPE, arithExpr, {makeInlineAttr()})
       << "\n";
   }
   s << "\n";

lib/smack/SmackRep.cpp

@@ -585,6 +585,9 @@ const Expr *SmackRep::integerToPointer(const Expr *e, unsigned width) {
     e = Expr::fn(opName("$trunc", {width, ptrSizeInBits}), e);
   e = bitConversion(e, SmackOptions::BitPrecise,
                     SmackOptions::BitPrecisePointers);
+  // Non-bitvector pointers use the signed-canonical machine representation.
+  if (SmackOptions::WrappedIntegerEncoding && !SmackOptions::BitPrecisePointers)
+    e = Expr::fn(opName(Naming::getIntWrapFunc(false), {ptrSizeInBits}), e);
   return e;
 }
 

test/c/data/wrapped_pointer_arithmetic.c

@@ -0,0 +1,19 @@
+#include "smack.h"
+#include <assert.h>
+#include <stdlib.h>
+
+// @expect verified
+// @flag --integer-encoding=wrapped-integer
+
+int main() {
+  int *arr = (int *)malloc(3 * sizeof(int));
+  unsigned long long idx = __VERIFIER_nondet_unsigned_long_long();
+
+  assume(arr[0] < 4);
+  assume(arr[1] < 5);
+  assume(arr[2] < 6);
+  assume(idx < 3);
+
+  assert(arr[idx] <= 5);
+  return 0;
+}

test/llvm/wrapped-pointer-comparison.ll

@@ -0,0 +1,40 @@
+; @expect verified
+; @flag --integer-encoding=wrapped-integer
+
+target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128"
+target triple = "x86_64-unknown-linux-gnu"
+
+define i32 @main() {
+  %base_value = call i64 @__SMACK_nondet_unsigned_long_long()
+  %is_signed_max = icmp eq i64 %base_value, 9223372036854775807
+  %base_assume_arg = zext i1 %is_signed_max to i32
+  call void @__VERIFIER_assume(i32 %base_assume_arg)
+
+  %base_pointer = inttoptr i64 %base_value to i8*
+  %incremented_pointer = getelementptr i8, i8* %base_pointer, i64 1
+  %signed_min_pointer = inttoptr i64 -9223372036854775808 to i8*
+  %arithmetic_is_correct = icmp eq i8* %incremented_pointer, %signed_min_pointer
+
+  %value = call i64 @__SMACK_nondet_unsigned_long_long()
+  %is_minus_one = icmp eq i64 %value, -1
+  %assume_arg = zext i1 %is_minus_one to i32
+  call void @__VERIFIER_assume(i32 %assume_arg)
+
+  %pointer = inttoptr i64 %value to i8*
+  %roundtrip_value = ptrtoint i8* %pointer to i64
+  %roundtrip_pointer = inttoptr i64 %roundtrip_value to i8*
+  %roundtrip_is_correct = icmp eq i8* %roundtrip_pointer, %pointer
+  %is_unsigned_lt_null = icmp ult i8* %pointer, null
+  %is_signed_lt_null = icmp slt i8* %pointer, null
+  %is_not_unsigned_lt_null = xor i1 %is_unsigned_lt_null, true
+  %comparison_is_correct = and i1 %is_not_unsigned_lt_null, %is_signed_lt_null
+  %cast_and_comparison_are_correct = and i1 %roundtrip_is_correct, %comparison_is_correct
+  %result_is_correct = and i1 %arithmetic_is_correct, %cast_and_comparison_are_correct
+  %assert_arg = zext i1 %result_is_correct to i32
+  call void @__VERIFIER_assert(i32 %assert_arg)
+  ret i32 0
+}
+
+declare i64 @__SMACK_nondet_unsigned_long_long()
+declare void @__VERIFIER_assume(i32)
+declare void @__VERIFIER_assert(i32)