File tree 6 files changed +68
-0
lines changed
builtin_nontemporal_load_store
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)
252
252
}
253
253
else if (expr.id ()==ID_clang_builtin_convertvector)
254
254
{
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" );
255
257
typecheck_type (expr.type ());
258
+ typecast_exprt tmp (expr.op0 (), expr.type ());
259
+ tmp.add_source_location ()=expr.source_location ();
260
+ expr.swap (tmp);
256
261
}
257
262
else if (expr.id ()==ID_builtin_offsetof)
258
263
typecheck_expr_builtin_offsetof (expr);
@@ -2192,6 +2197,31 @@ exprt c_typecheck_baset::do_special_functions(
2192
2197
2193
2198
return bswap_expr;
2194
2199
}
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
+ }
2195
2225
else if (
2196
2226
identifier == " __builtin_fpclassify" ||
2197
2227
identifier == CPROVER_PREFIX " fpclassify" )
Original file line number Diff line number Diff line change 1
1
__gcc_v4sf __builtin_shufflevector (__gcc_v4sf , __gcc_v4sf , ...);
2
2
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
+
3
10
int __builtin_flt_rounds (void );
You can’t perform that action at this time.
0 commit comments