Fixing missing concKeccakSimpExpr for wordToAddr, maybeLitByte, etc.

[msooseth]

Description

It turns out that as per #618 we ran simplify instead of run concKeccakSimpExpr on wordToAddr. Furthermore, we should run concKeccakSimpExpr on maybeLitByte, maybeLitAddr etc. so more things can run concretely.

Also added hexStringToByteString to test.hs, which makes it a LOT easier to create ConcreteBuf-s via e.g. ConcreteBuf (hexStringToByteString "0a0056"). It's been really painful to try to debug without this.

Added a test case to verify that indeed the caase in #618 is fixed.

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[blishko]

Are you sure the maybe methods are the place where simplification should happen?
Shouldn't these methods stay trivial, and shouldn't the simplification happen in somewhere else?

[msooseth]

@blishko Hmmmm I found it cleaner this way. I would need to add it to, at least:

• forceConcrete
• forceConcrete2
• OpSstore
• OpReturn
• precompiledContract
• decodeBuf
  ...

And that's just EVM.hs and maybeLitWord. I do see your point, though, i.e. to be more explicit in its use. However, these maybe... functions either force the execution to error out or to do something less convenient when they return a Nothing, so I think we'd need to put the concKeccakSimp almost all the places they are used.

But maybe I'm wrong. I just see it to be a larger diff, and hence more clutter. But it's not such a big deal, I can be convinced the other way. If you think it's better, I'll adjust this PR to use concKeccakSimp almost everywhere -- I think there'd be 2-3 places where it wouldn't be needed -- in Format.hs for example, though still maybe nice to output the concrete value, too, if possible.

[blishko]

I see your point. I don't know the codebase well enough, but my opinion is that you are quite drastically changing the meaning of these functions. Maybe you can introduce a new functions where it would be explicit that they are applying simplifications first? maybeLitWordAfterSimpl?

Having a quick look at forceConcrete for example, I think it would be good to see explicitly that it is trying to simplify the expression before trying to extract the concrete value, if that it what it is supposed to do.

But I do not want to force my viewpoint onto you. Feel free to ignore me :)

[msooseth]

Yeah, renaming of the functions is a very good idea, actually, thanks! Misleading without it.

forceConcrete is definitely a good place where we really ought to try to simplify as much as possible. In fact, it should even try to run an SMT solver. For example at wordToAddr @d-xo wrote:

-- TODO: make this smarter, probably we will need to use the solver here?
wordToAddr :: Expr EWord -> Maybe (Expr EAddr)
wordToAddr e = case (concKeccakSimpExpr e) of
[...]

And I actually agree with this idea In fact, we'd need that here: #581 In order to remove that symbolic jump issue, we'd need to run an SMT solver, and get out all possible jump destinations, and explore the execution with all. That's a bit of a more involved case. For that to work, we will need to rewrite some of the places where these functions are used, because if the number of solution is limited (like in #581 where it's limited to the number of functions in the contracts), then we should try all -- and of course in these cases neither simplify, nor concKeccakSimpExpr will be able to get out a single concrete value, since there are multiple possible concrete values.

Let me rename the functions, let's see if that helps :)

[msooseth]

@blishko I renamed them. I had a look, I didn't see a reason why I would use a non-simplified version of the functions in the places where it's being used, so I left them-as is. Even at the formatting, it seems like it's used to print some kind of visual clue/information to the user, and so if we have a Just, we print more concrete information, which I think is more valuable. I'm actually thinking about printing a simplified version even during formatting, like this?

      , "arguments: "
      , indent 2 $ T.unlines . fmap formatSomeExpr $ args
+      , "simplified arguments: "
+      , indent 2 $ T.unlines . fmap formatSomeExprSimp $ args

Where formatSomeExprSimp calls Expr.concKeccakSimpExpr on the argument first.

What do you think?

[blishko]

I guess also maybeLitByte should have the Simp suffix?

[msooseth]

It's about holidays time, but when you are back, I'd be grateful for a review, @blishko :) Happy holidays in the meanwhile!

[msooseth]

I guess also maybeLitByte should have the Simp suffix?

Yesss, thanks, I added it! Can you perhaps review in the coming days? Also, if you could review #625 that's on top of this that'd be nice :)

[blishko]

Seems OK now. Although, you might need to rebase to resolve the conflicts.

[msooseth]

Thanks! Resolved the conflicts, thankfully they were quite minimal :)