Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'develop-fix-signum'. Close #278.
**Description** The translation of the function `signum` to C99 differs from the meaning of the same function in the interpreter. The C99 backend uses the function `copysign`, whose meaning differs from Haskell's `signum`. For example, as evaluated by the interpreter, `signum 0` returns `0`, but the C99 code generated for it (which executes `copysign(1.0, 0)`), returns `1`. Moreover, when dealing with floating-point numbers, `signum (-0)` and `signum NaN` return `-0` and `NaN`, respectively, in the interpreter, but the C99-based implementation returns `-1.0` and `±1.0` (depending on the sign bit of the `NaN`), respectively. The meaning of all Copilot constructs should be consistent between the interpreter and all backends. **Type** - Bug: the interpreter and the C99 backend assign inconsistent meanings to the same Copilot construct. **Additional context** - See https://github.com/Copilot-Language/copilot/blob/v3.8/copilot-core/src/Copilot/Core/Interpret/Eval.hs#L205 for the evaluation of `Sign` in the interpreter. - See https://github.com/Copilot-Language/copilot/blob/v3.8/copilot-c99/src/Copilot/Compile/C99/Translate.hs#L58 for the translation of `Sign` in the C99 backend. **Requester** - Ryan Scott (@RyanGlScott), Galois Inc. **Method to check presence of bug** The following Copilot specification will present a different result if evaluated in the interpreter or if compiled to C. Dockerfile and auxiliary files follow: ``` --- Dockerfile-verify-278 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 main.c main.c ADD test-278 test-278 ADD Signum.hs Signum.hs RUN chmod a+x test-278 CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. && cabal v1-install copilot/copilot**/ && ./test-278 --- main.c #include <stdint.h> #include <stdio.h> #include "signum.h" uint8_t numsWord8[5] = { 0, 1, 2, 3, 4 }; uint8_t streamWord8; void funcWord8 (uint8_t sign) { printf ("funcWord8,%d\n", sign); } uint16_t numsWord16[5] = { 0, 1, 2, 3, 4 }; uint16_t streamWord16; void funcWord16 (uint16_t sign) { printf ("funcWord16,%d\n", sign); } uint32_t numsWord32[5] = { 0, 1, 2, 3, 4 }; uint32_t streamWord32; void funcWord32 (uint32_t sign) { printf ("funcWord32,%d\n", sign); } uint64_t numsWord64[5] = { 0, 1, 2, 3, 4 }; uint64_t streamWord64; void funcWord64 (uint64_t sign) { printf ("funcWord64,%ld\n", sign); } int8_t numsInt8[5] = { -2, -1, 0, 1, 2 }; int8_t streamInt8; void funcInt8 (int8_t sign) { printf ("funcInt8,%d\n", sign); } int16_t numsInt16[5] = { -2, -1, 0, 1, 2 }; int16_t streamInt16; void funcInt16 (int16_t sign) { printf ("funcInt16,%d\n", sign); } int32_t numsInt32[5] = { -2, -1, 0, 1, 2 }; int32_t streamInt32; void funcInt32 (int32_t sign) { printf ("funcInt32,%d\n", sign); } int64_t numsInt64[5] = { -2, -1, 0, 1, 2 }; int64_t streamInt64; void funcInt64 (int64_t sign) { printf ("funcInt64,%ld\n", sign); } float numsFloat[5] = { -2, -1, 0, 1, 2 }; float streamFloat; void funcFloat (float sign) { printf ("funcFloat,%f\n", sign); } double numsDouble[5] = { -2, -1, 0, 1, 2 }; double streamDouble; void funcDouble (double sign) { printf ("funcDouble,%lf\n", sign); } int main () { int i = 0; for (i=0; i<5; i++) { streamWord8 = numsWord8[i]; streamWord16 = numsWord16[i]; streamWord32 = numsWord32[i]; streamWord64 = numsWord64[i]; streamInt8 = numsInt8[i]; streamInt16 = numsInt16[i]; streamInt32 = numsInt32[i]; streamInt64 = numsInt64[i]; streamFloat = numsFloat[i]; streamDouble = numsDouble[i]; printf ("#\n"); // Step step(); } return 0; } --- Signum.hs {-# LANGUAGE CPP #-} {-# LANGUAGE NoImplicitPrelude #-} -- Copyright © 2021 National Institute of Aerospace / Galois, Inc. -- | An example of a specification using the 'signum' function. module Main where import Data.List (genericLength) import Copilot.Compile.C99 import Language.Copilot numsWord8 :: [Word8] numsWord8 = [0, 1, 2, 3, 4] streamWord8 :: Stream Word8 streamWord8 = extern "streamWord8" (Just numsWord8) numsWord16 :: [Word16] numsWord16 = [0, 1, 2, 3, 4] streamWord16 :: Stream Word16 streamWord16 = extern "streamWord16" (Just numsWord16) numsWord32 :: [Word32] numsWord32 = [0, 1, 2, 3, 4] streamWord32 :: Stream Word32 streamWord32 = extern "streamWord32" (Just numsWord32) numsWord64 :: [Word64] numsWord64 = [0, 1, 2, 3, 4] streamWord64 :: Stream Word64 streamWord64 = extern "streamWord64" (Just numsWord64) numsInt8 :: [Int8] numsInt8 = [-2, -1, 0, 1, 2] streamInt8 :: Stream Int8 streamInt8 = extern "streamInt8" (Just numsInt8) numsInt16 :: [Int16] numsInt16 = [-2, -1, 0, 1, 2] streamInt16 :: Stream Int16 streamInt16 = extern "streamInt16" (Just numsInt16) numsInt32 :: [Int32] numsInt32 = [-2, -1, 0, 1, 2] streamInt32 :: Stream Int32 streamInt32 = extern "streamInt32" (Just numsInt32) numsInt64 :: [Int64] numsInt64 = [-2, -1, 0, 1, 2] streamInt64 :: Stream Int64 streamInt64 = extern "streamInt64" (Just numsInt64) numsFloat :: [Float] numsFloat = [-2, -1, 0, 1, 2] streamFloat :: Stream Float streamFloat = extern "streamFloat" (Just numsFloat) numsDouble :: [Double] numsDouble = [-2, -1, 0, 1, 2] streamDouble :: Stream Double streamDouble = extern "streamDouble" (Just numsDouble) spec :: Spec spec = do trigger "funcWord8" true [arg (signum streamWord8)] trigger "funcWord16" true [arg (signum streamWord16)] trigger "funcWord32" true [arg (signum streamWord32)] trigger "funcWord64" true [arg (signum streamWord64)] trigger "funcInt8" true [arg (signum streamInt8)] trigger "funcInt16" true [arg (signum streamInt16)] trigger "funcInt32" true [arg (signum streamInt32)] trigger "funcInt64" true [arg (signum streamInt64)] trigger "funcFloat" true [arg (signum streamFloat)] trigger "funcDouble" true [arg (signum streamDouble)] main :: IO () main = do spec' <- reify spec #ifdef INTERPRET csv (genericLength numsInt32) spec #else compile "signum" spec' #endif --- test-278 #!/bin/bash # Used to locate imports and other scripts MY_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" COPILOT_SPEC="${MY_DIR}/Signum.hs" COPILOT_C="${MY_DIR}/signum" MAIN_C="${MY_DIR}/main.c" MAIN="${MY_DIR}/main" set -x set -e cabal v1-exec -- runhaskell -DINTERPRET ${COPILOT_SPEC} | grep -ve '^Note' > output-interpreter cabal v1-exec -- runhaskell ${COPILOT_SPEC} gcc -o ${MAIN} ${MAIN_C} ${COPILOT_C}.c # We modify the output to limit trailing zeroes since the Haskell interpreter does that ./main | sed -e 's/\.0\+/.0/g' > output-compiled diff output-interpreter output-compiled echo Success ``` It can be executed with: ``` docker run -e "REPO=<REPO_URL>" -e "NAME=<DIR>" -e "COMMIT=<TAG_BRANCH_OR_HASH>" -it copilot-verify-278 ``` **Expected result** The above script should print the text Success if the bug is not present. If the bug is present, the differences between the output from the interpreter and the compiled code for the examples tried will be presented. **Solution implemented** Replaces the `copysign`-based implementation such that `signum e` now returns `e > 0 ? 1 : (e < 0 ? -1 : e)`. This new implementation follows the definition of signum in Haskell's base, including for cases where `e` is `±0` or `NaN`. **Further notes** The solution proposed above is consistent with the implementation in the `base` library Haskell (used by the interpreter): https://gitlab.haskell.org/ghc/ghc/-/blob/aed98ddaf72cc38fb570d8415cac5de9d8888818/libraries/base/GHC/Float.hs#L523-L525 This summary borrows from @RyanGlScott message, commit summaries, and pull request. The change was implemented by Ryan Scott and further modified by Ivan Perez.
- Loading branch information
