Add a formal HAL specification for the MPU API

Add a formal HAL specification consisting of:
-defined and undefined behavior
-test descriptions
-enable doxygen for MPU

Author: c1728p9

TESTS/mbed_hal/mpu/main.cpp

@@ -22,6 +22,7 @@
 #include <stdlib.h>
 
 #include "mpu_api.h"
+#include "mpu_test.h"
 
 #if !DEVICE_MPU
 #error [NOT_SUPPORTED] MPU API not supported for this target

TESTS/mbed_hal/mpu/mpu_test.h

@@ -0,0 +1,94 @@
+/* mbed Microcontroller Library
+ * Copyright (c) 2018-2018 ARM Limited
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+/** \addtogroup hal_mpu_tests
+ *  @{
+ */
+
+#ifndef MBED_MPU_TEST_H
+#define MBED_MPU_TEST_H
+
+#if DEVICE_MPU
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/** Test that ::mbed_mpu_init can be called multiple times.
+ *
+ *  Given board provides MPU.
+ *  When ::mbed_mpu_init is called multiple times.
+ *  Then ::mbed_mpu_init are successfully performed (no exception is generated).
+ *
+ */
+void mpu_init_test(void);
+
+/** Test that ::mbed_mpu_free disables the MPU
+ *
+ * Given board provides MPU.
+ * When ::mbed_mpu_free is called.
+ * Then execution from RAM is allowed.
+ *
+ */
+void mpu_free_test(void);
+
+/** Test that MPU protection works for global data
+ *
+ * Given board provides MPU.
+ * When RAM execution is disabled with a call to ::mbed_mpu_enable_ram_xn.
+ * Then execution from global initialized data results in a fault.
+ *
+ */
+void mpu_fault_test_data(void);
+
+/** Test that MPU protection works for zero initialized data
+ *
+ * Given board provides MPU.
+ * When RAM execution is disabled with a call to ::mbed_mpu_enable_ram_xn.
+ * Then execution from global uninitialized data results in a fault.
+ *
+ */
+void mpu_fault_test_bss(void);
+
+/** Test that MPU protection works for the stack
+ *
+ * Given board provides MPU.
+ * When RAM execution is disabled with a call to ::mbed_mpu_enable_ram_xn.
+ * Then execution from stack memory results in a fault.
+ *
+ */
+void mpu_fault_test_stack(void);
+
+/** Test that MPU protection works for the heap
+ *
+ * Given board provides MPU.
+ * When RAM execution is disabled with a call to ::mbed_mpu_enable_ram_xn.
+ * Then execution from heap memory results in a fault.
+ *
+ */
+void mpu_fault_test_heap(void);
+
+/**@}*/
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+#endif
+
+/** @}*/

doxyfile_options

@@ -2083,6 +2083,7 @@ PREDEFINED             = DOXYGEN_ONLY            \
                          DEVICE_INTERRUPTIN      \
                          DEVICE_ITM              \
                          DEVICE_LPTICKER         \
+                         DEVICE_MPU              \
                          DEVICE_PORTIN           \
                          DEVICE_PORTINOUT        \
                          DEVICE_PORTOUT          \

doxygen_options.json

@@ -6,7 +6,7 @@
     "SEARCH_INCLUDES": "YES",
     "INCLUDE_PATH": "",
     "INCLUDE_FILE_PATTERNS": "",
-    "PREDEFINED": "DOXYGEN_ONLY DEVICE_ANALOGIN DEVICE_ANALOGOUT DEVICE_CAN DEVICE_CRC DEVICE_ETHERNET DEVICE_EMAC DEVICE_FLASH  DEVICE_I2C DEVICE_I2CSLAVE DEVICE_I2C_ASYNCH DEVICE_INTERRUPTIN DEVICE_ITM DEVICE_LPTICKER DEVICE_PORTIN DEVICE_PORTINOUT DEVICE_PORTOUT DEVICE_PWMOUT DEVICE_RTC DEVICE_TRNG DEVICE_SERIAL DEVICE_SERIAL_ASYNCH DEVICE_SERIAL_FC DEVICE_SLEEP DEVICE_SPI DEVICE_SPI_ASYNCH DEVICE_SPISLAVE DEVICE_QSPI DEVICE_STORAGE \"MBED_DEPRECATED_SINCE(f, g)=\" \"MBED_ENABLE_IF_CALLBACK_COMPATIBLE(F, M)=\" \"MBED_DEPRECATED(s)=\"",
+    "PREDEFINED": "DOXYGEN_ONLY DEVICE_ANALOGIN DEVICE_ANALOGOUT DEVICE_CAN DEVICE_CRC DEVICE_ETHERNET DEVICE_EMAC DEVICE_FLASH  DEVICE_I2C DEVICE_I2CSLAVE DEVICE_I2C_ASYNCH DEVICE_INTERRUPTIN DEVICE_ITM DEVICE_LPTICKER DEVICE_MPU DEVICE_PORTIN DEVICE_PORTINOUT DEVICE_PORTOUT DEVICE_PWMOUT DEVICE_RTC DEVICE_TRNG DEVICE_SERIAL DEVICE_SERIAL_ASYNCH DEVICE_SERIAL_FC DEVICE_SLEEP DEVICE_SPI DEVICE_SPI_ASYNCH DEVICE_SPISLAVE DEVICE_QSPI DEVICE_STORAGE \"MBED_DEPRECATED_SINCE(f, g)=\" \"MBED_ENABLE_IF_CALLBACK_COMPATIBLE(F, M)=\" \"MBED_DEPRECATED(s)=\"",
     "EXPAND_AS_DEFINED": "",
     "SKIP_FUNCTION_MACROS": "NO",
     "STRIP_CODE_COMMENTS": "NO",

hal/mpu_api.h

@@ -28,6 +28,37 @@ extern "C" {
 
 #if DEVICE_MPU
 
+/**
+ * \defgroup hal_mpu MPU hal
+ *
+ * The MPU hal provides a simple MPU API to enhance device security by preventing
+ * execution from ram.
+ *
+ * # Defined behavior
+ * * The function ::mbed_mpu_init is safe to call repeatedly - Verified by ::mpu_init_test
+ * * The function ::mbed_mpu_free disables MPU protection - Verified by ::mpu_free_test
+ * * Execution from RAM results in a fault when execute never is enabled.
+ *      This RAM includes heap, stack, data and zero init - Verified  by ::mpu_fault_test_data,
+ *      ::mpu_fault_test_bss, ::mpu_fault_test_stack and ::mpu_fault_test_heap.
+ *
+ * # Undefined behavior
+ * * Calling any function other than ::mbed_mpu_init before the initialization of the MPU.
+ *
+ * @see hal_mpu_tests
+ *
+ * @{
+ */
+
+/**
+ * \defgroup hal_mpu_tests MPU hal tests
+ * The MPU test validates proper implementation of the MPU hal.
+ *
+ * To run the MPU hal tests use the command:
+ *
+ *     mbed test -t <toolchain> -m <target> -n tests-mbed_hal-mpu*
+ */
+
+
 /**
  * Initialize the MPU
  *
@@ -53,6 +84,8 @@ void mbed_mpu_enable_ram_xn(bool enable);
  */
 void mbed_mpu_free(void);
 
+/**@}*/
+
 #else
 
 #define mbed_mpu_init()