add clang's __builtin_ia32_undefX and __builtin_nontemporal_store and __builtin_nontemporal_load

Author: Daniel 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$
+--

regression/goto-clang/Makefile

@@ -0,0 +1,20 @@
+default: tests.log
+
+test:
+	@../test.pl -p -c ../../../src/goto-cc/goto-cc
+
+tests.log: ../test.pl
+	@../test.pl -p -c ../../../src/goto-cc/goto-cc
+
+show:
+	@for dir in *; do \
+	  if [ -d "$$dir" ]; then \
+	    vim -o "$$dir/*.c" "$$dir/*.out"; \
+	  fi; \
+	done;
+
+clean:
+	find -name '*.o' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	find -name '*.goto-cc-saved' -execdir $(RM) '{}' \;
+	$(RM) tests.log

src/ansi-c/c_typecheck_expr.cpp

@@ -2198,6 +2198,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);