Custom view shows another contract and uses the wrong PC in the kcfg viewer

Issue

When launching the kcfg-viewer, the custom view is not very useful because it rarely shows the correct executed part of the Solidity source.
There are two reasons of that:

• Only the testing contract is passed to the source map (1)
• Source maps are indexed by instruction index, but are fetched by PC (2)

(1)

When calling the exec_foundry_view_kcfg function

https://github.com/runtimeverification/evm-semantics/blob/master/kevm-pyk/src/kevm_pyk/__main__.py#L630

We get the name of the testing contract

https://github.com/runtimeverification/evm-semantics/blob/master/kevm-pyk/src/kevm_pyk/__main__.py#L633

And only this one is passed to the source mapping structure

https://github.com/runtimeverification/evm-semantics/blob/master/kevm-pyk/src/kevm_pyk/__main__.py#L641-L642

Then if any external contract is called, we will not see the executed part in the source code

(2)

The instr_to_pc is correctly implemented but not used here

https://github.com/runtimeverification/evm-semantics/blob/master/kevm-pyk/src/kevm_pyk/solc_to_k.py#L296

Here

https://github.com/runtimeverification/evm-semantics/blob/master/kevm-pyk/src/kevm_pyk/solc_to_k.py#L324

We should probably rewrite it as:

_srcmap[instr_to_pc[i]] = (s, l, f, j, m)

Ideas

There is no way to know which contract is executed from the PC information only, because it may overlap (it starts at PC = 0 when executing a new contract).

Then when calling back _custom_view(), we may want to pass the contract name.

So a solution would be to allow writing the name of the contract that is currently executed in the K cell although not very desirable probably.

A better solution would be to write the bytecode of the contract that is currently executed in the node and we could fetch the contract, but if two contracts have the same bytecode then it may display the wrong one and may confuse the user.

Trace exec_foundry_view_kcfg in kevm-pyk/src/kevm_pyk/main.py and the source-map construction in kevm-pyk/src/kevm_pyk/solc_to_k.py, including instr_to_pc. Determine how _custom_view receives execution context, then define and test a way for the custom view to select the correct contract and source span for external calls.