[pull] main from a16z:main

README.md

@@ -41,7 +41,9 @@ Refer to the [getting started guide](docs/getting-started.md) and the [examples]
 
 ## Contributing
 
-Refer to the [contributing guidelines](CONTRIBUTING.md).
+Refer to the [contributing guidelines](CONTRIBUTING.md), and explore the list of issues labeled ["good first issue" or "help wanted."][issues]
+
+[issues]: <https://github.com/a16z/halmos/issues?q=is%3Aopen+is%3Aissue+label%3A%22good+first+issue%22%2C%22help+wanted%22>
 
 ## Disclaimer
 

docs/getting-started.md

@@ -58,8 +58,10 @@ contract MyToken is ERC20 {
 Then you can write a `setUp()` function that creates a new token contract with a _symbolic_ initial supply, as follows:
 ```solidity
 import {SymTest} from "halmos-cheatcodes/SymTest.sol";
+import {Test} from "forge-std/Test.sol";
+import {MyToken} from "../src/MyToken.sol";
 
-contract MyTokenTest is SymTest {
+contract MyTokenTest is SymTest, Test {
     MyToken token;
 
     function setUp() public {
@@ -104,7 +106,7 @@ Below is an example symbolic test for the token transfer function:
 function check_transfer(address sender, address receiver, uint256 amount) public {
     // specify input conditions
     vm.assume(receiver != address(0));
-    vm.assume(token.balance(sender) >= amount);
+    vm.assume(token.balanceOf(sender) >= amount);
 
     // record the current balance of sender and receiver
     uint256 balanceOfSender = token.balanceOf(sender);
@@ -179,7 +181,7 @@ Recall that symbolic tests take into account all possible input combinations. Ho
 In our example, the conditions for the valid sender and receiver addresses are specified as follows:
 ```solidity
 vm.assume(receiver != address(0));
-vm.assume(token.balance(sender) >= amount);
+vm.assume(token.balanceOf(sender) >= amount);
 ```
 Like fuzz tests, any input combinations that don't satisfy the `assume()` conditions are disregarded. This means that, after executing the above `assume()` statements, only the input combinations in which the receiver is non-zero and the sender has sufficient balance are considered. Other input combinations that violate these conditions are ignored.
 

examples/simple/src/BadElections.sol

@@ -0,0 +1,38 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import {ECDSA} from "openzeppelin/utils/cryptography/ECDSA.sol";
+
+/// DO NOT USE, this demonstrates signature malleability problems
+contract BadElections {
+    event Voted(uint256 proposalId, bool support, address voter);
+
+    mapping (bytes32 => bool) hasVoted;
+
+    // maps proposalId to vote count
+    mapping (uint256 => uint256) public votesFor;
+    mapping (uint256 => uint256) public votesAgainst;
+
+    // vote on a proposal by signature, anyone can cast a vote on behalf of someone else
+    function vote(uint256 proposalId, bool support, address voter, bytes calldata signature) public {
+        bytes32 sigHash = keccak256(signature);
+        require(!hasVoted[sigHash], "already voted");
+
+        bytes32 badSigDigest = keccak256(abi.encode(proposalId, support, voter));
+        address recovered = ECDSA.recover(badSigDigest, signature);
+        require(recovered == voter, "invalid signature");
+        require(recovered != address(0), "invalid signature");
+
+        // prevent replay
+        hasVoted[sigHash] = true;
+
+        // record vote
+        if (support) {
+            votesFor[proposalId]++;
+        } else {
+            votesAgainst[proposalId]++;
+        }
+
+        emit Voted(proposalId, support, voter);
+    }
+}

examples/simple/test/BadElections.t.sol

@@ -0,0 +1,60 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import "forge-std/Test.sol";
+
+import {SymTest} from "halmos-cheatcodes/SymTest.sol";
+
+import {BadElections} from "src/BadElections.sol";
+
+contract BadElectionsTest is SymTest, Test {
+    BadElections elections;
+
+    function setUp() public {
+        elections = new BadElections();
+    }
+
+    /// The output will look something like this:
+    ///
+    ///     Running 1 tests for test/BadElections.t.sol:BadElectionsTest
+    ///     Counterexample:
+    ///         halmos_fakeSig_bytes_01 = 0x00000000000000000000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffff5d576e7357a4501ddfe92f46681b20a100 (65 bytes)
+    ///         p_proposalId_uint256 = 0x0000000000000000000000000000000000000000000000000000000000000000 (0)
+    ///     [FAIL] check_canNotVoteTwice(uint256) (paths: 7, time: 0.63s, bounds: [])
+    ///
+    /// the counterexample values are not meaningful, but examining the trace shows
+    /// that halmos found a signature s.t. the voter can vote twice on the same proposal,
+    /// and the final vote count is 2
+    function check_canNotVoteTwice(uint256 proposalId) public {
+        // setup
+        bool support = true;
+        (address voter, uint256 privateKey) = makeAddrAndKey("voter");
+
+        bytes32 sigDigest = keccak256(abi.encode(proposalId, support, voter));
+        (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, sigDigest);
+        bytes memory signature = abi.encodePacked(r, s, v);
+
+        // we start with no vote
+        assertEq(elections.votesFor(proposalId), 0);
+
+        // when we cast the vote
+        elections.vote(proposalId, support, voter, signature);
+
+        // then the vote count increases
+        assertEq(elections.votesFor(proposalId), 1);
+
+        // when we vote again with the same signature, it reverts
+        try elections.vote(proposalId, support, voter, signature) {
+            assert(false);
+        } catch {
+            // expected
+        }
+
+        // when the same voter votes with a different signature
+        elections.vote(proposalId, support, voter, svm.createBytes(65, "fakeSig"));
+
+        // then the vote count remains unchanged
+        // @note spoiler alert: it does not
+        assertEq(elections.votesFor(proposalId), 1);
+    }
+}

src/halmos/__main__.py

@@ -1017,25 +1017,52 @@ def copy_model(model: Model) -> Dict:
 def solve(
     query: str, args: Namespace, dump_filename: Optional[str] = None
 ) -> Tuple[CheckSatResult, Model]:
-    if dump_filename:
+    if args.dump_smt_queries or args.solver_command:
+        if not dump_filename:
+            dump_filename = f"/tmp/{uuid.uuid4().hex}.smt2"
+
         with open(dump_filename, "w") as f:
+            print(f"Writing SMT query to {dump_filename}")
             f.write("(set-logic QF_AUFBV)\n")
             f.write(query)
             f.write("(get-model)\n")
 
-    solver = mk_solver(args, ctx=Context(), assertion=True)
-    solver.from_string(query)
-    result = solver.check()
-    model = copy_model(solver.model()) if result == sat else None
-    return result, model
+    if args.solver_command:
+        if args.verbose >= 1:
+            print(f"  Checking with external solver process")
+            print(f"    {args.solver_command} {dump_filename} >{dump_filename}.out")
+
+        cmd = args.solver_command.split() + [dump_filename]
+        res_str = subprocess.run(cmd, capture_output=True, text=True).stdout.strip()
+        res_str_head = res_str.split("\n", 1)[0]
+
+        with open(f"{dump_filename}.out", "w") as f:
+            f.write(res_str)
+
+        if args.verbose >= 1:
+            print(f"    {res_str_head}")
+
+        if res_str_head == "unsat":
+            return unsat, None
+        elif res_str_head == "sat":
+            return sat, f"{dump_filename}.out"
+        else:
+            return unknown, None
+
+    else:
+        solver = mk_solver(args, ctx=Context(), assertion=True)
+        solver.from_string(query)
+        result = solver.check()
+        model = copy_model(solver.model()) if result == sat else None
+        return result, model
 
 
 def gen_model_from_sexpr(fn_args: GenModelArgs) -> ModelWithContext:
     args, idx, sexpr = fn_args.args, fn_args.idx, fn_args.sexpr
 
-    dump_dirname = fn_args.dump_dirname if args.dump_smt_queries else None
-    dump_filename = f"{dump_dirname}/{idx+1}.smt2" if dump_dirname else None
-    if dump_dirname:
+    dump_dirname = fn_args.dump_dirname
+    dump_filename = f"{dump_dirname}/{idx+1}.smt2"
+    if args.dump_smt_queries or args.solver_command:
         if not os.path.isdir(dump_dirname):
             os.makedirs(dump_dirname)
             print(f"Generating SMT queries in {dump_dirname}")
@@ -1049,39 +1076,8 @@ def gen_model_from_sexpr(fn_args: GenModelArgs) -> ModelWithContext:
         if args.verbose >= 1:
             print(f"  Checking again with refinement")
 
-        res, model = solve(
-            refine(sexpr),
-            args,
-            dump_filename.replace(".smt2", ".refined.smt2") if dump_filename else None,
-        )
-
-    if args.solver_subprocess and is_unknown(res, model):
-        fname = f"/tmp/{uuid.uuid4().hex}.smt2"
-
-        if args.verbose >= 1:
-            print(f"  Checking again in an external process")
-            print(f"    {args.solver_subprocess_command} {fname} >{fname}.out")
-
-        query = refine(sexpr)
-        with open(fname, "w") as f:
-            f.write("(set-logic QF_AUFBV)\n")
-            f.write(query)
-
-        cmd = args.solver_subprocess_command.split() + [fname]
-        res_str = subprocess.run(cmd, capture_output=True, text=True).stdout.strip()
-        res_str_head = res_str.split("\n", 1)[0]
-
-        with open(f"{fname}.out", "w") as f:
-            f.write(res_str)
-
-        if args.verbose >= 1:
-            print(f"    {res_str_head}")
-
-        if res_str_head == "unsat":
-            res = unsat
-        elif res_str_head == "sat":
-            res = sat
-            model = f"{fname}.out"
+        refined_filename = dump_filename.replace(".smt2", ".refined.smt2")
+        res, model = solve(refine(sexpr), args, refined_filename)
 
     return package_result(model, idx, res, args)
 
@@ -1140,10 +1136,21 @@ def package_result(
 def is_model_valid(model: AnyModel) -> bool:
     # TODO: evaluate the path condition against the given model after excluding evm_* symbols,
     #       since the evm_* symbols may still appear in valid models.
-    for decl in model:
-        if str(decl).startswith("evm_"):
-            return False
-    return True
+
+    # model is a filename, containing solver output
+    if isinstance(model, str):
+        with open(model, "r") as f:
+            for line in f:
+                if "evm_" in line:
+                    return False
+        return True
+
+    # z3 model object
+    else:
+        for decl in model:
+            if str(decl).startswith("evm_"):
+                return False
+        return True
 
 
 def to_str_model(model: Model, print_full_model: bool) -> StrModel: