Additional units for unit checker; fixes #4116

checker-qual/src/main/java/org/checkerframework/checker/units/qual/Volume.java

@@ -0,0 +1,19 @@
+package org.checkerframework.checker.units.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+/**
+ * Units of volume.
+ *
+ * @checker_framework.manual #units-checker Units Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf(UnknownUnits.class)
+public @interface Volume {}

checker-qual/src/main/java/org/checkerframework/checker/units/qual/km3.java

@@ -0,0 +1,20 @@
+package org.checkerframework.checker.units.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+/**
+ * Cubic kilometer.
+ *
+ * @checker_framework.manual #units-checker Units Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf(Volume.class)
+@SuppressWarnings("checkstyle:typename")
+public @interface km3 {}

checker-qual/src/main/java/org/checkerframework/checker/units/qual/m3.java

@@ -0,0 +1,20 @@
+package org.checkerframework.checker.units.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+/**
+ * Cubic meter.
+ *
+ * @checker_framework.manual #units-checker Units Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf(Volume.class)
+@SuppressWarnings("checkstyle:typename")
+public @interface m3 {}

checker-qual/src/main/java/org/checkerframework/checker/units/qual/mm3.java

@@ -0,0 +1,20 @@
+package org.checkerframework.checker.units.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+/**
+ * Cubic millimeter.
+ *
+ * @checker_framework.manual #units-checker Units Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf(Volume.class)
+@SuppressWarnings("checkstyle:typename")
+public @interface mm3 {}

checker-util/src/main/java/org/checkerframework/checker/units/util/UnitsTools.java

@@ -10,14 +10,17 @@
 import org.checkerframework.checker.units.qual.kg;
 import org.checkerframework.checker.units.qual.km;
 import org.checkerframework.checker.units.qual.km2;
+import org.checkerframework.checker.units.qual.km3;
 import org.checkerframework.checker.units.qual.kmPERh;
 import org.checkerframework.checker.units.qual.m;
 import org.checkerframework.checker.units.qual.m2;
+import org.checkerframework.checker.units.qual.m3;
 import org.checkerframework.checker.units.qual.mPERs;
 import org.checkerframework.checker.units.qual.mPERs2;
 import org.checkerframework.checker.units.qual.min;
 import org.checkerframework.checker.units.qual.mm;
 import org.checkerframework.checker.units.qual.mm2;
+import org.checkerframework.checker.units.qual.mm3;
 import org.checkerframework.checker.units.qual.mol;
 import org.checkerframework.checker.units.qual.radians;
 import org.checkerframework.checker.units.qual.s;
@@ -49,6 +52,11 @@ public class UnitsTools {
     public static final @m2 int m2 = 1;
     public static final @km2 int km2 = 1;
 
+    // Volume
+    public static final @mm3 int mm3 = 1;
+    public static final @m3 int m3 = 1;
+    public static final @km3 int km3 = 1;
+
     // Current
     public static final @A int A = 1;
 

checker/src/main/java/org/checkerframework/checker/units/UnitsRelationsDefault.java

@@ -7,19 +7,22 @@
 import org.checkerframework.checker.units.qual.Prefix;
 import org.checkerframework.checker.units.qual.h;
 import org.checkerframework.checker.units.qual.km2;
+import org.checkerframework.checker.units.qual.km3;
 import org.checkerframework.checker.units.qual.kmPERh;
 import org.checkerframework.checker.units.qual.m;
 import org.checkerframework.checker.units.qual.m2;
+import org.checkerframework.checker.units.qual.m3;
 import org.checkerframework.checker.units.qual.mPERs;
 import org.checkerframework.checker.units.qual.mPERs2;
 import org.checkerframework.checker.units.qual.mm2;
+import org.checkerframework.checker.units.qual.mm3;
 import org.checkerframework.checker.units.qual.s;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 
 /** Default relations between SI units. */
 public class UnitsRelationsDefault implements UnitsRelations {
     /** SI units. */
-    protected AnnotationMirror m, km, mm, m2, km2, mm2, s, h, mPERs, kmPERh, mPERs2;
+    protected AnnotationMirror m, km, mm, m2, km2, mm2, m3, km3, mm3, s, h, mPERs, kmPERh, mPERs2;
     /** The Element Utilities from the Units Checker's processing environment. */
     protected Elements elements;
 
@@ -39,6 +42,10 @@ public UnitsRelations init(ProcessingEnvironment env) {
         km2 = UnitsRelationsTools.buildAnnoMirrorWithNoPrefix(env, km2.class);
         mm2 = UnitsRelationsTools.buildAnnoMirrorWithNoPrefix(env, mm2.class);
 
+        m3 = UnitsRelationsTools.buildAnnoMirrorWithNoPrefix(env, m3.class);
+        km3 = UnitsRelationsTools.buildAnnoMirrorWithNoPrefix(env, km3.class);
+        mm3 = UnitsRelationsTools.buildAnnoMirrorWithNoPrefix(env, mm3.class);
+
         s = UnitsRelationsTools.buildAnnoMirrorWithDefaultPrefix(env, s.class);
         h = UnitsRelationsTools.buildAnnoMirrorWithNoPrefix(env, h.class);
 
@@ -83,6 +90,12 @@ public UnitsRelations init(ProcessingEnvironment env) {
             } else {
                 return null;
             }
+        } else if (havePairOfUnitsIgnoringOrder(lht, m, rht, m2)) {
+            return m3;
+        } else if (havePairOfUnitsIgnoringOrder(lht, km, rht, km2)) {
+            return km3;
+        } else if (havePairOfUnitsIgnoringOrder(lht, mm, rht, mm2)) {
+            return mm3;
         } else if (havePairOfUnitsIgnoringOrder(lht, s, rht, mPERs)) {
             // s * mPERs or mPERs * s => m
             return m;
@@ -118,6 +131,24 @@ public UnitsRelations init(ProcessingEnvironment env) {
         } else if (havePairOfUnits(lht, mm2, rht, mm)) {
             // mm2 / mm => mm
             return mm;
+        } else if (havePairOfUnits(lht, m3, rht, m)) {
+            // m3 / m => m2
+            return m2;
+        } else if (havePairOfUnits(lht, km3, rht, km)) {
+            // km3 / km => km2
+            return km2;
+        } else if (havePairOfUnits(lht, mm3, rht, mm)) {
+            // mm3 / mm => mm2
+            return mm2;
+        } else if (havePairOfUnits(lht, m3, rht, m2)) {
+            // m3 / m2 => m
+            return m;
+        } else if (havePairOfUnits(lht, km3, rht, km2)) {
+            // km3 / km2 => km
+            return km;
+        } else if (havePairOfUnits(lht, mm3, rht, mm2)) {
+            // mm3 / mm2 => mm
+            return mm;
         } else if (havePairOfUnits(lht, m, rht, mPERs)) {
             // m / mPERs => s
             return s;

checker/tests/units/Addition.java

@@ -16,14 +16,17 @@
 import org.checkerframework.checker.units.qual.kg;
 import org.checkerframework.checker.units.qual.km;
 import org.checkerframework.checker.units.qual.km2;
+import org.checkerframework.checker.units.qual.km3;
 import org.checkerframework.checker.units.qual.kmPERh;
 import org.checkerframework.checker.units.qual.m;
 import org.checkerframework.checker.units.qual.m2;
+import org.checkerframework.checker.units.qual.m3;
 import org.checkerframework.checker.units.qual.mPERs;
 import org.checkerframework.checker.units.qual.mPERs2;
 import org.checkerframework.checker.units.qual.min;
 import org.checkerframework.checker.units.qual.mm;
 import org.checkerframework.checker.units.qual.mm2;
+import org.checkerframework.checker.units.qual.mm3;
 import org.checkerframework.checker.units.qual.mol;
 import org.checkerframework.checker.units.qual.s;
 import org.checkerframework.checker.units.util.UnitsTools;
@@ -77,6 +80,11 @@ void good() {
         @km2 int bSquareKilometer = 5 * UnitsTools.km2;
         @km2 int sSquareKilometer = aSquareKilometer + bSquareKilometer;
 
+        // Cubic kilometer
+        @km3 int aCubicKilometer = 5 * UnitsTools.km3;
+        @km3 int bCubicKilometer = 5 * UnitsTools.km3;
+        @km3 int sCubicKilometer = aCubicKilometer + bCubicKilometer;
+
         // Kilometer per hour
         @kmPERh int aKilometerPerHour = 5 * UnitsTools.kmPERh;
         @kmPERh int bKilometerPerHour = 5 * UnitsTools.kmPERh;
@@ -92,6 +100,11 @@ void good() {
         @m2 int bSquareMeter = 5 * UnitsTools.m2;
         @m2 int sSquareMeter = aSquareMeter + bSquareMeter;
 
+        // Cubic meter
+        @m3 int aCubicMeter = 5 * UnitsTools.m3;
+        @m3 int bCubicMeter = 5 * UnitsTools.m3;
+        @m3 int sCubicMeter = aCubicMeter + bCubicMeter;
+
         // Meter per second
         @mPERs int aMeterPerSecond = 5 * UnitsTools.mPERs;
         @mPERs int bMeterPerSecond = 5 * UnitsTools.mPERs;
@@ -117,6 +130,11 @@ void good() {
         @mm2 int bSquareMillimeter = 5 * UnitsTools.mm2;
         @mm2 int sSquareMillimeter = aSquareMillimeter + bSquareMillimeter;
 
+        // Cubic millimeter
+        @mm3 int aCubicMillimeter = 5 * UnitsTools.mm3;
+        @mm3 int bCubicMillimeter = 5 * UnitsTools.mm3;
+        @mm3 int sCubicMillimeter = aCubicMillimeter + bCubicMillimeter;
+
         // Mole
         @mol int aMole = 5 * UnitsTools.mol;
         @mol int bMole = 5 * UnitsTools.mol;

checker/tests/units/BasicUnits.java

@@ -1,12 +1,15 @@
 import org.checkerframework.checker.units.qual.Area;
 import org.checkerframework.checker.units.qual.Prefix;
+import org.checkerframework.checker.units.qual.Volume;
 import org.checkerframework.checker.units.qual.degrees;
 import org.checkerframework.checker.units.qual.h;
 import org.checkerframework.checker.units.qual.km;
 import org.checkerframework.checker.units.qual.km2;
+import org.checkerframework.checker.units.qual.km3;
 import org.checkerframework.checker.units.qual.kmPERh;
 import org.checkerframework.checker.units.qual.m;
 import org.checkerframework.checker.units.qual.m2;
+import org.checkerframework.checker.units.qual.m3;
 import org.checkerframework.checker.units.qual.mPERs;
 import org.checkerframework.checker.units.qual.mPERs2;
 import org.checkerframework.checker.units.qual.radians;
@@ -60,6 +63,15 @@ void demo() {
         // :: error: (assignment.type.incompatible)
         @km2 int bae1 = m * m;
 
+        @Volume int vol = m * m * m;
+        @m3 int gvol = m * m * m;
+
+        // :: error: (assignment.type.incompatible)
+        @Volume int bvol = m * m * m * m;
+
+        // :: error: (assignment.type.incompatible)
+        @km3 int bvol1 = m * m * m;
+
         @radians double rad = 20.0d * UnitsTools.rad;
         @degrees double deg = 30.0d * UnitsTools.deg;
 

checker/tests/units/Division.java

@@ -1,13 +1,16 @@
 import org.checkerframework.checker.units.qual.h;
 import org.checkerframework.checker.units.qual.km;
 import org.checkerframework.checker.units.qual.km2;
+import org.checkerframework.checker.units.qual.km3;
 import org.checkerframework.checker.units.qual.kmPERh;
 import org.checkerframework.checker.units.qual.m;
 import org.checkerframework.checker.units.qual.m2;
+import org.checkerframework.checker.units.qual.m3;
 import org.checkerframework.checker.units.qual.mPERs;
 import org.checkerframework.checker.units.qual.mPERs2;
 import org.checkerframework.checker.units.qual.mm;
 import org.checkerframework.checker.units.qual.mm2;
+import org.checkerframework.checker.units.qual.mm3;
 import org.checkerframework.checker.units.qual.s;
 import org.checkerframework.checker.units.util.UnitsTools;
 
@@ -37,6 +40,9 @@ void d() {
         @mPERs int mPERs = 20 * UnitsTools.mPERs;
         @kmPERh int kmPERh = 2 * UnitsTools.kmPERh;
         @mPERs2 int mPERs2 = 30 * UnitsTools.mPERs2;
+        @m3 int m3 = 125 * UnitsTools.m3;
+        @km3 int km3 = 27 * UnitsTools.km3;
+        @mm3 int mm3 = 64 * UnitsTools.mm3;
 
         // m / s = mPERs
         @mPERs int velocitym = m / s;
@@ -63,6 +69,21 @@ void d() {
         // :: error: (assignment.type.incompatible)
         distancemm = km2 / mm;
 
+        // m3 / m2 = m
+        distancem = m3 / m2;
+        // :: error: (assignment.type.incompatible)
+        distancem = m3 / km2;
+
+        // km3 / km2 = km
+        distancekm = km3 / km2;
+        // :: error: (assignment.type.incompatible)
+        distancekm = km3 / m2;
+
+        // mm3 / mm2 = mm
+        distancemm = mm3 / mm2;
+        // :: error: (assignment.type.incompatible)
+        distancemm = km3 / mm2;
+
         // m / mPERs = s
         @s int times = m / mPERs;
         // :: error: (assignment.type.incompatible)

checker/tests/units/Multiples.java

@@ -4,13 +4,16 @@
 import org.checkerframework.checker.units.qual.kg;
 import org.checkerframework.checker.units.qual.km;
 import org.checkerframework.checker.units.qual.km2;
+import org.checkerframework.checker.units.qual.km3;
 import org.checkerframework.checker.units.qual.kmPERh;
 import org.checkerframework.checker.units.qual.m;
 import org.checkerframework.checker.units.qual.m2;
+import org.checkerframework.checker.units.qual.m3;
 import org.checkerframework.checker.units.qual.mPERs;
 import org.checkerframework.checker.units.qual.mPERs2;
 import org.checkerframework.checker.units.qual.mm;
 import org.checkerframework.checker.units.qual.mm2;
+import org.checkerframework.checker.units.qual.mm3;
 import org.checkerframework.checker.units.qual.s;
 import org.checkerframework.checker.units.util.UnitsTools;
 
@@ -89,6 +92,48 @@ void m() {
         // :: error: (assignment.type.incompatible)
         @km2 int areammbad2 = mm * mm;
 
+        // m * m2 = m3
+        @m3 int volume = m * area;
+        // :: error: (assignment.type.incompatible)
+        @km3 int volumembad1 = m * area;
+        // :: error: (assignment.type.incompatible)
+        @mm3 int volumembad2 = m * area;
+
+        // km * km2 = km3
+        @km3 int kvolume = km * karea;
+        // :: error: (assignment.type.incompatible)
+        @m3 int volumekmbad1 = km * karea;
+        // :: error: (assignment.type.incompatible)
+        @mm3 int volumekmbad2 = km * karea;
+
+        // mm * mm2 = mm3
+        @mm3 int mvolume = mm * marea;
+        // :: error: (assignment.type.incompatible)
+        @m3 int volumemmbad1 = mm * marea;
+        // :: error: (assignment.type.incompatible)
+        @km3 int volumemmbad2 = mm * marea;
+
+        // m2 * m = m3
+        volume = area * m;
+        // :: error: (assignment.type.incompatible)
+        volumembad1 = area * m;
+        // :: error: (assignment.type.incompatible)
+        volumembad2 = area * m;
+
+        // km2 * km = km3
+        kvolume = karea * km;
+        // :: error: (assignment.type.incompatible)
+        volumekmbad1 = karea * km;
+        // :: error: (assignment.type.incompatible)
+        volumekmbad2 = karea * km;
+
+        // mm2 * mm = mm3
+        mvolume = marea * mm;
+        // :: error: (assignment.type.incompatible)
+        volumemmbad1 = marea * mm;
+        // :: error: (assignment.type.incompatible)
+        volumemmbad2 = marea * mm;
+
         // s * mPERs = m
         @mPERs int speedm = 10 * UnitsTools.mPERs;
         @m int lengthm = s * speedm;