Join GitHub today
GitHub is home to over 50 million developers working together to host and review code, manage projects, and build software together.
Sign upGitHub is where the world builds software
Millions of developers and companies build, ship, and maintain their software on GitHub — the largest and most advanced development platform in the world.
[SMTChecker] Support to BitVector and bitwise `and` #8926
Conversation
|
@chriseth all parts done, ready for review |
05bdf8b
to
d70997e
|
Managed to change the CVC4 interface for |
|
Can you check the test failure? |
|
Yep, checking. At least now the Ubuntu ones are ok. |
|
I think we need ethereum/solc-js#468 for that test to pass here |
|
No that doesn't really solve it... |
| @@ -126,7 +126,7 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> con | |||
| result = CheckResult::ERROR; | |||
|
|
|||
| vector<string> values; | |||
| if (result == CheckResult::SATISFIABLE && result != CheckResult::ERROR) | |||
| if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty()) | |||
leonardoalt
May 27, 2020
Author
Member
@chriseth this was apparently a bug here that caused the solc-js test failure. No model was requested in this test (it uses only literals), and because of the solver response sat\n, it was parsing an empty value which caused an assertion failure at BMC.cpp:767.
@chriseth this was apparently a bug here that caused the solc-js test failure. No model was requested in this test (it uses only literals), and because of the solver response sat\n, it was parsing an empty value which caused an assertion failure at BMC.cpp:767.
| return m_context.mkExpr(CVC4::kind::ITE, | ||
| m_context.mkExpr( | ||
| CVC4::kind::EQUAL, | ||
| m_context.mkExpr(CVC4::kind::BITVECTOR_EXTRACT, extractOp, arguments[0]), |
chriseth
May 27, 2020
Contributor
Is this tested?
Is this tested?
leonardoalt
May 27, 2020
Author
Member
Yep, the tests also run CVC4, even different versions of it
Yep, the tests also run CVC4, even different versions of it
|
@chriseth updated & squashed |
Ref #9043
This PR adds the
BitVectorSortwhich will be used for bitwise operators, and adds the bitwiseandoperator to test that.For the SMTEncoder, the strategy to support bitwise operations is to convert the arguments (represented as SMT Integers) to BVs, apply the operation, then convert back to Integer. This works also for signed Integers.
The Yul constraint optimizer might want to use BVs directly.