add clang's __builtin_ia32_undefX and __builtin_nontemporal_store and __builtin_nontemporal_load

Author: kroening

regression/ansi-c/builtin_ia32_undef/main.c

@@ -0,0 +1,11 @@
+int main()
+{
+  #ifdef __clang__
+  long long A __attribute__ ((__vector_size__ (16))) =
+    __builtin_ia32_undef128();
+  long long B __attribute__ ((__vector_size__ (32))) =
+    __builtin_ia32_undef256();
+  long long C __attribute__ ((__vector_size__ (64))) =
+    __builtin_ia32_undef512();
+  #endif
+}

regression/ansi-c/builtin_ia32_undef/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ansi-c/builtin_nontemporal_load_store/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  #ifdef __clang__
+  int var, value;
+  __builtin_nontemporal_store(1, &var);
+  value = __builtin_nontemporal_load(&var);
+  #endif
+}

regression/ansi-c/builtin_nontemporal_load_store/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--

src/ansi-c/c_typecheck_expr.cpp

@@ -2197,6 +2197,31 @@ exprt c_typecheck_baset::do_special_functions(
 
     return bswap_expr;
   }
+  else if(identifier=="__builtin_nontemporal_load")
+  {
+    typecheck_function_call_arguments(expr);
+
+    if(expr.arguments().size()!=1)
+    {
+      err_location(f_op);
+      error() << identifier << " expects one operand" << eom;
+      throw 0;
+    }
+
+    // these return the subtype of the argument
+    exprt &ptr_arg=expr.arguments().front();
+
+    if(ptr_arg.type().id()!=ID_pointer)
+    {
+      err_location(f_op);
+      error() << "__builtin_nontemporal_load takes pointer as argument" << eom;
+      throw 0;
+    }
+
+    expr.type()=expr.arguments().front().type().subtype();
+
+    return expr;
+  }
   else if(
     identifier == "__builtin_fpclassify" ||
     identifier == CPROVER_PREFIX "fpclassify")

src/ansi-c/clang_builtin_headers.h

@@ -1,3 +1,10 @@
 __gcc_v4sf __builtin_shufflevector(__gcc_v4sf, __gcc_v4sf, ...);
 
+__gcc_v2di __builtin_ia32_undef128(void);
+__gcc_v4di __builtin_ia32_undef256(void);
+__gcc_v8di __builtin_ia32_undef512(void);
+
+void __builtin_nontemporal_store();
+void __builtin_nontemporal_load();
+
 int __builtin_flt_rounds(void);