Merge branch 'main' into 45-feature-gather-requirements-for-ta1-tooling

.github/workflows/main.yml

@@ -25,6 +25,8 @@ jobs:
               run: |
                 cd components/mission_protection_system/src
                 SENSORS=NotSimulated SELF_TEST=Enabled make rts
+                make clean
+                SENSORS=NotSimulated SELF_TEST=Enabled make rts_bottom
 
     mps-test:
       runs-on: ubuntu-latest

.github/workflows/proofs.yml

@@ -0,0 +1,48 @@
+# This is a basic workflow to help you get started with Actions
+
+name: Code Verification
+
+# Controls when the workflow will run
+on:
+  # Triggers the workflow on push or pull request events but only for the develop branch
+  push:
+
+  # Allows you to run this workflow manually from the Actions tab
+  #workflow_dispatch:
+
+# A workflow run is made up of one or more jobs that can run sequentially or in parallel
+jobs:
+
+  mps-verify-cn:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository and submodules
+        uses: actions/checkout@v4
+      - name: Prove MPS Components
+        uses: addnab/docker-run-action@v3
+        with:
+          image: podhrmic/cerberus:release
+          options: -v ${{ github.workspace }}:/data
+          # This action seems to override the docker image entrypoint, as a result
+          # we need to run "eval `opam env`" first
+          # Use `>` so newlines will be replaced with spaces
+          run: >
+            eval `opam env` &&
+            cd components/mission_protection_system/src &&
+            make -f cn.mk proofs
+
+  mps-verify-frama-c:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository and submodules
+        uses: actions/checkout@v4
+      - name: Prove MPS Components
+        uses: addnab/docker-run-action@v3
+        with:
+          image: framac/frama-c:dev
+          options: -v ${{ github.workspace }}:/work -w /work
+          run: |
+            cd components/mission_protection_system/src
+            mkdir -p /tmp/wp-session/script
+            mkdir -p /tmp/wp-session/cache
+            make -f frama_c.mk proofs

.gitignore

@@ -50,3 +50,6 @@ modules.order
 Module.symvers
 Mkfile.old
 dkms.conf
+
+# Python cache
+*/__pycache__/*

components/mission_protection_system/src/Makefile

@@ -160,7 +160,7 @@ endif
 
 BUILD_MSG = BUILD CC=$(CC) PLATFORM=$(PLATFORM) EXECUTION=$(EXECUTION) SELF_TEST_PERIOD_SEC=$(SELF_TEST_PERIOD_SEC) SELF_TEST=$(SELF_TEST)
 
-.PHONY: all rts clean linux macos proof generate_sources generate_c generate_sv self_test_data/tests.inc.c core.c
+.PHONY: all rts clean generate_sources generate_c generate_sv self_test_data/tests.inc.c core.c
 
 all: rts
 

components/mission_protection_system/src/bottom.c

@@ -169,7 +169,7 @@ int send_actuation_command(uint8_t actuator, struct actuation_command *cmd) {
   return 0;
 }
 
-int set_display_line(uint8_t line_number, const char *display, uint32_t size) {
+int set_display_line(struct ui_values *ui, uint8_t line_number, char *display, uint32_t size) {
   assert(0);
   return 0;
 }

components/mission_protection_system/src/cn.mk

@@ -0,0 +1,8 @@
+CN_FLAGS=-I include --include=include/wars.h --magic-comment-char-dollar --batch
+CN=cn $(CN_FLAGS)
+
+proofs: actuator_proof
+
+.PHONY: actuator_proof
+actuator_proof: components/actuator.c
+	$(CN) $<

components/mission_protection_system/src/common.c

@@ -35,18 +35,6 @@ struct core_state core = {0};
 struct instrumentation_state instrumentation[4];
 struct actuation_logic actuation_logic[2];
 
-/*@ function (u8) NINSTR() @*/
-uint8_t c_NINSTR() /*@ cn_function NINSTR; @*/ { return NINSTR; }
-
-/*@ function (u8) NTRIP() @*/
-uint8_t c_NTRIP() /*@ cn_function NTRIP; @*/ { return NTRIP; }
-
-/*@ function (u8) NVOTE_LOGIC() @*/
-uint8_t c_NVOTE_LOGIC() /*@ cn_function NVOTE_LOGIC; @*/ { return NVOTE_LOGIC; }
-
-/*@ function (u8) NDEV() @*/
-uint8_t c_NDEV() /*@ cn_function NDEV; @*/ { return NDEV; }
-
 // channel -> sensor # -> val
 uint32_t sensors[2][2];
 // channel -> sensor # -> demux output # -> val

components/mission_protection_system/src/components/actuator.c

@@ -27,16 +27,16 @@
 #define w1 uint8_t
 #define w2 uint8_t
 
-/* @ requires \true; DONE
-  @ assigns core.test.test_device_done[0..2]; TODO
-  @ assigns core.test.test_device_result[0..2]; TODO
-  @ ensures \true; DONE
+/* @ requires \true; // DONE
+  @ assigns core.test.test_device_done[0..2]; // TODO
+  @ assigns core.test.test_device_result[0..2]; // TODO
+  @ ensures \true; // DONE
 */
 int actuate_devices(void)
-/*@
+/*$
     requires true;
     ensures true;
-@*/
+$*/
 {
   int err = 0;
   int do_test = is_test_running() && is_actuation_unit_test_complete(get_test_actuation_unit());
@@ -48,18 +48,21 @@ int actuate_devices(void)
     set_actuate_test_complete(1, 0);
   }
 
-  /* @ loop invariant 0 <= d && d <= NDEV; DONE
-    @ loop assigns d, err, core.test.test_device_done[0..2], core.test.test_device_result[0..2]; TODO
+  /* @ loop invariant 0 <= d && d <= NDEV; // DONE
+    @ loop assigns d, err, core.test.test_device_done[0..2], core.test.test_device_result[0..2]; // TODO
     */
   for (uint8_t d = 0; d < NDEV; ++d)
-    /*@ inv 0u8 <= d && d <= NDEV(); @*/
+    /*$ inv 0u8 <= d && d <= NDEV(); $*/
   {
     uint8_t votes = 0;
     uint8_t test_votes = 0;
 
+    /*@ loop invariant 0 <= l && l <= NVOTE_LOGIC;
+      @ loop assigns l, err, test_votes, votes;
+    */
     for (uint8_t l = 0; l < NVOTE_LOGIC; ++l)
-      /*@ inv 0u8 <= l && l <= NVOTE_LOGIC();
-              0u8 <= d && d < NDEV(); @*/
+      /*$ inv 0u8 <= l && l <= NVOTE_LOGIC();
+              0u8 <= d && d < NDEV(); $*/
     {
       uint8_t this_vote = 0;
       err   |= get_actuation_state(l, d, &this_vote);

components/mission_protection_system/src/frama_c.mk

@@ -0,0 +1,36 @@
+#   Copyright 2021, 2022, 2023 Galois, Inc.
+#
+#   Licensed under the Apache License, Version 2.0 (the "License");
+#   you may not use this file except in compliance with the License.
+#   You may obtain a copy of the License at
+#
+#       http://www.apache.org/licenses/LICENSE-2.0
+#
+#   Unless required by applicable law or agreed to in writing, software
+#   distributed under the License is distributed on an "AS IS" BASIS,
+#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#   See the License for the specific language governing permissions and
+#   limitations under the License.
+
+F ?=
+FRAMAC_FLAGS= -cpp-extra-args="-I include" -c11 -wp-split -wp-session /tmp/wp-session -wp-cache /tmp/update -wp-smoke-tests $(F)
+FRAMAC=frama-c $(FRAMAC_FLAGS) -wp-rte -wp $(FRAMAC_FLAGS) -wp-prover tip,alt-ergo,z3
+
+EXCLUDE_ACT=$(addprefix -wp-skip-fct , rotl1 rotl2 rotr1 rotr2 )
+EXCLUDE_ACTU=$(addprefix -wp-skip-fct , rotl1 rotl2 rotl8 rotr1 rotr2 rotr8)
+EXCLUDE_INSTR=$(addprefix -wp-skip-fct , rotl1 rotl2 rotl3 rotl32 rotr1 rotr2 rotr3 rotr32)
+
+proofs: actuator_proof actuation_unit_proof instrumentation_proof
+
+actuator_proof:
+	$(FRAMAC) components/actuator.c
+	$(FRAMAC) -cpp-extra-args='-include "common.h" -include "actuate.h"' generated/C/actuator_impl.c $(EXCLUDE_ACT)
+
+actuation_unit_proof:
+	$(FRAMAC) components/actuation_unit.c
+	$(FRAMAC) -cpp-extra-args='-include "common.h" -include "actuation_logic.h"'  generated/C/actuation_unit_impl.c $(EXCLUDE_ACTU)
+
+instrumentation_proof:
+	$(FRAMAC) components/instrumentation.c
+	$(FRAMAC) -cpp-extra-args='-include "common.h" -include "instrumentation.h"' generated/C/instrumentation_impl.c $(EXCLUDE_INSTR)
+	$(FRAMAC) -cpp-extra-args='-include "common.h" -include "instrumentation.h"' handwritten/C/instrumentation_impl.c

components/mission_protection_system/src/include/actuate.h

@@ -27,13 +27,18 @@ int actuate_devices(void);
 // Return whether or not a device with the provided votes should be actuated
 // Bit i = vote by logic unit i
 // This function is generated directly from the Cryptol model
+/*@ assigns \nothing;
+  @ ensures \result == 0 || \result == 1;
+  @ ensures \result == 1 <==> ((vs & 0x01) || (vs & 0x02));
+  @ ensures ActuateActuator(vs) <==> \result == 1;
+*/
 uint8_t ActuateActuator(uint8_t vs);
-/*@ spec ActuateActuator(u8 vs);
+/*$ spec ActuateActuator(u8 vs);
     requires true;
     ensures (return == 0u8 || return == 1u8);
       (return == 1u8) == (bw_and_uf(vs, 1u8) != 0u8 || bw_and_uf(vs, 2u8) != 0u8);
       ActuateActuator(vs) == (return == 1u8);
- @*/
+ $*/
 
 int actuate_devices_generated_C(void);
 

components/mission_protection_system/src/include/actuation_logic.h

@@ -23,20 +23,20 @@
 #include "core.h"
 #include "models.acsl"
 
-/* @requires \valid(&trips[0.. NINSTR -1]);
+/*@requires \valid(&trips[0.. NINSTR -1]);
   @assigns \nothing;
   @ensures (\result != 0) <==> Coincidence_2_4(trips);
 */
 uint8_t Coincidence_2_4(uint8_t trips[4]);
 
-/* @requires \valid(&trips[0.. NTRIP - 1][0.. NINSTR - 1]);
+/*@requires \valid(&trips[0.. NTRIP - 1][0.. NINSTR - 1]);
   @requires \valid(trips + (0.. NTRIP-1));
   @assigns \nothing;
   @ensures (\result != 0) <==> Actuate_D0(&trips[T][0], &trips[P][0], &trips[S][0], old != 0);
 */
 uint8_t Actuate_D0(uint8_t trips[3][4], uint8_t old);
 
-/* @requires \valid(&trips[0.. NTRIP-1][0.. NINSTR-1]);
+/*@requires \valid(&trips[0.. NTRIP-1][0.. NINSTR-1]);
   @requires \valid(trips + (0.. NTRIP-1));
   @assigns \nothing;
   @ensures (\result != 0) <==> Actuate_D1(&trips[T][0], &trips[P][0], &trips[S][0], old != 0);
@@ -52,7 +52,7 @@ extern struct actuation_logic actuation_logic[2];
 
 /* The main logic of the actuation unit */
 
-/* @requires \valid(state);
+/*@requires \valid(state);
   @requires logic_no <= 1;
   @assigns state->manual_actuate[0.. NDEV-1];
   @assigns state->vote_actuate[0.. NDEV-1];

components/mission_protection_system/src/include/common.h

@@ -26,7 +26,12 @@
 // Instrumentation
 // Trip modes:
 #define NINSTR 4
-uint8_t c_NINSTR();
+// These wrapper functions need their definitions exposed to CN, but must not
+// cause multiple definition errors in the linker, so they must be static. They
+// will not actually be called so this is OK.
+/*$ function (u8) NINSTR() $*/
+static
+uint8_t c_NINSTR() /*$ cn_function NINSTR; $*/ { return NINSTR; }
 #define NMODES 3
 #define BYPASS 0
 #define OPERATE 1
@@ -39,16 +44,22 @@ uint8_t c_NINSTR();
 
 // Channel/Trip signal IDs
 #define NTRIP 3
-uint8_t c_NTRIP();
+/*$ function (u8) NTRIP() $*/
+static
+uint8_t c_NTRIP() /*$ cn_function NTRIP; $*/ { return NTRIP; }
 #define T 0
 #define P 1
 #define S 2
 
 // Actuation
 #define NVOTE_LOGIC 2
-uint8_t c_NVOTE_LOGIC();
+/*$ function (u8) NVOTE_LOGIC() $*/
+static
+uint8_t c_NVOTE_LOGIC() /*$ cn_function NVOTE_LOGIC; $*/ { return NVOTE_LOGIC; }
 #define NDEV 2
-uint8_t c_NDEV();
+/*$ function (u8) NDEV() $*/
+static
+uint8_t c_NDEV() /*$ cn_function NDEV; $*/ { return NDEV; }
 
 // Core
 // Command Types

components/mission_protection_system/src/include/instrumentation.h

@@ -63,10 +63,10 @@ struct instrumentation_state {
 };
 
 void instrumentation_init(struct instrumentation_state *state);
-/*@ spec instrumentation_init(pointer state);
+/*$ spec instrumentation_init(pointer state);
     requires take i = Block<struct instrumentation_state>(state);
     ensures take o = Owned<struct instrumentation_state>(state);
-@*/
+$*/
 
 /* @requires \valid(state);
   @requires \valid(state->reading + (0.. NTRIP-1));

components/mission_protection_system/src/include/models.acsl

@@ -20,13 +20,18 @@
 
 // TODO rename to models.cn or something
 
-/*@
+/*$
 function (bool) ActuateActuator(u8 input) {
   ((bw_and_uf(input, 1u8) != 0u8) || (bw_and_uf(input, 2u8) != 0u8))
 }
-@*/
+$*/
 
-/*
+/*@ axiomatic Actuator {
+  @
+  @ // Refines RTS::Actuator::ActuateActuator
+  @ logic boolean ActuateActuator(uint8_t input) =
+  @   ((input & 0x1) != 0) || ((input & 0x2) != 0);
+  @ }
   @
   @
   @ axiomatic ActuationUnit {