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

ddcc added a comment. FYI the fix for the 1-bit APSInt issue is in https://reviews.llvm.org/D35450#change-ifYnQ3IlVso https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/list

[PATCH] D33308: [analyzer]: Improve test handling with multiple constraint managers

ddcc added a comment. @dcoughlin @zaks.anna @NoQ @xazax.hun Ping, I'd appreciate it if I could get a review for this (https://reviews.llvm.org/D33308), https://reviews.llvm.org/D28955, https://reviews.llvm.org/D28953, and https://reviews.llvm.org/D28954. Rebasing and fixing up these commits is

[PATCH] D33308: [analyzer]: Improve test handling with multiple constraint managers

This revision was automatically updated to reflect the committed changes. Closed by commit rL305480: [analyzer]: Improve test handling with multiple constraint managers (authored by ddcc). Changed prior to commit: https://reviews.llvm.org/D33308?vs=99394&id=102682#toc Repository: rL LLVM ht

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

ddcc added inline comments. Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:356 QualType ResultTy) { - if (!State->isTainted(RHS) && !State->isTainted(LHS)) -return UnknownVal(); zaks.anna wrote: > I am concerned that

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

ddcc added a comment. > Can we drop computing these for some expressions that we know the > RangeConstraintManager will not utilize? It's possible, though I'm not sure what the actual limitations of the RangeConstraintManager are, since there are a lot of intermediate steps that attempt to tra

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

ddcc updated this revision to Diff 103239. ddcc added a comment. Rebase, decrease simplification complexity https://reviews.llvm.org/D28953 Files: include/clang/StaticAnalyzer/Checkers/SValExplainer.h lib/StaticAnalyzer/Core/SValBuilder.cpp lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

ddcc added a comment. I forgot to mention that the only remaining test failure is on `plist-macros.cpp`; there is a `Assuming condition is true` path note that only appears with the RangeConstraintManager but not with Z3ConstraintManager, and I can't `#ifdef` it because the annotations are chec

[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

ddcc added a comment. In https://reviews.llvm.org/D35450#1116535, @george.karpenkov wrote: > @ddcc Hi, are you still interested in landing the fixes associated with this > patch? I can take a look as I'm currently reviewing > https://reviews.llvm.org/D45517, but it is likely that the patch woul

[PATCH] D47603: [analyzer] fix bug with 1-bit APSInt types in Z3ConstraintManager

ddcc created this revision. ddcc added reviewers: george.karpenkov, NoQ. Herald added subscribers: a.sidorin, szepet, xazax.hun. Clang does not have a corresponding QualType for a 1-bit APSInt, so use the BoolTy and extend the APSInt. Split from https://reviews.llvm.org/D35450. Repository: rC

[PATCH] D47603: [analyzer] fix bug with 1-bit APSInt types in Z3ConstraintManager

ddcc added a comment. In https://reviews.llvm.org/D47603#1118138, @vlad.tsyrklevich wrote: > In https://reviews.llvm.org/D47603#1118106, @george.karpenkov wrote: > > > Would it be possible to add tests? I know we have very few unit tests, but > > I assume you could actually use an integration te

[PATCH] D47603: [analyzer] fix bug with 1-bit APSInt types in Z3ConstraintManager

ddcc updated this revision to Diff 149356. ddcc added a comment. Add test, address comments Repository: rC Clang https://reviews.llvm.org/D47603 Files: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp test/Analysis/apsint.c Index: test/Analysis/apsint.c ==

[PATCH] D47603: [analyzer] fix bug with 1-bit APSInt types in Z3ConstraintManager

This revision was automatically updated to reflect the committed changes. Closed by commit rL333704: [analyzer] fix bug with 1-bit APSInt types in Z3ConstraintManager (authored by ddcc, committed by ). Herald added a subscriber: llvm-commits. Repository: rL LLVM https://reviews.llvm.org/D47603

[PATCH] D47617: [Analyzer] Fix Z3ConstraintManager crash (PR37646)

ddcc added a comment. In https://reviews.llvm.org/D47617#1119257, @george.karpenkov wrote: > LGTM with a nit on a test name. Same. In https://reviews.llvm.org/D47617#1119268, @NoQ wrote: > Also does this test need to be z3-specific? We would also not like to crash > here without z3. I had

[PATCH] D47726: [Analyzer][Z3] Test fixes for Z3 constraint manager

ddcc added a subscriber: dcoughlin. ddcc added a comment. In https://reviews.llvm.org/D47726#1121395, @george.karpenkov wrote: > - Do all tests for Z3 run when LLVM is configured to use Z3? I'm not sure if > that's the right thing: do all tests start to take 10x time to run once Z3 is > enabled

[PATCH] D47726: [Analyzer][Z3] Test fixes for Z3 constraint manager

ddcc added a comment. > @ddcc To be completely honest, I see a few design issues with the current > implementation of Z3 backend, > the main one being that it checks satisfiability after every single exploded > node. > To the best of my knowledge, reasonable scalability would not be achieved

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. 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 ve

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. 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 CM

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. In D54978#1431430 , @mikhail.ramalho wrote: > 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. Sounds like this mi

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. In D54978#1431935 , @delcypher wrote: > Would one of you be able to file a bug against Z3 to fix this? I am no longer > in a position to contribute to Z3 so I can't do this. I've opened https://github.com/Z3Prover/z3/issues/2184 .

[PATCH] D54978: Move the SMT API to LLVM

ddcc added inline comments. Comment at: llvm/cmake/modules/FindZ3.cmake:92 + + set(Z3_VERSION_STRING ${Z3_MAJOR}.${Z3_MINOR}.${Z3_MAJOR}) + unset(z3_version_str) Should be ${Z3_MAJOR}.${Z3_MINOR}.${Z3_BUILD_NUMBER} CHANGES SINCE LAST ACTION https://reviews.

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. In D54978#1433646 , @mikhail.ramalho wrote: > 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

[PATCH] D54978: Move the SMT API to LLVM

ddcc added subscribers: delcypher, ddcc. ddcc added a comment. The likely reason for this versioning problem is that the current versioning implementation in FindZ3.cmake is best-effort only: among other conditions, if the z3 binary is available, it will execute it and parse out the version numb

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. In D54978#1395268 , @brzycki wrote: > I think I found why others are struggling to recreate this issue. I did not > have the package `z3/bionic` installed. This provides the `/usr/bin/z3` > executable which `llvm/cmake/modules/FindZ

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. In D54978#1395425 , @brzycki wrote: > This works for everything I could throw at it. If you think it's reasonable I > can open another ticket and have the code reviewed as a separate fix. Sounds good to me, although I think it'd be

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. In D54978#1396403 , @brzycki wrote: > That is almost exactly what I was thinking about this morning. I'd prefer the > following since it's more robust for older versions: The old `version.h` header isn't externally exposed, only th

[PATCH] D54978: Move the SMT API to LLVM

ddcc added a comment. In D54978#1397316 , @mikhail.ramalho wrote: > I just sent the first prototype of the solution. All the magic happens inside > the `CHECK_CXX_SOURCE_RUNS` call. I think hardcoding the version into the binary is too brittle. Instead

[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

ddcc added inline comments. Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:364 if (symLHS && symRHS && - (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp) + (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp) return

[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

ddcc added inline comments. Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:364 if (symLHS && symRHS && - (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp) + (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp) return

[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

ddcc updated this revision to Diff 113505. ddcc added a comment. Rebase, make complexity limits configurable https://reviews.llvm.org/D35450 Files: include/clang/AST/Expr.h include/clang/Config/config.h.cmake include/clang/StaticAnalyzer/Checkers/SValExplainer.h include/clang/StaticAnal

[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

ddcc marked 5 inline comments as done. ddcc added a comment. All testcases pass, except the issue with `range_casts.c`. The cause is still the range intersection discussed in https://reviews.llvm.org/D35450#810469. https://reviews.llvm.org/D35450 _

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

ddcc updated this revision to Diff 113619. ddcc added a comment. Rebase, factor out floating-point changes, fix Z3 type bug, support general APSInt comparison https://reviews.llvm.org/D28955 Files: include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h include/clang/StaticAnal

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

ddcc added a comment. @dcoughlin No, all three patches are separate. I have been testing them with each applied incrementally onto the previous, with the order trunk, https://reviews.llvm.org/D35450, https://reviews.llvm.org/D28954, then https://reviews.llvm.org/D28955 (this). But since these a

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

ddcc added a comment. @NoQ Does the proposal in https://reviews.llvm.org/D28955#652465 satisfy your concern? https://reviews.llvm.org/D28955 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-

[PATCH] D77705: [Driver] Forward pass plugin arguments to gold

ddcc created this revision. ddcc added a reviewer: tejohnson. Herald added a project: clang. Support forwarding `-fplugin` and `-fpass-plugin` arguments for loading pass plugins Depends on: D77704 Repository: rG LLVM Github Monorepo https://reviews.llvm.org

[PATCH] D77705: [Driver] Forward pass plugin arguments to gold

ddcc added a comment. Originally, I tried forwarding the `-Xclang -load` arguments, but couldn't access the `options::OPT_plugin` arguments from the argument list. I'm not familiar with tablegen and argument processing, there was some issue with the group not being available causing the argumen

[PATCH] D77704: [gold] Add support for loading pass plugins

ddcc marked an inline comment as done. ddcc added a comment. Thanks, seems to be working now for statically-built passes on a default LLVM build without `LLVM_LINK_LLVM_DYLIB`. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D77704/new/ https://revie

[PATCH] D77704: [gold] Add support for loading pass plugins

ddcc updated this revision to Diff 259981. ddcc added a comment. Herald added a project: clang. Herald added a subscriber: cfe-commits. Support statically-built passes Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D77704/new/ https://reviews.llvm.or

[PATCH] D77704: [gold] Add support for loading pass plugins

ddcc added a comment. In order to reload the gold plugin, I'm modifying the Clang driver to pass in our own path as a separate argument, which is the most generic approach. Another method would be to use e.g. `dladdr()` to grab our own path from one of our exported functions, but that method ap

[PATCH] D77704: [gold] Add support for loading pass plugins

ddcc added a comment. ping, any feedback? Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D77704/new/ https://reviews.llvm.org/D77704 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.

[PATCH] D132003: [clang][ARM][NFC] Clean up signed conversion and undefined macros in builtin header

ddcc updated this revision to Diff 458581. ddcc marked an inline comment as done. ddcc added a comment. Fix typo in __revsh Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D132003/new/ https://reviews.llvm.org/D132003 Files: clang/lib/Headers/arm_a

[PATCH] D132003: [clang][ARM][NFC] Clean up signed conversion and undefined macros in builtin header

ddcc added a comment. Yup, thanks! Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D132003/new/ https://reviews.llvm.org/D132003 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.or

[PATCH] D132003: [clang][ARM][NFC] Clean up signed conversion and undefined macros in builtin header

This revision was landed with ongoing or failed builds. This revision was automatically updated to reflect the committed changes. Closed by commit rGac77b3fde120: [clang][ARM][NFC] Clean up signed conversion and undefined macros in builtin… (authored by ddcc). Repository: rG LLVM Github Monorep

[PATCH] D130800: [clang][Headers] Avoid compiler warnings in builtin headers

ddcc created this revision. ddcc added reviewers: efriedma, rnk, aaron.ballman. Herald added a project: All. ddcc requested review of this revision. Herald added a project: clang. While debugging module support using -Wsystem-headers, we discovered that if -Werror, and -Wundef or -Wmacro-redefined

[PATCH] D130800: [clang][Headers] Avoid compiler warnings in builtin headers

ddcc updated this revision to Diff 449118. ddcc added a comment. Undef macros instead, handle other header files Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D130800/new/ https://reviews.llvm.org/D130800 Files: clang/lib/Headers/__clang_cuda_bui

[PATCH] D130800: [clang][Headers] Avoid compiler warnings in builtin headers

ddcc added inline comments. Comment at: clang/lib/Headers/__clang_cuda_builtin_vars.h:37 -#if __cplusplus >= 201103L +#if defined(__cplusplus) && __cplusplus >= 201103L #define __DELETE =delete tra wrote: > Are there actual use cases where CUDA headers are use

[PATCH] D130800: [clang][Headers] Avoid compiler warnings in builtin headers

ddcc updated this revision to Diff 449403. ddcc added a comment. Error out on undef __cplusplus in CUDA headers Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D130800/new/ https://reviews.llvm.org/D130800 Files: clang/lib/Headers/__clang_cuda_buil

[PATCH] D130800: [clang][Headers] Avoid compiler warnings in builtin headers

ddcc added inline comments. Comment at: clang/lib/Headers/__clang_hip_cmath.h:381 // decltype is only available in C++11 and above. -#if __cplusplus >= 201103L +#if defined(__cplusplus) && __cplusplus >= 201103L // __hip_promote tra wrote: > HIP headers are als

[PATCH] D130800: [clang][Headers] Avoid compiler warnings in builtin headers

ddcc updated this revision to Diff 449458. ddcc added a comment. Drop changes to CUDA/HIP/OpenMP headers Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D130800/new/ https://reviews.llvm.org/D130800 Files: clang/lib/Headers/float.h clang/lib/Head

[PATCH] D130800: [clang][Headers] Avoid compiler warnings in builtin headers

ddcc added inline comments. Comment at: clang/lib/Headers/stdint.h:99-100 typedef __UINT64_TYPE__ uint64_t; +# undef __int_least64_t # define __int_least64_t int64_t +# undef __uint_least64_t iana wrote: > iana wrote: > > What are you seeing that's defining `__

[PATCH] D130800: [clang][Headers] Avoid compiler warnings in builtin headers

This revision was landed with ongoing or failed builds. This revision was automatically updated to reflect the committed changes. Closed by commit rGbbf19005714b: [clang][Headers] Avoid compiler warnings in builtin headers (authored by ddcc). Changed prior to commit: https://reviews.llvm.org/D1

[PATCH] D131213: [clang][Headers] Fix unintentional error in D130800

ddcc created this revision. ddcc added reviewers: aaron.ballman, iana. Herald added a project: All. ddcc requested review of this revision. Herald added a project: clang. Undefined macros evaluate to zero, so when checking for a smaller value, we need to include the case when the macro is undefine

[PATCH] D131213: [clang][Headers] Fix unintentional error in D130800

ddcc added a comment. I missed line 19, yeah that makes sense. @iana is that ok with you? Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D131213/new/ https://reviews.llvm.org/D131213 ___ cfe-commits mailin

[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

ddcc added a comment. @NoQ ping https://reviews.llvm.org/D35450 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D88349: Fix inconsistent flag for disabling Dead Virtual Function Elimination

ddcc created this revision. ddcc added a reviewer: ostannard. Herald added a subscriber: dang. Herald added a project: clang. ddcc requested review of this revision. Repository: rG LLVM Github Monorepo https://reviews.llvm.org/D88349 Files: clang/include/clang/Driver/Options.td Index: clan

[PATCH] D88349: Fix inconsistent flag for disabling Dead Virtual Function Elimination

ddcc added a comment. ping Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D88349/new/ https://reviews.llvm.org/D88349 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/

[PATCH] D88349: Fix inconsistent flag for disabling Dead Virtual Function Elimination

ddcc updated this revision to Diff 296782. ddcc added a comment. Add test Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D88349/new/ https://reviews.llvm.org/D88349 Files: clang/include/clang/Driver/Options.td clang/test/CodeGenCXX/virtual-funct

[PATCH] D88349: Fix inconsistent flag for disabling Dead Virtual Function Elimination

ddcc updated this revision to Diff 296826. ddcc added a comment. Update tests Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D88349/new/ https://reviews.llvm.org/D88349 Files: clang/test/CodeGenCXX/virtual-function-elimination.cpp Index: clang/t

[PATCH] D88349: Fix inconsistent flag for disabling Dead Virtual Function Elimination

ddcc added a comment. Hmm, looks like this was already fixed by e5158b52730d323bb8cd2cba6dc6c89b90cba452 . I guess I'll just commit the test then? Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://re

[PATCH] D88349: Fix inconsistent flag for disabling Dead Virtual Function Elimination

This revision was landed with ongoing or failed builds. This revision was automatically updated to reflect the committed changes. Closed by commit rGc10248829357: Add test for disabling Dead Virtual Function Elimination (authored by ddcc). Repository: rG LLVM Github Monorepo CHANGES SINCE LAST

[PATCH] D132003: [clang][ARM][NFC] Clean up signed conversion and undefined macros in builtin header

ddcc created this revision. ddcc added reviewers: tmatheson, javed.absar, SjoerdMeijer. Herald added a subscriber: kristof.beyls. Herald added a project: All. ddcc requested review of this revision. Herald added a project: clang. These warnings were identified while debugging modules with Wsystem-

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

ddcc added a comment. I don't have the time to rebase and retest this currently, so it might be better for someone else to take over this patch. Unfortunately, it's been long enough that I don't remember the details of these changes. CHANGES SINCE LAST ACTION https://reviews.llvm.org/D28955/

[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

ddcc added inline comments. Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:60 +// Set timeout to 15000ms = 15s +Z3_set_param_value(Config, "timeout", "15000"); + } xazax.hun wrote: > Sorry for being a bit late in the party, I was wondering w

[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

ddcc updated this revision to Diff 93587. ddcc marked 4 inline comments as done. ddcc added a comment. Use direct bitcasting instead of string conversion for APFloat casting, add reference counting for Z3_sort, eliminate some duplicate code https://reviews.llvm.org/D28952 Files: CMakeLists.t

[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

ddcc added a comment. Thanks for the feedback! My main constraint is that the results from the floating-point analysis weren't very interesting (see #652894 <#652894>), so I'm not actively working on further development. > FYI I've been working on floating point support in KLEE and have extende

[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

ddcc updated this revision to Diff 93588. ddcc added a comment. Fix erroneous comment https://reviews.llvm.org/D28952 Files: CMakeLists.txt cmake/modules/FindZ3.cmake include/clang/Config/config.h.cmake include/clang/StaticAnalyzer/Core/Analyses.def include/clang/StaticAnalyzer/Core/P

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

ddcc updated this revision to Diff 93589. ddcc added a comment. Rebase https://reviews.llvm.org/D28953 Files: include/clang/StaticAnalyzer/Checkers/SValExplainer.h lib/StaticAnalyzer/Core/SValBuilder.cpp lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp test/Analysis/bitwise-ops.c test/An

[PATCH] D28954: [analyzer] Add support for symbolic float expressions

ddcc updated this revision to Diff 93590. ddcc added a comment. Rebase, update tests, fix bugs https://reviews.llvm.org/D28954 Files: include/clang/StaticAnalyzer/Checkers/Checkers.td include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h include/clang/StaticAnalyzer/Core/Pat

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

ddcc updated this revision to Diff 93591. ddcc added a comment. Rebase https://reviews.llvm.org/D28955 Files: include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h lib/StaticAnalyzer/Checkers/BoolAssignmentChecker

[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

ddcc added inline comments. Comment at: cmake/modules/FindZ3.cmake:3 +# in the find_path() and find_library() calls +find_package(PkgConfig QUIET) +PKG_CHECK_MODULES(PC_Z3 QUIET libz3) delcypher wrote: > @ddcc Seeing as you don't want to use the new upstream Z3 C

[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

ddcc updated this revision to Diff 93974. ddcc added a comment. Fix support for 128-bit APInt creation, drop pkg-config from CMake module https://reviews.llvm.org/D28952 Files: CMakeLists.txt cmake/modules/FindZ3.cmake include/clang/Config/config.h.cmake include/clang/StaticAnalyzer/Cor

[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

This revision was automatically updated to reflect the committed changes. Closed by commit rL299463: [analyzer] Add new Z3 constraint manager backend (authored by ddcc). Changed prior to commit: https://reviews.llvm.org/D28952?vs=93974&id=94107#toc Repository: rL LLVM https://reviews.llvm.o

[PATCH] D31756: [cmake] Support Gentoo install for z3

ddcc accepted this revision. ddcc added a comment. This revision is now accepted and ready to land. Thanks! Repository: rL LLVM https://reviews.llvm.org/D31756 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/

[PATCH] D26061: [analyzer] Refactor and simplify SimpleConstraintManager

ddcc updated this revision to Diff 85136. ddcc added a comment. Rebase https://reviews.llvm.org/D26061 Files: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h lib/StaticAnalyzer/Core/CMakeLists.tx

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

ddcc updated this revision to Diff 85139. ddcc added a comment. Fix rebase https://reviews.llvm.org/D28953 Files: include/clang/StaticAnalyzer/Checkers/SValExplainer.h lib/StaticAnalyzer/Core/SValBuilder.cpp lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp test/Analysis/bitwise-ops.c tes

[PATCH] D28954: [analyzer] Add support for symbolic float expressions

ddcc created this revision. Herald added a subscriber: mgorny. With the Z3 constraint manager, symbolic floating-point constraints can also be reasoned about. This commit includes a basic floating-point checker for domain errors with math functions. https://reviews.llvm.org/D28954 Files: in

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

ddcc created this revision. With the Z3 constraint manager, symbolic extension and truncation of variables can be fully reasoned about. https://reviews.llvm.org/D28955 Files: include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h include/clang/StaticAnalyzer/Core/PathSensitive

[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

ddcc added a comment. This is a fairly large patch, but the core of it is the actual implementation of the Z3 constraint solver backend. In its current form, the backend is implemented as a Clang plugin, but I also have a git commit that has it inside the static analyzer. The non-plugin approa

[PATCH] D28954: [analyzer] Add support for symbolic float expressions

ddcc added a comment. - This patch introduces a virtual overloaded `llvm::APFloat getSymVal()` for returning the value of known floating-point constants. In the long term, both `getSymVal()` functions should probably be refactored to return something like a `llvm::Con - There are also long-term

[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

ddcc added a comment. Do you want me to replace this version of the patch with one that omits the test case changes? The underlying git commit for just the Z3 constraint manager implementation is https://github.com/ddcc/clang/commit/e1414d300882c1459f461424d3e89d1613ecf03c , and https://githu

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

ddcc added a comment. When I was testing this patch, it was on top of both https://reviews.llvm.org/D28952 and https://reviews.llvm.org/D28953. For `malloc.c`, the change on line 1708 from `int` to `size_t` is necessary to prevent a false positive warning at line 1710. The other three changes d

[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

ddcc added a comment. > For such test cases i'd consider something like this: > > // RUN: ... -analyzer-constraints=range -DRANGE ... > // RUN: ... -analyzer-constraints=z3 ... > > #ifdef RANGE > foo(); // expected-warning{{}} > #else > foo(); // no-warning > #endif Would this b

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

ddcc added a comment. > We should have expected-warning on 64-bit targets (where `size_t` easily > overflows `int`) and no-warning on 32-bit targets (where they are of the same > size and the fix for the original issue > https://llvm.org/bugs/show_bug.cgi?id=16558 applies). I think we should ha

[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

ddcc updated this revision to Diff 85313. ddcc added a comment. Convert to plugin, add move/assignment constructor, avoid Z3_simplify(), use Z3_mk_simple_solver(), generate logical and of all constraints in solver https://reviews.llvm.org/D28952 Files: CMakeLists.txt cmake/modules/FindZ3.c

[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

ddcc added a comment. I'd like to note that one of the main challenges with this implementation was needing to perform type reinference and implicit casting within the constraint manager, since the constraints are sometimes implicit. (e.g. `(int) x` instead of `x == 0`). It also didn't help tha

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

ddcc updated this revision to Diff 85314. ddcc added a comment. Rebase https://reviews.llvm.org/D28953 Files: include/clang/StaticAnalyzer/Checkers/SValExplainer.h lib/StaticAnalyzer/Core/SValBuilder.cpp lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp test/Analysis/bitwise-ops.c test/An

[PATCH] D28954: [analyzer] Add support for symbolic float expressions

ddcc updated this revision to Diff 85315. ddcc added a comment. Rebase https://reviews.llvm.org/D28954 Files: include/clang/StaticAnalyzer/Checkers/Checkers.td include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintMan

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

ddcc updated this revision to Diff 85316. ddcc added a comment. Rebase https://reviews.llvm.org/D28955 Files: include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h lib/StaticAnalyzer/Checkers/BoolAssignmentChecker

[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

ddcc added a comment. > - That said, I think there are still significant optimization opportunities. > It looks like when performing a query you create a new solver for each set of > constraints. My understanding (and perhaps @nlopes can correct me here) is > that these days Z3 is quite good at

[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

ddcc updated this revision to Diff 85621. ddcc added a comment. Add CMake CLANG_BUILD_Z3 option, add Z3Model and Z3Solver classes, reuse solver in checkNull() and getSymVal() https://reviews.llvm.org/D28952 Files: CMakeLists.txt cmake/modules/FindZ3.cmake include/clang/Config/config.h.cm

[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

ddcc added a comment. > Regarding incremental solving with Z3 (or with most SMT solvers in general), > let me just lower the expectations a bit: Ok, that is good to know. It seems that the performance benefits of incremental solving are unclear, and would be nontrivial to implement (maybe stor

[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

ddcc added a comment. In https://reviews.llvm.org/D28952#659728, @nlopes wrote: > Let me give just 2 more Z3-related suggestions: > > - instead of re-creating the solver, it might be faster to do Z3_solver_reset > - "once in a while" it might be helpful to delete everything (all solvers, > asts,

[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

ddcc added a comment. I added support for a callback field in lit's configuration (see https://reviews.llvm.org/D29684), which is used to execute each testcase for each supported constraint solver backends at runtime. I believe this resolves all remaining issues, except for the remaining two te

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

ddcc added a comment. ping https://reviews.llvm.org/D28953 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

ddcc updated this revision to Diff 105913. ddcc marked an inline comment as done. ddcc added a comment. Drop duplicate code https://reviews.llvm.org/D28953 Files: include/clang/StaticAnalyzer/Checkers/SValExplainer.h lib/StaticAnalyzer/Core/SValBuilder.cpp lib/StaticAnalyzer/Core/SimpleSV

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

ddcc added a comment. I tested the following software, both before and after applying this patch, using RangeConstraintManager. Software, Version, Compile Time (before), Bugs Reported (before), Compile Time (after), Bugs Reported (after) openssl, 1.1.0f, 11 min, 126, 12 min, 126 sqlite, 3.18.2,

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

ddcc added a comment. I've also uploaded the results to https://dcddcc.com/csa https://reviews.llvm.org/D28953 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

ddcc updated this revision to Diff 106084. ddcc added a comment. Split plist-macros.cpp, and update analyzer_test.py to support tests that require not z3 https://reviews.llvm.org/D28953 Files: include/clang/StaticAnalyzer/Checkers/SValExplainer.h lib/StaticAnalyzer/Core/SValBuilder.cpp l

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

This revision was automatically updated to reflect the committed changes. Closed by commit rL307833: [analyzer] Support generating and reasoning over more symbolic constraint types (authored by ddcc). Changed prior to commit: https://reviews.llvm.org/D28953?vs=106084&id=106284#toc Repository:

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

ddcc added a comment. Reverted in https://reviews.llvm.org/rL307853 Repository: rL LLVM https://reviews.llvm.org/D28953 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

ddcc added a comment. Reverted in https://reviews.llvm.org/rL307853 Repository: rL LLVM https://reviews.llvm.org/D28953 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

  1   2   >