Implement validity checks for case expressions

Ref. #907

rflx/expression.py

@@ -2775,20 +2775,135 @@ def _entity_name(expr: Expr) -> str:
 
 class Case(Expr):
     def __init__(
-        self, expr: Expr, choices: List[Tuple[List[StrID], Expr]], location: Location = None
+        self,
+        expr: Expr,
+        choices: List[Tuple[List[Union[ID, Number]], Expr]],
+        location: Location = None,
     ) -> None:
         super().__init__(rty.Undefined(), location)
         self.expr = expr
         self.choices = choices
 
     def _update_str(self) -> None:
-        data = ",\n".join(f"\n   when {' | '.join(map(str, c))} => {e}" for c, e in self.choices)
-        self._str = intern(f"(case {self.expr} is{data})")
+        data = ",\n".join(f"      when {' | '.join(map(str, c))} => {e}" for c, e in self.choices)
+        self._str = intern(f"(case {self.expr} is\n{data})")
+
+    def _check_enumeration(self) -> RecordFluxError:
+        assert isinstance(self.expr.type_, rty.Enumeration)
+        assert self.expr.type_.literals
+
+        error = RecordFluxError()
+        literals = [
+            c.name for (choice, _) in self.choices for c in choice if isinstance(c, (str, ID))
+        ]
+        type_literals = [l.name for l in self.expr.type_.literals]
+        missing = set(type_literals) - set(literals)
+        if missing:
+            error.extend(
+                [
+                    (
+                        "not all enumeration literals covered by case expression",
+                        Subsystem.MODEL,
+                        Severity.ERROR,
+                        self.location,
+                    ),
+                    *[
+                        (
+                            f'missing literal "{l.name}"',
+                            Subsystem.MODEL,
+                            Severity.WARNING,
+                            self.expr.type_.location,
+                        )
+                        for l in missing
+                    ],
+                ]
+            )
+
+        invalid = set(literals) - set(type_literals)
+        if invalid:
+            error.extend(
+                [
+                    (
+                        "invalid literals used in case expression",
+                        Subsystem.MODEL,
+                        Severity.ERROR,
+                        self.location,
+                    ),
+                    *[
+                        (
+                            f'literal "{l.name}" not part of {self.expr.type_.identifier}',
+                            Subsystem.MODEL,
+                            Severity.WARNING,
+                            self.expr.type_.location,
+                        )
+                        for l in invalid
+                    ],
+                ]
+            )
+        return error
+
+    def _check_integer(self) -> RecordFluxError:
+        assert isinstance(self.expr.type_, rty.Integer)
+        assert self.expr.type_.bounds.lower
+        assert self.expr.type_.bounds.upper
 
-    def _check_type_subexpr(self) -> RecordFluxError:
         error = RecordFluxError()
+        literals = [
+            c.value for (choice, _) in self.choices for c in choice if isinstance(c, Number)
+        ]
+        type_literals = range(self.expr.type_.bounds.lower, self.expr.type_.bounds.upper + 1)
 
+        missing = set(type_literals) - set(literals)
+        if missing:
+            error.extend(
+                [
+                    (
+                        f"case expression does not cover full range of "
+                        f"{self.expr.type_.identifier}",
+                        Subsystem.MODEL,
+                        Severity.ERROR,
+                        self.location,
+                    ),
+                    *[
+                        (
+                            f'missing literal "{l}"',
+                            Subsystem.MODEL,
+                            Severity.WARNING,
+                            self.expr.type_.location,
+                        )
+                        for l in missing
+                    ],
+                ]
+            )
+
+        invalid = set(literals) - set(type_literals)
+        if invalid:
+            error.extend(
+                [
+                    (
+                        "invalid literals used in case expression",
+                        Subsystem.MODEL,
+                        Severity.ERROR,
+                        self.location,
+                    ),
+                    *[
+                        (
+                            f'literal "{l}" not part of {self.expr.type_.identifier}',
+                            Subsystem.MODEL,
+                            Severity.WARNING,
+                            self.expr.type_.location,
+                        )
+                        for l in invalid
+                    ],
+                ]
+            )
+
+        return error
+
+    def _check_type_subexpr(self) -> RecordFluxError:
+        error = RecordFluxError()
         resulttype: rty.Type = rty.Any()
+        literals = [c for (choice, _) in self.choices for c in choice]
 
         for _, expr in self.choices:
             error += expr.check_type_instance(rty.Any)
@@ -2818,7 +2933,38 @@ def _check_type_subexpr(self) -> RecordFluxError:
         error += self.expr.check_type_instance(rty.Any)
         error.propagate()
 
-        if not isinstance(self.expr.type_, (rty.AnyInteger, rty.Enumeration)):
+        duplicates = [
+            e1
+            for i1, e1 in enumerate(literals)
+            for i2, e2 in enumerate(literals)
+            if i1 > i2 and e1 == e2
+        ]
+        if duplicates:
+            error.extend(
+                [
+                    (
+                        "duplicate literals used in case expression",
+                        Subsystem.MODEL,
+                        Severity.ERROR,
+                        self.location,
+                    ),
+                    *[
+                        (
+                            f'duplicate literal "{l}"',
+                            Subsystem.MODEL,
+                            Severity.WARNING,
+                            l.location,
+                        )
+                        for l in duplicates
+                    ],
+                ]
+            )
+
+        if isinstance(self.expr.type_, rty.Enumeration):
+            error += self._check_enumeration()
+        elif isinstance(self.expr.type_, rty.Integer):
+            error += self._check_integer()
+        else:
             error.extend(
                 [
                     (
@@ -2870,7 +3016,10 @@ def precedence(self) -> Precedence:
 
     def ada_expr(self) -> ada.Expr:
         choices = [
-            (Literal(choice).ada_expr(), expr.ada_expr())
+            (
+                Literal(choice).ada_expr() if isinstance(choice, (str, ID)) else choice.ada_expr(),
+                expr.ada_expr(),
+            )
             for choices, expr in self.choices
             for choice in choices
         ]

rflx/model/type_.py

@@ -85,7 +85,9 @@ def constraints(
 class Integer(Scalar):
     @property
     def type_(self) -> rty.Type:
-        return rty.Integer(self.full_name, rty.Bounds(self.first.value, self.last.value))
+        return rty.Integer(
+            self.full_name, rty.Bounds(self.first.value, self.last.value), location=self.location
+        )
 
     @property
     def value_count(self) -> expr.Number:
@@ -498,7 +500,12 @@ def __str__(self) -> str:
 
     @property
     def type_(self) -> rty.Type:
-        return rty.Enumeration(self.full_name, self.always_valid)
+        return rty.Enumeration(
+            self.full_name,
+            list(map(ID, self.literals.keys())),
+            self.always_valid,
+            location=self.location,
+        )
 
     @property
     def value_count(self) -> expr.Number:
@@ -698,7 +705,7 @@ def type_(self) -> rty.Type:
     ],
     expr.Number(1),
     always_valid=False,
-    location=Location((0, 0), Path(str(const.BUILTINS_PACKAGE)), (0, 0)),
+    location=rty.BOOLEAN.location,
 )
 
 BUILTIN_TYPES = {

rflx/specification/parser.py

@@ -645,13 +645,29 @@ def create_selected(expression: lang.Expr, filename: Path) -> expr.Expr:
 
 def create_case(expression: lang.Expr, filename: Path) -> expr.Expr:
     assert isinstance(expression, lang.CaseExpression)
-    choices: List[Tuple[List[StrID], expr.Expr]] = [
+
+    def create_choice(
+        value: Union[lang.AbstractID, lang.Expr], filename: Path
+    ) -> Union[ID, expr.Number]:
+        if isinstance(value, lang.AbstractID):
+            return create_id(value, filename)
+        assert isinstance(value, lang.Expr)
+        result = create_numeric_literal(value, filename)
+        assert isinstance(result, expr.Number)
+        return result
+
+    choices: List[Tuple[List[Union[ID, expr.Number]], expr.Expr]] = [
         (
-            [create_id(s, filename) for s in c.f_selectors if isinstance(s, lang.AbstractID)],
+            [
+                create_choice(s, filename)
+                for s in c.f_selectors
+                if isinstance(s, (lang.AbstractID, lang.Expr))
+            ],
             create_expression(c.f_expression, filename),
         )
         for c in expression.f_choices
     ]
+
     return expr.Case(
         create_expression(expression.f_expression, filename),
         choices,

rflx/typing_.py

@@ -1,5 +1,6 @@
 import typing as ty
 from abc import abstractmethod
+from pathlib import Path
 
 import attr
 
@@ -108,13 +109,19 @@ def common_type(self, other: Type) -> Type:
 @attr.s(frozen=True)
 class Enumeration(IndependentType):
     DESCRIPTIVE_NAME: ty.ClassVar[str] = "enumeration type"
+    literals: ty.Sequence[ID] = attr.ib()
     always_valid: bool = attr.ib(False)
+    location: ty.Optional[Location] = attr.ib(default=None, cmp=False)
 
     def __str__(self) -> str:
         return f'{self.DESCRIPTIVE_NAME} "{self.identifier}"'
 
 
-BOOLEAN = Enumeration(const.BUILTINS_PACKAGE * "Boolean")
+BOOLEAN = Enumeration(
+    const.BUILTINS_PACKAGE * "Boolean",
+    [ID("False"), ID("True")],
+    location=Location((0, 0), Path(str(const.BUILTINS_PACKAGE)), (0, 0)),
+)
 
 
 @attr.s(frozen=True)
@@ -172,6 +179,7 @@ class Integer(AnyInteger):
     DESCRIPTIVE_NAME: ty.ClassVar[str] = "integer type"
     identifier: ID = attr.ib(converter=ID)
     bounds: Bounds = attr.ib(Bounds(None, None))
+    location: ty.Optional[Location] = attr.ib(default=None, cmp=False)
 
     def __str__(self) -> str:
         return f'{self.DESCRIPTIVE_NAME} "{self.identifier}" ({self.bounds})'

tests/data/models.py

@@ -1,3 +1,4 @@
+from rflx.error import Location
 from rflx.expression import (
     Aggregate,
     And,
@@ -306,6 +307,7 @@
     [("Zero", Number(0)), ("One", Number(1)), ("Two", Number(2))],
     Number(8),
     always_valid=False,
+    location=Location((10, 2)),
 )
 
 MESSAGE = Message(

tests/integration/specification_model_test.py

@@ -787,3 +787,41 @@ def test_rfi_files(tmp_path: Path, rfi_content: str, match_error: str) -> None:
         with pytest.raises(RecordFluxError, match=regex):
             p.parse(test_spec)
             p.create_model()
+
+
+def test_parse_case_expression() -> None:
+    p = parser.Parser()
+    p.parse_string(
+        """
+           package Test is
+              type T is range 1 .. 3 with Size => 8;
+
+              generic
+                  with function Get_V return T;
+              session Session with
+                 Initial => A,
+                 Final => B
+              is
+              begin
+                 state A
+                 is
+                    V : T := Get_V;
+                    E : Boolean;
+                 begin
+                    E := (case V is
+                          when 1 => True,
+                          when 2 => False,
+                          when 3 => True);
+                 transition
+                    goto B
+                        if E = True
+                    goto A
+                 end A;
+
+                 state B is null state;
+              end Session;
+           end Test;
+        """
+    )
+    m = p.create_model()
+    assert m