@@ -2,7 +2,11 @@ use crackers::synthesis::assignment_model::AssignmentModel;
22use jingle:: modeling:: { ModeledBlock , ModelingContext } ;
33use jingle:: python:: modeled_block:: PythonModeledBlock ;
44use jingle:: python:: state:: PythonState ;
5- use pyo3:: { pyclass, pymethods} ;
5+ use jingle:: python:: varode_iterator:: VarNodeIterator ;
6+ use jingle:: python:: z3:: ast:: { TryFromPythonZ3 , TryIntoPythonZ3 } ;
7+ use pyo3:: exceptions:: PyRuntimeError ;
8+ use pyo3:: { pyclass, pymethods, Py , PyAny , PyResult } ;
9+ use z3:: ast:: BV ;
610
711#[ pyclass( unsendable) ]
812pub struct PythonAssignmentModel {
@@ -11,6 +15,17 @@ pub struct PythonAssignmentModel {
1115
1216#[ pymethods]
1317impl PythonAssignmentModel {
18+
19+ fn eval_bv ( & self , bv : Py < PyAny > , model_completion : bool ) -> PyResult < Py < PyAny > > {
20+ let bv = BV :: try_from_python ( bv) ?;
21+ let val = self
22+ . inner
23+ . model ( )
24+ . eval ( & bv, model_completion)
25+ . ok_or ( PyRuntimeError :: new_err ( "Could not eval model" ) ) ?;
26+ val. try_into_python ( )
27+ }
28+
1429 pub fn initial_state ( & self ) -> Option < PythonState > {
1530 self . inner . gadgets . first ( ) . map ( |f| PythonState {
1631 state : f. get_original_state ( ) . clone ( ) ,
@@ -31,4 +46,26 @@ impl PythonAssignmentModel {
3146 . map ( |g| PythonModeledBlock { instr : g } )
3247 . collect ( )
3348 }
49+
50+ pub fn inputs ( & self ) -> Option < VarNodeIterator > {
51+ let state = self . inner . initial_state ( ) ?;
52+ Some ( VarNodeIterator :: new (
53+ state. clone ( ) ,
54+ self . inner
55+ . gadgets
56+ . iter ( )
57+ . flat_map ( |g| g. get_inputs ( ) . into_iter ( ) ) ,
58+ ) )
59+ }
60+
61+ pub fn outputs ( & self ) -> Option < VarNodeIterator > {
62+ let state = self . inner . initial_state ( ) ?;
63+ Some ( VarNodeIterator :: new (
64+ state. clone ( ) ,
65+ self . inner
66+ . gadgets
67+ . iter ( )
68+ . flat_map ( |g| g. get_outputs ( ) . into_iter ( ) ) ,
69+ ) )
70+ }
3471}
0 commit comments