Issue 494, 650, 659, 663, 665, 669: Switch to GNAT Community 2021 and add preparatory work for session support

.github/workflows/tests.yml

@@ -16,7 +16,7 @@ jobs:
       - id: skip_check
         uses: fkirc/skip-duplicate-actions@v3.4.0
         with:
-          paths_ignore: '["*.gpr", "examples/apps/**", "tests/spark/**"]'
+          paths_ignore: '["*.gpr", "examples/**", "tests/spark/**"]'
 
   checks:
     name: Checks
@@ -51,7 +51,7 @@ jobs:
         key: ${{ runner.os }}-python${{ env.PYTHON_VERSION }}-${{ hashFiles('setup.py', '*.cfg', '*.ini', '.pylintrc', '.flake8') }}
     - name: Install toolchain
       if: ${{ needs.skip_check_general.outputs.should_skip != 'true' }}
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
     - name: Install dependencies
@@ -85,8 +85,7 @@ jobs:
         python -m pip install --upgrade pip wheel
     - name: Install
       run: |
-        python setup.py sdist
-        pip install RecordFlux --no-deps --no-index --find-links dist/
+        make test_installation
 
   skip_check_python:
     name: Skip Check Python
@@ -144,7 +143,7 @@ jobs:
         key: ${{ runner.os }}-python${{ env.PYTHON_VERSION }}-${{ hashFiles('setup.py', '*.cfg', '*.ini', '.pylintrc', '.flake8') }}
     - name: Install toolchain
       if: ${{ needs.skip_check_python.outputs.should_skip != 'true' }}
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
     - name: Install dependencies
@@ -195,7 +194,7 @@ jobs:
           ~/.local/bin
         key: ${{ runner.os }}-python${{ env.PYTHON_VERSION }}-${{ hashFiles('setup.py', '*.cfg', '*.ini', '.pylintrc', '.flake8') }}
     - name: Install toolchain
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
     - name: Install dependencies
@@ -241,7 +240,7 @@ jobs:
         submodules: true
     - name: Install toolchain
       if: ${{ needs.skip_check_spark.outputs.should_skip != 'true' }}
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
     - name: Test
@@ -259,19 +258,12 @@ jobs:
       with:
         submodules: true
     - name: Install toolchain
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
-    - name: Build runtime
-      run: |
-        git clone https://github.com/Componolit/ada-runtime
-        cd ada-runtime
-        git checkout 280a4867f1d872412aec00f35aa28b35ff295e60
-        cd ..
-        make -C ada-runtime
     - name: Build
       run: |
-        gprbuild -Ptest --RTS=ada-runtime/build/posix/obj -Xaunit=no -Xoptimization=yes
+        make test_runtime
 
   verification_spark:
     name: Verification
@@ -291,6 +283,7 @@ jobs:
           - "sequence"
           - "derivation"
           - "expression"
+          - "fixed_size"
     steps:
     - uses: actions/checkout@v2
       if: ${{ needs.skip_check_spark.outputs.should_skip != 'true' }}
@@ -316,7 +309,7 @@ jobs:
         key: ${{ runner.os }}-python${{ env.PYTHON_VERSION }}-${{ hashFiles('setup.py', '*.cfg', '*.ini', '.pylintrc', '.flake8') }}
     - name: Install toolchain
       if: ${{ needs.skip_check_spark.outputs.should_skip != 'true' }}
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
     - name: Install dependencies
@@ -362,7 +355,7 @@ jobs:
           ~/.local/bin
         key: ${{ runner.os }}-python${{ env.PYTHON_VERSION }}-${{ hashFiles('setup.py', '*.cfg', '*.ini', '.pylintrc', '.flake8') }}
     - name: Install toolchain
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
     - name: Install dependencies
@@ -424,7 +417,7 @@ jobs:
         key: ${{ runner.os }}-python${{ env.PYTHON_VERSION }}-${{ hashFiles('setup.py', '*.cfg', '*.ini', '.pylintrc', '.flake8') }}
     - name: Install toolchain
       if: ${{ needs.skip_check_apps.outputs.should_skip != 'true' }}
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
     - name: Install dependencies
@@ -471,7 +464,7 @@ jobs:
           ~/.local/bin
         key: ${{ runner.os }}-python${{ env.PYTHON_VERSION }}-${{ hashFiles('setup.py', '*.cfg', '*.ini', '.pylintrc', '.flake8') }}
     - name: Install toolchain
-      uses: ada-actions/toolchain@ce2020
+      uses: ada-actions/toolchain@ce2021
       with:
         distrib: community
     - name: Install dependencies
@@ -484,3 +477,62 @@ jobs:
     - name: Verify
       run: |
         make prove_apps
+
+  skip_check_specs:
+    name: Skip Check Specs
+    continue-on-error: true
+    runs-on: ubuntu-latest
+    outputs:
+      should_skip: ${{ steps.skip_check.outputs.should_skip }}
+    steps:
+      - id: skip_check
+        uses: fkirc/skip-duplicate-actions@v3.4.0
+        with:
+          paths: '["defaults.gpr", "examples/specs/**", "rflx/**"]'
+
+  tests_specs:
+    name: Tests (specs)
+    needs: skip_check_specs
+    runs-on: ubuntu-20.04
+    steps:
+    - uses: actions/checkout@v2
+      if: ${{ needs.skip_check_specs.outputs.should_skip != 'true' }}
+      with:
+        submodules: true
+    - name: Set up Python ${{ matrix.python-version }}
+      if: ${{ needs.skip_check_specs.outputs.should_skip != 'true' }}
+      uses: actions/setup-python@v2
+      with:
+        python-version: 3.7
+    - name: Determine exact Python version
+      if: ${{ needs.skip_check_specs.outputs.should_skip != 'true' }}
+      run:
+        echo "PYTHON_VERSION=$(python -c 'import platform; print(platform.python_version())')" >> $GITHUB_ENV
+    - name: Cache Python dependencies
+      if: ${{ needs.skip_check_specs.outputs.should_skip != 'true' }}
+      uses: actions/cache@v2
+      with:
+        path: |
+          ~/.cache/pip
+          ~/.local/lib/python${{ matrix.python-version }}/site-packages
+          ~/.local/bin
+        key: ${{ runner.os }}-python${{ env.PYTHON_VERSION }}-${{ hashFiles('setup.py', '*.cfg', '*.ini', '.pylintrc', '.flake8') }}
+    - name: Install toolchain
+      if: ${{ needs.skip_check_specs.outputs.should_skip != 'true' }}
+      uses: ada-actions/toolchain@ce2021
+      with:
+        distrib: community
+    - name: Install dependencies
+      if: ${{ needs.skip_check_specs.outputs.should_skip != 'true' }}
+      run: |
+        echo "$HOME/.local/bin" >> $GITHUB_PATH
+        echo "PYTHONPATH=$PWD" >> $GITHUB_ENV
+        echo "HYPOTHESIS_PROFILE=ci" >> $GITHUB_ENV
+        echo "PYTEST_ADDOPTS=--basetemp=build" >> $GITHUB_ENV
+        sudo apt install graphviz libgmp-dev patchelf
+        python -m pip install --upgrade pip wheel
+        pip install .[devel]
+    - name: Test
+      if: ${{ needs.skip_check_specs.outputs.should_skip != 'true' }}
+      run: |
+        make test_specs

.gitignore

@@ -13,5 +13,4 @@ dist
 gnatinspect.db
 htmlcov
 why3session.xml.bak
-why3shapes.gz
 why3shapes.gz.bak

Makefile

@@ -20,7 +20,8 @@ test-files := $(addprefix $(noprefix-dir)/, $(subst /rflx-,/,$(test-files)))
 endif
 
 .PHONY: check check_black check_isort check_flake8 check_pylint check_mypy format \
-	test test_python test_spark test_apps prove prove_tests prove_apps clean
+	test test_python test_spark test_apps test_specs test_runtime \
+	prove prove_tests prove_apps clean
 
 all: check test prove
 
@@ -57,7 +58,7 @@ format:
 	black -l 100 $(python-packages) ide/gnatstudio
 	isort $(python-packages) ide/gnatstudio
 
-test: test_python_coverage test_python_property test_spark
+test: test_python_coverage test_python_property test_spark test_runtime test_installation
 
 test_python:
 	python3 -m pytest -n$(shell nproc) -vv -m "not hypothesis" tests
@@ -89,7 +90,23 @@ test_spark_optimized: $(test-files)
 	$(test-bin)
 
 test_apps:
-	python3 -m pytest -n$(shell nproc) -vv -m "root or not root" tests/integration/example_apps_test.py
+	python3 examples/apps/icmp_socket.py
+	$(MAKE) -C examples/apps/ping test_python
+	$(MAKE) -C examples/apps/ping test_spark
+
+test_specs:
+	cd examples/specs && python3 -m pytest -n$(shell nproc) -vv tests/test_specs.py
+
+test_runtime:
+	rm -rf $(build-dir)/ada-runtime
+	git clone --depth=1 --branch recordflux https://github.com/Componolit/ada-runtime $(build-dir)/ada-runtime
+	$(MAKE) -C build/ada-runtime
+	gprbuild -Ptest --RTS=build/ada-runtime/build/posix/obj -Xaunit=no -Xoptimization=yes
+
+test_installation:
+	rm -rf $(build-dir)/pip
+	python setup.py sdist
+	pip install RecordFlux --no-deps --no-index --find-links dist/ --target $(build-dir)/pip
 
 prove: prove_tests prove_apps
 

README.md

@@ -268,7 +268,7 @@ if parse_message(b"\x01\x00\x04\x01\x02\x03\x04") != create_message():
 
 As a prerequisite, the following dependencies need to be installed:
 
-- [GNAT Community](https://www.adacore.com/download) >= 2020
+- [GNAT Community](https://www.adacore.com/download) >= 2021
 - [GMP](https://gmplib.org/) This is provided as a package for various distributions, e.g., libgmp-dev (Debian/Ubuntu), gmp-devel (Fedora) or gmp (Arch Linux).
 
 RecordFlux can be installed from PyPI:

defaults.gpr

@@ -8,9 +8,10 @@ abstract project Defaults is
       "--memlimit=1000",
       "--checks-as-errors",
       "--warnings=error",
-      "--proof-warnings",
+      --  ISSUE: Componolit/RecordFlux#670
+      --  "--proof-warnings",
       "--no-axiom-guard",
-      "--no-counterexample",
+      "--counterexamples=off",
       "-j0"
    );
 

doc/Language-Reference.md

@@ -79,6 +79,10 @@ type Ether_Type is
 with Size => 16, Always_Valid;
 ```
 
+### Boolean
+
+`Boolean` is a built-in enumeration type with the literals `False => 0` and `True => 1` with a size of 1 bit.
+
 ## Message Type
 
 A message type is a collection components. Additional then clauses allow to define conditions and dependencies between components.
@@ -87,7 +91,7 @@ A message type is a collection components. Additional then clauses allow to defi
 
 *message_type* ::= __type__ *name* __is__ *message_definition* __;__
 
-*message_definition* ::= __message__ [ *null_component* ] *component* { *component* } __end message__ | __null message__
+*message_definition* ::= __message__ [ *null_component* ] *component* { *component* } __end message__ [ __with__ *message_aspects* ] | __null message__
 
 *component* ::= *component_name* __:__ *component_type*
                    [__with__ *aspects*]
@@ -115,11 +119,29 @@ A message type is a collection components. Additional then clauses allow to defi
 
 *condition* ::= *boolean_expression*
 
+*message_aspects* ::= *message_aspect* { __,__ *message_aspect* }
+
+*message_aspect* ::= *checksum_aspect*
+
+*checksum_aspect* ::= __Checksum__ __=>__ (*checksum_definition* { __,__ *checksum_definition* })
+
+*checksum_definition* ::= *name* __=>__ (*checksum_element* { __,__ *checksum_element* }
+
+*checksum_element* ::= *name* | *name* __'Size__ | *field_range*
+
+*field_range* ::= *field_range_first* __..__ *field_range_last*
+
+*field_range_first* ::= *name* __'First__ | *name* __'Last + 1__
+
+*field_range_last* ::= *name* __'Last | *name* __'First - 1__
+
 #### Static Semantics
 
 A message type specifies the message format of a protocol. Each component corresponds to one field in a message. A then clause of a component allows to define which field follows. If no then clause is given, it is assumed that always the next component of the message follows. If no further component follows, it is assumed that the message ends with this field. The end of a message can also be denoted explicitly by adding a then clause to __null__. Optionally a then clause can contain a condition under which the corresponding field follows and aspects which allow to define the size of the next field and the location of its first bit. These aspects can also be specified in the component. Each aspect can be specified either in the component or in all incoming then clauses, but not in both. The condition can refer to previous fields (including the component containing the then clause). A condition can also be added to a component. A component condition is equivalent to adding a condition to all incoming then clauses. If a component condition as well as a condition at an incoming then clause exists, both conditions are combined by a logical conjunction. If required, a null component can be used to specify the size of the first field in the message. An empty message can be represented by a null message.
 
-The size of a message must be a multiple of 8 bit. Opaque fields and sequence fields must be byte aligned.
+The field type `Opaque` represents an unconstrained sequence of bytes. The size of opaque fields must be always defined by a size aspect. Opaque fields and sequence fields must be byte aligned. The size of a message must be a multiple of 8 bit.
+
+A checksum aspect specifies which parts of a message is covered by a checksum. The definition of the checksum calculation is not part of the specification. Code based on the message specification must provide a function which is able to verify a checksum using the specified checksum elements. A checksum element can be a field value, a field size or a range of fields. The point where a checksum should be checked during parsing or generated during serialization must be defined for each checksum. For this purpose the `Valid_Checksum` attribute is added to a condition. All message parts on which the checksum depends have to be known at this point.
 
 #### Example
 

examples/apps/ping/ping.gpr

@@ -30,18 +30,7 @@ project Ping is
 
    package Prove is
       for Proof_Dir use "proof";
-
-      for Proof_Switches ("Ada") use (
-         "-j0",
-         "--prover=cvc4,z3,altergo",
-         "--steps=0",
-         "--timeout=90",
-         "--memlimit=1000",
-         "--checks-as-errors",
-         "--warnings=error",
-         "--proof-warnings",
-         "--no-axiom-guard"
-      );
+      for Proof_Switches ("Ada") use Defaults.Proof_Switches;
    end Prove;
 
 end Ping;