From b73bf7ae1a1c1c8b166d4823bb25fdd9a96d8e28 Mon Sep 17 00:00:00 2001
From: "google-labs-jules[bot]"
 <161369871+google-labs-jules[bot]@users.noreply.github.com>
Date: Fri, 23 Jan 2026 09:58:26 +0000
Subject: [PATCH] Implement Variable.div method with NPE fix and bounds
 propagation

- Fixed NullPointerException in `div` when safe/edge lists are null.
- Implemented correct handling for DomainValue.BOTTOM.
- Added logic to propagate `safe` and `edge` constraints from dividend to result, assuming integer division.
- Added `VariableTest` to verify `div` behavior.
---
 src/main/java/staticAnalyzer/Variable.java    | 33 ++++++------
 .../java/staticAnalyzer/VariableTest.java     | 54 +++++++++++++++++++
 2 files changed, 70 insertions(+), 17 deletions(-)
 create mode 100644 src/test/java/staticAnalyzer/VariableTest.java

diff --git a/src/main/java/staticAnalyzer/Variable.java b/src/main/java/staticAnalyzer/Variable.java
index 4777e6f..87f5adf 100644
--- a/src/main/java/staticAnalyzer/Variable.java
+++ b/src/main/java/staticAnalyzer/Variable.java
@@ -311,29 +311,28 @@ public Variable add( Variable v ) {
         return newLocal();
     }
 
-    public Variable div( Variable v ) { //@TODO
-        DomainValue dv;
-        if (   getDomainValue() == DomainValue.TOP
-          || v.getDomainValue() == DomainValue.TOP ) {
-            dv = DomainValue.TOP;
-        } else {
-            dv = DomainValue.GEQ0;
+    public Variable div( Variable v ) {
+        if (getDomainValue() == DomainValue.BOTTOM || v.getDomainValue() == DomainValue.BOTTOM) {
+            return new Variable(type, Kind.LOCAL, DomainValue.BOTTOM, Integer.MAX_VALUE, 0);
         }
-        Variable r = new Variable(v.type,Kind.LOCAL,dv
-                ,Integer.MAX_VALUE,0);
+
+        if (getDomainValue() == DomainValue.TOP || v.getDomainValue() == DomainValue.TOP) {
+            return new Variable(type, Kind.LOCAL, DomainValue.TOP, Integer.MAX_VALUE, 0);
+        }
+
+        Variable r = new Variable(type, Kind.LOCAL, DomainValue.GEQ0, Integer.MAX_VALUE, 0);
 
         // analyze safe and edge
-        Iterator i = safe.iterator();
-        while( i.hasNext() ) {
-            Variable s = (Variable)i.next();
-            if (v.safe.contains(s)) {
+        // For integer arithmetic: result = this / v.
+        // If this >= 0 and v >= 1, then result <= this.
+        // Propagate safe (strict upper bounds) and edge (inclusive upper bounds).
+        if (safe != null) {
+            for (Variable s : safe) {
                 r.addSafe(s);
             }
         }
-        i = edge.iterator();
-        while( i.hasNext() ) {
-            Variable s = (Variable)i.next();
-            if (v.edge.contains(s)) {
+        if (edge != null) {
+            for (Variable s : edge) {
                 r.addEdge(s);
             }
         }
diff --git a/src/test/java/staticAnalyzer/VariableTest.java b/src/test/java/staticAnalyzer/VariableTest.java
new file mode 100644
index 0000000..9c4e6a9
--- /dev/null
+++ b/src/test/java/staticAnalyzer/VariableTest.java
@@ -0,0 +1,54 @@
+package staticAnalyzer;
+
+import org.junit.jupiter.api.Test;
+import static org.junit.jupiter.api.Assertions.*;
+
+public class VariableTest {
+
+    @Test
+    public void testDivNPE() {
+        Variable v1 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.GEQ0, 1, 0);
+        Variable v2 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.GEQ0, 2, 0);
+
+        // This is expected to fail with NPE before fix
+        assertDoesNotThrow(() -> v1.div(v2), "div should not throw NPE even if safe/edge lists are null");
+    }
+
+    @Test
+    public void testDivLogic() {
+        Variable v1 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.GEQ0, 1, 0);
+        Variable v2 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.G0, 2, 0);
+
+        Variable s1 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.TOP, 3, 0);
+        Variable e1 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.TOP, 4, 0);
+
+        v1.addSafe(s1);
+        v1.addEdge(e1);
+
+        Variable res = v1.div(v2);
+
+        // Verify result is GEQ0
+        assertEquals(Variable.DomainValue.GEQ0, res.getDomainValue());
+
+        // Verify bounds propagation (v1 / v2 <= v1 < s1) => res < s1
+        assertTrue(res.isSafe(s1), "Result should be safe for s1");
+
+        // Verify bounds propagation (v1 / v2 <= v1 <= e1) => res <= e1
+        assertTrue(res.isEdge(e1), "Result should be edge for e1");
+    }
+
+    @Test
+    public void testDivBottom() {
+        Variable v1 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.BOTTOM, 1, 0);
+        Variable v2 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.GEQ0, 2, 0);
+
+        Variable res = v1.div(v2);
+        assertEquals(Variable.DomainValue.BOTTOM, res.getDomainValue());
+
+        Variable v3 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.GEQ0, 3, 0);
+        Variable v4 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.BOTTOM, 4, 0);
+
+        Variable res2 = v3.div(v4);
+        assertEquals(Variable.DomainValue.BOTTOM, res2.getDomainValue());
+    }
+}