Implement MPS specs (#116)

Remove workarounds for issues 231 and 233
Add workarounds for issue 399

Contagious use of globals is causing extremely slow performance.
Sometimes these specs cause hangs in CN, so some previously verified
functions now hang.

components/platform_crypto/shave_trusted_boot/cn_memcpy.h → components/include/cn_memory.h

@@ -1,6 +1,18 @@
 #ifndef CN_MEMCPY_H_
 #define CN_MEMCPY_H_
 
+void *memset(void *dest, int v, size_t n);
+/*$
+spec memset(pointer dest, i32 v, u64 n);
+requires
+    take Dest = each (u64 i; 0u64 <= i && i < n ) { Block<unsigned char>(array_shift<unsigned char>(dest, i)) };
+
+ensures
+    take DestR = each (u64 i; 0u64 <= i && i < n ) { Owned<unsigned char>(array_shift<unsigned char>(dest, i)) };
+    each (u64 i; 0u64 <= i && i < n ) { DestR[i] == (u8)v };
+    ptr_eq(return, dest);
+$*/
+
 int _memcmp(const unsigned char *dest, const unsigned char *src, size_t n);
 /*$ spec _memcmp(pointer dest, pointer src, u64 n);
 
@@ -30,4 +42,31 @@ ensures
     each (u64 i; 0u64 <= i && i < n ) { SrcR[i] == DestR[i] };
 $*/
 
+void _free(void *p);
+/*$
+spec _free(pointer p);
+requires
+    !is_null(p);
+    take log = Alloc(p);
+    allocs[(alloc_id)p] == log;
+    let base = array_shift<char>(p, 0u64);
+    log.base == (u64) base;
+    take i = each(u64 j; j >= 0u64 && j < log.size) {Block<uint8_t>(array_shift<uint8_t>(p, j))};
+ensures
+    true;
+$*/
+
+void *_malloc(size_t n);
+/*$
+spec _malloc(u64 n);
+requires true;
+ensures
+    !is_null(return);
+    take log = Alloc(return);
+    allocs[(alloc_id)return] == log;
+    log.base == (u64) return;
+    log.size == n;
+    take i = each(u64 j; j >= 0u64 && j < n) {Block<uint8_t>(array_shift<uint8_t>(return, j))};
+$*/
+
 #endif // CN_MEMCPY_H_

components/include/wars.h

@@ -7,6 +7,10 @@
 // code and the deployed code
 #define CN_ENV 1
 
+// CN issue https://github.com/rems-project/cerberus/issues/254
+// Local variables need to be Owned when entering loops
+#define WAR_CN_254 1
+
 // CN issue https://github.com/rems-project/cerberus/issues/284
 // GCC atributes not supported
 #define WAR_CN_284 1
@@ -21,11 +25,63 @@
 #define WAR_CN_285 1
 
 // CN issue https://github.com/rems-project/cerberus/issues/309
-// String literals are created in the global context but the function doesn't have a resource for them
+// String literals are created in the global context but the function doesn't
+// have a resource for them
 #define WAR_CN_309
 
+// CN issue https://github.com/rems-project/cerberus/issues/353
+// It's not possible to use static local variables
+#define WAR_CN_353 1
+
+// CN issue https://github.com/rems-project/cerberus/issues/358
+// posix headers exist, but they're only accessible as posix/unistd.h rather
+// than unistd.h and they fail when including other posix headers
+#define WAR_CN_358
+
 // CN issue https://github.com/GaloisInc/VERSE-Toolchain/issues/103
 // memcmp not supported
 #define WAR_VERSE_TOOLCHAIN_103 1
 
+// the simplest workaround for unions (making it a struct) don't make sense if
+// the union is used to access the same data from different perspectives, but if
+// it's just used as a simple sum type it's merely wasteful to use a struct
+// instead.
+#define WAR_NO_UNIONS 1
+
+// no workaround besides not using it
+#define WAR_NO_DOUBLES 1
+
+// no workaround besides not using it
+#define WAR_NO_VARIADICS 1
+
+// CN can handle them but working with them in arbitrary orders is currently difficult
+#define WAR_NESTED_ARRAYS 1
+
+#if WAR_NO_DOUBLES
+#define double unsigned long
+#endif
+
+// define out things we can't handle yet
+#ifdef WAR_NO_VARIADICS
+#define fprintf(a,b,...) fprintf(a,b)
+#define fscanf(a,b,...) fscanf(a,b)
+#define printf(a,...) printf(a)
+#define sprintf(a,b,...) sprintf(a,b)
+#define snprintf(a,b,c,...) snprintf(a,b,c)
+#define scanf(a,...) scanf(a)
+#define sscanf(a,b,...) sscanf(a,b)
+#endif
+
+// CN issue https://github.com/rems-project/cerberus/issues/437
+// Some headers mention structs only as f(struct x *y) and never define x. C
+// accepts this but CN rejects it
+#define WAR_CN_437 1
+
+#ifdef WAR_CN_437
+// this is required so we can mention FILE* parameters
+struct _IO_FILE {
+    int x;
+};
+#endif
+
 #endif // __CN_WARS_H__

components/mission_protection_system/src/cn.mk

@@ -1,13 +1,89 @@
-CN_FLAGS=-I include --include=include/wars.h --magic-comment-char-dollar
+#CN_FLAGS=-I include --include=include/wars.h --magic-comment-char-dollar -I /Users/guso/.opam/default/lib/cerberus/runtime/libc/include/posix
+CN_FLAGS=-I include -I ../../include --include=../../include/wars.h --magic-comment-char-dollar -DPLATFORM_HOST
+#CN=cn verify --solver-type cvc5 $(CN_FLAGS)
 CN=cn verify $(CN_FLAGS)
 
-proofs: components/actuator.cn \
+proofs: \
  components/instrumentation_common.cn \
- components/instrumentation.cn \
- components/actuation_unit.cn
+ components/actuation_unit.cn \
+ posix_main.cn \
+ common.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
+
+# these have symbol naming issues but they should be processed eventually
+# variants/instrumentation_handwritten_C.cn \
+# variants/actuator_generated_C.cn \
+# variants/saturation_generated_C.cn \
+# variants/instrumentation_generated_C.cn \
+# variants/actuation_unit_generated_C.cn \
+# handwritten/C/instrumentation_impl.cn
+
+# needed for a mode of core.c
+# self_test_data/tests.inc.cn
+
+# explicitly not included:
+# bottom.cn is just assert(0) stubs
+# generated/C/actuation_unit_impl.cn
+# generated/C/instrumentation_impl.cn
+# generated/C/saturation_impl.cn
+# generated/C/actuator_impl.cn
 
 %.cn: %.c
 	$(CN) $<
 
+#actuation_logic_collect_trips nested arrays, can be done
+#actuation_logic_vote_trips_tgt times out
+#output_actuation_signals_tgt times out
+#actuation_unit_step_tgt times out
 components/actuation_unit.cn: components/actuation_unit.c
-	$(CN) $< --skip=actuation_logic_collect_trips
+	$(CN) $< --skip=actuation_logic_collect_trips,actuation_logic_vote_trips,output_actuation_signals,actuation_unit_step
+
+components/instrumentation.cn: components/instrumentation.c
+# CN #399
+#	$(CN) $< --only=instrumentation_step_trip
+# also CN #399
+#	$(CN) $< --only=instrumentation_set_output_trips
+#	$(CN) $< --skip=instrumentation_step_trip,instrumentation_step,instrumentation_set_output_trips
+#	$(CN) $< --only=instrumentation_step
+#	$(CN) $<
+
+#send_actuation_command malloc
+#read_actuation_command global variables and a scope issue, CN issue #353
+#update_sensor_errors contains a 2-level and 3-level array with the same variables used as indices in both, CN issue #357
+#update_sensors also CN issue #357
+#clear_screen need to claim that stdin is a valid pointer while using `accesses`. Could just use take but it's a global
+posix_main.cn: posix_main.c
+#	$(CN) $< --skip=main,start1,start0,update_sensor_errors,clear_screen,update_sensors,send_actuation_command,read_actuation_command
+	$(CN) $< --skip=main,read_actuation_command,send_actuation_command,update_display,update_sensors,clear_screen,update_sensor_errors,update_sensor_simulation
+
+.PHONY: common.cn
+
+#accesses common.c-local struct:
+#  get_instrumentation_trip
+#  get_instrumentation_value
+#  get_instrumentation_mode
+#  get_instrumentation_maintenance
+#  reset_actuation_logic
+#timeout/hang:
+#  get_test_instrumentation
+#  get_instrumentation_test_setpoints
+#other:
+#  set_output_actuation_logic
+#  read_test_instrumentation_channel
+#  read_instrumentation_trip_signals
+common.cn:  common.c
+	$(CN) $< --skip=get_instrumentation_trip,get_instrumentation_value,get_instrumentation_mode,get_instrumentation_maintenance,reset_actuation_logic,set_output_actuation_logic,read_test_instrumentation_channel,read_instrumentation_trip_signals,get_test_instrumentation,get_instrumentation_test_setpoints,get_test_device,get_test_actuation_unit
+
+#update_ui_actuation needs to reason about c strings and that snprint, mostly the reference to the string literal though
+#set_display_line needs to handle strings and use memset
+#core_step and core_init have trouble with core_state_ok
+core.cn: core.c
+	$(CN) $< --skip=update_ui_actuation,set_display_line,core_step,core_init,update_ui,update_ui_actuation,update_ui_instr
+	# undefined behavior in tests.inc.c currently
+	#$(CN) -DENABLE_SELF_TEST $< --skip=update_ui_actuation,set_display_line,core_step,core_init