Generalize load-immediate operations on ARM #203

gergo- · 2017-09-15T09:11:19Z

On ARM, movw and movt can always be used to load immediates into general-purpose registers. This used to be only done in Thumb mode. It is simpler than the series of orr operations that used to be emitted in ARM mode.

Also, the ARMv6 flavor targeted by CompCert is in fact ARMv6T2 (with Thumb2).

The ARMv6 comes in two flavors depending on the version of the Thumb instruction set supported: ARMv6 for the original Thumb, ARMv6T2 for Thumb2. CompCert only supports Thumb2, so its ARMv6 architecture should really be called ARMv6T2. This makes a difference: the GNU assembler rejects most of the instructions CompCert generates for ARMv6 with "-mthumb" if the architecture is specified as ".arch armv6" as opposed to ".arch armv6t2". This patch fixes the architecture specification in the target printer and the internal name of the architecture. It does not change the configure script's flags to avoid breaking changes.

These move-immediate instructions used to be only emitted in Thumb mode, not in ARM mode. As far as I understand ARM's documentation, these instructions are available in *both* modes in ARMv6T2 and above. This should cover all of CompCert's ARM targets. Tested for ARMv6 and ARMv7, both with and without Thumb2. The behavior is now identical to Clang, and the GNU assembler accepts these instructions in all configurations.

xavierleroy · 2017-09-15T09:55:57Z

Indeed, the question is whether we want to support "plain" ARMv6 (before ARMv6T2) or not. If the answer is "yes" we need to keep the old, ORR-based code. If "no", the movw/movt sequence is probably better in almost all cases.

Also, the ARMv6 flavor targeted by CompCert is in fact ARMv6T2 (with Thumb2).

What makes you conclude this? If the option -thumb is not given, doesn't CompCert generate "plain" ARMv6 (not T2) code?

gergo- · 2017-09-15T11:22:35Z

If the option -thumb is not given, doesn't CompCert generate "plain" ARMv6 (not T2) code?

Yes, it does. Sorry if I was unclear. My understanding is that if -mthumb is not specified, it doesn't matter whether the architecture is called armv6 or armv6t2. I'm not aware of differences in ARM mode among these architectures (but I'm not an expert on this corner of the ecosystem). The test suite passes.

However, if CompCert is configured for armv6, and -mthumb is given, then it generates Thumb version 2, and the architecture must be called armv6t2 in the assembly code, otherwise the assembler rejects the code in all nontrivial cases.

So I think the check in the target printer could also be written as follows:
| "armv6" -> (if !Clflags.option_mthumb then "armv6t2" else "armv6")
and a similar guard could be added to runtime/arm/sysdeps.h. But I don't think it would add value.

gergo- · 2017-09-15T11:30:21Z

I'm not aware of differences in ARM mode among these architectures

Except, of course, exactly the very instructions being discussed here. Sorry, I'm getting confused by this topic. However:

Indeed, the question is whether we want to support "plain" ARMv6 (before ARMv6T2) or not.

If the answer to that question is yes, compilers configured for armv6 and armv6t2 would have to behave differently: The armv6 compiler would have to reject the -mthumb flag, because CompCert has no Thumb version 1 code generator.

- define separate architecture models for ARMv6 and ARMv6T2 - introduce `Archi.move_imm` parameter on ARM to identify models with `movw`/`movt` move-immediate instructions (all except ARMv6, in both ARM and Thumb mode)

gergo- · 2017-09-15T14:12:15Z

Added a patch to separate the ARMv6 and ARMv6T2 cases. There are now the following cases:

ARMv6. This is "plain" ARM without any version of Thumb. -mthumb and -marm flags are not supported, movw and movt are never generated.
ARMv6T2. Supports Thumb (version 2). Supports and generates movw and movt in both ARM and Thumb modes.
ARMv7 (various flavors). Supports Thumb. Supports and generates movw and movt in both ARM and Thumb modes.

The generation of movw and movt therefore now only depends on the configuration, not on command line flags. The choice is represented by the new Archi.move_imm parameter.

For the Archi.move_imm = false case (plain ARMv6), I added the old orr immedate generation back in.

Let me know if you think this is the way to go.

xavierleroy · 2017-09-15T15:34:04Z

This looks very good to me, thanks. A few nits in the code review that follows.

I don't know if there is commercial interest in "plain" ARMv6 (pre-Thumb-2) processors. Some Raspberry Pis were plain ARMv6: I remember because I had to buy a more modern ARM platform to test the Thumb2 mode of CompCert. At any rate, it cannot hurt to keep plain ARMv6 support in CompCert for the time being.

Just for the record: besides movw and movt ARMv6T2 introduces a few other instructions that are available both in ARM and Thumb2 encodings, esp. bit-field manipulation instructions bfc, bfi, sbfx, ubfx.

xavierleroy

A couple of suggestions.

xavierleroy · 2017-09-15T15:38:28Z

arm/Archi.v

 Parameter abi: abi_kind.
+
+(** Whether to generate [movw] and [movt] instructions. *)
+Parameter move_imm: bool.


I would prefer a different name and intuitive meaning for this parameter, one that means "plain ARMv6" versus "ARMv6T2 and above". One reason being that there are other instructions that are not in "plain ARMv6" and that we may want to generate some day. Some possible names:

thumb2_support or T2_support

armv6_only (with the opposite meaning: true for ARMv6, false for ARMv6T2 and up).

xavierleroy · 2017-09-15T15:40:00Z

driver/Driver.ml

-    [ Exact "-mthumb", Set option_mthumb;
-      Exact "-marm", Unset option_mthumb; ]
+    if Configuration.model = "armv6" then [] (* Thumb needs ARMv6T2 or ARMv7 *)
+    else


Just to nit-pick: the -marm option should be available on ARMv6 as well, so that a user who absolutely wants ARM encoding can express this intention by putting -marm, and still be able to compile on ARMv6.

- rename relevant parameter to `Archi.thumb2_support` - on ARMv6 without Thumb2, silently accept -marm flag (but not -mthumb) - allow generation of `sbfx` in ARM mode if Thumb2 is supported

gergo- · 2017-09-15T17:25:20Z

Thanks for the review, I added a new patch. Good point about sbfx in particular, which can now also be generated in ARM on models with Thumb2 support.

xavierleroy · 2017-09-18T07:24:47Z

I forgot that CompCert is already using the sbfx instruction! It's good to be able to use it in ARM mode as well as in Thumb mode.

The current code looks good to me. Maybe @m-schmidt or @bschommer would like to have a quick look at it before we merge?

bschommer · 2017-09-18T08:25:20Z

Looks good to us.

xavierleroy · 2017-09-18T12:35:06Z

All right, I merge, then.

At least OCaml 4.05 is now required as well as Coq 8.8.

gergo- added 2 commits September 15, 2017 10:31

Separate ARMv6 and ARMv6T2; no movw/movt on ARMv6

f77c945

- define separate architecture models for ARMv6 and ARMv6T2 - introduce `Archi.move_imm` parameter on ARM to identify models with `movw`/`movt` move-immediate instructions (all except ARMv6, in both ARM and Thumb mode)

xavierleroy reviewed Sep 15, 2017

View reviewed changes

Fixes for support for architectures with Thumb2

619da5d

- rename relevant parameter to `Archi.thumb2_support` - on ARMv6 without Thumb2, silently accept -marm flag (but not -mthumb) - allow generation of `sbfx` in ARM mode if Thumb2 is supported

xavierleroy merged commit c4dcf7c into AbsInt:master Sep 18, 2017

gergo- deleted the general-movw-movt branch September 22, 2017 08:43

xavierleroy pushed a commit that referenced this pull request Oct 31, 2019

Raise minimal required versions for OCaml and Coq (#203)

029329c

At least OCaml 4.05 is now required as well as Coq 8.8.

Generalize load-immediate operations on ARM #203

Generalize load-immediate operations on ARM #203

Uh oh!

Conversation

gergo- commented Sep 15, 2017

Uh oh!

xavierleroy commented Sep 15, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

gergo- commented Sep 15, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

gergo- commented Sep 15, 2017

Uh oh!

gergo- commented Sep 15, 2017

Uh oh!

xavierleroy commented Sep 15, 2017

Uh oh!

xavierleroy left a comment

Choose a reason for hiding this comment

Uh oh!

xavierleroy Sep 15, 2017

Choose a reason for hiding this comment

Uh oh!

xavierleroy Sep 15, 2017

Choose a reason for hiding this comment

Uh oh!

gergo- commented Sep 15, 2017

Uh oh!

xavierleroy commented Sep 18, 2017

Uh oh!

bschommer commented Sep 18, 2017

Uh oh!

xavierleroy commented Sep 18, 2017

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

xavierleroy commented Sep 15, 2017 •

edited

Loading

gergo- commented Sep 15, 2017 •

edited

Loading