Issue 1048: Use signed integers for storage

.github/workflows/tests.yml

@@ -194,7 +194,7 @@ jobs:
       uses: ./.github/actions/install_spark_pro
       if: ${{ needs.skip_check_python.outputs.should_skip != 'true' }}
       with:
-        version: "23.0w-20220128"
+        version: "23.0w-20220612"
         ssh_key: ${{ secrets.MEMCACHED_SSH_KEY }}
         server: ${{ secrets.MEMCACHED_SERVER }}
     - name: Install dependencies
@@ -444,7 +444,7 @@ jobs:
     - name: Install SPARK Pro
       uses: ./.github/actions/install_spark_pro
       with:
-        version: "23.0w-20220128"
+        version: "23.0w-20220612"
         ssh_key: ${{ secrets.MEMCACHED_SSH_KEY }}
         server: ${{ secrets.MEMCACHED_SERVER }}
     - name: Install dependencies
@@ -585,7 +585,7 @@ jobs:
       uses: ./.github/actions/install_spark_pro
       if: ${{ needs.skip_check_spark.outputs.should_skip != 'true' }}
       with:
-        version: "23.0w-20220128"
+        version: "23.0w-20220612"
         ssh_key: ${{ secrets.MEMCACHED_SSH_KEY }}
         server: ${{ secrets.MEMCACHED_SERVER }}
     - name: Install dependencies
@@ -766,7 +766,7 @@ jobs:
       uses: ./.github/actions/install_spark_pro
       if: ${{ needs.skip_check_apps.outputs.should_skip != 'true' }}
       with:
-        version: "23.0w-20220128"
+        version: "23.0w-20220612"
         ssh_key: ${{ secrets.MEMCACHED_SSH_KEY }}
         server: ${{ secrets.MEMCACHED_SERVER }}
     - name: Install dependencies

defaults.gpr

@@ -62,7 +62,7 @@ abstract project Defaults is
 
    Proof_Switches :=
    (
-      "--prover=z3,cvc4,altergo",
+      "--prover=z3,cvc4,altergo,colibri",
       "--steps=0",
       "--timeout=180",
       "--memlimit=2000",

examples/apps/dhcp_client/Makefile

@@ -19,7 +19,7 @@ clean:
 	rm -rf generated/* obj obj_optimized
 
 binary_size: $(bin-optimized)
-	test $(shell size -A -d obj_optimized/dhcp_client | grep .text | awk '{ print $$2 }') -le 174000
+	test $(shell size -A -d obj_optimized/dhcp_client | grep .text | awk '{ print $$2 }') -le 175000
 
 $(src): $(specs)
 	rflx generate -d generated --debug built-in $^

examples/apps/dhcp_client/src/dhcp_client.adb

@@ -84,4 +84,9 @@ begin
       end loop;
       DHCP_Client_Session.Run (Ctx);
    end loop;
+   pragma Warnings (Off, "statement has no effect");
+   pragma Warnings (Off, """Ctx"" is set by ""Finalize"" but not used after the call");
+   DHCP_Client_Session.Finalize (Ctx);
+   pragma Warnings (On, "statement has no effect");
+   pragma Warnings (On, """Ctx"" is set by ""Finalize"" but not used after the call");
 end DHCP_Client;

examples/apps/ping/src/basalt-strings_generic.ads

@@ -12,7 +12,7 @@
 package Basalt.Strings_Generic with
    SPARK_Mode,
    Pure,
-   Annotate => (GNATprove, Terminating)
+   Annotate => (GNATprove, Always_Return)
 is
 
    type Residue_Class_Ring is new Integer range 0 .. 16;

examples/apps/ping/src/generic_checksum.adb

@@ -20,8 +20,8 @@ is
    is
       use type ICMP.Checksum;
       use type Types.Index;
-      Checksum : ICMP.Checksum := Shift_Left (ICMP.Checksum (ICMP.To_U64 (Tag)))
-                                  + ICMP.Checksum (ICMP.To_U64 (Code));
+      Checksum : ICMP.Checksum := Shift_Left (ICMP.Checksum (ICMP.To_Base_Integer (Tag)))
+                                  + ICMP.Checksum (ICMP.To_Base_Integer (Code));
       Index    : Types.Index;
    begin
       Checksum := Add (Checksum, Add (ICMP.Checksum (Identifier), ICMP.Checksum (Sequence_Number)));

examples/apps/ping/src/icmpv4.adb

@@ -169,6 +169,8 @@ is
                        Last :    out RFLX.RFLX_Builtin_Types.Index)
    is
       use type RFLX.ICMP.Sequence_Number;
+      use RFLX.IPv4.Packet;
+      use type RFLX.RFLX_Builtin_Types.Bit_Length;
       IP_Context   : RFLX.IPv4.Packet.Context;
       ICMP_Context : RFLX.ICMP.Message.Context;
       Data         : constant RFLX.RFLX_Builtin_Types.Bytes (1 .. 56) := (others => 65);
@@ -196,6 +198,7 @@ is
       RFLX.IPv4.Packet.Initialize_Payload (IP_Context);
       if RFLX.IPv4.Contains.ICMP_Message_In_Packet_Payload (IP_Context) then
          RFLX.IPv4.Contains.Switch_To_Payload (IP_Context, ICMP_Context);
+         pragma Assert (Field_Size (IP_Context, F_Payload) = 512);
          RFLX.ICMP.Message.Set_Tag (ICMP_Context, RFLX.ICMP.Echo_Request);
          RFLX.ICMP.Message.Set_Code_Zero (ICMP_Context, 0);
          RFLX.ICMP.Message.Set_Checksum (ICMP_Context,

rflx/const.py

@@ -2,3 +2,8 @@
 
 BUILTINS_PACKAGE = ID("__BUILTINS__")
 INTERNAL_PACKAGE = ID("__INTERNAL__")
+
+# ISSUE: Componolit/RecordFlux#1077
+# size of integers is limited to 63bits
+
+MAX_SCALAR_SIZE = 63

rflx/generator/common.py

@@ -66,7 +66,7 @@ def substitution(
     prefix: str,
     embedded: bool = False,
     public: bool = False,
-    target_type: Optional[ID] = const.TYPES_U64,
+    target_type: Optional[ID] = const.TYPES_BASE_INT,
 ) -> Callable[[expr.Expr], expr.Expr]:
     facts = substitution_facts(message, prefix, embedded, public, target_type)
 
@@ -152,7 +152,7 @@ def byte_aggregate(aggregate: expr.Aggregate) -> expr.Aggregate:
                 other = expression.left
             if boolean_literal and other:
                 return expression.__class__(
-                    other, type_conversion(expr.Call("To_U64", [boolean_literal]))
+                    other, type_conversion(expr.Call("To_Base_Integer", [boolean_literal]))
                 )
 
         def field_value(field: model.Field) -> expr.Expr:
@@ -194,7 +194,7 @@ def substitution_facts(
     prefix: str,
     embedded: bool = False,
     public: bool = False,
-    target_type: Optional[ID] = const.TYPES_U64,
+    target_type: Optional[ID] = const.TYPES_BASE_INT,
 ) -> Mapping[expr.Name, expr.Expr]:
     def prefixed(name: str) -> expr.Expr:
         return expr.Variable(rid.ID("Ctx") * name) if not embedded else expr.Variable(name)
@@ -233,8 +233,8 @@ def field_size(field: model.Field) -> expr.Expr:
     def parameter_value(parameter: model.Field, parameter_type: model.Type) -> expr.Expr:
         if isinstance(parameter_type, model.Enumeration):
             if embedded:
-                return expr.Call("To_U64", [expr.Variable(parameter.name)])
-            return expr.Call("To_U64", [expr.Variable("Ctx" * parameter.identifier)])
+                return expr.Call("To_Base_Integer", [expr.Variable(parameter.name)])
+            return expr.Call("To_Base_Integer", [expr.Variable("Ctx" * parameter.identifier)])
         if isinstance(parameter_type, model.Scalar):
             if embedded:
                 return expr.Variable(parameter.name)
@@ -245,7 +245,9 @@ def parameter_value(parameter: model.Field, parameter_type: model.Type) -> expr.
     def field_value(field: model.Field, field_type: model.Type) -> expr.Expr:
         if isinstance(field_type, model.Enumeration):
             if public:
-                return expr.Call("To_U64", [expr.Call(f"Get_{field.name}", [expr.Variable("Ctx")])])
+                return expr.Call(
+                    "To_Base_Integer", [expr.Call(f"Get_{field.name}", [expr.Variable("Ctx")])]
+                )
             return expr.Selected(
                 expr.Indexed(cursors, expr.Variable(field.affixed_name)),
                 "Value",
@@ -281,14 +283,14 @@ def type_conversion(expression: expr.Expr) -> expr.Expr:
             for f, t in message.field_types.items()
         },
         **{
-            expr.Variable(l): type_conversion(expr.Call("To_U64", [expr.Variable(l)]))
+            expr.Variable(l): type_conversion(expr.Call("To_Base_Integer", [expr.Variable(l)]))
             for t in message.types.values()
             if isinstance(t, model.Enumeration) and t != model.BOOLEAN
             for l in t.literals.keys()
         },
         **{
             expr.Variable(t.package * l): type_conversion(
-                expr.Call("To_U64", [expr.Variable(prefix * t.package * l)])
+                expr.Call("To_Base_Integer", [expr.Variable(prefix * t.package * l)])
             )
             for t in message.types.values()
             if isinstance(t, model.Enumeration) and t != model.BOOLEAN
@@ -937,7 +939,7 @@ def create_sequence_instantiation(
                 str(element_type.size),
                 prefix * element_type_package * f"Valid_{element_type.name}",
                 prefix * element_type_package * "To_Actual",
-                prefix * element_type_package * "To_U64",
+                prefix * element_type_package * "To_Base_Integer",
             ],
         )
     else:

rflx/generator/const.py

@@ -49,6 +49,7 @@
 TYPES_TO_LAST_BIT_INDEX = TYPES * "To_Last_Bit_Index"
 TYPES_OFFSET = TYPES * "Offset"
 TYPES_U64 = TYPES * "U64"
+TYPES_BASE_INT = TYPES * "Base_Integer"
 TYPES_BYTE_ORDER = TYPES * "Byte_Order"
 TYPES_HIGH_ORDER_FIRST = TYPES * "High_Order_First"
 TYPES_LOW_ORDER_FIRST = TYPES * "Low_Order_First"

rflx/generator/generator.py

@@ -84,7 +84,7 @@
     WithClause,
 )
 from rflx.common import file_name
-from rflx.const import BUILTINS_PACKAGE, INTERNAL_PACKAGE
+from rflx.const import BUILTINS_PACKAGE, INTERNAL_PACKAGE, MAX_SCALAR_SIZE
 from rflx.error import Subsystem, fail, warn
 from rflx.integration import Integration
 from rflx.model import (
@@ -316,7 +316,7 @@ def _create_unit(  # pylint: disable = too-many-arguments
                 formal_parameters=formal_parameters,
                 aspects=[
                     SparkMode(),
-                    *([Annotate("GNATprove", "Terminating")] if terminating else []),
+                    *([Annotate("GNATprove", "Always_Return")] if terminating else []),
                     *aspects,
                 ],
             ),
@@ -719,7 +719,7 @@ def _integer_functions(self, integer: Integer) -> UnitPart:
                 ),
                 *(
                     [expr.LessEqual(expr.Variable("Val"), integer.last)]
-                    if integer.last.simplified() != expr.Number(2**64 - 1)
+                    if integer.last.simplified() != expr.Number(2**MAX_SCALAR_SIZE - 1)
                     else []
                 ),
             ).simplified()
@@ -738,7 +738,7 @@ def _integer_functions(self, integer: Integer) -> UnitPart:
                 ]
             )
         else:
-            specification.append(UseTypeClause(self._prefix * const.TYPES_U64))
+            specification.append(UseTypeClause(self._prefix * const.TYPES_BASE_INT))
 
         specification.append(
             self._type_validation_function(integer.name, "Val", constraints.ada_expr())
@@ -760,14 +760,14 @@ def _integer_functions(self, integer: Integer) -> UnitPart:
         return UnitPart(specification)
 
     def _enumeration_functions(self, enum: Enumeration) -> UnitPart:
-        incomplete = len(enum.literals) < 2**64
+        incomplete = len(enum.literals) < 2**MAX_SCALAR_SIZE
 
         specification: ty.List[Declaration] = []
 
         validation_expression = (
             (
                 Less(Variable("Val"), Pow(Number(2), enum.size.ada_expr()))
-                if enum.size.simplified() != expr.Number(64)
+                if enum.size.simplified() != expr.Number(MAX_SCALAR_SIZE)
                 else TRUE
             )
             if enum.always_valid
@@ -777,7 +777,7 @@ def _enumeration_functions(self, enum: Enumeration) -> UnitPart:
         )
 
         if validation_expression != TRUE:
-            specification.append(UseTypeClause(self._prefix * const.TYPES_U64))
+            specification.append(UseTypeClause(self._prefix * const.TYPES_BASE_INT))
 
         specification.append(
             self._type_validation_function(
@@ -811,8 +811,8 @@ def _enumeration_functions(self, enum: Enumeration) -> UnitPart:
         specification.append(
             ExpressionFunctionDeclaration(
                 FunctionSpecification(
-                    "To_U64",
-                    self._prefix * const.TYPES_U64,
+                    "To_Base_Integer",
+                    self._prefix * const.TYPES_BASE_INT,
                     [
                         Parameter(
                             ["Enum"],
@@ -835,7 +835,7 @@ def _enumeration_functions(self, enum: Enumeration) -> UnitPart:
         conversion_function = FunctionSpecification(
             "To_Actual",
             self._prefix * ID(enum.identifier),
-            [Parameter(["Val"], self._prefix * const.TYPES_U64)],
+            [Parameter(["Val"], self._prefix * const.TYPES_BASE_INT)],
         )
         precondition = Precondition(Call(f"Valid_{enum.name}", [Variable("Val")]))
         conversion_cases: ty.List[ty.Tuple[Expr, Expr]] = []
@@ -869,17 +869,16 @@ def _enumeration_functions(self, enum: Enumeration) -> UnitPart:
             specification.append(
                 ExpressionFunctionDeclaration(
                     FunctionSpecification(
-                        "To_U64",
-                        self._prefix * const.TYPES_U64,
+                        "To_Base_Integer",
+                        self._prefix * const.TYPES_BASE_INT,
                         [Parameter(["Val"], self._prefix * ID(enum.identifier))],
                     ),
                     If(
-                        [(Variable("Val.Known"), Call("To_U64", [Variable("Val.Enum")]))],
+                        [(Variable("Val.Known"), Call("To_Base_Integer", [Variable("Val.Enum")]))],
                         Variable("Val.Raw"),
                     ),
                 )
             )
-
         else:
             conversion_cases.extend(
                 [
@@ -1313,7 +1312,7 @@ def _type_validation_function(
             FunctionSpecification(
                 f"Valid_{type_name}",
                 "Boolean",
-                [Parameter([enum_value], self._prefix * const.TYPES_U64)],
+                [Parameter([enum_value], self._prefix * const.TYPES_BASE_INT)],
             ),
             validation_expression,
         )
@@ -1322,17 +1321,17 @@ def _integer_conversion_functions(self, integer: Integer) -> ty.Sequence[Subprog
         return [
             ExpressionFunctionDeclaration(
                 FunctionSpecification(
-                    "To_U64",
-                    self._prefix * const.TYPES_U64,
+                    "To_Base_Integer",
+                    self._prefix * const.TYPES_BASE_INT,
                     [Parameter(["Val"], self._prefix * ID(integer.identifier))],
                 ),
-                Call(self._prefix * const.TYPES_U64, [Variable("Val")]),
+                Call(self._prefix * const.TYPES_BASE_INT, [Variable("Val")]),
             ),
             ExpressionFunctionDeclaration(
                 FunctionSpecification(
                     "To_Actual",
                     self._prefix * ID(integer.identifier),
-                    [Parameter(["Val"], self._prefix * const.TYPES_U64)],
+                    [Parameter(["Val"], self._prefix * const.TYPES_BASE_INT)],
                 ),
                 Call(self._prefix * ID(integer.identifier), [Variable("Val")]),
                 [Precondition(Call(f"Valid_{integer.name}", [Variable("Val")]))],
@@ -1444,7 +1443,7 @@ def enumeration_types(enum: Enumeration) -> ty.List[Declaration]:
                     "Known",
                     [
                         Variant([TRUE], [Component("Enum", common.enum_name(enum))]),
-                        Variant([FALSE], [Component("Raw", const.TYPES_U64)]),
+                        Variant([FALSE], [Component("Raw", const.TYPES_BASE_INT)]),
                     ],
                 ),
             )