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
19,375 Commits 348 Branches 121 Tags
40221a90c41fe626ced3c0e93323fdec4ac76c51
Commit Graph
100 Commits
This Branch
This Branch
All Branches
Author SHA1 Message Date
Leonardo Alt 40221a90c4 Update smtCheckerTests for z3 4.8.10 2021-01-26 10:18:52 +01:00
Leonardo ead1a26f21 Merge pull request #10797 from ethereum/refactor-and-shellcheck-cleanup-in-report-errors-sh 
Refactor and shellcheck cleanup in report_errors.sh and check_style.sh
 2021-01-22 12:12:39 +01:00
Leonardo 3045770a6f Merge pull request #10828 from ethereum/smt_cex_value 
[SMTChecker] Add msgvalue to cex if > 0
 2021-01-21 21:34:38 +01:00
Leonardo Alt a612daa783 Add msgvalue to cex 2021-01-21 19:05:44 +01:00
Leonardo a75b87c80e Merge pull request #10813 from ethereum/smt_targets_option 
Add CLI and JSON option to select SMTChecker targets
 2021-01-20 18:37:08 +01:00
Leonardo Alt 3b23cadbdc Add CLI and JSON option to select SMTChecker targets 2021-01-20 17:35:37 +01:00
Leonardo 0b023b893e Merge pull request #10817 from ethereum/splitShiftBytesTest 
Split shift bytes test.
 2021-01-19 16:16:45 +01:00
Leonardo 9bde92ca20 Merge pull request #10807 from ethereum/fixIRReasonStrings 
Properly omit require revert strings in IR code generator if requested.
 2021-01-19 10:31:15 +01:00
Leonardo 957e9995a0 Merge pull request #10801 from blishko/issue-10793 
[SMTChecker] Gather local variables also from nested try/catch clauses
 2021-01-18 22:37:16 +01:00
Leonardo 51b7dc69b7 Merge pull request #10802 from ethereum/smt_fix_override 
[SMTChecker] Fix static virtual resolution
 2021-01-18 17:10:31 +01:00
Leonardo Alt c7ca87c012 Fix static virtual resolution 2021-01-18 16:23:38 +01:00
Leonardo 726c5ff68c Merge pull request #10777 from blishko/smt-fix-checked 
[SMTChecker] Fix BMC crash related to `unchecked` blocks
 2021-01-15 16:46:32 +01:00
Leonardo 93b25dc783 Merge pull request #10741 from ethereum/smt_cex_external_calls 
[SMTChecker] Synthesize untrusted functions called externally
 2021-01-15 15:31:56 +01:00
Leonardo Alt 007d39871b [SMTChecker] Synthesize untrusted functions called externally 2021-01-15 11:56:26 +01:00
Leonardo 110e0e1f25 Merge pull request #10763 from blishko/smt-abi-fixes 
[SMTChecker] Small fixes in handling ABI functions
 2021-01-14 16:00:49 +01:00
Leonardo 501461147e Merge pull request #10750 from blishko/issue-10657 
[SMTChecker] Fixed pushing string literal to bytes array
 2021-01-13 17:28:42 +01:00
Leonardo fe344ed6e5 Merge pull request #10748 from blishko/smt-refactoring 
[SMTChecker] Refactoring common functionality
 2021-01-13 14:23:19 +01:00
Leonardo fa28e48415 Merge pull request #10727 from ethereum/smt_cex_internal_calls 
[SMTChecker] Report internal calls in CHC transaction trace
 2021-01-12 15:44:12 +01:00
Leonardo Alt b3c3836388 Output internal calls 2021-01-12 14:57:04 +01:00
Leonardo Alt f1ae24abc7 Remove extra line breaks 2021-01-12 14:00:07 +01:00
Leonardo 66a773aef9 Merge pull request #10721 from blishko/smt-try-catch 
[SMTChecker] Support try-catch statements
 2021-01-12 12:04:38 +01:00
Leonardo 7824ccb56d Merge pull request #10663 from ethereum/check_style_exclude_list_support 
scripts/check_style.sh: add exclude list support.
 2021-01-12 11:28:26 +01:00
Leonardo Alt 5f39662235 Fix BFS visit 2021-01-11 13:18:59 +01:00
Leonardo d11cf15d37 Merge pull request #10722 from ethereum/smt_cex_calls 
[SMTChecker] Refactor cex loop
 2021-01-07 23:57:52 +01:00
Leonardo Alt 11f56861c3 Refactor cex loop 2021-01-07 23:13:02 +01:00
Leonardo 130fc0701b Merge pull request #10716 from ethereum/rename_bfs 
Make BFS correct again
 2021-01-06 11:55:34 +01:00
Leonardo Alt ced79497f5 Fix BFS 2021-01-06 10:17:17 +01:00
Leonardo fdbb4d9a8f Merge pull request #10705 from ethereum/smt_cex_contract 
[SMTChecker] Output contract's name in counterexample
 2021-01-04 12:57:06 +01:00
Leonardo Alt b02722ebda Add contract name to called function in cex 2021-01-04 10:03:16 +01:00
Leonardo Alt 78d55e6b4a [SMTChecker] Support check/unchecked 2020-12-30 12:14:30 +01:00
Leonardo eb05826857 Merge pull request #10702 from blishko/smt-block-constraints 
[SMTChecker] Add missing constraints for block properties
 2020-12-30 09:14:47 +01:00
Leonardo 86c30b4cf5 Merge pull request #10685 from ethereum/smt_virtual_functions 
[SMTChecker] Fix calls to virtual/overriden functions
 2020-12-29 15:05:29 +01:00
Leonardo Alt 9482e7de23 [SMTChecker] Fix calls to virtual/overriden functions 2020-12-29 11:25:20 +01:00
Leonardo 840b194bea Merge pull request #10662 from blishko/smt-external-error 
[SMTChecker] Carry error information across external calls
 2020-12-29 11:05:21 +01:00
Leonardo 03946bcd3c Merge pull request #10694 from suriyaa/patch-1 
Update Natspec documentation URL
 2020-12-28 11:08:02 +01:00
Leonardo 6bcae84610 Merge pull request #10678 from blishko/refactor 
[SMTChecker] Small refactoring to define a single way of gathering functions belonging to a given contract.
 2020-12-22 13:50:26 +01:00
Leonardo a48106ca1f Merge pull request #10670 from blishko/smt-virtual-modifiers-fix 
[SMTChecker] Fix virtual modifier called statically
 2020-12-21 18:05:02 +01:00
Leonardo 158154bac3 Merge pull request #10345 from ethereum/ir-runtime 
Output runtime object in IR
 2020-12-18 17:19:40 +01:00
Leonardo Alt 034d1ab90f [SMTChecker] Replace constants by their value in-place 2020-12-18 14:22:28 +01:00
Leonardo 6b482d4b41 Merge pull request #10647 from ethereum/ppaStaticRelease 
Build solidity-upgrade and yul-phaser statically on static PPA builds.
 2020-12-18 14:20:44 +01:00
Leonardo 16832985f5 Merge pull request #10614 from blishko/smt-overidden-modifiers 
[SMTChecker] Fix analysis of overriding modifiers
 2020-12-18 09:26:34 +01:00
Leonardo Alt 50be39fc21 Add and update tests 2020-12-17 14:42:49 +01:00
Leonardo Alt 7ba91cdc33 Changelog 2020-12-17 14:03:17 +01:00
Leonardo Alt 2cbf33ca1c SMTChecker support ABI functions as UFs 2020-12-17 14:03:17 +01:00
Leonardo Alt f5c96ea6da Fix constant evaluation build 2020-12-16 17:59:00 +01:00
Leonardo Alt 80e85b772b [SMTChecker] Apply const eval to arithmetic binary expressions 2020-12-16 14:58:00 +01:00
Leonardo Alt 59428b8f76 Fix SMTChecker tests on breaking 2020-12-15 19:49:57 +01:00
Leonardo 2552a9b7b0 Merge pull request #10601 from blishko/smt-fix-constructor-recursive-struct 
[SMTChecker] Fix internal error on constructor of a recursive struct
 2020-12-15 12:15:16 +01:00
Leonardo d83ce0bcdd Merge pull request #10599 from blishko/smt-inc-dec-push-fix 
[SMTChecker] Fix internal error when increment/decrement is applied on a result of push().
 2020-12-14 23:52:54 +01:00
Leonardo 2ca70bd71a Merge pull request #10597 from blishko/smt-fix-abstract-modifier 
[SMTChecker] Fix internal error on abstract modifier
 2020-12-14 19:34:44 +01:00
Leonardo e21be30df4 Merge pull request #10588 from blishko/smt-push-bytes-fix 
[SMTChecker] Fix internal error on bytes.push on the LHS of an assignment
 2020-12-14 18:19:35 +01:00
Leonardo ccf1626f0d Merge pull request #10581 from blishko/issue-10524 
[SMTChecker] Fix handling of function calls where the function identifier is nested in a tuple.
 2020-12-14 17:20:18 +01:00
Leonardo db9aa36d6c Merge pull request #10567 from blishko/unary-operators-fix 
[SMTChecker] Fix CHC analysis of increment/decrement
 2020-12-11 18:52:12 +01:00
Leonardo da9cede0fe Merge pull request #10348 from ethereum/simplify-compiler 
Simplify abstraction of Compiler/CompilerContext/CompilerStack
 2020-12-11 17:42:36 +01:00
Leonardo 7972d8eb98 Merge pull request #10578 from ethereum/ast-test 
Properly print sources in ASTJSONTest
 2020-12-11 17:41:31 +01:00
Leonardo adead3072d Merge pull request #10570 from ethereum/abiv2-isabelle-test-values-fix-bugs 
Ensure empty arrays are not visited and fix formatting issues
 2020-12-11 17:38:15 +01:00
Leonardo Alt 64f81fe82b Fix SMT tests 2020-12-10 18:54:52 +01:00
Leonardo 7e930f7bb3 Merge pull request #10543 from ethereum/abiv2-isabelle-encode-test 
Isabelle abiv2 fuzzer: Add type string
 2020-12-09 23:33:41 +01:00
Leonardo 9e07981920 Merge pull request #10477 from ethereum/smt_isoltest_cex 
[SMTChecker] Move CHC counterexamples to primary location
 2020-12-09 20:37:24 +01:00
Leonardo Alt 3c142e0e94 Move CHC counterexamples to primary location 2020-12-09 19:55:18 +01:00
Leonardo c34a2f27e5 Merge pull request #10540 from ethereum/smt_file_level 
Do not run SMTChecker when file level functions/constants are present.
 2020-12-09 15:39:18 +01:00
Leonardo Alt a961a76263 Do not run SMTChecker when file level functions/constants are present. 2020-12-09 12:18:55 +01:00
Leonardo 3ca4a5136d Merge pull request #10539 from blishko/test-issue-10502 
[SMTChecker] Adding test witnessing that SMTChecker no longer crashes when producing CEX with arrays
 2020-12-09 11:03:53 +01:00
Leonardo e78ca14368 Merge pull request #10510 from blishko/struct_in_cex 
[SMTChecker] Adding support for reporting values of structs in CEX in CHC engine
 2020-12-08 18:09:31 +01:00
Leonardo 71a4a4efb1 Merge pull request #10529 from blishko/compound_assignment 
[SMTChecker] Remove assert that is not true for compound assignment with right shift
 2020-12-08 15:43:36 +01:00
Leonardo b23d923023 Merge pull request #10490 from blishko/issue-10439 
[SMTChecker] Fixing type conversion from StringLiteral to FixedBytes
 2020-12-07 20:39:09 +01:00
Leonardo 51e27dd3d3 Merge pull request #9543 from ethereum/smt_return 
[SMTChecker] Support return in CHC
 2020-12-07 19:15:18 +01:00
Leonardo Alt b7ac207391 [SMTChecker] Support return in CHC 2020-12-07 18:17:33 +01:00
Leonardo d47a9dedd0 Merge pull request #10494 from ethereum/tempRefMemberSegfault 
Add const ref to prevent segfaults.
 2020-12-04 15:49:47 +01:00
Leonardo 4e4aaaf028 Merge pull request #10389 from ethereum/smt_constructors_nonlinear_clauses 
[SMTChecker] Use nonlinear clauses instead of inlining base constructors in CHC
 2020-12-04 14:03:15 +01:00
Leonardo Alt 7490ffbe13 Use nonlinear clauses instead of inlining for base constructors 2020-12-04 13:25:56 +01:00
Leonardo a27d7707c8 Merge pull request #10493 from ethereum/smt_fix_487 
[SMTChecker] Do not request proof for old z3
 2020-12-03 22:17:41 +01:00
Leonardo Alt 4210e09d9a Do not request proof for old z3 2020-12-03 20:57:23 +01:00
Leonardo 088b694f0b Merge pull request #10207 from ethereum/smt_tests_asserts 
[SMTChecker] Add uncovered test and replace uncovered tests by asserts
 2020-12-03 08:59:48 +01:00
Leonardo 3cd0b25220 Merge pull request #10442 from blishko/this-public-getters 
[SMTChecker] Adding support for public getters on `this`
 2020-12-02 18:06:29 +01:00
Leonardo Alt fa561dbd0e Add uncovered test and replace uncovered tests by asserts 2020-11-30 18:46:47 +01:00
Leonardo 3287341f1e Merge pull request #10316 from blishko/bmc_branches 
[SMTChecker] Handle branches with return statements properly in BMC engine
 2020-11-30 13:50:09 +01:00
Leonardo 84ff925de4 Merge pull request #10431 from Jaime-Iglesias/issue-10284 
[docs] Add clarification to struct initialization in previous versions
 2020-11-30 11:12:42 +01:00
Leonardo 61425e3541 Merge pull request #10378 from ethereum/smt_fix_spellcheck 
Fix spelling in SMTChecker comment
 2020-11-23 18:14:58 -01:00
Leonardo Alt 68cfa0a901 Fix spelling in SMTChecker comment 2020-11-23 19:40:29 +01:00
Leonardo 243ac16cea Merge pull request #10374 from blishko/smtchecker-type-identifiers 
[SMTChecker] Do not report warning when encountered a Type identifier.
 2020-11-23 15:54:06 -01:00
Leonardo cbfd47cc9a Merge pull request #10360 from blishko/struct_constructor 
[SMTChecker] Adding support for struct constructor
 2020-11-23 12:56:10 -01:00
Leonardo 61069ec77d Merge pull request #10355 from blishko/smtchecker-refactoring 
[SMTChecker] Small refactoring of assignments to provide a common low-level point for model checking engines to hook into.
 2020-11-20 14:31:32 -01:00
Leonardo ae8f484ed4 Merge pull request #10234 from ethereum/smt_named_arguments 
[SMTChecker] Support named arguments in function calls
 2020-11-20 12:24:51 -01:00
Leonardo Alt e4339b0526 [SMTChecker] Support named arguments in function calls 2020-11-20 11:52:26 -01:00
Leonardo 65c2089b43 Merge pull request #10310 from blishko/issue-10306 
[SMTChecker] Adding a dummy frame to the call stack for the implicit constructor
 2020-11-17 09:34:49 -01:00
Leonardo 81b3a13333 Merge pull request #10289 from ethereum/fix-standard-json-crash-on-linker-references-without-colon 
Fix standard JSON crash on linker references without a colon
 2020-11-16 19:27:35 -01:00
Leonardo f1846b57a2 Merge pull request #10244 from blishko/this-external-calls 
[SMTChecker] Analyzing external calls to `this`
 2020-11-13 11:28:34 +00:00
Leonardo 55ac5de472 Merge pull request #10240 from ethereum/immutablesPureValue 
Immutables with literal values are pure.
 2020-11-10 15:23:33 +00:00
Leonardo b9d2f9f10f Merge pull request #10241 from ethereum/solc-ewasm-exception 
[solc] Handle exceptions in AssemblyStack.translate() gracefully
 2020-11-09 19:41:05 +00:00
Leonardo 25b2a38d8b Merge pull request #10202 from ethereum/smt_fix_modifiers_branches 
[SMTChecker] Fix CHC false positives when using branches inside modifiers
 2020-11-09 16:42:30 +00:00
Leonardo 8d5b32e5b9 Merge pull request #10232 from ethereum/sol-yul-better-assertion-message-from-yulutilfunctions-conversionfunction 
More informative assertion message on invalid conversions YulUtilFunctions::conversionFunction()
 2020-11-09 13:19:48 +00:00
Leonardo 6fa42b5efd Merge pull request #10206 from ethereum/smt_add_bmc_specific 
Isoltest SMTChecker option and BMC specific tests
 2020-11-06 17:16:02 +00:00
Leonardo Alt 00858c0ccf Isoltets SMTChecker option and BMC specific tests 2020-11-06 15:03:38 +00:00
Leonardo Alt 1b6abfa37f Make timeout tests harder 2020-11-06 13:35:07 +00:00
Leonardo 6309d78762 Merge pull request #10222 from ethereum/smt_remove_nondet 
[SMTChecker] Decrease nondeterminism
 2020-11-06 13:27:29 +00:00
Leonardo Alt 89dce24f24 Force SMT variable creation order 2020-11-06 11:51:01 +00:00
Leonardo Alt 646be53f2f Sort variables and expressions by AST id 2020-11-06 11:50:43 +00:00
Leonardo Alt 1dbd8f8d67 Fix CHC false positives when using branches inside modifiers 2020-11-04 21:47:07 +00:00
Leonardo 62535c2fd4 Merge pull request #10181 from ethereum/smt_user_timeout 
[SMTChecker] User timeout option
 2020-11-04 10:55:28 +00:00