Compare boxed values by value in Java

aas_core_codegen/java/transpilation.py

@@ -4,6 +4,7 @@
 import io
 import textwrap
 from typing import (
+    Final,
     Tuple,
     List,
     Mapping,
@@ -158,6 +159,27 @@ def _is_parenthesized_is_instance(node: parse_tree.Node) -> bool:
     return isinstance(node, parse_tree.IsInstance) and len(node.classes) > 1
 
 
+#: Map the primitive types to the primitive Java types which unbox their values,
+#: see :py:meth:`Transpiler.transform_comparison`
+_UNBOXED_TYPE_BY_PRIMITIVE_TYPE: Final[
+    Mapping[intermediate_type_inference.PrimitiveType, str]
+] = {
+    intermediate_type_inference.PrimitiveType.BOOL: "boolean",
+    intermediate_type_inference.PrimitiveType.INT: "long",
+    intermediate_type_inference.PrimitiveType.FLOAT: "double",
+}
+
+#: List the nodes which are transpiled to Java primitives, and never to boxed values,
+#: see :py:meth:`Transpiler.transform_comparison`
+_CERTAINLY_PRIMITIVE_NODE_TYPES: Final = (
+    parse_tree.Constant,
+    parse_tree.Add,
+    parse_tree.Sub,
+    parse_tree.Mod,
+    parse_tree.Neg,
+)
+
+
 class Transpiler(
     parse_tree.RestrictedTransformer[Tuple[Optional[Stripped], Optional[Error]]]
 ):
@@ -647,12 +669,46 @@ def transform_comparison(
             parse_tree.Slice,
         )
 
-        if isinstance(node.left, no_parentheses_types) and isinstance(
-            node.right, no_parentheses_types
+        if not (
+            isinstance(node.left, no_parentheses_types)
+            and isinstance(node.right, no_parentheses_types)
         ):
-            return Stripped(f"{left} {comparator} {right}"), None
+            left = Stripped(f"({left})")
+            right = Stripped(f"({right})")
+
+        # NOTE (mristin):
+        # We represent the integers, the floats and the booleans as ``Long``'s,
+        # ``Double``'s and ``Boolean``'s in the arguments, the properties and
+        # the collections. The operators ``==`` and ``!=`` compare the references of
+        # two such boxed values, which are equal only by chance, *e.g.*, for
+        # the ``Long``'s between -128 and 127, which Java caches. Hence, we unbox
+        # the left operand, unless an operand is certainly a primitive already, as
+        # Java then unboxes the other operand itself.
+        if node.op in (parse_tree.Comparator.EQ, parse_tree.Comparator.NE):
+            left_primitive_type = intermediate_type_inference.try_primitive_type(
+                self.type_map[node.left]
+            )
+            right_primitive_type = intermediate_type_inference.try_primitive_type(
+                self.type_map[node.right]
+            )
+
+            unboxed_type = (
+                _UNBOXED_TYPE_BY_PRIMITIVE_TYPE.get(left_primitive_type, None)
+                if left_primitive_type is not None
+                else None
+            )
+
+            if (
+                unboxed_type is not None
+                and right_primitive_type is not None
+                and right_primitive_type
+                is not intermediate_type_inference.PrimitiveType.LENGTH
+                and not isinstance(node.left, _CERTAINLY_PRIMITIVE_NODE_TYPES)
+                and not isinstance(node.right, _CERTAINLY_PRIMITIVE_NODE_TYPES)
+            ):
+                left = Stripped(f"({unboxed_type}) {left}")
 
-        return Stripped(f"({left}) {comparator} ({right})"), None
+        return Stripped(f"{left} {comparator} {right}"), None
 
     @ensure(lambda result: (result[0] is not None) ^ (result[1] is not None))
     def transform_is_in(

dev/test_data/common_meta_models/list_of_primitives.py

@@ -60,6 +60,39 @@ def ints_are_unique(numbers: Sequence[int]) -> bool:
     return True
 
 
+@verification
+def contains_by_loop(number: int, numbers: Sequence[int]) -> bool:
+    """
+    Check whether :paramref:`number` is in :paramref:`numbers`, item by item.
+
+    Java boxes both :paramref:`number` and the items as ``Long``'s, so that ``==``
+    would compare their references. The test data looks up the numbers beyond -128
+    and 127 on purpose, as Java caches the boxed values in that range, and
+    the references would be equal by chance.
+    """
+    for other in numbers:
+        if other == number:
+            return True
+
+    return False
+
+
+@verification
+def floats_are_unique(numbers: Sequence[float]) -> bool:
+    """
+    Check that :paramref:`numbers` are unique by comparing them pair-wise.
+
+    Java boxes the items as ``Double``'s, so that ``==`` would compare their
+    references.
+    """
+    for i in range(0, len(numbers)):
+        for j in range(i + 1, len(numbers)):
+            if numbers[i] == numbers[j]:
+                return False
+
+    return True
+
+
 @verification
 def is_separator(text: str) -> bool:
     """Check whether :paramref:`text` is one of the separators."""
@@ -87,6 +120,14 @@ def contains_dot(text: str) -> bool:
     return "." in text
 
 
+@invariant(
+    lambda self: floats_are_unique(self.some_floats),
+    "Some floats must be unique.",
+)
+@invariant(
+    lambda self: not contains_by_loop(-500, self.some_ints),
+    "Some ints must not contain -500.",
+)
 @invariant(
     lambda self: all(not is_separator(text) for text in self.some_strings),
     "Some strings must not be separators.",

dev/test_data/intermediate/common_meta_models/list_of_primitives/expected_symbol_table.txt

@@ -421,6 +421,41 @@ SymbolTable(
                 original_node=...),
               original_node=...)"""),
           specified_for='Reference to ConcreteClass Something',
+          parsed=...),
+        Invariant(
+          description='Some ints must not contain -500.',
+          body=textwrap.dedent("""\
+            Not(
+              operand=FunctionCall(
+                name='contains_by_loop',
+                args=[
+                  Constant(
+                    value=-500,
+                    original_node=...),
+                  Member(
+                    instance=Name(
+                      identifier='self',
+                      original_node=...),
+                    name='some_ints',
+                    original_node=...)],
+                original_node=...),
+              original_node=...)"""),
+          specified_for='Reference to ConcreteClass Something',
+          parsed=...),
+        Invariant(
+          description='Some floats must be unique.',
+          body=textwrap.dedent("""\
+            FunctionCall(
+              name='floats_are_unique',
+              args=[
+                Member(
+                  instance=Name(
+                    identifier='self',
+                    original_node=...),
+                  name='some_floats',
+                  original_node=...)],
+              original_node=...)"""),
+          specified_for='Reference to ConcreteClass Something',
           parsed=...)],
       serialization=Serialization(
         with_model_type=False),
@@ -561,6 +596,80 @@ SymbolTable(
         postconditions=[]),
       parsed=...,
       arguments_by_name=...),
+    TranspilableVerification(
+      name='contains_by_loop',
+      visibility='PUBLIC',
+      arguments=[
+        Argument(
+          name='number',
+          type_annotation=PrimitiveTypeAnnotation(
+            a_type='INT',
+            parsed=...),
+          default=None,
+          mutable=False,
+          parsed=...),
+        Argument(
+          name='numbers',
+          type_annotation=ListTypeAnnotation(
+            items=PrimitiveTypeAnnotation(
+              a_type='INT',
+              parsed=...),
+            parsed=...),
+          default=None,
+          mutable=False,
+          parsed=...)],
+      returns=PrimitiveTypeAnnotation(
+        a_type='BOOL',
+        parsed=...),
+      description=DescriptionOfSignature(
+        summary='<paragraph>Check whether <ReferenceToArgument refuri="number">number</ReferenceToArgument> is in <ReferenceToArgument refuri="numbers">numbers</ReferenceToArgument>, item by item.</paragraph>',
+        remarks=[
+          textwrap.dedent("""\
+            <paragraph>Java boxes both <ReferenceToArgument refuri="number">number</ReferenceToArgument> and the items as <literal>Long</literal>'s, so that <literal>==</literal>
+            would compare their references. The test data looks up the numbers beyond -128
+            and 127 on purpose, as Java caches the boxed values in that range, and
+            the references would be equal by chance.</paragraph>""")],
+        arguments_by_name=[],
+        returns=None,
+        parsed=...),
+      contracts=Contracts(
+        preconditions=[],
+        snapshots=[],
+        postconditions=[]),
+      parsed=...,
+      arguments_by_name=...),
+    TranspilableVerification(
+      name='floats_are_unique',
+      visibility='PUBLIC',
+      arguments=[
+        Argument(
+          name='numbers',
+          type_annotation=ListTypeAnnotation(
+            items=PrimitiveTypeAnnotation(
+              a_type='FLOAT',
+              parsed=...),
+            parsed=...),
+          default=None,
+          mutable=False,
+          parsed=...)],
+      returns=PrimitiveTypeAnnotation(
+        a_type='BOOL',
+        parsed=...),
+      description=DescriptionOfSignature(
+        summary='<paragraph>Check that <ReferenceToArgument refuri="numbers">numbers</ReferenceToArgument> are unique by comparing them pair-wise.</paragraph>',
+        remarks=[
+          textwrap.dedent("""\
+            <paragraph>Java boxes the items as <literal>Double</literal>'s, so that <literal>==</literal> would compare their
+            references.</paragraph>""")],
+        arguments_by_name=[],
+        returns=None,
+        parsed=...),
+      contracts=Contracts(
+        preconditions=[],
+        snapshots=[],
+        postconditions=[]),
+      parsed=...,
+      arguments_by_name=...),
     TranspilableVerification(
       name='is_separator',
       visibility='PUBLIC',

dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/floats_not_unique.json

@@ -0,0 +1,10 @@
+{
+  "someBools": [],
+  "someInts": [],
+  "someFloats": [
+    2.5,
+    2.5
+  ],
+  "someStrings": [],
+  "someBytes": []
+}

dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/ints_contain_minus_500.json

@@ -0,0 +1,9 @@
+{
+  "someBools": [],
+  "someInts": [
+    -500
+  ],
+  "someFloats": [],
+  "someStrings": [],
+  "someBytes": []
+}

dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/floats_not_unique.xml

@@ -0,0 +1 @@
+<something xmlns="https://dummy.com"><someBools /><someInts /><someFloats><v>2.5</v><v>2.5</v></someFloats><someStrings /><someBytes /></something>

dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/ints_contain_minus_500.xml

@@ -0,0 +1 @@
+<something xmlns="https://dummy.com"><someBools /><someInts><v>-500</v></someInts><someFloats /><someStrings /><someBytes /></something>

dev/test_data/main/cpp/expected/list_of_primitives/expected_output/include/dummy/verification.hpp

@@ -234,6 +234,25 @@ bool IntsAreUnique(
   const std::vector<int64_t>& numbers
 );
 
+/// \brief Check whether \p number is in \p numbers, item by item.
+///
+/// Java boxes both \p number and the items as `Long`'s, so that `==`
+/// would compare their references. The test data looks up the numbers beyond -128
+/// and 127 on purpose, as Java caches the boxed values in that range, and
+/// the references would be equal by chance.
+bool ContainsByLoop(
+  int64_t number,
+  const std::vector<int64_t>& numbers
+);
+
+/// \brief Check that \p numbers are unique by comparing them pair-wise.
+///
+/// Java boxes the items as `Double`'s, so that `==` would compare their
+/// references.
+bool FloatsAreUnique(
+  const std::vector<double>& numbers
+);
+
 /// \brief Check whether \p text is one of the separators.
 bool IsSeparator(
   const std::wstring& text

dev/test_data/main/cpp/expected/list_of_primitives/expected_output/src/verification.cpp

@@ -92,6 +92,31 @@ bool IntsAreUnique(
   return true;
 }
 
+bool ContainsByLoop(
+  int64_t number,
+  const std::vector<int64_t>& numbers
+) {
+  for (int64_t other : numbers) {
+    if (other == number) {
+      return true;
+    }
+  }
+  return false;
+}
+
+bool FloatsAreUnique(
+  const std::vector<double>& numbers
+) {
+  for (size_t i = 0; i < numbers.size(); ++i) {
+    for (size_t j = i + (1); j < numbers.size(); ++j) {
+      if (numbers.at(i) == numbers.at(j)) {
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
 bool IsSeparator(
   const std::wstring& text
 ) {
@@ -304,6 +329,29 @@ bool Something_9(
   );
 }
 
+bool Something_10(
+  const void* value
+) {
+  const types::ISomething* that = (
+    static_cast<const types::ISomething*>(value)
+  );
+  return !verification::ContainsByLoop(
+    -500,
+    that->some_ints()
+  );
+}
+
+bool Something_11(
+  const void* value
+) {
+  const types::ISomething* that = (
+    static_cast<const types::ISomething*>(value)
+  );
+  return verification::FloatsAreUnique(
+    that->some_floats()
+  );
+}
+
 /**
  * Give out the checks of the values of the \p shape.
  */
@@ -351,6 +399,14 @@ const std::vector<Check>& ChecksOf(Shape shape) {
         {
           &Something_9,
           L"Some strings must not be separators."
+        },
+        {
+          &Something_10,
+          L"Some ints must not contain -500."
+        },
+        {
+          &Something_11,
+          L"Some floats must be unique."
         }
       };
       return checks;