New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

z3 conditions #2538

Merged
merged 14 commits into from Aug 23, 2017

Conversation

Projects
None yet
3 participants
@chriseth
Contributor

chriseth commented Jul 7, 2017

No description provided.

@axic

This comment has been minimized.

Show comment
Hide comment
@axic

axic Jul 10, 2017

Member

Appveyor:

Performing configure step for 'z3-project'
  '.\configure' is not recognized as an internal or external command,
  operable program or batch file.
C:\Program Files (x86)\MSBuild\Microsoft.Cpp\v4.0\V140\Microsoft.CppCommon.targets(171,5): error MSB6006: "cmd.exe" exited with code 9009. [C:\projects\solidity\build\z3-project.vcxproj]

And emscripten tests ran out of memory - restarted to see if it is a permanent issue.

Member

axic commented Jul 10, 2017

Appveyor:

Performing configure step for 'z3-project'
  '.\configure' is not recognized as an internal or external command,
  operable program or batch file.
C:\Program Files (x86)\MSBuild\Microsoft.Cpp\v4.0\V140\Microsoft.CppCommon.targets(171,5): error MSB6006: "cmd.exe" exited with code 9009. [C:\projects\solidity\build\z3-project.vcxproj]

And emscripten tests ran out of memory - restarted to see if it is a permanent issue.

@chriseth

This comment has been minimized.

Show comment
Hide comment
@chriseth

chriseth Jul 10, 2017

Contributor

Concerning the configure error: I ran this against emscripten and it resulted in a 50mb .js file. It loaded quite fast but then also did not terminate while compiling.

I'm currently refactoring this to use the standardized LIBSMT2 interface between solc and the solver, this would also allow us to swap z3 by other solvers and provide it through remixd for browser-solidity.

Contributor

chriseth commented Jul 10, 2017

Concerning the configure error: I ran this against emscripten and it resulted in a 50mb .js file. It loaded quite fast but then also did not terminate while compiling.

I'm currently refactoring this to use the standardized LIBSMT2 interface between solc and the solver, this would also allow us to swap z3 by other solvers and provide it through remixd for browser-solidity.

@axic

This comment has been minimized.

Show comment
Hide comment
@axic

axic Jul 11, 2017

Member

Please rebase.

Member

axic commented Jul 11, 2017

Please rebase.

@chriseth

This comment has been minimized.

Show comment
Hide comment
@chriseth

chriseth Jul 12, 2017

Contributor

Discussion result: Link against z3 library if available. If not, report warning on the pragma. On emscripten / in jsonCompiler: provide callback for SMTLIB2.

Contributor

chriseth commented Jul 12, 2017

Discussion result: Link against z3 library if available. If not, report warning on the pragma. On emscripten / in jsonCompiler: provide callback for SMTLIB2.

@chriseth

This comment has been minimized.

Show comment
Hide comment
@chriseth

chriseth Jul 24, 2017

Contributor

Removed the "fixup"s.

Contributor

chriseth commented Jul 24, 2017

Removed the "fixup"s.

@@ -145,6 +145,17 @@ inline std::string toHex(u256 val, HexPrefix prefix = HexPrefix::DontAdd)
return (prefix == HexPrefix::Add) ? "0x" + str : str;
}
/// Returns decimal representation for small numbers and hex for large numbers.
inline std::string formatNumber(bigint const& _value)

This comment has been minimized.

@axic

axic Jul 27, 2017

Member

This isn't used anywhere? Though I am fine adding it as a helper.

@axic

axic Jul 27, 2017

Member

This isn't used anywhere? Though I am fine adding it as a helper.

This comment has been minimized.

@chriseth

chriseth Jul 27, 2017

Contributor

Hm, at least it should print big and small numbers differently, let me check again.

@chriseth

chriseth Jul 27, 2017

Contributor

Hm, at least it should print big and small numbers differently, let me check again.

@@ -290,7 +290,8 @@ class CompilerStack: boost::noncopyable
std::string target;
};
ReadFile::Callback m_readFile;
ReadCallback::Callback m_readFile;
ReadCallback::Callback m_smtQuery;

This comment has been minimized.

@axic

axic Aug 11, 2017

Member

This is never assigned to?

@axic

axic Aug 11, 2017

Member

This is never assigned to?

This comment has been minimized.

@chriseth

chriseth Aug 14, 2017

Contributor

Yeah, let's keep it like that for now. This is the endpoint where systems that do not have libz3 tie in, for example the jsonCompiler. We still have to decide how the interface for specifying such a callback would look like.

@chriseth

chriseth Aug 14, 2017

Contributor

Yeah, let's keep it like that for now. This is the endpoint where systems that do not have libz3 tie in, for example the jsonCompiler. We still have to decide how the interface for specifying such a callback would look like.

@chriseth

This comment has been minimized.

Show comment
Hide comment
@chriseth

chriseth Aug 15, 2017

Contributor

@axic can this be merged?

Contributor

chriseth commented Aug 15, 2017

@axic can this be merged?

@axic axic added the nextrelease label Aug 15, 2017

void SMTChecker::setValue(Declaration const& _decl, bool _setToZero)
{
auto const& intType = dynamic_cast<IntegerType const&>(*_decl.type());

This comment has been minimized.

@axic

axic Aug 21, 2017

Member

Shouldn't be there an assertion _decl is of IntegerType?

@axic

axic Aug 21, 2017

Member

Shouldn't be there an assertion _decl is of IntegerType?

This comment has been minimized.

@chriseth

chriseth Aug 21, 2017

Contributor

This basically is an assertion. It will throw an exception if the cast cannot be performed.

@chriseth

chriseth Aug 21, 2017

Contributor

This basically is an assertion. It will throw an exception if the cast cannot be performed.

This comment has been minimized.

@axic

axic Aug 21, 2017

Member

👍

Wasn't sure the const ref one behaves as an assertion (since the const pointer doesn't).

@axic

axic Aug 21, 2017

Member

👍

Wasn't sure the const ref one behaves as an assertion (since the const pointer doesn't).

This comment has been minimized.

@chriseth

chriseth Aug 21, 2017

Contributor

Yes, pointer returns nullptr for failure, ref throws on failure.

@chriseth

chriseth Aug 21, 2017

Contributor

Yes, pointer returns nullptr for failure, ref throws on failure.

return _decl.name() + "_" + to_string(_decl.id());
}
string SMTChecker::uniqueSymbol(Expression const& _expr)

This comment has been minimized.

@axic

axic Aug 21, 2017

Member

const function?

@axic

axic Aug 21, 2017

Member

const function?

This comment has been minimized.

@chriseth

chriseth Aug 21, 2017

Contributor

changed it to static

@chriseth

chriseth Aug 21, 2017

Contributor

changed it to static

);
}
string SMTChecker::uniqueSymbol(Declaration const& _decl)

This comment has been minimized.

@axic

axic Aug 21, 2017

Member

const function?

@axic

axic Aug 21, 2017

Member

const function?

This comment has been minimized.

@chriseth

chriseth Aug 21, 2017

Contributor

changed it to static

@chriseth

chriseth Aug 21, 2017

Contributor

changed it to static

return smt::Expression(_t.minValue());
}
smt::Expression SMTChecker::maxValue(IntegerType const& _t)

This comment has been minimized.

@axic

axic Aug 21, 2017

Member

These are const function?

@axic

axic Aug 21, 2017

Member

These are const function?

This comment has been minimized.

@chriseth

chriseth Aug 21, 2017

Contributor

changed it to static

@chriseth

chriseth Aug 21, 2017

Contributor

changed it to static

@axic

axic approved these changes Aug 21, 2017

@axic

This comment has been minimized.

Show comment
Hide comment
@axic

axic Aug 21, 2017

Member

Tests fail: some of the SAT/UNSAT cases were not updated.

Member

axic commented Aug 21, 2017

Tests fail: some of the SAT/UNSAT cases were not updated.

@axic

This comment has been minimized.

Show comment
Hide comment
@axic

axic Aug 23, 2017

Member

@chriseth oops just merged the cmake changes and this needs to be updated.

Member

axic commented Aug 23, 2017

@chriseth oops just merged the cmake changes and this needs to be updated.

@axic axic merged commit 957f23a into develop Aug 23, 2017

2 checks passed

continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details

@axic axic deleted the z3Conditions branch Aug 23, 2017

@axic axic removed the nextrelease label Aug 23, 2017

@axic

This comment has been minimized.

Show comment
Hide comment
@axic

axic Aug 23, 2017

Member

@chriseth I shouldn't have merged this without rebasing after #2783. One of the scripts was removed which this depended on.

@chfast can you check if cmake/FindZ3.cmake can be done without that script?

Member

axic commented Aug 23, 2017

@chriseth I shouldn't have merged this without rebasing after #2783. One of the scripts was removed which this depended on.

@chfast can you check if cmake/FindZ3.cmake can be done without that script?

@chfast

This comment has been minimized.

Show comment
Hide comment
@chfast

chfast Aug 24, 2017

Contributor

Fixed in #2791.

Contributor

chfast commented Aug 24, 2017

Fixed in #2791.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment