copilot-core: ROS, FPrime and Copilot backends expect handlers to be named differently

[Andersen0]

Issue: Linker Error During Compilation of ROS Application

Summary

I am encountering a linker error towards the end of compiling a ROS application, specifically with undefined references to various handlers. This issue is preventing the successful build of the copilot package.

Details

The compilation process fails with the following linker error:
collect2: error: ld returned 1 exit status

Affected Environment

• ROS2 Version: Humble Hawksbill
• Operating System: Ubuntu 22.04.4 LTS (Jammy Jellyfish)(https://releases.ubuntu.com/jammy)

Steps to Reproduce

• Download the ROS application source code: ros_demo.zip
• Attempt to build the application using colcon build.

Expected Behavior

The application should compile successfully without any linker errors.

Actual Behavior

The build process fails with a linker error related to undefined references to handlers.

Additional Context

Terminal output showcasing the error:

Please note that the undefined reference to "halt" can be ignored for the purposes of this issue.

Request for Assistance

Any insights or suggestions on how to resolve these undefined reference errors would be greatly appreciated. If further information or clarification is needed, please let me know.

[ivanperez-keera]

Description

The Spec to Copilot translator and the FPrime and ROS translators generate handler names in slightly different ways. The latter adds an extra prop to handler names, which means that the combination of both requires a manual edit before they can be integrated.

Type

• Bug: backend generates incompatible code.

Additional context

None.

Requester

• Tage Andersen and Elias Evjen Hartmark (NMBU, Norway)

Method to check presence of bug

Compiling the following trivial spec with both the ROS and the Copilot backends should produce files that can be compiled together without edits:

--- reqs.json
{
  "test_componentSpec": {
    "Functions": [
    ],
    "Internal_variables": [
    ],
    "Other_variables": [
      {
        "name": "a",
        "type": "bool"
      }
    ],
    "Requirements": [
      {
        "CoCoSpecCode": "true",
        "fretish": "unimportant",
        "name": "testCopilot",
        "ptLTL": "a"
      }
    ]
  }
}

--- variable-db
("a","bool","/a","Bool")

Expected result

Compiling the spec above using both the Copilot and the ROS backends should produce a ROS app that includes the monitors and compiles correctly without edits.

Desired result

Compiling the spec above using both the Copilot and the ROS backends should produce a ROS app that includes the monitors and compiles correctly without edits.

Proposed solution

Modify FPrime and ROS app generators to not include the extra "prop" in handler names.

Further notes

None.

[ivanperez-keera]

Change Manager: Confirmed that the issue exists.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

Technical Lead: Issue scheduled for fixing in Ogma 1.3.

Fix assigned to: @ivanperez-keera.

[ivanperez-keera]

Implementor: Solution implemented, review requested.

[ivanperez-keera]

Change Manager: Verified that:

• Solution is implemented:

  • The code proposed compiles passes the tests. Details:
    Docker image:

    FROM ubuntu:trusty
    
    RUN apt-get update
    
    RUN apt-get install --yes software-properties-common
    RUN add-apt-repository ppa:hvr/ghc
    RUN apt-get update
    
    RUN apt-get install --yes ghc-8.6.5 cabal-install-2.4
    RUN apt-get install --yes libz-dev
    
    ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH
    
    RUN cabal update
    RUN cabal v1-sandbox init
    RUN cabal v1-install alex happy
    RUN apt-get install --yes git
    
    # We install the application first and then test it, in case any tests need to
    # run the tool.
    CMD git clone $REPO && \
        cd $NAME && \
        git checkout $COMMIT && \
        cd .. && \
        cabal v1-install $NAME/$PAT**/ --enable-tests && \
        cabal v1-install $NAME/$PAT**/ --enable-tests --run-tests -j1

    Command:

    $ docker run -e "REPO=https://github.com/nasa/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=8082ff83059dec71ac1073dcc5ef3c7ab77ee198" -it ogma-test

  • The solution proposed fixes the issues described. Details:
    The following Dockerfile compiles a spec with the ROS and Copilot standalone backends and uses the ROS tools to build the monitoring application:

    --- Dockerfile-verify-130
    FROM ubuntu:focal
    
    ENV DEBIAN_FRONTEND=noninteractive
    
    RUN apt-get update
    SHELL ["/bin/bash", "-c"]
    
    RUN apt-get install --yes software-properties-common
    RUN add-apt-repository universe
    RUN apt-get update
    RUN apt-get install curl -y
    RUN curl -sSL https://raw.githubusercontent.com/ros/rosdistro/master/ros.key -o /usr/share/keyrings/ros-archive-keyring.gpg
    RUN echo "deb [arch=$(dpkg --print-architecture) signed-by=/usr/share/keyrings/ros-archive-keyring.gpg] http://packages.ros.org/ros2/ubuntu $(source /etc/os-release && echo $UBUNTU_CODENAME) main" | tee /etc/apt/sources.list.d/ros2.list
    RUN apt-get update
    RUN apt-get upgrade -y
    RUN apt-get install -y ros-foxy-ros-base python3-argcomplete
    RUN apt-get install -y ros-dev-tools
    
    RUN add-apt-repository ppa:hvr/ghc
    RUN apt-get update
    
    RUN apt-get install --yes ghc-8.6.5 cabal-install-2.4
    RUN apt-get install --yes libz-dev
    
    ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH
    
    RUN cabal update
    RUN cabal v1-sandbox init
    RUN cabal v1-install alex happy
    RUN cabal v1-install copilot-3.19
    RUN apt-get install --yes git
    
    ADD reqs.json /tmp/reqs.json
    ADD variable-db /tmp/variable-db
    
    CMD git clone $REPO && \
        cd $NAME && \
        git checkout $COMMIT && \
        cd .. && \
        cabal v1-install --force-reinstall $NAME/$PAT**/ && \
        ogma ros --fret-file-name /tmp/reqs.json --variable-db /tmp/variable-db && \
        ogma fret-component-spec --fret-file-name /tmp/reqs.json --target-file-name monitor > CS.hs && \
        cabal v1-exec -- runhaskell CS.hs && \
        mv monitor* ros/src/ && \
        cd ros/ && \
        source /opt/ros/foxy/setup.bash && \
        colcon build && \
        echo "Success"
    
    --- reqs.json
    {
      "test_componentSpec": {
        "Functions": [
        ],
        "Internal_variables": [
        ],
        "Other_variables": [
          {
            "name": "a",
            "type": "bool"
          }
        ],
        "Requirements": [
          {
            "CoCoSpecCode": "true",
            "fretish": "unimportant",
            "name": "testCopilot",
            "ptLTL": "a"
          }
        ]
      }
    }
    
    --- variables-db
    ("a","bool","/a","Bool")

    Command:

    $ docker run -e "REPO=https://github.com/nasa/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=8082ff83059dec71ac1073dcc5ef3c7ab77ee198" -it ogma-verify-130

• Implementation is documented. Details:
  No changes needed.
• Change history is clear.
• Commit messages are clear.
• Changelogs are updated.
• Examples are updated. Details:
  No examples affected.
• Required version bumps are evaluated. Details:
  No bump needed (bug fix).

[ivanperez-keera]

Change Manager: Implementation ready to be merged.