Commit a05552d
committed
std_detect: RISC-V: Best effort implication by target config (C-related)
On the RISC-V architecture, there are some complex implications around the
"C" extension. This commit implements implication of such target features
in a best effort manner.
The reason why we can make this exact is lack of `"zcd"` and `"zcf"`
target features (that would require additional feature handling system).
Still, weaker implications implemented here are formally verified to be
optimal if we have to avoid tautology (except `"c"`) and uses of `"zcf"`
and `"zcd"` are prohibited.
For "C", the author deduced minimal expression which makes equal to the
"C" extension and extracted all cases where `"zcd"` and `"zcf"` are not
involved.
For "Zcd" and "Zcf", the author created proof statements, each stating
that implication expression (which avoids tautology and accidentally
avoids using `"zcd"` or `"zcf"`) is optimal to force corresponding
target feature to be enabled.1 parent bd2bb51 commit a05552d
1 file changed
+10
-2
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
270 | 270 | | |
271 | 271 | | |
272 | 272 | | |
| 273 | + | |
| 274 | + | |
| 275 | + | |
| 276 | + | |
| 277 | + | |
| 278 | + | |
| 279 | + | |
| 280 | + | |
273 | 281 | | |
274 | 282 | | |
275 | 283 | | |
276 | 284 | | |
277 | | - | |
| 285 | + | |
278 | 286 | | |
279 | 287 | | |
280 | | - | |
| 288 | + | |
281 | 289 | | |
282 | 290 | | |
283 | 291 | | |
| |||
0 commit comments