-
Notifications
You must be signed in to change notification settings - Fork 48
Called Contract and Executing Contract Example #162
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Called Contract and Executing Contract Example #162
Conversation
CVLByExample/Summarization/CalledContractAndExecutingContract/README.md
Outdated
Show resolved
Hide resolved
...ple/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.spec
Outdated
Show resolved
Hide resolved
| ### `executingContract` | ||
| - Represents the address of the contract that is *actually executing* the code. | ||
| - For **internal** and **delegate** calls, this will be the same as `calledContract`. | ||
| - For **external** calls, it will be the address of the caller (since the receiving contract code runs *there*), while `calledContract` is the address of the receiver. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure this is correct? The request was to see the caller, and it indeed only differs from calledContract on external calls that are not delegate, but I'm not sure if this "actually executing" and "code runs there" is an accurate description of the situation. Isn't it rather that in the delegate call case, the calledContract is the caller for this reason, since it's actually executed in the context of the caller? For normal external calls, they are different exactly because one calls and one is called without any shenanigans about the call context.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, now that I'm thinking about it (and after reading a little bit more on the subject) I think that a better description of the situation would be the "contract that initiated the call", or the "contract who executed the call". Also I think the whole "(since the receiving contract code runs there)" is wrong and we should delete it and simplify the explanation.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I like it much better already now. This is really a bit of a tricky concept, so I think it's valuable for us to figure out how to make it really clear 😊
| ### Additional Notes on the Keywords | ||
|
|
||
| - **`calledContract`** is only valid within the `methods` block (i.e., inside function summaries). It is essentially `address(this)` in the context of the original call you are summarizing. | ||
| - **`executingContract`** is also only valid within the `methods` block (and in certain hook bodies) and distinguishes the actual execution context when calls involve libraries or delegate calls. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Here we also still speak about "actual execution context". Maybe just something like "represents the caller of the original call you are summarizing"?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Or maybe just no further details here if you like my idea about how to change the section above?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I changed it to your suggestion. It seems clearer.
CVLByExample/Summarization/CalledContractAndExecutingContract/README.md
Outdated
Show resolved
Hide resolved
| ### `calledContract` | ||
| - Represents the address of the contract on which the summarized method was called. | ||
| - For **internal calls**, `calledContract` is the same as the contract containing the function (i.e., “this”). | ||
| - For **library calls** and **delegate calls**, `calledContract` can be the contract *initiating* the code execution (since libraries and delegate calls run in the caller’s context). |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We said that it's always "this", the point being that "this" is surprising in delegate calls... I wonder if we can make that clearer by pulling the hint about that up to the first point here.
Also, for non-delegate external calls, we can maybe mention them in the second point of just being the one containing the function as well? How about something like:
- Represents the address of the contract on which the summarized method was called, or more precisely in whose context it runs. It is essentially `address(this)` in the context of the original call you are summarizing.
- For **internal calls**, and non-delegate **external calls** `calledContract` is the same as the contract containing the function.
- For **library calls** and **delegate calls**, `calledContract` is the contract *initiating* the code execution (since libraries and delegate calls run in the caller’s context).
And maybe then in the Additional Notes section we don't need to mention what each of them means again, and only mention their validity constraints?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes I actually agree
| "Primary:secondary=Secondary", | ||
| "Primary:tertiary=Tertiary" | ||
| ], | ||
| "process": "emv", |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
| "process": "emv", | |
| "Primary:tertiary=Tertiary" | ||
| ], | ||
| "process": "emv", | ||
| "solc": "solc8.0", |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
| "solc": "solc8.0", | |
| contract Secondary { | ||
| // the `callee` methods are summarized | ||
|
|
||
| function calleeExternal() external { } |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
name is kind of misleading, why "callee"? it's just a externalFunction and internalFunction, no?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just to represent that these are the functions the examples are calling and look at what happen when they are called.
christiane-certora
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thank you!
No description provided.