Commits on May 8, 2024

1. 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.

   

   blishko committed May 8, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for 2572e13
   • Browse repository at this point

   Copy the full SHA

   2572e13 View commit details

   Browse the repository at this point in the history