Chains API model and test gen material

8 files changed, 459 insertions, 0 deletions

diff --git a/formal/promela/models/chains/.gitignore b/formal/promela/models/chains/.gitignore
new file mode 100644
index 00000000..daa24295
--- /dev/null
+++ b/formal/promela/models/chains/.gitignore
@@ -0,0 +1 @@
+tr-model-chains-api-*.c
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 00000000..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 00000000..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 <rtems.h>
+#include <rtems/test.h>
+#include <rtems/chain.h>
+#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 00000000..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. 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.
+
+NAME: |
+  const char rtems_test_name[] = "Model_Chain_API";
+
+memory_DCL: item {0}[{1}];
+
+nptr_DCL: item *
+
+chain_DCL: rtems_chain_control
+
+INIT: rtems_chain_initialize_empty( &chain );
+
+append: |
+  memory[{1}].val = {0};
+  rtems_chain_append_unprotected( &chain, (rtems_chain_node*)&memory[{1}] );
+
+getNonNull: |
+  nptr = get_item( &chain );
+  T_eq_ptr( nptr, &memory[{0}] );
+
+nptr: T_eq_ptr( nptr, &memory[{0}] );
+
+nptr_PTR: |
+  T_eq_ptr( nptr, NULL );
+  T_eq_ptr( nptr, &memory[{0}] );
+
+itm_FSCALAR:   T_eq_int( {0}->val, {1} );
+
+nxt_FPTR: |
+  T_eq_ptr( {0}->node.next->next, NULL );
+  T_eq_ptr( {0}->node.next, &memory[{1}] );
+
+prv_FPTR: |
+  T_eq_ptr( {0}->node.previous->previous, NULL );
+  T_eq_ptr( {0}->node.previous, &memory[{1}] );
+
+chain_SEQ: |
+  show_chain( &chain, ctx->buffer );
+  T_eq_str( ctx->buffer, "{0} 0" );
diff --git a/formal/promela/models/chains/chains-api-model-run.h b/formal/promela/models/chains/chains-api-model-run.h
new file mode 100644
index 00000000..292718ee
--- /dev/null
+++ b/formal/promela/models/chains/chains-api-model-run.h
@@ -0,0 +1,18 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+void RtemsModelChainsAPI_Run{0}(
+)
+{{
+  Context ctx;
+
+  memset( &ctx, 0, sizeof( ctx ) );
+
+  T_set_verbosity( T_NORMAL );
+
+  TestSegment0( &ctx );
+}}
+
+T_TEST_CASE( RtemsModelChainAPI{0} )
+{{
+  RtemsModelChainsAPI_Run{0}( );
+}}
diff --git a/formal/promela/models/chains/chains-api-model.pml b/formal/promela/models/chains/chains-api-model.pml
new file mode 100644
index 00000000..b76a8628
--- /dev/null
+++ b/formal/promela/models/chains/chains-api-model.pml
@@ -0,0 +1,203 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/******************************************************************************
+ * chains-api-model.pml
+ *
+ * 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.
+ ******************************************************************************/
+
+// Sizings, MEM_SIZE = 2 ** PTR_SIZE
+#define PTR_SIZE 3
+#define MEM_SIZE 8
+
+// Nodes types
+typedef Node {
+  unsigned nxt  : PTR_SIZE
+; unsigned prv  : PTR_SIZE
+; byte     itm
+}
+
+inline ncopy (dst,src) {
+  dst.nxt = src.nxt; dst.prv=src.prv; dst.itm = src.itm
+}
+
+// Memory
+Node memory[MEM_SIZE] ;
+unsigned nptr : PTR_SIZE ;  // one node pointer
+
+// We ignore pointer values here as their values depend on $RTEMS_DEBUG
+inline show_node (){
+   atomic{
+     printf("@@@ 0 PTR nptr %d\n",nptr);
+     if
+     :: nptr -> printf("@@@ 0 STRUCT nptr\n");
+                // printf("@@@ 0 PTR nxt %d\n", memory[nptr].nxt);
+                // printf("@@@ 0 PTR prv %d\n", memory[nptr].prv);
+                printf("@@@ 0 SCALAR itm %d\n", memory[nptr].itm);
+                printf("@@@ 0 END nptr\n")
+     :: else -> skip
+     fi
+   }
+}
+
+typedef Control {
+  unsigned head : PTR_SIZE
+; unsigned tail : PTR_SIZE
+; unsigned size : PTR_SIZE
+}
+
+Control chain ; // one chain
+
+
+inline show_chain () {
+   int cnp;
+   atomic{
+     cnp = chain.head;
+     printf("@@@ 0 SEQ chain\n");
+     do
+       :: (cnp == 0) -> break;
+       :: (cnp != 0) ->
+            printf("@@@ 0 SCALAR _ %d\n",memory[cnp].itm);
+            cnp = memory[cnp].nxt
+     od
+     printf("@@@ 0 END chain\n");
+   }
+}
+
+inline append(ch,np) {
+  assert(np!=0);
+  assert(ch.size < 7);
+  if
+    :: (ch.head == 0) ->
+         ch.head = np;
+         ch.tail = np;
+         ch.size = 1;
+         memory[np].nxt = 0;
+         memory[np].prv = 0;
+    :: (ch.head != 0) ->
+         memory[ch.tail].nxt = np;
+         memory[np].prv = ch.tail;
+         ch.tail = np;
+         ch.size = ch.size + 1;
+  fi
+}
+
+proctype doAppend(int addr; int val) {
+  atomic{
+    memory[addr].itm = val;
+    append(chain,addr);
+    printf("@@@ 0 CALL append %d %d\n",val,addr);
+    show_chain();
+  } ;
+}
+
+/* np = get(ch) */
+inline get(ch,np) {
+  np = ch.head ;
+  if
+    :: (np != 0) ->
+         ch.head = memory[np].nxt;
+         ch.size = ch.size - 1;
+         // memory[np].nxt = 0
+    :: (np == 0) -> skip
+  fi
+  if
+    :: (ch.head == 0) -> ch.tail = 0
+    :: (ch.head != 0) -> skip
+  fi
+}
+
+proctype doGet() {
+  atomic{
+    get(chain,nptr);
+    printf("@@@ 0 CALL get %d\n",nptr);
+    show_chain();
+    assert(nptr != 0);
+    show_node();
+  } ;
+}
+
+/* -----------------------------
+ doNonNullGet waits for a non-empty chain
+ before doing a get.
+ In generated sequential C code this can be simply be treated
+  the same as a call to doGet()
+*/
+proctype doNonNullGet() {
+  atomic{
+    chain.head != 0;
+    get(chain,nptr);
+    printf("@@@ 0 CALL getNonNull %d\n",nptr);
+    show_chain();
+    assert(nptr != 0);
+    show_node();
+  } ;
+}
+
+
+init {
+  pid nr;
+  atomic{
+    printf("\n\n Chain Model running.\n");
+    printf("@@@ 0 NAME Chain_AutoGen\n")
+    printf("@@@ 0 DEF MAX_SIZE 8\n");
+    printf("@@@ 0 DCLARRAY Node memory MAX_SIZE\n");
+    printf("@@@ 0 DECL unsigned nptr NULL\n")
+    printf("@@@ 0 DECL Control chain\n");
+
+    printf("\nInitialising...\n")
+    printf("@@@ 0 INIT\n");
+    chain.head = 0; chain.tail = 0; chain.size = 0;
+    show_chain();
+    show_node();
+  } ;
+
+  nr = _nr_pr;
+
+  run doAppend(6,21);
+  run doAppend(3,22);
+  run doAppend(4,23);
+  run doNonNullGet();
+  run doNonNullGet();
+  run doNonNullGet();
+
+  nr == _nr_pr;
+
+#ifdef TEST_GEN
+  assert (chain.size != 0);
+#else
+  assert (chain.size == 0);
+#endif
+
+  printf("\nChain Model finished !\n\n")
+}
diff --git a/formal/promela/models/chains/tr-chains-api-model.c b/formal/promela/models/chains/tr-chains-api-model.c
new file mode 100644
index 00000000..05938362
--- /dev/null
+++ b/formal/promela/models/chains/tr-chains-api-model.c
@@ -0,0 +1,70 @@
+/* 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 <rtems.h>
+#include <rtems/test.h>
+#include <rtems/chain.h>
+#include "tr-chains-api-model.h"
+
+item* get_item( rtems_chain_control* control )
+{
+    return (item*) rtems_chain_get_unprotected( control );
+}
+
+void show_chain( rtems_chain_control *control, char *str )
+{
+    item *itm;
+    rtems_chain_node *nod;
+    int cp, len;
+    char *s;
+
+    nod = (rtems_chain_node *)&control->Head;
+    itm = (item *)nod->next;
+    // itm is not NULL
+    s = str;
+    len = BUFSIZE;
+    while ( (item*)((rtems_chain_node*)itm)->next ) { // NULL when at control
+        cp = T_snprintf( s, len, " %d",itm->val );
+        s += cp;
+        len -= cp;
+        itm = (item*)((rtems_chain_node*)itm)->next;
+     }
+     cp = T_snprintf( s, len, " 0" );
+     s += cp;
+     len -= cp;
+}
diff --git a/formal/promela/models/chains/tr-chains-api-model.h b/formal/promela/models/chains/tr-chains-api-model.h
new file mode 100644
index 00000000..18c2c9b6
--- /dev/null
+++ b/formal/promela/models/chains/tr-chains-api-model.h
@@ -0,0 +1,57 @@
+/* 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.
+ ******************************************************************************/
+
+
+typedef struct item
+{
+    rtems_chain_node node;
+    int               val;
+} item;
+
+item* get_item( rtems_chain_control* control);
+
+void show_chain(rtems_chain_control *control, char *str);
+
+#define BUFSIZE 80
+
+typedef struct {
+  int stuff;
+  char buffer[BUFSIZE];
+} RtemsModelChainsAPI_Context;
+
+typedef RtemsModelChainsAPI_Context Context;