Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
SMTChecker: Fix equality of array literals
There are two kinds of array literals in Solidity: string literals (arrays of characters/bytes) and proper array literals (e.g., [1,2,3]). While array literals cannot be directly tested for equality in Solidity, it is possible to compute hash of these values and compare hashes. The expectation is that hashes of the same array literals would be the same, but previously SMTChecker returned false positive in this case, saying that they don't have to be equal. The reason for the false positive was the following. We represent Solidity array literal as a tuple `(elements, length)` where `length` is an integer representing the actualy length of the array literal, and `elements` are an SMT-LIB array, where the first `length` elements represent the actual content of the array literal. However, SMT-LIB arrays are infinite objects (more like functions from indices to elements). Previously, we left the part after `length`-th element unspecified. For the solver this meant that two array literals equal at the Solidity level were represented with two different SMT-LIB arrays. The proposed solution is to always start from a constant-zero array, and use store operations to build an SMT-LIB array that matches the Solidity array literal.
- Loading branch information
Showing
14 changed files
with
103 additions
and
55 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.