Dynamic exception type: std::bad_cast

PaulRBerg commented 1 year ago

Description

I followed the SMTChecker docs and added the following annotation to all of my PRBMath functions:

/// @custom:smtchecker abstract-function-nondet

See commit 588c91.

I then proceeded with running the SMTChecker in a private repo that has PRBMath as a dependency, when I got this error:

❯ FOUNDRY_PROFILE=smt forge build --ignored-error-codes 7737
[⠊] Compiling...
[⠊] Compiling 221 files with 0.8.18
[⠒] Solc 0.8.18 finished in 10.34s
Error:
Compiler run failed
Unknown exception during compilation: Dynamic exception type: std::bad_cast
std::exception::what: std::bad_cast

Prior to adding the abstract-function-nondet annotation, the SMTChecker was running successfully.

Environment

Compiler version: 0.8.18
Target EVM version (as per compiler settings): default
Framework/IDE (e.g. Truffle or Remix): Forge
EVM execution environment / backend / blockchain client: REVM
Operating system: macOS (Apple Silicon)

Steps to Reproduce

Create a Forge project.
Install PRBMath from commit [de5ccb9][de5ccb9].
Use any PRBMath function.
Enable the SMTChecker in the Foundry config e.g. with the config below:

[profile.smt.model_checker]
  engine = "chc"
  targets = [
    "assert",
    "constantCondition",
    "divByZero",
    "outOfBounds",
    "overflow",
    "underflow",
  ]

leonardoalt commented 1 year ago

Thanks for the report! Nice to see that feature being used, even if it's broken lol. After a quick look I think I know what's wrong, will try to fix tomorrow.

PaulRBerg commented 1 year ago

Thanks, Leo.

While we are at it, I have another related question about the proper usage of this annotation. The docs say this:

Certain functions ... may be too complex to be analyzed in a fully automated way

I imagine that this is more "touch and feel" than science, but I'm curious if there's any additional thoughts you could share about what "complex" means for SMTChecker?

For instance, should I add the non-deterministic annotation to my implementation of avg?

function avg(UD60x18 x, UD60x18 y) pure returns (UD60x18 result) {
    uint256 xUint = unwrap(x);
    uint256 yUint = unwrap(y);
    unchecked {
        result = wrap((xUint & yUint) + ((xUint ^ yUint) >> 1));
    }
}

It uses bitwise operators - does this qualify as "complex" for SMTChecker purposes?

leonardoalt commented 1 year ago

You're right that the simplest answer is indeed "touch and feel". An informed heuristic though depends on the engine and requires some extra knowledge about how they work.

In pure SMT, indeed bitwise operations are more complicated than arithmetic. Nonlinear arithmetic though (multiplication or division between variables) is more complicated than bitwise ops. Solving Bitvectors (required by bitwise ops) in an SMT solver is NP-complete, so it's bad but they manage sort of often. Nonlinear arithmetic is straight up undecidable, so you're lucky if anything is solved.

Regardless of the above, the main question is how these functions are used in the code that has the property you're trying to prove. If the function is used in a very local way, in a way that doesn't really affect storage or need storage, BMC might be able to handle it (precisely, without the abstraction annotation). However if such function is used in combination with state transitions (as in the contract's lifetime) to imply the property you're trying to prove, BMC won't help since it only analyzes external functions in isolation and inlines function calls. At this point you need CHC to prove your property, since it does handle state properly. The trade off of having this capability is the overhead of requiring inductive invariants (very hard to compute) even for simple cases. If the property requires bitwise/nonlinear reasoning, the CHC solver will need to compute inductive invariants on top of Bitvectors/Nonlinear arithmetic, resp, which is even harder. At this point you might need to abstract the function.

What I usually do in such cases when dealing with a lot of math (did it for code like Uniswap and code that uses your fixed point lib) is just try the precise version and then annotate function by function. The annoying thing is that in the end you might need to abstract too many things to have it go through, which might be too abstract and just give you ridiculous false positives.

What I'd also recommend is trying out Eldarica as a solver for the CHC engine. It's slower than z3 but it can solve problems that z3 can't (which doesn't imply it will be able to solve math stuff). You need to have it available in the system and use the option settings.modelChecker.solvers = [ "eld" ] in standard JSON for example. I think I didn't add the modelChecker.solvers option to the Foundry config yet, but shouldn't be hard and I intend to do it soon.

Finally, the most advanced thing you can do (which is also what I do) for the most complex single properties, is to dump the smtlib2 file (SMT theorem) for either the BMC or CHC engine (depending whether your property needs state reasoning or not), and try out different configurations of different solvers (by that I mean tens or hundreds or thousands of configurations). The SMTChecker only tries out 2 configurations of z3 and 1 configuration of Eldarica, which is very likely not enough for the hardest properties. It's a hard balance to find since spawning a massive load of solvers/configurations would be too much for the normal user. In the FV industry this is a common approach (spawning tons of solvers/configs) for complex properties, where different configurations might even consist of just changing the random seed in a solver run, since these solvers are very sensitive to changes and such change might be the difference between solving something quite quickly or not at all (long timeout). If you eventually wanna go that route lmk so I can give you some pointers.

PaulRBerg commented 1 year ago

Thank you for the taking the time to write this detailed answer, @leonardoalt. Some of the points you made here may be well worth including in the SMTChecker documentation page.

In pure SMT, indeed bitwise operations are more complicated than arithmetic. Nonlinear arithmetic though (multiplication or division between variables) is more complicated than bitwise ops

Great, so non-linear arithmetic > bitwise > linear arithmetic.

What I usually do in such cases when dealing with a lot of math (did it for code like Uniswap and code that uses your fixed point lib) is just try the precise version and then annotate function by function

Thanks for the tip! From the perspective of a library developer, the downside of this approach is that it makes it difficult to decide what should be marked as abstract-nondet, and what not.

I think I will just annotate all of the functions; based on your explanation above, it seems to me that the solver will have a hard time proving things with most functions in PRBMath, because they use either bitwise operations or inline assembly. Sophisticated users can just copy-paste the function they are interested in and remove the annotation to make it precise.

What I'd also recommend is trying out Eldarica as a solver for the CHC engine

Thanks, I'll give it a go.

I think I didn't add the modelChecker.solvers option to the Foundry config yet, but shouldn't be hard and I intend to do it soon.

This would be super helpful, thanks very much. A related issue I bumped into recently is the lack of the showUnproved config option in Foundry - I wanted to use this after receiving the following warning from the compiler:

Warning: CHC: 10 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems.

the most advanced thing you can do (which is also what I do)

Chad.

to dump the smtlib2 file (SMT theorem) for either the BMC or CHC engine (depending whether your property needs state reasoning or not), and try out different configurations of different solvers (by that I mean tens or hundreds or thousands of configurations)

Interesting. I do have a few questions about this, but I will follow up separately, in private, if I do end up pursuing this approach.

If you eventually wanna go that route lmk so I can give you some pointers

Thank you, ser.

PaulRBerg commented 1 year ago

It looks like now there is support for solvers and show_unproved in Foundry thanks to @wiasliaw's recent PR in ethers-rs:

https://github.com/gakonst/ethers-rs/pull/2147

ethereum / solidity