B13: memcpy, memmove, memset, memcmp, and abs through models, and quantifiers over shifted slices

clang/lib/Headers/cppverify.h

@@ -218,6 +218,93 @@ struct map {
 };
 map map_empty();
 
+/* The meaning the verifier gives to the C library's memcpy, memmove, memset,
+ * and memcmp. A call with pointers to an integer type T, written before their
+ * conversion to void *, and a size of k * sizeof(T) bytes is a call of the
+ * model for T with k: whole objects, which keep their values bit for bit.
+ * The models are trusted: a proof that uses one names it in [trusts=...].
+ * Distinct pointer parameters of which one is mutable address separate
+ * objects (memcpy's ranges must not overlap); memmove's may overlap. */
+namespace model {
+
+#define __CPPVERIFY_MEMORY_MODELS(T)                                           \
+  [[cppverify::trusted]] T *memcpy(T *d, const T *s, __SIZE_TYPE__ k)          \
+      cppverify::pre(cppverify::valid(d, k) && cppverify::valid(s, k))         \
+      cppverify::modifies(d[0 : k])                                            \
+      cppverify::post(cppverify::forall(i, 0, k, d[i] == cppverify::old(s[i])))\
+      cppverify::post(cppverify::result == d);                                 \
+  [[cppverify::trusted]] T *memmove(T *d, const T *s, __SIZE_TYPE__ k)         \
+      cppverify::aliases(d, s)                                                 \
+      cppverify::pre(cppverify::valid(d, k) && cppverify::valid(s, k))         \
+      cppverify::modifies(d[0 : k])                                            \
+      cppverify::post(cppverify::forall(i, 0, k, d[i] == cppverify::old(s[i])))\
+      cppverify::post(cppverify::result == d);
+
+/* memset(d, c, n) stores the byte (unsigned char)c in every byte: v is that
+ * byte repeated in an object of type T. */
+#define __CPPVERIFY_MEMSET_MODEL(T)                                            \
+  [[cppverify::trusted]] T *memset(T *d, T v, __SIZE_TYPE__ k)                 \
+      cppverify::pre(cppverify::valid(d, k))                                   \
+      cppverify::modifies(d[0 : k])                                            \
+      cppverify::post(cppverify::forall(i, 0, k, d[i] == v))                   \
+      cppverify::post(cppverify::result == d);
+
+/* memcmp is 0 exactly when the objects are equal. Of bytes, its sign is that
+ * of the first difference, as unsigned char; of wider objects that depends
+ * on the byte order, and only equality is modeled. */
+#define __CPPVERIFY_MEMCMP_MODEL(T)                                            \
+  [[cppverify::trusted]] int memcmp(const T *a, const T *b, __SIZE_TYPE__ k)   \
+      cppverify::pre(cppverify::valid(a, k) && cppverify::valid(b, k))         \
+      cppverify::post((cppverify::result == 0) ==                              \
+                      cppverify::forall(i, 0, k, a[i] == b[i]));
+#define __CPPVERIFY_BYTE_MEMCMP_MODEL(T)                                       \
+  [[cppverify::trusted]] int memcmp(const T *a, const T *b, __SIZE_TYPE__ k)   \
+      cppverify::pre(cppverify::valid(a, k) && cppverify::valid(b, k))         \
+      cppverify::post((cppverify::result == 0) ==                              \
+                      cppverify::forall(i, 0, k, a[i] == b[i]))                \
+      cppverify::post(cppverify::forall(                                       \
+          j, 0, k,                                                             \
+          !cppverify::forall(i, 0, j, a[i] == b[i]) || a[j] == b[j] ||         \
+              (cppverify::result < 0) ==                                       \
+                  ((a[j] & 255) < (b[j] & 255))));
+
+#define __CPPVERIFY_WIDE_MODELS(T)                                             \
+  __CPPVERIFY_MEMORY_MODELS(T)                                                 \
+  __CPPVERIFY_MEMSET_MODEL(T)                                                  \
+  __CPPVERIFY_MEMCMP_MODEL(T)
+#define __CPPVERIFY_BYTE_MODELS(T)                                             \
+  __CPPVERIFY_MEMORY_MODELS(T)                                                 \
+  __CPPVERIFY_MEMSET_MODEL(T)                                                  \
+  __CPPVERIFY_BYTE_MEMCMP_MODEL(T)
+
+__CPPVERIFY_MEMORY_MODELS(bool)
+__CPPVERIFY_MEMCMP_MODEL(bool)
+__CPPVERIFY_BYTE_MODELS(char)
+__CPPVERIFY_BYTE_MODELS(signed char)
+__CPPVERIFY_BYTE_MODELS(unsigned char)
+__CPPVERIFY_WIDE_MODELS(wchar_t)
+#if __cplusplus >= 201103L
+__CPPVERIFY_WIDE_MODELS(char16_t)
+__CPPVERIFY_WIDE_MODELS(char32_t)
+#endif
+__CPPVERIFY_WIDE_MODELS(short)
+__CPPVERIFY_WIDE_MODELS(unsigned short)
+__CPPVERIFY_WIDE_MODELS(int)
+__CPPVERIFY_WIDE_MODELS(unsigned)
+__CPPVERIFY_WIDE_MODELS(long)
+__CPPVERIFY_WIDE_MODELS(unsigned long)
+__CPPVERIFY_WIDE_MODELS(long long)
+__CPPVERIFY_WIDE_MODELS(unsigned long long)
+
+#undef __CPPVERIFY_MEMORY_MODELS
+#undef __CPPVERIFY_MEMSET_MODEL
+#undef __CPPVERIFY_MEMCMP_MODEL
+#undef __CPPVERIFY_BYTE_MEMCMP_MODEL
+#undef __CPPVERIFY_WIDE_MODELS
+#undef __CPPVERIFY_BYTE_MODELS
+
+} // namespace model
+
 } // namespace cppverify
 
 #endif /* __cplusplus */

clang/lib/Verify/Backend/Obligation.cpp

@@ -276,6 +276,8 @@ ObligationKind verify::obligationKind(ProofObligationKind Kind) {
     return ObligationKind::MissingReturn;
   case ProofObligationKind::Unreachable:
     return ObligationKind::Unreachable;
+  case ProofObligationKind::BuiltinArgument:
+    return ObligationKind::BuiltinArgument;
   case ProofObligationKind::Unsupported:
     return ObligationKind::Unsupported;
   }
@@ -328,6 +330,8 @@ const char *verify::obligationKindName(ObligationKind Kind) {
     return "missing-return";
   case ObligationKind::Unreachable:
     return "unreachable";
+  case ObligationKind::BuiltinArgument:
+    return "builtin-argument";
   case ObligationKind::Unsupported:
     return "unsupported";
   }
@@ -2515,12 +2519,13 @@ class ObligationBuilder {
                        Stmt->Focus, Stmt->Clause});
     }
 
-    std::vector<
-        std::tuple<ObligationKind, std::unique_ptr<VCExpr>, std::string>>
+    std::vector<std::tuple<ObligationKind, std::unique_ptr<VCExpr>,
+                           std::string, SourceSpan>>
         ExitAsserts;
     for (const PassiveExitAssert &Exit : P.ExitAsserts)
       ExitAsserts.emplace_back(obligationKind(Exit.ProofKind),
-                               fromVExpr(Exit.Cond.get()), Exit.Note);
+                               fromVExpr(Exit.Cond.get()), Exit.Note,
+                               Exit.Anchor);
 
     // A theorem only where it speaks of the entry state alone: the body's
     // later states are not part of it.
@@ -2594,22 +2599,27 @@ class ObligationBuilder {
     auto appendObligation = [&](ObligationKind Kind, const VCExpr *Condition,
                                 uint64_t TraceEventCount,
                                 const std::string &Note = "",
-                                SourceSpan Focus = {}, SourceSpan Clause = {}) {
+                                SourceSpan Focus = {}, SourceSpan Clause = {},
+                                SourceSpan Anchor = {}) {
       Obligation Item;
       Item.Kind = Kind;
       Item.Note = Note;
       Item.Focus = Focus;
       Item.Clause = Clause;
-      Item.Loc = Condition->Loc;
-      Item.BeginLoc = Condition->BeginLoc;
-      Item.EndLoc = Condition->EndLoc;
+      if (Anchor.isValid())
+        Item.Focus = {Condition->Loc, Condition->BeginLoc, Condition->EndLoc};
+      else
+        Anchor = {Condition->Loc, Condition->BeginLoc, Condition->EndLoc};
+      Item.Loc = Anchor.Loc;
+      Item.BeginLoc = Anchor.BeginLoc;
+      Item.EndLoc = Anchor.EndLoc;
       Item.TraceEventCount = TraceEventCount;
       Item.Id = Identity + "::obligation:" + std::to_string(++ObligationIndex);
       Item.Goal = makeGoal(Condition);
       Item.CounterexampleQuery = vcNot(cloneLogicExpr(Item.Goal.get()));
-      Item.CounterexampleQuery->Loc = Condition->Loc;
-      Item.CounterexampleQuery->BeginLoc = Condition->BeginLoc;
-      Item.CounterexampleQuery->EndLoc = Condition->EndLoc;
+      Item.CounterexampleQuery->Loc = Anchor.Loc;
+      Item.CounterexampleQuery->BeginLoc = Anchor.BeginLoc;
+      Item.CounterexampleQuery->EndLoc = Anchor.EndLoc;
       M.Obligations.push_back(std::move(Item));
     };
 
@@ -2625,8 +2635,9 @@ class ObligationBuilder {
       if (oversize())
         return ObligationSizeError::obligations(size(), MaxNodes);
     }
-    for (const auto &[Kind, Exit, Note] : ExitAsserts) {
-      appendObligation(Kind, Exit.get(), M.TraceEvents.size(), Note);
+    for (const auto &[Kind, Exit, Note, Anchor] : ExitAsserts) {
+      appendObligation(Kind, Exit.get(), M.TraceEvents.size(), Note, {}, {},
+                       Anchor);
       if (oversize())
         return ObligationSizeError::obligations(size(), MaxNodes);
     }

clang/lib/Verify/Backend/Obligation.h

@@ -285,6 +285,7 @@ enum class ObligationKind {
   Deallocation,
   MissingReturn,
   Unreachable,
+  BuiltinArgument,
   Unsupported
 };
 

clang/lib/Verify/Backend/ObligationSerialization.cpp

@@ -329,6 +329,8 @@ uint8_t obligationTag(ObligationKind Kind) {
     return 21;
   case ObligationKind::Unreachable:
     return 23;
+  case ObligationKind::BuiltinArgument:
+    return 24;
   case ObligationKind::Unsupported:
     return 22;
   }
@@ -386,6 +388,10 @@ std::optional<ObligationKind> obligationFromTag(uint8_t Tag, uint32_t Version) {
     return ObligationKind::Unsupported;
   case 23:
     return ObligationKind::Unreachable;
+  case 24:
+    if (Version < 6)
+      return std::nullopt;
+    return ObligationKind::BuiltinArgument;
   default:
     return std::nullopt;
   }

clang/lib/Verify/Driver/Counterexample.cpp

@@ -193,6 +193,7 @@ bool isDefinedness(ObligationKind Kind) {
   case ObligationKind::Initialization:
   case ObligationKind::PointerDifference:
   case ObligationKind::PointerValidity:
+  case ObligationKind::BuiltinArgument:
     return true;
   default:
     return false;
@@ -289,8 +290,7 @@ FailurePlace verify::failingPlace(const ObligationModule &Module,
       return nullptr;
     }
     if (Generated && E->K == LogicExpr::Or && E->Children.size() == 2 &&
-        E->Children[0]->K == LogicExpr::Not && isFalse(E->Children[0].get()) &&
-        isFalse(E->Children[1].get()))
+        isFalse(E->Children[0].get()) && isFalse(E->Children[1].get()))
       if (const LogicExpr *Part = falsePart(E->Children[1].get()))
         return Part;
     return placed(E) ? E : nullptr;