Adapt messages for ConstraintErrors

CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java

@@ -478,12 +478,7 @@ private void propagateIndirectlyEnsuredPredicate(
             Collection<Integer> indices = relevantStatements.get(statement);
             for (Integer index : indices) {
                 AbstractPredicate predForOtherSeed =
-                        createPredicate(
-                                indirectPred.getGeneratingSeed(),
-                                predicate,
-                                statement,
-                                index,
-                                violations);
+                        createPredicate(this, predicate, statement, index, violations);
 
                 notifyExpectingSeeds(predForOtherSeed, false);
             }
@@ -502,7 +497,7 @@ private AbstractPredicate createIndirectPredicate(
                     unEnsPred.getPredicate(),
                     statement,
                     -1,
-                    new HashSet<>());
+                    unEnsPred.getViolations());
         }
 
         // If the generating seed ensured a valid predicate, we have to check if the current seed is

CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractError.java

@@ -3,11 +3,9 @@
 import boomerang.scene.Method;
 import boomerang.scene.Statement;
 import crypto.analysis.IAnalysisSeed;
-import crysl.rule.CrySLMethod;
 import crysl.rule.CrySLRule;
 import java.util.Collection;
 import java.util.HashSet;
-import java.util.Map;
 import java.util.Objects;
 
 public abstract class AbstractError {
@@ -16,8 +14,8 @@ public abstract class AbstractError {
     private final Statement errorStmt;
     private final CrySLRule rule;
 
-    private final Collection<AbstractError> precedingErrors; // preceding
-    private final Collection<AbstractError> subsequentErrors; // subsequent
+    private final Collection<AbstractError> precedingErrors;
+    private final Collection<AbstractError> subsequentErrors;
 
     public AbstractError(IAnalysisSeed seed, Statement errorStmt, CrySLRule rule) {
         this.seed = seed;
@@ -82,38 +80,6 @@ protected String getObjectType() {
         return " on object of type " + seed.getFact().getType();
     }
 
-    protected String formatMethodNames(Collection<CrySLMethod> methods) {
-        StringBuilder builder = new StringBuilder();
-        builder.append("{");
-
-        for (CrySLMethod method : methods) {
-            String formattedName = formatMethodName(method);
-            builder.append(formattedName);
-            builder.append(", ");
-        }
-        builder.delete(builder.length() - 2, builder.length());
-        builder.append("}");
-
-        return builder.toString();
-    }
-
-    protected String formatMethodName(CrySLMethod method) {
-        StringBuilder builder = new StringBuilder();
-        builder.append(method.getShortMethodName());
-        builder.append("(");
-
-        if (!method.getParameters().isEmpty()) {
-            for (Map.Entry<String, String> param : method.getParameters()) {
-                builder.append(param.getValue());
-                builder.append(", ");
-            }
-            builder.delete(builder.length() - 2, builder.length());
-        }
-
-        builder.append(")");
-        return builder.toString();
-    }
-
     @Override
     public int hashCode() {
         return Objects.hash(seed, errorStmt, rule);

CryptoAnalysis/src/main/java/crypto/analysis/errors/AlternativeReqPredicateError.java

@@ -2,8 +2,11 @@
 
 import crypto.analysis.IAnalysisSeed;
 import crypto.constraints.AlternativeReqPredicate;
+import crypto.constraints.RequiredPredicate;
 import crypto.predicates.UnEnsuredPredicate;
+import crypto.utils.CrySLUtils;
 import crysl.rule.CrySLRule;
+import java.util.ArrayList;
 import java.util.Collection;
 import java.util.Objects;
 
@@ -39,7 +42,25 @@ public AlternativeReqPredicate getViolatedPredicate() {
 
     @Override
     public String toErrorMarkerString() {
-        return "";
+        StringBuilder builder = new StringBuilder();
+
+        if (violatedPredicate.predicates().isEmpty()) {
+            return "";
+        }
+
+        int index = violatedPredicate.predicates().stream().findFirst().get().index();
+        builder.append(CrySLUtils.getIndexAsString(index));
+        builder.append(" parameter was not properly generated as ");
+
+        Collection<String> predNames = new ArrayList<>();
+        for (RequiredPredicate predicate : violatedPredicate.predicates()) {
+            predNames.add(predicate.predicate().getPredName());
+        }
+
+        String preds = String.join(" OR ", predNames);
+        builder.append(preds);
+
+        return builder.toString();
     }
 
     @Override

CryptoAnalysis/src/main/java/crypto/analysis/errors/ConstraintError.java

@@ -3,10 +3,11 @@
 import boomerang.scene.Statement;
 import crypto.analysis.IAnalysisSeed;
 import crypto.constraints.EvaluableConstraint;
-import crypto.constraints.IViolatedConstraint;
+import crypto.constraints.violations.IViolatedConstraint;
 import crysl.rule.CrySLRule;
 import java.util.Objects;
 
+/** Represents an error for a violated constraint from the CONSTRAINTS section */
 public class ConstraintError extends AbstractConstraintsError {
 
     private final EvaluableConstraint evaluableConstraint;
@@ -39,118 +40,14 @@ public IViolatedConstraint getViolatedConstraint() {
 
     @Override
     public String toErrorMarkerString() {
-        return "Constraint "
+        return "Constraint \""
                 + evaluableConstraint
-                + " on object "
+                + "\" on object "
                 + getSeed().getFact().getVariableName()
-                + " is violated due to the following reasons:";
+                + " is violated due to the following reason: "
+                + violatedConstraint.getErrorMessage();
     }
 
-    /*private String evaluateBrokenConstraint(final ISLConstraint constraint) {
-        StringBuilder msg = new StringBuilder();
-        if (constraint instanceof CrySLValueConstraint) {
-            return evaluateValueConstraint((CrySLValueConstraint) constraint);
-        } else if (constraint instanceof CrySLArithmeticConstraint brokenArithConstraint) {
-            msg.append(brokenArithConstraint.getLeft());
-            msg.append(" ");
-            msg.append(brokenArithConstraint.getOperator());
-            msg.append(" ");
-            msg.append(brokenArithConstraint.getRight());
-        } else if (constraint instanceof CrySLComparisonConstraint brokenCompCons) {
-            msg.append(" Variable ");
-            msg.append(brokenCompCons.getLeft().getLeft().getName());
-            msg.append(" must be ");
-            msg.append(evaluateCompOp(brokenCompCons.getOperator()));
-            msg.append(" ");
-            msg.append(brokenCompCons.getRight().getLeft().getName());
-        } else if (constraint instanceof CrySLConstraint crySLConstraint) {
-            final ISLConstraint leftSide = crySLConstraint.getLeft();
-            final ISLConstraint rightSide = crySLConstraint.getRight();
-            switch (crySLConstraint.getOperator()) {
-                case and:
-                    msg.append(evaluateBrokenConstraint(leftSide));
-                    msg.append(" or ");
-                    msg.append(evaluateBrokenConstraint(rightSide));
-                    break;
-                case implies:
-                    msg.append(evaluateBrokenConstraint(rightSide));
-                    break;
-                case or:
-                    msg.append(evaluateBrokenConstraint(leftSide));
-                    msg.append(" and ");
-                    msg.append(evaluateBrokenConstraint(rightSide));
-                    break;
-                default:
-                    break;
-            }
-        }
-        return msg.toString();
-    }
-
-    private String evaluateCompOp(CrySLComparisonConstraint.CompOp operator) {
-        return switch (operator) {
-            case ge -> "at least";
-            case g -> "greater than";
-            case l -> "lesser than";
-            case le -> "at most";
-            case eq -> "equal to";
-            case neq -> "not equal to";
-        };
-    }
-
-    private String evaluateValueConstraint(final CrySLValueConstraint brokenConstraint) {
-        StringBuilder msg = new StringBuilder();
-        msg.append(" should be any of ");
-        CrySLSplitter splitter = brokenConstraint.getVar().getSplitter();
-        if (splitter != null) {
-            Statement stmt = callSite.callSiteWithParam().statement();
-            String[] splitValues = new String[] {""};
-            if (stmt.isAssign()) {
-                Val rightSide = stmt.getRightOp();
-                if (rightSide.isConstant()) {
-                    splitValues =
-                            filterQuotes(rightSide.getVariableName()).split(splitter.getSplitter());
-                } else if (stmt.containsInvokeExpr()) {
-                    Collection<Val> parameters = stmt.getInvokeExpr().getArgs();
-
-                    for (Val parameter : parameters) {
-                        Type parameterType = parameter.getType();
-                        String javaType = brokenConstraint.getVar().getJavaType();
-
-                        if (parameterType.toString().equals(javaType)) {
-                            splitValues =
-                                    filterQuotes(parameter.getVariableName())
-                                            .split(splitter.getSplitter());
-                            break;
-                        }
-                    }
-                }
-            }
-
-            if (splitValues.length >= splitter.getIndex()) {
-                for (int i = 0; i < splitter.getIndex(); i++) {
-                    msg.append(splitValues[i]);
-                    msg.append(splitter.getSplitter());
-                }
-            }
-        }
-        msg.append("{");
-        for (final String val : brokenConstraint.getValueRange()) {
-            if (val.isEmpty()) {
-                msg.append("Empty String");
-            } else {
-                msg.append(val);
-            }
-            msg.append(", ");
-        }
-        msg.delete(msg.length() - 2, msg.length());
-        return msg.append('}').toString();
-    }
-
-    public static String filterQuotes(final String dirty) {
-        return CharMatcher.anyOf("\"").removeFrom(dirty);
-    }*/
-
     @Override
     public int hashCode() {
         return Objects.hash(super.hashCode(), violatedConstraint);

CryptoAnalysis/src/main/java/crypto/analysis/errors/ForbiddenMethodError.java

@@ -3,6 +3,7 @@
 import boomerang.scene.DeclaredMethod;
 import boomerang.scene.Statement;
 import crypto.analysis.IAnalysisSeed;
+import crypto.utils.CrySLUtils;
 import crysl.rule.CrySLMethod;
 import crysl.rule.CrySLRule;
 import java.util.Collection;
@@ -43,7 +44,7 @@ public String toErrorMarkerString() {
 
         if (!getAlternatives().isEmpty()) {
             msg.append(". Instead, call one of the methods ");
-            String altMethods = formatMethodNames(alternatives);
+            String altMethods = CrySLUtils.formatMethodNames(alternatives);
             msg.append(altMethods);
         }
         return msg.toString();

CryptoAnalysis/src/main/java/crypto/analysis/errors/ImpreciseValueExtractionError.java

@@ -40,9 +40,9 @@ public EvaluableConstraint getViolatedConstraint() {
 
     @Override
     public String toErrorMarkerString() {
-        return "Constraint "
+        return "Constraint \""
                 + violatedConstraint
-                + " could not be evaluated due to insufficient information.";
+                + "\" could not be evaluated due to insufficient information.";
     }
 
     @Override

CryptoAnalysis/src/main/java/crypto/analysis/errors/IncompleteOperationError.java

@@ -3,6 +3,7 @@
 import boomerang.scene.InvokeExpr;
 import boomerang.scene.Statement;
 import crypto.analysis.IAnalysisSeed;
+import crypto.utils.CrySLUtils;
 import crysl.rule.CrySLMethod;
 import crysl.rule.CrySLRule;
 import java.util.Collection;
@@ -86,7 +87,7 @@ private String getErrorMarkerStringForSingleDataflowPath() {
         msg.append(getObjectType());
         msg.append(" not completed. Expected call to one of the methods ");
 
-        String altMethods = formatMethodNames(expectedMethodCalls);
+        String altMethods = CrySLUtils.formatMethodNames(expectedMethodCalls);
         msg.append(altMethods);
         return msg.toString();
     }
@@ -105,7 +106,7 @@ private String getErrorMarkerStringForMultipleDataflowPaths() {
         msg.append(
                 " is on a dataflow path with an incomplete operation. Potential missing call to one of the methods ");
 
-        String altMethods = formatMethodNames(expectedMethodCalls);
+        String altMethods = CrySLUtils.formatMethodNames(expectedMethodCalls);
         msg.append(altMethods);
         return msg.toString();
     }

CryptoAnalysis/src/main/java/crypto/analysis/errors/TypestateError.java

@@ -2,6 +2,7 @@
 
 import boomerang.scene.Statement;
 import crypto.analysis.IAnalysisSeed;
+import crypto.utils.CrySLUtils;
 import crysl.rule.CrySLMethod;
 import crysl.rule.CrySLRule;
 import java.util.Collection;
@@ -33,7 +34,7 @@ public String toErrorMarkerString() {
         msg.append(getErrorStatement().getInvokeExpr().getMethod());
         msg.append(getObjectType());
 
-        String altMethods = formatMethodNames(expectedMethodCalls);
+        String altMethods = CrySLUtils.formatMethodNames(expectedMethodCalls);
 
         if (!altMethods.isEmpty()) {
             msg.append(". Expected a call to one of the following methods ");

CryptoAnalysis/src/main/java/crypto/constraints/BinaryConstraint.java

@@ -4,11 +4,20 @@
 import com.google.common.collect.Multimap;
 import crypto.analysis.AnalysisSeedWithSpecification;
 import crypto.analysis.errors.ConstraintError;
+import crypto.constraints.violations.IViolatedConstraint;
+import crypto.constraints.violations.ViolatedBinaryConstraint;
 import crypto.extractparameter.ParameterWithExtractedValues;
 import crysl.rule.CrySLConstraint;
 import crysl.rule.ISLConstraint;
 import java.util.Collection;
 
+/**
+ * A binary constraint represents two constraints 'left' and 'right' that are connected by a logical
+ * operator. During the evaluation, both sites are evaluated individually and, depending on the
+ * operator, evaluated by the basic logic rules. For example, an implication 'A implies B' evaluates
+ * to false if A is true and B is false, otherwise it evaluates to true. Currently, we have
+ * implications, conjunctions and disjunctions.
+ */
 public class BinaryConstraint extends EvaluableConstraint {
 
     private final CrySLConstraint constraint;
@@ -118,8 +127,7 @@ public EvaluationResult evaluate() {
             }
         }
 
-        IViolatedConstraint violatedConstraint =
-                new IViolatedConstraint.ViolatedBinaryConstraint(this);
+        IViolatedConstraint violatedConstraint = new ViolatedBinaryConstraint(this);
         ConstraintError error =
                 new ConstraintError(
                         seed, seed.getOrigin(), seed.getSpecification(), this, violatedConstraint);