Solidity: SMT: display large values in a nicer format

[axic]

nonlinear.sol:7:12: Warning: Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
        uint c = a * b;
                 ^---^
  for:
  a = 2
  b = 0x8000000000000000000000000000000000000000000000000000000000000000
  c = 0
  value = 0x010000000000000000000000000000000000000000000000000000000000000000

I think the values should be displayed in a more friendly way. @ekpyron suggested that it should detect powers of 2 and powers of 2 minus one and display them accordingly.

It is hard to compare these numbers without sitting down to compare/calculate.

[ekpyron]

We could also consider counting the (pairs of) trailing zeros and replace them by * 2^x or by << x if the count exceeds a given value, let's say 8. At least partly - maybe for each * 2^(2^n), which are the "usual" data type boundaries.

[chriseth]

Please note that the utility function currently in use has to be split for use by the smt component for human-targeted output and the yul optimizer for yul output (which can only have simple hex or decimal numbers, but those should still be "readable").

[axic]

My suggestion is that in libdevcore/CommonData.h formatNumber is extended to either have a flag or have another function (like formatNumberReadable) in which case it decomposes the number as suggested by @ekpyron.

This function is currently used by both the SMT checker and the Yul optimiser.

[gitcoinbot]

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

---

__This issue now has a funding of 425.0 DAI (425.0 USD @ $1.0/DAI) attached to it__ as part of the Ethereum Foundation fund__.__

• If you would like to work on this issue you can 'start work' on the Gitcoin Issue Details page.
  
  
  
  • Want to chip in? Add your own contribution here.
  
  
  • Questions? Checkout Gitcoin Help or the Gitcoin Slack
  
  
  • $22,696.04 more funded OSS Work available on the Gitcoin Issue Explorer
  
  

[gitcoinbot]

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

---

__Work has been started__.

These users each claimed they can complete the work by 6 months, 3 weeks from now.
Please review their action plans below:

1) irmacias has applied to start work _(Funders only: approve worker | reject worker)_.

I can follow the suggestions and implement the solution by converting from hex.

Learn more on the Gitcoin Issue Details page.

2) chriscates has been approved to start work.

Submitted a sample of how it should work.

Learn more on the Gitcoin Issue Details page.

3) kevinkelley has been approved to start work.

I'd like to work on this.

I note that 'formatNumber' is called from 3 places: 1 in jul, 1 in codegen; and then in SMTChecker.

I'd probably go with changing the SMTChecker calls to 'formatNumberReadable'; then implement that as a new function, which which detects trailing zeroes (and trailing FF), and for those cases returns "0xSomenumber * 2^X" (or ... * 2^X - 1". ...Choice of whether to limit to multiple-succeeding-powers-of-two (2^8, 2^16, 2^32, ...) is your call; I think that since this is for human comparison of big numbers, just limiting it to multiples of 8 might be best (so that the exponent is a count of trailing zeroes in the hex representation).

This could be done for codegen too, as long as the emitted string is always a valid expression in yul or sol...

Learn more on the Gitcoin Issue Details page.

[ChrisCates]

Here is my suggestion as an implementation.

formatNumber(), now has an optional argument bool readable:

inline std::string formatNumber(bigint const& _value, bool readable = false)
{
    if (_value < 0)
        return "-" + formatNumber(-_value);
    else if (_value > 0x1000000 && readable == false)
        return toHex(toCompactBigEndian(_value), 2, HexPrefix::Add);
    else if (_value > 0x100000 && readable == true)
        return removeLeadingZeros(toHex(toCompactBigEndian(_value), 2, HexPrefix::Add));
    else
        return _value.str();
}
//Also applies to the overloaded method for u256

When readable = true for formatNumber(), it then invokes the removeLeadingZeros() function:

// Convenience function for removing leading zeros for large hex numbers for readability
inline std::string removeLeadingZeros(std::string hex)
{
    for (int i = hex.size(); i > 2; i--) 
    {
        if (hex[i] != "0") 
        {
            return hex.substr(0, i) + "  +  " + std::to_string(hex.size() - i) + " more zeroes";
        }
    }

    return hex;
}

If you have any feedback. Let me know.
If not, I'll submit a pull request with a proper solution.

[ChrisCates]

Also, can the CommonData.h (and all other files) use using namespace std...
The std:: prefix can be used if there are any conflicts in function declarations...

Saves time in the future, and, looks cleaner, since obviously the standard library is frequently used.

[leonardoalt]

@ChrisCates I don't think that solution does it.

I think we should rather go with @ekpyron 's suggestion (https://github.com/ethereum/solidity/issues/4648#issuecomment-409722658), also brought up by @KevinKelley (Solution 3 here: https://github.com/ethereum/solidity/issues/4648#issuecomment-425289955)

[ChrisCates]

@leonardoalt, makes sense... Since, all I'm doing is just truncating trailing zeros.

I've made some revisions that may be more preferable and work along the lines of what @ekpyron and Kevin proposed...

std::string formatNumberReadable(std::string hex) 
{
    for (int i = hex.size() - 1; i >= 2; i--) 
    {   
        if (std::strncmp(&hex[i], "0", 1) > 0) {
            if ((hex.size() - 1) % 2 != 0) i++;
            int superscript = ((hex.size() - i) / 2) * 8;
            return hex.substr(0, i + 1) + " * 2^" + std::to_string(superscript);
        }
    }

    return hex;
}

I've also written test cases...
Please verify that the following are correct...

formatNumberReadable("0x80000"); // Results in 0x8 * 2^16
formatNumberReadable("0x800000"); // Results in 0x80 * 2^16
formatNumberReadable("0x8000000"); // Results in 0x8 * 2^24
formatNumberReadable("0x80000000"); // Results in 0x80 * 2^24
formatNumberReadable("0x800000000"); // Results in 0x8 * 2^32

Please let me know if there are any issues with the solution I provided! 👍
If not, I assume we need to be accountable for adding flags for the optional argument bool readable when piping it into the command line... As well as allowing compilers to properly parse results.

[KevinKelley]

@ChrisCates ...another testcase for your code... that line if ((hex.size() - 1) % 2) != 0) i++; is suspect :)
BOOST_CHECK_EQUAL(formatNumberReadableChris("0x880000"), "0x88 * 2^16");
// yields 0x880 * 2^16; should be 0x88 * 2^16

I've got a prelim version working, slightly differently... I take a template parameter for the input value, accepting u256 or bigint; and I'm also handling the ...ffff cases.

[ChrisCates]

Feel free to share a gist @KevinKelley!

Also thanks for catching that!
I should have a reference counter for the number of zeros as opposed to checking the length of the string...

Since I actually use an inverse for loop. I can't simply just use int i.
Also, thanks for mentioning 0xf.. cases... Something that should also be accounted for.

[KevinKelley]

My pleasure... gist

...another possibility: underscore separators, maybe every 4 bytes; or dotted excisions. Usually when looking at these hashes it's enough to see the first 8, or first 4 and last 4, digits...

I guess I want to know, do we know exactly what we want? If so let's see some test cases and implement it; if not maybe let's experiment a little?

[ChrisCates]

@KevinKelley, hmm, these edge cases you're mentioning are very important... Seems that I underestimated the scope of the issue.

I'll look into providing some edits later.

[vs77bb]

@ChrisCates @KevinKelley I just approved you both to continue work on this bounty in a 'cooperative' fashion, as you've both already done regardless (love it!). Are either (or both) of you still interested in taking this forward?

[KevinKelley]

Excellent! Yes, I'll be glad to keep on.

[ChrisCates]

@vs77bb, absolutely, I wasn't sure what was going on with this specifically, hence why I didn't continue, but, thank you for following up.

Let's see if we can get a PR going this week.

Also this is a good time to discuss cases we need to account for, @KevinKelley, please let me know if I'm missing anything:

• [ ] 0 and f hexadecimal cases covered (the most essential, any other cases I'm missing, please let me know!).

• [ ] Compatibility with all Solidity Compilers which means properly parsing strings.

• [ ] (To discuss) How does it display? Be able to see the first 4 or 8 digits?

• [ ] (To discuss) Do we automatically flag bool readable = true if the output is intended for Command Line? Do we even need a flag if the output will be compatible with all compilers regardless, should this be the intended output for large hexadecimal values?

I think members of the Solidity Repository should discuss (once we finalize the objectives) as there are some things we should think about when implementing.

[chriseth]

I think the function should be split into two: One that generates numbers that do not have to be super readable, but are proper yul literals (mostly the same as solidity literals). This is basically the current behaviour. The other one generates numbers that are readable by humans without any further requirements.

[ChrisCates]

Hey there,
I pushed up some stuff (for debugging purposes): https://github.com/ChrisCates/solidity/tree/chriscates/hexreadable

I seem to running into problems with the formatNumberReadable() function.

It seems I get these errors:

/Users/cc/Projects/solidity/libdevcore/CommonData.h:143:29: error: no viable overloaded '>>='
        for (T v = _val; v; ++i, v >>= 8)
                                 ~ ^   ~
/Users/cc/Projects/solidity/libdevcore/CommonData.h:212:16: note: in instantiation of function template specialization
      'dev::toCompactBigEndian<boost::multiprecision::detail::expression<boost::multiprecision::detail::add_immediates,
      boost::multiprecision::number<boost::multiprecision::backends::cpp_int_backend<0, 0, boost::multiprecision::signed_magnitude, boost::multiprecision::unchecked,
      std::__1::allocator<unsigned long long> >, boost::multiprecision::et_on>, int, void, void> >' requested here
                return toHex(toCompactBigEndian(v + 1), 2, HexPrefix::Add) + " * 2^" + std::to_string(i * 8) + " - 1";
                             ^
/Users/cc/Projects/solidity/libsolidity/formal/SMTChecker.cpp:682:13: note: in instantiation of function template specialization
      'dev::formatNumberReadable<boost::multiprecision::number<boost::multiprecision::backends::cpp_int_backend<0, 0, boost::multiprecision::signed_magnitude,
      boost::multiprecision::unchecked, std::__1::allocator<unsigned long long> >, boost::multiprecision::et_on> >' requested here
                                value = formatNumberReadable(bigint(value));
                                        ^
In file included from /Users/cc/Projects/solidity/libsolidity/formal/SMTChecker.cpp:18:
In file included from /Users/cc/Projects/solidity/libsolidity/formal/SMTChecker.h:22:
In file included from /Users/cc/Projects/solidity/libsolidity/formal/SSAVariable.h:20:
In file included from /Users/cc/Projects/solidity/libsolidity/formal/SymbolicVariable.h:22:
In file included from /Users/cc/Projects/solidity/libsolidity/ast/AST.h:35:
In file included from /Users/cc/Projects/solidity/libdevcore/FixedHash.h:26:
/Users/cc/Projects/solidity/libdevcore/CommonData.h:105:43: error: no viable overloaded '>>='
        for (auto i = o_out.size(); i != 0; _val >>= 8, i--)
                                            ~~~~ ^   ~
/Users/cc/Projects/solidity/libdevcore/CommonData.h:147:2: note: in instantiation of function template specialization
      'dev::toBigEndian<boost::multiprecision::detail::expression<boost::multiprecision::detail::add_immediates,
      boost::multiprecision::number<boost::multiprecision::backends::cpp_int_backend<0, 0, boost::multiprecision::signed_magnitude, boost::multiprecision::unchecked,
      std::__1::allocator<unsigned long long> >, boost::multiprecision::et_on>, int, void, void>, std::__1::vector<unsigned char, std::__1::allocator<unsigned char> > >' requested here
        toBigEndian(_val, ret);
        ^
/Users/cc/Projects/solidity/libdevcore/CommonData.h:212:16: note: in instantiation of function template specialization
      'dev::toCompactBigEndian<boost::multiprecision::detail::expression<boost::multiprecision::detail::add_immediates,
      boost::multiprecision::number<boost::multiprecision::backends::cpp_int_backend<0, 0, boost::multiprecision::signed_magnitude, boost::multiprecision::unchecked,
      std::__1::allocator<unsigned long long> >, boost::multiprecision::et_on>, int, void, void> >' requested here
                return toHex(toCompactBigEndian(v + 1), 2, HexPrefix::Add) + " * 2^" + std::to_string(i * 8) + " - 1";
                             ^
/Users/cc/Projects/solidity/libsolidity/formal/SMTChecker.cpp:682:13: note: in instantiation of function template specialization
      'dev::formatNumberReadable<boost::multiprecision::number<boost::multiprecision::backends::cpp_int_backend<0, 0, boost::multiprecision::signed_magnitude,
      boost::multiprecision::unchecked, std::__1::allocator<unsigned long long> >, boost::multiprecision::et_on> >' requested here
                                value = formatNumberReadable(bigint(value));

I've made some modifications to the algorithm to cast to bigint (just so that other numbers don't need to be verbosely casted to the specified the template type). @KevinKelley, I'll be working on this tomorrow... I believe I may not be invoking it correctly to the SMTChecker Object.

[ChrisCates]

Also, I think I may modify the bool readable to the number of trailing
zeros you want in the readable format... Where zero specifies the normal
format.

[gitcoinbot]

@KevinKelley Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

@KevinKelley Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[KevinKelley]

(PR here)[https://github.com/ethereum/solidity/pull/5214], not intended for use, just to show work

I've added a little more to it; there are 4 features now.

• ends-in-zeroes shows as * 2^N
• ends-in-FFs shows as * 2^N - 1
• non-special hashes get truncated for display to 8(?) characters
• mixed-case Hex like 0xABCDabcd...

Haven't integrated yet; just added the formatNumberReadable and some tests to exercise it.

[KevinKelley]

@chriseth Yes, I agree that current behavior for yul and sol literals needs to be kept; this "human-readable" push is just to make error messages and such, be easier to understand. If we want to produce "pretty" code...I guess that would be another thing, but not likely useful I think? I mean normally you don't generate literal signatures into contracts very often.

I'm thinking this "readable" issue we're working on here, needs to be kept to the human-viewed output, not the code-generators.

Of course... now I'm wondering about tooling that might want to parse errors... editors and IDEs that take error output and grep it. Even so I think the readable version is best, in that case too...if the tooling is smart enough to pull error description out of the stdout dump, still it's going to be best if the message details are readable.

[KevinKelley]

@ChrisCates ...guessing that you're past the template error you had, by now. If not, I'd suggest refactoring to straight non-template function that takes bigint, make sure that works first...

Back to your checklist, yeah, that's about right. We can do the first couple cases easily, already working; and the third point about how many digits to display (and my suggestion of like 0xABCDabcd...) is still to be talked about. Final point is making sure that this "pretty" stuff doesn't break the codegen ...

[ChrisCates]

@KevinKelley, it was a very bizarre issue...
All I had to do to fix it was:

if (i > 2)
    {
        v++;
        return toHex(toCompactBigEndian(v), 2, HexPrefix::Add) + " * 2^" + std::to_string(i * 8) + " - 1";
    }

instead of:

if (i > 2)
        return toHex(toCompactBigEndian(v + 1), 2, HexPrefix::Add) + " * 2^" + std::to_string(i * 8) + " - 1";

I'm not sure why this caused an error... I'm using Mac OS Mojave with the LTS of LLVM and Clang...

Also, it works fine with a template now.
I'll look into getting everything integrated... As well as preparing some solidity smart contracts to validate the SMTChecker file.

[ChrisCates]

@chriseth I've noticed that there are some places where truncation is used in a way other then that we specified:

test.sol:3:16: Error: Type int_const 5789...(69 digits omitted)...9968 is not implicitly convertible to expected type uint16.
    uint16 a = 0x8000000000000000000000000000000000000000000000000000000000000000;
               ^----------------------------------------------------------------^
test.sol:4:16: Error: Type int_const 5789...(69 digits omitted)...9968 is not implicitly convertible to expected type uint16.
    uint16 b = 0x8000000000000000000000000000000000000000000000000000000000000000;
               ^----------------------------------------------------------------^

Do you want the same implementation done for large numbers specified in the error message?

Type int_const 5789...(69 digits omitted)...9968

Should be:

Error: Type int_const 0x8 * (2 ^ N) is not implicitly convertible to expected type uint16.

Or even we can drop the hex prefix altogether for error messages for formality.
If not, I won't bother changing these messages.

[leonardoalt]

@KevinKelley You are right that this feature will be used only for humans, and not in code generation. I'm not sure though, about non-special hashes get truncated for display to 8(?) characters. These values are output by the SMTChecker when a counterexample is found for a failed assertion, so it still needs to be precise when telling the developer which exact values break the assertion.

[KevinKelley]

@leonardoalt So... can we tell, when do we need the precise value, and when do we just need to know what it looks like? Sounds like you're saying, sometimes the humans need to see all the bits; and that makes sense.

I'm wishing for a tool output page that has abbreviated values you can click on for full info when you need it...this is really a display issue, where you'd like to see the pretty version for quick understanding, but have available the details.

But we're dealing with console output here, and I'm not sure quite how to make it great... should there be an API access point with full info, separate from the console display? Or that the console display is abbreviated from?

Another thing to consider... the 2^N (and 2^N-1) truncation... it's cool, but how likely is that? I mean I'm glad to write the code, but you guys know how often those will happen, outside of simple testing situations.

Nicknames for signatures (the 0xabcd.(skipsome).dbca idea)? I guess the sig is already a nickname, we're just talking about dropping some bits so it's easier to recognize...question is, when do you need to get back to the bits?

I don't really know. I'll take some time looking at what SMTSolver is doing, anyway.

[leonardoalt]

@KevinKelley I think the other features are great as they are, and 2^n and 2^(n-1) are very likely in our scenario.
Developers will always need all the bits when a counterexample is found, but H*2^n and H*2^(n-1) are not abstractions or truncated values, they still contain all the bits, so also good.

[KevinKelley]

@leonardoalt Okay, true, 2^N truncations are still perfectly accurate. Question for others is, do we want a display mode that does truncate some bits, in the interest of being quickly recognizable?

I'm taking it from this, that we need to keep the two sides separated, if we do it at all... accurate vs. readable...

[gitcoinbot]

@ChrisCates Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

@ChrisCates Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

@KevinKelley Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

@KevinKelley Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

---

@ChrisCates due to inactivity, we have escalated this issue to Gitcoin's moderation team. Let us know if you believe this has been done in error!

• [x] warning (3 days)
• [x] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

---

@ChrisCates due to inactivity, we have escalated this issue to Gitcoin's moderation team. Let us know if you believe this has been done in error!

• [x] warning (3 days)
• [x] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

---

@KevinKelley due to inactivity, we have escalated this issue to Gitcoin's moderation team. Let us know if you believe this has been done in error!

• [x] warning (3 days)
• [x] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

---

@KevinKelley due to inactivity, we have escalated this issue to Gitcoin's moderation team. Let us know if you believe this has been done in error!

• [x] warning (3 days)
• [x] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[ChrisCates]

Hey,

This reminder was helpful.
Im going to push a more complete PR with test outputs to check later today
or tomorrow.

Sorry, for the delays! I know this isnt top priority stuff, but still nice
to have it done in a timely manner.

[rmshea]

@ChrisCates Thanks for the update! I've snoozed @gitcoinbot for 3 days. Let me know if you have any questions with this. I'm here to help 😸 🔨

[rmshea]

@KevinKelley are you still working on this? Let me know! 👍

[KevinKelley]

Yep, I've redone my prev submit according to the comments I got. I ran into some github issues (lack of knowledge, lol) when I tried to re-submit the PR, so had to work that out. Then I decided to clean up a little more, before resubmitting.

Current features are

• ends-in-zeroes shows as x * 2**N
• ends-in-FFs shows as x * 2**N - 1
• non-special hashes get truncated for display to 8(?) characters
• mixed-case Hex like 0xABCDabcd0987fedc

I'd like to hear feedback on the mixed-case idea, and on truncation. Mixed case seems to me fine, helps readability but doesn't break anything. Truncation... nice for human reader to differentiate between hashes, but deletes info about what the hash actually is... and it sounds like some people need that full hash in some situations.

downside of the mixed-case, is that it only applies to the a..f, so doesn't always actually help. An underscore every 4 chars would always work, but adds 25% to the length... and breaks the interpreters

So I'm not sure if that one should be done... or if we should try to find a way to toggle it

[leonardoalt]

@KevinKelley In my opinion the accurate case should be default.
What exactly is the question about the mixed-case?

[KevinKelley]

@leonardoalt to me it seemed like it helps...
0xAAAAAAAAAAAAAAAABAAAAAAAAAAAAAAAAAAAAAAA
vs
0xAAAAaaaaAAAAaaaaBAAAaaaaAAAAaaaaAAAAaaaa

When the hex is long, you have to chunk it to compare; having detectable chunk boundaries helps me do that.

[edit]
...err...guess I didn't actually answer you. My question is, is this idea worth including?

Similar question about the various truncation ideas:
0x01234567...
0x0123...+N+...CDEF

[leonardoalt]

Ah ok I see now.
I think those 2 features do make it much more human-readable.
I would suggest an extension of what @chriseth suggested, that is, that we have 2 functions:
1- One that generates numbers that do not have to be super readable, but are proper yul literals (mostly the same as solidity literals). This is basically the current behaviour. So we keep it.
2- A new function that formats the number into a human-readable but still accurate representation, with a flag to toggle truncation and mixed-case. This function will then be used by the SMTChecker in the accurate mode, and other modules might use it with the "super-readable" mode on.

[KevinKelley]

Sounds good to me... I'm on it.

[gitcoinbot]

@ChrisCates Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

@ChrisCates Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[ChrisCates]

I really hate that I didn't mention anything til now.
I've been having really severe dishydrotic eczema past couple weeks, last
week was awful, this week has gotten relatively worse... Sleeping has also
gotten a lot worse.

Really hate using excuses, but, it is what it is.

If my hands aren't balloons later down the line, and I see where I can
contribute... I'll be happy to do a PR.

Also, I didn't really contribute any useful commits. So Kevin should most
definitely receive the bounty considering he did majority of the actual
work in terms of implementation.

Any, sorry about the inconvenience.

[gitcoinbot]

@KevinKelley Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[KevinKelley]

4 features implemented:

• ends-in-zeroes
• ends-in FFs
• alternating-case
• internal truncation

See what you think of the truncation examples below...

0x80000000000: 
    0x08 * 2**40

0x7ffffffffff: 
    0x08 * 2**40 - 1

0xAAAAaaaaAAAAaaaaFFFFffffFFFFffffFFFFffffFFFFffffFFFFffffFFFFffff:
    0xAAAAaaaaAAAAaaab * 2**192 - 1

0x5555555555555555555555555555555555555555555555555555555555555555:
    0x5555...{+56 more}...5555

0xabcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789:
    0xABCD...{+56 more}...6789

I'm satisfied with it, myself, but welcome input.

I'm working now on a proper way to make this switchable, so that the truncation can be turned off when full output is needed

[gitcoinbot]

@ChrisCates Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

@ChrisCates Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

@KevinKelley Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[KevinKelley]

As far as usages of this: there are 3 places, currently, where the formatNumber function is called.

In solidity codegen ExpressionCompiler, it's used for error messages. This, I'll change to use formatNumberReadable, but make it switchable by runtime flag.

In formal/SMTChecker, it's used twice, to format a message saying Underflow, less than minValue or greater than maxValue for a type... so the output will only be either 0 or 0x01 * 2**256 - 1... to me this seems fine. If the actual value is decided to be shown, it should also be subject to the runtime flag for accurate output, in case of need.

The third usage is in yul... to build an assembly Literal. This should never use abbreviated output; I'm leaving it to continue to use the original formatNumber function.

[gitcoinbot]

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

---

@ChrisCates due to inactivity, we have escalated this issue to Gitcoin's moderation team. Let us know if you believe this has been done in error!

• [x] warning (3 days)
• [x] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

---

@ChrisCates due to inactivity, we have escalated this issue to Gitcoin's moderation team. Let us know if you believe this has been done in error!

• [x] warning (3 days)
• [x] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[rmshea]

Hey @KevinKelley, Ryan from Gitcoin here! What is the status of this bounty? Can I be of any assistance with payout / admin? Wanted to check in to make sure 🌮 😄 💯

[gitcoinbot]

@KevinKelley Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

@KevinKelley Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

---

@KevinKelley due to inactivity, we have escalated this issue to Gitcoin's moderation team. Let us know if you believe this has been done in error!

• [x] warning (3 days)
• [x] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

---

@KevinKelley due to inactivity, we have escalated this issue to Gitcoin's moderation team. Let us know if you believe this has been done in error!

• [x] reminder (3 days)
• [x] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[ChrisCates]

Hi @ryan-shea,
Sorry about a while back...

I've integrated --hex-readable into the SMTChecker with a flag.

Here is an example output from a test contract:

test.sol:

pragma experimental SMTChecker;

contract test {
    uint128 a = 0x8000000000000000000000000;
    uint128 b = 0x8000000000000000000000000;
    uint128 c = 0;

    constructor() public {
        c = a * b;
    }
}

output:

$ ./solc/solc ./test.sol --hex-readable

Warning: This is a pre-release compiler version, please do not use it in production.
./test.sol:1:1: Warning: Source file does not specify required compiler version!
pragma experimental SMTChecker;
^ (Relevant source part starts here and spans across multiple lines).
./test.sol:8:5: Warning: Assertion checker does not yet support constructors and functions with modifiers.
    constructor() public {
    ^ (Relevant source part starts here and spans across multiple lines).
./test.sol:9:13: Warning: Overflow (resulting value larger than 0x01 * 2**128 - 1) happens here
        c = a * b;
            ^---^
  for:
  <result> = 0x01 * 2**128
  a = 2
  b = 0x80 * 2**120
  c = 0


./test.sol:9:9: Warning: Overflow (resulting value larger than 0x01 * 2**128 - 1) happens here
        c = a * b;
        ^-------^
  for:
  <result> = 0x01 * 2**128
  a = 2
  b = 0x80 * 2**120
  c = 0



======= ./test.sol:test =======

Also, the command line interface was updated with a --hex-readable flag:

$ ./solc/solc --help

...
Allowed options:
    --hex-readable       Output hex in a readable format when using the SMT Checker.
...

I've provided the pull request here: https://github.com/ethereum/solidity/pull/5447

I've tried to followed @chriseth's style requests that were originally asked for from @KevinKelley. @chriseth, let me know if there are any style issues in regards to the code provided on the Pull Request itself. The tests and output seem to be in good order otherwise.

[gitcoinbot]

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

---

__Work for 425.0 DAI (425.0 USD @ $1.0/DAI) has been submitted by__:

1. @chriscates

@vs77bb please take a look at the submitted work:

• PR by @ChrisCates

---

• Learn more on the Gitcoin Issue Details page
• Want to chip in? Add your own contribution here.
• Questions? Checkout Gitcoin Help or the Gitcoin Slack
• $53,133.56 more funded OSS Work available on the Gitcoin Issue Explorer

[gitcoinbot]

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

---

__Work for 425.0 DAI (425.0 USD @ $1.0/DAI) has been submitted by__:

1. @chriscates
2. @kevinkelley

@vs77bb please take a look at the submitted work:

• PR by @KevinKelley
• PR by @ChrisCates

---

• Learn more on the Gitcoin Issue Details page
• Want to chip in? Add your own contribution here.
• Questions? Checkout Gitcoin Help or the Gitcoin Slack
• $38,273.41 more funded OSS Work available on the Gitcoin Issue Explorer

[ChrisCates]

Im going to add more tests and get full codecov on CommonData.h,
CommonData.cpp...

The CI check failing is really bugging me.

Im just unsure if improving codecov should be on this Pull Request.

[KevinKelley]

@ChrisCates ...looking at your PRs, seems you started from where I left off, added the command-lind switching that I hadn't got to. I approve, looking good to me...

I got sidetracked, or bogged down, with the options switching. I got the idea that we'd maybe want more options to be switchable, since there's code to make it possible... so I wrote up a HexFormat class, like:

enum class HexFormat
{
    ShowLeadingOx = 1,
    UseMixedCase = 2,
    ShowFormulaicValues = 4,
    UseInternalTruncation = 8
};

where each is independently selectable. But then that started to seem too bulky and over-engineered... so I stewed for a while.

Anyway my feeling now is that the situation as in @ChrisCates PR is probably best option... Except, it looks like the code for truncation is doing the first way
`0xABCD...
rather than my latest:
0xABCD...{+56 more}...6789

Let me know if you want that bit

[ChrisCates]

@KevinKelley, there are plenty of great refactoring methods we could implement into the standard library, and I am definitely in favour of a Hex Class, however, I think it should be agnostic to any numerical value. This way you can tune the parameters of the class and use it for any decimal value, or any integer. You can either return the original decimal value or return different versions through other function calls.

This type of formatting would be very valuable for several other parts of the codebase, and for other datatypes, more specifically the syntax parsing itself. For the time being, this is out of scope (atleast the other structs/classes we could be creating), and, may be better to open a new issue for discussion.

[KevinKelley]

Okay, I've combined @ChrisCates code (command-line switching) and mine (4 types of formatting) into one PR

I think there's still stylecheck issues, I'll do the fixups if/when anybody wants to use this.

[KevinKelley]

Hey @KevinKelley, Ryan from Gitcoin here! What is the status of this bounty? Can I be of any assistance with payout / admin? Wanted to check in to make sure

@ryan-shea ...I'm thinking this should be resolved, finished, now... but haven't heard anything after my last series of PR/fixes. Anyone? Are we done?

[leonardoalt]

Done in #5476

[rmshea]

hey @vs77bb, looks like this one is ready to be reviewed

[KevinKelley]

@ryan-shea @vs77bb yes, can this be reviewd/closed/bounty decided and paid? been a while..

[rmshea]

@KevinKelley on it ! will get paid by EOW

[KevinKelley]

@ryan-shea good to hear, thanks!

[gitcoinbot]

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

---

__The funding of 425.0 DAI (425.0 USD @ $1.0/DAI) attached to this issue has been approved & issued to @KevinKelley.__

• Learn more on the Gitcoin Issue Details page
• Questions? Checkout Gitcoin Help or the Gitcoin Slack
• $53,032.10 more funded OSS Work available on the Gitcoin Issue Explorer