[PATCH] D54978: Move the SMT API to LLVM

[guangqing.chen via Phabricator via cfe-commits]

gou4shi1 added a comment.

@mikhail.ramalho

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!


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

[guangqing.chen via Phabricator via cfe-commits]

gou4shi1 added a comment.

> ! 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 :)


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

[guangqing.chen via Phabricator via cfe-commits]

gou4shi1 added a comment.

> ! In D54978#1441547 , 
> @mikhail.ramalho wrote:
>  You can get the sort size by calling getBitvectorSortSize().

found, thx


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

[guangqing.chen via Phabricator via cfe-commits]

gou4shi1 added a comment.

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.


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

[guangqing.chen via Phabricator via cfe-commits]

gou4shi1 added a comment.

In D54978#1457318 , @mikhail.ramalho 
wrote:

> 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?


I build llvm with `cmake -DCMAKE_BUILD_TYPE=Debug -DLLVM_TARGETS_TO_BUILD=X86 
-DLLVM_ENABLE_PROJECTS=clang  ../llvm`
I have make a mini reproduce example at 
https://github.com/gou4shi1/mini-repro-pass
you can build this example with `mkdir build && cd build && cmake 
-DCMAKE_BUILD_TYPE=Debug .. && make`
you can run this example with `opt -load-pass-plugin=t/t.so 
-passes="t" ../test/add100.ll`


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