Re: [PATCH 1/1] RSB: Mitigate too short error reports
On 12/21/22 00:06, Chris Johns wrote:
On 21/12/2022 3:44 am, Frank Kuehndel wrote:
From: Frank Kühndel
Close #4642
---
source-builder/sb/ereport.py | 4
1 file changed, 4 insertions(+)
diff --git a/source-builder/sb/ereport.py b/source-builder/sb/ereport.py
index d8fb5f6..d391917 100755
--- a/source-builder/sb/ereport.py
+++ b/source-builder/sb/ereport.py
@@ -55,6 +55,10 @@ def generate(name, opts, header = None, footer = None):
with open(name, 'w') as l:
l.write(os.linesep.join(r))
log.notice(' See error report: %s' % (name))
+log.notice(' (Hint: The first error may be in front of a '
+'line containing\n'
+' "Error 1" [GNU make] and may be only in the whole log '
Is this too specific to GNU make? What ifs a package uses cmake or something
else?
As the text indicates, this is specific to GNU make. For those using
something else reading this text will still hint that the first error
may not be in the end of the report "and may be only in the whole log".
Another weak point in this text is that by far not all errors
originating from "make". Yet, the true trouble is the original "See
error report: %s" where it can sometimes happen that the error is not in
this "error report" at all.
I found it difficult to find a wording which is short, clear and helpful
to the reader and at the same time not confusing. I am not perfectly
happy with the notice above. I just found it a reasonable compromise.
If you prefer more generic texts - such as the examples below - I will
send a new patch with the suggested test.
"Hint: The first error may be far way from the end of the
report and in cases can only be found in the whole build log."
"Hint: The error is most likely in the error report otherwise
see the whole build log [--log option]."
If you find any such change might cause more confusion than it might be
helpful, I think it better to close this bug than to try to fix it.
Greetings,
Frank
--
embedded brains GmbH
Herr Frank KÜHNDEL
Dornierstr. 4
82178 Puchheim
Germany
email: frank.kuehn...@embedded-brains.de
phone: +49-89-18 94 741 - 23
mobile: +49-176-15 22 06 - 11
fax:+49-89-18 94 741 - 08
Registergericht: Amtsgericht München
Registernummer: HRB 157899
Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler
Unsere Datenschutzerklärung finden Sie hier:
https://embedded-brains.de/datenschutzerklaerung/
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel
[PATCH 1/5] bsp/qoriq: Use only pic_is_ipi()
---
bsps/powerpc/qoriq/irq/irq.c | 17 ++---
1 file changed, 6 insertions(+), 11 deletions(-)
diff --git a/bsps/powerpc/qoriq/irq/irq.c b/bsps/powerpc/qoriq/irq/irq.c
index 2858ff7581..cadd503a6f 100644
--- a/bsps/powerpc/qoriq/irq/irq.c
+++ b/bsps/powerpc/qoriq/irq/irq.c
@@ -293,7 +293,7 @@ static volatile qoriq_pic_src_cfg
*get_src_cfg(rtems_vector_number vector)
}
}
-static bool is_ipi(rtems_vector_number vector)
+static bool pic_is_ipi(rtems_vector_number vector)
{
return (vector - QORIQ_IRQ_IPI_BASE) < 4;
}
@@ -340,7 +340,7 @@ rtems_status_code bsp_interrupt_set_affinity(
{
volatile qoriq_pic_src_cfg *src_cfg;
- if (is_ipi(vector)) {
+ if (pic_is_ipi(vector)) {
return RTEMS_UNSATISFIED;
}
@@ -356,7 +356,7 @@ rtems_status_code bsp_interrupt_get_affinity(
{
volatile qoriq_pic_src_cfg *src_cfg;
- if (is_ipi(vector)) {
+ if (pic_is_ipi(vector)) {
return RTEMS_UNSATISFIED;
}
@@ -383,7 +383,7 @@ rtems_status_code bsp_interrupt_get_attributes(
rtems_interrupt_attributes *attributes
)
{
- bool vector_is_ipi = is_ipi(vector);
+ bool vector_is_ipi = pic_is_ipi(vector);
attributes->is_maskable = true;
attributes->can_enable = true;
attributes->maybe_enable = true;
@@ -422,7 +422,7 @@ rtems_status_code bsp_interrupt_raise(rtems_vector_number
vector)
{
bsp_interrupt_assert(bsp_interrupt_is_valid_vector(vector));
- if (is_ipi(vector)) {
+ if (pic_is_ipi(vector)) {
raise_on(vector, rtems_scheduler_get_processor());
return RTEMS_SUCCESSFUL;
}
@@ -438,7 +438,7 @@ rtems_status_code bsp_interrupt_raise_on(
{
bsp_interrupt_assert(bsp_interrupt_is_valid_vector(vector));
- if (is_ipi(vector)) {
+ if (pic_is_ipi(vector)) {
raise_on(vector, cpu_index);
return RTEMS_SUCCESSFUL;
}
@@ -498,11 +498,6 @@ void bsp_interrupt_dispatch(uintptr_t exception_number)
}
}
-static bool pic_is_ipi(rtems_vector_number vector)
-{
- return QORIQ_IRQ_IPI_0 <= vector && vector <= QORIQ_IRQ_IPI_3;
-}
-
static void pic_reset(void)
{
qoriq.pic.gcr = GCR_RST;
--
2.35.3
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel
[PATCH 0/5] bsp/qoriq: Improve PCIe support
Sebastian Huber (5): bsp/qoriq: Use only pic_is_ipi() bsp/qoriq: Clear shared message signaled interrupts bsp/qoriq: Support message signaled interrupts bsp/qoriq: Add qoriq_mmu_find_free_tlb1_entry() bsp/qoriq: Add qoriq_mmu_adjust_and_write_to_tlb1() bsps/powerpc/qoriq/include/bsp/irq.h | 48 +++-- bsps/powerpc/qoriq/include/bsp/mmu.h | 12 ++ bsps/powerpc/qoriq/irq/irq.c | 253 --- bsps/powerpc/qoriq/start/bspsmp.c| 9 +- bsps/powerpc/qoriq/start/mmu.c | 52 +- 5 files changed, 330 insertions(+), 44 deletions(-) -- 2.35.3 ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
[PATCH 2/5] bsp/qoriq: Clear shared message signaled interrupts
---
bsps/powerpc/qoriq/irq/irq.c | 5 +
1 file changed, 5 insertions(+)
diff --git a/bsps/powerpc/qoriq/irq/irq.c b/bsps/powerpc/qoriq/irq/irq.c
index cadd503a6f..f33b7c24ae 100644
--- a/bsps/powerpc/qoriq/irq/irq.c
+++ b/bsps/powerpc/qoriq/irq/irq.c
@@ -545,6 +545,11 @@ void bsp_interrupt_facility_initialize(void)
qoriq.pic.svr = SPURIOUS;
qoriq.pic.gcr = GCR_M;
+ /* Clear shared message signaled interrupts */
+ for (i = 0; i < 8; ++i) {
+ qoriq.pic.msir[i].reg;
+ }
+
pic_global_timer_init();
}
--
2.35.3
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel
[PATCH 5/5] bsp/qoriq: Add qoriq_mmu_adjust_and_write_to_tlb1()
---
bsps/powerpc/qoriq/include/bsp/mmu.h | 10 ++
bsps/powerpc/qoriq/start/bspsmp.c| 9 ++---
bsps/powerpc/qoriq/start/mmu.c | 26 ++
3 files changed, 38 insertions(+), 7 deletions(-)
diff --git a/bsps/powerpc/qoriq/include/bsp/mmu.h
b/bsps/powerpc/qoriq/include/bsp/mmu.h
index 2a69f683bc..52c4c36627 100644
--- a/bsps/powerpc/qoriq/include/bsp/mmu.h
+++ b/bsps/powerpc/qoriq/include/bsp/mmu.h
@@ -105,6 +105,16 @@ void qoriq_tlb1_write(
int tsize
);
+void qoriq_mmu_adjust_and_write_to_tlb1(
+ int tlb,
+ uintptr_t begin,
+ uintptr_t last,
+ uint32_t mas1,
+ uint32_t mas2,
+ uint32_t mas3,
+ uint32_t mas7
+);
+
void qoriq_tlb1_invalidate(int esel);
/** @} */
diff --git a/bsps/powerpc/qoriq/start/bspsmp.c
b/bsps/powerpc/qoriq/start/bspsmp.c
index 376854c5f3..ec261cb981 100644
--- a/bsps/powerpc/qoriq/start/bspsmp.c
+++ b/bsps/powerpc/qoriq/start/bspsmp.c
@@ -118,11 +118,8 @@ static void bsp_inter_processor_interrupt(void *arg)
static void setup_boot_page(void)
{
#ifdef QORIQ_IS_HYPERVISOR_GUEST
- qoriq_mmu_context mmu_context;
-
- qoriq_mmu_context_init(&mmu_context);
- qoriq_mmu_add(
-&mmu_context,
+ qoriq_mmu_adjust_and_write_to_tlb1(
+QORIQ_TLB1_ENTRY_COUNT - 1,
0xf000,
0x,
0,
@@ -130,8 +127,6 @@ static void setup_boot_page(void)
FSL_EIS_MAS3_SR | FSL_EIS_MAS3_SW,
0
);
- qoriq_mmu_partition(&mmu_context, 1);
- qoriq_mmu_write_to_tlb1(&mmu_context, QORIQ_TLB1_ENTRY_COUNT - 1);
#endif
}
diff --git a/bsps/powerpc/qoriq/start/mmu.c b/bsps/powerpc/qoriq/start/mmu.c
index e2b4009ac6..acd481fe12 100644
--- a/bsps/powerpc/qoriq/start/mmu.c
+++ b/bsps/powerpc/qoriq/start/mmu.c
@@ -406,3 +406,29 @@ int qoriq_mmu_find_free_tlb1_entry(void)
return -1;
}
+
+void qoriq_mmu_adjust_and_write_to_tlb1(
+ int tlb,
+ uintptr_t begin,
+ uintptr_t last,
+ uint32_t mas1,
+ uint32_t mas2,
+ uint32_t mas3,
+ uint32_t mas7
+)
+{
+ qoriq_mmu_context context;
+
+ qoriq_mmu_context_init(&context);
+ qoriq_mmu_add(
+ &context,
+ begin,
+ last,
+ mas1,
+ mas2,
+ mas3,
+ mas7
+ );
+ qoriq_mmu_partition(&context, 1);
+ qoriq_mmu_write_to_tlb1(&context, tlb);
+}
--
2.35.3
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel
[PATCH 4/5] bsp/qoriq: Add qoriq_mmu_find_free_tlb1_entry()
---
bsps/powerpc/qoriq/include/bsp/mmu.h | 2 ++
bsps/powerpc/qoriq/start/mmu.c | 26 +-
2 files changed, 27 insertions(+), 1 deletion(-)
diff --git a/bsps/powerpc/qoriq/include/bsp/mmu.h
b/bsps/powerpc/qoriq/include/bsp/mmu.h
index e9aad505b5..2a69f683bc 100644
--- a/bsps/powerpc/qoriq/include/bsp/mmu.h
+++ b/bsps/powerpc/qoriq/include/bsp/mmu.h
@@ -91,6 +91,8 @@ void qoriq_mmu_write_to_tlb1(qoriq_mmu_context *self, int
first_tlb);
void qoriq_mmu_change_perm(uint32_t test, uint32_t set, uint32_t clear);
+int qoriq_mmu_find_free_tlb1_entry(void);
+
void qoriq_mmu_config(bool boot_processor, int first_tlb, int scratch_tlb);
void qoriq_tlb1_write(
diff --git a/bsps/powerpc/qoriq/start/mmu.c b/bsps/powerpc/qoriq/start/mmu.c
index fa24357852..e2b4009ac6 100644
--- a/bsps/powerpc/qoriq/start/mmu.c
+++ b/bsps/powerpc/qoriq/start/mmu.c
@@ -358,12 +358,14 @@ void qoriq_mmu_change_perm(uint32_t test, uint32_t set,
uint32_t clear)
{
int i = 0;
- for (i = 0; i < 16; ++i) {
+ for (i = 0; i < QORIQ_TLB1_ENTRY_COUNT; ++i) {
uint32_t mas0 = FSL_EIS_MAS0_TLBSEL | FSL_EIS_MAS0_ESEL(i);
uint32_t mas1 = 0;
PPC_SET_SPECIAL_PURPOSE_REGISTER(FSL_EIS_MAS0, mas0);
+ ppc_synchronize_instructions();
ppc_tlbre();
+ ppc_synchronize_instructions();
mas1 = PPC_SPECIAL_PURPOSE_REGISTER(FSL_EIS_MAS1);
if ((mas1 & FSL_EIS_MAS1_V) != 0) {
@@ -382,3 +384,25 @@ void qoriq_mmu_change_perm(uint32_t test, uint32_t set,
uint32_t clear)
}
}
}
+
+int qoriq_mmu_find_free_tlb1_entry(void)
+{
+ int i = 0;
+
+ for (i = 0; i < QORIQ_TLB1_ENTRY_COUNT; ++i) {
+ uint32_t mas0 = FSL_EIS_MAS0_TLBSEL | FSL_EIS_MAS0_ESEL(i);
+ uint32_t mas1;
+
+ PPC_SET_SPECIAL_PURPOSE_REGISTER(FSL_EIS_MAS0, mas0);
+ ppc_synchronize_instructions();
+ ppc_tlbre();
+ ppc_synchronize_instructions();
+
+ mas1 = PPC_SPECIAL_PURPOSE_REGISTER(FSL_EIS_MAS1);
+ if ((mas1 & FSL_EIS_MAS1_V) == 0) {
+ return i;
+ }
+ }
+
+ return -1;
+}
--
2.35.3
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel
[PATCH 3/5] bsp/qoriq: Support message signaled interrupts
---
bsps/powerpc/qoriq/include/bsp/irq.h | 48 --
bsps/powerpc/qoriq/irq/irq.c | 233 +--
2 files changed, 255 insertions(+), 26 deletions(-)
diff --git a/bsps/powerpc/qoriq/include/bsp/irq.h
b/bsps/powerpc/qoriq/include/bsp/irq.h
index 0f1581542e..8f73c6f3de 100644
--- a/bsps/powerpc/qoriq/include/bsp/irq.h
+++ b/bsps/powerpc/qoriq/include/bsp/irq.h
@@ -331,15 +331,15 @@ extern "C" {
* @{
*/
-#define QORIQ_IRQ_MSI_BASE (QORIQ_IRQ_MI_7 + 1)
-#define QORIQ_IRQ_MSI_0 (QORIQ_IRQ_MSI_BASE + 0)
-#define QORIQ_IRQ_MSI_1 (QORIQ_IRQ_MSI_BASE + 1)
-#define QORIQ_IRQ_MSI_2 (QORIQ_IRQ_MSI_BASE + 2)
-#define QORIQ_IRQ_MSI_3 (QORIQ_IRQ_MSI_BASE + 3)
-#define QORIQ_IRQ_MSI_4 (QORIQ_IRQ_MSI_BASE + 4)
-#define QORIQ_IRQ_MSI_5 (QORIQ_IRQ_MSI_BASE + 5)
-#define QORIQ_IRQ_MSI_6 (QORIQ_IRQ_MSI_BASE + 6)
-#define QORIQ_IRQ_MSI_7 (QORIQ_IRQ_MSI_BASE + 7)
+#define QORIQ_IRQ_MSI_MULTIPLEX_BASE (QORIQ_IRQ_MI_7 + 1)
+#define QORIQ_IRQ_MSI_0 (QORIQ_IRQ_MSI_MULTIPLEX_BASE + 0)
+#define QORIQ_IRQ_MSI_1 (QORIQ_IRQ_MSI_MULTIPLEX_BASE + 1)
+#define QORIQ_IRQ_MSI_2 (QORIQ_IRQ_MSI_MULTIPLEX_BASE + 2)
+#define QORIQ_IRQ_MSI_3 (QORIQ_IRQ_MSI_MULTIPLEX_BASE + 3)
+#define QORIQ_IRQ_MSI_4 (QORIQ_IRQ_MSI_MULTIPLEX_BASE + 4)
+#define QORIQ_IRQ_MSI_5 (QORIQ_IRQ_MSI_MULTIPLEX_BASE + 5)
+#define QORIQ_IRQ_MSI_6 (QORIQ_IRQ_MSI_MULTIPLEX_BASE + 6)
+#define QORIQ_IRQ_MSI_7 (QORIQ_IRQ_MSI_MULTIPLEX_BASE + 7)
/** @} */
@@ -363,7 +363,25 @@ extern "C" {
#define QORIQ_IRQ_GT_B_2 (QORIQ_IRQ_GT_BASE + 6)
#define QORIQ_IRQ_GT_B_3 (QORIQ_IRQ_GT_BASE + 7)
-#define BSP_INTERRUPT_VECTOR_COUNT (QORIQ_IRQ_GT_B_3 + 1)
+#define QORIQ_INTERRUPT_SOURCE_COUNT (QORIQ_IRQ_GT_B_3 + 1)
+
+#define QORIQ_IS_INTERRUPT_SOURCE(vector) \
+ (((rtems_vector_number) (vector)) < QORIQ_INTERRUPT_SOURCE_COUNT)
+
+#define QORIQ_IRQ_MSI_BASE QORIQ_INTERRUPT_SOURCE_COUNT
+
+#define QORIQ_IRQ_MSI_COUNT 256
+
+#define QORIQ_IRQ_MSI_INDEX(vector) ((vector) - QORIQ_IRQ_MSI_BASE)
+
+#define QORIQ_IRQ_MSI_VECTOR(index) (QORIQ_IRQ_MSI_BASE + (index))
+
+#define QORIQ_IRQ_MSI_REGISTER(vector) (QORIQ_IRQ_MSI_INDEX(vector) / 32)
+
+#define QORIQ_IRQ_IS_MSI(vector) \
+ (QORIQ_IRQ_MSI_INDEX(vector) < QORIQ_IRQ_MSI_COUNT)
+
+#define BSP_INTERRUPT_VECTOR_COUNT QORIQ_IRQ_MSI_VECTOR(QORIQ_IRQ_MSI_COUNT)
/** @} */
@@ -403,6 +421,16 @@ rtems_status_code bsp_interrupt_get_affinity(
Processor_mask *affinity
);
+rtems_status_code qoriq_pic_msi_allocate(rtems_vector_number *vector);
+
+rtems_status_code qoriq_pic_msi_free(rtems_vector_number vector);
+
+rtems_status_code qoriq_pic_msi_map(
+ rtems_vector_number vector,
+ uint64_t *addr,
+ uint32_t *data
+);
+
/** @} */
#ifdef __cplusplus
diff --git a/bsps/powerpc/qoriq/irq/irq.c b/bsps/powerpc/qoriq/irq/irq.c
index f33b7c24ae..81eb742b5d 100644
--- a/bsps/powerpc/qoriq/irq/irq.c
+++ b/bsps/powerpc/qoriq/irq/irq.c
@@ -34,6 +34,7 @@
*/
#include
+#include
#include
@@ -307,6 +308,10 @@ rtems_status_code qoriq_pic_set_priority(
rtems_status_code sc = RTEMS_SUCCESSFUL;
uint32_t old_vpr = 0;
+ if (QORIQ_IRQ_IS_MSI(vector)) {
+ return RTEMS_UNSATISFIED;
+ }
+
if (bsp_interrupt_is_valid_vector(vector)) {
volatile qoriq_pic_src_cfg *src_cfg = get_src_cfg(vector);
@@ -344,6 +349,10 @@ rtems_status_code bsp_interrupt_set_affinity(
return RTEMS_UNSATISFIED;
}
+ if (QORIQ_IRQ_IS_MSI(vector)) {
+ return RTEMS_UNSATISFIED;
+ }
+
src_cfg = get_src_cfg(vector);
src_cfg->dr = _Processor_mask_To_uint32_t(affinity, 0);
return RTEMS_SUCCESSFUL;
@@ -360,22 +369,34 @@ rtems_status_code bsp_interrupt_get_affinity(
return RTEMS_UNSATISFIED;
}
+ if (QORIQ_IRQ_IS_MSI(vector)) {
+ return RTEMS_UNSATISFIED;
+ }
+
src_cfg = get_src_cfg(vector);
_Processor_mask_From_uint32_t(affinity, src_cfg->dr, 0);
return RTEMS_SUCCESSFUL;
}
-static void pic_vector_enable(rtems_vector_number vector, uint32_t msk)
+static rtems_status_code pic_vector_set_mask(
+ rtems_vector_number vector,
+ uint32_t msk
+)
{
volatile qoriq_pic_src_cfg *src_cfg;
rtems_interrupt_lock_context lock_context;
bsp_interrupt_assert(bsp_interrupt_is_valid_vector(vector));
+ if (QORIQ_IRQ_IS_MSI(vector)) {
+ return RTEMS_UNSATISFIED;
+ }
+
src_cfg = get_src_cfg(vector);
rtems_interrupt_lock_acquire(&lock, &lock_context);
src_cfg->vpr = (src_cfg->vpr & ~VPR_MSK) | msk;
rtems_interrupt_lock_release(&lock, &lock_context);
+ return RTEMS_SUCCESSFUL;
}
rtems_status_code bsp_interrupt_get_attributes(
@@ -383,17 +404,25 @@ rtems_status_code bsp_interrupt_get_attributes(
rtems_interrupt_attributes *attributes
)
{
- bool vector_is_ipi = pic_is_ipi(vector);
+ bool is_ipi = pic_is_ipi(vector);
+ bool
[PATCH 1/3] spec/build/riscv: Default rv64* BSPs to medany cmodel
From: Hesham Almatary Currently generic RISC-V BSPs (riscv/riscv) that start with rv64 and not rv64*_medany will start at 0x7000. This adds high maintenance overhead and deviates from almost all other RISC-V-based OSes and baremetal programs that start at 0x8000. Further, testing now has to account for an extra parameter (medany or not) that doubles the number of BSPs need to be tested. This commit defaults all RV64 BSPs to use medany code model to allow starting all BSPs at 0x8000. BSPs that require different code models and/or start addresses are custom and need to add their own entries. Updates #4775 --- spec/build/bsps/riscv/riscv/abi.yml | 13 ++--- 1 file changed, 2 insertions(+), 11 deletions(-) diff --git a/spec/build/bsps/riscv/riscv/abi.yml b/spec/build/bsps/riscv/riscv/abi.yml index 3ef8b0681d..29dd7b449d 100644 --- a/spec/build/bsps/riscv/riscv/abi.yml +++ b/spec/build/bsps/riscv/riscv/abi.yml @@ -21,21 +21,17 @@ default-by-variant: - -mabi=lp64d - -mcmodel=medany variants: - - riscv/rv64imafdc_medany -- value: - - -march=rv64imafdc - - -mabi=lp64d - variants: - riscv/rv64imafdc - value: - -march=rv64imafd - -mabi=lp64d - -mcmodel=medany variants: - - riscv/rv64imafd_medany + - riscv/rv64imafd - value: - -march=rv64imafd - -mabi=lp64d + - -mcmodel=medany variants: - riscv/rv64imafd - value: @@ -43,11 +39,6 @@ default-by-variant: - -mabi=lp64 - -mcmodel=medany variants: - - riscv/rv64imac_medany -- value: - - -march=rv64imac - - -mabi=lp64 - variants: - riscv/rv64imac - value: [] variants: -- 2.25.1 ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
[PATCH 2/3] spec/build/riscv: Start all riscv/riscv BSPs at 0x80000000
From: Hesham Almatary To follow other RISC-V-based OSes conventions. Delete generic BSPs that start at 0x7000 as BSPs are now medany by default. Updates #4775 --- spec/build/bsps/riscv/optrambegin.yml | 6 -- 1 file changed, 6 deletions(-) diff --git a/spec/build/bsps/riscv/optrambegin.yml b/spec/build/bsps/riscv/optrambegin.yml index 90133411cf..8890334915 100644 --- a/spec/build/bsps/riscv/optrambegin.yml +++ b/spec/build/bsps/riscv/optrambegin.yml @@ -10,12 +10,6 @@ copyrights: - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) default: 2147483648 default-by-variant: -- value: 2147483648 - variants: - - riscv/rv64.*medany -- value: 1879048192 - variants: - - riscv/rv64.* - value: 0 variants: - riscv/noel.* -- 2.25.1 ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
[PATCH 3/3] RISC-V: Always probe for HTIF and remove RISCV_ENABLE_HTIF_SUPPORT
From: Hesham Almatary
Updates #4779
---
bsps/riscv/noel/include/bsp/riscv.h | 2 --
bsps/riscv/riscv/console/console-config.c | 10 ++
bsps/riscv/riscv/console/htif.c | 4
bsps/riscv/riscv/include/bsp/riscv.h | 2 --
bsps/riscv/riscv/irq/irq.c| 15 +--
bsps/riscv/riscv/start/bsp_fatal_halt.c | 11 +++
6 files changed, 18 insertions(+), 26 deletions(-)
diff --git a/bsps/riscv/noel/include/bsp/riscv.h
b/bsps/riscv/noel/include/bsp/riscv.h
index 8ac049bb7c..3ab75573f0 100644
--- a/bsps/riscv/noel/include/bsp/riscv.h
+++ b/bsps/riscv/noel/include/bsp/riscv.h
@@ -50,9 +50,7 @@ extern uint32_t riscv_hart_count;
uint32_t riscv_get_hart_index_by_phandle(uint32_t phandle);
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
void htif_poweroff(void);
-#endif
#ifdef __cplusplus
}
diff --git a/bsps/riscv/riscv/console/console-config.c
b/bsps/riscv/riscv/console/console-config.c
index 7908c2f325..fe339c2353 100644
--- a/bsps/riscv/riscv/console/console-config.c
+++ b/bsps/riscv/riscv/console/console-config.c
@@ -60,9 +60,7 @@
static fe310_uart_context fe310_uart_instance;
#endif
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
static htif_console_context htif_console_instance;
-#endif
#if RISCV_CONSOLE_MAX_NS16550_DEVICES > 0
static ns16550_context ns16550_instances[RISCV_CONSOLE_MAX_NS16550_DEVICES];
@@ -165,7 +163,7 @@ static void riscv_console_probe(void)
compat_len = 0;
}
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
+/* Search for HTIF (eg. on Spike) and use it if found */
if (fdt_stringlist_contains(compat, compat_len, "ucb,htif0")) {
htif_console_context_init(&htif_console_instance.base, node);
@@ -173,7 +171,6 @@ static void riscv_console_probe(void)
riscv_console.putchar = htif_console_putchar;
riscv_console.getchar = htif_console_getchar;
};
-#endif
#if RISCV_CONSOLE_MAX_NS16550_DEVICES > 0
if (
@@ -280,10 +277,9 @@ rtems_status_code console_initialize(
void *arg
)
{
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
rtems_termios_device_context *base;
char htif_path[] = "/dev/ttyShtif";
-#endif
+
#if RISCV_CONSOLE_MAX_NS16550_DEVICES > 0
char path[] = "/dev/ttyS?";
size_t i;
@@ -296,14 +292,12 @@ rtems_status_code console_initialize(
rtems_termios_initialize();
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
base = &htif_console_instance.base;
rtems_termios_device_install(htif_path, &htif_console_handler, NULL, base);
if (base == riscv_console.context) {
link(htif_path, CONSOLE_DEVICE_NAME);
}
-#endif
#if RISCV_CONSOLE_MAX_NS16550_DEVICES > 0
for (i = 0; i < RISCV_CONSOLE_MAX_NS16550_DEVICES; ++i) {
diff --git a/bsps/riscv/riscv/console/htif.c b/bsps/riscv/riscv/console/htif.c
index bcfe6a5db5..750abe6e3e 100644
--- a/bsps/riscv/riscv/console/htif.c
+++ b/bsps/riscv/riscv/console/htif.c
@@ -29,8 +29,6 @@
#include
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
-
#include
#include
@@ -139,5 +137,3 @@ const rtems_termios_device_handler htif_console_handler = {
.poll_read = htif_console_getchar,
.mode = TERMIOS_POLLED
};
-
-#endif /* RISCV_ENABLE_HTIF_SUPPORT */
diff --git a/bsps/riscv/riscv/include/bsp/riscv.h
b/bsps/riscv/riscv/include/bsp/riscv.h
index d38f46c069..a11ae4291e 100644
--- a/bsps/riscv/riscv/include/bsp/riscv.h
+++ b/bsps/riscv/riscv/include/bsp/riscv.h
@@ -52,9 +52,7 @@ extern uint32_t riscv_hart_count;
uint32_t riscv_get_hart_index_by_phandle(uint32_t phandle);
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
void htif_poweroff(void);
-#endif
#ifdef __cplusplus
}
diff --git a/bsps/riscv/riscv/irq/irq.c b/bsps/riscv/riscv/irq/irq.c
index 3ef06a16bd..f0ccc6f5f0 100644
--- a/bsps/riscv/riscv/irq/irq.c
+++ b/bsps/riscv/riscv/irq/irq.c
@@ -247,13 +247,16 @@ static void riscv_plic_init(const void *fdt)
node = fdt_node_offset_by_compatible(fdt, -1, "riscv,plic0");
plic = riscv_fdt_get_address(fdt, node);
+
if (plic == NULL) {
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
-/* Spike platform has HTIF and does not have a PLIC */
-return;
-#else
-bsp_fatal(RISCV_FATAL_NO_PLIC_REG_IN_DEVICE_TREE);
-#endif
+ node = fdt_node_offset_by_compatible(fdt, -1, "ucb,htif0");
+
+ /* Spike platform has HTIF and does not have a PLIC */
+ if (node != -1) {
+ return;
+ } else {
+ bsp_fatal(RISCV_FATAL_NO_PLIC_REG_IN_DEVICE_TREE);
+ }
}
riscv_plic = plic;
diff --git a/bsps/riscv/riscv/start/bsp_fatal_halt.c
b/bsps/riscv/riscv/start/bsp_fatal_halt.c
index fb0787c606..cd7c5f20c5 100644
--- a/bsps/riscv/riscv/start/bsp_fatal_halt.c
+++ b/bsps/riscv/riscv/start/bsp_fatal_halt.c
@@ -38,14 +38,17 @@ void _CPU_Fatal_halt( uint32_t source, CPU_Uint32ptr error )
int node;
volatile uint32_t *sifive_test;
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
- htif_poweroff();
-#endif
+ fdt = bsp_fdt_get();
+
+ node = fdt_node_offset_by_compatible(fdt, -1, "ucb,htif0");
+
+ if (node != -1)
+ htif_poweroff();
+
#if RISCV_E
Re: [PATCH 1/3] spec/build/riscv: Default rv64* BSPs to medany cmodel
On 22/12/2022 11:42, heshamelmat...@gmail.com wrote: From: Hesham Almatary Currently generic RISC-V BSPs (riscv/riscv) that start with rv64 and not rv64*_medany will start at 0x7000. This adds high maintenance overhead and deviates from almost all other RISC-V-based OSes and baremetal programs that start at 0x8000. Further, testing now has to account for an extra parameter (medany or not) that doubles the number of BSPs need to be tested. This commit defaults all RV64 BSPs to use medany code model to allow starting all BSPs at 0x8000. BSPs that require different code models and/or start addresses are custom and need to add their own entries. Updates #4775 Thanks, the patch set looks good. Maybe we should also remove the *medany BSP variants: spec/build/bsps/riscv/riscv/bsprv64imacmedany.yml spec/build/bsps/riscv/riscv/bsprv64imafdcmedany.yml spec/build/bsps/riscv/riscv/bsprv64imafdmedany.yml -- embedded brains GmbH Herr Sebastian HUBER Dornierstr. 4 82178 Puchheim Germany email: sebastian.hu...@embedded-brains.de phone: +49-89-18 94 741 - 16 fax: +49-89-18 94 741 - 08 Registergericht: Amtsgericht München Registernummer: HRB 157899 Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler Unsere Datenschutzerklärung finden Sie hier: https://embedded-brains.de/datenschutzerklaerung/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
[PATCH 00/18] Adds Formal Verification Material
>From 3390ccc51f46ce0a4baa60422a62530c7c3c29bd Mon Sep 17 00:00:00 2001 From: Andrew Butterfield Date: Wed, 21 Dec 2022 18:03:47 + Subject: [PATCH 00/18] Adds Formal Verification Material This patch-set adds in the Promela/SPIN models and tools developed as part of the ESA-sponsored activity "Qualification of RTEMS Symmetric Multiprocessing (SMP)" as well as result of ongoing contributions by students at Trinity College Dublin to improve and extend them. It is a subset of the material contained at https://github.com/andrewbutterfield/RTEMS-SMP-Formal It focusses in the main on what currently produces RTEMS test code. Andrew Butterfield (18): adds in high-level directories and READMEs adds barrier manager model adds barrier manager generated material adds chains API model adds chain api generated material adds event manager model adds event manager generated material adds message manager model adds message manager generated material adds weak memory models adds in draft MrsP models for requirements and code third party code - promela parser modifies 3rd party code - promela parser third party code - comment filter modifies 3rd party code - comment filter adds test generation source code adds tests for testgen code adds automatic testgen examples formal/.gitignore |3 + formal/README.md | 27 + formal/promela/.gitignore |4 + formal/promela/README.md | 27 + formal/promela/models/README.md | 53 + formal/promela/models/barriers/README.md | 11 + formal/promela/models/barriers/STATUS.md | 95 + .../20221220-102256/barrier-mgr-model-0.spn | 220 +++ .../20221220-102256/barrier-mgr-model-1.spn | 216 +++ .../20221220-102256/barrier-mgr-model-10.spn | 233 +++ .../20221220-102256/barrier-mgr-model-11.spn | 229 +++ .../20221220-102256/barrier-mgr-model-12.spn | 236 +++ .../20221220-102256/barrier-mgr-model-13.spn | 232 +++ .../20221220-102256/barrier-mgr-model-14.spn | 212 +++ .../20221220-102256/barrier-mgr-model-15.spn | 208 +++ .../20221220-102256/barrier-mgr-model-16.spn | 224 +++ .../20221220-102256/barrier-mgr-model-17.spn | 220 +++ .../20221220-102256/barrier-mgr-model-18.spn | 297 +++ .../20221220-102256/barrier-mgr-model-19.spn | 293 +++ .../20221220-102256/barrier-mgr-model-2.spn | 220 +++ .../20221220-102256/barrier-mgr-model-3.spn | 216 +++ .../20221220-102256/barrier-mgr-model-4.spn | 227 +++ .../20221220-102256/barrier-mgr-model-5.spn | 223 +++ .../20221220-102256/barrier-mgr-model-6.spn | 233 +++ .../20221220-102256/barrier-mgr-model-7.spn | 229 +++ .../20221220-102256/barrier-mgr-model-8.spn | 233 +++ .../20221220-102256/barrier-mgr-model-9.spn | 229 +++ .../barrier-mgr-model.pml1.trail | 355 .../barrier-mgr-model.pml10.trail | 384 .../barrier-mgr-model.pml11.trail | 393 .../barrier-mgr-model.pml12.trail | 390 .../barrier-mgr-model.pml13.trail | 406 + .../barrier-mgr-model.pml14.trail | 403 + .../barrier-mgr-model.pml15.trail | 349 .../barrier-mgr-model.pml16.trail | 346 .../barrier-mgr-model.pml17.trail | 385 .../barrier-mgr-model.pml18.trail | 382 .../barrier-mgr-model.pml19.trail | 705 .../barrier-mgr-model.pml2.trail | 352 .../barrier-mgr-model.pml20.trail | 702 +++ .../barrier-mgr-model.pml3.trail | 354 .../barrier-mgr-model.pml4.trail | 351 .../barrier-mgr-model.pml5.trail | 388 .../barrier-mgr-model.pml6.trail | 385 .../barrier-mgr-model.pml7.trail | 394 .../barrier-mgr-model.pml8.trail | 391 .../barrier-mgr-model.pml9.trail | 387 .../archive/20221220-102256/model-0-test.log | 1469 +++ .../20221220-102256/tr-barrier-mgr-model-0.c | 399 .../20221220-102256/tr-barrier-mgr-model-1.c | 372 .../20221220-102256/tr-barrier-mgr-model-10.c | 414 + .../20221220-102256/tr-barrier-mgr-model-11.c | 387 .../20221220-102256/tr-barrier-mgr-model-12.c | 419 + .../20221220-102256/tr-barrier-mgr-model-13.c | 392 .../20221220-102256/tr-barrier-mgr-model-14.c | 380 .../20221220-102256/tr-barrier-mgr-model-15.c | 353 .../20221220-102256/tr-barrier-mgr-model-16.c | 395 .../20221220-102256/tr-barrier-mgr-model-17.c | 368 .../20221220-102256/tr-barrier-mgr-model-18.c | 401 .../20221220-102256/tr-barrier-mgr-model-19.c | 374 .../20221220-102256/tr-barrier-mgr-model-2.c | 399 .../20221220-102256/tr-barrier-mgr-model-3.c | 372 .../20221220-102256/tr-barrier-mgr-model-4.c
[PATCH 01/18] adds in high-level directories and READMEs
--- formal/.gitignore | 3 ++ formal/README.md| 27 + formal/promela/.gitignore | 4 ++ formal/promela/README.md| 27 + formal/promela/models/README.md | 53 formal/promela/src/README.md| 71 + 6 files changed, 185 insertions(+) create mode 100644 formal/.gitignore create mode 100644 formal/README.md create mode 100644 formal/promela/.gitignore create mode 100644 formal/promela/README.md create mode 100644 formal/promela/models/README.md create mode 100644 formal/promela/src/README.md diff --git a/formal/.gitignore b/formal/.gitignore new file mode 100644 index ..2cfdbe69 --- /dev/null +++ b/formal/.gitignore @@ -0,0 +1,3 @@ +NOTES.pdf +*.out + diff --git a/formal/README.md b/formal/README.md new file mode 100644 index ..d3ff71a6 --- /dev/null +++ b/formal/README.md @@ -0,0 +1,27 @@ +# Formal Verification + +`formal` + +This directory contains the models and tooling developed as part of the ESA-sponsored activity ***Qualification of RTEMS Symmetric Multiprocessing (SMP)***, that has been added into RTEMS in the `rtems-central` repository. + +## Contributors + +* Andrew Butterfield +* Frédéric Tuong +* Robert Jennings +* Jerzy Jaśkuć +* Eoin Lynch +* James Gooding Hunt + +## License + +This project is licensed under the +[BSD-2-Clause](https://spdx.org/licenses/BSD-2-Clause.html) or +[CC-BY-SA-4.0](https://spdx.org/licenses/CC-BY-SA-4.0.html). + +## Overview + +At present, the only formal verification in play here is the use of Promela to build formal models of key RTEMS components, and the SPIN model-checker to perform C test generation. + +This can be found in the `promela` sub-directory + diff --git a/formal/promela/.gitignore b/formal/promela/.gitignore new file mode 100644 index ..5b5b65fa --- /dev/null +++ b/formal/promela/.gitignore @@ -0,0 +1,4 @@ +*/refine_command.py +*/spin2test.py +*/pan* +*/testbuilder.yml diff --git a/formal/promela/README.md b/formal/promela/README.md new file mode 100644 index ..87f7299e --- /dev/null +++ b/formal/promela/README.md @@ -0,0 +1,27 @@ +# Promela/SPIN + +`formal/promela` + +This directory contains formal models written in Promela and tools that use SPIN to do test generation from those models. + +## Contributors + +* Andrew Butterfield +* Frédéric Tuong +* Robert Jennings +* Jerzy Jaśkuć +* Eoin Lynch +* James Gooding Hunt + +## License + +This project is licensed under the +[BSD-2-Clause](https://spdx.org/licenses/BSD-2-Clause.html) or +[CC-BY-SA-4.0](https://spdx.org/licenses/CC-BY-SA-4.0.html). + +## Overview + +The Promela models and supporting material can be found in the `models` subdirectory. + +The tools, written in Python3, are in the `src` directory. + diff --git a/formal/promela/models/README.md b/formal/promela/models/README.md new file mode 100644 index ..17de6f2b --- /dev/null +++ b/formal/promela/models/README.md @@ -0,0 +1,53 @@ +# RTEMS Promela Models + +`formal/promela/models/' + +This directory contains formal models written in Promela to support test generation. + +## Contributors + +* Andrew Butterfield +* Frédéric Tuong +* Robert Jennings +* Jerzy Jaśkuć +* Eoin Lynch + +## License + +This project is licensed under the +[BSD-2-Clause](https://spdx.org/licenses/BSD-2-Clause.html) or +[CC-BY-SA-4.0](https://spdx.org/licenses/CC-BY-SA-4.0.html). + +## Models Overview + +There are currently five models present. Four are test-generation ready, whilst the fifth is still work in progress. + +We identify the usual RTEMS name for the component, +the Promela "model-name", and the path to the model directory. + +* Barrier Manager: "barrier-mgr-model" `formal/promela/models/barriers` +* Chains API: "chains-api-model" `formal/promela/models/chains` +* Event Manager "event-mgr-model" `formal/promela/models/events` +* Message Manager "msg-mgr-model" `formal/promela/models/messages` +* MrsP Thread Queues "mrsp-threadq-model" `formal/promela/models/threadq` + +## Doing Test Generation + +Ensure that the virtual environment defined in `formal/promela/src/env` is active. + +We shall assume that the alias `tb` has been defined as suggested in `formal/promela/src/README.md`. + +Simply enter the relevant model sub-directory and invoke `tb` from the command line with desired command line arguments. + +A simple sequence that clears out all previously generated tests (from all models), clears all generated artifacts from this model, +and then does the whole test generation process is: + +``` +tb zero +tb clean +tb all +``` + +This will produce a test report in `-test.log`. + + diff --git a/formal/promela/src/README.md b/formal/promela/src/README.md new file mode 100644 index ..dd80420a --- /dev/null +++ b/formal/promela/src/README.md @@ -0,0 +1,71 @@ +# Test Generation Tools + +`formal/promela/src` + +This directory contains tools that use SPIN to do test generation
[PATCH 02/18] adds barrier manager model
--- formal/promela/models/barriers/README.md | 11 + formal/promela/models/barriers/STATUS.md | 95 ++ .../models/barriers/barrier-mgr-model-post.h | 44 + .../models/barriers/barrier-mgr-model-pre.h | 51 + .../models/barriers/barrier-mgr-model-rfn.yml | 169 +++ .../models/barriers/barrier-mgr-model-run.h | 91 ++ .../models/barriers/barrier-mgr-model.pml | 1158 + .../models/barriers/tc-barrier-mgr-model.c| 180 +++ .../models/barriers/tr-barrier-mgr-model.c| 249 .../models/barriers/tr-barrier-mgr-model.h| 197 +++ 10 files changed, 2245 insertions(+) create mode 100644 formal/promela/models/barriers/README.md create mode 100644 formal/promela/models/barriers/STATUS.md create mode 100644 formal/promela/models/barriers/barrier-mgr-model-post.h create mode 100644 formal/promela/models/barriers/barrier-mgr-model-pre.h create mode 100644 formal/promela/models/barriers/barrier-mgr-model-rfn.yml create mode 100644 formal/promela/models/barriers/barrier-mgr-model-run.h create mode 100644 formal/promela/models/barriers/barrier-mgr-model.pml create mode 100644 formal/promela/models/barriers/tc-barrier-mgr-model.c create mode 100644 formal/promela/models/barriers/tr-barrier-mgr-model.c create mode 100644 formal/promela/models/barriers/tr-barrier-mgr-model.h diff --git a/formal/promela/models/barriers/README.md b/formal/promela/models/barriers/README.md new file mode 100644 index ..5ed32946 --- /dev/null +++ b/formal/promela/models/barriers/README.md @@ -0,0 +1,11 @@ +# Barrier Manager model + +Developer: Jerzy Jaśkuć + +SPIN/Promela based test generation framework for RTEMS Barrier Manager + +This directory contains all of the necessary files needed to perform test generation for [RTEMS](https://www.rtems.org/ "RTEMS Homepage") [Barrier Manager](https://docs.rtems.org/branches/master/c-user/barrier/background.html "Barrier Manager") using SPIN/Promela framework. + +It is a subset of the material available at [Jerzy Jaśkuć's project repository](https://github.com/EZCodes/SPIN-PromelaRTEMSTestGen). + +These files were produced as a part of his research work done in Trinity College Dublin in partial fulfilment of the requirements for the degree of MCS in Integrated Computer Science. diff --git a/formal/promela/models/barriers/STATUS.md b/formal/promela/models/barriers/STATUS.md new file mode 100644 index ..5e8f52de --- /dev/null +++ b/formal/promela/models/barriers/STATUS.md @@ -0,0 +1,95 @@ +# BARRIER MANAGER status + +## 7th Nov 2022 COMPLETE + +* Platform: Dell G5, Ubuntu 20.04.5 LTS +* Generated: OK +* Compiles: OK +* Runs: OK +* All Tests Pass: OK + +See `barriers/archive/20221107-131233` + +## 7th Nov 2022 DIAGNOSIS + +Test cases 12 and 13 fail because there is a misinterpretation of how the +maximum number of barriers is determined. The actual configuration is set statically +in `ts-config.h` to be 7, as `TEST_MAXIMUM_BARRIERS`. In `ts-default.h`, this is used to set the +value of `CONFIGURE_MAXIMUM_BARRIERS`. This is not easily changed. + +The current Promela model only allows 2 barriers. + +## 5th Nov 2022 TEST FAIL + +* Platform: Dell G5, Ubuntu 20.04.5 LTS +* Generated: OK +* Compiles: OK +* Runs: OK +* All Tests Pass: No, 4 fail + +Log extract showing all four fails: + +``` +:0.19:0:WRK0/PML-BarrierMgr013:tr-barrier-mgr-model-13.c:185:RTEMS_SUCCESSFUL == RTEMS_TOO_MANY +F:*:0:RUN:*:*:RTEMS barrier leak (1) +E:RtemsModelBarrierMgr13:N:33:F:2:D:0.011053 + +F:0.21:0:WRK0/PML-BarrierMgr012:tr-barrier-mgr-model-12.c:203:RTEMS_SUCCESSFUL == RTEMS_TOO_MANY +F:*:0:RUN:*:*:RTEMS barrier leak (1) +E:RtemsModelBarrierMgr12:N:36:F:2:D:0.011254 +``` + +# 4th Nov 2022 TEST FAIL + +* Platform: Dell G5, Ubuntu 20.04.5 LTS +* Generated: OK +* Compiles: OK +* Runs: OK +* All Tests Pass: No, 27 fail + +Log extract showing representative sample: + +``` +F:0.7:0:RUN/PML-BarrierMgr000:tr-barrier-mgr-model-9.c:332:1 == 4 +F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4 +E:RtemsModelBarrierMgr9:N:33:F:2:D:0.012084 + +F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4 +E:RtemsModelBarrierMgr8:N:36:F:1:D:0.012003 + +F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4 +E:RtemsModelBarrierMgr14:N:37:F:1:D:0.012264 + +F:0.19:0:WRK0/PML-BarrierMgr013:tr-barrier-mgr-model-13.c:185:RTEMS_SUCCESSFUL == RTEMS_TOO_MANY +F:*:0:RUN:*:*:RTEMS barrier leak (1) +F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4 +E:RtemsModelBarrierMgr13:N:33:F:3:D:0.011301 + +F:0.21:0:WRK0/PML-BarrierMgr012:tr-barrier-mgr-model-12.c:203:RTEMS_SUCCESSFUL == RTEMS_TOO_MANY +F:*:0:RUN:*:*:RTEMS barrier leak (1) +F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4 +E:RtemsModelBarrierMgr12:N:36:F:3:D:0.011563 + +F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4 +E:RtemsModelBarrierMgr0:N:36:F:1:D:0.009776 +Z:Model0:C:22:N:757:F:27:D:0.246403 +Y:ReportHash:SHA256:H_j2zroRO1RaYJR3cZx9Bn68EfP5EBnpXZej6By5tIU= +cpu
[PATCH 04/18] adds chains API model
--- formal/promela/models/chains/.gitignore | 1 + formal/promela/models/chains/STATUS.md| 11 + .../models/chains/chains-api-model-post.h | 3 + .../models/chains/chains-api-model-pre.h | 43 .../models/chains/chains-api-model-rfn.yml| 64 ++ .../models/chains/chains-api-model-run.h | 18 ++ .../models/chains/chains-api-model.pml| 203 ++ .../models/chains/tr-chains-api-model.c | 70 ++ .../models/chains/tr-chains-api-model.h | 57 + 9 files changed, 470 insertions(+) create mode 100644 formal/promela/models/chains/.gitignore create mode 100644 formal/promela/models/chains/STATUS.md create mode 100644 formal/promela/models/chains/chains-api-model-post.h create mode 100644 formal/promela/models/chains/chains-api-model-pre.h create mode 100644 formal/promela/models/chains/chains-api-model-rfn.yml create mode 100644 formal/promela/models/chains/chains-api-model-run.h create mode 100644 formal/promela/models/chains/chains-api-model.pml create mode 100644 formal/promela/models/chains/tr-chains-api-model.c create mode 100644 formal/promela/models/chains/tr-chains-api-model.h diff --git a/formal/promela/models/chains/.gitignore b/formal/promela/models/chains/.gitignore new file mode 100644 index ..daa24295 --- /dev/null +++ b/formal/promela/models/chains/.gitignore @@ -0,0 +1 @@ +tr-model-chains-api-*.c diff --git a/formal/promela/models/chains/STATUS.md b/formal/promela/models/chains/STATUS.md new file mode 100644 index ..e45cc5d3 --- /dev/null +++ b/formal/promela/models/chains/STATUS.md @@ -0,0 +1,11 @@ +# CHAINS API status + +## 3rd Nov 2022 COMPLETE + +* Platform: Dell G5, Ubuntu 20.04.5 LTS +* Generated: OK +* Compiles: OK +* Runs: OK +* All Tests Pass: OK + +See `chains/archive/20221103-163702` diff --git a/formal/promela/models/chains/chains-api-model-post.h b/formal/promela/models/chains/chains-api-model-post.h new file mode 100644 index ..d826725d --- /dev/null +++ b/formal/promela/models/chains/chains-api-model-post.h @@ -0,0 +1,3 @@ +/* SPDX-License-Identifier: BSD-2-Clause */ + +/* post-amble empty for now */ diff --git a/formal/promela/models/chains/chains-api-model-pre.h b/formal/promela/models/chains/chains-api-model-pre.h new file mode 100644 index ..9816a5ad --- /dev/null +++ b/formal/promela/models/chains/chains-api-model-pre.h @@ -0,0 +1,43 @@ +/* SPDX-License-Identifier: BSD-2-Clause */ + +/** + * Chains API Model + * + * Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie) + * + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above + * copyright notice, this list of conditions and the following + * disclaimer in the documentation and/or other materials provided + * with the distribution. + * + * * Neither the name of the copyright holders nor the names of its + * contributors may be used to endorse or promote products derived + * from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT + * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, + * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT + * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + **/ + + +#include +#include +#include +#include "tr-chains-api-model.h" diff --git a/formal/promela/models/chains/chains-api-model-rfn.yml b/formal/promela/models/chains/chains-api-model-rfn.yml new file mode 100644 index ..103e32ce --- /dev/null +++ b/formal/promela/models/chains/chains-api-model-rfn.yml @@ -0,0 +1,64 @@ +# SPDX-License-Identifier: BSD-2-Clause +# Event Manager: Promela to RTEMS Refinement + +# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie) +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions +# are met: +# 1. Re
[PATCH 06/18] adds event manager model
---
formal/promela/models/events/.gitignore | 1 +
formal/promela/models/events/STATUS.md| 21 +
.../models/events/event-mgr-model-post.h | 8 +
.../models/events/event-mgr-model-pre.h | 51 ++
.../models/events/event-mgr-model-rfn.yml | 182
.../models/events/event-mgr-model-run.h | 164
.../promela/models/events/event-mgr-model.pml | 848 ++
.../models/events/tc-event-mgr-model.c| 358
.../models/events/tr-event-mgr-model.c| 257 ++
.../models/events/tr-event-mgr-model.h| 245 +
10 files changed, 2135 insertions(+)
create mode 100644 formal/promela/models/events/.gitignore
create mode 100644 formal/promela/models/events/STATUS.md
create mode 100644 formal/promela/models/events/event-mgr-model-post.h
create mode 100644 formal/promela/models/events/event-mgr-model-pre.h
create mode 100644 formal/promela/models/events/event-mgr-model-rfn.yml
create mode 100644 formal/promela/models/events/event-mgr-model-run.h
create mode 100644 formal/promela/models/events/event-mgr-model.pml
create mode 100644 formal/promela/models/events/tc-event-mgr-model.c
create mode 100644 formal/promela/models/events/tr-event-mgr-model.c
create mode 100644 formal/promela/models/events/tr-event-mgr-model.h
diff --git a/formal/promela/models/events/.gitignore
b/formal/promela/models/events/.gitignore
new file mode 100644
index ..a1fcab96
--- /dev/null
+++ b/formal/promela/models/events/.gitignore
@@ -0,0 +1 @@
+tr-model-events-mgr-*.c
diff --git a/formal/promela/models/events/STATUS.md
b/formal/promela/models/events/STATUS.md
new file mode 100644
index ..71518926
--- /dev/null
+++ b/formal/promela/models/events/STATUS.md
@@ -0,0 +1,21 @@
+# EVENT MANAGER status
+
+## 7th Nov 2022 COMPLETE
+
+* Platform: Dell G5, Ubuntu 20.04.5 LTS
+* Generated: OK
+* Compiles: OK
+* Runs: OK
+* All Tests Pass: OK
+
+See `events/archive/20221107-165035`
+
+## 3rd Nov 2022 COMPLETE
+
+* Platform: Dell G5, Ubuntu 20.04.5 LTS
+* Generated: OK
+* Compiles: OK
+* Runs: OK
+* All Tests Pass: OK
+
+See `events/archive/20221103-165851`
diff --git a/formal/promela/models/events/event-mgr-model-post.h
b/formal/promela/models/events/event-mgr-model-post.h
new file mode 100644
index ..df2738a4
--- /dev/null
+++ b/formal/promela/models/events/event-mgr-model-post.h
@@ -0,0 +1,8 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+static void Runner( RtemsModelEventsMgr_Context *ctx )
+{
+ T_log( T_NORMAL, "Runner running" );
+ TestSegment4( ctx );
+ T_log( T_NORMAL, "Runner finished" );
+}
diff --git a/formal/promela/models/events/event-mgr-model-pre.h
b/formal/promela/models/events/event-mgr-model-pre.h
new file mode 100644
index ..9a764a82
--- /dev/null
+++ b/formal/promela/models/events/event-mgr-model-pre.h
@@ -0,0 +1,51 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * @file
+ *
+ * @ingroup RTEMSTestCaseRtemsModelEventsMgr
+ */
+
+/*
+ * Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de)
+ *Trinity College Dublin (http://www.tcd.ie)
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ *notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ *notice, this list of conditions and the following disclaimer in the
+ *documentation and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ */
+
+/*
+ * This file was automatically generated. Do not edit it manually.
+ * Please have a look at
+ *
+ * https://docs.rtems.org/branches/master/eng/req/howto.html
+ *
+ * for information how to maintain and re-generate this file.
+ */
+
+#ifndef HAVE_CONFIG_H
+#include "config.h"
+#endif
+
+#include
+
+
+#include "tr-event-mgr-model.h"
diff --git a/formal/promela/models/events/event-mgr-model-rfn.yml
b/formal/promela/models/events/event-mgr-model-rfn.yml
new file mode 100644
index ..96727b88
--- /dev/null
+
[PATCH 08/18] adds message manager model
>From 4364f65705b387697c33181cb8a9a7b772ea7f58 Mon Sep 17 00:00:00 2001
From: Andrew Butterfield
Date: Wed, 21 Dec 2022 16:31:40 +
Subject: [PATCH 08/18] adds message manager model
---
formal/promela/models/messages/README.md | 10 +
formal/promela/models/messages/STATUS.md | 14 +
.../models/messages/msg-mgr-model-post.h | 8 +
.../models/messages/msg-mgr-model-pre.h | 51 ++
.../models/messages/msg-mgr-model-rfn.yml | 202 +
.../models/messages/msg-mgr-model-run.h | 191
.../promela/models/messages/msg-mgr-model.pml | 842 ++
.../models/messages/tc-msg-mgr-model.c| 211 +
.../models/messages/tr-msg-mgr-model.c| 240 +
.../models/messages/tr-msg-mgr-model.h| 132 +++
10 files changed, 1901 insertions(+)
create mode 100644 formal/promela/models/messages/README.md
create mode 100644 formal/promela/models/messages/STATUS.md
create mode 100644 formal/promela/models/messages/msg-mgr-model-post.h
create mode 100644 formal/promela/models/messages/msg-mgr-model-pre.h
create mode 100644 formal/promela/models/messages/msg-mgr-model-rfn.yml
create mode 100644 formal/promela/models/messages/msg-mgr-model-run.h
create mode 100644 formal/promela/models/messages/msg-mgr-model.pml
create mode 100644 formal/promela/models/messages/tc-msg-mgr-model.c
create mode 100644 formal/promela/models/messages/tr-msg-mgr-model.c
create mode 100644 formal/promela/models/messages/tr-msg-mgr-model.h
diff --git a/formal/promela/models/messages/README.md
b/formal/promela/models/messages/README.md
new file mode 100644
index ..2eb723b5
--- /dev/null
+++ b/formal/promela/models/messages/README.md
@@ -0,0 +1,10 @@
+# Message Manager model
+
+Developer: Eoin Lynch
+
+This directory contains the code for the generation/running of tests for the
[RTEMS Message
Manager](https://docs.rtems.org/branches/master/c-user/message/index.html)
+
+It is a subset of the material available at [Eoin Lynch's project
repository](https://github.com/lynche12/SPIN-PromelaTestGeneration).
+
+This project is research work done for his dissertation as part of the MAI in
Computer Engineering program at Trinity College Dublin
+
diff --git a/formal/promela/models/messages/STATUS.md
b/formal/promela/models/messages/STATUS.md
new file mode 100644
index ..361984c6
--- /dev/null
+++ b/formal/promela/models/messages/STATUS.md
@@ -0,0 +1,14 @@
+# MESSAGE MANAGER status
+
+## 3rd Nov 2022 TEST FAIL
+
+* Platform: Dell G5, Ubuntu 20.04.5 LTS
+* Generated: OK
+* Compiles: OK
+* Runs: OK
+* All Tests Pass: NO, 1 failure
+```
+F:0.17:0:"x/PML-MessageMgr022:tr-msg-mgr-model-22.c:192:RTEMS_SUCCESSFUL ==
RTEMS_TIMEOUT
+```
+
+See `events/archive/20221103-170322`
diff --git a/formal/promela/models/messages/msg-mgr-model-post.h
b/formal/promela/models/messages/msg-mgr-model-post.h
new file mode 100644
index ..9a9606d3
--- /dev/null
+++ b/formal/promela/models/messages/msg-mgr-model-post.h
@@ -0,0 +1,8 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+static void Runner( RtemsModelMessageMgr_Context *ctx )
+{
+ T_log( T_NORMAL, "Runner running" );
+ TestSegment3( ctx );
+ T_log( T_NORMAL, "Runner finished" );
+}
diff --git a/formal/promela/models/messages/msg-mgr-model-pre.h
b/formal/promela/models/messages/msg-mgr-model-pre.h
new file mode 100644
index ..f3986267
--- /dev/null
+++ b/formal/promela/models/messages/msg-mgr-model-pre.h
@@ -0,0 +1,51 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * @file
+ *
+ * @ingroup RTEMSTestCaseRtemsModelMessageMgr
+ */
+
+/*
+ * Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de)
+ *Trinity College Dublin (http://www.tcd.ie)
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ *notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ *notice, this list of conditions and the following disclaimer in the
+ *documentation and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF
[PATCH 10/18] adds weak memory models
--- .../models/threadq/Weak-Memory/RAM.pml| 48 + .../models/threadq/Weak-Memory/SPARC-TSO.pml | 198 ++ .../threadq/Weak-Memory/memory_model.pml | 60 ++ .../models/threadq/Weak-Memory/wmemory.pml| 74 +++ 4 files changed, 380 insertions(+) create mode 100644 formal/promela/models/threadq/Weak-Memory/RAM.pml create mode 100644 formal/promela/models/threadq/Weak-Memory/SPARC-TSO.pml create mode 100644 formal/promela/models/threadq/Weak-Memory/memory_model.pml create mode 100644 formal/promela/models/threadq/Weak-Memory/wmemory.pml diff --git a/formal/promela/models/threadq/Weak-Memory/RAM.pml b/formal/promela/models/threadq/Weak-Memory/RAM.pml new file mode 100644 index ..70851917 --- /dev/null +++ b/formal/promela/models/threadq/Weak-Memory/RAM.pml @@ -0,0 +1,48 @@ +/* SPDX-License-Identifier: BSD-2-Clause */ + +/** + * RAM + * + * Copyright (C) 2021 Trinity College Dublin (www.tcd.ie) + * + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above + * copyright notice, this list of conditions and the following + * disclaimer in the documentation and/or other materials provided + * with the distribution. + * + * * Neither the name of the copyright holders nor the names of its + * contributors may be used to endorse or promote products derived + * from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT + * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, + * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT + * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + **/ + +#ifndef _FORMAL_MEMORY_RAM +#define _FORMAL_MEMORY_RAM + + +// We assume a byte-memory +#define MEM_SIZE 8 +byte memory[MEM_SIZE] ; + + +#endif diff --git a/formal/promela/models/threadq/Weak-Memory/SPARC-TSO.pml b/formal/promela/models/threadq/Weak-Memory/SPARC-TSO.pml new file mode 100644 index ..d47e1284 --- /dev/null +++ b/formal/promela/models/threadq/Weak-Memory/SPARC-TSO.pml @@ -0,0 +1,198 @@ +/* SPDX-License-Identifier: BSD-2-Clause */ + +/** + * SPARC-TSO.pml + * + * Copyright (C) 2021 Trinity College Dublin (www.tcd.ie) + * + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above + * copyright notice, this list of conditions and the following + * disclaimer in the documentation and/or other materials provided + * with the distribution. + * + * * Neither the name of the copyright holders nor the names of its + * contributors may be used to endorse or promote products derived + * from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT + * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, + * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT + * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + **
[PATCH 12/18] third party code - promela parser
forked from https://github.com/johnyf/promela, commit 32d14184a50e920a92201058e4f601329be8c9c7 --- .../src/src/modules/promela_yacc/.gitignore | 20 + .../src/src/modules/promela_yacc/.travis.yml | 21 + .../src/src/modules/promela_yacc/LICENSE | 31 + .../src/src/modules/promela_yacc/MANIFEST.in |4 + .../src/src/modules/promela_yacc/README.md| 27 + .../src/src/modules/promela_yacc/doc.md | 100 ++ .../modules/promela_yacc/promela/__init__.py |6 + .../src/modules/promela_yacc/promela/ast.py | 1035 + .../src/modules/promela_yacc/promela/lex.py | 211 .../src/modules/promela_yacc/promela/yacc.py | 955 +++ .../src/src/modules/promela_yacc/setup.py | 65 ++ .../modules/promela_yacc/tests/yacc_test.py | 759 12 files changed, 3234 insertions(+) create mode 100644 formal/promela/src/src/modules/promela_yacc/.gitignore create mode 100644 formal/promela/src/src/modules/promela_yacc/.travis.yml create mode 100644 formal/promela/src/src/modules/promela_yacc/LICENSE create mode 100644 formal/promela/src/src/modules/promela_yacc/MANIFEST.in create mode 100644 formal/promela/src/src/modules/promela_yacc/README.md create mode 100644 formal/promela/src/src/modules/promela_yacc/doc.md create mode 100644 formal/promela/src/src/modules/promela_yacc/promela/__init__.py create mode 100644 formal/promela/src/src/modules/promela_yacc/promela/ast.py create mode 100644 formal/promela/src/src/modules/promela_yacc/promela/lex.py create mode 100644 formal/promela/src/src/modules/promela_yacc/promela/yacc.py create mode 100644 formal/promela/src/src/modules/promela_yacc/setup.py create mode 100644 formal/promela/src/src/modules/promela_yacc/tests/yacc_test.py diff --git a/formal/promela/src/src/modules/promela_yacc/.gitignore b/formal/promela/src/src/modules/promela_yacc/.gitignore new file mode 100644 index ..f4cd3f85 --- /dev/null +++ b/formal/promela/src/src/modules/promela_yacc/.gitignore @@ -0,0 +1,20 @@ +build/* +dist/* +promela/_version.py +*parsetab.py +.coverage +.DS_Store +Icon? + +*.*~ +__pycache__ +*.pyc +*.swp +*.pdf +*.PDF +*.txt +*.log +*.egg-info +*.html +*.css + diff --git a/formal/promela/src/src/modules/promela_yacc/.travis.yml b/formal/promela/src/src/modules/promela_yacc/.travis.yml new file mode 100644 index ..2fee40c9 --- /dev/null +++ b/formal/promela/src/src/modules/promela_yacc/.travis.yml @@ -0,0 +1,21 @@ +language: python + +python: + - 2.7 + - 3.4 + - 3.5 + - 3.6 + +install: + - sudo apt-get update -qq + - sudo apt-get install -y graphviz + - pip install --upgrade pip setuptools + - pip install -r requirements.txt + - pip install . + +script: + - cd tests/ + - nosetests --with-coverage --cover-package=promela + +after_success: + - coveralls diff --git a/formal/promela/src/src/modules/promela_yacc/LICENSE b/formal/promela/src/src/modules/promela_yacc/LICENSE new file mode 100644 index ..bebe3694 --- /dev/null +++ b/formal/promela/src/src/modules/promela_yacc/LICENSE @@ -0,0 +1,31 @@ +Copyright (c) 2014-2018 by California Institute of Technology +Copyright (c) 2014-2018 by Ioannis Filippidis +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + +1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + +3. Neither the name of the California Institute of Technology nor + the names of its contributors may be used to endorse or promote + products derived from this software without specific prior + written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL CALTECH OR THE +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/formal/promela/src/src/modules/promela_yacc/MANIFEST.in b/formal/promela/src/src/modules/promela_yacc/MANIFEST.in new file mode 100644 index ..bbacf5bf --- /dev/null +++ b/formal/promela/src/src/modules/promela_yacc/MANIFEST.in @@ -0,0 +1,4 @@ +include tests/*.py
[PATCH 13/18] modifies 3rd party code - promela parser
---
.../src/src/modules/promela_yacc/.gitignore | 20 -
.../src/src/modules/promela_yacc/.travis.yml | 21 -
.../src/src/modules/promela_yacc/LICENSE | 1 +
.../src/src/modules/promela_yacc/MANIFEST.in | 4 -
.../src/src/modules/promela_yacc/doc.md | 100 ---
.../src/modules/promela_yacc/promela/ast.py | 120 ++-
.../src/modules/promela_yacc/promela/lex.py | 18 +-
.../src/modules/promela_yacc/promela/yacc.py | 207 +++--
.../modules/promela_yacc/tests/yacc_test.py | 759 --
9 files changed, 228 insertions(+), 1022 deletions(-)
delete mode 100644 formal/promela/src/src/modules/promela_yacc/.gitignore
delete mode 100644 formal/promela/src/src/modules/promela_yacc/.travis.yml
delete mode 100644 formal/promela/src/src/modules/promela_yacc/MANIFEST.in
delete mode 100644 formal/promela/src/src/modules/promela_yacc/doc.md
delete mode 100644
formal/promela/src/src/modules/promela_yacc/tests/yacc_test.py
diff --git a/formal/promela/src/src/modules/promela_yacc/.gitignore
b/formal/promela/src/src/modules/promela_yacc/.gitignore
deleted file mode 100644
index f4cd3f85..
--- a/formal/promela/src/src/modules/promela_yacc/.gitignore
+++ /dev/null
@@ -1,20 +0,0 @@
-build/*
-dist/*
-promela/_version.py
-*parsetab.py
-.coverage
-.DS_Store
-Icon?
-
-*.*~
-__pycache__
-*.pyc
-*.swp
-*.pdf
-*.PDF
-*.txt
-*.log
-*.egg-info
-*.html
-*.css
-
diff --git a/formal/promela/src/src/modules/promela_yacc/.travis.yml
b/formal/promela/src/src/modules/promela_yacc/.travis.yml
deleted file mode 100644
index 2fee40c9..
--- a/formal/promela/src/src/modules/promela_yacc/.travis.yml
+++ /dev/null
@@ -1,21 +0,0 @@
-language: python
-
-python:
- - 2.7
- - 3.4
- - 3.5
- - 3.6
-
-install:
- - sudo apt-get update -qq
- - sudo apt-get install -y graphviz
- - pip install --upgrade pip setuptools
- - pip install -r requirements.txt
- - pip install .
-
-script:
- - cd tests/
- - nosetests --with-coverage --cover-package=promela
-
-after_success:
- - coveralls
diff --git a/formal/promela/src/src/modules/promela_yacc/LICENSE
b/formal/promela/src/src/modules/promela_yacc/LICENSE
index bebe3694..40f0a792 100644
--- a/formal/promela/src/src/modules/promela_yacc/LICENSE
+++ b/formal/promela/src/src/modules/promela_yacc/LICENSE
@@ -1,3 +1,4 @@
+Copyright (c) 2019-2021 by Trinity College Dublin, Ireland
Copyright (c) 2014-2018 by California Institute of Technology
Copyright (c) 2014-2018 by Ioannis Filippidis
All rights reserved.
diff --git a/formal/promela/src/src/modules/promela_yacc/MANIFEST.in
b/formal/promela/src/src/modules/promela_yacc/MANIFEST.in
deleted file mode 100644
index bbacf5bf..
--- a/formal/promela/src/src/modules/promela_yacc/MANIFEST.in
+++ /dev/null
@@ -1,4 +0,0 @@
-include tests/*.py
-include README.md
-include LICENSE
-include doc.md
diff --git a/formal/promela/src/src/modules/promela_yacc/doc.md
b/formal/promela/src/src/modules/promela_yacc/doc.md
deleted file mode 100644
index 02d73431..
--- a/formal/promela/src/src/modules/promela_yacc/doc.md
+++ /dev/null
@@ -1,100 +0,0 @@
-This package provides a lexer, parser, and abstract syntax tree (AST) for the
[Promela](http://en.wikipedia.org/wiki/Promela) modeling language.
-The lexer and parser are generated using
[PLY](https://pypi.python.org/pypi/ply/3.4) (Python `lex`-`yacc`).
-The [grammar](http://spinroot.com/spin/Man/grammar.html) is based on that used
in the [SPIN](http://spinroot.com/spin/whatispin.html) model checker (in the
files `spin.y` and `spinlex.c` of SPIN's source distribution), with
modifications where needed.
-
-To instantiate a Promela parser:
-
-```python
-from promela.yacc import Parser
-parser = Parser()
-```
-
-Then Promela code, as a string, can be parsed by:
-
-```python
-s = '''
-active proctype foo(){
- int x;
- do
- :: x = x + 1;
- od
-}
-'''
-program = parser.parse(s)
-```
-
-then
-
-```python
->>> print(program)
-active [1] proctype foo(){
- int x
- do
- :: x = (x + 1)
- od;
-}
-```
-
-The parser returns the result as an abstract syntax tree using classes from
the `promela.ast` module.
-The top production rule returns a `Program` instance, which itself is a `list`.
-The contents of this list
-
-There are two categories of AST classes: those that represent control flow
constructs:
-
-- `Proctype`, (`Init`, `NeverClaim`), `Node`, (`Expression`, `Assignment`,
`Assert`, `Options` (if, do), `Else`, `Break`, `Goto`, `Label`, `Call`,
`Return`, `Run`), `Sequence`
-
-and those that represent only syntax inside an expression:
-
-- `Terminal`, (`VarRef`, `Integer`, `Bool`), `Operator`, (`Binary`, `Unary`)
-
-The classes in parentheses are subclasses of the last class preceding the
parentheses.
-Each control flow class has a method `to_pg` that recursively converts the
abstract syntax tree to a program graph.
-
-A program graph is a directed graph whose edges are labeled with statements
from the program.
[PATCH 14/18] third party code - comment filter
forked from https://github.com/quic/comment-filter/commits/master commit 9cfb52318e5f71af56b5808e280a9b089b9abc32 --- .../comment-filter/.circleci/config.yml | 9 + .../src/modules/comment-filter/.coveragerc| 2 + .../src/src/modules/comment-filter/.gitignore | 104 + .../src/src/modules/comment-filter/AUTHORS| 7 + .../modules/comment-filter/CODE-OF-CONDUCT.md | 73 +++ .../modules/comment-filter/CONTRIBUTING.md| 87 .../src/src/modules/comment-filter/Dockerfile | 9 + .../src/src/modules/comment-filter/LICENSE| 13 + .../src/modules/comment-filter/MANIFEST.in| 7 + .../src/src/modules/comment-filter/README.md | 158 +++ .../src/modules/comment-filter/bin/comments | 25 ++ .../comment-filter/bin/testdata/hello.c | 8 + .../comment-filter/comment_filter/__init__.py | 1 + .../comment-filter/comment_filter/_version.py | 0 .../comment-filter/comment_filter/language.py | 60 +++ .../comment-filter/comment_filter/rfc.py | 423 ++ .../comment-filter/comment_filter/rfc_test.py | 258 +++ .../src/src/modules/comment-filter/setup.cfg | 5 + .../src/src/modules/comment-filter/setup.py | 12 + .../src/src/modules/comment-filter/tox.ini| 12 + 20 files changed, 1273 insertions(+) create mode 100644 formal/promela/src/src/modules/comment-filter/.circleci/config.yml create mode 100644 formal/promela/src/src/modules/comment-filter/.coveragerc create mode 100644 formal/promela/src/src/modules/comment-filter/.gitignore create mode 100644 formal/promela/src/src/modules/comment-filter/AUTHORS create mode 100644 formal/promela/src/src/modules/comment-filter/CODE-OF-CONDUCT.md create mode 100644 formal/promela/src/src/modules/comment-filter/CONTRIBUTING.md create mode 100644 formal/promela/src/src/modules/comment-filter/Dockerfile create mode 100644 formal/promela/src/src/modules/comment-filter/LICENSE create mode 100644 formal/promela/src/src/modules/comment-filter/MANIFEST.in create mode 100644 formal/promela/src/src/modules/comment-filter/README.md create mode 100755 formal/promela/src/src/modules/comment-filter/bin/comments create mode 100644 formal/promela/src/src/modules/comment-filter/bin/testdata/hello.c create mode 100644 formal/promela/src/src/modules/comment-filter/comment_filter/__init__.py create mode 100644 formal/promela/src/src/modules/comment-filter/comment_filter/_version.py create mode 100644 formal/promela/src/src/modules/comment-filter/comment_filter/language.py create mode 100644 formal/promela/src/src/modules/comment-filter/comment_filter/rfc.py create mode 100644 formal/promela/src/src/modules/comment-filter/comment_filter/rfc_test.py create mode 100644 formal/promela/src/src/modules/comment-filter/setup.cfg create mode 100644 formal/promela/src/src/modules/comment-filter/setup.py create mode 100644 formal/promela/src/src/modules/comment-filter/tox.ini diff --git a/formal/promela/src/src/modules/comment-filter/.circleci/config.yml b/formal/promela/src/src/modules/comment-filter/.circleci/config.yml new file mode 100644 index ..dc96c5c2 --- /dev/null +++ b/formal/promela/src/src/modules/comment-filter/.circleci/config.yml @@ -0,0 +1,9 @@ +version: 2 +jobs: + build: +docker: + - image: themattrix/tox +steps: + - checkout + - run: + command: tox diff --git a/formal/promela/src/src/modules/comment-filter/.coveragerc b/formal/promela/src/src/modules/comment-filter/.coveragerc new file mode 100644 index ..9b6154a0 --- /dev/null +++ b/formal/promela/src/src/modules/comment-filter/.coveragerc @@ -0,0 +1,2 @@ +[run] +omit = *_test.py diff --git a/formal/promela/src/src/modules/comment-filter/.gitignore b/formal/promela/src/src/modules/comment-filter/.gitignore new file mode 100644 index ..af2f5375 --- /dev/null +++ b/formal/promela/src/src/modules/comment-filter/.gitignore @@ -0,0 +1,104 @@ +# Byte-compiled / optimized / DLL files +__pycache__/ +*.py[cod] +*$py.class + +# C extensions +*.so + +# Distribution / packaging +.Python +build/ +develop-eggs/ +dist/ +downloads/ +eggs/ +.eggs/ +lib/ +lib64/ +parts/ +sdist/ +var/ +wheels/ +*.egg-info/ +.installed.cfg +*.egg +MANIFEST + +# PyInstaller +# Usually these files are written by a python script from a template +# before PyInstaller builds the exe, so as to inject date/other infos into it. +*.manifest +*.spec + +# Installer logs +pip-log.txt +pip-delete-this-directory.txt + +# Unit test / coverage reports +htmlcov/ +.tox/ +.coverage +.coverage.* +.cache +nosetests.xml +coverage.xml +*.cover +.hypothesis/ + +# Translations +*.mo +*.pot + +# Django stuff: +*.log +.static_storage/ +.media/ +local_settings.py + +# Flask stuff: +instance/ +.webassets-cache + +# Scrapy stuff: +.scrapy + +# Sphinx documentation +docs/_build/ + +# PyBuilder +target/ + +# Jupyter Notebook +.ipynb_checkpoints + +# pyenv +.python-version + +# celery beat schedule file +celerybeat-schedule +
[PATCH 15/18] modifies 3rd party code - comment filter
--- .../comment-filter/.circleci/config.yml | 9 - .../src/modules/comment-filter/.coveragerc| 2 - .../src/src/modules/comment-filter/.gitignore | 104 --- .../modules/comment-filter/CODE-OF-CONDUCT.md | 73 - .../modules/comment-filter/CONTRIBUTING.md| 87 -- .../src/src/modules/comment-filter/Dockerfile | 9 - .../src/src/modules/comment-filter/LICENSE| 4 +- .../src/modules/comment-filter/MANIFEST.in| 7 - .../src/modules/comment-filter/bin/comments | 25 -- .../comment-filter/bin/testdata/hello.c | 8 - .../comment-filter/comment_filter/_version.py | 0 .../comment-filter/comment_filter/language.py | 14 +- .../comment-filter/comment_filter/rfc.py | 62 +++-- .../comment-filter/comment_filter/rfc_test.py | 258 -- 14 files changed, 42 insertions(+), 620 deletions(-) delete mode 100644 formal/promela/src/src/modules/comment-filter/.circleci/config.yml delete mode 100644 formal/promela/src/src/modules/comment-filter/.coveragerc delete mode 100644 formal/promela/src/src/modules/comment-filter/.gitignore delete mode 100644 formal/promela/src/src/modules/comment-filter/CODE-OF-CONDUCT.md delete mode 100644 formal/promela/src/src/modules/comment-filter/CONTRIBUTING.md delete mode 100644 formal/promela/src/src/modules/comment-filter/Dockerfile delete mode 100644 formal/promela/src/src/modules/comment-filter/MANIFEST.in delete mode 100755 formal/promela/src/src/modules/comment-filter/bin/comments delete mode 100644 formal/promela/src/src/modules/comment-filter/bin/testdata/hello.c delete mode 100644 formal/promela/src/src/modules/comment-filter/comment_filter/_version.py delete mode 100644 formal/promela/src/src/modules/comment-filter/comment_filter/rfc_test.py diff --git a/formal/promela/src/src/modules/comment-filter/.circleci/config.yml b/formal/promela/src/src/modules/comment-filter/.circleci/config.yml deleted file mode 100644 index dc96c5c2.. --- a/formal/promela/src/src/modules/comment-filter/.circleci/config.yml +++ /dev/null @@ -1,9 +0,0 @@ -version: 2 -jobs: - build: -docker: - - image: themattrix/tox -steps: - - checkout - - run: - command: tox diff --git a/formal/promela/src/src/modules/comment-filter/.coveragerc b/formal/promela/src/src/modules/comment-filter/.coveragerc deleted file mode 100644 index 9b6154a0.. --- a/formal/promela/src/src/modules/comment-filter/.coveragerc +++ /dev/null @@ -1,2 +0,0 @@ -[run] -omit = *_test.py diff --git a/formal/promela/src/src/modules/comment-filter/.gitignore b/formal/promela/src/src/modules/comment-filter/.gitignore deleted file mode 100644 index af2f5375.. --- a/formal/promela/src/src/modules/comment-filter/.gitignore +++ /dev/null @@ -1,104 +0,0 @@ -# Byte-compiled / optimized / DLL files -__pycache__/ -*.py[cod] -*$py.class - -# C extensions -*.so - -# Distribution / packaging -.Python -build/ -develop-eggs/ -dist/ -downloads/ -eggs/ -.eggs/ -lib/ -lib64/ -parts/ -sdist/ -var/ -wheels/ -*.egg-info/ -.installed.cfg -*.egg -MANIFEST - -# PyInstaller -# Usually these files are written by a python script from a template -# before PyInstaller builds the exe, so as to inject date/other infos into it. -*.manifest -*.spec - -# Installer logs -pip-log.txt -pip-delete-this-directory.txt - -# Unit test / coverage reports -htmlcov/ -.tox/ -.coverage -.coverage.* -.cache -nosetests.xml -coverage.xml -*.cover -.hypothesis/ - -# Translations -*.mo -*.pot - -# Django stuff: -*.log -.static_storage/ -.media/ -local_settings.py - -# Flask stuff: -instance/ -.webassets-cache - -# Scrapy stuff: -.scrapy - -# Sphinx documentation -docs/_build/ - -# PyBuilder -target/ - -# Jupyter Notebook -.ipynb_checkpoints - -# pyenv -.python-version - -# celery beat schedule file -celerybeat-schedule - -# SageMath parsed files -*.sage.py - -# Environments -.env -.venv -env/ -venv/ -ENV/ -env.bak/ -venv.bak/ - -# Spyder project settings -.spyderproject -.spyproject - -# Rope project settings -.ropeproject - -# mkdocs documentation -/site - -# mypy -.mypy_cache/ diff --git a/formal/promela/src/src/modules/comment-filter/CODE-OF-CONDUCT.md b/formal/promela/src/src/modules/comment-filter/CODE-OF-CONDUCT.md deleted file mode 100644 index 7ef343f5.. --- a/formal/promela/src/src/modules/comment-filter/CODE-OF-CONDUCT.md +++ /dev/null @@ -1,73 +0,0 @@ -# Contributor Covenant Code of Conduct - -## Our Pledge - -In the interest of fostering an open and welcoming environment, we as -contributors and maintainers pledge to making participation in our project and -our community a harassment-free experience for everyone, regardless of age, body -size, disability, ethnicity, gender identity and expression, level of experience, -nationality, personal appearance, race, religion, or sexual identity and -orientation. - -## Our Standards - -Examples of behavior that contributes to creating a positive environment -include: - -* Using welco
[PATCH 18/18] adds automatic testgen examples
---
formal/promela/src/examples/draft/make.sh | 77 +++
formal/promela/src/examples/draft/parse.pml | 129 ++
.../src/examples/model_checker/spin.pml | 8 ++
formal/promela/src/examples/requirements.txt | 35 +
4 files changed, 249 insertions(+)
create mode 100644 formal/promela/src/examples/draft/make.sh
create mode 100644 formal/promela/src/examples/draft/parse.pml
create mode 100644 formal/promela/src/examples/model_checker/spin.pml
create mode 100644 formal/promela/src/examples/requirements.txt
diff --git a/formal/promela/src/examples/draft/make.sh
b/formal/promela/src/examples/draft/make.sh
new file mode 100644
index ..b4da0981
--- /dev/null
+++ b/formal/promela/src/examples/draft/make.sh
@@ -0,0 +1,77 @@
+#!/bin/bash
+
+# SPDX-License-Identifier: BSD-3-Clause
+# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+
+set -e
+set -x
+
+##
+
+HOME0="$(dirname "$(python3 -c "import os; print(os.path.realpath('$0'))")")"
+cd "$HOME0"
+
+##
+
+pip_check_test='true'
+function pip_check () {
+if [ "$pip_check_test" ] ; then
+ set +e
+ version=$(pip3 show "$1")
+ st="$?"
+ set -e
+ [ "$st" = 0 ] || (echo '`'"pip3 show $1"'`'" failed: "'`'"pip3 install
$1"'`' && exit "$st")
+
+ version=$(echo "$version" | grep -m 1 Version | cut -d ' ' -f 2)
+set +x
+ [ "$version" = "$2" ] || (echo "$1 version $version installed instead
of $2: "'`'"pip3 install $1==$2"'`' && echo -n "Continue? (ENTER/CTRL+C): " &&
read)
+set -x
+fi
+}
+
+# The compilation will require the installation of these libraries:
+
+pip_check coconut 1.4.3
+pip_check mypy 0.761
+
+coconut --target 3 library.coco --mypy --ignore-missing-imports
--allow-redefinition
+coconut --target 3 syntax_pml.coco --mypy --ignore-missing-imports
--allow-redefinition
+coconut --target 3 syntax_yaml.coco --mypy --ignore-missing-imports
--allow-redefinition
+coconut --target 3 syntax_ml.coco --mypy --ignore-missing-imports
--allow-redefinition
+coconut --target 3 refine_command.coco refine_command.py
+coconut --target 3 testgen.coco --mypy --follow-imports silent
--ignore-missing-imports --allow-redefinition
+
+##
+
+# as well as all dependencies of ( https://github.com/johnyf/promela ):
+
+pip_check promela 0.0.2
+
+# The above command was mainly executed to install dependencies of the package.
+
+## git clone g...@gitlab.scss.tcd.ie:tuongf/promela_yacc.git # see also
deliverables/FV2-201/wip/ftuong/src_ext
+
+##
+
+# Additionally, we use a library to do various operations on C-style comments
( https://github.com/codeauroraforum/comment-filter ):
+
+## git clone g...@gitlab.scss.tcd.ie:tuongf/comment-filter.git # see also
deliverables/FV2-201/wip/ftuong/src_ext
+
+# We also modify $PYTHONPATH (so that the library can be used, at least while
mypy is executing):
+
+export PYTHONPATH=`pwd`/comment-filter
+
+##
+
+# At run-time, we will need these libraries:
+
+pip_check parsec 3.5
+## apt install spin # 6.4.6+dfsg-2
+
+##
+
+cd -
+
+# Finally, the main execution proceeds as follows:
+
+exec python3 "$HOME0/testgen.py" "$@"
diff --git a/formal/promela/src/examples/draft/parse.pml
b/formal/promela/src/examples/draft/parse.pml
new file mode 100644
index ..ec86d1fd
--- /dev/null
+++ b/formal/promela/src/examples/draft/parse.pml
@@ -0,0 +1,129 @@
+/**
+ * FV2-201
+ *
+ * Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+ *
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * * Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * * Redistributions in binary form must reproduce the above
+ * copyright notice, this list of conditions and the following
+ * disclaimer in the documentation and/or other materials provided
+ * with the distribution.
+ *
+ * * Neither the name of the copyright holders nor the names of its
+ * contributors may be used to endorse or promote products derived
+ * from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHE
[PATCH v2 2/3] spec/build/riscv: Start all riscv/riscv BSPs at 0x80000000
From: Hesham Almatary To follow other RISC-V-based OSes conventions. Delete generic BSPs that start at 0x7000 as BSPs are now medany by default. Updates #4775 --- spec/build/bsps/riscv/optrambegin.yml | 6 -- 1 file changed, 6 deletions(-) diff --git a/spec/build/bsps/riscv/optrambegin.yml b/spec/build/bsps/riscv/optrambegin.yml index 90133411cf..8890334915 100644 --- a/spec/build/bsps/riscv/optrambegin.yml +++ b/spec/build/bsps/riscv/optrambegin.yml @@ -10,12 +10,6 @@ copyrights: - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) default: 2147483648 default-by-variant: -- value: 2147483648 - variants: - - riscv/rv64.*medany -- value: 1879048192 - variants: - - riscv/rv64.* - value: 0 variants: - riscv/noel.* -- 2.25.1 ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
[PATCH v2 1/3] spec/build/riscv: Default rv64* BSPs to medany cmodel
From: Hesham Almatary Currently generic RISC-V BSPs (riscv/riscv) that start with rv64 and not rv64*_medany will start at 0x7000. This adds high maintenance overhead and deviates from almost all other RISC-V-based OSes and baremetal programs that start at 0x8000. Further, testing now has to account for an extra parameter (medany or not) that doubles the number of BSPs need to be tested. This commit defaults all RV64 BSPs to use medany code model to allow starting all BSPs at 0x8000. BSPs that require different code models and/or start addresses are custom and need to add their own entries. Updates #4775 --- spec/build/bsps/riscv/riscv/abi.yml | 13 ++--- .../bsps/riscv/riscv/bsprv64imacmedany.yml| 19 --- .../bsps/riscv/riscv/bsprv64imafdcmedany.yml | 19 --- .../bsps/riscv/riscv/bsprv64imafdmedany.yml | 19 --- 4 files changed, 2 insertions(+), 68 deletions(-) delete mode 100644 spec/build/bsps/riscv/riscv/bsprv64imacmedany.yml delete mode 100644 spec/build/bsps/riscv/riscv/bsprv64imafdcmedany.yml delete mode 100644 spec/build/bsps/riscv/riscv/bsprv64imafdmedany.yml diff --git a/spec/build/bsps/riscv/riscv/abi.yml b/spec/build/bsps/riscv/riscv/abi.yml index 3ef8b0681d..29dd7b449d 100644 --- a/spec/build/bsps/riscv/riscv/abi.yml +++ b/spec/build/bsps/riscv/riscv/abi.yml @@ -21,21 +21,17 @@ default-by-variant: - -mabi=lp64d - -mcmodel=medany variants: - - riscv/rv64imafdc_medany -- value: - - -march=rv64imafdc - - -mabi=lp64d - variants: - riscv/rv64imafdc - value: - -march=rv64imafd - -mabi=lp64d - -mcmodel=medany variants: - - riscv/rv64imafd_medany + - riscv/rv64imafd - value: - -march=rv64imafd - -mabi=lp64d + - -mcmodel=medany variants: - riscv/rv64imafd - value: @@ -43,11 +39,6 @@ default-by-variant: - -mabi=lp64 - -mcmodel=medany variants: - - riscv/rv64imac_medany -- value: - - -march=rv64imac - - -mabi=lp64 - variants: - riscv/rv64imac - value: [] variants: diff --git a/spec/build/bsps/riscv/riscv/bsprv64imacmedany.yml b/spec/build/bsps/riscv/riscv/bsprv64imacmedany.yml deleted file mode 100644 index c0db3e0720..00 --- a/spec/build/bsps/riscv/riscv/bsprv64imacmedany.yml +++ /dev/null @@ -1,19 +0,0 @@ -SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause -arch: riscv -bsp: rv64imac_medany -build-type: bsp -cflags: [] -copyrights: -- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) -cppflags: [] -enabled-by: true -family: riscv -includes: [] -install: [] -links: -- role: build-dependency - uid: ../../opto2 -- role: build-dependency - uid: grp -source: [] -type: build diff --git a/spec/build/bsps/riscv/riscv/bsprv64imafdcmedany.yml b/spec/build/bsps/riscv/riscv/bsprv64imafdcmedany.yml deleted file mode 100644 index e4ecd4736a..00 --- a/spec/build/bsps/riscv/riscv/bsprv64imafdcmedany.yml +++ /dev/null @@ -1,19 +0,0 @@ -SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause -arch: riscv -bsp: rv64imafdc_medany -build-type: bsp -cflags: [] -copyrights: -- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) -cppflags: [] -enabled-by: true -family: riscv -includes: [] -install: [] -links: -- role: build-dependency - uid: ../../opto2 -- role: build-dependency - uid: grp -source: [] -type: build diff --git a/spec/build/bsps/riscv/riscv/bsprv64imafdmedany.yml b/spec/build/bsps/riscv/riscv/bsprv64imafdmedany.yml deleted file mode 100644 index 9e01572c70..00 --- a/spec/build/bsps/riscv/riscv/bsprv64imafdmedany.yml +++ /dev/null @@ -1,19 +0,0 @@ -SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause -arch: riscv -bsp: rv64imafd_medany -build-type: bsp -cflags: [] -copyrights: -- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) -cppflags: [] -enabled-by: true -family: riscv -includes: [] -install: [] -links: -- role: build-dependency - uid: ../../opto2 -- role: build-dependency - uid: grp -source: [] -type: build -- 2.25.1 ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
[PATCH v2 3/3] RISC-V: Always probe for HTIF and remove RISCV_ENABLE_HTIF_SUPPORT
From: Hesham Almatary
Updates #4779
---
bsps/riscv/noel/include/bsp/riscv.h | 2 --
bsps/riscv/riscv/console/console-config.c | 10 ++
bsps/riscv/riscv/console/htif.c | 4
bsps/riscv/riscv/include/bsp/riscv.h | 2 --
bsps/riscv/riscv/irq/irq.c| 15 +--
bsps/riscv/riscv/start/bsp_fatal_halt.c | 11 +++
6 files changed, 18 insertions(+), 26 deletions(-)
diff --git a/bsps/riscv/noel/include/bsp/riscv.h
b/bsps/riscv/noel/include/bsp/riscv.h
index 8ac049bb7c..3ab75573f0 100644
--- a/bsps/riscv/noel/include/bsp/riscv.h
+++ b/bsps/riscv/noel/include/bsp/riscv.h
@@ -50,9 +50,7 @@ extern uint32_t riscv_hart_count;
uint32_t riscv_get_hart_index_by_phandle(uint32_t phandle);
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
void htif_poweroff(void);
-#endif
#ifdef __cplusplus
}
diff --git a/bsps/riscv/riscv/console/console-config.c
b/bsps/riscv/riscv/console/console-config.c
index 7908c2f325..fe339c2353 100644
--- a/bsps/riscv/riscv/console/console-config.c
+++ b/bsps/riscv/riscv/console/console-config.c
@@ -60,9 +60,7 @@
static fe310_uart_context fe310_uart_instance;
#endif
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
static htif_console_context htif_console_instance;
-#endif
#if RISCV_CONSOLE_MAX_NS16550_DEVICES > 0
static ns16550_context ns16550_instances[RISCV_CONSOLE_MAX_NS16550_DEVICES];
@@ -165,7 +163,7 @@ static void riscv_console_probe(void)
compat_len = 0;
}
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
+/* Search for HTIF (eg. on Spike) and use it if found */
if (fdt_stringlist_contains(compat, compat_len, "ucb,htif0")) {
htif_console_context_init(&htif_console_instance.base, node);
@@ -173,7 +171,6 @@ static void riscv_console_probe(void)
riscv_console.putchar = htif_console_putchar;
riscv_console.getchar = htif_console_getchar;
};
-#endif
#if RISCV_CONSOLE_MAX_NS16550_DEVICES > 0
if (
@@ -280,10 +277,9 @@ rtems_status_code console_initialize(
void *arg
)
{
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
rtems_termios_device_context *base;
char htif_path[] = "/dev/ttyShtif";
-#endif
+
#if RISCV_CONSOLE_MAX_NS16550_DEVICES > 0
char path[] = "/dev/ttyS?";
size_t i;
@@ -296,14 +292,12 @@ rtems_status_code console_initialize(
rtems_termios_initialize();
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
base = &htif_console_instance.base;
rtems_termios_device_install(htif_path, &htif_console_handler, NULL, base);
if (base == riscv_console.context) {
link(htif_path, CONSOLE_DEVICE_NAME);
}
-#endif
#if RISCV_CONSOLE_MAX_NS16550_DEVICES > 0
for (i = 0; i < RISCV_CONSOLE_MAX_NS16550_DEVICES; ++i) {
diff --git a/bsps/riscv/riscv/console/htif.c b/bsps/riscv/riscv/console/htif.c
index bcfe6a5db5..750abe6e3e 100644
--- a/bsps/riscv/riscv/console/htif.c
+++ b/bsps/riscv/riscv/console/htif.c
@@ -29,8 +29,6 @@
#include
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
-
#include
#include
@@ -139,5 +137,3 @@ const rtems_termios_device_handler htif_console_handler = {
.poll_read = htif_console_getchar,
.mode = TERMIOS_POLLED
};
-
-#endif /* RISCV_ENABLE_HTIF_SUPPORT */
diff --git a/bsps/riscv/riscv/include/bsp/riscv.h
b/bsps/riscv/riscv/include/bsp/riscv.h
index d38f46c069..a11ae4291e 100644
--- a/bsps/riscv/riscv/include/bsp/riscv.h
+++ b/bsps/riscv/riscv/include/bsp/riscv.h
@@ -52,9 +52,7 @@ extern uint32_t riscv_hart_count;
uint32_t riscv_get_hart_index_by_phandle(uint32_t phandle);
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
void htif_poweroff(void);
-#endif
#ifdef __cplusplus
}
diff --git a/bsps/riscv/riscv/irq/irq.c b/bsps/riscv/riscv/irq/irq.c
index 3ef06a16bd..f0ccc6f5f0 100644
--- a/bsps/riscv/riscv/irq/irq.c
+++ b/bsps/riscv/riscv/irq/irq.c
@@ -247,13 +247,16 @@ static void riscv_plic_init(const void *fdt)
node = fdt_node_offset_by_compatible(fdt, -1, "riscv,plic0");
plic = riscv_fdt_get_address(fdt, node);
+
if (plic == NULL) {
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
-/* Spike platform has HTIF and does not have a PLIC */
-return;
-#else
-bsp_fatal(RISCV_FATAL_NO_PLIC_REG_IN_DEVICE_TREE);
-#endif
+ node = fdt_node_offset_by_compatible(fdt, -1, "ucb,htif0");
+
+ /* Spike platform has HTIF and does not have a PLIC */
+ if (node != -1) {
+ return;
+ } else {
+ bsp_fatal(RISCV_FATAL_NO_PLIC_REG_IN_DEVICE_TREE);
+ }
}
riscv_plic = plic;
diff --git a/bsps/riscv/riscv/start/bsp_fatal_halt.c
b/bsps/riscv/riscv/start/bsp_fatal_halt.c
index fb0787c606..cd7c5f20c5 100644
--- a/bsps/riscv/riscv/start/bsp_fatal_halt.c
+++ b/bsps/riscv/riscv/start/bsp_fatal_halt.c
@@ -38,14 +38,17 @@ void _CPU_Fatal_halt( uint32_t source, CPU_Uint32ptr error )
int node;
volatile uint32_t *sifive_test;
-#if RISCV_ENABLE_HTIF_SUPPORT != 0
- htif_poweroff();
-#endif
+ fdt = bsp_fdt_get();
+
+ node = fdt_node_offset_by_compatible(fdt, -1, "ucb,htif0");
+
+ if (node != -1)
+ htif_poweroff();
+
#if RISCV_E
Re: [PATCH v2 1/3] spec/build/riscv: Default rv64* BSPs to medany cmodel
On 22/12/2022 13:22, heshamelmat...@gmail.com wrote: From: Hesham Almatary Currently generic RISC-V BSPs (riscv/riscv) that start with rv64 and not rv64*_medany will start at 0x7000. This adds high maintenance overhead and deviates from almost all other RISC-V-based OSes and baremetal programs that start at 0x8000. Further, testing now has to account for an extra parameter (medany or not) that doubles the number of BSPs need to be tested. This commit defaults all RV64 BSPs to use medany code model to allow starting all BSPs at 0x8000. BSPs that require different code models and/or start addresses are custom and need to add their own entries. Updates #4775 Thanks, the patch set looks good. -- embedded brains GmbH Herr Sebastian HUBER Dornierstr. 4 82178 Puchheim Germany email: sebastian.hu...@embedded-brains.de phone: +49-89-18 94 741 - 16 fax: +49-89-18 94 741 - 08 Registergericht: Amtsgericht München Registernummer: HRB 157899 Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler Unsere Datenschutzerklärung finden Sie hier: https://embedded-brains.de/datenschutzerklaerung/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: [PATCH 1/2] bsps: Import xilinx support code
On Thu, Dec 22, 2022 at 12:58 AM Sebastian Huber <
sebastian.hu...@embedded-brains.de> wrote:
> On 21/12/2022 21:54, Kinsey Moore wrote:
> > +includes:
> > +- bsps/include/xilinx_support/
> > +- bsps/include/xilinx_support/${XIL_SUPPORT_PATH}/
>
> Is the xilinx_support a name from you or Xilinx? Maybe just name it
> xilinx or xil to make the paths shorter.
>
> Could you please add a notice to the commit message from where you
> obtained the files and some version information. This is helpful if you
> want to update the code at some point in time. If it is imported from a
> Git repository, a file like this is useful: cpukit/dtc/VERSION.
>
Those were added by my choice. I'll shorten them and add the requested
version information in v2. I mentioned part of it in 2/2, but better to
have it in both.
Thanks,
Kinsey
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel
Re: [PATCH] rtems_shell_main_mmove problem
Bump On Wed, 14 Dec 2022 at 20:12, zack leung wrote: > Closes #4556 > --- > cpukit/libmisc/shell/main_mmove.c | 2 +- > 1 file changed, 1 insertion(+), 1 deletion(-) > > diff --git a/cpukit/libmisc/shell/main_mmove.c > b/cpukit/libmisc/shell/main_mmove.c > index 38731b10a2..0029882d62 100644 > --- a/cpukit/libmisc/shell/main_mmove.c > +++ b/cpukit/libmisc/shell/main_mmove.c > @@ -62,7 +62,7 @@ static int rtems_shell_main_mmove( >/* > * Now copy the memory. > */ > - memcpy(dst, src, length); > + memmove(dst, src, length); > > return 0; > } > -- > 2.38.1 > ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: [PATCH v2 1/2] bsps: Import Xilinx support code
On 22/12/2022 19:56, Kinsey Moore wrote: This support code is necessary for many Xilinx-provided bare metal device drivers supported on ARM, AArch64, and MicroBlaze platforms. Support for all of these architectures is kept under bsps/include due to multiple architecture variants being supported which requires complex logic in the build system. The imported files are and should be able to remain unmodified. Import information is kept in bsps/shared/xil/VERSION. Thanks, looks good. -- embedded brains GmbH Herr Sebastian HUBER Dornierstr. 4 82178 Puchheim Germany email: sebastian.hu...@embedded-brains.de phone: +49-89-18 94 741 - 16 fax: +49-89-18 94 741 - 08 Registergericht: Amtsgericht München Registernummer: HRB 157899 Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler Unsere Datenschutzerklärung finden Sie hier: https://embedded-brains.de/datenschutzerklaerung/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
