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; +} _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
