CP 2024 snapshot

README.MD

@@ -0,0 +1,36 @@
+# Fuzz Testing CPMpy
+
+Repository for the future testing of CPMpy with the use of differential testing and metamorphic testing.
+
+It also will contain a tool to reduce the model in case a bug is found and a way to obtain CPMpy models to test CPMpy using the two techniques above.
+
+This repository builds futher on the work of the thesis by Ruben Kindt which was under guidance of Tias Guns and Ignace Bleukx.
+
+If an error is found in an internal function, a file with the name internalfunctioncrash will be created, containing 
+function, argument, originalmodel, error and mutators used that cause the error.
+
+If a model becomes unsat after transformations, a file with the name lasterrormodel is created, containing 
+model (the unsat model), originalmodel, mutators (list of mutators that were used)
+
+These files can be read by using pickle.load, as you can see in the example code in errorexploration.py
+That file also contains some code to reproduce the found bugs, and ways used to categorise all the bugs found during the experiments for CP24
+That was done dynamically and is out of scope of the 2024 paper, so this code can not be used as is.
+
+Commandline usage:
+when measuring code coverage, first set the environment variable COVERAGE_FILE, as to be able to compare multiple files.
+> export COVERAGE_FILE='.coverage_metamorphic-ortools5iter10hrs'
+
+To rerun the experiments form the 2024 paper:
+run the metamorphic test with the specified solver, number of mutations per input model, and time to run in hours.
+> nohup coverage run metamorphic_tests.py ortools 10 5 >/dev/null 2>&1 &
+(for each verification method, number of mutations(n=1, 2, 5, 10) and solver = {ortools, minizinc) )
+
+Every verification method has it's own python executable that works in a similar manner:
+- metamorphic_tests.py : Satisifiability check
+- equivalence check.py : All-Solutions check
+- model_counting.py    : Solution count check
+- optimization.py      : Optimisation check
+- solution_check.py    : 1-Solution check
+
+note that the experiments other than the one testing the number of mutations always use 5 mutations, so this 3rd parameter can be left out.
+

bug_minimization.py

@@ -0,0 +1,162 @@
+from cpmpy import Model
+from cpmpy.transformations.get_variables import get_variables
+
+def mes_naive(soft, hard=[], solver="ortools"):
+    """
+        Like MUS algorithm but in stead of looking for the model becoming sat
+        we look for the solve call to not throw an error anymore
+    """
+    m = Model(hard + soft)
+    no_error = False
+    try:
+        m.solve(solver=solver)
+        no_error = True
+    except Exception:
+        pass
+    if no_error:
+        raise AssertionError("model should throw error during solve")
+
+    mes = []
+    # order so that constraints with many variables are tried and removed first
+    core = sorted(soft, key=lambda c: -len(get_variables(c)))
+    for i in range(len(core)):
+        subcore = mes + core[i + 1:]  # check if all but 'i' makes core SAT
+
+        try:
+            Model(hard + subcore).solve(solver=solver)
+            #removing it gives no more error, keep it
+            mes.append(core[i])
+        except:
+            pass
+    return mes
+
+def mes_naive_solveAll(soft, hard=[], solver="ortools"):
+    """
+        Like MUS algorithm but in stead of looking for the model becoming sat
+        we look for the solve call to not throw an error anymore
+    """
+    m = Model(hard + soft)
+    no_error = False
+    try:
+        m.solveAll(solver=solver)
+        no_error = True
+    except Exception:
+        pass
+    if no_error:
+        raise AssertionError("model should throw error during solve")
+
+    mes = []
+    # order so that constraints with many variables are tried and removed first
+    core = sorted(soft, key=lambda c: -len(get_variables(c)))
+    for i in range(len(core)):
+        subcore = mes + core[i + 1:]  # check if all but 'i' makes core SAT
+
+        try:
+            Model(hard + subcore).solveAll(solver=solver)
+            #removing it gives no more error, keep it
+            mes.append(core[i])
+        except:
+            pass
+    return mes
+
+def mes_optimistic(soft,hard = [],solver='ortools'):
+    #faster version, assuming that just 1 constraint leads to the bug. try them one by one
+    m = Model(hard + soft)
+    no_error = False
+    try:
+        m.solve(solver=solver)
+        no_error = True
+    except Exception:
+        pass
+    if no_error:
+        raise AssertionError("model should throw error during solve")
+
+    for con in reversed(soft):
+        try:
+            Model(hard + [con]).solve(solver=solver)
+        except:
+            return con
+
+    return None #no single constraint leads to the error
+def mis_naive(soft,internalfunction, hard=[]):
+    """
+        Like MUS algorithm but in stead of looking for the model becoming sat
+        we look for the internal transformation call to not throw an error anymore
+    """
+    no_error = False
+    try:
+        internalfunction(soft + hard)
+        no_error = True
+    except Exception:
+        pass
+    if no_error:
+        raise AssertionError("function call should throw error")
+
+    mis = []
+    # order so that constraints with many variables are tried and removed first
+    core = sorted(soft, key=lambda c: -len(get_variables(c)))
+    for i in range(len(core)):
+        subcore = mis + core[i + 1:]  # check if all but 'i' makes core SAT
+
+        try:
+            internalfunction(hard + subcore)
+            #removing it gives no more error, keep it
+            mis.append(core[i])
+        except:
+            pass
+    return mis
+
+def solutions_missing(cons1,cons2,solver='ortools'):
+    '''
+    '''
+    vars = set(get_variables(cons1))
+    vars2 = set(get_variables(cons2))
+    sols1 = set()
+    sols2 = set()
+    Model(cons2).solveAll(solver=solver,display=lambda: sols2.add(tuple(var == var.value() for var in vars2 if var in vars)))
+    Model(cons1).solveAll(solver=solver,display=lambda: sols1.add(tuple(var == var.value() for var in vars)))
+
+    disappeared = sols1 - sols2
+    appeared = sols2 - sols1
+    print('sols1: ' + str(len(sols1)))
+    print('sols2: ' + str(len(sols2)))
+    print('dis: ' + str(len(disappeared)))
+    print('add: ' + str(len(appeared)))
+    return appeared, disappeared
+
+def mus_naive_counting(soft, hard=[], solver="ortools"):
+    """
+        A naive pure CP deletion-based MUS algorithm
+
+        Will repeatedly solve the problem from scratch with one less constraint
+        For anything but tiny sets of constraints, this will be terribly slow.
+
+        Best to only use for testing on solvers that do not support assumptions.
+        For others, use `mus()`
+
+        :param: soft: soft constraints, list of expressions
+        :param: hard: hard constraints, optional, list of expressions
+        :param: solver: name of a solver, see SolverLookup.solvernames()
+    """
+    # ensure toplevel list
+
+    m = Model(hard + soft)
+    assert m.solveAll(solver=solver) == 0, "MUS: model must return 0 solutions"
+    mus = []
+    # order so that constraints with many variables are tried and removed first
+    core = sorted(soft, key=lambda c: -len(get_variables(c)))
+    for i in range(len(core)):
+        subcore = mus + core[i + 1:]  # check if all but 'i' makes core SAT
+        try:
+            #print(hard + subcore)
+            if Model(hard + subcore).solveAll(solver=solver)>0:
+                # removing it makes it SAT, must keep for UNSAT
+                mus.append(core[i])
+            # else: still UNSAT so don't need this candidate
+        except:
+            # solver error, call mes
+            mes = mes_naive(hard + subcore)
+            print("messing")
+            return mes
+
+    return mus