From 4c7650c3eaf4dfbe5971864bf084e76f844051ee Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 8 Jul 2016 15:44:46 +0200 Subject: 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 ), 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. --- common/AST.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'common/AST.v') 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 -- cgit