Optimize execution loop (#293)

.github/workflows/test-external.yml

@@ -9,7 +9,8 @@ on:
 
 jobs:
   test:
-    runs-on: macos-latest
+    runs-on: ubuntu-latest
+    container: ghcr.io/emperororokusaki/solvers:0.1.0
 
     strategy:
       fail-fast: false
@@ -22,11 +23,11 @@ jobs:
           - repo: "a16z/cicada"
             dir: "cicada"
             cmd: "halmos --contract LibUint1024Test --function testProve --loop 256"
-            branch: ""
+            branch: "pin-solc"
           - repo: "a16z/cicada"
             dir: "cicada"
             cmd: "halmos --contract LibPrimeTest --function testProve --loop 256"
-            branch: ""
+            branch: "pin-solc"
           - repo: "farcasterxyz/contracts"
             dir: "farcaster-contracts"
             cmd: "halmos"
@@ -52,20 +53,6 @@ jobs:
           ref: ${{ matrix.branch }}
           submodules: recursive
 
-      - name: Install Foundry
-        uses: foundry-rs/foundry-toolchain@v1
-
-      - name: Set up Python
-        uses: actions/setup-python@v5
-        with:
-          python-version: "3.12"
-
-      - name: Install dependencies
-        run: python -m pip install --upgrade pip
-
-      - name: Install Halmos
-        run: python -m pip install -e ./halmos
-
       - name: Test external repo
-        run: ${{ matrix.cmd }} -v -st --solver-timeout-assertion 0 --solver-threads 2
+        run: ${{ matrix.cmd }} --statistics --debug --solver-timeout-assertion 0 --solver-threads 4 --solver-command=yices-smt2
         working-directory: ${{ matrix.dir }}

src/halmos/__main__.py

@@ -299,6 +299,7 @@ def run_bytecode(hexcode: str, args: Namespace) -> List[Exec]:
         caller=mk_caller(args),
         value=mk_callvalue(),
         data=ByteVec(),
+        call_scheme=EVM.CALL,
     )
 
     sevm = SEVM(options)
@@ -357,6 +358,7 @@ def deploy_test(
         caller=mk_caller(args),
         value=0,
         data=ByteVec(),
+        call_scheme=EVM.CREATE,
     )
 
     ex = sevm.mk_exec(
@@ -449,6 +451,7 @@ def setup(
                 caller=setup_ex.message().caller,
                 value=0,
                 data=calldata,
+                call_scheme=EVM.CALL,
             ),
         )
 
@@ -593,6 +596,7 @@ def run(
         caller=setup_ex.caller(),
         value=0,
         data=cd,
+        call_scheme=EVM.CALL,
     )
 
     #
@@ -1018,7 +1022,8 @@ def solve(
             dump_filename = f"/tmp/{uuid.uuid4().hex}.smt2"
 
         with open(dump_filename, "w") as f:
-            print(f"Writing SMT query to {dump_filename}")
+            if args.verbose >= 1:
+                print(f"Writing SMT query to {dump_filename}")
             f.write("(set-logic QF_AUFBV)\n")
             f.write(query)
             f.write("(get-model)\n")

src/halmos/bytevec.py

@@ -295,7 +295,7 @@ def __eq__(self, other) -> bool:
         return self.length == len(other) and eq(self.unwrap(), other.unwrap())
 
     def __repr__(self) -> str:
-        return f"SymbolicChunk({self.data!r})"
+        return f"SymbolicChunk({self.data!r}, start={self.start}, length={self.length})"
 
 
 @dataclass