From 77a9c02200c4cc09fff98f77eab37cacaf057d1e Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Fri, 4 Apr 2025 00:12:21 +0200 Subject: [PATCH] refactor: Use FormulaUtils where appropriate These are shorter and thus easier to read. --- .../diffdetective/analysis/logic/SAT.java | 7 +- .../cpp/ControllingCExpressionVisitor.java | 16 +- .../jpp/ControllingJPPExpressionVisitor.java | 19 +- .../diffdetective/util/fide/FormulaUtils.java | 15 ++ src/test/java/CPPParserTest.java | 192 +++++++++--------- src/test/java/FeatureIDETest.java | 30 +-- src/test/java/FixTrueFalseTest.java | 45 ++-- src/test/java/JPPParserTest.java | 35 ++-- src/test/java/PCTest.java | 38 ++-- src/test/java/SATTest.java | 33 +-- src/test/java/ViewTest.java | 10 +- 11 files changed, 237 insertions(+), 203 deletions(-) diff --git a/src/main/java/org/variantsync/diffdetective/analysis/logic/SAT.java b/src/main/java/org/variantsync/diffdetective/analysis/logic/SAT.java index 5a792178a..438f2807f 100644 --- a/src/main/java/org/variantsync/diffdetective/analysis/logic/SAT.java +++ b/src/main/java/org/variantsync/diffdetective/analysis/logic/SAT.java @@ -9,6 +9,7 @@ import java.util.HashMap; import static org.variantsync.diffdetective.util.fide.FormulaUtils.negate; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.and; /** * Class with static functions for satisfiability solving, potentially with some optimizations. @@ -123,7 +124,7 @@ public static boolean implies(final Node left, final Node right) { /// = TAUT(!left || right) /// = !SAT(!(!left || right)) /// = !SAT(left && !right)) - return !isSatisfiable(new And(left, negate(right))); + return !isSatisfiable(and(left, negate(right))); } /** @@ -134,6 +135,6 @@ public static boolean implies(final Node left, final Node right) { * @return True iff left <=> right is a tautology. */ public static boolean equivalent(final Node left, final Node right) { - return isTautology(new Equals(left, right)); + return isTautology(FormulaUtils.equivalent(left, right)); } -} \ No newline at end of file +} diff --git a/src/main/java/org/variantsync/diffdetective/feature/cpp/ControllingCExpressionVisitor.java b/src/main/java/org/variantsync/diffdetective/feature/cpp/ControllingCExpressionVisitor.java index 1ffdd0761..4a29ee296 100644 --- a/src/main/java/org/variantsync/diffdetective/feature/cpp/ControllingCExpressionVisitor.java +++ b/src/main/java/org/variantsync/diffdetective/feature/cpp/ControllingCExpressionVisitor.java @@ -4,17 +4,17 @@ import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor; import org.antlr.v4.runtime.tree.ParseTree; import org.antlr.v4.runtime.tree.ParseTreeVisitor; -import org.prop4j.And; -import org.prop4j.Literal; import org.prop4j.Node; -import org.prop4j.Not; -import org.prop4j.Or; import org.variantsync.diffdetective.feature.antlr.CExpressionParser; import org.variantsync.diffdetective.feature.antlr.CExpressionVisitor; +import org.variantsync.diffdetective.util.fide.FormulaUtils; import java.util.List; import java.util.function.Function; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.negate; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.var; + /** * Visitor that controls how formulas given as an ANTLR parse tree are abstracted. * To this end, the visitor traverses the parse tree, searching for subtrees that should be abstracted. @@ -73,7 +73,7 @@ public Node visitPrimaryExpression(CExpressionParser.PrimaryExpressionContext ct // Negation can be modeled in the formula. // All other unary operators need to be abstracted. if (ctx.unaryOperator().getText().equals("!")) { - return new Not(ctx.primaryExpression().accept(this)); + return negate(ctx.primaryExpression().accept(this)); } else { return abstractToLiteral(ctx); } @@ -250,7 +250,7 @@ public Node visitInclusiveOrExpression(CExpressionParser.InclusiveOrExpressionCo // ; @Override public Node visitLogicalAndExpression(CExpressionParser.LogicalAndExpressionContext ctx) { - return visitLogicalExpression(ctx, And::new); + return visitLogicalExpression(ctx, FormulaUtils::and); } // logicalOrExpression @@ -258,7 +258,7 @@ public Node visitLogicalAndExpression(CExpressionParser.LogicalAndExpressionCont // ; @Override public Node visitLogicalOrExpression(CExpressionParser.LogicalOrExpressionContext ctx) { - return visitLogicalExpression(ctx, Or::new); + return visitLogicalExpression(ctx, FormulaUtils::or); } // logicalOperand @@ -302,6 +302,6 @@ private Node recurseOnSingleChild(ParserRuleContext ctx) { } private Node abstractToLiteral(ParserRuleContext ctx) { - return new Literal(ctx.accept(abstractingVisitor).toString()); + return var(ctx.accept(abstractingVisitor).toString()); } } diff --git a/src/main/java/org/variantsync/diffdetective/feature/jpp/ControllingJPPExpressionVisitor.java b/src/main/java/org/variantsync/diffdetective/feature/jpp/ControllingJPPExpressionVisitor.java index e6caf2e04..ba8eb234c 100644 --- a/src/main/java/org/variantsync/diffdetective/feature/jpp/ControllingJPPExpressionVisitor.java +++ b/src/main/java/org/variantsync/diffdetective/feature/jpp/ControllingJPPExpressionVisitor.java @@ -3,16 +3,17 @@ import org.antlr.v4.runtime.ParserRuleContext; import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor; import org.antlr.v4.runtime.tree.ParseTree; -import org.prop4j.And; -import org.prop4j.Literal; import org.prop4j.Node; -import org.prop4j.Or; import org.variantsync.diffdetective.feature.antlr.JPPExpressionParser; import org.variantsync.diffdetective.feature.antlr.JPPExpressionVisitor; +import org.variantsync.diffdetective.util.fide.FormulaUtils; import java.util.List; import java.util.function.Function; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.negate; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.var; + /** * Transform a parse tree into a {@link org.prop4j.Node formula}. * Non-boolean sub-expressions are abstracted using @@ -33,7 +34,7 @@ public Node visitExpression(JPPExpressionParser.ExpressionContext ctx) { // ; @Override public Node visitLogicalOrExpression(JPPExpressionParser.LogicalOrExpressionContext ctx) { - return visitLogicalExpression(ctx, Or::new); + return visitLogicalExpression(ctx, FormulaUtils::or); } // logicalAndExpression @@ -41,7 +42,7 @@ public Node visitLogicalOrExpression(JPPExpressionParser.LogicalOrExpressionCont // ; @Override public Node visitLogicalAndExpression(JPPExpressionParser.LogicalAndExpressionContext ctx) { - return visitLogicalExpression(ctx, And::new); + return visitLogicalExpression(ctx, FormulaUtils::and); } // primaryExpression @@ -68,7 +69,7 @@ public Node visitPrimaryExpression(JPPExpressionParser.PrimaryExpressionContext // ; @Override public Node visitComparisonExpression(JPPExpressionParser.ComparisonExpressionContext ctx) { - return new Literal(ctx.getText()); + return var(ctx.getText()); } // operand @@ -79,7 +80,7 @@ public Node visitComparisonExpression(JPPExpressionParser.ComparisonExpressionCo // ; @Override public Node visitOperand(JPPExpressionParser.OperandContext ctx) { - return new Literal(ctx.getText()); + return var(ctx.getText()); } // definedExpression @@ -87,7 +88,7 @@ public Node visitOperand(JPPExpressionParser.OperandContext ctx) { // ; @Override public Node visitDefinedExpression(JPPExpressionParser.DefinedExpressionContext ctx) { - return new Literal(String.format("defined(%s)", ctx.Identifier().getText())); + return var(String.format("defined(%s)", ctx.Identifier().getText())); } // undefinedExpression @@ -95,7 +96,7 @@ public Node visitDefinedExpression(JPPExpressionParser.DefinedExpressionContext // ; @Override public Node visitUndefinedExpression(JPPExpressionParser.UndefinedExpressionContext ctx) { - return new Literal(String.format("defined(%s)", ctx.Identifier().getText()), false); + return negate(var(String.format("defined(%s)", ctx.Identifier().getText()))); } // propertyExpression diff --git a/src/main/java/org/variantsync/diffdetective/util/fide/FormulaUtils.java b/src/main/java/org/variantsync/diffdetective/util/fide/FormulaUtils.java index b03072c14..ece56aae0 100644 --- a/src/main/java/org/variantsync/diffdetective/util/fide/FormulaUtils.java +++ b/src/main/java/org/variantsync/diffdetective/util/fide/FormulaUtils.java @@ -1,9 +1,12 @@ package org.variantsync.diffdetective.util.fide; import org.prop4j.And; +import org.prop4j.Equals; +import org.prop4j.Implies; import org.prop4j.Literal; import org.prop4j.Node; import org.prop4j.Not; +import org.prop4j.Or; import org.variantsync.diffdetective.analysis.logic.SAT; import org.variantsync.diffdetective.util.Assert; import org.variantsync.functjonal.Cast; @@ -45,6 +48,18 @@ public static And and(Node... nodes) { return new And(nodes); } + public static Or or(Node... nodes) { + return new Or(nodes); + } + + public static Implies implies(Node a, Node b) { + return new Implies(a, b); + } + + public static Equals equivalent(Node a, Node b) { + return new Equals(a, b); + } + /** Recursively counts the number of instances of {@link Literal} in {@code formula}. */ public static int numberOfLiterals(final Node formula) { if (formula instanceof Literal) { diff --git a/src/test/java/CPPParserTest.java b/src/test/java/CPPParserTest.java index 9e94c64b0..f7192f1a3 100644 --- a/src/test/java/CPPParserTest.java +++ b/src/test/java/CPPParserTest.java @@ -1,10 +1,6 @@ import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.MethodSource; -import org.prop4j.And; -import org.prop4j.Literal; import org.prop4j.Node; -import org.prop4j.Not; -import org.prop4j.Or; import org.variantsync.diffdetective.error.UnparseableFormulaException; import org.variantsync.diffdetective.feature.cpp.CPPDiffLineFormulaExtractor; @@ -12,6 +8,10 @@ import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertThrows; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.and; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.or; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.var; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.negate; public class CPPParserTest { private static record TestCase(String formula, Node expected) { @@ -22,101 +22,101 @@ private static record ThrowingTestCase(String formula) { private static List testCases() { return List.of( - new TestCase("#if A", new Literal("A")), - new TestCase("#ifdef A", new Literal("defined(A)")), - new TestCase("#ifndef A", new Literal("defined(A)", false)), - new TestCase("#elif A", new Literal("A")), - - new TestCase("#if !A", new Not(new Literal("A"))), - new TestCase("#if A && B", new And(new Literal("A"), new Literal("B"))), - new TestCase("#if A || B", new Or(new Literal("A"), new Literal("B"))), - new TestCase("#if A && (B || C)", new And(new Literal("A"), new Or(new Literal("B"), new Literal("C")))), - new TestCase("#if A && B || C", new Or(new And(new Literal("A"), new Literal("B")), new Literal("C"))), - - new TestCase("#if 1 > -42", new Literal("1>-42")), - new TestCase("#if 1 > +42", new Literal("1>+42")), - new TestCase("#if 42 > A", new Literal("42>A")), - new TestCase("#if 42 > ~A", new Literal("42>~A")), - new TestCase("#if A + B > 42", new Literal("A+B>42")), - new TestCase("#if A << B", new Literal("A<= B && C > D", new And(new Literal("A>=B"), new Literal("C>D"))), - new TestCase("#if A * (B + C)", new Literal("A*(B+C)")), - new TestCase("#if defined(A) && (B * 2) > C", new And(new Literal("defined(A)"), new Literal("(B*2)>C"))), - new TestCase("#if(STDC == 1) && (defined(LARGE) || defined(COMPACT))", new And(new Literal("STDC==1"), new Or(new Literal("defined(LARGE)"), new Literal("defined(COMPACT)")))), - new TestCase("#if (('Z' - 'A') == 25)", new Literal("('Z'-'A')==25")), - new TestCase("#if APR_CHARSET_EBCDIC && !(('Z' - 'A') == 25)", new And(new Literal("APR_CHARSET_EBCDIC"), new Not(new Literal("('Z'-'A')==25")))), + new TestCase("#if A", var("A")), + new TestCase("#ifdef A", var("defined(A)")), + new TestCase("#ifndef A", negate(var("defined(A)"))), + new TestCase("#elif A", var("A")), + + new TestCase("#if !A", negate(var("A"))), + new TestCase("#if A && B", and(var("A"), var("B"))), + new TestCase("#if A || B", or(var("A"), var("B"))), + new TestCase("#if A && (B || C)", and(var("A"), or(var("B"), var("C")))), + new TestCase("#if A && B || C", or(and(var("A"), var("B")), var("C"))), + + new TestCase("#if 1 > -42", var("1>-42")), + new TestCase("#if 1 > +42", var("1>+42")), + new TestCase("#if 42 > A", var("42>A")), + new TestCase("#if 42 > ~A", var("42>~A")), + new TestCase("#if A + B > 42", var("A+B>42")), + new TestCase("#if A << B", var("A<= B && C > D", and(var("A>=B"), var("C>D"))), + new TestCase("#if A * (B + C)", var("A*(B+C)")), + new TestCase("#if defined(A) && (B * 2) > C", and(var("defined(A)"), var("(B*2)>C"))), + new TestCase("#if(STDC == 1) && (defined(LARGE) || defined(COMPACT))", and(var("STDC==1"), or(var("defined(LARGE)"), var("defined(COMPACT)")))), + new TestCase("#if (('Z' - 'A') == 25)", var("('Z'-'A')==25")), + new TestCase("#if APR_CHARSET_EBCDIC && !(('Z' - 'A') == 25)", and(var("APR_CHARSET_EBCDIC"), negate(var("('Z'-'A')==25")))), new TestCase("# if ((GNUTLS_VERSION_MAJOR + (GNUTLS_VERSION_MINOR > 0 || GNUTLS_VERSION_PATCH >= 20)) > 3)", - new Literal("(GNUTLS_VERSION_MAJOR+(GNUTLS_VERSION_MINOR>0||GNUTLS_VERSION_PATCH>=20))>3")), - - new TestCase("#if A && (B > C)", new And(new Literal("A"), new Literal("B>C"))), - new TestCase("#if (A && B) > C", new Literal("(A&&B)>C")), - new TestCase("#if C == (A || B)", new Literal("C==(A||B)")), - new TestCase("#if ((A && B) > C)", new Literal("(A&&B)>C")), - new TestCase("#if A && ((B + 1) > (C || D))", new And(new Literal("A"), new Literal("(B+1)>(C||D)"))), - - new TestCase("#if __has_include", new Literal("__has_include")), - new TestCase("#if defined __has_include", new Literal("defined(__has_include)")), - new TestCase("#if __has_include()", new Literal("__has_include()")), - new TestCase("#if __has_include()", new Literal("__has_include()")), - new TestCase("#if __has_include(\"nss3/nss.h\")", new Literal("__has_include(\"nss3/nss.h\")")), - new TestCase("#if __has_include(\"nss.h\")", new Literal("__has_include(\"nss.h\")")), - - new TestCase("#if __has_attribute", new Literal("__has_attribute")), - new TestCase("#if defined __has_attribute", new Literal("defined(__has_attribute)")), - new TestCase("# if __has_attribute (nonnull)", new Literal("__has_attribute(nonnull)")), - new TestCase("#if defined __has_attribute && __has_attribute (nonnull)", new And(new Literal("defined(__has_attribute)"), new Literal("__has_attribute(nonnull)"))), - - new TestCase("#if __has_cpp_attribute", new Literal("__has_cpp_attribute")), - new TestCase("#if defined __has_cpp_attribute", new Literal("defined(__has_cpp_attribute)")), - new TestCase("#if __has_cpp_attribute (nonnull)", new Literal("__has_cpp_attribute(nonnull)")), - new TestCase("#if __has_cpp_attribute (nonnull) && A", new And(new Literal("__has_cpp_attribute(nonnull)"), new Literal("A"))), - - new TestCase("#if defined __has_c_attribute", new Literal("defined(__has_c_attribute)")), - new TestCase("#if __has_c_attribute", new Literal("__has_c_attribute")), - new TestCase("#if __has_c_attribute (nonnull)", new Literal("__has_c_attribute(nonnull)")), - new TestCase("#if __has_c_attribute (nonnull) && A", new And(new Literal("__has_c_attribute(nonnull)"), new Literal("A"))), - - new TestCase("#if defined __has_builtin", new Literal("defined(__has_builtin)")), - new TestCase("#if __has_builtin", new Literal("__has_builtin")), - new TestCase("#if __has_builtin (__nonnull)", new Literal("__has_builtin(__nonnull)")), - new TestCase("#if __has_builtin (nonnull) && A", new And(new Literal("__has_builtin(nonnull)"), new Literal("A"))), - - new TestCase("#if A // Comment && B", new Literal("A")), - new TestCase("#if A /* Comment */ && B", new And(new Literal("A"), new Literal("B"))), - new TestCase("#if A && B /* Multiline Comment", new And(new Literal("A"), new Literal("B"))), - - new TestCase("#if A == B", new Literal("A==B")), - new TestCase("#if A == 1", new Literal("A==1")), - - new TestCase("#if defined A", new Literal("defined(A)")), - new TestCase("#if defined(A)", new Literal("defined(A)")), - new TestCase("#if defined (A)", new Literal("defined(A)")), - new TestCase("#if defined ( A )", new Literal("defined(A)")), - new TestCase("#if (defined A)", new Literal("defined(A)")), - new TestCase("#if MACRO (A)", new Literal("MACRO(A)")), - new TestCase("#if MACRO (A, B)", new Literal("MACRO(A,B)")), - new TestCase("#if MACRO (A, B + C)", new Literal("MACRO(A,B+C)")), - new TestCase("#if MACRO (A, B) == 1", new Literal("MACRO(A,B)==1")), - - new TestCase("#if ifndef", new Literal("ifndef")), - - new TestCase("#if __has_include_next()", new Literal("__has_include_next()")), - new TestCase("#if __is_target_arch(x86)", new Literal("__is_target_arch(x86)")), - new TestCase("#if A || (defined(NAME) && (NAME >= 199630))", new Or(new Literal("A"), new And(new Literal("defined(NAME)"), new Literal("NAME>=199630")))), - new TestCase("#if MACRO(part:part)", new Literal("MACRO(part:part)")), - new TestCase("#if MACRO(x=1)", new Literal("MACRO(x=1)")), - new TestCase("#if A = 3", new Literal("A=3")), - new TestCase("#if ' ' == 32", new Literal("' '==32")), - new TestCase("#if (NAME<<1) > (1<(1<0||GNUTLS_VERSION_PATCH>=20))>3")), + + new TestCase("#if A && (B > C)", and(var("A"), var("B>C"))), + new TestCase("#if (A && B) > C", var("(A&&B)>C")), + new TestCase("#if C == (A || B)", var("C==(A||B)")), + new TestCase("#if ((A && B) > C)", var("(A&&B)>C")), + new TestCase("#if A && ((B + 1) > (C || D))", and(var("A"), var("(B+1)>(C||D)"))), + + new TestCase("#if __has_include", var("__has_include")), + new TestCase("#if defined __has_include", var("defined(__has_include)")), + new TestCase("#if __has_include()", var("__has_include()")), + new TestCase("#if __has_include()", var("__has_include()")), + new TestCase("#if __has_include(\"nss3/nss.h\")", var("__has_include(\"nss3/nss.h\")")), + new TestCase("#if __has_include(\"nss.h\")", var("__has_include(\"nss.h\")")), + + new TestCase("#if __has_attribute", var("__has_attribute")), + new TestCase("#if defined __has_attribute", var("defined(__has_attribute)")), + new TestCase("# if __has_attribute (nonnull)", var("__has_attribute(nonnull)")), + new TestCase("#if defined __has_attribute && __has_attribute (nonnull)", and(var("defined(__has_attribute)"), var("__has_attribute(nonnull)"))), + + new TestCase("#if __has_cpp_attribute", var("__has_cpp_attribute")), + new TestCase("#if defined __has_cpp_attribute", var("defined(__has_cpp_attribute)")), + new TestCase("#if __has_cpp_attribute (nonnull)", var("__has_cpp_attribute(nonnull)")), + new TestCase("#if __has_cpp_attribute (nonnull) && A", and(var("__has_cpp_attribute(nonnull)"), var("A"))), + + new TestCase("#if defined __has_c_attribute", var("defined(__has_c_attribute)")), + new TestCase("#if __has_c_attribute", var("__has_c_attribute")), + new TestCase("#if __has_c_attribute (nonnull)", var("__has_c_attribute(nonnull)")), + new TestCase("#if __has_c_attribute (nonnull) && A", and(var("__has_c_attribute(nonnull)"), var("A"))), + + new TestCase("#if defined __has_builtin", var("defined(__has_builtin)")), + new TestCase("#if __has_builtin", var("__has_builtin")), + new TestCase("#if __has_builtin (__nonnull)", var("__has_builtin(__nonnull)")), + new TestCase("#if __has_builtin (nonnull) && A", and(var("__has_builtin(nonnull)"), var("A"))), + + new TestCase("#if A // Comment && B", var("A")), + new TestCase("#if A /* Comment */ && B", and(var("A"), var("B"))), + new TestCase("#if A && B /* Multiline Comment", and(var("A"), var("B"))), + + new TestCase("#if A == B", var("A==B")), + new TestCase("#if A == 1", var("A==1")), + + new TestCase("#if defined A", var("defined(A)")), + new TestCase("#if defined(A)", var("defined(A)")), + new TestCase("#if defined (A)", var("defined(A)")), + new TestCase("#if defined ( A )", var("defined(A)")), + new TestCase("#if (defined A)", var("defined(A)")), + new TestCase("#if MACRO (A)", var("MACRO(A)")), + new TestCase("#if MACRO (A, B)", var("MACRO(A,B)")), + new TestCase("#if MACRO (A, B + C)", var("MACRO(A,B+C)")), + new TestCase("#if MACRO (A, B) == 1", var("MACRO(A,B)==1")), + + new TestCase("#if ifndef", var("ifndef")), + + new TestCase("#if __has_include_next()", var("__has_include_next()")), + new TestCase("#if __is_target_arch(x86)", var("__is_target_arch(x86)")), + new TestCase("#if A || (defined(NAME) && (NAME >= 199630))", or(var("A"), and(var("defined(NAME)"), var("NAME>=199630")))), + new TestCase("#if MACRO(part:part)", var("MACRO(part:part)")), + new TestCase("#if MACRO(x=1)", var("MACRO(x=1)")), + new TestCase("#if A = 3", var("A=3")), + new TestCase("#if ' ' == 32", var("' '==32")), + new TestCase("#if (NAME<<1) > (1<(1<= 199905) && (NAME < 1991011)) || (NAME >= 300000) || defined(NAME)", - new Or(new And(new Literal("defined(NAME)"), new Literal("NAME>=199905"), new Literal("NAME<1991011")), new Literal("NAME>=300000"), new Literal("defined(NAME)"))), - new TestCase("#if __has_warning(\"-Wa-warning\"_foo)", new Literal("__has_warning(\"-Wa-warning\"_foo)")), + or(and(var("defined(NAME)"), var("NAME>=199905"), var("NAME<1991011")), var("NAME>=300000"), var("defined(NAME)"))), + new TestCase("#if __has_warning(\"-Wa-warning\"_foo)", var("__has_warning(\"-Wa-warning\"_foo)")), - new TestCase("#if A && (B - (C || D))", new And(new Literal("A"), new Literal("B-(C||D)"))), - new TestCase("#if A == '1'", new Literal("A=='1'")) + new TestCase("#if A && (B - (C || D))", and(var("A"), var("B-(C||D)"))), + new TestCase("#if A == '1'", var("A=='1'")) ); } diff --git a/src/test/java/FeatureIDETest.java b/src/test/java/FeatureIDETest.java index b4621371f..d1ef53623 100644 --- a/src/test/java/FeatureIDETest.java +++ b/src/test/java/FeatureIDETest.java @@ -1,11 +1,17 @@ import de.ovgu.featureide.fm.core.editing.NodeCreator; import org.junit.jupiter.api.Test; -import org.prop4j.*; +import org.prop4j.False; +import org.prop4j.Literal; +import org.prop4j.Node; +import org.prop4j.True; import org.variantsync.diffdetective.analysis.logic.SAT; import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertFalse; import static org.junit.jupiter.api.Assertions.assertTrue; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.and; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.or; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.var; import java.util.HashMap; import java.util.Map; @@ -37,8 +43,8 @@ public void falseIsContradiction() { @Test public void trueAndA_Equals_A() { final Node tru = createTrue(); - final Node a = new Literal("A"); - final Node trueAndA = new And(tru, a); + final Node a = var("A"); + final Node trueAndA = and(tru, a); assertTrue(SAT.equivalent(trueAndA, a)); } @@ -47,15 +53,15 @@ public void trueAndA_Equals_A() { */ @Test public void A_Equals_A() { - final Node a = new Literal("A"); + final Node a = var("A"); assertTrue(SAT.equivalent(a, a)); } @Test public void falseOrA_Equals_A() { final Node no = createFalse(); - final Node a = new Literal("A"); - final Node noOrA = new Or(no, a); + final Node a = var("A"); + final Node noOrA = or(no, a); assertTrue(SAT.equivalent(noOrA, a)); } @@ -67,7 +73,7 @@ public void atomString() { // assume the following does not crash createTrue().toString(); createFalse().toString(); - new And(createFalse(), createTrue()).toString(); + and(createFalse(), createTrue()).toString(); } @Test @@ -79,23 +85,23 @@ public void atomValuesEqual() { @Test public void noAssignmentOfAtomsNecessary() { final Map emptyAssignment = new HashMap<>(); - Node formula = new And(createFalse(), createTrue()); + Node formula = and(createFalse(), createTrue()); formula.getValue(emptyAssignment); } // @Test // public void ontest() { // final Node tru = createTrue(); -// final Node a = new Literal("A"); -// final Node trueAndA = new And(tru, a); -// final Node eq = new Equals(trueAndA, a); +// final Node a = var("A"); +// final Node trueAndA = and(tru, a); +// final Node eq = equivalent(trueAndA, a); // System.out.println(eq); // System.out.println(FixTrueFalse.On(eq)); // } @Test public void testWeirdVariableNames() { - final Node node = new Literal("A@#$%^&*( )}{]`~]}\\|,./<>?`[)(_"); + final Node node = var("A@#$%^&*( )}{]`~]}\\|,./<>?`[)(_"); assertTrue(SAT.isSatisfiable(node)); } diff --git a/src/test/java/FixTrueFalseTest.java b/src/test/java/FixTrueFalseTest.java index 976b36dec..bb450c048 100644 --- a/src/test/java/FixTrueFalseTest.java +++ b/src/test/java/FixTrueFalseTest.java @@ -1,6 +1,7 @@ import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.MethodSource; -import org.prop4j.*; +import org.prop4j.Literal; +import org.prop4j.Node; import org.variantsync.diffdetective.util.fide.FixTrueFalse; import java.util.List; @@ -8,7 +9,11 @@ import static org.junit.jupiter.api.Assertions.assertEquals; import static org.variantsync.diffdetective.util.fide.FixTrueFalse.False; import static org.variantsync.diffdetective.util.fide.FixTrueFalse.True; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.and; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.equivalent; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.implies; import static org.variantsync.diffdetective.util.fide.FormulaUtils.negate; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.or; public class FixTrueFalseTest { private record TestCase(Node formula, Node expectedResult) {} @@ -16,34 +21,34 @@ private record TestCase(Node formula, Node expectedResult) {} private final static Literal A = new Literal("A"); private final static Literal B = new Literal("B"); private final static Literal C = new Literal("C"); - private final static Node SomeIrreducible = new And(A, new Implies(A, B)); + private final static Node SomeIrreducible = and(A, implies(A, B)); public static List testCases() { return List.of( - new TestCase(new And(True, A), A), - new TestCase(new Or(False, A), A), - new TestCase(new And(False, A), False), - new TestCase(new Or(True, A), True), + new TestCase(and(True, A), A), + new TestCase(or(False, A), A), + new TestCase(and(False, A), False), + new TestCase(or(True, A), True), - new TestCase(new Implies(False, A), True), - new TestCase(new Implies(A, False), negate(A)), - new TestCase(new Implies(True, A), A), - new TestCase(new Implies(A, True), True), + new TestCase(implies(False, A), True), + new TestCase(implies(A, False), negate(A)), + new TestCase(implies(True, A), A), + new TestCase(implies(A, True), True), - new TestCase(new Equals(A, True), A), - new TestCase(new Equals(True, A), A), - new TestCase(new Equals(A, False), negate(A)), - new TestCase(new Equals(False, A), negate(A)), + new TestCase(equivalent(A, True), A), + new TestCase(equivalent(True, A), A), + new TestCase(equivalent(A, False), negate(A)), + new TestCase(equivalent(False, A), negate(A)), new TestCase( - new Equals( - new Or( - new And(False, True, A), + equivalent( + or( + and(False, True, A), SomeIrreducible ), - new Implies( - new Or(False, C), - new Not(False) + implies( + or(False, C), + negate(False) ) ), SomeIrreducible) diff --git a/src/test/java/JPPParserTest.java b/src/test/java/JPPParserTest.java index e4469924c..93f0591bb 100644 --- a/src/test/java/JPPParserTest.java +++ b/src/test/java/JPPParserTest.java @@ -1,10 +1,7 @@ import org.apache.commons.io.IOUtils; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.MethodSource; -import org.prop4j.And; -import org.prop4j.Literal; import org.prop4j.Node; -import org.prop4j.Or; import org.variantsync.diffdetective.diff.result.DiffParseException; import org.variantsync.diffdetective.error.UnparseableFormulaException; import org.variantsync.diffdetective.feature.PreprocessorAnnotationParser; @@ -27,6 +24,10 @@ import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertThrows; import static org.variantsync.diffdetective.util.Assert.fail; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.and; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.negate; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.or; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.var; // Test cases for a parser of https://www.slashdev.ca/javapp/ public class JPPParserTest { @@ -41,35 +42,35 @@ private static List> abstractionTests() { /// #if expression // expression := | [!]defined(name) // expression := operand == operand - new JPPParserTest.TestCase<>("//#if 1 == -42", new Literal("1==-42")), + new JPPParserTest.TestCase<>("//#if 1 == -42", var("1==-42")), // expression := operand != operand - new JPPParserTest.TestCase<>("// #if 1 != 0", new Literal("1!=0")), + new JPPParserTest.TestCase<>("// #if 1 != 0", var("1!=0")), // expression := operand <= operand - new JPPParserTest.TestCase<>("//#if -1 <= 0", new Literal("-1<=0")), + new JPPParserTest.TestCase<>("//#if -1 <= 0", var("-1<=0")), // expression := operand < operand - new JPPParserTest.TestCase<>("//#if \"str\" < 0", new Literal("\"str\"<0")), + new JPPParserTest.TestCase<>("//#if \"str\" < 0", var("\"str\"<0")), // expression := operand >= operand - new JPPParserTest.TestCase<>("// #if \"str\" >= \"str\"", new Literal("\"str\">=\"str\"")), + new JPPParserTest.TestCase<>("// #if \"str\" >= \"str\"", var("\"str\">=\"str\"")), // expression := operand > operand - new JPPParserTest.TestCase<>("// #if 1.2 > 0", new Literal("1.2>0")), + new JPPParserTest.TestCase<>("// #if 1.2 > 0", var("1.2>0")), // expression := defined(name) - new JPPParserTest.TestCase<>("//#if defined(property)", new Literal("defined(property)")), + new JPPParserTest.TestCase<>("//#if defined(property)", var("defined(property)")), // expression := !defined(name) - new JPPParserTest.TestCase<>("//#if !defined(property)", new Literal("defined(property)", false)), + new JPPParserTest.TestCase<>("//#if !defined(property)", negate(var("defined(property)"))), // operand := ${property} - new JPPParserTest.TestCase<>("//#if ${os_version} == 4.1", new Literal("${os_version}==4.1")), + new JPPParserTest.TestCase<>("//#if ${os_version} == 4.1", var("${os_version}==4.1")), /// #if expression and expression - new JPPParserTest.TestCase<>("//#if 1 > 2 and defined( FEAT_A )", new And(new Literal("1>2"), new Literal("defined(FEAT_A)"))), + new JPPParserTest.TestCase<>("//#if 1 > 2 and defined( FEAT_A )", and(var("1>2"), var("defined(FEAT_A)"))), /// #if expression or expression - new JPPParserTest.TestCase<>("//#if !defined(left) or defined(right)", new Or(new Literal("defined(left)", false), new Literal("defined(right)"))), + new JPPParserTest.TestCase<>("//#if !defined(left) or defined(right)", or(negate(var("defined(left)")), var("defined(right)"))), /// #if expression and expression or expression - new JPPParserTest.TestCase<>("//#if ${os_version} == 4.1 and 1 > -42 or defined(ALL)", new Or(new And(new Literal("${os_version}==4.1"), new Literal("1>-42")), new Literal("defined(ALL)"))), + new JPPParserTest.TestCase<>("//#if ${os_version} == 4.1 and 1 > -42 or defined(ALL)", or(and(var("${os_version}==4.1"), var("1>-42")), var("defined(ALL)"))), /// #if "string with whitespace" - new JPPParserTest.TestCase<>("//#if ${ test } == \"a b\"", new Literal("${test}==\"a b\"")) + new JPPParserTest.TestCase<>("//#if ${ test } == \"a b\"", var("${test}==\"a b\"")) ); } @@ -103,7 +104,7 @@ private static List> fullDiffTests() { @ParameterizedTest @MethodSource("abstractionTests") - public void testCase(JPPParserTest.TestCase testCase) throws UnparseableFormulaException { + public void testCase(JPPParserTest.TestCase testCase) throws UnparseableFormulaException { assertEquals( testCase.expected, new JPPDiffLineFormulaExtractor().extractFormula(testCase.input()) diff --git a/src/test/java/PCTest.java b/src/test/java/PCTest.java index 7944dcdef..361a9b53f 100644 --- a/src/test/java/PCTest.java +++ b/src/test/java/PCTest.java @@ -1,7 +1,5 @@ import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.MethodSource; -import org.prop4j.And; -import org.prop4j.Literal; import org.prop4j.Node; import org.tinylog.Logger; import org.variantsync.diffdetective.analysis.logic.SAT; @@ -16,16 +14,18 @@ import java.util.Map; import static org.junit.jupiter.api.Assertions.assertTrue; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.and; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.negate; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.var; import static org.variantsync.diffdetective.variation.diff.Time.AFTER; import static org.variantsync.diffdetective.variation.diff.Time.BEFORE; -import static org.variantsync.diffdetective.util.fide.FormulaUtils.negate; public class PCTest { - private static final Literal A = new Literal("A"); - private static final Literal B = new Literal("B"); - private static final Literal C = new Literal("C"); - private static final Literal D = new Literal("D"); - private static final Literal E = new Literal("E"); + private static final Node A = var("A"); + private static final Node B = var("B"); + private static final Node C = var("C"); + private static final Node D = var("D"); + private static final Node E = var("E"); record ExpectedPC(Node before, Node after) {} record TestCase(Path file, Map expectedResult) { @Override @@ -38,27 +38,27 @@ public String toString() { private final static TestCase a = new TestCase( Path.of("a.diff"), Map.of( - "1", new ExpectedPC(A, new And(A, B)), - "2", new ExpectedPC(A, new And(A, C, negate(B))), - "3", new ExpectedPC(new And(A, D, E), new And(A, D)), + "1", new ExpectedPC(A, and(A, B)), + "2", new ExpectedPC(A, and(A, C, negate(B))), + "3", new ExpectedPC(and(A, D, E), and(A, D)), "4", new ExpectedPC(A, A) )); private final static TestCase elif = new TestCase( Path.of("elif.diff"), Map.of( "1", new ExpectedPC(A, A), - "2", new ExpectedPC(new And(negate(A), B), new And(negate(A), B)), - "3", new ExpectedPC(new And(negate(A), negate(B), C), new And(negate(A), B)), - "4", new ExpectedPC(new And(negate(A), negate(B), C), new And(negate(A), negate(B), D)), - "5", new ExpectedPC(new And(negate(A), negate(B), negate(C)), new And(negate(A), negate(B), negate(D))) + "2", new ExpectedPC(and(negate(A), B), and(negate(A), B)), + "3", new ExpectedPC(and(negate(A), negate(B), C), and(negate(A), B)), + "4", new ExpectedPC(and(negate(A), negate(B), C), and(negate(A), negate(B), D)), + "5", new ExpectedPC(and(negate(A), negate(B), negate(C)), and(negate(A), negate(B), negate(D))) )); private final static TestCase elze = new TestCase( Path.of("else.diff"), Map.of( - "1", new ExpectedPC(A, new And(A, B)), - "2", new ExpectedPC(new And(negate(A), C), new And(A, negate(B), C)), - "3", new ExpectedPC(new And(negate(A), C), new And(A, negate(B), negate(C))), - "4", new ExpectedPC(new And(negate(A), negate(C)), negate(A)) + "1", new ExpectedPC(A, and(A, B)), + "2", new ExpectedPC(and(negate(A), C), and(A, negate(B), C)), + "3", new ExpectedPC(and(negate(A), C), and(A, negate(B), negate(C))), + "4", new ExpectedPC(and(negate(A), negate(C)), negate(A)) )); private static String errorAt(final String node, String time, Node is, Node should) { diff --git a/src/test/java/SATTest.java b/src/test/java/SATTest.java index 26075c25a..549069cb3 100644 --- a/src/test/java/SATTest.java +++ b/src/test/java/SATTest.java @@ -1,6 +1,6 @@ import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.MethodSource; -import org.prop4j.*; +import org.prop4j.Node; import org.variantsync.diffdetective.analysis.logic.SAT; import org.variantsync.diffdetective.analysis.logic.Tseytin; import org.variantsync.diffdetective.util.fide.FixTrueFalse; @@ -10,20 +10,25 @@ import static org.junit.jupiter.api.Assertions.assertFalse; import static org.junit.jupiter.api.Assertions.assertTrue; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.and; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.equivalent; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.implies; import static org.variantsync.diffdetective.util.fide.FormulaUtils.negate; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.or; +import static org.variantsync.diffdetective.util.fide.FormulaUtils.var; public class SATTest { - private static final Literal A = new Literal("A"); - private static final Literal B = new Literal("B"); - private static final Literal C = new Literal("C"); - private static final Literal D = new Literal("D"); + private static final Node A = var("A"); + private static final Node B = var("B"); + private static final Node C = var("C"); + private static final Node D = var("D"); public static List tautologyTestCases() { return List.of( FixTrueFalse.True, negate(FixTrueFalse.False), - new Or(A, negate(A)), - new Implies(new And(A, new Implies(A, B)), B) // modus ponens + or(A, negate(A)), + implies(and(A, implies(A, B)), B) // modus ponens ); } @@ -31,7 +36,7 @@ public static List contradictoryTestCases() { return List.of( FixTrueFalse.False, negate(FixTrueFalse.True), - new And(A, negate(A)) + and(A, negate(A)) ); } @@ -39,12 +44,12 @@ public static List satisfiableTestCases() { var satisfiableTestCases = new ArrayList<>(List.of( A, negate(A), - negate(new And(A, B)), - new And(A, B), - new Or(A, B), - new Implies(A, B), - new Equals(A, B), - new And(A, B, new Or(negate(C), new Implies(D, A))) + negate(and(A, B)), + and(A, B), + or(A, B), + implies(A, B), + equivalent(A, B), + and(A, B, or(negate(C), implies(D, A))) )); satisfiableTestCases.addAll(tautologyTestCases()); return satisfiableTestCases; diff --git a/src/test/java/ViewTest.java b/src/test/java/ViewTest.java index f033d66b2..595ce6dd1 100644 --- a/src/test/java/ViewTest.java +++ b/src/test/java/ViewTest.java @@ -105,10 +105,10 @@ void test(String filename) throws IOException, DiffParseException { ); } -// showViews(initialVDiff, new VariantQuery(new And(new Literal("X")))); -// showViews(initialVDiff, new VariantQuery(new And(new Literal("Y")))); -// showViews(initialVDiff, new VariantQuery(new And(negate(new Literal("X"))))); -// showViews(initialVDiff, new VariantQuery(new And(negate(new Literal("Y"))))); +// showViews(initialVDiff, new VariantQuery(and(var("X")))); +// showViews(initialVDiff, new VariantQuery(and(var("Y")))); +// showViews(initialVDiff, new VariantQuery(and(negate(var("X"))))); +// showViews(initialVDiff, new VariantQuery(and(negate(var("Y"))))); // showViews(initialVDiff, new FeatureQuery("X")); // showViews(initialVDiff, new FeatureQuery("Y")); // showViews(initialVDiff, new ArtifactQuery("y")); @@ -145,7 +145,7 @@ void inspectRunningExample(String filename) throws IOException, DiffParseExcepti // Figure 3 final Configure configureExample1 = new Configure( - and(featureRing, /* FM = */ negate(new And(featureDoubleLink, featureRing))) + and(featureRing, /* FM = */ negate(and(featureDoubleLink, featureRing))) ); GameEngine.showAndAwaitAll( Show.tree(TreeView.tree(b, configureExample1), "Figure 3: view_{tree}(Figure 1, " + configureExample1 + ")")