Add EXPLICIT fork policy

manticore/core/manticore.py

@@ -480,7 +480,7 @@ def from_saved_state(cls, filename: str, *args, **kwargs):
 
         return cls(deserialized, *args, **kwargs)
 
-    def _fork(self, state, expression, policy="ALL", setstate=None):
+    def _fork(self, state, expression, policy="ALL", setstate=None, values=None):
         """
         Fork state on expression concretizations.
         Using policy build a list of solutions for expression.
@@ -510,7 +510,7 @@ def setstate(x, y):
                 pass
 
         # Find a set of solutions for expression
-        solutions = state.concretize(expression, policy)
+        solutions = state.concretize(expression, policy, explicit_values=values)
 
         if not solutions:
             raise ManticoreError("Forking on unfeasible constraint set")

manticore/core/state.py

@@ -21,11 +21,11 @@
 
 
 class StateException(Exception):
-    """ All state related exceptions """
+    """All state related exceptions"""
 
 
 class TerminateState(StateException):
-    """ Terminates current state exploration """
+    """Terminates current state exploration"""
 
     def __init__(self, message, testcase=False):
         super().__init__(message)
@@ -51,9 +51,19 @@ class Concretize(StateException):
 
     """
 
-    _ValidPolicies = ["MIN", "MAX", "MINMAX", "ALL", "SAMPLED", "ONE", "PESSIMISTIC", "OPTIMISTIC"]
-
-    def __init__(self, message, expression, setstate=None, policy=None, **kwargs):
+    _ValidPolicies = [
+        "MIN",
+        "MAX",
+        "MINMAX",
+        "ALL",
+        "SAMPLED",
+        "ONE",
+        "PESSIMISTIC",
+        "OPTIMISTIC",
+        "EXPLICIT",
+    ]
+
+    def __init__(self, message, expression, setstate=None, policy=None, values=None, **kwargs):
         if policy is None:
             policy = "ALL"
         if policy not in self._ValidPolicies:
@@ -63,6 +73,7 @@ def __init__(self, message, expression, setstate=None, policy=None, **kwargs):
         self.expression = expression
         self.setstate = setstate
         self.policy = policy
+        self.values = values
         self.message = f"Concretize: {message} (Policy: {policy})"
         super().__init__(**kwargs)
 
@@ -365,7 +376,7 @@ def new_symbolic_value(self, nbits, label=None, taint=frozenset()):
         self._input_symbols.append(expr)
         return expr
 
-    def concretize(self, symbolic, policy, maxcount=7):
+    def concretize(self, symbolic, policy, maxcount=7, explicit_values=None):
         """This finds a set of solutions for symbolic using policy.
 
         This limits the number of solutions returned to `maxcount` to avoid
@@ -415,6 +426,8 @@ def concretize(self, symbolic, policy, maxcount=7):
             else:
                 # We assume the path constraint was feasible to begin with
                 vals = (True,)
+        elif policy == "EXPLICIT":
+            vals = explicit_values[:maxcount]
         else:
             assert policy == "ALL"
             vals = self._solver.get_all_values(

manticore/core/worker.py

@@ -155,7 +155,7 @@ def run(self, *args):
                         # Though, normally fork() saves the spawned childs,
                         # returns a None and let _get_state choose what to explore
                         # next
-                        m._fork(current_state, exc.expression, exc.policy, exc.setstate)
+                        m._fork(current_state, exc.expression, exc.policy, exc.setstate, exc.values)
                         current_state = None
 
                     except TerminateState as exc: