From bcd5df127db2145986370b7c2db9b2a968905911 Mon Sep 17 00:00:00 2001 From: Gus O'Hanley Date: Mon, 30 Dec 2024 18:38:54 -0600 Subject: [PATCH] use hendwritten mutex specs --- .../mission_protection_system/src/cn.mk | 4 +- .../mission_protection_system/src/common.c | 93 +++++++++++++++++++ .../src/components/instrumentation.c | 2 - .../src/include/instrumentation.h | 4 - .../src/include/platform.h | 23 ++--- 5 files changed, 104 insertions(+), 22 deletions(-) diff --git a/components/mission_protection_system/src/cn.mk b/components/mission_protection_system/src/cn.mk index 47626611..2c3de882 100644 --- a/components/mission_protection_system/src/cn.mk +++ b/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 diff --git a/components/mission_protection_system/src/common.c b/components/mission_protection_system/src/common.c index abc853c7..39a9f954 100644 --- a/components/mission_protection_system/src/common.c +++ b/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(p); + assert(core_state_ok(cout)); + return cout; + } else { + return default; + } +} + +predicate (map > >) Mx_Sensors_Demux(pointer p, boolean c) +{ + if (c) { + assert(ptr_eq(p, &sensors_demux)); + take cout = Owned(p); + return cout; + } else { + return default > > >; + } +} + +predicate (map) Mx_Error_Instrumentation(pointer p, boolean c) +{ + if (c) { + assert(ptr_eq(p, &error_instrumentation)); + //take cout = Owned(p); + take cout = each(u64 i; i >= 0u64 && i < (u64)NINSTR()) {Owned(array_shift(p, i))}; + return cout; + } else { + return default >; + } +} + +predicate (map) Mx_Instrumentation(pointer p, boolean c) +{ + if (c) { + assert(ptr_eq(p, &instrumentation)); + take cout = each(u64 i; i >= 0u64 && i < (u64)NINSTR()) {Owned(array_shift(p, i))}; + return cout; + } else { + return default >; + } +} + //take eii = each(u64 i; i >= 0u64 && i < (u64)NINSTR()) {Owned(array_shift(&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, (u64)division; $*/ + /*$ extract Owned, (u64)division; $*/ + /*$ extract Owned, (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, (u64)division; $*/ + /*$ extract Owned, (u64)division; $*/ + /*$ extract Owned, (u64)ch; $*/ + /*$ split_case(ch == division); $*/ if (!error_instrumentation[division]) *value = instrumentation[division].sensor_trip[ch]; MUTEX_UNLOCK(&mem_mutex); diff --git a/components/mission_protection_system/src/components/instrumentation.c b/components/mission_protection_system/src/components/instrumentation.c index b62d2f0a..0ad21d94 100644 --- a/components/mission_protection_system/src/components/instrumentation.c +++ b/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(state); - //take ci = Owned(&core); ensures take so = Owned(state); -1i32 <= return; return <= 0i32; si.mode == so.mode; - //take co = Owned(&core); $*/ { int err = 0; diff --git a/components/mission_protection_system/src/include/instrumentation.h b/components/mission_protection_system/src/include/instrumentation.h index 71e7271e..c7b6ee82 100644 --- a/components/mission_protection_system/src/include/instrumentation.h +++ b/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(state); - take ci = Owned(&core); //each(u64 j; j < (u64)NTRIP()) {statein.mode[j] < NMODES()}; div < NINSTR(); - //core_state_ok(ci); ensures take stateout = Owned(state); //each(u64 j; j < (u64)NTRIP()) {stateout.mode[j] < NMODES()}; - take co = Owned(&core); - //core_state_ok(co); $*/ #ifdef __cplusplus diff --git a/components/mission_protection_system/src/include/platform.h b/components/mission_protection_system/src/include/platform.h index af3d57a8..b2a4ce19 100644 --- a/components/mission_protection_system/src/include/platform.h +++ b/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(val); - take sdi = Owned(&sensors_demux); ensures take valout = Owned(val); -1i32 <= return; return <= 0i32; //TODO (return == 0i32) ? (valout <= 0x80000000u32) : true; - take sdo = Owned(&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(value); - //take eii = each(u64 i; i >= 0u64 && i < (u64)NINSTR()) {Owned(array_shift(&error_instrumentation,i))}; ensures // TODO currently no way to tell if value was written take vo = Owned(value); - //take eio = each(u64 i; i >= 0u64 && i < (u64)NINSTR()) {Owned(array_shift(&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(value); - // TODO use helpers - //take eii = each(u64 i; i >= 0u64 && i < (u64)NINSTR()) {Owned(array_shift(&error_instrumentation,i))}; ensures // TODO currently no way to tell if value was written take vo = Owned(value); - //take eio = each(u64 i; i >= 0u64 && i < (u64)NINSTR()) {Owned(array_shift(&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(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(&core); ensures true; - take co = Owned(&core); $*/ /*@ assigns \nothing; */ void set_test_running(int val); /*$ spec set_test_running(i32 val); requires true; - take ci = Owned(&core); ensures true; - take co = Owned(&core); $*/ /*@ assigns \nothing;