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
23,867 Commits 348 Branches 121 Tags 100 MiB
smtlib-interface-for-everything
Commit Graph

23867 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Martin Blicha
475cfe2532 Ignore standard error output from solvers 2023-09-05 12:39:20 +02:00
Martin Blicha
a4b4e70b67 Get invariants from eldarica 2023-09-05 12:39:20 +02:00
Martin Blicha
d8c1a124e7 Bring back solving with temporary file for Eldarica 2023-09-05 12:39:19 +02:00
Martin Blicha
497ca183b4 Small cleanup 2023-09-05 12:39:19 +02:00
Martin Blicha
1b68b5764d SMTChecker: Ignore model checking without callback 2023-09-05 12:39:19 +02:00
Martin Blicha
b6326f4d4d Do not stop reading solver's output after it terminated 2023-09-05 12:39:19 +02:00
Martin Blicha
8e0e2cb1ae Throw when trying to read past the end of SMTLib stream 2023-09-05 12:39:19 +02:00
Martin Blicha
d3bbc51ee9 Update test after change in variable names 2023-09-05 12:39:19 +02:00
Martin Blicha
4101c67cba Update to let inlining 2023-09-05 12:39:19 +02:00
Martin Blicha
bbd7ef447f Updates to command-line tests 2023-09-05 12:39:19 +02:00
Martin Blicha
ec10f46acb Parse BMC counterexample properly 2023-09-05 12:39:19 +02:00
Martin Blicha
af1acaba64 Refactor SMTLib parser to separate file 2023-09-05 12:39:19 +02:00
Martin Blicha
3a01b432c4 Hack to get around problem in Z3 2023-09-05 12:39:19 +02:00
Martin Blicha
8c99c125c4 Add support for parsing invariants 2023-09-05 12:39:19 +02:00
Martin Blicha
b8f89fa45d SMTSolverCommand: Use pipe instead of temporary file for the query 2023-09-05 12:39:19 +02:00
Martin Blicha
3f22118bbe More checks 2023-09-05 12:39:19 +02:00
Martin Blicha
01ed412714 Stronger checks 2023-09-05 12:39:19 +02:00
Martin Blicha
0c13b7ee8f Turn asserts into solAsserts 2023-09-05 12:39:19 +02:00
Martin Blicha
83b60754a9 Update to the tests to combat nondeterminism 2023-09-05 12:39:19 +02:00
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