From 8e8ee81627dc63138ff101f2f6975645e458d907 Mon Sep 17 00:00:00 2001 From: Paul Gazzillo Date: Thu, 18 Jul 2024 12:15:21 -0400 Subject: [PATCH 1/9] Import multiprocessing and the tqdm progress bar --- kmax/kismet | 2 ++ setup.py | 1 + 2 files changed, 3 insertions(+) diff --git a/kmax/kismet b/kmax/kismet index bf6ce39c..f7400f4c 100644 --- a/kmax/kismet +++ b/kmax/kismet @@ -15,6 +15,8 @@ import logging import subprocess import csv from time import perf_counter +from multiprocessing import Pool +import tqdm import kmax.about # to enable the --version flag def __get_time_refpoint(): diff --git a/setup.py b/setup.py index 55a24fd5..0aa94178 100644 --- a/setup.py +++ b/setup.py @@ -49,6 +49,7 @@ def read(fname): 'requests', 'whatthepatch', 'packaging', + 'tqdm', ], include_package_data=True, ) From 1b7575ed3748f1ad1e5a66335ebe1eced4748bd4 Mon Sep 17 00:00:00 2001 From: Paul Gazzillo Date: Thu, 18 Jul 2024 12:16:44 -0400 Subject: [PATCH 2/9] Remove main method to make use of parallelism easier This avoids the use of nested functions in main, which made using the multiprocessor library harder to use --- kmax/kismet | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/kmax/kismet b/kmax/kismet index f7400f4c..654d4224 100644 --- a/kmax/kismet +++ b/kmax/kismet @@ -240,7 +240,7 @@ def get_unmet_constraints(arch, selectors=None, selectees=None, syntactical_opti return unmet_constraints_mapping -def main(): +if __name__ == '__main__': t_start_main = __get_time_refpoint() argparser = argparse.ArgumentParser() @@ -1083,14 +1083,13 @@ def main(): if row: csv_writer.writerow(row) info("Summary csv was written.") -if __name__ == '__main__': - try: - main() - except Arch.CantOpenKconfigFiles as e: - kc = e.kextract_complaints - message = "Can't open Kconfig files:" - for i in kc: - message += "\n %s" % i - error(message) - exit(1) + # try: + # main() + # except Arch.CantOpenKconfigFiles as e: + # kc = e.kextract_complaints + # message = "Can't open Kconfig files:" + # for i in kc: + # message += "\n %s" % i + # error(message) + # exit(1) From d0a87ee4352de8119d837ea7ea5cca4ca97b339c Mon Sep 17 00:00:00 2001 From: Paul Gazzillo Date: Thu, 18 Jul 2024 12:19:57 -0400 Subject: [PATCH 3/9] Add an argument for the number of processes to use --- kmax/kismet | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/kmax/kismet b/kmax/kismet index 654d4224..bb65fe5a 100644 --- a/kmax/kismet +++ b/kmax/kismet @@ -325,6 +325,10 @@ if __name__ == '__main__': argparser.add_argument('--allow-config-broken', action="store_true", help="""Allow CONFIG_BROKEN dependencies. """) + argparser.add_argument('--processes', '-p', + type=int, + default=None, + help=f"""Number of concurrent processes to run. Defaults to os.cpu_count() ({os.cpu_count()})""") argparser.add_argument('--verbose', action="store_true", help="""Verbose mode prints additional messages to stderr.""") @@ -359,6 +363,7 @@ if __name__ == '__main__': summary_txt_path = args.summary_txt if args.summary_txt != None else "kismet_summary_%s.txt" % arch_name summary_use_testcase_realpath= args.use_fullpath_in_summary disable_config_broken = not args.allow_config_broken + processes=args.processes verbose = args.verbose if not precise_SAT_pass: From 7b0320dd5d1056f22dc2d3d0289d07d73a56d0cc Mon Sep 17 00:00:00 2001 From: Paul Gazzillo Date: Thu, 18 Jul 2024 12:26:53 -0400 Subject: [PATCH 4/9] Get a set of triples for each check (selectee, selector, visib_id) The original loops over a triple array with three loops. This set of triples will be used to replace that triple-loop body with a function that we can call each triple on to do the analysis steps. --- kmax/kismet | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kmax/kismet b/kmax/kismet index bb65fe5a..533b1bb6 100644 --- a/kmax/kismet +++ b/kmax/kismet @@ -532,6 +532,8 @@ if __name__ == '__main__': def dump_optimizedtest_progress(): current_time = datetime.datetime.now().strftime("%H:%M:%S") info("%s Optimized SAT pass progress: %s." % (current_time, dumps_progress(checked, total_to_check)), ending="\r") + # get set of triples to check + triples = [ (selectee, selector, visib_id) for selectee in unmet_constraints for selector in unmet_constraints[selectee] for visib_id in unmet_constraints[selectee][selector] ] if optimized_SAT_pass: total_to_check = counts[UnmetDepResult.UNMET_ALARM] From d39b5f70eb565e9a2af89dd18bc33e214494cc78 Mon Sep 17 00:00:00 2001 From: Paul Gazzillo Date: Thu, 18 Jul 2024 13:14:15 -0400 Subject: [PATCH 5/9] Replace the optimized analysis loop with a multiprocessor pool The body of the loop has been factored out into do_optimized, which takes a triple of the elements from the original triple loop. It returns a tuple of the results that were originally collected within the loop. The creation of the pool can fail if ulimit is too low, so there is a try-except to check for it. The pool is run with imap_unordered, which goes over the triples as an iterable in any order and runs do_optimized on each element. The results are run through tqdm to provide a progress bar. The results are looped over and saved in the unmet_constraints results structure. The counter for optimized pass found cases has been moved into the multiprocessor loop to avoid having to make a multiprocessor counter. --- kmax/kismet | 90 ++++++++++++++++++++++++++++++++--------------------- 1 file changed, 54 insertions(+), 36 deletions(-) diff --git a/kmax/kismet b/kmax/kismet index 533b1bb6..11147b5a 100644 --- a/kmax/kismet +++ b/kmax/kismet @@ -542,45 +542,63 @@ if __name__ == '__main__': count_sat_options_created = 0 info("Doing optimized SAT pass for %d constructs" % total_to_check) t_start_optimizedpass = __get_time_refpoint() - - for selectee in unmet_constraints: - for selector in unmet_constraints[selectee]: - for visib_id in unmet_constraints[selectee][selector]: - # dump progress - dump_optimizedtest_progress() - analysis_result = unmet_constraints[selectee][selector][visib_id]["generic"]["analysis_result"] - - # if the result from the previous step(s) is ALARM, check if now can prove safe - if analysis_result == UnmetDepResult.UNMET_ALARM: - checked += 1 - constraint = unmet_constraints[selectee][selector][visib_id]["generic"]["constraint"] - - if not check_sat(constraint): - unmet_constraints[selectee][selector][visib_id]["generic"]["analysis_result"] = UnmetDepResult.UNMET_SAFE_OPTIMIZED_PASS - optimized_pass_eliminated += 1 - else: - # can't draw a conclusion yet, need precise test - - # if explore_whole_unmet_space, multiple different solutions will - # be checked per select construct on varying SAT expressions for - # optimized constraints. create the constraints here. - if explore_whole_unmet_space: - all_sat_exprs_to_optimized_constraints = get_all_sat_exprs(constraint) - - # push each SAT expr to be checked at precise test - unmet_constraints[selectee][selector][visib_id]["sat_options"] = [] - for i, c in enumerate(all_sat_exprs_to_optimized_constraints): - sat_option = { - "constraint" : c, - "analysis_result" : UnmetDepResult.UNMET_ALARM } - unmet_constraints[selectee][selector][visib_id]["sat_options"].append(sat_option) - count_sat_options_created += 1 - - # dump progress - dump_optimizedtest_progress() + def do_optimized(triple): + selectee, selector, visib_id = triple + # # dump progress + # dump_optimizedtest_progress() + + analysis_result = unmet_constraints[selectee][selector][visib_id]["generic"]["analysis_result"] + sat_options = [] + + # if the result from the previous step(s) is ALARM, check if now can prove safe + if analysis_result == UnmetDepResult.UNMET_ALARM: + # checked += 1 + constraint = unmet_constraints[selectee][selector][visib_id]["generic"]["constraint"] + + if not check_sat(constraint): + analysis_result = UnmetDepResult.UNMET_SAFE_OPTIMIZED_PASS + # optimized_pass_eliminated += 1 + else: + pass + # can't draw a conclusion yet, need precise test + + # # if explore_whole_unmet_space, multiple different solutions will + # # be checked per select construct on varying SAT expressions for + # # optimized constraints. create the constraints here. + # if explore_whole_unmet_space: + # all_sat_exprs_to_optimized_constraints = get_all_sat_exprs(constraint) + + # # push each SAT expr to be checked at precise test + # sat_options = [] + # for i, c in enumerate(all_sat_exprs_to_optimized_constraints): + # sat_option = { + # "constraint" : c, + # "analysis_result" : UnmetDepResult.UNMET_ALARM } + # sat_options.append(sat_option) + # # count_sat_options_created += 1 + + # # dump progress + # dump_optimizedtest_progress() + else: + pass + + return selectee, selector, visib_id, analysis_result, sat_options info("") # complete progress + # optimized checks for all triples + try: + p = Pool(processes=processes) + except OSError: + logging.exception("Could not create multiprocessing pool. Try increasing ulimit or lowering the number of processes.") + exit(13) + with p: + for selectee, selector, visib_id, analysis_result, sat_options in tqdm.tqdm(p.imap_unordered(do_optimized, triples), total=len(triples)): + unmet_constraints[selectee][selector][visib_id]["generic"]["analysis_result"] = analysis_result + unmet_constraints[selectee][selector][visib_id]["sat_options"] = sat_options + if analysis_result == UnmetDepResult.UNMET_SAFE_OPTIMIZED_PASS: + optimized_pass_eliminated += 1 + # update the counts after the optimized pass counts[UnmetDepResult.UNMET_ALARM] -= optimized_pass_eliminated # this doesn't account for SAT options due to explore_whole_unmet_space since alarm is per unique select constructs counts[UnmetDepResult.UNMET_SAFE_OPTIMIZED_PASS] = optimized_pass_eliminated From bd10e4c37112bfc4ba3ffa622e8184d1c1b76735 Mon Sep 17 00:00:00 2001 From: Paul Gazzillo Date: Thu, 18 Jul 2024 14:18:06 -0400 Subject: [PATCH 6/9] Paralleize the precise checker This is similar to the parallelization of the optimized checker, with the body of the triple look factored out into a separate function, and a multiprocessor pool calling it on each triple (selectee, selector, visib_id) and aggregating the results. --- kmax/kismet | 121 ++++++++++++++++++++++++++++++---------------------- 1 file changed, 71 insertions(+), 50 deletions(-) diff --git a/kmax/kismet b/kmax/kismet index 11147b5a..adb7e544 100644 --- a/kmax/kismet +++ b/kmax/kismet @@ -664,64 +664,85 @@ if __name__ == '__main__': current_time = datetime.datetime.now().strftime("%H:%M:%S") info("%s Precise SAT pass progress: %s." % (current_time, dumps_progress(checked, total_to_check)), ending="\r") - for selectee in unmet_constraints: - for selector in unmet_constraints[selectee]: - for visib_id in unmet_constraints[selectee][selector]: - # dump progress - dump_precisetest_progress() + def do_precise(triple): + selectee, selector, visib_id = triple + # # dump progress + # dump_precisetest_progress() - analysis_result = unmet_constraints[selectee][selector][visib_id]["generic"]["analysis_result"] - - # if the result from the previous step(s) is ALARM, check if now can prove safe - if analysis_result == UnmetDepResult.UNMET_ALARM: - - generic_constraint = unmet_constraints[selectee][selector][visib_id]["generic"]["constraint"] + analysis_result = unmet_constraints[selectee][selector][visib_id]["generic"]["analysis_result"] + config_content = None - try_force_udd_param = selectee if force_target_udd_only else None - is_sat, payload, is_target_udd_only_forced = precise_check(optimized_constraints=generic_constraint, try_force_target_udd_only_for_selectee=try_force_udd_param) - - if not is_sat: - unmet_constraints[selectee][selector][visib_id]["generic"]["analysis_result"] = UnmetDepResult.UNMET_SAFE_PRECISE_PASS + # if the result from the previous step(s) is ALARM, check if now can prove safe + if analysis_result == UnmetDepResult.UNMET_ALARM: - num_precise_safe += 1 - else: - if force_target_udd_only: unmet_constraints[selectee][selector][visib_id]["generic"]["forced_target_udd_only"] = is_target_udd_only_forced - unmet_constraints[selectee][selector][visib_id]["generic"]["analysis_result"] = UnmetDepResult.UNMET_ALARM - unmet_constraints[selectee][selector][visib_id]["generic"]["model"] = payload + generic_constraint = unmet_constraints[selectee][selector][visib_id]["generic"]["constraint"] - num_models += 1 - num_alarms += 1 - - checked += 1 + try_force_udd_param = selectee if force_target_udd_only else None + is_sat, payload, is_target_udd_only_forced = precise_check(optimized_constraints=generic_constraint, try_force_target_udd_only_for_selectee=try_force_udd_param) - # - # Explore whole unmet space - # - if explore_whole_unmet_space and is_sat: - is_generic_sat = is_sat - sat_options = unmet_constraints[selectee][selector][visib_id]["sat_options"] + if not is_sat: + analysis_result = UnmetDepResult.UNMET_SAFE_PRECISE_PASS + # num_precise_safe += 1 + else: + if force_target_udd_only: unmet_constraints[selectee][selector][visib_id]["generic"]["forced_target_udd_only"] = is_target_udd_only_forced + analysis_result = UnmetDepResult.UNMET_ALARM + config_content = Klocalizer.get_config_from_model(payload, arch, set_tristate_m=False, allow_non_visibles=False) - if not is_generic_sat: - for sat_option in sat_options: - sat_option["analysis_result"] = UnmetDepResult.UNMET_SAFE_PRECISE_PASS - else: - for sat_option in sat_options: - is_sat, payload, is_target_udd_only_forced = precise_check(optimized_constraints=sat_option["constraint"], try_force_target_udd_only_for_selectee=try_force_udd_param) - - if not is_sat: - sat_option["analysis_result"] = UnmetDepResult.UNMET_SAFE_PRECISE_PASS - num_precise_safe_sat_options += 1 - else: - if force_target_udd_only: sat_option["forced_target_udd_only"] = is_target_udd_only_forced - sat_option["analysis_result"] = UnmetDepResult.UNMET_ALARM - sat_option["model"] = payload - num_alarms_sat_options += 1 - num_models += 1 - - # dump progress - dump_precisetest_progress() + # num_models += 1 + # num_alarms += 1 + + # checked += 1 + + # # + # # Explore whole unmet space + # # + # if explore_whole_unmet_space and is_sat: + # is_generic_sat = is_sat + # sat_options = unmet_constraints[selectee][selector][visib_id]["sat_options"] + + # if not is_generic_sat: + # for sat_option in sat_options: + # sat_option["analysis_result"] = UnmetDepResult.UNMET_SAFE_PRECISE_PASS + # else: + # for sat_option in sat_options: + # is_sat, payload, is_target_udd_only_forced = precise_check(optimized_constraints=sat_option["constraint"], try_force_target_udd_only_for_selectee=try_force_udd_param) + + # if not is_sat: + # sat_option["analysis_result"] = UnmetDepResult.UNMET_SAFE_PRECISE_PASS + # # num_precise_safe_sat_options += 1 + # else: + # if force_target_udd_only: sat_option["forced_target_udd_only"] = is_target_udd_only_forced + # sat_option["analysis_result"] = UnmetDepResult.UNMET_ALARM + # sat_option["model"] = payload + # # num_alarms_sat_options += 1 + # # num_models += 1 + + # # dump progress + # dump_precisetest_progress() + else: + pass + return selectee, selector, visib_id, analysis_result, config_content + info("") # complete the progress + + try: + p = Pool(processes=processes) + except OSError: + logging.exception("Could not create multiprocessing pool. Try increasing ulimit or lowering the number of processes.") + exit(13) + with p: + for selectee, selector, visib_id, analysis_result, config_content in tqdm.tqdm(p.imap_unordered(do_precise, triples), total=len(triples)): + unmet_constraints[selectee][selector][visib_id]["generic"]["analysis_result"] = analysis_result + unmet_constraints[selectee][selector][visib_id]["generic"]["config_content"] = config_content + if analysis_result == UnmetDepResult.UNMET_SAFE_PRECISE_PASS: + num_precise_safe += 1 + checked += 1 + elif analysis_result == UnmetDepResult.UNMET_ALARM: + num_models += 1 + num_alarms += 1 + checked += 1 + # update the counts after the optimized pass counts[UnmetDepResult.UNMET_ALARM] = num_alarms counts[UnmetDepResult.UNMET_SAFE_PRECISE_PASS] = num_precise_safe From 54788986ec8262be358c73f741f3ac03dbb51c75 Mon Sep 17 00:00:00 2001 From: Paul Gazzillo Date: Thu, 18 Jul 2024 14:21:37 -0400 Subject: [PATCH 7/9] Generate the config file from the model inside the precise checker z3 data structure fail to be serialized, making them not work as a return value from multiprocessor processes. Instead, do_precise generates the resulting config file from the z3 model, which can be serialized as a return value. --- kmax/kismet | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/kmax/kismet b/kmax/kismet index adb7e544..40c68920 100644 --- a/kmax/kismet +++ b/kmax/kismet @@ -812,8 +812,7 @@ if __name__ == '__main__': dump_testcasegen_progress() if generic_result == UnmetDepResult.UNMET_ALARM: - z3_model = unmet_constraints[selectee][selector][visib_id]["generic"]["model"] - config_content = Klocalizer.get_config_from_model(z3_model, arch, set_tristate_m=False, allow_non_visibles=False) + config_content = unmet_constraints[selectee][selector][visib_id]["generic"]["config_content"] cfgfilepath = get_cfgfilepath(selectee, selector, visib_id, 0) # TODO: include metadata as comment in the config file for later convenience From 84173bf01c26315617aa6abdd61f74e3db3b0dcd Mon Sep 17 00:00:00 2001 From: Paul Gazzillo Date: Thu, 18 Jul 2024 14:24:01 -0400 Subject: [PATCH 8/9] No longer need this progress out with tqdm --- kmax/kismet | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/kmax/kismet b/kmax/kismet index 40c68920..cf73eec4 100644 --- a/kmax/kismet +++ b/kmax/kismet @@ -529,9 +529,10 @@ if __name__ == '__main__': # Optimized test # # do optimized-constraints pass -- the SAT solver pass only on optimized constraints -- without full kclause constraints - def dump_optimizedtest_progress(): - current_time = datetime.datetime.now().strftime("%H:%M:%S") - info("%s Optimized SAT pass progress: %s." % (current_time, dumps_progress(checked, total_to_check)), ending="\r") + # def dump_optimizedtest_progress(): + # current_time = datetime.datetime.now().strftime("%H:%M:%S") + # info("%s Optimized SAT pass progress: %s." % (current_time, dumps_progress(checked, total_to_check)), ending="\r") + # get set of triples to check triples = [ (selectee, selector, visib_id) for selectee in unmet_constraints for selector in unmet_constraints[selectee] for visib_id in unmet_constraints[selectee][selector] ] @@ -660,9 +661,9 @@ if __name__ == '__main__': return is_sat, payload, is_target_udd_only_forced - def dump_precisetest_progress(): - current_time = datetime.datetime.now().strftime("%H:%M:%S") - info("%s Precise SAT pass progress: %s." % (current_time, dumps_progress(checked, total_to_check)), ending="\r") + # def dump_precisetest_progress(): + # current_time = datetime.datetime.now().strftime("%H:%M:%S") + # info("%s Precise SAT pass progress: %s." % (current_time, dumps_progress(checked, total_to_check)), ending="\r") def do_precise(triple): selectee, selector, visib_id = triple From 24d0ed867aef1526f504bced340791a85a5fb631 Mon Sep 17 00:00:00 2001 From: Paul Gazzillo Date: Thu, 18 Jul 2024 14:24:56 -0400 Subject: [PATCH 9/9] Remove the --explore-whole-unmet-space option until parallelized This option has a complex structure with z3 objects that need to be converted to be serializable to be used with multiprocessing. The option doesn't apparently need to be used for existing kismet applications. Leaving it for later if needed. --- kmax/kismet | 116 ++++++++++++++++++++++++++-------------------------- 1 file changed, 58 insertions(+), 58 deletions(-) diff --git a/kmax/kismet b/kmax/kismet index cf73eec4..e2e91604 100644 --- a/kmax/kismet +++ b/kmax/kismet @@ -278,9 +278,9 @@ if __name__ == '__main__': argparser.add_argument('--force-target-udd-only', action="store_true", help="""Force no other unmet direct dependency than the target one for each analyzed construct. If such constraints are not satisfiable, the constraints are relaxed and tried again.""") - argparser.add_argument('--explore-whole-unmet-space', - action="store_true", - help="""Explore the whole unmet space by analysing for each solution to optimized unmet direct dependency constraints.""") + # argparser.add_argument('--explore-whole-unmet-space', + # action="store_true", + # help="""Explore the whole unmet space by analysing for each solution to optimized unmet direct dependency constraints.""") argparser.add_argument('--dump-optimized-constraints', action="store_true", help="""Dump optimized constraints for each select construct in smt2 format in the test cases directory.""") @@ -349,7 +349,7 @@ if __name__ == '__main__': optimized_SAT_pass = not args.no_optimized_SAT_check precise_SAT_pass = not args.no_precise_SAT_check force_target_udd_only = args.force_target_udd_only - explore_whole_unmet_space = args.explore_whole_unmet_space + # explore_whole_unmet_space = args.explore_whole_unmet_space generate_sample = not args.no_test_case_generation verify = not args.no_verification samples_dir = args.test_cases_dir @@ -381,9 +381,9 @@ if __name__ == '__main__': warning("Enabling sample generation (i.e., ignoring --no-test-case-generation) for verification of alarms. Use --no-verification as well to turn off test case generation.") sample_models = verify or generate_sample - if not optimized_SAT_pass and explore_whole_unmet_space: - warning("Ignoring exploring whole unmet space (i.e., --explore-whole-unmet-space) since optimized SAT pass is disabled (i.e., --no-optimized-SAT-check).") - explore_whole_unmet_space = False + # if not optimized_SAT_pass and explore_whole_unmet_space: + # warning("Ignoring exploring whole unmet space (i.e., --explore-whole-unmet-space) since optimized SAT pass is disabled (i.e., --no-optimized-SAT-check).") + # explore_whole_unmet_space = False if arch_name not in Arch.ARCHS: argparser.print_help() @@ -613,9 +613,9 @@ if __name__ == '__main__': info("Optimized SAT test was done in %.2fsec. %d constructs with alarms were checked. unmet safe due to optimized SAT test: %d. alarms: %d." \ % (t_spent_optimizedpass, count_optimizedpass_checked, count_optimizedpass_unmet_safe, count_optimizedpass_unmet_alarms_unique_constructs)) - if explore_whole_unmet_space: - info("Since exploring whole unmet space is enabled, %d additional SAT options were created for %d unique selects constructs with alarms." \ - % (count_optimizedpass_sat_options_created, count_optimizedpass_unmet_alarms_unique_constructs)) + # if explore_whole_unmet_space: + # info("Since exploring whole unmet space is enabled, %d additional SAT options were created for %d unique selects constructs with alarms." \ + # % (count_optimizedpass_sat_options_created, count_optimizedpass_unmet_alarms_unique_constructs)) # # Precise test @@ -764,23 +764,23 @@ if __name__ == '__main__': info("Precise SAT test was done in %.2fsec. %d constructs with alarms were checked. unmet safe due to precise SAT test: %d. alarms: %d." \ % (t_spent_precisepass, count_precisepass_checked_generic, count_precisepass_unmet_safe_generic, count_precisepass_unmet_alarm_generic)) - if explore_whole_unmet_space: - info("During precise SAT test, due to exploring whole unmet space, %d additional constraints were checked, leading to %d in total. Among all: unmet safe due to optimized SAT test: %d. alarms: %d." \ - % (count_precisepass_checked_satoptions, \ - count_precisepass_checked_generic + count_precisepass_checked_satoptions, \ - count_precisepass_unmet_safe_generic + count_precisepass_unmet_safe_satoptions, \ - count_precisepass_unmet_alarm_generic + count_precisepass_unmet_alarms_satoptions)) + # if explore_whole_unmet_space: + # info("During precise SAT test, due to exploring whole unmet space, %d additional constraints were checked, leading to %d in total. Among all: unmet safe due to optimized SAT test: %d. alarms: %d." \ + # % (count_precisepass_checked_satoptions, \ + # count_precisepass_checked_generic + count_precisepass_checked_satoptions, \ + # count_precisepass_unmet_safe_generic + count_precisepass_unmet_safe_satoptions, \ + # count_precisepass_unmet_alarm_generic + count_precisepass_unmet_alarms_satoptions)) info("During precise SAT test, %d models were generated." % count_precisepass_models) # end of precise pass - if precise_SAT_pass and count_precisepass_models == 0: - if sample_models: - info("Skipping test case generation since there are no models to generate test cases for.") - sample_models = False - if verify: - info("Skipping verification since there are no test cases to verify.") - verify = False + # if precise_SAT_pass and count_precisepass_models == 0: + # if sample_models: + # info("Skipping test case generation since there are no models to generate test cases for.") + # sample_models = False + # if verify: + # info("Skipping verification since there are no test cases to verify.") + # verify = False # TODO: allow putting comments in the config files def get_cfgfilepath(selectee, selector, visib_id, type_id): @@ -828,25 +828,25 @@ if __name__ == '__main__': dump_testcasegen_progress() # If exploring whole unmet space is set, dump the config samples for sat options with alarms too - if explore_whole_unmet_space: - sat_options = unmet_constraints[selectee][selector][visib_id]["sat_options"] - for i, sat_option in enumerate(sat_options): - sat_option_result = sat_option["analysis_result"] - - if sat_option_result == UnmetDepResult.UNMET_ALARM: - z3_model = sat_option["model"] - config_content = Klocalizer.get_config_from_model(z3_model, arch, set_tristate_m=False, allow_non_visibles=False) - cfgfilepath = get_cfgfilepath(selectee, selector, visib_id, i+1) - - with open(cfgfilepath, "w") as f: - f.write(config_content) + # if explore_whole_unmet_space: + # sat_options = unmet_constraints[selectee][selector][visib_id]["sat_options"] + # for i, sat_option in enumerate(sat_options): + # sat_option_result = sat_option["analysis_result"] + + # if sat_option_result == UnmetDepResult.UNMET_ALARM: + # z3_model = sat_option["model"] + # config_content = Klocalizer.get_config_from_model(z3_model, arch, set_tristate_m=False, allow_non_visibles=False) + # cfgfilepath = get_cfgfilepath(selectee, selector, visib_id, i+1) + + # with open(cfgfilepath, "w") as f: + # f.write(config_content) - sat_option["testcase_cfgpath"] = cfgfilepath + # sat_option["testcase_cfgpath"] = cfgfilepath - config_samples_created += 1 + # config_samples_created += 1 - # dump progress - dump_testcasegen_progress() + # # dump progress + # dump_testcasegen_progress() info("") # complete the progress # Collect stats @@ -948,20 +948,20 @@ if __name__ == '__main__': dump_verification_progress() # verify sat_options, if available - if explore_whole_unmet_space: - sat_options = unmet_constraints[selectee][selector][visib_id]["sat_options"] - for sat_option in sat_options: - if sat_option["analysis_result"] == UnmetDepResult.UNMET_ALARM: - cfgfilepath = sat_option["testcase_cfgpath"] - is_verified = verify_test_case(cfgfilepath, selectee, selector, arch_name) - sat_option["is_verified"] = is_verified - some_verified = some_verified or is_verified - all_verified = all_verified and is_verified - num_verified += is_verified - num_checked += 1 - - # dump progress - dump_verification_progress() + # if explore_whole_unmet_space: + # sat_options = unmet_constraints[selectee][selector][visib_id]["sat_options"] + # for sat_option in sat_options: + # if sat_option["analysis_result"] == UnmetDepResult.UNMET_ALARM: + # cfgfilepath = sat_option["testcase_cfgpath"] + # is_verified = verify_test_case(cfgfilepath, selectee, selector, arch_name) + # sat_option["is_verified"] = is_verified + # some_verified = some_verified or is_verified + # all_verified = all_verified and is_verified + # num_verified += is_verified + # num_checked += 1 + + # # dump progress + # dump_verification_progress() some_testcase_verifies += some_verified all_testcases_verify += all_verified @@ -1048,8 +1048,8 @@ if __name__ == '__main__': f.write("%d select constructs with alarms from the previous stage were checked during optimized SAT pass.\n" % count_optimizedpass_checked) f.write("%d select constructs were found udd SAFE through optimized SAT pass.\n" % count_optimizedpass_unmet_safe) f.write("%d select constructs were found udd ALARM through optimized SAT pass.\n" % count_optimizedpass_unmet_alarms_unique_constructs) - if explore_whole_unmet_space: - f.write("%d additional constraints were identified as SAT options for optimized constraints to explore whole unmet space for %d udd alarms.\n" % (count_optimizedpass_sat_options_created, count_optimizedpass_unmet_alarms_unique_constructs)) + # if explore_whole_unmet_space: + # f.write("%d additional constraints were identified as SAT options for optimized constraints to explore whole unmet space for %d udd alarms.\n" % (count_optimizedpass_sat_options_created, count_optimizedpass_unmet_alarms_unique_constructs)) # precise SAT pass if precise_SAT_pass: @@ -1057,9 +1057,9 @@ if __name__ == '__main__': f.write("%d select constructs with alarms from the previous stage were checked during precise SAT pass.\n" % count_precisepass_checked_generic) f.write("%d select constructs were found udd SAFE through precise SAT pass.\n" % count_precisepass_unmet_safe_generic) f.write("%d select constructs were found udd ALARM through precise SAT pass.\n" % count_precisepass_unmet_alarm_generic) - if explore_whole_unmet_space: - f.write("%d SAT options for %d alarms were checked due to exploring whole unmet space.\n" % count_precisepass_checked_satoptions) - f.write("%d SAT options were found udd SAFE while %d SAT options were found udd ALARM.\n" % (count_precisepass_unmet_safe_satoptions, count_precisepass_unmet_alarms_satoptions)) + # if explore_whole_unmet_space: + # f.write("%d SAT options for %d alarms were checked due to exploring whole unmet space.\n" % count_precisepass_checked_satoptions) + # f.write("%d SAT options were found udd SAFE while %d SAT options were found udd ALARM.\n" % (count_precisepass_unmet_safe_satoptions, count_precisepass_unmet_alarms_satoptions)) if sample_models: f.write("\n== Test case generation ==\n")