C translation doesn't correctly select operations based on types

[robdockins]

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.

[robdockins]

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

[robdockins]

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

[ivanperez-keera]

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.

[ivanperez-keera]

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.

[ivanperez-keera]

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.

[ivanperez-keera]

@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).

[ivanperez-keera]

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

[ivanperez-keera]

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.