diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index e9727bff..eb19a132 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -95,7 +95,36 @@ 3.2.1 - + + + org.jacoco + jacoco-maven-plugin + 0.8.12 + + + prepare-agent + + prepare-agent + + + + java.* + javax.* + sun.* + jdk.* + com.sun.* + + + + + report + test + + report + + + + org.antlr antlr4-maven-plugin 4.7.1 diff --git a/liquidjava-verifier/src/test/java/liquidjava/integration/ContextIntegrationTest.java b/liquidjava-verifier/src/test/java/liquidjava/integration/ContextIntegrationTest.java new file mode 100644 index 00000000..7c9820fd --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/integration/ContextIntegrationTest.java @@ -0,0 +1,278 @@ +package liquidjava.integration; + +import static org.junit.jupiter.api.Assertions.*; + +import java.util.List; + +import liquidjava.processor.context.*; +import liquidjava.rj_language.Predicate; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; + +import spoon.Launcher; +import spoon.reflect.factory.Factory; +import spoon.reflect.reference.CtTypeReference; + +/** + * Integration tests for Context management with variables, functions, ghosts, and refinements These tests verify that + * multiple components work together correctly in realistic scenarios + */ +class ContextIntegrationTest { + + private Context context; + private Factory factory; + + @BeforeEach + void setUp() { + Launcher launcher = new Launcher(); + factory = launcher.getFactory(); + context = Context.getInstance(); + context.reinitializeAllContext(); + } + + @Test + void testCompleteVariableLifecycle() { + // Scenario: Create variables, enter/exit contexts, track refinements + CtTypeReference intType = factory.Type().integerPrimitiveType(); + Predicate initialPred = Predicate.createOperation(Predicate.createVar("x"), ">", + Predicate.createLit("0", "int")); + + // Add variable in base scope + context.addVarToContext("x", intType, initialPred, factory.createLiteral(0)); + assertTrue(context.hasVariable("x"), "Variable should exist in base scope"); + + // Enter new scope and add local variable + context.enterContext(); + Predicate localPred = Predicate.createOperation(Predicate.createVar("y"), "<", + Predicate.createLit("100", "int")); + context.addVarToContext("y", intType, localPred, factory.createLiteral(0)); + + assertTrue(context.hasVariable("x"), "Base scope variable accessible in nested scope"); + assertTrue(context.hasVariable("y"), "Local variable exists"); + assertEquals(2, context.getAllVariables().size(), "Should have 2 variables"); + + // Update refinement for x + Predicate newPred = Predicate.createOperation(Predicate.createVar("x"), ">=", Predicate.createLit("5", "int")); + context.newRefinementToVariableInContext("x", newPred); + assertEquals(newPred.toString(), context.getVariableRefinements("x").toString()); + + // Exit scope + context.exitContext(); + assertTrue(context.hasVariable("x"), "Base scope variable still exists"); + assertFalse(context.hasVariable("y"), "Local variable removed"); + assertEquals(1, context.getAllVariables().size(), "Only base scope variable remains"); + } + + @Test + void testFunctionRegistrationAndRetrieval() { + // Scenario: Register functions with refinements and retrieve them + CtTypeReference intType = factory.Type().integerPrimitiveType(); + + // Create function with arguments and return refinement + RefinedFunction func = new RefinedFunction(); + func.setName("calculate"); + func.setClass("MathUtils"); + func.setType(intType); + func.addArgRefinements("x", intType, + Predicate.createOperation(Predicate.createVar("x"), ">", Predicate.createLit("0", "int"))); + func.addArgRefinements("y", intType, + Predicate.createOperation(Predicate.createVar("y"), ">", Predicate.createLit("0", "int"))); + func.setRefReturn( + Predicate.createOperation(Predicate.createVar("result"), ">", Predicate.createLit("0", "int"))); + + context.addFunctionToContext(func); + + // Retrieve and verify + RefinedFunction retrieved = context.getFunction("calculate", "MathUtils", 2); + assertNotNull(retrieved, "Function should be found by name, class, and arity"); + assertEquals(2, retrieved.getArguments().size(), "Should have 2 arguments"); + + // Add another function with same name but different arity + RefinedFunction func2 = new RefinedFunction(); + func2.setName("calculate"); + func2.setClass("MathUtils"); + func2.setType(intType); + func2.addArgRefinements("x", intType, new Predicate()); + context.addFunctionToContext(func2); + + List overloads = context.getAllMethodsWithNameSize("calculate", 1); + assertEquals(1, overloads.size(), "Should find function with arity 1"); + + overloads = context.getAllMethodsWithNameSize("calculate", 2); + assertEquals(1, overloads.size(), "Should find function with arity 2"); + } + + @Test + void testGhostStatesAndRefinements() { + // Scenario: Register ghost states and verify refinements + context.addGhostClass("Stack"); + + // Define states using GhostState + List> emptyList = List.of(); + GhostState isEmpty = new GhostState("isEmpty", emptyList, factory.Type().booleanPrimitiveType(), "Stack"); + isEmpty.setRefinement( + Predicate.createEquals(Predicate.createInvocation("Stack.size", Predicate.createVar("this")), + Predicate.createLit("0", "int"))); + + GhostState isNonEmpty = new GhostState("isNonEmpty", emptyList, factory.Type().booleanPrimitiveType(), "Stack"); + isNonEmpty.setRefinement( + Predicate.createOperation(Predicate.createInvocation("Stack.size", Predicate.createVar("this")), ">", + Predicate.createLit("0", "int"))); + + context.addToGhostClass("Stack", isEmpty); + context.addToGhostClass("Stack", isNonEmpty); + + List states = context.getGhostState("Stack"); + assertEquals(2, states.size(), "Should have 2 states"); + + // Verify state refinements + assertTrue(states.get(0).getRefinement().toString().contains("0")); + assertTrue(states.get(1).getRefinement().toString().contains(">")); + } + + @Test + void testVariableInstanceTracking() { + // Scenario: Track variable instances through assignments and control flow + CtTypeReference intType = factory.Type().integerPrimitiveType(); + Predicate initialRefinement = Predicate.createVar("x"); + + Variable var = new Variable("x", intType, initialRefinement); + context.addVarToContext(var); + + // Simulate assignment: x = 5 + VariableInstance instance1 = new VariableInstance("x_1", intType, + Predicate.createEquals(Predicate.createVar("x_1"), Predicate.createLit("5", "int"))); + var.addInstance(instance1); + context.addSpecificVariable(instance1); + context.addRefinementInstanceToVariable("x", "x_1"); + + assertTrue(var.getLastInstance().isPresent(), "Should have instance"); + assertEquals("x_1", var.getLastInstance().get().getName()); + + // Simulate second assignment: x = x + 1 + VariableInstance instance2 = new VariableInstance("x_2", intType, + Predicate.createEquals(Predicate.createVar("x_2"), + Predicate.createOperation(Predicate.createVar("x_1"), "+", Predicate.createLit("1", "int")))); + var.addInstance(instance2); + context.addSpecificVariable(instance2); + context.addRefinementInstanceToVariable("x", "x_2"); + + assertEquals("x_2", var.getLastInstance().get().getName(), "Latest instance should be x_2"); + } + + @Test + void testIfBranchCombination() { + // Scenario: Track variables through if-then-else branches + CtTypeReference intType = factory.Type().integerPrimitiveType(); + + Variable var = new Variable("x", intType, Predicate.createVar("x")); + context.addVarToContext(var); + + // Before if + context.variablesSetBeforeIf(); + + // Then branch: x = 10 + VariableInstance thenInstance = new VariableInstance("x_then", intType, + Predicate.createEquals(Predicate.createVar("x_then"), Predicate.createLit("10", "int"))); + var.addInstance(thenInstance); + context.variablesSetThenIf(); + + // Else branch: x = 20 + VariableInstance elseInstance = new VariableInstance("x_else", intType, + Predicate.createEquals(Predicate.createVar("x_else"), Predicate.createLit("20", "int"))); + var.addInstance(elseInstance); + context.variablesSetElseIf(); + + // Combine branches + Predicate condition = Predicate.createVar("condition"); + context.variablesNewIfCombination(); + context.variablesCombineFromIf(condition); + context.variablesFinishIfCombination(); + + // Should create combined instance with ITE predicate + assertTrue(context.hasVariable("x"), "Variable x should still exist"); + } + + @Test + void testComplexScenarioWithMultipleComponents() { + // Realistic scenario: Function with refinements and variables + CtTypeReference intType = factory.Type().integerPrimitiveType(); + + // Create function with precondition + RefinedFunction processFunc = new RefinedFunction(); + processFunc.setName("process"); + processFunc.setClass("Processor"); + processFunc.setType(intType); + + Predicate precondition = Predicate.createOperation(Predicate.createVar("input"), ">", + Predicate.createLit("0", "int")); + processFunc.addArgRefinements("input", intType, precondition); + + Predicate postcondition = Predicate.createOperation(Predicate.createVar("result"), ">=", + Predicate.createVar("input")); + processFunc.setRefReturn(postcondition); + + context.addFunctionToContext(processFunc); + + // Add variables with refinements + context.addVarToContext("input", intType, precondition, factory.createLiteral(0)); + context.addVarToContext("result", intType, postcondition, factory.createLiteral(0)); + + // Verify everything is integrated + assertNotNull(context.getFunction("process", "Processor"), "Function registered"); + assertTrue(context.hasVariable("input"), "Input variable exists"); + assertTrue(context.hasVariable("result"), "Result variable exists"); + + // Get all variables with supertypes (for subtyping checks) + List varsWithSupertypes = context.getAllVariablesWithSupertypes(); + assertNotNull(varsWithSupertypes, "Should return variables list"); + } + + @Test + void testGlobalVariableManagement() { + // Scenario: Global variables persist across context resets + CtTypeReference intType = factory.Type().integerPrimitiveType(); + + context.addGlobalVariableToContext("GLOBAL_CONST", intType, + Predicate.createEquals(Predicate.createVar("GLOBAL_CONST"), Predicate.createLit("42", "int"))); + + assertTrue(context.hasVariable("GLOBAL_CONST"), "Global variable should exist"); + + // Add local variable + context.addVarToContext("local", intType, new Predicate(), factory.createLiteral(0)); + // getAllVariables() only returns local/scoped variables, not global ones + assertEquals(1, context.getAllVariables().size(), "Should have 1 local variable"); + // Verify both variables are accessible via hasVariable + assertTrue(context.hasVariable("GLOBAL_CONST"), "Global variable accessible"); + assertTrue(context.hasVariable("local"), "Local variable accessible"); + + // Reinitialize context (not all) + context.reinitializeContext(); + + assertTrue(context.hasVariable("GLOBAL_CONST"), "Global variable persists"); + assertFalse(context.hasVariable("local"), "Local variable removed"); + } + + @Test + void testCounterIncrement() { + // Verify counter is used for unique variable generation + int counter1 = context.getCounter(); + int counter2 = context.getCounter(); + int counter3 = context.getCounter(); + + assertTrue(counter2 > counter1, "Counter should increment"); + assertTrue(counter3 > counter2, "Counter should continue incrementing"); + assertEquals(1, counter2 - counter1, "Should increment by 1"); + } + + @Test + void testContextToString() { + // Test context string representation + CtTypeReference intType = factory.Type().integerPrimitiveType(); + context.addVarToContext("x", intType, new Predicate(), factory.createLiteral(0)); + + String result = context.toString(); + assertNotNull(result, "toString should not return null"); + assertTrue(result.contains("Variables"), "Should contain Variables section"); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/integration/PredicateExpressionIntegrationTest.java b/liquidjava-verifier/src/test/java/liquidjava/integration/PredicateExpressionIntegrationTest.java new file mode 100644 index 00000000..4d4708a9 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/integration/PredicateExpressionIntegrationTest.java @@ -0,0 +1,327 @@ +package liquidjava.integration; + +import static org.junit.jupiter.api.Assertions.*; + +import java.util.List; + +import liquidjava.processor.context.Context; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.*; +import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; + +import spoon.Launcher; + +/** + * Integration tests for Predicate and Expression classes working together Tests realistic scenarios of expression + * building, manipulation, and evaluation + */ +class PredicateExpressionIntegrationTest { + + @BeforeEach + void setUp() { + Launcher launcher = new Launcher(); + launcher.getFactory(); + Context.getInstance().reinitializeAllContext(); + } + + @Test + void testComplexPredicateConstruction() { + // Build: (x > 5 && y < 10) || (x == 0 && y == 0) + Predicate x = Predicate.createVar("x"); + Predicate y = Predicate.createVar("y"); + Predicate five = Predicate.createLit("5", "int"); + Predicate ten = Predicate.createLit("10", "int"); + Predicate zero = Predicate.createLit("0", "int"); + + Predicate xGreater5 = Predicate.createOperation(x, ">", five); + Predicate yLess10 = Predicate.createOperation(y, "<", ten); + Predicate leftBranch = Predicate.createConjunction(xGreater5, yLess10); + + Predicate xEquals0 = Predicate.createEquals(x, zero); + Predicate yEquals0 = Predicate.createEquals(y, zero); + Predicate rightBranch = Predicate.createConjunction(xEquals0, yEquals0); + + Predicate complex = Predicate.createDisjunction(leftBranch, rightBranch); + + String result = complex.toString(); + assertNotNull(result, "Should produce valid string"); + assertTrue(result.contains("x") && result.contains("y"), "Should contain both variables"); + assertTrue(result.contains("||"), "Should contain disjunction"); + assertTrue(result.contains("&&"), "Should contain conjunction"); + } + + @Test + void testVariableSubstitutionInComplexExpression() { + // Create: x + y * z + Predicate x = Predicate.createVar("x"); + Predicate y = Predicate.createVar("y"); + Predicate z = Predicate.createVar("z"); + + Predicate yTimesZ = Predicate.createOperation(y, "*", z); + Predicate expr = Predicate.createOperation(x, "+", yTimesZ); + + // Substitute x with a + Predicate substituted = expr.substituteVariable("x", "a"); + String result = substituted.toString(); + + assertTrue(result.contains("a"), "Should contain substituted variable"); + assertFalse(result.contains("x"), "Should not contain original variable"); + assertTrue(result.contains("y") && result.contains("z"), "Other variables unchanged"); + } + + @Test + void testExpressionCloningAndModification() { + // Create expression and clone it + Predicate original = Predicate.createOperation(Predicate.createVar("x"), "+", Predicate.createLit("10", "int")); + + Predicate cloned = original.clone(); + + // Modify clone + Predicate modified = cloned.substituteVariable("x", "y"); + + // Original should be unchanged + assertTrue(original.toString().contains("x"), "Original unchanged"); + assertTrue(modified.toString().contains("y"), "Clone modified"); + assertFalse(modified.toString().contains("x"), "Clone doesn't have old var"); + } + + @Test + void testNestedFunctionInvocations() { + // Create: outer(inner(x, y), z) + Predicate x = Predicate.createVar("x"); + Predicate y = Predicate.createVar("y"); + Predicate z = Predicate.createVar("z"); + + Predicate inner = Predicate.createInvocation("inner", x, y); + Predicate outer = Predicate.createInvocation("outer", inner, z); + + String result = outer.toString(); + assertTrue(result.contains("outer"), "Should contain outer function"); + assertTrue(result.contains("inner"), "Should contain inner function"); + assertTrue(result.contains("x") && result.contains("y") && result.contains("z"), + "Should contain all variables"); + } + + @Test + void testIfThenElsePredicates() { + // Create: if (x > 0) then x else -x + Predicate x = Predicate.createVar("x"); + Predicate zero = Predicate.createLit("0", "int"); + Predicate condition = Predicate.createOperation(x, ">", zero); + + Predicate negX = Predicate.createOperation(Predicate.createLit("-1", "int"), "*", x); + + Predicate ite = Predicate.createITE(condition, x, negX); + + assertNotNull(ite, "ITE predicate should be created"); + Expression iteExpr = ite.getExpression(); + assertTrue(iteExpr instanceof Ite, "Should be Ite expression"); + + Ite iteNode = (Ite) iteExpr; + assertNotNull(iteNode.getCondition(), "Should have condition"); + assertNotNull(iteNode.getThen(), "Should have then branch"); + assertNotNull(iteNode.getElse(), "Should have else branch"); + } + + @Test + void testOldVariableTracking() { + // Create: old(x) + y + Predicate oldX = Predicate.createInvocation("old", Predicate.createVar("x")); + Predicate y = Predicate.createVar("y"); + Predicate expr = Predicate.createOperation(oldX, "+", y); + + List oldVars = expr.getOldVariableNames(); + assertEquals(1, oldVars.size(), "Should have 1 old variable"); + assertTrue(oldVars.contains("x"), "Should contain x"); + + // Test changeOldMentions method executes + Predicate changed = expr.changeOldMentions("x", "newX"); + assertNotNull(changed, "Change should produce result"); + + // Verify original expression still accessible + assertNotNull(expr.getExpression(), "Original expression should exist"); + assertTrue(expr.toString().contains("old"), "Original should still contain old reference"); + } + + @Test + void testVariableNameExtraction() { + // Create complex expression and extract all variables + Predicate expr = Predicate.createOperation( + Predicate.createOperation(Predicate.createVar("a"), "+", Predicate.createVar("b")), "*", + Predicate.createOperation(Predicate.createVar("c"), "-", Predicate.createVar("d"))); + + List vars = expr.getVariableNames(); + assertEquals(4, vars.size(), "Should find 4 variables"); + assertTrue(vars.contains("a"), "Should contain a"); + assertTrue(vars.contains("b"), "Should contain b"); + assertTrue(vars.contains("c"), "Should contain c"); + assertTrue(vars.contains("d"), "Should contain d"); + } + + @Test + void testPredicateSimplificationIntegration() { + // Create: (2 + 3) * 4 - should simplify to 20 + Predicate two = Predicate.createLit("2", "int"); + Predicate three = Predicate.createLit("3", "int"); + Predicate four = Predicate.createLit("4", "int"); + + Predicate sum = Predicate.createOperation(two, "+", three); + Predicate product = Predicate.createOperation(sum, "*", four); + + ValDerivationNode simplified = product.simplify(); + assertNotNull(simplified, "Simplification should succeed"); + assertNotNull(simplified.getValue(), "Should have simplified value"); + } + + @Test + void testPredicateNegation() { + // Create predicate and negate it + Predicate x = Predicate.createVar("x"); + Predicate five = Predicate.createLit("5", "int"); + Predicate xGreater5 = Predicate.createOperation(x, ">", five); + + Predicate negated = xGreater5.negate(); + assertTrue(negated.toString().contains("!"), "Negated should contain !"); + + // Double negation + Predicate doubleNegated = negated.negate(); + assertTrue(doubleNegated.toString().contains("!"), "Should have negation operator"); + } + + @Test + void testBooleanLiteralPredicates() { + Predicate truePred = Predicate.createLit("true", "boolean"); + Predicate falsePred = Predicate.createLit("false", "boolean"); + + assertTrue(truePred.isBooleanTrue(), "True literal is boolean true"); + assertFalse(falsePred.isBooleanTrue(), "False literal is not boolean true"); + + // Combine with logic operators + Predicate andResult = Predicate.createConjunction(truePred, falsePred); + assertFalse(andResult.isBooleanTrue(), "true && false = false"); + + Predicate orResult = Predicate.createDisjunction(truePred, falsePred); + assertNotNull(orResult, "true || false should create valid predicate"); + } + + @Test + void testArithmeticWithVariablesAndConstants() { + // Create: (x * 2 + 5) / (y - 3) + Predicate x = Predicate.createVar("x"); + Predicate y = Predicate.createVar("y"); + Predicate two = Predicate.createLit("2", "int"); + Predicate five = Predicate.createLit("5", "int"); + Predicate three = Predicate.createLit("3", "int"); + + Predicate xTimes2 = Predicate.createOperation(x, "*", two); + Predicate numerator = Predicate.createOperation(xTimes2, "+", five); + + Predicate denominator = Predicate.createOperation(y, "-", three); + + Predicate division = Predicate.createOperation(numerator, "/", denominator); + + List vars = division.getVariableNames(); + assertEquals(2, vars.size(), "Should have x and y"); + + String result = division.toString(); + assertTrue(result.contains("x") && result.contains("y"), "Should contain both variables"); + assertTrue(result.contains("2") && result.contains("5") && result.contains("3"), + "Should contain all constants"); + } + + @Test + void testExpressionWithMixedTypes() { + // Create expressions with different literal types + Predicate intVal = Predicate.createLit("42", "int"); + Predicate doubleVal = Predicate.createLit("3.14", "double"); + Predicate boolVal = Predicate.createLit("true", "boolean"); + Predicate longVal = Predicate.createLit("1000000", "long"); + + assertNotNull(intVal.getExpression(), "Int literal created"); + assertNotNull(doubleVal.getExpression(), "Double literal created"); + assertNotNull(boolVal.getExpression(), "Boolean literal created"); + assertNotNull(longVal.getExpression(), "Long literal created"); + + assertTrue(intVal.getExpression().isLiteral(), "Int is literal"); + assertTrue(doubleVal.getExpression().isLiteral(), "Double is literal"); + assertTrue(boolVal.getExpression().isLiteral(), "Boolean is literal"); + } + + @Test + void testComparisonOperations() { + // Test all comparison operators + Predicate x = Predicate.createVar("x"); + Predicate five = Predicate.createLit("5", "int"); + + Predicate eq = Predicate.createEquals(x, five); + Predicate lt = Predicate.createOperation(x, "<", five); + Predicate gt = Predicate.createOperation(x, ">", five); + Predicate lte = Predicate.createOperation(x, "<=", five); + Predicate gte = Predicate.createOperation(x, ">=", five); + Predicate neq = Predicate.createOperation(x, "!=", five); + + assertTrue(eq.toString().contains("=="), "Equals uses =="); + assertTrue(lt.toString().contains("<"), "Less than uses <"); + assertTrue(gt.toString().contains(">"), "Greater than uses >"); + assertTrue(lte.toString().contains("<="), "Less or equal uses <="); + assertTrue(gte.toString().contains(">="), "Greater or equal uses >="); + assertTrue(neq.toString().contains("!="), "Not equal uses !="); + } + + @Test + void testComplexSubstitutionScenario() { + // Scenario: Function call with arguments that need substitution + // Original: f(x, y) where we want to substitute x -> a+b and y -> c*d + Predicate a = Predicate.createVar("a"); + Predicate b = Predicate.createVar("b"); + Predicate c = Predicate.createVar("c"); + Predicate d = Predicate.createVar("d"); + + Predicate aPlusB = Predicate.createOperation(a, "+", b); + Predicate cTimesD = Predicate.createOperation(c, "*", d); + + // Create function invocation + Predicate func = Predicate.createInvocation("f", aPlusB, cTimesD); + + List vars = func.getVariableNames(); + assertTrue(vars.contains("a") && vars.contains("b") && vars.contains("c") && vars.contains("d"), + "Should contain all nested variables"); + } + + @Test + void testChainedOperations() { + // Create: a + b + c + d + Predicate a = Predicate.createVar("a"); + Predicate b = Predicate.createVar("b"); + Predicate c = Predicate.createVar("c"); + Predicate d = Predicate.createVar("d"); + + Predicate ab = Predicate.createOperation(a, "+", b); + Predicate abc = Predicate.createOperation(ab, "+", c); + Predicate abcd = Predicate.createOperation(abc, "+", d); + + List vars = abcd.getVariableNames(); + assertEquals(4, vars.size(), "Should have all 4 variables"); + + // Verify structure is maintained + Expression expr = abcd.getExpression(); + assertTrue(expr instanceof BinaryExpression, "Top level should be binary"); + assertTrue(expr.hasChildren(), "Should have children"); + } + + @Test + void testPredicateEquality() { + // Test that identical predicates are recognized + Predicate p1 = Predicate.createOperation(Predicate.createVar("x"), "+", Predicate.createLit("5", "int")); + Predicate p2 = Predicate.createOperation(Predicate.createVar("x"), "+", Predicate.createLit("5", "int")); + + assertEquals(p1.toString(), p2.toString(), "Identical predicates have same string form"); + + // Different predicates + Predicate p3 = Predicate.createOperation(Predicate.createVar("x"), "+", Predicate.createLit("6", "int")); + + assertNotEquals(p1.toString(), p3.toString(), "Different predicates have different strings"); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/integration/VerificationWorkflowIntegrationTest.java b/liquidjava-verifier/src/test/java/liquidjava/integration/VerificationWorkflowIntegrationTest.java new file mode 100644 index 00000000..107121d3 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/integration/VerificationWorkflowIntegrationTest.java @@ -0,0 +1,355 @@ +package liquidjava.integration; + +import static org.junit.jupiter.api.Assertions.*; + +import java.util.List; + +import liquidjava.processor.context.*; +import liquidjava.rj_language.Predicate; +import liquidjava.utils.Pair; +import liquidjava.utils.Utils; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; + +import spoon.Launcher; +import spoon.reflect.factory.Factory; +import spoon.reflect.reference.CtTypeReference; + +/** + * Integration tests for complete verification workflows Tests the interaction of utilities, context, predicates, and + * refinements in realistic scenarios + */ +class VerificationWorkflowIntegrationTest { + + private Context context; + private Factory factory; + + @BeforeEach + void setUp() { + Launcher launcher = new Launcher(); + factory = launcher.getFactory(); + context = Context.getInstance(); + context.reinitializeAllContext(); + } + + @Test + void testUtilityFunctionsIntegration() { + // Test Utils with Factory for type resolution + CtTypeReference intType = Utils.getType("int", factory); + CtTypeReference stringType = Utils.getType("String", factory); + CtTypeReference boolType = Utils.getType("boolean", factory); + + assertNotNull(intType, "Int type resolved"); + assertNotNull(stringType, "String type resolved"); + assertNotNull(boolType, "Boolean type resolved"); + + assertTrue(intType.isPrimitive(), "Int is primitive"); + assertFalse(stringType.isPrimitive(), "String is not primitive"); + + // Test name qualification + String qualified = Utils.qualifyName("com.example", "MyClass"); + assertEquals("com.example.MyClass", qualified); + + // Reserved names should not be qualified + assertEquals("old", Utils.qualifyName("com.example", "old")); + assertEquals("length", Utils.qualifyName("com.example", "length")); + + // Test simple name extraction + assertEquals("MyClass", Utils.getSimpleName("com.example.MyClass")); + assertEquals("MyClass", Utils.getSimpleName("MyClass")); + } + + @Test + void testPairUtility() { + // Test Pair utility class in context of verification + Pair> varTypePair = new Pair<>("x", factory.Type().integerPrimitiveType()); + + assertEquals("x", varTypePair.getFirst()); + assertNotNull(varTypePair.getSecond()); + + // Use in a map scenario + List> argPairs = List.of(new Pair<>("arg1", "int"), new Pair<>("arg2", "String"), + new Pair<>("arg3", "boolean")); + + assertEquals(3, argPairs.size()); + assertEquals("arg1", argPairs.get(0).getFirst()); + assertEquals("int", argPairs.get(0).getSecond()); + } + + @Test + void testFunctionPreconditionPostconditionWorkflow() { + // Complete workflow: Define function with pre/post conditions and verify + CtTypeReference intType = factory.Type().integerPrimitiveType(); + + // Create function: int divide(int x, int y) with precondition y != 0 + RefinedFunction divideFunc = new RefinedFunction(); + divideFunc.setName("divide"); + divideFunc.setClass("MathUtils"); + divideFunc.setType(intType); + + // Precondition: y != 0 + Predicate yNotZero = Predicate.createOperation(Predicate.createVar("y"), "!=", Predicate.createLit("0", "int")); + + // Add arguments with refinements + divideFunc.addArgRefinements("x", intType, new Predicate()); + divideFunc.addArgRefinements("y", intType, yNotZero); + + // Postcondition: result * y == x (approximately) + Predicate postcondition = Predicate.createEquals( + Predicate.createOperation(Predicate.createVar("result"), "*", Predicate.createVar("y")), + Predicate.createVar("x")); + divideFunc.setRefReturn(postcondition); + + context.addFunctionToContext(divideFunc); + + // Verify function can be retrieved + RefinedFunction retrieved = context.getFunction("divide", "MathUtils", 2); + assertNotNull(retrieved, "Function should be retrievable"); + + List args = retrieved.getArguments(); + assertEquals(2, args.size(), "Should have 2 arguments"); + + // Verify second argument has the precondition + Variable yArg = args.get(1); + Predicate yRefinement = yArg.getRefinement(); + assertTrue(yRefinement.toString().contains("y"), "y refinement should reference y"); + assertTrue(yRefinement.toString().contains("0"), "y refinement should check for zero"); + } + + @Test + void testCompleteVariableRefinementWorkflow() { + // Scenario: Track variable through multiple assignments with refinement updates + CtTypeReference intType = factory.Type().integerPrimitiveType(); + + // Initial state: int x; + Variable x = new Variable("x", intType, new Predicate()); + context.addVarToContext(x); + + // Assignment 1: x = 5; + VariableInstance x1 = new VariableInstance("x_1", intType, + Predicate.createEquals(Predicate.createVar("x_1"), Predicate.createLit("5", "int"))); + x.addInstance(x1); + context.addSpecificVariable(x1); + context.addRefinementInstanceToVariable("x", "x_1"); + + // Verify refinement + assertTrue(context.hasVariable("x_1"), "Instance should be in context"); + + // Assignment 2: x = x + 10; + VariableInstance x2 = new VariableInstance("x_2", intType, Predicate.createEquals(Predicate.createVar("x_2"), + Predicate.createOperation(Predicate.createVar("x_1"), "+", Predicate.createLit("10", "int")))); + x.addInstance(x2); + context.addSpecificVariable(x2); + context.addRefinementInstanceToVariable("x", "x_2"); + + // At this point, x_2 should be x_1 + 10, which is 5 + 10 = 15 + assertEquals("x_2", x.getLastInstance().get().getName()); + + // Get all variables - should include x, x_1, x_2 + List allVars = context.getAllVariables(); + assertTrue(allVars.stream().anyMatch(v -> v.getName().equals("x"))); + } + + @Test + void testGhostStateVerificationWorkflow() { + // Scenario: Define ghost states and track state transitions + context.addGhostClass("Stack"); + + // Define states + List> emptyList = List.of(); + GhostState empty = new GhostState("isEmpty", emptyList, factory.Type().booleanPrimitiveType(), "Stack"); + empty.setRefinement( + Predicate.createEquals(Predicate.createInvocation("Stack.size", Predicate.createVar("this")), + Predicate.createLit("0", "int"))); + + GhostState nonEmpty = new GhostState("isNonEmpty", emptyList, factory.Type().booleanPrimitiveType(), "Stack"); + nonEmpty.setRefinement( + Predicate.createOperation(Predicate.createInvocation("Stack.size", Predicate.createVar("this")), ">", + Predicate.createLit("0", "int"))); + + context.addToGhostClass("Stack", empty); + context.addToGhostClass("Stack", nonEmpty); + + // Retrieve states + List states = context.getGhostState("Stack"); + assertEquals(2, states.size(), "Should have 2 states"); + + // Verify refinements are set + assertNotNull(states.get(0).getRefinement(), "First state should have refinement"); + assertNotNull(states.get(1).getRefinement(), "Second state should have refinement"); + } + + @Test + void testMethodOverloadingResolution() { + // Test resolution of overloaded methods + CtTypeReference intType = factory.Type().integerPrimitiveType(); + CtTypeReference stringType = factory.Type().stringType(); + + // Add overloaded methods: process(int), process(int, int), process(String) + RefinedFunction process1 = new RefinedFunction(); + process1.setName("process"); + process1.setClass("Processor"); + process1.setType(intType); + process1.addArgRefinements("x", intType, new Predicate()); + context.addFunctionToContext(process1); + + RefinedFunction process2 = new RefinedFunction(); + process2.setName("process"); + process2.setClass("Processor"); + process2.setType(intType); + process2.addArgRefinements("x", intType, new Predicate()); + process2.addArgRefinements("y", intType, new Predicate()); + context.addFunctionToContext(process2); + + RefinedFunction process3 = new RefinedFunction(); + process3.setName("process"); + process3.setClass("Processor"); + process3.setType(intType); + process3.addArgRefinements("s", stringType, new Predicate()); + context.addFunctionToContext(process3); + + // Resolve by arity + assertNotNull(context.getFunction("process", "Processor", 1), "Should find process(int)"); + assertNotNull(context.getFunction("process", "Processor", 2), "Should find process(int, int)"); + + List allWithName1 = context.getAllMethodsWithNameSize("process", 1); + List allWithName2 = context.getAllMethodsWithNameSize("process", 2); + + assertTrue(allWithName1.size() >= 2, "Should find at least 2 single-arg variants"); + assertEquals(1, allWithName2.size(), "Should find 1 two-arg variant"); + } + + @Test + void testScopedVariableLifetime() { + // Test variables in nested scopes with same names + CtTypeReference intType = factory.Type().integerPrimitiveType(); + + // Base scope x + context.addVarToContext("x", intType, Predicate.createLit("0", "int"), factory.createLiteral(0)); + assertEquals(1, context.getAllVariables().size()); + + // Enter scope 1 + context.enterContext(); + context.addVarToContext("x", intType, Predicate.createLit("1", "int"), factory.createLiteral(0)); + context.addVarToContext("y", intType, Predicate.createLit("2", "int"), factory.createLiteral(0)); + assertEquals(3, context.getAllVariables().size(), "Global x + scope1 x + scope1 y"); + + // Enter scope 2 + context.enterContext(); + context.addVarToContext("z", intType, Predicate.createLit("3", "int"), factory.createLiteral(0)); + assertEquals(4, context.getAllVariables().size()); + + // Exit scope 2 + context.exitContext(); + assertEquals(3, context.getAllVariables().size()); + + // Exit scope 1 + context.exitContext(); + assertEquals(1, context.getAllVariables().size()); + assertTrue(context.hasVariable("x"), "Base scope x remains"); + } + + @Test + void testComplexRefinementConjunction() { + // Build complex refinement from multiple conditions + Predicate x = Predicate.createVar("x"); + Predicate y = Predicate.createVar("y"); + Predicate z = Predicate.createVar("z"); + + // x > 0 + Predicate cond1 = Predicate.createOperation(x, ">", Predicate.createLit("0", "int")); + + // y < 100 + Predicate cond2 = Predicate.createOperation(y, "<", Predicate.createLit("100", "int")); + + // z == x + y + Predicate cond3 = Predicate.createEquals(z, Predicate.createOperation(x, "+", y)); + + // Combine: (x > 0) && (y < 100) && (z == x + y) + Predicate combined = Predicate.createConjunction(cond1, cond2); + combined = Predicate.createConjunction(combined, cond3); + + List vars = combined.getVariableNames(); + assertTrue(vars.contains("x") && vars.contains("y") && vars.contains("z"), + "Should contain all three variables"); + + String result = combined.toString(); + assertTrue(result.contains("&&"), "Should contain conjunction operators"); + } + + @Test + void testTypeResolutionWithArrays() { + // Test array type resolution through Utils + CtTypeReference intArray = Utils.getType("int[]", factory); + assertNotNull(intArray, "Int array type should be resolved"); + assertTrue(intArray.isArray(), "Should be array type"); + + // Use in context + context.addVarToContext("numbers", intArray, new Predicate(), factory.createLiteral(0)); + assertTrue(context.hasVariable("numbers"), "Array variable should be in context"); + + RefinedVariable var = context.getVariableByName("numbers"); + assertTrue(var.getType().isArray(), "Variable should have array type"); + } + + @Test + void testContextResetPreservesGlobals() { + // Verify context reinitialize preserves what it should + CtTypeReference intType = factory.Type().integerPrimitiveType(); + + // Add global variable + context.addGlobalVariableToContext("GLOBAL_MAX", intType, Predicate.createLit("100", "int")); + + // Add local variable + context.addVarToContext("local", intType, new Predicate(), factory.createLiteral(0)); + + // Add function + RefinedFunction func = new RefinedFunction(); + func.setName("test"); + func.setClass("TestClass"); + func.setType(intType); + context.addFunctionToContext(func); + + // Reinitialize (not all) + context.reinitializeContext(); + + // Check what persists + assertTrue(context.hasVariable("GLOBAL_MAX"), "Global variable persists"); + assertNotNull(context.getFunction("test", "TestClass"), "Function persists"); + assertFalse(context.hasVariable("local"), "Local variable cleared"); + } + + @Test + void testStringUtilityFunctions() { + // Test string utility functions + String stripped = Utils.stripParens("(expression)"); + assertEquals("expression", stripped, "Parens should be stripped"); + + String notStripped = Utils.stripParens("expression"); + assertEquals("expression", notStripped, "Non-paren string unchanged"); + + String emptyParens = Utils.stripParens("()"); + assertEquals("", emptyParens, "Empty parens result in empty string"); + } + + @Test + void testVariableInstanceParenting() { + // Test parent-child relationship between Variable and VariableInstance + CtTypeReference intType = factory.Type().integerPrimitiveType(); + + Variable parent = new Variable("x", intType, new Predicate()); + context.addVarToContext(parent); + + VariableInstance child = new VariableInstance("x_1", intType, + Predicate.createEquals(Predicate.createVar("x_1"), Predicate.createLit("5", "int"))); + + parent.addInstance(child); + context.addSpecificVariable(child); + context.addRefinementInstanceToVariable("x", "x_1"); + + // Verify relationship + Variable retrievedParent = context.getVariableFromInstance(child); + assertNotNull(retrievedParent, "Should find parent"); + assertEquals(parent, retrievedParent, "Parent should match"); + } +}