Skip to content

Commit e599b85

Browse files
qinhepingqinheping
committed
Add enumerative loop invariant synthesizer
Implement the functionality described below. Motivation --- This loop invariant synthesizer use the idea counter-example-guided synthesis (CEGIS) to synthesize loop invariants for programs with only checks instrumented by `goto-instrument` with flag `--pointer-check`. This PR contain the driver of the synthesizer and the verifier we use to check invariant candidates. Verifier --- The verifier take as input a goto program with pointer checks and a map from loop id to loop invariant candidates. It first annotate and apply the loop invariant candidates into the goto model; and then simulate the CBMC api to verify the instrumented goto program. If there are some violations---loop invariants are not inductive, or some pointer checks fail---, it record valuation from trace generated by the back end to construct a formatted counterexample `cext`. Counterexample --- A counterexample `cext` record valuations of variables in the trace, and other information about the violation. The valuation we record including 1. set of live variables upon the entry of the loop. 2. the havoced value of all primitive-typed variables; 3. the havoced offset and the object size of all pointer-typed variables; 4. history values of 2 and 3. The valuations will be used as true positive (history values) and true negative (havcoed valuation) to filter out bad invariant clause with the idea of the Daikon invariant detector in a following PR. However, in this PR we only construct the valuation but not actually use them. Synthesizer --- Loop invariants we synthesize are of the form `` (in_clause || !guard) && (!guard -> pos_clause)`` where `in_clause` and `out_clause` are predicates we store in two different map, and `guard` is the loop guard. The idea is that we separately synthesize the condition `in_clause` that should hold before the execution of the loop body, and condition `pos_clause` that should hold as post-condition of the loop. When the violation happen in the loop, we update `in_clause`. When the violation happen after the loop, we update `pos_clause`. When the invariant candidate it not inductive, we enumerate strengthening clause to make it inductive. To be more efficient, we choose different synthesis strategy for different type of violation * For out-of-boundary violation, we choose to use the violated predicate as the new clause, which is the WLP of the violation if the violation is only dependent on the havocing instruction. **TODO**: to make it more complete, we need to implement a WLP algorithm * For null-pointer violation, we choose `__CPROVER_same_object(ptr, __CPROVER_loop_entry(ptr))` as the new clause. That is, the havoced pointer should points to the same object at the start of every iteration of the loop. It is a heuristic choice. This can be extended with the idea of alias analysis if needed. * For invariant-not-preserved violation, we enumerate strengthening clauses and check that if the invariant will be inductive after strengthening (disjunction with the new clause). The synthesizer works as follow 1. initialize the two invariant maps, 2. verify the current candidates built from the two maps, _a. return the candidate if there is no violation _b. synthesize a new clause to resolve the **first** violation and add it to the correct map, 3. repeat 2.
1 parent 3ff3980 commit e599b85

21 files changed

+4622
-0
lines changed

‎src/ansi-c/compiler_headers/arm_builtin_headers.inc

+45
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
"// clang-format off\n"
2+
"void __breakpoint(int val);\n"
3+
"void __cdp(unsigned int coproc, unsigned int ops, unsigned int regs);\n"
4+
"void __clrex(void);\n"
5+
"unsigned char __clz(unsigned int val);\n"
6+
"unsigned int __current_pc(void);\n"
7+
"unsigned int __current_sp(void);\n"
8+
"int __disable_fiq(void);\n"
9+
"int __disable_irq(void);\n"
10+
"void __enable_fiq(void);\n"
11+
"void __enable_irq(void);\n"
12+
"double __fabs(double val);\n"
13+
"float __fabs(float val);\n"
14+
"void __force_stores(void);\n"
15+
"unsigned int __ldrex(volatile void *ptr);\n"
16+
"unsigned long long __ldrexd(volatile void *ptr);\n"
17+
"unsigned int __ldrt(const volatile void *ptr);\n"
18+
"void __memory_changed(void);\n"
19+
"void __nop(void);\n"
20+
"void __pld();\n"
21+
"void __pldw();\n"
22+
"void __pli();\n"
23+
"void __promise(expr);\n"
24+
"int __qadd(int val1, int val2);\n"
25+
"int __qdbl(int val);\n"
26+
"int __qsub(int val1, int val2);\n"
27+
"unsigned int __rbit(unsigned int val);\n"
28+
"unsigned int __rev(unsigned int val);\n"
29+
"unsigned int __return_address(void);\n"
30+
"unsigned int __ror(unsigned int val, unsigned int shift);\n"
31+
"void __schedule_barrier(void);\n"
32+
"int __semihost(int val, const void *ptr);\n"
33+
"void __sev(void);\n"
34+
"void __sev(void);\n"
35+
"float __sqrtf(float);\n"
36+
"int __ssat(int val, unsigned int sat);\n"
37+
"int __strex(unsigned int val, volatile void *ptr);\n"
38+
"int __strexd(unsigned long long val, volatile void *ptr);\n"
39+
"void __strt(unsigned int val, volatile void *ptr);\n"
40+
"unsigned int __swp(unsigned int val, volatile void *ptr);\n"
41+
"int __usat(unsigned int val, unsigned int sat);\n"
42+
"void __wfe(void);\n"
43+
"void __wfi(void);\n"
44+
"void __yield(void);\n"
45+
"// clang-format on\n"

‎src/ansi-c/compiler_headers/clang_builtin_headers.inc

+96
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,96 @@
1+
"// clang-format off\n"
2+
"__gcc_v2di __builtin_ia32_undef128(void);\n"
3+
"__gcc_v4di __builtin_ia32_undef256(void);\n"
4+
"__gcc_v8di __builtin_ia32_undef512(void);\n"
5+
"\n"
6+
"__gcc_v8hi __builtin_ia32_cvtne2ps2bf16_128(__gcc_v4sf, __gcc_v4sf);\n"
7+
"__gcc_v16hi __builtin_ia32_cvtne2ps2bf16_256(__gcc_v8sf, __gcc_v8sf);\n"
8+
"__gcc_v32hi __builtin_ia32_cvtne2ps2bf16_512(__gcc_v16sf, __gcc_v16sf);\n"
9+
"__gcc_v8hi __builtin_ia32_cvtneps2bf16_128_mask(__gcc_v4sf, __gcc_v8hi, unsigned char);\n"
10+
"__gcc_v8hi __builtin_ia32_cvtneps2bf16_256_mask(__gcc_v8sf, __gcc_v8hi, unsigned char);\n"
11+
"__gcc_v16si __builtin_ia32_cvtneps2bf16_512_mask(__gcc_v16sf, __gcc_v16hi, unsigned short);\n"
12+
"__gcc_v4sf __builtin_ia32_dpbf16ps_128(__gcc_v4sf, __gcc_v4si, __gcc_v4si);\n"
13+
"__gcc_v8sf __builtin_ia32_dpbf16ps_256(__gcc_v8sf, __gcc_v8si, __gcc_v8si);\n"
14+
"__gcc_v16sf __builtin_ia32_dpbf16ps_512(__gcc_v16sf, __gcc_v16si, __gcc_v16si);\n"
15+
"float __builtin_ia32_cvtsbf162ss_32(unsigned short);\n"
16+
"\n"
17+
"void __builtin_ia32_vp2intersect_d_512(__gcc_v16si, __gcc_v16si, unsigned short *, unsigned short *);\n"
18+
"void __builtin_ia32_vp2intersect_d_256(__gcc_v8si, __gcc_v8si, unsigned char *, unsigned char *);\n"
19+
"void __builtin_ia32_vp2intersect_d_128(__gcc_v4si, __gcc_v4si, unsigned char *, unsigned char *);\n"
20+
"\n"
21+
"__gcc_v16qi __builtin_ia32_selectb_128(unsigned short, __gcc_v16qi, __gcc_v16qi);\n"
22+
"__gcc_v32qi __builtin_ia32_selectb_256(unsigned int, __gcc_v32qi, __gcc_v32qi);\n"
23+
"__gcc_v64qi __builtin_ia32_selectb_512(unsigned long int, __gcc_v64qi, __gcc_v64qi);\n"
24+
"__gcc_v8hi __builtin_ia32_selectw_128(unsigned char, __gcc_v8hi, __gcc_v8hi);\n"
25+
"__gcc_v16hi __builtin_ia32_selectw_256(unsigned short, __gcc_v16hi, __gcc_v16hi);\n"
26+
"__gcc_v32hi __builtin_ia32_selectw_512(unsigned int, __gcc_v32hi, __gcc_v32hi);\n"
27+
"__gcc_v4si __builtin_ia32_selectd_128(unsigned char, __gcc_v4si, __gcc_v4si);\n"
28+
"__gcc_v8si __builtin_ia32_selectd_256(unsigned char, __gcc_v8si, __gcc_v8si);\n"
29+
"__gcc_v16si __builtin_ia32_selectd_512(unsigned short, __gcc_v16si, __gcc_v16si);\n"
30+
"__gcc_v4sf __builtin_ia32_selectps_128(unsigned char, __gcc_v4sf, __gcc_v4sf);\n"
31+
"__gcc_v8sf __builtin_ia32_selectps_256(unsigned char, __gcc_v8sf, __gcc_v8sf);\n"
32+
"__gcc_v16sf __builtin_ia32_selectps_512(unsigned short, __gcc_v16sf, __gcc_v16sf);\n"
33+
"__gcc_v2df __builtin_ia32_selectpd_128(unsigned char, __gcc_v2df, __gcc_v2df);\n"
34+
"__gcc_v4df __builtin_ia32_selectpd_256(unsigned char, __gcc_v4df, __gcc_v4df);\n"
35+
"__gcc_v8df __builtin_ia32_selectpd_512(unsigned char, __gcc_v8df, __gcc_v8df);\n"
36+
"__gcc_v4sf __builtin_ia32_selectss_128(unsigned char, __gcc_v4sf, __gcc_v4sf);\n"
37+
"__gcc_v2df __builtin_ia32_selectsd_128(unsigned char, __gcc_v2df, __gcc_v2df);\n"
38+
"\n"
39+
"__gcc_v4sf __builtin_ia32_vfmaddss3_mask(__gcc_v4sf, __gcc_v4sf, __gcc_v4sf, unsigned char, int);\n"
40+
"__gcc_v4sf __builtin_ia32_vfmaddss3_maskz(__gcc_v4sf, __gcc_v4sf, __gcc_v4sf, unsigned char, int);\n"
41+
"__gcc_v4sf __builtin_ia32_vfmaddss3_mask3(__gcc_v4sf, __gcc_v4sf, __gcc_v4sf, unsigned char, int);\n"
42+
"__gcc_v2df __builtin_ia32_vfmaddsd3_mask(__gcc_v2df, __gcc_v2df, __gcc_v2df, unsigned char, int);\n"
43+
"__gcc_v2df __builtin_ia32_vfmaddsd3_maskz(__gcc_v2df, __gcc_v2df, __gcc_v2df, unsigned char, int);\n"
44+
"__gcc_v2df __builtin_ia32_vfmaddsd3_mask3(__gcc_v2df, __gcc_v2df, __gcc_v2df, unsigned char, int);\n"
45+
"__gcc_v2df __builtin_ia32_vfmsubsd3_mask3(__gcc_v2df, __gcc_v2df, __gcc_v2df, unsigned char, int);\n"
46+
"__gcc_v4sf __builtin_ia32_vfmsubss3_mask3(__gcc_v4sf, __gcc_v4sf, __gcc_v4sf, unsigned char, int);\n"
47+
"\n"
48+
"__gcc_v4sf __builtin_ia32_cvtsd2ss_round_mask(__gcc_v4sf, __gcc_v2df, __gcc_v4sf, unsigned char, int);\n"
49+
"__gcc_v2df __builtin_ia32_cvtss2sd_round_mask(__gcc_v2df, __gcc_v4sf, __gcc_v2df, unsigned char, int);\n"
50+
"\n"
51+
"void __builtin_ia32_tile_loadconfig_internal(const void *);\n"
52+
"__gcc_v256si __builtin_ia32_tileloadd64_internal(unsigned short, unsigned short, const void *, __CPROVER_size_t);\n"
53+
"__gcc_v256si __builtin_ia32_tileloaddt164_internal(unsigned short, unsigned short, const void *, __CPROVER_size_t);\n"
54+
"__gcc_v256si __builtin_ia32_tdpbssd_internal(unsigned short, unsigned short, unsigned short, __gcc_v256si, __gcc_v256si, __gcc_v256si);\n"
55+
"__gcc_v256si __builtin_ia32_tdpbsud_internal(unsigned short, unsigned short, unsigned short, __gcc_v256si, __gcc_v256si, __gcc_v256si);\n"
56+
"__gcc_v256si __builtin_ia32_tdpbusd_internal(unsigned short, unsigned short, unsigned short, __gcc_v256si, __gcc_v256si, __gcc_v256si);\n"
57+
"__gcc_v256si __builtin_ia32_tdpbuud_internal(unsigned short, unsigned short, unsigned short, __gcc_v256si, __gcc_v256si, __gcc_v256si);\n"
58+
"void __builtin_ia32_tilestored64_internal(unsigned short, unsigned short, void *, __CPROVER_size_t, __gcc_v256si);\n"
59+
"__gcc_v256si __builtin_ia32_tilezero_internal(unsigned short, unsigned short);\n"
60+
"__gcc_v256si __builtin_ia32_tdpbf16ps_internal(unsigned short, unsigned short, unsigned short, __gcc_v256si, __gcc_v256si, __gcc_v256si);\n"
61+
"void __builtin_ia32_tile_loadconfig(const void *);\n"
62+
"void __builtin_ia32_tile_storeconfig(const void *);\n"
63+
"void __builtin_ia32_tilerelease(void);\n"
64+
"void __builtin_ia32_tilezero(unsigned char);\n"
65+
"void __builtin_ia32_tileloadd64(__tile, const void *, __CPROVER_size_t);\n"
66+
"void __builtin_ia32_tileloaddt164(__tile, const void *, __CPROVER_size_t);\n"
67+
"void __builtin_ia32_tilestored64(__tile, void *, __CPROVER_size_t);\n"
68+
"void __builtin_ia32_tdpbssd(__tile, __tile, __tile);\n"
69+
"void __builtin_ia32_tdpbsud(__tile, __tile, __tile);\n"
70+
"void __builtin_ia32_tdpbusd(__tile, __tile, __tile);\n"
71+
"void __builtin_ia32_tdpbuud(__tile, __tile, __tile);\n"
72+
"void __builtin_ia32_tdpbf16ps(__tile, __tile, __tile);\n"
73+
"void __builtin_ia32_ptwrite64(unsigned long long int);\n"
74+
"\n"
75+
"void __builtin_nontemporal_store();\n"
76+
"void __builtin_nontemporal_load();\n"
77+
"\n"
78+
"int __builtin_flt_rounds(void);\n"
79+
"\n"
80+
"unsigned char __builtin_bitreverse8(unsigned char);\n"
81+
"unsigned short __builtin_bitreverse16(unsigned short);\n"
82+
"unsigned int __builtin_bitreverse32(unsigned int);\n"
83+
"unsigned long long __builtin_bitreverse64(unsigned long long);\n"
84+
"\n"
85+
"unsigned char __builtin_rotateleft8(unsigned char, unsigned char);\n"
86+
"unsigned short __builtin_rotateleft16(unsigned short, unsigned short);\n"
87+
"unsigned int __builtin_rotateleft32(unsigned int, unsigned int);\n"
88+
"unsigned long long __builtin_rotateleft64(unsigned long long, unsigned long long);\n"
89+
"\n"
90+
"unsigned char __builtin_rotateright8(unsigned char, unsigned char);\n"
91+
"unsigned short __builtin_rotateright16(unsigned short, unsigned short);\n"
92+
"unsigned int __builtin_rotateright32(unsigned int, unsigned int);\n"
93+
"unsigned long long __builtin_rotateright64(unsigned long long, unsigned long long);\n"
94+
"\n"
95+
"void __builtin_assume(__CPROVER_bool);\n"
96+
"// clang-format on\n"

‎src/ansi-c/compiler_headers/cw_builtin_headers.inc

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
"// clang-format off\n"
2+
"int __abs(int);\n"
3+
"void __builtin_va_info();\n"
4+
"__CPROVER_size_t __builtin_force_const(__CPROVER_size_t);\n"
5+
"// clang-format on\n"

‎src/ansi-c/compiler_headers/gcc_builtin_headers_alpha.inc

+48
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
"// clang-format off\n"
2+
"long __builtin_alpha_implver(void);\n"
3+
"long __builtin_alpha_rpcc(void);\n"
4+
"long __builtin_alpha_amask(long);\n"
5+
"long __builtin_alpha_cmpbge(long, long);\n"
6+
"long __builtin_alpha_extbl(long, long);\n"
7+
"long __builtin_alpha_extwl(long, long);\n"
8+
"long __builtin_alpha_extll(long, long);\n"
9+
"long __builtin_alpha_extql(long, long);\n"
10+
"long __builtin_alpha_extwh(long, long);\n"
11+
"long __builtin_alpha_extlh(long, long);\n"
12+
"long __builtin_alpha_extqh(long, long);\n"
13+
"long __builtin_alpha_insbl(long, long);\n"
14+
"long __builtin_alpha_inswl(long, long);\n"
15+
"long __builtin_alpha_insll(long, long);\n"
16+
"long __builtin_alpha_insql(long, long);\n"
17+
"long __builtin_alpha_inswh(long, long);\n"
18+
"long __builtin_alpha_inslh(long, long);\n"
19+
"long __builtin_alpha_insqh(long, long);\n"
20+
"long __builtin_alpha_mskbl(long, long);\n"
21+
"long __builtin_alpha_mskwl(long, long);\n"
22+
"long __builtin_alpha_mskll(long, long);\n"
23+
"long __builtin_alpha_mskql(long, long);\n"
24+
"long __builtin_alpha_mskwh(long, long);\n"
25+
"long __builtin_alpha_msklh(long, long);\n"
26+
"long __builtin_alpha_mskqh(long, long);\n"
27+
"long __builtin_alpha_umulh(long, long);\n"
28+
"long __builtin_alpha_zap(long, long);\n"
29+
"long __builtin_alpha_zapnot(long, long);\n"
30+
"long __builtin_alpha_pklb(long);\n"
31+
"long __builtin_alpha_pkwb(long);\n"
32+
"long __builtin_alpha_unpkbl(long);\n"
33+
"long __builtin_alpha_unpkbw(long);\n"
34+
"long __builtin_alpha_minub8(long, long);\n"
35+
"long __builtin_alpha_minsb8(long, long);\n"
36+
"long __builtin_alpha_minuw4(long, long);\n"
37+
"long __builtin_alpha_minsw4(long, long);\n"
38+
"long __builtin_alpha_maxub8(long, long);\n"
39+
"long __builtin_alpha_maxsb8(long, long);\n"
40+
"long __builtin_alpha_maxuw4(long, long);\n"
41+
"long __builtin_alpha_maxsw4(long, long);\n"
42+
"long __builtin_alpha_perr(long, long);\n"
43+
"long __builtin_alpha_cttz(long);\n"
44+
"long __builtin_alpha_ctlz(long);\n"
45+
"long __builtin_alpha_ctpop(long);\n"
46+
"void *__builtin_thread_pointer(void);\n"
47+
"void __builtin_set_thread_pointer(void *);\n"
48+
"// clang-format on\n"

‎src/ansi-c/compiler_headers/gcc_builtin_headers_arm.inc

+136
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
"// clang-format off\n"
2+
"int __builtin_arm_getwcx(int);\n"
3+
"void __builtin_arm_setwcx(int, int);\n"
4+
"int __builtin_arm_textrmsb(__gcc_v8qi, int);\n"
5+
"int __builtin_arm_textrmsh(__gcc_v4hi, int);\n"
6+
"int __builtin_arm_textrmsw(__gcc_v2si, int);\n"
7+
"int __builtin_arm_textrmub(__gcc_v8qi, int);\n"
8+
"int __builtin_arm_textrmuh(__gcc_v4hi, int);\n"
9+
"int __builtin_arm_textrmuw(__gcc_v2si, int);\n"
10+
"__gcc_v8qi __builtin_arm_tinsrb(__gcc_v8qi, int);\n"
11+
"__gcc_v4hi __builtin_arm_tinsrh(__gcc_v4hi, int);\n"
12+
"__gcc_v2si __builtin_arm_tinsrw(__gcc_v2si, int);\n"
13+
"long long __builtin_arm_tmia(long long, int, int);\n"
14+
"long long __builtin_arm_tmiabb(long long, int, int);\n"
15+
"long long __builtin_arm_tmiabt(long long, int, int);\n"
16+
"long long __builtin_arm_tmiaph(long long, int, int);\n"
17+
"long long __builtin_arm_tmiatb(long long, int, int);\n"
18+
"long long __builtin_arm_tmiatt(long long, int, int);\n"
19+
"int __builtin_arm_tmovmskb(__gcc_v8qi);\n"
20+
"int __builtin_arm_tmovmskh(__gcc_v4hi);\n"
21+
"int __builtin_arm_tmovmskw(__gcc_v2si);\n"
22+
"long long __builtin_arm_waccb(__gcc_v8qi);\n"
23+
"long long __builtin_arm_wacch(__gcc_v4hi);\n"
24+
"long long __builtin_arm_waccw(__gcc_v2si);\n"
25+
"__gcc_v8qi __builtin_arm_waddb(__gcc_v8qi, __gcc_v8qi);\n"
26+
"__gcc_v8qi __builtin_arm_waddbss(__gcc_v8qi, __gcc_v8qi);\n"
27+
"__gcc_v8qi __builtin_arm_waddbus(__gcc_v8qi, __gcc_v8qi);\n"
28+
"__gcc_v4hi __builtin_arm_waddh(__gcc_v4hi, __gcc_v4hi);\n"
29+
"__gcc_v4hi __builtin_arm_waddhss(__gcc_v4hi, __gcc_v4hi);\n"
30+
"__gcc_v4hi __builtin_arm_waddhus(__gcc_v4hi, __gcc_v4hi);\n"
31+
"__gcc_v2si __builtin_arm_waddw(__gcc_v2si, __gcc_v2si);\n"
32+
"__gcc_v2si __builtin_arm_waddwss(__gcc_v2si, __gcc_v2si);\n"
33+
"__gcc_v2si __builtin_arm_waddwus(__gcc_v2si, __gcc_v2si);\n"
34+
"__gcc_v8qi __builtin_arm_walign(__gcc_v8qi, __gcc_v8qi, int);\n"
35+
"long long __builtin_arm_wand(long long, long long);\n"
36+
"long long __builtin_arm_wandn(long long, long long);\n"
37+
"__gcc_v8qi __builtin_arm_wavg2b(__gcc_v8qi, __gcc_v8qi);\n"
38+
"__gcc_v8qi __builtin_arm_wavg2br(__gcc_v8qi, __gcc_v8qi);\n"
39+
"__gcc_v4hi __builtin_arm_wavg2h(__gcc_v4hi, __gcc_v4hi);\n"
40+
"__gcc_v4hi __builtin_arm_wavg2hr(__gcc_v4hi, __gcc_v4hi);\n"
41+
"__gcc_v8qi __builtin_arm_wcmpeqb(__gcc_v8qi, __gcc_v8qi);\n"
42+
"__gcc_v4hi __builtin_arm_wcmpeqh(__gcc_v4hi, __gcc_v4hi);\n"
43+
"__gcc_v2si __builtin_arm_wcmpeqw(__gcc_v2si, __gcc_v2si);\n"
44+
"__gcc_v8qi __builtin_arm_wcmpgtsb(__gcc_v8qi, __gcc_v8qi);\n"
45+
"__gcc_v4hi __builtin_arm_wcmpgtsh(__gcc_v4hi, __gcc_v4hi);\n"
46+
"__gcc_v2si __builtin_arm_wcmpgtsw(__gcc_v2si, __gcc_v2si);\n"
47+
"__gcc_v8qi __builtin_arm_wcmpgtub(__gcc_v8qi, __gcc_v8qi);\n"
48+
"__gcc_v4hi __builtin_arm_wcmpgtuh(__gcc_v4hi, __gcc_v4hi);\n"
49+
"__gcc_v2si __builtin_arm_wcmpgtuw(__gcc_v2si, __gcc_v2si);\n"
50+
"long long __builtin_arm_wmacs(long long, __gcc_v4hi, __gcc_v4hi);\n"
51+
"long long __builtin_arm_wmacsz(__gcc_v4hi, __gcc_v4hi);\n"
52+
"long long __builtin_arm_wmacu(long long, __gcc_v4hi, __gcc_v4hi);\n"
53+
"long long __builtin_arm_wmacuz(__gcc_v4hi, __gcc_v4hi);\n"
54+
"__gcc_v4hi __builtin_arm_wmadds(__gcc_v4hi, __gcc_v4hi);\n"
55+
"__gcc_v4hi __builtin_arm_wmaddu(__gcc_v4hi, __gcc_v4hi);\n"
56+
"__gcc_v8qi __builtin_arm_wmaxsb(__gcc_v8qi, __gcc_v8qi);\n"
57+
"__gcc_v4hi __builtin_arm_wmaxsh(__gcc_v4hi, __gcc_v4hi);\n"
58+
"__gcc_v2si __builtin_arm_wmaxsw(__gcc_v2si, __gcc_v2si);\n"
59+
"__gcc_v8qi __builtin_arm_wmaxub(__gcc_v8qi, __gcc_v8qi);\n"
60+
"__gcc_v4hi __builtin_arm_wmaxuh(__gcc_v4hi, __gcc_v4hi);\n"
61+
"__gcc_v2si __builtin_arm_wmaxuw(__gcc_v2si, __gcc_v2si);\n"
62+
"__gcc_v8qi __builtin_arm_wminsb(__gcc_v8qi, __gcc_v8qi);\n"
63+
"__gcc_v4hi __builtin_arm_wminsh(__gcc_v4hi, __gcc_v4hi);\n"
64+
"__gcc_v2si __builtin_arm_wminsw(__gcc_v2si, __gcc_v2si);\n"
65+
"__gcc_v8qi __builtin_arm_wminub(__gcc_v8qi, __gcc_v8qi);\n"
66+
"__gcc_v4hi __builtin_arm_wminuh(__gcc_v4hi, __gcc_v4hi);\n"
67+
"__gcc_v2si __builtin_arm_wminuw(__gcc_v2si, __gcc_v2si);\n"
68+
"__gcc_v4hi __builtin_arm_wmulsm(__gcc_v4hi, __gcc_v4hi);\n"
69+
"__gcc_v4hi __builtin_arm_wmulul(__gcc_v4hi, __gcc_v4hi);\n"
70+
"__gcc_v4hi __builtin_arm_wmulum(__gcc_v4hi, __gcc_v4hi);\n"
71+
"long long __builtin_arm_wor(long long, long long);\n"
72+
"__gcc_v2si __builtin_arm_wpackdss(long long, long long);\n"
73+
"__gcc_v2si __builtin_arm_wpackdus(long long, long long);\n"
74+
"__gcc_v8qi __builtin_arm_wpackhss(__gcc_v4hi, __gcc_v4hi);\n"
75+
"__gcc_v8qi __builtin_arm_wpackhus(__gcc_v4hi, __gcc_v4hi);\n"
76+
"__gcc_v4hi __builtin_arm_wpackwss(__gcc_v2si, __gcc_v2si);\n"
77+
"__gcc_v4hi __builtin_arm_wpackwus(__gcc_v2si, __gcc_v2si);\n"
78+
"long long __builtin_arm_wrord(long long, long long);\n"
79+
"long long __builtin_arm_wrordi(long long, int);\n"
80+
"__gcc_v4hi __builtin_arm_wrorh(__gcc_v4hi, long long);\n"
81+
"__gcc_v4hi __builtin_arm_wrorhi(__gcc_v4hi, int);\n"
82+
"__gcc_v2si __builtin_arm_wrorw(__gcc_v2si, long long);\n"
83+
"__gcc_v2si __builtin_arm_wrorwi(__gcc_v2si, int);\n"
84+
"__gcc_v2si __builtin_arm_wsadb(__gcc_v8qi, __gcc_v8qi);\n"
85+
"__gcc_v2si __builtin_arm_wsadbz(__gcc_v8qi, __gcc_v8qi);\n"
86+
"__gcc_v2si __builtin_arm_wsadh(__gcc_v4hi, __gcc_v4hi);\n"
87+
"__gcc_v2si __builtin_arm_wsadhz(__gcc_v4hi, __gcc_v4hi);\n"
88+
"__gcc_v4hi __builtin_arm_wshufh(__gcc_v4hi, int);\n"
89+
"long long __builtin_arm_wslld(long long, long long);\n"
90+
"long long __builtin_arm_wslldi(long long, int);\n"
91+
"__gcc_v4hi __builtin_arm_wsllh(__gcc_v4hi, long long);\n"
92+
"__gcc_v4hi __builtin_arm_wsllhi(__gcc_v4hi, int);\n"
93+
"__gcc_v2si __builtin_arm_wsllw(__gcc_v2si, long long);\n"
94+
"__gcc_v2si __builtin_arm_wsllwi(__gcc_v2si, int);\n"
95+
"long long __builtin_arm_wsrad(long long, long long);\n"
96+
"long long __builtin_arm_wsradi(long long, int);\n"
97+
"__gcc_v4hi __builtin_arm_wsrah(__gcc_v4hi, long long);\n"
98+
"__gcc_v4hi __builtin_arm_wsrahi(__gcc_v4hi, int);\n"
99+
"__gcc_v2si __builtin_arm_wsraw(__gcc_v2si, long long);\n"
100+
"__gcc_v2si __builtin_arm_wsrawi(__gcc_v2si, int);\n"
101+
"long long __builtin_arm_wsrld(long long, long long);\n"
102+
"long long __builtin_arm_wsrldi(long long, int);\n"
103+
"__gcc_v4hi __builtin_arm_wsrlh(__gcc_v4hi, long long);\n"
104+
"__gcc_v4hi __builtin_arm_wsrlhi(__gcc_v4hi, int);\n"
105+
"__gcc_v2si __builtin_arm_wsrlw(__gcc_v2si, long long);\n"
106+
"__gcc_v2si __builtin_arm_wsrlwi(__gcc_v2si, int);\n"
107+
"__gcc_v8qi __builtin_arm_wsubb(__gcc_v8qi, __gcc_v8qi);\n"
108+
"__gcc_v8qi __builtin_arm_wsubbss(__gcc_v8qi, __gcc_v8qi);\n"
109+
"__gcc_v8qi __builtin_arm_wsubbus(__gcc_v8qi, __gcc_v8qi);\n"
110+
"__gcc_v4hi __builtin_arm_wsubh(__gcc_v4hi, __gcc_v4hi);\n"
111+
"__gcc_v4hi __builtin_arm_wsubhss(__gcc_v4hi, __gcc_v4hi);\n"
112+
"__gcc_v4hi __builtin_arm_wsubhus(__gcc_v4hi, __gcc_v4hi);\n"
113+
"__gcc_v2si __builtin_arm_wsubw(__gcc_v2si, __gcc_v2si);\n"
114+
"__gcc_v2si __builtin_arm_wsubwss(__gcc_v2si, __gcc_v2si);\n"
115+
"__gcc_v2si __builtin_arm_wsubwus(__gcc_v2si, __gcc_v2si);\n"
116+
"__gcc_v4hi __builtin_arm_wunpckehsb(__gcc_v8qi);\n"
117+
"__gcc_v2si __builtin_arm_wunpckehsh(__gcc_v4hi);\n"
118+
"long long __builtin_arm_wunpckehsw(__gcc_v2si);\n"
119+
"__gcc_v4hi __builtin_arm_wunpckehub(__gcc_v8qi);\n"
120+
"__gcc_v2si __builtin_arm_wunpckehuh(__gcc_v4hi);\n"
121+
"long long __builtin_arm_wunpckehuw(__gcc_v2si);\n"
122+
"__gcc_v4hi __builtin_arm_wunpckelsb(__gcc_v8qi);\n"
123+
"__gcc_v2si __builtin_arm_wunpckelsh(__gcc_v4hi);\n"
124+
"long long __builtin_arm_wunpckelsw(__gcc_v2si);\n"
125+
"__gcc_v4hi __builtin_arm_wunpckelub(__gcc_v8qi);\n"
126+
"__gcc_v2si __builtin_arm_wunpckeluh(__gcc_v4hi);\n"
127+
"long long __builtin_arm_wunpckeluw(__gcc_v2si);\n"
128+
"__gcc_v8qi __builtin_arm_wunpckihb(__gcc_v8qi, __gcc_v8qi);\n"
129+
"__gcc_v4hi __builtin_arm_wunpckihh(__gcc_v4hi, __gcc_v4hi);\n"
130+
"__gcc_v2si __builtin_arm_wunpckihw(__gcc_v2si, __gcc_v2si);\n"
131+
"__gcc_v8qi __builtin_arm_wunpckilb(__gcc_v8qi, __gcc_v8qi);\n"
132+
"__gcc_v4hi __builtin_arm_wunpckilh(__gcc_v4hi, __gcc_v4hi);\n"
133+
"__gcc_v2si __builtin_arm_wunpckilw(__gcc_v2si, __gcc_v2si);\n"
134+
"long long __builtin_arm_wxor(long long, long long);\n"
135+
"long long __builtin_arm_wzero();\n"
136+
"// clang-format on\n"

0 commit comments

Comments
 (0)