Copilot-Language/copilot

`copilot-theorem`: Introduce testing infrastructure

ivanperez-keera opened this issue · 6 comments

ivanperez-keera commented

Description

As part of the requirements for Class D (NPR7150.2C), we need unit tests for all of copilot.

A natural next step is to introduce the testing infrastructure for copilot-theorem.

Type

  • Management: conformance with new requirement.

Additional context

None.

Requester

  • Ivan Perez

Method to check presence of bug

Not applicable (not a bug).

Expected result

The library copilot-theorem includes tests for what4. Introducing (some classes of) errors in the implementation of copilot-theorem makes the tests detect those errors.

Desired result

The library copilot-theorem includes tests for what4. Introducing (some classes of) errors in the implementation of copilot-theorem makes the tests detect those errors.

Proposed solution

Add tests for copilot-theorem that tests basic properties whose result is known with one of the existing backends.

Further notes

Due to the magnitude of this change, we decide to simplify the issue in three ways:

  • Focus only on what4, which is likely going to replace other backends in copilot-theorem.
  • Focus only on one of the SMT solvers.
  • Focus only on the core of the infrastructure, leaving it to a future issue to have a more comprehensive list of properties.
ivanperez-keera commented

Change Manager: Confirmed that the issue exists.

ivanperez-keera commented

Technical Lead: Confirmed that the issue should be addressed.

ivanperez-keera commented

Technical Lead: Issue scheduled for fixing in Copilot 3.18.

Fix assigned to: @ivanperez-keera .

ivanperez-keera commented

Implementor: Solution implemented, review requested.

ivanperez-keera commented

Change Manager: Verified that:

  • Solution is implemented:

    • The code proposed compiles and passes all tests. Details:
      Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/267963797

    • The solution proposed produces the expected result. Details:
      The following Dockerfile checks that copilot-theorem's tests can be executed, in which case it prints the message Success:

      --- Dockerfile-verify-474
FROM ubuntu:focal

RUN apt-get update

RUN apt-get install --yes libz-dev
RUN apt-get install --yes git

RUN apt-get install --yes wget
RUN mkdir -p $HOME/.ghcup/bin
RUN wget https://downloads.haskell.org/~ghcup/0.1.19.2/x86_64-linux-ghcup-0.1.19.2 -O $HOME/.ghcup/bin/ghcup

RUN chmod a+x $HOME/.ghcup/bin/ghcup
ENV PATH=$PATH:/root/.ghcup/bin/
ENV PATH=$PATH:/root/.cabal/bin/
RUN apt-get install --yes curl
RUN apt-get install --yes gcc make libgmp3-dev g++

SHELL ["/bin/bash", "-c"]

RUN ghcup install ghc 9.4.7
RUN ghcup install cabal 3.8
RUN ghcup set ghc 9.4.7
RUN cabal update

RUN apt-get install --yes z3

CMD git clone $REPO && \
    cd $NAME && \
    git checkout $COMMIT && \
    cd copilot-theorem && \
    cabal test copilot-theorem:unit-tests && \
    echo Success

      Command (adjust repo as necessary):

      $ docker run -e "REPO=https://github.com/ivanperez-keera/copilot" -e "NAME=copilot" -e "COMMIT=e717ae2620bfd7cf8e2339addb74eb2c7e1f64ea" -it copilot-verify-474
  • Implementation is documented. Details:
    Change to tests. No changes to the public documentation are needed. Comments are added to all new modules and functions.
  • Change history is clear.
  • Commit messages are clear.
  • Changelogs are updated.
  • Examples are updated. Details:
    No updates needed.
  • Required version bumps are evaluated. Details:
    Bump not needed. This is a change to the tests.
ivanperez-keera commented

Change Manager: Implementation ready to be merged.