Merge pull request #61 from GaloisInc/11-implement-mps

MPS: specs for components complete except for one function in actuation_unit.c

components/mission_protection_system/README.md

@@ -48,6 +48,18 @@ The system is connected to two temperature sensors and two fuel pressure sensors
 
 The MPS is being adapted from a high-assurance model reactor control system (HARDENS) which includes converting the Frama-C ACSL specifications to CN specifications. 
 Many C features are not yet supported by CN, the ones that most seriously affect the MPS are lack of variadic functions (all logging printfs) and lack of unions (the instrumentation_command struct).
+
+In CN `each` constructs, the index must be u64 or CN will not be able to automatically supply them. 
+CN cannot see preprocessor defines, so you must use a logical helper function that's associated with a C function that can see the definition. It looks like this:
+
+``` c
+#define NMODES 3
+/*$ function (u8) NMODES() $*/
+static
+uint8_t c_NMODES() /*$ cn_function NMODES; $*/ { return NMODES; }
+```
+
+
 ACSL constructs mostly have direct analogs in CN:
 
 - `requires` and `ensures` are the same

components/mission_protection_system/src/cn.mk

@@ -1,8 +1,13 @@
-CN_FLAGS=-I include --include=include/wars.h --magic-comment-char-dollar --batch
+CN_FLAGS=-I include --include=include/wars.h --magic-comment-char-dollar
 CN=cn $(CN_FLAGS)
 
-proofs: actuator_proof
+proofs: components/actuator.cn \
+ components/instrumentation_common.cn \
+ components/instrumentation.cn \
+ components/actuation_unit.cn
 
-.PHONY: actuator_proof
-actuator_proof: components/actuator.c
+%.cn: %.c
 	$(CN) $<
+
+components/actuation_unit.cn: components/actuation_unit.c
+	$(CN) $< --skip=actuation_logic_collect_trips

components/mission_protection_system/src/common.c

@@ -65,8 +65,14 @@ uint8_t error_sensor_demux[2][2][2];
 
 int read_instrumentation_channel(uint8_t div, uint8_t channel, uint32_t *val) {
   MUTEX_LOCK(&mem_mutex);
+#if !WAR_CN_231
   int sensor = div/2;
   int demux_out = div%2;
+#else
+  // valid for the valid range of the argument
+  int sensor = div >= 2 ? 1 : 0;
+  int demux_out = div&1;
+#endif
   *val = sensors_demux[channel][sensor][demux_out];
   MUTEX_UNLOCK(&mem_mutex);
   DEBUG_PRINTF(("<common.c> read_instrumentation_channel: div=%u,channel=%u,val=%u\n",div,channel,*val));
@@ -317,3 +323,34 @@ int is_actuate_test_complete(uint8_t dev)
   DEBUG_PRINTF(("<common.c> is_actuate_test_complete: %i\n",ret));
   return ret;
 }
+
+void zero_u8_arr(uint8_t *a, unsigned int n)
+{
+  for (unsigned int j = 0; j < n; j++)
+  /*$ inv take al = each(u64 k; k < (u64)j) { Owned<uint8_t>( array_shift<uint8_t>(a, k)) };
+    take ar = each(u64 l; (u64)j <= l && l < (u64)n) { Block<uint8_t>( array_shift<uint8_t>(a, l)) };
+    {a} unchanged; {n} unchanged;
+    j <= (u32)n;
+    $*/
+  {
+    /*$ extract Block<uint8_t>, (u64)j;$*/
+    /*$ extract Owned<uint8_t>, (u64)j;$*/
+    a[j] = 0;
+  }
+}
+
+void zero_u32_arr(uint32_t *a, unsigned int n)
+{
+  for (unsigned int j = 0; j < n; j++)
+  /*$ inv take al = each(u64 k; k < (u64)j) { Owned<uint32_t>( array_shift<uint32_t>(a, k)) };
+    take ar = each(u64 i; (u64)j <= i && i < (u64)n) { Block<uint32_t>( array_shift<uint32_t>(a, i)) };
+    {a} unchanged; {n} unchanged;
+    j <= (u32)n;
+    $*/
+  {
+    /*$ extract Block<uint32_t>, (u64)j;$*/
+    /*$ extract Owned<uint32_t>, (u64)j;$*/
+    a[j] = 0;
+  }
+}
+

components/mission_protection_system/src/components/actuation_unit.c

@@ -19,7 +19,9 @@
 #include "actuation_logic.h"
 
 #ifdef PLATFORM_HOST
+#if !WAR_NO_VARIADICS
 #include <stdio.h>
+#endif
 #else
 #include "printf.h"
 #endif
@@ -33,6 +35,12 @@
 */
 static int
 actuation_logic_collect_trips(uint8_t logic_no, int do_test, uint8_t trip[3][4], uint8_t trip_test[3][4])
+/*$
+  requires take tin = each(u64 i; i < 3u64) {Block<uint8_t[4]>(array_shift(trip, i))};
+  requires take ttestin = each(u64 i; i < 3u64) {Block<uint8_t[4]>(array_shift(trip_test, i))};
+  ensures take tout = each(u64 i; i < 3u64) {Owned<uint8_t[4]>(array_shift(trip, i))};
+  ensures take ttestout = each(u64 i; i < 3u64) {Owned<uint8_t[4]>(array_shift(trip_test, i))};
+$*/
 {
     int err = 0;
     uint8_t test_div[2];
@@ -72,6 +80,11 @@ actuation_logic_collect_trips(uint8_t logic_no, int do_test, uint8_t trip[3][4],
 */
 static uint8_t
 actuate_device(uint8_t device, uint8_t trips[3][4], int old)
+/*$
+  requires take tin = Owned<uint8_t[3][4]>(trips);
+  requires device < NDEV();
+  ensures take tout = Owned<uint8_t[3][4]>(trips);
+$*/
 {
     uint8_t res = 0;
     if (device == 0) {
@@ -81,10 +94,21 @@ actuate_device(uint8_t device, uint8_t trips[3][4], int old)
     }
     DEBUG_PRINTF(("<actuation_unit.c> actuate_device: device=0x%X, old=0x%X, out=0x%X,trips=[\n", device, old, res));
     /*@ loop assigns i; */
-    for (int i = 0; i < 3; ++i) {
+    for (int i = 0; i < 3; ++i)
+    /*$ inv (i <= 3i32) && (0i32 <= i);
+        take tinv = each(u64 j; j < 3u64) {Owned<uint8_t[4]>(array_shift(trips, j))};
+        {trips} unchanged;
+    $*/
+    {
         DEBUG_PRINTF(("["));
         /*@ loop assigns div; */
-        for (int div = 0; div < 4; ++div) {
+        for (int div = 0; div < 4; ++div)
+        /*$ inv div <= 4i32; 0i32 <= div;
+            take tinv2 = each(u64 k; k < 3u64) {Owned<uint8_t[4]>(array_shift(trips, k))};
+            {trips} unchanged;
+            0i32 <= i && i < 3i32;
+        $*/
+        {
         DEBUG_PRINTF(("%u,",trips[i][div]));
         }
         DEBUG_PRINTF(("],"));
@@ -106,13 +130,25 @@ actuate_device(uint8_t device, uint8_t trips[3][4], int old)
 */
 static void
 actuation_logic_vote_trips(uint8_t logic_no, int do_test, uint8_t device, uint8_t trip[3][4], uint8_t trip_test[3][4], struct actuation_logic *state)
+/*$
+  requires take sin = Owned(state);
+  requires take tin = Owned<uint8_t[3][4]>(trip);
+  requires take ttestin = each(u64 i; i < 3u64) {Owned<uint8_t[4]>(array_shift(trip_test, i))};
+  requires logic_no < NVOTE_LOGIC();
+  requires device < NDEV();
+  ensures take sout = Owned(state);
+  ensures take tout = Owned<uint8_t[3][4]>(trip);
+  ensures take ttestout = each(u64 i; i < 3u64) {Owned<uint8_t[4]>(array_shift(trip_test, i))};
+$*/
 {
     if (do_test && get_test_device() == device) {
         if (!is_actuation_unit_test_complete(logic_no)) {
+            /*$ extract Owned<uint8_t>, (u64)device; $*/
             set_actuation_unit_test_input_vote(logic_no, state->vote_actuate[device] != 0);
             state->vote_actuate[device] = actuate_device(device, trip_test, state->vote_actuate[device] != 0);
         }
     } else {
+        /*$ extract Owned<uint8_t>, (u64)device; $*/
         state->vote_actuate[device] = actuate_device(device, trip, state->vote_actuate[device] != 0);
     }
 }
@@ -126,6 +162,11 @@ actuation_logic_vote_trips(uint8_t logic_no, int do_test, uint8_t device, uint8_
 */
 static int
 actuation_logic_vote(uint8_t logic_no, int do_test, struct actuation_logic *state)
+/*$
+  requires logic_no < NVOTE_LOGIC();
+  requires take sin = Owned(state);
+  ensures take sout = Owned(state);
+ $*/
 {
     int err = 0;
     uint8_t trip[3][4];
@@ -147,9 +188,18 @@ actuation_logic_vote(uint8_t logic_no, int do_test, struct actuation_logic *stat
 */
 static int
 actuation_handle_command(uint8_t logic_no, struct actuation_command *cmd, struct actuation_logic *state)
+/*$
+  requires take cin = Owned(cmd);
+  requires take sin = Owned(state);
+  ensures take cout = Owned(cmd);
+  ensures take sout = Owned(state);
+  ensures return >= -1i32 && return <= 0i32;
+$*/
 {
-    if (cmd->device <= 1)
+    if (cmd->device <= 1) {
+        /*$ extract Owned<uint8_t>, (u64)cin.device; $*/
         state->manual_actuate[cmd->device] = cmd->on;
+    }
     return 0;
 }
 
@@ -161,22 +211,38 @@ actuation_handle_command(uint8_t logic_no, struct actuation_command *cmd, struct
 */
 static int
 output_actuation_signals(uint8_t logic_no, int do_test, struct actuation_logic *state)
+/*$
+  requires take sin = Owned(state);
+  requires logic_no < NVOTE_LOGIC();
+  ensures take sout = Owned(state);
+  ensures return >= -1i32 && return <= 0i32;
+$*/
 {
     int err = 0;
 
     /*@ loop invariant 0 <= d <= NDEV;
       @ loop invariant -1 <= err <= 0;
       @ loop assigns d, err;
     */
-    for (int d = 0; d < NDEV; ++d) {
+    for (int d = 0; d < NDEV; ++d)
+    /*$ inv d >= 0i32; d <= (i32)NDEV();
+        take sinv = Owned(state);
+        {state} unchanged;
+        {logic_no} unchanged;
+        -1i32 <= err; err <= 0i32;
+    $*/
+    {
+        /*$ extract Owned<uint8_t>, (u64)d; $*/
         uint8_t on = state->vote_actuate[d] || state->manual_actuate[d];
         if (!do_test || !is_actuation_unit_test_complete(logic_no)) {
             err |= set_output_actuation_logic(logic_no, d, BIT(do_test, on));
         }
     }
     if (do_test && !is_actuation_unit_test_complete(logic_no)) {
         // Reset internal state
+        /*$ extract Owned<uint8_t>, 0u64; $*/
         state->vote_actuate[0] = 0;
+        /*$ extract Owned<uint8_t>, 1u64; $*/
         state->vote_actuate[1] = 0;
         set_actuation_unit_test_complete(logic_no, 1);
     }
@@ -190,6 +256,10 @@ int actuation_unit_step(uint8_t logic_no, struct actuation_logic *state)
     uint8_t test_div[2];
 
     get_test_instrumentation(test_div);
+    /*$ extract Owned<uint8_t>, 0u64; $*/
+    /*$ instantiate 0u64; $*/
+    /*$ extract Owned<uint8_t>, 1u64; $*/
+    /*$ instantiate 1u64; $*/
     int do_test = logic_no == get_test_actuation_unit() &&
                   is_instrumentation_test_complete(test_div[0]) &&
                   is_instrumentation_test_complete(test_div[1]) &&

components/mission_protection_system/src/components/actuator.c

@@ -34,10 +34,10 @@
 #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;
+  @ assigns core.test.test_device_done[0..2];
+  @ assigns core.test.test_device_result[0..2];
+  @ ensures \true;
 */
 int actuate_devices(void)
 /*$
@@ -55,8 +55,8 @@ 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;
+    @ loop assigns d, err, core.test.test_device_done[0..2], core.test.test_device_result[0..2];
     */
   for (uint8_t d = 0; d < NDEV; ++d)
     /*$ inv 0u8 <= d && d <= NDEV(); $*/