1- from typing import Callable , Iterable , Optional , Union
1+ from typing import Callable , Dict , Iterable , List , Optional , Tuple , Union
22
33from z3 import z3 # type: ignore
44
@@ -65,11 +65,16 @@ class CrackersLogLevel:
6565 Trace : int
6666 Warn : int
6767
68+ class LoadedLibraryConfig :
69+ path : str
70+ base_address : Optional [int ]
71+
6872class GadgetLibraryConfig :
6973 max_gadget_length : int
7074 path : str
7175 sample_size : Optional [int ]
7276 base_address : Optional [int ]
77+ loaded_libraries : Optional [List [LoadedLibraryConfig ]]
7378
7479class MemoryEqualityConstraint :
7580 space : str
@@ -91,7 +96,7 @@ class PointerRangeConstraints:
9196class SleighConfig :
9297 ghidra_path : str
9398
94- # New: represent the two possible shapes of the specification
99+ # Represent the two possible shapes of the specification
95100class BinaryFileSpecification :
96101 """
97102 Represents the binary-file variant of the specification.
@@ -110,7 +115,7 @@ class RawPcodeSpecification:
110115
111116 raw_pcode : str
112117
113- # SpecificationConfig is now a discriminated union of the two variants above.
118+ # SpecificationConfig is a discriminated union of the two variants above.
114119SpecificationConfig = Union [BinaryFileSpecification , RawPcodeSpecification ]
115120
116121class StateEqualityConstraint :
@@ -137,7 +142,7 @@ class SelectionFailure:
137142
138143class PythonDecisionResult_Unsat (DecisionResult ):
139144 _0 : SelectionFailure
140- pass
145+ __match_args__ = ( "_0" ,)
141146
142147class DecisionResult :
143148 AssignmentFound : PythonDecisionResult_AssignmentFound
@@ -151,8 +156,7 @@ StateConstraintGenerator = Callable[[State, int], z3.BoolRef]
151156TransitionConstraintGenerator = Callable [[ModeledBlock ], z3 .BoolRef ]
152157
153158class SynthesisParams :
154- def run (self ) -> "DecisionResultType" : ...
155- def add_precondition (self , fn : StateConstraintGenerator ): ...
156- def add_postcondition (self , fn : StateConstraintGenerator ): ...
157- def add_transition_constraint (self , fn : TransitionConstraintGenerator ): ...
158- pass
159+ def run (self ) -> DecisionResultType : ...
160+ def add_precondition (self , fn : StateConstraintGenerator ) -> None : ...
161+ def add_postcondition (self , fn : StateConstraintGenerator ) -> None : ...
162+ def add_transition_constraint (self , fn : TransitionConstraintGenerator ) -> None : ...
0 commit comments