[analyzer][StdLibraryFunctionsChecker] Elaborate the summary of fread and fwrite

[martong]

Summary

Add the BufferSize argument constraint to fread and fwrite. This change
itself makes it possible to discover a security critical case, described
in SEI-CERT ARR38-C.

We also add the not-null constraint on the 3rd arguments.

In this patch, I also remove those lambdas that don't take any
parameters (Fwrite, Fread, Getc), thus making the code better
structured.

[balazske]

This checker will make an additional assumption on fread and fwrite with the ReturnValueCondition. The return value is constrained by StreamChecker too but it splits the error (if returned value is less that arg 3) and non-error cases into separate branches. I think this causes no problem because it will refine the assumption made here (if this assumption is made first) or the assumption here has no effect (if the split happened already).

[martong]

In D87081#2256636, @balazske wrote:

This checker will make an additional assumption on fread and fwrite with the ReturnValueCondition.

There is nothing new in that. This assumption described by the .Case has been here since the inception of this Checker. This patch does not change it. This patch adds two new argument constraints.

The return value is constrained by StreamChecker too but it splits the error (if returned value is less that arg 3) and non-error cases into separate branches. I think this causes no problem because it will refine the assumption made here (if this assumption is made first) or the assumption here has no effect (if the split happened already).

Either way, this is not a problem. However, in a similar case with the CallAndMessage Checker, we decided to list the more specific Checker as a dependency. We could do that with StreamChecker too, if you think that's better that way. But I'd rather keep that as it is now, since as you suggests, it works now and will work even after this patch.

[Szelethus]

The patch looks great, in fact, it demonstrates how well thought out your summary crafting machinery is.

In D87081#2258579, @martong wrote:

However, in a similar case with the CallAndMessage Checker, we decided to list the more specific Checker as a dependency.

We got the answer to D77061#2057063! We should turn it into a weak dependency though (D80905).

In D87081#2256636, @balazske wrote:

This checker will make an additional assumption on fread and fwrite with the ReturnValueCondition. The return value is constrained by StreamChecker too but it splits the error (if returned value is less that arg 3) and non-error cases into separate branches. I think this causes no problem because it will refine the assumption made here (if this assumption is made first) or the assumption here has no effect (if the split happened already).

Be sure to triple check whether the ExplodedGraph looks okay with both checkers enabled.

[martong]

In D87081#2258637, @Szelethus wrote:

The patch looks great, in fact, it demonstrates how well thought out your summary crafting machinery is.

In D87081#2258579, @martong wrote:

However, in a similar case with the CallAndMessage Checker, we decided to list the more specific Checker as a dependency.

We got the answer to D77061#2057063! We should turn it into a weak dependency though (D80905).

In D87081#2256636, @balazske wrote:

This checker will make an additional assumption on fread and fwrite with the ReturnValueCondition. The return value is constrained by StreamChecker too but it splits the error (if returned value is less that arg 3) and non-error cases into separate branches. I think this causes no problem because it will refine the assumption made here (if this assumption is made first) or the assumption here has no effect (if the split happened already).

Be sure to triple check whether the ExplodedGraph looks okay with both checkers enabled.

I'll try to create tests that check the state in both order.

[martong]

• Add tests to verify compatibility of the two checkers

[Szelethus]

@balazske may have some closing words.

clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp

1262

differant->different

[martong]

There is a blatant regression we introduced in D87240. Actually, the test added here could have catched that regression.
See https://reviews.llvm.org/D87240#inline-812062
I am putting back the modeling dependency with this patch.

[martong]

Actually, the test added here could have catched that regression.

Correction: It is the new BufferSize argument constraint in fread's summary and the existing test test_fread_uninitialized in std-c-library-functions.c that could have catched that regression. (Not the test in std-c-library-functions-vs-stream-checker.c.)

[Szelethus]

Post-commit LGTM on the post-commit changes!

clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp

struct AddToFunctionSummaryMap {
     bool operator()(StringRef Name, Signature Sign, Summary Sum) {
       return operator()(Name, Sum.setSignature(Sign));
     }
     // Add several summaries for the given name.
     void operator()(StringRef Name, const std::vector<Summary> &Summaries) {
       for (const Summary &S : Summaries)
         operator()(Name, S);
     }
+    // Add the same summary for different names with the Signature explicitly
+    // given.
+    void operator()(std::vector<StringRef> Names, Signature Sign, Summary Sum) {
+      for (StringRef Name : Names)
+        operator()(Name, Sign, Sum);
+    }
   } addToFunctionSummaryMap(ACtx, FunctionSummaryMap, DisplayLoadedSummaries);
 
   // Below are helpers functions to create the summaries.
   auto ArgumentCondition = [](ArgNo ArgN, RangeKind Kind,
                               IntRangeVector Ranges) {
     return std::make_shared<RangeConstraint>(ArgN, Kind, Ranges);
   };
   auto BufferSize = [](auto... Args) {
auto NotNull = [&](ArgNo ArgN) {
     return std::make_shared<NotNullConstraint>(ArgN);
   };
 
   Optional<QualType> FileTy = lookupTy("FILE");
   Optional<QualType> FilePtrTy = getPointerTy(FileTy);
   Optional<QualType> FilePtrRestrictTy = getRestrictTy(FilePtrTy);
 
   // Templates for summaries that are reused by many functions.
-  auto Getc = [&]() {
-    return Summary(ArgTypes{FilePtrTy}, RetType{IntTy}, NoEvalCall)
-        .Case({ReturnValueCondition(WithinRange,
-                                    {{EOFv, EOFv}, {0, UCharRangeMax}})});
-  };
   auto Read = [&](RetType R, RangeInt Max) {
     return Summary(ArgTypes{Irrelevant, Irrelevant, SizeTy}, RetType{R},
                    NoEvalCall)
         .Case({ReturnValueCondition(LessThanOrEq, ArgNo(2)),
                ReturnValueCondition(WithinRange, Range(-1, Max))});
   };
-  auto Fread = [&]() {
-    return Summary(
-               ArgTypes{VoidPtrRestrictTy, SizeTy, SizeTy, FilePtrRestrictTy},
-               RetType{SizeTy}, NoEvalCall)
-        .Case({
-            ReturnValueCondition(LessThanOrEq, ArgNo(2)),
-        })
-        .ArgConstraint(NotNull(ArgNo(0)));
-  };
-  auto Fwrite = [&]() {
-    return Summary(ArgTypes{ConstVoidPtrRestrictTy, SizeTy, SizeTy,
-                            FilePtrRestrictTy},
-                   RetType{SizeTy}, NoEvalCall)
-        .Case({
-            ReturnValueCondition(LessThanOrEq, ArgNo(2)),
-        })
-        .ArgConstraint(NotNull(ArgNo(0)));
-  };
   auto Getline = [&](RetType R, RangeInt Max) {
     return Summary(ArgTypes{Irrelevant, Irrelevant, Irrelevant}, RetType{R},
                    NoEvalCall)
         .Case({ReturnValueCondition(WithinRange, {{-1, -1}, {1, Max}})});
   };
 
   // We are finally ready to define specifications for all supported functions.
   //
addToFunctionSummaryMap(
                      .ArgConstraint(ArgumentCondition(
                          0U, WithinRange, {{EOFv, EOFv}, {0, UCharRangeMax}})));
   addToFunctionSummaryMap(
       "toascii", Summary(ArgTypes{IntTy}, RetType{IntTy}, EvalCallAsPure)
                      .ArgConstraint(ArgumentCondition(
                          0U, WithinRange, {{EOFv, EOFv}, {0, UCharRangeMax}})));
 
   // The getc() family of functions that returns either a char or an EOF.
-    addToFunctionSummaryMap("getc", Getc());
-    addToFunctionSummaryMap("fgetc", Getc());
+  addToFunctionSummaryMap(
+      {"getc", "fgetc"}, Signature(ArgTypes{FilePtrTy}, RetType{IntTy}),
+      Summary(NoEvalCall)
+          .Case({ReturnValueCondition(WithinRange,
+                                      {{EOFv, EOFv}, {0, UCharRangeMax}})}));
   addToFunctionSummaryMap(
       "getchar", Summary(ArgTypes{}, RetType{IntTy}, NoEvalCall)
                      .Case({ReturnValueCondition(
                          WithinRange, {{EOFv, EOFv}, {0, UCharRangeMax}})}));
 
   // read()-like functions that never return more than buffer size.
-    addToFunctionSummaryMap("fread", Fread());
-    addToFunctionSummaryMap("fwrite", Fwrite());
+  auto FreadSummary =
+      Summary(NoEvalCall)
+          .Case({
+              ReturnValueCondition(LessThanOrEq, ArgNo(2)),
+          })
+          .ArgConstraint(NotNull(ArgNo(0)))
+          .ArgConstraint(NotNull(ArgNo(3)))
+          .ArgConstraint(BufferSize(/*Buffer=*/ArgNo(0), /*BufSize=*/ArgNo(1),
+                                    /*BufSizeMultiplier=*/ArgNo(2)));
+
+  // size_t fread(void *restrict ptr, size_t size, size_t nitems,
+  //              FILE *restrict stream);
+  addToFunctionSummaryMap(
+      "fread",
+      Signature(ArgTypes{VoidPtrRestrictTy, SizeTy, SizeTy, FilePtrRestrictTy},
+                RetType{SizeTy}),
+      FreadSummary);
+  // size_t fwrite(const void *restrict ptr, size_t size, size_t nitems,
+  //               FILE *restrict stream);
+  addToFunctionSummaryMap("fwrite",
+                          Signature(ArgTypes{ConstVoidPtrRestrictTy, SizeTy,
+                                             SizeTy, FilePtrRestrictTy},
+                                    RetType{SizeTy}),
+                          FreadSummary);
 
   // We are not sure how ssize_t is defined on every platform, so we
   // provide three variants that should cover common cases.
+  // FIXME Use lookupTy("ssize_t") instead of the `Read` lambda.
   // FIXME these are actually defined by POSIX and not by the C standard, we
   // should handle them together with the rest of the POSIX functions.
   addToFunctionSummaryMap("read", {Read(IntTy, IntMax), Read(LongTy, LongMax),
                                    Read(LongLongTy, LongLongMax)});
   addToFunctionSummaryMap("write", {Read(IntTy, IntMax), Read(LongTy, LongMax),
                                     Read(LongLongTy, LongLongMax)});
 
   // getline()-like functions either fail or read at least the delimiter.
+  // FIXME Use lookupTy("ssize_t") instead of the `Getline` lambda.
   // FIXME these are actually defined by POSIX and not by the C standard, we
   // should handle them together with the rest of the POSIX functions.
   addToFunctionSummaryMap("getline",
                           {Getline(IntTy, IntMax), Getline(LongTy, LongMax),
                            Getline(LongLongTy, LongLongMax)});
+  // FIXME getdelim's signature is differant than getline's!
   addToFunctionSummaryMap("getdelim",
                           {Getline(IntTy, IntMax), Getline(LongTy, LongMax),
                            Getline(LongLongTy, LongLongMax)});
 
   if (ModelPOSIX) {
 
     // long a64l(const char *str64);
     addToFunctionSummaryMap(

clang/test/Analysis/std-c-library-functions-arg-constraints.c

 void test_notnull_symbolic2(FILE *fp, int *buf) {
   if (!buf)                          // bugpath-note{{Assuming 'buf' is null}} \
             // bugpath-note{{Taking true branch}}
     fread(buf, sizeof(int), 10, fp); // \
     // report-warning{{Function argument constraint is not satisfied}} \
     // bugpath-warning{{Function argument constraint is not satisfied}} \
     // bugpath-note{{Function argument constraint is not satisfied}}
 }
+typedef __WCHAR_TYPE__ wchar_t;
+// This is one test case for the ARR38-C SEI-CERT rule.
+void ARR38_C_F(FILE *file) {
+  enum { BUFFER_SIZE = 1024 };
+  wchar_t wbuf[BUFFER_SIZE]; // bugpath-note{{'wbuf' initialized here}}
+
+  const size_t size = sizeof(*wbuf);
+  const size_t nitems = sizeof(wbuf);
+
+  // The 3rd parameter should be the number of elements to read, not
+  // the size in bytes.
+  fread(wbuf, size, nitems, file); // \
+  // report-warning{{Function argument constraint is not satisfied}} \
+  // bugpath-warning{{Function argument constraint is not satisfied}} \
+  // bugpath-note{{Function argument constraint is not satisfied}}
+}
 
 int __two_constrained_args(int, int);
 void test_constraints_on_multiple_args(int x, int y) {
   // State split should not happen here. I.e. x == 1 should not be evaluated
   // FALSE.
   __two_constrained_args(x, y);
   clang_analyzer_eval(x == 1); // \
   // report-warning{{TRUE}} \