Fix formatting

Author: toolCHAINZ

crackers_python/crackers/crackers_types.pyi

@@ -1,10 +1,28 @@
 from typing import Optional, Union, Callable, Iterable
-
-from z3 import z3
-
 from .jingle_types import State, ModeledBlock, ResolvedVarNode
-from ._internal.crackers import CrackersLogLevel
-from ._internal.crackers import SynthesisSelectionStrategy
+from z3 import z3  # type: ignore
+
+__all__ = [
+    "AssignmentModel",
+    "ConstraintConfig",
+    "CrackersConfig",
+    "CrackersLogLevel",
+    "DecisionResult",
+    "GadgetLibraryConfig",
+    "MemoryEqualityConstraint",
+    "MetaConfig",
+    "PointerRange",
+    "PointerRangeConstraints",
+    "SleighConfig",
+    "SpecificationConfig",
+    "StateEqualityConstraint",
+    "SynthesisConfig",
+    "SynthesisParams",
+    "SynthesisSelectionStrategy",
+    "DecisionResultType",
+    "StateConstraintGenerator",
+    "TransitionConstraintGenerator"
+]
 
 class AssignmentModel:
     def eval_bv(self, bv: z3.BitVecRef, model_completion: bool) -> z3.BitVecRef: ...
@@ -42,11 +60,11 @@ class CrackersConfig:
 
 
 class CrackersLogLevel:
-    Debug = CrackersLogLevel.Debug
-    Error = CrackersLogLevel.Error
-    Info = CrackersLogLevel.Info
-    Trace = CrackersLogLevel.Trace
-    Warn = CrackersLogLevel.Warn
+    Debug: int
+    Error: int
+    Info: int
+    Trace: int
+    Warn: int
 
 
 
@@ -92,8 +110,8 @@ class StateEqualityConstraint:
     memory: Optional[MemoryEqualityConstraint]
 
 class SynthesisSelectionStrategy:
-    SatStrategy = SynthesisSelectionStrategy.SatStrategy
-    OptimizeStrategy = SynthesisSelectionStrategy.OptimizeStrategy
+    SatStrategy: int
+    OptimizeStrategy: int
 
 class SynthesisConfig:
     strategy: SynthesisSelectionStrategy
@@ -118,13 +136,13 @@ class DecisionResult:
     Unsat : PythonDecisionResult_Unsat
 
 
-DecisionResultType = Union[DecisionResult.AssignmentFound, DecisionResult.Unsat]
+DecisionResultType = Union["PythonDecisionResult_AssignmentFound", "PythonDecisionResult_Unsat"]
 
 StateConstraintGenerator = Callable[[State, int], z3.BitVecRef]
 TransitionConstraintGenerator = Callable[[ModeledBlock], z3.BitVecRef]
 
 class SynthesisParams:
-    def run(self) -> DecisionResultType: ...
+    def run(self) -> "DecisionResultType": ...
     def add_precondition(self, fn: StateConstraintGenerator): ...
     def add_postcondition(self, fn: StateConstraintGenerator): ...
     def add_transition_constraint(self, fn: TransitionConstraintGenerator): ...

crackers_python/crackers/jingle_types.pyi

@@ -1,6 +1,6 @@
 from typing import Optional, Iterable, List
 
-from z3 import z3
+from z3 import z3  # type: ignore
 
 
 class Instruction:
@@ -40,7 +40,7 @@ class SleighContext:
     Represents a Sleigh context in python.
     """
 
-    def __init__(self, binary_path: str, ghidra: str) -> SleighContext: ...
+    def __init__(self, binary_path: str, ghidra: str) -> None: ...
 
     def instruction_at(self, offset: int) -> Optional[Instruction]: ...
 
@@ -50,7 +50,7 @@ class SleighContext:
 
 
 class State:
-    def __init__(self, jingle: SleighContext) -> State: ...
+    def __init__(self, jingle: SleighContext) -> None: ...
 
     def direct_varnode(self, space: str, offset: int, size: int) -> ResolvedVarNode: ...
 

crackers_python/mypy.ini

@@ -0,0 +1,5 @@
+[mypy]
+# Global mypy options can go here
+
+[mypy-z3.*]
+ignore_missing_imports = True

crackers_python/pyproject.toml

@@ -26,5 +26,6 @@ module-name = "crackers._internal"
 dev = [
     "ruff",
     "mypy",
-    "nox"
+    "nox",
+    "z3-solver"
 ]