ARM Cortex M4 #242
ARM Cortex M4 #242
Conversation
| x = #BIC(x, -1); | ||
|
|
||
| // Shifts. | ||
| x = #BIC(x, arg0, #LSL(0)); |
There was a problem hiding this comment.
Personally, I do not like the syntax #LSL(0).
I think it is better to use arg0 << 0
There was a problem hiding this comment.
I will not block the PR for this. But at least we should discuss it
There was a problem hiding this comment.
Yes, we will need some lowering for Copn arguments (should be easy with the existing function in arm_lowering, I did not complete it to get these changes merged as soon as possible).
| let { L.pl_loc = loc ; L.pl_desc = s } = id in | ||
| let name, sz = extract_size s in | ||
| (* TODO_ARM: Merge this. *) |
There was a problem hiding this comment.
I have the impression that the change in the code
comes from #LSL(0) argument is it true ?
There was a problem hiding this comment.
Partly. To emit an ARM instruction we need to look for the mnemonic (e.g. ADD) but also for the S and cc suffixes (specifying whether it set flags or nor) and then the arguments (to check if they have a shifter register as an argument). That's why the tt_prim function now takes the arguments as well: ADD x, y, z << 2 needs to become ADD x, y, z, 2 and be tagged as having a LSL shift. Maybe there is a better way of doing this.
| @@ -1369,7 +1377,9 @@ let tt_prim asmOp ws id = | |||
| | PrimV pr -> (match sz with SAv (s, ve, sz) -> pr ws s ve sz | _ -> rs_tyerror ~loc (PrimIsVector s)) | |||
| | PrimX pr -> (match sz with SAx(sz1, sz2) -> pr ws sz1 sz2 | _ -> rs_tyerror ~loc (PrimIsX s)) | |||
| | PrimVV pr -> (match sz with SAvv (ve, sz, ve', sz') -> pr ws ve sz ve' sz' | _ -> rs_tyerror ~loc (PrimIsVectorVector s)) | |||
| | PrimARM _ -> failwith "tt_prim ARM M4" | |||
There was a problem hiding this comment.
The ARM case should be handled by the target_arch match. After the merge I will write a single tt_prim function that deals with all architectures uniformly.
| @@ -6,10 +6,65 @@ Set Implicit Arguments. | |||
| Unset Strict Implicit. | |||
| Unset Printing Implicit Defensive. | |||
|
|
|||
| Lemma disjoint_subset_diff xs ys : | |||
There was a problem hiding this comment.
Maybe, my remark is not related to this commit.
Why those proofs are not done for all set, i.e it is done only for Sv.
There was a problem hiding this comment.
Do you mean this should be a module like MSetEqProperties.EqProperties and then define something like SvP? Sorry, I'm not used to Coq modules yet
|
I’m going to merge this pull request soon. Can I squash all the commits in this branch into a single commit? |
I have no objection to squashing. But I still haven't pushed the changes to the parser we discussed because I don't know if the approach I mentioned on Zulip is viable. However I could also do it after merging. |
The idea is to make a release just before merging your branch, so that we have some time to fix and polish things, so I'd suggest to merge that as soon as possible and deal with all fixes/improvements in other PRs. |
Then I'll do the fixes in separate PRs later. |
vbgl
force-pushed
the
arm_m4
branch
2 times, most recently
from
32c4526
to
1dbdfb5
Compare
|
I’ve excluded the If you like type-class puzzles, here is one: https://gitlab.com/jasmin-lang/jasmin/-/jobs/3119039375 Any volunteer to give a look? |
|
The typeclass issue arises systematically with Coq 8.16 (and mathcomp 1.15). |
|
See #261 for a quick-and-dirty fix. |
No description provided.