Check for always true conditions in refinements

ref #662
AdaCore · Nov 15, 2022 · 2ac7000 · 2ac7000
1 parent 3068f38
commit 2ac7000
Show file tree

Hide file tree

Showing 3 changed files with 53 additions and 2 deletions.
diff --git a/rflx/model/message.py b/rflx/model/message.py
@@ -2665,6 +2665,27 @@ def _verify(self) -> None:
                     ],
                 )
 
+        if self.condition != expr.TRUE:
+            proof = expr.TRUE.check(
+                [
+                    *self.pdu.type_constraints(self.condition),
+                    *self.pdu.type_constraints(self.pdu.path_condition(self.field)),
+                    expr.Equal(self.condition, expr.FALSE),
+                ]
+            )
+            if proof.result == expr.ProofResult.UNSAT:
+                self.error.extend(
+                    [
+                        (
+                            f'condition "{self.condition}" in refinement of'
+                            f' "{self.pdu.identifier}" is always true',
+                            Subsystem.MODEL,
+                            Severity.ERROR,
+                            self.field.identifier.location,
+                        )
+                    ]
+                )
+
     def __str__(self) -> str:
         condition = f"\n   if {self.condition}" if self.condition != expr.TRUE else ""
         return f"for {self.pdu.name} use ({self.field.name} => {self.sdu.name}){condition}"

diff --git a/tests/integration/specification_model_generator_test.py b/tests/integration/specification_model_generator_test.py
@@ -140,7 +140,7 @@ def test_potential_name_conflicts_with_enum_literals(tmp_path: Path) -> None:
     spec = f"""\
         package Test is
 
-           type A is ({enum_literals}) with Size => 8;
+           type A is ({enum_literals}, Extra_Literal) with Size => 8;
 
            type B is sequence of A;
 
@@ -424,7 +424,7 @@ def test_refinement_with_self(tmp_path: Path) -> None:
         """\
         package Test is
 
-           type Tag is (T1 => 1) with Size => 8;
+           type Tag is (T1 => 1, T2 => 2) with Size => 8;
 
            type Length is range 0 .. 2 ** 8 - 1 with Size => 8;
 

diff --git a/tests/unit/model/message_test.py b/tests/unit/model/message_test.py
@@ -4309,3 +4309,33 @@ def test_boolean_variable_as_condition() -> None:
             Field("Has_Tag"): BOOLEAN,
         },
     )
+
+
+def test_always_true_refinement() -> None:
+    message = Message(
+        "P::M",
+        [
+            Link(INITIAL, Field("Tag")),
+            Link(Field("Tag"), Field("Value")),
+            Link(Field("Value"), FINAL),
+        ],
+        {
+            Field("Tag"): TLV_TAG,
+            Field("Value"): OPAQUE,
+        },
+    )
+    refinement = Refinement(
+        "In_Message",
+        message,
+        Field(ID("Value", location=Location((10, 20)))),
+        MESSAGE,
+        Or(
+            Equal(Variable("Tag"), Variable("TLV::Msg_Data")),
+            Equal(Variable("Tag"), Variable("TLV::Msg_Error")),
+        ),
+    )
+    assert_type_error(
+        refinement,
+        r'^<stdin>:10:20: model: error: condition "Tag = TLV::Msg_Data\n'
+        'or Tag = TLV::Msg_Error" in refinement of "P::M" is always true$',
+    )