We use the function name and types only to construct this signature, Wouldn't it be better to take signature directly?
I was looking at the users of this function, and basically the only user is symRun, which constructs the signature anyway.

I am not 100% sure I understand what you are saying, I'm sorry.

We actually don't really get a calldata from the SMT solver, because we try to minimize each part of the calldata. So we get chunks of the calldata (i.e. the values for the types), and that's why I am using this function to re-assemble it. Also, we may want to, in the future, rewrite the Cex in other ways, not just minimize it, so I thought it'd best to re-assemble it from the Cex, rather than try to pass it from the SMT solver directly. I find this somewhat cleaner, plus it helps to essentially fuzz our de- and re-construction of the calldata from the types + values.

Is this what you were referring to? Or is there some place where symRun has the calldata that I don't see? I think it's only reconstructing a pretty calldata here:

        txtFails <- symFailure opts testName (fst cd) types toPrintData

which calls:

      mkMsg conf (leaf, cex, repro) = intercalate "\n" $
        ["Counterexample:   " <> reproToText repro
        ,"  calldata: " <> let ?context = dappContext (traceContext leaf)
                           in prettyCalldata cex cd testName types
        ,"  result:   " <> showRes leaf
        ] <> verbText conf leaf

But I think that doesn't actually give us a raw calldata? Or am I missing something? Sorry, I am a bit confused.

My comment related to this code:

It will be great to have two functions:

• A function to transform a CEX into a high-level solidity call (e.g. f(1,2,3)).
• A function to transform a high-level solidity call into calldata to run the transaction and verify the result.

So the user will be able to see the values in the call, and then debug an invalid CEX if necessary. Echidna already have the code for these two can that can be easily adapted or even re-used here if necessary.

Hi,

The A function to transform a CEX into a high-level solidity call (e.g. f(1,2,3)). is already available, it's called prettyCallData, it's called in symFailure like this: prettyCalldata cex buf funName types. It returns a text that does what you want, I think!

The A function to transform a high-level solidity call into calldata to run the transaction and verify the result. that's what I wrote, I think, i.e. calldataFromCex cex buf funName types.

At least as far as I can understand, that's what they do. However, it may be that I am misunderstanding what you mean, or that you need something more specific/etc.

I had a second look and instead of taking Text and [AbyType], I think this method should be taking Sig.
And we should have a method to convert this to the text representation of a signature. Not sure if Show does that for Sig or not.
We should not have to repeat code like (funName <> "(" <> T.intercalate "," (map abiTypeSolidity types) <> ")")

I had a second look and instead of taking Text and [AbyType], I think this method should be taking Sig.
And we should have a method to convert this to the text representation of a signature. Not sure if Show does that for Sig or not.
We should not have to repeat code like (funName <> "(" <> T.intercalate "," (map abiTypeSolidity types) <> ")")