Skip to content

Commit 957407e

Browse files
copilot-c99: Fix issue in C99 implementation of signum. Refs #278.
copilot-c99's 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. This commit 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`. It is possible to reproduce the error, and check the fix, by comparing the output of the compiled code and the interpreter for a stream with signum. For example, given the following specification: ``` {-# LANGUAGE CPP #-} {-# LANGUAGE NoImplicitPrelude #-} -- | An example of a specification using the 'signum' function. module Main where import Data.List (genericLength) import Copilot.Compile.C99 import Language.Copilot nums :: [Int32] nums = [-2, -1, 0, 1, 2] stream :: Stream Int32 stream = extern "stream" (Just nums) spec :: Spec spec = trigger "func" true [arg (signum stream)] main :: IO () main = do spec' <- reify spec #ifdef INTERPRET csv (genericLength nums) spec #else compile "signum" spec' #endif ``` with -DINTERPRET, the program will print: ``` $ cabal v1-exec -- runhaskell -DINTERPRET Signum.hs Note: CSV format does not output observers. # func,-1 # func,-1 # func,0 # func,1 # func,1 ``` The generated C99 can be executed with the following main: ``` #include <stdint.h> #include <stdio.h> #include "signum.h" int32_t nums[5] = { -2, -1, 0, 1, 2 }; int32_t stream; void func (int32_t sign) { printf ("%d\n", sign); } int main () { int i = 0; for (i=0; i<5; i++) { stream = nums[i]; step(); } return 0; } ``` And it will print: ``` -1 -1 1 1 1 ``` so long as the bug is present. The new implementation corrects that behavior to print, instead, the same values produced by the interpreter. Co-authored-by: Ivan Perez <ivan.perezdominguez@nasa.gov>
1 parent bd750ae commit 957407e

File tree

1 file changed

+53
-1
lines changed

1 file changed

+53
-1
lines changed

copilot-c99/src/Copilot/Compile/C99/Translate.hs

Lines changed: 53 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ transop1 :: Op1 a b -> C.Expr -> C.Expr
5555
transop1 op e = case op of
5656
Not -> (C..!) e
5757
Abs _ -> funcall "abs" [e]
58-
Sign _ -> funcall "copysign" [C.LitDouble 1.0, e]
58+
Sign ty -> transSign ty e
5959
Recip _ -> C.LitDouble 1.0 C../ e
6060
Exp _ -> funcall "exp" [e]
6161
Sqrt _ -> funcall "sqrt" [e]
@@ -112,6 +112,58 @@ transop3 :: Op3 a b c d -> C.Expr -> C.Expr -> C.Expr -> C.Expr
112112
transop3 op e1 e2 e3 = case op of
113113
Mux _ -> C.Cond e1 e2 e3
114114

115+
-- | Translate @'Sign' e@ in Copilot Core into a C99 expression.
116+
--
117+
-- Sign is is translated as @e > 0 ? 1 : (e < 0 ? -1 : e)@, that is:
118+
--
119+
-- 1. If @e@ is positive, return @1@.
120+
--
121+
-- 2. If @e@ is negative, return @-1@.
122+
--
123+
-- 3. Otherwise, return @e@. This handles the case where @e@ is @0@ when the
124+
-- type is an integral type. If the type is a floating-point type, it also
125+
-- handles the cases where @e@ is @-0@ or @NaN@.
126+
--
127+
-- This implementation is modeled after how GHC implements 'signum'
128+
-- <https://gitlab.haskell.org/ghc/ghc/-/blob/aed98ddaf72cc38fb570d8415cac5de9d8888818/libraries/base/GHC/Float.hs#L523-L525 here>.
129+
transSign :: Type a -> C.Expr -> C.Expr
130+
transSign ty e = positiveCase $ negativeCase e
131+
where
132+
-- If @e@ is positive, return @1@, otherwise fall back to argument.
133+
--
134+
-- Produces the following code, where @<arg>@ is the argument to this
135+
-- function:
136+
-- @
137+
-- e > 0 ? 1 : <arg>
138+
-- @
139+
positiveCase :: C.Expr -- ^ Value returned if @e@ is not positive.
140+
-> C.Expr
141+
positiveCase =
142+
C.Cond (C.BinaryOp C.GT e (constNumTy ty 0)) (constNumTy ty 1)
143+
144+
-- If @e@ is negative, return @1@, otherwise fall back to argument.
145+
--
146+
-- Produces the following code, where @<arg>@ is the argument to this
147+
-- function:
148+
-- @
149+
-- e < 0 ? -1 : <arg>
150+
-- @
151+
negativeCase :: C.Expr -- ^ Value returned if @e@ is not negative.
152+
-> C.Expr
153+
negativeCase =
154+
C.Cond (C.BinaryOp C.LT e (constNumTy ty 0)) (constNumTy ty (-1))
155+
156+
-- Translate a literal number of type @ty@ into a C99 literal.
157+
--
158+
-- PRE: The type of PRE is numeric (integer or floating-point), that
159+
-- is, not boolean, struct or array.
160+
constNumTy :: Type a -> Integer -> C.Expr
161+
constNumTy ty =
162+
case ty of
163+
Float -> C.LitFloat . fromInteger
164+
Double -> C.LitDouble . fromInteger
165+
_ -> C.LitInt
166+
115167
-- | Transform a Copilot Core literal, based on its value and type, into a C99
116168
-- literal.
117169
constty :: Type a -> a -> C.Expr

0 commit comments

Comments
 (0)