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

[Ella Ma via Phabricator via cfe-commits]

OikawaKirie updated this revision to Diff 333708.
OikawaKirie added a comment.

In D83660#2597025 <https://reviews.llvm.org/D83660#2597025>, @steakhal wrote:

> I'm somewhat bothered that this patch is not landed yet. :|
>
> I made a **crude** mock to trigger the bug using `LD_PRELOAD`. F15707493: LD_PRELOAD-workaround.patch <https://reviews.llvm.org/F15707493>
> The test reproduces the issue and passes if you apply the fix from this patch.
>
> However, it requires compiling a shared object with the same compiler you used for building clang. I'm using the `c++` compiler, for now.
> I think it's a good starting point.

Simply replace the c++ compiler with `%host_cxx` compiler to compile the mock Z3 solver.


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D83660/new/

https://reviews.llvm.org/D83660

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
  clang/test/Analysis/z3/D83660.c
  clang/test/Analysis/z3/Inputs/MockZ3_solver_check.c


Index: clang/test/Analysis/z3/Inputs/MockZ3_solver_check.c
===================================================================
--- /dev/null
+++ 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;
+}
Index: clang/test/Analysis/z3/D83660.c
===================================================================
--- /dev/null
+++ 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
+}
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -146,7 +146,7 @@
       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


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D83660.333708.patch
Type: text/x-patch
Size: 2875 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20210328/4aaa98bc/attachment.bin>