BLOCKHASH opcodes should return concrete results.

[nbanmp]

Right now, the blockhash and number opcodes always return symbolic values. When connected to a node via rpc, this information is available when the opcodes are called with concrete arguments. We can retrieve that information and return it.

Returning the correct blockhash and number will be especially helpful in generating test cases for contracts that use these as a source of randomness.

Note that the dependence on predictable vars module searches through constraints for the term "blockhash," so it will also be necessary to update that module to use annotations.

[JoranHonig]

I don't think we should do this. It would only degrade the quality of our analysis.
For example, if there is a vulnerability that can be accessed at block x, but the current block is x-10. Then we wouldn't report it, but it would be vulnerable. Keeping these variables symbolic is keeps us from reporting false negatives.

Furthermore, (correct me if I'm wrong) but the blockhash is calculated over the block in which the executing transaction is. Which would make it impossible to determine, because we analyse hypothetical transactions, which are in yet non-existent block(s)

[nbanmp]

The blockhash opcode takes an argument for the number of the block to retrieve the hash for.

Your point stands for number, we probably shouldn't implement that, but there is no downside to returning the blockhash when a concrete block number is provided as an argument.

[JoranHonig]

Ah right @nbanmp for blockhash it would make sense, unless ofc you calculate blockhash(number) if that is possible