Use Base_Integer as common type of integer operations

Ref. eng/recordflux/RecordFlux#1697

rflx/generator/session.py

@@ -5193,7 +5193,10 @@ def _convert_type(
         expression: ir.Expr,
         target_type: rty.Type,
     ) -> ir.Expr:
-        if target_type.is_compatible_strong(expression.type_):
+        if target_type.is_compatible_strong(expression.type_) and not isinstance(
+            expression,
+            ir.BinaryIntExpr,
+        ):
             return expression
 
         assert isinstance(target_type, (rty.Integer, rty.Enumeration)), target_type
@@ -5202,18 +5205,25 @@ def _convert_type(
 
         if isinstance(expression, ir.BinaryIntExpr):
             assert isinstance(target_type, rty.Integer)
-            return expression.__class__(
-                ir.IntConversion(
+            left = (
+                expression.left
+                if target_type.is_compatible_strong(expression.left.type_)
+                else ir.IntConversion(
                     self._ada_type(target_type.identifier),
                     expression.left,
                     target_type,
-                ),
-                ir.IntConversion(
+                )
+            )
+            right = (
+                expression.right
+                if target_type.is_compatible_strong(expression.right.type_)
+                else ir.IntConversion(
                     self._ada_type(target_type.identifier),
                     expression.right,
                     target_type,
-                ),
+                )
             )
+            return expression.__class__(left, right)
 
         return ir.Conversion(self._ada_type(target_type.identifier), expression, target_type)
 

rflx/ir.py

@@ -195,7 +195,11 @@ def substituted(self, mapping: Mapping[ID, ID]) -> Assign:
         )
 
     def preconditions(self, variable_id: Generator[ID, None, None]) -> list[Cond]:
-        return self.expression.preconditions(variable_id)
+        return (
+            self.expression.preconditions(variable_id, self.type_)
+            if isinstance(self.expression, BinaryIntExpr)
+            else self.expression.preconditions(variable_id)
+        )
 
     def to_z3_expr(self) -> z3.BoolRef:
         target: Var
@@ -856,6 +860,14 @@ class BinaryIntExpr(BinaryExpr, IntExpr):
     right: BasicIntExpr
     origin: Optional[Origin] = None
 
+    @abstractmethod
+    def preconditions(
+        self,
+        variable_id: Generator[ID, None, None],
+        target_type: rty.Type | None = None,
+    ) -> list[Cond]:
+        raise NotImplementedError
+
     @property
     def type_(self) -> rty.AnyInteger:
         type_ = self.left.type_.common_type(self.right.type_)
@@ -884,12 +896,17 @@ class Add(BinaryIntExpr):
     def to_z3_expr(self) -> z3.ArithRef:
         return self.left.to_z3_expr() + self.right.to_z3_expr()
 
-    def preconditions(self, variable_id: Generator[ID, None, None]) -> list[Cond]:
+    def preconditions(
+        self,
+        variable_id: Generator[ID, None, None],
+        target_type: rty.Type | None = None,
+    ) -> list[Cond]:
+        target_type = target_type or self.type_
         v_id = next(variable_id)
-        v_type = to_integer(self.type_)
+        v_type = rty.BASE_INTEGER
         upper_bound = (
-            self.type_.bounds.upper
-            if isinstance(self.type_, rty.AnyInteger) and self.type_.bounds is not None
+            target_type.bounds.upper
+            if isinstance(target_type, rty.AnyInteger) and target_type.bounds is not None
             else INT_MAX
         )
         return [
@@ -935,7 +952,11 @@ class Sub(BinaryIntExpr):
     def to_z3_expr(self) -> z3.ArithRef:
         return self.left.to_z3_expr() - self.right.to_z3_expr()
 
-    def preconditions(self, _variable_id: Generator[ID, None, None]) -> list[Cond]:
+    def preconditions(
+        self,
+        _variable_id: Generator[ID, None, None],
+        _target_type: rty.Type | None = None,
+    ) -> list[Cond]:
         return [
             # Left >= Right
             Cond(GreaterEqual(self.left, self.right)),
@@ -951,12 +972,17 @@ class Mul(BinaryIntExpr):
     def to_z3_expr(self) -> z3.ArithRef:
         return self.left.to_z3_expr() * self.right.to_z3_expr()
 
-    def preconditions(self, variable_id: Generator[ID, None, None]) -> list[Cond]:
+    def preconditions(
+        self,
+        variable_id: Generator[ID, None, None],
+        target_type: rty.Type | None = None,
+    ) -> list[Cond]:
+        target_type = target_type or self.type_
         v_id = next(variable_id)
-        v_type = to_integer(self.type_)
+        v_type = rty.BASE_INTEGER
         upper_bound = (
-            self.type_.bounds.upper
-            if isinstance(self.type_, rty.AnyInteger) and self.type_.bounds is not None
+            target_type.bounds.upper
+            if isinstance(target_type, rty.AnyInteger) and target_type.bounds is not None
             else INT_MAX
         )
         return [
@@ -994,7 +1020,11 @@ class Div(BinaryIntExpr):
     def to_z3_expr(self) -> z3.ArithRef:
         return self.left.to_z3_expr() / self.right.to_z3_expr()
 
-    def preconditions(self, _variable_id: Generator[ID, None, None]) -> list[Cond]:
+    def preconditions(
+        self,
+        _variable_id: Generator[ID, None, None],
+        _target_type: rty.Type | None = None,
+    ) -> list[Cond]:
         return [
             # Right /= 0
             Cond(NotEqual(self.right, IntVal(0))),
@@ -1010,12 +1040,17 @@ class Pow(BinaryIntExpr):
     def to_z3_expr(self) -> z3.ArithRef:
         return self.left.to_z3_expr() ** self.right.to_z3_expr()
 
-    def preconditions(self, variable_id: Generator[ID, None, None]) -> list[Cond]:
+    def preconditions(
+        self,
+        variable_id: Generator[ID, None, None],
+        target_type: rty.Type | None = None,
+    ) -> list[Cond]:
+        target_type = target_type or self.type_
         v_id = next(variable_id)
-        v_type = to_integer(self.type_)
+        v_type = rty.BASE_INTEGER
         upper_bound = (
-            self.type_.bounds.upper
-            if isinstance(self.type_, rty.AnyInteger) and self.type_.bounds is not None
+            target_type.bounds.upper
+            if isinstance(target_type, rty.AnyInteger) and target_type.bounds is not None
             else INT_MAX
         )
         return [
@@ -1027,7 +1062,7 @@ def preconditions(self, variable_id: Generator[ID, None, None]) -> list[Cond]:
                 ),
                 [
                     VarDecl(v_id, v_type, None, origin=self.origin),
-                    Assign(v_id, self, to_integer(self.type_), origin=self.origin),
+                    Assign(v_id, self, v_type, origin=self.origin),
                 ],
             ),
         ]
@@ -1042,7 +1077,11 @@ class Mod(BinaryIntExpr):
     def to_z3_expr(self) -> z3.ArithRef:
         return self.left.to_z3_expr() % self.right.to_z3_expr()
 
-    def preconditions(self, _variable_id: Generator[ID, None, None]) -> list[Cond]:
+    def preconditions(
+        self,
+        _variable_id: Generator[ID, None, None],
+        _target_type: rty.Type | None = None,
+    ) -> list[Cond]:
         return [
             # Right /= 0
             Cond(NotEqual(self.right, IntVal(0))),

rflx/typing_.py

@@ -113,10 +113,10 @@ def common_type(self, other: Type) -> Type:
             return UniversalInteger(
                 Bounds.merge(self.bounds, other.bounds),
             )
-        if isinstance(other, AnyInteger):
-            return other
         if other == Any() or self == other:
             return self
+        if isinstance(other, AnyInteger):
+            return BASE_INTEGER
         return Undefined()
 
 
@@ -145,16 +145,10 @@ def is_compatible_strong(self, other: Type) -> bool:
         )
 
     def common_type(self, other: Type) -> Type:
-        if isinstance(other, UniversalInteger):
+        if other == Any():
             return self
-        if isinstance(other, Integer) and (
-            self.identifier != other.identifier or self.bounds != other.bounds
-        ):
-            return BASE_INTEGER
         if isinstance(other, AnyInteger):
-            return other
-        if other == Any() or self == other:
-            return self
+            return BASE_INTEGER
         return Undefined()
 
 

tests/feature/session_comprehension_on_message_field/generated/rflx-test-session.adb

@@ -297,7 +297,7 @@ is
       pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type));
       Universal.Message.Set_Message_Type (Ctx.P.Message_Ctx, Universal.MT_Option_Types);
       pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Length));
-      Universal.Message.Set_Length (Ctx.P.Message_Ctx, Universal.Length (T_5) / Universal.Length (8));
+      Universal.Message.Set_Length (Ctx.P.Message_Ctx, Universal.Length (T_5) / 8);
       if not Universal.Message.Valid_Length (Ctx.P.Message_Ctx, Universal.Message.F_Option_Types, Universal.Option_Types.Byte_Size (Option_Types_Ctx)) then
          Ctx.P.Next_State := S_Final;
          pragma Assert (Process_Invariant);

tests/feature/session_comprehension_on_sequence/generated/rflx-test-session.adb

@@ -331,7 +331,7 @@ is
       pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.Message_1_Ctx, Universal.Message.F_Message_Type));
       Universal.Message.Set_Message_Type (Ctx.P.Message_1_Ctx, Universal.MT_Option_Types);
       pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.Message_1_Ctx, Universal.Message.F_Length));
-      Universal.Message.Set_Length (Ctx.P.Message_1_Ctx, Universal.Length (T_2) / Universal.Length (8));
+      Universal.Message.Set_Length (Ctx.P.Message_1_Ctx, Universal.Length (T_2) / 8);
       if not Universal.Message.Valid_Length (Ctx.P.Message_1_Ctx, Universal.Message.F_Option_Types, Universal.Option_Types.Byte_Size (Option_Types_Ctx)) then
          Ctx.P.Next_State := S_Final;
          pragma Assert (Process_Invariant);
@@ -459,7 +459,7 @@ is
       pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.Message_2_Ctx, Universal.Message.F_Message_Type));
       Universal.Message.Set_Message_Type (Ctx.P.Message_2_Ctx, Universal.MT_Options);
       pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.Message_2_Ctx, Universal.Message.F_Length));
-      Universal.Message.Set_Length (Ctx.P.Message_2_Ctx, Universal.Length (T_4) / Universal.Length (8));
+      Universal.Message.Set_Length (Ctx.P.Message_2_Ctx, Universal.Length (T_4) / 8);
       if not Universal.Message.Valid_Length (Ctx.P.Message_2_Ctx, Universal.Message.F_Options, Universal.Options.Byte_Size (Message_Options_Ctx)) then
          Ctx.P.Next_State := S_Final;
          pragma Assert (Process_Invariant);

tests/feature/session_functions/generated/rflx-test-session.adb

@@ -118,7 +118,7 @@ is
          goto Finalize_Process;
       end if;
       -- tests/feature/session_functions/test.rflx:58:10
-      Length := Test.Length (T_6) / Test.Length (T_7);
+      Length := Test.Length (T_6) / T_7;
       -- tests/feature/session_functions/test.rflx:60:10
       declare
          Definite_Message : Test.Definite_Message.Structure;
@@ -188,7 +188,7 @@ is
       -- tests/feature/session_functions/test.rflx:79:20
       T_8 := RFLX.RFLX_Types.Base_Integer (Universal.Message.Size (Ctx.P.Message_Ctx));
       -- tests/feature/session_functions/test.rflx:79:10
-      Length := Test.Length (T_8) / Test.Length (8);
+      Length := Test.Length (T_8) / 8;
       -- tests/feature/session_functions/test.rflx:81:10
       declare
          Definite_Message : Test.Definite_Message.Structure;

tests/feature/session_message_creation/generated/rflx-test-session.adb

@@ -123,7 +123,7 @@ is
       pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.M_S_Ctx, Universal.Message.F_Message_Type));
       Universal.Message.Set_Message_Type (Ctx.P.M_S_Ctx, Universal.MT_Data);
       pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.M_S_Ctx, Universal.Message.F_Length));
-      Universal.Message.Set_Length (Ctx.P.M_S_Ctx, Universal.Length (T_11) / Universal.Length (8));
+      Universal.Message.Set_Length (Ctx.P.M_S_Ctx, Universal.Length (T_11) / 8);
       declare
          function RFLX_Process_Data_Pre (Length : RFLX_Types.Length) return Boolean is
            (Universal.Message.Has_Buffer (Ctx.P.M_R_Ctx)

tests/feature/session_sequence_append/generated/rflx-test-session.adb

@@ -114,7 +114,7 @@ is
       pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type));
       Universal.Message.Set_Message_Type (Ctx.P.Message_Ctx, Universal.MT_Options);
       pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Length));
-      Universal.Message.Set_Length (Ctx.P.Message_Ctx, Universal.Length (T_0) / Universal.Length (8));
+      Universal.Message.Set_Length (Ctx.P.Message_Ctx, Universal.Length (T_0) / 8);
       if not Universal.Message.Valid_Length (Ctx.P.Message_Ctx, Universal.Message.F_Options, Universal.Options.Byte_Size (Options_Ctx)) then
          Ctx.P.Next_State := S_Final;
          pragma Assert (Process_Invariant);

tests/feature/session_setting_of_message_fields/generated/rflx-test-session.adb

@@ -143,7 +143,7 @@ is
       pragma Assert (Universal.Message.Sufficient_Space (Local_Message_Ctx, Universal.Message.F_Message_Type));
       Universal.Message.Set_Message_Type (Local_Message_Ctx, Universal.MT_Data);
       pragma Assert (Universal.Message.Sufficient_Space (Local_Message_Ctx, Universal.Message.F_Length));
-      Universal.Message.Set_Length (Local_Message_Ctx, Universal.Length (T_7) / Universal.Length (8));
+      Universal.Message.Set_Length (Local_Message_Ctx, Universal.Length (T_7) / 8);
       declare
          pragma Warnings (Off, "is not modified, could be declared constant");
          RFLX_Ctx_P_Message_Ctx_Tmp : Universal.Message.Context := Ctx.P.Message_Ctx;

tests/feature/session_variable_initialization/generated/rflx-test-session.adb

@@ -63,8 +63,8 @@ is
    is
       Local : Universal.Value := 2;
       T_0 : Universal.Value;
-      T_2 : Universal.Value;
-      T_3 : Universal.Value;
+      T_2 : RFLX.RFLX_Types.Base_Integer;
+      T_3 : RFLX.RFLX_Types.Base_Integer;
       T_1 : RFLX.RFLX_Types.Base_Integer;
       function Process_Invariant return Boolean is
         (Ctx.P.Slots.Slot_Ptr_1 = null)
@@ -82,9 +82,9 @@ is
       end if;
       T_0 := Universal.Message.Get_Value (Ctx.P.Message_Ctx);
       -- tests/feature/session_variable_initialization/test.rflx:22:19
-      T_2 := 255 - T_0;
+      T_2 := 255 - RFLX.RFLX_Types.Base_Integer (T_0);
       -- tests/feature/session_variable_initialization/test.rflx:22:19
-      if not (RFLX.RFLX_Types.Base_Integer (Local) <= RFLX.RFLX_Types.Base_Integer (T_2)) then
+      if not (RFLX.RFLX_Types.Base_Integer (Local) <= T_2) then
          Ctx.P.Next_State := S_Final;
          pragma Assert (Process_Invariant);
          goto Finalize_Process;
@@ -96,7 +96,7 @@ is
       -- tests/feature/session_variable_initialization/test.rflx:24:20
       T_3 := 255 - 20;
       -- tests/feature/session_variable_initialization/test.rflx:24:20
-      if not (RFLX.RFLX_Types.Base_Integer (Ctx.P.Uninitialized_Global) <= RFLX.RFLX_Types.Base_Integer (T_3)) then
+      if not (RFLX.RFLX_Types.Base_Integer (Ctx.P.Uninitialized_Global) <= T_3) then
          Ctx.P.Next_State := S_Final;
          pragma Assert (Process_Invariant);
          goto Finalize_Process;
@@ -110,7 +110,7 @@ is
       pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type));
       Universal.Message.Set_Message_Type (Ctx.P.Message_Ctx, Universal.MT_Value);
       pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Length));
-      Universal.Message.Set_Length (Ctx.P.Message_Ctx, Universal.Length (T_1) / Universal.Length (8));
+      Universal.Message.Set_Length (Ctx.P.Message_Ctx, Universal.Length (T_1) / 8);
       pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Value));
       Universal.Message.Set_Value (Ctx.P.Message_Ctx, Ctx.P.Global);
       if RFLX.RFLX_Types.Base_Integer (Local) < RFLX.RFLX_Types.Base_Integer (Ctx.P.Global) then