refactor: data structure of path conditions (#310)

src/halmos/__main__.py

@@ -376,7 +376,7 @@ def run_bytecode(hexcode: str, args: HalmosConfig) -> List[Exec]:
             print(f"Return data: {returndata}")
             dump_dirname = f"/tmp/halmos-{uuid.uuid4().hex}"
             model_with_context = gen_model_from_sexpr(
-                GenModelArgs(args, idx, ex.path.solver.to_smt2(), dump_dirname)
+                GenModelArgs(args, idx, ex.path.to_smt2(), dump_dirname)
             )
             print(f"Input example: {model_with_context.model}")
 
@@ -510,7 +510,7 @@ def setup(
             error = setup_ex.context.output.error
 
             if error is None:
-                setup_exs_no_error.append((setup_ex, setup_ex.path.solver.to_smt2()))
+                setup_exs_no_error.append((setup_ex, setup_ex.path.to_smt2()))
 
             else:
                 if opcode not in [EVM.REVERT, EVM.INVALID]:
@@ -753,7 +753,7 @@ def future_callback(future_model):
             if args.verbose >= VERBOSITY_TRACE_COUNTEREXAMPLE:
                 traces[idx] = rendered_trace(ex.context)
 
-            query = ex.path.solver.to_smt2()
+            query = ex.path.to_smt2()
 
             future_model = thread_pool.submit(
                 gen_model_from_sexpr, GenModelArgs(args, idx, query, dump_dirname)

src/halmos/sevm.py

@@ -477,28 +477,34 @@ class Path:
     solver: Solver
     num_scopes: int
     # path constraints include both explicit branching conditions and implicit assumptions (eg, no hash collisions)
-    # TODO: separate these two types of constraints, so that we can display only branching conditions to users
-    conditions: List
-    branching: List  # indexes of conditions
+    conditions: Dict  # cond -> bool (true if explicit branching conditions)
     pending: List
 
     def __init__(self, solver: Solver):
         self.solver = solver
         self.num_scopes = 0
-        self.conditions = []
-        self.branching = []
+        self.conditions = {}
         self.pending = []
         self.forked = False
 
     def __deepcopy__(self, memo):
         raise NotImplementedError(f"use the branch() method instead of deepcopy()")
 
     def __str__(self) -> str:
-        branching_conds = [self.conditions[idx] for idx in self.branching]
         return "".join(
-            [f"- {cond}\n" for cond in branching_conds if str(cond) != "True"]
+            [
+                f"- {cond}\n"
+                for cond in self.conditions
+                if self.conditions[cond] and str(cond) != "True"
+            ]
         )
 
+    def to_smt2(self) -> str:
+        return self.solver.to_smt2()
+
+    def check(self, cond):
+        return self.solver.check(cond)
+
     def branch(self, cond):
         if len(self.pending) > 0:
             raise ValueError("branching from an inactive path", self)
@@ -547,19 +553,17 @@ def append(self, cond, branching=False):
         if is_true(cond):
             return
 
-        self.solver.add(cond)
-        self.conditions.append(cond)
-
-        if branching:
-            self.branching.append(len(self.conditions) - 1)
+        if cond not in self.conditions:
+            self.solver.add(cond)
+            self.conditions[cond] = branching
 
     def extend(self, conds, branching=False):
         for cond in conds:
             self.append(cond, branching=branching)
 
     def extend_path(self, path):
         # branching conditions are not preserved
-        self.extend(path.conditions)
+        self.extend(path.conditions.keys())
 
 
 class Exec:  # an execution path
@@ -737,7 +741,7 @@ def check(self, cond: Any) -> Any:
         if is_false(cond):
             return unsat
 
-        return self.path.solver.check(cond)
+        return self.path.check(cond)
 
     def select(self, array: Any, key: Word, arrays: Dict) -> Word:
         if array in arrays: