Check length and alignment of Opaque fields

Ref. #288

rflx/model.py

@@ -25,6 +25,7 @@
     Length,
     Less,
     LessEqual,
+    Mod,
     Mul,
     Not,
     NotEqual,
@@ -1012,10 +1013,17 @@ def get_constraints(aggregate: Aggregate, field: Variable) -> Sequence[Expr]:
             if isinstance(r.left, Variable) and isinstance(r.right, Aggregate):
                 aggregate_constraints.extend(get_constraints(r.right, r.left))
 
-        return aggregate_constraints + [
-            c for n, t in scalar_types for c in t.constraints(name=n, proof=True)
+        message_constraints: List[Expr] = [
+            Equal(Mod(First("Message"), Number(8)), Number(1)),
+            Equal(Mod(Length("Message"), Number(8)), Number(0)),
         ]
 
+        return (
+            message_constraints
+            + aggregate_constraints
+            + [c for n, t in scalar_types for c in t.constraints(name=n, proof=True)]
+        )
+
     def __prove_conflicting_conditions(self) -> None:
         for f in (INITIAL, *self.fields):
             for i1, c1 in enumerate(self.outgoing(f)):
@@ -1239,6 +1247,39 @@ def __prove_field_positions(self) -> None:
                     )
                     return
 
+                if f in self.__types and isinstance(self.__types[f], Opaque):
+                    start_aligned = Not(
+                        Equal(Mod(self.__target_first(last), Number(8)), Number(1), last.location)
+                    )
+                    proof = start_aligned.check([*facts, *self.__type_constraints(start_aligned)])
+                    if proof.result != ProofResult.unsat:
+                        path_message = " -> ".join([p.target.name for p in path])
+                        self.error.append(
+                            f'opaque field "{f.name}" not aligned to 8 bit boundary'
+                            f" ({path_message})",
+                            Subsystem.MODEL,
+                            Severity.ERROR,
+                            self.location,
+                        )
+                        return
+
+                    length_multiple_8 = Not(
+                        Equal(Mod(self.__target_length(last), Number(8)), Number(0), last.location)
+                    )
+                    proof = length_multiple_8.check(
+                        [*facts, *self.__type_constraints(length_multiple_8)]
+                    )
+                    if proof.result != ProofResult.unsat:
+                        path_message = " -> ".join([p.target.name for p in path])
+                        self.error.append(
+                            f'length of opaque field "{f.name}" not multiple of 8 bit'
+                            f" ({path_message})",
+                            Subsystem.MODEL,
+                            Severity.ERROR,
+                            self.location,
+                        )
+                        return
+
     def __prove_coverage(self) -> None:
         """
         Prove that the fields of a message cover all message bits, i.e. there are no holes in the

specs/tls_handshake.rflx

@@ -60,7 +60,7 @@ package TLS_Handshake is
          Tag : Extension_Type;
          Data_Length : Data_Length
             then Data
-               with Length => Data_Length;
+               with Length => 8 * Data_Length;
          Data : Opaque;
       end message;
 
@@ -354,7 +354,7 @@ package TLS_Handshake is
          Name_Type : Name_Type;
          Length : Name_Length
             then Name
-               with Length => Length;
+               with Length => 8 * Length;
          Name : Opaque;
       end message;
 
@@ -365,7 +365,7 @@ package TLS_Handshake is
       message
          Length : Server_Name_List_Length
             then Server_Name_List
-               with Length => Length;
+               with Length => 8 * Length;
          Server_Name_List : Server_Names;
       end message;
 
@@ -402,7 +402,7 @@ package TLS_Handshake is
       message
          Length : Supported_Versions_Length
             then Versions
-               with Length => Length;
+               with Length => 8 * Length;
          Versions : Protocol_Versions;
       end message;
 
@@ -426,7 +426,7 @@ package TLS_Handshake is
       message
          Length : Cookie_Length
             then Cookie
-               with Length => Length;
+               with Length => 8 * Length;
          Cookie : Opaque;
       end message;
 
@@ -444,7 +444,7 @@ package TLS_Handshake is
       message
          Length : Signature_Algorithms_Length
             then Algorithms
-               with Length => Length;
+               with Length => 8 * Length;
          Algorithms : Signature_Schemes;
       end message;
 
@@ -457,7 +457,7 @@ package TLS_Handshake is
       message
          Length : Signature_Algorithms_Length
             then Algorithms
-               with Length => Length;
+               with Length => 8 * Length;
          Algorithms : Signature_Schemes;
       end message;
 
@@ -484,7 +484,7 @@ package TLS_Handshake is
       message
          Length : Distinguished_Name_Length
             then Name
-               with Length => Length;
+               with Length => 8 * Length;
          Name : Opaque;
       end message;
 
@@ -494,7 +494,7 @@ package TLS_Handshake is
       message
          Length : Certificate_Authorities_Length
             then Authorities
-               with Length => Length;
+               with Length => 8 * Length;
          Authorities : Distinguished_Names;
       end message;
 
@@ -513,11 +513,11 @@ package TLS_Handshake is
       message
          OID_Length : OID_Length
             then OID
-               with Length => OID_Length;
+               with Length => 8 * OID_Length;
          OID : Opaque;
          Values_Length : Values_Length
             then Values
-               with Length => Values_Length;
+               with Length => 8 * Values_Length;
          Values : Opaque;
       end message;
 
@@ -527,7 +527,7 @@ package TLS_Handshake is
       message
          Length : Filters_Length
             then Filters
-               with Length => Length;
+               with Length => 8 * Length;
          Filters : Filters;
       end message;
 
@@ -566,7 +566,7 @@ package TLS_Handshake is
       message
          Length : Supported_Groups_Length
             then Groups
-               with Length => Length;
+               with Length => 8 * Length;
          Groups : Named_Groups;
       end message;
 
@@ -584,7 +584,7 @@ package TLS_Handshake is
          Group : Named_Group;
          Length : Key_Exchange_Length
             then Key_Exchange
-               with Length => Length;
+               with Length => 8 * Length;
          Key_Exchange : Opaque;
       end message;
 
@@ -596,7 +596,7 @@ package TLS_Handshake is
       message
          Length : Key_Shares_Length
             then Shares
-               with Length => Length;
+               with Length => 8 * Length;
          Shares : Key_Share_Entries;
       end message;
 
@@ -629,7 +629,7 @@ package TLS_Handshake is
       message
          Length : PSK_Key_Exchange_Modes_Length
             then Modes
-               with Length => Length;
+               with Length => 8 * Length;
          Modes : Key_Exchange_Modes;
       end message;
 
@@ -663,7 +663,7 @@ package TLS_Handshake is
       message
          Length : Identity_Length
             then Identity
-               with Length => Length;
+               with Length => 8 * Length;
          Identity : Opaque;
          Obfuscated_Ticket_Age : Obfuscated_Ticket_Age;
       end message;
@@ -676,7 +676,7 @@ package TLS_Handshake is
       message
          Length : PSK_Binder_Entry_Length
             then PSK_Binder_Entry
-               with Length => Length;
+               with Length => 8 * Length;
          PSK_Binder_Entry : Opaque;
       end message;
 
@@ -689,11 +689,11 @@ package TLS_Handshake is
       message
          Identities_Length : Identities_Length
             then Identities
-               with Length => Identities_Length;
+               with Length => 8 * Identities_Length;
          Identities : PSK_Identities;
          Binders_Length : Binders_Length
             then Binders
-               with Length => Binders_Length;
+               with Length => 8 * Binders_Length;
          Binders : PSK_Binder_Entries;
       end message;
 
@@ -717,7 +717,7 @@ package TLS_Handshake is
       message
          Length : Protocol_Name_Length
             then Name
-               with Length => Length;
+               with Length => 8 * Length;
          Name : Opaque;
       end message;
 
@@ -728,7 +728,7 @@ package TLS_Handshake is
       message
          Length : Protocol_Name_List_Length
             then Protocol_Name_List
-               with Length => Length;
+               with Length => 8 * Length;
          Protocol_Name_List : Protocol_Names;
       end message;
 

tests/enumeration_type.rflx

@@ -2,6 +2,6 @@ package Enumeration_Type is
 
    type Day is (Mon => 1, Tue => 2, Wed => 3, Thu => 4, Fri => 5, Sat => 6, Sun => 7) with Size => 3;
    type Gender is (M, F) with Size => 1, Always_Valid => False;
-   type Priority is (LOW => 1, MEDIUM => 4, HIGH => 7) with Always_Valid, Size => 3;
+   type Priority is (LOW => 1, MEDIUM => 4, HIGH => 7) with Always_Valid, Size => 8;
 
 end Enumeration_Type;

tests/feature_integration.rflx

@@ -14,16 +14,16 @@ package Feature_Integration is
                if Enumeration = Enumeration_Type.HIGH;
          Integer : Integer_Type.Byte
             then Scalar_Array
-               with Length => Integer;
+               with Length => 8 * Integer;
          Scalar_Array : Array_Type.Bytes
             then Message_Array
-               with Length => Integer;
+               with Length => 8 * Integer;
          Message_Array : Array_Type.Bar;
          Message_Type : Message_Type.PDU;
          Message_In_Message : Message_In_Message.Message;
          Derived_Message_In_Message : Message_In_Message.Derived_Message
             then Opaque
-               with Length => Integer;
+               with Length => 8 * Integer;
          Opaque : Opaque;
       end message;
 

tests/message_in_message.rflx

@@ -6,7 +6,7 @@ package Message_In_Message is
       message
          Length : Length
             then Value
-               with Length => Length;
+               with Length => 8 * Length;
          Value : Opaque;
       end message;
 

tests/test_integration.py

@@ -145,7 +145,7 @@ def test_comparison_big_integers(condition: str) -> None:
         f"""
            package Test is
 
-              type D is range 17179869177 .. 17179869178 with Size => 35;
+              type D is range 17179869177 .. 17179869178 with Size => 40;
 
               type E is
                  message