`copilot-c99`: Pass output arrays as arguments to trigger argument functions. Refs #431.

[RyanGlScott]

This commit changes array trigger argument functions so that they receive a pointer to an array for the output argument. The part of the generated code that applies the trigger argument functions has also been updated accordingly such that when the argument has an array type, the output array is passed directly as an argument (e.g., f_arg0(temp_array)) rather than being assigned (e.g., temp_array = f_arg0()).

Addresses #431.

[ivanperez-keera]

Change Manager: Verified that:

• Solution is implemented:

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

  • [X] The solution proposed produces the expected result. Details: The following Dockerfile checks that passing a stream of arrays as an argument to a trigger, when compiled with and without optimizations, produces the same results, in which case it prints the message Success. The docker image produces a diff of the two outputs if not.

    
    --- Dockerfile-verify-431
    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

  ADD Array.hs /tmp/Array.hs ADD array_driver.c /tmp/array_driver.c

  SHELL ["/bin/bash", "-c"] CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \ && cabal v1-install $NAME/copilot**/ \ && cabal v1-exec -- runhaskell /tmp/Array.hs \ && gcc -O0 /tmp/array_driver.c array.c -I. -o main-no-op && ./main-no-op > no-optimizations \ && gcc -O /tmp/array_driver.c array.c -I. -o main-op && ./main-op > with-optimizations \ && diff no-optimizations with-optimizations \ && echo "Success"

  --- Array.hs {-# LANGUAGE DataKinds #-} module Main where

  import Copilot.Compile.C99 import Language.Copilot import qualified Prelude as P

  spec :: Spec spec = trigger "f" true [arg stream] where stream :: Stream (Array 2 Int16) stream = constant (array [3,4])

  main :: IO () main = reify spec >>= compile "array"

  --- array_driver.c

  include

  include

  include "array_types.h"

  include "array.h"

  void f (int16_t f_arg0[(2)]) { printf("([%d,%d])\n", f_arg0[0], f_arg0[1]); }

  int main(void) { int i = 0;

  printf("f:\n");

  for (i=0; i<5; i++) { step(); } return 0; }

  Command (adjust repo as necessary):

  $ docker run -e "REPO=https://github.com/GaloisInc/copilot-1" -e "NAME=copilot-1" -e "COMMIT=e975b4a0e007241f14e1c1032f46111ec4d69e83" -it copilot-verify-431

• [X] Implementation is documented. Details: Internal change. No changes to the public documentation are needed. Comments are added to new internal functions.
• [X] Change history is clear.
• [X] Commit messages are clear.
• [X] Changelogs are updated.
• [X] Examples are updated. Details: No updates needed.
• [X] Required version bumps are evaluated. Details: Bump not needed. This change is internal. The bug fix is in a function in a hidden module, the changes do not affect how to interface with the C code produced, and any new functions introduced are not exposed.