copilot-c99: Raise error when compiling empty array or struct. Refs #695.

[chathhorn-galois]

Copilot allows defining empty arrays (i.e., values of type Array 0) and empty structs (i.e., structs with no fields), but using empty arrays or structs in C99 is undefined behavior. copilot-c99 will often crash if you attempt to compile a Copilot specification that uses an empty array or struct with an unhelpful error message (NonEmpty.fromList: empty list), but even if it doesn't, you're left with an invalid C program.

This PR adds a check for attempts to translate specs that contain zero-length arrays or structs with no fields and raises an appropriate error, preventing such specs from being translated into invalid C.

Fixes#695.

[ivanperez-keera]

Change Manager: Can you please change the commit messages to the following.

First commit:

copilot-c99: Raise error when compiling empty array or struct. Refs #695.
Copilot allows defining empty arrays (i.e., values of type Array 0) and empty
structs (i.e., structs with no fields), but using empty arrays or structs in
C99 is undefined behavior. Moreover, copilot-c99 will often crash if you
attempt to compile a Copilot specification that uses an empty array or struct.
This commit raises an appropriate error when attempting to translate a
zero-length array or a struct with no fields to C99. Previously, Copilot would
either crash with a confusing error or silently translate the offending spec to
invalid C99.

Second commit:

copilot-c99: Test for error when compiling empty array or struct. Refs #695.
Copilot allows defining empty arrays (i.e., values of type Array 0) and empty
structs (i.e., structs with no fields), but using empty arrays or structs in
C99 is undefined behavior. Moreover, copilot-c99 will often crash if you
attempt to compile a Copilot specification that uses an empty array or struct.
A prior commit introduced a solution for this problem that makes the C99
backend detect these undesired struct or array types.
This commit adds a test to check that attempting to compile specs containing
zero-length arrays or empty structs to C99 raises an appropriate error.

Commit 3:

copilot-c99: Document changes in CHANGELOG. Refs #695.

[chathhorn]

Implementor: Fix implemented, review requested.

[ivanperez-keera]

Change Manager: Process deviation.

Change Manger communicated with Implementor via email to notify of required change. Hand off back to Change Manager for verification communicated via email by Implementor.

[ivanperez-keera]

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/277630107
  • The solution proposed produces the expected result. Details:
    The following Dockerfile checks that compiling an empty struct or array raises fails during compilation, after which it prints the message Success:

    --- Dockerfile-verify-695
    FROM ubuntu:focal
    ENV DEBIAN_FRONTEND=noninteractive
    SHELL ["/bin/bash", "-c"]
    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 git alex happy
    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
    ADD EmptyArray.hs /tmp/
    ADD EmptyStruct.hs /tmp/
    CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
    && cabal v1-install \
    $NAME/copilot \
    $NAME/copilot-c99 \
    $NAME/copilot-core \
    $NAME/copilot-interpreter \
    $NAME/copilot-language \
    $NAME/copilot-libraries \
    $NAME/copilot-prettyprinter \
    $NAME/copilot-theorem \
    && ! cabal v1-exec -- runhaskell /tmp/EmptyArray.hs \
    && ! cabal v1-exec -- runhaskell /tmp/EmptyStruct.hs \
    && echo "Success"
    --- EmptyArray.hs
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE NoImplicitPrelude #-}
    module Main (main) where
    import Copilot.Compile.C99 (compile)
    import Language.Copilot
    main :: IO ()
    main = do
    spec' <- reify spec
    compile "empty_array" spec'
    spec :: Spec
    spec = trigger "trig" true [arg arrs]
    arrs :: Stream (Array 0 Bool)
    arrs = constant (array [])
    --- EmptyStruct.hs
    {-# LANGUAGE DeriveGeneric #-}
    {-# LANGUAGE NoImplicitPrelude #-}
    module Main (main) where
    import GHC.Generics (Generic)
    import Copilot.Compile.C99 (compile)
    import Language.Copilot
    main :: IO ()
    main = do
    spec' <- reify spec
    compile "empty_struct" spec'
    spec :: Spec
    spec = trigger "trig" true [arg structs]
    structs :: Stream Empty
    structs = constant Empty
    -- * Empty struct type
    data Empty = Empty
    deriving Generic
    instance Struct Empty where
    typeName = typeNameDefault
    toValues = toValuesDefault
    updateField = updateFieldDefault
    instance Typed Empty where
    typeOf = typeOfDefault
    

    Command (substitute variables based on new path after merge):

    $ docker run -e REPO=https://github.com/GaloisInc/copilot-1 -e NAME=copilot-1 -e COMMIT=a0126958b9899c2c26ae7907aa66a6aad17e6750 copilot-verify-695
    

• Implementation is documented. Details:
  The new functions introduced are documented, and the error cases are documented.
• Change history is clear.
• Commit messages are clear.
• Changelogs are updated.
• Examples are updated. Details:
  No updates needed; change does not affect any examples.
• Author is internal or has provided signed CLA.
• Required version bumps are evaluated. Details:
  Bump required; some specs that Copilot used to accept, even if it produced invalid C code for, are now no longer accepted by Copilot.