cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

[SMTChecker] Use rlimit instead of tlimit for SMT queries

Browse Source
This commit is contained in:
Leonardo Alt 2019-12-03 01:11:21 +01:00
parent d0f9201ed4
commit 67d82fc8a7
7 changed files with 17 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/CVC4Interface.cpp
View File

@ -35,7 +35,7 @@ void CVC4Interface::reset()
m_variables.clear(); m_variables.clear();
m_solver.reset(); m_solver.reset();
m_solver.setOption("produce-models", true); m_solver.setOption("produce-models", true);
m_solver.setTimeLimit(queryTimeout); m_solver.setResourceLimit(resourceLimit);
} }
void CVC4Interface::push() void CVC4Interface::push()

6
libsolidity/formal/CVC4Interface.h
View File

@ -63,6 +63,12 @@ private:
CVC4::ExprManager m_context; CVC4::ExprManager m_context;
CVC4::SmtEngine m_solver; CVC4::SmtEngine m_solver;
std::map<std::string, CVC4::Expr> m_variables; std::map<std::string, CVC4::Expr> m_variables;
// CVC4 "basic resources" limit.
// This is used to make the runs more deterministic and platform/machine independent.
// The tests start failing for CVC4 with less than 6000,
// so using double that.
static int const resourceLimit = 12000;
}; };
} }

4
libsolidity/formal/SolverInterface.h
View File

@ -359,10 +359,6 @@ public:
/// @returns how many SMT solvers this interface has. /// @returns how many SMT solvers this interface has.
virtual unsigned solvers() { return 1; } virtual unsigned solvers() { return 1; }
protected:
// SMT query timeout in milliseconds.
static int const queryTimeout = 10000;
}; };
} }

5
libsolidity/formal/Z3CHCInterface.cpp
View File

@ -29,10 +29,9 @@ Z3CHCInterface::Z3CHCInterface():
m_context(m_z3Interface->context()), m_context(m_z3Interface->context()),
m_solver(*m_context) m_solver(*m_context)
{ {
// This needs to be set globally. // These need to be set globally.
z3::set_param("rewriter.pull_cheap_ite", true); z3::set_param("rewriter.pull_cheap_ite", true);
// This needs to be set in the context. z3::set_param("rlimit", Z3Interface::resourceLimit);
m_context->set("timeout", queryTimeout);
// Spacer options. // Spacer options.
// These needs to be set in the solver. // These needs to be set in the solver.

3
libsolidity/formal/Z3CHCInterface.h
View File

@ -54,9 +54,6 @@ private:
z3::context* m_context; z3::context* m_context;
// Horn solver. // Horn solver.
z3::fixedpoint m_solver; z3::fixedpoint m_solver;
// SMT query timeout in milliseconds.
static int const queryTimeout = 10000;
}; };
} }

5
libsolidity/formal/Z3Interface.cpp
View File

@ -27,10 +27,9 @@ using namespace dev::solidity::smt;
Z3Interface::Z3Interface(): Z3Interface::Z3Interface():
m_solver(m_context) m_solver(m_context)
{ {
// This needs to be set globally. // These need to be set globally.
z3::set_param("rewriter.pull_cheap_ite", true); z3::set_param("rewriter.pull_cheap_ite", true);
// This needs to be set in the context. z3::set_param("rlimit", resourceLimit);
m_context.set("timeout", queryTimeout);
} }
void Z3Interface::reset() void Z3Interface::reset()

6
libsolidity/formal/Z3Interface.h
View File

@ -50,6 +50,12 @@ public:
z3::context* context() { return &m_context; } z3::context* context() { return &m_context; }
// Z3 "basic resources" limit.
// This is used to make the runs more deterministic and platform/machine independent.
// The tests start failing for Z3 with less than 20000000,
// so using double that.
static int const resourceLimit = 40000000;
private: private:
void declareFunction(std::string const& _name, Sort const& _sort); void declareFunction(std::string const& _name, Sort const& _sort);