Set types in message conditions

ref #776

rflx/expression.py

@@ -1209,6 +1209,8 @@ def ada_expr(self) -> ada.Expr:
 
     @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
+        if self.type_ == rty.BOOLEAN:
+            return z3.Bool(self.name)
         if self.negative:
             return -z3.Int(self.name)
         return z3.Int(self.name)

rflx/model/message.py

@@ -155,6 +155,7 @@ def __init__(
                     self._state.parameter_types = {
                         f: t for f, t in self._types.items() if f not in fields
                     }
+                self._set_types()
             byte_order = byte_order if byte_order else ByteOrder.HIGH_ORDER_FIRST
             if not isinstance(byte_order, dict):
                 assert isinstance(byte_order, ByteOrder)
@@ -817,6 +818,33 @@ def _compute_path_condition(self, field: Field) -> expr.Expr:
             location=field.identifier.location,
         )
 
+    def _set_types(self) -> None:
+        def set_types(expression: expr.Expr) -> expr.Expr:
+            return self._typed_variable(expression, self.types)
+
+        for link in self.structure:
+            link.condition = link.condition.substituted(set_types)
+            link.size = link.size.substituted(set_types)
+            link.first = link.first.substituted(set_types)
+
+    def _typed_variable(self, expression: expr.Expr, types: Mapping[Field, mty.Type]) -> expr.Expr:
+        expression = copy(expression)
+        if isinstance(expression, expr.Variable):
+            assert expression.identifier not in {
+                *self._qualified_enum_literals,
+                *self._type_literals,
+            }, f'variable "{expression.identifier}" has the same name as a literal'
+            if expression.name.lower() == "message":
+                expression.type_ = rty.OPAQUE
+            elif Field(expression.identifier) in types:
+                expression.type_ = types[Field(expression.identifier)].type_
+        if isinstance(expression, expr.Literal):
+            if expression.identifier in self._qualified_enum_literals:
+                expression.type_ = self._qualified_enum_literals[expression.identifier].type_
+            elif expression.identifier in self._type_literals:
+                expression.type_ = self._type_literals[expression.identifier].type_
+        return expression
+
 
 class Message(AbstractMessage):
     # pylint: disable=too-many-arguments
@@ -989,9 +1017,6 @@ def size(
         the given field values.
         """
 
-        def typed_variable(expression: expr.Expr) -> expr.Expr:
-            return self._typed_variable(expression, self.types)
-
         field_values = field_values if field_values else {}
 
         if subpath:
@@ -1132,7 +1157,6 @@ def remove_variable_prefix(expression: expr.Expr) -> expr.Expr:
                     )
                     .substituted(mapping=to_mapping(link_size_expressions + facts))
                     .substituted(mapping=type_constraints)
-                    .substituted(typed_variable)
                     .substituted(add_message_prefix)
                     .substituted(remove_variable_prefix)
                     .simplified()
@@ -1141,7 +1165,6 @@ def remove_variable_prefix(expression: expr.Expr) -> expr.Expr:
                     expr.Size(expr.Variable(field.name, type_=self.types[field].type_))
                     .substituted(mapping=to_mapping(link_size_expressions + facts))
                     .substituted(mapping=type_constraints)
-                    .substituted(typed_variable)
                     .substituted(add_message_prefix)
                     .substituted(remove_variable_prefix)
                 )
@@ -1310,7 +1333,7 @@ def _verify_use_of_literals(self) -> None:
                     ]
                 )
 
-    def _verify_expression_types(self) -> None:
+    def _verify_expression_types(self) -> None:  # pylint: disable=too-many-branches
         types: dict[Field, mty.Type] = {}
 
         def typed_variable(expression: expr.Expr) -> expr.Expr:
@@ -1319,6 +1342,33 @@ def typed_variable(expression: expr.Expr) -> expr.Expr:
         for p in self.paths(FINAL):
             types = {f: t for f, t in self.types.items() if f in self.parameters}
             path = []
+            type_error = False
+
+            for l in p:
+                path.append(l.target)
+                for expression in [l.condition, l.size, l.first]:
+                    if expression == expr.UNDEFINED:
+                        continue
+
+                    error = expression.check_type(rty.Any())
+
+                    self.error.extend(error)
+
+                    if error.check():
+                        self.error.extend(
+                            [
+                                (
+                                    "on path " + " -> ".join(f.name for f in path),
+                                    Subsystem.MODEL,
+                                    Severity.INFO,
+                                    expression.location,
+                                )
+                            ],
+                        )
+                        type_error = True
+
+            if type_error:
+                break
 
             try:
                 # check for contradictions in conditions of path
@@ -1328,7 +1378,27 @@ def typed_variable(expression: expr.Expr) -> expr.Expr:
             except expr.Z3TypeError:
                 pass
 
+            path = []
+            untyped_path = []
+
+            def remove_types(expression: expr.Expr) -> expr.Expr:
+                if isinstance(expression, expr.Variable):
+                    expression = copy(expression)
+                    expression.type_ = rty.Undefined()
+                return expression
+
             for l in p:
+                untyped_path.append(
+                    Link(
+                        source=l.source,
+                        target=l.target,
+                        condition=l.condition.substituted(remove_types),
+                        first=l.first.substituted(remove_types),
+                        size=l.size.substituted(remove_types),
+                    )
+                )
+
+            for l in untyped_path:
                 path.append(l.target)
 
                 if l.source in self.types:
@@ -2056,24 +2126,6 @@ def _link_expressions(self, link: Link, ignore_implicit_sizes: bool = False) ->
             *expression_list(link.condition),
         ]
 
-    def _typed_variable(self, expression: expr.Expr, types: Mapping[Field, mty.Type]) -> expr.Expr:
-        expression = copy(expression)
-        if isinstance(expression, expr.Variable):
-            assert expression.identifier not in {
-                *self._qualified_enum_literals,
-                *self._type_literals,
-            }, f'variable "{expression.identifier}" has the same name as a literal'
-            if expression.name.lower() == "message":
-                expression.type_ = rty.OPAQUE
-            elif Field(expression.identifier) in types:
-                expression.type_ = types[Field(expression.identifier)].type_
-        if isinstance(expression, expr.Literal):
-            if expression.identifier in self._qualified_enum_literals:
-                expression.type_ = self._qualified_enum_literals[expression.identifier].type_
-            elif expression.identifier in self._type_literals:
-                expression.type_ = self._type_literals[expression.identifier].type_
-        return expression
-
 
 class DerivedMessage(Message):
     # pylint: disable=too-many-arguments
@@ -2178,7 +2230,7 @@ def merged(
 
             message = self._merge_inner_message(message, *inner_message, message_arguments)
 
-    def _merge_inner_message(
+    def _merge_inner_message(  # pylint: disable=too-many-locals
         self,
         message: UnprovenMessage,
         field: Field,
@@ -2199,6 +2251,9 @@ def _merge_inner_message(
         )
         structure = []
 
+        def set_types(expression: expr.Expr) -> expr.Expr:
+            return self._typed_variable(expression, inner_message.types)
+
         for path in message.paths(FINAL):
             for link in path:
                 if link.target == field:
@@ -2222,6 +2277,7 @@ def _merge_inner_message(
                         merged_condition = expr.And(
                             link.condition, final_link.condition
                         ).substituted(mapping=substitution)
+                        merged_condition = merged_condition.substituted(set_types)
                         proof = merged_condition.check(
                             [
                                 *inner_message.message_constraints(),

rflx/model/type_.py

@@ -181,8 +181,12 @@ def constraints(
     ) -> abc.Sequence[expr.Expr]:
         if proof:
             return [
-                expr.Less(expr.Variable(name), self._modulus, location=self.location),
-                expr.GreaterEqual(expr.Variable(name), expr.Number(0), location=self.location),
+                expr.Less(
+                    expr.Variable(name, type_=self.type_), self._modulus, location=self.location
+                ),
+                expr.GreaterEqual(
+                    expr.Variable(name, type_=self.type_), expr.Number(0), location=self.location
+                ),
                 expr.Equal(expr.Size(name), self.size, location=self.location),
             ]
 
@@ -344,8 +348,12 @@ def constraints(
     ) -> abc.Sequence[expr.Expr]:
         if proof:
             return [
-                expr.GreaterEqual(expr.Variable(name), self.first, location=self.location),
-                expr.LessEqual(expr.Variable(name), self.last, location=self.location),
+                expr.GreaterEqual(
+                    expr.Variable(name, type_=self.type_), self.first, location=self.location
+                ),
+                expr.LessEqual(
+                    expr.Variable(name, type_=self.type_), self.last, location=self.location
+                ),
                 expr.Equal(expr.Size(name), self.size, location=self.location),
             ]
 
@@ -531,14 +539,19 @@ def constraints(
             result: list[expr.Expr] = [
                 expr.Or(
                     *[
-                        expr.Equal(expr.Variable(name), expr.Literal(l), self.location)
+                        expr.Equal(
+                            expr.Variable(name, type_=self.type_), expr.Literal(l), self.location
+                        )
                         for l in literals
                     ],
                     location=self.location,
                 )
             ]
             result.extend(
-                [expr.Equal(expr.Literal(l), v, self.location) for l, v in literals.items()]
+                [
+                    expr.Equal(expr.Literal(l, type_=self.type_), v, self.location)
+                    for l, v in literals.items()
+                ]
             )
             result.append(expr.Equal(expr.Size(name), self.size, self.location))
             return result

tests/ide/ide_test.py

@@ -39,14 +39,14 @@ def test_multiple_errors() -> None:
         [
             f'{path}:6:9: parser: error: illegal prefix "RFLX" in package identifier'
             ' "RFLX_Invalid"',
-            f'{path}:297:5: parser: error: inconsistent package identifier "Inconsistent"',
+            f'{path}:298:5: parser: error: inconsistent package identifier "Inconsistent"',
             f'{path}:6:9: parser: info: previous identifier was "RFLX_Invalid"',
             f'{path}:6:9: parser: error: file name does not match unit name "RFLX_Invalid",'
             ' should be "rflx_invalid.rflx"',
             f'{path}:40:4: model: error: illegal redefinition of built-in type "Boolean"',
             f'{path}:6:9: parser: error: illegal prefix "RFLX" in package identifier'
             ' "RFLX_Invalid"',
-            f'{path}:297:5: parser: error: inconsistent package identifier "Inconsistent"',
+            f'{path}:298:5: parser: error: inconsistent package identifier "Inconsistent"',
             f'{path}:6:9: parser: info: previous identifier was "RFLX_Invalid"',
             f'{path}:6:9: parser: error: file name does not match unit name "RFLX_Invalid", should'
             ' be "rflx_invalid.rflx"',
@@ -105,58 +105,56 @@ def test_multiple_errors() -> None:
             f'{path}:134:21: parser: error: undefined base message "RFLX_Invalid::Ref1"'
             " in derived message",
             f'{path}:142:19: model: error: undefined variable "Undef_Var"',
-            f'{path}:144:23: model: error: undefined variable "F1"',
             f"{path}:142:19: model: info: on path Length -> Data",
-            f'{path}:148:19: model: error: undefined variable "F1"',
-            f"{path}:148:25: model: error: expected integer type",
-            f"{path}:148:25: model: info: found aggregate with element type universal integer"
+            f"{path}:149:25: model: error: expected integer type",
+            f"{path}:149:25: model: info: found aggregate with element type universal integer"
             " (5 .. 20)",
-            f"{path}:148:19: model: info: on path Length -> Data -> F1",
-            f'{path}:156:24: model: error: expected integer type "RFLX_Invalid::R" (5 .. 23)',
-            f"{path}:156:24: model: info: found aggregate with element type universal integer"
+            f"{path}:149:19: model: info: on path Length -> Data -> F1",
+            f'{path}:157:24: model: error: expected integer type "RFLX_Invalid::R" (5 .. 23)',
+            f"{path}:157:24: model: info: found aggregate with element type universal integer"
             " (1 .. 100)",
-            f"{path}:156:19: model: info: on path Length -> Data -> F1 -> F2 -> Final",
-            f'{path}:152:19: model: error: invalid use of size attribute for "1"',
-            f'{path}:168:10: model: error: name conflict for "F2_F1" in "RFLX_Invalid::M5"',
-            f'{path}:159:9: model: info: when merging message "RFLX_Invalid::M4"',
-            f'{path}:166:10: model: info: into field "F2"',
-            f'{path}:180:27: model: error: expected sequence type "RFLX_Invalid::R_Sequence"'
+            f"{path}:157:19: model: info: on path Length -> Data -> F1 -> F2 -> Final",
+            f'{path}:153:19: model: error: invalid use of size attribute for "1"',
+            f'{path}:169:10: model: error: name conflict for "F2_F1" in "RFLX_Invalid::M5"',
+            f'{path}:160:9: model: info: when merging message "RFLX_Invalid::M4"',
+            f'{path}:167:10: model: info: into field "F2"',
+            f'{path}:181:27: model: error: expected sequence type "RFLX_Invalid::R_Sequence"'
             ' with element integer type "RFLX_Invalid::R" (5 .. 23)',
-            f"{path}:180:27: model: info: found aggregate with element type universal integer"
+            f"{path}:181:27: model: info: found aggregate with element type universal integer"
             " (1 .. 1000)",
-            f"{path}:180:19: model: info: on path Length -> Data1 -> Data2",
-            f'{path}:184:27: model: error: expected sequence type "__INTERNAL__::Opaque"'
+            f"{path}:181:19: model: info: on path Length -> Data1 -> Data2",
+            f'{path}:185:27: model: error: expected sequence type "__INTERNAL__::Opaque"'
             ' with element integer type "Byte" (0 .. 255)',
-            f"{path}:184:27: model: info: found aggregate with element type universal integer"
+            f"{path}:185:27: model: info: found aggregate with element type universal integer"
             " (1 .. 1000)",
-            f"{path}:184:19: model: info: on path Length -> Data1 -> Data2 -> Final",
-            f'{path}:187:36: parser: error: undefined element type "RFLX_Invalid::M5"',
-            f'{path}:193:17: parser: error: undefined type "RFLX_Invalid::M5_Sequence"',
-            f'{path}:193:10: model: error: missing type for field "Data" in "RFLX_Invalid::M7"',
-            f'{path}:204:10: model: error: conflicting conditions for field "F1"',
-            f"{path}:208:19: model: info: condition 0 (F1 -> F2): F1 < 80",
-            f"{path}:206:19: model: info: condition 1 (F1 -> Final): F1 > 50",
-            f'{path}:216:10: model: error: unreachable field "F2" in "RFLX_Invalid::M9"',
-            f'{path}:231:18: model: error: fixed size field "F1" with size aspect',
-            f"{path}:241:30: model: error: illegal first aspect at initial link",
-            f'{path}:250:19: model: error: undefined variable "F1"',
-            f"{path}:250:19: model: info: on path F1",
-            f'{path}:257:18: model: error: negative size for field "F2" (F1 -> F2)',
-            f"{path}:257:18: model: error: size of opaque field "
+            f"{path}:185:19: model: info: on path Length -> Data1 -> Data2 -> Final",
+            f'{path}:188:36: parser: error: undefined element type "RFLX_Invalid::M5"',
+            f'{path}:194:17: parser: error: undefined type "RFLX_Invalid::M5_Sequence"',
+            f'{path}:194:10: model: error: missing type for field "Data" in "RFLX_Invalid::M7"',
+            f'{path}:205:10: model: error: conflicting conditions for field "F1"',
+            f"{path}:209:19: model: info: condition 0 (F1 -> F2): F1 < 80",
+            f"{path}:207:19: model: info: condition 1 (F1 -> Final): F1 > 50",
+            f'{path}:217:10: model: error: unreachable field "F2" in "RFLX_Invalid::M9"',
+            f'{path}:232:18: model: error: fixed size field "F1" with size aspect',
+            f"{path}:242:30: model: error: illegal first aspect at initial link",
+            f'{path}:251:19: model: error: undefined variable "F1"',
+            f"{path}:251:19: model: info: on path F1",
+            f'{path}:258:18: model: error: negative size for field "F2" (F1 -> F2)',
+            f"{path}:258:18: model: error: size of opaque field "
             f'"F2" not multiple of 8 bit (F1 -> F2)',
-            f'{path}:254:9: model: error: negative start for field "Final" (F1 -> F2 -> Final)',
-            f"{path}:257:18: model: info: unsatisfied \"F2'Last ="
+            f'{path}:255:9: model: error: negative start for field "Final" (F1 -> F2 -> Final)',
+            f"{path}:258:18: model: info: unsatisfied \"F2'Last ="
             " (F1'Last + 1 + (F1 - 2 ** 33)) - 1\"",
-            f"{path}:256:10: model: info: unsatisfied \"F1'Last = (Message'First + 32) - 1\"",
-            f'{path}:199:9: model: info: unsatisfied "F1 < 2 ** 32"',
-            f"{path}:260:10: model: info: unsatisfied \"F2'Last + 1 >= Message'First\"",
-            f'{path}:266:10: model: error: unconstrained field "F1" without size aspect',
-            f'{path}:272:9: model: error: field "F3" not congruent with overlaid field "F1"',
-            f"{path}:272:9: model: info: unsatisfied \"F1'First = Message'First\"",
-            f"{path}:274:10: model: info: unsatisfied \"F1'Last = (Message'First + 8) - 1\"",
-            f"{path}:276:13: model: info: unsatisfied \"(F1'First + 16) - 1 = F1'Last\"",
-            f'{path}:288:29: model: error: size aspect for final field in "RFLX_Invalid::M17"',
-            f"{path}:291:9: model: error: unnecessary always-valid aspect"
+            f"{path}:257:10: model: info: unsatisfied \"F1'Last = (Message'First + 32) - 1\"",
+            f'{path}:200:9: model: info: unsatisfied "F1 < 2 ** 32"',
+            f"{path}:261:10: model: info: unsatisfied \"F2'Last + 1 >= Message'First\"",
+            f'{path}:267:10: model: error: unconstrained field "F1" without size aspect',
+            f'{path}:273:9: model: error: field "F3" not congruent with overlaid field "F1"',
+            f"{path}:273:9: model: info: unsatisfied \"F1'First = Message'First\"",
+            f"{path}:275:10: model: info: unsatisfied \"F1'Last = (Message'First + 8) - 1\"",
+            f"{path}:277:13: model: info: unsatisfied \"(F1'First + 16) - 1 = F1'Last\"",
+            f'{path}:289:29: model: error: size aspect for final field in "RFLX_Invalid::M17"',
+            f"{path}:292:9: model: error: unnecessary always-valid aspect"
             ' on "Unnecessary_Always_Valid_Enum"',
             f'{path}:37:9: model: error: name conflict for type "RFLX_Invalid::R"',
             f'{path}:8:9: model: info: previous occurrence of "RFLX_Invalid::R"',