Unwanted partial constant propagation in 64-bit integer arguments to builtins

Here are two examples that cause an internal error in Asmexpand.ml:

volatile long long x; void f(unsigned int i) { x = i; }

unsigned g(unsigned i) { return __builtin_clzll(i); }

The argument "i" to builtin volatile store or __builtin_clzll is turned into a BA_splitlong(BA_int 0, BA <variable i>), which Asmexpand.ml doesn't know how to handle.

The fix (in AST.builtin_arg_ok) is to prevent this 'optimization' for all builtins except those of the "OK_all" kind, i.e. __builtin_annot.

Regression tests were added and tested on IA32.  Need to retest on ARM and PowerPC.

8 files changed, 18 insertions, 1 deletions

diff --git a/common/AST.v b/common/AST.v
index 0b524eb8..ae7178f4 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -684,7 +684,7 @@ Inductive builtin_arg_constraint : Type :=
 Definition builtin_arg_ok
        (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) :=
   match ba, c with
-  | (BA _ | BA_splitlong _ _), _ => true
+  | (BA _ | BA_splitlong (BA _) (BA _)), _ => true
   | (BA_int _ | BA_long _ | BA_float _ | BA_single _), OK_const => true
   | BA_addrstack _, (OK_addrstack | OK_addrany) => true
   | BA_addrglobal _ _, (OK_addrglobal | OK_addrany) => true
diff --git a/test/regression/Results/builtins-arm b/test/regression/Results/builtins-arm
index 40cb6048..f637fb16 100644
--- a/test/regression/Results/builtins-arm
+++ b/test/regression/Results/builtins-arm
@@ -3,6 +3,7 @@ bswap16(1234) = 3412
 clz(12345678) = 3
 clzll(12345678) = 35
 clzll(1234567812345678) = 3
+clzll(78563412) = 33
 fsqrt(3.141590) = 1.772453
 read_16_rev = 3412
 read_32_rev = efbeadde
diff --git a/test/regression/Results/builtins-ia32 b/test/regression/Results/builtins-ia32
index a7669f14..6ab71f0d 100644
--- a/test/regression/Results/builtins-ia32
+++ b/test/regression/Results/builtins-ia32
@@ -3,9 +3,11 @@ bswap16(1234) = 3412
 clz(12345678) = 3
 clzll(12345678) = 35
 clzll(1234567812345678) = 3
+clzll(78563412) = 33
 ctz(1234) = 2
 ctzll(1234567812345678) = 3
 ctzll(1234567800000000) = 35
+ctzll(78563412) = 1
 fsqrt(3.141590) = 1.772453
 fmin(3.141590, 2.718000) = 2.718000
 fmax(3.141590, 2.718000) = 3.141590
diff --git a/test/regression/Results/builtins-powerpc b/test/regression/Results/builtins-powerpc
index bb4edf3a..a3c63ad6 100644
--- a/test/regression/Results/builtins-powerpc
+++ b/test/regression/Results/builtins-powerpc
@@ -3,6 +3,7 @@ mulhwu(12345678, deadbeef) = fd5bdee
 clz(12345678) = 3
 clzll(12345678) = 35
 clzll(1234567812345678) = 3
+clzll(78563412) = 33
 bswap(12345678) = 78563412
 bswap16(1234) = 3412
 fmadd(3.141590, 2.718000, 1.414000) = 9.952842
diff --git a/test/regression/builtins-arm.c b/test/regression/builtins-arm.c
index 5fa867c2..709343ce 100644
--- a/test/regression/builtins-arm.c
+++ b/test/regression/builtins-arm.c
@@ -7,6 +7,7 @@ int main(int argc, char ** argv)
   unsigned int x = 0x12345678;
   unsigned int y = 0xDEADBEEF;
   unsigned long long xx = 0x1234567812345678ULL;
+  unsigned z;
   double a = 3.14159;
   unsigned short s = 0x1234;
 
@@ -15,6 +16,8 @@ int main(int argc, char ** argv)
   printf("clz(%x) = %d\n", x, __builtin_clz(x));
   printf("clzll(%llx) = %d\n", (unsigned long long) x, __builtin_clzll(x));
   printf("clzll(%llx) = %d\n", xx, __builtin_clzll(xx));
+  z = __builtin_bswap(x);
+  printf("clzll(%lx) = %d\n", z, __builtin_clzll(z));
   printf("fsqrt(%f) = %f\n", a, __builtin_fsqrt(a));
   
   printf ("read_16_rev = %x\n", __builtin_read16_reversed(&s));
diff --git a/test/regression/builtins-ia32.c b/test/regression/builtins-ia32.c
index 8df81800..9b7ed126 100644
--- a/test/regression/builtins-ia32.c
+++ b/test/regression/builtins-ia32.c
@@ -8,6 +8,7 @@ int main(int argc, char ** argv)
   unsigned int y = 0xDEADBEEF;
   unsigned long long xx = 0x1234567812345678ULL;
   unsigned long long yy = 0x1234567800000000ULL;
+  unsigned z;
   double a = 3.14159;
   double b = 2.718;
   double c = 1.414;
@@ -18,9 +19,12 @@ int main(int argc, char ** argv)
   printf("clz(%x) = %d\n", x, __builtin_clz(x));
   printf("clzll(%llx) = %d\n", (unsigned long long) x, __builtin_clzll(x));
   printf("clzll(%llx) = %d\n", xx, __builtin_clzll(xx));
+  z = __builtin_bswap(x);
+  printf("clzll(%lx) = %d\n", z, __builtin_clzll(z));
   printf("ctz(%x) = %d\n", s, __builtin_ctz(s));
   printf("ctzll(%llx) = %d\n", xx, __builtin_ctzll(xx));
   printf("ctzll(%llx) = %d\n", yy, __builtin_ctzll(yy));
+  printf("ctzll(%lx) = %d\n", z, __builtin_ctzll(z));
 
   printf("fsqrt(%f) = %f\n", a, __builtin_fsqrt(a));
   printf("fmin(%f, %f) = %f\n", a, b, __builtin_fmin(a, b));
diff --git a/test/regression/builtins-powerpc.c b/test/regression/builtins-powerpc.c
index 1d220c11..23e9d191 100644
--- a/test/regression/builtins-powerpc.c
+++ b/test/regression/builtins-powerpc.c
@@ -14,6 +14,7 @@ int main(int argc, char ** argv)
   unsigned int x = 0x12345678;
   unsigned int y = 0xDEADBEEF;
   unsigned long long xx = 0x1234567812345678ULL;
+  unsigned z;
   double a = 3.14159;
   double b = 2.718;
   double c = 1.414;
@@ -24,6 +25,8 @@ int main(int argc, char ** argv)
   printf("clz(%x) = %d\n", x, __builtin_clz(x));
   printf("clzll(%llx) = %d\n", (unsigned long long) x, __builtin_clzll(x));
   printf("clzll(%llx) = %d\n", xx, __builtin_clzll(xx));
+  z = __builtin_bswap(x);
+  printf("clzll(%lx) = %d\n", z, __builtin_clzll(z));
   printf("bswap(%x) = %x\n", x, __builtin_bswap(x));
   printf("bswap16(%x) = %x\n", s, __builtin_bswap16(s));
 
diff --git a/test/regression/volatile2.c b/test/regression/volatile2.c
index 3bad6ae2..bd2a93a3 100644
--- a/test/regression/volatile2.c
+++ b/test/regression/volatile2.c
@@ -13,6 +13,7 @@ unsigned char guc;
 signed short gss;
 unsigned short gus;
 int gi;
+unsigned gu;
 float gf;
 double gd;
 long long gll;
@@ -44,6 +45,8 @@ int main()
   TEST("global float", float, gf, 0.5, 256.0);
   TEST("global double", double, gd, 3.1415, 2.718);
   TEST("global long long", long long, gll, 0x123456789ABCDEFLL, 0x789ABCDEF1234567LL);
+  /* Test for unwanted partial constant propagation */
+  *((volatile long long *) &gll) = gu;
   return 0;
 }