Collision in address is "possible" as per hevm, even though it's not

[zoep]

Should hevm enforce freshness conditions on newly created symbolic addresses?

I am working with this example:

contract A {
    uint public x;

    constructor ()  {
	x = 42;
    }
}

contract B {

    A a1;
    A a2;

    constructor() {
	a1 = new A();
	a2 = new A();
	assert (address(a1) != address(a2));
    }
}

running hevm symbolic --sig "B()" --code <the-creation-code> returns

Discovered the following counterexamples:

Calldata:
  0x32e7c5bf

Storage:
  Addr SymAddr "entrypoint": [(0x0,0x0),(0x1,0x0)]
  Addr SymAddr "miner": []
  Addr SymAddr "origin": []

Transaction Context:
  TxValue: 0x0

the same happens with --initial-storage Empty.

Removing the assertion results in QED.

[msooseth]

Aliasing bug

[msooseth]

Yay this should be fixed with #641

Took me a looooooong time. But got there eventually.

$ solc --bin --optimize stuff.sol  
======= stuff.sol:A =======
Binary:
6080604052348015600e575f80fd5b50602a5f55607980601e5f395ff3fe6080604052348015600e575f80fd5b50600436106026575f3560e01c80630c55699c14602a575b5f80fd5b60315f5481565b60405190815260200160405180910390f3fea2646970667358221220a28109598464f5c9a677254859396694964348a7b5228bedfd9cf318169566f564736f6c634300081a0033

======= stuff.sol:B =======
Binary:
6080604052348015600e575f80fd5b5060405160199060a6565b604051809103905ff0801580156031573d5f803e3d5ffd5b505f80546001600160a01b0319166001600160a01b0392909216919091179055604051605b9060a6565b604051809103905ff0801580156073573d5f803e3d5ffd5b50600180546001600160a01b0319166001600160a01b039283169081179091555f549091160360a25760a260b2565b60c6565b60978061011083390190565b634e487b7160e01b5f52600160045260245ffd5b603e806100d25f395ff3fe60806040525f80fdfea2646970667358221220daa692e74d5328af58dc112e8f317e1421d86a6068b92f39db243be6059c4b0b64736f6c634300081a00336080604052348015600e575f80fd5b50602a5f55607980601e5f395ff3fe6080604052348015600e575f80fd5b50600436106026575f3560e01c80630c55699c14602a575b5f80fd5b60315f5481565b60405190815260200160405180910390f3fea2646970667358221220a28109598464f5c9a677254859396694964348a7b5228bedfd9cf318169566f564736f6c634300081a0033

Then:

cabal run exe:hevm symbolic -- --sig "B()" --code "6080604052348015600e575f80fd5b5060405160199060a6565b604051809103905ff0801580156031573d5f803e3d5ffd5b505f80546001600160a01b0319166001600160a01b0392909216919091179055604051605b9060a6565b604051809103905ff0801580156073573d5f803e3d5ffd5b50600180546001600160a01b0319166001600160a01b039283169081179091555f549091160360a25760a260b2565b60c6565b60978061011083390190565b634e487b7160e01b5f52600160045260245ffd5b603e806100d25f395ff3fe60806040525f80fdfea2646970667358221220daa692e74d5328af58dc112e8f317e1421d86a6068b92f39db243be6059c4b0b64736f6c634300081a00336080604052348015600e575f80fd5b50602a5f55607980601e5f395ff3fe6080604052348015600e575f80fd5b50600436106026575f3560e01c80630c55699c14602a575b5f80fd5b60315f5481565b60405190815260200160405180910390f3fea2646970667358221220a28109598464f5c9a677254859396694964348a7b5228bedfd9cf318169566f564736f6c634300081a0033"

QED: No reachable property violations discovered

Without the PR:

cabal run exe:hevm symbolic -- --sig "B()" --code "6080604052348015600e575f80fd5b5060405160199060a6565b604051809103905ff0801580156031573d5f803e3d5ffd5b505f80546001600160a01b0319166001600160a01b0392909216919091179055604051605b9060a6565b604051809103905ff0801580156073573d5f803e3d5ffd5b50600180546001600160a01b0319166001600160a01b039283169081179091555f549091160360a25760a260b2565b60c6565b60978061011083390190565b634e487b7160e01b5f52600160045260245ffd5b603e806100d25f395ff3fe60806040525f80fdfea2646970667358221220daa692e74d5328af58dc112e8f317e1421d86a6068b92f39db243be6059c4b0b64736f6c634300081a00336080604052348015600e575f80fd5b50602a5f55607980601e5f395ff3fe6080604052348015600e575f80fd5b50600436106026575f3560e01c80630c55699c14602a575b5f80fd5b60315f5481565b60405190815260200160405180910390f3fea2646970667358221220a28109598464f5c9a677254859396694964348a7b5228bedfd9cf318169566f564736f6c634300081a0033"

Discovered the following 1 counterexample(s):

Calldata:
  0x32e7c5bf
Storage:
  Addr SymAddr "entrypoint": [(0x0,0x0)]
  Addr SymAddr "miner": []
  Addr SymAddr "origin": []
Transaction Context:
  TxValue: 0x0
Addrs:
  SymAddr "freshSymAddr1": 0xFFfFfFffFFfffFFfFFfFFFFFffFFFffffFfFFFfF
  SymAddr "freshSymAddr2": 0xFFfFfFffFFfffFFfFFfFFFFFffFFFffffFfFFFfF