automation/eclair_analysis: deviate linker symbols for Rule 18.2

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 <[email protected]>
Acked-by: Stefano Stabellini <[email protected]>

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'" \

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()"}

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}"
+)

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"

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"
 )

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}"
 

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