Support bytes concat #14685

pgebal · 2023-11-17T10:40:10Z

Closes #11997

pgebal · 2023-11-28T11:09:50Z

test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol

@@ -28,7 +28,7 @@ contract C
 	}
 	function g(uint x) public {
 		require(x < severalMaps.length);
-		f(severalMaps[x]);
+		f(severalMaps[x]); //should hold


This shouldn't be reported. I don't know how to fix it.

pgebal · 2023-11-29T12:23:05Z

test/libsolidity/smtCheckerTests/functions/getters/array_2.sol

 // ----
-// Warning 6328: (242-256): CHC: Assertion violation happens here.\nCounterexample:\na = [[], [], [0, 0, 0, 0]]\ny = 0\n\nTransaction trace:\nC.constructor()\nState: a = [[], [], [0, 0, 0, 0]]\nC.f()
+// Warning 6328: (242-256): CHC: Assertion violation happens here.


I don't know why no counterexample here

libsolidity/formal/PredicateInstance.cpp

pgebal · 2023-11-30T16:18:02Z

Explanation on 1 argument bytes.concat call:

If the argument is of type bytes memory: bytes.concat call is defined as value of the argument.
If the argument is of other type: fixed bytes, etc, bytes.concat is defined as a function (just as 2+ arguments calls)

Maybe it could be done differently, but I would have to cast values of types fixed bytes, string literals to values of type bytes memory

r0qs · 2023-11-30T16:52:25Z

Explanation on 1 argument bytes.concat call:
1. If the argument is of type `bytes memory`: `bytes.concat` call is defined as value of the argument.

2. If the argument is of other type: fixed bytes, etc, `bytes.concat` is defined as a function (just as 2+ arguments calls)
Maybe it could be done differently, but I would have to cast values of types fixed bytes, string literals to values of type bytes memory

Hey @pgebal the two tests failing seems to be due to out of memory in the CI jobs: https://app.circleci.com/pipelines/github/ethereum/solidity/31908/workflows/a54b0a16-fb08-4f77-989d-13a1bebba3b2/jobs/1425767/resources. If there is no memory leak in the current implementation, and the memory increase is expected, you may need to increase the resource_class of the job, which, by the way, is already using a large image, i.e. base_ubuntu2204_large.

pgebal · 2023-12-01T13:57:20Z

@r0qs Thanks, I noticed that too. I am not sure about the memory increase caused by my changes. I asked @leonardoalt to have a look on this code. Maybe he can find something suspicious here. If Leo thinks it seems right I'll increase resource class to see if that helps.

libsolidity/formal/SMTEncoder.cpp

blishko

I think this looks good!

Left just a few small comments, but I think this should be soon good to go!

Also, it looks like this PR needs rebase.

libsolidity/formal/CHC.cpp

libsolidity/formal/CHC.h

libsolidity/formal/Predicate.cpp

blishko · 2024-01-22T13:57:42Z

libsolidity/formal/Predicate.cpp

@@ -381,7 +384,7 @@ std::vector<std::optional<std::string>> Predicate::summaryPostInputValues(std::v

 	auto const& inParams = function->parameters();

-	auto first = _args.begin() + 6 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
+	auto first = _args.begin() + (long)firstArgIndex() + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;


Why do you need to cast to long?

because return type of firstArgIndex() is size_t (which seemed to me it makes most sense)
and operator + for iterator takes long as an argument

Since the other offsets use static_cast<int> maybe we should at least be consistent with that?
In general, we should prefer static_cast from C++ to C-style casts.

Right! It's being used in the same line and I didn't notice it!

libsolidity/formal/Predicate.h

blishko

LGTM!

blishko · 2024-01-23T14:55:11Z

@pgebal You have to update test expectations for the test where you changed the indentation.
Also you can now update the main description of the PR again, since the test is no longer deleted.

pgebal force-pushed the pgebal/bytes_concat branch 3 times, most recently from 4a80492 to effab73 Compare November 17, 2023 14:13

cameel added the smt label Nov 19, 2023

pgebal force-pushed the pgebal/bytes_concat branch 7 times, most recently from be52960 to 9e713cb Compare November 22, 2023 17:28

pgebal force-pushed the pgebal/bytes_concat branch 3 times, most recently from f5270cd to 4528fcc Compare November 28, 2023 10:58

pgebal commented Nov 28, 2023

View reviewed changes

pgebal force-pushed the pgebal/bytes_concat branch 5 times, most recently from 6cd0cc1 to ba2959e Compare November 29, 2023 11:40

pgebal commented Nov 29, 2023

View reviewed changes

pgebal marked this pull request as ready for review November 29, 2023 12:29

pgebal requested a review from leonardoalt November 29, 2023 12:29

blishko reviewed Nov 30, 2023

View reviewed changes

libsolidity/formal/PredicateInstance.cpp Outdated Show resolved Hide resolved

blishko reviewed Dec 3, 2023

View reviewed changes

libsolidity/formal/SMTEncoder.cpp Outdated Show resolved Hide resolved

libsolidity/formal/SMTEncoder.cpp Outdated Show resolved Hide resolved

pgebal force-pushed the pgebal/bytes_concat branch 2 times, most recently from 691a920 to e21eab9 Compare December 4, 2023 11:33

pgebal force-pushed the pgebal/bytes_concat branch 14 times, most recently from f535a42 to 0992050 Compare January 18, 2024 09:26

blishko reviewed Jan 22, 2024

View reviewed changes

pgebal force-pushed the pgebal/bytes_concat branch 3 times, most recently from da5b178 to 4585079 Compare January 23, 2024 14:04

blishko previously approved these changes Jan 23, 2024

View reviewed changes

Support bytes concat

a8d6a44

pgebal dismissed blishko’s stale review via a8d6a44 January 23, 2024 16:12

pgebal force-pushed the pgebal/bytes_concat branch from 4585079 to a8d6a44 Compare January 23, 2024 16:12

pgebal requested a review from blishko January 23, 2024 16:13

blishko approved these changes Jan 23, 2024

View reviewed changes

pgebal merged commit ce98680 into ethereum:develop Jan 24, 2024
65 checks passed

aarlt pushed a commit that referenced this pull request Jan 25, 2024

Support bytes concat in formal verification (#14685)

47a63f9

Ruko97 pushed a commit to Ruko97/solidity that referenced this pull request Apr 7, 2024

Support bytes concat in formal verification (ethereum#14685)

f7e1315

Ruko97 pushed a commit to Ruko97/solidity that referenced this pull request Oct 20, 2024

Support bytes concat in formal verification (ethereum#14685)

9e2cfe7

Ruko97 pushed a commit to Ruko97/solidity that referenced this pull request Oct 20, 2024

Support bytes concat in formal verification (ethereum#14685)

2086267

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support bytes concat #14685

Support bytes concat #14685

pgebal commented Nov 17, 2023 •

edited

Loading

pgebal Nov 28, 2023

pgebal Nov 29, 2023

pgebal commented Nov 30, 2023 •

edited

Loading

r0qs commented Nov 30, 2023 •

edited

Loading

pgebal commented Dec 1, 2023

blishko left a comment

blishko Jan 22, 2024

pgebal Jan 22, 2024

blishko Jan 22, 2024

pgebal Jan 22, 2024

blishko left a comment

blishko commented Jan 23, 2024

Support bytes concat #14685

Support bytes concat #14685

Conversation

pgebal commented Nov 17, 2023 • edited Loading

pgebal Nov 28, 2023

Choose a reason for hiding this comment

pgebal Nov 29, 2023

Choose a reason for hiding this comment

pgebal commented Nov 30, 2023 • edited Loading

r0qs commented Nov 30, 2023 • edited Loading

pgebal commented Dec 1, 2023

blishko left a comment

Choose a reason for hiding this comment

blishko Jan 22, 2024

Choose a reason for hiding this comment

pgebal Jan 22, 2024

Choose a reason for hiding this comment

blishko Jan 22, 2024

Choose a reason for hiding this comment

pgebal Jan 22, 2024

Choose a reason for hiding this comment

blishko left a comment

Choose a reason for hiding this comment

blishko commented Jan 23, 2024

pgebal commented Nov 17, 2023 •

edited

Loading

pgebal commented Nov 30, 2023 •

edited

Loading

r0qs commented Nov 30, 2023 •

edited

Loading