1. Patchew
  2. Xen
  3. View series

[XEN PATCH v2] automation/eclair_analysis: deviate linker symbols for Rule 18.2

Nicola Vetrini posted 1 patch 2 months, 2 weeks ago
Patches applied successfully (tree, apply log)
git fetch https://gitlab.com/xen-project/patchew/xen tags/patchew/e3a9c3268685562ae557248d6e76376579d99715.1725714006.git.nicola.vetrini@bugseng.com
automation/eclair_analysis/ECLAIR/analyze.sh  |  6 ----
.../eclair_analysis/ECLAIR/deviations.ecl     | 11 +++++++
.../ECLAIR/generate-linker-symbols.sh         | 31 +++++++++++++++++++
.../eclair_analysis/ECLAIR/generate_ecl.sh    |  3 ++
automation/eclair_analysis/prepare.sh         |  6 +++-
automation/scripts/eclair                     |  3 ++
docs/misra/deviations.rst                     | 10 ++++++
7 files changed, 63 insertions(+), 7 deletions(-)
create mode 100755 automation/eclair_analysis/ECLAIR/generate-linker-symbols.sh
[XEN PATCH v2] automation/eclair_analysis: deviate linker symbols for Rule 18.2
Posted by Nicola Vetrini 2 months, 2 weeks ago 
MISRA C Rule 18.2 states: "Subtraction between pointers shall
only be applied to pointers that address elements of the same array".

Subtractions between pointer where at least one symbol is a
symbol defined by the linker are safe and thus deviated, because
the compiler cannot exploit the undefined behaviour that would
arise from violating the rules in this case.

To create an ECLAIR configuration that contains the list of
linker-defined symbols, the script "linker-symbols.sh" is used
after a build of xen (without static analysis) is performed.
The generated file "linker_symbols.ecl" is then used as part of the
static analysis configuration.

Additional changes to the ECLAIR integration are:
- perform a build of xen without static analysis during prepare.sh
- run the scripts to generated ECL configuration during the prepare.sh,
  rather than analysis.sh
- export ECLAIR_PROJECT_ROOT earlier, to allow such generation

Additionally, the macro page_to_mfn performs a subtraction that is safe,
so its uses are deviated.

No functional changes.

Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
Acked-by: Stefano Stabellini <sstabellini@kernel.org>
---
Changes in v2:
- renamed new file generate_linker_symbols.sh to use dashes instead of
  underscores as separators

Macro page_to_pdx is also the cause of some caution reports:
perhaps that should be deviated as well, since its definition is very
similar to page_to_mfn.

Relevant CI runs:

- arm64: https://saas.eclairit.com:3787/fs/var/local/eclair/xen-project.ecdf/xen-project/people/bugseng/xen/ECLAIR_normal/MC3R1.R18.2/ARM64/7769096695/PROJECT.ecd;/by_service/MC3R1.R18.2.html

- x86_64: https://saas.eclairit.com:3787/fs/var/local/eclair/xen-project.ecdf/xen-project/people/bugseng/xen/ECLAIR_normal/MC3R1.R18.2/X86_64/7769096694/PROJECT.ecd;/by_service/MC3R1.R18.2.html
- x86_64 (without page_to_pdx reports): https://saas.eclairit.com:3787/fs/var/local/eclair/xen-project.ecdf/xen-project/people/bugseng/xen/ECLAIR_normal/MC3R1.R18.2/X86_64/7769096694/PROJECT.ecd;/by_service/MC3R1.R18.2.html#{"select":true,"selection":{"hiddenAreaKinds":[],"hiddenSubareaKinds":[],"show":false,"selector":{"enabled":true,"negated":false,"kind":0,"domain":"message","inputs":[{"enabled":true,"text":"^.*expanded from macro `page_to_pdx'"}]}}}
---
 automation/eclair_analysis/ECLAIR/analyze.sh  |  6 ----
 .../eclair_analysis/ECLAIR/deviations.ecl     | 11 +++++++
 .../ECLAIR/generate-linker-symbols.sh         | 31 +++++++++++++++++++
 .../eclair_analysis/ECLAIR/generate_ecl.sh    |  3 ++
 automation/eclair_analysis/prepare.sh         |  6 +++-
 automation/scripts/eclair                     |  3 ++
 docs/misra/deviations.rst                     | 10 ++++++
 7 files changed, 63 insertions(+), 7 deletions(-)
 create mode 100755 automation/eclair_analysis/ECLAIR/generate-linker-symbols.sh

diff --git a/automation/eclair_analysis/ECLAIR/analyze.sh b/automation/eclair_analysis/ECLAIR/analyze.sh
index e96456c3c18d..1dc63c1bc2d0 100755
--- a/automation/eclair_analysis/ECLAIR/analyze.sh
+++ b/automation/eclair_analysis/ECLAIR/analyze.sh
@@ -73,17 +73,11 @@ export ECLAIR_WORKSPACE="${ECLAIR_DATA_DIR}/eclair_workspace"
 
 # Identifies the particular build of the project.
 export ECLAIR_PROJECT_NAME="XEN_${VARIANT}-${SET}"
-# All paths mentioned in ECLAIR reports that are below this directory
-# will be presented as relative to ECLAIR_PROJECT_ROOT.
-export ECLAIR_PROJECT_ROOT="${PWD}"
 
 # Erase and recreate the output directory and the data directory.
 rm -rf "${ECLAIR_OUTPUT_DIR:?}/*"
 mkdir -p "${ECLAIR_DATA_DIR}"
 
-# Generate additional configuration files 
-"${SCRIPT_DIR}/generate_ecl.sh"
-
 # Perform the build (from scratch) in an ECLAIR environment.
 "${ECLAIR_BIN_DIR}eclair_env" \
     "-config_file='${SCRIPT_DIR}/analysis.ecl'" \
diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl b/automation/eclair_analysis/ECLAIR/deviations.ecl
index 9051f4160282..a56805a993cd 100644
--- a/automation/eclair_analysis/ECLAIR/deviations.ecl
+++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
@@ -533,6 +533,17 @@ safe."
 # Series 18.
 #
 
+-doc_begin="Subtractions between pointers involving at least one of the linker symbols specified by the regex below
+are guaranteed not to be exploited by a compiler that relies on the absence of
+C99 Undefined Behaviour 45: Pointers that do not point into, or just beyond, the same array object are subtracted (6.5.6)."
+-eval_file=linker_symbols.ecl
+-config=MC3R1.R18.2,reports+={safe, "any_area(stmt(operator(sub)&&child(lhs||rhs, skip(__non_syntactic_paren_stmts, ref(linker_symbols)))))"}
+-doc_end
+
+-doc_begin="The following macro performs a subtraction between pointers to obtain the mfn, but does not lead to undefined behaviour."
+-config=MC3R1.R18.2,reports+={safe, "any_area(any_loc(any_exp(macro(^page_to_mfn$))))"}
+-doc_end
+
 -doc_begin="Flexible array members are deliberately used and XEN developers are aware of the dangers related to them:
 unexpected result when the structure is given as argument to a sizeof() operator and the truncation in assignment between structures."
 -config=MC3R1.R18.7,reports+={deliberate, "any()"}
diff --git a/automation/eclair_analysis/ECLAIR/generate-linker-symbols.sh b/automation/eclair_analysis/ECLAIR/generate-linker-symbols.sh
new file mode 100755
index 000000000000..19943ba98d46
--- /dev/null
+++ b/automation/eclair_analysis/ECLAIR/generate-linker-symbols.sh
@@ -0,0 +1,31 @@
+#!/bin/bash
+
+set -e
+
+script_name="$(basename "$0")"
+script_dir="$(
+  cd "$(dirname "$0")"
+  echo "${PWD}"
+)"
+
+fatal() {
+  echo "${script_name}: $*" >&2
+  exit 1
+}
+
+arch=""
+if [ "${XEN_TARGET_ARCH}" == "x86_64" ]; then
+  arch=x86
+elif [ "${XEN_TARGET_ARCH}" == "arm64" ]; then
+  arch=arm
+else
+  fatal "Unknown configuration: $1"
+fi
+
+outfile=${script_dir}/linker_symbols.ecl
+
+(
+  echo -n "-decl_selector+={linker_symbols, \"^(" >"${outfile}"
+  "${script_dir}/../linker-symbols.sh" "${arch}" | sort -u | tr '\n' '|' | sed '$ s/|//' >>"${outfile}"
+  echo -n ")$\"}" >>"${outfile}"
+)
diff --git a/automation/eclair_analysis/ECLAIR/generate_ecl.sh b/automation/eclair_analysis/ECLAIR/generate_ecl.sh
index 66766b23abb7..b955783904a8 100755
--- a/automation/eclair_analysis/ECLAIR/generate_ecl.sh
+++ b/automation/eclair_analysis/ECLAIR/generate_ecl.sh
@@ -17,3 +17,6 @@ accepted_rst="${ECLAIR_PROJECT_ROOT}/docs/misra/rules.rst"
 
 # Generate accepted guidelines
 "${script_dir}/accepted_guidelines.sh" "${accepted_rst}"
+
+# Generate the list of linker-defined symbols (must be run after a Xen build)
+"${script_dir}/generate-linker-symbols.sh"
diff --git a/automation/eclair_analysis/prepare.sh b/automation/eclair_analysis/prepare.sh
index 47b2a2f32a84..3a646414a392 100755
--- a/automation/eclair_analysis/prepare.sh
+++ b/automation/eclair_analysis/prepare.sh
@@ -39,10 +39,14 @@ fi
     cp "${CONFIG_FILE}" xen/.config
     make clean
     find . -type f -name "*.safparse" -print -delete
+    "${script_dir}/build.sh" "$1"
+    # Generate additional configuration files
+    "${script_dir}/ECLAIR/generate_ecl.sh"
+    make clean
     cd xen
     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
     # Translate function-properties.json into ECLAIR properties
-    python3 ${script_dir}/propertyparser.py
+    python3 "${script_dir}/propertyparser.py"
 )
diff --git a/automation/scripts/eclair b/automation/scripts/eclair
index 3ec760bab8b3..0a2353c20a92 100755
--- a/automation/scripts/eclair
+++ b/automation/scripts/eclair
@@ -3,6 +3,9 @@
 ECLAIR_ANALYSIS_DIR=automation/eclair_analysis
 ECLAIR_DIR="${ECLAIR_ANALYSIS_DIR}/ECLAIR"
 ECLAIR_OUTPUT_DIR=$(realpath "${ECLAIR_OUTPUT_DIR}")
+# All paths mentioned in ECLAIR reports that are below this directory
+# will be presented as relative to ECLAIR_PROJECT_ROOT.
+export ECLAIR_PROJECT_ROOT="${PWD}"
 
 "${ECLAIR_ANALYSIS_DIR}/prepare.sh" "${VARIANT}"
 
diff --git a/docs/misra/deviations.rst b/docs/misra/deviations.rst
index b66c271c4e7c..39cd1de1e5b2 100644
--- a/docs/misra/deviations.rst
+++ b/docs/misra/deviations.rst
@@ -501,6 +501,16 @@ Deviations related to MISRA C:2012 Rules:
          - __builtin_memset()
          - cpumask_check()
 
+   * - R18.2
+     - Subtractions between pointers where at least one of the operand is a
+       pointer to a symbol defined by the linker are safe.
+     - Tagged as `safe` for ECLAIR.
+
+   * - R18.2
+     - Subtraction between pointers encapsulated by macro page_to_mfn
+       are safe.
+     - Tagged as `safe` for ECLAIR.
+
    * - R20.4
      - The override of the keyword \"inline\" in xen/compiler.h is present so
        that section contents checks pass when the compiler chooses not to
-- 
2.43.0
Re: [XEN PATCH v2] automation/eclair_analysis: deviate linker symbols for Rule 18.2
Posted by Jan Beulich 2 months, 2 weeks ago 
On 07.09.2024 15:03, Nicola Vetrini wrote:
> --- a/docs/misra/deviations.rst
> +++ b/docs/misra/deviations.rst
> @@ -501,6 +501,16 @@ Deviations related to MISRA C:2012 Rules:
>           - __builtin_memset()
>           - cpumask_check()
>  
> +   * - R18.2
> +     - Subtractions between pointers where at least one of the operand is a
> +       pointer to a symbol defined by the linker are safe.

Imo there should be "deemed" in there, as such subtractions aren't
necessarily safe. We've merely settled on considering the risk as
acceptable, iirc.

> +     - Tagged as `safe` for ECLAIR.
> +
> +   * - R18.2
> +     - Subtraction between pointers encapsulated by macro page_to_mfn
> +       are safe.
> +     - Tagged as `safe` for ECLAIR.

This one is a result of using frame_table[], aiui. Alternative approaches
were discussed before. Did that not lead anywhere, requiring a purely
textual / configurational deviation?

Jan
Re: [XEN PATCH v2] automation/eclair_analysis: deviate linker symbols for Rule 18.2
Posted by Stefano Stabellini 2 months, 2 weeks ago 
On Mon, 9 Sep 2024, Jan Beulich wrote:
> On 07.09.2024 15:03, Nicola Vetrini wrote:
> > --- a/docs/misra/deviations.rst
> > +++ b/docs/misra/deviations.rst
> > @@ -501,6 +501,16 @@ Deviations related to MISRA C:2012 Rules:
> >           - __builtin_memset()
> >           - cpumask_check()
> >  
> > +   * - R18.2
> > +     - Subtractions between pointers where at least one of the operand is a
> > +       pointer to a symbol defined by the linker are safe.
> 
> Imo there should be "deemed" in there, as such subtractions aren't
> necessarily safe. We've merely settled on considering the risk as
> acceptable, iirc.

I can add it on commit


> > +     - Tagged as `safe` for ECLAIR.
> > +
> > +   * - R18.2
> > +     - Subtraction between pointers encapsulated by macro page_to_mfn
> > +       are safe.
> > +     - Tagged as `safe` for ECLAIR.
> 
> This one is a result of using frame_table[], aiui. Alternative approaches
> were discussed before. Did that not lead anywhere, requiring a purely
> textual / configurational deviation?

During the last MISRA discussion we agree that this was an acceptable
approach. What else did you have in mind? In any case, keep in mind that
exploring options is a task in itself and we could use our efforts on
reducing the numbers of violations instead which I think is more useful.
Re: [XEN PATCH v2] automation/eclair_analysis: deviate linker symbols for Rule 18.2
Posted by Jan Beulich 2 months, 2 weeks ago 
On 10.09.2024 06:46, Stefano Stabellini wrote:
> On Mon, 9 Sep 2024, Jan Beulich wrote:
>> On 07.09.2024 15:03, Nicola Vetrini wrote:
>>> +   * - R18.2
>>> +     - Subtraction between pointers encapsulated by macro page_to_mfn
>>> +       are safe.
>>> +     - Tagged as `safe` for ECLAIR.
>>
>> This one is a result of using frame_table[], aiui. Alternative approaches
>> were discussed before. Did that not lead anywhere, requiring a purely
>> textual / configurational deviation?
> 
> During the last MISRA discussion we agree that this was an acceptable
> approach. What else did you have in mind?

One was to have the linker scripts provide the symbol. I think there were
one or two more, yet I - perhaps wrongly - haven't been taking notes ...

> In any case, keep in mind that
> exploring options is a task in itself and we could use our efforts on
> reducing the numbers of violations instead which I think is more useful.

Sure. Otoh quickest is not always best.

Jan
Re: [XEN PATCH v2] automation/eclair_analysis: deviate linker symbols for Rule 18.2
Posted by Nicola Vetrini 2 months, 1 week ago 
On 2024-09-10 08:26, Jan Beulich wrote:
> On 10.09.2024 06:46, Stefano Stabellini wrote:
>> On Mon, 9 Sep 2024, Jan Beulich wrote:
>>> On 07.09.2024 15:03, Nicola Vetrini wrote:
>>>> +   * - R18.2
>>>> +     - Subtraction between pointers encapsulated by macro 
>>>> page_to_mfn
>>>> +       are safe.
>>>> +     - Tagged as `safe` for ECLAIR.
>>> 
>>> This one is a result of using frame_table[], aiui. Alternative 
>>> approaches
>>> were discussed before. Did that not lead anywhere, requiring a purely
>>> textual / configurational deviation?
>> 
>> During the last MISRA discussion we agree that this was an acceptable
>> approach. What else did you have in mind?
> 
> One was to have the linker scripts provide the symbol. I think there 
> were
> one or two more, yet I - perhaps wrongly - haven't been taking notes 
> ...
> 

One thing I'm fairly sure has been suggested for symbols that were not 
linker-defined is the following mitigation:

gcc -fsanitize=address,pointer-subtract
ASAN_OPTIONS=detect_invalid_pointer_pairs=2 ./a.out

See GCC manual Section "3.12 Program Instrumentation Options"
https://gcc.gnu.org/onlinedocs/gcc-12.1.0/gcc.pdf


>> In any case, keep in mind that
>> exploring options is a task in itself and we could use our efforts on
>> reducing the numbers of violations instead which I think is more 
>> useful.
> 
> Sure. Otoh quickest is not always best.
> 


-- 
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)
Re: [XEN PATCH v2] automation/eclair_analysis: deviate linker symbols for Rule 18.2
Posted by Jan Beulich 2 months, 1 week ago 
On 10.09.2024 10:18, Nicola Vetrini wrote:
> On 2024-09-10 08:26, Jan Beulich wrote:
>> On 10.09.2024 06:46, Stefano Stabellini wrote:
>>> On Mon, 9 Sep 2024, Jan Beulich wrote:
>>>> On 07.09.2024 15:03, Nicola Vetrini wrote:
>>>>> +   * - R18.2
>>>>> +     - Subtraction between pointers encapsulated by macro 
>>>>> page_to_mfn
>>>>> +       are safe.
>>>>> +     - Tagged as `safe` for ECLAIR.
>>>>
>>>> This one is a result of using frame_table[], aiui. Alternative 
>>>> approaches
>>>> were discussed before. Did that not lead anywhere, requiring a purely
>>>> textual / configurational deviation?
>>>
>>> During the last MISRA discussion we agree that this was an acceptable
>>> approach. What else did you have in mind?
>>
>> One was to have the linker scripts provide the symbol. I think there 
>> were
>> one or two more, yet I - perhaps wrongly - haven't been taking notes 
>> ...
>>
> 
> One thing I'm fairly sure has been suggested for symbols that were not 
> linker-defined is the following mitigation:
> 
> gcc -fsanitize=address,pointer-subtract
> ASAN_OPTIONS=detect_invalid_pointer_pairs=2 ./a.out

ASAN in general was mentioned in the discussion, yet it didn't look like
anyone would be up to actually making ASAN usable with Xen. Iirc Andrew
estimated the effort to a man-year.

Jan
Re: [XEN PATCH v2] automation/eclair_analysis: deviate linker symbols for Rule 18.2
Posted by Stefano Stabellini 2 months, 1 week ago 
On Tue, 10 Sep 2024, Jan Beulich wrote:
> On 10.09.2024 10:18, Nicola Vetrini wrote:
> > On 2024-09-10 08:26, Jan Beulich wrote:
> >> On 10.09.2024 06:46, Stefano Stabellini wrote:
> >>> On Mon, 9 Sep 2024, Jan Beulich wrote:
> >>>> On 07.09.2024 15:03, Nicola Vetrini wrote:
> >>>>> +   * - R18.2
> >>>>> +     - Subtraction between pointers encapsulated by macro 
> >>>>> page_to_mfn
> >>>>> +       are safe.
> >>>>> +     - Tagged as `safe` for ECLAIR.
> >>>>
> >>>> This one is a result of using frame_table[], aiui. Alternative 
> >>>> approaches
> >>>> were discussed before. Did that not lead anywhere, requiring a purely
> >>>> textual / configurational deviation?
> >>>
> >>> During the last MISRA discussion we agree that this was an acceptable
> >>> approach. What else did you have in mind?
> >>
> >> One was to have the linker scripts provide the symbol. I think there 
> >> were
> >> one or two more, yet I - perhaps wrongly - haven't been taking notes 
> >> ...
> >>
> > 
> > One thing I'm fairly sure has been suggested for symbols that were not 
> > linker-defined is the following mitigation:
> > 
> > gcc -fsanitize=address,pointer-subtract
> > ASAN_OPTIONS=detect_invalid_pointer_pairs=2 ./a.out
> 
> ASAN in general was mentioned in the discussion, yet it didn't look like
> anyone would be up to actually making ASAN usable with Xen. Iirc Andrew
> estimated the effort to a man-year.

Given this, let's stay with the patch and deviation in the current form
Re: [XEN PATCH v2] automation/eclair_analysis: deviate linker symbols for Rule 18.2
Posted by Nicola Vetrini 2 months, 2 weeks ago 
On 2024-09-07 15:03, Nicola Vetrini wrote:
> MISRA C Rule 18.2 states: "Subtraction between pointers shall
> only be applied to pointers that address elements of the same array".
> 
> Subtractions between pointer where at least one symbol is a
> symbol defined by the linker are safe and thus deviated, because
> the compiler cannot exploit the undefined behaviour that would
> arise from violating the rules in this case.
> 
> To create an ECLAIR configuration that contains the list of
> linker-defined symbols, the script "linker-symbols.sh" is used
> after a build of xen (without static analysis) is performed.
> The generated file "linker_symbols.ecl" is then used as part of the
> static analysis configuration.
> 
> Additional changes to the ECLAIR integration are:
> - perform a build of xen without static analysis during prepare.sh
> - run the scripts to generated ECL configuration during the prepare.sh,
>   rather than analysis.sh
> - export ECLAIR_PROJECT_ROOT earlier, to allow such generation
> 
> Additionally, the macro page_to_mfn performs a subtraction that is 
> safe,
> so its uses are deviated.
> 
> No functional changes.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
> Acked-by: Stefano Stabellini <sstabellini@kernel.org>

Forgot to Cc the maintainers, sorry.

> ---
> Changes in v2:
> - renamed new file generate_linker_symbols.sh to use dashes instead of
>   underscores as separators
> 
> Macro page_to_pdx is also the cause of some caution reports:
> perhaps that should be deviated as well, since its definition is very
> similar to page_to_mfn.
> 
> Relevant CI runs:
> 
> - arm64: 
> https://saas.eclairit.com:3787/fs/var/local/eclair/xen-project.ecdf/xen-project/people/bugseng/xen/ECLAIR_normal/MC3R1.R18.2/ARM64/7769096695/PROJECT.ecd;/by_service/MC3R1.R18.2.html
> 
> - x86_64: 
> https://saas.eclairit.com:3787/fs/var/local/eclair/xen-project.ecdf/xen-project/people/bugseng/xen/ECLAIR_normal/MC3R1.R18.2/X86_64/7769096694/PROJECT.ecd;/by_service/MC3R1.R18.2.html
> - x86_64 (without page_to_pdx reports): 
> https://saas.eclairit.com:3787/fs/var/local/eclair/xen-project.ecdf/xen-project/people/bugseng/xen/ECLAIR_normal/MC3R1.R18.2/X86_64/7769096694/PROJECT.ecd;/by_service/MC3R1.R18.2.html#{"select":true,"selection":{"hiddenAreaKinds":[],"hiddenSubareaKinds":[],"show":false,"selector":{"enabled":true,"negated":false,"kind":0,"domain":"message","inputs":[{"enabled":true,"text":"^.*expanded 
> from macro `page_to_pdx'"}]}}}
> ---
>  automation/eclair_analysis/ECLAIR/analyze.sh  |  6 ----
>  .../eclair_analysis/ECLAIR/deviations.ecl     | 11 +++++++
>  .../ECLAIR/generate-linker-symbols.sh         | 31 +++++++++++++++++++
>  .../eclair_analysis/ECLAIR/generate_ecl.sh    |  3 ++
>  automation/eclair_analysis/prepare.sh         |  6 +++-
>  automation/scripts/eclair                     |  3 ++
>  docs/misra/deviations.rst                     | 10 ++++++
>  7 files changed, 63 insertions(+), 7 deletions(-)
>  create mode 100755 
> automation/eclair_analysis/ECLAIR/generate-linker-symbols.sh
> 
> diff --git a/automation/eclair_analysis/ECLAIR/analyze.sh 
> b/automation/eclair_analysis/ECLAIR/analyze.sh
> index e96456c3c18d..1dc63c1bc2d0 100755
> --- a/automation/eclair_analysis/ECLAIR/analyze.sh
> +++ b/automation/eclair_analysis/ECLAIR/analyze.sh
> @@ -73,17 +73,11 @@ export 
> ECLAIR_WORKSPACE="${ECLAIR_DATA_DIR}/eclair_workspace"
> 
>  # Identifies the particular build of the project.
>  export ECLAIR_PROJECT_NAME="XEN_${VARIANT}-${SET}"
> -# All paths mentioned in ECLAIR reports that are below this directory
> -# will be presented as relative to ECLAIR_PROJECT_ROOT.
> -export ECLAIR_PROJECT_ROOT="${PWD}"
> 
>  # Erase and recreate the output directory and the data directory.
>  rm -rf "${ECLAIR_OUTPUT_DIR:?}/*"
>  mkdir -p "${ECLAIR_DATA_DIR}"
> 
> -# Generate additional configuration files
> -"${SCRIPT_DIR}/generate_ecl.sh"
> -
>  # Perform the build (from scratch) in an ECLAIR environment.
>  "${ECLAIR_BIN_DIR}eclair_env" \
>      "-config_file='${SCRIPT_DIR}/analysis.ecl'" \
> diff --git a/automation/eclair_analysis/ECLAIR/deviations.ecl 
> b/automation/eclair_analysis/ECLAIR/deviations.ecl
> index 9051f4160282..a56805a993cd 100644
> --- a/automation/eclair_analysis/ECLAIR/deviations.ecl
> +++ b/automation/eclair_analysis/ECLAIR/deviations.ecl
> @@ -533,6 +533,17 @@ safe."
>  # Series 18.
>  #
> 
> +-doc_begin="Subtractions between pointers involving at least one of 
> the linker symbols specified by the regex below
> +are guaranteed not to be exploited by a compiler that relies on the 
> absence of
> +C99 Undefined Behaviour 45: Pointers that do not point into, or just 
> beyond, the same array object are subtracted (6.5.6)."
> +-eval_file=linker_symbols.ecl
> +-config=MC3R1.R18.2,reports+={safe, 
> "any_area(stmt(operator(sub)&&child(lhs||rhs, 
> skip(__non_syntactic_paren_stmts, ref(linker_symbols)))))"}
> +-doc_end
> +
> +-doc_begin="The following macro performs a subtraction between 
> pointers to obtain the mfn, but does not lead to undefined behaviour."
> +-config=MC3R1.R18.2,reports+={safe, 
> "any_area(any_loc(any_exp(macro(^page_to_mfn$))))"}
> +-doc_end
> +
>  -doc_begin="Flexible array members are deliberately used and XEN 
> developers are aware of the dangers related to them:
>  unexpected result when the structure is given as argument to a 
> sizeof() operator and the truncation in assignment between structures."
>  -config=MC3R1.R18.7,reports+={deliberate, "any()"}
> diff --git 
> a/automation/eclair_analysis/ECLAIR/generate-linker-symbols.sh 
> b/automation/eclair_analysis/ECLAIR/generate-linker-symbols.sh
> new file mode 100755
> index 000000000000..19943ba98d46
> --- /dev/null
> +++ b/automation/eclair_analysis/ECLAIR/generate-linker-symbols.sh
> @@ -0,0 +1,31 @@
> +#!/bin/bash
> +
> +set -e
> +
> +script_name="$(basename "$0")"
> +script_dir="$(
> +  cd "$(dirname "$0")"
> +  echo "${PWD}"
> +)"
> +
> +fatal() {
> +  echo "${script_name}: $*" >&2
> +  exit 1
> +}
> +
> +arch=""
> +if [ "${XEN_TARGET_ARCH}" == "x86_64" ]; then
> +  arch=x86
> +elif [ "${XEN_TARGET_ARCH}" == "arm64" ]; then
> +  arch=arm
> +else
> +  fatal "Unknown configuration: $1"
> +fi
> +
> +outfile=${script_dir}/linker_symbols.ecl
> +
> +(
> +  echo -n "-decl_selector+={linker_symbols, \"^(" >"${outfile}"
> +  "${script_dir}/../linker-symbols.sh" "${arch}" | sort -u | tr '\n' 
> '|' | sed '$ s/|//' >>"${outfile}"
> +  echo -n ")$\"}" >>"${outfile}"
> +)
> diff --git a/automation/eclair_analysis/ECLAIR/generate_ecl.sh 
> b/automation/eclair_analysis/ECLAIR/generate_ecl.sh
> index 66766b23abb7..b955783904a8 100755
> --- a/automation/eclair_analysis/ECLAIR/generate_ecl.sh
> +++ b/automation/eclair_analysis/ECLAIR/generate_ecl.sh
> @@ -17,3 +17,6 @@ 
> accepted_rst="${ECLAIR_PROJECT_ROOT}/docs/misra/rules.rst"
> 
>  # Generate accepted guidelines
>  "${script_dir}/accepted_guidelines.sh" "${accepted_rst}"
> +
> +# Generate the list of linker-defined symbols (must be run after a Xen 
> build)
> +"${script_dir}/generate-linker-symbols.sh"
> diff --git a/automation/eclair_analysis/prepare.sh 
> b/automation/eclair_analysis/prepare.sh
> index 47b2a2f32a84..3a646414a392 100755
> --- a/automation/eclair_analysis/prepare.sh
> +++ b/automation/eclair_analysis/prepare.sh
> @@ -39,10 +39,14 @@ fi
>      cp "${CONFIG_FILE}" xen/.config
>      make clean
>      find . -type f -name "*.safparse" -print -delete
> +    "${script_dir}/build.sh" "$1"
> +    # Generate additional configuration files
> +    "${script_dir}/ECLAIR/generate_ecl.sh"
> +    make clean
>      cd xen
>      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
>      # Translate function-properties.json into ECLAIR properties
> -    python3 ${script_dir}/propertyparser.py
> +    python3 "${script_dir}/propertyparser.py"
>  )
> diff --git a/automation/scripts/eclair b/automation/scripts/eclair
> index 3ec760bab8b3..0a2353c20a92 100755
> --- a/automation/scripts/eclair
> +++ b/automation/scripts/eclair
> @@ -3,6 +3,9 @@
>  ECLAIR_ANALYSIS_DIR=automation/eclair_analysis
>  ECLAIR_DIR="${ECLAIR_ANALYSIS_DIR}/ECLAIR"
>  ECLAIR_OUTPUT_DIR=$(realpath "${ECLAIR_OUTPUT_DIR}")
> +# All paths mentioned in ECLAIR reports that are below this directory
> +# will be presented as relative to ECLAIR_PROJECT_ROOT.
> +export ECLAIR_PROJECT_ROOT="${PWD}"
> 
>  "${ECLAIR_ANALYSIS_DIR}/prepare.sh" "${VARIANT}"
> 
> diff --git a/docs/misra/deviations.rst b/docs/misra/deviations.rst
> index b66c271c4e7c..39cd1de1e5b2 100644
> --- a/docs/misra/deviations.rst
> +++ b/docs/misra/deviations.rst
> @@ -501,6 +501,16 @@ Deviations related to MISRA C:2012 Rules:
>           - __builtin_memset()
>           - cpumask_check()
> 
> +   * - R18.2
> +     - Subtractions between pointers where at least one of the operand 
> is a
> +       pointer to a symbol defined by the linker are safe.
> +     - Tagged as `safe` for ECLAIR.
> +
> +   * - R18.2
> +     - Subtraction between pointers encapsulated by macro page_to_mfn
> +       are safe.
> +     - Tagged as `safe` for ECLAIR.
> +
>     * - R20.4
>       - The override of the keyword \"inline\" in xen/compiler.h is 
> present so
>         that section contents checks pass when the compiler chooses not 
> to

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

Patchew 2.1-devel-b67e4c2

© 2016 - 2024 Red Hat, Inc.