cerc-io/solidity
11
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
23,848 Commits 348 Branches 121 Tags
342df8a515a11f84c8d14d3644a31e04ebb8ce74
Commit Graph
23848 Commits
This Branch
This Branch
All Branches
Author SHA1 Message Date
Martin Blicha 342df8a515 Ensure SMT-LIB file is complete 2023-09-05 12:39:19 +02:00
Martin Blicha 5569aaee78 Fix coding style 2023-09-05 12:39:19 +02:00
Martin Blicha ecded11833 Tests: Disable checking CEX 
In this case I observed brittle behaviour with Z3, which behaved
differently on two equivalent queries with only variables renamed.
The reason for different versions was that in isoltest, we add version
pragma to the source code and this changes the ids of AST nodes. These
are in turn used to generate uniques names for SMT variables.
 2023-09-05 12:39:19 +02:00
Martin Blicha 799f418bef Make counterexample deterministic 2023-09-05 12:39:19 +02:00
Martin Blicha 4ecaa476fd Handle custom tuple sorts in a general way 2023-09-05 12:39:19 +02:00
Martin Blicha 742642ebae Use answer from second Z3 call only when solved 2023-09-05 12:39:19 +02:00
Martin Blicha 0fbeb3a69d Throw exception on unhandled cases in SMT-LIB Expression conversion 2023-09-05 12:39:19 +02:00
Martin Blicha 4b50f26834 Negative numbers do not have to be atoms 2023-09-05 12:39:19 +02:00
Martin Blicha 779db2d84f Use shared pointers, not raw pointers, for caching sorts 2023-09-05 12:39:19 +02:00
Martin Blicha b65c37029d Fix parsing array expressions from SMT-LIB proof 2023-09-05 12:39:19 +02:00
Martin Blicha d773e76704 Remove outdated FIXME 2023-09-05 12:39:19 +02:00
Martin Blicha 451b6f8ced Fix handling of structs in SMT-LIB CEX 2023-09-05 12:39:19 +02:00
Martin Blicha 9339b7074a Fix parsing of let expression to allow shadowing values 2023-09-05 12:39:19 +02:00
Martin Blicha 92689e4256 Fix code style problems 2023-09-05 12:39:19 +02:00
Martin Blicha 8ea8a1eb99 Cache sorts already in SMTLib2Interface 
This allows us to ask for a sort of a sort from its string
representation parsed from an SMT-LIB solver response
 2023-09-05 12:39:19 +02:00
Martin Blicha 6acbe2ec35 Towards translating proof from SMT-LIB response 2023-09-05 12:39:19 +02:00
Martin Blicha 479bb9c3de Fix missing std 2023-09-05 12:39:19 +02:00
Martin Blicha 2195b5e57a Solve UNSAT queries again with proof production enabled 2023-09-05 12:39:19 +02:00
Martin Blicha c90b48af02 Update to the tests 2023-09-05 12:39:19 +02:00
Martin Blicha 58d0579ba6 SMTCheckerTests: Use SMT callback 2023-09-05 12:39:19 +02:00
Martin Blicha 1d60559551 Use same spacer parameters as before 2023-09-05 12:39:19 +02:00
Martin Blicha d9dc8f475e Enable resource limit for Z3 2023-09-05 12:39:19 +02:00
Martin Blicha c6f274892e Fix SMTLib2Interface 2023-09-05 12:39:19 +02:00
Martin Blicha f4b849972c Remove smtlib2 solver option 2023-09-05 12:39:17 +02:00
Martin Blicha 72974adb92 Fix check for SMT query in UniversalCallback 2023-09-05 12:37:56 +02:00
Martin Blicha e7fe310bc2 Remove unnecessary header 2023-09-05 12:37:56 +02:00
Martin Blicha da2f4cb100 Try to parse values only for satisfiable answer 2023-09-05 12:37:56 +02:00
Martin Blicha efb0d4253c Use callback properly in SMTLib2 interface 2023-09-05 12:37:56 +02:00
Martin Blicha cabec89872 Removing SMT portfolio 2023-09-05 12:37:56 +02:00
Martin Blicha 1e190abf6e Initial work on unified way to interact with solvers 2023-09-05 12:37:56 +02:00
Daniel 16ae76cad7 Merge pull request #14533 from ethereum/fix-std-namespace-asan 
Fix missing std qualifier for ASAN
 2023-09-05 11:04:13 +02:00
Nikola Matic ae36323edb Fix missing std qualifier for ASAN 2023-09-05 08:49:23 +02:00
Daniel e43968599e Merge pull request #14468 from ethereum/push0-rematerializer-default-sequence 
Push0 rematerializer default sequence
 2023-09-04 19:27:33 +02:00
Nikola Matic fdc6699159 Rematerialize zero literals with default cleanup sequence 
Add unused pruner step to the end of the default cleanup sequence
 2023-09-04 15:40:33 +02:00
Daniel 1b8e792eb6 Merge pull request #14530 from ethereum/fix-oz-failing-test 
Fix failing OZ test
 2023-09-04 13:08:47 +02:00
Nikola Matic 76e0d81354 Fix failing OZ test 2023-09-04 12:23:12 +02:00
Nikola Matić 737c1abbdf Merge pull request #14525 from molecula451/purge-std 
deprecate using namespace std
 2023-09-04 11:02:15 +02:00
PaulandNikola Matić b3230b0bdc deprecate using namespace std 
test: updat filereader test

deprecate namespace std

deprecate namespace std

deprecate namespace std

deprecate namespace std

deprecate namespace std

deprecate namespace std

deprecate namespace std

deprecate namespace std

deprecated std namespace

deprecated std namespace

deprecated std namespace

deprecated std namespace

deprecated std namespace

deprecated std namespace

deprecated std namespace

deprecated std namespace

deprecated std namespace

depecrate namespace std

deprecated namespace std

check ci

clean line

Co-authored-by: Nikola Matić <nikola.matic@ethereum.org>

purge line

pure line

deprecate std

deprecate std

deprecate std

deprecate std

deprecate std

deprecate

deprecate std

bye namespace
 2023-09-04 10:12:07 +02:00
Nikola Matić df03f1412d Merge pull request #14522 from junaire/purge-using-namespace-std-in-libyul 
Purge using namespace std in libyul
 2023-08-29 12:38:50 +02:00
Jun Zhang eff410eb74 Purge using namespace std in libyul 
Signed-off-by: Jun Zhang <jun@junz.org>
 2023-08-29 11:51:59 +02:00
Daniel 26912e0ee2 Merge pull request #14515 from junaire/bump-fmtlib-version 
Bump fmtlib to 9.1.0
 2023-08-28 17:24:20 +02:00
Nikola Matić 88b8368932 Merge pull request #14512 from junaire/yul-opt-kill-namespace-std 
Purge using namespace std from libyul/optimiser
 2023-08-28 16:01:03 +02:00
Jun Zhang c2362c3362 Purge using namespace std from libyul/optimiser 
Signed-off-by: Jun Zhang <jun@junz.org>
 2023-08-28 21:14:56 +08:00
Jun Zhang 2cf23e15d8 Bump fmtlib to 9.1.0 
In our downstream project, we have two dependencies: solidity and spdlog.
Both of them depend on fmtlib. Unfortunately, the versions of fmtlib they
use do not match, which leads to compilation failure.

The issue arises because spdlog attempts to use solidity's fmtlib, but the
specific version (v8.0.1) has a bug. Ref: https://github.com/gabime/spdlog/issues/2142

While we could keep this change in our own fork, we believe it would
be worthwhile to contribute it back to the upstream since spdlog is a
very popular logging library.

Signed-off-by: Jun Zhang <jun@junz.org>
 2023-08-28 13:58:56 +08:00
Nikola Matić 925bfeb24b Merge pull request #14513 from junaire/yul-backend-namespace-std 
Purge using namespace std from libyul/backends
 2023-08-28 07:56:38 +02:00
Jun Zhang 1ebdab43d8 Purge using namespace std from libyul/backends 
Signed-off-by: Jun Zhang <jun@junz.org>
 2023-08-24 11:12:52 +08:00
Daniel 37e18612c5 Merge pull request #14505 from ethereum/syntax-test-more-extension-points 
Make `SyntaxTest` easier to extend with custom expectations
 2023-08-23 18:48:37 +02:00
Kamil Śliwak e847596e39 CommonSyntaxTest: Add support for syntax tests with custom expectations in addition to expected errors 2023-08-23 18:00:01 +02:00
Kamil Śliwak c965d6332c SyntaxTest: Allow derived test cases to filter out warnings and infos 2023-08-23 18:00:01 +02:00
Kamil Śliwak 73b9077ab0 SyntaxTest: Default-initialize boolean fields without showing the value 
- These get re-initialized in constructor anyway. The only purpose if initializing here is our convention to always initialize primitive types at declaration time. We don't want to have to repeat the defaults though.
 2023-08-23 18:00:01 +02:00