C translation doesn't correctly select operations based on types

See:

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

Lines 56 to 106 in 11ab89f

    
           transop1 :: Op1 a b -> C.Expr -> C.Expr 
        
           transop1 op e = case op of 
        
             Not             -> (C..!) e 
        
             Abs      _      -> funcall "abs"      [e] 
        
             Sign     _      -> funcall "copysign" [C.LitDouble 1.0, e] 
        
             Recip    _      -> C.LitDouble 1.0 C../ e 
        
             Exp      _      -> funcall "exp"   [e] 
        
             Sqrt     _      -> funcall "sqrt"  [e] 
        
             Log      _      -> funcall "log"   [e] 
        
             Sin      _      -> funcall "sin"   [e] 
        
             Tan      _      -> funcall "tan"   [e] 
        
             Cos      _      -> funcall "cos"   [e] 
        
             Asin     _      -> funcall "asin"  [e] 
        
             Atan     _      -> funcall "atan"  [e] 
        
             Acos     _      -> funcall "acos"  [e] 
        
             Sinh     _      -> funcall "sinh"  [e] 
        
             Tanh     _      -> funcall "tanh"  [e] 
        
             Cosh     _      -> funcall "cosh"  [e] 
        
             Asinh    _      -> funcall "asinh" [e] 
        
             Atanh    _      -> funcall "atanh" [e] 
        
             Acosh    _      -> funcall "acosh" [e] 
        
             BwNot    _      -> (C..~) e 
        
             Cast     _ ty  -> C.Cast (transtypename ty) e 
        
             GetField (Struct _)  _ f -> C.Dot e (accessorname f) 
        
           -- | Translates a Copilot binary operator and its arguments into a C99 
        
           -- expression. 
        
           transop2 :: Op2 a b c -> C.Expr -> C.Expr -> C.Expr 
        
           transop2 op e1 e2 = case op of 
        
             And          -> e1 C..&& e2 
        
             Or           -> e1 C..|| e2 
        
             Add      _   -> e1 C..+  e2 
        
             Sub      _   -> e1 C..-  e2 
        
             Mul      _   -> e1 C..*  e2 
        
             Mod      _   -> e1 C..%  e2 
        
             Div      _   -> e1 C../  e2 
        
             Fdiv     _   -> e1 C../  e2 
        
             Pow      _   -> funcall "pow" [e1, e2] 
        
             Logb     _   -> funcall "log" [e2] C../ funcall "log" [e1] 
        
             Eq       _   -> e1 C..== e2 
        
             Ne       _   -> e1 C..!= e2 
        
             Le       _   -> e1 C..<= e2 
        
             Ge       _   -> e1 C..>= e2 
        
             Lt       _   -> e1 C..<  e2 
        
             Gt       _   -> e1 C..>  e2 
        
             BwAnd    _   -> e1 C..&  e2 
        
             BwOr     _   -> e1 C..|  e2 
        
             BwXor    _   -> e1 C..^  e2 
        
             BwShiftL _ _ -> e1 C..<< e2 
        
             BwShiftR _ _ -> e1 C..>> e2 
        
             Index    _   -> C.Index e1 e2

Code generation selects a function to call based only on the operation, without paying attention the type. This is almost certainly not what is desired. For example abs is a function on int, but is applied also to float and double values. This causes the C compiler to (silently (!)) perform numerical coercions to/from int. Instead the generator should select fabs or fabsf. Likewise choosing between copysign or copysignf, cos or cosf, etc.

The abs case for integer values is actually even tricker, as copilot uses the fixed-width intX_t types, but, as far as I know, the standard library does not provide operations for fixed-width types, but instead only provides abs, labs, and llabs for int, long and long long respectively. The Sign operation is also troublesome, as it applies also to integer operations on the copilot side, but has no corresponding C primitive that I know of. These may have to be provided as macros to get correct behavior.

clang can be convinced to halt compilation on these kinds of problems by passing the -Wconversion -Werror flags.

I've also just learned about tgmath.h, which provides type-generic macros for math.h functions. It seems it first appeared in C99. This might make it slightly easier, at least for the floating-point functions.

https://en.cppreference.com/w/c/numeric/tgmath

Yes, we have recently talked about this (Alwyn, Frank and I).

This is what I meant today when I said that the meaning of some math operations will change.

copilot-c99: Use more specific operations for floats. Refs Copilot-La…

@joeyh

I've been looking into this issue. My solution spelled out the types a bit more in the case selections for OP{1,2}, in an attempt at preventing future developers from defaulting to a "f" suffix by mistake for functions that may not support it (i.e., it directed the developer to "spell it out").

I've tried to merge your solution and mine, into a simpler, shared version available here: https://github.com/Copilot-Language/copilot/tree/develop-specialize-math-types. I removed some checks on errors on input types, mainly because the GADT would disallow them by construction.

Still, it seems like there's "too much logic" and too much ad-hocness. (The whole C99-backend can be vastly simplified.)

I also went down the path of tgmath.h, and I agree with Rob: if it's well supported, it's likely the simplest and best solution. I know arduino is not our main target, but I'd definitely want to hear @joeyh's thoughts on this.

I just tried compiling an arduino example with gcc-avr it does not find a <tgmath.h>. It does not seem to be part of the standard avr-libc anymore.

Note that the variants specialized for floats in math.h in avr are just aliases for the double-based versions of the same functions, so there's just no difference. In that platform, it makes no sense to specialize for different types (except for abs/fabs).

I've sent a message to the avr-libc users mailing list to see if there's a reason for that file not being included.

@joeyh

@joeyh for arduino, I found that the following compiles:

Adaptation to Makefile, to include user library:

USER_LIB_PATH := $(realpath libraries)
BOARD_TAG = uno
include /usr/share/arduino/Arduino.mk

New libraries/tgmath/tgmath.h file, which simply imports math.h:

#include <math.h>

Would this be an acceptable adaptation to arduino-copilot?

The following question is for everyone:
If the above works with arduino-copilot, are there any reasons not to use tgmath.h? This solution is much cleaner, I think it requires very few changes (see last 3 commits in https://github.com/Copilot-Language/copilot/tree/develop-specialize-math-types-tgmath, or compare branches).

Btw, tgmath.h does not provide a macro for abs, so we'd still need to distinguish between (integer) abs and fabs.

Ok, after some deliberation with the Copilot team, discussions on the avr mailing list, etc. I'm making an executive decision to merge the change as implemented in the branch above (that is, without tgmath.h). The reason is that tgmath.h relies on specific compiler extensions, its implementation is compiler- (and architecture-) dependent, all of which makes it harder for people to reason about specifically which version of the function will be executed (they know in principle, but tgmath.h hides details away to a point where V&V might get harder).

It's very borderline though, and I could be convinced of the opposite, especially if we can make a good argument in favor of verification. And, more generally, I would be interested in seeing if it's possible to optimize that boilerplate code away in some other clean way.

Just to clarify, when you say "the branch above", you're referring to https://github.com/Copilot-Language/copilot/tree/develop-specialize-math-types?

@robdockins

I am.

Clarification: @robdockins is right that abs, labs, etc. may have to be used for larger integers, but they operate on int, not fixed-sized ints. I'm looking into that.

I think a reasonable implementation would be to use abs for 16-bit-sized ints/word and below, casting fro and back, and labs for 32-bit sized ints and above, but I'll check that the results are correct.

We could avoid casts by expanding Abs to something like:

(x + (x >> (8*sizeof(int64_t) - 1))) ^ (x >> (8*sizeof(int64_t) - 1));

replacing int64_t with whatever type Abs should be applied to.

Probably too late to matter, but: I could make arduino-copilot deal with tgmath being used, I'm sure. Modifying the Makefile would not be my preferred option, for one it's intrusive and also arduino-copilot users may not only use the Makefile but may opt to load the generated C code into the Arduino IDE and flash it that way.

Also I checked Zephyr and it seems to include tgmath.h, although I have not verified it works there.

Document changes in CHANGELOG. Refs #263.

Great! Fixed, pushed and waiting for tests / CI.

I mean, it makes sense when you look at the definition (which includes parentheses only around the argument):

#  define isnan(x) __builtin_isnan (x)

I don't think this is specific to llvm.

Implementor: solution implemented, review requested.

Change Manager: Verified that:

Solution is implemented:

The code proposed compiles. Details:
Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/250130870

The code proposed passes the tests. Details:
Docker image:

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

CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. && cabal v1-install copilot/copilot**/ --enable-tests --run-tests

Command:

$ docker run -e "REPO=https://github.com/copilot-language/copilot" -e "NAME=copilot" -e "COMMIT=170f5282fe7d3a5204b187354503cf27cb7e6866" -it copilot-test

The solution proposed produces the expected result: the function picked is the specialized version depending on the type. The following files run an experiment that compares the version chosen by Copilot with the one picked by tgmath.h based on the type:

--- Dockerfile-verify-263
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 Spec.hs /Spec.hs
ADD main-263.c /main-263.c

# We negate the exit code of the last command, which should fail if the module
# is exposed by the library, but succeed otherwise.
SHELL ["/bin/bash", "-c"]
CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
    && cabal v1-install copilot/copilot**/ \
    && cabal v1-exec -- runhaskell Spec.hs \
    && gcc main-263.c spec.c -lm -o main-263 \
    && ./main-263 \
    && echo "Success"
    
--- Test.hs
import Copilot.Compile.C99
import Copilot.Language
import Copilot.Language.Prelude
import Language.Copilot
import Prelude ()

ext :: Stream Float
ext = extern "input_stream" Nothing

streamAbs :: Stream Float
streamAbs = abs ext

streamSin :: Stream Float
streamSin = sin ext

-- Ensure that argument to acosh is higher than 1 so that it is within
-- range.
streamAcosh :: Stream Float
streamAcosh = acosh (1 + ext)

streamExp :: Stream Float
streamExp = exp ext

streamLog :: Stream Float
streamLog = log ext

streamSqrt :: Stream Float
streamSqrt = sqrt ext

spec = do
  trigger "handlerAbs"   true [ arg streamAbs ]
  trigger "handlerSin"   true [ arg streamSin ]
  trigger "handlerAcosh" true [ arg streamAcosh ]
  trigger "handlerExp"   true [ arg streamExp ]
  trigger "handlerLog"   true [ arg streamLog ]
  trigger "handlerSqrt"  true [ arg streamSqrt ]

main = do
  r <- reify spec
  compile "spec" r

--- main-263.c
#include <tgmath.h>
#include <stdio.h>
#include <stdlib.h>

#include "spec.h"

float input_stream = 0;

int err_code = 0;

void assert_eq (char* name, float v1, float v2) {
   if (v1 != v2) {
      float diff = v1 - v2;
      printf("Error (%s):\t%.8f\t%.8f\t%.8f\t%.8f\n",
             name,
             input_stream,
             v1,
             v2,
             diff);
      err_code = 1;
   }
}

void handlerSin (float arg) {
   float f = sin(input_stream);
   assert_eq ("sin", f, arg);
}

void handlerAbs (float arg) {
   float f = fabs(input_stream);
   assert_eq ("abs", f, arg);
}

void handlerAcosh (float arg) {
   float f = acosh(1 + input_stream);
   assert_eq ("acosh", f, arg);
}

void handlerSqrt (float arg) {
   float f = sqrt(input_stream);
   assert_eq ("sqrt", f, arg);
}

void handlerExp (float arg) {
   float f = exp(input_stream);
   assert_eq ("exp", f, arg);
}

void handlerLog (float arg) {
   float f = log(input_stream);
   assert_eq ("log", f, arg);
}

int main()
{
    int i;
    for (i = 0; i < 2000; i++) {
        input_stream = (float)rand() / RAND_MAX;
        step();
    }
    return err_code;
}

Command:

$ docker run -e "REPO=https://github.com/copilot-language/copilot" -e "NAME=copilot" -e "COMMIT=170f5282fe7d3a5204b187354503cf27cb7e6866" -it copilot-verify-263

Implementation is documented. Details:
No need for additional documentation (change to implementation without affecting interface).
Change history is clear.
Commit messages are clear.

Change Manager: Implementation ready to be merged.

Hah. Funny enough, we've ran into the same issue on our side. Usually, if you invoke the isnan(x) function, it refers to a macro, but if you surround it with parentheses (e.g., (isnan)(x)), then Clang resolves isnan to a specific function over double! LLVM can be strange like that.

Just wanted to chime in here that this is a general C-ism, not just for LLVM; surrounding a function name in parens explicitly disables macro expansion, so having the C99 pretty-printer do that isn't totally benign. Some C standard library functions are intended to be used as macros, and disabling macro-expansion may not work as expected.

@robdockins

Thanks, @robdockins . Good point!

That's an interesting challenge from the point of view of creating a C99 AST and pretty printer. Normal algorithms to minimize the number of parenthesis might not work well, and, potentially, the AST should provide a way to say "between parentheses" even though ASTs would normally not do that because that's more concrete syntax.

I'll discuss it with Frank, who maintains the c99 library we are using atm.

If I were designing a solution to this issue, I'd probably have two function call forms in the AST: one for "named" function calls (which take an identifier and a list of arguments, and the identifier is never parenthised, and might be a macro) and one for "expression" function calls (which takes an expression and a list of arguments, and the expression is always parenthised, and is never a macro).

It's probably best to discuss that in the https://github.com/fdedden/language-c99 package, since it's likely the one that will have to address it.

Navigation Menu

Repository navigation

C translation doesn't correctly select operations based on types #263

59 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

	transop1 :: Op1 a b -> C.Expr -> C.Expr
	transop1 op e = case op of
	Not -> (C..!) e
	Abs _ -> funcall "abs" [e]
	Sign _ -> funcall "copysign" [C.LitDouble 1.0, e]
	Recip _ -> C.LitDouble 1.0 C../ e
	Exp _ -> funcall "exp" [e]
	Sqrt _ -> funcall "sqrt" [e]
	Log _ -> funcall "log" [e]
	Sin _ -> funcall "sin" [e]
	Tan _ -> funcall "tan" [e]
	Cos _ -> funcall "cos" [e]
	Asin _ -> funcall "asin" [e]
	Atan _ -> funcall "atan" [e]
	Acos _ -> funcall "acos" [e]
	Sinh _ -> funcall "sinh" [e]
	Tanh _ -> funcall "tanh" [e]
	Cosh _ -> funcall "cosh" [e]
	Asinh _ -> funcall "asinh" [e]
	Atanh _ -> funcall "atanh" [e]
	Acosh _ -> funcall "acosh" [e]
	BwNot _ -> (C..~) e
	Cast _ ty -> C.Cast (transtypename ty) e
	GetField (Struct _) _ f -> C.Dot e (accessorname f)

	-- \| Translates a Copilot binary operator and its arguments into a C99
	-- expression.
	transop2 :: Op2 a b c -> C.Expr -> C.Expr -> C.Expr
	transop2 op e1 e2 = case op of
	And -> e1 C..&& e2
	Or -> e1 C..\|\| e2
	Add _ -> e1 C..+ e2
	Sub _ -> e1 C..- e2
	Mul _ -> e1 C..* e2
	Mod _ -> e1 C..% e2
	Div _ -> e1 C../ e2
	Fdiv _ -> e1 C../ e2
	Pow _ -> funcall "pow" [e1, e2]
	Logb _ -> funcall "log" [e2] C../ funcall "log" [e1]
	Eq _ -> e1 C..== e2
	Ne _ -> e1 C..!= e2
	Le _ -> e1 C..<= e2
	Ge _ -> e1 C..>= e2
	Lt _ -> e1 C..< e2
	Gt _ -> e1 C..> e2
	BwAnd _ -> e1 C..& e2
	BwOr _ -> e1 C..\| e2
	BwXor _ -> e1 C..^ e2
	BwShiftL _ _ -> e1 C..<< e2
	BwShiftR _ _ -> e1 C..>> e2
	Index _ -> C.Index e1 e2

C translation doesn't correctly select operations based on types #263

Description

Activity

robdockins commented on Oct 15, 2021

robdockins commented on Oct 16, 2021

ivanperez-keera commented on Oct 16, 2021

ivanperez-keera commented on Apr 21, 2022

ivanperez-keera commented on Apr 22, 2022

ivanperez-keera commented on Apr 22, 2022

ivanperez-keera commented on Apr 22, 2022

ivanperez-keera commented on Apr 22, 2022

RyanGlScott commented on Apr 22, 2022

ivanperez-keera commented on Apr 22, 2022

joeyh commented on Apr 22, 2022

59 remaining items

ivanperez-keera commented on May 2, 2022

ivanperez-keera commented on May 2, 2022

ivanperez-keera commented on May 2, 2022

ivanperez-keera commented on May 2, 2022

ivanperez-keera commented on May 2, 2022

robdockins commented on May 9, 2022

ivanperez-keera commented on May 9, 2022

robdockins commented on May 9, 2022

ivanperez-keera commented on May 9, 2022

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions