@@ -3,6 +3,7 @@ use std::fs;
33use std:: path:: PathBuf ;
44
55use clap:: { Parser , Subcommand } ;
6+ use jingle:: analysis:: varnode:: VarNodeSet ;
67use toml_edit:: ser:: to_string_pretty;
78use tracing:: { Level , event} ;
89use tracing_indicatif:: IndicatifLayer ;
@@ -22,7 +23,7 @@ use crackers::synthesis::DecisionResult;
2223use crackers:: synthesis:: assignment_model:: AssignmentModel ;
2324use jingle:: display:: JingleDisplayable ;
2425use jingle:: modeling:: ModelingContext ;
25- use jingle:: sleigh:: SpaceType ;
26+ use jingle:: sleigh:: { SpaceType , VarNode } ;
2627use jingle:: varnode:: ResolvedVarnode ;
2728use std:: collections:: BTreeSet ;
2829
@@ -58,10 +59,31 @@ fn main() {
5859 CrackersCommands :: New { config, library } => {
5960 init_basic_logging ( ) ;
6061 event ! ( Level :: INFO , "Creating new config file" ) ;
61- new (
62- config. clone ( ) . unwrap_or ( PathBuf :: from ( "./crackers.toml" ) ) ,
63- library. clone ( ) ,
64- )
62+ // If the user explicitly provided a config path, refuse to overwrite an existing file.
63+ if let Some ( cfg_path) = config {
64+ if cfg_path. exists ( ) {
65+ event ! (
66+ Level :: WARN ,
67+ "Refusing to create new config: file already exists: {}" ,
68+ cfg_path. display( )
69+ ) ;
70+ std:: process:: exit ( 1 ) ;
71+ }
72+ new ( cfg_path. clone ( ) , library. clone ( ) )
73+ } else {
74+ // If the user did not specify a config path, check the default file and
75+ // refuse to overwrite it as well.
76+ let default_path = PathBuf :: from ( "./crackers.toml" ) ;
77+ if default_path. exists ( ) {
78+ event ! (
79+ Level :: WARN ,
80+ "Refusing to create new config: default file already exists: {}" ,
81+ default_path. display( )
82+ ) ;
83+ std:: process:: exit ( 1 ) ;
84+ }
85+ new ( default_path, library. clone ( ) )
86+ }
6587 }
6688 CrackersCommands :: Synth { config } => {
6789 // Synth initializes its own logging with config
@@ -114,7 +136,7 @@ fn new(path: PathBuf, library: Option<PathBuf>) -> anyhow::Result<()> {
114136 ESI = COPY 0x40:4
115137 EDX = COPY 0x7b:4
116138 EAX = COPY 0xfacefeed:4
117- BRANCH 0xdeadbeef:1
139+ BRANCH 0xdeadbeef:8
118140 "
119141 . to_string ( ) ,
120142 ) ,
@@ -256,6 +278,104 @@ fn format_resolved_varnode<T: ModelingContext>(
256278 }
257279}
258280
281+ /// Shared helper to collect varnodes (registers and iptr-style) from the model.
282+ ///
283+ /// - `collect_inputs`: if true, collects gadget inputs; otherwise collects outputs.
284+ /// - `use_original_state`: if true, reads values from the chain's original state; otherwise final state.
285+ ///
286+ /// Returns: (register_vector, varnode_set, iptr_description_set)
287+ fn collect_varnodes < T : ModelingContext > (
288+ model : & AssignmentModel < T > ,
289+ collect_inputs : bool ,
290+ use_original_state : bool ,
291+ ) -> ( Vec < ( String , String ) > , VarNodeSet , BTreeSet < String > ) {
292+ let mut reg_vec: Vec < ( String , String ) > = Vec :: new ( ) ;
293+ let mut reg_seen: BTreeSet < String > = BTreeSet :: new ( ) ;
294+
295+ let mut iptr_vn_set: VarNodeSet = VarNodeSet :: default ( ) ;
296+ let mut iptr_descs: BTreeSet < String > = BTreeSet :: new ( ) ;
297+
298+ for gadget in model. gadgets . iter ( ) {
299+ let iter = if collect_inputs {
300+ gadget. get_inputs ( )
301+ } else {
302+ gadget. get_outputs ( )
303+ } ;
304+
305+ for vn in iter {
306+ match & vn {
307+ ResolvedVarnode :: Direct ( d) => {
308+ let space_info = model. arch_info . get_space ( d. space_index ) ;
309+ let is_register = space_info. map ( |s| s. name == "register" ) . unwrap_or ( false ) ;
310+ let is_iptr = space_info
311+ . map ( |s| s. _type == SpaceType :: IPTR_PROCESSOR )
312+ . unwrap_or ( false ) ;
313+
314+ let desc = format_resolved_varnode ( & vn, model) ;
315+
316+ // choose state to read from
317+ let read_result = if use_original_state {
318+ gadget. get_original_state ( ) . read_resolved ( & vn)
319+ } else {
320+ gadget. get_final_state ( ) . read_resolved ( & vn)
321+ } ;
322+
323+ let val_str = match read_result {
324+ Ok ( bv) => match model. model ( ) . eval ( & bv, true ) {
325+ Some ( v) => format ! ( "{}" , v) ,
326+ None => "<unable to evaluate>" . to_string ( ) ,
327+ } ,
328+ Err ( _) => "<unable to read>" . to_string ( ) ,
329+ } ;
330+
331+ if is_register {
332+ if !reg_seen. contains ( & desc) {
333+ reg_seen. insert ( desc. clone ( ) ) ;
334+ reg_vec. push ( ( desc, val_str) ) ;
335+ }
336+ } else if is_iptr {
337+ // convert Direct resolved varnode into VarNode and insert
338+ let vn_struct = VarNode {
339+ size : d. size ,
340+ space_index : d. space_index ,
341+ offset : d. offset ,
342+ } ;
343+ iptr_vn_set. insert ( & vn_struct) ;
344+ iptr_descs. insert ( format ! ( "{} = {}" , desc, val_str) ) ;
345+ }
346+ }
347+ ResolvedVarnode :: Indirect ( i) => {
348+ // insert the pointer_location varnode into set
349+ let ptr_loc = & i. pointer_location ;
350+ let vn_struct = VarNode {
351+ size : ptr_loc. size ,
352+ space_index : ptr_loc. space_index ,
353+ offset : ptr_loc. offset ,
354+ } ;
355+ iptr_vn_set. insert ( & vn_struct) ;
356+
357+ let desc = format_resolved_varnode ( & vn, model) ;
358+ let read_result = if use_original_state {
359+ gadget. get_original_state ( ) . read_resolved ( & vn)
360+ } else {
361+ gadget. get_final_state ( ) . read_resolved ( & vn)
362+ } ;
363+ let val_str = match read_result {
364+ Ok ( bv) => match model. model ( ) . eval ( & bv, true ) {
365+ Some ( v) => format ! ( "{}" , v) ,
366+ None => "<unable to evaluate>" . to_string ( ) ,
367+ } ,
368+ Err ( _) => "<unable to read>" . to_string ( ) ,
369+ } ;
370+ iptr_descs. insert ( format ! ( "{} = {}" , desc, val_str) ) ;
371+ }
372+ }
373+ }
374+ }
375+
376+ ( reg_vec, iptr_vn_set, iptr_descs)
377+ }
378+
259379fn print_assignment_details < T : ModelingContext > ( model : & AssignmentModel < T > ) {
260380 println ! ( "\n ========== Assignment Model Details ==========\n " ) ;
261381
@@ -267,79 +387,34 @@ fn print_assignment_details<T: ModelingContext>(model: &AssignmentModel<T>) {
267387 "If you need this, consider using the rust or python API to encode your constraint.\n "
268388 ) ;
269389
270- // Collect all inputs and their valuations
271- println ! ( "--- Inputs (Locations Read) ---" ) ;
272- let mut inputs_set: BTreeSet < String > = BTreeSet :: new ( ) ;
273-
274- for ( gadget_idx, gadget) in model. gadgets . iter ( ) . enumerate ( ) {
275- println ! ( "Gadget {}:" , gadget_idx) ;
276- for input in gadget. get_inputs ( ) {
277- // Filter out unique space variables (keep only IPTR_PROCESSOR)
278- let should_print = match & input {
279- ResolvedVarnode :: Direct ( d) => model
280- . arch_info
281- . get_space ( d. space_index )
282- . map ( |s| s. _type == SpaceType :: IPTR_PROCESSOR )
283- . unwrap_or ( false ) ,
284- ResolvedVarnode :: Indirect ( _) => true ,
285- } ;
286-
287- if !should_print {
288- continue ;
289- }
390+ // Inputs (read values from original state)
391+ println ! ( "--- Inputs (Locations Read) ---\n " ) ;
392+ let ( mut reg_vec, _iptr_vn_set, iptr_descs) = collect_varnodes ( model, true , true ) ;
290393
291- let input_desc = format_resolved_varnode ( & input, model) ;
394+ // sort alphabetically by register description
395+ reg_vec. sort_by ( |a, b| a. 0 . cmp ( & b. 0 ) ) ;
292396
293- // Try to read the value from the initial state of this gadget
294- if let Ok ( bv) = gadget. get_original_state ( ) . read_resolved ( & input) {
295- if let Some ( val) = model. model ( ) . eval ( & bv, true ) {
296- println ! ( " {} = {}" , input_desc, val) ;
297- inputs_set. insert ( input_desc) ;
298- } else {
299- println ! ( " {} = <unable to evaluate>" , input_desc) ;
300- }
301- } else {
302- println ! ( " {} = <unable to read>" , input_desc) ;
303- }
304- }
397+ for ( desc, val) in & reg_vec {
398+ println ! ( " {} = {}" , desc, val) ;
399+ }
400+ for desc in & iptr_descs {
401+ println ! ( " {}" , desc) ;
305402 }
403+
306404 println ! ( ) ;
307405
308- // Collect all outputs and their valuations at the end of the chain
309- println ! ( "--- Outputs (Locations Written) ---" ) ;
310- let mut outputs_set: BTreeSet < String > = BTreeSet :: new ( ) ;
311-
312- for ( gadget_idx, gadget) in model. gadgets . iter ( ) . enumerate ( ) {
313- println ! ( "Gadget {}:" , gadget_idx) ;
314- for output in gadget. get_outputs ( ) {
315- // Filter out unique space variables (keep only IPTR_PROCESSOR)
316- let should_print = match & output {
317- ResolvedVarnode :: Direct ( d) => model
318- . arch_info
319- . get_space ( d. space_index )
320- . map ( |s| s. _type == SpaceType :: IPTR_PROCESSOR )
321- . unwrap_or ( false ) ,
322- ResolvedVarnode :: Indirect ( _) => true ,
323- } ;
324-
325- if !should_print {
326- continue ;
327- }
406+ // Outputs (read values from final state)
407+ println ! ( "--- Outputs (Locations Written) ---\n " ) ;
408+ let ( mut out_reg_vec, _out_iptr_vn_set, out_iptr_descs) = collect_varnodes ( model, false , false ) ;
328409
329- let output_desc = format_resolved_varnode ( & output, model) ;
410+ // sort alphabetically by register description
411+ out_reg_vec. sort_by ( |a, b| a. 0 . cmp ( & b. 0 ) ) ;
330412
331- // Read the value from the final state of this gadget
332- if let Ok ( bv) = gadget. get_final_state ( ) . read_resolved ( & output) {
333- if let Some ( val) = model. model ( ) . eval ( & bv, true ) {
334- println ! ( " {} = {}" , output_desc, val) ;
335- outputs_set. insert ( output_desc) ;
336- } else {
337- println ! ( " {} = <unable to evaluate>" , output_desc) ;
338- }
339- } else {
340- println ! ( " {} = <unable to read>" , output_desc) ;
341- }
342- }
413+ for ( desc, val) in & out_reg_vec {
414+ println ! ( " {} = {}" , desc, val) ;
415+ }
416+ for desc in & out_iptr_descs {
417+ println ! ( " {}" , desc) ;
343418 }
344419
345420 println ! ( "\n ==============================================\n " ) ;
0 commit comments