Early multi-solutions system

[msooseth]

Description

Making progress towards symbolic jumpdestinations via SMT solving. This PR allows us to branch out to all potential jumpdests.

The system can restrict the returned value's number of relevant bytes to a fixed value. So if we are looking for a JUMP, it ignores high bytes, because it's impossible to have a PC that's more than 2^16 (more than 65K instructions). Similarly for addresses. This matters, because it can happen that there's some junk that's not restricted and we could get thousands of solutions, but they are actually all the same address if we ignore the bits other than the 160b that an address has.

Currently, it launches a new query for each new solution, which is very slow. This needs to be improved in a new PR. That will require a slight re-engineering of Solvers.hs, so we can query the system for more than one solution at a time.

Number of potential concrete is set to 10 by default. This is actually kinda low. However, we need to be a bit cautious, as things can blow up quickly, so I set 10. It can be changed via --max-branch K.

Currently, it does NOT use incremental solving to get multiple solutions. This is not optimal. Hence, it's called "early", as a next PR will fix that.

Checklist

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

[blishko]

I don't understand why this function needs an argument that you are then ignoring anyway?

[msooseth]

Let me make it a BIT more sane, but it's basically that we use this function here, above:

delegateCall this gas xTo' xTo' (Lit 0) xInOffset xInSize xOutOffset xOutSize xs fallback $

where delegateCall-s last argument is a function of the type: (Expr EAddr -> EVM t s ()). But we don't need the first argument. I wanted to be able to pass this function to delegateCall and also use it here:

False -> fallback undefined
and here:
Nothing -> fallback undefined

But yeah, it's annoying. I'll make a helper function strip1st :: (x) ->(a->x) that makes a Monadic function that takes no arguments into a Monadic function that takes 1 argument, and ignores it. Then it will be maybe cleaner!

[msooseth]

aaaah, there is a built-in function for this! https://hackage.haskell.org/package/base-4.21.0.0/docs/Prelude.html#v:const

[msooseth]

Ha nice, OK, it's fixed now, using const. Thanks, this was useful. I tried figuring out this function, I also didn't like it, but I couldn't find it. I now used LLMs because, why not. It told me about const. Can you check if it's better now?

[blishko]

Can you explain this a bit? I just probably don't understand choose and PleaseChoosePath, but what does the parameter leftOrRight represents and where is it actually passed in?

For the case of 2, if leftOrRight is false, isn't this just ignoring the first value? I don't see where the "we run both" from the comment actually happens.

[msooseth]

Yeah, sorry. It's actually not CHOOSING anything. It's running both. It USED to be choosing things, because there was a debugger! But no longer. Let me rename that thing and then it'll be lot easier to understand :)

[msooseth]

Yay, OK, it should be a lot cleaner now, renamed all relevant functions and datatypes. Can you re-review?

[msooseth]

BTW, I also added a test:

+     , test "symbolic-to-concrete-multi" $ do
+        Just c <- solcRuntime "MyContract"
+            [i|
+            interface Vm {
+              function deal(address,uint256) external;
+            }
+            contract MyContract {
+              function fun(uint160 a) external {
+                Vm vm = Vm(0x7109709ECfa91a80626fF3989D68f67F5b1DD12D);
+                uint160 c = 10 + (a % 2);
+                address b = address(c);
+                vm.deal(b, 10);
+              }
+             }
+            |]
+        let sig =Just (Sig "fun(uint160)" [AbiUIntType 160])
+        (e, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+        assertBoolM "The expression is not partial" $ Prelude.not (Expr.containsNode isPartial e)

Which failed before.

[blishko]

Looks better, but I still don't understand the leftOrRight argument of runMore.
Can you explain what it represents? What is its type? Where is it provided?

[msooseth]

Looks better, but I still don't understand the leftOrRight argument of runMore. Can you explain what it represents? What is its type? Where is it provided?

Yes. So this is a Bool. I have renamed it to firstThread. If true, we are running the 1st thread. If it's false, it's the 2nd thread. What we do is that if there are exactly 2 things to run, we run the 1st on the 1st thread, and the 2nd on the 2nd thread.

If there are more than 2 things to run, we run the 1st on the 1st thread, and then the rest on the 2nd thread, by calling ourselves in the 2nd thread. Then, there'll be 1 less things to run... and so on. So it does this:

- 4 values to run: `a,b,c,d`
- we run `a` in the 1st thread, and call ourselves with `b,c,d` in the 2nd thread
- we run `b` in the 1st thread, and call ourselves with `c,d` in the 2nd thread
- Only 2 left. We can do this in one go! We run `c` in the 1st thread, and `d` in the 2nd thread.

Do you have some idea how to express this better in code? I recognize this is non-trivial, but this kind of recursive self-calling with elements is kinda normal for Haskell. Maybe it could be done with some kind of foldr or something....

[msooseth]

(sorry, had to update above description to be more precise)

[blishko]

Hmm, I can give it another look in the evening. But it's fine if you want to merge this and move on right away.

[msooseth]

There is no rush actually :) Take your time!

[msooseth]

Ahhh, I see you approved... OK, let me merge. You can ask me about issues if have some. I feel like it's a non-trivial change, mostly because Ask hasn't been working for a long while due to the debugger being stripped away. The code now reflects this conceptual change better.