Integrate CVC4 - Githubissues

anithag commented 9 years ago

I have built metasmt with CVC4 and Z3 (only). The build suceeded. Now I am trying to build klee with this metaSMT. I have made few changes to make sure CVC4 backend is accepted. I get build error. Relevant change and error is shown below:

@@ -314,6 +315,10 @@ Executor::Executor(const InterpreterOptions &opts, backend = "Z3"; coreSolver = new MetaSMTSolver< DirectSolver_Context < Z3_Backend > > (UseForkedCoreSolver, CoreSolverOptimizeDivides); break;

case METASMT_BACKEND_CVC4:
backend = "CVC4";
coreSolver = new MetaSMTSolver< DirectSolver_Context < CVC4 > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
break; case METASMT_BACKEND_BOOLECTOR: backend = "Boolector";

This is giving me following compilation error. Any idea why? Note that METASMT_BACKEND_CVC4 is recognised and I have included CVC4.hpp in Executor.cpp. CVC4 is getting recognized but still is giving template 1 is invalid. Most of the code follows Z3_Backend.

Executor.cpp: In constructor ‘klee::Executor::Executor(const klee::Interpreter::InterpreterOptions&, klee::InterpreterHandler*)’: Executor.cpp:320:75: error: template argument 1 is invalid coreSolver = new MetaSMTSolver< DirectSolver_Context < CVC4 > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); ^ Executor.cpp:320:77: error: template argument 1 is invalid coreSolver = new MetaSMTSolver< DirectSolver_Context < CVC4 > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);

anithag commented 9 years ago

I should add that below errors preceed the above errors (I missed these earlier as I was using make -j2)

/home/anitha/kleestr/metasmt/build/root/include/metaSMT/backend/CVC4.hpp:229:51: error: template argument 1 is invalid mpl::pair<predtags::and_tag, Op2 > /home/anitha/kleestr/metasmt/build/root/include/metaSMT/backend/CVC4.hpp:229:53: error: template argument 2 is invalid mpl::pair<predtags::and_tag, Op2 > ^ /home/anitha/kleestr/metasmt/build/root/include/metaSMT/backend/CVC4.hpp:230:54: error: template argument 1 is invalid , mpl::pair<predtags::nand_tag, NotOp2 > ^

finnhaedicke commented 9 years ago

Hi @anithag,

The error in your first post could be cause by the error in the second. Can you provide some more information to help debugging?

Can you post a gist of the complete complete compile output of make -j1?
Can you extract parts of the mpl::map in CVC4.hpp:229 to see which part of the template argument is invalid? Please place this block in the same method above the map and see if new compile erros are generated:

bool x1 = (AND == AND);

typedef Op2<AND> Op2And;
Op2And * x2 = NULL;

typedef mpl::pair<predtags::and_tag, Op2And> AndPair;
AndPair * x3 = NULL;

This might be unrelated: Are you using the current git version of Klee? I could not find "Executor.cpp". I found metaSMT related code in https://github.com/klee/klee/blob/master/lib/Solver/Solver.cpp.

anithag commented 9 years ago

I haven't used gist before. But assuming we create public gists and then share the link(Is this the way to work with gists?), this is the link containing my patch and make logs.

https://gist.github.com/anithag/09f50c553513c77c8146

anithag commented 9 years ago

@finnhaedicke

This might be unrelated: Are you using the current git version of Klee? I could not find "Executor.cpp". I found metaSMT related code in https://github.com/klee/klee/blob/master/lib/Solver/Solver.cpp.

Yes. Executor.cpp is present under lib/Core

anithag commented 9 years ago

@finnhaedicke

Can you extract parts of the mpl::map in CVC4.hpp:229 to see which part of the template argument is invalid?

I am not sure I understand this completely. From the error messages, it appears that compiler is complaining about both arguments (template argument 1 and template argument 2 are invalid). Let me know if you want me to further ivestigate this issue. I'll be happy to report.

Please place this block in the same method above the map and see if new compile erros are generated

2 new errors got generated. Pasted below. (markdown would not display <> without escapes :( )

In file included from Solver.cpp:55:0: /home/anitha/kleestr/metasmt/build/root/include/metaSMT/backend/CVC4.hpp:228:16: error: template argument 1 is invalid typedef Op2 Op2And; ^ /home/anitha/kleestr/metasmt/build/root/include/metaSMT/backend/CVC4.hpp:228:24: error: invalid type in declaration before ‘;’ token typedef Op2 Op2And; ^

finnhaedicke commented 9 years ago

Ah, I had not seen lib/Core/Executor.cpp... The gist works well for me. Thanks.

from your last comment, I suspect a name clash (or Macros). If there is a name clash, you can try fixing it by fully qualifying all the CVC4 opcodes (insert ::CVC4::kind::). E.g.

-          mpl::pair<predtags::and_tag,     Op2<AND> >
+          mpl::pair<predtags::and_tag,     Op2<::CVC4::kind::AND> >

If this still fails, it would be interesting to look at the preprocessed source code to check if the AND was replaced by something different. I ran git grep AND|OR|XOR on the klee source code and did not find anything, so I hope this does not apply.

anithag commented 9 years ago

@finnhaedicke

from your last comment, I suspect a name clash (or Macros). If there is a name clash, you can try fixing it by fully qualifying all the CVC4 opcodes (insert ::CVC4::kind::). E.g.

Looks true! I could move one step ahead. Will make other changes and see if build goes through.

In file included from Solver.cpp:55:0: /home/anitha/kleestr/metasmt/build/root/include/metaSMT/backend/CVC4.hpp:227:27: error: reference to ‘AND’ is ambiguous bool x1 = (AND == AND); ^ In file included from STPBuilder.h:20:0, from Solver.cpp:14: /home/anitha/kleestr/stp-r940/install/include/stp/c_interface.h:392:7: note: candidates are: exprkind_t AND AND, ^ In file included from /home/anitha/kleestr/metasmt/deps/cvc4-1.4/include/cvc4/expr/expr.h:57:0, from /home/anitha/kleestr/metasmt/deps/cvc4-1.4/include/cvc4/smt/smt_engine.h:28, from /home/anitha/kleestr/metasmt/deps/cvc4-1.4/include/cvc4/cvc4.h:21, from /home/anitha/kleestr/metasmt/build/root/include/metaSMT/backend/CVC4.hpp:6, from Solver.cpp:55: /home/anitha/kleestr/metasmt/deps/cvc4-1.4/include/cvc4/expr/kind.h:89:3: note: CVC4::kind::Kind_t AND AND, /*< logical and (N-ary) (23) / ^ In file included from Solver.cpp:55:0: /home/anitha/kleestr/metasmt/build/root/include/metaSMT/backend/CVC4.hpp:235:54: error: template argument 1 is invalid , mpl::pair<predtags::nand_tag, NotOp2 > ^

anithag commented 9 years ago

@finnhaedicke

The build proceeded past the template issues in CVC4.hpp; however I still have this error from Solver.cpp in klee code. Can you suggest what might be causing this? The header files are included properly. "CVC4" class gets recognized, but the compiler still complains of invalid argument. I tried reducing the testcase...could not reproduce the error in reduced testcase.

Updated the gist with new make log. https://gist.github.com/anithag/09f50c553513c77c8146#file-makelogafterchangestocvc4

Solver.cpp:1268:58: error: template argument 1 is invalid template class MetaSMTSolver< DirectSolver_Context < CVC4> >; ^ Solver.cpp:1268:60: error: template argument 1 is invalid template class MetaSMTSolver< DirectSolver_Context < CVC4>>;

anithag commented 9 years ago

ok. I now could successfully build klee with cvc4 using scope as below.

template class MetaSMTSolver< DirectSolver_Context < CVC4>>; <template class MetaSMTSolver< DirectSolver_Context < ::metaSMT::solver::CVC4>>;

To sanity test working of cvc4, I used the well-known example from klee/examples. And klee dies :-( I haven't debugged yet.

$klee --use-metasmt=cvc4 get_sign.o KLEE: output directory is "/home/anitha/kleestr/klee/examples/get_sign/klee-out-0" Starting MetaSMTSolver(CVC4) ... klee: /home/anitha/kleestr/metasmt/build/root/include/metaSMT/backend/CVC4.hpp:200: metaSMT::solver::CVC4::result_type metaSMT::solver::CVC4::operator()(TagT, boost::any) [with TagT = metaSMT::logic::Array::tag::array_var_tag; metaSMT::solver::CVC4::result_type = CVC4::Expr]: Assertion `false' failed. 0 klee 0x000000000108d5af 1 klee 0x000000000108db4c 2 libpthread.so.0 0x00007f3d16098c90 3 libc.so.6 0x00007f3d13332d27 gsignal + 55 4 libc.so.6 0x00007f3d13334418 abort + 328 5 libc.so.6 0x00007f3d1332bbd6 6 libc.so.6 0x00007f3d1332bc82 7 klee 0x000000000090055b std::pair<unsigned int, CVC4::Expr> std::make_pair<unsigned int, CVC4::Expr>(unsigned int, CVC4::Expr) + 0 8 klee 0x00000000008f76d3 metaSMT::DirectSolverContextmetaSMT::solver::CVC4::operator()(boost::proto::tagns::tag::terminal, metaSMT::logic::Array::tag::array_var_tag) + 305 9 klee 0x00000000008ee6ca boost::proto::context::callableeval<metaSMT::logic::Array::Array<boost::proto::exprns::basicexpr<boost::proto::tagns::tag::terminal, boost::proto::argsns_::term, 0l> > const, metaSMT::DirectSolverContextmetaSMT::solver::CVC4, 0l>::operator()(metaSMT::logic::Array::Array<boost::proto::exprns::basicexpr<boost::proto::tagns::tag::terminal, boost::proto::argsns_::term, 0l> > const&, metaSMT::DirectSolver_ContextmetaSMT::solver::CVC4&) const + 104 ...

Full Error Log: https://gist.github.com/anithag/09f50c553513c77c8146#file-cvcruntimeissue

finnhaedicke commented 9 years ago

I patched our dependency version of CVC4 last week. Can you please check you used the patched version of CVC4? There was a problem when linking CVC4 to other libraries that include Minisat (like STP). When you used the unpatched version of CVC4 remove it from the deps and deps/build directory and run bootstrap again.

anithag commented 9 years ago

@finnhaedicke

I patched our dependency version of CVC4 last week. Can you please check you used the patched version of CVC4?

I pulled the changes now. And am rebuilding metasmt.

There was a problem when linking CVC4 to other libraries that include Minisat (like STP).

It might be worth mentioning that I build only CVC4 and Z3. So I am not sure if the patched version helps. My bootstrap looks like this:

https://github.com/anithag/kleestr/blob/metasmt/metasmt/bootstrap.sh

(The "metasmt" branch is my working branch. It includes CVC4 changes discussed above + Klee modified to use CVC4)

finnhaedicke commented 9 years ago

I think it is still required, because Klee uses its own version of STP with Minisat. See https://github.com/anithag/kleestr/blob/master/stp-r940/src/sat/core/Solver.h

Node your might want to also pull the new version Z3 (zZ3-git, MIT license).

anithag commented 9 years ago

Ok. Shall update once build completes. Earlier, there was a link issue in klee w.r.t undefined reference to __gmp_init_set_si. So i just updated the klee makefile in tools/klee/makefile to use lgmp.

I am wondering if cvc4 has been used at all in metasmt. Or is this runtime issue specific to my build? I really want to get it running.

finnhaedicke commented 9 years ago

CVC4 is the latest addition in metaSMT. I added it 2 month ago and it had the Minisat problem all the time. We tested CVC4 manually be disabling all incompatible backends until we fixed the problem last week.

anithag commented 9 years ago

While building metasmt, I get this error for downloading Z3. What should I do?

calling download for Z3-git Cloning into '.'... Permission denied (publickey). fatal: Could not read from remote repository.

Please make sure you have the correct access rights and the repository exists. error: pathspec 'unstable' did not match any file(s) known to git. ERROR: download failed for Z3-git

TERMINATING building dependencies boost-1_55_0

cvc4-1.4 Z3-git failed. -- Boost version: 1.55.0 -- Found the following Boost libraries: -- iostreams -- thread -- system -- python -- metaSMT VERSION: 4 -- -- The following OPTIONAL packages have been found:

Boost , Portable C++ libraries
PythonLibs
PythonInterp

-- Configuring done -- Generating done -- Build files have been written to: /home/anitha/kleestr/metasmt/build

If I ignore this and proceed to make in "build" directory, I get this error

[ 23%] Built target metaSMT [ 30%] Built target boost_test Linking CXX executable direct_CVC4 /usr/bin/ld: CMakeFiles/direct_CVC4.dir/direct_CVC4.cpp.o: undefined reference to symbol '__gmpz_init_set_si' /usr/lib/x86_64-linux-gnu/libgmp.so.10: error adding symbols: DSO missing from command line collect2: error: ld returned 1 exit status

finnhaedicke commented 9 years ago

I copy&pasted the wrong github url for Z3. I fixed it 2 weeks ago. Please make sure your have this commit in your checkout: https://github.com/agra-uni-bremen/dependencies/commit/5e66da6f5c986c99fe1b45337bea0ed291fbe5f8

For the missing gmp when building CVC4 tests I created #24.

anithag commented 9 years ago

Got everything rebuilt with updated metaSMT. (I faced another build issue in * klee* complaining about undefined reference to __gmpz_init_set_si. Changed the makefiles to include lgmp, but otherwise everything else went fine)

However CVC4 still dumps core when invoked with "klee --use-metasmt=cvc4 get_sign.o". Any idea on how to proceed forward? (Maybe some option to klee?)

finnhaedicke commented 9 years ago

sorry, but if direct_CVC4 works (modulo timeouts), I can not help you there. I do not know the klee internals. In metaSMT I got random segfaults with the Minisat mixup. But this was fixed with the CVC4 patch.

anithag commented 9 years ago

@finnhaedicke

if direct_CVC4 works (modulo timeouts)

Can you elaborate what direct_CVC4 working means? How do I check that?

From my log, it appears that the very first step of invoking CVC4 seemed to fail. I am wondering what the assertion failure means. I'll try to debug the issue.

CVC4.hpp:200: metaSMT::solver::CVC4::result_type metaSMT::solver::CVC4::operator()(TagT, boost::any) [with TagT = metaSMT::logic::Array::tag::array_var_tag; metaSMT::solver::CVC4::result_type = CVC4::Expr]: Assertion `false' failed.

finnhaedicke commented 9 years ago

For me only 2 direct_CVC4 tests timeout and I see no other failures:

$ cd metaSMT/build
$ ctest -R direct_CVC4 -j8
...
98% tests passed, 2 tests failed out of 95

Total Test time (real) =   5.19 sec

The following tests FAILED:
    1811 - direct_CVC4/QF_BV/bvshl_all (Timeout)
    1829 - direct_CVC4/cardinality_t/test_bdd_cardinality_with_bv (Timeout)
Errors while running CTest

The assertion you reported is Helpful again. Klee is trying to build an array formula, as can be seen from the assertion (from TagT = metaSMT::logic::Array::tag::array_var_tag, though not very obvious).

CVC4.hpp:200: metaSMT::solver::CVC4::result_type metaSMT::solver::CVC4::operator()(TagT, 
boost::any) [with TagT = metaSMT::logic::Array::tag::array_var_tag; 
metaSMT::solver::CVC4::result_type = CVC4::Expr]: Assertion `false' failed.

The Problem is that I did not implement Array support in CVC4. For the same reason that we do not support Array with STP (see #4). Our test cases assume the solver supports equality of array variables, but this is not required by the SMT standard and not supported by CVC4 and STP. As I currently can not test it, I decided to not implement array support.

finnhaedicke commented 9 years ago

I created #25 to keep track of the missing Array support.

anithag commented 9 years ago

I see. Z3 works just fine with the same example. So I assumed CVC4 might also work. The limitation is probably large for me :( I can work on this if required. Can you briefly outline me the changes necessary? I am also pretty new to these SMT theories.

EDIT: Will the changes to array theory be similar to #4 but in CVC4.hpp ?

(I want to try basic string theory with metaSMT. So I am looking for a backend that already has string theory support so that I can modify metaSMT to support for strings (basic). I have a strict deadline in another 2 weeks. Apart from CVC4 and Z3, I don't think any other backend has string theory support that I can start using)

Here are direct_CVC4 results for me. 3 tests timeout.

97% tests passed, 3 tests failed out of 95

Total Test time (real) = 7.61 sec

The following tests FAILED: 560 - direct_CVC4/QF_BV/bvshl_all (Timeout) 578 - direct_CVC4/cardinality_t/test_bdd_cardinality_with_bv (Timeout) 579 - direct_CVC4/cardinality_t/test_adder_cardinality_with_bv (Timeout) Errors while running CTest

anithag commented 9 years ago

@finnhaedicke Thanks for the prompt responses. :-)

anithag commented 9 years ago

Let me paraphrase in one-line if I got the issue right:

Official CVC4 supports theory of arrays but the CVC4 backend in metaSMT does not.

finnhaedicke commented 9 years ago

Array support is just implementing 3 operator() overloads. One for new Array variable (Array of bitvectors), one for read and one for write operations. For STP you can see the required changes in pull request #4: https://github.com/agra-uni-bremen/metaSMT/pull/4/files

On your plan for strings. I can just repeat, what I wrote 3 weeks ago (repeated here without some typos)]:

Define tags for the variables, constants and operations in the theory, see tags directory.

Define the input language for the theory. See frontend directory. This is based in boost.proto and rather obscure at times.

Write tests for the logic. Using each of the defined operations. Usually a set of simple satisfiable or unsatisfiable assertion.

Implement support for the new theory in one or more backends.

Overall I still think this is quite a lot of work for a theory/logic that is not yet standardized. As you have to extract the common interface of Z3-str and CVC4.

anithag commented 9 years ago

@finnhaedicke

I wish there is a mailing list or some sort to discuss this. Would you mind helping me generate Array Expression in CVC4? As I understand to create array variable, I would probably need to generate an expression. I am using mkVar(). My patch currently looks like below. Barring syntax errors, is this doing what it is supposed to do? It gets compiled. (I might get better eventually at figuring out stuff).

@@ -90,6 +91,23 @@ namespace metaSMT { return exprManager_.mkExpr(::CVC4::kind::ITE, a, b, c); }

+ result_type operator() (arraytags::array_var_tag const &var,

boost::any const & ) {
if (var.id == 0 ) {
throw std::runtime_error("uninitialized array used");
}
::CVC4::Type indexsort = exprManager.mkBitVectorType(var.index_width);
::CVC4::Type elemsort = exprManager.mkBitVectorType(var.elem_width);
::CVC4::Type ty = exprManager_.mkArrayType(index_sort, elem_sort);
char buf[64];
sprintf(buf, "var_%u", var.id);
//How to generate expression for array? Can we use mkVar()??
return exprManager_.mkVar(buf, ty);
}

anithag commented 9 years ago

Ah, just got through the testing and it works. Let me know if I can submit the patch for #25 for review.

finnhaedicke commented 9 years ago

Feel free to fork metaSMT, commit your patch to a branch and submit a pull request.

agra-uni-bremen / metaSMT

Integrate CVC4 #23