use hendwritten mutex specs

components/mission_protection_system/src/cn.mk

@@ -8,10 +8,10 @@ proofs: \
  components/actuation_unit.cn \
  posix_main.cn \
  common.cn \
+ components/instrumentation.cn \
  core.cn
 
 # some are verified but now hang or time out
-#components/instrumentation.cn \
 # all verified but hang or time out
  #sense_actuate.cn
  #components/actuator.cn
@@ -51,7 +51,7 @@ components/instrumentation.cn: components/instrumentation.c
 #	$(CN) $< --only=instrumentation_set_output_trips
 #	$(CN) $< --skip=instrumentation_step_trip,instrumentation_step,instrumentation_set_output_trips
 #	$(CN) $< --only=instrumentation_step
-#	$(CN) $<
+	$(CN) $<
 
 #send_actuation_command malloc
 #read_actuation_command global variables and a scope issue, CN issue #353

components/mission_protection_system/src/common.c

@@ -73,6 +73,92 @@ uint8_t error_sensor_mode[2][2];
 uint8_t error_sensor[2][2];
 uint8_t error_sensor_demux[2][2][2];
 
+
+#ifdef CN_ENV
+void *display_mutex;
+void *mem_mutex;
+#endif
+
+/*$
+predicate (struct core_state) Mx_Core(pointer p, boolean c)
+{
+  if (c) {
+    assert(ptr_eq(p, &core));
+    take cout = Owned<struct core_state>(p);
+    assert(core_state_ok(cout));
+    return cout;
+  } else {
+    return default<struct core_state>;
+  }
+}
+
+predicate (map<u64, map<u64, map<u64, u32> > >) Mx_Sensors_Demux(pointer p, boolean c)
+{
+  if (c) {
+    assert(ptr_eq(p, &sensors_demux));
+    take cout = Owned<uint32_t[2][2][2]>(p);
+    return cout;
+  } else {
+    return default<map<u64,map<u64,map<u64,u32> > > >;
+  }
+}
+
+predicate (map<u64, u8>) Mx_Error_Instrumentation(pointer p, boolean c)
+{
+  if (c) {
+    assert(ptr_eq(p, &error_instrumentation));
+    //take cout = Owned<uint8_t[2]>(p);
+    take cout = each(u64 i; i >= 0u64 && i < (u64)NINSTR()) {Owned<uint8_t>(array_shift<uint8_t>(p, i))};
+    return cout;
+  } else {
+    return default<map<u64, u8> >;
+  }
+}
+
+predicate (map<u64, struct instrumentation_state>) Mx_Instrumentation(pointer p, boolean c)
+{
+  if (c) {
+    assert(ptr_eq(p, &instrumentation));
+    take cout = each(u64 i; i >= 0u64 && i < (u64)NINSTR()) {Owned<struct instrumentation_state>(array_shift<struct instrumentation_state>(p, i))};
+    return cout;
+  } else {
+    return default<map<u64, struct instrumentation_state> >;
+  }
+}
+    //take eii = each(u64 i; i >= 0u64 && i < (u64)NINSTR()) {Owned<uint8_t>(array_shift<uint8_t>(&error_instrumentation,i))};
+$*/
+void cn_mutex_lock(void *p)
+/*$
+requires
+  ptr_eq(p, &mem_mutex) || ptr_eq(p, &display_mutex);
+ensures
+  take core_in = Mx_Core(&core, ptr_eq(p, &mem_mutex));
+  take sdi = Mx_Sensors_Demux(&sensors_demux, ptr_eq(p, &mem_mutex));
+  take ei = Mx_Error_Instrumentation(&error_instrumentation, ptr_eq(p, &mem_mutex));
+  take i = Mx_Instrumentation(&instrumentation, ptr_eq(p, &mem_mutex));
+  // TODO actuation_logic
+  // TODO device_actuation_logic
+  // TODO actuator_state
+  // TODO trip_signals
+$*/
+{
+
+}
+
+void cn_mutex_unlock(void *p)
+/*$
+requires
+  ptr_eq(p, &mem_mutex) || ptr_eq(p, &display_mutex);
+  take core_in = Mx_Core(&core, ptr_eq(p, &mem_mutex));
+  take sdi = Mx_Sensors_Demux(&sensors_demux, ptr_eq(p, &mem_mutex));
+  take ei = Mx_Error_Instrumentation(&error_instrumentation, ptr_eq(p, &mem_mutex));
+  take i = Mx_Instrumentation(&instrumentation, ptr_eq(p, &mem_mutex));
+ensures
+  true;
+$*/
+{
+}
+
 int read_instrumentation_channel(uint8_t div, uint8_t channel, uint32_t *val) {
   MUTEX_LOCK(&mem_mutex);
   int sensor = div/2;
@@ -88,6 +174,9 @@ int read_instrumentation_channel(uint8_t div, uint8_t channel, uint32_t *val) {
 
 int get_instrumentation_value(uint8_t division, uint8_t ch, uint32_t *value) {
   MUTEX_LOCK(&mem_mutex);
+  /*$ extract Owned<uint8_t>, (u64)division; $*/
+  /*$ extract Owned<struct instrumentation_state>, (u64)division; $*/
+  /*$ extract Owned<uint32_t>, (u64)ch; $*/
   if (!error_instrumentation[division])
     *value = instrumentation[division].reading[ch];
   MUTEX_UNLOCK(&mem_mutex);
@@ -97,6 +186,10 @@ int get_instrumentation_value(uint8_t division, uint8_t ch, uint32_t *value) {
 
 int get_instrumentation_trip(uint8_t division, uint8_t ch, uint8_t *value) {
   MUTEX_LOCK(&mem_mutex);
+  /*$ extract Owned<uint8_t>, (u64)division; $*/
+  /*$ extract Owned<struct instrumentation_state>, (u64)division; $*/
+  /*$ extract Owned<uint8_t>, (u64)ch; $*/
+  /*$ split_case(ch == division); $*/
   if (!error_instrumentation[division])
     *value = instrumentation[division].sensor_trip[ch];
   MUTEX_UNLOCK(&mem_mutex);

components/mission_protection_system/src/components/instrumentation.c

@@ -39,11 +39,9 @@ static int instrumentation_step_trip(uint8_t div,
 /*$
     requires div < NINSTR();
       take si = Owned<struct instrumentation_state>(state);
-      //take ci = Owned<struct core_state>(&core);
     ensures take so = Owned<struct instrumentation_state>(state);
       -1i32 <= return; return <= 0i32;
       si.mode == so.mode;
-      //take co = Owned<struct core_state>(&core);
 $*/
 {
   int err = 0;

components/mission_protection_system/src/include/instrumentation.h

@@ -114,15 +114,11 @@ void instrumentation_init(struct instrumentation_state *state);
 int instrumentation_step(uint8_t div, struct instrumentation_state *state);
 /*$ spec instrumentation_step(u8 div, pointer state);
     requires take statein = Owned<struct instrumentation_state>(state);
-      take ci = Owned<struct core_state>(&core);
       //each(u64 j; j < (u64)NTRIP()) {statein.mode[j] < NMODES()};
       div < NINSTR();
-      //core_state_ok(ci);
     ensures
       take stateout = Owned<struct instrumentation_state>(state);
       //each(u64 j; j < (u64)NTRIP()) {stateout.mode[j] < NMODES()};
-      take co = Owned<struct core_state>(&core);
-      //core_state_ok(co);
 $*/
 
 #ifdef __cplusplus

components/mission_protection_system/src/include/platform.h

@@ -79,6 +79,12 @@ extern pthread_mutex_t display_mutex;
 extern pthread_mutex_t mem_mutex;
 #define MUTEX_LOCK(x) pthread_mutex_lock(x)
 #define MUTEX_UNLOCK(x) pthread_mutex_unlock(x)
+#elif defined(CN_ENV)
+
+extern void *display_mutex;
+extern void *mem_mutex;
+#define MUTEX_LOCK(x) cn_mutex_lock(x)
+#define MUTEX_UNLOCK(x) cn_mutex_unlock(x)
 #else
 #define MUTEX_LOCK(x)
 #define MUTEX_UNLOCK(x)
@@ -102,44 +108,37 @@ int read_instrumentation_channel(uint8_t div, uint8_t channel, uint32_t *val);
       //channel < NTRIP();
       channel < 2u8; //NTRIP();
       take valin = Owned<uint32_t>(val);
-      take sdi = Owned<uint32_t[2][2][2]>(&sensors_demux);
     ensures take valout = Owned<uint32_t>(val);
       -1i32 <= return; return <= 0i32;
       //TODO (return == 0i32) ? (valout <= 0x80000000u32) : true;
-      take sdo = Owned<uint32_t[2][2][2]>(&sensors_demux);
 $*/
 
 int get_instrumentation_value(uint8_t division, uint8_t ch, uint32_t *value);
 /*$ spec get_instrumentation_value(u8 div, u8 ch, pointer value);
   requires
-    div < 4u8;
+    div < NINSTR();
     ch < NTRIP();
     take vi = Owned<uint32_t>(value);
-    //take eii = each(u64 i; i >= 0u64 && i < (u64)NINSTR()) {Owned<uint8_t>(array_shift<uint8_t>(&error_instrumentation,i))};
   ensures
   // TODO currently no way to tell if value was written
     take vo = Owned<uint32_t>(value);
-    //take eio = each(u64 i; i >= 0u64 && i < (u64)NINSTR()) {Owned<uint8_t>(array_shift<uint8_t>(&error_instrumentation,i))};
     return == 0i32;
 $*/
 int get_instrumentation_trip(uint8_t division, uint8_t ch, uint8_t *value);
 /*$ spec get_instrumentation_trip(u8 div, u8 ch, pointer value);
   requires
-    div < 4u8;
+    div < NINSTR();
     ch < NTRIP();
     take vi = Owned<uint8_t>(value);
-    // TODO use helpers
-    //take eii = each(u64 i; i >= 0u64 && i < (u64)NINSTR()) {Owned<uint8_t>(array_shift<uint8_t>(&error_instrumentation,i))};
   ensures
   // TODO currently no way to tell if value was written
     take vo = Owned<uint8_t>(value);
-    //take eio = each(u64 i; i >= 0u64 && i < (u64)NINSTR()) {Owned<uint8_t>(array_shift<uint8_t>(&error_instrumentation,i))};
     return == 0i32;
 $*/
 int get_instrumentation_mode(uint8_t division, uint8_t ch, uint8_t *value);
 /*$ spec get_instrumentation_mode(u8 div, u8 ch, pointer value);
   requires
-    div < 4u8;
+    div < NINSTR();
     ch < NTRIP();
     take vi = Owned<uint8_t>(value);
   ensures
@@ -337,18 +336,14 @@ int send_actuation_command(uint8_t actuator,
 uint8_t is_test_running(void);
 /*$ spec is_test_running();
     requires true;
-      take ci = Owned<struct core_state>(&core);
     ensures true;
-      take co = Owned<struct core_state>(&core);
 $*/
 
 /*@ assigns \nothing; */
 void set_test_running(int val);
 /*$ spec set_test_running(i32 val);
     requires true;
-      take ci = Owned<struct core_state>(&core);
     ensures true;
-      take co = Owned<struct core_state>(&core);
 $*/
 
 /*@ assigns \nothing;