77
88from pathos .pools import ProcessPool # type: ignore
99from pyk .cli_utils import dir_path , file_path
10- from pyk .kast import KApply , KAtt , KClaim , KDefinition , KFlatModule , KImport , KInner , KRequire , KRule , KToken
11- from pyk .kastManip import minimize_term
10+ from pyk .cterm import CTerm
11+ from pyk .kast import KApply , KAtt , KDefinition , KFlatModule , KImport , KInner , KRequire , KRewrite , KRule , KToken
12+ from pyk .kastManip import flatten_label , minimize_term , push_down_rewrites
1213from pyk .kcfg import KCFG
14+ from pyk .ktool .kit import KIT
1315from pyk .ktool .krun import _krun
14- from pyk .prelude .ml import mlTop
16+ from pyk .prelude .ml import is_top , mlTop
1517
1618from .gst_to_kore import gst_to_kore
1719from .kevm import KEVM , Foundry
1820from .solc_to_k import Contract , contract_to_main_module , method_to_cfg , solc_compile
19- from .utils import KPrint_make_unparsing , KProve_prove_claim , add_include_arg
21+ from .utils import KCFG__replace_node , KPrint_make_unparsing , KProve_prove_claim , add_include_arg , sanitize_config
2022
2123T = TypeVar ('T' )
2224
@@ -267,19 +269,19 @@ def exec_foundry_prove(
267269 workers : int = 1 ,
268270 minimize : bool = True ,
269271 lemmas : Iterable [str ] = (),
272+ simplify_init : bool = True ,
270273 ** kwargs : Any ,
271274) -> None :
272275 _ignore_arg (kwargs , 'main_module' , f'--main-module: { kwargs ["main_module" ]} )
273276 _ignore_arg (kwargs , 'syntax_module' , f'--syntax-module: { kwargs ["syntax_module" ]} )
274277 _ignore_arg (kwargs , 'definition_dir' , f'--definition: { kwargs ["definition_dir" ]} )
275278 _ignore_arg (kwargs , 'spec_module' , f'--spec-module: { kwargs ["spec_module" ]} )
276279 if workers <= 0 :
277- _LOGGER .error (f'Must have at least one worker, found: --workers { workers } )
278- sys .exit (1 )
280+ raise ValueError (f'Must have at least one worker, found: --workers { workers } )
279281 definition_dir = foundry_out / 'kompiled'
280282 use_directory = foundry_out / 'specs'
281283 use_directory .mkdir (parents = True , exist_ok = True )
282- kcfgs_dir = definition_dir / 'kcfgs'
284+ kcfgs_dir = foundry_out / 'kcfgs'
283285 if not kcfgs_dir .exists ():
284286 kcfgs_dir .mkdir ()
285287 foundry = Foundry (definition_dir , profile = profile , use_directory = use_directory )
@@ -315,7 +317,7 @@ def exec_foundry_prove(
315317 if unfound_tests :
316318 raise ValueError (f'Test identifiers not found: { unfound_tests } )
317319
318- kcfgs : Dict [str , KCFG ] = {}
320+ kcfgs : Dict [str , Tuple [ KCFG , Path ] ] = {}
319321 for test in tests :
320322 kcfg_file = kcfgs_dir / f'{ test }
321323 if reinit or not kcfg_file .exists ():
@@ -325,38 +327,138 @@ def exec_foundry_prove(
325327 method = [m for m in contract .methods if m .name == method_name ][0 ]
326328 empty_config = foundry .definition .empty_config (Foundry .Sorts .FOUNDRY_CELL )
327329 cfg = method_to_cfg (empty_config , contract , method )
328- kcfgs [test ] = cfg
330+ if simplify_init :
331+ _LOGGER .info (f'Simplifying initial state for test: { test } )
332+ edge = KCFG .Edge (cfg .get_unique_init (), cfg .get_unique_target (), mlTop (), - 1 )
333+ claim = edge .to_claim ()
334+ init_simplified = foundry .prove_claim (
335+ claim , f'simplify-init-{ cfg .get_unique_init ().id } , args = ['--depth' , '0' ]
336+ )
337+ init_simplified = sanitize_config (foundry .definition , init_simplified )
338+ cfg = KCFG__replace_node (cfg , cfg .get_unique_init ().id , CTerm (init_simplified ))
339+ _LOGGER .info (f'Simplifying target state for test: { test } )
340+ edge = KCFG .Edge (cfg .get_unique_target (), cfg .get_unique_init (), mlTop (), - 1 )
341+ claim = edge .to_claim ()
342+ target_simplified = foundry .prove_claim (
343+ claim , f'simplify-target-{ cfg .get_unique_target ().id } , args = ['--depth' , '0' ]
344+ )
345+ target_simplified = sanitize_config (foundry .definition , target_simplified )
346+ cfg = KCFG__replace_node (cfg , cfg .get_unique_target ().id , CTerm (target_simplified ))
347+ kcfgs [test ] = (cfg , kcfg_file )
329348 with open (kcfg_file , 'w' ) as kf :
330349 kf .write (json .dumps (cfg .to_dict ()))
331350 kf .close ()
332351 _LOGGER .info (f'Wrote file: { kcfg_file } )
333352 else :
334353 with open (kcfg_file , 'r' ) as kf :
335- kcfgs [test ] = KCFG .from_dict (json .loads (kf .read ()))
336-
337- def _kcfg_unproven_to_claim (_kcfg : KCFG ) -> KClaim :
338- return _kcfg .create_edge (_kcfg .get_unique_init ().id , _kcfg .get_unique_target ().id , mlTop (), depth = - 1 ).to_claim ()
354+ kcfgs [test ] = (KCFG .from_dict (json .loads (kf .read ())), kcfg_file )
339355
340356 lemma_rules = [KRule (KToken (lr , 'K' ), att = KAtt ({'simplification' : '' })) for lr in lemmas ]
341357
342- def prove_it (_id_and_cfg : Tuple [str , KCFG ]) -> bool :
343- _cfg_id , _cfg = _id_and_cfg
344- _claim = _kcfg_unproven_to_claim (_cfg )
358+ def _write_cfg (_cfg : KCFG , _cfgpath : Path ) -> None :
359+ with open (_cfgpath , 'w' ) as cfgfile :
360+ cfgfile .write (json .dumps (_cfg .to_dict ()))
361+ _LOGGER .info (f'Updated CFG file: { _cfgpath } )
362+
363+ def prove_it (_id_and_cfg : Tuple [str , Tuple [KCFG , Path ]]) -> bool :
364+ _cfg_id , (_cfg , _cfg_path ) = _id_and_cfg
365+ if len (_cfg .frontier ) == 0 :
366+ return True
367+ _init_node = _cfg .frontier [0 ]
368+ _target_node = _cfg .get_unique_target ()
369+ _claim = KCFG .Edge (_init_node , _target_node , mlTop (), - 1 ).to_claim ()
345370 _claim_id = _cfg_id .replace ('.' , '-' ).replace ('_' , '-' )
346371 ret , result = KProve_prove_claim (foundry , _claim , _claim_id , _LOGGER , depth = depth , lemmas = lemma_rules )
347- if minimize :
348- result = minimize_term (result )
349- print (f'Result for { _cfg_id } \n { foundry .pretty_print (result )} \n ' )
350- return ret
372+ _cfg .add_expanded (_init_node .id )
373+ if is_top (result ):
374+ _cfg .create_edge (_cfg .get_unique_init ().id , _cfg .get_unique_target ().id , mlTop (), - 1 )
375+ _LOGGER .info (f'Proof passed: { _cfg_id } )
376+ else :
377+ _cfg .add_expanded (_init_node .id )
378+ for result_state in flatten_label ('#Or' , result ):
379+ result_state = sanitize_config (foundry .definition , result_state )
380+ new_node = _cfg .get_or_create_node (CTerm (result_state ))
381+ _cfg .create_edge (_cfg .get_unique_init ().id , new_node .id , mlTop (), - 1 )
382+ if minimize :
383+ result_state = minimize_term (result_state )
384+ _LOGGER .error (f'Proof failed: { _cfg_id } \n { foundry .pretty_print (result_state )} )
385+ _write_cfg (_cfg , _cfg_path )
386+ failure_nodes = _cfg .frontier + _cfg .stuck
387+ return len (failure_nodes ) == 0
351388
352389 with ProcessPool (ncpus = workers ) as process_pool :
353390 results = process_pool .map (prove_it , kcfgs .items ())
354391 process_pool .close ()
355392
356- failed_cfgs = [cid for ((cid , _ ), failed ) in zip (kcfgs .items (), results ) if failed ]
357- if failed_cfgs :
358- print (f'Failed to prove KCFGs: { failed_cfgs } \n ' )
359- sys .exit (len (failed_cfgs ))
393+ failed = 0
394+ for (cid , _ ), succeeded in zip (kcfgs .items (), results ):
395+ if succeeded :
396+ print (f'PASSED: { cid } )
397+ else :
398+ print (f'FAILED: { cid } )
399+ failed += 1
400+ sys .exit (failed )
401+
402+
403+ def exec_foundry_show (
404+ profile : bool ,
405+ foundry_out : Path ,
406+ test : str ,
407+ nodes : Iterable [str ] = (),
408+ node_deltas : Iterable [Tuple [str , str ]] = (),
409+ minimize : bool = True ,
410+ ** kwargs : Any ,
411+ ) -> None :
412+ definition_dir = foundry_out / 'kompiled'
413+ use_directory = foundry_out / 'specs'
414+ use_directory .mkdir (parents = True , exist_ok = True )
415+ kcfgs_dir = foundry_out / 'kcfgs'
416+ foundry = Foundry (definition_dir , profile = profile , use_directory = use_directory )
417+ kcfg_file = kcfgs_dir / f'{ test }
418+ with open (kcfg_file , 'r' ) as kf :
419+ kcfg = KCFG .from_dict (json .loads (kf .read ()))
420+ list (map (print , kcfg .pretty (foundry )))
421+ for node_id in nodes :
422+ kast = kcfg .node (node_id ).cterm .kast
423+ if minimize :
424+ kast = minimize_term (kast )
425+ print (f'\n \n Node { node_id } \n \n { foundry .pretty_print (kast )} \n ' )
426+ for node_id_1 , node_id_2 in node_deltas :
427+ config_1 = kcfg .node (node_id_1 ).cterm .config
428+ config_2 = kcfg .node (node_id_2 ).cterm .config
429+ config_delta = push_down_rewrites (KRewrite (config_1 , config_2 ))
430+ if minimize :
431+ config_delta = minimize_term (config_delta )
432+ print (f'\n \n State Delta { node_id_1 } { node_id_2 } \n \n { foundry .pretty_print (config_delta )} \n ' )
433+
434+
435+ def exec_foundry_list (
436+ profile : bool ,
437+ foundry_out : Path ,
438+ details : bool = True ,
439+ ** kwargs : Any ,
440+ ) -> None :
441+ kcfgs_dir = foundry_out / 'kcfgs'
442+ pattern = '*.json'
443+ paths = kcfgs_dir .glob (pattern )
444+ for kcfg_file in paths :
445+ with open (kcfg_file , 'r' ) as kf :
446+ kcfg = KCFG .from_dict (json .loads (kf .read ()))
447+ kcfg_name = kcfg_file .name [0 :- 5 ]
448+ total_nodes = len (kcfg .nodes )
449+ frontier_nodes = len (kcfg .frontier )
450+ stuck_nodes = len (kcfg .stuck )
451+ proven = 'failed'
452+ if stuck_nodes == 0 :
453+ proven = 'pending'
454+ if frontier_nodes == 0 :
455+ proven = 'passed'
456+ print (f'{ kcfg_name } { proven } )
457+ if details :
458+ print (f' nodes: { total_nodes } )
459+ print (f' frontier: { frontier_nodes } )
460+ print (f' stuck: { stuck_nodes } )
461+ print ()
360462
361463
362464def exec_run (
@@ -599,6 +701,60 @@ def parse(s: str) -> List[T]:
599701 action = 'store_true' ,
600702 help = 'Reinitialize KCFGs even if they already exist.' ,
601703 )
704+ foundry_prove_args .add_argument (
705+ '--simplify-init' ,
706+ dest = 'simplify_init' ,
707+ default = True ,
708+ action = 'store_true' ,
709+ help = 'Simplify the initial and target states at startup.' ,
710+ )
711+ foundry_prove_args .add_argument (
712+ '--no-simplify-init' ,
713+ dest = 'simplify_init' ,
714+ action = 'store_false' ,
715+ help = 'Do not simplify the initial and target states at startup.' ,
716+ )
717+
718+ foundry_show_args = command_parser .add_parser (
719+ 'foundry-show' ,
720+ help = 'Display a given Foundry CFG.' ,
721+ parents = [shared_args , k_args ],
722+ )
723+ foundry_show_args .add_argument ('foundry_out' , type = dir_path , help = 'Path to Foundry output directory.' )
724+ foundry_show_args .add_argument ('test' , type = str , help = 'Display the CFG for this test.' )
725+ foundry_show_args .add_argument (
726+ '--node' ,
727+ type = str ,
728+ dest = 'nodes' ,
729+ default = [],
730+ action = 'append' ,
731+ help = 'List of nodes to display as well.' ,
732+ )
733+ foundry_show_args .add_argument (
734+ '--node-delta' ,
735+ type = KIT .arg_pair_of (str , str ),
736+ dest = 'node_deltas' ,
737+ default = [],
738+ action = 'append' ,
739+ help = 'List of nodes to display delta for.' ,
740+ )
741+ foundry_show_args .add_argument (
742+ '--minimize' , dest = 'minimize' , default = True , action = 'store_true' , help = 'Minimize output.'
743+ )
744+ foundry_show_args .add_argument (
745+ '--no-minimize' , dest = 'minimize' , action = 'store_false' , help = 'Do not minimize output.'
746+ )
747+
748+ foundry_list_args = command_parser .add_parser (
749+ 'foundry-list' ,
750+ help = 'List information about KCFGs on disk' ,
751+ parents = [shared_args , k_args ],
752+ )
753+ foundry_list_args .add_argument ('foundry_out' , type = dir_path , help = 'Path to Foundry output directory.' )
754+ foundry_list_args .add_argument (
755+ '--details' , dest = 'details' , default = True , action = 'store_true' , help = 'Information about progress on each KCFG.'
756+ )
757+ foundry_list_args .add_argument ('--no-details' , dest = 'details' , action = 'store_false' , help = 'Just list the KCFGs.' )
602758
603759 return parser
604760
0 commit comments