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

[Balázs Benics via Phabricator via cfe-commits]

This revision was automatically updated to reflect the committed changes.
Closed by commit rGd882750f1105: [analyzer] Fix a crash for dereferencing an empty llvm::Optional variable in… (authored by OikawaKirie, committed by steakhal).

Changed prior to commit:
  https://reviews.llvm.org/D83660?vs=333708&id=342738#toc

Repository:
  rG LLVM Github Monorepo

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.342738.patch
Type: text/x-patch
Size: 2873 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20210504/f8e5b486/attachment-0001.bin>