Re: [PATCH v2 00/13] Support gcov instrumentation

[Chris Johns]

OK

Thanks
Chris

On 1/7/2022 9:49 pm, Sebastian Huber wrote:
> This patch set adds support to build the RTEMS libraries with gcov
> instrumentation to get code and branch coverage.  There are some improvements
> necessary in the build system to support different compiler flags for 
> libraries
> and tests.  In general, code coverage is enabled by the new RTEMS_COVERAGE
> build configuration option.  The user can fine tune the build through the
> BSP_OPTIMIZATION_FLAGS, CPUKIT_OPTIMIZATION_FLAGS, TEST_OPTIMIZATION_FLAGS, 
> and
> COVERAGE_COMPILER_FLAGS, COVERAGE_LINKER_FLAGS options.  The gcov information
> is dumped after each test case in a base64 encoded gcfn and gcda data stream.
> It looks like this:
> 
> *** BEGIN OF GCOV INFO BASE64 ***
> bmZjZyAxMkJSL3RtcC9zaC9iLXJ0ZW1zL2FybS94aWxpbnhfenlucV9hOV9xZW11L2NwdWtp
> dC9saWJjc3VwcG9ydC9zcmMvX19nZXR0b2QuYy42NS5nY2RhAGFkY2cgMTJCPoT6qo6mcBUB
> DOOrF1pxp0aIPrK7wAAAoQHwAQwAAADTfDdNQYCYwJ9ZRL0AAKEBIAQA
> ...
> srvAAAChAfD///8BDMXOxS0Rhzqx6Old2wAAoQH4AQwAAACYh8U9/rgJ5hMc
> ig8AAKEB2P///wEMN3+9YAwMW8gTHIoPAAChAdj///8BDDAwMx4TuamFPrK7
> wAAAoQHwAQwAAACvassJzDNWd/lKs3wAAKEB8P///wA=
> *** END OF GCOV INFO BASE64 ***
> 
> On the host you can decode the block and pipe it through the gcov-tool to
> produce the *.gcda files.  Example Python code:
> 
> block = some regex stuff to get the block between the BEGIN/END OF ...
> stream = base64.b64decode(block)
> subprocess.run(["arm-rtems6-gcov-tool", "merge-stream"], input=stream)
> 
> v2:
> 
> * Rename RTEMS_COVERAGE in RTEMS_GCOV_COVERAGE
> 
> * Add  and provide gcov_info linker set in separate file.
> 
> * Split LIBRARY_OPTIMIZATION_FLAGS in BSP_OPTIMIZATION_FLAGS and
>   CPUKIT_OPTIMIZATION_FLAGS.
> 
> Sebastian Huber (13):
>   build: Add more flags to BuildItemContext
>   build: Move BSP_INCLUDES split
>   build: Fix identifier pattern
>   build: Improve value substitution
>   build: Add cppflags, cflags, cxxflags to groups
>   build: Fix optimization flags definition order
>   build: Allow separate optimization flags
>   gcov: Add fork(), etc. gcov wrappers
>   gcov: Add functions to dump the gcov information
>   gcov: Add wrapper to dump the gcov info
>   build: Add RTEMS_GCOV_COVERAGE option
>   samples/minimum: Prevent a stack overflow
>   libtests/crypt01: Avoid stack overflows
> 
>  cpukit/include/rtems/score/gcov.h |  66 ++
>  cpukit/include/rtems/score/io.h   |   4 +
>  cpukit/include/rtems/test-info.h  |   6 +
>  cpukit/libcsupport/src/gcovfork.c |  94 ++
>  cpukit/libtest/testgcovbspreset.c |  54 
>  cpukit/libtest/testgcovcpufatalhalt.c |  54 
>  cpukit/libtest/testgcovdumpinfo.c |  66 ++
>  cpukit/score/src/gcovinfoset.c|  42 ++
>  cpukit/score/src/iogcovdumpinfo.c |  97 ++
>  cpukit/score/src/iogcovdumpinfobase64.c   | 111 
>  spec/build/bsps/aarch64/a53/grp.yml   |   3 +
>  spec/build/bsps/aarch64/a72/grp.yml   |   3 +
>  spec/build/bsps/aarch64/grp.yml   |   3 +
>  spec/build/bsps/aarch64/xilinx-versal/grp.yml |   3 +
>  .../bsps/aarch64/xilinx-versal/grp_qemu.yml   |   3 +
>  .../bsps/aarch64/xilinx-versal/grp_vck190.yml |   3 +
>  spec/build/bsps/aarch64/xilinx-zynqmp/grp.yml |   3 +
>  .../bsps/aarch64/xilinx-zynqmp/grp_zu3eg.yml  |   5 +-
>  spec/build/bsps/arm/beagle/bspboardorig.yml   |   4 +-
>  spec/build/bsps/arm/beagle/bspboardxm.yml |   4 +-
>  spec/build/bsps/arm/beagle/bspboneblack.yml   |   4 +-
>  spec/build/bsps/arm/beagle/bspbonewhite.yml   |   4 +-
>  spec/build/bsps/arm/beagle/grp.yml|   3 +
>  spec/build/bsps/arm/csb337/bspcsb337.yml  |   4 +-
>  spec/build/bsps/arm/csb337/bspcsb637.yml  |   4 +-
>  spec/build/bsps/arm/csb337/bspkit637v6.yml|   4 +-
>  spec/build/bsps/arm/csb337/grp.yml|   3 +
>  spec/build/bsps/arm/fvp/bspcortexr52.yml  |   4 +-
>  spec/build/bsps/arm/fvp/grp.yml   |   3 +
>  spec/build/bsps/arm/grp.yml   |   3 +
>  spec/build/bsps/arm/lm3s69xx/bsplm3s3749.yml  |   4 +-
>  spec/build/bsps/arm/lm3s69xx/bsplm3s6965.yml  |   4 +-
>  spec/build/bsps/arm/lm3s69xx/bsplm4f120.yml   |   4 +-
>  spec/build/bsps/arm/lm3s69xx/bspqemu.yml  |   4 +-
>  spec/build/bsps/arm/lm3s69xx/grp.yml  |   3 +
>  .../build/bsps/arm/lpc176x/bsplpc1768mbed.yml |   4 +-
>  .../bsps/arm/lpc176x/bsplpc1768mbedahbram.yml |   4 +-
>  .../arm/lpc176x/bsplpc1768mbedahbrameth.yml   |   4 +-
>  spec/build/bsps/arm/lpc176x/grp.yml   |   3 +
>  .../bsps/arm/lpc24xx/bsplpc17xxearam.yml  |   4 +-
>  .../bsps/arm/lpc24xx/bsplpc17xxearomint.yml   |   4 +-
>  .../bsps/arm/lpc24xx/bsplpc17xxplx800ram.yml  |   4 +-
>  .../arm/lpc24xx/bsplpc17xxplx800romint.yml|   4 +-
>  spec/build/bsps/arm/lpc24xx/bsplpc2362.yml|   4 +-
>  

Re: [PATCH] samples/cdtest: Test execeptions during system init

[Chris Johns]

OK

Thanks
Chris

On 1/7/2022 8:02 pm, Sebastian Huber wrote:
> Update #4668.
> Update #4672.
> ---
>  testsuites/samples/cdtest/main.cc | 44 ---
>  1 file changed, 35 insertions(+), 9 deletions(-)
> 
> diff --git a/testsuites/samples/cdtest/main.cc 
> b/testsuites/samples/cdtest/main.cc
> index 894e404ba1..44cdaf84bb 100644
> --- a/testsuites/samples/cdtest/main.cc
> +++ b/testsuites/samples/cdtest/main.cc
> @@ -25,9 +25,11 @@
>  #include 
>  #include 
>  #include 
> +#include 
>  
>  #include 
>  #include 
> +#include 
>  #include 
>  
>  #ifdef RTEMS_TEST_IO_STREAM
> @@ -44,13 +46,6 @@ extern rtems_task main_task(rtems_task_argument);
>  
>  static int num_inst = 0;
>  
> -static void check_begin_of_test(void)
> -{
> -  if ( num_inst == 0 ) {
> -TEST_BEGIN();
> -  }
> -}
> -
>  static void check_end_of_test(void)
>  {
>if ( num_inst == 0 ) {
> @@ -62,7 +57,6 @@ class AClass {
>  public:
>AClass(const char *p = "LOCAL" ) : ptr( p )
>  {
> -check_begin_of_test();
>  num_inst++;
>  printf(
>"%s: Hey I'm in base class constructor number %d for %p.\n",
> @@ -104,7 +98,6 @@ class BClass : public AClass {
>  public:
>BClass(const char *p = "LOCAL" ) : AClass( p )
>  {
> -check_begin_of_test();
>  num_inst++;
>  printf(
>"%s: Hey I'm in derived class constructor number %d for %p.\n",
> @@ -244,3 +237,36 @@ rtems_task main_task(
>  printf( "Global Dtors should be called after this line\n" );
>  exit(0);
>  }
> +
> +static void early_exception()
> +{
> +try
> +{
> +  throw "early exception";
> +}
> +catch( const char *e )
> +{
> +  rtems_test_assert(strcmp(e, "early exception") == 0);
> +  throw "early exception 2";
> +}
> +}
> +
> +static void test_exceptions_during_system_init()
> +{
> +TEST_BEGIN();
> +
> +try
> +{
> +  early_exception();
> +}
> +catch( const char *e )
> +{
> +  rtems_test_assert(strcmp(e, "early exception 2") == 0);
> +}
> +}
> +
> +RTEMS_SYSINIT_ITEM(
> +test_exceptions_during_system_init,
> +RTEMS_SYSINIT_IDLE_THREADS,
> +RTEMS_SYSINIT_ORDER_LAST
> +);
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Integrating the Formal Methods part of Qualification

[Chris Johns]

On 2/7/2022 12:59 am, Andrew Butterfield wrote:
> On 1 Jul 2022, at 00:59, Chris Johns  > wrote:
>>
>> On 28/6/2022 11:09 pm, andrew.butterfi...@scss.tcd.ie
>>  wrote:
>>> Dear RTEMS Developers,
>>>
>>> While the validation tests from the RTEMS pre-qualification activity are
>>> now merged into the RTEMS master, the work done in investigating and
>>> deploying formal methods techniques is not yet merged.
>>>
>>> The activity had two main phases: a planning phase (Nov 2018-Oct 2019)
>>> that explored various formal techniques, followed by an execution phase
>>> (Oct 2019-Nov 2021) that then applied selected techniques to selected
>>> parts of RTEMS. Some discussions occurred with the RTEMS community
>>> via the mailings lists over this time. A short third phase (Nov 2021 - Dec 
>>> 2021)
>>> then reported on the outcomes. Each phase resulted in a technical report.
>>>
>>> The key decision made was to use Promela/SPIN for test generation, and
>>> to apply it to the Chains API, the Event Manager, and the SMP scheduler
>>> thread queues. This involved developing models in the Promela language
>>> and using the SPIN model-checker tool to both check their correctness
>>> and to generate execution scenarios that could be used to generate tests.
>>> Tools were developed using Python 3.8 to support this. Initial documentation
>>> about tools and how to use them was put into the 2nd phase report.
>>
>> Congratulations for the work and results you and others have managed to 
>> achieve.
>> It is exciting to see this happening with RTEMS and being made public.
>>
>>> We now come to the part where we explore the best way to integrate this
>>> into RTEMS. I am proposing to do this under the guidance of Sebastian Huber.
>>>
>>> The first suggested step is adding in new documentation to the RTEMS
>>> Software Engineering manual, as a new Formal Methods chapter. This would
>>> provide some motivation, as well as a "howto".
>>>
>>> I assume that I would initially describe the proposed changes using the 
>>> patch
>>> review process described in the section on Preparing and Sending Patches in
>>> the User Manual.
>>>
>>> How do you feel I should best proceed?
>>
>> It is hard for me to answer until I understand what is being submitted and 
>> who
>> maintains it? I am sure you understand this due to the specialised nature of 
>> the
>> work.
> 
> Indeed, I quite agree.  I have some short answers below, with suggestions.

Thanks.

> 
>>
>> What will be submitted, ie SPIN files, scripts, etc?
> 
> Promela/SPIN model files (ASCII text, C-like syntax)
> C template files (.h,.c) to assist test code generation
> YAML files to provide a mapping from model concepts to RTEMS C test code 
> python scripts to automate the test generation
> Documentation - largely RTEMS compliant sphinx sources (.rst)
> 
>>
>> Where are you looking to add these pieces?
> 
> Everything except the documentation could live in a top-level folder 
> ('formal')
> in rtems-central.
> In fact there is no particular constraint from my perspective for where they 
> can go.

Using rtems-central is fine.

> The plan would be to add the pertinent parts of our project documentation into
> new chapters
> in the RTEMS software engineering manual. So that would be eng/ in the
> rtems-docs repo.

Great.

>> How is the verification run against the code? Do we manage regression testing
>> and is that even possible?
> 
> The python scripts basically run SPIN in such a way as to generate scenarios
> that model
> correct behaviour which then get turned into standard RTEMS test programs. 
> These all
> get added into a new testsuite in the rtems repo (testsuites/models, say).
> They are properly integrated into the RTEMS test system, so get built and run 
> by
> waf.
> This is similar to how the tests generated by Sebastian in 
> testsuites/validation
> are handled.
> 
> From the perspective of a user that works out of git.rtems.org/rtems
> , 
> there will be no obvious impact - just some extra tests in among the ones that
> already exist.

Thanks and this make sense.

> 
>>
>> I hope my simple questions highlight a lack of understand on how this works 
>> and
>> how we maintain it and use it once integrated.
> 
> I intend to continue to work and maintain this for the foreseeable future. I
> would hope as this beds in that other Promela/SPIN users out there will also 
> get
> more involved over time.

Thank, it is appreciated.

> It is expected that Promela models will be as static as the corresponding 
> APIs.
> They capture the specified behaviour of API calls, not their detailed
> implementation.
> 
> The python scripts should also be fairly stable, although I can see some
> tweaking for a while to improve workflow issues that might arise.
> 
> There are some extra python libraries that are required over and above what is
> currently specified in rtems-central/requirements.txt

This 

Re: [PATCH v2] irq/arm-gicv3.h: Customize ICC_IGRPEN0/1 init

[Chris Johns]

On 1/7/2022 11:21 pm, Sebastian Huber wrote:
> Use the existing WRITE_SR() abstraction to access the interrupt group 0 and 1
> enable registers.  This fixes the build for the AArch32 target.
> ---
>  bsps/include/dev/irq/arm-gicv3.h  | 30 ---
>  spec/build/bsps/aarch64/a53/grp.yml   |  2 ++
>  spec/build/bsps/aarch64/a53/obj.yml   |  1 -
>  spec/build/bsps/aarch64/a72/grp.yml   |  2 ++
>  spec/build/bsps/aarch64/a72/obj.yml   |  1 -
>  spec/build/bsps/aarch64/grp.yml   |  1 -
>  spec/build/bsps/aarch64/xilinx-versal/grp.yml |  2 ++
>  spec/build/bsps/aarch64/xilinx-versal/obj.yml |  1 -
>  spec/build/bsps/arm/fvp/grp.yml   |  2 ++
>  spec/build/bsps/arm/fvp/obj.yml   |  1 -
>  spec/build/bsps/arm/grp.yml   |  1 -
>  spec/build/bsps/objarmgic.yml | 21 +
>  spec/build/bsps/optarmgic-icc-igrpen0.yml | 20 +
>  spec/build/bsps/optarmgic-icc-igrpen1.yml | 17 +++
>  14 files changed, 78 insertions(+), 24 deletions(-)
>  create mode 100644 spec/build/bsps/objarmgic.yml
>  create mode 100644 spec/build/bsps/optarmgic-icc-igrpen0.yml
>  create mode 100644 spec/build/bsps/optarmgic-icc-igrpen1.yml
> 
> diff --git a/bsps/include/dev/irq/arm-gicv3.h 
> b/bsps/include/dev/irq/arm-gicv3.h
> index a79368ebdf..4cd8cfaaed 100644
> --- a/bsps/include/dev/irq/arm-gicv3.h
> +++ b/bsps/include/dev/irq/arm-gicv3.h
> @@ -116,9 +116,11 @@ extern "C" {
>  #else /* ARM_MULTILIB_ARCH_V4 */
>  
>  /* AArch64 GICv3 registers are not named in GCC */
> -#define ICC_IGRPEN0 "S3_0_C12_C12_6, %0"
> -#define ICC_IGRPEN1 "S3_0_C12_C12_7, %0"
> +#define ICC_IGRPEN0_EL1 "S3_0_C12_C12_6, %0"
> +#define ICC_IGRPEN1_EL1 "S3_0_C12_C12_7, %0"
>  #define ICC_IGRPEN1_EL3 "S3_6_C12_C12_7, %0"
> +#define ICC_IGRPEN0 ICC_IGRPEN0_EL1
> +#define ICC_IGRPEN1 ICC_IGRPEN1_EL1
>  #define ICC_PMR "S3_0_C4_C6_0, %0"
>  #define ICC_EOIR1   "S3_0_C12_C12_1, %0"
>  #define ICC_SRE "S3_0_C12_C12_5, %0"
> @@ -300,20 +302,6 @@ static void gicv3_init_dist(volatile gic_dist *dist)
>}
>  }
>  
> -/*
> - * A better way to access these registers than special opcodes
> - */
> -#define isb() __asm __volatile("isb" : : : "memory")
> -
> -#define  WRITE_SPECIALREG(reg, _val)\
> -  __asm __volatile("msr  " __STRING(reg) ", %0" : : "r"((uint64_t)_val))
> -
> -#define  gic_icc_write(reg, val)\
> -do {\
> -  WRITE_SPECIALREG(icc_ ##reg ##_el1, val); \
> -  isb();\
> -} while (0)
> -
>  static void gicv3_init_cpu_interface(uint32_t cpu_index)
>  {
>uint32_t sre_value = 0x7;
> @@ -334,8 +322,14 @@ static void gicv3_init_cpu_interface(uint32_t cpu_index)
>  sgi_ppi->icspiprior[id] = PRIORITY_DEFAULT;
>}
>  
> -  /* Enable interrupt groups 0 and 1 */
> -  gic_icc_write(IGRPEN1, 1);
> +  /* Initialize the group 0 and 1 interrupt enable */
> +#ifdef BSP_ARM_GIC_ICC_IGRPEN0
> +  WRITE_SR(ICC_IGRPEN0, BSP_ARM_GIC_ICC_IGRPEN0);
> +#endif

I think more things will surface in this driver over time and configuring at the
per register level may become unwieldy. This write depends on the EL levels
available, secure/non-secure support and the boot wrapper used for the different
classes of devices. Maybe the config support and macro reflecting this would
serve us better over time?

> +#ifdef BSP_ARM_GIC_ICC_IGRPEN1
> +  WRITE_SR(ICC_IGRPEN1, BSP_ARM_GIC_ICC_IGRPEN1);
> +#endif

I am yet to see if this works on a secure/non-secure Arvm8-A at EL1. The
hardware is being used on another task and I need access to it. My review of the
code looks OK but I would like to make sure first.

Chris
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel