[PATCH] D145584: [libc] Add support for setjmp and longjmp in riscv

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 508187.
mikhail.ramalho added a comment.

Update return


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D145584

Files:
  clang/docs/tools/clang-formatted-files.txt
  libc/config/linux/riscv64/entrypoints.txt
  libc/config/linux/riscv64/headers.txt
  libc/include/llvm-libc-types/jmp_buf.h
  libc/src/setjmp/CMakeLists.txt
  libc/src/setjmp/longjmp.cpp
  libc/src/setjmp/riscv64/CMakeLists.txt
  libc/src/setjmp/riscv64/longjmp.cpp
  libc/src/setjmp/riscv64/setjmp.cpp
  libc/src/setjmp/setjmp.cpp
  libc/src/setjmp/x86_64/CMakeLists.txt
  libc/src/setjmp/x86_64/longjmp.cpp
  libc/src/setjmp/x86_64/setjmp.cpp

Index: libc/src/setjmp/x86_64/setjmp.cpp
===
--- libc/src/setjmp/x86_64/setjmp.cpp
+++ libc/src/setjmp/x86_64/setjmp.cpp
@@ -7,15 +7,15 @@
 //===--===//
 
 #include "src/__support/common.h"
-#include "src/__support/macros/properties/architectures.h"
 #include "src/setjmp/setjmp_impl.h"
 
-#include 
+#if !defined(LIBC_TARGET_ARCH_IS_X86_64)
+#error "Invalid file include"
+#endif
 
 namespace __llvm_libc {
 
 LLVM_LIBC_FUNCTION(int, setjmp, (__jmp_buf * buf)) {
-#ifdef LIBC_TARGET_ARCH_IS_X86_64
   register __UINT64_TYPE__ rbx __asm__("rbx");
   register __UINT64_TYPE__ r12 __asm__("r12");
   register __UINT64_TYPE__ r13 __asm__("r13");
@@ -50,10 +50,6 @@
   buf->rsp = reinterpret_cast<__UINTPTR_TYPE__>(__builtin_frame_address(0)) +
  sizeof(__UINTPTR_TYPE__) * 2;
   buf->rip = reinterpret_cast<__UINTPTR_TYPE__>(__builtin_return_address(0));
-#else // LIBC_TARGET_ARCH_IS_X86_64
-#error "setjmp implementation not available for the target architecture."
-#endif
-
   return 0;
 }
 
Index: libc/src/setjmp/x86_64/longjmp.cpp
===
--- libc/src/setjmp/x86_64/longjmp.cpp
+++ libc/src/setjmp/x86_64/longjmp.cpp
@@ -8,14 +8,14 @@
 
 #include "src/setjmp/longjmp.h"
 #include "src/__support/common.h"
-#include "src/__support/macros/properties/architectures.h"
 
-#include 
+#if !defined(LIBC_TARGET_ARCH_IS_X86_64)
+#error "Invalid file include"
+#endif
 
 namespace __llvm_libc {
 
 LLVM_LIBC_FUNCTION(void, longjmp, (__jmp_buf * buf, int val)) {
-#ifdef LIBC_TARGET_ARCH_IS_X86_64
   register __UINT64_TYPE__ rbx __asm__("rbx");
   register __UINT64_TYPE__ rbp __asm__("rbp");
   register __UINT64_TYPE__ r12 __asm__("r12");
@@ -38,9 +38,6 @@
   LIBC_INLINE_ASM("mov %1, %0\n\t" : "=r"(r15) : "m"(buf->r15) :);
   LIBC_INLINE_ASM("mov %1, %0\n\t" : "=r"(rsp) : "m"(buf->rsp) :);
   LIBC_INLINE_ASM("jmp *%0\n\t" : : "m"(buf->rip));
-#else // LIBC_TARGET_ARCH_IS_X86_64
-#error "longjmp implementation not available for the target architecture."
-#endif
 }
 
 } // namespace __llvm_libc
Index: libc/src/setjmp/x86_64/CMakeLists.txt
===
--- libc/src/setjmp/x86_64/CMakeLists.txt
+++ libc/src/setjmp/x86_64/CMakeLists.txt
@@ -3,12 +3,12 @@
   SRCS
 setjmp.cpp
   HDRS
-setjmp_impl.h
-  COMPILE_OPTIONS
--O3 # We do not want any local variables in setjmp
--fno-omit-frame-pointer # The implementation assumes frame pointer on to the stack
+../setjmp_impl.h
   DEPENDS
 libc.include.setjmp
+  COMPILE_OPTIONS
+-O3
+-fno-omit-frame-pointer
 )
 
 add_entrypoint_object(
@@ -16,9 +16,10 @@
   SRCS
 longjmp.cpp
   HDRS
-longjmp.h
-  COMPILE_OPTIONS
--O3 # We do not want any local variables in longjmp
+../longjmp.h
   DEPENDS
 libc.include.setjmp
+  COMPILE_OPTIONS
+-O3
+-fno-omit-frame-pointer
 )
Index: libc/src/setjmp/riscv64/setjmp.cpp
===
--- /dev/null
+++ libc/src/setjmp/riscv64/setjmp.cpp
@@ -0,0 +1,56 @@
+//===-- Implementation of setjmp --===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===--===//
+
+#include "src/__support/common.h"
+#include "src/setjmp/setjmp_impl.h"
+
+#include 
+
+#if !defined(LIBC_TARGET_ARCH_IS_RISCV64)
+#error "Invalid file include"
+#endif
+
+namespace __llvm_libc {
+
+LLVM_LIBC_FUNCTION(int, setjmp, (__jmp_buf * buf)) {
+  LIBC_INLINE_ASM("sd ra, %0\n\t" : : "m"(buf->__pc) :);
+  LIBC_INLINE_ASM("sd s0, %0\n\t" : : "m"(buf->__regs[0]) :);
+  LIBC_INLINE_ASM("sd s1, %0\n\t" : : "m"(buf->__regs[1]) :);
+  LIBC_INLINE_ASM("sd s2, %0\n\t" : : "m"(buf->__regs[2]) :);
+  LIBC_INLINE_ASM("sd s3, %0\n\t" : : "m"(buf->__regs[3]) :);
+  LIBC_INLINE_ASM("sd s4, %0\n\t" : : "m"(buf->__regs[4]) :);
+  LIBC_INLINE_ASM("sd s5, %0\n\t" : : 

[PATCH] D145584: [libc] Add support for setjmp and longjmp in riscv

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added inline comments.



Comment at: libc/src/setjmp/riscv64/longjmp.cpp:54-55
+
+  LIBC_INLINE_ASM("seqz %0, %1" : "+r"(buf) : "r"(val) :);
+  LIBC_INLINE_ASM("add %0, %0, %1" : "+r"(buf) : "r"(val), "r"(buf) :);
+}

sivachandra wrote:
> Your comment is in the previous diff but thanks for the explanation. I think 
> we have missed the `val` check for zero in the x86_64 case and should be 
> fixed separately.
> 
> For the above two instructions, in the interest of reducing the amount of 
> logic in inline assembly, can we do:
> 
> ```
>   val = val == 0 ? 1 : val;
>   LIBC_INLINE_ASM("add a0, %0, zero\n\t" : : "r"(val) :);
> ```
> Your comment is in the previous diff but thanks for the explanation. I think 
> we have missed the `val` check for zero in the x86_64 case and should be 
> fixed separately.

no problem, do you want me to fix the x86_64 version?

> 
> For the above two instructions, in the interest of reducing the amount of 
> logic in inline assembly, can we do:
> 
> ```
>   val = val == 0 ? 1 : val;
>   LIBC_INLINE_ASM("add a0, %0, zero\n\t" : : "r"(val) :);
> ```

Done, I'll rerun the tests now.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D145584

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D145584: [libc] Add support for setjmp and longjmp in riscv

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added inline comments.



Comment at: libc/src/setjmp/riscv64/longjmp.h:56
+
+  LIBC_INLINE_ASM("seqz %0, %1" : "+r"(buf) : "r"(val) :);
+  LIBC_INLINE_ASM("add %0, %0, %1" : "+r"(buf) : "r"(val), "r"(buf) :);

sivachandra wrote:
> Why is this required? Can we just copy `val` to `a0` and return? Or, even 
> better would be just `return val;` if we can make this a `naked` function?
This is the fake return mentioned on the Linux man page:
```
Following  a  successful  longjmp(), execution continues as if setjmp()
had returned for a second time.  This  "fake"  return  can  be  distin-
guished from a true setjmp() call because the "fake" return returns the
value provided in val.  If the programmer mistakenly passes the value 0
in val, the "fake" return will instead return 1.
```

We can't return normally here, since `longjmp` has no return.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D145584

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D145584: [libc] Add support for setjmp and longjmp in riscv

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 507700.
mikhail.ramalho marked 6 inline comments as done.
mikhail.ramalho added a comment.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

Address comments


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D145584

Files:
  clang/docs/tools/clang-formatted-files.txt
  libc/config/linux/riscv64/entrypoints.txt
  libc/config/linux/riscv64/headers.txt
  libc/include/llvm-libc-types/jmp_buf.h
  libc/src/setjmp/CMakeLists.txt
  libc/src/setjmp/longjmp.cpp
  libc/src/setjmp/riscv64/CMakeLists.txt
  libc/src/setjmp/riscv64/longjmp.cpp
  libc/src/setjmp/riscv64/setjmp.cpp
  libc/src/setjmp/setjmp.cpp
  libc/src/setjmp/x86_64/CMakeLists.txt
  libc/src/setjmp/x86_64/longjmp.cpp
  libc/src/setjmp/x86_64/setjmp.cpp

Index: libc/src/setjmp/x86_64/setjmp.cpp
===
--- libc/src/setjmp/x86_64/setjmp.cpp
+++ libc/src/setjmp/x86_64/setjmp.cpp
@@ -7,15 +7,15 @@
 //===--===//
 
 #include "src/__support/common.h"
-#include "src/__support/macros/properties/architectures.h"
 #include "src/setjmp/setjmp_impl.h"
 
-#include 
+#if !defined(LIBC_TARGET_ARCH_IS_X86_64)
+#error "Invalid file include"
+#endif
 
 namespace __llvm_libc {
 
 LLVM_LIBC_FUNCTION(int, setjmp, (__jmp_buf * buf)) {
-#ifdef LIBC_TARGET_ARCH_IS_X86_64
   register __UINT64_TYPE__ rbx __asm__("rbx");
   register __UINT64_TYPE__ r12 __asm__("r12");
   register __UINT64_TYPE__ r13 __asm__("r13");
@@ -50,10 +50,6 @@
   buf->rsp = reinterpret_cast<__UINTPTR_TYPE__>(__builtin_frame_address(0)) +
  sizeof(__UINTPTR_TYPE__) * 2;
   buf->rip = reinterpret_cast<__UINTPTR_TYPE__>(__builtin_return_address(0));
-#else // LIBC_TARGET_ARCH_IS_X86_64
-#error "setjmp implementation not available for the target architecture."
-#endif
-
   return 0;
 }
 
Index: libc/src/setjmp/x86_64/longjmp.cpp
===
--- libc/src/setjmp/x86_64/longjmp.cpp
+++ libc/src/setjmp/x86_64/longjmp.cpp
@@ -8,14 +8,14 @@
 
 #include "src/setjmp/longjmp.h"
 #include "src/__support/common.h"
-#include "src/__support/macros/properties/architectures.h"
 
-#include 
+#if !defined(LIBC_TARGET_ARCH_IS_X86_64)
+#error "Invalid file include"
+#endif
 
 namespace __llvm_libc {
 
 LLVM_LIBC_FUNCTION(void, longjmp, (__jmp_buf * buf, int val)) {
-#ifdef LIBC_TARGET_ARCH_IS_X86_64
   register __UINT64_TYPE__ rbx __asm__("rbx");
   register __UINT64_TYPE__ rbp __asm__("rbp");
   register __UINT64_TYPE__ r12 __asm__("r12");
@@ -38,9 +38,6 @@
   LIBC_INLINE_ASM("mov %1, %0\n\t" : "=r"(r15) : "m"(buf->r15) :);
   LIBC_INLINE_ASM("mov %1, %0\n\t" : "=r"(rsp) : "m"(buf->rsp) :);
   LIBC_INLINE_ASM("jmp *%0\n\t" : : "m"(buf->rip));
-#else // LIBC_TARGET_ARCH_IS_X86_64
-#error "longjmp implementation not available for the target architecture."
-#endif
 }
 
 } // namespace __llvm_libc
Index: libc/src/setjmp/x86_64/CMakeLists.txt
===
--- libc/src/setjmp/x86_64/CMakeLists.txt
+++ libc/src/setjmp/x86_64/CMakeLists.txt
@@ -3,12 +3,12 @@
   SRCS
 setjmp.cpp
   HDRS
-setjmp_impl.h
-  COMPILE_OPTIONS
--O3 # We do not want any local variables in setjmp
--fno-omit-frame-pointer # The implementation assumes frame pointer on to the stack
+../setjmp_impl.h
   DEPENDS
 libc.include.setjmp
+  COMPILE_OPTIONS
+-O3
+-fno-omit-frame-pointer
 )
 
 add_entrypoint_object(
@@ -16,9 +16,10 @@
   SRCS
 longjmp.cpp
   HDRS
-longjmp.h
-  COMPILE_OPTIONS
--O3 # We do not want any local variables in longjmp
+../longjmp.h
   DEPENDS
 libc.include.setjmp
+  COMPILE_OPTIONS
+-O3
+-fno-omit-frame-pointer
 )
Index: libc/src/setjmp/riscv64/setjmp.cpp
===
--- /dev/null
+++ libc/src/setjmp/riscv64/setjmp.cpp
@@ -0,0 +1,56 @@
+//===-- Implementation of setjmp --===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===--===//
+
+#include "src/__support/common.h"
+#include "src/setjmp/setjmp_impl.h"
+
+#include 
+
+#if !defined(LIBC_TARGET_ARCH_IS_RISCV64)
+#error "Invalid file include"
+#endif
+
+namespace __llvm_libc {
+
+LLVM_LIBC_FUNCTION(int, setjmp, (__jmp_buf * buf)) {
+  LIBC_INLINE_ASM("sd ra, %0\n\t" : : "m"(buf->__pc) :);
+  LIBC_INLINE_ASM("sd s0, %0\n\t" : : "m"(buf->__regs[0]) :);
+  LIBC_INLINE_ASM("sd s1, %0\n\t" : : "m"(buf->__regs[1]) :);
+  LIBC_INLINE_ASM("sd s2, %0\n\t" : : "m"(buf->__regs[2]) :);
+  LIBC_INLINE_ASM("sd s3, %0\n\t" : : 

[PATCH] D140891: [analyzer] Fix assertion failure in SMT conversion for unary operator on floats.

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho accepted this revision.
mikhail.ramalho added a comment.
This revision is now accepted and ready to land.

LGTM.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D140891

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

Indeed it looks like a copy & paste error, I'm surprised no one found it 
earlier.

Regarding the tests, we used to have `make check-clang-analysis-z3` (or 
something similar) that would run only the analyzer's tests, but using Z3 as 
the constraint solver. It looks like this change broke it: 
https://reviews.llvm.org/D62445


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

https://reviews.llvm.org/D83660

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D96090: [analyzer] Replace StoreManager::CastRetrievedVal with SValBuilder::evalCast

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

I'm glad to see these patches, the SMT API will benefit greatly from them!


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

https://reviews.llvm.org/D96090

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D86223: [analyzer][z3] Use more elaborate Z3 variable names

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho accepted this revision.
mikhail.ramalho added a comment.
This revision is now accepted and ready to land.

LGTM!


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D86223

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D86223: [analyzer][z3] Use more elaborate z3 variable names in debug build

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho requested changes to this revision.
mikhail.ramalho added a comment.
This revision now requires changes to proceed.

In D86223#2231991 , @steakhal wrote:

> In D86223#2231959 , @mikhail.ramalho 
> wrote:
>
>> I don't mind having it for release builds as well, why are you applying it 
>> only for debug builds?
>
> It might introduce a slight overhead since Z3 will parse longer the symbol 
> names.

That overhead should be negligible, in the worst case you are adding just a few 
extra characters to the variable's name.

I rather have it for release builds as well so we don't introduce different 
outputs depending on the build options, and we can improve debugging for 
release builds as well.

Also as a bonus, we don't have to change the test scripts for a single test.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D86223

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D86223: [analyzer][z3] Use more elaborate z3 variable names in debug build

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

I don't mind having it for release builds as well, why are you applying it only 
for debug builds?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D86223

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D78457: [analyzer][Z3-refutation] Fix a refutation BugReporterVisitor bug

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

Nice work, @steakhal!

I remember discussing with @NoQ a way of going backward on the bug report, from 
the error node, and never add constraints of symbols that were already 
collected; that way we would always have the tighter constraints.

I don't quite remember if I ever implemented it that way though.


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

https://reviews.llvm.org/D78457



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D73062: [analyzer] Simplify BoolAssignmentChecker

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 239397.
mikhail.ramalho added a comment.

Update the condition to flag an issue.


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

https://reviews.llvm.org/D73062

Files:
  clang/lib/StaticAnalyzer/Checkers/BoolAssignmentChecker.cpp

Index: clang/lib/StaticAnalyzer/Checkers/BoolAssignmentChecker.cpp
===
--- clang/lib/StaticAnalyzer/Checkers/BoolAssignmentChecker.cpp
+++ clang/lib/StaticAnalyzer/Checkers/BoolAssignmentChecker.cpp
@@ -70,8 +70,8 @@
   // Get the value of the right-hand side.  We only care about values
   // that are defined (UnknownVals and UndefinedVals are handled by other
   // checkers).
-  Optional DV = val.getAs();
-  if (!DV)
+  Optional NV = val.getAs();
+  if (!NV)
 return;
 
   // Check if the assigned value meets our criteria for correctness.  It must
@@ -79,78 +79,17 @@
   // the value is possibly < 0 (for a negative value) or greater than 1.
   ProgramStateRef state = C.getState();
   SValBuilder  = C.getSValBuilder();
+  BasicValueFactory  = svalBuilder.getBasicValueFactory();
   ConstraintManager  = C.getConstraintManager();
 
-  // First, ensure that the value is >= 0.
-  DefinedSVal zeroVal = svalBuilder.makeIntVal(0, valTy);
-  SVal greaterThanOrEqualToZeroVal =
-svalBuilder.evalBinOp(state, BO_GE, *DV, zeroVal,
-  svalBuilder.getConditionType());
+  llvm::APSInt Zero = BVF.getValue(0, valTy);
+  llvm::APSInt One = BVF.getValue(1, valTy);
 
-  Optional greaterThanEqualToZero =
-  greaterThanOrEqualToZeroVal.getAs();
+  ProgramStateRef StIn, StOut;
+  std::tie(StIn, StOut) = CM.assumeInclusiveRangeDual(state, *NV, Zero, One);
 
-  if (!greaterThanEqualToZero) {
-// The SValBuilder cannot construct a valid SVal for this condition.
-// This means we cannot properly reason about it.
-return;
-  }
-
-  ProgramStateRef stateLT, stateGE;
-  std::tie(stateGE, stateLT) = CM.assumeDual(state, *greaterThanEqualToZero);
-
-  // Is it possible for the value to be less than zero?
-  if (stateLT) {
-// It is possible for the value to be less than zero.  We only
-// want to emit a warning, however, if that value is fully constrained.
-// If it it possible for the value to be >= 0, then essentially the
-// value is underconstrained and there is nothing left to be done.
-if (!stateGE)
-  emitReport(stateLT, C);
-
-// In either case, we are done.
-return;
-  }
-
-  // If we reach here, it must be the case that the value is constrained
-  // to only be >= 0.
-  assert(stateGE == state);
-
-  // At this point we know that the value is >= 0.
-  // Now check to ensure that the value is <= 1.
-  DefinedSVal OneVal = svalBuilder.makeIntVal(1, valTy);
-  SVal lessThanEqToOneVal =
-svalBuilder.evalBinOp(state, BO_LE, *DV, OneVal,
-  svalBuilder.getConditionType());
-
-  Optional lessThanEqToOne =
-  lessThanEqToOneVal.getAs();
-
-  if (!lessThanEqToOne) {
-// The SValBuilder cannot construct a valid SVal for this condition.
-// This means we cannot properly reason about it.
-return;
-  }
-
-  ProgramStateRef stateGT, stateLE;
-  std::tie(stateLE, stateGT) = CM.assumeDual(state, *lessThanEqToOne);
-
-  // Is it possible for the value to be greater than one?
-  if (stateGT) {
-// It is possible for the value to be greater than one.  We only
-// want to emit a warning, however, if that value is fully constrained.
-// If it is possible for the value to be <= 1, then essentially the
-// value is underconstrained and there is nothing left to be done.
-if (!stateLE)
-  emitReport(stateGT, C);
-
-// In either case, we are done.
-return;
-  }
-
-  // If we reach here, it must be the case that the value is constrained
-  // to only be <= 1.
-  assert(stateLE == state);
+  if (!StIn)
+emitReport(StOut, C);
 }
 
 void ento::registerBoolAssignmentChecker(CheckerManager ) {
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28955: [analyzer] Enable support for symbolic extension/truncation

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 239186.
mikhail.ramalho added a comment.
Herald added subscribers: llvm-commits, hiraditya.
Herald added a project: LLVM.

Two changes:

- Moved the BoolAssignmentChecker changes to separate revision (D73062 
).
- Rebased on top of master.

There are a few cases failing, some because clang is trying to match some 
strings printed by the ranged constraint manager and there is at least 1 
segfault.


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

https://reviews.llvm.org/D28955

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
  clang/lib/StaticAnalyzer/Core/ProgramState.cpp
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  clang/lib/StaticAnalyzer/Core/Store.cpp
  llvm/include/llvm/Support/SMTAPI.h
  llvm/lib/Support/Z3Solver.cpp

Index: llvm/lib/Support/Z3Solver.cpp
===
--- llvm/lib/Support/Z3Solver.cpp
+++ llvm/lib/Support/Z3Solver.cpp
@@ -872,6 +872,8 @@
 
   bool isFPSupported() override { return true; }
 
+  bool isExtTruncSupported() override { return true; }
+
   /// Reset the solver and remove all constraints.
   void reset() override { Z3_solver_reset(Context.Context, Solver); }
 
Index: llvm/include/llvm/Support/SMTAPI.h
===
--- llvm/include/llvm/Support/SMTAPI.h
+++ llvm/include/llvm/Support/SMTAPI.h
@@ -433,6 +433,9 @@
   /// Checks if the solver supports floating-points.
   virtual bool isFPSupported() = 0;
 
+  /// Checks if the solver supports extension/truncation.
+  virtual bool isExtTruncSupported() = 0;
+
   virtual void print(raw_ostream ) const = 0;
 };
 
Index: clang/lib/StaticAnalyzer/Core/Store.cpp
===
--- clang/lib/StaticAnalyzer/Core/Store.cpp
+++ clang/lib/StaticAnalyzer/Core/Store.cpp
@@ -532,7 +532,9 @@
 elementType, Offset, cast(ElemR->getSuperRegion()), Ctx));
   }
 
-  const llvm::APSInt& OffI = Offset.castAs().getValue();
+  // FIXME: This isn't quite correct, but avoids casting the Offset symbol
+  llvm::APSInt OffI = APSIntType(BaseIdxI).convert(
+  Offset.castAs().getValue());
   assert(BaseIdxI.isSigned());
 
   // Compute the new index.
Index: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
===
--- clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -72,6 +72,8 @@
 }
 
 SVal SimpleSValBuilder::evalCastFromNonLoc(NonLoc val, QualType castTy) {
+  ConstraintManager  = getStateManager().getConstraintManager();
+
   bool isLocType = Loc::isLocType(castTy);
   if (val.getAs())
 return val;
@@ -79,28 +81,37 @@
   if (Optional LI = val.getAs()) {
 if (isLocType)
   return LI->getLoc();
+
 // FIXME: Correctly support promotions/truncations.
-unsigned castSize = Context.getIntWidth(castTy);
-if (castSize == LI->getNumBits())
+unsigned castSize = Context.getTypeSize(castTy);
+if (!CM.canReasonAboutSymbolicExtTrunc() && castSize == LI->getNumBits())
   return val;
+
 return makeLocAsInteger(LI->getLoc(), castSize);
   }
 
   if (const SymExpr *se = val.getAsSymbolicExpression()) {
 QualType T = Context.getCanonicalType(se->getType());
-// If types are the same or both are integers, ignore the cast.
+// If types are the same, ignore the cast.
+if (haveSameType(T, castTy))
+  return val;
+
+// If types are both integers, ignore the cast.
 // FIXME: Remove this hack when we support symbolic truncation/extension.
 // HACK: If both castTy and T are integers, ignore the cast.  This is
 // not a permanent solution.  Eventually we want to precisely handle
 // extension/truncation of symbolic integers.  This prevents us from losing
 // precision when we assign 'x = y' and 'y' is symbolic and x and y are
 // different integer types.
-   if (haveSameType(T, castTy))
+if (!CM.canReasonAboutSymbolicExtTrunc() &&
+(T->isIntegralOrEnumerationType() &&
+castTy->isIntegralOrEnumerationType()))
   return val;
 
-if (!isLocType)
-  return makeNonLoc(se, T, castTy);
-return UnknownVal();
+if (isLocType)
+  return UnknownVal();
+
+return makeNonLoc(se, T, castTy);
   }
 
   // If value is a non-integer constant, produce unknown.
Index: clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ 

[PATCH] D73062: [analyzer] Simplify BoolAssignmentChecker

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho created this revision.
mikhail.ramalho added a reviewer: NoQ.
Herald added subscribers: cfe-commits, Charusso.
Herald added a project: clang.
mikhail.ramalho retitled this revision from "Simplify BoolAssignmentChecker" to 
"[analyzer] Simplify BoolAssignmentChecker".
Herald added subscribers: dkrupp, donat.nagy, Szelethus, a.sidorin, szepet, 
baloghadamsoftware, xazax.hun.

Instead of checking the range manually, changed the checker to use 
assumeInclusiveRangeDual instead.

This patch was part of D28955 .


Repository:
  rC Clang

https://reviews.llvm.org/D73062

Files:
  clang/lib/StaticAnalyzer/Checkers/BoolAssignmentChecker.cpp
  clang/test/Analysis/bool-assignment.c
  clang/test/Analysis/dead-stores.m
  clang/test/Analysis/misc-ps-eager-assume.m

Index: clang/test/Analysis/misc-ps-eager-assume.m
===
--- clang/test/Analysis/misc-ps-eager-assume.m
+++ clang/test/Analysis/misc-ps-eager-assume.m
@@ -1,5 +1,4 @@
 // RUN: %clang_analyze_cc1 -analyzer-checker=core,alpha.core -analyzer-store=region -verify -fblocks %s
-// expected-no-diagnostics
 
 // Delta-reduced header stuff (needed for test cases).
 typedef signed char BOOL;
@@ -56,7 +55,7 @@
 void handle_symbolic_cast_in_condition(void) {
   NSAutoreleasePool* pool = [[NSAutoreleasePool alloc] init];
 
-  BOOL needsAnArray = [@"aString" isEqualToString:@"anotherString"];
+  BOOL needsAnArray = [@"aString" isEqualToString:@"anotherString"]; // expected-warning {{Assignment of a non-Boolean value}}
   NSMutableArray* array = needsAnArray ? [[NSMutableArray alloc] init] : 0;
   if(needsAnArray)
 [array release];
Index: clang/test/Analysis/dead-stores.m
===
--- clang/test/Analysis/dead-stores.m
+++ clang/test/Analysis/dead-stores.m
@@ -54,7 +54,7 @@
 - (void) bar_rbar8527823
 {
  @synchronized(self) {
-   BOOL isExec = baz_rdar8527823(); // no-warning
+   BOOL isExec = baz_rdar8527823(); // expected-warning {{Assignment of a non-Boolean value}}
if (isExec) foo_rdar8527823();
  }
 }
Index: clang/test/Analysis/bool-assignment.c
===
--- clang/test/Analysis/bool-assignment.c
+++ clang/test/Analysis/bool-assignment.c
@@ -43,11 +43,7 @@
 return;
   }
   if (y > 200 && y < 250) {
-#ifdef ANALYZER_CM_Z3
 BOOL x = y; // expected-warning {{Assignment of a non-Boolean value}}
-#else
-BOOL x = y; // no-warning
-#endif
 return;
   }
   if (y >= 127 && y < 150) {
Index: clang/lib/StaticAnalyzer/Checkers/BoolAssignmentChecker.cpp
===
--- clang/lib/StaticAnalyzer/Checkers/BoolAssignmentChecker.cpp
+++ clang/lib/StaticAnalyzer/Checkers/BoolAssignmentChecker.cpp
@@ -70,8 +70,8 @@
   // Get the value of the right-hand side.  We only care about values
   // that are defined (UnknownVals and UndefinedVals are handled by other
   // checkers).
-  Optional DV = val.getAs();
-  if (!DV)
+  Optional NV = val.getAs();
+  if (!NV)
 return;
 
   // Check if the assigned value meets our criteria for correctness.  It must
@@ -79,78 +79,17 @@
   // the value is possibly < 0 (for a negative value) or greater than 1.
   ProgramStateRef state = C.getState();
   SValBuilder  = C.getSValBuilder();
+  BasicValueFactory  = svalBuilder.getBasicValueFactory();
   ConstraintManager  = C.getConstraintManager();
 
-  // First, ensure that the value is >= 0.
-  DefinedSVal zeroVal = svalBuilder.makeIntVal(0, valTy);
-  SVal greaterThanOrEqualToZeroVal =
-svalBuilder.evalBinOp(state, BO_GE, *DV, zeroVal,
-  svalBuilder.getConditionType());
+  llvm::APSInt Zero = BVF.getValue(0, valTy);
+  llvm::APSInt One = BVF.getValue(1, valTy);
 
-  Optional greaterThanEqualToZero =
-  greaterThanOrEqualToZeroVal.getAs();
+  ProgramStateRef StIn, StOut;
+  std::tie(StIn, StOut) = CM.assumeInclusiveRangeDual(state, *NV, Zero, One);
 
-  if (!greaterThanEqualToZero) {
-// The SValBuilder cannot construct a valid SVal for this condition.
-// This means we cannot properly reason about it.
-return;
-  }
-
-  ProgramStateRef stateLT, stateGE;
-  std::tie(stateGE, stateLT) = CM.assumeDual(state, *greaterThanEqualToZero);
-
-  // Is it possible for the value to be less than zero?
-  if (stateLT) {
-// It is possible for the value to be less than zero.  We only
-// want to emit a warning, however, if that value is fully constrained.
-// If it it possible for the value to be >= 0, then essentially the
-// value is underconstrained and there is nothing left to be done.
-if (!stateGE)
-  emitReport(stateLT, C);
-
-// In either case, we are done.
-return;
-  }
-
-  // If we reach here, it must be the case that the value is constrained
-  // to only be >= 0.
-  assert(stateGE == state);
-
-  // At this point we know that the 

[PATCH] D28955: [analyzer] Enable support for symbolic extension/truncation

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

I can give some help here, but my time is quite limited as well :/

Let me at least rebase against master.


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

https://reviews.llvm.org/D28955



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D62445: [test] Fix plugin tests

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.
Herald added a subscriber: Charusso.

Hi, I just found this revision.

Could you point out how can I run the CSA tests with Z3 as backend? We used to 
do `$ ninja check-clang-analyzer-z3`, however, it now fails and suggests:

   $ ninja check-clang-analyzer-z3
  ninja: error: unknown target 'check-clang-analyzer-z3', did you mean 
'check-clang-analysis-z3'?

`check-clang-analysis-z3` only runs one test though.


Repository:
  rL LLVM

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

https://reviews.llvm.org/D62445



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

In D54978#1447107 , @gou4shi1 wrote:

> My own out-of-tree pass `#include ` and use cmake's 
> `add_llvm_library` to compile it into a `.so`
>  However, `opt -load-pass-plugin=my-pass.so -passes="foo" bar.ll` fails:
>  `opt: symbol lookup error: Passes/libStackPasses.so: undefined symbol: 
> _ZN4llvm14CreateZ3SolverEv`
>  (c++filt: `llvm::CreateZ3Solver()`)
>  If I move the content of `Z3Solver.cpp` into another file of `llvm/Support` 
> (like `llvm/Support/raw_ostream.cpp`)
>  everything works.


I can't reproduce the error, can you send me a small example?


Repository:
  rL LLVM

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

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

In D54978#1442493 , @aprantl wrote:

> I'm afraid this broke some bots that build with `LLVM_ENABLE_MODULES=1`.
>
> For example:
>
> http://green.lab.llvm.org/green/view/LLDB/job/lldb-cmake/22411/consoleFull#710926295dd1929ea-7054-4089-b7ef-4624c3781fa4
>
>   Undefined symbols for architecture x86_64:
> "llvm::errs()", referenced from:
> llvm::SMTExpr::dump() const in 
> liblldbDebugserverCommon.a(RNBSocket.cpp.o)
> llvm::SMTSolver::dump() const in 
> liblldbDebugserverCommon.a(RNBSocket.cpp.o)
> llvm::SMTSort::dump() const in 
> liblldbDebugserverCommon.a(RNBSocket.cpp.o)
> llvm::SMTExpr::dump() const in 
> liblldbDebugserverCommon.a(SocketAddress.cpp.o)
> llvm::SMTSolver::dump() const in 
> liblldbDebugserverCommon.a(SocketAddress.cpp.o)
> llvm::SMTSort::dump() const in 
> liblldbDebugserverCommon.a(SocketAddress.cpp.o)
>
>
> Long story short: You can't have an LLVM_DUMP_METHOD defined inline inside of 
> a module.
>
> One way to fix this would be to move the function body of the various
>
>   LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
>
>
> functions into .cpp files.


Unfortunately, I was not able to reproduce the bug locally (when I enable 
modules, clang complains about some `std::shared_ptr`), 
however, I just pushed r356994 and I'll keep an eye on the bot.

Thanks for the report.


Repository:
  rL LLVM

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

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

In D54978#1441453 , @gou4shi1 wrote:

> > ! In D54978#1441417 , 
> > @mikhail.ramalho wrote:
> >  Sure, I'll create a new revision with the added functions tonight.
>
> I am very happy with your quickly reply.
>  btw, `Z3_get_bv_sort_size` is also needed :)
>  Thanks for your nice job!


You can get the sort size by calling getBitvectorSortSize().


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

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

> ! In D54978#1440464 , @ddcc wrote:
> 
> Do you know if this configuration builds fine now?

It's working fine now, I'll push it later today.

> ! In D54978#1441355 , @gou4shi1 
> wrote:
> 
> Can you plz add some wrappers of overflow predicates  like 
> Z3_mk_bvadd_no_overflow, Z3_mk_bvadd_no_underflow, ... to SMTAPI.h and 
> Z3Solver.cpp?
>  It could help me, thanks!

Sure, I'll create a new revision with the added functions tonight.


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

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho marked an inline comment as done.
mikhail.ramalho added a comment.

Fixed.


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

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 191305.
mikhail.ramalho added a comment.

Fix copy-and-paste error.


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

https://reviews.llvm.org/D54978

Files:
  clang/CMakeLists.txt
  clang/cmake/modules/FindZ3.cmake
  clang/include/clang/Config/config.h.cmake
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
  clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  clang/lib/StaticAnalyzer/Core/CMakeLists.txt
  clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  clang/test/CMakeLists.txt
  clang/test/lit.site.cfg.py.in
  llvm/CMakeLists.txt
  llvm/cmake/modules/FindZ3.cmake
  llvm/cmake/modules/LLVMConfig.cmake.in
  llvm/include/llvm/Config/config.h.cmake
  llvm/include/llvm/Support/SMTAPI.h
  llvm/lib/Support/CMakeLists.txt
  llvm/lib/Support/Z3Solver.cpp

Index: llvm/lib/Support/Z3Solver.cpp
===
--- llvm/lib/Support/Z3Solver.cpp
+++ llvm/lib/Support/Z3Solver.cpp
@@ -1,4 +1,4 @@
-//== Z3ConstraintManager.cpp *- C++ -*--==//
+//== Z3Solver.cpp ---*- C++ -*--==//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
@@ -6,18 +6,14 @@
 //
 //===--===//
 
-#include "clang/Basic/TargetInfo.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
+#include "llvm/ADT/Twine.h"
+#include "llvm/Config/config.h"
+#include "llvm/Support/SMTAPI.h"
+#include 
 
-#include "clang/Config/config.h"
+using namespace llvm;
 
-using namespace clang;
-using namespace ento;
-
-#if CLANG_ANALYZER_WITH_Z3
+#if LLVM_WITH_Z3
 
 #include 
 
@@ -818,18 +814,13 @@
 
 #endif
 
-SMTSolverRef clang::ento::CreateZ3Solver() {
-#if CLANG_ANALYZER_WITH_Z3
+llvm::SMTSolverRef llvm::CreateZ3Solver() {
+#if LLVM_WITH_Z3
   return llvm::make_unique();
 #else
   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
-   "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
+   "with -DLLVM_ENABLE_Z3_SOLVER=ON",
false);
   return nullptr;
 #endif
 }
-
-std::unique_ptr
-ento::CreateZ3ConstraintManager(ProgramStateManager , SubEngine *Eng) {
-  return llvm::make_unique(Eng, StMgr.getSValBuilder());
-}
Index: llvm/lib/Support/CMakeLists.txt
===
--- llvm/lib/Support/CMakeLists.txt
+++ llvm/lib/Support/CMakeLists.txt
@@ -44,6 +44,13 @@
   set (delayload_flags delayimp -delayload:shell32.dll -delayload:ole32.dll)
 endif()
 
+# Link Z3 if the user wants to build it.
+if(LLVM_WITH_Z3)
+  set(Z3_LINK_FILES ${Z3_LIBRARIES})
+else()
+  set(Z3_LINK_FILES "")
+endif()
+
 add_llvm_library(LLVMSupport
   AArch64TargetParser.cpp
   ARMTargetParser.cpp
@@ -152,6 +159,7 @@
   regfree.c
   regstrlcpy.c
   xxhash.cpp
+  Z3Solver.cpp
 
 # System
   Atomic.cpp
@@ -177,7 +185,14 @@
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/ADT
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/Support
   ${Backtrace_INCLUDE_DIRS}
-  LINK_LIBS ${system_libs} ${delayload_flags}
+  LINK_LIBS ${system_libs} ${delayload_flags} ${Z3_LINK_FILES}
   )
 
 set_property(TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS "${system_libs}")
+
+if(LLVM_WITH_Z3)
+  target_include_directories(LLVMSupport SYSTEM
+PRIVATE
+${Z3_INCLUDE_DIR}
+)
+endif()
Index: llvm/include/llvm/Support/SMTAPI.h
===
--- llvm/include/llvm/Support/SMTAPI.h
+++ llvm/include/llvm/Support/SMTAPI.h
@@ -11,15 +11,16 @@
 //
 //===--===//
 
-#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
-#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
+#ifndef LLVM_SUPPORT_SMTAPI_H
+#define LLVM_SUPPORT_SMTAPI_H
 
-#include "clang/Basic/TargetInfo.h"
+#include "llvm/ADT/APFloat.h"
 #include "llvm/ADT/APSInt.h"
 #include "llvm/ADT/FoldingSet.h"
+#include "llvm/Support/raw_ostream.h"
+#include 
 
-namespace clang {
-namespace ento {
+namespace llvm {
 
 /// Generic base class for SMT sorts
 class SMTSort {
@@ -399,7 +400,6 @@
 /// Convenience method to create and Z3Solver object
 SMTSolverRef CreateZ3Solver();
 
-} // namespace ento
-} // namespace clang
+} // namespace llvm
 
 #endif
Index: llvm/include/llvm/Config/config.h.cmake

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

Hi all,

I just updated the CMake script to get the version by parsing the header, 
however, I just found a potential issue in the previous approach: if we have 
incompatible libs in the path (32-bits libs when compiling in 64-bit mode) the 
CMake config will succeed but the compilation will fail.

To fix that, I changed the script slightly: we first try to dinamically get the 
Z3's version, if we fail and we are cross compiling, then we try to parse the 
headers. Right now, it should just work but I'd like to add a message to warn 
the user that we found the lib but we don't know if it'll link.

Let me know your thoughts.


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

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 191152.
mikhail.ramalho added a comment.

Updated script to parse Z3's headers and changed the workflow to handle cross 
compilation cases.


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

https://reviews.llvm.org/D54978

Files:
  clang/CMakeLists.txt
  clang/cmake/modules/FindZ3.cmake
  clang/include/clang/Config/config.h.cmake
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
  clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  clang/lib/StaticAnalyzer/Core/CMakeLists.txt
  clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  clang/test/CMakeLists.txt
  clang/test/lit.site.cfg.py.in
  llvm/CMakeLists.txt
  llvm/cmake/modules/FindZ3.cmake
  llvm/cmake/modules/LLVMConfig.cmake.in
  llvm/include/llvm/Config/config.h.cmake
  llvm/include/llvm/Support/SMTAPI.h
  llvm/lib/Support/CMakeLists.txt
  llvm/lib/Support/Z3Solver.cpp

Index: llvm/lib/Support/Z3Solver.cpp
===
--- llvm/lib/Support/Z3Solver.cpp
+++ llvm/lib/Support/Z3Solver.cpp
@@ -1,4 +1,4 @@
-//== Z3ConstraintManager.cpp *- C++ -*--==//
+//== Z3Solver.cpp ---*- C++ -*--==//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
@@ -6,18 +6,14 @@
 //
 //===--===//
 
-#include "clang/Basic/TargetInfo.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
+#include "llvm/ADT/Twine.h"
+#include "llvm/Config/config.h"
+#include "llvm/Support/SMTAPI.h"
+#include 
 
-#include "clang/Config/config.h"
+using namespace llvm;
 
-using namespace clang;
-using namespace ento;
-
-#if CLANG_ANALYZER_WITH_Z3
+#if LLVM_WITH_Z3
 
 #include 
 
@@ -818,18 +814,13 @@
 
 #endif
 
-SMTSolverRef clang::ento::CreateZ3Solver() {
-#if CLANG_ANALYZER_WITH_Z3
+llvm::SMTSolverRef llvm::CreateZ3Solver() {
+#if LLVM_WITH_Z3
   return llvm::make_unique();
 #else
   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
-   "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
+   "with -DLLVM_ENABLE_Z3_SOLVER=ON",
false);
   return nullptr;
 #endif
 }
-
-std::unique_ptr
-ento::CreateZ3ConstraintManager(ProgramStateManager , SubEngine *Eng) {
-  return llvm::make_unique(Eng, StMgr.getSValBuilder());
-}
Index: llvm/lib/Support/CMakeLists.txt
===
--- llvm/lib/Support/CMakeLists.txt
+++ llvm/lib/Support/CMakeLists.txt
@@ -44,6 +44,13 @@
   set (delayload_flags delayimp -delayload:shell32.dll -delayload:ole32.dll)
 endif()
 
+# Link Z3 if the user wants to build it.
+if(LLVM_WITH_Z3)
+  set(Z3_LINK_FILES ${Z3_LIBRARIES})
+else()
+  set(Z3_LINK_FILES "")
+endif()
+
 add_llvm_library(LLVMSupport
   AArch64TargetParser.cpp
   ARMTargetParser.cpp
@@ -152,6 +159,7 @@
   regfree.c
   regstrlcpy.c
   xxhash.cpp
+  Z3Solver.cpp
 
 # System
   Atomic.cpp
@@ -177,7 +185,14 @@
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/ADT
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/Support
   ${Backtrace_INCLUDE_DIRS}
-  LINK_LIBS ${system_libs} ${delayload_flags}
+  LINK_LIBS ${system_libs} ${delayload_flags} ${Z3_LINK_FILES}
   )
 
 set_property(TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS "${system_libs}")
+
+if(LLVM_WITH_Z3)
+  target_include_directories(LLVMSupport SYSTEM
+PRIVATE
+${Z3_INCLUDE_DIR}
+)
+endif()
Index: llvm/include/llvm/Support/SMTAPI.h
===
--- llvm/include/llvm/Support/SMTAPI.h
+++ llvm/include/llvm/Support/SMTAPI.h
@@ -11,15 +11,16 @@
 //
 //===--===//
 
-#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
-#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
+#ifndef LLVM_SUPPORT_SMTAPI_H
+#define LLVM_SUPPORT_SMTAPI_H
 
-#include "clang/Basic/TargetInfo.h"
+#include "llvm/ADT/APFloat.h"
 #include "llvm/ADT/APSInt.h"
 #include "llvm/ADT/FoldingSet.h"
+#include "llvm/Support/raw_ostream.h"
+#include 
 
-namespace clang {
-namespace ento {
+namespace llvm {
 
 /// Generic base class for SMT sorts
 class SMTSort {
@@ -399,7 +400,6 @@
 /// Convenience method to create and Z3Solver object
 SMTSolverRef CreateZ3Solver();
 
-} // namespace ento
-} // namespace clang
+} // namespace llvm
 
 #endif
Index: 

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 191095.
mikhail.ramalho added a comment.

Fixes:

- `FindZ3.cmake` format .
- Wrong `SMTExpr` namespace in `SMTConstraintManager.h`.


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

https://reviews.llvm.org/D54978

Files:
  clang/CMakeLists.txt
  clang/cmake/modules/FindZ3.cmake
  clang/include/clang/Config/config.h.cmake
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
  clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  clang/lib/StaticAnalyzer/Core/CMakeLists.txt
  clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  clang/test/CMakeLists.txt
  clang/test/lit.site.cfg.py.in
  llvm/CMakeLists.txt
  llvm/cmake/modules/FindZ3.cmake
  llvm/cmake/modules/LLVMConfig.cmake.in
  llvm/include/llvm/Config/config.h.cmake
  llvm/include/llvm/Support/SMTAPI.h
  llvm/lib/Support/CMakeLists.txt
  llvm/lib/Support/Z3Solver.cpp

Index: llvm/lib/Support/Z3Solver.cpp
===
--- llvm/lib/Support/Z3Solver.cpp
+++ llvm/lib/Support/Z3Solver.cpp
@@ -1,4 +1,4 @@
-//== Z3ConstraintManager.cpp *- C++ -*--==//
+//== Z3Solver.cpp ---*- C++ -*--==//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
@@ -6,18 +6,14 @@
 //
 //===--===//
 
-#include "clang/Basic/TargetInfo.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
+#include "llvm/ADT/Twine.h"
+#include "llvm/Config/config.h"
+#include "llvm/Support/SMTAPI.h"
+#include 
 
-#include "clang/Config/config.h"
+using namespace llvm;
 
-using namespace clang;
-using namespace ento;
-
-#if CLANG_ANALYZER_WITH_Z3
+#if LLVM_WITH_Z3
 
 #include 
 
@@ -818,18 +814,13 @@
 
 #endif
 
-SMTSolverRef clang::ento::CreateZ3Solver() {
-#if CLANG_ANALYZER_WITH_Z3
+llvm::SMTSolverRef llvm::CreateZ3Solver() {
+#if LLVM_WITH_Z3
   return llvm::make_unique();
 #else
   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
-   "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
+   "with -DLLVM_ENABLE_Z3_SOLVER=ON",
false);
   return nullptr;
 #endif
 }
-
-std::unique_ptr
-ento::CreateZ3ConstraintManager(ProgramStateManager , SubEngine *Eng) {
-  return llvm::make_unique(Eng, StMgr.getSValBuilder());
-}
Index: llvm/lib/Support/CMakeLists.txt
===
--- llvm/lib/Support/CMakeLists.txt
+++ llvm/lib/Support/CMakeLists.txt
@@ -44,6 +44,13 @@
   set (delayload_flags delayimp -delayload:shell32.dll -delayload:ole32.dll)
 endif()
 
+# Link Z3 if the user wants to build it.
+if(LLVM_WITH_Z3)
+  set(Z3_LINK_FILES ${Z3_LIBRARIES})
+else()
+  set(Z3_LINK_FILES "")
+endif()
+
 add_llvm_library(LLVMSupport
   AArch64TargetParser.cpp
   ARMTargetParser.cpp
@@ -152,6 +159,7 @@
   regfree.c
   regstrlcpy.c
   xxhash.cpp
+  Z3Solver.cpp
 
 # System
   Atomic.cpp
@@ -177,7 +185,14 @@
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/ADT
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/Support
   ${Backtrace_INCLUDE_DIRS}
-  LINK_LIBS ${system_libs} ${delayload_flags}
+  LINK_LIBS ${system_libs} ${delayload_flags} ${Z3_LINK_FILES}
   )
 
 set_property(TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS "${system_libs}")
+
+if(LLVM_WITH_Z3)
+  target_include_directories(LLVMSupport SYSTEM
+PRIVATE
+${Z3_INCLUDE_DIR}
+)
+endif()
Index: llvm/include/llvm/Support/SMTAPI.h
===
--- llvm/include/llvm/Support/SMTAPI.h
+++ llvm/include/llvm/Support/SMTAPI.h
@@ -11,15 +11,16 @@
 //
 //===--===//
 
-#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
-#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
+#ifndef LLVM_SUPPORT_SMTAPI_H
+#define LLVM_SUPPORT_SMTAPI_H
 
-#include "clang/Basic/TargetInfo.h"
+#include "llvm/ADT/APFloat.h"
 #include "llvm/ADT/APSInt.h"
 #include "llvm/ADT/FoldingSet.h"
+#include "llvm/Support/raw_ostream.h"
+#include 
 
-namespace clang {
-namespace ento {
+namespace llvm {
 
 /// Generic base class for SMT sorts
 class SMTSort {
@@ -399,7 +400,6 @@
 /// Convenience method to create and Z3Solver object
 SMTSolverRef CreateZ3Solver();
 
-} // namespace ento
-} // namespace clang
+} // namespace llvm
 
 #endif
Index: 

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

In D54978#1431788 , @ddcc wrote:

> The only relevant commit that I can find is 
> https://github.com/Z3Prover/z3/commit/2cb4223979cc94e2ebc4e49a9e83adbdcd2b6979
>  , but it first landed in z3 4.6.0. It looks like it's specific to CMake 
> though, so is it different if you use the python build? I haven't tried the 
> CMake build.


Indeed, it seems to be cmake specific (even the commit message says that the 
python scripts were not changed).


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

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

In D54978#1431786 , @ddcc wrote:

> In D54978#1431430 , @mikhail.ramalho 
> wrote:
>
> > Sorry for the massive delay, but I just updated the `FindZ3` script to 
> > retrieve the version from the lib. I changed it to use `try_run` instead of 
> > `try_compile` so we can get the version number.
> >
> > I tried to use @brzycki code to get the version from the header, however, 
> > it's not working for Z3 4.8.4. In Z3 4.8.3 the FULL_VERSION is a nice `"Z3 
> > 4.8.3.0"` but in version 4.8.4 it's `"Z3 4.8.4.10272 d6df51951f4c master 
> > z3-4.8.4"` and cmake fails with the following message:
>
>
> Thanks for making the changes! Is this being parsed from e.g. 
> `/usr/include/z3_version.h`? I checked their code, and I have a local build 
> of z3 4.8.5.0, but I'm not seeing those changes to the version string:
>
>   #define Z3_FULL_VERSION"Z3 4.8.5.0"
>


Nope, I downloaded it from release page on github: 
https://github.com/Z3Prover/z3/releases


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

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

Hi all,

Sorry for the massive delay, but I just updated the `FindZ3` script to retrieve 
the version from the lib. I changed it to use `try_run` instead of 
`try_compile` so we can get the version number.

I tried to use @brzycki code to get the version from the header, however, it's 
not working for Z3 4.8.4. In Z3 4.8.3 the FULL_VERSION is a nice `"Z3 4.8.3.0"` 
but in version 4.8.4 it's `"Z3 4.8.4.10272 d6df51951f4c master z3-4.8.4"` and 
cmake fails with the following message:

  -- Could NOT find Z3: Found unsuitable version "#define Z3_FULL_VERSION
"Z3 4.8.4.10272 d6df51951f4c master z3-4.8.4"", but required is at least 
"4.7.1" (found /home/mgadelha/z3/bin/libz3.so)

I believe we have a few options here:

1. Update the regex to handle the new format for `Z3_FULL_VERSION`.
2. Instead of parsing `Z3_FULL_VERSION`, we can parse `Z3_MAJOR_VERSION`, 
`Z3_MINOR_VERSION` and `Z3_BUILD_NUMBER` which are also available in the same 
header.

But, we'll still face the same problem of them changing the string format and 
breaking the scripts.


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

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 190893.
mikhail.ramalho added a comment.

Update Z3 script to use cmake's `try_run` in order to retrieve the version from 
the lib.


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

https://reviews.llvm.org/D54978

Files:
  clang/CMakeLists.txt
  clang/cmake/modules/FindZ3.cmake
  clang/include/clang/Config/config.h.cmake
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
  clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  clang/lib/StaticAnalyzer/Core/CMakeLists.txt
  clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  clang/test/CMakeLists.txt
  clang/test/lit.site.cfg.py.in
  llvm/CMakeLists.txt
  llvm/cmake/modules/FindZ3.cmake
  llvm/cmake/modules/LLVMConfig.cmake.in
  llvm/include/llvm/Config/config.h.cmake
  llvm/include/llvm/Support/SMTAPI.h
  llvm/lib/Support/CMakeLists.txt
  llvm/lib/Support/Z3Solver.cpp

Index: llvm/lib/Support/Z3Solver.cpp
===
--- llvm/lib/Support/Z3Solver.cpp
+++ llvm/lib/Support/Z3Solver.cpp
@@ -1,4 +1,4 @@
-//== Z3ConstraintManager.cpp *- C++ -*--==//
+//== Z3Solver.cpp ---*- C++ -*--==//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
@@ -6,18 +6,14 @@
 //
 //===--===//
 
-#include "clang/Basic/TargetInfo.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
+#include "llvm/ADT/Twine.h"
+#include "llvm/Config/config.h"
+#include "llvm/Support/SMTAPI.h"
+#include 
 
-#include "clang/Config/config.h"
+using namespace llvm;
 
-using namespace clang;
-using namespace ento;
-
-#if CLANG_ANALYZER_WITH_Z3
+#if LLVM_WITH_Z3
 
 #include 
 
@@ -818,18 +814,13 @@
 
 #endif
 
-SMTSolverRef clang::ento::CreateZ3Solver() {
-#if CLANG_ANALYZER_WITH_Z3
+llvm::SMTSolverRef llvm::CreateZ3Solver() {
+#if LLVM_WITH_Z3
   return llvm::make_unique();
 #else
   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
-   "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
+   "with -DLLVM_ENABLE_Z3_SOLVER=ON",
false);
   return nullptr;
 #endif
 }
-
-std::unique_ptr
-ento::CreateZ3ConstraintManager(ProgramStateManager , SubEngine *Eng) {
-  return llvm::make_unique(Eng, StMgr.getSValBuilder());
-}
Index: llvm/lib/Support/CMakeLists.txt
===
--- llvm/lib/Support/CMakeLists.txt
+++ llvm/lib/Support/CMakeLists.txt
@@ -44,6 +44,13 @@
   set (delayload_flags delayimp -delayload:shell32.dll -delayload:ole32.dll)
 endif()
 
+# Link Z3 if the user wants to build it.
+if(LLVM_WITH_Z3)
+  set(Z3_LINK_FILES ${Z3_LIBRARIES})
+else()
+  set(Z3_LINK_FILES "")
+endif()
+
 add_llvm_library(LLVMSupport
   AArch64TargetParser.cpp
   ARMTargetParser.cpp
@@ -152,6 +159,7 @@
   regfree.c
   regstrlcpy.c
   xxhash.cpp
+  Z3Solver.cpp
 
 # System
   Atomic.cpp
@@ -177,7 +185,14 @@
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/ADT
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/Support
   ${Backtrace_INCLUDE_DIRS}
-  LINK_LIBS ${system_libs} ${delayload_flags}
+  LINK_LIBS ${system_libs} ${delayload_flags} ${Z3_LINK_FILES}
   )
 
 set_property(TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS "${system_libs}")
+
+if(LLVM_WITH_Z3)
+  target_include_directories(LLVMSupport SYSTEM
+PRIVATE
+${Z3_INCLUDE_DIR}
+)
+endif()
Index: llvm/include/llvm/Support/SMTAPI.h
===
--- llvm/include/llvm/Support/SMTAPI.h
+++ llvm/include/llvm/Support/SMTAPI.h
@@ -11,15 +11,16 @@
 //
 //===--===//
 
-#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
-#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
+#ifndef LLVM_SUPPORT_SMTAPI_H
+#define LLVM_SUPPORT_SMTAPI_H
 
-#include "clang/Basic/TargetInfo.h"
+#include "llvm/ADT/APFloat.h"
 #include "llvm/ADT/APSInt.h"
 #include "llvm/ADT/FoldingSet.h"
+#include "llvm/Support/raw_ostream.h"
+#include 
 
-namespace clang {
-namespace ento {
+namespace llvm {
 
 /// Generic base class for SMT sorts
 class SMTSort {
@@ -399,7 +400,6 @@
 /// Convenience method to create and Z3Solver object
 SMTSolverRef CreateZ3Solver();
 
-} // namespace ento
-} // namespace clang
+} // namespace llvm
 
 #endif
Index: 

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

Hi guys,

I just sent the first prototype of the solution. All the magic happens inside 
the `CHECK_CXX_SOURCE_RUNS` call.

There is still one thing to do: currently, the program is hard-coded to check 
for version 4.7.1. We should either get it from the `find_package` call or 
remove the minimum version from the `find_package` call and rely only on the 
program. I'm not a big fan of the latter.


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

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 186757.
mikhail.ramalho added a comment.

Update FindZ3.cmake to do a runtime check of the version.


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

https://reviews.llvm.org/D54978

Files:
  clang/CMakeLists.txt
  clang/cmake/modules/FindZ3.cmake
  clang/include/clang/Config/config.h.cmake
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
  clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  clang/lib/StaticAnalyzer/Core/CMakeLists.txt
  clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  clang/test/CMakeLists.txt
  clang/test/lit.site.cfg.py.in
  llvm/CMakeLists.txt
  llvm/cmake/modules/FindZ3.cmake
  llvm/cmake/modules/LLVMConfig.cmake.in
  llvm/include/llvm/Config/config.h.cmake
  llvm/include/llvm/Support/SMTAPI.h
  llvm/lib/Support/CMakeLists.txt
  llvm/lib/Support/Z3Solver.cpp

Index: llvm/lib/Support/Z3Solver.cpp
===
--- llvm/lib/Support/Z3Solver.cpp
+++ llvm/lib/Support/Z3Solver.cpp
@@ -1,4 +1,4 @@
-//== Z3ConstraintManager.cpp *- C++ -*--==//
+//== Z3Solver.cpp ---*- C++ -*--==//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
@@ -6,18 +6,14 @@
 //
 //===--===//
 
-#include "clang/Basic/TargetInfo.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
+#include "llvm/ADT/Twine.h"
+#include "llvm/Config/config.h"
+#include "llvm/Support/SMTAPI.h"
+#include 
 
-#include "clang/Config/config.h"
+using namespace llvm;
 
-using namespace clang;
-using namespace ento;
-
-#if CLANG_ANALYZER_WITH_Z3
+#if LLVM_WITH_Z3
 
 #include 
 
@@ -818,18 +814,13 @@
 
 #endif
 
-SMTSolverRef clang::ento::CreateZ3Solver() {
-#if CLANG_ANALYZER_WITH_Z3
+llvm::SMTSolverRef llvm::CreateZ3Solver() {
+#if LLVM_WITH_Z3
   return llvm::make_unique();
 #else
   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
-   "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
+   "with -DLLVM_ENABLE_Z3_SOLVER=ON",
false);
   return nullptr;
 #endif
 }
-
-std::unique_ptr
-ento::CreateZ3ConstraintManager(ProgramStateManager , SubEngine *Eng) {
-  return llvm::make_unique(Eng, StMgr.getSValBuilder());
-}
Index: llvm/lib/Support/CMakeLists.txt
===
--- llvm/lib/Support/CMakeLists.txt
+++ llvm/lib/Support/CMakeLists.txt
@@ -44,6 +44,13 @@
   set (delayload_flags delayimp -delayload:shell32.dll -delayload:ole32.dll)
 endif()
 
+# Link Z3 if the user wants to build it.
+if(LLVM_WITH_Z3)
+  set(Z3_LINK_FILES ${Z3_LIBRARIES})
+else()
+  set(Z3_LINK_FILES "")
+endif()
+
 add_llvm_library(LLVMSupport
   AArch64TargetParser.cpp
   ARMTargetParser.cpp
@@ -151,6 +158,7 @@
   regfree.c
   regstrlcpy.c
   xxhash.cpp
+  Z3Solver.cpp
 
 # System
   Atomic.cpp
@@ -176,7 +184,14 @@
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/ADT
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/Support
   ${Backtrace_INCLUDE_DIRS}
-  LINK_LIBS ${system_libs} ${delayload_flags}
+  LINK_LIBS ${system_libs} ${delayload_flags} ${Z3_LINK_FILES}
   )
 
 set_property(TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS "${system_libs}")
+
+if(LLVM_WITH_Z3)
+  target_include_directories(LLVMSupport SYSTEM
+PRIVATE
+${Z3_INCLUDE_DIR}
+)
+endif()
Index: llvm/include/llvm/Support/SMTAPI.h
===
--- llvm/include/llvm/Support/SMTAPI.h
+++ llvm/include/llvm/Support/SMTAPI.h
@@ -11,15 +11,16 @@
 //
 //===--===//
 
-#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
-#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
+#ifndef LLVM_SUPPORT_SMTAPI_H
+#define LLVM_SUPPORT_SMTAPI_H
 
-#include "clang/Basic/TargetInfo.h"
+#include "llvm/ADT/APFloat.h"
 #include "llvm/ADT/APSInt.h"
 #include "llvm/ADT/FoldingSet.h"
+#include "llvm/Support/raw_ostream.h"
+#include 
 
-namespace clang {
-namespace ento {
+namespace llvm {
 
 /// Generic base class for SMT sorts
 class SMTSort {
@@ -399,7 +400,6 @@
 /// Convenience method to create and Z3Solver object
 SMTSolverRef CreateZ3Solver();
 
-} // namespace ento
-} // namespace clang
+} // namespace llvm
 
 #endif
Index: llvm/include/llvm/Config/config.h.cmake

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

In D54978#1395561 , @brzycki wrote:

> In D54978#1395476 , @mikhail.ramalho 
> wrote:
>
> > I'm wondering if we can remove the binary requirement all together: is it 
> > possible to run a small program that would return EXIT_SUCCESS if the 
> > library is the correct version?
>
>
> Hi @mikhail.ramalho, I don't think this is feasible unfortunately. If we're 
> using a cross-compiler the emitted binary won't be native to the platform. In 
> other words, you cannot test for Z3 as a run-time property.


Hi @brzycki, but isn't it exactly what we want? I mean, if we try to 
cross-compile and it fails for any reason (non-native library, wrong version), 
then Z3_FOUND shouldn't be set.

I just finished a small patch that checks the version as a run-time property. 
Please, let me know your thoughts.

If you agree with this approach I'll create a separate revision for it (it 
seems to work on ubuntu and fedora for me).


Repository:
  rC Clang

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

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

Looks like my last email got lost:

I'm wondering if we can remove the binary requirement all together: is it 
possible to run a small program that would return EXIT_SUCCESS if the library 
is the correct version?

Something like:

  #include 
  
  int main()
  {
unsigned int major, minor, build, revision;
Z3_get_version(, , , );

if(major >= 4 && minor >= 7 && build >= 1)
  return EXIT_SUCCESS;
  
return EXIT_FAILURE;
  }

This would be part of FindZ3.cmake and would set Z3_FOUND.

Do you guys think it's possible? I'm almost certain it can be done with 
autotools, but I'm clueless when it comes to cmake.


Repository:
  rC Clang

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

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

I found a `CHECK_CXX_SOURCE_COMPILES`, which seems to be used in a number of 
places in LLVM. I'll give it a try.


Repository:
  rC Clang

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

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

@brzycki, I can't reproduce your error. Maybe you're missing 
`-DLLVM_ENABLE_Z3_SOLVER=OFF`?

  $ cmake -GNinja ../llvm -DLLVM_ENABLE_PROJECTS=clang -DBUILD_SHARED_LIBS=ON 
-DCMAKE_INSTALL_PREFIX=/home/mgadelha/myclang -DCMAKE_LINKER=/usr/bin/ld.gold 
-DLLVM_ENABLE_BACKTRACES=OFF -DLLVM_TARGETS_TO_BUILD=host 
-DLLVM_ENABLE_Z3_SOLVER=ON -DCMAKE_BUILD_TYPE=RelWithDebInfo
  -- clang project is enabled
  -- compiler-rt project is disabled
  -- debuginfo-tests project is disabled
  -- libclc project is disabled
  -- libcxx project is disabled
  -- libcxxabi project is disabled
  -- libunwind project is disabled
  -- lld project is disabled
  -- lldb project is disabled
  -- llgo project is disabled
  -- llvm project is disabled
  -- openmp project is disabled
  -- parallel-libs project is disabled
  -- polly project is disabled
  -- pstl project is disabled
  -- Could NOT find Z3: Found unsuitable version "4.4.1", but required is at 
least "4.7.1" (found /usr/lib/x86_64-linux-gnu/libz3.so)
  CMake Error at CMakeLists.txt:406 (message):
LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.
  
  
  -- Configuring incomplete, errors occurred!
  See also "/home/mgadelha/llvm/build/CMakeFiles/CMakeOutput.log".


Repository:
  rC Clang

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

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho reopened this revision.
mikhail.ramalho added a comment.
This revision is now accepted and ready to land.

Reopening the revision as it was reverted.


Repository:
  rC Clang

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

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

Hi everyone, I just saw your messages and reverted the commits.

Sorry for the inconvenience, but for some reason I didn't get any email from 
the bots. Could you send me the link with the failure?

@brzycki, I'm using Ubuntu 18.04.2 and I'll try to reproduce the error.

@thakis, do you have any idea why this was not sent to the llvm mailing lists?


Repository:
  rC Clang

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

https://reviews.llvm.org/D54978



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D54391: Fix compatibility with z3-4.8.1

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

Since we're supporting version 4.8.1 now, the cmake file should be changed to 
"minimum" instead of "exact".


Repository:
  rL LLVM

https://reviews.llvm.org/D54391



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D50594: [analyzer] [NFC] Introduce separate targets for testing the analyzer: check-clang-analyzer and check-clang-analyzer-z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

I can't comment on the code but it works correctly for me.

I wish I had it a couple of months ago :)


https://reviews.llvm.org/D50594



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D49536: [Analyzer] Quick Fix for exponential execution time when simpilifying complex additive expressions

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

> Uhm, dunno, plist/FileCheck tests are annoying. What i usually do to make 
> sense out of them is update the tested output with the actual output and look 
> at git diff. From that it's usually obvious what exactly happened (warnings 
> added, warnings removed, warnings moved to a different location, intermediate 
> diagnostics added, intermediate diagnostics removed, intermediate diagnostics 
> moved to a different location). Could you do that and see if it makes sense 
> or attach the diff here so that we could have a look?

The diff using Z3 is the removal of all lines inserted in `plist-macros.cpp` by 
this commit. I think it's a note in the first if (assuming condition is true) 
of:

  #define noPathNoteMacro y+y
  int macroInExpressionNoNote(int *p, int y) {
y++;
if (5 + noPathNoteMacro)
  if (p)
;
return *p; // expected-warning {{Dereference of null pointer}}
  }

Maybe using Z3 as CM, the CSA finds the other path, where the condition is 
false?


Repository:
  rL LLVM

https://reviews.llvm.org/D49536



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D49536: [Analyzer] Quick Fix for exponential execution time when simpilifying complex additive expressions

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

I getting the following error when analyzing `test/Analysis/plist-macros.cpp`, 
usign z3 as constraint manager (`-analyzer-constraints=z3 -DANALYZER_CM_Z3`):

  /home/mgadelha/llvm/tools/clang/test/Analysis/plist-macros.cpp:640:16: error: 
CHECK-NEXT: expected string not found in input
  // CHECK-NEXT: line36
 ^
  
/home/mgadelha/llvm/build/tools/clang/test/Analysis/Output/plist-macros.cpp.tmp.plist:562:2:
 note: scanning from here
   line37
   ^

I bisected back to this commit. I reverted it locally and the error goes away.

Any idea why it doesn't work with z3?


Repository:
  rL LLVM

https://reviews.llvm.org/D49536



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D49749: [analyzer] Admit that we can't simplify the newly produced mixed Loc/NonLoc expressions.

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

It fixes Xerces verification. Thanks.


Repository:
  rC Clang

https://reviews.llvm.org/D49749



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D48561: [Analyzer] Moved RangeConstraintManager to header. NFC.

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho abandoned this revision.
mikhail.ramalho added a comment.

We won't need this patch anymore because we'll try another approach in 
https://reviews.llvm.org/D48565.


Repository:
  rC Clang

https://reviews.llvm.org/D48561



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D48561: [Analyzer] Moved RangeConstraintManager to header. NFC.

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

In https://reviews.llvm.org/D48561#1146114, @george.karpenkov wrote:

> After thinking about this change a bit longer, I think it does not make sense.
>
> Albeit poorly named, the previous design had a purpose: 
> `RangedConstraintManager` is a public interface, and `RangeConstraintManager` 
> is a private implementation.
>  Exposing both in the header does not make sense.
>
> For exposing the factory could you just move the factory and it's getter?
>  Another solution is just merging the two classes entirely, but that's more 
> heavyweight, and would force exposing private functions in a header (but 
> those could be just moved to static C functions).
>  @NoQ further comments?


Since we decided to go with the other approach in 
https://reviews.llvm.org/D48565, we don't actually need this patch anymore.


Repository:
  rC Clang

https://reviews.llvm.org/D48561



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D45517: [analyzer] False positive refutation with Z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 149664.
mikhail.ramalho edited the summary of this revision.
mikhail.ramalho added a comment.

Fix naming issue.


https://reviews.llvm.org/D45517

Files:
  include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
  include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
  lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
  lib/StaticAnalyzer/Core/BugReporter.cpp
  lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  test/Analysis/z3-crosscheck.c

Index: test/Analysis/z3-crosscheck.c
===
--- /dev/null
+++ test/Analysis/z3-crosscheck.c
@@ -0,0 +1,51 @@
+// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -DNO_CROSSCHECK -verify %s
+// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: z3
+
+int foo(int x) 
+{
+  int *z = 0;
+  if ((x & 1) && ((x & 1) ^ 1))
+#ifdef NO_CROSSCHECK
+  return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
+#else
+  return *z; // no-warning
+#endif
+  return 0;
+}
+
+void g(int d);
+
+void f(int *a, int *b) {
+  int c = 5;
+  if ((a - b) == 0)
+c = 0;
+  if (a != b)
+#ifdef NO_CROSSCHECK
+g(3 / c); // expected-warning {{Division by zero}}
+#else
+g(3 / c); // no-warning
+#endif
+}
+
+_Bool nondet_bool();
+
+void h(int d) {
+  int x, y, k, z = 1;
+#ifdef NO_CROSSCHECK
+  while (z < k) { // expected-warning {{The right operand of '<' is a garbage value}}
+#else
+  while (z < k) { // expected-warning {{The right operand of '<' is a garbage value}}
+#endif
+z = 2 * z;
+  }
+}
+
+void i() {
+  _Bool c = nondet_bool();
+  if (c) {
+h(1);
+  } else {
+h(2);
+  }
+}
Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===
--- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -44,6 +44,7 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/None.h"
 #include "llvm/ADT/Optional.h"
@@ -2354,3 +2355,46 @@
 
   return std::make_shared(L, "Taint originated here");
 }
+
+static bool
+areConstraintsUnfeasible(BugReporterContext ,
+ const llvm::SmallVector ) {
+  // Create a refutation manager
+  std::unique_ptr RefutationMgr = CreateZ3ConstraintManager(
+  BRC.getStateManager(), BRC.getStateManager().getOwningEngine());
+
+  SMTConstraintManager *SMTRefutationMgr =
+  static_cast(RefutationMgr.get());
+
+  // Add constraints to the solver
+  for (const auto  : Cs)
+SMTRefutationMgr->addRangeConstraints(C);
+
+  // And check for satisfiability
+  return SMTRefutationMgr->isModelFeasible().isConstrainedFalse();
+}
+
+std::shared_ptr
+FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *N,
+const ExplodedNode *PrevN,
+BugReporterContext ,
+BugReport ) {
+  // Collect the constraint for the current state
+  const ConstraintRangeTy  = N->getState()->get();
+  Constraints.push_back(CR);
+
+  // If there are no predecessor, we reached the root node. In this point,
+  // a new refutation manager will be created and the path will be checked
+  // for reachability
+  if (PrevN->pred_size() == 0 && areConstraintsUnfeasible(BRC, Constraints)) {
+BR.markInvalid("Infeasible constraints", N->getLocationContext());
+  }
+
+  return nullptr;
+}
+
+void FalsePositiveRefutationBRVisitor::Profile(
+llvm::FoldingSetNodeID ) const {
+  static int Tag = 0;
+  ID.AddPointer();
+}
Index: lib/StaticAnalyzer/Core/BugReporter.cpp
===
--- lib/StaticAnalyzer/Core/BugReporter.cpp
+++ lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -3143,10 +3143,15 @@
 PathDiagnosticBuilder PDB(*this, R, ErrorGraph.BackMap, );
 const ExplodedNode *N = ErrorGraph.ErrorNode;
 
+// Register refutation visitors first, if they mark the bug invalid no
+// further analysis is required
+R->addVisitor(llvm::make_unique());
+if (getAnalyzerOptions().shouldCrosscheckWithZ3())
+  R->addVisitor(llvm::make_unique());
+
 // Register additional node visitors.
 R->addVisitor(llvm::make_unique());
 R->addVisitor(llvm::make_unique());
-R->addVisitor(llvm::make_unique());
 R->addVisitor(llvm::make_unique());
 
 BugReport::VisitorList visitors;
Index: lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
===
--- 

[PATCH] D45517: [analyzer] False positive refutation with Z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a subscriber: rnkovacs.
mikhail.ramalho added a comment.

> Awesome! Does it mean that the optimization for adding less constraints
>  was in fact buggy?

I pretty sure it was not related to the optimizations, I removed them days
ago (in the previous version of this patch) and the bug was still there.

> 
> 
> 2. Could it be something unrelated to your changes? Any given trunk version 
> can be buggy, but usually those are resolved very fast, so if you update now 
> the issue can go away.
> 
>   Watching cfe-commits mailing list might be helpful there.

I update my repo every other day and it's been happening for the past
two/three weeks :/

The compiler shows the following error:

posix_spawn failed: Argument list too long

There are some discussions in several places about it.


https://reviews.llvm.org/D45517



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D45517: [analyzer] False positive refutation with Z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added inline comments.



Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2366
+
+  SMTConstraintManager *SMTRefutationMgr =
+  static_cast(RefutationMgr.get());

I'm not happy about this cast. Suggestions are welcome.


https://reviews.llvm.org/D45517



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D45517: [analyzer] False positive refutation with Z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 149653.
mikhail.ramalho added a comment.

Update patch based on https://reviews.llvm.org/D47640 and 
https://reviews.llvm.org/D47689.

I updated the test case as the cross check is not marking the true bug as 
invalid anymore.

My `make clang-test` is still failing `Driver/response-file.c` whenever I 
compile clang with Z3. I'll update the patch as soon as I find the reason why.


https://reviews.llvm.org/D45517

Files:
  include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
  include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
  lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
  lib/StaticAnalyzer/Core/BugReporter.cpp
  lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  test/Analysis/z3-crosscheck.c

Index: test/Analysis/z3-crosscheck.c
===
--- /dev/null
+++ test/Analysis/z3-crosscheck.c
@@ -0,0 +1,51 @@
+// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -DNO_CROSSCHECK -verify %s
+// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: z3
+
+int foo(int x) 
+{
+  int *z = 0;
+  if ((x & 1) && ((x & 1) ^ 1))
+#ifdef NO_CROSSCHECK
+  return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
+#else
+  return *z; // no-warning
+#endif
+  return 0;
+}
+
+void g(int d);
+
+void f(int *a, int *b) {
+  int c = 5;
+  if ((a - b) == 0)
+c = 0;
+  if (a != b)
+#ifdef NO_CROSSCHECK
+g(3 / c); // expected-warning {{Division by zero}}
+#else
+g(3 / c); // no-warning
+#endif
+}
+
+_Bool nondet_bool();
+
+void h(int d) {
+  int x, y, k, z = 1;
+#ifdef NO_CROSSCHECK
+  while (z < k) { // expected-warning {{The right operand of '<' is a garbage value}}
+#else
+  while (z < k) { // expected-warning {{The right operand of '<' is a garbage value}}
+#endif
+z = 2 * z;
+  }
+}
+
+void i() {
+  _Bool c = nondet_bool();
+  if (c) {
+h(1);
+  } else {
+h(2);
+  }
+}
Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===
--- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -44,6 +44,7 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/None.h"
 #include "llvm/ADT/Optional.h"
@@ -2354,3 +2355,46 @@
 
   return std::make_shared(L, "Taint originated here");
 }
+
+static bool
+check_constraints(BugReporterContext ,
+  const llvm::SmallVector ) {
+  // Create a refutation manager
+  std::unique_ptr RefutationMgr = CreateZ3ConstraintManager(
+  BRC.getStateManager(), BRC.getStateManager().getOwningEngine());
+
+  SMTConstraintManager *SMTRefutationMgr =
+  static_cast(RefutationMgr.get());
+
+  // Add constraints to the solver
+  for (const auto  : Cs)
+SMTRefutationMgr->addRangeConstraints(C);
+
+  // And check for satisfiability
+  return SMTRefutationMgr->isModelFeasible().isConstrainedFalse();
+}
+
+std::shared_ptr
+FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *N,
+const ExplodedNode *PrevN,
+BugReporterContext ,
+BugReport ) {
+  // Collect the constraint for the current state
+  const ConstraintRangeTy  = N->getState()->get();
+  Constraints.push_back(CR);
+
+  // If there are no predecessor, we reached the root node. In this point,
+  // a new refutation manager will be created and the path will be checked
+  // for reachability
+  if (PrevN->pred_size() == 0 && check_constraints(BRC, Constraints)) {
+BR.markInvalid("Infeasible constraints", N->getLocationContext());
+  }
+
+  return nullptr;
+}
+
+void FalsePositiveRefutationBRVisitor::Profile(
+llvm::FoldingSetNodeID ) const {
+  static int Tag = 0;
+  ID.AddPointer();
+}
Index: lib/StaticAnalyzer/Core/BugReporter.cpp
===
--- lib/StaticAnalyzer/Core/BugReporter.cpp
+++ lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -3143,10 +3143,15 @@
 PathDiagnosticBuilder PDB(*this, R, ErrorGraph.BackMap, );
 const ExplodedNode *N = ErrorGraph.ErrorNode;
 
+// Register refutation visitors first, if they mark the bug invalid no
+// further analysis is required
+R->addVisitor(llvm::make_unique());
+if (getAnalyzerOptions().shouldCrosscheckWithZ3())
+  R->addVisitor(llvm::make_unique());
+
 // Register additional node visitors.
 R->addVisitor(llvm::make_unique());
 R->addVisitor(llvm::make_unique());
-

[PATCH] D45517: [analyzer] False positive refutation with Z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 149524.
mikhail.ramalho added a comment.

- Simplified the API even further by constructing a Z3ConstraintManager object 
directly.
- Update isModelFeasible to return a isModelFeasible
- Update code with the fix for 1-bit long integer


https://reviews.llvm.org/D45517

Files:
  include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
  include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/Z3ConstraintManager.h
  lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
  lib/StaticAnalyzer/Core/BugReporter.cpp
  lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  test/Analysis/z3-crosscheck.c

Index: test/Analysis/z3-crosscheck.c
===
--- /dev/null
+++ test/Analysis/z3-crosscheck.c
@@ -0,0 +1,57 @@
+// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -DNO_CROSSCHECK -verify %s
+// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: z3
+
+#ifndef NO_CROSSCHECK
+// expected-no-diagnostics
+#endif
+
+int foo(int x) 
+{
+  int *z = 0;
+  if ((x & 1) && ((x & 1) ^ 1))
+#ifdef NO_CROSSCHECK
+  return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
+#else
+  return *z; // no-warning
+#endif
+  return 0;
+}
+
+void g(int d);
+
+void f(int *a, int *b) {
+  int c = 5;
+  if ((a - b) == 0)
+c = 0;
+  if (a != b)
+#ifdef NO_CROSSCHECK
+g(3 / c); // expected-warning {{Division by zero}}
+#else
+g(3 / c); // no-warning
+#endif
+}
+
+_Bool nondet_bool();
+
+void h(int d) {
+  int x, y, k, z = 1;
+#ifdef NO_CROSSCHECK
+  while (z < k) { // expected-warning {{The right operand of '<' is a garbage value}}
+#else
+  // FIXME: Should warn about 'k' being a garbage value
+  while (z < k) { // no-warning
+#endif
+z = 2 * z;
+  }
+}
+
+void i() {
+  _Bool c = nondet_bool();
+  if (c) {
+h(1);
+  } else {
+h(2);
+  }
+}
+
Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -8,7 +8,7 @@
 //===--===//
 
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/Z3ConstraintManager.h"
 
 using namespace clang;
@@ -1013,6 +1013,50 @@
   return State->set(CZ);
 }
 
+void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
+  for (const auto  : CR) {
+SymbolRef Sym = I.first;
+
+Z3Expr Constraints = Z3Expr::fromBoolean(false);
+
+for (const auto  : I.second) {
+  const llvm::APSInt  = Range.From();
+  const llvm::APSInt  = Range.To();
+
+  QualType FromTy;
+  llvm::APSInt NewFromInt;
+  std::tie(NewFromInt, FromTy) = fixAPSInt(From);
+  Z3Expr FromExp = Z3Expr::fromAPSInt(NewFromInt);
+
+  QualType SymTy;
+  Z3Expr Exp = getZ3Expr(Sym, );
+  bool IsSignedTy = SymTy->isSignedIntegerOrEnumerationType();
+
+  QualType ToTy;
+  llvm::APSInt NewToInt;
+  std::tie(NewToInt, ToTy) = fixAPSInt(To);
+  Z3Expr ToExp = Z3Expr::fromAPSInt(NewToInt);
+  assert(FromTy == ToTy && "Range values have different types!");
+
+  Z3Expr LHS =
+  getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, FromTy, /*RetTy=*/nullptr);
+  Z3Expr RHS =
+  getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, FromTy, /*RetTy=*/nullptr);
+  Z3Expr SymRange = Z3Expr::fromBinOp(LHS, BO_LAnd, RHS, IsSignedTy);
+  Constraints =
+  Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy);
+}
+Solver.addConstraint(Constraints);
+  }
+}
+
+clang::ento::ConditionTruthVal Z3ConstraintManager::isModelFeasible() {
+  if(Solver.check() == Z3_L_FALSE)
+return false;
+
+  return ConditionTruthVal();
+}
+
 //===--===//
 // Internal implementation.
 //===--===//
Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===
--- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -41,6 +41,7 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
+#include 

[PATCH] D45517: [analyzer] False positive refutation with Z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added inline comments.



Comment at: 
include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:183
+  virtual void reset() {}
+  virtual bool isModelFeasible() { return true; }
+  virtual void addRangeConstraints(ConstraintRangeTy) {}

george.karpenkov wrote:
> mikhail.ramalho wrote:
> > george.karpenkov wrote:
> > > Making those virtual does not make much sense to me.
> > > Returning `true` by default is not correct.
> > > When we are using the visitor, we should already know we have a 
> > > `Z3ConstraintsManager`, why can't we just use methods of that class?
> > Z3ConstraintManager is fully contained inside a .cpp file, so we need 
> > isModelFeasible and addRangeConstraints to be exposed via its base class.
> > 
> > Another solution is to split Z3ConstraintManager into a .h and a .cpp file 
> > and include the header. We would then be able to use it directly, instead 
> > of through a ConstraintManager object.
> > 
> > I honestly prefer the latter. What do you think?
> Yeah, I think we would need a header here.
> In general we try to avoid inheritance and virtual functions unless they are 
> very beneficial, and here they are not.
Cool, I'll create a separate patch for that then.


https://reviews.llvm.org/D45517



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D45517: [analyzer] False positive refutation with Z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added inline comments.



Comment at: 
include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:183
+  virtual void reset() {}
+  virtual bool isModelFeasible() { return true; }
+  virtual void addRangeConstraints(ConstraintRangeTy) {}

george.karpenkov wrote:
> Making those virtual does not make much sense to me.
> Returning `true` by default is not correct.
> When we are using the visitor, we should already know we have a 
> `Z3ConstraintsManager`, why can't we just use methods of that class?
Z3ConstraintManager is fully contained inside a .cpp file, so we need 
isModelFeasible and addRangeConstraints to be exposed via its base class.

Another solution is to split Z3ConstraintManager into a .h and a .cpp file and 
include the header. We would then be able to use it directly, instead of 
through a ConstraintManager object.

I honestly prefer the latter. What do you think?


https://reviews.llvm.org/D45517



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D45517: [analyzer] False positive refutation with Z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added inline comments.



Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2391
+if (!RefutationMgr->isModelFeasible())
+  BR.markInvalid("Infeasible constraints", N->getLocationContext());
+  }

george.karpenkov wrote:
> That would be checking all constraints in all nodes one by one. I thought the 
> idea was to encode all constraints from the entire path and then check all of 
> it.
All the constraints are being added in the previous for loop, isModelFeasible 
only calls check().



Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:925
 
+  void reset() override { Solver.reset(); }
+

george.karpenkov wrote:
> We don't need `reset` anymore.
We don't need it but there's no reason to remove it, right? I might be useful 
in the future.


https://reviews.llvm.org/D45517



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D45517: [analyzer] False positive refutation with Z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added subscribers: dcoughlin, george.karpenkov, NoQ.
mikhail.ramalho added a comment.

Hi,

> Just a bit of context and to have some expectation management regarding
>  this patch. The main purpose of this implementation was to back a thesis.
>  It was made under a very serious time pressure and the main goal was to be
>  able to measure on real world projects as soon as possible and in the
>  meantime to be flexible so we can measure multiple configurations (like
>  incremental solving).
> 
> So the goal was a flexible proof of concept that is sensible to measure in
>  the shortest possible time. After the thesis was done, Reka started to work
>  an another GSoC project, so she had no time to review the code with the
>  requirements of upstreaming in mind. Nevertheless we found that sharing the
>  proof of concept could be useful for the community.  So it is perfectly
>  reasonable if you disagree with some design decisions behind this patch,
>  because the requirements for the thesis (in the short time frame) was very
>  different from the requirements of upstreaming this work. In a different
>  context these decisions made perfect sense.

Just want to comment here and give thanks again for the first version of
the refutation code. It's being really helpful to develop the approach this
code as a base; things would definitely be slower if I had to start it from
scratch.

Thanks!


https://reviews.llvm.org/D45517



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D45517: [analyzer] False positive refutation with Z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 149317.
mikhail.ramalho marked 6 inline comments as not done.
mikhail.ramalho added a comment.

- Simplified refutation process: it now collects all the constraints in a given 
path and, only when it reaches the root node, the refutation manager is created 
and the constraints are checked for reachability. All the optimizations were 
removed.
- Moved RangedConstraintManager.h to include/
- Moved refutation check to be the first in the list of BugVisitors
- Added dump method to Z3Solver (to print the formula)
- Added more documentation/comments


https://reviews.llvm.org/D45517

Files:
  include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
  include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
  lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
  lib/StaticAnalyzer/Core/BugReporter.cpp
  lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  lib/StaticAnalyzer/Core/RangedConstraintManager.h
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  test/Analysis/z3-crosscheck.c

Index: test/Analysis/z3-crosscheck.c
===
--- /dev/null
+++ test/Analysis/z3-crosscheck.c
@@ -0,0 +1,57 @@
+// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -DNO_CROSSCHECK -verify %s
+// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: z3
+
+#ifndef NO_CROSSCHECK
+// expected-no-diagnostics
+#endif
+
+int foo(int x) 
+{
+  int *z = 0;
+  if ((x & 1) && ((x & 1) ^ 1))
+#ifdef NO_CROSSCHECK
+  return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
+#else
+  return *z; // no-warning
+#endif
+  return 0;
+}
+
+void g(int d);
+
+void f(int *a, int *b) {
+  int c = 5;
+  if ((a - b) == 0)
+c = 0;
+  if (a != b)
+#ifdef NO_CROSSCHECK
+g(3 / c); // expected-warning {{Division by zero}}
+#else
+g(3 / c); // no-warning
+#endif
+}
+
+_Bool nondet_bool();
+
+void h(int d) {
+  int x, y, k, z = 1;
+#ifdef NO_CROSSCHECK
+  while (z < k) { // expected-warning {{The right operand of '<' is a garbage value}}
+#else
+  // FIXME: Should warn about 'k' being a garbage value
+  while (z < k) { // no-warning
+#endif
+z = 2 * z;
+  }
+}
+
+void i() {
+  _Bool c = nondet_bool();
+  if (c) {
+h(1);
+  } else {
+h(2);
+  }
+}
+
Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -10,6 +10,7 @@
 #include "clang/Basic/TargetInfo.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
 
 #include "clang/Config/config.h"
@@ -880,6 +881,12 @@
 
   /// Reset the solver and remove all constraints.
   void reset() { Z3_solver_reset(Z3Context::ZC, Solver); }
+
+  void print(raw_ostream ) const {
+OS << Z3_solver_to_string(Z3Context::ZC, Solver);
+  }
+
+  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
 }; // end class Z3Solver
 
 void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
@@ -915,6 +922,17 @@
   void print(ProgramStateRef St, raw_ostream , const char *nl,
  const char *sep) override;
 
+  void reset() override { Solver.reset(); }
+
+  bool isModelFeasible() override {
+return Solver.check() != Z3_L_FALSE;
+  }
+
+  /// Converts the ranged constraints of a set of symbols to SMT
+  ///
+  /// \param CR The set of constraints.
+  void addRangeConstraints(ConstraintRangeTy CR) override;
+
   //===--===//
   // Implementation for interface from SimpleConstraintManager.
   //===--===//
@@ -1235,6 +1253,42 @@
   return State->set(CZ);
 }
 
+void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
+  for (const auto  : CR) {
+SymbolRef Sym = I.first;
+
+Z3Expr Constraints = Z3Expr::fromBoolean(false);
+
+for (const auto  : I.second) {
+  const llvm::APSInt  = Range.From();
+  const llvm::APSInt  = Range.To();
+
+  assert((getAPSIntType(From) == getAPSIntType(To)) &&
+ "Range values have different types!");
+  QualType RangeTy = getAPSIntType(From);
+  // Skip ranges whose endpoints cannot be converted to APSInts with
+  // a valid APSIntType.
+  // FIXME: fix available in D35450

[PATCH] D45517: [analyzer] False positive refutation with Z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 148969.
mikhail.ramalho marked 6 inline comments as done.
mikhail.ramalho added a comment.

1. Moved FalsePositiveRefutationBRVisitor::Profile definition to 
BugReporterVisitor.cpp
2. Update test cases two run twice, with and without the crosscheck
3. Removed the FirstNodeVisited flag (the solver is being reset after checking 
the bug reachability)
4. Use ranged loop when adding the constraints


https://reviews.llvm.org/D45517

Files:
  include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
  include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
  lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
  lib/StaticAnalyzer/Core/BugReporter.cpp
  lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  lib/StaticAnalyzer/Core/ProgramState.cpp
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  test/Analysis/analyzer-config.c
  test/Analysis/analyzer-config.cpp
  test/Analysis/z3-crosscheck.c

Index: test/Analysis/z3-crosscheck.c
===
--- /dev/null
+++ test/Analysis/z3-crosscheck.c
@@ -0,0 +1,57 @@
+// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -DNO_CROSSCHECK -verify %s
+// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: z3
+
+#ifndef NO_CROSSCHECK
+// expected-no-diagnostics
+#endif
+
+int foo(int x) 
+{
+  int *z = 0;
+  if ((x & 1) && ((x & 1) ^ 1))
+#ifdef NO_CROSSCHECK
+  return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
+#else
+  return *z; // no-warning
+#endif
+  return 0;
+}
+
+void g(int d);
+
+void f(int *a, int *b) {
+  int c = 5;
+  if ((a - b) == 0)
+c = 0;
+  if (a != b)
+#ifdef NO_CROSSCHECK
+g(3 / c); // expected-warning {{Division by zero}}
+#else
+g(3 / c); // no-warning
+#endif
+}
+
+_Bool nondet_bool();
+
+void h(int d) {
+  int x, y, k, z = 1;
+#ifdef NO_CROSSCHECK
+  while (z < k) { // expected-warning {{The right operand of '<' is a garbage value}}
+#else
+  // FIXME: Should warn about 'k' being a garbage value
+  while (z < k) { // no-warning
+#endif
+z = 2 * z;
+  }
+}
+
+void i() {
+  _Bool c = nondet_bool();
+  if (c) {
+h(1);
+  } else {
+h(2);
+  }
+}
+
Index: test/Analysis/analyzer-config.cpp
===
--- test/Analysis/analyzer-config.cpp
+++ test/Analysis/analyzer-config.cpp
@@ -32,6 +32,7 @@
 // CHECK-NEXT: cfg-rich-constructors = true
 // CHECK-NEXT: cfg-scopes = false
 // CHECK-NEXT: cfg-temporary-dtors = true
+// CHECK-NEXT: crosscheck-with-z3 = false
 // CHECK-NEXT: experimental-enable-naive-ctu-analysis = false
 // CHECK-NEXT: exploration_strategy = unexplored_first_queue
 // CHECK-NEXT: faux-bodies = true
@@ -50,4 +51,4 @@
 // CHECK-NEXT: unroll-loops = false
 // CHECK-NEXT: widen-loops = false
 // CHECK-NEXT: [stats]
-// CHECK-NEXT: num-entries = 30
+// CHECK-NEXT: num-entries = 31
Index: test/Analysis/analyzer-config.c
===
--- test/Analysis/analyzer-config.c
+++ test/Analysis/analyzer-config.c
@@ -18,6 +18,7 @@
 // CHECK-NEXT: cfg-rich-constructors = true
 // CHECK-NEXT: cfg-scopes = false
 // CHECK-NEXT: cfg-temporary-dtors = true
+// CHECK-NEXT: crosscheck-with-z3 = false
 // CHECK-NEXT: exploration_strategy = unexplored_first_queue
 // CHECK-NEXT: faux-bodies = true
 // CHECK-NEXT: graph-trim-interval = 1000
@@ -35,4 +36,4 @@
 // CHECK-NEXT: unroll-loops = false
 // CHECK-NEXT: widen-loops = false
 // CHECK-NEXT: [stats]
-// CHECK-NEXT: num-entries = 23
+// CHECK-NEXT: num-entries = 24
Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -7,6 +7,7 @@
 //
 //===--===//
 
+#include "RangedConstraintManager.h"
 #include "clang/Basic/TargetInfo.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
@@ -915,6 +916,13 @@
   void print(ProgramStateRef St, raw_ostream , const char *nl,
  const char *sep) override;
 
+  void reset() override;
+
+  bool isModelFeasible() override;
+
+  void addRangeConstraints(ConstraintRangeTy PrevCR, ConstraintRangeTy SuccCR,
+   bool OnlyPurged) override;
+
   //===--===//
   // Implementation for interface from SimpleConstraintManager.
   //===--===//
@@ -1235,6 +1243,58 @@
   return 

[PATCH] D45517: [analyzer] False positive refutation with Z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 148828.
mikhail.ramalho retitled this revision from "[analyzer] WIP: False positive 
refutation with Z3" to "[analyzer] False positive refutation with Z3".
mikhail.ramalho added a comment.

Added test cases and updated the analyzer-config tests with the new crosscheck 
flag.

Currently, there is one test failing that does not fail when building without 
the crosscheck:

  llvm/tools/clang/test/Driver/response-file.c:18:10: error: expected string 
not found in input
  // LONG: extern int it_works;
   ^
  :1:1: note: scanning from here
  clang version 7.0.0 (trunk 52) (llvm/trunk 74)
  ^
  :8:3: note: possible intended match here
  Selected GCC installation: /usr/lib/gcc/x86_64-redhat-linux/6.4.1
^


https://reviews.llvm.org/D45517

Files:
  include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
  include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
  lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
  lib/StaticAnalyzer/Core/BugReporter.cpp
  lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  lib/StaticAnalyzer/Core/ProgramState.cpp
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  test/Analysis/analyzer-config.c
  test/Analysis/analyzer-config.cpp
  test/Analysis/z3-crosscheck.c

Index: test/Analysis/z3-crosscheck.c
===
--- /dev/null
+++ test/Analysis/z3-crosscheck.c
@@ -0,0 +1,41 @@
+// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: z3
+// expected-no-diagnostics
+
+int foo(int x) 
+{
+  int *z = 0;
+  if ((x & 1) && ((x & 1) ^ 1))
+  return *z; // no-warning
+  return 0;
+}
+
+void g(int d);
+
+void f(int *a, int *b) {
+  int c = 5;
+  if ((a - b) == 0)
+c = 0;
+  if (a != b)
+g(3 / c); // no-warning
+}
+
+_Bool nondet_bool();
+
+void h(int d) {
+  int x, y, k, z = 1;
+  // FIXME: Should warn about 'k' being a garbage value
+  while (z < k) { // no-warning
+z = 2 * z;
+  }
+}
+
+void i() {
+  _Bool c = nondet_bool();
+  if (c) {
+h(1);
+  } else {
+h(2);
+  }
+}
+
Index: test/Analysis/analyzer-config.cpp
===
--- test/Analysis/analyzer-config.cpp
+++ test/Analysis/analyzer-config.cpp
@@ -32,6 +32,7 @@
 // CHECK-NEXT: cfg-rich-constructors = true
 // CHECK-NEXT: cfg-scopes = false
 // CHECK-NEXT: cfg-temporary-dtors = true
+// CHECK-NEXT: crosscheck-with-z3 = false
 // CHECK-NEXT: experimental-enable-naive-ctu-analysis = false
 // CHECK-NEXT: exploration_strategy = unexplored_first_queue
 // CHECK-NEXT: faux-bodies = true
@@ -50,4 +51,4 @@
 // CHECK-NEXT: unroll-loops = false
 // CHECK-NEXT: widen-loops = false
 // CHECK-NEXT: [stats]
-// CHECK-NEXT: num-entries = 30
+// CHECK-NEXT: num-entries = 31
Index: test/Analysis/analyzer-config.c
===
--- test/Analysis/analyzer-config.c
+++ test/Analysis/analyzer-config.c
@@ -18,6 +18,7 @@
 // CHECK-NEXT: cfg-rich-constructors = true
 // CHECK-NEXT: cfg-scopes = false
 // CHECK-NEXT: cfg-temporary-dtors = true
+// CHECK-NEXT: crosscheck-with-z3 = false
 // CHECK-NEXT: exploration_strategy = unexplored_first_queue
 // CHECK-NEXT: faux-bodies = true
 // CHECK-NEXT: graph-trim-interval = 1000
@@ -35,4 +36,4 @@
 // CHECK-NEXT: unroll-loops = false
 // CHECK-NEXT: widen-loops = false
 // CHECK-NEXT: [stats]
-// CHECK-NEXT: num-entries = 23
+// CHECK-NEXT: num-entries = 24
Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -7,6 +7,7 @@
 //
 //===--===//
 
+#include "RangedConstraintManager.h"
 #include "clang/Basic/TargetInfo.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
@@ -915,6 +916,13 @@
   void print(ProgramStateRef St, raw_ostream , const char *nl,
  const char *sep) override;
 
+  void reset() override;
+
+  bool isModelFeasible() override;
+
+  void addRangeConstraints(ConstraintRangeTy PrevCR, ConstraintRangeTy SuccCR,
+   bool OnlyPurged) override;
+
   //===--===//
   // Implementation for interface from SimpleConstraintManager.
   //===--===//
@@ -1235,6 +1243,58 @@
   return State->set(CZ);
 }
 
+void Z3ConstraintManager::reset() { Solver.reset(); }
+
+bool Z3ConstraintManager::isModelFeasible() {
+  return Solver.check() != Z3_L_FALSE;
+}
+
+void 

[PATCH] D42966: Fix USR generation in the presence of #line directives or linemarkes

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

> Could you provide a minimal example where USRs are not generated? It might
>  be the case that there are other ways to fix it.

Sure, I'll try to reduce our testcase, but basically we have an
ASTFrontendAction [0] that adds a set of intrinsics [1] to the preprocessor
[2].

[0]
https://github.com/esbmc/esbmc/blob/master/src/clang-c-frontend/AST/esbmc_action.h
[1]
https://github.com/esbmc/esbmc/blob/master/src/clang-c-frontend/clang_c_language.cpp#L206
[2]
https://github.com/esbmc/esbmc/blob/master/src/clang-c-frontend/AST/esbmc_action.h#L31


Repository:
  rC Clang

https://reviews.llvm.org/D42966



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D45517: [analyzer] WIP: False positive refutation with Z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

Commandeering the PR because of GSoC.


https://reviews.llvm.org/D45517



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D45920: [analyzer] Move RangeSet related declarations into the RangedConstraintManager header.

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho commandeered this revision.
mikhail.ramalho added a reviewer: rnkovacs.
mikhail.ramalho added a comment.

Commandeering the PR because of GSoC.


Repository:
  rC Clang

https://reviews.llvm.org/D45920



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D36610: [Tooling] Add option to getFullyQualifiedName using a custom PritingPolicy

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 145255.
mikhail.ramalho added a comment.

Fixed the test case.


https://reviews.llvm.org/D36610

Files:
  include/clang/AST/QualTypeNames.h
  lib/AST/QualTypeNames.cpp
  unittests/Tooling/QualTypeNamesTest.cpp


Index: unittests/Tooling/QualTypeNamesTest.cpp
===
--- unittests/Tooling/QualTypeNamesTest.cpp
+++ unittests/Tooling/QualTypeNamesTest.cpp
@@ -26,9 +26,13 @@
 std::string ExpectedName =
 ExpectedQualTypeNames.lookup(VD->getNameAsString());
 if (ExpectedName != "") {
-  std::string ActualName =
-  TypeName::getFullyQualifiedName(VD->getType(), *Context,
-  WithGlobalNsPrefix);
+  PrintingPolicy Policy(Context->getPrintingPolicy());
+  Policy.SuppressScope = false;
+  Policy.AnonymousTagLocations = true;
+  Policy.PolishForDeclaration = true;
+  Policy.SuppressUnwrittenScope = true;
+  std::string ActualName = TypeName::getFullyQualifiedName(
+  VD->getType(), *Context, Policy, WithGlobalNsPrefix);
   if (ExpectedName != ActualName) {
 // A custom message makes it much easier to see what declaration
 // failed compared to EXPECT_EQ.
@@ -217,6 +221,26 @@
   "  }\n"
   "}\n"
   );
+
+  TypeNameVisitor AnonStrucs;
+  AnonStrucs.ExpectedQualTypeNames["a"] = "short";
+  AnonStrucs.ExpectedQualTypeNames["un_in_st_1"] =
+  "union (anonymous struct at input.cc:1:1)::(anonymous union at "
+  "input.cc:2:27)";
+  AnonStrucs.ExpectedQualTypeNames["b"] = "short";
+  AnonStrucs.ExpectedQualTypeNames["un_in_st_2"] =
+  "union (anonymous struct at input.cc:1:1)::(anonymous union at "
+  "input.cc:5:27)";
+  AnonStrucs.ExpectedQualTypeNames["anon_st"] =
+  "struct (anonymous struct at input.cc:1:1)";
+  AnonStrucs.runOver(R"(struct {
+  union {
+short a;
+  } un_in_st_1;
+  union {
+short b;
+  } un_in_st_2;
+} anon_st;)");
 }
 
 }  // end anonymous namespace
Index: lib/AST/QualTypeNames.cpp
===
--- lib/AST/QualTypeNames.cpp
+++ lib/AST/QualTypeNames.cpp
@@ -452,12 +452,8 @@
 
 std::string getFullyQualifiedName(QualType QT,
   const ASTContext ,
+  const PrintingPolicy ,
   bool WithGlobalNsPrefix) {
-  PrintingPolicy Policy(Ctx.getPrintingPolicy());
-  Policy.SuppressScope = false;
-  Policy.AnonymousTagLocations = false;
-  Policy.PolishForDeclaration = true;
-  Policy.SuppressUnwrittenScope = true;
   QualType FQQT = getFullyQualifiedType(QT, Ctx, WithGlobalNsPrefix);
   return FQQT.getAsString(Policy);
 }
Index: include/clang/AST/QualTypeNames.h
===
--- include/clang/AST/QualTypeNames.h
+++ include/clang/AST/QualTypeNames.h
@@ -72,6 +72,7 @@
 /// \param[in] WithGlobalNsPrefix - If true, then the global namespace
 /// specifier "::" will be prepended to the fully qualified name.
 std::string getFullyQualifiedName(QualType QT, const ASTContext ,
+  const PrintingPolicy ,
   bool WithGlobalNsPrefix = false);
 
 /// \brief Generates a QualType that can be used to name the same type


Index: unittests/Tooling/QualTypeNamesTest.cpp
===
--- unittests/Tooling/QualTypeNamesTest.cpp
+++ unittests/Tooling/QualTypeNamesTest.cpp
@@ -26,9 +26,13 @@
 std::string ExpectedName =
 ExpectedQualTypeNames.lookup(VD->getNameAsString());
 if (ExpectedName != "") {
-  std::string ActualName =
-  TypeName::getFullyQualifiedName(VD->getType(), *Context,
-  WithGlobalNsPrefix);
+  PrintingPolicy Policy(Context->getPrintingPolicy());
+  Policy.SuppressScope = false;
+  Policy.AnonymousTagLocations = true;
+  Policy.PolishForDeclaration = true;
+  Policy.SuppressUnwrittenScope = true;
+  std::string ActualName = TypeName::getFullyQualifiedName(
+  VD->getType(), *Context, Policy, WithGlobalNsPrefix);
   if (ExpectedName != ActualName) {
 // A custom message makes it much easier to see what declaration
 // failed compared to EXPECT_EQ.
@@ -217,6 +221,26 @@
   "  }\n"
   "}\n"
   );
+
+  TypeNameVisitor AnonStrucs;
+  AnonStrucs.ExpectedQualTypeNames["a"] = "short";
+  AnonStrucs.ExpectedQualTypeNames["un_in_st_1"] =
+  "union (anonymous struct at input.cc:1:1)::(anonymous union at "
+  "input.cc:2:27)";
+  AnonStrucs.ExpectedQualTypeNames["b"] = "short";
+  AnonStrucs.ExpectedQualTypeNames["un_in_st_2"] =
+  "union (anonymous 

[PATCH] D36610: [Tooling] Add option to getFullyQualifiedName using a custom PritingPolicy

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

Thanks.

I just need someone to push it, as I don't have write access to the repo.


https://reviews.llvm.org/D36610



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D42966: Fix USR generation in the presence of #line directives or linemarkes

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

Hi,

> I would say "yes". Let's not rely on linemarkers, unless we can explain
>  why that's a good idea.

Sounds reasonable to me, specially considering cases like rename and
find-declaration.

> Where do virtual files come from in the first place?

From the linemarker:
https://gcc.gnu.org/onlinedocs/cpp/Preprocessor-Output.html

For instance:

$ cat foo.c

int f(int a);

1 "file1.c" 1
=

int g(int b);

clang generates:

| -FunctionDecl 0x6866ff0  col:5 f 'int (int)' |
| `-ParmVarDecl 0x6866f30  col:11 a 'int'  |
|

`-FunctionDecl 0x6867138  col:5 g 'int (int)'

  `-ParmVarDecl 0x68670b0  col:11 b 'int'

Note that the location of f and g are different, despite being in the same
file.

The preprocessor inserts linemarkers by default:

$ clang foo.c -E

1. 1 "foo.c"
2. 1 "" 1
3. 1 "" 3
4. 349 "" 3
5. 1 "" 1
6. 1 "" 2
7. 1 "foo.c" 2

int f(int a);

1 "file1.c" 1
=

int g(int b);

unless you call it with -P:

$ clang foo.c -E -P

int f(int a);

int g(int b);

> Repository:
> 
>   rC Clang
> 
> https://reviews.llvm.org/D42966


Repository:
  rC Clang

https://reviews.llvm.org/D42966



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D42966: Fix USR generation in the presence of #line directives or linemarkes

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

Hi,

> Filename + offset for things like function parameters, where we have to
>  identify the particular function declaration they're part of.
>  For static functions themselveds, just the filename. I think this is
>  current behavior in both cases.

But then we're back to the initial question, what to do when there are
linemarkers that change the filename/line number?

Should we ignore linemarkers and use filename + offset of the real file?
Should we try to calculate the offset of the decl in the virtual file?

Thank you,


Repository:
  rC Clang

https://reviews.llvm.org/D42966



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D36610: [Tooling] Add option to getFullyQualifiedName using a custom PritingPolicy

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added subscribers: rsmith, rnk.
mikhail.ramalho added a comment.

Last review asked to change the test case, I just want to make sure
everything is fine this time.


https://reviews.llvm.org/D36610



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D42966: Fix USR generation in the presence of #line directives or linemarkes

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

Hi,

> After thinking about this a bit, and use cases like rename and
>  find-declaration that could be USR based, I think including some location
>  information is the right way to go, which I think is the current behavior.

What do you man by location information? Only the filename or filename +
offset (current behaviour)?


Repository:
  rC Clang

https://reviews.llvm.org/D42966



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D36610: [Tooling] Add option to getFullyQualifiedName using a custom PritingPolicy

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho marked an inline comment as done.
mikhail.ramalho added a comment.

Ping.


https://reviews.llvm.org/D36610



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D42966: Fix USR generation in the presence of #line directives or linemarkes

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a subscriber: rsmith.
mikhail.ramalho added a comment.

Hi,

> Or is the that whenever there's a `#line` directive we get into a
>  "virtual" file that's not registered in the `SourceManager`?

The virtual file is actually registered in the SourceManager but the
FileEntry for it is NULL (USRGeneration.cpp:33), which forces printLoc to
return true (USRGeneration.cpp:38) and the USR is not generated.

I believe the USR gen for params should have follow the functionDecl
convention. I'm reworking the patch now.

> int func(int param1);
>  int func(int param2);
>  // param1 and param2 could both have the same USR, but different names.
>  That might (or might not) be surprising.

I agree here, they should have the same USR.


Repository:
  rC Clang

https://reviews.llvm.org/D42966



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D42966: Fix USR generation in the presence of #line directives or linemarkes

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a subscriber: arphaman.
mikhail.ramalho added a comment.

> Why wasn't there a file for function parameter? Function parameters *are*
>  declared in some file, or am I missing something?

They are declared in some file defined by the line markers; the file are
not registered in the SourceManager as actual files, so getting the
FileEntry will always fail, that's why I changed it to get the PresumedLoc.

More general question is: how do we want USRs for function parameters to

> work, specifically should USR of the same param of different declarations
>  be the same or different?

That's a good point, this patch will generated different names for the same
function param if a function is first defined then declared somewhere else.

I guess it should follow the USR generation pattern for FunctionDecls, what
do you think?


Repository:
  rC Clang

https://reviews.llvm.org/D42966



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D36610: [Tooling] Add option to getFullyQualifiedName using a custom PritingPolicy

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho marked an inline comment as done.
mikhail.ramalho added a comment.

ping.




Comment at: unittests/Tooling/QualTypeNamesTest.cpp:225
+
+  TypeNameVisitor PrintingPolicy;
+  PrintingPolicy.ExpectedQualTypeNames["a"] = "short";

rnk wrote:
> Please choose a different variable name that doesn't clash with the 
> PrintingPolicy type.
Done.


https://reviews.llvm.org/D36610



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D42966: Fix USR generation in the presence of #line directives or linemarkes

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

ping.


Repository:
  rC Clang

https://reviews.llvm.org/D42966



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D42966: Fix USR generation in the presence of #line directives or linemarkes

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

Sure. Basically, the previous code would not generate the USR for the 
function's parameters.

The issue was that SM.getFileEntryForID would return NULL because there is no 
actual file, that's why I changed to get the presumedLoc and build the name 
using the column/line.

I know that using column/line not the preferable method to generate USR but I 
couldn't find a way to generate the offset of a presumed location.


Repository:
  rC Clang

https://reviews.llvm.org/D42966



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D36610: [Tooling] Add option to getFullyQualifiedName using a custom PritingPolicy

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 142709.
mikhail.ramalho added a comment.

Renamed variables in the test so it doesn't match the type name


https://reviews.llvm.org/D36610

Files:
  include/clang/AST/QualTypeNames.h
  lib/AST/QualTypeNames.cpp
  unittests/Tooling/QualTypeNamesTest.cpp


Index: unittests/Tooling/QualTypeNamesTest.cpp
===
--- unittests/Tooling/QualTypeNamesTest.cpp
+++ unittests/Tooling/QualTypeNamesTest.cpp
@@ -26,9 +26,13 @@
 std::string ExpectedName =
 ExpectedQualTypeNames.lookup(VD->getNameAsString());
 if (ExpectedName != "") {
-  std::string ActualName =
-  TypeName::getFullyQualifiedName(VD->getType(), *Context,
-  WithGlobalNsPrefix);
+  PrintingPolicy Policy(Context->getPrintingPolicy());
+  Policy.SuppressScope = false;
+  Policy.AnonymousTagLocations = true;
+  Policy.PolishForDeclaration = true;
+  Policy.SuppressUnwrittenScope = true;
+  std::string ActualName = TypeName::getFullyQualifiedName(
+  VD->getType(), *Context, Policy, WithGlobalNsPrefix);
   if (ExpectedName != ActualName) {
 // A custom message makes it much easier to see what declaration
 // failed compared to EXPECT_EQ.
@@ -217,6 +221,26 @@
   "  }\n"
   "}\n"
   );
+
+  TypeNameVisitor AnonStrucs;
+  AnonStrucs.ExpectedQualTypeNames["a"] = "short";
+  AnonStrucs.ExpectedQualTypeNames["un_in_st_1"] =
+  "union (anonymous struct at input.cc:1:1)::(anonymous union at "
+  "input.cc:2:31)";
+  AnonStrucs.ExpectedQualTypeNames["b"] = "short";
+  AnonStrucs.ExpectedQualTypeNames["un_in_st_2"] =
+  "union (anonymous struct at input.cc:1:1)::(anonymous union at "
+  "input.cc:5:31)";
+  AnonStrucs.ExpectedQualTypeNames["anon_st"] =
+  "struct (anonymous struct at input.cc:1:1)";
+  AnonStrucs.runOver(R"(struct {
+  union {
+short a;
+  } un_in_st_1;
+  union {
+short b;
+  } un_in_st_2;
+} anon_st;)");
 }
 
-}  // end anonymous namespace
+} // end anonymous namespace
Index: lib/AST/QualTypeNames.cpp
===
--- lib/AST/QualTypeNames.cpp
+++ lib/AST/QualTypeNames.cpp
@@ -450,14 +450,9 @@
   return QT;
 }
 
-std::string getFullyQualifiedName(QualType QT,
-  const ASTContext ,
+std::string getFullyQualifiedName(QualType QT, const ASTContext ,
+  const PrintingPolicy ,
   bool WithGlobalNsPrefix) {
-  PrintingPolicy Policy(Ctx.getPrintingPolicy());
-  Policy.SuppressScope = false;
-  Policy.AnonymousTagLocations = false;
-  Policy.PolishForDeclaration = true;
-  Policy.SuppressUnwrittenScope = true;
   QualType FQQT = getFullyQualifiedType(QT, Ctx, WithGlobalNsPrefix);
   return FQQT.getAsString(Policy);
 }
Index: include/clang/AST/QualTypeNames.h
===
--- include/clang/AST/QualTypeNames.h
+++ include/clang/AST/QualTypeNames.h
@@ -72,6 +72,7 @@
 /// \param[in] WithGlobalNsPrefix - If true, then the global namespace
 /// specifier "::" will be prepended to the fully qualified name.
 std::string getFullyQualifiedName(QualType QT, const ASTContext ,
+  const PrintingPolicy ,
   bool WithGlobalNsPrefix = false);
 
 /// \brief Generates a QualType that can be used to name the same type


Index: unittests/Tooling/QualTypeNamesTest.cpp
===
--- unittests/Tooling/QualTypeNamesTest.cpp
+++ unittests/Tooling/QualTypeNamesTest.cpp
@@ -26,9 +26,13 @@
 std::string ExpectedName =
 ExpectedQualTypeNames.lookup(VD->getNameAsString());
 if (ExpectedName != "") {
-  std::string ActualName =
-  TypeName::getFullyQualifiedName(VD->getType(), *Context,
-  WithGlobalNsPrefix);
+  PrintingPolicy Policy(Context->getPrintingPolicy());
+  Policy.SuppressScope = false;
+  Policy.AnonymousTagLocations = true;
+  Policy.PolishForDeclaration = true;
+  Policy.SuppressUnwrittenScope = true;
+  std::string ActualName = TypeName::getFullyQualifiedName(
+  VD->getType(), *Context, Policy, WithGlobalNsPrefix);
   if (ExpectedName != ActualName) {
 // A custom message makes it much easier to see what declaration
 // failed compared to EXPECT_EQ.
@@ -217,6 +221,26 @@
   "  }\n"
   "}\n"
   );
+
+  TypeNameVisitor AnonStrucs;
+  AnonStrucs.ExpectedQualTypeNames["a"] = "short";
+  AnonStrucs.ExpectedQualTypeNames["un_in_st_1"] =
+  "union (anonymous struct at input.cc:1:1)::(anonymous union at "
+  

[PATCH] D36610: [Tooling] Add option to getFullyQualifiedName using a custom PritingPolicy

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 142578.
mikhail.ramalho added a comment.

Rebased to current master.

Removed the getFullyQualifiedName overloaded function.


https://reviews.llvm.org/D36610

Files:
  include/clang/AST/QualTypeNames.h
  lib/AST/QualTypeNames.cpp
  unittests/Tooling/QualTypeNamesTest.cpp


Index: unittests/Tooling/QualTypeNamesTest.cpp
===
--- unittests/Tooling/QualTypeNamesTest.cpp
+++ unittests/Tooling/QualTypeNamesTest.cpp
@@ -26,9 +26,13 @@
 std::string ExpectedName =
 ExpectedQualTypeNames.lookup(VD->getNameAsString());
 if (ExpectedName != "") {
-  std::string ActualName =
-  TypeName::getFullyQualifiedName(VD->getType(), *Context,
-  WithGlobalNsPrefix);
+  PrintingPolicy Policy(Context->getPrintingPolicy());
+  Policy.SuppressScope = false;
+  Policy.AnonymousTagLocations = true;
+  Policy.PolishForDeclaration = true;
+  Policy.SuppressUnwrittenScope = true;
+  std::string ActualName = TypeName::getFullyQualifiedName(
+  VD->getType(), *Context, Policy, WithGlobalNsPrefix);
   if (ExpectedName != ActualName) {
 // A custom message makes it much easier to see what declaration
 // failed compared to EXPECT_EQ.
@@ -217,6 +221,26 @@
   "  }\n"
   "}\n"
   );
+
+  TypeNameVisitor PrintingPolicy;
+  PrintingPolicy.ExpectedQualTypeNames["a"] = "short";
+  PrintingPolicy.ExpectedQualTypeNames["un_in_st_1"] =
+  "union (anonymous struct at input.cc:1:1)::(anonymous union at "
+  "input.cc:2:31)";
+  PrintingPolicy.ExpectedQualTypeNames["b"] = "short";
+  PrintingPolicy.ExpectedQualTypeNames["un_in_st_2"] =
+  "union (anonymous struct at input.cc:1:1)::(anonymous union at "
+  "input.cc:5:31)";
+  PrintingPolicy.ExpectedQualTypeNames["anon_st"] =
+  "struct (anonymous struct at input.cc:1:1)";
+  PrintingPolicy.runOver(R"(struct {
+  union {
+short a;
+  } un_in_st_1;
+  union {
+short b;
+  } un_in_st_2;
+} anon_st;)");
 }
 
 }  // end anonymous namespace
Index: lib/AST/QualTypeNames.cpp
===
--- lib/AST/QualTypeNames.cpp
+++ lib/AST/QualTypeNames.cpp
@@ -450,14 +450,9 @@
   return QT;
 }
 
-std::string getFullyQualifiedName(QualType QT,
-  const ASTContext ,
+std::string getFullyQualifiedName(QualType QT, const ASTContext ,
+  const PrintingPolicy ,
   bool WithGlobalNsPrefix) {
-  PrintingPolicy Policy(Ctx.getPrintingPolicy());
-  Policy.SuppressScope = false;
-  Policy.AnonymousTagLocations = false;
-  Policy.PolishForDeclaration = true;
-  Policy.SuppressUnwrittenScope = true;
   QualType FQQT = getFullyQualifiedType(QT, Ctx, WithGlobalNsPrefix);
   return FQQT.getAsString(Policy);
 }
Index: include/clang/AST/QualTypeNames.h
===
--- include/clang/AST/QualTypeNames.h
+++ include/clang/AST/QualTypeNames.h
@@ -72,6 +72,7 @@
 /// \param[in] WithGlobalNsPrefix - If true, then the global namespace
 /// specifier "::" will be prepended to the fully qualified name.
 std::string getFullyQualifiedName(QualType QT, const ASTContext ,
+  const PrintingPolicy ,
   bool WithGlobalNsPrefix = false);
 
 /// \brief Generates a QualType that can be used to name the same type


Index: unittests/Tooling/QualTypeNamesTest.cpp
===
--- unittests/Tooling/QualTypeNamesTest.cpp
+++ unittests/Tooling/QualTypeNamesTest.cpp
@@ -26,9 +26,13 @@
 std::string ExpectedName =
 ExpectedQualTypeNames.lookup(VD->getNameAsString());
 if (ExpectedName != "") {
-  std::string ActualName =
-  TypeName::getFullyQualifiedName(VD->getType(), *Context,
-  WithGlobalNsPrefix);
+  PrintingPolicy Policy(Context->getPrintingPolicy());
+  Policy.SuppressScope = false;
+  Policy.AnonymousTagLocations = true;
+  Policy.PolishForDeclaration = true;
+  Policy.SuppressUnwrittenScope = true;
+  std::string ActualName = TypeName::getFullyQualifiedName(
+  VD->getType(), *Context, Policy, WithGlobalNsPrefix);
   if (ExpectedName != ActualName) {
 // A custom message makes it much easier to see what declaration
 // failed compared to EXPECT_EQ.
@@ -217,6 +221,26 @@
   "  }\n"
   "}\n"
   );
+
+  TypeNameVisitor PrintingPolicy;
+  PrintingPolicy.ExpectedQualTypeNames["a"] = "short";
+  PrintingPolicy.ExpectedQualTypeNames["un_in_st_1"] =
+  "union 

[PATCH] D42966: Fix USR generation in the presence of #line directives or linemarkes

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

ping.


Repository:
  rC Clang

https://reviews.llvm.org/D42966



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D42966: Fix USR generation in the presence of #line directives or linemarkes

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho created this revision.
mikhail.ramalho added reviewers: arphaman, rsmith.
Herald added a subscriber: cfe-commits.

Small change on how the USRGen code prints the location.

The patch fixes an issue when there are #line directives or linemarkes in the 
file, e.g.:

  #line 3
  int Func(int arg);
  
  #line 10 "file.h"
  int Func(int arg1);
  
  # 1 "file1.c" 1
  int Func(int arg);

These testes were added to test/Index/usrs.cpp.

I changed the printLoc function to, instead of adding the declaration offset to 
the name, it gets the presumedLoc (which handles line directives or 
linemarkes), and adds the line and column to the name, in the format 
:.

The patch only changes the printLoc function in lib/index/USRGeneration.cpp; 
the other changes are test updates.


Repository:
  rC Clang

https://reviews.llvm.org/D42966

Files:
  lib/Index/USRGeneration.cpp
  test/Index/cxx11-lambdas.cpp
  test/Index/get-cursor.cpp
  test/Index/index-templates.cpp
  test/Index/pch-opaque-value.cpp
  test/Index/usrs.cpp
  test/Index/usrs.m

Index: test/Index/usrs.m
===
--- test/Index/usrs.m
+++ test/Index/usrs.m
@@ -102,14 +102,14 @@
 
 // RUN: c-index-test -test-load-source-usrs all -target x86_64-apple-macosx10.7 %s -isystem %S/Inputs | FileCheck %s
 // CHECK: usrs-system.h c:@macro@MACRO_FROM_SYSTEM_HEADER_1 Extent=[1:9 - 1:40]
-// CHECK: usrs.m c:usrs.m@1265@macro@MACRO1 Extent=[94:9 - 94:19]
-// CHECK: usrs.m c:usrs.m@1285@macro@MACRO2 Extent=[96:9 - 96:19]
-// CHECK: usrs.m c:usrs.m@1318@macro@MACRO2 Extent=[98:9 - 98:19]
-// CHECK: usrs.m c:usrs.m@1338@macro@MACRO3 Extent=[100:9 - 100:25]
-// CHECK: usrs.m c:usrs.m@1363@macro@MACRO3 Extent=[101:9 - 101:25]
+// CHECK: usrs.m c:usrs.m@94:9@macro@MACRO1 Extent=[94:9 - 94:19]
+// CHECK: usrs.m c:usrs.m@96:9@macro@MACRO2 Extent=[96:9 - 96:19]
+// CHECK: usrs.m c:usrs.m@98:9@macro@MACRO2 Extent=[98:9 - 98:19]
+// CHECK: usrs.m c:usrs.m@100:9@macro@MACRO3 Extent=[100:9 - 100:25]
+// CHECK: usrs.m c:usrs.m@101:9@macro@MACRO3 Extent=[101:9 - 101:25]
 // CHECK: usrs.m c:usrs.m@F@my_helper Extent=[3:1 - 3:60]
-// CHECK: usrs.m c:usrs.m@95@F@my_helper@x Extent=[3:29 - 3:34]
-// CHECK: usrs.m c:usrs.m@102@F@my_helper@y Extent=[3:36 - 3:41]
+// CHECK: usrs.m c:usrs.m@3:29@F@my_helper@x Extent=[3:29 - 3:34]
+// CHECK: usrs.m c:usrs.m@3:36@F@my_helper@y Extent=[3:36 - 3:41]
 // CHECK: usrs.m c:@Ea@ABA Extent=[5:1 - 8:2]
 // CHECK: usrs.m c:@Ea@ABA@ABA Extent=[6:3 - 6:6]
 // CHECK: usrs.m c:@Ea@ABA@CADABA Extent=[7:3 - 7:9]
@@ -131,22 +131,22 @@
 // CHECK: usrs.m c:objc(cs)Foo(py)d1 Extent=[31:1 - 31:17]
 // CHECK: usrs.m c:objc(cs)Foo(im)d1 Extent=[31:15 - 31:17]
 // CHECK: usrs.m c:objc(cs)Foo(im)setD1: Extent=[31:15 - 31:17]
-// CHECK: usrs.m c:usrs.m@352objc(cs)Foo(im)setD1:@d1 Extent=[31:15 - 31:17]
+// CHECK: usrs.m c:usrs.m@31:15objc(cs)Foo(im)setD1:@d1 Extent=[31:15 - 31:17]
 // CHECK: usrs.m c:objc(cs)Foo Extent=[34:1 - 45:2]
 // CHECK: usrs.m c:objc(cs)Foo(im)godzilla Extent=[35:1 - 39:2]
-// CHECK: usrs.m c:usrs.m@402objc(cs)Foo(im)godzilla@a Extent=[36:3 - 36:19]
+// CHECK: usrs.m c:usrs.m@36:3objc(cs)Foo(im)godzilla@a Extent=[36:3 - 36:19]
 // CHECK: usrs.m c:@z Extent=[37:3 - 37:15]
 // CHECK: usrs.m c:objc(cs)Foo(cm)kingkong Extent=[40:1 - 43:2]
-// CHECK: usrs.m c:usrs.m@470objc(cs)Foo(cm)kingkong@local_var Extent=[41:3 - 41:16]
+// CHECK: usrs.m c:usrs.m@41:3objc(cs)Foo(cm)kingkong@local_var Extent=[41:3 - 41:16]
 // CHECK: usrs.m c:objc(cs)Foo(py)d1 Extent=[44:1 - 44:15]
 // CHECK: usrs.m c:@z Extent=[47:1 - 47:6]
 // CHECK: usrs.m c:usrs.m@F@local_func Extent=[49:1 - 49:43]
-// CHECK: usrs.m c:usrs.m@551@F@local_func@x Extent=[49:23 - 49:28]
+// CHECK: usrs.m c:usrs.m@49:23@F@local_func@x Extent=[49:23 - 49:28]
 // CHECK: usrs.m c:objc(cs)CWithExt Extent=[51:1 - 53:5]
 // CHECK: usrs.m c:objc(cs)CWithExt(im)meth1 Extent=[52:1 - 52:14]
-// CHECK: usrs.m c:objc(ext)CWithExt@usrs.m@612 Extent=[54:1 - 56:5]
+// CHECK: usrs.m c:objc(ext)CWithExt@usrs.m@54:1 Extent=[54:1 - 56:5]
 // CHECK: usrs.m c:objc(cs)CWithExt(im)meth2 Extent=[55:1 - 55:14]
-// CHECK: usrs.m c:objc(ext)CWithExt@usrs.m@654 Extent=[57:1 - 59:5]
+// CHECK: usrs.m c:objc(ext)CWithExt@usrs.m@57:1 Extent=[57:1 - 59:5]
 // CHECK: usrs.m c:objc(cs)CWithExt(im)meth3 Extent=[58:1 - 58:14]
 // CHECK: usrs.m c:objc(cy)CWithExt@Bar Extent=[60:1 - 62:5]
 // CHECK: usrs.m c:objc(cs)CWithExt(im)meth4 Extent=[61:1 - 61:14]
@@ -158,13 +158,13 @@
 // CHECK: usrs.m c:objc(cs)CWithExt(im)meth4 Extent=[69:1 - 69:27]
 // CHECK: usrs.m c:@F@aux_1 Extent=[72:1 - 72:26]
 // CHECK: usrs.m c:@F@test_multi_declaration Extent=[73:1 - 77:2]
-// CHECK: usrs.m c:usrs.m@980@F@test_multi_declaration@foo Extent=[74:3 - 74:14]
-// CHECK: usrs.m c:usrs.m@980@F@test_multi_declaration@bar Extent=[74:16 - 74:23]
-// CHECK: usrs.m c:usrs.m@980@F@test_multi_declaration@baz Extent=[74:25 - 74:32]
+// CHECK: usrs.m c:usrs.m@74:3@F@test_multi_declaration@foo 

[PATCH] D36610: [Tooling] Add option to getFullyQualifiedName using a custom PritingPolicy

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

Should we keep just the version with the custom printing policy then?


https://reviews.llvm.org/D36610



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D36610: [Tooling] Add option to getFullyQualifiedName using a custom PritingPolicy

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho marked an inline comment as done.
mikhail.ramalho added a comment.

ping


https://reviews.llvm.org/D36610



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D36610: [Tooling] Add option to getFullyQualifiedName using a custom PritingPolicy

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 63.
mikhail.ramalho added a comment.

Updated QualTypeNamesTest.cpp to use multiline string in all tests.

Also ran clang-format -style=LLVM for code style.


https://reviews.llvm.org/D36610

Files:
  include/clang/Tooling/Core/QualTypeNames.h
  lib/Tooling/Core/QualTypeNames.cpp
  unittests/Tooling/QualTypeNamesTest.cpp

Index: unittests/Tooling/QualTypeNamesTest.cpp
===
--- unittests/Tooling/QualTypeNamesTest.cpp
+++ unittests/Tooling/QualTypeNamesTest.cpp
@@ -7,28 +7,40 @@
 //
 //===--===//
 
-#include "clang/Tooling/Core/QualTypeNames.h"
 #include "TestVisitor.h"
+#include "clang/Tooling/Core/QualTypeNames.h"
 using namespace clang;
 
 namespace {
 struct TypeNameVisitor : TestVisitor {
   llvm::StringMap ExpectedQualTypeNames;
   bool WithGlobalNsPrefix = false;
+  bool CustomPrintingPolicy = false;
 
   // ValueDecls are the least-derived decl with both a qualtype and a
   // name.
   bool traverseDecl(Decl *D) {
-return true;  // Always continue
+return true; // Always continue
   }
 
   bool VisitValueDecl(const ValueDecl *VD) {
 std::string ExpectedName =
 ExpectedQualTypeNames.lookup(VD->getNameAsString());
 if (ExpectedName != "") {
-  std::string ActualName =
-  TypeName::getFullyQualifiedName(VD->getType(), *Context,
-  WithGlobalNsPrefix);
+  std::string ActualName;
+  if (!CustomPrintingPolicy)
+ActualName = TypeName::getFullyQualifiedName(VD->getType(), *Context,
+ WithGlobalNsPrefix);
+  else {
+PrintingPolicy Policy(Context->getPrintingPolicy());
+Policy.SuppressScope = false;
+Policy.AnonymousTagLocations = true;
+Policy.PolishForDeclaration = true;
+Policy.SuppressUnwrittenScope = true;
+ActualName = TypeName::getFullyQualifiedName(
+VD->getType(), *Context, Policy, WithGlobalNsPrefix);
+  }
+
   if (ExpectedName != ActualName) {
 // A custom message makes it much easier to see what declaration
 // failed compared to EXPECT_EQ.
@@ -93,94 +105,92 @@
   Visitor.ExpectedQualTypeNames["CheckM"] = "const A::B::Class0 *";
   Visitor.ExpectedQualTypeNames["CheckN"] = "const X *";
   Visitor.runOver(
-  "int CheckInt;\n"
-  "template \n"
-  "class OuterTemplateClass { };\n"
-  "namespace A {\n"
-  " namespace B {\n"
-  "   class Class0 { };\n"
-  "   namespace C {\n"
-  " typedef int MyInt;"
-  " template \n"
-  " using InnerAlias = OuterTemplateClass;\n"
-  " InnerAlias AliasTypeVal;\n"
-  "   }\n"
-  "   template class Template0;"
-  "   template class Template1;"
-  "   typedef B::Class0 AnotherClass;\n"
-  "   void Function1(Template0 CheckC);\n"
-  "   void Function2(Template0,\n"
-  "Template0 > CheckD);\n"
-  "   void Function3(const B::Class0* CheckM);\n"
-  "  }\n"
-  "template class Variadic {};\n"
-  "Variadic, "
-  " B::Template1, "
-  " B::C::MyInt > CheckE;\n"
-  " namespace BC = B::C;\n"
-  " BC::MyInt CheckL;\n"
-  "}\n"
-  "using A::B::Class0;\n"
-  "void Function(Class0 CheckF);\n"
-  "using namespace A::B::C;\n"
-  "void Function(MyInt CheckG);\n"
-  "void f() {\n"
-  "  struct X {} CheckH;\n"
-  "}\n"
-  "struct X;\n"
-  "void f(const ::X* CheckN) {}\n"
-  "namespace {\n"
-  "  class aClass {};\n"
-  "   aClass CheckI;\n"
-  "}\n"
-  "namespace A {\n"
-  "  struct aStruct {} CheckJ;\n"
-  "}\n"
-  "namespace {\n"
-  "  namespace D {\n"
-  "namespace {\n"
-  "  class aStruct {};\n"
-  "  aStruct CheckK;\n"
-  "}\n"
-  "  }\n"
-  "}\n"
-  "template struct Foo {\n"
-  "  typedef typename T::A dependent_type;\n"
-  "  typedef int non_dependent_type;\n"
-  "  dependent_type dependent_type_var;\n"
-  "  non_dependent_type non_dependent_type_var;\n"
-  "};\n"
-  "struct X { typedef int A; };"
-  "Foo var;"
-  "void F() {\n"
-  "  var.dependent_type_var = 0;\n"
-  "var.non_dependent_type_var = 0;\n"
-  "}\n"
-  "class EnumScopeClass {\n"
-  "public:\n"
-  "  enum AnEnum { ZERO, ONE };\n"
-  "};\n"
-  "EnumScopeClass::AnEnum AnEnumVar;\n",
-  TypeNameVisitor::Lang_CXX11
-);
+  R"(int CheckInt;
+ template 
+ class OuterTemplateClass { };
+ namespace A {
+  namespace B {
+class Class0 { };
+namespace C {
+  typedef int MyInt;
+ 

[PATCH] D36610: [Tooling] Add option to getFullyQualifiedName using a custom PritingPolicy

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

Should I update the other tests in QualTypeNamesTest.cpp to use multiline 
strings as well?


https://reviews.llvm.org/D36610



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D36610: [Tooling] Add option to getFullyQualifiedName using a custom PritingPolicy

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho created this revision.
Herald added a subscriber: klimek.

In our user case, we need to generate unique names for every tag, including 
anonymous structs/unions.

This adds a custom PrintingPolicy option to getFullyQualifiedName and the test 
case shows that different names are generated for different anonymous 
unions/structs.


https://reviews.llvm.org/D36610

Files:
  include/clang/Tooling/Core/QualTypeNames.h
  lib/Tooling/Core/QualTypeNames.cpp
  unittests/Tooling/QualTypeNamesTest.cpp

Index: unittests/Tooling/QualTypeNamesTest.cpp
===
--- unittests/Tooling/QualTypeNamesTest.cpp
+++ unittests/Tooling/QualTypeNamesTest.cpp
@@ -15,6 +15,7 @@
 struct TypeNameVisitor : TestVisitor {
   llvm::StringMap ExpectedQualTypeNames;
   bool WithGlobalNsPrefix = false;
+  bool CustomPrintingPolicy = false;
 
   // ValueDecls are the least-derived decl with both a qualtype and a
   // name.
@@ -26,9 +27,22 @@
 std::string ExpectedName =
 ExpectedQualTypeNames.lookup(VD->getNameAsString());
 if (ExpectedName != "") {
-  std::string ActualName =
-  TypeName::getFullyQualifiedName(VD->getType(), *Context,
-  WithGlobalNsPrefix);
+  std::string ActualName;
+  if (!CustomPrintingPolicy)
+ActualName =
+TypeName::getFullyQualifiedName(VD->getType(), *Context,
+WithGlobalNsPrefix);
+  else {
+PrintingPolicy Policy(Context->getPrintingPolicy());
+Policy.SuppressScope = false;
+Policy.AnonymousTagLocations = true;
+Policy.PolishForDeclaration = true;
+Policy.SuppressUnwrittenScope = true;
+ActualName =
+TypeName::getFullyQualifiedName(VD->getType(), *Context,
+Policy, WithGlobalNsPrefix);
+  }
+
   if (ExpectedName != ActualName) {
 // A custom message makes it much easier to see what declaration
 // failed compared to EXPECT_EQ.
@@ -217,6 +231,32 @@
   "  }\n"
   "}\n"
   );
+
+  TypeNameVisitor PrintingPolicy;
+  PrintingPolicy.CustomPrintingPolicy = true;
+  PrintingPolicy.ExpectedQualTypeNames["a"] = "short";
+  PrintingPolicy.ExpectedQualTypeNames["un_in_st_1"] =
+  "union (anonymous struct at input.cc:1:1)::(anonymous union at "
+  "input.cc:3:3)";
+  PrintingPolicy.ExpectedQualTypeNames["b"] = "short";
+  PrintingPolicy.ExpectedQualTypeNames["un_in_st_2"] =
+  "union (anonymous struct at input.cc:1:1)::(anonymous union at "
+  "input.cc:7:3)";
+  PrintingPolicy.ExpectedQualTypeNames["anon_st"] =
+  "struct (anonymous struct at input.cc:1:1)";
+  PrintingPolicy.runOver(
+  "struct\n"
+  "{\n"
+  "  union\n"
+  "  {\n"
+  "short a;\n"
+  "  } un_in_st_1;\n"
+  "  union\n"
+  "  {\n"
+  "short b;\n"
+  "  } un_in_st_2;\n"
+  "} anon_st;\n"
+  );
 }
 
 }  // end anonymous namespace
Index: lib/Tooling/Core/QualTypeNames.cpp
===
--- lib/Tooling/Core/QualTypeNames.cpp
+++ lib/Tooling/Core/QualTypeNames.cpp
@@ -463,14 +463,21 @@
 
 std::string getFullyQualifiedName(QualType QT,
   const ASTContext ,
+  const PrintingPolicy ,
+  bool WithGlobalNsPrefix) {
+  QualType FQQT = getFullyQualifiedType(QT, Ctx, WithGlobalNsPrefix);
+  return FQQT.getAsString(Policy);
+}
+
+std::string getFullyQualifiedName(QualType QT,
+  const ASTContext ,
   bool WithGlobalNsPrefix) {
   PrintingPolicy Policy(Ctx.getPrintingPolicy());
   Policy.SuppressScope = false;
   Policy.AnonymousTagLocations = false;
   Policy.PolishForDeclaration = true;
   Policy.SuppressUnwrittenScope = true;
-  QualType FQQT = getFullyQualifiedType(QT, Ctx, WithGlobalNsPrefix);
-  return FQQT.getAsString(Policy);
+  return getFullyQualifiedName(QT, Ctx, Policy, WithGlobalNsPrefix);
 }
 
 }  // end namespace TypeName
Index: include/clang/Tooling/Core/QualTypeNames.h
===
--- include/clang/Tooling/Core/QualTypeNames.h
+++ include/clang/Tooling/Core/QualTypeNames.h
@@ -74,6 +74,11 @@
 std::string getFullyQualifiedName(QualType QT,
   const ASTContext ,
   bool WithGlobalNsPrefix = false);
+
+std::string getFullyQualifiedName(QualType QT,
+  const ASTContext ,
+  const PrintingPolicy ,
+  bool WithGlobalNsPrefix = false);
 }  // end namespace TypeName
 }  // end namespace clang
 #endif  // LLVM_CLANG_TOOLING_CORE_QUALTYPENAMES_H
___
cfe-commits mailing list