Change handling of strings

Ref. #291

rflx/expression.py

@@ -2057,11 +2057,15 @@ def simplified(self) -> Expr:
         return self
 
     def z3expr(self) -> z3.ExprRef:
-        raise NotImplementedError
+        return z3.BoolVal(False)
 
     def validate(self, declarations: Mapping[ID, Declaration]) -> None:
         pass
 
+    @property
+    def aggregate(self) -> Aggregate:
+        return Aggregate(*[Number(ord(c)) for c in self.data])
+
 
 def substitution(
     mapping: Mapping[Name, Expr], func: Callable[["Expr"], "Expr"] = None

rflx/generator/common.py

@@ -1,4 +1,4 @@
-from typing import Callable, Mapping, Sequence
+from typing import Callable, Mapping, Sequence, Union
 
 from rflx.ada import (
     Assignment,
@@ -39,6 +39,7 @@
     Relation,
     Selected,
     Size,
+    String,
     Sub,
     Val,
     ValidChecksum,
@@ -73,7 +74,8 @@ def substitution(
     facts = substitution_facts(message, embedded, public, target_type)
 
     def func(expression: Expr) -> Expr:
-        def byte_aggregate(aggregate: Aggregate) -> Aggregate:
+        def byte_aggregate(expression: Union[Aggregate, String]) -> Aggregate:
+            aggregate = expression.aggregate if isinstance(expression, String) else expression
             return Aggregate(*[Val(const.TYPES_BYTE, e) for e in aggregate.elements])
 
         if isinstance(expression, Name) and expression in facts:
@@ -82,10 +84,14 @@ def byte_aggregate(aggregate: Aggregate) -> Aggregate:
         if isinstance(expression, (Equal, NotEqual)):
             field = None
             aggregate = None
-            if isinstance(expression.left, Variable) and isinstance(expression.right, Aggregate):
+            if isinstance(expression.left, Variable) and isinstance(
+                expression.right, (Aggregate, String)
+            ):
                 field = Field(expression.left.name)
                 aggregate = byte_aggregate(expression.right)
-            elif isinstance(expression.left, Aggregate) and isinstance(expression.right, Variable):
+            elif isinstance(expression.left, (Aggregate, String)) and isinstance(
+                expression.right, Variable
+            ):
                 field = Field(expression.right.name)
                 aggregate = byte_aggregate(expression.left)
             if field and aggregate:

rflx/model.py

@@ -35,6 +35,7 @@
     Pow,
     ProofResult,
     Relation,
+    String,
     Sub,
     ValidChecksum,
     ValueRange,
@@ -1093,7 +1094,7 @@ def resolve_type(expr: Expr) -> Optional[TypeExpr]:
 
         def invalid_relation(left: TypeExpr, right: TypeExpr) -> bool:
             return (
-                (isinstance(left, Opaque) and not isinstance(right, (Opaque, Aggregate)))
+                (isinstance(left, Opaque) and not isinstance(right, (Opaque, Aggregate, String)))
                 or (isinstance(left, Array) and not isinstance(right, (Array, Aggregate)))
                 or (isinstance(left, Aggregate) and not isinstance(right, Composite))
             )

rflx/parser/grammar.py

@@ -54,6 +54,7 @@
     Or,
     Pow,
     Relation,
+    String,
     Sub,
     ValidChecksum,
     ValueRange,
@@ -143,6 +144,12 @@ def numeric_literal() -> Token:
     )
 
 
+def string_literal() -> Token:
+    return locatedExpr(QuotedString('"')).setParseAction(
+        lambda s, l, t: String(t[0][1], location=parser_location(t[0][0], t[0][2], s))
+    )
+
+
 def logical_expression() -> Token:
     relational_operator = (
         Keyword("<=") | Keyword(">=") | Keyword("=") | Keyword("/=") | Keyword("<") | Keyword(">")
@@ -176,12 +183,9 @@ def mathematical_expression() -> Token:
     )
     array_aggregate.setParseAction(parse_array_aggregate)
 
-    string = QuotedString('"')
-    string.setParseAction(parse_string)
-
     concatenation = (
         infixNotation(
-            array_aggregate | string,
+            array_aggregate | string_literal(),
             [(Suppress(Keyword("&")), 2, opAssoc.LEFT, parse_concatenation)],
             lpar=left_parenthesis(),
             rpar=right_parenthesis(),
@@ -429,14 +433,15 @@ def parse_array_aggregate(string: str, location: int, tokens: ParseResults) -> E
     return Aggregate(*tokens[1:-1], location=parser_location(tokens[0], tokens[-1], string))
 
 
-@fatalexceptions
-def parse_string(string: str, location: int, tokens: ParseResults) -> Expr:
-    return Aggregate(*[Number(ord(c)) for c in tokens[0]])
-
-
 @fatalexceptions
 def parse_concatenation(string: str, location: int, tokens: ParseResults) -> Expr:
-    return Aggregate(*[e for t in tokens[0] for e in t.elements])
+    aggregates = [t.aggregate if isinstance(t, String) else t for t in tokens[0]]
+    return Aggregate(
+        *[e for t in aggregates for e in t.elements],
+        location=Location(
+            tokens[0][0].location.start, tokens[0][0].location.source, tokens[0][-1].location.end
+        ),
+    )
 
 
 @fatalexceptions

tests/test_expression.py

@@ -1339,6 +1339,10 @@ def test_string_simplified() -> None:
     assert String("Test").simplified() == String("Test")
 
 
+def test_string_aggregate() -> None:
+    assert String("Test").aggregate == Aggregate(Number(84), Number(101), Number(115), Number(116))
+
+
 def test_selected_variables() -> None:
     result = Selected(Variable("X"), "Y").variables()
     expected = [Variable("X")]

tests/test_integration.py

@@ -139,6 +139,37 @@ def test_comparison_big_integers(condition: str) -> None:
     )
 
 
+@pytest.mark.parametrize(
+    "condition",
+    [
+        'A = "Foo Bar"',
+        "A /= (0, 1, 2, 3, 4, 5, 6)",
+        'A = "Foo" & (0) & "Bar"',
+        '"Foo Bar" /= A',
+        "(0, 1, 2, 3, 4, 5, 6) = A",
+        '"Foo" & (0) & "Bar" /= A',
+    ],
+)
+def test_comparison_opaque(condition: str) -> None:
+    assert_compilable_code_string(
+        f"""
+           package Test is
+
+              type M is
+                 message
+                    null
+                       then A
+                          with Length => 7 * 8;
+                    A : Opaque
+                       then null
+                          if {condition};
+                 end message;
+
+           end Test;
+        """
+    )
+
+
 def test_potential_name_conflicts_fields_literals() -> None:
     assert_compilable_code_string(
         """

tests/test_parser.py

@@ -24,6 +24,7 @@
     NotEqual,
     Number,
     Pow,
+    String,
     Sub,
     ValueRange,
     Variable,
@@ -186,8 +187,7 @@ def test_mathematical_expression_aggregate_no_number() -> None:
 
 def test_mathematical_expression_string() -> None:
     assert_equal(
-        grammar.mathematical_expression().parseString('"PNG"')[0],
-        Aggregate(Number(80), Number(78), Number(71)),
+        grammar.mathematical_expression().parseString('"PNG"')[0], String("PNG"),
     )