Page MenuHomePhabricator

gou4shi1 (guangqing.chen)
User

Projects

User does not belong to any projects.

User Details

User Since
Mar 24 2019, 9:14 AM (170 w, 6 d)

Recent Activity

Apr 6 2019

gou4shi1 added a comment to D54978: Move the SMT API to LLVM.

My own out-of-tree pass #include <llvm/Support/SMTAPI.h> 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?

Apr 6 2019, 7:27 AM · Restricted Project, Restricted Project

Mar 28 2019

gou4shi1 added a comment to D54978: Move the SMT API to LLVM.

My own out-of-tree pass #include <llvm/Support/SMTAPI.h> 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.

Mar 28 2019, 6:32 PM · Restricted Project, Restricted Project

Mar 25 2019

gou4shi1 added a comment to D59796: New methods to check for under-/overflow in the SMT API.

It works, thx.

Mar 25 2019, 9:33 PM · Restricted Project
gou4shi1 accepted D59796: New methods to check for under-/overflow in the SMT API.
Mar 25 2019, 9:33 PM · Restricted Project
gou4shi1 added a comment to D54978: Move the SMT API to LLVM.

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

Mar 25 2019, 8:34 AM · Restricted Project, Restricted Project
gou4shi1 added a comment to D54978: Move the SMT API to LLVM.

! In D54978#1441417, @mikhail.ramalho wrote:
Sure, I'll create a new revision with the added functions tonight.

Mar 25 2019, 7:31 AM · Restricted Project, Restricted Project
gou4shi1 added a comment to D54978: Move the SMT API to LLVM.

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!

Mar 25 2019, 6:31 AM · Restricted Project, Restricted Project