[XEN PATCH 0/2] xen: deviate asm-only definitions for Rule 8.4

[XEN PATCH 0/2] xen: deviate asm-only definitions for Rule 8.4

[Nicola Vetrini]

As stated in 'docs/misra/rules.rst' the community decided to deviate from Rule 8.4
whereby the definitions concern entities that are only used in asm modules.
The chosen deviation mechanism is that of textual deviations, through the use of
/* SAF-n-safe */ comments.

Deviating variables needs more care, and is therefore postponed to another patch.

Nicola Vetrini (2):
  xen: apply deviation for Rule 8.4 (asm-only definitions)
  automation: execute SAF translation before the analysis with ECLAIR

 automation/eclair_analysis/prepare.sh | 3 +++
 docs/misra/safe.json                  | 8 ++++++++
 xen/arch/arm/cpuerrata.c              | 1 +
 xen/arch/arm/setup.c                  | 1 +
 xen/arch/arm/smpboot.c                | 1 +
 xen/arch/arm/traps.c                  | 7 +++++++
 xen/arch/x86/boot/cmdline.c           | 1 +
 xen/arch/x86/boot/reloc.c             | 1 +
 xen/arch/x86/extable.c                | 4 ++--
 xen/arch/x86/mm.c                     | 1 +
 xen/arch/x86/setup.c                  | 2 ++
 xen/arch/x86/traps.c                  | 9 +++++++++
 xen/common/efi/boot.c                 | 5 +++--
 13 files changed, 40 insertions(+), 4 deletions(-)

--
2.34.1

[XEN PATCH 1/2] xen: apply deviation for Rule 8.4 (asm-only definitions)

[Nicola Vetrini]

As stated in 'docs/misra/rules.rst' the functions that are used only by
asm modules do not need to conform to MISRA C:2012 Rule 8.4.
The deviations are carried out with a SAF comment.

Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
---
Where the identifier for a function definition is on the next line w.r.t. the
return type, they have been put on the same line (e.g. efi_start) to avoid
stylistically questionable constructs, such as

int
/* SAF-1-safe */
func(void) {
	...
}

This change is motivated by a shortcoming in the automatic translation of SAF
comments into ECLAIR-specific ones; the resulting comment deviates only the
single line following it, rather than the whole declarator. ECLAIR comments do
support deviating more than one line, and an extension to the conversion script
is already being discussed.
---
 docs/misra/safe.json        | 8 ++++++++
 xen/arch/arm/cpuerrata.c    | 1 +
 xen/arch/arm/setup.c        | 1 +
 xen/arch/arm/smpboot.c      | 1 +
 xen/arch/arm/traps.c        | 7 +++++++
 xen/arch/x86/boot/cmdline.c | 1 +
 xen/arch/x86/boot/reloc.c   | 1 +
 xen/arch/x86/extable.c      | 4 ++--
 xen/arch/x86/mm.c           | 1 +
 xen/arch/x86/setup.c        | 2 ++
 xen/arch/x86/traps.c        | 9 +++++++++
 xen/common/efi/boot.c       | 5 +++--
 12 files changed, 37 insertions(+), 4 deletions(-)

diff --git a/docs/misra/safe.json b/docs/misra/safe.json
index e3c8a1d8eb36..39c5c056c7d4 100644
--- a/docs/misra/safe.json
+++ b/docs/misra/safe.json
@@ -12,6 +12,14 @@
         },
         {
             "id": "SAF-1-safe",
+            "analyser": {
+                "eclair": "MC3R1.R8.4"
+            },
+            "name": "Rule 8.4: asm-only definition",
+            "text": "Functions and variables used only by asm modules do not need to have a visible declaration prior to their definition."
+        },
+        {
+            "id": "SAF-2-safe",
             "analyser": {},
             "name": "Sentinel",
             "text": "Next ID to be used"
diff --git a/xen/arch/arm/cpuerrata.c b/xen/arch/arm/cpuerrata.c
index fcf32892a7ef..9137958fb682 100644
--- a/xen/arch/arm/cpuerrata.c
+++ b/xen/arch/arm/cpuerrata.c
@@ -370,6 +370,7 @@ custom_param("spec-ctrl", parse_spec_ctrl);

 /* Arm64 only for now as for Arm32 the workaround is currently handled in C. */
 #ifdef CONFIG_ARM_64
+/* SAF-1-safe */
 void __init arm_enable_wa2_handling(const struct alt_instr *alt,
                                     const uint32_t *origptr,
                                     uint32_t *updptr, int nr_inst)
diff --git a/xen/arch/arm/setup.c b/xen/arch/arm/setup.c
index 44ccea03ca14..db748839d383 100644
--- a/xen/arch/arm/setup.c
+++ b/xen/arch/arm/setup.c
@@ -1077,6 +1077,7 @@ static bool __init is_dom0less_mode(void)
 size_t __read_mostly dcache_line_bytes;

 /* C entry point for boot CPU */
+/* SAF-1-safe */
 void __init start_xen(unsigned long boot_phys_offset,
                       unsigned long fdt_paddr)
 {
diff --git a/xen/arch/arm/smpboot.c b/xen/arch/arm/smpboot.c
index e107b86b7b44..6efd17eb3500 100644
--- a/xen/arch/arm/smpboot.c
+++ b/xen/arch/arm/smpboot.c
@@ -302,6 +302,7 @@ smp_prepare_cpus(void)
 }

 /* Boot the current CPU */
+/* SAF-1-safe */
 void start_secondary(void)
 {
     unsigned int cpuid = init_data.cpuid;
diff --git a/xen/arch/arm/traps.c b/xen/arch/arm/traps.c
index 46c9a4031b30..ce89f16404d9 100644
--- a/xen/arch/arm/traps.c
+++ b/xen/arch/arm/traps.c
@@ -161,6 +161,7 @@ void init_traps(void)
     isb();
 }

+/* SAF-1-safe */
 void __div0(void)
 {
     printk("Division by zero in hypervisor.\n");
@@ -1954,6 +1955,7 @@ static inline bool needs_ssbd_flip(struct vcpu *v)
  * Actions that needs to be done after entering the hypervisor from the
  * guest and before the interrupts are unmasked.
  */
+/* SAF-1-safe */
 void enter_hypervisor_from_guest_preirq(void)
 {
     struct vcpu *v = current;
@@ -1968,6 +1970,7 @@ void enter_hypervisor_from_guest_preirq(void)
  * guest and before we handle any request. Depending on the exception trap,
  * this may be called with interrupts unmasked.
  */
+/* SAF-1-safe */
 void enter_hypervisor_from_guest(void)
 {
     struct vcpu *v = current;
@@ -1996,6 +1999,7 @@ void enter_hypervisor_from_guest(void)
     vgic_sync_from_lrs(v);
 }

+/* SAF-1-safe */
 void do_trap_guest_sync(struct cpu_user_regs *regs)
 {
     const union hsr hsr = { .bits = regs->hsr };
@@ -2191,11 +2195,13 @@ void do_trap_guest_serror(struct cpu_user_regs *regs)
     __do_trap_serror(regs, true);
 }

+/* SAF-1-safe */
 void do_trap_irq(struct cpu_user_regs *regs)
 {
     gic_interrupt(regs, 0);
 }

+/* SAF-1-safe */
 void do_trap_fiq(struct cpu_user_regs *regs)
 {
     gic_interrupt(regs, 1);
@@ -2269,6 +2275,7 @@ static bool check_for_vcpu_work(void)
  *
  * The function will return with IRQ masked.
  */
+/* SAF-1-safe */
 void leave_hypervisor_to_guest(void)
 {
     local_irq_disable();
diff --git a/xen/arch/x86/boot/cmdline.c b/xen/arch/x86/boot/cmdline.c
index 74997703b31e..f9eee756aaed 100644
--- a/xen/arch/x86/boot/cmdline.c
+++ b/xen/arch/x86/boot/cmdline.c
@@ -340,6 +340,7 @@ static void vga_parse(const char *cmdline, early_boot_opts_t *ebo)
 }
 #endif

+/* SAF-1-safe */
 void __stdcall cmdline_parse_early(const char *cmdline, early_boot_opts_t *ebo)
 {
     if ( !cmdline )
diff --git a/xen/arch/x86/boot/reloc.c b/xen/arch/x86/boot/reloc.c
index e22bb974bf20..609b02cb73dc 100644
--- a/xen/arch/x86/boot/reloc.c
+++ b/xen/arch/x86/boot/reloc.c
@@ -347,6 +347,7 @@ static multiboot_info_t *mbi2_reloc(uint32_t mbi_in, uint32_t video_out)
     return mbi_out;
 }

+/* SAF-1-safe */
 void *__stdcall reloc(uint32_t magic, uint32_t in, uint32_t trampoline,
                       uint32_t video_info)
 {
diff --git a/xen/arch/x86/extable.c b/xen/arch/x86/extable.c
index c3771c2e3937..74b14246e9d8 100644
--- a/xen/arch/x86/extable.c
+++ b/xen/arch/x86/extable.c
@@ -194,8 +194,8 @@ static int __init cf_check stub_selftest(void)
 __initcall(stub_selftest);
 #endif

-unsigned long
-search_pre_exception_table(struct cpu_user_regs *regs)
+/* SAF-1-safe */
+unsigned long search_pre_exception_table(struct cpu_user_regs *regs)
 {
     unsigned long addr = regs->rip;
     unsigned long fixup = search_one_extable(
diff --git a/xen/arch/x86/mm.c b/xen/arch/x86/mm.c
index 28fdf820ef3b..828786932021 100644
--- a/xen/arch/x86/mm.c
+++ b/xen/arch/x86/mm.c
@@ -143,6 +143,7 @@
 /* Mapping of the fixmap space needed early. */
 l1_pgentry_t __section(".bss.page_aligned") __aligned(PAGE_SIZE)
     l1_fixmap[L1_PAGETABLE_ENTRIES];
+/* SAF-1-safe */
 l1_pgentry_t __section(".bss.page_aligned") __aligned(PAGE_SIZE)
     l1_fixmap_x[L1_PAGETABLE_ENTRIES];

diff --git a/xen/arch/x86/setup.c b/xen/arch/x86/setup.c
index 3358d9a0ff63..7e2979f419af 100644
--- a/xen/arch/x86/setup.c
+++ b/xen/arch/x86/setup.c
@@ -153,6 +153,7 @@ char __section(".init.bss.stack_aligned") __aligned(STACK_SIZE)
 void *stack_start = cpu0_stack + STACK_SIZE - sizeof(struct cpu_info);

 /* Used by the boot asm to stash the relocated multiboot info pointer. */
+/* SAF-1-safe */
 unsigned int __initdata multiboot_ptr;

 struct cpuinfo_x86 __read_mostly boot_cpu_data = { 0, 0, 0, 0, -1 };
@@ -968,6 +969,7 @@ static struct domain *__init create_dom0(const module_t *image,
 /* How much of the directmap is prebuilt at compile time. */
 #define PREBUILT_MAP_LIMIT (1 << L2_PAGETABLE_SHIFT)

+/* SAF-1-safe */
 void __init noreturn __start_xen(unsigned long mbi_p)
 {
     const char *memmap_type = NULL;
diff --git a/xen/arch/x86/traps.c b/xen/arch/x86/traps.c
index a898e1f2d731..dead728ce329 100644
--- a/xen/arch/x86/traps.c
+++ b/xen/arch/x86/traps.c
@@ -833,6 +833,7 @@ void fatal_trap(const struct cpu_user_regs *regs, bool show_remote)
           (regs->eflags & X86_EFLAGS_IF) ? "" : " IN INTERRUPT CONTEXT");
 }

+/* SAF-1-safe */
 void do_unhandled_trap(struct cpu_user_regs *regs)
 {
     unsigned int trapnr = regs->entry_vector;
@@ -920,6 +921,7 @@ static bool extable_fixup(struct cpu_user_regs *regs, bool print)
     return true;
 }

+/* SAF-1-safe */
 void do_trap(struct cpu_user_regs *regs)
 {
     unsigned int trapnr = regs->entry_vector;
@@ -1152,6 +1154,7 @@ void cpuid_hypervisor_leaves(const struct vcpu *v, uint32_t leaf,
     }
 }

+/* SAF-1-safe */
 void do_invalid_op(struct cpu_user_regs *regs)
 {
     u8 bug_insn[2];
@@ -1197,6 +1200,7 @@ void do_invalid_op(struct cpu_user_regs *regs)
     panic("FATAL TRAP: vector = %d (invalid opcode)\n", X86_EXC_UD);
 }

+/* SAF-1-safe */
 void do_int3(struct cpu_user_regs *regs)
 {
     struct vcpu *curr = current;
@@ -1564,6 +1568,7 @@ static int fixup_page_fault(unsigned long addr, struct cpu_user_regs *regs)
     return 0;
 }

+/* SAF-1-safe */
 void do_page_fault(struct cpu_user_regs *regs)
 {
     unsigned long addr;
@@ -1641,6 +1646,7 @@ void do_page_fault(struct cpu_user_regs *regs)
  * during early boot (an issue was seen once, but was most likely a hardware
  * problem).
  */
+/* SAF-1-safe */
 void __init do_early_page_fault(struct cpu_user_regs *regs)
 {
     static unsigned int __initdata stuck;
@@ -1841,6 +1847,7 @@ void trigger_nmi_continuation(void)
     apic_wait_icr_idle();
 }

+/* SAF-1-safe */
 void do_device_not_available(struct cpu_user_regs *regs)
 {
 #ifdef CONFIG_PV
@@ -1877,6 +1884,7 @@ void do_device_not_available(struct cpu_user_regs *regs)
 #endif
 }

+/* SAF-1-safe */
 void do_debug(struct cpu_user_regs *regs)
 {
     unsigned long dr6;
@@ -2002,6 +2010,7 @@ void do_debug(struct cpu_user_regs *regs)
     pv_inject_hw_exception(X86_EXC_DB, X86_EVENT_NO_EC);
 }

+/* SAF-1-safe */
 void do_entry_CP(struct cpu_user_regs *regs)
 {
     static const char errors[][10] = {
diff --git a/xen/common/efi/boot.c b/xen/common/efi/boot.c
index 79a654af69b0..99cb033e2a6f 100644
--- a/xen/common/efi/boot.c
+++ b/xen/common/efi/boot.c
@@ -1253,8 +1253,9 @@ static void __init efi_exit_boot(EFI_HANDLE ImageHandle, EFI_SYSTEM_TABLE *Syste
     efi_fw_vendor = (void *)efi_fw_vendor + DIRECTMAP_VIRT_START;
 }

-void EFIAPI __init noreturn
-efi_start(EFI_HANDLE ImageHandle, EFI_SYSTEM_TABLE *SystemTable)
+/* SAF-1-safe */
+void EFIAPI __init noreturn efi_start(EFI_HANDLE ImageHandle,
+                                      EFI_SYSTEM_TABLE *SystemTable)
 {
     static EFI_GUID __initdata loaded_image_guid = LOADED_IMAGE_PROTOCOL;
     static EFI_GUID __initdata shim_lock_guid = SHIM_LOCK_PROTOCOL_GUID;
--
2.34.1

Re: [XEN PATCH 1/2] xen: apply deviation for Rule 8.4 (asm-only definitions)

[Jan Beulich]

On 01.09.2023 18:34, Nicola Vetrini wrote:
> As stated in 'docs/misra/rules.rst' the functions that are used only by
> asm modules do not need to conform to MISRA C:2012 Rule 8.4.
> The deviations are carried out with a SAF comment.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
> ---
> Where the identifier for a function definition is on the next line w.r.t. the
> return type, they have been put on the same line (e.g. efi_start) to avoid
> stylistically questionable constructs, such as
> 
> int
> /* SAF-1-safe */
> func(void) {
> 	...
> }

And

/* SAF-1-safe */
int
func(void) {

is not an option?

Further in the cover letter you say "Deviating variables needs more care, and
is therefore postponed to another patch", yet then here you annotate a couple
of variables as well. Could you clarify what the criteria are for "needs more
care"?

Jan

Re: [XEN PATCH 1/2] xen: apply deviation for Rule 8.4 (asm-only definitions)

[Nicola Vetrini]

On 04/09/2023 09:02, Jan Beulich wrote:
> On 01.09.2023 18:34, Nicola Vetrini wrote:
>> As stated in 'docs/misra/rules.rst' the functions that are used only 
>> by
>> asm modules do not need to conform to MISRA C:2012 Rule 8.4.
>> The deviations are carried out with a SAF comment.
>> 
>> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
>> ---
>> Where the identifier for a function definition is on the next line 
>> w.r.t. the
>> return type, they have been put on the same line (e.g. efi_start) to 
>> avoid
>> stylistically questionable constructs, such as
>> 
>> int
>> /* SAF-1-safe */
>> func(void) {
>> 	...
>> }
> 
> And
> 
> /* SAF-1-safe */
> int
> func(void) {
> 
> is not an option?
> 

Not at the moment, as it would deviate the line with the return type and 
not the one below,
and this is not configurable in the scripts under 
xen/scripts/xen-analysis:

/* SAF-1-safe */ -> /* -E> safe ... 1 */
int                 int
func(void)          func(void)

As I said, this can perhaps be solved by allowing markers to specify 
either a row count, such as

/* SAF-1-safe 2 */ -> /* -E> safe ... 2 */
int                   int
func(void)            func(void)

or count the line span of the whole function declarator in the python 
script and translating
/* SAF-1-safe */ -> /* -E> safe ... 2 */.

> Further in the cover letter you say "Deviating variables needs more 
> care, and
> is therefore postponed to another patch", yet then here you annotate a 
> couple
> of variables as well. Could you clarify what the criteria are for 
> "needs more
> care"?
> 

I see. I did not intend for those changes to end up in this patch, 
although those two are
clearly only used by asm code and therefore are excepted.
Most of the variables I left out are also used by C code, therefore they 
may be eligible for
a declaration, but where to put this declaration requires a careful 
examination in my opinion.
They are not too many, tough.

-- 
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)

Re: [XEN PATCH 1/2] xen: apply deviation for Rule 8.4 (asm-only definitions)

[Jan Beulich]

On 04.09.2023 09:19, Nicola Vetrini wrote:
> On 04/09/2023 09:02, Jan Beulich wrote:
>> Further in the cover letter you say "Deviating variables needs more 
>> care, and
>> is therefore postponed to another patch", yet then here you annotate a 
>> couple
>> of variables as well. Could you clarify what the criteria are for 
>> "needs more
>> care"?
> 
> I see. I did not intend for those changes to end up in this patch, 
> although those two are
> clearly only used by asm code and therefore are excepted.
> Most of the variables I left out are also used by C code, therefore they 
> may be eligible for
> a declaration, but where to put this declaration requires a careful 
> examination in my opinion.
> They are not too many, tough.

Anything also used by C code (and not in the same CU) clearly wants a
declaration.

Jan

Re: [XEN PATCH 1/2] xen: apply deviation for Rule 8.4 (asm-only definitions)

[Nicola Vetrini]

On 04/09/2023 10:09, Jan Beulich wrote:
> On 04.09.2023 09:19, Nicola Vetrini wrote:
>> On 04/09/2023 09:02, Jan Beulich wrote:
>>> Further in the cover letter you say "Deviating variables needs more
>>> care, and
>>> is therefore postponed to another patch", yet then here you annotate 
>>> a
>>> couple
>>> of variables as well. Could you clarify what the criteria are for
>>> "needs more
>>> care"?
>> 
>> I see. I did not intend for those changes to end up in this patch,
>> although those two are
>> clearly only used by asm code and therefore are excepted.
>> Most of the variables I left out are also used by C code, therefore 
>> they
>> may be eligible for
>> a declaration, but where to put this declaration requires a careful
>> examination in my opinion.
>> They are not too many, tough.
> 
> Anything also used by C code (and not in the same CU) clearly wants a
> declaration.
> 
> Jan

I think that a declaration (in an header) is a good idea also when a 
symbol is defined in a translation unit
and it used both by C code in that TU and asm modules. This also allows 
C code that uses
that symbol to be moved around freely without other changes.

-- 
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)

Re: [XEN PATCH 1/2] xen: apply deviation for Rule 8.4 (asm-only definitions)

[Stefano Stabellini]

On Mon, 4 Sep 2023, Nicola Vetrini wrote:
> > Further in the cover letter you say "Deviating variables needs more care,
> > and
> > is therefore postponed to another patch", yet then here you annotate a
> > couple
> > of variables as well. Could you clarify what the criteria are for "needs
> > more
> > care"?
> > 
> 
> I see. I did not intend for those changes to end up in this patch, although
> those two are
> clearly only used by asm code and therefore are excepted.

I reviewed the patch checking that every function and variable is
actually only called/used from asm. Everything checks out, so:

Reviewed-by: Stefano Stabellini <sstabellini@kernel.org>

However, I think we should drop the change below (could be done on
commit) because it doesn't make sense to add SAF-1-safe for l1_fixmap_x
but not for l1_fixmap.  l1_fixmap has a declaration in
xen/arch/x86/include/asm/page.h but it is not actually used.

diff --git a/xen/arch/x86/mm.c b/xen/arch/x86/mm.c
index 28fdf820ef3b..828786932021 100644
--- a/xen/arch/x86/mm.c
+++ b/xen/arch/x86/mm.c
@@ -143,6 +143,7 @@
 /* Mapping of the fixmap space needed early. */
 l1_pgentry_t __section(".bss.page_aligned") __aligned(PAGE_SIZE)
     l1_fixmap[L1_PAGETABLE_ENTRIES];
+/* SAF-1-safe */
 l1_pgentry_t __section(".bss.page_aligned") __aligned(PAGE_SIZE)
     l1_fixmap_x[L1_PAGETABLE_ENTRIES];

[XEN PATCH 2/2] automation: execute SAF translation before the analysis with ECLAIR

[Nicola Vetrini]

This allows local MISRA deviation comments to be translated into
the format recognized by ECLAIR.

Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
---
 automation/eclair_analysis/prepare.sh | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/automation/eclair_analysis/prepare.sh b/automation/eclair_analysis/prepare.sh
index 275a1a3f517c..0cac5eba00ae 100755
--- a/automation/eclair_analysis/prepare.sh
+++ b/automation/eclair_analysis/prepare.sh
@@ -38,5 +38,8 @@ fi
     cd xen
     cp "${CONFIG_FILE}" .config
     make clean
+    find . -type f -name "*.safparse" -print -delete
     make -f ${script_dir}/Makefile.prepare prepare
+    # Translate the /* SAF-n-safe */ comments into ECLAIR CBTs
+    scripts/xen-analysis.py --run-eclair --no-build --no-clean
 )
-- 
2.34.1

Re: [XEN PATCH 2/2] automation: execute SAF translation before the analysis with ECLAIR

[Stefano Stabellini]

On Fri, 1 Sep 2023, Nicola Vetrini wrote:
> This allows local MISRA deviation comments to be translated into
> the format recognized by ECLAIR.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>

Acked-by: Stefano Stabellini <sstabellini@kernel.org>


> ---
>  automation/eclair_analysis/prepare.sh | 3 +++
>  1 file changed, 3 insertions(+)
> 
> diff --git a/automation/eclair_analysis/prepare.sh b/automation/eclair_analysis/prepare.sh
> index 275a1a3f517c..0cac5eba00ae 100755
> --- a/automation/eclair_analysis/prepare.sh
> +++ b/automation/eclair_analysis/prepare.sh
> @@ -38,5 +38,8 @@ fi
>      cd xen
>      cp "${CONFIG_FILE}" .config
>      make clean
> +    find . -type f -name "*.safparse" -print -delete
>      make -f ${script_dir}/Makefile.prepare prepare
> +    # Translate the /* SAF-n-safe */ comments into ECLAIR CBTs
> +    scripts/xen-analysis.py --run-eclair --no-build --no-clean
>  )
> -- 
> 2.34.1
>