support for Uniswap v2 testing workflow

[0xkarmacoma]

Describe the bug

Different sha3_expr in in create2 init code lead to different inferred address vs actually deployed address.

In the example below, uniswapV2Factory.createPair(address(token), address(weth)) results in the following sha3_expr:

sha3_expr=f_sha3_680(Concat(372682917519380244141939632342652170012265661726725,
              f_sha3_320(4184670640661422675847470105623367512667768574483259588612),
              f_sha3_93088(...init code concrete value...)))

But in the pairFor helper function, this is the expression used:

    pair = address(uint(keccak256(abi.encodePacked(
            hex'ff',
            factory,
            keccak256(abi.encodePacked(token0, token1)),
            hex'96e8ac4277198ff8b6f785478aa9a39f403cb768dd02cbee326c3e7da348845f' // init code hash
        ))));

(note the hardcoded initcode hash value)

On the halmos side, it results in the following sha3_expr:

sha3_expr=f_sha3_680(Concat(372682917519380244141939632342652170012265661726725, 
              f_sha3_320(4184670640661422675847470105623367512667768574483259588612), 
              68258024698789349894765071221733254692395760896603232917352833510768193864799))

If we were to evaluate f_sha3_93088(...init code concrete value...) concretely, we would indeed get the same value:

keccak(bytes.fromhex(hex(a)[2:])).hex()
'96e8ac4277198ff8b6f785478aa9a39f403cb768dd02cbee326c3e7da348845f'

Because of the sha3_expr mismatch, pairFor returns a different address (bbbb0011) than the address actually deployed (bbbb000b) and subsequent calls fail

To Reproduce

necessary steps from https://github.com/igorganich/damn-vulnerable-defi-halmos/blob/master/test/puppet-v2/PuppetV2_Halmos.t.sol#L86 (h/t @igorganich)

    function setUp() public {
        // Deploy tokens to be traded
        token = new DamnValuableToken();
        weth = new WETH();

        // Deploy Uniswap V2 Factory and Router
        uniswapV2Factory = IUniswapV2Factory(/* deploy here */);
        uniswapV2Router = IUniswapV2Router02(/* deploy here */);

        // Create Uniswap pair
        address pair = uniswapV2Factory.createPair(address(token), address(weth));
        address inferredPair = pairFor(address(uniswapV2Factory), address(token), address(weth));
        assertEq(deployedPair, inferredPair);
    }

[0xkarmacoma]

fixed in #507