Enable x86 indirect branch tracking in code and proofs (#203)

* x86: add script for adding endbr{32,64} instructions

* Implement CET for amd64

* Sync AT&T syntax files

* Add ENDBR64 to x86 model

This is intended to support the insertion of ENDBR64 into the x86
code to support indirect branch tracking (IBT), part of CET
(control-flow enforcement technology).

The actual semantics assumed is simply a NOP; on machines without
CET enabled, including older machines from before the feature
existed, this is indeed how it behaves. We do not attempt to model
the restrictions that are imposed when CET is enabled, and such
restrictions arguably belong on the indirect branches themselves, of
which there are none in s2n-bignum itself.

For more discussion see

  https://stackoverflow.com/questions/56905811/what-does-the-endbr64-instruction-actually-do

* Enable IBT by default in the code

This makes the code compile with IBT unless explicitly flagged
otherwise in the compiler options, hence inserting one initial
ENDBR64 instruction at the main entry point for each function.

The copy of the code given in each "define_assert_from_elf" is
also updated correspondingly.

So far, the proofs are not updated, though the

* Re-derive non-IBT version of code and restore proofs

This uses the function define_trimmed that trims away the first 4
bytes of the code (expected to be ENDBR64) and makes a definition
matching the non-IBT original, hence restoring the proofs.

* Use symbolic lengths for most x86 toplevel correctness theorems

This switches most xxx_SUBROUTINE_CORRECT statements to use
explicit "LENGTH code" hypotheses in place of explicit numbers.
The main unchanged ones are those with data in the text section
as well.

* Add IBT variants of x86 toplevel correctness statements

Every xxx_SUBROUTINE_CORRECT result, both standard and Windows ABI,
now has a variant xxx_IBT_SUBROUTINE_CORRECT in the file, with a
proof that mostly works automatically via the new ADD_IBT_RULE,
corresponding to the case where the code is prefixed by ENDBR64.
This rule fails to handle the cases with data in the text section;
this occurs in these proofs that will need fixing next:

        edwards25519_scalarmuldouble_alt.ml
        edwards25519_scalarmuldouble.ml
        edwards25519_scalarmulbase_alt.ml
        edwards25519_scalarmulbase.ml
        curve25519_x25519base_alt.ml
        curve25519_x25519base.ml

* Fix remaining IBT proof breaks

This is done by making ADD_IBT_RULE a little more robust so that it
handles the case of appended code and data tables, and also modifies
explicit code length numbers as well as symbolic lengths.

* Invert naming conventions for x86 Windows and IBT versions

This switches around the naming conventions in correctness theorems
and machine code definitions:

 * Instead of the IBT forms of correctness theorems having their names
   flagged with _IBT, that is now the default and the others are
   labelled explicitly as _NOIBT

 * The WINDOWS_ modifier is used as a suffix not a prefix in correctness
   statements, and likewise for windows_ in the machine code definitions.

 * The full machine code with ENDBR64 has a name ending _mc and the
   trimmed form without ENDBR64 has a name ending _tmc (t for trimmed).

* Use platform CET header where possible

The explicit ENDBR64 definition is now only used if the platform is
not already enabling CET. This improvement was suggested by lgv5 in
the discussion at #173

* Expand ENDBR64 explanatory comment, fix whitespace

Where "fix whitespace" means both of the following:

  (1) remove all trailing spaces
  (2) expand all tabs to spaces, except in Makefiles and tools.

* Install libpcre2-dev in the CI codebuild

---------

Co-authored-by: Lucas Gabriel Vuotto <[email protected]>

Author: jargh

arm/fastmul/bignum_emontredc_8n.S

@@ -19,10 +19,10 @@
 // ----------------------------------------------------------------------------
 #include "_internal_s2n_bignum.h"
 
-					S2N_BN_SYM_VISIBILITY_DIRECTIVE(bignum_emontredc_8n_cdiff_base)
-					S2N_BN_SYM_PRIVACY_DIRECTIVE(bignum_emontredc_8n_cdiff_base)
-					.text
-					.balign 4
+                                        S2N_BN_SYM_VISIBILITY_DIRECTIVE(bignum_emontredc_8n_cdiff_base)
+                                        S2N_BN_SYM_PRIVACY_DIRECTIVE(bignum_emontredc_8n_cdiff_base)
+                                        .text
+                                        .balign 4
 
         // Silly SLOTHY limitation: It needs the loop counter to have the name 'count'
         count .req x27 // inner loop counter
@@ -247,10 +247,10 @@ bignum_emontredc_8n_cdiff_base_outerloop:
           vmul_2x_64_64_128 v21, x4, v0, v1
           mov x14, v0.d[0]
           mov x15, v0.d[1]
-          mul	x12, x4, x8
+          mul   x12, x4, x8
           adds x17, x17, x12
           umulh x12, x4, x8
-          mul	x13, x4, x9
+          mul   x13, x4, x9
           adcs x19, x19, x13
           umulh x13, x4, x9
           adcs x20, x20, x14
@@ -270,12 +270,12 @@ bignum_emontredc_8n_cdiff_base_outerloop:
           vmul_2x_64_64_128 v21, x5, v0, v1
           mov x14, v0.d[0]
           mov x15, v0.d[1]
-          mul	x12, x5, x8
-          adds	x19, x19, x12
-          umulh	x12, x5, x8
-          mul	x13, x5, x9
-          adcs	x20, x20, x13
-          umulh	x13, x5, x9
+          mul   x12, x5, x8
+          adds  x19, x19, x12
+          umulh x12, x5, x8
+          mul   x13, x5, x9
+          adcs  x20, x20, x13
+          umulh x13, x5, x9
           adcs x21, x21, x14
           adcs x22, x22, x15
           mov x14, v1.d[0]
@@ -289,49 +289,49 @@ bignum_emontredc_8n_cdiff_base_outerloop:
 
           // Montgomery step 2
 
-          mul	x6, x20, x3
+          mul   x6, x20, x3
           // NEON: Calculate x6 * (x10, x11) that does two 64x64->128-bit multiplications.
           vmul_2x_64_64_128 v21, x6, v21, v1
           mov   x14, v21.d[0]
           mov   x15, v21.d[1]
-          mul	x12, x6, x8
-          adds	x20, x20, x12
-          umulh	x12, x6, x8
-          mul	x13, x6, x9
-          adcs	x21, x21, x13
-          umulh	x13, x6, x9
+          mul   x12, x6, x8
+          adds  x20, x20, x12
+          umulh x12, x6, x8
+          mul   x13, x6, x9
+          adcs  x21, x21, x13
+          umulh x13, x6, x9
           adcs  x22, x22, x14
           adcs  x23, x23, x15
           mov   x14, v1.d[0]
           mov   x15, v1.d[1]
-          adc	x24, xzr, xzr
-          adds	x21, x21, x12
-          mul	x7, x21, x3
-          adcs	x22, x22, x13
-          adcs	x23, x23, x14
-          adc	x24, x24, x15
+          adc   x24, xzr, xzr
+          adds  x21, x21, x12
+          mul   x7, x21, x3
+          adcs  x22, x22, x13
+          adcs  x23, x23, x14
+          adc   x24, x24, x15
 
           stph x6, x7, x1, #16, t1
 
           // Montgomery step 3
 
-          mul	x12, x7, x8
-          mul	x13, x7, x9
-          mul	x14, x7, x10
-          mul	x15, x7, x11
-          adds	x21, x21, x12
-          umulh	x12, x7, x8
-          adcs	x22, x22, x13
-          umulh	x13, x7, x9
-          adcs	x23, x23, x14
-          umulh	x14, x7, x10
-          adcs	x24, x24, x15
-          umulh	x15, x7, x11
-          adc	x25, xzr, xzr
-          adds	x12, x22, x12
-          adcs	x13, x23, x13
-          adcs	x14, x24, x14
-          adc	x15, x25, x15
+          mul   x12, x7, x8
+          mul   x13, x7, x9
+          mul   x14, x7, x10
+          mul   x15, x7, x11
+          adds  x21, x21, x12
+          umulh x12, x7, x8
+          adcs  x22, x22, x13
+          umulh x13, x7, x9
+          adcs  x23, x23, x14
+          umulh x14, x7, x10
+          adcs  x24, x24, x15
+          umulh x15, x7, x11
+          adc   x25, xzr, xzr
+          adds  x12, x22, x12
+          adcs  x13, x23, x13
+          adcs  x14, x24, x14
+          adc   x15, x25, x15
 
           lsr count, x0, #5