File tree Expand file tree Collapse file tree 6 files changed +68
-0
lines changed
builtin_nontemporal_load_store Expand file tree Collapse file tree 6 files changed +68
-0
lines changed Original file line number Diff line number Diff line change 1+ int main ()
2+ {
3+ #ifdef __clang__
4+ long long A __attribute__ ((__vector_size__ (16 ))) =
5+ __builtin_ia32_undef128 ();
6+ long long B __attribute__ ((__vector_size__ (32 ))) =
7+ __builtin_ia32_undef256 ();
8+ long long C __attribute__ ((__vector_size__ (64 ))) =
9+ __builtin_ia32_undef512 ();
10+ #endif
11+ }
Original file line number Diff line number Diff line change 1+ CORE
2+ main.c
3+
4+ ^EXIT=0$
5+ ^SIGNAL=0$
6+ --
Original file line number Diff line number Diff line change 1+ int main ()
2+ {
3+ #ifdef __clang__
4+ int var , value ;
5+ __builtin_nontemporal_store (1 , & var );
6+ value = __builtin_nontemporal_load (& var );
7+ #endif
8+ }
Original file line number Diff line number Diff line change 1+ CORE
2+ main.c
3+
4+ ^EXIT=0$
5+ ^SIGNAL=0$
6+ --
Original file line number Diff line number Diff line change @@ -252,7 +252,12 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
252252 }
253253 else if (expr.id ()==ID_clang_builtin_convertvector)
254254 {
255+ // This has one operand and a type, and acts like a typecast
256+ DATA_INVARIANT (expr.operands ().size ()==1 , " clang_builtin_convertvector has one operand" );
255257 typecheck_type (expr.type ());
258+ typecast_exprt tmp (expr.op0 (), expr.type ());
259+ tmp.add_source_location ()=expr.source_location ();
260+ expr.swap (tmp);
256261 }
257262 else if (expr.id ()==ID_builtin_offsetof)
258263 typecheck_expr_builtin_offsetof (expr);
@@ -2192,6 +2197,31 @@ exprt c_typecheck_baset::do_special_functions(
21922197
21932198 return bswap_expr;
21942199 }
2200+ else if (identifier==" __builtin_nontemporal_load" )
2201+ {
2202+ typecheck_function_call_arguments (expr);
2203+
2204+ if (expr.arguments ().size ()!=1 )
2205+ {
2206+ err_location (f_op);
2207+ error () << identifier << " expects one operand" << eom;
2208+ throw 0 ;
2209+ }
2210+
2211+ // these return the subtype of the argument
2212+ exprt &ptr_arg=expr.arguments ().front ();
2213+
2214+ if (ptr_arg.type ().id ()!=ID_pointer)
2215+ {
2216+ err_location (f_op);
2217+ error () << " __builtin_nontemporal_load takes pointer as argument" << eom;
2218+ throw 0 ;
2219+ }
2220+
2221+ expr.type ()=expr.arguments ().front ().type ().subtype ();
2222+
2223+ return expr;
2224+ }
21952225 else if (
21962226 identifier == " __builtin_fpclassify" ||
21972227 identifier == CPROVER_PREFIX " fpclassify" )
Original file line number Diff line number Diff line change 11__gcc_v4sf __builtin_shufflevector (__gcc_v4sf , __gcc_v4sf , ...);
22
3+ __gcc_v2di __builtin_ia32_undef128 (void );
4+ __gcc_v4di __builtin_ia32_undef256 (void );
5+ __gcc_v8di __builtin_ia32_undef512 (void );
6+
7+ void __builtin_nontemporal_store ();
8+ void __builtin_nontemporal_load ();
9+
310int __builtin_flt_rounds (void );
You can’t perform that action at this time.
0 commit comments