Commit f2fd2b2
committed
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.2 files changed
+56
-1
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
1 | 4 | | |
2 | 5 | | |
3 | 6 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
55 | 55 | | |
56 | 56 | | |
57 | 57 | | |
58 | | - | |
| 58 | + | |
59 | 59 | | |
60 | 60 | | |
61 | 61 | | |
| |||
112 | 112 | | |
113 | 113 | | |
114 | 114 | | |
| 115 | + | |
| 116 | + | |
| 117 | + | |
| 118 | + | |
| 119 | + | |
| 120 | + | |
| 121 | + | |
| 122 | + | |
| 123 | + | |
| 124 | + | |
| 125 | + | |
| 126 | + | |
| 127 | + | |
| 128 | + | |
| 129 | + | |
| 130 | + | |
| 131 | + | |
| 132 | + | |
| 133 | + | |
| 134 | + | |
| 135 | + | |
| 136 | + | |
| 137 | + | |
| 138 | + | |
| 139 | + | |
| 140 | + | |
| 141 | + | |
| 142 | + | |
| 143 | + | |
| 144 | + | |
| 145 | + | |
| 146 | + | |
| 147 | + | |
| 148 | + | |
| 149 | + | |
| 150 | + | |
| 151 | + | |
| 152 | + | |
| 153 | + | |
| 154 | + | |
| 155 | + | |
| 156 | + | |
| 157 | + | |
| 158 | + | |
| 159 | + | |
| 160 | + | |
| 161 | + | |
| 162 | + | |
| 163 | + | |
| 164 | + | |
| 165 | + | |
| 166 | + | |
115 | 167 | | |
116 | 168 | | |
117 | 169 | | |
| |||
0 commit comments