[clang] d882750 - [analyzer] Fix a crash for dereferencing an empty llvm::Optional variable in SMTConstraintManager.h.

[Balazs Benics via cfe-commits]

Author: Ella Ma
Date: 2021-05-04T16:50:21+02:00
New Revision: d882750f1105b20d892545e7ebd96f82166dcb53

URL: https://github.com/llvm/llvm-project/commit/d882750f1105b20d892545e7ebd96f82166dcb53
DIFF: https://github.com/llvm/llvm-project/commit/d882750f1105b20d892545e7ebd96f82166dcb53.diff

LOG: [analyzer] Fix a crash for dereferencing an empty llvm::Optional variable in SMTConstraintManager.h.

The first crash reported in the bug report 44338.

Condition `!isSat.hasValue() || isNotSat.getValue()` here should be
`!isNotSat.hasValue() || isNotSat.getValue()`.
`getValue()` here crashed when we used the static analyzer to analyze
postgresql-12.0.

Patch By: OikawaKirie

Reviewed By: steakhal, martong

Differential Revision: https://reviews.llvm.org/D83660

Added: 
    clang/test/Analysis/z3/D83660.c
    clang/test/Analysis/z3/Inputs/MockZ3_solver_check.c

Modified: 
    clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

Removed: 
    


################################################################################
diff  --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index 07fc73a670f35..e4878d4e01564 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -146,7 +146,7 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
       Solver->addConstraint(NotExp);
 
       Optional<bool> isNotSat = Solver->check();
-      if (!isSat.hasValue() || isNotSat.getValue())
+      if (!isNotSat.hasValue() || isNotSat.getValue())
         return nullptr;
 
       // This is the only solution, store it

diff  --git a/clang/test/Analysis/z3/D83660.c b/clang/test/Analysis/z3/D83660.c
new file mode 100644
index 0000000000000..fd463333a51e3
--- /dev/null
+++ b/clang/test/Analysis/z3/D83660.c
@@ -0,0 +1,23 @@
+// RUN: rm -rf %t && mkdir %t
+// RUN: %host_cxx -shared -fPIC %S/Inputs/MockZ3_solver_check.c -o %t/MockZ3_solver_check.so
+//
+// RUN: LD_PRELOAD="%t/MockZ3_solver_check.so"                                       \
+// RUN: %clang_cc1 -analyze -analyzer-constraints=z3 -setup-static-analyzer          \
+// RUN:   -analyzer-checker=core,debug.ExprInspection %s -verify 2>&1 | FileCheck %s
+//
+// REQUIRES: z3, asserts, shell, system-linux
+//
+// Works only with the z3 constraint manager.
+// expected-no-diagnostics
+
+// CHECK:      Z3_solver_check returns the real value: TRUE
+// CHECK-NEXT: Z3_solver_check returns the real value: TRUE
+// CHECK-NEXT: Z3_solver_check returns the real value: TRUE
+// CHECK-NEXT: Z3_solver_check returns the real value: TRUE
+// CHECK-NEXT: Z3_solver_check returns a mocked value: UNDEF
+
+void D83660(int b) {
+  if (b) {
+  }
+  (void)b; // no-crash
+}

diff  --git a/clang/test/Analysis/z3/Inputs/MockZ3_solver_check.c b/clang/test/Analysis/z3/Inputs/MockZ3_solver_check.c
new file mode 100644
index 0000000000000..9c63a64ada220
--- /dev/null
+++ b/clang/test/Analysis/z3/Inputs/MockZ3_solver_check.c
@@ -0,0 +1,28 @@
+#include <dlfcn.h>
+#include <stdio.h>
+
+#include <z3.h>
+
+// Mock implementation: return UNDEF for the 5th invocation, otherwise it just
+// returns the result of the real invocation.
+Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s) {
+  static Z3_lbool (*OriginalFN)(Z3_context, Z3_solver);
+  if (!OriginalFN) {
+    OriginalFN = (Z3_lbool(*)(Z3_context, Z3_solver))dlsym(RTLD_NEXT,
+                                                           "Z3_solver_check");
+  }
+
+  // Invoke the actual solver.
+  Z3_lbool Result = OriginalFN(c, s);
+
+  // Mock the 5th invocation to return UNDEF.
+  static unsigned int Counter = 0;
+  if (++Counter == 5) {
+    fprintf(stderr, "Z3_solver_check returns a mocked value: UNDEF\n");
+    return Z3_L_UNDEF;
+  }
+  fprintf(stderr, "Z3_solver_check returns the real value: %s\n",
+          (Result == Z3_L_UNDEF ? "UNDEF"
+                                : ((Result == Z3_L_TRUE ? "TRUE" : "FALSE"))));
+  return Result;
+}