Skip to content

Commit

Permalink
Merge branch 'main' into handle-library-placeholder
Browse files Browse the repository at this point in the history
  • Loading branch information
daejunpark authored Aug 3, 2023
2 parents 5d6792e + eb6e4a1 commit 8d4fe8b
Show file tree
Hide file tree
Showing 5 changed files with 59 additions and 27 deletions.
52 changes: 42 additions & 10 deletions src/halmos/__main__.py
Original file line number Diff line number Diff line change
Expand Up @@ -231,23 +231,18 @@ def run_bytecode(hexcode: str, args: Namespace) -> List[Exec]:
return exs


def setup(
def deploy_test(
hexcode: str,
abi: List,
setup_info: FunctionInfo,
sevm: SEVM,
args: Namespace,
) -> Exec:
setup_start = timer()

# test contract creation bytecode
contract = Contract.from_hexcode(hexcode)

solver = mk_solver(args)
this = mk_this()
options = mk_options(args)

sevm = SEVM(options)

setup_ex = sevm.mk_exec(
ex = sevm.mk_exec(
code={this: contract},
storage={this: {}},
balance=mk_balance(),
Expand All @@ -260,6 +255,43 @@ def setup(
solver=solver,
)

# create test contract
(exs, _, _) = sevm.run(ex)

# sanity check
if len(exs) != 1:
raise ValueError(f"constructor: # of paths: {len(exs)}")
ex = exs[0]
if ex.failed:
raise ValueError(f"constructor: failed: {ex.error}")
if ex.current_opcode() not in [EVM.STOP, EVM.RETURN]:
raise ValueError(f"constructor: failed: {ex.current_opcode()}: {ex.error}")

# deployed bytecode
ex.code[this] = Contract(ex.output)

# reset vm state
ex.pc = 0
ex.st = State()
ex.jumpis = {}
ex.output = None
ex.prank = Prank()

return ex


def setup(
hexcode: str,
abi: List,
setup_info: FunctionInfo,
args: Namespace,
) -> Exec:
setup_start = timer()

sevm = SEVM(mk_options(args))

setup_ex = deploy_test(hexcode, sevm, args)

setup_mid = timer()

setup_sig, setup_name, setup_selector = (
Expand Down Expand Up @@ -1073,7 +1105,7 @@ def _main(_args=None) -> MainResult:
if contract_type != "contract":
continue

hexcode = contract_json["deployedBytecode"]["object"]
hexcode = contract_json["bytecode"]["object"]
abi = contract_json["abi"]
methodIdentifiers = contract_json["methodIdentifiers"]

Expand Down
4 changes: 2 additions & 2 deletions tests/expected/all.json
Original file line number Diff line number Diff line change
Expand Up @@ -992,8 +992,8 @@
"test/TestConstructor.t.sol:TestConstructorTest": [
{
"name": "check_value()",
"exitcode": 1,
"num_models": 1,
"exitcode": 0,
"num_models": 0,
"num_paths": null,
"time": null,
"num_bounded_loops": null
Expand Down
15 changes: 12 additions & 3 deletions tests/test/TestConstructor.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,20 @@
pragma solidity >=0.8.0 <0.9.0;

contract TestConstructorTest {
uint initialized = 1;
uint constant const = 2;
uint immutable flag;
uint value;

uint public value = 1;
constructor () {
flag = 3;
value = 4;
}

function check_value() public view {
assert(value == 1); // fail // TODO: consider test contract constructor
assert(initialized == 1);
assert(const == 2);
assert(flag == 3);
assert(value == 4);
}

}
9 changes: 0 additions & 9 deletions tests/test_cli.py
Original file line number Diff line number Diff line change
Expand Up @@ -119,15 +119,6 @@ def test_run_bytecode(args):
assert exs[0].current_opcode() == EVM.STOP


def test_setup(setup_abi, setup_name, setup_sig, setup_selector, args):
hexcode = "600100"
abi = setup_abi
setup_ex = halmos.__main__.setup(
hexcode, abi, FunctionInfo(setup_name, setup_sig, setup_selector), args
)
assert setup_ex.st.stack == [1]


def test_instruction():
assert str(Instruction(con(0))) == "STOP"
assert str(Instruction(con(1))) == "ADD"
Expand Down
6 changes: 3 additions & 3 deletions tests/test_halmos.py
Original file line number Diff line number Diff line change
Expand Up @@ -65,8 +65,8 @@ def assert_eq(m1: Dict, m2: Dict) -> int:
for c in m1:
l1 = sorted(m1[c], key=lambda x: x["name"])
l2 = sorted(m2[c], key=lambda x: x["name"])
assert len(l1) == len(l2)
assert len(l1) == len(l2), c
for r1, r2 in zip(l1, l2):
assert r1["name"] == r2["name"]
assert r1["exitcode"] == r2["exitcode"]
assert r1["num_models"] == r2["num_models"]
assert r1["exitcode"] == r2["exitcode"], f"{c} {r1['name']}"
assert r1["num_models"] == r2["num_models"], f"{c} {r1['name']}"

0 comments on commit 8d4fe8b

Please sign in to comment.