diff --git a/fuzz_test.py b/fuzz_test.py index 1d8a7dd6..5baf87ca 100644 --- a/fuzz_test.py +++ b/fuzz_test.py @@ -6,6 +6,8 @@ import time from pathlib import Path from multiprocessing import Process,Lock, Manager, set_start_method,Pool, cpu_count +import csv +from datetime import datetime import cpmpy as cp @@ -26,7 +28,7 @@ def check_positive(value): return ivalue parser = argparse.ArgumentParser(description = "A python application to fuzz_test your solver(s)") - parser.add_argument("-s", "--solver", help = "The Solver to use", required = False,type=str,choices=available_solvers, default=available_solvers[0]) + parser.add_argument("-s", "--solver", help = "The Solver to use", required = False,type=str,choices=available_solvers, nargs='+', default=[available_solvers[0]]) parser.add_argument("-m", "--models", help = "The path to load the models", required=False, type=str, default="models") parser.add_argument("-o", "--output-dir", help = "The directory to store the output (will be created if it does not exist).", required=False, type=str, default="output") parser.add_argument("-g", "--skip-global-constraints", help = "Skip the global constraints when testing", required=False, default = False) @@ -34,6 +36,7 @@ def check_positive(value): parser.add_argument("--max-minutes", help = "The maximum time (in minutes) the tests should run (by default the tests will run forever). The tests will quit sooner if max-bugs was set and reached or an keyboardinterrupt occured", required=False, default=math.inf ,type=check_positive) parser.add_argument("-mpm","--mutations-per-model", help = "The amount of mutations that will be executed on every model", required=False, default=5 ,type=check_positive) parser.add_argument("-p","--amount-of-processes", help = "The amount of processes that will be used to run the tests", required=False, default=cpu_count()-1 ,type=check_positive) # the -1 is for the main process + parser.add_argument("--mm-prob", help="The probability that a metamorphic mutation will be chosen in case of a verifier that allows other mutations", required=False, default=1, type=float) args = parser.parse_args() models = [] max_failed_tests = args.max_failed_tests @@ -49,7 +52,7 @@ def check_positive(value): os.makedirs(args.output_dir, exist_ok=True) # showing the info about the given params to the user - print("\nUsing solver '"+args.solver+"' with models in '"+args.models+"' and writing to '"+args.output_dir+"'." ,flush=True,end="\n\n") + print("\nUsing solver(s): '" + ", ".join(args.solver)+"' with models in '"+args.models+"' and writing to '"+args.output_dir+"'." ,flush=True,end="\n\n") print("Will use "+str(args.amount_of_processes)+ " parallel executions, starting...",flush=True,end="\n\n") # creating the vars for the multiprocessing @@ -65,9 +68,20 @@ def check_positive(value): # creating processes to run all the tests processes = [] - process_args = (current_amount_of_tests, current_amount_of_error, lock, args.solver, args.mutations_per_model ,models ,max_failed_tests,args.output_dir, max_time) + + # FOR EXPERIMENTS: + solvers = ['ortools', 'minizinc', 'choco', 'gurobi'] + verifiers = ["solver_vote_count_verifier", "solver_vote_eq_verifier", "solver_vote_sat_verifier", "solver_vote_sol_verifier", "strengthening_weakening_verifier"] + solver_counts = {s: manager.Value(f"{s}", 0) for s in solvers} + verifier_counts = {v: manager.Value(f"{v}", 0) for v in verifiers} + verifier_run_times = {v: manager.Value(f"{v}", 0) for v in verifiers} + from itertools import combinations + solver_combos = [list(c) for c in combinations(solvers, 2)] for x in range(args.amount_of_processes): + process_args = (current_amount_of_tests, current_amount_of_error, lock, solver_combos[x], + args.mutations_per_model, models, max_failed_tests, args.output_dir, max_time, args.mm_prob, + solver_counts, verifier_counts, verifier_run_times) # PAS TERUG AAN NA EXPERIMENTEN processes.append(Process(target=run_verifiers,args=process_args)) try: @@ -76,8 +90,14 @@ def check_positive(value): process.start() for process in processes: - process.join() - process.close() + process.join(timeout=args.max_minutes*60) # wait max double minutes + + # If any process is still alive after timeout, terminate it + for process in processes: + if process.is_alive(): + print(f"Forcefully terminating process {process.pid}", flush=True) + process.terminate() + process.join() # Clean up except KeyboardInterrupt as e: print("interrupting...",flush=True,end="\n") @@ -96,4 +116,45 @@ def check_positive(value): else: print("Succesfully executed " +str(current_amount_of_tests.value) + " tests, "+str(current_amount_of_error.value)+" tests failed",flush=True,end="\n") + run_name = args.output_dir + minutes_ran = args.max_minutes + mpm = args.mutations_per_model + mm_prob = args.mm_prob + amnt_tests = current_amount_of_tests.value + amnt_errors = current_amount_of_error.value + solver_count_vals = {s: c.value for s, c in solver_counts.items()} + verifier_count_vals = {v: c.value for v, c in verifier_counts.items()} + verifier_runtime_vals = {v: t.value for v, t in verifier_run_times.items()} + print(f"Run \"{run_name}\" ran for {minutes_ran} minutes and executed {amnt_tests} tests of which {amnt_errors} failed.") + print("Amount of times each solver ran for:", solver_count_vals) + print("Amount of times each verifier ran:", verifier_count_vals) + print("Time each verifier ran:", verifier_runtime_vals) + + # Prepare timestamp and filename + timestamp = datetime.now().strftime("%Y%m%d_%H%M%S") + stats_filename = f"{run_name}_{timestamp}.csv" + + # Create the rows for the CSV + headers = ["run_name", "mutations_per_model", "mm_probability", "minutes_ran", "amnt_tests", "amnt_errors"] + row = [run_name, mpm, mm_prob, minutes_ran, amnt_tests, amnt_errors] + + # Optionally, flatten solver and verifier data into columns + for s, count in solver_count_vals.items(): + headers.append(f"solver_count_{s}") + row.append(count) + + for v, count in verifier_count_vals.items(): + headers.append(f"verifier_count_{v}") + row.append(count) + + for v, t in verifier_runtime_vals.items(): + headers.append(f"verifier_runtime_{v}") + row.append(t) + + # Save to CSV + with open(stats_filename, mode="w", newline="") as f: + writer = csv.writer(f) + writer.writerow(headers) + writer.writerow(row) + print(f"Saved run statistics to {stats_filename}") diff --git a/fuzz_test_rerunner.py b/fuzz_test_rerunner.py index 0cc002a1..4bc80f79 100644 --- a/fuzz_test_rerunner.py +++ b/fuzz_test_rerunner.py @@ -33,7 +33,10 @@ def rerun_file(failed_model_file,output_dir ): error_data = pickle.loads(fpcl.read()) random.seed(error_data["seed"]) if error_data["error"]["type"].name != "fuzz_test_crash": # if it is a fuzz_test crash error we skip it - verifier_kwargs = {'solver': error_data["solver"], "mutations_per_model": error_data["mutations_per_model"], "exclude_dict": {}, "time_limit": time.time()*3600, "seed": error_data["seed"]} + solver = error_data["solver"] + verifier_kwargs = {'solver': solver, "mutations_per_model": error_data["mutations_per_model"], "exclude_dict": {}, "time_limit": time.time()*3600, "seed": error_data["seed"]} + if 'mm_prob' in error_data["error"]: + verifier_kwargs['mm_prob'] = error_data["error"]["mm_prob"] error = lookup_verifier(error_data["verifier"])(**verifier_kwargs).rerun(error_data["error"]) error_data["error"] = error diff --git a/fuzz_test_utils/mutators.py b/fuzz_test_utils/mutators.py index c05a6148..4182d4e9 100644 --- a/fuzz_test_utils/mutators.py +++ b/fuzz_test_utils/mutators.py @@ -1,21 +1,56 @@ import copy import random +import numpy as np +from cpmpy.expressions.globalfunctions import GlobalFunction, Abs, Minimum, Maximum, Element, Count, Among, NValue, \ + NValueExcept from cpmpy.transformations.negation import push_down_negation from cpmpy.transformations.to_cnf import flat2cnf from cpmpy import intvar, Model -from cpmpy.expressions.core import Operator, Comparison +from cpmpy.expressions.core import Operator, Comparison, BoolVal, Expression from cpmpy.transformations.decompose_global import decompose_in_tree from cpmpy.transformations.get_variables import get_variables from cpmpy.transformations.linearize import linearize_constraint, only_positive_bv, canonical_comparison -from cpmpy.expressions.utils import is_boolexpr, is_any_list +from cpmpy.expressions.utils import is_boolexpr, is_any_list, is_bool, is_int, is_num from cpmpy.transformations.flatten_model import flatten_constraint, normalized_boolexpr, normalized_numexpr, \ flatten_objective, __is_flat_var from cpmpy.transformations.normalize import toplevel_list, simplify_boolean from cpmpy.transformations.reification import only_bv_reifies, reify_rewrite from cpmpy.transformations.comparison import only_numexpr_equality -from cpmpy.expressions.globalconstraints import Xor +from cpmpy.expressions.globalconstraints import Xor, AllDifferent, AllDifferentExceptN, AllEqual, AllEqualExceptN, \ + Circuit, Inverse, Table, NegativeTable, IfThenElse, InDomain, Cumulative, Precedence, NoOverlap, \ + GlobalCardinalityCount, Increasing, Decreasing, IncreasingStrict, DecreasingStrict, LexLess, LexLessEq, \ + LexChainLess, LexChainLessEq, GlobalConstraint +# from cpmpy.expressions.globalfunctions import Abs, Mimimum(GlobalFunction), Maximum +from cpmpy.expressions.variables import boolvar, _IntVarImpl, NDVarArray + + +class Function: + def __init__(self, name, func, type_: str, int_args: int, bool_args: int, + bool_return: bool | None, + min_args: int = None, + max_args: int = None): + """ + type = string that describes the type of function it is + int_args = the amount of args of type int it requires + bool_args = the amount of args of type bool it requires + bool_return = a boolean representing whether it returns a boolean (False means int return type, None means it can be either) + min_args = the minimum amount of args the function takes + max_args = the maximum amount of args the function takes + """ + self.name = name + self.func = func + self.type = type_ + self.int_args = int_args + self.bool_args = bool_args + self.bool_return = bool_return + self.min_args = min_args + self.max_args = max_args + + def __repr__(self): + return (f"Operation({self.name}, {self.type}, {self.int_args}, {self.bool_args}, " + f"{self.bool_return}, min_args={self.min_args}, max_args={self.max_args})") '''TRUTH TABLE BASED MORPHS''' @@ -23,40 +58,45 @@ def not_morph(cons): con = random.choice(cons) ncon = ~con return [~ncon] + + def xor_morph(cons): '''morph two constraints with XOR''' - con1, con2 = random.choices(cons,k=2) - #add a random option as per xor truth table + con1, con2 = random.choices(cons, k=2) + # add a random option as per xor truth table return [random.choice(( Xor([con1, ~con2]), Xor([~con1, con2]), ~Xor([~con1, ~con2]), ~Xor([con1, con2])))] + def and_morph(cons): '''morph two constraints with AND''' - con1, con2 = random.choices(cons,k=2) + con1, con2 = random.choices(cons, k=2) return [random.choice(( ~((con1) & (~con2)), ~((~con1) & (~con2)), ~((~con1) & (con2)), ((con1) & (con2))))] + def or_morph(cons): '''morph two constraints with OR''' - con1, con2 = random.choices(cons,k=2) - #add all options as per xor truth table + con1, con2 = random.choices(cons, k=2) + # add all options as per xor truth table return [random.choice(( ((con1) | (~con2)), ~((~con1) | (~con2)), ((~con1) | (con2)), ((con1) | (con2))))] + def implies_morph(cons): '''morph two constraints with ->''' - con1, con2 = random.choices(cons,k=2) + con1, con2 = random.choices(cons, k=2) try: - #add all options as per xor truth table + # add all options as per xor truth table return [random.choice(( ~((con1).implies(~con2)), ((~con1).implies(~con2)), @@ -67,10 +107,12 @@ def implies_morph(cons): ((~con2).implies(con1)), ((con2).implies(con1))))] except Exception as e: - raise MetamorphicError(implies_morph,cons,e) + raise MetamorphicError(implies_morph, cons, e) + '''CPMPY-TRANSFORMATION MORPHS''' + def canonical_comparison_morph(cons): n = random.randint(1, len(cons)) randcons = random.choices(cons, k=n) @@ -79,16 +121,17 @@ def canonical_comparison_morph(cons): except Exception as e: raise MetamorphicError(canonical_comparison, cons, e) + def flatten_morph(cons, flatten_all=False): if flatten_all is False: - n = random.randint(1,len(cons)) - randcons = random.choices(cons,k=n) + n = random.randint(1, len(cons)) + randcons = random.choices(cons, k=n) else: randcons = cons try: return flatten_constraint(randcons) except Exception as e: - raise MetamorphicError(flatten_constraint,randcons, e) + raise MetamorphicError(flatten_constraint, randcons, e) def simplify_boolean_morph(cons): @@ -98,10 +141,10 @@ def simplify_boolean_morph(cons): raise MetamorphicError(simplify_boolean, cons, e) -def only_numexpr_equality_morph(cons,supported=frozenset()): +def only_numexpr_equality_morph(cons, supported=frozenset()): n = random.randint(1, len(cons)) randcons = random.choices(cons, k=n) - flatcons = flatten_morph(randcons, flatten_all=True) # only_numexpr_equality requires flat constraints + flatcons = flatten_morph(randcons, flatten_all=True) # only_numexpr_equality requires flat constraints try: newcons = only_numexpr_equality(flatcons, supported=supported) return newcons @@ -122,6 +165,7 @@ def normalized_boolexpr_morph(cons): else: return cons + def normalized_numexpr_morph(const): try: cons = copy.deepcopy(const) @@ -131,9 +175,9 @@ def normalized_numexpr_morph(const): res = pickaritmetic(con, log=[i]) if res != []: firstcon = random.choice(res) - break #numexpr found + break # numexpr found if firstcon is None: - #no numexpressions found but still call the function to test on all inputs + # no numexpressions found but still call the function to test on all inputs randcon = random.choice(cons) try: con, newcons = normalized_numexpr(randcon) @@ -141,7 +185,7 @@ def normalized_numexpr_morph(const): except Exception as e: raise MetamorphicError(normalized_numexpr, randcon, e) else: - #get the numexpr + # get the numexpr arg = cons[firstcon[0]] newfirst = arg for i in firstcon[1:]: @@ -172,21 +216,22 @@ def normalized_numexpr_morph(const): raise MetamorphicError(normalized_numexpr_morph, cons, e) -def linearize_constraint_morph(cons,linearize_all=False,supported={}): +def linearize_constraint_morph(cons, linearize_all=False, supported={}): if linearize_all: randcons = cons else: n = random.randint(1, len(cons)) randcons = random.choices(cons, k=n) - #only apply linearize after only_bv_reifies - decomcons = decompose_in_tree_morph(randcons,decompose_all=True,supported=supported) + # only apply linearize after only_bv_reifies + decomcons = decompose_in_tree_morph(randcons, decompose_all=True, supported=supported) flatcons = only_bv_reifies_morph(decomcons, morph_all=True) try: return linearize_constraint(flatcons, supported={'mul'}) except Exception as e: raise MetamorphicError(linearize_constraint, flatcons, e) + def reify_rewrite_morph(cons): n = random.randint(1, len(cons)) randcons = random.choices(cons, k=n) @@ -212,14 +257,15 @@ def flatten_objective_morph(objective): except Exception as e: raise MetamorphicError(flatten_objective, objective, e) -def decompose_in_tree_morph(cons,decompose_all=False,supported={}): + +def decompose_in_tree_morph(cons, decompose_all=False, supported={}): try: - return decompose_in_tree(cons,supported=supported) + return decompose_in_tree(cons, supported=supported) except Exception as e: raise MetamorphicError(decompose_in_tree, cons, e) -def only_bv_reifies_morph(cons,morph_all=True): +def only_bv_reifies_morph(cons, morph_all=True): if morph_all: randcons = cons else: @@ -231,22 +277,24 @@ def only_bv_reifies_morph(cons,morph_all=True): except Exception as e: raise MetamorphicError(only_bv_reifies, flatcons, e) + def only_positive_bv_morph(cons): - lincons = linearize_constraint_morph(cons,linearize_all=True,supported={}) + lincons = linearize_constraint_morph(cons, linearize_all=True, supported={}) try: return only_positive_bv(lincons) except Exception as e: raise MetamorphicError(only_positive_bv, lincons, e) - def flat2cnf_morph(cons): - #flatcons = flatten_morph(cons,flatten_all=True) - onlycons = only_bv_reifies_morph(cons,morph_all=True) + # flatcons = flatten_morph(og_cons,flatten_all=True) + onlycons = only_bv_reifies_morph(cons, morph_all=True) try: return flat2cnf(onlycons) except Exception as e: raise MetamorphicError(flat2cnf, onlycons, e) + + def toplevel_list_morph(cons): try: return toplevel_list(cons) @@ -262,6 +310,7 @@ def add_solution(cons): raise MetamorphicError(add_solution, cons, e) return [var == var.value() for var in vars if var.value() is not None] + def semanticFusion(const): try: firstcon = None @@ -269,28 +318,28 @@ def semanticFusion(const): cons = copy.deepcopy(const) random.shuffle(cons) for i, con in enumerate(cons): - res = pickaritmetic(con,log=[i]) + res = pickaritmetic(con, log=[i]) if res != []: if firstcon == None: firstcon = random.choice(res) elif secondcon == None: secondcon = random.choice(res) - break #stop when 2 constraints found. still random because cons are shuffled + break # stop when 2 constraints found. still random because og_cons are shuffled if secondcon != None: - #two constraints with aritmetic expressions found, perform semantic fusion on them - #get the expressions to fuse + # two constraints with aritmetic expressions found, perform semantic fusion on them + # get the expressions to fuse arg = cons[firstcon[0]] newfirst = copy.deepcopy(arg) count = 0 for i in firstcon[1:]: count += 1 arg = arg.args[i] - if hasattr(arg,'name'): + if hasattr(arg, 'name'): if arg.name in ['div', 'mod', 'pow']: if len(firstcon) > count + 1: if firstcon[count + 1] == 1: - return [] #we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 + return [] # we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 firstexpr = arg arg = cons[secondcon[0]] @@ -299,25 +348,25 @@ def semanticFusion(const): for i in secondcon[1:]: count += 1 arg = arg.args[i] - if hasattr(arg,'name'): + if hasattr(arg, 'name'): if arg.name in ['div', 'mod', 'pow']: if len(secondcon) > count + 1: if secondcon[count + 1] == 1: - return [] #we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 + return [] # we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 secondexpr = arg - lb,ub = Operator('sum',[firstexpr,secondexpr]).get_bounds() + lb, ub = Operator('sum', [firstexpr, secondexpr]).get_bounds() z = intvar(lb, ub) firstexpr, secondexpr = z - secondexpr, z - firstexpr - #make the new constraints + # make the new constraints arg = newfirst c = 1 firststr = str(firstexpr) for i in firstcon[1:]: if str(arg) in firststr: - return [] #cyclical - c+=1 + return [] # cyclical + c += 1 if c == len(firstcon): if isinstance(arg.args, tuple): arg.args = list(arg.args) @@ -330,7 +379,7 @@ def semanticFusion(const): secondstr = str(secondexpr) for i in secondcon[1:]: if str(arg) in secondstr: - return [] #cyclical + return [] # cyclical c += 1 if c == len(secondcon): if isinstance(arg.args, tuple): @@ -339,15 +388,16 @@ def semanticFusion(const): else: arg = arg.args[i] - return [newfirst,newsecond] + return [newfirst, newsecond] else: - #no expressions found to fuse + # no expressions found to fuse return [] except Exception as e: raise MetamorphicError(semanticFusion, cons, e) + def semanticFusionMinus(const): try: firstcon = None @@ -355,28 +405,28 @@ def semanticFusionMinus(const): cons = copy.deepcopy(const) random.shuffle(cons) for i, con in enumerate(cons): - res = pickaritmetic(con,log=[i]) + res = pickaritmetic(con, log=[i]) if res != []: if firstcon == None: firstcon = random.choice(res) elif secondcon == None: secondcon = random.choice(res) - break #stop when 2 constraints found. still random because cons are shuffled + break # stop when 2 constraints found. still random because og_cons are shuffled if secondcon != None: - #two constraints with aritmetic expressions found, perform semantic fusion on them - #get the expressions to fuse + # two constraints with aritmetic expressions found, perform semantic fusion on them + # get the expressions to fuse arg = cons[firstcon[0]] newfirst = copy.deepcopy(arg) count = 0 for i in firstcon[1:]: count += 1 arg = arg.args[i] - if hasattr(arg,'name'): + if hasattr(arg, 'name'): if arg.name in ['div', 'mod', 'pow']: if len(firstcon) > count + 1: if firstcon[count + 1] == 1: - return [] #we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 + return [] # we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 firstexpr = arg arg = cons[secondcon[0]] @@ -385,25 +435,25 @@ def semanticFusionMinus(const): for i in secondcon[1:]: count += 1 arg = arg.args[i] - if hasattr(arg,'name'): + if hasattr(arg, 'name'): if arg.name in ['div', 'mod', 'pow']: if len(secondcon) > count + 1: if secondcon[count + 1] == 1: - return [] #we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 + return [] # we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 secondexpr = arg - lb,ub = Operator('sub',[firstexpr,secondexpr]).get_bounds() + lb, ub = Operator('sub', [firstexpr, secondexpr]).get_bounds() z = intvar(lb, ub) firstexpr, secondexpr = z + secondexpr, firstexpr - z - #make the new constraints + # make the new constraints arg = newfirst c = 1 firststr = str(firstexpr) for i in firstcon[1:]: if str(arg) in firststr: - return [] #cyclical - c+=1 + return [] # cyclical + c += 1 if c == len(firstcon): if isinstance(arg.args, tuple): arg.args = list(arg.args) @@ -416,7 +466,7 @@ def semanticFusionMinus(const): secondstr = str(secondexpr) for i in secondcon[1:]: if str(arg) in secondstr: - return [] #cyclical + return [] # cyclical c += 1 if c == len(secondcon): if isinstance(arg.args, tuple): @@ -425,15 +475,16 @@ def semanticFusionMinus(const): else: arg = arg.args[i] - return [newfirst,newsecond] + return [newfirst, newsecond] else: - #no expressions found to fuse + # no expressions found to fuse return [] except Exception as e: raise MetamorphicError(semanticFusionMinus, cons, e) + def semanticFusionwsum(const): try: firstcon = None @@ -441,58 +492,61 @@ def semanticFusionwsum(const): cons = copy.deepcopy(const) random.shuffle(cons) for i, con in enumerate(cons): - res = pickaritmetic(con,log=[i]) + res = pickaritmetic(con, log=[i]) if res != []: if firstcon == None: firstcon = random.choice(res) elif secondcon == None: secondcon = random.choice(res) - break #stop when 2 constraints found. still random because cons are shuffled + break # stop when 2 constraints found. still random because og_cons are shuffled if secondcon != None: - #two constraints with aritmetic expressions found, perform semantic fusion on them - #get the expressions to fuse + # two constraints with aritmetic expressions found, perform semantic fusion on them + # get the expressions to fuse arg = cons[firstcon[0]] newfirst = copy.deepcopy(arg) count = 0 for i in firstcon[1:]: count += 1 arg = arg.args[i] - if hasattr(arg,'name'): + if hasattr(arg, 'name'): if arg.name in ['div', 'mod', 'pow']: if len(firstcon) > count + 1: if firstcon[count + 1] == 1: - return [] #we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 + return [] # we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 firstexpr = arg arg = cons[secondcon[0]] - #newsecond = copy.deepcopy(arg) + # newsecond = copy.deepcopy(arg) newsecond = (arg) count = 0 for i in secondcon[1:]: count += 1 arg = arg.args[i] - if hasattr(arg,'name'): + if hasattr(arg, 'name'): if arg.name in ['div', 'mod', 'pow']: if len(secondcon) > count + 1: if secondcon[count + 1] == 1: - return [] #we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 + return [] # we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 secondexpr = arg l = random.randint(1, 10) n = random.randint(1, 10) m = random.randint(1, 10) - lb, ub = Operator('wsum',[[l, m, n], [firstexpr, secondexpr, 1]]).get_bounds() + lb, ub = Operator('wsum', [[l, m, n], [firstexpr, secondexpr, 1]]).get_bounds() z = intvar(lb, ub) - firstexpr, secondexpr = Operator('wsum',[[1, -m, -n], [z, secondexpr, 1]]) / l, Operator('wsum',[[1, -l, -n], [z, firstexpr, 1]]) / m - #make the new constraints + firstexpr, secondexpr = Operator('wsum', [[1, -m, -n], [z, secondexpr, 1]]) / l, Operator('wsum', + [[1, -l, -n], + [z, firstexpr, + 1]]) / m + # make the new constraints arg = newfirst c = 1 firststr = str(firstexpr) for i in firstcon[1:]: if str(arg) in firststr: - return [] #cyclical - c+=1 + return [] # cyclical + c += 1 if c == len(firstcon): if isinstance(arg.args, tuple): arg.args = list(arg.args) @@ -505,7 +559,7 @@ def semanticFusionwsum(const): secondstr = str(secondexpr) for i in secondcon[1:]: if str(arg) in secondstr: - return [] #cyclical + return [] # cyclical c += 1 if c == len(secondcon): if isinstance(arg.args, tuple): @@ -517,11 +571,13 @@ def semanticFusionwsum(const): return [newfirst, newsecond] else: - #no expressions found to fuse + # no expressions found to fuse return [] except Exception as e: raise MetamorphicError(semanticFusionwsum, cons, e) + + def semanticFusionCountingwsum(const): try: firstcon = None @@ -529,28 +585,28 @@ def semanticFusionCountingwsum(const): cons = copy.deepcopy(const) random.shuffle(cons) for i, con in enumerate(cons): - res = pickaritmetic(con,log=[i]) + res = pickaritmetic(con, log=[i]) if res != []: if firstcon == None: firstcon = random.choice(res) elif secondcon == None: secondcon = random.choice(res) - break #stop when 2 constraints found. still random because cons are shuffled + break # stop when 2 constraints found. still random because og_cons are shuffled if secondcon != None: - #two constraints with aritmetic expressions found, perform semantic fusion on them - #get the expressions to fuse + # two constraints with aritmetic expressions found, perform semantic fusion on them + # get the expressions to fuse arg = cons[firstcon[0]] newfirst = copy.deepcopy(arg) count = 0 for i in firstcon[1:]: count += 1 arg = arg.args[i] - if hasattr(arg,'name'): + if hasattr(arg, 'name'): if arg.name in ['div', 'mod', 'pow']: if len(firstcon) > count + 1: if firstcon[count + 1] == 1: - return [] #we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 + return [] # we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 firstexpr = arg arg = cons[secondcon[0]] @@ -559,29 +615,32 @@ def semanticFusionCountingwsum(const): for i in secondcon[1:]: count += 1 arg = arg.args[i] - if hasattr(arg,'name'): + if hasattr(arg, 'name'): if arg.name in ['div', 'mod', 'pow']: if len(secondcon) > count + 1: if secondcon[count + 1] == 1: - return [] #we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 + return [] # we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 secondexpr = arg l = random.randint(1, 10) n = random.randint(1, 10) m = random.randint(1, 10) - lb, ub = Operator('wsum',[[l, m, n], [firstexpr, secondexpr, 1]]).get_bounds() + lb, ub = Operator('wsum', [[l, m, n], [firstexpr, secondexpr, 1]]).get_bounds() z = intvar(lb, ub) thirdcon = z == Operator('wsum', [[l, m, n], [firstexpr, secondexpr, 1]]) - firstexpr, secondexpr = Operator('wsum',[[1, -m, -n], [z, secondexpr, 1]]) / l, Operator('wsum',[[1, -l, -n], [z, firstexpr, 1]]) / m + firstexpr, secondexpr = Operator('wsum', [[1, -m, -n], [z, secondexpr, 1]]) / l, Operator('wsum', + [[1, -l, -n], + [z, firstexpr, + 1]]) / m - #make the new constraints + # make the new constraints arg = newfirst c = 1 firststr = str(firstexpr) for i in firstcon[1:]: if str(arg) in firststr: - return [] #cyclical - c+=1 + return [] # cyclical + c += 1 if c == len(firstcon): if isinstance(arg.args, tuple): arg.args = list(arg.args) @@ -594,7 +653,7 @@ def semanticFusionCountingwsum(const): secondstr = str(secondexpr) for i in secondcon[1:]: if str(arg) in secondstr: - return [] #cyclical + return [] # cyclical c += 1 if c == len(secondcon): if isinstance(arg.args, tuple): @@ -606,7 +665,7 @@ def semanticFusionCountingwsum(const): return [newfirst, newsecond, thirdcon] else: - #no expressions found to fuse + # no expressions found to fuse return [] except Exception as e: @@ -620,28 +679,28 @@ def semanticFusionCounting(const): cons = copy.deepcopy(const) random.shuffle(cons) for i, con in enumerate(cons): - res = pickaritmetic(con,log=[i]) + res = pickaritmetic(con, log=[i]) if res != []: if firstcon == None: firstcon = random.choice(res) elif secondcon == None: secondcon = random.choice(res) - break #stop when 2 constraints found. still random because cons are shuffled + break # stop when 2 constraints found. still random because og_cons are shuffled if secondcon != None: - #two constraints with aritmetic expressions found, perform semantic fusion on them - #get the expressions to fuse + # two constraints with aritmetic expressions found, perform semantic fusion on them + # get the expressions to fuse arg = cons[firstcon[0]] newfirst = copy.deepcopy(arg) count = 0 for i in firstcon[1:]: count += 1 arg = arg.args[i] - if hasattr(arg,'name'): + if hasattr(arg, 'name'): if arg.name in ['div', 'mod', 'pow']: if len(firstcon) > count + 1: if firstcon[count + 1] == 1: - return [] #we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 + return [] # we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 firstexpr = arg arg = cons[secondcon[0]] @@ -650,26 +709,26 @@ def semanticFusionCounting(const): for i in secondcon[1:]: count += 1 arg = arg.args[i] - if hasattr(arg,'name'): + if hasattr(arg, 'name'): if arg.name in ['div', 'mod', 'pow']: if len(secondcon) > count + 1: if secondcon[count + 1] == 1: - return [] #we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 + return [] # we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 secondexpr = arg - lb,ub = Operator('sum',[firstexpr,secondexpr]).get_bounds() + lb, ub = Operator('sum', [firstexpr, secondexpr]).get_bounds() z = intvar(lb, ub) firstexpr, secondexpr = z - secondexpr, z - firstexpr thirdcon = z == firstexpr + secondexpr - #make the new constraints + # make the new constraints arg = newfirst c = 1 firststr = str(firstexpr) for i in firstcon[1:]: if str(arg) in firststr: - return [] #cyclical - c+=1 + return [] # cyclical + c += 1 if c == len(firstcon): if isinstance(arg.args, tuple): arg.args = list(arg.args) @@ -682,7 +741,7 @@ def semanticFusionCounting(const): secondstr = str(secondexpr) for i in secondcon[1:]: if str(arg) in secondstr: - return [] #cyclical + return [] # cyclical c += 1 if c == len(secondcon): if isinstance(arg.args, tuple): @@ -691,15 +750,16 @@ def semanticFusionCounting(const): else: arg = arg.args[i] - return [newfirst,newsecond, thirdcon] + return [newfirst, newsecond, thirdcon] else: - #no expressions found to fuse + # no expressions found to fuse return [] except Exception as e: raise MetamorphicError(semanticFusionCounting, cons, e) + def semanticFusionCountingMinus(const): try: firstcon = None @@ -707,28 +767,28 @@ def semanticFusionCountingMinus(const): cons = copy.deepcopy(const) random.shuffle(cons) for i, con in enumerate(cons): - res = pickaritmetic(con,log=[i]) + res = pickaritmetic(con, log=[i]) if res != []: if firstcon == None: firstcon = random.choice(res) elif secondcon == None: secondcon = random.choice(res) - break #stop when 2 constraints found. still random because cons are shuffled + break # stop when 2 constraints found. still random because og_cons are shuffled if secondcon != None: - #two constraints with aritmetic expressions found, perform semantic fusion on them - #get the expressions to fuse + # two constraints with aritmetic expressions found, perform semantic fusion on them + # get the expressions to fuse arg = cons[firstcon[0]] newfirst = copy.deepcopy(arg) count = 0 for i in firstcon[1:]: count += 1 arg = arg.args[i] - if hasattr(arg,'name'): + if hasattr(arg, 'name'): if arg.name in ['div', 'mod', 'pow']: if len(firstcon) > count + 1: if firstcon[count + 1] == 1: - return [] #we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 + return [] # we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 firstexpr = arg arg = cons[secondcon[0]] @@ -737,25 +797,25 @@ def semanticFusionCountingMinus(const): for i in secondcon[1:]: count += 1 arg = arg.args[i] - if hasattr(arg,'name'): + if hasattr(arg, 'name'): if arg.name in ['div', 'mod', 'pow']: if len(secondcon) > count + 1: if secondcon[count + 1] == 1: - return [] #we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 + return [] # we don't want to mess with the divisor of a division, since we can't divide by a domain containing 0 secondexpr = arg - lb,ub = Operator('sub',[firstexpr,secondexpr]).get_bounds() + lb, ub = Operator('sub', [firstexpr, secondexpr]).get_bounds() z = intvar(lb, ub) firstexpr, secondexpr = z + secondexpr, firstexpr - z thirdcon = z == firstexpr - secondexpr - #make the new constraints + # make the new constraints arg = newfirst c = 1 firststr = str(firstexpr) for i in firstcon[1:]: if str(arg) in firststr: - return [] #cyclical - c+=1 + return [] # cyclical + c += 1 if c == len(firstcon): if isinstance(arg.args, tuple): arg.args = list(arg.args) @@ -768,7 +828,7 @@ def semanticFusionCountingMinus(const): secondstr = str(secondexpr) for i in secondcon[1:]: if str(arg) in secondstr: - return [] #cyclical + return [] # cyclical c += 1 if c == len(secondcon): if isinstance(arg.args, tuple): @@ -780,15 +840,13 @@ def semanticFusionCountingMinus(const): return [newfirst, newsecond, thirdcon] else: - #no expressions found to fuse + # no expressions found to fuse return [] except Exception as e: raise MetamorphicError(semanticFusionCountingMinus, cons, e) - - def aritmetic_comparison_morph(const): try: cons = copy.deepcopy(const) @@ -818,14 +876,14 @@ def aritmetic_comparison_morph(const): rhs2 = rhs + 7 lhs3 = lhs - 7 rhs3 = rhs - 7 - lhs, rhs = random.choice([(lhs3,rhs3),(lhs2,rhs2),(lhs1,rhs1)]) - newcon = Comparison(name=firstexpr.name,left=lhs,right=rhs) + lhs, rhs = random.choice([(lhs3, rhs3), (lhs2, rhs2), (lhs1, rhs1)]) + newcon = Comparison(name=firstexpr.name, left=lhs, right=rhs) except Exception as e: raise MetamorphicError(aritmetic_comparison_morph, firstexpr, e) # make the new constraint (newfirst) arg = newfirst - if len(firstcon) == 1: #toplevel comparison + if len(firstcon) == 1: # toplevel comparison return [newcon] c = 1 for i in firstcon[1:]: @@ -844,64 +902,1027 @@ def aritmetic_comparison_morph(const): except Exception as e: raise MetamorphicError(aritmetic_comparison_morph, cons, e) + +def type_aware_operator_replacement(constraints: list): + """ + Replaces a random operator of a random constraint from a list of given constraints. + IMPORTANT: This can change satisfiability of the constraint! Only to be used with verifiers that allow this! + This means it returns a list of ALL constraints and has to be handled accordingly in the 'generate_mutations' + function to swap out the constraints instead of adding them. + + ~ Parameters: + - constraints: a list of all the constraints to possibly be mutated + ~ Return: + - final_cons: a list of the same constraints where one constraint has a mutated operator + + Types of operators ('...' means the amount of arguments is variable): + - Int, Bool -> Bool : == != < <= > >= + - Bool, Int -> Bool : == != < <= > >= + - Int, Int -> Bool : == != < <= > >= + - [Bool, Bool] -> Bool : and or -> + - [Bool, ...] -> Bool : and or + - [Bool] -> Bool : not + - Int, Int -> Int : sum sub mul div mod pow (IMPORTANT: div mod gives problems with domains containing 0, pow with domains containing negative numbers) + - [Int, ...] -> Int : sum + - [Int] -> Int : - + - [Int, ...] [Int, ...] (arrays of same len) -> Int : wsum + """ + try: + final_cons = copy.deepcopy(constraints) + # pick a random constraint and calculate whether they have a mutable expression until they do + candidates = [] + for item in constraints: + if not any(item is cand for cand in candidates): + candidates.append(item) + # candidates = list(set(constraints)) # does not work with NDVarArray + random.shuffle(candidates) + for con in candidates: + exprs = get_all_mutable_op_exprs(con) # e.g. for (x + y) // z > 0. The tree goes >(0, //(+(x,y), z)) + # which means either >, // or + can get mutated + if exprs: + break + else: # In case there isn't any mutable expression in any constraint + return final_cons + + # Remove the constraint from the constraints + final_cons.remove(con) + + # Choose an expression to change + expr = random.choice(exprs) + + # Mutate this expression (= change the operator) + mutate_op_expression(expr, con) + + # Add the changed constraint back + final_cons.append(con) + return final_cons + + except Exception as e: + raise Exception(e) + + +def mutate_op_expression(expr: Expression, con: Expression): + """ + Mutates the constraint containing the expression by mutating said expression. + Only to be called when the expression is known to be in the constraint. + + ~ Parameters: + - expr: the expression that will be mutated + - con: the constraint containing the expression + ~ No return. Mutates the constraint! + """ + # TODO: other types of functions should also be added (e.g. global constraints/functions) + # Types that can be converted into each-other + comparisons = {'==', '!=', '<', '<=', '>', '>='} + int_ops = {'sum', 'sub', 'mul', + 'pow', 'mod', 'div'} + logic_ops = {'and', 'or', '->'} + logic_ops_inf_args = {'and', 'or'} + if expr == con: # Found the expression to mutate + # Determine the type of the operator + if expr.name in comparisons: # a, b -> Bool (Comparison() always has two arguments) + possible_replacements = comparisons - {expr.name} + elif expr.name in int_ops and len(expr.args) == 2: # a, a -> Int + possible_replacements = int_ops - {expr.name} + elif expr.name in logic_ops and len(expr.args) == 2: # [Bool, Bool] -> Bool + possible_replacements = logic_ops - {expr.name} + elif expr.name in logic_ops_inf_args: # [Bool, ...] -> Bool + possible_replacements = logic_ops_inf_args - {expr.name} + else: + raise ValueError(f"Unknown operator type: {expr.name}. (You should not be able to get here)") + + new_operator = random.choice(list(possible_replacements)) + expr.name = new_operator # Mutate expression by changing its name + return + + # Recursively search for the expression in arguments + if hasattr(con, "args"): + for arg in con.args: + mutate_op_expression(expr, arg) + return + + +def get_all_mutable_op_exprs(con: Expression): + """ + Returns a list of all expressions inside the given constraint of which the + operator can be mutated into another one. + + ~ Parameters: + - con: a single constraint, possibly containing multiple expressions + ~ Return: + - mutable_exprs: all expressions in the constraint that can be mutated + """ + # TODO: other types of functions should also be added (e.g. global constraints/functions) + comparisons = {'==', '!=', '<', '<=', '>', '>='} + int_ops = {'sum', 'sub', 'mul', 'div', 'mod', 'pow'} + logic_ops = {'and', 'or', '->'} + logic_ops_inf_args = {'and', 'or'} + mutable_exprs = [] + for expr in get_all_op_exprs(con): + if expr.name in comparisons: # a, b -> Bool (Comparison() always has two arguments) + mutable_exprs.append(expr) + elif expr.name in int_ops and len(expr.args) == 2: # a, b -> Int + mutable_exprs.append(expr) + elif expr.name in logic_ops and len(expr.args) == 2: # [Bool, Bool] -> Bool + mutable_exprs.append(expr) + elif expr.name in logic_ops_inf_args: # [Bool, ...] -> Bool + mutable_exprs.append(expr) + return mutable_exprs + + +def get_all_op_exprs(con: Expression): + """ + Helper function to get all expressions WITH an operator in a given constraint + """ + # TODO: other types of functions should also be added (e.g. global constraints/functions) + if type(con) in {Comparison, Operator}: + return sum((get_all_op_exprs(arg) for arg in con.args), []) + [con] # All subexpressions + current expression + else: + return [] + + +def get_all_non_op_exprs(con: Expression): + """ + Helper function to get all expressions WITHOUT an operator in a given constraint + """ + # TODO: other types of functions should also be added (e.g. global constraints/functions) + if hasattr(con, 'args') and not isinstance(con, NDVarArray) and con.name != 'boolval': + return sum((get_all_non_op_exprs(arg) for arg in con.args), []) + elif isinstance(con, list) or isinstance(con, NDVarArray) or isinstance(con, tuple): + return sum((get_all_non_op_exprs(e) for e in con), []) + else: + return [con] + + +def get_all_exprs(con: Expression): + """ + Helper function to get all expressions in a given constraint + """ + return get_all_op_exprs(con)[::-1] + get_all_non_op_exprs(con) + + +def get_all_exprs_mult(cons: list): + """ + Helper function to get all expressions in a given list of constraints (e.g. to get all possible arguments for an + expression replacement) + """ + all_exprs = [] + for con in cons: + all_exprs += get_all_exprs(con) + return all_exprs + + +def satisfies_args(func: Function, ints: int, bools: int, constants: int, vars: int, has_bool_return: bool): + """ + Returns whether a new function of the given type `func` can be created with the given amount of arguments. + ~ Parameters: + - `ints`: The amount of integers in the possible arguments (including constants and variables) + - bools`: The amount of booleans in the possible arguments (including variables) + - `constants`: The amount of constants in the possible arguments (only numbers) + - `vars`: The amount of variables in the possible arguments (intvars and boolvars) + - `has_bool_return`: Indicates whether the return type should be boolean (True) or int (False) + ~ Returns: + - True if it is possible to create a new function of given type with the given arguments, False otherwise + """ + match func.type: + case 'op' | 'comp': + match func.name: + case 'wsum': + return constants >= 1 and ints + bools >= func.min_args and has_bool_return == func.bool_return + case 'pow': + return constants >= 1 and ints + bools >= 1 and has_bool_return == func.bool_return + case _: + return ((func.int_args == -1 or func.int_args <= ints + bools) and # enough int args + (func.bool_args == -1 or func.bool_args <= bools) and # enough bool args + (ints + bools >= func.min_args) and # enough args in general + (bools >= func.min_args if func.bool_args == -1 else True) and # enough bools + has_bool_return == func.bool_return) # return type matches + case 'gfun': + match func.name: + case 'Abs' | 'NValue' | 'Count': + return ints + bools >= func.min_args and not has_bool_return + case 'Minimum' | 'Maximum' | 'Element': # We make these have only ints, so it always has the same return type + return constants >= func.min_args and not has_bool_return + case 'Among' | 'NValueExcept': + return constants >= 1 and ints >= func.min_args - 1 and not has_bool_return + case 'gcon': + match func.name: + case 'GlobalCardinalityCount': + return constants >= func.min_args and has_bool_return + case 'IfThenElse' | 'Xor': + return bools >= func.min_args and has_bool_return + case 'Table' | 'NegativeTable' | 'InDomain': + return vars >= 1 and constants >= max(1, func.min_args - 1) and has_bool_return + case 'LexLess' | 'LexLessEq' | 'LexChainLess' | 'LexChainLessEq': + return vars >= func.min_args and has_bool_return + case 'Circuit' | 'Inverse': + return has_bool_return # No arguments required. We fill in the arrays with logical numbers + case _: + return ints + bools >= func.min_args and has_bool_return + + +def generate_new_operator(func: Function, ints: list, bools: list, constants: list, variables: list): + """ + Creates a new function of the given type with the arguments given + ~ Parameters: + - `ints`: The integers in the possible arguments (including constants and variables) + - `bools`: The booleans in the possible arguments (including variables) + - `constants`: The constants in the possible arguments (only numbers) + - `variables`: The variables in the possible arguments (intvars and boolvars) + ~ Returns: + - A new function with arguments from the given lists (or other arguments based on the Function `func`) + """ + comb = ints + bools + match func.type: + case 'op' | 'comp': + # Separate logic for wsum and pow + if func.name == 'wsum': # (-1, 0, False, 2, max_args, 2) + amnt_args = random.randint(func.min_args // 2, min(len(constants), func.max_args // 2)) + # First take constants + constants = random.sample(constants, amnt_args) + # Then the other expressions + others = random.sample(comb, amnt_args) + return Operator(func.name, [constants, others]) + if func.name == 'pow': + args = random.choice(comb), random.choice(constants) + return Operator(func.name, args) + # Logic for all other operators and comparisons is the same + if func.int_args == -1: + amnt_args = random.randint(func.min_args, min(len(comb), + func.max_args)) # Take at least min_args and at most max_args arguments + args = random.sample(comb, amnt_args) + elif func.int_args > 0: + args = random.sample(comb, func.int_args) + if func.bool_args == -1: + amnt_args = random.randint(func.min_args, min(len(bools), + func.max_args)) # Take at least min_args and at most max_args arguments + args = random.sample(bools, amnt_args) + elif func.bool_args > 0: + args = random.sample(bools, func.bool_args) + if func.type == 'op': + return Operator(func.name, args) + if func.type == 'comp': + return Comparison(func.name, *args) + case 'gfun': + match func.name: + case 'Abs': + args = random.choice(comb), + case 'Minimum' | 'Maximum': + amnt_args = random.randint(func.min_args, min(len(constants), func.max_args)) + args = random.sample(constants, amnt_args), + case 'Element': + amnt_args = random.randint(func.min_args, min(len(constants), func.max_args)) + first_arg = random.sample(constants, amnt_args) + # idx = random.randint(0, amnt_args - 1) + constants_filtered = [e for e in constants if (isinstance(e, int) and e <= amnt_args - 1)] # Make sure you can't take an integer out of bounds + idx = random.choice(constants_filtered + variables) + args = first_arg, idx + case 'NValue': + amnt_args = random.randint(func.min_args, min(len(comb), func.max_args)) + args = random.sample(comb, amnt_args), + case 'Count': + amnt_args = random.randint(func.min_args, min(len(comb), func.max_args)) + first_arg = random.sample(comb, amnt_args - 1) + last_arg = random.choice(comb) + args = first_arg, last_arg + case 'Among': + amnt_fst_arg = random.randint(func.min_args // 2, min(len(comb), func.max_args // 2)) + amnt_snd_arg = random.randint(func.min_args // 2, min(len(constants), func.max_args // 2)) + first_arg = random.sample(comb, amnt_fst_arg) + second_arg = random.sample(constants, amnt_snd_arg) + args = first_arg, second_arg + case 'NValueExcept': + amnt_fst_arg = random.randint(func.min_args // 2, min(len(comb), func.max_args // 2)) + first_arg = random.sample(comb, amnt_fst_arg) + second_arg = random.choice(constants) + args = first_arg, second_arg + return func.func(*args) + case 'gcon': + match func.name: + case 'AllDifferent' | 'AllEqual' | 'Increasing' | 'Decreasing' | 'IncreasingStrict' | 'DecreasingStrict': + amnt_args = random.randint(func.min_args, min(len(comb), func.max_args)) + args = random.sample(comb, amnt_args) + case 'AllDifferentExceptN' | 'AllEqualExceptN': + amnt_fst_args = random.randint(func.min_args // 2, min(len(comb), func.max_args // 2)) + amnt_snd_args = random.randint(func.min_args // 2, min(len(comb), func.max_args - amnt_fst_args)) + args = random.sample(comb, amnt_fst_args), random.sample(comb, amnt_snd_args) + case 'LexLess' | 'LexLessEq': + half_amnt_args = random.randint(func.min_args // 2, min(len(variables), func.max_args // 2)) + args = random.sample(variables, half_amnt_args), random.sample(variables, half_amnt_args) + case 'LexChainLess' | 'LexChainLessEq': + amnt_fst_args = random.randint(1, min(len(variables), func.max_args // 4)) + fst_args = random.sample(variables, amnt_fst_args) + amnt_snd_args = random.randint(1, func.max_args // 4) # the amnt of arrays of len of the first one + snd_args = [random.sample(variables, amnt_fst_args) for _ in range(amnt_snd_args)] + args = [fst_args] + snd_args, + case 'Circuit': + amnt_args = random.randint(func.min_args, func.max_args) + args = random.sample(range(amnt_args), amnt_args), + case 'Inverse': + amnt_args = random.randint(func.min_args // 2, func.max_args // 2) + args = random.sample(range(amnt_args), amnt_args), random.sample(range(amnt_args), amnt_args) + case 'IfThenElse': + amnt_args = random.randint(func.min_args, min(len(bools), func.max_args)) + args = random.sample(bools, amnt_args) + case 'Xor': + amnt_args = random.randint(func.min_args, min(len(bools), func.max_args)) + args = random.sample(bools, amnt_args), + case 'Table' | 'NegativeTable': + amnt_fst_arg = random.randint(1, min(len(variables), len(constants), func.max_args // 4)) + amnt_snd_args = random.randint(1, min(len(constants), + func.max_args - amnt_fst_arg) // amnt_fst_arg) * amnt_fst_arg + fst_args = random.sample(variables, amnt_fst_arg) + snd_args = random.sample(constants, amnt_snd_args) + snd_args_transformed = [snd_args[i * amnt_fst_arg:(i + 1) * amnt_fst_arg] for i in + range(int(amnt_snd_args / amnt_fst_arg))] + args = fst_args, snd_args_transformed + case 'InDomain': + fst_arg = random.choice(variables) + amnt_snd_args = random.randint(func.min_args - 1, min(len(constants), func.max_args - 1)) + snd_args = random.sample(constants, amnt_snd_args) + args = fst_arg, snd_args + case 'NoOverlap': + amnt_args = random.randint(func.min_args, min(len(comb), func.max_args // 3)) + args = random.sample(comb, amnt_args), random.sample(comb, amnt_args), random.sample(comb, + amnt_args) + case 'GlobalCardinalityCount': + amnt_fst_args = random.randint(1, min(len(constants), func.max_args - 2)) + amnt_snd_args = random.randint(1, min(len(constants), (func.max_args - amnt_fst_args) // 2)) + counts = [random.randint(0, amnt_fst_args) for _ in range(amnt_snd_args)] + args = random.sample(constants, amnt_fst_args), counts, random.sample(constants, amnt_snd_args) + case _: + args = [] + return func.func(*args) + + +def get_operator(args: list, ret_type: str | bool): + """ + Randomly generates a new Expression that can be created with the given arguments `args` and return type `ret_type`. + ~ Parameters: + - `args`: all arguments that should be in the newly generated function. + - `ret_type`: the return type that the new function should have (usually generated by `get_return_type`). + There are four options: + -> 'constant' for numbers only + -> 'variable' for variables only + -> True for boolean (including variables) + -> False for int (including numbers and variables) + ~ Returns: + - A new Expression with arguments from the given list and with given return type + """ + ints = [e for e in args if not (is_boolexpr(e) or isinstance(e, list) or isinstance(e, NDVarArray) or isinstance(e, tuple))] + bools = [e for e in args if is_boolexpr(e)] + constants = [e for e in args if isinstance(e, int)] + variables = get_variables(args) + if ret_type == 'constant': + if constants: + return random.choice(constants) # Some expressions can't be replaced by functions + intvars = [e for e in variables if not (is_boolexpr(e) or isinstance(e, list) or isinstance(e, NDVarArray) or isinstance(e, tuple))] + if intvars: + return random.choice(intvars) + if ret_type == 'variable' and variables: + return random.choice(variables) # Some expressions can't be replaced by functions + ints_cnt = len(ints) + bools_cnt = len(bools) + constants_cnt = len(constants) + vars_cnt = len(variables) + max_args = 12 # TODO: parametriseer? + + # Operators: + ops = { + # name: (type, int_args, bool_args, bool_return, min_args, max_args) .._args -1 = n-ary, min 2 + name: Function(name, name, *attrs) + for name, attrs in { + 'and': ('op', 0, -1, True, 2, max_args), + 'or': ('op', 0, -1, True, 2, max_args), + '->': ('op', 0, 2, True, 2, 2), + 'not': ('op', 0, 1, True, 1, 1), + 'sum': ('op', -1, 0, False, 2, max_args), + 'wsum': ('op', -1, 0, False, 2, max_args), + 'sub': ('op', 2, 0, False, 2, 2), + 'mul': ('op', 2, 0, False, 2, 2), + 'div': ('op', 2, 0, False, 2, 2), + 'mod': ('op', 2, 0, False, 2, 2), + 'pow': ('op', 2, 0, False, 2, 2), + '-': ('op', 1, 0, False, 1, 1), + }.items() + } + # Comparisons + comps = { + # name: (type, int_args, bool_args, bool_return) .._args -1 = n-ary, min 2 + name: Function(name, name, *attrs) + for name, attrs in { + '==': ('comp', 2, 0, True, 2, 2), + '!=': ('comp', 2, 0, True, 2, 2), + '<=': ('comp', 2, 0, True, 2, 2), + '<': ('comp', 2, 0, True, 2, 2), + '>=': ('comp', 2, 0, True, 2, 2), + '>': ('comp', 2, 0, True, 2, 2) + }.items() + } + # Global functions + global_fns = { + # name: (type, int_args, bool_args, bool_return, min_args, max_args) .._args -1 = n-ary, min 2 + name: Function(name.__name__, name, *attrs) + for name, attrs in { + Abs: ('gfun', 1, 0, False, 1, 1), # expr | (min 1, max 1, /) + Minimum: ('gfun', -1, 0, None, 2, max_args), # [...] | Can return a boolean but this is not known beforehand (min 2, max /) + Maximum: ('gfun', -1, 0, None, 2, max_args), # [...] | Can return a boolean but this is not known beforehand (min 2, max /) + NValue: ('gfun', -1, 0, False, 2, max_args), # [...] | (min 2, max /) + Element: ('gfun', -1, 0, None, 2, max_args), # [...], idx | Can return a boolean but this is not known beforehand (min 2, max /) + # Denk best enkel de array vullen en de idx gewoon tussen 0 en len-1 pakken + Count: ('gfun', -1, 0, False, 2, max_args), # [...], expr | (min 2, max /) + Among: ('gfun', -1, 0, False, 2, max_args), # [...], [...] | Second array can only have constants, no expressions (not even BoolVal()) (min 2, max /) + NValueExcept: ('gfun', -1, 0, False, 2, max_args) # [...], val | Second argument can only have constants, no expressions (not even BoolVal()) (min 2, max /) + }.items() + } + # Global constraints + global_cons = { + # name: (type, int_args, bool_args, bool_return, min_args, max_args, multiple) .._args -1 = n-ary, min 2 + name: Function(name.__name__, name, *attrs) + for name, attrs in { + AllDifferent: ('gcon', -1, 0, True, 2, max_args), # [...] | (min 2, max /) + AllDifferentExceptN: ('gcon', -1, 0, True, 2, max_args), # [...], [...] | Second arg can also be a single non-list constant (min 2, max /) + AllEqual: ('gcon', -1, 0, True, 2, max_args), # [...] | (min 2, max /) + AllEqualExceptN: ('gcon', -1, 0, True, 2, max_args), # [...], [...] | Second arg can also be a single non-list constant (min 2, max /) + Circuit: ('gcon', -1, 0, True, 2, max_args), # [...] | Can only have ints, NO BOOLS! (min 2, max /) + Inverse: ('gcon', -1, 0, True, 2, max_args), # [...], [...] | Can only have ints, NO BOOLS! (min 2, max /) + Table: ('gcon', -1, 0, True, 2, max_args), # [...], [[...],[...],...] | First argument only variables, Second argument should have a multiple amnt of args as the first one (min 2, max /) + NegativeTable: ('gcon', -1, 0, True, 2, max_args), # [...], [[...],[...],...] | First argument only variables, Second argument should have a multiple amnt of args as the first one (min 2, max /) + IfThenElse: ('gcon', 0, 3, True, 3, 3), # arg1, arg2, arg3 (min 3, max 3) + InDomain: ('gcon', -1, 0, True, 2, max_args), # val, [...] | (min 2, max /) + Xor: ('gcon', 0, -1, True, 1, max_args), # [...] | (min 1, max /) + # Cumulative: (-1, 0, True), # st, dur, end, demand, cap (Ingewikkelde constraint) + # Precedence: (?, ?, True), # (Ingewikkelde constraint) + NoOverlap: ('gcon', -1, 0, True, 3, max_args), # [...], [...], [...] | Three lists all have same length (min 3, max /) + GlobalCardinalityCount: ('gcon', -1, 0, True, 2, max_args), # [...], [...], [...] | The first and last list have to be the same length and + # they all have to be ints, NO BOOLS (min 2, max /) + Increasing: ('gcon', -1, 0, True, 2, max_args), # [...] (min 2, max /, /) + Decreasing: ('gcon', -1, 0, True, 2, max_args), # [...] (min 2, max /, /) + IncreasingStrict: ('gcon', -1, 0, True, 2, max_args), # [...] (min 2, max /, /) + DecreasingStrict: ('gcon', -1, 0, True, 2, max_args), # [...] (min 2, max /, /) + LexLess: ('gcon', -1, 0, True, 2, max_args), # [...], [...] | Lists have same length (min 2, max /), ONLY VARS + LexLessEq: ('gcon', -1, 0, True, 2, max_args), # [...], [...] | Lists have same length (min 2, max /), ONLY VARS + LexChainLess: ('gcon', -1, 0, True, 2, max_args), # [...][...] | Rows have same length (min 2, max /), ONLY VARS + LexChainLessEq: ('gcon', -1, 0, True, 2, max_args), # [...][...] | Rows have same length (min 2, max /), ONLY VARS + }.items() + } + all_ops = ops | comps | global_fns | global_cons + # print(f"ints_cnt={ints_cnt},bools_cnt={bools_cnt},has_bool_return={has_bool_return}") + assert isinstance(ret_type, bool), f"Getting here means the return type should be a boolean. It is {ret_type}." + after = {k: v for k, v in all_ops.items() if + satisfies_args(v, ints_cnt, bools_cnt, constants_cnt, vars_cnt, ret_type)} + if after: + func = random.choice(list(after.values())) + else: + return None + return generate_new_operator(func, ints, bools, constants, variables) + + +def find_all_occurrences(con: Expression, target_expr: Expression): + """ + Recursively finds all occurrences of `target_expr` in the expression `con`. + ~ Parameters: + - `con`: constraint in which we search + - `target_expr`: the expression we're searching the occurrences for + ~ Returns: + - `occurrences`: a list of paths (as tuples) to each occurrence. + """ + occurrences = [] + # np.int32 didn't match with `is` + if (isinstance(con, np.int32) and isinstance(target_expr, np.int32) and con == target_expr) or \ + con is target_expr: + occurrences.append(()) + if hasattr(con, 'args') and not isinstance(con, NDVarArray) and con.name != 'boolval': + for i, arg in enumerate(con.args): + for path in find_all_occurrences(arg, target_expr): + occurrences.append((i,) + path) # Add index to the path + elif isinstance(con, list) or isinstance(con, NDVarArray) or isinstance(con, tuple): + for i, arg in enumerate(con): + for path in find_all_occurrences(arg, target_expr): + occurrences.append((i,) + path) + return occurrences + + +def replace_at_path(con: Expression, path: tuple, new_expr: Expression): + """ + Replace the Expression at the given `path` in the expression tree `con` with `new_expr`. + + ~ Parameters: + - `con`: The constraint in which we will replace an expression + - `path`: The path to the expression we will mutate (e.g. y has path (0, 1) in (x > y) -> p) + - `new_expr`: The new expression which will be at the specified `path` + ~ Returns: + - `con`: The mutated constraint + """ + if not path: # Replace main expression + return new_expr + new_expr = copy.deepcopy(new_expr) # Important to avoid infinite recursion! + parent = con + + # Traverse the parents until we have the final parent + for idx in path[:-1]: + if hasattr(parent, 'args') and not isinstance(parent, NDVarArray) and parent.name != 'boolval': + parent = parent.args[idx] + elif isinstance(parent, list) or isinstance(parent, NDVarArray) or isinstance(parent, tuple): + parent = parent[idx] + + # Change the arguments of the parent + if hasattr(parent, 'args') and not isinstance(parent, NDVarArray) and parent.name != 'boolval': + args = list(parent.args) + args[path[-1]] = new_expr + parent.update_args(args) + elif isinstance(parent, list) or isinstance(parent, NDVarArray): + parent[path[-1]] = new_expr + elif isinstance(parent, tuple): + parent = list(parent) + parent[path[-1]] = new_expr + parent = tuple(parent) + return con + + +def expr_at_path(con: Expression, path: tuple, expr: Expression): + """ + Helper function for checking whether the given expression is on the given path in the given constraint. + Upon encountering `None` in a path, it will return True. + """ + if not path and con is expr: + return True + # Traverse the parents until we have the final parent + for idx in path: + if idx is not None: + if hasattr(con, 'args') and not isinstance(con, NDVarArray) and con.name != 'boolval': + con = con.args[idx] + elif isinstance(con, list) or isinstance(con, NDVarArray) or isinstance(con, tuple): + con = con[idx] + else: + return len(find_all_occurrences(con, expr)) > 0 + return con is expr + + +def get_return_type(expr: Expression, con: Expression): + """ + Function to get the return type of expressions that are allowed to replace `expr` in a given constraint `con`. + There are four options: + - boolean (any type of boolean including 'Expression's which are of type boolean (e.g. BoolVal(True), x == 5, p, ...)) + - int (any type of integer including 'Expression's which are of type int (e.g. 1, 1 + 2, x, ...)) + - constant (integers that are constants. No 'Expression's allowed. (e.g. 1, 2, ...; NOT: 1 + 2, x, ...)) + - variable (variables that aren't 'Expression's. (e.g. x, y, p, q; NOT: x == y, x > y, ...)) + ~ Parameters: + - `expr`: the expression which we want to mutate + - `con`: the constraint in which the expression is found + ~ Returns: + - `path`: the path at which the expression would be mutated + - `ret_type`: the type that the expression is allowed to be mutated by, given either as a string or a boolean. + """ + # Define functions of which the arguments are restricted to be constants and the remaining path length the argument would be in + constant_restricted_functions = {Minimum: (1, (None,)), + Maximum: (1, (None,)), + Element: (2, (None,)), + Among: (2, (1, None)), + NValueExcept: (1, (1,)), + Circuit: (1, (None,)), + Inverse: (2, (None,)), + GlobalCardinalityCount: (2, (None,)), + Table: (3, (1, None)), + NegativeTable: (3, (1, None)), + # Count: (1, (1, None)), # TODO: Is this still necessary? + 'pow': (1, (1, None)), + 'wsum': (2, (0, None))} + variable_restricted_functions = {Table: (2, (0, None)), + NegativeTable: (2, (0, None)), + LexLess: (2, (None,)), + LexLessEq: (2, (None,)), + LexChainLess: (2, (None,)), + LexChainLessEq: (2, (None,))} + + paths = find_all_occurrences(con, expr) + path = random.choice(paths) + path_len = len(path) + for i, idx in enumerate(path): + if type(con) in constant_restricted_functions: + remaining_path_len, remaining_path = constant_restricted_functions[type(con)] + if path_len - i == remaining_path_len and expr_at_path(con, remaining_path, expr): + return path, 'constant' + elif isinstance(con, Operator) and (con.name == 'wsum' or con.name == 'pow'): + remaining_path_len, remaining_path = constant_restricted_functions[con.name] + if path_len - i == remaining_path_len and expr_at_path(con, remaining_path, expr): + return path, 'constant' + if type(con) in variable_restricted_functions: + remaining_path_len, remaining_path = variable_restricted_functions[type(con)] + if path_len - i == remaining_path_len and expr_at_path(con, remaining_path, expr): + return path, 'variable' + if hasattr(con, 'args') and not isinstance(con, NDVarArray) and con.name != 'boolval': + con = con.args[idx] + elif isinstance(con, list) or isinstance(con, NDVarArray) or isinstance(con, tuple): + con = con[idx] + # We should only get here if the argument isn't in one of the functions above + return path, is_boolexpr(expr) + + +def type_aware_expression_replacement(constraints: list): + """ + Replaces a random expression of a random constraint from a list of given constraints. It replaces this expression + by an operator with the same return type that takes as arguments the other expressions from all constraints. + IMPORTANT: This can change satisfiability of the constraint! Only to be used with verifiers that allow this! + This means it returns a list of ALL constraints and has to be handled accordingly in the 'generate_mutations' + function to swap out the constraints instead of adding them. + + ~ Parameters: + - `constraints`: a list of all the constraints to possibly be mutated + ~ Return: + - `final_cons`: a list of the same constraints where one constraint has a mutated expression + """ + try: + final_cons = copy.deepcopy(constraints) + + # 1. Neem een (random) expression van een (random) constraint en de return type + rand_con = random.choice(final_cons) + all_con_exprs = get_all_exprs(rand_con) + expr = random.choice(all_con_exprs) + path, ret_type = get_return_type(expr, rand_con) # Also gives us the taken path of the expression in the constraint + # (Might be more than one occurrence so we should take the right one) + # 2. Tel het aantal resterende params van elk type + all_exprs = get_all_exprs_mult(final_cons) + + # 3. Zoek een operator die <= aantal params nodig heeft met zelfde return type + new_expr = get_operator(all_exprs, ret_type) + + # 4. Vervang expression (+ vervang constraint) + if new_expr: + new_con = replace_at_path(rand_con, path, new_expr=new_expr) + + # 5. Return the new constraints + # final_cons.remove(rand_con) DOES NOT WORK because it uses == instead of 'is' + index = None + for i, constraint in enumerate(final_cons): + if constraint is rand_con: + index = i + break + if index is not None: + del final_cons[index] + final_cons.append(new_con) + return final_cons + except Exception as e: + raise Exception(e) + + +def has_positive_parity(expr: Expression, con: Expression, curr_path: tuple) -> tuple | None: + """ + Function to retrieve the parity of an expression `expr` in the given constraint `con`. This means it shows + whether the constraint weakens or strengthens when the expression does. + ~ Parameters: + - `expr`: the expression that would be strengthened/weakened. + - `con`: the constraint that would be strengthened/weakened. + ~ Returns: + - `pos_parity`: True if the constraint strengthens (weakens) upon the expression strengthening, + False if it doesn't, + None if it is unknown. + """ + # Basecase 1: `expr` cannot be strengthened or weakened + if hasattr(expr, 'name'): + # NOTE: these are not necessarily the only expressions that can be strengthened/weakened. + # (some double work is being done in function `is_changeable` so todo?) + changeable_ops = {'and', 'or', '->', 'xor', '==', '!=', '<=', '<', '>=', '>'} + changeable_globals = {AllDifferent, AllDifferentExceptN, AllEqual, AllEqualExceptN, + Table, NegativeTable, IncreasingStrict, DecreasingStrict, + LexLess, LexChainLess, Increasing, Decreasing, LexLessEq, + LexChainLessEq, InDomain} + if not (expr.name in changeable_ops or type(expr) in changeable_globals): + return None + else: + return None + + # Basecase 2: + if expr is con: + return True, curr_path + + # Recursively check in the arguments and change result upon encountering "not" operators + # TODO: extend with other operators. e.g. the left side of `->` also has negative parity + if con.name == 'not': + curr_path += 0, + neg_res = has_positive_parity(expr, con.args[0], curr_path) + return not neg_res, curr_path if neg_res is not None else None + if con.name == 'and' or con.name == 'or': + args = con.args + subtrees = list(enumerate(args)) + random.shuffle(subtrees) + for path, subtree in subtrees: + if any(expr is e for e in get_all_exprs(subtree)): # check if expr is in the subtree + curr_path += path, + return has_positive_parity(expr, subtree, curr_path) + raise Exception(f"The given expression {expr} is not in any of the arguments: {args}.") + + # If the constraint is anything else, we don't know the parity + return None + + +def strengthen_expr(expr: Expression, path: tuple, con: Expression) -> Expression: + """ + Strengthen the given expression `expr` in the given constraint `con`. + ~ Parameters: + - `expr`: the expression that will be strengthened. + - `con`: the constraint that will be strengthened/weakened. + ~ Returns: + - `con`: the constraint after the mutation. + """ + # TODO: 'and' & 'or' strengthenable by adding/removing args + other functions too + match expr.name: # {'or', '->', '!=', '<=', '>='} + case 'or': # and, xor, !=, <, > + args = expr.args + if len(args) != 2: + return con + comps = ['!=', '<', '>'] + ops = ['and'] + others = ['xor'] + new_op = random.choice(comps + ops + others) + case '->': # and, ==, < + comps = ['==', '<'] + ops = ['and'] + new_op = random.choice(comps + ops) + args = expr.args + case '!=': # <, > + comps = ['<', '>'] + new_op = random.choice(comps) + args = expr.args + case '<=': # <, == + comps = ['<', '=='] + new_op = random.choice(comps) + args = expr.args + case '>=': # >, == + comps = ['>', '=='] + new_op = random.choice(comps) + args = expr.args + + match expr: + case Increasing(): + expr.name = 'IncreasingStrict' + case Decreasing(): + expr.name = 'DecreasingStrict' + case LexLessEq(): + expr.name = 'LexLess' + case LexChainLessEq(): + expr.name = 'LexChainLess' + case NegativeTable(): + fst_args, snd_args = expr.args + random_idx = random.randrange(len(fst_args)) + new_fst_args = fst_args[:random_idx] + fst_args[random_idx + 1:] + new_snd_args = [arg[:random_idx] + arg[random_idx + 1:] for arg in snd_args] + expr.update_args((new_fst_args, new_snd_args)) + case InDomain(): + fst_args, snd_args = expr.args + random_idx = random.randrange(len(snd_args)) + new_snd_args = snd_args[:random_idx] + snd_args[random_idx + 1:] + expr.update_args((fst_args, new_snd_args)) + + if 'new_op' in locals(): # Rewrite this later + if new_op in comps: + expr = Comparison(new_op, *args) + elif new_op in ops: + expr = Operator(new_op, args) + elif new_op == 'xor': + expr = Xor(args) + + con = replace_at_path(con, path, expr) + return con + + +def weaken_expr(expr: Expression, path: tuple, con: Expression) -> Expression: + """ + Weaken the given expression `expr` in the given constraint `con`. + ~ Parameters: + - `expr`: the expression that will be weakened. + - `con`: the constraint that will be strengthened/weakened. + ~ Returns: + - `con`: the constraint after the mutation. + """ + # TODO: 'and' & 'or' weakenable by removing/adding args + other functions too + match expr.name: # {'and', 'xor', '==', '<', '>'} + case 'and': # or, ->, ==, <=, >= + args = expr.args + if len(args) != 2: + return con + comps = ['==', '<=', '>='] + ops = ['or', '->'] + new_op = random.choice(comps + ops) + case 'xor': # or + args = expr.args + if len(args) != 2: + return con + new_op = 'or' + case '==': # <=, >= + comps = ['<=', '>='] + new_op = random.choice(comps) + args = expr.args + case '<': # !=, <= + comps = ['!=', '<='] + new_op = random.choice(comps) + args = expr.args + case '>': # != >= + comps = ['!=', '>='] + new_op = random.choice(comps) + args = expr.args + + match expr: + case IncreasingStrict(): + expr.name = 'Increasing' + case DecreasingStrict(): + expr.name = 'Decreasing' + case LexLess(): + expr.name = 'LexLessEq' + case LexChainLess(): + expr.name = 'LexChainLessEq' + case Table(): + fst_args, snd_args = expr.args + random_idx = random.randrange(len(fst_args)) + new_fst_args = fst_args[:random_idx] + fst_args[random_idx + 1:] + new_snd_args = [arg[:random_idx] + arg[random_idx + 1:] for arg in snd_args] + expr.update_args((new_fst_args, new_snd_args)) + case AllDifferent() | AllEqual(): + old_args = expr.args + random_idx = random.randrange(len(old_args)) + new_args = old_args[:random_idx] + old_args[random_idx + 1:] + expr.update_args(new_args) + case AllDifferentExceptN() | AllEqualExceptN(): + fst_args, snd_args = expr.args + random_idx = random.randrange(len(fst_args)) + new_fst_args = fst_args[:random_idx] + fst_args[random_idx + 1:] + expr.update_args((new_fst_args, snd_args)) + + if 'new_op' in locals(): # Rewrite this later + if new_op in comps: + expr = Comparison(new_op, *args) + elif new_op in ops: + expr = Operator(new_op, args) + elif new_op == 'xor': + expr = Xor(args) + + con = replace_at_path(con, path, expr) + return con + + +def is_changeable(strengthen: bool, expr: Expression, pos_parity: bool) -> bool: + # Sets to be extended when more weakening and strengthening options get added + if strengthen ^ pos_parity: # weakening + is_changeable_op = expr.name in {'and', 'xor', '==', '>', '<'} + is_changeable_global = type(expr) in {AllDifferent, AllDifferentExceptN, AllEqual, AllEqualExceptN, + Table, NegativeTable, IncreasingStrict, DecreasingStrict, + LexLess, LexChainLess} + else: # strengthening + is_changeable_op = expr.name in {'or', '->', '!=', '<=', '>='} + is_changeable_global = type(expr) in {Increasing, Decreasing, LexLessEq, LexChainLessEq, NegativeTable, InDomain} + return is_changeable_op or is_changeable_global + + +def strengthening_weakening_mutator(constraints: list, strengthen: bool = True) -> list | Exception: + """ + Strengthens or weakens a (random?) constraint from a list of given constraints by replacing an operator of this constraint. + IMPORTANT: This can change satisfiability of the constraint! Only to be used with verifiers that allow this! + This means it returns a list of ALL constraints and has to be handled accordingly in the 'generate_mutations' + function to swap out the constraints instead of adding them. + + ~ Parameters: + - `constraints`: a list of all the constraints to possibly be mutated + - `strengthen`: a boolean indicating whether the mutator should strengthen or weaken a constraint + ~ Return: + - `final_cons`: a list of the same constraints where one constraint has a mutated operator + """ + # TODO: right now: checks for possible expressions to strengthen/weaken and THEN calculates whether it should be + # strengthened or weakened. + # should be: calculate parity while searching for possible expressions and dismiss them if they can't be + # strengthened or weakened based on that. + try: + final_cons = copy.deepcopy(constraints) + + # pick a random constraint and calculate whether they have a mutable expression until they do + candidates = [] + for item in constraints: + if not any(item is cand for cand in candidates): + candidates.append(item) + # candidates = list(set(constraints)) # does not work with NDVarArray + random.shuffle(candidates) + for con in candidates: + exprs = [] + for e in get_all_exprs(con): + parity = has_positive_parity(e, con, curr_path=tuple()) + if parity is not None and is_changeable(strengthen, e, parity[0]): + exprs.append((e, parity)) + if exprs: + break + else: # In case there isn't any mutable (weakening/strengthening depending on `strengthen`) expression in any constraint + return final_cons + + # Remove the constraint from the constraints + final_cons.remove(con) + + # Choose an expression to change + expr, (pos_parity, path) = random.choice(exprs) + + # Mutate this expression + if strengthen ^ pos_parity: # weaken if parity is different from `strengthen` + con = weaken_expr(expr, path, con) + else: + con = strengthen_expr(expr, path, con) + + # Add the changed constraint back + final_cons.append(con) + return final_cons + + except Exception as e: + raise Exception(e) + + +def change_domain_mutator(constraints: list, strengthen: bool): + # TODO? something else for boolean variables? + try: + # Take random integer variable + variables = [v for v in get_variables(constraints) if not is_boolexpr(v)] + if variables: # Don't change if no integer variables + rand_var = random.choice(variables) + + lb = rand_var.lb + ub = rand_var.ub + if strengthen: + rand_var.lb = random.randint(lb, max(lb, ub - 1)) + rand_var.ub = random.randint(min(ub, rand_var.lb + 1), ub) + else: + expansion_param = 2 # How much bigger should the domain possibly be + avg = (ub + lb) / 2 + max_ub = int(avg + (ub - avg) * expansion_param) + min_lb = int(avg + (lb - avg) * expansion_param) + rand_var.lb = random.randint(min_lb, lb) + rand_var.ub = random.randint(ub, max_ub) + + # Return the given constraints to be compatible with how the other non-metamorphic mutators are called + return constraints + + except Exception as e: + raise Exception(e) + + class MetamorphicError(Exception): pass + ''' returns a list of aritmetic expressions (as lists of indexes to traverse the expression tree) that occur in the input expression. One (random) candidate is taken from each level of the expression if there exists one ''' -def pickaritmetic(con,log=[], candidates=[]): - if hasattr(con,'name'): + + +def pickaritmetic(con, log=[], candidates=[]): + if hasattr(con, 'name'): if con.name == 'wsum': - #wsum has lists as arguments so we need a separate case - #wsum is the lowest possible level + # wsum has lists as arguments so we need a separate case + # wsum is the lowest possible level return candidates + [log] - if con.name == "element":# or con.name == "table" or con.name == "cumulative": - #no good way to know if element will return bool or not so ignore it + if con.name == "element": # or con.name == "table" or con.name == "cumulative": + # no good way to know if element will return bool or not so ignore it return candidates if hasattr(con, "args"): iargs = [(j, e) for j, e in enumerate(con.args)] random.shuffle(iargs) for j, arg in iargs: if is_boolexpr(arg): - res = pickaritmetic(arg,log+[j]) + res = pickaritmetic(arg, log + [j]) if res != []: return res elif is_any_list(arg): - return pickaritmetic((arg,log+[j],candidates)) + return pickaritmetic((arg, log + [j], candidates)) else: - return pickaritmetic(arg,log+[j],candidates+[log+[j]]) + return pickaritmetic(arg, log + [j], candidates + [log + [j]]) return candidates + ''' Adapted pickaritmetic that only picks from arithmetic comparisons used for mutators that i.e. multiple both sides with a number returns a list of aritmetic expressions (as lists of indexes to traverse the expression tree) that occur in the input expression. One (random) candidate is taken from each level of the expression if there exists one ''' -def pickaritmeticComparison(con,log=[], candidates=[]): - if hasattr(con,'name'): + + +def pickaritmeticComparison(con, log=[], candidates=[]): + if hasattr(con, 'name'): if con.name == 'wsum': - #wsum has lists as arguments so we need a separate case - #wsum is the lowest possible level + # wsum has lists as arguments so we need a separate case + # wsum is the lowest possible level return candidates if con.name == "element" or con.name == "table" or con.name == 'cumulative': - #no good way to know if element will return bool or not so ignore it (lists and element always return false to isbool) + # no good way to know if element will return bool or not so ignore it (lists and element always return false to isbool) return candidates if hasattr(con, "args"): iargs = [(j, e) for j, e in enumerate(con.args)] random.shuffle(iargs) for j, arg in iargs: if is_boolexpr(arg): - res = pickaritmeticComparison(arg,log+[j], candidates) + res = pickaritmeticComparison(arg, log + [j], candidates) if res != []: return res else: - if isinstance(con,Comparison): - return pickaritmeticComparison(arg,log+[j],candidates+[log]) + if isinstance(con, Comparison): + return pickaritmeticComparison(arg, log + [j], candidates + [log]) else: - return pickaritmeticComparison(arg,log+[j],candidates) + return pickaritmeticComparison(arg, log + [j], candidates) - return candidates \ No newline at end of file + return candidates diff --git a/fuzz_test_utils/output_writer.py b/fuzz_test_utils/output_writer.py index 98399c8e..09f63b5d 100644 --- a/fuzz_test_utils/output_writer.py +++ b/fuzz_test_utils/output_writer.py @@ -1,7 +1,12 @@ import math import pickle +import csv +import glob +import os from os.path import join from datetime import datetime +from fuzz_test_utils.mutators import type_aware_operator_replacement, type_aware_expression_replacement, strengthening_weakening_mutator + def create_error_output_text(error_data: dict) -> str: """ @@ -24,6 +29,61 @@ def create_error_output_text(error_data: dict) -> str: # return a more readable/user friendly error description ready to write to a file return f"An error occured while running a test\n\nUsed solver: {error_data['solver']}\n{verifier_text}\nWith {error_data['mutations_per_model']} mutations per model\nWith seed: {error_data['seed']}\nThe test failed in {execution_time_text}\n\nError Details:\n{error_text}" +def match_conditions(exc_str): + return [ + (lambda s: any(x in s for x in ["'bool' object is not iterable", "'_BoolVarImpl' object is not iterable"]), "01_bool_obj_not_iterable/"), + (lambda s: "slice indices must be integers or None or have an __index__ method" in s, "02_slice_indices_must_be_ints/"), + (lambda s: all(x in s for x in ["Expecting value: line", "column ", "(char "]), "03_line_x_column_x/"), + (lambda s: any(x in s for x in ["lhs cannot be an integer at this point!", "not supported: model.get_or_make_boolean_index(boolval(False))"]), "04_lhs_no_int/"), + (lambda s: "'bool' object has no attribute 'implies'" in s, "05_bool_obj_no_implies/"), + (lambda s: " has no constraints" in s, "06_no_constraints_TO_FIX/"), + (lambda s: any(x in s for x in ["or-tools does not accept a 'modulo' operation where '0' is in the domain of the divisor", "An int_mod must have a strictly positive modulo argument", "The domain of the divisor cannot contain 0", "Modulo with a divisor domain containing 0 is not supported.", "Power operator: For integer values, exponent must be non-negative:"]), "07_div0_pow-neg/"), + (lambda s: "object of type '_BoolVarImpl' has no len()" in s, "08_object_type_boolvarimpl_no_len/"), + (lambda s: any(x in s for x in ["'int' object has no attribute 'lb'", "object has no attribute 'lb'"]), "09_int_obj_no_attr_lb/"), + (lambda s: all(x in s for x in ["Cannot convert", "to Choco variable"]), "10_cannot_convert_to_choco_var/"), + (lambda s: any(x in s for x in ["Translation of gurobi status 11 to CPMpy status not implemented", "KeyboardInterrupt", "cannot access local variable 'proc' where it is not associated with a value"]), "11_keyboard_interrupt/"), + (lambda s: "Cannot modify read-only attribute 'args', use 'update_args()'" in s, "12_cant_modify_args/"), + (lambda s: "Gurobi only supports division by constants, but got " in s, "13_gurobi_only_div_cst/"), + (lambda s: any(x in s for x in ["Could not resolve host: ", "Maximum number of failing server authorization attempts reached"]), "_temp/"), + (lambda s: "'int' object has no attribute 'get_bounds'" in s, "14_int_objc_no_attr_getbounds/"), + (lambda s: all(x in s for x in ["Domain of ", " only contains 0"]), "15_dom_only_contains_0/"), + (lambda s: "'int' object has no attribute 'handle'" in s, "16_int_obj_no_attr_handle/"), + (lambda s: "not an linear expression: " in s, "17_not_lin_expr_bool/"), + (lambda s: "empty range for randrange()" in s, "18_empty_randrange/"), + (lambda s: "Results of the solvers are not equal. Solver results:" in s, "19_amnt_sol_neq/"), + (lambda s: "in method 'int_array_set', argument 2 of type 'int'" in s, "20_argx_type_y/"), + (lambda s: "'bool' object has no attribute 'has_subexpr'" in s, "21_bool_obj_no_has_subexpr/"), + (lambda s: "'int' object has no attribute 'is_bool'" in s, "22_int_obj_no_is_bool/"), + (lambda s: "not supported: model.get_or_make_boolean_index(" in s, "23_not_supported_get_or_make_boolean_index/"), + (lambda s: any(x in s for x in ["'BoolVal' object has no attribute 'get_integer_var_value_map'", "Not a known var "]), "24_not_known_var/"), + (lambda s: "ut of memory" in s, "25_out_of_mem/"), + (lambda s: all(x in s for x in ["Unsupported boolexpr", "in reification"]), "26_unsupported_boolexpr/"), + (lambda s: "not a variable" in s, "27_not_a_variable/"), + (lambda s: "Invalid rhs argument for general constraint of indicator type" in s, "28_invalid_rhs_arg/"), + (lambda s: "MiniZinc stopped with a non-zero exit code, but did not output an error message." in s, "29_minizinc_nonzero_exitcode/"), + (lambda s: "The size of a performed interval must be >= 0 in constraint" in s, "30_interval_size_gt0/"), + (lambda s: "must be real number, not" in s, "31_must_be_real/"), + (lambda s: "n-ary operators require at least one argument" in s, "32_n-ary_ops_gt_1_arg/"), + (lambda s: "Bound requested for unknown expression" in s, "33_bound_request_unknown_expression/"), + (lambda s: "arrays cannot be elements of arrays" in s, "34_arrays_no_elem_of_array/"), + (lambda s: "not enough values to unpack" in s, "35_not_enough_values_unpack/"), + ] + +def get_logging_dir(error_data, logging_dir): + logging_dir += "/" + error = error_data["error"] + exception = error["exception"] + exc_str = str(exception) + + # Check whether the exception matches some format + for condition, path in match_conditions(exc_str): + if condition(exc_str): + logging_dir += path + break + else: + logging_dir += "UNKNOWN/" + + return logging_dir def write_error(error_data: dict, output_dir: str) -> None: """ @@ -40,4 +100,168 @@ def write_error(error_data: dict, output_dir: str) -> None: pickle.dump(error_data, file=ff) with open(join(output_dir, f"{error_data['error']['type'].name}_{date_text}.txt"), "w") as ff: - ff.write(create_error_output_text(error_data)) \ No newline at end of file + ff.write(create_error_output_text(error_data)) + + +# Below are all help functions for writing the csv file +def get_bug_class(error_data): + exc_str = str(error_data['error']['exception']) + # Check whether the exception matches some format + for condition, classification in match_conditions(exc_str): + if condition(exc_str): + bug_class = classification[3:-1] + break + else: + bug_class = "UNKNOWN" + return bug_class + + +def get_verifier(error_data): + return error_data['verifier'] + + +def get_solvers(error_data): + return error_data['solver'] + + +def get_seed(error_data): + return error_data['error']['seed'] + + +def get_time_taken(error_data): + return error_data['execution_time'] + + +def get_bug_type(error_data): + return error_data['error']['type'] + + +def get_exception(error_data): + return error_data['error']['exception'] + + +def get_original_cons(error_data): + return error_data['error']['originalmodel'].constraints + + +def get_current_cons(error_data): + return error_data['error']['constraints'] + + +def get_mutations(error_data): + if 'mutators' in error_data['error']: + return error_data['error']['mutators'][2::3] + else: + return [] + + +def get_nr_mm_mutations(error_data): + return len([m for m in get_mutations(error_data) if + m not in {type_aware_expression_replacement, type_aware_operator_replacement, + strengthening_weakening_mutator}]) + + +def get_nr_gen_mutations(error_data): + return len([m for m in get_mutations(error_data) if + m in {type_aware_expression_replacement, type_aware_operator_replacement, + strengthening_weakening_mutator}]) + + +def get_nr_mutations(error_data): + return len(get_mutations(error_data)) + + +def get_bugged_solver(error_data): + error = error_data['error'] + all_solvers = ['minizinc', 'ortools', 'gurobi', 'choco', 'z3'] + if 'stacktrace' in error: + stacktrace = error['stacktrace'] + for solver in all_solvers: + if solver in str(stacktrace): + return solver + elif 'exception' in error: # In case of a failed model (no crash) + exc = error['exception'] + possibly_bugged = [s for s in all_solvers if s in str(exc)] + if possibly_bugged: + return possibly_bugged + return 'UNKNOWN' + + +def get_objective(error_data): + return error_data['error']['originalmodel'].objective + + +def get_variables(error_data): + return error_data['error']['variables'] + + +def get_nr_solve_checks(error_data): + return error_data['error']['nr_solve_checks'] + + +def get_cause(error_data): + return error_data['error']['caused_by'] + + +def get_nr_timed_out_solve_calls(error_data): + return error_data['error']['nr_timed_out'] + + +def extract_last_stacktrace_lines(error_data) -> str: + stacktrace = error_data['error']['stacktrace'] + lines = stacktrace.strip().splitlines() + last_file_index = None + + for i, line in enumerate(lines): + if line.strip().startswith("File"): + last_file_index = i + + if last_file_index is not None: + return '\n'.join(lines[last_file_index:]).strip() + else: + return '' + + +def write_csv(error_data: dict, output_path) -> None: + columns_and_functions = [ + ("bug_class", get_bug_class), + ("verifier", get_verifier), + ("solvers", get_solvers), + ("seed", get_seed), + ("time_taken", get_time_taken), + ("bug_type", get_bug_type), + ("exception", get_exception), + ("last_stacktrace_line", extract_last_stacktrace_lines), + ("original_constraints", get_original_cons), + ("current_constraints", get_current_cons), + ("total_nr_mutations", get_nr_mutations), + ("nr_mm_mutations", get_nr_mm_mutations), + ("nr_gen_mutations", get_nr_gen_mutations), + ("mutations", get_mutations), + ("bugged_solver", get_bugged_solver), + ("objective", get_objective), + ("variables", get_variables), + ("nr_solve_checks", get_nr_solve_checks), + ("bug_cause", get_cause), + ("nr_timed_out_solve_calls", get_nr_timed_out_solve_calls) + ] + + file_exists = os.path.isfile(output_path) + + with open(output_path, mode='a', newline='', encoding='utf-8') as csvfile: + writer = csv.writer(csvfile) + + if not file_exists: + # Write header + headers = [col for col, _ in columns_and_functions] + writer.writerow(headers) + + # Write the error data row + row = [] + for _, func in columns_and_functions: + try: + value = func(error_data) + except Exception as e: + value = f"ERROR: {e}" + row.append(value) + writer.writerow(row) diff --git a/verifiers/__init__.py b/verifiers/__init__.py index 390208df..b8dd4412 100644 --- a/verifiers/__init__.py +++ b/verifiers/__init__.py @@ -13,6 +13,11 @@ from .model_counting_verifier import Model_Count_Verifier from .equivalance_verifier import Equivalance_Verifier from .optimization_verifier import Optimization_Verifier +from .solver_voting_sat_verifier import Solver_Vote_Sat_Verifier +from .solver_voting_count_verifier import Solver_Vote_Count_Verifier +from .strengthening_weakening_verifier import Strengthening_Weakening_Verifier +from .solver_voting_eq_verifier import Solver_Vote_Eq_Verifier +from .solver_voting_sol_verifier import Solver_Vote_Sol_Verifier from .verifier_runner import run_verifiers, get_all_verifiers @@ -31,7 +36,22 @@ def lookup_verifier(verfier_name: str) -> Verifier: elif verfier_name == "equivalance verifier": return Equivalance_Verifier - - else: + + elif verfier_name == "solver_vote_sat_verifier": + return Solver_Vote_Sat_Verifier + + elif verfier_name == "solver_vote_count_verifier": + return Solver_Vote_Count_Verifier + + elif verfier_name == "strengthening_weakening_verifier": + return Strengthening_Weakening_Verifier + + elif verfier_name == "solver_vote_eq_verifier": + return Solver_Vote_Eq_Verifier + + elif verfier_name == "solver_vote_sol_verifier": + return Solver_Vote_Sol_Verifier + + else: raise ValueError(f"Error verifier with name {verfier_name} does not exist") return None \ No newline at end of file diff --git a/verifiers/model_counting_verifier.py b/verifiers/model_counting_verifier.py index 169b1167..f226becc 100644 --- a/verifiers/model_counting_verifier.py +++ b/verifiers/model_counting_verifier.py @@ -34,7 +34,11 @@ def initialize_run(self) -> None: assert (len(self.cons)>0), f"{self.model_file} has no constraints" self.cons = toplevel_list(self.cons) - self.sol_count = cp.Model(self.cons).solveAll(solver=self.solver,time_limit=max(1,min(250,self.time_limit-time.time()))) + if self.solver == 'gurobi': + self.sol_lim = 10000 # Should this be hardcoded? + self.sol_count = cp.Model(self.cons).solveAll(solver=self.solver,time_limit=max(1,min(250,self.time_limit-time.time())), solution_limit=self.sol_lim) + else: + self.sol_count = cp.Model(self.cons).solveAll(solver=self.solver,time_limit=max(1,min(250,self.time_limit-time.time()))) self.mutators = [copy.deepcopy(self.cons)] #keep track of list of cons alternated with mutators that transformed it into the next list of cons. def verify_model(self) -> dict: @@ -42,7 +46,10 @@ def verify_model(self) -> dict: model = cp.Model(self.cons) time_limit=max(1,min(200,self.time_limit-time.time())) # set the max time limit to the given time limit or to 1 if the self.time_limit-time.time() would be smaller then 1 - new_count = model.solveAll(solver=self.solver, time_limit=time_limit) + if hasattr(self, 'sol_lim'): + new_count = model.solveAll(solver=self.solver, time_limit=time_limit, solution_limit=self.sol_lim) + else: + new_count = model.solveAll(solver=self.solver, time_limit=time_limit) if model.status().runtime > time_limit-10: # timeout, skip print('T', end='', flush=True) diff --git a/verifiers/solver_voting_count_verifier.py b/verifiers/solver_voting_count_verifier.py new file mode 100644 index 00000000..e4b69697 --- /dev/null +++ b/verifiers/solver_voting_count_verifier.py @@ -0,0 +1,149 @@ +from verifiers import * +from verifiers.solver_voting_verifier import Solver_Voting_Verifier + + +class Solver_Vote_Count_Verifier(Solver_Voting_Verifier): + """ + The Solver Count Verifier will verify if the amount of solutions is the same for all solvers after running multiple mutations + """ + + def __init__(self, solver: str, mutations_per_model: int, exclude_dict: dict, time_limit: float, seed: int, mm_prob: float): + self.name = "solver_vote_count_verifier" + self.type = 'sat' + + self.solvers = solver + + self.mutations_per_model = mutations_per_model + self.exclude_dict = exclude_dict + self.time_limit = time_limit + self.seed = random.Random().random() + self.mm_mutators = [xor_morph, and_morph, or_morph, implies_morph, not_morph, + linearize_constraint_morph, + flatten_morph, + only_numexpr_equality_morph, + normalized_numexpr_morph, + reify_rewrite_morph, + only_bv_reifies_morph, + only_positive_bv_morph, + flat2cnf_morph, + toplevel_list_morph, + decompose_in_tree_morph, + push_down_negation_morph, + simplify_boolean_morph, + canonical_comparison_morph, + aritmetic_comparison_morph, + semanticFusionCounting, + semanticFusionCountingMinus, + semanticFusionCountingwsum, + semanticFusionCounting, + semanticFusionCountingMinus, + semanticFusionCountingwsum] + self.gen_mutators = [type_aware_operator_replacement, type_aware_expression_replacement] + self.mutators = [] + self.original_model = None + self.nr_solve_checks = 0 + self.bug_cause = 'STARTMODEL' + self.nr_timed_out = 0 + self.last_mut = None + self.mm_prob = mm_prob + + def initialize_run(self) -> None: + if self.original_model == None: + with open(self.model_file, 'rb') as fpcl: + self.original_model = pickle.loads(fpcl.read()) + self.cons = self.original_model.constraints + assert (len(self.cons) > 0), f"{self.model_file} has no constraints" + self.cons = toplevel_list(self.cons) + assert len(self.solvers) > 1, f"More than 1 solver required, given solvers: {self.solvers}." + if 'gurobi' in [s.lower() for s in self.solvers]: # Because gurobi can't run solveAll without solution_limit + self.sol_lim = 10000 # Should this be hardcoded? + + # Optional: Check before applying the mutations. This should never fail... + + self.mutators = [copy.deepcopy( + self.cons)] # keep track of list of cons alternated with mutators that transformed it into the next list of cons. + + + def verify_model(self, is_bug_check=False) -> None | dict: + try: + model = cp.Model(self.cons) + + # if is_bug_check: + # max_search_time = 20 + # else: + # max_search_time = 40 + max_search_time = 40 + + time_limit = max(1, min(max_search_time, # TODO: change `max_search_time` back to 200 + self.time_limit - time.time())) # set the max time limit to the given time limit or to 1 if the self.time_limit-time.time() would be smaller then 1 + + # Get the actual solver results and their execution times. + # We do it this way because a solver might crash, meaning the other solver doesn't get a turn. + solvers_results = [] + solvers_times = [] + for s in self.solvers: + self.nr_solve_checks += 1 + if hasattr(self, 'sol_lim'): + solvers_results.append(model.solveAll(solver=s, solution_limit=self.sol_lim, time_limit=time_limit)) + solvers_times.append(model.status().runtime) + else: + solvers_results.append(model.solveAll(solver=s, time_limit=time_limit)) + solvers_times.append(model.status().runtime) + + nr_timed_out_solvers = sum([t > time_limit * 0.8 for t in solvers_times]) + if nr_timed_out_solvers > 0: + # timeout, skip + self.bug_cause = 'UNKNOWN' + self.nr_timed_out += nr_timed_out_solvers + if not is_bug_check: + print('T', end='', flush=True) + return None + elif all(s1 == s2 for i, s1 in enumerate(solvers_results) for j, s2 in enumerate(solvers_results) if i < j): + # has to be same + if not is_bug_check: + print('.', end='', flush=True) + return None + else: + solver_results_str = ", ".join( + f"{solver}: {result}" for solver, result in zip(self.solvers, solvers_results)) + if is_bug_check: + print('X', end='', flush=True) + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.failed_model, + originalmodel_file=self.model_file, + exception=f"Results of the solvers are not equal. Solver results: {solver_results_str}.", + constraints=self.cons, + mutators=self.mutators, + model=model, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + + except Exception as e: + if isinstance(e, (CPMpyException, NotImplementedError)): + # expected error message, ignore + return None + if is_bug_check: + print('E', end='', flush=True) + + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.internalcrash, + originalmodel_file=self.model_file, + exception=e, + stacktrace=traceback.format_exc(), + constraints=self.cons, + mutators=self.mutators, + model=model, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) diff --git a/verifiers/solver_voting_eq_verifier.py b/verifiers/solver_voting_eq_verifier.py new file mode 100644 index 00000000..a9e3a3c3 --- /dev/null +++ b/verifiers/solver_voting_eq_verifier.py @@ -0,0 +1,158 @@ +from verifiers import * +from verifiers.solver_voting_verifier import Solver_Voting_Verifier + + +class Solver_Vote_Eq_Verifier(Solver_Voting_Verifier): + """ + The Solver Equivalence Verifier will verify if the solutions are the same for all solvers after running multiple mutations + """ + + def __init__(self, solver: str, mutations_per_model: int, exclude_dict: dict, time_limit: float, seed: int, mm_prob: float): + self.name = "solver_vote_eq_verifier" + self.type = 'sat' + + self.solvers = solver + + self.mutations_per_model = mutations_per_model + self.exclude_dict = exclude_dict + self.time_limit = time_limit + self.seed = random.Random().random() + self.mm_mutators = [xor_morph, and_morph, or_morph, implies_morph, not_morph, + linearize_constraint_morph, + flatten_morph, + only_numexpr_equality_morph, + normalized_numexpr_morph, + reify_rewrite_morph, + only_bv_reifies_morph, + only_positive_bv_morph, + flat2cnf_morph, + toplevel_list_morph, + decompose_in_tree_morph, + push_down_negation_morph, + simplify_boolean_morph, + canonical_comparison_morph, + aritmetic_comparison_morph, + semanticFusionCounting, + semanticFusionCountingMinus, + semanticFusionCountingwsum, + semanticFusionCounting, + semanticFusionCountingMinus, + semanticFusionCountingwsum] + self.gen_mutators = [type_aware_operator_replacement, type_aware_expression_replacement] + self.mutators = [] + self.original_model = None + self.nr_solve_checks = 0 + self.bug_cause = 'STARTMODEL' + self.nr_timed_out = 0 + self.last_mut = None + self.mm_prob = mm_prob + + def initialize_run(self) -> None: + if self.original_model == None: + with open(self.model_file, 'rb') as fpcl: + self.original_model = pickle.loads(fpcl.read()) + self.cons = self.original_model.constraints + assert (len(self.cons) > 0), f"{self.model_file} has no constraints" + self.cons = toplevel_list(self.cons) + assert len(self.solvers) > 1, f"More than 1 solver required, given solvers: {self.solvers}." + if 'gurobi' in [s.lower() for s in self.solvers]: # Because gurobi can't run solveAll without solution_limit + self.sol_lim = 10000 # Should this be hardcoded? + + self.original_vars = get_variables(self.cons) # New auxiliary variables will be added so we need to do this here + + self.mutators = [copy.deepcopy( + self.cons)] # keep track of list of cons alternated with mutators that transformed it into the next list of cons. + + + def verify_model(self, is_bug_check=False) -> None | dict: + try: + model = cp.Model(self.cons) + + # if is_bug_check: + # max_search_time = 20 + # else: + # max_search_time = 40 + max_search_time = 40 + + time_limit = max(1, min(max_search_time, # TODO: change `max_search_time` back to 200 + self.time_limit - time.time())) # set the max time limit to the given time limit or to 1 if the self.time_limit-time.time() would be smaller then 1 + + # Get the actual solver results and their execution times. + # We do it this way because a solver might crash, meaning the other solver doesn't get a turn. + all_sols = [set() for i, s in enumerate(self.solvers)] + solvers_times = [] + for i, s in enumerate(self.solvers): + self.nr_solve_checks += 1 + if hasattr(self, 'sol_lim'): + res = model.solveAll(solver=s, time_limit=time_limit, display=lambda: all_sols[i].add( + tuple([v.value() for v in self.original_vars])), solution_limit=self.sol_lim) + solvers_times.append(model.status().runtime) + else: + model.solveAll(solver=s, time_limit=time_limit, display=lambda: all_sols[i].add( + tuple([v.value() for v in self.original_vars]))) + solvers_times.append(model.status().runtime) + + nr_timed_out_solvers = sum([t > time_limit * 0.8 for t in solvers_times]) + if nr_timed_out_solvers > 0: + # timeout, skip + self.bug_cause = 'UNKNOWN' + self.nr_timed_out += nr_timed_out_solvers + if not is_bug_check: + print('T', end='', flush=True) + return None + elif all(len(s1.symmetric_difference(s2)) == 0 for i, s1 in enumerate(all_sols) for j, s2 in enumerate(all_sols) if i < j) or (hasattr(self, 'sol_lim') and res == self.sol_lim): + # has to be same + if not is_bug_check: + print('.', end='', flush=True) + return None + else: + solver_results_str = "" + from itertools import combinations + for (i, s1), (j, s2) in combinations(enumerate(all_sols), 2): + if len(solver_results_str) > 0: + solver_results_str += "\n" + solver_name_1 = self.solvers[i] + solver_name_2 = self.solvers[j] + diff = s1.symmetric_difference(s2) + solver_results_str += f"{solver_name_1} vs {solver_name_2}: {len(diff)} differences" + if is_bug_check: + print('X', end='', flush=True) + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.failed_model, + originalmodel_file=self.model_file, + exception=f"Results of the solvers are not equal. Solver results: {solver_results_str}", + constraints=self.cons, + mutators=self.mutators, + model=model, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + + except Exception as e: + if isinstance(e, (CPMpyException, NotImplementedError)): + # expected error message, ignore + return None + if is_bug_check: + print('E', end='', flush=True) + + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.internalcrash, + originalmodel_file=self.model_file, + exception=e, + stacktrace=traceback.format_exc(), + constraints=self.cons, + mutators=self.mutators, + model=model, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) diff --git a/verifiers/solver_voting_sat_verifier.py b/verifiers/solver_voting_sat_verifier.py new file mode 100644 index 00000000..c92f2831 --- /dev/null +++ b/verifiers/solver_voting_sat_verifier.py @@ -0,0 +1,141 @@ +from verifiers import * +from verifiers.solver_voting_verifier import Solver_Voting_Verifier + + +class Solver_Vote_Sat_Verifier(Solver_Voting_Verifier): + """ + The Solver Satisfiability Verifier will verify if the satisfiability is the same for all solvers after running multiple mutations + """ + + def __init__(self, solver: str, mutations_per_model: int, exclude_dict: dict, time_limit: float, seed: int, mm_prob: float): + self.name = "solver_vote_sat_verifier" + self.type = 'sat' + + self.solvers = solver + + self.mutations_per_model = mutations_per_model + self.exclude_dict = exclude_dict + self.time_limit = time_limit + self.seed = random.Random().random() + self.mm_mutators = [xor_morph, and_morph, or_morph, implies_morph, not_morph, + linearize_constraint_morph, + flatten_morph, + only_numexpr_equality_morph, + normalized_numexpr_morph, + reify_rewrite_morph, + only_bv_reifies_morph, + only_positive_bv_morph, + flat2cnf_morph, + toplevel_list_morph, + decompose_in_tree_morph, + push_down_negation_morph, + simplify_boolean_morph, + canonical_comparison_morph, + aritmetic_comparison_morph, + semanticFusionCounting, + semanticFusionCountingMinus, + semanticFusionCountingwsum, + semanticFusionCounting, + semanticFusionCountingMinus, + semanticFusionCountingwsum] + self.gen_mutators = [type_aware_operator_replacement, type_aware_expression_replacement] + self.mutators = [] + self.original_model = None + self.nr_solve_checks = 0 + self.bug_cause = 'STARTMODEL' + self.nr_timed_out = 0 + self.last_mut = None + self.mm_prob = mm_prob + + def initialize_run(self) -> None: + if self.original_model == None: + with open(self.model_file, 'rb') as fpcl: + self.original_model = pickle.loads(fpcl.read()) + self.cons = self.original_model.constraints + assert (len(self.cons) > 0), f"{self.model_file} has no constraints" + self.cons = toplevel_list(self.cons) + assert len(self.solvers) > 1, f"More than 1 solver required, given solvers: {self.solvers}." + + # No other preparation necessary + # Optional: Check before applying the mutations. This should never fail... + + self.mutators = [copy.deepcopy( + self.cons)] # keep track of list of cons alternated with mutators that transformed it into the next list of cons. + + def verify_model(self, is_bug_check=False) -> None | dict: + try: + model = cp.Model(self.cons) + + if is_bug_check: + max_search_time = 10 + else: + max_search_time = 20 + + time_limit = max(1, min(max_search_time, # TODO: change `max_search_time` back to 200 + self.time_limit - time.time())) # set the max time limit to the given time limit or to 1 if the self.time_limit-time.time() would be smaller then 1 + + # Get the actual solver results and their execution times. + # We do it this way because a solver might crash, meaning the other solver doesn't get a turn. + solvers_results = [] + solvers_times = [] + for s in self.solvers: + self.nr_solve_checks += 1 + solvers_results.append(model.solve(solver=s, time_limit=time_limit)) + solvers_times.append(model.status().runtime) + + nr_timed_out_solvers = sum([t > time_limit * 0.8 for t in solvers_times]) + if nr_timed_out_solvers > 0: + # timeout, skip + self.bug_cause = 'UNKNOWN' + self.nr_timed_out += nr_timed_out_solvers + if not is_bug_check: + print('T', end='', flush=True) + return None + elif all(s1 == s2 for i, s1 in enumerate(solvers_results) for j, s2 in enumerate(solvers_results) if i < j): + # has to be same + if not is_bug_check: + print('.', end='', flush=True) + return None + else: + solver_results_str = ", ".join( + f"{solver}: {result}" for solver, result in zip(self.solvers, solvers_results)) + if is_bug_check: + print('X', end='', flush=True) + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.failed_model, + originalmodel_file=self.model_file, + exception=f"Results of the solvers are not equal. Solver results: {solver_results_str}.", + constraints=self.cons, + mutators=self.mutators, + model=model, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + + except Exception as e: + if isinstance(e, (CPMpyException, NotImplementedError)): + # expected error message, ignore + return None + if is_bug_check: + print('E', end='', flush=True) + + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.internalcrash, + originalmodel_file=self.model_file, + exception=e, + stacktrace=traceback.format_exc(), + constraints=self.cons, + mutators=self.mutators, + model=model, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) diff --git a/verifiers/solver_voting_sol_verifier.py b/verifiers/solver_voting_sol_verifier.py new file mode 100644 index 00000000..4eb245cf --- /dev/null +++ b/verifiers/solver_voting_sol_verifier.py @@ -0,0 +1,147 @@ +from verifiers import * +from verifiers.solver_voting_verifier import Solver_Voting_Verifier + + +class Solver_Vote_Sol_Verifier(Solver_Voting_Verifier): + """ + The Solver Sol Verifier will verify if a single solution is also in all other solvers after running multiple mutations + """ + + def __init__(self, solver: str, mutations_per_model: int, exclude_dict: dict, time_limit: float, seed: int, mm_prob: float): + self.name = "solver_vote_sol_verifier" + self.type = 'sat' + + self.solvers = solver + + self.mutations_per_model = mutations_per_model + self.exclude_dict = exclude_dict + self.time_limit = time_limit + self.seed = random.Random().random() + self.mm_mutators = [xor_morph, and_morph, or_morph, implies_morph, not_morph, + linearize_constraint_morph, + flatten_morph, + only_numexpr_equality_morph, + normalized_numexpr_morph, + reify_rewrite_morph, + only_bv_reifies_morph, + only_positive_bv_morph, + flat2cnf_morph, + toplevel_list_morph, + decompose_in_tree_morph, + push_down_negation_morph, + simplify_boolean_morph, + canonical_comparison_morph, + aritmetic_comparison_morph, + semanticFusionCounting, + semanticFusionCountingMinus, + semanticFusionCountingwsum, + semanticFusionCounting, + semanticFusionCountingMinus, + semanticFusionCountingwsum] + self.gen_mutators = [type_aware_operator_replacement, type_aware_expression_replacement] + self.mutators = [] + self.original_model = None + self.nr_solve_checks = 0 + self.bug_cause = 'STARTMODEL' + self.nr_timed_out = 0 + self.last_mut = None + self.mm_prob = mm_prob + + def initialize_run(self) -> None: + if self.original_model == None: + with open(self.model_file, 'rb') as fpcl: + self.original_model = pickle.loads(fpcl.read()) + self.cons = self.original_model.constraints + assert (len(self.cons) > 0), f"{self.model_file} has no constraints" + self.cons = toplevel_list(self.cons) + assert len(self.solvers) > 1, f"More than 1 solver required, given solvers: {self.solvers}." + + self.og_vars = get_variables(self.cons) + + self.mutators = [copy.deepcopy( + self.cons)] # keep track of list of cons alternated with mutators that transformed it into the next list of cons. + + def verify_model(self, is_bug_check=False) -> None | dict: + try: + model = cp.Model(self.cons) + + # if is_bug_check: + # max_search_time = 20 + # else: + # max_search_time = 40 + max_search_time = 40 + + time_limit = max(1, min(max_search_time, # TODO: change `max_search_time` back to 200 + self.time_limit - time.time())) # set the max time limit to the given time limit or to 1 if the self.time_limit-time.time() would be smaller then 1 + + # Get the actual solver results and their execution times. + # We do it this way because a solver might crash, meaning the other solver doesn't get a turn. + rand_solver = random.choice(self.solvers) + model.solve(solver=rand_solver, time_limit=time_limit) + sol = [var == var.value() for var in self.og_vars if var.value() is not None] + model += sol + + solvers_results = [] + solvers_times = [] + for s in self.solvers: + self.nr_solve_checks += 1 + solvers_results.append(model.solve(solver=s, time_limit=time_limit)) + solvers_times.append(model.status().runtime) + + nr_timed_out_solvers = sum([t > time_limit * 0.8 for t in solvers_times]) + if nr_timed_out_solvers > 0: + # timeout, skip + self.bug_cause = 'UNKNOWN' + self.nr_timed_out += nr_timed_out_solvers + if not is_bug_check: + print('T', end='', flush=True) + return None + elif all(s1 == s2 for i, s1 in enumerate(solvers_results) for j, s2 in enumerate(solvers_results) if i < j): + # has to be same + if not is_bug_check: + print('.', end='', flush=True) + return None + else: + solver_results_str = ", ".join( + f"{solver}: {result}" for solver, result in zip(self.solvers, solvers_results)) + if is_bug_check: + print('X', end='', flush=True) + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.failed_model, + originalmodel_file=self.model_file, + exception=f"Results of the solvers are not equal. Solver results: {solver_results_str}.", + constraints=self.cons, + mutators=self.mutators, + model=model, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + + except Exception as e: + if isinstance(e, (CPMpyException, NotImplementedError)): + # expected error message, ignore + return None + if is_bug_check: + print('E', end='', flush=True) + + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.internalcrash, + originalmodel_file=self.model_file, + exception=e, + stacktrace=traceback.format_exc(), + constraints=self.cons, + mutators=self.mutators, + model=model, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) diff --git a/verifiers/solver_voting_verifier.py b/verifiers/solver_voting_verifier.py new file mode 100644 index 00000000..612f10dd --- /dev/null +++ b/verifiers/solver_voting_verifier.py @@ -0,0 +1,397 @@ +import random + +from verifiers import * + + +class Solver_Voting_Verifier(Verifier): + """ + The base class containing the base functions for each verifier. + """ + + def __init__(self, solver: str, mutations_per_model: int, exclude_dict: dict, time_limit: float, seed: int, mm_prob: float): + self.solvers = solver + + self.mutations_per_model = mutations_per_model + self.exclude_dict = exclude_dict + self.time_limit = time_limit + self.seed = random.Random().random() + self.mm_mutators = [xor_morph, and_morph, or_morph, implies_morph, not_morph, + linearize_constraint_morph, + flatten_morph, + only_numexpr_equality_morph, + normalized_numexpr_morph, + reify_rewrite_morph, + only_bv_reifies_morph, + only_positive_bv_morph, + flat2cnf_morph, + toplevel_list_morph, + decompose_in_tree_morph, + push_down_negation_morph, + simplify_boolean_morph, + canonical_comparison_morph, + aritmetic_comparison_morph, + semanticFusionCounting, + semanticFusionCountingMinus, + semanticFusionCountingwsum, + semanticFusionCounting, + semanticFusionCountingMinus, + semanticFusionCountingwsum] + self.gen_mutators = [type_aware_operator_replacement, type_aware_expression_replacement] + self.mutators = [] + self.original_model = None + self.nr_solve_checks = 0 + self.bug_cause = 'STARTMODEL' + self.nr_timed_out = 0 + self.last_mut = None + self.mm_prob = mm_prob + + def generate_mutations(self) -> None | dict: + """ + Will generate random mutations based on mutations_per_model for the model + """ + for i in range(self.mutations_per_model): + # # choose a mutation (not in exclude_dict) + # valid_mutators = list(set(self.mm_mutators).union(set(self.gen_mutators)) - set( + # self.exclude_dict[self.model_file])) if self.model_file in self.exclude_dict else list( + # set(self.mm_mutators).union(set(self.gen_mutators))) + if random.random() <= self.mm_prob: # mm_prob probability to choose metamorphic mutation + mutator_list = self.mm_mutators + else: # 1-mm_prob to choose generation-based mutation + mutator_list = self.gen_mutators + + # valid = [m for m in mutator_list if m in valid_mutators] + # if valid: + # m = random.choice(valid) + # else: + # continue + m = random.choice(mutator_list) + + self.mutators += [self.seed] + # an error can occur in the transformations, so even before the solve call. + # log function and arguments in that case + self.mutators += [m] + try: + if m in self.gen_mutators: + self.bug_cause = 'during GEN' + self.cons = m(self.cons) # apply a generative mutation and REPLACE constraints + self.bug_cause = 'GEN' + else: + self.bug_cause = 'during MM' + self.cons += m(self.cons) # apply a metamorphic mutation and add to constraints + self.bug_cause = 'MM' + self.mutators += [copy.deepcopy(self.cons)] + except MetamorphicError as exc: + # add to exclude_dict, to avoid running into the same error + if self.model_file in self.exclude_dict: + self.exclude_dict[self.model_file] += [m] + else: + self.exclude_dict[self.model_file] = [m] + function, argument, e = exc.args + if isinstance(e, CPMpyException): + # expected behavior if we throw a cpmpy exception, do not log + return None + elif function == semanticFusion: + return None + # don't log semanticfusion crash + + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.internalfunctioncrash, + originalmodel_file=self.model_file, + exception=e, + function=function, + argument=argument, + stacktrace=traceback.format_exc(), + mutators=self.mutators, + constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + return None + + def initialize_run(self) -> None: + """ + Abstract function that gets executed before generating the mutation, + This function is ued for getting the right data from the model. + Each verifier needs to implement this function + """ + raise NotImplementedError(f"method 'initialize_run' is not implemented for class {type(self)}") + + def verify_model(self, is_bug_check=False) -> dict: + """ + Abstract function that will solve the newly created model with the mutations. + It will check if the test succeeded or not. + Each verifier needs to implement this function + """ + raise NotImplementedError(f"method 'verify_model' is not implemented for class {type(self)}") + + def run(self, model_file: str) -> dict | None: + """ + This function will run a single tests on the given model + """ + try: + random.seed(self.seed) + self.model_file = model_file + self.initialize_run() + gen_mutations_error = self.generate_mutations() + + # check if no error occured while generation the mutations + if gen_mutations_error == None: + # FOLLOWING 5 LINES CHANGED! + verify_model_error = self.verify_model() + if verify_model_error == None: + return None + else: + return self.find_error_rerun(verify_model_error) + else: + return self.find_error_rerun(gen_mutations_error) + except AssertionError as e: + print("A", end='', flush=True) + error_type = Fuzz_Test_ErrorTypes.crashed_model + if "is not sat" in str(e): + error_type = Fuzz_Test_ErrorTypes.unsat_model + elif "has no constraints" in str(e): + error_type = Fuzz_Test_ErrorTypes.no_constraints_model + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=error_type, + originalmodel_file=self.model_file, + exception=e, + stacktrace=traceback.format_exc(), + constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + + except Exception as e: + print('C', end='', flush=True) + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.crashed_model, + originalmodel_file=self.model_file, + exception=e, + stacktrace=traceback.format_exc(), + constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + mutators=self.mutators, + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + + def find_error_rerun(self, error_dict) -> dict: + try: + random.seed(self.seed) + error_type = error_dict['type'] + self.initialize_run() # initialize empty (self.)model, cons, mutators + + # This should always be the case + if error_type in [Fuzz_Test_ErrorTypes.internalcrash, Fuzz_Test_ErrorTypes.failed_model]: # Error type 'E', often during model.solve() or solveAll or type 'X' + return self.bug_search_run_and_verify_model() + elif error_type == Fuzz_Test_ErrorTypes.internalfunctioncrash: + mutations = error_dict['mutators'][2::3] + return self.bug_search_run_and_verify_model(nr_mutations=len(mutations)) + + except AssertionError as e: + print("A", end='', flush=True) + type = Fuzz_Test_ErrorTypes.crashed_model + if "is not sat" in str(e): + type = Fuzz_Test_ErrorTypes.unsat_model + elif "has no constraints" in str(e): + type = Fuzz_Test_ErrorTypes.no_constraints_model + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=type, + originalmodel_file=self.model_file, + exception=e, + stacktrace=traceback.format_exc(), + constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + + except Exception as e: + print('C', end='', flush=True) + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.crashed_model, + originalmodel_file=self.model_file, + exception=e, + stacktrace=traceback.format_exc(), + constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + + def bug_search_run_and_verify_model(self, nr_mutations=None) -> dict: + if nr_mutations is not None: + self.mutations_per_model = nr_mutations + for _ in range(self.mutations_per_model): + last_bug_cause = self.bug_cause + + # # Generate the type of mutation that will happen + # valid_mutators = list(set(self.mm_mutators).union(set(self.gen_mutators)) - set( + # self.exclude_dict[self.model_file])) if self.model_file in self.exclude_dict else list( + # set(self.mm_mutators).union(set(self.gen_mutators))) + if random.random() <= self.mm_prob: # mm_prob probability to choose metamorphic mutation + mutator_list = self.mm_mutators + new_mut_type = 'MM' + else: # 1-mm_prob to choose generation-based mutation + mutator_list = self.gen_mutators + new_mut_type = 'GEN' + + # valid = [m for m in mutator_list if m in valid_mutators] + # if valid: + # m = random.choice(valid) + # else: + # continue + m = random.choice(mutator_list) + + # Check whether verify_model returns an error before the new mutation, because the cause is then at the old mutation + if new_mut_type != last_bug_cause: + verify_model_error = self.verify_model(is_bug_check=True) + if verify_model_error is not None: + return verify_model_error + + # Then, apply the new mutation and check whether it gives an error + gen_mut_error = self.apply_single_mutation(m) + if gen_mut_error is not None: + return gen_mut_error + + # Finally, check the model at the end. This SHOULD give an error + verify_model_error = self.verify_model(is_bug_check=True) + if verify_model_error is not None: + return verify_model_error + else: + print('_', end='', flush=True) + + def apply_single_mutation(self, m) -> dict | None: + """ + Will generate one random mutation and apply it to the model + """ + self.mutators += [self.seed] + # an error can occur in the transformations, so even before the solve call. + # log function and arguments in that case + self.mutators += [m] + try: + if m in self.gen_mutators: + self.bug_cause = f'during GEN, after {self.bug_cause}' + self.cons = m(self.cons) # apply a generative mutation and REPLACE constraints + self.bug_cause = 'GEN' + else: + self.bug_cause = f'during MM, after {self.bug_cause}' + self.cons += m(self.cons) # apply a metamorphic mutation and add to constraints + self.bug_cause = 'MM' + self.mutators += [copy.deepcopy(self.cons)] + except MetamorphicError as exc: + # add to exclude_dict, to avoid running into the same error + if self.model_file in self.exclude_dict: + self.exclude_dict[self.model_file] += [m] + else: + self.exclude_dict[self.model_file] = [m] + function, argument, e = exc.args + if isinstance(e, CPMpyException): + # expected behavior if we throw a cpmpy exception, do not log + return None + elif function == semanticFusion: + return None + # don't log semanticfusion crash + + print('I', end='', flush=True) + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.internalfunctioncrash, + originalmodel_file=self.model_file, + exception=e, + function=function, + argument=argument, + stacktrace=traceback.format_exc(), + mutators=self.mutators, + constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + return None + + def rerun(self, error: dict) -> dict: + """ + This function will rerun a previous failed test + """ + try: + if 'seed' in error: + run_seed = error['seed'] + random.seed(run_seed) + else: + random.seed(self.seed) + self.model_file = error["originalmodel_file"] + self.original_model = error["originalmodel"] + self.exclude_dict = {} + self.initialize_run() + gen_mutations_error = self.generate_mutations() + + # check if no error occured while generation the mutations + if gen_mutations_error == None: + return self.verify_model() + else: + return gen_mutations_error + # self.og_cons = error["constraints"] + # return self.verify_model() + + except AssertionError as e: + print("A", end='', flush=True) + type = Fuzz_Test_ErrorTypes.crashed_model + if "is not sat" in str(e): + type = Fuzz_Test_ErrorTypes.unsat_model + elif "has no constraints" in str(e): + type = Fuzz_Test_ErrorTypes.no_constraints_model + return dict(type=type, + originalmodel_file=self.model_file, + exception=e, + stacktrace=traceback.format_exc(), + constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model + ) + + except Exception as e: + print('C', end='', flush=True) + return dict(type=Fuzz_Test_ErrorTypes.crashed_model, + originalmodel_file=self.model_file, + exception=e, + stacktrace=traceback.format_exc(), + constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model + ) + + def getType(self) -> str: + """This function is used for getting the type of the problem the verifier verifies""" + return self.type + + def getName(self) -> str: + """This function is used for getting the name of the verifier""" + return self.name diff --git a/verifiers/strengthening_weakening_verifier.py b/verifiers/strengthening_weakening_verifier.py new file mode 100644 index 00000000..7a427175 --- /dev/null +++ b/verifiers/strengthening_weakening_verifier.py @@ -0,0 +1,524 @@ +import random + +from verifiers import * + +class Strengthening_Weakening_Verifier(Verifier): + """ + The Strengthening Weakening Verifier will verify if the amount of solutions is the same for all solvers after running multiple mutations + """ + + def __init__(self, solver: str, mutations_per_model: int, exclude_dict: dict, time_limit: float, seed: int, mm_prob: float): + self.name = "strengthening_weakening_verifier" + self.type = 'sat' + + self.solvers = solver + + self.mutations_per_model = mutations_per_model + self.exclude_dict = exclude_dict + self.time_limit = time_limit + self.seed = random.Random().random() + self.mm_mutators = [xor_morph, and_morph, or_morph, implies_morph, not_morph, + linearize_constraint_morph, + flatten_morph, + only_numexpr_equality_morph, + normalized_numexpr_morph, + reify_rewrite_morph, + only_bv_reifies_morph, + only_positive_bv_morph, + flat2cnf_morph, + toplevel_list_morph, + decompose_in_tree_morph, + push_down_negation_morph, + simplify_boolean_morph, + canonical_comparison_morph, + aritmetic_comparison_morph, + semanticFusionCounting, + semanticFusionCountingMinus, + semanticFusionCountingwsum, + semanticFusionCounting, + semanticFusionCountingMinus, + semanticFusionCountingwsum] + self.gen_mutators = [type_aware_operator_replacement, type_aware_expression_replacement] + self.str_wkn_mutators = [strengthening_weakening_mutator, change_domain_mutator] + self.mutators = [] + self.original_model = None + self.nr_solve_checks = 0 + self.bug_cause = 'STARTMODEL' + self.nr_timed_out = 0 + self.last_mut = None + self.mm_prob = mm_prob + + def initialize_run(self) -> None: + if self.original_model == None: + with open(self.model_file, 'rb') as fpcl: + self.original_model = pickle.loads(fpcl.read()) + self.cons = self.original_model.constraints + assert (len(self.cons) > 0), f"{self.model_file} has no constraints" + self.cons = toplevel_list(self.cons) + assert len(self.solvers) > 1, f"More than 1 solver required, given solvers: {self.solvers}." + if 'gurobi' in [s.lower() for s in self.solvers]: # Because gurobi can't run solveAll without solution_limit + self.sol_lim = 10000 # Should this be hardcoded? + + # Optional: Check before applying the mutations. This should never fail... + + self.mutators = [copy.deepcopy( + self.cons)] # keep track of list of cons alternated with mutators that transformed it into the next list of cons. + + def generate_mutations(self) -> None | dict: + """ + Will generate random mutations based on mutations_per_model for the model + """ + for i in range(self.mutations_per_model): + + # choose a mutator. 33% of the time, this will be a strengthening/weakening mutation. + # choose a mutation (not in exclude_dict) + # valid_mutators = list(set(self.mm_mutators).union(set(self.gen_mutators)).union(set(self.str_wkn_mutators)) - set( + # self.exclude_dict[self.model_file])) if self.model_file in self.exclude_dict else list( + # set(self.mm_mutators).union(set(self.gen_mutators)).union(set(self.str_wkn_mutators))) + rand = random.random() + if rand <= 1/3 * (1 - self.mm_prob): + mutator_list = self.str_wkn_mutators + elif rand - (1/3 * (1 - self.mm_prob)) <= 2/3 * self.mm_prob: # ~~ remaining mm_prob + mutator_list = self.mm_mutators + else: + mutator_list = self.gen_mutators + + # valid = [m for m in mutator_list if m in valid_mutators] + # if valid: + # m = random.choice(valid) + # else: + # continue # No valid mutator? => go to next mutation + m = random.choice(mutator_list) + + self.mutators += [self.seed] + # an error can occur in the transformations, so even before the solve call. + # log function and arguments in that case + self.mutators += [m] + try: + if m in self.gen_mutators: + self.bug_cause = 'during GEN' + self.cons = m(self.cons) # apply a generative (non-metamorphic) mutation and REPLACE constraints + self.bug_cause = 'GEN' + elif m in self.str_wkn_mutators: + s = random.choice(self.solvers) + self.nr_solve_checks += 1 + sat = cp.Model(self.cons).solve(solver=s) + if sat: + self.bug_cause = 'during STR' + self.cons = m(self.cons, strengthen=True) + self.bug_cause = 'STR' + else: + self.bug_cause = 'during WKN' + self.cons = m(self.cons, strengthen=False) + self.bug_cause = 'WKN' + else: + self.bug_cause = 'during MM' + self.cons += m(self.cons) + self.bug_cause = 'MM' + if not m == self.mutators[-1]: + self.mutators[-1] = m + self.mutators += [copy.deepcopy(self.cons)] + + except MetamorphicError as exc: + # add to exclude_dict, to avoid running into the same error + if self.model_file in self.exclude_dict: + self.exclude_dict[self.model_file] += [m] + else: + self.exclude_dict[self.model_file] = [m] + function, argument, e = exc.args + if isinstance(e, CPMpyException): + # expected behavior if we throw a cpmpy exception, do not log + return None + elif function == semanticFusion: + return None + # don't log semanticfusion crash + + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.internalfunctioncrash, + originalmodel_file=self.model_file, + exception=e, + function=function, + argument=argument, + stacktrace=traceback.format_exc(), + mutators=self.mutators, + constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + return None + + def verify_model(self, is_bug_check=False) -> None | dict: + try: + model = cp.Model(self.cons) + + # if is_bug_check: + # max_search_time = 20 + # else: + # max_search_time = 40 + max_search_time = 40 + + time_limit = max(1, min(max_search_time, # TODO: change `max_search_time` back to 200 + self.time_limit - time.time())) # set the max time limit to the given time limit or to 1 if the self.time_limit-time.time() would be smaller then 1 + + # Get the actual solver results and their execution times. + # We do it this way because a solver might crash, meaning the other solver doesn't get a turn. + solvers_results = [] + solvers_times = [] + for s in self.solvers: + # print("I add to nrsolvechecks") + self.nr_solve_checks += 1 + if hasattr(self, 'sol_lim'): + solvers_results.append(model.solveAll(solver=s, solution_limit=self.sol_lim, time_limit=time_limit)) + solvers_times.append(model.status().runtime) + else: + solvers_results.append(model.solveAll(solver=s, time_limit=time_limit)) + solvers_times.append(model.status().runtime) + + nr_timed_out_solvers = sum([t > time_limit * 0.8 for t in solvers_times]) + if nr_timed_out_solvers > 0: + # timeout, skip + self.bug_cause = 'UNKNOWN' + self.nr_timed_out += nr_timed_out_solvers + if not is_bug_check: + print('T', end='', flush=True) + return None + elif all(s1 == s2 for i, s1 in enumerate(solvers_results) for j, s2 in enumerate(solvers_results) if i < j): + # has to be same + if not is_bug_check: + print('.', end='', flush=True) + return None + else: + solver_results_str = ", ".join( + f"{solver}: {result}" for solver, result in zip(self.solvers, solvers_results)) + if is_bug_check: + print('X', end='', flush=True) + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.failed_model, + originalmodel_file=self.model_file, + exception=f"Results of the solvers are not equal. Solver results: {solver_results_str}.", + constraints=self.cons, + mutators=self.mutators, + model=model, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + + except Exception as e: + if isinstance(e, (CPMpyException, NotImplementedError)): + # expected error message, ignore + return None + if is_bug_check: + print('E', end='', flush=True) + + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.internalcrash, + originalmodel_file=self.model_file, + exception=e, + stacktrace=traceback.format_exc(), + constraints=self.cons, + mutators=self.mutators, + model=model, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + + + def run(self, model_file: str) -> dict | None: + """ + This function will run a single tests on the given model + """ + try: + random.seed(self.seed) + self.model_file = model_file + self.initialize_run() + gen_mutations_error = self.generate_mutations() + + # check if no error occured while generation the mutations + if gen_mutations_error == None: + # FOLLOWING 5 LINES CHANGED! + verify_model_error = self.verify_model() + if verify_model_error == None: + return None + else: + return self.find_error_rerun(verify_model_error) + else: + return self.find_error_rerun(gen_mutations_error) + except AssertionError as e: + print("A", end='', flush=True) + error_type = Fuzz_Test_ErrorTypes.crashed_model + if "is not sat" in str(e): + error_type = Fuzz_Test_ErrorTypes.unsat_model + elif "has no constraints" in str(e): + error_type = Fuzz_Test_ErrorTypes.no_constraints_model + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=error_type, + originalmodel_file=self.model_file, + exception=e, + stacktrace=traceback.format_exc(), + constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + + except Exception as e: + print('C', end='', flush=True) + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.crashed_model, + originalmodel_file=self.model_file, + exception=e, + stacktrace=traceback.format_exc(), + constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + mutators=self.mutators, + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + + def find_error_rerun(self, error_dict) -> dict: + try: + # print("WE ARE NOW RUNNING A FIND_ERROR_RERUN!") + random.seed(self.seed) + error_type = error_dict['type'] + self.initialize_run() # initialize empty (self.)model, cons, mutators + + # This should always be the case + if error_type in [Fuzz_Test_ErrorTypes.internalcrash, Fuzz_Test_ErrorTypes.failed_model]: # Error type 'E', often during model.solve() or solveAll or type 'X' + return self.bug_search_run_and_verify_model() + elif error_type == Fuzz_Test_ErrorTypes.internalfunctioncrash: + mutations = error_dict['mutators'][2::3] + return self.bug_search_run_and_verify_model(nr_mutations=len(mutations)) + + except AssertionError as e: + print("A", end='', flush=True) + type = Fuzz_Test_ErrorTypes.crashed_model + if "is not sat" in str(e): + type = Fuzz_Test_ErrorTypes.unsat_model + elif "has no constraints" in str(e): + type = Fuzz_Test_ErrorTypes.no_constraints_model + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=type, + originalmodel_file=self.model_file, + exception=e, + stacktrace=traceback.format_exc(), + constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + + except Exception as e: + print('C', end='', flush=True) + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.crashed_model, + originalmodel_file=self.model_file, + exception=e, + stacktrace=traceback.format_exc(), + constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + + def bug_search_run_and_verify_model(self, nr_mutations=None) -> dict: + if nr_mutations is not None: + self.mutations_per_model = nr_mutations + for _ in range(self.mutations_per_model): + last_bug_cause = self.bug_cause + + # # choose a mutator. 33% of the time, this will be a strengthening/weakening mutation. + # # choose a mutation (not in exclude_dict) + # valid_mutators = list( + # set(self.mm_mutators).union(set(self.gen_mutators)).union({strengthening_weakening_mutator}) - set( + # self.exclude_dict[self.model_file])) if self.model_file in self.exclude_dict else list( + # set(self.mm_mutators).union(set(self.gen_mutators)).union(self.str_wkn_mutators)) + rand = random.random() + if rand <= 1 / 3 * (1 - self.mm_prob): + mutator_list = self.str_wkn_mutators + new_mut_type = 'STRWK' + elif rand - (1 / 3 * (1 - self.mm_prob)) <= 2 / 3 * self.mm_prob: # ~~ remaining mm_prob + mutator_list = self.mm_mutators + new_mut_type = 'MM' + else: + mutator_list = self.gen_mutators + new_mut_type = 'GEN' + + # valid = [m for m in mutator_list if m in valid_mutators] + # if valid: + # m = random.choice(valid) + # else: + # continue # No valid mutator? => go to next mutation + m = random.choice(mutator_list) + + # Check whether verify_model returns an error before the new mutation, because the cause is then at the old mutation + if new_mut_type != last_bug_cause: + verify_model_error = self.verify_model(is_bug_check=True) + if verify_model_error is not None: + return verify_model_error + + # Then, apply the new mutation and check whether it gives an error + gen_mut_error = self.apply_single_mutation(m) + if gen_mut_error is not None: + return gen_mut_error + + # Finally, check the model at the end. This SHOULD give an error + verify_model_error = self.verify_model(is_bug_check=True) + if verify_model_error is not None: + return verify_model_error + else: + print('_', end='', flush=True) + + def apply_single_mutation(self, m) -> dict | None: + """ + Will generate one random mutation and apply it to the model + """ + self.mutators += [self.seed] + # an error can occur in the transformations, so even before the solve call. + # log function and arguments in that case + self.mutators += [m] + try: + if m in self.gen_mutators: + self.bug_cause = 'during GEN' + self.cons = m(self.cons) # apply a generative (non-metamorphic) mutation and REPLACE constraints + self.bug_cause = 'GEN' + elif m in self.str_wkn_mutators: + s = random.choice(self.solvers) + self.nr_solve_checks += 1 + sat = cp.Model(self.cons).solve(solver=s) + if sat: + self.bug_cause = 'during STR' + self.cons = m(self.cons, strengthen=True) + self.bug_cause = 'STR' + else: + self.bug_cause = 'during WKN' + self.cons = m(self.cons, strengthen=False) + self.bug_cause = 'WKN' + else: + self.bug_cause = 'during MM' + self.cons += m(self.cons) # apply a metamorphic mutation and add to constraints + self.bug_cause = 'MM' + if not m == self.mutators[-1]: + self.mutators[-1] = m + # print(f"Mutator in bug_find is {self.mutators[-1]}.") + self.mutators += [copy.deepcopy(self.cons)] + except MetamorphicError as exc: + # add to exclude_dict, to avoid running into the same error + if self.model_file in self.exclude_dict: + self.exclude_dict[self.model_file] += [m] + else: + self.exclude_dict[self.model_file] = [m] + function, argument, e = exc.args + if isinstance(e, CPMpyException): + # expected behavior if we throw a cpmpy exception, do not log + return None + elif function == semanticFusion: + return None + # don't log semanticfusion crash + + print('I', end='', flush=True) + return dict(seed=self.seed, + mm_prob=self.mm_prob, + type=Fuzz_Test_ErrorTypes.internalfunctioncrash, + originalmodel_file=self.model_file, + exception=e, + function=function, + argument=argument, + stacktrace=traceback.format_exc(), + mutators=self.mutators, + constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model, + nr_solve_checks=self.nr_solve_checks, + caused_by=self.bug_cause, + nr_timed_out=self.nr_timed_out + ) + return None + + def rerun(self, error: dict) -> dict: + """ + This function will rerun a previous failed test + """ + try: + if 'seed' in error: + run_seed = error['seed'] + random.seed(run_seed) + else: + random.seed(self.seed) + self.model_file = error["originalmodel_file"] + self.original_model = error["originalmodel"] + self.exclude_dict = {} + self.initialize_run() + gen_mutations_error = self.generate_mutations() + + # check if no error occured while generation the mutations + if gen_mutations_error == None: + # FOLLOWING 5 LINES CHANGED! + verify_model_error = self.verify_model() + if verify_model_error == None: + return None + else: + return self.find_error_rerun(verify_model_error) + else: + return gen_mutations_error # This error requires no rerun + # self.og_cons = error["constraints"] + # return self.verify_model() + + except AssertionError as e: + print("A", end='', flush=True) + type = Fuzz_Test_ErrorTypes.crashed_model + if "is not sat" in str(e): + type = Fuzz_Test_ErrorTypes.unsat_model + elif "has no constraints" in str(e): + type = Fuzz_Test_ErrorTypes.no_constraints_model + return dict(type=type, + originalmodel_file=self.model_file, + exception=e, + stacktrace=traceback.format_exc(), + constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model + ) + + except Exception as e: + print('C', end='', flush=True) + return dict(type=Fuzz_Test_ErrorTypes.crashed_model, + originalmodel_file=self.model_file, + exception=e, + stacktrace=traceback.format_exc(), + constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], + originalmodel=self.original_model + ) \ No newline at end of file diff --git a/verifiers/verifier.py b/verifiers/verifier.py index e729dd1b..0a3d5678 100644 --- a/verifiers/verifier.py +++ b/verifiers/verifier.py @@ -16,31 +16,32 @@ def __init__(self, name: str, type: str, solver: str, mutations_per_model: int, self.time_limit = time_limit self.seed = seed self.mm_mutators = [xor_morph, and_morph, or_morph, implies_morph, not_morph, - linearize_constraint_morph, - flatten_morph, - only_numexpr_equality_morph, - normalized_numexpr_morph, - reify_rewrite_morph, - only_bv_reifies_morph, - only_positive_bv_morph, - flat2cnf_morph, - toplevel_list_morph, - decompose_in_tree_morph, - push_down_negation_morph, - simplify_boolean_morph, - canonical_comparison_morph, - aritmetic_comparison_morph, - semanticFusionCounting, - semanticFusionCountingMinus, - semanticFusionCountingwsum, - semanticFusionCounting, - semanticFusionCountingMinus, - semanticFusionCountingwsum] + linearize_constraint_morph, + flatten_morph, + only_numexpr_equality_morph, + normalized_numexpr_morph, + reify_rewrite_morph, + only_bv_reifies_morph, + only_positive_bv_morph, + flat2cnf_morph, + toplevel_list_morph, + decompose_in_tree_morph, + push_down_negation_morph, + simplify_boolean_morph, + canonical_comparison_morph, + aritmetic_comparison_morph, + semanticFusionCounting, + semanticFusionCountingMinus, + semanticFusionCountingwsum, + semanticFusionCounting, + semanticFusionCountingMinus, + semanticFusionCountingwsum, + type_aware_operator_replacement] self.mutators = [] self.original_model = None - def generate_mutations(self) -> None: + def generate_mutations(self) -> dict | None: """ Will generate random mutations based on mutations_per_model for the model """ @@ -56,7 +57,10 @@ def generate_mutations(self) -> None: # log function and arguments in that case self.mutators += [m] try: - self.cons += m(self.cons) # apply a metamorphic mutation + if m in {type_aware_operator_replacement, type_aware_expression_replacement, strengthening_weakening_mutator}: + self.cons = m(self.cons) # apply an operator change and REPLACE constraints + else: + self.cons += m(self.cons) # apply a metamorphic mutation and add to constraints self.mutators += [copy.deepcopy(self.cons)] except MetamorphicError as exc: #add to exclude_dict, to avoid running into the same error @@ -81,6 +85,8 @@ def generate_mutations(self) -> None: stacktrace=traceback.format_exc(), mutators=self.mutators, constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], originalmodel=self.original_model ) return None @@ -129,6 +135,8 @@ def run(self, model_file: str) -> dict: exception=e, stacktrace=traceback.format_exc(), constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], originalmodel=self.original_model ) @@ -139,6 +147,8 @@ def run(self, model_file: str) -> dict: exception=e, stacktrace=traceback.format_exc(), constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], mutators=self.mutators, originalmodel=self.original_model ) @@ -150,7 +160,11 @@ def rerun(self,error: dict) -> dict: This function will rerun a previous failed test """ try: - random.seed(self.seed) + if 'seed' in error: + run_seed = error['seed'] + random.seed(run_seed) + else: + random.seed(self.seed) self.model_file = error["originalmodel_file"] self.original_model = error["originalmodel"] self.exclude_dict = {} @@ -162,7 +176,7 @@ def rerun(self,error: dict) -> dict: return self.verify_model() else: return gen_mutations_error - # self.cons = error["constraints"] + # self.og_cons = error["constraints"] # return self.verify_model() except AssertionError as e: @@ -177,6 +191,8 @@ def rerun(self,error: dict) -> dict: exception=e, stacktrace=traceback.format_exc(), constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], originalmodel=self.original_model ) @@ -187,6 +203,8 @@ def rerun(self,error: dict) -> dict: exception=e, stacktrace=traceback.format_exc(), constraints=self.cons, + variables=[(var, var.lb, var.ub) if not is_boolexpr(var) else (var, "bool") for var in + get_variables(self.cons)], originalmodel=self.original_model ) diff --git a/verifiers/verifier_runner.py b/verifiers/verifier_runner.py index 5e737691..ab5bae88 100644 --- a/verifiers/verifier_runner.py +++ b/verifiers/verifier_runner.py @@ -1,14 +1,23 @@ import glob import math +import os +import random import warnings from os.path import join +import gc +from fuzz_test_utils.output_writer import get_logging_dir, write_csv from verifiers import * from fuzz_test_utils import Fuzz_Test_ErrorTypes -def get_all_verifiers() -> list: - return [Solution_Verifier,Optimization_Verifier,Model_Count_Verifier,Metamorphic_Verifier,Equivalance_Verifier] +def get_all_verifiers(single_solver) -> list: + if single_solver: + return [Solution_Verifier,Optimization_Verifier,Model_Count_Verifier,Metamorphic_Verifier,Equivalance_Verifier] + else: + return [Solver_Vote_Count_Verifier, Solver_Vote_Sat_Verifier, Strengthening_Weakening_Verifier, + Solver_Vote_Eq_Verifier, Solver_Vote_Sol_Verifier] -def run_verifiers(current_amount_of_tests, current_amount_of_error, lock, solver: str, mutations_per_model: int, folders: list, max_error_treshold: int, output_dir: str, time_limit: float) -> None: +def run_verifiers(current_amount_of_tests, current_amount_of_error, lock, solver: list[str], mutations_per_model: int, folders: list, max_error_treshold: int, output_dir: str, time_limit: float, mm_prob: float, + solver_counts, verifier_counts, verifier_runtimes) -> None: """ This function will be used to run different verifiers @@ -28,36 +37,62 @@ def run_verifiers(current_amount_of_tests, current_amount_of_error, lock, solver exclude_dict = {} random_seed = random.random() random.seed(random_seed) + solver = solver[0] if len(solver) == 1 else solver # Take the solver as a string if there is only one + if solver == 'pysat': + solver = random.Random().sample(['minizinc', 'ortools', 'gurobi', 'choco'], 2) # Andere solvers hebben problemen met hun time_limit + print(f"Running with solvers {solver}") verifier_kwargs = {"solver":solver, "mutations_per_model":mutations_per_model, "exclude_dict":exclude_dict,"time_limit": time_limit, "seed":random_seed} execution_time = 0 try: while time.time() < time_limit and current_amount_of_error.value < max_error_treshold: - random_verifier = random.choice(get_all_verifiers())(**verifier_kwargs) + if isinstance(solver, str): + random_verifier = random.choice(get_all_verifiers(single_solver=True))(**verifier_kwargs) + elif isinstance(solver, list): + verifier_kwargs["mm_prob"] = mm_prob # add probability to choose mm_mut instead of gen_mut + random_verifier = random.choice(get_all_verifiers(single_solver=False))(**verifier_kwargs) + else: + raise Exception(f"The given solvers are not in the correct format. Should be either a single solver (str) or a list of solvers ([str]), but is {type(solver)}.") fmodels = [] for folder in folders: fmodels.extend(glob.glob(join(folder,random_verifier.getType(), "*"))) if len(fmodels) > 0: - fmodel = random.choice(fmodels) + fmodel = random.Random().choice(fmodels) # random.choice used the random.seed()! Same models were being tested! + for s in solver: + solver_counts[s].value += 1 + verifier_counts[random_verifier.name].value += 1 start_time = time.time() error = random_verifier.run(fmodel) - execution_time = math.floor(time.time() - start_time) + end_time = time.time() + execution_time = math.floor(end_time - start_time) + verifier_runtimes[random_verifier.name].value += end_time - start_time + # check if we got an error if error is not None: lock.acquire() try: + if 'seed' in error: # Give every run its own seed, otherwise same mutations happen + random_seed = error['seed'] error_data = {'verifier':random_verifier.getName(),'solver' : solver, 'mutations_per_model' : mutations_per_model, "seed": random_seed, "execution_time": execution_time, "error" :error} - write_error(error_data,output_dir) - current_amount_of_error.value +=1 + logging_dir = get_logging_dir(error_data, output_dir) if get_logging_dir(error_data, output_dir) else output_dir + os.makedirs(logging_dir, exist_ok=True) # create if it doesn't already exist + write_error(error_data, logging_dir) + write_csv(error_data, output_dir+'.csv') + current_amount_of_error.value += 1 finally: - lock.release() + lock.release() + # Memory fix? + del random_verifier + import gc + gc.collect() lock.acquire() try: current_amount_of_tests.value += 1 finally: lock.release() + print(f"Process {os.getpid()} with solvers {solver} exiting at {time.time()} > {time_limit}", flush=True) except Exception as e: print(traceback.format_exc(),flush=True)