From 3ebbb40c86ace9ebc0a7d02121470aa0a7bcd495 Mon Sep 17 00:00:00 2001 From: Jason Belt Date: Fri, 10 Jan 2025 18:25:21 -0600 Subject: [PATCH] update attestation artifacts --- .github/workflows/ci-hamr.yml | 15 +- .github/workflows/hamr-ci.cmd | 98 ---- .github/workflows/hamr/attestation-utils.cmd | 53 ++ .github/workflows/hamr/hamr-ci.cmd | 43 ++ isolette/.ci/ci.cmd | 22 +- ...lette_isolette_single_sensor_Instance.json | 506 ------------------ .../aadl/packages/Abstract_Definitions.aadl | 2 +- isolette/aadl/bin/clean.cmd | 126 ++--- isolette/attestation/aadl_composite.txt | 1 + isolette/attestation/aadl_micro_composite.txt | Bin 0 -> 32 bytes isolette/attestation/aadl_model_args.json | 3 + isolette/attestation/micro_composite.txt | 1 - isolette/attestation/microkit_composite.txt | Bin 0 -> 32 bytes isolette/attestation/model.golden | 1 - isolette/attestation/model_args.json | 2 - isolette/attestation/run-attestation.cmd | 129 +++++ isolette/attestation/sysml_composite.txt | 1 + .../attestation/sysml_micro_composite.txt | 2 + isolette/attestation/sysml_model_args.json | 3 + isolette/attestation/system.golden | 1 - isolette/attestation/system_args.json | 5 +- .../heat_source_cpi_heat_controller_user.c | 2 +- .../src/operator_interface_oip_oit_user.c | 2 +- .../temperature_sensor_cpi_thermostat_user.c | 2 +- .../src/thermostat_mt_ma_ma_user.c | 2 +- .../src/thermostat_mt_mmi_mmi_user.c | 2 +- .../src/thermostat_mt_mmm_mmm_user.c | 2 +- .../src/thermostat_rt_drf_drf_user.c | 2 +- .../src/thermostat_rt_mhs_mhs_user.c | 6 +- .../src/thermostat_rt_mri_mri_user.c | 2 +- .../src/thermostat_rt_mrm_mrm_user.c | 2 +- isolette/hamr/slang/versions.properties | 6 +- isolette/readme.md | 49 +- .../three_domain_simple/.ci/ci.cmd | 9 +- .../three_domain_simple/aadl/bin/clean.cmd | 2 +- .../{model.golden => aadl_composite.txt} | 0 ...composite.txt => aadl_micro_composite.txt} | 0 .../attestation/aadl_model_args.json | 3 + .../{system.golden => microkit_composite.txt} | Bin .../attestation/model_args.json | 2 - .../attestation/run-attestation.cmd | 129 +++++ .../attestation/system_args.json | 5 +- .../three_domain_simple/readme.md | 11 +- micro-examples/microkit/Dockerfile | 66 ++- .../aadl_port_types/data/array/.ci/ci.cmd | 7 + .../{model.golden => aadl_composite.txt} | 0 ...composite.txt => aadl_micro_composite.txt} | 0 .../array/attestation/aadl_model_args.json | 3 + .../{system.golden => microkit_composite.txt} | 0 .../data/array/attestation/model_args.json | 2 - .../array/attestation/run-attestation.cmd | 129 +++++ .../data/array/attestation/system_args.json | 5 +- .../aadl_port_types/data/array/readme.md | 13 +- .../aadl_port_types/data/base_type/.ci/ci.cmd | 7 + .../{system.golden => aadl_composite.txt} | 0 ...composite.txt => aadl_micro_composite.txt} | Bin .../attestation/aadl_model_args.json | 3 + ...microkit.golden => microkit_composite.txt} | 0 .../base_type/attestation/model_args.json | 2 - .../base_type/attestation/run-attestation.cmd | 129 +++++ .../base_type/attestation/system_args.json | 5 +- .../aadl_port_types/data/base_type/readme.md | 13 +- .../aadl_port_types/data/struct/.ci/ci.cmd | 7 + .../{model.golden => aadl_composite.txt} | 0 ...composite.txt => aadl_micro_composite.txt} | Bin .../struct/attestation/aadl_model_args.json | 3 + .../{system.golden => microkit_composite.txt} | 0 .../data/struct/attestation/model_args.json | 2 - .../struct/attestation/run-attestation.cmd | 129 +++++ .../data/struct/attestation/system_args.json | 5 +- .../aadl_port_types/data/struct/readme.md | 13 +- .../microkit/aadl_port_types/event/.ci/ci.cmd | 7 + .../{model.golden => aadl_composite.txt} | 0 ...composite.txt => aadl_micro_composite.txt} | 0 .../event/attestation/aadl_model_args.json | 3 + .../{system.golden => microkit_composite.txt} | Bin .../event/attestation/model_args.json | 2 - .../event/attestation/run-attestation.cmd | 129 +++++ .../event/attestation/system_args.json | 5 +- .../microkit/aadl_port_types/event/readme.md | 13 +- .../event_data/array/.ci/ci.cmd | 7 + .../{model.golden => aadl_composite.txt} | Bin ...composite.txt => aadl_micro_composite.txt} | 0 .../array/attestation/aadl_model_args.json | 3 + .../{system.golden => microkit_composite.txt} | Bin .../array/attestation/model_args.json | 2 - .../array/attestation/run-attestation.cmd | 129 +++++ .../array/attestation/system_args.json | 5 +- .../event_data/array/readme.md | 13 +- .../event_data/base_type/.ci/ci.cmd | 7 + .../{model.golden => aadl_composite.txt} | 0 ...composite.txt => aadl_micro_composite.txt} | 0 .../attestation/aadl_model_args.json | 3 + .../{system.golden => microkit_composite.txt} | Bin .../base_type/attestation/model_args.json | 2 - .../base_type/attestation/run-attestation.cmd | 129 +++++ .../base_type/attestation/system_args.json | 5 +- .../event_data/base_type/readme.md | 13 +- .../event_data/struct/.ci/ci.cmd | 7 + .../{model.golden => aadl_composite.txt} | 0 ...composite.txt => aadl_micro_composite.txt} | 0 .../struct/attestation/aadl_model_args.json | 3 + .../{system.golden => microkit_composite.txt} | Bin .../struct/attestation/model_args.json | 2 - .../struct/attestation/run-attestation.cmd | 129 +++++ .../struct/attestation/system_args.json | 5 +- .../event_data/struct/readme.md | 12 +- .../port_queues/event_data_array/.ci/ci.cmd | 7 + .../{model.golden => aadl_composite.txt} | 0 ...composite.txt => aadl_micro_composite.txt} | 0 .../attestation/aadl_model_args.json | 3 + .../{system.golden => microkit_composite.txt} | 0 .../attestation/model_args.json | 2 - .../attestation/run-attestation.cmd | 129 +++++ .../attestation/system_args.json | 5 +- .../port_queues/event_data_array/readme.md | 13 +- .../event_data_base_types/.ci/ci.cmd | 7 + .../{model.golden => aadl_composite.txt} | 0 ...composite.txt => aadl_micro_composite.txt} | 0 .../attestation/aadl_model_args.json | 3 + .../{system.golden => microkit_composite.txt} | 0 .../attestation/model_args.json | 2 - .../attestation/run-attestation.cmd | 129 +++++ .../attestation/system_args.json | 5 +- .../event_data_base_types/readme.md | 13 +- .../port_queues/event_data_struct/.ci/ci.cmd | 7 + .../{model.golden => aadl_composite.txt} | 0 ...composite.txt => aadl_micro_composite.txt} | 0 .../attestation/aadl_model_args.json | 3 + .../{system.golden => microkit_composite.txt} | 0 .../attestation/model_args.json | 2 - .../attestation/run-attestation.cmd | 129 +++++ .../attestation/system_args.json | 5 +- .../port_queues/event_data_struct/readme.md | 12 +- .../microkit/vms/data/receiver/.ci/ci.cmd | 11 + .../{model.golden => aadl_composite.txt} | 0 ...composite.txt => aadl_micro_composite.txt} | Bin .../receiver/attestation/aadl_model_args.json | 3 + .../{system.golden => microkit_composite.txt} | 0 .../data/receiver/attestation/model_args.json | 2 - .../receiver/attestation/run-attestation.cmd | 129 +++++ .../receiver/attestation/system_args.json | 5 +- .../isolate-ethernet-simple/.ci/ci.cmd | 9 +- .../aadl/bin/clean.cmd | 2 +- .../aadl/bin/run-hamr.cmd | 2 +- .../attestation/aadl_composite.txt | 1 + .../attestation/aadl_micro_composite.txt | 1 + .../attestation/aadl_model_args.json | 3 + .../attestation/micro_composite.txt | 1 - .../{system.golden => microkit_composite.txt} | 0 .../attestation/model.golden | 1 - .../attestation/model_args.json | 2 - .../attestation/run-attestation.cmd | 129 +++++ .../attestation/system_args.json | 5 +- .../{ => hamr}/microkit/Makefile | 0 .../microkit/components/pacer/src/pacer.c | 0 .../include/seL4_ArduPilot_ArduPilot.h | 0 .../src/seL4_ArduPilot_ArduPilot.c | 0 .../src/seL4_ArduPilot_ArduPilot_MON.c | 0 .../src/seL4_ArduPilot_ArduPilot_user.c | 0 .../include/seL4_Firewall_Firewall.h | 0 .../src/seL4_Firewall_Firewall.c | 0 .../src/seL4_Firewall_Firewall_MON.c | 0 .../src/seL4_Firewall_Firewall_user.c | 0 ...velEthernetDriver_LowLevelEthernetDriver.h | 0 ...velEthernetDriver_LowLevelEthernetDriver.c | 0 ...thernetDriver_LowLevelEthernetDriver_MON.c | 0 ...hernetDriver_LowLevelEthernetDriver_user.c | 0 .../{ => hamr}/microkit/microkit.dot | 0 .../{ => hamr}/microkit/microkit.system | 0 .../{ => hamr}/microkit/system.mk | 0 .../microkit/types/include/sb_aadl_types.h | 0 .../microkit/types/include/sb_event_counter.h | 0 ..._queue_base_SW_RawEthernetMessage_Impl_1.h | 0 .../microkit/types/include/sb_types.h | 0 ..._queue_base_SW_RawEthernetMessage_Impl_1.c | 0 .../{ => hamr}/microkit/util/include/printf.h | 0 .../{ => hamr}/microkit/util/include/util.h | 0 .../{ => hamr}/microkit/util/src/printf.c | 0 .../{ => hamr}/microkit/util/src/util.c | 0 .../isolate-ethernet-simple/readme.md | 12 +- 181 files changed, 2393 insertions(+), 833 deletions(-) delete mode 100755 .github/workflows/hamr-ci.cmd create mode 100755 .github/workflows/hamr/attestation-utils.cmd create mode 100755 .github/workflows/hamr/hamr-ci.cmd create mode 100644 isolette/attestation/aadl_composite.txt create mode 100644 isolette/attestation/aadl_micro_composite.txt create mode 100644 isolette/attestation/aadl_model_args.json delete mode 100644 isolette/attestation/micro_composite.txt create mode 100644 isolette/attestation/microkit_composite.txt delete mode 100644 isolette/attestation/model.golden delete mode 100644 isolette/attestation/model_args.json create mode 100755 isolette/attestation/run-attestation.cmd create mode 100644 isolette/attestation/sysml_composite.txt create mode 100644 isolette/attestation/sysml_micro_composite.txt create mode 100644 isolette/attestation/sysml_model_args.json delete mode 100644 isolette/attestation/system.golden rename micro-examples/domain-scheduling-models/three_domain_simple/attestation/{model.golden => aadl_composite.txt} (100%) rename micro-examples/domain-scheduling-models/three_domain_simple/attestation/{micro_composite.txt => aadl_micro_composite.txt} (100%) create mode 100644 micro-examples/domain-scheduling-models/three_domain_simple/attestation/aadl_model_args.json rename micro-examples/domain-scheduling-models/three_domain_simple/attestation/{system.golden => microkit_composite.txt} (100%) delete mode 100644 micro-examples/domain-scheduling-models/three_domain_simple/attestation/model_args.json create mode 100755 micro-examples/domain-scheduling-models/three_domain_simple/attestation/run-attestation.cmd rename micro-examples/microkit/aadl_port_types/data/array/attestation/{model.golden => aadl_composite.txt} (100%) rename micro-examples/microkit/aadl_port_types/data/array/attestation/{micro_composite.txt => aadl_micro_composite.txt} (100%) create mode 100644 micro-examples/microkit/aadl_port_types/data/array/attestation/aadl_model_args.json rename micro-examples/microkit/aadl_port_types/data/array/attestation/{system.golden => microkit_composite.txt} (100%) delete mode 100644 micro-examples/microkit/aadl_port_types/data/array/attestation/model_args.json create mode 100755 micro-examples/microkit/aadl_port_types/data/array/attestation/run-attestation.cmd rename micro-examples/microkit/aadl_port_types/data/base_type/attestation/{system.golden => aadl_composite.txt} (100%) rename micro-examples/microkit/aadl_port_types/data/base_type/attestation/{micro_composite.txt => aadl_micro_composite.txt} (100%) create mode 100644 micro-examples/microkit/aadl_port_types/data/base_type/attestation/aadl_model_args.json rename micro-examples/microkit/aadl_port_types/data/base_type/attestation/{microkit.golden => microkit_composite.txt} (100%) delete mode 100644 micro-examples/microkit/aadl_port_types/data/base_type/attestation/model_args.json create mode 100755 micro-examples/microkit/aadl_port_types/data/base_type/attestation/run-attestation.cmd rename micro-examples/microkit/aadl_port_types/data/struct/attestation/{model.golden => aadl_composite.txt} (100%) rename micro-examples/microkit/aadl_port_types/data/struct/attestation/{micro_composite.txt => aadl_micro_composite.txt} (100%) create mode 100644 micro-examples/microkit/aadl_port_types/data/struct/attestation/aadl_model_args.json rename micro-examples/microkit/aadl_port_types/data/struct/attestation/{system.golden => microkit_composite.txt} (100%) delete mode 100644 micro-examples/microkit/aadl_port_types/data/struct/attestation/model_args.json create mode 100755 micro-examples/microkit/aadl_port_types/data/struct/attestation/run-attestation.cmd rename micro-examples/microkit/aadl_port_types/event/attestation/{model.golden => aadl_composite.txt} (100%) rename micro-examples/microkit/aadl_port_types/event/attestation/{micro_composite.txt => aadl_micro_composite.txt} (100%) create mode 100644 micro-examples/microkit/aadl_port_types/event/attestation/aadl_model_args.json rename micro-examples/microkit/aadl_port_types/event/attestation/{system.golden => microkit_composite.txt} (100%) delete mode 100644 micro-examples/microkit/aadl_port_types/event/attestation/model_args.json create mode 100755 micro-examples/microkit/aadl_port_types/event/attestation/run-attestation.cmd rename micro-examples/microkit/aadl_port_types/event_data/array/attestation/{model.golden => aadl_composite.txt} (100%) rename micro-examples/microkit/aadl_port_types/event_data/array/attestation/{micro_composite.txt => aadl_micro_composite.txt} (100%) create mode 100644 micro-examples/microkit/aadl_port_types/event_data/array/attestation/aadl_model_args.json rename micro-examples/microkit/aadl_port_types/event_data/array/attestation/{system.golden => microkit_composite.txt} (100%) delete mode 100644 micro-examples/microkit/aadl_port_types/event_data/array/attestation/model_args.json create mode 100755 micro-examples/microkit/aadl_port_types/event_data/array/attestation/run-attestation.cmd rename micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/{model.golden => aadl_composite.txt} (100%) rename micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/{micro_composite.txt => aadl_micro_composite.txt} (100%) create mode 100644 micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/aadl_model_args.json rename micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/{system.golden => microkit_composite.txt} (100%) delete mode 100644 micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/model_args.json create mode 100755 micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/run-attestation.cmd rename micro-examples/microkit/aadl_port_types/event_data/struct/attestation/{model.golden => aadl_composite.txt} (100%) rename micro-examples/microkit/aadl_port_types/event_data/struct/attestation/{micro_composite.txt => aadl_micro_composite.txt} (100%) create mode 100644 micro-examples/microkit/aadl_port_types/event_data/struct/attestation/aadl_model_args.json rename micro-examples/microkit/aadl_port_types/event_data/struct/attestation/{system.golden => microkit_composite.txt} (100%) delete mode 100644 micro-examples/microkit/aadl_port_types/event_data/struct/attestation/model_args.json create mode 100755 micro-examples/microkit/aadl_port_types/event_data/struct/attestation/run-attestation.cmd rename micro-examples/microkit/port_queues/event_data_array/attestation/{model.golden => aadl_composite.txt} (100%) rename micro-examples/microkit/port_queues/event_data_array/attestation/{micro_composite.txt => aadl_micro_composite.txt} (100%) create mode 100644 micro-examples/microkit/port_queues/event_data_array/attestation/aadl_model_args.json rename micro-examples/microkit/port_queues/event_data_array/attestation/{system.golden => microkit_composite.txt} (100%) delete mode 100644 micro-examples/microkit/port_queues/event_data_array/attestation/model_args.json create mode 100755 micro-examples/microkit/port_queues/event_data_array/attestation/run-attestation.cmd rename micro-examples/microkit/port_queues/event_data_base_types/attestation/{model.golden => aadl_composite.txt} (100%) rename micro-examples/microkit/port_queues/event_data_base_types/attestation/{micro_composite.txt => aadl_micro_composite.txt} (100%) create mode 100644 micro-examples/microkit/port_queues/event_data_base_types/attestation/aadl_model_args.json rename micro-examples/microkit/port_queues/event_data_base_types/attestation/{system.golden => microkit_composite.txt} (100%) delete mode 100644 micro-examples/microkit/port_queues/event_data_base_types/attestation/model_args.json create mode 100755 micro-examples/microkit/port_queues/event_data_base_types/attestation/run-attestation.cmd rename micro-examples/microkit/port_queues/event_data_struct/attestation/{model.golden => aadl_composite.txt} (100%) rename micro-examples/microkit/port_queues/event_data_struct/attestation/{micro_composite.txt => aadl_micro_composite.txt} (100%) create mode 100644 micro-examples/microkit/port_queues/event_data_struct/attestation/aadl_model_args.json rename micro-examples/microkit/port_queues/event_data_struct/attestation/{system.golden => microkit_composite.txt} (100%) delete mode 100644 micro-examples/microkit/port_queues/event_data_struct/attestation/model_args.json create mode 100755 micro-examples/microkit/port_queues/event_data_struct/attestation/run-attestation.cmd rename micro-examples/microkit/vms/data/receiver/attestation/{model.golden => aadl_composite.txt} (100%) rename micro-examples/microkit/vms/data/receiver/attestation/{micro_composite.txt => aadl_micro_composite.txt} (100%) create mode 100644 micro-examples/microkit/vms/data/receiver/attestation/aadl_model_args.json rename micro-examples/microkit/vms/data/receiver/attestation/{system.golden => microkit_composite.txt} (100%) delete mode 100644 micro-examples/microkit/vms/data/receiver/attestation/model_args.json create mode 100755 micro-examples/microkit/vms/data/receiver/attestation/run-attestation.cmd create mode 100644 open-platform-models/isolate-ethernet-simple/attestation/aadl_composite.txt create mode 100644 open-platform-models/isolate-ethernet-simple/attestation/aadl_micro_composite.txt create mode 100644 open-platform-models/isolate-ethernet-simple/attestation/aadl_model_args.json delete mode 100644 open-platform-models/isolate-ethernet-simple/attestation/micro_composite.txt rename open-platform-models/isolate-ethernet-simple/attestation/{system.golden => microkit_composite.txt} (100%) delete mode 100644 open-platform-models/isolate-ethernet-simple/attestation/model.golden delete mode 100644 open-platform-models/isolate-ethernet-simple/attestation/model_args.json create mode 100755 open-platform-models/isolate-ethernet-simple/attestation/run-attestation.cmd rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/Makefile (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/components/pacer/src/pacer.c (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/components/seL4_ArduPilot_ArduPilot/include/seL4_ArduPilot_ArduPilot.h (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot.c (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot_MON.c (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot_user.c (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/components/seL4_Firewall_Firewall/include/seL4_Firewall_Firewall.h (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall.c (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall_MON.c (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall_user.c (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/include/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.h (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.c (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_MON.c (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_user.c (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/microkit.dot (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/microkit.system (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/system.mk (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/types/include/sb_aadl_types.h (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/types/include/sb_event_counter.h (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/types/include/sb_queue_base_SW_RawEthernetMessage_Impl_1.h (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/types/include/sb_types.h (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/types/src/sb_queue_base_SW_RawEthernetMessage_Impl_1.c (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/util/include/printf.h (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/util/include/util.h (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/util/src/printf.c (100%) rename open-platform-models/isolate-ethernet-simple/{ => hamr}/microkit/util/src/util.c (100%) diff --git a/.github/workflows/ci-hamr.yml b/.github/workflows/ci-hamr.yml index 5b658e3..6a8ffac 100644 --- a/.github/workflows/ci-hamr.yml +++ b/.github/workflows/ci-hamr.yml @@ -12,12 +12,12 @@ on: - 'micro-examples/microkit/**' - 'isolette/**' schedule: - - cron: "0 2 * * 6" # every sunday at 2am + - cron: "0 2 * * 6" # every sunday at 2am + jobs: - container: + ci: runs-on: ubuntu-latest - container: - image: jasonbelt/microkit_domain_scheduling:latest + container: jasonbelt/microkit_domain_scheduling:latest name: HAMR-codegen steps: - name: Checkout @@ -66,10 +66,11 @@ jobs: export MICROKIT_SDK=$(find /home/microkit/microkit/release/ -type d -name microkit-sdk*) export MICROKIT_BOARD=qemu_virt_aarch64 - export DEMO_ROOT=$HOME/ku + export DEMO_ROOT=$HOME/provers mv $(pwd)/INSPECTA-models $DEMO_ROOT/ + rm -rf ${DEMO_ROOT}/Sireum # remove bootstrap version export SIREUM_HOME=$(pwd)/Sireum export PATH=$SIREUM_HOME/bin:$PATH @@ -88,7 +89,7 @@ jobs: sireum slang run $SIREUM_HOME/hamr/codegen/bin/build.cmd install-osate-gumbo export OSATE_HOME=$SIREUM_HOME/bin/linux/osate - export ASP_BIN=/home/microkit/ku/asp-libs/bin + export ASP_BIN=/home/microkit/provers/asp-libs/bin #env - $DEMO_ROOT/INSPECTA-models/.github/workflows/hamr-ci.cmd + $DEMO_ROOT/INSPECTA-models/.github/workflows/hamr/hamr-ci.cmd diff --git a/.github/workflows/hamr-ci.cmd b/.github/workflows/hamr-ci.cmd deleted file mode 100755 index 1eee34d..0000000 --- a/.github/workflows/hamr-ci.cmd +++ /dev/null @@ -1,98 +0,0 @@ -::/*#! 2> /dev/null # -@ 2>/dev/null # 2>nul & echo off & goto BOF # -if [ -z ${SIREUM_HOME} ]; then # - echo "Please set SIREUM_HOME env var" # - exit -1 # -fi # -exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" # -:BOF -setlocal -if not defined SIREUM_HOME ( - echo Please set SIREUM_HOME env var - exit /B -1 -) -%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* -exit /B %errorlevel% -::!#*/ -// #Sireum - -import org.sireum._ - -val rootDir = Os.slashDir.up.up - -val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" -val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") - -val excludes: ops.ISZOps[Os.Path] = ops.ISZOps(ISZ( - rootDir / "micro-examples" / "case-transition-models" -)) - -var result: Z = 0 -def findCIs(p: Os.Path): Unit = { - if (!excludes.contains(p)) { - if(p.isFile && p.name == "ci.cmd") { - val r = proc"$sireum slang run $p".console.echo.run() - result = result + r.exitCode - result = result + Tasks.attestation(p.up.up) - } else if(p.isDir) { - p.list.foreach((m: Os.Path) => findCIs(m)) - } - } -} -findCIs(rootDir) - -Os.exit(result) - - - -object Tasks { - def run(title: String, verbose: B, proc: OsProto.Proc): Z = { - println(s"$title ...") - val r = (if (verbose) proc.console.echo else proc).run() - - if (r.exitCode != 1) { // TODO Test.sh script grep needs to be updated - println(s"$title failed!") - cprintln(F, r.out) - cprintln(T, r.err) - } - return if (r.exitCode == 1) 0 else 1 - } - - def attestation(p: Os.Path): Z = { - - val attestationDir = p / "attestation" - if (Os.env("MICROKIT_SDK").nonEmpty && Os.env("DEMO_ROOT").nonEmpty && attestationDir.exists) { - println() - val testsDir = Os.path(Os.env("DEMO_ROOT").get) / "am-cakeml" / "tests" - - val micro_composite = testsDir / "DemoFiles" / "goldenFiles"/ "micro_composite.txt" - val cached_micro_composite = p / "attestation" / "micro_composite.txt" - - var aargs = ISZ[String]((testsDir / "CI" / "Test.sh").value, "-t", "micro", "-h", - "-m", (attestationDir / "model_args.json").value, "-s", (attestationDir / "system_args.json").value) - - if (ops.ISZOps(Os.cliArgs).contains("provision")) { - aargs = aargs :+ "-p" - var result = run(s"Provisioning $p", F, Os.proc(aargs)) - if (result == 0) { - micro_composite.copyOverTo(cached_micro_composite) - } - return result - } else { - var result = 1 - for(retry <- 0 until 5 if result != 0) { - cached_micro_composite.copyOverTo(micro_composite) - result = run(s"Appraising $p${if (retry > 0) s": Retry $retry" else ""}", F, Os.proc(aargs)) - assert (result == 0, result) - - val resp = testsDir / "DemoFiles" / "Generated" / "output_resp.json" - println(resp.read) - result = if (resp.read == "Resolute Policy check: SUCCESS") 0 else 1 - } - println(s"Appraisal ${if (result == 0) "succeeded" else "failed"}!") - return result - } - } - return 0 - } -} diff --git a/.github/workflows/hamr/attestation-utils.cmd b/.github/workflows/hamr/attestation-utils.cmd new file mode 100755 index 0000000..098034b --- /dev/null +++ b/.github/workflows/hamr/attestation-utils.cmd @@ -0,0 +1,53 @@ +::/*#! 2> /dev/null # +@ 2>/dev/null # 2>nul & echo off & goto BOF # +if [ -z ${SIREUM_HOME} ]; then # + echo "Please set SIREUM_HOME env var" # + exit -1 # +fi # +exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" # +:BOF +setlocal +if not defined SIREUM_HOME ( + echo Please set SIREUM_HOME env var + exit /B -1 +) +%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* +exit /B %errorlevel% +::!#*/ +// #Sireum + +import org.sireum._ + +val rootDir = Os.slashDir.up.up.up + +val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" +val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") + +val attestations = Os.Path.walk(rootDir, T, T, p => p.name == "attestation" && p.isDir && (p / "run-attestation.cmd").exists) + +val canonical = rootDir / "isolette" / "attestation" / "run-attestation.cmd" + +if (ops.ISZOps(Os.cliArgs).contains("update")) { + for (a <- attestations if (a != canonical.up)) { + a.removeAll() + a.mkdir() + canonical.copyOverTo(a / "run-attestation.cmd") + println(s"Wrote: ${a / "run-attestation.cmd"}") + } +} else if (ops.ISZOps(Os.cliArgs).contains("provision")) { + for (a <- attestations if (a != canonical.up)) { + proc"$sireum slang run ${a / "run-attestation.cmd"} provision".console.run() + } +} else if (ops.ISZOps(Os.cliArgs).contains("appraise")) { + for (a <- attestations) { + if ( (a.up / "aadl").exists) { + proc"$sireum slang run ${a / "run-attestation.cmd"} aadl".console.run() + } + if ( (a.up / "sysml").exists) { + proc"$sireum slang run ${a / "run-attestation.cmd"} sysml".console.run() + } + } +} else { + println("Usage: update | provision | appraise") +} + diff --git a/.github/workflows/hamr/hamr-ci.cmd b/.github/workflows/hamr/hamr-ci.cmd new file mode 100755 index 0000000..a7dddc1 --- /dev/null +++ b/.github/workflows/hamr/hamr-ci.cmd @@ -0,0 +1,43 @@ +::/*#! 2> /dev/null # +@ 2>/dev/null # 2>nul & echo off & goto BOF # +if [ -z ${SIREUM_HOME} ]; then # + echo "Please set SIREUM_HOME env var" # + exit -1 # +fi # +exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" # +:BOF +setlocal +if not defined SIREUM_HOME ( + echo Please set SIREUM_HOME env var + exit /B -1 +) +%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* +exit /B %errorlevel% +::!#*/ +// #Sireum + +import org.sireum._ + +val rootDir = Os.slashDir.up.up.up + +val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" +val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") + +val excludes: ops.ISZOps[Os.Path] = ops.ISZOps(ISZ( + rootDir / "micro-examples" / "case-transition-models" +)) + +var result: Z = 0 +def findCIs(p: Os.Path): Unit = { + if (!excludes.contains(p)) { + if(p.isFile && p.name == "ci.cmd") { + val r = proc"$sireum slang run $p".console.echo.run() + result = result + r.exitCode + } else if(p.isDir) { + p.list.foreach((m: Os.Path) => findCIs(m)) + } + } +} +findCIs(rootDir) + +Os.exit(result) diff --git a/isolette/.ci/ci.cmd b/isolette/.ci/ci.cmd index 7092cc1..41334e3 100755 --- a/isolette/.ci/ci.cmd +++ b/isolette/.ci/ci.cmd @@ -45,16 +45,16 @@ if (result == 0) { result = run("Cleaning", F, proc"$sireum slang run ${homeDir / "aadl" / "bin" / "clean.cmd"}") } -if (result == 0) { - result = run("Running codegen from AADL model targeting JVM", F, proc"$sireum slang run ${homeDir / "aadl" / "bin" / "run-hamr.cmd"} JVM") +if (result == 0 && !(homeDir / "sysml" / "sysml-aadl-libraries").exists) { + result = run("Cloning https://github.com/santoslab/sysml-aadl-libraries.git", F, proc"git clone https://github.com/santoslab/sysml-aadl-libraries.git sysml-aadl-libraries".at(homeDir / "sysml")) } if (result == 0) { - result = run("Verifying via Logika", T, proc"$sireum slang run ${homeDir / "hamr" / "slang" / "bin" / "run-logika.cmd"}") + result = run("Running codegen from AADL model targeting JVM", F, proc"$sireum slang run ${homeDir / "aadl" / "bin" / "run-hamr.cmd"} JVM") } if (result == 0) { - result = run("Cloning https://github.com/santoslab/sysml-aadl-libraries.git", F, proc"git clone https://github.com/santoslab/sysml-aadl-libraries.git sysml/sysml-aadl-libraries".at(homeDir / "sysml")) + result = run("Verifying via Logika", T, proc"$sireum slang run ${homeDir / "hamr" / "slang" / "bin" / "run-logika.cmd"}") } if (result == 0) { @@ -73,16 +73,30 @@ if (result == 0) { result = run("Running codegen from AADL model targeting Microkit", F, proc"$sireum slang run ${homeDir / "aadl" / "bin" / "run-hamr.cmd"} Microkit") } +if (result == 0) { + result = run("Running AADL attestation", F, proc"$sireum slang run ${homeDir / "attestation" / "run-attestation.cmd"} aadl") +} + if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) { result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit")) + if ((homeDir / "hamr" / "microkit" / "build").exists) { + (homeDir / "hamr" / "microkit" / "build").removeAll() + } } if (result == 0) { result = run("Running codegen from SysMLv2 model targeting Microkit", F, proc"$sireum slang run ${homeDir / "sysml" / "bin" / "run-hamr.cmd"} Microkit") } +if (result == 0) { + result = run("Running SysMLv2 attestation", F, proc"$sireum slang run ${homeDir / "attestation" / "run-attestation.cmd"} sysml") +} + if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) { result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit")) + if ((homeDir / "hamr" / "microkit" / "build").exists) { + (homeDir / "hamr" / "microkit" / "build").removeAll() + } } Os.exit(result) diff --git a/isolette/aadl/.slang/Isolette_isolette_single_sensor_Instance.json b/isolette/aadl/.slang/Isolette_isolette_single_sensor_Instance.json index 1866604..3a52c11 100644 --- a/isolette/aadl/.slang/Isolette_isolette_single_sensor_Instance.json +++ b/isolette/aadl/.slang/Isolette_isolette_single_sensor_Instance.json @@ -2972,52 +2972,6 @@ ], "appliesTo" : [ ] - }, - { - "type" : "Property", - "name" : { - "type" : "Name", - "name" : ["Isolette_Single_Sensor_Instance", "thermostat", "rt", "mri", "mri", "Timing_Properties::Compute_Execution_Time"], - "pos" : { - "type" : "Some", - "value" : { - "type" : "Position", - "uriOpt" : { - "type" : "Some", - "value" : "\/org.osate.aadl2.contrib\/resources\/properties\/Predeclared_Property_Sets\/Timing_Properties.aadl" - }, - "beginLine" : 54, - "beginColumn" : 5, - "endLine" : 55, - "endColumn" : 78, - "offset" : 3905, - "length" : 112 - } - } - }, - "propertyValues" : [ - { - "type" : "RangeProp", - "low" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - }, - "high" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - } - } - ], - "appliesTo" : [ - ] } ], "flows" : [ @@ -11693,52 +11647,6 @@ ], "appliesTo" : [ ] - }, - { - "type" : "Property", - "name" : { - "type" : "Name", - "name" : ["Isolette_Single_Sensor_Instance", "thermostat", "rt", "mhs", "mhs", "Timing_Properties::Compute_Execution_Time"], - "pos" : { - "type" : "Some", - "value" : { - "type" : "Position", - "uriOpt" : { - "type" : "Some", - "value" : "\/org.osate.aadl2.contrib\/resources\/properties\/Predeclared_Property_Sets\/Timing_Properties.aadl" - }, - "beginLine" : 54, - "beginColumn" : 5, - "endLine" : 55, - "endColumn" : 78, - "offset" : 3905, - "length" : 112 - } - } - }, - "propertyValues" : [ - { - "type" : "RangeProp", - "low" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - }, - "high" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - } - } - ], - "appliesTo" : [ - ] } ], "flows" : [ @@ -18303,52 +18211,6 @@ ], "appliesTo" : [ ] - }, - { - "type" : "Property", - "name" : { - "type" : "Name", - "name" : ["Isolette_Single_Sensor_Instance", "thermostat", "rt", "mrm", "mrm", "Timing_Properties::Compute_Execution_Time"], - "pos" : { - "type" : "Some", - "value" : { - "type" : "Position", - "uriOpt" : { - "type" : "Some", - "value" : "\/org.osate.aadl2.contrib\/resources\/properties\/Predeclared_Property_Sets\/Timing_Properties.aadl" - }, - "beginLine" : 54, - "beginColumn" : 5, - "endLine" : 55, - "endColumn" : 78, - "offset" : 3905, - "length" : 112 - } - } - }, - "propertyValues" : [ - { - "type" : "RangeProp", - "low" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - }, - "high" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - } - } - ], - "appliesTo" : [ - ] } ], "flows" : [ @@ -26648,52 +26510,6 @@ ], "appliesTo" : [ ] - }, - { - "type" : "Property", - "name" : { - "type" : "Name", - "name" : ["Isolette_Single_Sensor_Instance", "thermostat", "rt", "drf", "drf", "Timing_Properties::Compute_Execution_Time"], - "pos" : { - "type" : "Some", - "value" : { - "type" : "Position", - "uriOpt" : { - "type" : "Some", - "value" : "\/org.osate.aadl2.contrib\/resources\/properties\/Predeclared_Property_Sets\/Timing_Properties.aadl" - }, - "beginLine" : 54, - "beginColumn" : 5, - "endLine" : 55, - "endColumn" : 78, - "offset" : 3905, - "length" : 112 - } - } - }, - "propertyValues" : [ - { - "type" : "RangeProp", - "low" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - }, - "high" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - } - } - ], - "appliesTo" : [ - ] } ], "flows" : [ @@ -32280,52 +32096,6 @@ ], "appliesTo" : [ ] - }, - { - "type" : "Property", - "name" : { - "type" : "Name", - "name" : ["Isolette_Single_Sensor_Instance", "thermostat", "mt", "mmi", "mmi", "Timing_Properties::Compute_Execution_Time"], - "pos" : { - "type" : "Some", - "value" : { - "type" : "Position", - "uriOpt" : { - "type" : "Some", - "value" : "\/org.osate.aadl2.contrib\/resources\/properties\/Predeclared_Property_Sets\/Timing_Properties.aadl" - }, - "beginLine" : 54, - "beginColumn" : 5, - "endLine" : 55, - "endColumn" : 78, - "offset" : 3905, - "length" : 112 - } - } - }, - "propertyValues" : [ - { - "type" : "RangeProp", - "low" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - }, - "high" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - } - } - ], - "appliesTo" : [ - ] } ], "flows" : [ @@ -40123,52 +39893,6 @@ ], "appliesTo" : [ ] - }, - { - "type" : "Property", - "name" : { - "type" : "Name", - "name" : ["Isolette_Single_Sensor_Instance", "thermostat", "mt", "ma", "ma", "Timing_Properties::Compute_Execution_Time"], - "pos" : { - "type" : "Some", - "value" : { - "type" : "Position", - "uriOpt" : { - "type" : "Some", - "value" : "\/org.osate.aadl2.contrib\/resources\/properties\/Predeclared_Property_Sets\/Timing_Properties.aadl" - }, - "beginLine" : 54, - "beginColumn" : 5, - "endLine" : 55, - "endColumn" : 78, - "offset" : 3905, - "length" : 112 - } - } - }, - "propertyValues" : [ - { - "type" : "RangeProp", - "low" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - }, - "high" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - } - } - ], - "appliesTo" : [ - ] } ], "flows" : [ @@ -50042,52 +49766,6 @@ ], "appliesTo" : [ ] - }, - { - "type" : "Property", - "name" : { - "type" : "Name", - "name" : ["Isolette_Single_Sensor_Instance", "thermostat", "mt", "mmm", "mmm", "Timing_Properties::Compute_Execution_Time"], - "pos" : { - "type" : "Some", - "value" : { - "type" : "Position", - "uriOpt" : { - "type" : "Some", - "value" : "\/org.osate.aadl2.contrib\/resources\/properties\/Predeclared_Property_Sets\/Timing_Properties.aadl" - }, - "beginLine" : 54, - "beginColumn" : 5, - "endLine" : 55, - "endColumn" : 78, - "offset" : 3905, - "length" : 112 - } - } - }, - "propertyValues" : [ - { - "type" : "RangeProp", - "low" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - }, - "high" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - } - } - ], - "appliesTo" : [ - ] } ], "flows" : [ @@ -54902,52 +54580,6 @@ ], "appliesTo" : [ ] - }, - { - "type" : "Property", - "name" : { - "type" : "Name", - "name" : ["Isolette_Single_Sensor_Instance", "thermostat", "mt", "dmf", "dmf", "Timing_Properties::Compute_Execution_Time"], - "pos" : { - "type" : "Some", - "value" : { - "type" : "Position", - "uriOpt" : { - "type" : "Some", - "value" : "\/org.osate.aadl2.contrib\/resources\/properties\/Predeclared_Property_Sets\/Timing_Properties.aadl" - }, - "beginLine" : 54, - "beginColumn" : 5, - "endLine" : 55, - "endColumn" : 78, - "offset" : 3905, - "length" : 112 - } - } - }, - "propertyValues" : [ - { - "type" : "RangeProp", - "low" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - }, - "high" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - } - } - ], - "appliesTo" : [ - ] } ], "flows" : [ @@ -63431,52 +63063,6 @@ ], "appliesTo" : [ ] - }, - { - "type" : "Property", - "name" : { - "type" : "Name", - "name" : ["Isolette_Single_Sensor_Instance", "operator_interface", "oip", "oit", "Timing_Properties::Compute_Execution_Time"], - "pos" : { - "type" : "Some", - "value" : { - "type" : "Position", - "uriOpt" : { - "type" : "Some", - "value" : "\/org.osate.aadl2.contrib\/resources\/properties\/Predeclared_Property_Sets\/Timing_Properties.aadl" - }, - "beginLine" : 54, - "beginColumn" : 5, - "endLine" : 55, - "endColumn" : 78, - "offset" : 3905, - "length" : 112 - } - } - }, - "propertyValues" : [ - { - "type" : "RangeProp", - "low" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - }, - "high" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - } - } - ], - "appliesTo" : [ - ] } ], "flows" : [ @@ -67399,52 +66985,6 @@ ], "appliesTo" : [ ] - }, - { - "type" : "Property", - "name" : { - "type" : "Name", - "name" : ["Isolette_Single_Sensor_Instance", "temperature_sensor", "cpi", "thermostat", "Timing_Properties::Compute_Execution_Time"], - "pos" : { - "type" : "Some", - "value" : { - "type" : "Position", - "uriOpt" : { - "type" : "Some", - "value" : "\/org.osate.aadl2.contrib\/resources\/properties\/Predeclared_Property_Sets\/Timing_Properties.aadl" - }, - "beginLine" : 54, - "beginColumn" : 5, - "endLine" : 55, - "endColumn" : 78, - "offset" : 3905, - "length" : 112 - } - } - }, - "propertyValues" : [ - { - "type" : "RangeProp", - "low" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - }, - "high" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - } - } - ], - "appliesTo" : [ - ] } ], "flows" : [ @@ -71040,52 +70580,6 @@ ], "appliesTo" : [ ] - }, - { - "type" : "Property", - "name" : { - "type" : "Name", - "name" : ["Isolette_Single_Sensor_Instance", "heat_source", "cpi", "heat_controller", "Timing_Properties::Compute_Execution_Time"], - "pos" : { - "type" : "Some", - "value" : { - "type" : "Position", - "uriOpt" : { - "type" : "Some", - "value" : "\/org.osate.aadl2.contrib\/resources\/properties\/Predeclared_Property_Sets\/Timing_Properties.aadl" - }, - "beginLine" : 54, - "beginColumn" : 5, - "endLine" : 55, - "endColumn" : 78, - "offset" : 3905, - "length" : 112 - } - } - }, - "propertyValues" : [ - { - "type" : "RangeProp", - "low" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - }, - "high" : { - "type" : "UnitProp", - "value" : "1.0E10", - "unit" : { - "type" : "Some", - "value" : "ps" - } - } - } - ], - "appliesTo" : [ - ] } ], "flows" : [ diff --git a/isolette/aadl/aadl/packages/Abstract_Definitions.aadl b/isolette/aadl/aadl/packages/Abstract_Definitions.aadl index b762bf2..15a1c34 100644 --- a/isolette/aadl/aadl/packages/Abstract_Definitions.aadl +++ b/isolette/aadl/aadl/packages/Abstract_Definitions.aadl @@ -7,7 +7,7 @@ public Period => Isolette_Properties::ThreadPeriod; - Timing_Properties::Compute_Execution_Time => Isolette_Properties::Default_Compute_Execution_Time; + --Timing_Properties::Compute_Execution_Time => Isolette_Properties::Default_Compute_Execution_Time; end Periodic_Thread; diff --git a/isolette/aadl/bin/clean.cmd b/isolette/aadl/bin/clean.cmd index 783136b..d9beac9 100755 --- a/isolette/aadl/bin/clean.cmd +++ b/isolette/aadl/bin/clean.cmd @@ -1,4 +1,4 @@ -::/*#! 2> /dev/null # +::#! 2> /dev/null # @ 2>/dev/null # 2>nul & echo off & goto BOF # if [ -z ${SIREUM_HOME} ]; then # echo "Please set SIREUM_HOME env var" # @@ -13,93 +13,65 @@ if not defined SIREUM_HOME ( ) %SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* exit /B %errorlevel% -::!#*/ +::!# // #Sireum import org.sireum._ -val aadlDir = Os.slashDir.up +val hamrDir: Os.Path = Os.slashDir.up.up / "hamr" +val microkitDir = hamrDir / "microkit" +val slangDir = hamrDir / "slang" +assert (hamrDir.exists) -val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" -val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") - -val osate: Os.Path = Os.env("OSATE_HOME") match { - case Some(s) => Os.path(s) / (if (Os.isWin) "osate.exe" else if (Os.isLinux) "osate" else "Contents/MacOs/osate") - case _ if (Os.isWin) => sireumBin / "win" / "fmide" / "fmide.exe" - case _ if (Os.isMac) => sireumBin / "mac" / "fmide.app" / "Contents" / "MacOs" / "osate" - case _ if (Os.isLinux) => sireumBin / "linux" / "fmide" / "fmide" - case _ => - println("Unsupported operating system") - Os.exit(1) - halt("") +@sig trait Keep { + @pure def keep(f: Os.Path): B } - -if (!osate.exists) { - eprintln("Please install FMIDE (e.g. '$SIREUM_HOME/bin/install/fmide.cmd') or OSATE (e.g. 'sireum hamr phantom -u')") - Os.exit(1) - halt("") +@datatype class KeepPath (path: Os.Path) extends Keep { + @pure def keep(f: Os.Path): B = { + return f == path + } } - -val osireum = ISZ(osate.string, "-nosplash", "--launcher.suppressErrors", "-data", "@user.home/.sireum", "-application", "org.sireum.aadl.osate.cli") - -if(Os.cliArgs.size > 1) { - eprintln("Only expecting a single argument") - Os.exit(1) +@datatype class KeepPattern (pattern: String) extends Keep { + @pure def keep(f: Os.Path): B = { + return ops.StringOps(f.value).contains(pattern) + } } -val platform: String = - if(Os.cliArgs.nonEmpty) Os.cliArgs(0) - else "JVM" - -val packageName = "isolette" - -val excludeComponentImpl = F - -val sel4_output_dir = - if (platform == "Microkit") "microkit" - else "camkes" - -var codegenArgs = ISZ("hamr", "codegen", - "--platform", platform, - "--package-name", packageName, - "--slang-output-dir", (aadlDir.up / "hamr" / "slang").string, - "--output-c-dir", (aadlDir.up / "hamr" / "c").string, - "--sel4-output-dir", (aadlDir.up / "hamr" / sel4_output_dir).string, - "--run-transpiler", - "--bit-width", "32", - "--max-string-size", "256", - "--max-array-size", "1", - "--verbose", - "--workspace-root-dir", aadlDir.string) - -if (platform == "JVM") { - codegenArgs = codegenArgs :+ "--runtime-monitoring" -} else { - println("***********************************************************************") - println(s"Note: runtime-monitoring support is not yet avialable for ${platform}") - println("***********************************************************************") -} - -if (excludeComponentImpl) { - codegenArgs = codegenArgs :+ "--exclude-component-impl" -} +val toKeep = ISZ( + KeepPattern(".gitignore"), + KeepPattern(".idea"), + KeepPattern("clean.cmd"), + KeepPattern("run-hamr.cmd"), + KeepPattern("run-logika.cmd"), + KeepPattern("run-attestation.cmd"), + KeepPath(slangDir / "src" / "main" / "component"), + KeepPath(slangDir / "src" / "test" / "bridge"), + KeepPath(slangDir / "src" / "test" / "system"), + KeepPattern("_user.c") // microkit user implementation files +) -if ((aadlDir.up / "hamr" / "slang" / ".idea").exists) { - codegenArgs = codegenArgs :+ "--no-proyek-ive" +@pure def keep(f: Os.Path): B = { + for (p <- toKeep if p.keep(f)) { + return T + } + return F } -codegenArgs = codegenArgs :+ (aadlDir / ".system").string - -val results = Os.proc(osireum ++ codegenArgs).echo.console.run() - -// Running under windows results in 23 which is an indication -// a platform restart was requested. Codegen completes -// successfully and the cli app returns 0 so -// not sure why this is being issued. -if(results.exitCode == 0 || results.exitCode == 23) { - Os.exit(0) -} else { - println(results.err) - Os.exit(results.exitCode) +def rec(p: Os.Path, onlyDelAutoGen: B): Unit = { + if(p.isFile) { + if ((!keep(p) && !onlyDelAutoGen) || ops.StringOps(p.read).contains("Do not edit")) { + p.remove() + println(s"Removed file: $p") + } + } else { + for (pp <- p.list) { + rec(pp, keep(p) || onlyDelAutoGen) + } + if (p.list.isEmpty) { + p.removeAll() + println(s"Removed empty directory: $p") + } + } } +rec(hamrDir, F) diff --git a/isolette/attestation/aadl_composite.txt b/isolette/attestation/aadl_composite.txt new file mode 100644 index 0000000..4811487 --- /dev/null +++ b/isolette/attestation/aadl_composite.txt @@ -0,0 +1 @@ +Bșo$'AdLxRU \ No newline at end of file diff --git a/isolette/attestation/aadl_micro_composite.txt b/isolette/attestation/aadl_micro_composite.txt new file mode 100644 index 0000000000000000000000000000000000000000..dc4f8e3419556810a6e4c487173829d028a6d62b GIT binary patch literal 32 qcmV+*0N?+_*m$o^#iExc695gFB$kRBSK-3;+O6M)+m3xRfnBfl`o=Dg6F-~a2Z_zA~50PA=UFaQ7m literal 0 HcmV?d00001 diff --git a/isolette/attestation/model.golden b/isolette/attestation/model.golden deleted file mode 100644 index 32ddeb2..0000000 --- a/isolette/attestation/model.golden +++ /dev/null @@ -1 +0,0 @@ -;&jST>M3]A|h:u \ No newline at end of file diff --git a/isolette/attestation/model_args.json b/isolette/attestation/model_args.json deleted file mode 100644 index 7db36ef..0000000 --- a/isolette/attestation/model_args.json +++ /dev/null @@ -1,2 +0,0 @@ -{"filepath": "/INSPECTA-models/isolette/sysml/Isolette.sysml", - "filepath-golden":"/INSPECTA-models/isolette/attestation/model.golden"} diff --git a/isolette/attestation/run-attestation.cmd b/isolette/attestation/run-attestation.cmd new file mode 100755 index 0000000..b3ff5be --- /dev/null +++ b/isolette/attestation/run-attestation.cmd @@ -0,0 +1,129 @@ +::/*#! 2> /dev/null # +@ 2>/dev/null # 2>nul & echo off & goto BOF # +if [ -z ${SIREUM_HOME} ]; then # + echo "Please set SIREUM_HOME env var" # + exit -1 # +fi # +exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" # +:BOF +setlocal +if not defined SIREUM_HOME ( + echo Please set SIREUM_HOME env var + exit /B -1 +) +%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* +exit /B %errorlevel% +::!#*/ +// #Sireum + +import org.sireum._ + +val home = Os.slashDir +val projectDir = home.up + +if (!(ops.ISZOps(Os.cliArgs).contains("aadl")) && + !(ops.ISZOps(Os.cliArgs).contains("sysml")) && + !(ops.ISZOps(Os.cliArgs).contains("provision"))) { + println(st"""Pass one of the following arguments: + | provision: Reruns provisioning + | aadl: Performs an appraisal on the AADL artifacts + | sysml: Performs an appraisal on the SysML artifacts""".render) + Os.exit(0) +} + +val repoRoot = { + def f(p: Os.Path): Option[Os.Path] = { + if ((p / ".git" / "config").exists) { + assert((p / "micro-examples").exists, s"Expected ${p / "micro-examples"} to exist") + return Some(p) + } + return f(p.up) + } + f(projectDir).get +} + +val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" +val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") + +val microkitFile = home.up / "hamr" / "microkit" / "microkit.system" +assert(microkitFile.exists, s"Didn't find MSD at $microkitFile") + +val aadlDir = projectDir / "aadl" +val sysmlDir = projectDir / "sysml" + +val model_args = "model_args.json" +val system_args = home / "system_args.json" + +def makeArgs(extension: String, modelDir: Os.Path): Unit = { + @strictpure def getDir(dir: Os.Path): String = s"/INSPECTA-models/${repoRoot.relativize(dir).value}" + (home / s"${extension}_$model_args").writeOver( + st"""{"dirpath": "${getDir(modelDir)}/", + | "suffix": ".$extension", + | "filepath-golden": "${getDir(home)}/${extension}_composite.txt"}""".render) + system_args.writeOver(st"""{"dirpath": "${getDir(microkitFile.up)}/", + | "suffix": ".system", + | "filepath-golden": "${getDir(home)}/microkit_composite.txt"}""".render) +} + +if (aadlDir.exists) { + makeArgs("aadl", aadlDir) +} + +if (sysmlDir.exists) { + makeArgs("sysml", sysmlDir) +} + + + +def run(title: String, proc: OsProto.Proc, verbose: B, checkExitCode: B): Z = { + println(s"$title ...") + val r = (if (verbose) proc.console.echo else proc).run() + if (checkExitCode &&r.exitCode != 0) { + println(s"$title failed!") + cprintln(F, r.out) + cprintln(T, r.err) + } + return if (r.exitCode == 0) 0 else 1 +} + +val DEMO_ROOT = repoRoot.up +assert (Os.env("DEMO_ROOT").nonEmpty && DEMO_ROOT.value == Os.env("DEMO_ROOT").get, "DEMO_ROOT environment variable not set") + +val testsDir = DEMO_ROOT / "am-cakeml" / "tests" + +val micro_composite = testsDir / "DemoFiles" / "goldenFiles" / "micro_composite.txt" + +var aargs = ISZ[String]((testsDir / "CI" / "Test.sh").value, "-t", "micro", "-h", + "-s", system_args.value) + +if (ops.ISZOps(Os.cliArgs).contains("provision")) { + def provision(extension: String): Unit = { + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + if (cached_micro_composite.exists) { + cached_micro_composite.remove() + } + val f = home / s"${extension}_$model_args" + run(s"Provisioning $f", Os.proc(aargs :+ "-m" :+ f.value :+ "-p"), F, F) + + assert(micro_composite.exists) + micro_composite.copyOverTo(cached_micro_composite) + } + if (aadlDir.exists) { + provision("aadl") + } + if (sysmlDir.exists) { + provision("sysml") + } + Os.exit(0) +} else { + val extension = + if (ops.ISZOps(Os.cliArgs).contains("aadl")) "aadl" + else if (ops.ISZOps(Os.cliArgs).contains("sysml")) "sysml" + else "aadl" + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + cached_micro_composite.copyOverTo(micro_composite) + val f = home / s"${extension}_$model_args" + val result = run(s"Appraising $f", Os.proc(aargs :+ "-m" :+ f.value), F, T) + println(s"Appraisal ${if (result == 0) "succeeded" else "failed"}!") + Os.exit(result) +} \ No newline at end of file diff --git a/isolette/attestation/sysml_composite.txt b/isolette/attestation/sysml_composite.txt new file mode 100644 index 0000000..5448aa6 --- /dev/null +++ b/isolette/attestation/sysml_composite.txt @@ -0,0 +1 @@ +eѰoiTQ @=JuI \ No newline at end of file diff --git a/isolette/attestation/sysml_micro_composite.txt b/isolette/attestation/sysml_micro_composite.txt new file mode 100644 index 0000000..0cbbf30 --- /dev/null +++ b/isolette/attestation/sysml_micro_composite.txt @@ -0,0 +1,2 @@ + (.m +q8;H(uk0b \ No newline at end of file diff --git a/isolette/attestation/sysml_model_args.json b/isolette/attestation/sysml_model_args.json new file mode 100644 index 0000000..fc78bf3 --- /dev/null +++ b/isolette/attestation/sysml_model_args.json @@ -0,0 +1,3 @@ +{"dirpath": "/INSPECTA-models/isolette/sysml/", + "suffix": ".sysml", + "filepath-golden": "/INSPECTA-models/isolette/attestation/sysml_composite.txt"} \ No newline at end of file diff --git a/isolette/attestation/system.golden b/isolette/attestation/system.golden deleted file mode 100644 index 6cf344b..0000000 --- a/isolette/attestation/system.golden +++ /dev/null @@ -1 +0,0 @@ --o8Rs9bΈO7;ٗ^" \ No newline at end of file diff --git a/isolette/attestation/system_args.json b/isolette/attestation/system_args.json index dfcf397..55aed10 100644 --- a/isolette/attestation/system_args.json +++ b/isolette/attestation/system_args.json @@ -1,2 +1,3 @@ -{"filepath": "/INSPECTA-models/isolette/hamr/microkit/microkit.system", - "filepath-golden":"/INSPECTA-models/isolette/attestation/system.golden"} +{"dirpath": "/INSPECTA-models/isolette/hamr/microkit/", + "suffix": ".system", + "filepath-golden": "/INSPECTA-models/isolette/attestation/microkit_composite.txt"} \ No newline at end of file diff --git a/isolette/hamr/microkit/components/heat_source_cpi_heat_controller/src/heat_source_cpi_heat_controller_user.c b/isolette/hamr/microkit/components/heat_source_cpi_heat_controller/src/heat_source_cpi_heat_controller_user.c index 2a96f8c..5e82231 100644 --- a/isolette/hamr/microkit/components/heat_source_cpi_heat_controller/src/heat_source_cpi_heat_controller_user.c +++ b/isolette/hamr/microkit/components/heat_source_cpi_heat_controller/src/heat_source_cpi_heat_controller_user.c @@ -5,7 +5,7 @@ isolette_Isolette_Data_Model_On_Off_Type heater_state = Off; void heat_source_cpi_heat_controller_initialize(void) { - //printf("%s: heat_source_cpi_heat_controller_initialize invoked\n", microkit_name); + printf("%s: heat_source_cpi_heat_controller_initialize invoked\n", microkit_name); heater_state = Off; diff --git a/isolette/hamr/microkit/components/operator_interface_oip_oit/src/operator_interface_oip_oit_user.c b/isolette/hamr/microkit/components/operator_interface_oip_oit/src/operator_interface_oip_oit_user.c index 226622e..b23d375 100644 --- a/isolette/hamr/microkit/components/operator_interface_oip_oit/src/operator_interface_oip_oit_user.c +++ b/isolette/hamr/microkit/components/operator_interface_oip_oit/src/operator_interface_oip_oit_user.c @@ -18,7 +18,7 @@ const isolette_Isolette_Data_Model_TempWstatus_i lastLowerAlarmTempWstatus = ini const isolette_Isolette_Data_Model_TempWstatus_i lastUpperAlarmTempWstatus = initUpperAlarmTempWstatus; void operator_interface_oip_oit_initialize(void) { - //printf("%s: operator_interface_oip_oit_initialize invoked\n", microkit_name); + printf("%s: operator_interface_oip_oit_initialize invoked\n", microkit_name); put_lower_desired_tempWstatus(&initLowerDesiredTempWstatus); put_upper_desired_tempWstatus(&initUpperDesiredTempWstatus); diff --git a/isolette/hamr/microkit/components/temperature_sensor_cpi_thermostat/src/temperature_sensor_cpi_thermostat_user.c b/isolette/hamr/microkit/components/temperature_sensor_cpi_thermostat/src/temperature_sensor_cpi_thermostat_user.c index 0a85805..111d477 100644 --- a/isolette/hamr/microkit/components/temperature_sensor_cpi_thermostat/src/temperature_sensor_cpi_thermostat_user.c +++ b/isolette/hamr/microkit/components/temperature_sensor_cpi_thermostat/src/temperature_sensor_cpi_thermostat_user.c @@ -18,7 +18,7 @@ const float delta = 1; int frame = 0; void temperature_sensor_cpi_thermostat_initialize(void) { - //printf("%s: temperature_sensor_cpi_thermostat_initialize invoked\n", microkit_name); + printf("%s: temperature_sensor_cpi_thermostat_initialize invoked\n", microkit_name); isolette_Isolette_Data_Model_Temp_i defaultTemp = {DEFAULT_CURRENT_TEMPERATURE}; isolette_Isolette_Data_Model_TempWstatus_i defaultTempWstatus = {defaultTemp.degrees, Valid}; diff --git a/isolette/hamr/microkit/components/thermostat_mt_ma_ma/src/thermostat_mt_ma_ma_user.c b/isolette/hamr/microkit/components/thermostat_mt_ma_ma/src/thermostat_mt_ma_ma_user.c index ecc97a0..0ea7bf0 100644 --- a/isolette/hamr/microkit/components/thermostat_mt_ma_ma/src/thermostat_mt_ma_ma_user.c +++ b/isolette/hamr/microkit/components/thermostat_mt_ma_ma/src/thermostat_mt_ma_ma_user.c @@ -5,7 +5,7 @@ isolette_Isolette_Data_Model_On_Off_Type lastCmd = Onn; void thermostat_mt_ma_ma_initialize(void) { - //printf("%s: thermostat_mt_ma_ma_initialize invoked\n", microkit_name); + printf("%s: thermostat_mt_ma_ma_initialize invoked\n", microkit_name); lastCmd = Off; put_alarm_control((const isolette_Isolette_Data_Model_On_Off_Type*) & lastCmd); diff --git a/isolette/hamr/microkit/components/thermostat_mt_mmi_mmi/src/thermostat_mt_mmi_mmi_user.c b/isolette/hamr/microkit/components/thermostat_mt_mmi_mmi/src/thermostat_mt_mmi_mmi_user.c index 9a5e71c..caa30e7 100644 --- a/isolette/hamr/microkit/components/thermostat_mt_mmi_mmi/src/thermostat_mt_mmi_mmi_user.c +++ b/isolette/hamr/microkit/components/thermostat_mt_mmi_mmi/src/thermostat_mt_mmi_mmi_user.c @@ -10,7 +10,7 @@ const bool DEFAULT_MONITOR_INTERFACE_FAILURE_FLAG = false; isolette_Isolette_Data_Model_On_Off_Type lastCmd = Onn; void thermostat_mt_mmi_mmi_initialize(void) { - //printf("%s: thermostat_mt_mmi_mmi_initialize invoked\n", microkit_name); + printf("%s: thermostat_mt_mmi_mmi_initialize invoked\n", microkit_name); // set initial lower desired temp const isolette_Isolette_Data_Model_Temp_i lowerAlarmTemp = { DEFAULT_LOWER_ALARM_TEMPERATURE }; diff --git a/isolette/hamr/microkit/components/thermostat_mt_mmm_mmm/src/thermostat_mt_mmm_mmm_user.c b/isolette/hamr/microkit/components/thermostat_mt_mmm_mmm/src/thermostat_mt_mmm_mmm_user.c index b1e8e61..4efa71b 100644 --- a/isolette/hamr/microkit/components/thermostat_mt_mmm_mmm/src/thermostat_mt_mmm_mmm_user.c +++ b/isolette/hamr/microkit/components/thermostat_mt_mmm_mmm/src/thermostat_mt_mmm_mmm_user.c @@ -9,7 +9,7 @@ bool timeout_condition_satisified() { } void thermostat_mt_mmm_mmm_initialize(void) { - //printf("%s: thermostat_mt_mmm_mmm_initialize invoked\n", microkit_name); + printf("%s: thermostat_mt_mmm_mmm_initialize invoked\n", microkit_name); lastMonitorMode = Init_Monitor_Mode; put_monitor_mode(&lastMonitorMode); diff --git a/isolette/hamr/microkit/components/thermostat_rt_drf_drf/src/thermostat_rt_drf_drf_user.c b/isolette/hamr/microkit/components/thermostat_rt_drf_drf/src/thermostat_rt_drf_drf_user.c index 08cf006..b95723a 100644 --- a/isolette/hamr/microkit/components/thermostat_rt_drf_drf/src/thermostat_rt_drf_drf_user.c +++ b/isolette/hamr/microkit/components/thermostat_rt_drf_drf/src/thermostat_rt_drf_drf_user.c @@ -3,7 +3,7 @@ // This file will not be overwritten if codegen is rerun void thermostat_rt_drf_drf_initialize(void) { - //printf("%s: thermostat_rt_drf_drf_initialize invoked\n", microkit_name); + printf("%s: thermostat_rt_drf_drf_initialize invoked\n", microkit_name); const isolette_Isolette_Data_Model_Failure_Flag_i internal_failure = { false }; put_internal_failure(&internal_failure); diff --git a/isolette/hamr/microkit/components/thermostat_rt_mhs_mhs/src/thermostat_rt_mhs_mhs_user.c b/isolette/hamr/microkit/components/thermostat_rt_mhs_mhs/src/thermostat_rt_mhs_mhs_user.c index ed9d6c5..55322ee 100644 --- a/isolette/hamr/microkit/components/thermostat_rt_mhs_mhs/src/thermostat_rt_mhs_mhs_user.c +++ b/isolette/hamr/microkit/components/thermostat_rt_mhs_mhs/src/thermostat_rt_mhs_mhs_user.c @@ -5,7 +5,7 @@ isolette_Isolette_Data_Model_On_Off_Type lastCmd = Onn; void thermostat_rt_mhs_mhs_initialize(void) { - //printf("%s: thermostat_rt_mhs_mhs_initialize invoked\n", microkit_name); + printf("%s: thermostat_rt_mhs_mhs_initialize invoked\n", microkit_name); lastCmd = Off; // REQ-MHS-1: If the Regulator Mode is INIT, the Heat Control shall be @@ -30,7 +30,9 @@ void thermostat_rt_mhs_mhs_timeTriggered(void) { isolette_Isolette_Data_Model_TempWstatus_i currentTemp; get_current_tempWstatus(¤tTemp); - // -------------- Get values of input ports ------------------ + //================ compute / control logic =========================== + + // current command defaults to value of last command (REQ-MHS-4) isolette_Isolette_Data_Model_On_Off_Type currentCmd = lastCmd; switch (regulator_mode) { diff --git a/isolette/hamr/microkit/components/thermostat_rt_mri_mri/src/thermostat_rt_mri_mri_user.c b/isolette/hamr/microkit/components/thermostat_rt_mri_mri/src/thermostat_rt_mri_mri_user.c index 5fedda7..ca7e592 100644 --- a/isolette/hamr/microkit/components/thermostat_rt_mri_mri/src/thermostat_rt_mri_mri_user.c +++ b/isolette/hamr/microkit/components/thermostat_rt_mri_mri/src/thermostat_rt_mri_mri_user.c @@ -9,7 +9,7 @@ const isolette_Isolette_Data_Model_Status_Type DEFAULT_REGULATOR_STATUS = Init_S const bool DEFAULT_REGULATOR_INTERFACE_FAILURE_FLAG = false; void thermostat_rt_mri_mri_initialize(void) { - //printf("%s: thermostat_rt_mri_mri_initialize invoked\n", microkit_name); + printf("%s: thermostat_rt_mri_mri_initialize invoked\n", microkit_name); // set initial upper desired temp const isolette_Isolette_Data_Model_Temp_i upper = { DEFAULT_UPPER_DESIRED_TEMPERATURE }; diff --git a/isolette/hamr/microkit/components/thermostat_rt_mrm_mrm/src/thermostat_rt_mrm_mrm_user.c b/isolette/hamr/microkit/components/thermostat_rt_mrm_mrm/src/thermostat_rt_mrm_mrm_user.c index c2bd96a..11f7316 100644 --- a/isolette/hamr/microkit/components/thermostat_rt_mrm_mrm/src/thermostat_rt_mrm_mrm_user.c +++ b/isolette/hamr/microkit/components/thermostat_rt_mrm_mrm/src/thermostat_rt_mrm_mrm_user.c @@ -5,7 +5,7 @@ isolette_Isolette_Data_Model_Regulator_Mode_Type lastRegulatorMode = Init_Regulator_Mode; void thermostat_rt_mrm_mrm_initialize(void) { - //printf("%s: thermostat_rt_mrm_mrm_initialize invoked\n", microkit_name); + printf("%s: thermostat_rt_mrm_mrm_initialize invoked\n", microkit_name); lastRegulatorMode = Init_Regulator_Mode; put_regulator_mode(&lastRegulatorMode); diff --git a/isolette/hamr/slang/versions.properties b/isolette/hamr/slang/versions.properties index 84015da..49a4de7 100644 --- a/isolette/hamr/slang/versions.properties +++ b/isolette/hamr/slang/versions.properties @@ -9,11 +9,11 @@ org.sireum%inspector-services-jvm%=0.6-SNAPSHOT # that ship with sireum (i.e. $SIREUM_HOME/bin/sireum --version) # Scala compiler plugin for Slang -org.sireum%%scalac-plugin%=4.20241022.278d005 +org.sireum%%scalac-plugin%=4.20241212.72b1947 -org.sireum.kekinian%%library%=1c0dea6321 +org.sireum.kekinian%%library%=d3c137b291 -org.sireum.kekinian%%hamr-vision%=1c0dea6321 +org.sireum.kekinian%%hamr-vision%=d3c137b291 org.scala-lang%scala-library%=2.13.15 org.scalatest%%scalatest%%=3.2.19 diff --git a/isolette/readme.md b/isolette/readme.md index 8ea575e..09602f2 100644 --- a/isolette/readme.md +++ b/isolette/readme.md @@ -124,6 +124,13 @@ ``` isolette/aadl/bin/run-hamr.cmd Microkit ``` + + Run the following to do an appraisal on the results (appraising will fail if any changes are made to the AADL files or the microkit.system file) + + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "bash \$HOME/bin/install-sireum.sh && \$HOME/provers/INSPECTA-models/isolette/attestation/run-attestation.cmd aadl" + ``` * From the [SysMLv2 model](sysml) @@ -133,6 +140,13 @@ isolette/sysml/bin/run-hamr.cmd Microkit ``` + Run the following to do an appraisal on the results (appraising will fail if any changes are made to the SysML files or the microkit.system file) + + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "\$HOME/provers/INSPECTA-models/isolette/attestation/run-attestation.cmd sysml" + ``` + 1. Build and simulate the seL4 Microkit image Run the following from this repository's root directory. The docker image ``jasonbelt/microkit_domain_scheduling`` contains customized versions of Microkit and seL4 that support domain scheduling. They were built off the following pull requests @@ -141,8 +155,8 @@ - [seL4 #1308](https://github.com/seL4/seL4/pull/1308) ``` - docker run -it --rm -v $(pwd):/home/microkit/ku/INSPECTA-models jasonbelt/microkit_domain_scheduling \ - bash -ci "cd \$HOME/ku/INSPECTA-models/isolette/hamr/microkit && make qemu" + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "cd \$HOME/provers/INSPECTA-models/isolette/hamr/microkit && make qemu" ``` Type ``CTRL-a x`` to exit the QEMU simulation @@ -150,55 +164,82 @@ You should see output similar to the following ``` + Bootstrapping kernel + Warning: Could not infer GIC interrupt target ID, assuming 0. + available phys memory regions: 1 + [60000000..c0000000] + reserved virt address space regions: 3 + [8060000000..8060348000] + [8060348000..80603ae000] + [80603ae000..80603b6000] Booting all finished, dropped to user space MON|INFO: Microkit Bootstrap MON|INFO: bootinfo untyped list matches expected list MON|INFO: Number of bootstrap invocations: 0x0000000a - MON|INFO: Number of system invocations: 0x000002ab + MON|INFO: Number of system invocations: 0x000002ac MON|INFO: completed bootstrap invocations + thermostat_mt_ma: thermostat_mt_ma_ma_initialize invoked MON|INFO: completed system invocations + thermostat_rt_mr: thermostat_rt_mri_mri_initialize invoked + thermostat_rt_mr: thermostat_rt_mrm_mrm_initialize invoked + thermostat_rt_mh: thermostat_rt_mhs_mhs_initialize invoked + thermostat_rt_dr: thermostat_rt_drf_drf_initialize invoked + heat_source_cpi_: heat_source_cpi_heat_controller_initialize invoked + operator_interfa: operator_interface_oip_oit_initialize invoked + temperature_sens: temperature_sensor_cpi_thermostat_initialize invoked + thermostat_mt_mm: thermostat_mt_mmm_mmm_initialize invoked + thermostat_mt_mm: thermostat_mt_mmi_mmi_initialize invoked + thermostat_mt_dm: thermostat_mt_dmf_dmf_timeTriggered invoked operator_interfa: Regulator Status: Init - operator_interfa: Monitor Status: On + operator_interfa: Monitor Status: Init operator_interfa: Display Temperature 0.000000 operator_interfa: Alamr: off ####### FRAME 0 ####### + thermostat_mt_dm: thermostat_mt_dmf_dmf_timeTriggered invoked operator_interfa: Regulator Status: On operator_interfa: Monitor Status: On operator_interfa: Display Temperature 97.000000 operator_interfa: Alamr: off ####### FRAME 1 ####### + thermostat_mt_dm: thermostat_mt_dmf_dmf_timeTriggered invoked heat_source_cpi_: Received command: On operator_interfa: Regulator Status: On operator_interfa: Monitor Status: On operator_interfa: Display Temperature 96.000000 operator_interfa: Alamr: on ####### FRAME 2 ####### + thermostat_mt_dm: thermostat_mt_dmf_dmf_timeTriggered invoked operator_interfa: Regulator Status: On operator_interfa: Monitor Status: On operator_interfa: Display Temperature 97.000000 operator_interfa: Alamr: on ####### FRAME 3 ####### + thermostat_mt_dm: thermostat_mt_dmf_dmf_timeTriggered invoked operator_interfa: Regulator Status: On operator_interfa: Monitor Status: On operator_interfa: Display Temperature 98.000000 operator_interfa: Alamr: off ####### FRAME 4 ####### + thermostat_mt_dm: thermostat_mt_dmf_dmf_timeTriggered invoked operator_interfa: Regulator Status: On operator_interfa: Monitor Status: On operator_interfa: Display Temperature 99.000000 operator_interfa: Alamr: off ####### FRAME 5 ####### + thermostat_mt_dm: thermostat_mt_dmf_dmf_timeTriggered invoked heat_source_cpi_: Received command: Off operator_interfa: Regulator Status: On operator_interfa: Monitor Status: On operator_interfa: Display Temperature 100.000000 operator_interfa: Alamr: off ####### FRAME 6 ####### + thermostat_mt_dm: thermostat_mt_dmf_dmf_timeTriggered invoked operator_interfa: Regulator Status: On operator_interfa: Monitor Status: On operator_interfa: Display Temperature 101.000000 operator_interfa: Alamr: off ####### FRAME 7 ####### + thermostat_mt_dm: thermostat_mt_dmf_dmf_timeTriggered invoked operator_interfa: Regulator Status: On operator_interfa: Monitor Status: On operator_interfa: Display Temperature 102.000000 diff --git a/micro-examples/domain-scheduling-models/three_domain_simple/.ci/ci.cmd b/micro-examples/domain-scheduling-models/three_domain_simple/.ci/ci.cmd index 1f6e231..be79955 100755 --- a/micro-examples/domain-scheduling-models/three_domain_simple/.ci/ci.cmd +++ b/micro-examples/domain-scheduling-models/three_domain_simple/.ci/ci.cmd @@ -50,7 +50,14 @@ if (result == 0) { } if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) { - result = run("Building the image", F, proc"make".at(homeDir / "microkit")) + result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit")) + if ((homeDir / "hamr" / "microkit" / "build").exists) { + (homeDir / "hamr" / "microkit" / "build").removeAll() + } +} + +if (result == 0) { + result = run("Running AADL attestation", F, proc"$sireum slang run ${homeDir / "attestation" / "run-attestation.cmd"} aadl") } Os.exit(result) \ No newline at end of file diff --git a/micro-examples/domain-scheduling-models/three_domain_simple/aadl/bin/clean.cmd b/micro-examples/domain-scheduling-models/three_domain_simple/aadl/bin/clean.cmd index b1fff77..eb202e5 100755 --- a/micro-examples/domain-scheduling-models/three_domain_simple/aadl/bin/clean.cmd +++ b/micro-examples/domain-scheduling-models/three_domain_simple/aadl/bin/clean.cmd @@ -20,7 +20,7 @@ import org.sireum._ val homeDir = Os.slashDir.up -val microkitDir = homeDir / "microkit" +val microkitDir = homeDir / "hamr" / "microkit" @sig trait Keep { @pure def keep(f: Os.Path): B diff --git a/micro-examples/domain-scheduling-models/three_domain_simple/attestation/model.golden b/micro-examples/domain-scheduling-models/three_domain_simple/attestation/aadl_composite.txt similarity index 100% rename from micro-examples/domain-scheduling-models/three_domain_simple/attestation/model.golden rename to micro-examples/domain-scheduling-models/three_domain_simple/attestation/aadl_composite.txt diff --git a/micro-examples/domain-scheduling-models/three_domain_simple/attestation/micro_composite.txt b/micro-examples/domain-scheduling-models/three_domain_simple/attestation/aadl_micro_composite.txt similarity index 100% rename from micro-examples/domain-scheduling-models/three_domain_simple/attestation/micro_composite.txt rename to micro-examples/domain-scheduling-models/three_domain_simple/attestation/aadl_micro_composite.txt diff --git a/micro-examples/domain-scheduling-models/three_domain_simple/attestation/aadl_model_args.json b/micro-examples/domain-scheduling-models/three_domain_simple/attestation/aadl_model_args.json new file mode 100644 index 0000000..c93e682 --- /dev/null +++ b/micro-examples/domain-scheduling-models/three_domain_simple/attestation/aadl_model_args.json @@ -0,0 +1,3 @@ +{"dirpath": "/INSPECTA-models/micro-examples/domain-scheduling-models/three_domain_simple/aadl/", + "suffix": ".aadl", + "filepath-golden": "/INSPECTA-models/micro-examples/domain-scheduling-models/three_domain_simple/attestation/aadl_composite.txt"} \ No newline at end of file diff --git a/micro-examples/domain-scheduling-models/three_domain_simple/attestation/system.golden b/micro-examples/domain-scheduling-models/three_domain_simple/attestation/microkit_composite.txt similarity index 100% rename from micro-examples/domain-scheduling-models/three_domain_simple/attestation/system.golden rename to micro-examples/domain-scheduling-models/three_domain_simple/attestation/microkit_composite.txt diff --git a/micro-examples/domain-scheduling-models/three_domain_simple/attestation/model_args.json b/micro-examples/domain-scheduling-models/three_domain_simple/attestation/model_args.json deleted file mode 100644 index 330d23e..0000000 --- a/micro-examples/domain-scheduling-models/three_domain_simple/attestation/model_args.json +++ /dev/null @@ -1,2 +0,0 @@ -{"filepath": "/INSPECTA-models/micro-examples/domain-scheduling-models/three_domain_simple/aadl/test_data_port_periodic_three_domains.aadl", - "filepath-golden":"/INSPECTA-models/micro-examples/domain-scheduling-models/three_domain_simple/attestation/model.golden"} diff --git a/micro-examples/domain-scheduling-models/three_domain_simple/attestation/run-attestation.cmd b/micro-examples/domain-scheduling-models/three_domain_simple/attestation/run-attestation.cmd new file mode 100755 index 0000000..b3ff5be --- /dev/null +++ b/micro-examples/domain-scheduling-models/three_domain_simple/attestation/run-attestation.cmd @@ -0,0 +1,129 @@ +::/*#! 2> /dev/null # +@ 2>/dev/null # 2>nul & echo off & goto BOF # +if [ -z ${SIREUM_HOME} ]; then # + echo "Please set SIREUM_HOME env var" # + exit -1 # +fi # +exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" # +:BOF +setlocal +if not defined SIREUM_HOME ( + echo Please set SIREUM_HOME env var + exit /B -1 +) +%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* +exit /B %errorlevel% +::!#*/ +// #Sireum + +import org.sireum._ + +val home = Os.slashDir +val projectDir = home.up + +if (!(ops.ISZOps(Os.cliArgs).contains("aadl")) && + !(ops.ISZOps(Os.cliArgs).contains("sysml")) && + !(ops.ISZOps(Os.cliArgs).contains("provision"))) { + println(st"""Pass one of the following arguments: + | provision: Reruns provisioning + | aadl: Performs an appraisal on the AADL artifacts + | sysml: Performs an appraisal on the SysML artifacts""".render) + Os.exit(0) +} + +val repoRoot = { + def f(p: Os.Path): Option[Os.Path] = { + if ((p / ".git" / "config").exists) { + assert((p / "micro-examples").exists, s"Expected ${p / "micro-examples"} to exist") + return Some(p) + } + return f(p.up) + } + f(projectDir).get +} + +val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" +val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") + +val microkitFile = home.up / "hamr" / "microkit" / "microkit.system" +assert(microkitFile.exists, s"Didn't find MSD at $microkitFile") + +val aadlDir = projectDir / "aadl" +val sysmlDir = projectDir / "sysml" + +val model_args = "model_args.json" +val system_args = home / "system_args.json" + +def makeArgs(extension: String, modelDir: Os.Path): Unit = { + @strictpure def getDir(dir: Os.Path): String = s"/INSPECTA-models/${repoRoot.relativize(dir).value}" + (home / s"${extension}_$model_args").writeOver( + st"""{"dirpath": "${getDir(modelDir)}/", + | "suffix": ".$extension", + | "filepath-golden": "${getDir(home)}/${extension}_composite.txt"}""".render) + system_args.writeOver(st"""{"dirpath": "${getDir(microkitFile.up)}/", + | "suffix": ".system", + | "filepath-golden": "${getDir(home)}/microkit_composite.txt"}""".render) +} + +if (aadlDir.exists) { + makeArgs("aadl", aadlDir) +} + +if (sysmlDir.exists) { + makeArgs("sysml", sysmlDir) +} + + + +def run(title: String, proc: OsProto.Proc, verbose: B, checkExitCode: B): Z = { + println(s"$title ...") + val r = (if (verbose) proc.console.echo else proc).run() + if (checkExitCode &&r.exitCode != 0) { + println(s"$title failed!") + cprintln(F, r.out) + cprintln(T, r.err) + } + return if (r.exitCode == 0) 0 else 1 +} + +val DEMO_ROOT = repoRoot.up +assert (Os.env("DEMO_ROOT").nonEmpty && DEMO_ROOT.value == Os.env("DEMO_ROOT").get, "DEMO_ROOT environment variable not set") + +val testsDir = DEMO_ROOT / "am-cakeml" / "tests" + +val micro_composite = testsDir / "DemoFiles" / "goldenFiles" / "micro_composite.txt" + +var aargs = ISZ[String]((testsDir / "CI" / "Test.sh").value, "-t", "micro", "-h", + "-s", system_args.value) + +if (ops.ISZOps(Os.cliArgs).contains("provision")) { + def provision(extension: String): Unit = { + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + if (cached_micro_composite.exists) { + cached_micro_composite.remove() + } + val f = home / s"${extension}_$model_args" + run(s"Provisioning $f", Os.proc(aargs :+ "-m" :+ f.value :+ "-p"), F, F) + + assert(micro_composite.exists) + micro_composite.copyOverTo(cached_micro_composite) + } + if (aadlDir.exists) { + provision("aadl") + } + if (sysmlDir.exists) { + provision("sysml") + } + Os.exit(0) +} else { + val extension = + if (ops.ISZOps(Os.cliArgs).contains("aadl")) "aadl" + else if (ops.ISZOps(Os.cliArgs).contains("sysml")) "sysml" + else "aadl" + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + cached_micro_composite.copyOverTo(micro_composite) + val f = home / s"${extension}_$model_args" + val result = run(s"Appraising $f", Os.proc(aargs :+ "-m" :+ f.value), F, T) + println(s"Appraisal ${if (result == 0) "succeeded" else "failed"}!") + Os.exit(result) +} \ No newline at end of file diff --git a/micro-examples/domain-scheduling-models/three_domain_simple/attestation/system_args.json b/micro-examples/domain-scheduling-models/three_domain_simple/attestation/system_args.json index 039a190..1b713c3 100644 --- a/micro-examples/domain-scheduling-models/three_domain_simple/attestation/system_args.json +++ b/micro-examples/domain-scheduling-models/three_domain_simple/attestation/system_args.json @@ -1,2 +1,3 @@ -{"filepath": "/INSPECTA-models/micro-examples/domain-scheduling-models/three_domain_simple/microkit/microkit.system", - "filepath-golden":"/INSPECTA-models/micro-examples/domain-scheduling-models/three_domain_simple/attestation/system.golden"} +{"dirpath": "/INSPECTA-models/micro-examples/domain-scheduling-models/three_domain_simple/hamr/microkit/", + "suffix": ".system", + "filepath-golden": "/INSPECTA-models/micro-examples/domain-scheduling-models/three_domain_simple/attestation/microkit_composite.txt"} \ No newline at end of file diff --git a/micro-examples/domain-scheduling-models/three_domain_simple/readme.md b/micro-examples/domain-scheduling-models/three_domain_simple/readme.md index 879d843..e2a0c3f 100644 --- a/micro-examples/domain-scheduling-models/three_domain_simple/readme.md +++ b/micro-examples/domain-scheduling-models/three_domain_simple/readme.md @@ -188,6 +188,13 @@ The above strategy with monitors also micro-examples/domain-scheduling-models/three_domain_simple/aadl/bin/run-hamr.cmd ``` + Run the following to do an appraisal on the results (appraising will fail if any changes are made to the AADL files or the microkit.system file) + + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "\$HOME/provers/INSPECTA-models/micro-examples/domain-scheduling-models/three_domain_simple/attestation/run-attestation.cmd aadl" + ``` + 1. Build and simulate the seL4 Microkit image Run the following from this repository's root directory. The docker image ``jasonbelt/microkit_domain_scheduling`` contains customized versions of Microkit and seL4 that support domain scheduling. They were built off the following pull requests @@ -196,8 +203,8 @@ The above strategy with monitors also - [seL4 #1308](https://github.com/seL4/seL4/pull/1308) ``` - docker run -it --rm -v $(pwd):/home/microkit/inspecta-models jasonbelt/microkit_domain_scheduling \ - bash -ci "cd \$HOME/inspecta-models/micro-examples/domain-scheduling-models/three_domain_simple/microkit \ + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "cd \$HOME/provers/INSPECTA-models/micro-examples/domain-scheduling-models/three_domain_simple/hamr/microkit \ && make qemu" ``` diff --git a/micro-examples/microkit/Dockerfile b/micro-examples/microkit/Dockerfile index 9645d57..aff7775 100644 --- a/micro-examples/microkit/Dockerfile +++ b/micro-examples/microkit/Dockerfile @@ -1,3 +1,7 @@ +# Switch 'Docker Virtual Machine Options' to 'Docker VMM' on Apple Silicon if you get build errors on Apple Silicon machines. +# However switch to 'Apple Virtualization framework' + 'Use Rosetta for x86 ...' when running as Docker VMM appears to be +# much slower even though Docker claims Docker VMM is the most performant. +# # docker build -t jasonbelt/microkit_domain_scheduling:latest . # docker login # docker push jasonbelt/microkit_domain_scheduling:latest @@ -6,20 +10,8 @@ FROM --platform=linux/amd64 ubuntu:24.04 ENV USER=microkit -RUN apt-get update && \ - apt install -y software-properties-common && \ - add-apt-repository ppa:deadsnakes/ppa && \ - apt install -y \ - curl wget emacs git sudo \ - gcc-riscv64-unknown-elf \ - cmake pandoc device-tree-compiler ninja-build \ - texlive-latex-base texlive-latex-recommended \ - texlive-fonts-recommended texlive-fonts-extra \ - libxml2-utils \ - python3.9 python3-pip python3.9-venv \ - qemu-system-arm qemu-system-misc \ - clang lld \ - libssl-dev tmux pkg-config netcat-openbsd && \ +RUN apt-get update && apt install -y sudo && \ + rm -rf /var/lib/apt/lists/* && \ useradd -m -s /bin/bash -N ${USER} && \ usermod -s /bin/bash ${USER} && \ echo "${USER} ALL=(ALL) NOPASSWD: ALL" > /etc/sudoers && \ @@ -38,7 +30,25 @@ ADD "https://api.github.com/repos/sel4/microkit/pulls/175/commits?per_page=1" la ADD "https://api.github.com/repos/ku-sldg/am-cakeml/commits/resolute?per_page=1" latest_am-cakeml_commit ADD "https://api.github.com/repos/ku-sldg/asp-libs/commits/resolute?per_page=1" latest_asp-libs_commit -RUN rm -rf latest_am-cakeml_commit latest_asp-libs_commit latest_sel4_commit latest_microkit_commit && \ +RUN sudo apt-get update && sudo apt install -y software-properties-common && \ + sudo add-apt-repository ppa:deadsnakes/ppa && \ + sudo apt install -y \ + curl wget emacs git \ + gcc-riscv64-unknown-elf \ + cmake pandoc device-tree-compiler ninja-build \ + texlive-latex-base texlive-latex-recommended \ + texlive-fonts-recommended texlive-fonts-extra \ + libxml2-utils \ + python3.9 python3-pip python3.9-venv \ + qemu-system-arm qemu-system-misc \ + clang lld \ + libssl-dev pkg-config netcat-openbsd \ + default-jre && \ + sudo rm -rf /var/lib/apt/lists/* && \ + rm -rf latest_am-cakeml_commit latest_asp-libs_commit latest_sel4_commit latest_microkit_commit && \ + echo "************************************************" && \ + echo "* Installing Rust *" && \ + echo "************************************************" && \ wget -O rustup-init.sh https://sh.rustup.rs && sh ${HOME}/rustup-init.sh -y && rm ${HOME}/rustup-init.sh && . ${HOME}/.cargo/env && \ rustup target add x86_64-unknown-linux-musl && rustup target add aarch64-unknown-linux-musl && \ echo "************************************************" && \ @@ -60,17 +70,31 @@ RUN rm -rf latest_am-cakeml_commit latest_asp-libs_commit latest_sel4_commit lat microkit=$(find ~/microkit/release/ -type d -name microkit-sdk*) && \ echo "export MICROKIT_SDK=${microkit}" >> ${HOME}/.bashrc && \ echo "export MICROKIT_BOARD=qemu_virt_aarch64" >> ${HOME}/.bashrc && \ + mkdir -p ${HOME}/provers && cd ${HOME}/provers && \ + echo "********************************************************************************" && \ + echo "* Installing a very minimal Sireum dist (e.g. uses container's jre rather than *" && \ + echo "* downloading a JDK) so that Slash scripts can be run *" && \ + echo "********************************************************************************" && \ + mkdir -p ${HOME}/provers/Sireum/bin/linux/java && ln -s /usr/lib/jvm/java-21-openjdk-amd64/* ${HOME}/provers/Sireum/bin/linux/java/ && \ + wget https://raw.githubusercontent.com/sireum/kekinian/refs/heads/master/versions.properties -O ${HOME}/provers/Sireum/versions.properties && echo "$(grep "^org.sireum.version.java=" provers/Sireum/versions.properties | cut -d'=' -f2)" > ${HOME}/provers/Sireum/bin/linux/java/VER && \ + wget https://raw.githubusercontent.com/sireum/kekinian/refs/heads/master/bin/init.sh -O ${HOME}/provers/Sireum/bin/init.sh && chmod 700 ${HOME}/provers/Sireum/bin/init.sh && SIREUM_NO_SETUP=true ${HOME}/provers/Sireum/bin/init.sh && ${HOME}/provers/Sireum/bin/sireum --init && \ + rm -rf ${HOME}/provers/Sireum/bin/linux/cs ${HOME}/provers/Sireum/bin/linux/cvc* ${HOME}/provers/Sireum/bin/linux/z3 ${HOME}/provers/Sireum/lib/jacoco* ${HOME}/provers/Sireum/lib/marytts_text2wav.jar && rm -rf ${HOME}/Downloads/sireum && \ + echo "export SIREUM_HOME=${HOME}/provers/Sireum" >> ${HOME}/.bashrc && \ echo "************************************************" && \ echo "* Building KU tools *" && \ echo "************************************************" && \ export PKG_CONFIG_PATH=/usr/lib/x86_64-linux-gnu/pkgconfig/ && \ - mkdir ${HOME}/ku && cd ${HOME}/ku && \ - wget https://github.com/CakeML/cakeml/releases/download/v2076/cake-x64-64.tar.gz && tar xzf cake-x64-64.tar.gz && \ - cd cake-x64-64 && make cake && sudo cp cake /usr/bin && cd ${HOME}/ku && rm -rf ${HOME}/ku/cake-x64-64* &&\ + wget https://github.com/CakeML/cakeml/releases/download/v2747/cake-x64-64.tar.gz && tar xzf cake-x64-64.tar.gz && \ + cd cake-x64-64 && make cake && sudo cp cake /usr/bin && cd ${HOME}/provers && rm -rf ${HOME}/provers/cake-x64-64* &&\ git clone -b resolute https://github.com/ku-sldg/am-cakeml.git && mkdir -p am-cakeml/build && cd am-cakeml/build && \ - cmake .. && make && cd ${HOME}/ku && \ + cmake .. && make && cd ${HOME}/provers && \ git clone -b resolute https://github.com/ku-sldg/asp-libs.git && cd asp-libs && make && \ - echo "export ASP_BIN=${HOME}/ku/asp-libs/bin" >> ${HOME}/.bashrc && \ + echo "export ASP_BIN=${HOME}/provers/asp-libs/bin" >> ${HOME}/.bashrc && \ + echo "export DEMO_ROOT=${HOME}/provers" >> ${HOME}/.bashrc && \ echo "alias env='env | sort'" >> ${HOME}/.bash_aliases && \ echo "alias dir='ls -lFGa'" >> ${HOME}/.bash_aliases && \ - echo "alias ..='cd ..'" >> ${HOME}/.bash_aliases + echo "alias ..='cd ..'" >> ${HOME}/.bash_aliases && \ + sudo apt purge --auto-remove -y \ + pandoc texlive-latex-base texlive-latex-recommended \ + texlive-fonts-recommended texlive-fonts-extra libxml2-utils + diff --git a/micro-examples/microkit/aadl_port_types/data/array/.ci/ci.cmd b/micro-examples/microkit/aadl_port_types/data/array/.ci/ci.cmd index 2043bd0..1e48a01 100755 --- a/micro-examples/microkit/aadl_port_types/data/array/.ci/ci.cmd +++ b/micro-examples/microkit/aadl_port_types/data/array/.ci/ci.cmd @@ -51,6 +51,13 @@ if (result == 0) { if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) { result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit")) + if ((homeDir / "hamr" / "microkit" / "build").exists) { + (homeDir / "hamr" / "microkit" / "build").removeAll() + } +} + +if (result == 0) { + result = run("Running AADL attestation", F, proc"$sireum slang run ${homeDir / "attestation" / "run-attestation.cmd"} aadl") } Os.exit(result) \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/data/array/attestation/model.golden b/micro-examples/microkit/aadl_port_types/data/array/attestation/aadl_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/data/array/attestation/model.golden rename to micro-examples/microkit/aadl_port_types/data/array/attestation/aadl_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/data/array/attestation/micro_composite.txt b/micro-examples/microkit/aadl_port_types/data/array/attestation/aadl_micro_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/data/array/attestation/micro_composite.txt rename to micro-examples/microkit/aadl_port_types/data/array/attestation/aadl_micro_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/data/array/attestation/aadl_model_args.json b/micro-examples/microkit/aadl_port_types/data/array/attestation/aadl_model_args.json new file mode 100644 index 0000000..506a686 --- /dev/null +++ b/micro-examples/microkit/aadl_port_types/data/array/attestation/aadl_model_args.json @@ -0,0 +1,3 @@ +{"dirpath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/array/aadl/", + "suffix": ".aadl", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/array/attestation/aadl_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/data/array/attestation/system.golden b/micro-examples/microkit/aadl_port_types/data/array/attestation/microkit_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/data/array/attestation/system.golden rename to micro-examples/microkit/aadl_port_types/data/array/attestation/microkit_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/data/array/attestation/model_args.json b/micro-examples/microkit/aadl_port_types/data/array/attestation/model_args.json deleted file mode 100644 index feeec0f..0000000 --- a/micro-examples/microkit/aadl_port_types/data/array/attestation/model_args.json +++ /dev/null @@ -1,2 +0,0 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/array/aadl/data_1_prod_2_cons.aadl", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/array/attestation/model.golden"} diff --git a/micro-examples/microkit/aadl_port_types/data/array/attestation/run-attestation.cmd b/micro-examples/microkit/aadl_port_types/data/array/attestation/run-attestation.cmd new file mode 100755 index 0000000..b3ff5be --- /dev/null +++ b/micro-examples/microkit/aadl_port_types/data/array/attestation/run-attestation.cmd @@ -0,0 +1,129 @@ +::/*#! 2> /dev/null # +@ 2>/dev/null # 2>nul & echo off & goto BOF # +if [ -z ${SIREUM_HOME} ]; then # + echo "Please set SIREUM_HOME env var" # + exit -1 # +fi # +exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" # +:BOF +setlocal +if not defined SIREUM_HOME ( + echo Please set SIREUM_HOME env var + exit /B -1 +) +%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* +exit /B %errorlevel% +::!#*/ +// #Sireum + +import org.sireum._ + +val home = Os.slashDir +val projectDir = home.up + +if (!(ops.ISZOps(Os.cliArgs).contains("aadl")) && + !(ops.ISZOps(Os.cliArgs).contains("sysml")) && + !(ops.ISZOps(Os.cliArgs).contains("provision"))) { + println(st"""Pass one of the following arguments: + | provision: Reruns provisioning + | aadl: Performs an appraisal on the AADL artifacts + | sysml: Performs an appraisal on the SysML artifacts""".render) + Os.exit(0) +} + +val repoRoot = { + def f(p: Os.Path): Option[Os.Path] = { + if ((p / ".git" / "config").exists) { + assert((p / "micro-examples").exists, s"Expected ${p / "micro-examples"} to exist") + return Some(p) + } + return f(p.up) + } + f(projectDir).get +} + +val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" +val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") + +val microkitFile = home.up / "hamr" / "microkit" / "microkit.system" +assert(microkitFile.exists, s"Didn't find MSD at $microkitFile") + +val aadlDir = projectDir / "aadl" +val sysmlDir = projectDir / "sysml" + +val model_args = "model_args.json" +val system_args = home / "system_args.json" + +def makeArgs(extension: String, modelDir: Os.Path): Unit = { + @strictpure def getDir(dir: Os.Path): String = s"/INSPECTA-models/${repoRoot.relativize(dir).value}" + (home / s"${extension}_$model_args").writeOver( + st"""{"dirpath": "${getDir(modelDir)}/", + | "suffix": ".$extension", + | "filepath-golden": "${getDir(home)}/${extension}_composite.txt"}""".render) + system_args.writeOver(st"""{"dirpath": "${getDir(microkitFile.up)}/", + | "suffix": ".system", + | "filepath-golden": "${getDir(home)}/microkit_composite.txt"}""".render) +} + +if (aadlDir.exists) { + makeArgs("aadl", aadlDir) +} + +if (sysmlDir.exists) { + makeArgs("sysml", sysmlDir) +} + + + +def run(title: String, proc: OsProto.Proc, verbose: B, checkExitCode: B): Z = { + println(s"$title ...") + val r = (if (verbose) proc.console.echo else proc).run() + if (checkExitCode &&r.exitCode != 0) { + println(s"$title failed!") + cprintln(F, r.out) + cprintln(T, r.err) + } + return if (r.exitCode == 0) 0 else 1 +} + +val DEMO_ROOT = repoRoot.up +assert (Os.env("DEMO_ROOT").nonEmpty && DEMO_ROOT.value == Os.env("DEMO_ROOT").get, "DEMO_ROOT environment variable not set") + +val testsDir = DEMO_ROOT / "am-cakeml" / "tests" + +val micro_composite = testsDir / "DemoFiles" / "goldenFiles" / "micro_composite.txt" + +var aargs = ISZ[String]((testsDir / "CI" / "Test.sh").value, "-t", "micro", "-h", + "-s", system_args.value) + +if (ops.ISZOps(Os.cliArgs).contains("provision")) { + def provision(extension: String): Unit = { + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + if (cached_micro_composite.exists) { + cached_micro_composite.remove() + } + val f = home / s"${extension}_$model_args" + run(s"Provisioning $f", Os.proc(aargs :+ "-m" :+ f.value :+ "-p"), F, F) + + assert(micro_composite.exists) + micro_composite.copyOverTo(cached_micro_composite) + } + if (aadlDir.exists) { + provision("aadl") + } + if (sysmlDir.exists) { + provision("sysml") + } + Os.exit(0) +} else { + val extension = + if (ops.ISZOps(Os.cliArgs).contains("aadl")) "aadl" + else if (ops.ISZOps(Os.cliArgs).contains("sysml")) "sysml" + else "aadl" + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + cached_micro_composite.copyOverTo(micro_composite) + val f = home / s"${extension}_$model_args" + val result = run(s"Appraising $f", Os.proc(aargs :+ "-m" :+ f.value), F, T) + println(s"Appraisal ${if (result == 0) "succeeded" else "failed"}!") + Os.exit(result) +} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/data/array/attestation/system_args.json b/micro-examples/microkit/aadl_port_types/data/array/attestation/system_args.json index 5266f95..780bb5a 100644 --- a/micro-examples/microkit/aadl_port_types/data/array/attestation/system_args.json +++ b/micro-examples/microkit/aadl_port_types/data/array/attestation/system_args.json @@ -1,2 +1,3 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/array/hamr/microkit/microkit.system", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/array/attestation/system.golden"} +{"dirpath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/array/hamr/microkit/", + "suffix": ".system", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/array/attestation/microkit_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/data/array/readme.md b/micro-examples/microkit/aadl_port_types/data/array/readme.md index 01b5ada..72a90ec 100644 --- a/micro-examples/microkit/aadl_port_types/data/array/readme.md +++ b/micro-examples/microkit/aadl_port_types/data/array/readme.md @@ -92,6 +92,13 @@ micro-examples/microkit/aadl_port_types/data/array/aadl/bin/run-hamr.cmd ``` + Run the following to do an appraisal on the results (appraising will fail if any changes are made to the AADL files or the microkit.system file) + + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "\$HOME/provers/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/array/attestation/run-attestation.cmd aadl" + ``` + 1. Build and simulate the seL4 Microkit image Run the following from this repository's root directory. The docker image ``jasonbelt/microkit_domain_scheduling`` contains customized versions of Microkit and seL4 that support domain scheduling. They were built off the following pull requests @@ -99,9 +106,9 @@ - [microkit #175](https://github.com/seL4/microkit/pull/175) - [seL4 #1308](https://github.com/seL4/seL4/pull/1308) - ``` - docker run -it --rm -v $(pwd):/home/microkit/inspecta-models jasonbelt/microkit_domain_scheduling \ - bash -ci "cd \$HOME/inspecta-models/micro-examples/microkit/aadl_port_types/data/array/hamr/microkit \ + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "cd \$HOME/provers/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/array/hamr/microkit \ && make qemu" ``` diff --git a/micro-examples/microkit/aadl_port_types/data/base_type/.ci/ci.cmd b/micro-examples/microkit/aadl_port_types/data/base_type/.ci/ci.cmd index d1790a8..4953363 100755 --- a/micro-examples/microkit/aadl_port_types/data/base_type/.ci/ci.cmd +++ b/micro-examples/microkit/aadl_port_types/data/base_type/.ci/ci.cmd @@ -51,6 +51,13 @@ if (result == 0) { if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) { result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit")) + if ((homeDir / "hamr" / "microkit" / "build").exists) { + (homeDir / "hamr" / "microkit" / "build").removeAll() + } +} + +if (result == 0) { + result = run("Running AADL attestation", F, proc"$sireum slang run ${homeDir / "attestation" / "run-attestation.cmd"} aadl") } Os.exit(result) \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/data/base_type/attestation/system.golden b/micro-examples/microkit/aadl_port_types/data/base_type/attestation/aadl_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/data/base_type/attestation/system.golden rename to micro-examples/microkit/aadl_port_types/data/base_type/attestation/aadl_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/data/base_type/attestation/micro_composite.txt b/micro-examples/microkit/aadl_port_types/data/base_type/attestation/aadl_micro_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/data/base_type/attestation/micro_composite.txt rename to micro-examples/microkit/aadl_port_types/data/base_type/attestation/aadl_micro_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/data/base_type/attestation/aadl_model_args.json b/micro-examples/microkit/aadl_port_types/data/base_type/attestation/aadl_model_args.json new file mode 100644 index 0000000..570e7fa --- /dev/null +++ b/micro-examples/microkit/aadl_port_types/data/base_type/attestation/aadl_model_args.json @@ -0,0 +1,3 @@ +{"dirpath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/base_type/aadl/", + "suffix": ".aadl", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/base_type/attestation/aadl_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/data/base_type/attestation/microkit.golden b/micro-examples/microkit/aadl_port_types/data/base_type/attestation/microkit_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/data/base_type/attestation/microkit.golden rename to micro-examples/microkit/aadl_port_types/data/base_type/attestation/microkit_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/data/base_type/attestation/model_args.json b/micro-examples/microkit/aadl_port_types/data/base_type/attestation/model_args.json deleted file mode 100644 index a2d7526..0000000 --- a/micro-examples/microkit/aadl_port_types/data/base_type/attestation/model_args.json +++ /dev/null @@ -1,2 +0,0 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/base_type/aadl/data_1_prod_2_cons.aadl", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/base_type/attestation/system.golden"} diff --git a/micro-examples/microkit/aadl_port_types/data/base_type/attestation/run-attestation.cmd b/micro-examples/microkit/aadl_port_types/data/base_type/attestation/run-attestation.cmd new file mode 100755 index 0000000..b3ff5be --- /dev/null +++ b/micro-examples/microkit/aadl_port_types/data/base_type/attestation/run-attestation.cmd @@ -0,0 +1,129 @@ +::/*#! 2> /dev/null # +@ 2>/dev/null # 2>nul & echo off & goto BOF # +if [ -z ${SIREUM_HOME} ]; then # + echo "Please set SIREUM_HOME env var" # + exit -1 # +fi # +exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" # +:BOF +setlocal +if not defined SIREUM_HOME ( + echo Please set SIREUM_HOME env var + exit /B -1 +) +%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* +exit /B %errorlevel% +::!#*/ +// #Sireum + +import org.sireum._ + +val home = Os.slashDir +val projectDir = home.up + +if (!(ops.ISZOps(Os.cliArgs).contains("aadl")) && + !(ops.ISZOps(Os.cliArgs).contains("sysml")) && + !(ops.ISZOps(Os.cliArgs).contains("provision"))) { + println(st"""Pass one of the following arguments: + | provision: Reruns provisioning + | aadl: Performs an appraisal on the AADL artifacts + | sysml: Performs an appraisal on the SysML artifacts""".render) + Os.exit(0) +} + +val repoRoot = { + def f(p: Os.Path): Option[Os.Path] = { + if ((p / ".git" / "config").exists) { + assert((p / "micro-examples").exists, s"Expected ${p / "micro-examples"} to exist") + return Some(p) + } + return f(p.up) + } + f(projectDir).get +} + +val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" +val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") + +val microkitFile = home.up / "hamr" / "microkit" / "microkit.system" +assert(microkitFile.exists, s"Didn't find MSD at $microkitFile") + +val aadlDir = projectDir / "aadl" +val sysmlDir = projectDir / "sysml" + +val model_args = "model_args.json" +val system_args = home / "system_args.json" + +def makeArgs(extension: String, modelDir: Os.Path): Unit = { + @strictpure def getDir(dir: Os.Path): String = s"/INSPECTA-models/${repoRoot.relativize(dir).value}" + (home / s"${extension}_$model_args").writeOver( + st"""{"dirpath": "${getDir(modelDir)}/", + | "suffix": ".$extension", + | "filepath-golden": "${getDir(home)}/${extension}_composite.txt"}""".render) + system_args.writeOver(st"""{"dirpath": "${getDir(microkitFile.up)}/", + | "suffix": ".system", + | "filepath-golden": "${getDir(home)}/microkit_composite.txt"}""".render) +} + +if (aadlDir.exists) { + makeArgs("aadl", aadlDir) +} + +if (sysmlDir.exists) { + makeArgs("sysml", sysmlDir) +} + + + +def run(title: String, proc: OsProto.Proc, verbose: B, checkExitCode: B): Z = { + println(s"$title ...") + val r = (if (verbose) proc.console.echo else proc).run() + if (checkExitCode &&r.exitCode != 0) { + println(s"$title failed!") + cprintln(F, r.out) + cprintln(T, r.err) + } + return if (r.exitCode == 0) 0 else 1 +} + +val DEMO_ROOT = repoRoot.up +assert (Os.env("DEMO_ROOT").nonEmpty && DEMO_ROOT.value == Os.env("DEMO_ROOT").get, "DEMO_ROOT environment variable not set") + +val testsDir = DEMO_ROOT / "am-cakeml" / "tests" + +val micro_composite = testsDir / "DemoFiles" / "goldenFiles" / "micro_composite.txt" + +var aargs = ISZ[String]((testsDir / "CI" / "Test.sh").value, "-t", "micro", "-h", + "-s", system_args.value) + +if (ops.ISZOps(Os.cliArgs).contains("provision")) { + def provision(extension: String): Unit = { + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + if (cached_micro_composite.exists) { + cached_micro_composite.remove() + } + val f = home / s"${extension}_$model_args" + run(s"Provisioning $f", Os.proc(aargs :+ "-m" :+ f.value :+ "-p"), F, F) + + assert(micro_composite.exists) + micro_composite.copyOverTo(cached_micro_composite) + } + if (aadlDir.exists) { + provision("aadl") + } + if (sysmlDir.exists) { + provision("sysml") + } + Os.exit(0) +} else { + val extension = + if (ops.ISZOps(Os.cliArgs).contains("aadl")) "aadl" + else if (ops.ISZOps(Os.cliArgs).contains("sysml")) "sysml" + else "aadl" + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + cached_micro_composite.copyOverTo(micro_composite) + val f = home / s"${extension}_$model_args" + val result = run(s"Appraising $f", Os.proc(aargs :+ "-m" :+ f.value), F, T) + println(s"Appraisal ${if (result == 0) "succeeded" else "failed"}!") + Os.exit(result) +} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/data/base_type/attestation/system_args.json b/micro-examples/microkit/aadl_port_types/data/base_type/attestation/system_args.json index c9acb83..a981e2e 100644 --- a/micro-examples/microkit/aadl_port_types/data/base_type/attestation/system_args.json +++ b/micro-examples/microkit/aadl_port_types/data/base_type/attestation/system_args.json @@ -1,2 +1,3 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/base_type/hamr/microkit/microkit.system", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/base_type/attestation/microkit.golden"} +{"dirpath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/base_type/hamr/microkit/", + "suffix": ".system", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/base_type/attestation/microkit_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/data/base_type/readme.md b/micro-examples/microkit/aadl_port_types/data/base_type/readme.md index eac1ed0..a0eb808 100644 --- a/micro-examples/microkit/aadl_port_types/data/base_type/readme.md +++ b/micro-examples/microkit/aadl_port_types/data/base_type/readme.md @@ -92,6 +92,13 @@ micro-examples/microkit/aadl_port_types/data/base_type/aadl/bin/run-hamr.cmd ``` + Run the following to do an appraisal on the results (appraising will fail if any changes are made to the AADL files or the microkit.system file) + + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "\$HOME/provers/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/base_type/attestation/run-attestation.cmd aadl" + ``` + 1. Build and simulate the seL4 Microkit image Run the following from this repository's root directory. The docker image ``jasonbelt/microkit_domain_scheduling`` contains customized versions of Microkit and seL4 that support domain scheduling. They were built off the following pull requests @@ -99,9 +106,9 @@ - [microkit #175](https://github.com/seL4/microkit/pull/175) - [seL4 #1308](https://github.com/seL4/seL4/pull/1308) - ``` - docker run -it --rm -v $(pwd):/home/microkit/inspecta-models jasonbelt/microkit_domain_scheduling \ - bash -ci "cd \$HOME/inspecta-models/micro-examples/microkit/aadl_port_types/data/base_type/hamr/microkit \ + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "cd \$HOME/provers/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/base_type/hamr/microkit \ && make qemu" ``` diff --git a/micro-examples/microkit/aadl_port_types/data/struct/.ci/ci.cmd b/micro-examples/microkit/aadl_port_types/data/struct/.ci/ci.cmd index 7f3fbf9..50675e6 100755 --- a/micro-examples/microkit/aadl_port_types/data/struct/.ci/ci.cmd +++ b/micro-examples/microkit/aadl_port_types/data/struct/.ci/ci.cmd @@ -51,6 +51,13 @@ if (result == 0) { if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) { result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit")) + if ((homeDir / "hamr" / "microkit" / "build").exists) { + (homeDir / "hamr" / "microkit" / "build").removeAll() + } +} + +if (result == 0) { + result = run("Running AADL attestation", F, proc"$sireum slang run ${homeDir / "attestation" / "run-attestation.cmd"} aadl") } Os.exit(result) \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/data/struct/attestation/model.golden b/micro-examples/microkit/aadl_port_types/data/struct/attestation/aadl_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/data/struct/attestation/model.golden rename to micro-examples/microkit/aadl_port_types/data/struct/attestation/aadl_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/data/struct/attestation/micro_composite.txt b/micro-examples/microkit/aadl_port_types/data/struct/attestation/aadl_micro_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/data/struct/attestation/micro_composite.txt rename to micro-examples/microkit/aadl_port_types/data/struct/attestation/aadl_micro_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/data/struct/attestation/aadl_model_args.json b/micro-examples/microkit/aadl_port_types/data/struct/attestation/aadl_model_args.json new file mode 100644 index 0000000..5aa4119 --- /dev/null +++ b/micro-examples/microkit/aadl_port_types/data/struct/attestation/aadl_model_args.json @@ -0,0 +1,3 @@ +{"dirpath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/struct/aadl/", + "suffix": ".aadl", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/struct/attestation/aadl_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/data/struct/attestation/system.golden b/micro-examples/microkit/aadl_port_types/data/struct/attestation/microkit_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/data/struct/attestation/system.golden rename to micro-examples/microkit/aadl_port_types/data/struct/attestation/microkit_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/data/struct/attestation/model_args.json b/micro-examples/microkit/aadl_port_types/data/struct/attestation/model_args.json deleted file mode 100644 index f621529..0000000 --- a/micro-examples/microkit/aadl_port_types/data/struct/attestation/model_args.json +++ /dev/null @@ -1,2 +0,0 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/struct/aadl/data_1_prod_2_cons.aadl", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/struct/attestation/model.golden"} diff --git a/micro-examples/microkit/aadl_port_types/data/struct/attestation/run-attestation.cmd b/micro-examples/microkit/aadl_port_types/data/struct/attestation/run-attestation.cmd new file mode 100755 index 0000000..b3ff5be --- /dev/null +++ b/micro-examples/microkit/aadl_port_types/data/struct/attestation/run-attestation.cmd @@ -0,0 +1,129 @@ +::/*#! 2> /dev/null # +@ 2>/dev/null # 2>nul & echo off & goto BOF # +if [ -z ${SIREUM_HOME} ]; then # + echo "Please set SIREUM_HOME env var" # + exit -1 # +fi # +exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" # +:BOF +setlocal +if not defined SIREUM_HOME ( + echo Please set SIREUM_HOME env var + exit /B -1 +) +%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* +exit /B %errorlevel% +::!#*/ +// #Sireum + +import org.sireum._ + +val home = Os.slashDir +val projectDir = home.up + +if (!(ops.ISZOps(Os.cliArgs).contains("aadl")) && + !(ops.ISZOps(Os.cliArgs).contains("sysml")) && + !(ops.ISZOps(Os.cliArgs).contains("provision"))) { + println(st"""Pass one of the following arguments: + | provision: Reruns provisioning + | aadl: Performs an appraisal on the AADL artifacts + | sysml: Performs an appraisal on the SysML artifacts""".render) + Os.exit(0) +} + +val repoRoot = { + def f(p: Os.Path): Option[Os.Path] = { + if ((p / ".git" / "config").exists) { + assert((p / "micro-examples").exists, s"Expected ${p / "micro-examples"} to exist") + return Some(p) + } + return f(p.up) + } + f(projectDir).get +} + +val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" +val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") + +val microkitFile = home.up / "hamr" / "microkit" / "microkit.system" +assert(microkitFile.exists, s"Didn't find MSD at $microkitFile") + +val aadlDir = projectDir / "aadl" +val sysmlDir = projectDir / "sysml" + +val model_args = "model_args.json" +val system_args = home / "system_args.json" + +def makeArgs(extension: String, modelDir: Os.Path): Unit = { + @strictpure def getDir(dir: Os.Path): String = s"/INSPECTA-models/${repoRoot.relativize(dir).value}" + (home / s"${extension}_$model_args").writeOver( + st"""{"dirpath": "${getDir(modelDir)}/", + | "suffix": ".$extension", + | "filepath-golden": "${getDir(home)}/${extension}_composite.txt"}""".render) + system_args.writeOver(st"""{"dirpath": "${getDir(microkitFile.up)}/", + | "suffix": ".system", + | "filepath-golden": "${getDir(home)}/microkit_composite.txt"}""".render) +} + +if (aadlDir.exists) { + makeArgs("aadl", aadlDir) +} + +if (sysmlDir.exists) { + makeArgs("sysml", sysmlDir) +} + + + +def run(title: String, proc: OsProto.Proc, verbose: B, checkExitCode: B): Z = { + println(s"$title ...") + val r = (if (verbose) proc.console.echo else proc).run() + if (checkExitCode &&r.exitCode != 0) { + println(s"$title failed!") + cprintln(F, r.out) + cprintln(T, r.err) + } + return if (r.exitCode == 0) 0 else 1 +} + +val DEMO_ROOT = repoRoot.up +assert (Os.env("DEMO_ROOT").nonEmpty && DEMO_ROOT.value == Os.env("DEMO_ROOT").get, "DEMO_ROOT environment variable not set") + +val testsDir = DEMO_ROOT / "am-cakeml" / "tests" + +val micro_composite = testsDir / "DemoFiles" / "goldenFiles" / "micro_composite.txt" + +var aargs = ISZ[String]((testsDir / "CI" / "Test.sh").value, "-t", "micro", "-h", + "-s", system_args.value) + +if (ops.ISZOps(Os.cliArgs).contains("provision")) { + def provision(extension: String): Unit = { + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + if (cached_micro_composite.exists) { + cached_micro_composite.remove() + } + val f = home / s"${extension}_$model_args" + run(s"Provisioning $f", Os.proc(aargs :+ "-m" :+ f.value :+ "-p"), F, F) + + assert(micro_composite.exists) + micro_composite.copyOverTo(cached_micro_composite) + } + if (aadlDir.exists) { + provision("aadl") + } + if (sysmlDir.exists) { + provision("sysml") + } + Os.exit(0) +} else { + val extension = + if (ops.ISZOps(Os.cliArgs).contains("aadl")) "aadl" + else if (ops.ISZOps(Os.cliArgs).contains("sysml")) "sysml" + else "aadl" + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + cached_micro_composite.copyOverTo(micro_composite) + val f = home / s"${extension}_$model_args" + val result = run(s"Appraising $f", Os.proc(aargs :+ "-m" :+ f.value), F, T) + println(s"Appraisal ${if (result == 0) "succeeded" else "failed"}!") + Os.exit(result) +} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/data/struct/attestation/system_args.json b/micro-examples/microkit/aadl_port_types/data/struct/attestation/system_args.json index 3bbc862..92866ab 100644 --- a/micro-examples/microkit/aadl_port_types/data/struct/attestation/system_args.json +++ b/micro-examples/microkit/aadl_port_types/data/struct/attestation/system_args.json @@ -1,2 +1,3 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/struct/hamr/microkit/microkit.system", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/struct/attestation/system.golden"} +{"dirpath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/struct/hamr/microkit/", + "suffix": ".system", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/struct/attestation/microkit_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/data/struct/readme.md b/micro-examples/microkit/aadl_port_types/data/struct/readme.md index 850c6cb..66c4f53 100644 --- a/micro-examples/microkit/aadl_port_types/data/struct/readme.md +++ b/micro-examples/microkit/aadl_port_types/data/struct/readme.md @@ -92,6 +92,13 @@ micro-examples/microkit/aadl_port_types/data/struct/aadl/bin/run-hamr.cmd ``` + Run the following to do an appraisal on the results (appraising will fail if any changes are made to the AADL files or the microkit.system file) + + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "\$HOME/provers/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/struct/attestation/run-attestation.cmd aadl" + ``` + 1. Build and simulate the seL4 Microkit image Run the following from this repository's root directory. The docker image ``jasonbelt/microkit_domain_scheduling`` contains customized versions of Microkit and seL4 that support domain scheduling. They were built off the following pull requests @@ -99,9 +106,9 @@ - [microkit #175](https://github.com/seL4/microkit/pull/175) - [seL4 #1308](https://github.com/seL4/seL4/pull/1308) - ``` - docker run -it --rm -v $(pwd):/home/microkit/inspecta-models jasonbelt/microkit_domain_scheduling \ - bash -ci "cd \$HOME/inspecta-models/micro-examples/microkit/aadl_port_types/data/struct/hamr/microkit \ + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "cd \$HOME/provers/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/struct/hamr/microkit \ && make qemu" ``` diff --git a/micro-examples/microkit/aadl_port_types/event/.ci/ci.cmd b/micro-examples/microkit/aadl_port_types/event/.ci/ci.cmd index 34d105c..c6060da 100755 --- a/micro-examples/microkit/aadl_port_types/event/.ci/ci.cmd +++ b/micro-examples/microkit/aadl_port_types/event/.ci/ci.cmd @@ -51,6 +51,13 @@ if (result == 0) { if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) { result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit")) + if ((homeDir / "hamr" / "microkit" / "build").exists) { + (homeDir / "hamr" / "microkit" / "build").removeAll() + } +} + +if (result == 0) { + result = run("Running AADL attestation", F, proc"$sireum slang run ${homeDir / "attestation" / "run-attestation.cmd"} aadl") } Os.exit(result) \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/event/attestation/model.golden b/micro-examples/microkit/aadl_port_types/event/attestation/aadl_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/event/attestation/model.golden rename to micro-examples/microkit/aadl_port_types/event/attestation/aadl_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/event/attestation/micro_composite.txt b/micro-examples/microkit/aadl_port_types/event/attestation/aadl_micro_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/event/attestation/micro_composite.txt rename to micro-examples/microkit/aadl_port_types/event/attestation/aadl_micro_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/event/attestation/aadl_model_args.json b/micro-examples/microkit/aadl_port_types/event/attestation/aadl_model_args.json new file mode 100644 index 0000000..ca82980 --- /dev/null +++ b/micro-examples/microkit/aadl_port_types/event/attestation/aadl_model_args.json @@ -0,0 +1,3 @@ +{"dirpath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event/aadl/", + "suffix": ".aadl", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event/attestation/aadl_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/event/attestation/system.golden b/micro-examples/microkit/aadl_port_types/event/attestation/microkit_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/event/attestation/system.golden rename to micro-examples/microkit/aadl_port_types/event/attestation/microkit_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/event/attestation/model_args.json b/micro-examples/microkit/aadl_port_types/event/attestation/model_args.json deleted file mode 100644 index 98bf80e..0000000 --- a/micro-examples/microkit/aadl_port_types/event/attestation/model_args.json +++ /dev/null @@ -1,2 +0,0 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event/aadl/event_2_prod_2_cons.aadl", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/event/attestation/model.golden"} diff --git a/micro-examples/microkit/aadl_port_types/event/attestation/run-attestation.cmd b/micro-examples/microkit/aadl_port_types/event/attestation/run-attestation.cmd new file mode 100755 index 0000000..b3ff5be --- /dev/null +++ b/micro-examples/microkit/aadl_port_types/event/attestation/run-attestation.cmd @@ -0,0 +1,129 @@ +::/*#! 2> /dev/null # +@ 2>/dev/null # 2>nul & echo off & goto BOF # +if [ -z ${SIREUM_HOME} ]; then # + echo "Please set SIREUM_HOME env var" # + exit -1 # +fi # +exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" # +:BOF +setlocal +if not defined SIREUM_HOME ( + echo Please set SIREUM_HOME env var + exit /B -1 +) +%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* +exit /B %errorlevel% +::!#*/ +// #Sireum + +import org.sireum._ + +val home = Os.slashDir +val projectDir = home.up + +if (!(ops.ISZOps(Os.cliArgs).contains("aadl")) && + !(ops.ISZOps(Os.cliArgs).contains("sysml")) && + !(ops.ISZOps(Os.cliArgs).contains("provision"))) { + println(st"""Pass one of the following arguments: + | provision: Reruns provisioning + | aadl: Performs an appraisal on the AADL artifacts + | sysml: Performs an appraisal on the SysML artifacts""".render) + Os.exit(0) +} + +val repoRoot = { + def f(p: Os.Path): Option[Os.Path] = { + if ((p / ".git" / "config").exists) { + assert((p / "micro-examples").exists, s"Expected ${p / "micro-examples"} to exist") + return Some(p) + } + return f(p.up) + } + f(projectDir).get +} + +val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" +val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") + +val microkitFile = home.up / "hamr" / "microkit" / "microkit.system" +assert(microkitFile.exists, s"Didn't find MSD at $microkitFile") + +val aadlDir = projectDir / "aadl" +val sysmlDir = projectDir / "sysml" + +val model_args = "model_args.json" +val system_args = home / "system_args.json" + +def makeArgs(extension: String, modelDir: Os.Path): Unit = { + @strictpure def getDir(dir: Os.Path): String = s"/INSPECTA-models/${repoRoot.relativize(dir).value}" + (home / s"${extension}_$model_args").writeOver( + st"""{"dirpath": "${getDir(modelDir)}/", + | "suffix": ".$extension", + | "filepath-golden": "${getDir(home)}/${extension}_composite.txt"}""".render) + system_args.writeOver(st"""{"dirpath": "${getDir(microkitFile.up)}/", + | "suffix": ".system", + | "filepath-golden": "${getDir(home)}/microkit_composite.txt"}""".render) +} + +if (aadlDir.exists) { + makeArgs("aadl", aadlDir) +} + +if (sysmlDir.exists) { + makeArgs("sysml", sysmlDir) +} + + + +def run(title: String, proc: OsProto.Proc, verbose: B, checkExitCode: B): Z = { + println(s"$title ...") + val r = (if (verbose) proc.console.echo else proc).run() + if (checkExitCode &&r.exitCode != 0) { + println(s"$title failed!") + cprintln(F, r.out) + cprintln(T, r.err) + } + return if (r.exitCode == 0) 0 else 1 +} + +val DEMO_ROOT = repoRoot.up +assert (Os.env("DEMO_ROOT").nonEmpty && DEMO_ROOT.value == Os.env("DEMO_ROOT").get, "DEMO_ROOT environment variable not set") + +val testsDir = DEMO_ROOT / "am-cakeml" / "tests" + +val micro_composite = testsDir / "DemoFiles" / "goldenFiles" / "micro_composite.txt" + +var aargs = ISZ[String]((testsDir / "CI" / "Test.sh").value, "-t", "micro", "-h", + "-s", system_args.value) + +if (ops.ISZOps(Os.cliArgs).contains("provision")) { + def provision(extension: String): Unit = { + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + if (cached_micro_composite.exists) { + cached_micro_composite.remove() + } + val f = home / s"${extension}_$model_args" + run(s"Provisioning $f", Os.proc(aargs :+ "-m" :+ f.value :+ "-p"), F, F) + + assert(micro_composite.exists) + micro_composite.copyOverTo(cached_micro_composite) + } + if (aadlDir.exists) { + provision("aadl") + } + if (sysmlDir.exists) { + provision("sysml") + } + Os.exit(0) +} else { + val extension = + if (ops.ISZOps(Os.cliArgs).contains("aadl")) "aadl" + else if (ops.ISZOps(Os.cliArgs).contains("sysml")) "sysml" + else "aadl" + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + cached_micro_composite.copyOverTo(micro_composite) + val f = home / s"${extension}_$model_args" + val result = run(s"Appraising $f", Os.proc(aargs :+ "-m" :+ f.value), F, T) + println(s"Appraisal ${if (result == 0) "succeeded" else "failed"}!") + Os.exit(result) +} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/event/attestation/system_args.json b/micro-examples/microkit/aadl_port_types/event/attestation/system_args.json index 3bc6b1a..a27c521 100644 --- a/micro-examples/microkit/aadl_port_types/event/attestation/system_args.json +++ b/micro-examples/microkit/aadl_port_types/event/attestation/system_args.json @@ -1,2 +1,3 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event/hamr/microkit/microkit.system", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/event/attestation/system.golden"} +{"dirpath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event/hamr/microkit/", + "suffix": ".system", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event/attestation/microkit_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/event/readme.md b/micro-examples/microkit/aadl_port_types/event/readme.md index abf2b7e..c8ffc63 100644 --- a/micro-examples/microkit/aadl_port_types/event/readme.md +++ b/micro-examples/microkit/aadl_port_types/event/readme.md @@ -91,6 +91,13 @@ micro-examples/microkit/aadl_port_types/event/aadl/bin/run-hamr.cmd ``` + Run the following to do an appraisal on the results (appraising will fail if any changes are made to the AADL files or the microkit.system file) + + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "\$HOME/provers/INSPECTA-models/micro-examples/microkit/aadl_port_types/event/attestation/run-attestation.cmd aadl" + ``` + 1. Build and simulate the seL4 Microkit image Run the following from this repository's root directory. The docker image ``jasonbelt/microkit_domain_scheduling`` contains customized versions of Microkit and seL4 that support domain scheduling. They were built off the following pull requests @@ -98,9 +105,9 @@ - [microkit #175](https://github.com/seL4/microkit/pull/175) - [seL4 #1308](https://github.com/seL4/seL4/pull/1308) - ``` - docker run -it --rm -v $(pwd):/home/microkit/inspecta-models jasonbelt/microkit_domain_scheduling \ - bash -ci "cd \$HOME/inspecta-models/micro-examples/microkit/aadl_port_types/event/hamr/microkit \ + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "cd \$HOME/provers/INSPECTA-models/micro-examples/microkit/aadl_port_types/event/hamr/microkit \ && make qemu" ``` diff --git a/micro-examples/microkit/aadl_port_types/event_data/array/.ci/ci.cmd b/micro-examples/microkit/aadl_port_types/event_data/array/.ci/ci.cmd index 78f521a..71fe0ca 100755 --- a/micro-examples/microkit/aadl_port_types/event_data/array/.ci/ci.cmd +++ b/micro-examples/microkit/aadl_port_types/event_data/array/.ci/ci.cmd @@ -51,6 +51,13 @@ if (result == 0) { if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) { result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit")) + if ((homeDir / "hamr" / "microkit" / "build").exists) { + (homeDir / "hamr" / "microkit" / "build").removeAll() + } +} + +if (result == 0) { + result = run("Running AADL attestation", F, proc"$sireum slang run ${homeDir / "attestation" / "run-attestation.cmd"} aadl") } Os.exit(result) \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/event_data/array/attestation/model.golden b/micro-examples/microkit/aadl_port_types/event_data/array/attestation/aadl_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/event_data/array/attestation/model.golden rename to micro-examples/microkit/aadl_port_types/event_data/array/attestation/aadl_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/event_data/array/attestation/micro_composite.txt b/micro-examples/microkit/aadl_port_types/event_data/array/attestation/aadl_micro_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/event_data/array/attestation/micro_composite.txt rename to micro-examples/microkit/aadl_port_types/event_data/array/attestation/aadl_micro_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/event_data/array/attestation/aadl_model_args.json b/micro-examples/microkit/aadl_port_types/event_data/array/attestation/aadl_model_args.json new file mode 100644 index 0000000..def75dc --- /dev/null +++ b/micro-examples/microkit/aadl_port_types/event_data/array/attestation/aadl_model_args.json @@ -0,0 +1,3 @@ +{"dirpath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/array/aadl/", + "suffix": ".aadl", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/array/attestation/aadl_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/event_data/array/attestation/system.golden b/micro-examples/microkit/aadl_port_types/event_data/array/attestation/microkit_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/event_data/array/attestation/system.golden rename to micro-examples/microkit/aadl_port_types/event_data/array/attestation/microkit_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/event_data/array/attestation/model_args.json b/micro-examples/microkit/aadl_port_types/event_data/array/attestation/model_args.json deleted file mode 100644 index caf4396..0000000 --- a/micro-examples/microkit/aadl_port_types/event_data/array/attestation/model_args.json +++ /dev/null @@ -1,2 +0,0 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/array/aadl/event_data_2_prod_2_cons.aadl", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/array/attestation/model.golden"} diff --git a/micro-examples/microkit/aadl_port_types/event_data/array/attestation/run-attestation.cmd b/micro-examples/microkit/aadl_port_types/event_data/array/attestation/run-attestation.cmd new file mode 100755 index 0000000..b3ff5be --- /dev/null +++ b/micro-examples/microkit/aadl_port_types/event_data/array/attestation/run-attestation.cmd @@ -0,0 +1,129 @@ +::/*#! 2> /dev/null # +@ 2>/dev/null # 2>nul & echo off & goto BOF # +if [ -z ${SIREUM_HOME} ]; then # + echo "Please set SIREUM_HOME env var" # + exit -1 # +fi # +exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" # +:BOF +setlocal +if not defined SIREUM_HOME ( + echo Please set SIREUM_HOME env var + exit /B -1 +) +%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* +exit /B %errorlevel% +::!#*/ +// #Sireum + +import org.sireum._ + +val home = Os.slashDir +val projectDir = home.up + +if (!(ops.ISZOps(Os.cliArgs).contains("aadl")) && + !(ops.ISZOps(Os.cliArgs).contains("sysml")) && + !(ops.ISZOps(Os.cliArgs).contains("provision"))) { + println(st"""Pass one of the following arguments: + | provision: Reruns provisioning + | aadl: Performs an appraisal on the AADL artifacts + | sysml: Performs an appraisal on the SysML artifacts""".render) + Os.exit(0) +} + +val repoRoot = { + def f(p: Os.Path): Option[Os.Path] = { + if ((p / ".git" / "config").exists) { + assert((p / "micro-examples").exists, s"Expected ${p / "micro-examples"} to exist") + return Some(p) + } + return f(p.up) + } + f(projectDir).get +} + +val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" +val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") + +val microkitFile = home.up / "hamr" / "microkit" / "microkit.system" +assert(microkitFile.exists, s"Didn't find MSD at $microkitFile") + +val aadlDir = projectDir / "aadl" +val sysmlDir = projectDir / "sysml" + +val model_args = "model_args.json" +val system_args = home / "system_args.json" + +def makeArgs(extension: String, modelDir: Os.Path): Unit = { + @strictpure def getDir(dir: Os.Path): String = s"/INSPECTA-models/${repoRoot.relativize(dir).value}" + (home / s"${extension}_$model_args").writeOver( + st"""{"dirpath": "${getDir(modelDir)}/", + | "suffix": ".$extension", + | "filepath-golden": "${getDir(home)}/${extension}_composite.txt"}""".render) + system_args.writeOver(st"""{"dirpath": "${getDir(microkitFile.up)}/", + | "suffix": ".system", + | "filepath-golden": "${getDir(home)}/microkit_composite.txt"}""".render) +} + +if (aadlDir.exists) { + makeArgs("aadl", aadlDir) +} + +if (sysmlDir.exists) { + makeArgs("sysml", sysmlDir) +} + + + +def run(title: String, proc: OsProto.Proc, verbose: B, checkExitCode: B): Z = { + println(s"$title ...") + val r = (if (verbose) proc.console.echo else proc).run() + if (checkExitCode &&r.exitCode != 0) { + println(s"$title failed!") + cprintln(F, r.out) + cprintln(T, r.err) + } + return if (r.exitCode == 0) 0 else 1 +} + +val DEMO_ROOT = repoRoot.up +assert (Os.env("DEMO_ROOT").nonEmpty && DEMO_ROOT.value == Os.env("DEMO_ROOT").get, "DEMO_ROOT environment variable not set") + +val testsDir = DEMO_ROOT / "am-cakeml" / "tests" + +val micro_composite = testsDir / "DemoFiles" / "goldenFiles" / "micro_composite.txt" + +var aargs = ISZ[String]((testsDir / "CI" / "Test.sh").value, "-t", "micro", "-h", + "-s", system_args.value) + +if (ops.ISZOps(Os.cliArgs).contains("provision")) { + def provision(extension: String): Unit = { + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + if (cached_micro_composite.exists) { + cached_micro_composite.remove() + } + val f = home / s"${extension}_$model_args" + run(s"Provisioning $f", Os.proc(aargs :+ "-m" :+ f.value :+ "-p"), F, F) + + assert(micro_composite.exists) + micro_composite.copyOverTo(cached_micro_composite) + } + if (aadlDir.exists) { + provision("aadl") + } + if (sysmlDir.exists) { + provision("sysml") + } + Os.exit(0) +} else { + val extension = + if (ops.ISZOps(Os.cliArgs).contains("aadl")) "aadl" + else if (ops.ISZOps(Os.cliArgs).contains("sysml")) "sysml" + else "aadl" + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + cached_micro_composite.copyOverTo(micro_composite) + val f = home / s"${extension}_$model_args" + val result = run(s"Appraising $f", Os.proc(aargs :+ "-m" :+ f.value), F, T) + println(s"Appraisal ${if (result == 0) "succeeded" else "failed"}!") + Os.exit(result) +} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/event_data/array/attestation/system_args.json b/micro-examples/microkit/aadl_port_types/event_data/array/attestation/system_args.json index 0ca1836..4bd05c4 100644 --- a/micro-examples/microkit/aadl_port_types/event_data/array/attestation/system_args.json +++ b/micro-examples/microkit/aadl_port_types/event_data/array/attestation/system_args.json @@ -1,2 +1,3 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/array/hamr/microkit/microkit.system", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/array/attestation/system.golden"} +{"dirpath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/array/hamr/microkit/", + "suffix": ".system", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/array/attestation/microkit_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/event_data/array/readme.md b/micro-examples/microkit/aadl_port_types/event_data/array/readme.md index cbb034e..9b67307 100644 --- a/micro-examples/microkit/aadl_port_types/event_data/array/readme.md +++ b/micro-examples/microkit/aadl_port_types/event_data/array/readme.md @@ -91,6 +91,13 @@ micro-examples/microkit/aadl_port_types/event_data/array/aadl/bin/run-hamr.cmd ``` + Run the following to do an appraisal on the results (appraising will fail if any changes are made to the AADL files or the microkit.system file) + + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "\$HOME/provers/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/array/attestation/run-attestation.cmd aadl" + ``` + 1. Build and simulate the seL4 Microkit image Run the following from this repository's root directory. The docker image ``jasonbelt/microkit_domain_scheduling`` contains customized versions of Microkit and seL4 that support domain scheduling. They were built off the following pull requests @@ -98,9 +105,9 @@ - [microkit #175](https://github.com/seL4/microkit/pull/175) - [seL4 #1308](https://github.com/seL4/seL4/pull/1308) - ``` - docker run -it --rm -v $(pwd):/home/microkit/inspecta-models jasonbelt/microkit_domain_scheduling \ - bash -ci "cd \$HOME/inspecta-models/micro-examples/microkit/aadl_port_types/event_data/array/hamr/microkit \ + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "cd \$HOME/provers/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/array/hamr/microkit \ && make qemu" ``` diff --git a/micro-examples/microkit/aadl_port_types/event_data/base_type/.ci/ci.cmd b/micro-examples/microkit/aadl_port_types/event_data/base_type/.ci/ci.cmd index ab15a9f..c5ba6ac 100755 --- a/micro-examples/microkit/aadl_port_types/event_data/base_type/.ci/ci.cmd +++ b/micro-examples/microkit/aadl_port_types/event_data/base_type/.ci/ci.cmd @@ -51,6 +51,13 @@ if (result == 0) { if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) { result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit")) + if ((homeDir / "hamr" / "microkit" / "build").exists) { + (homeDir / "hamr" / "microkit" / "build").removeAll() + } +} + +if (result == 0) { + result = run("Running AADL attestation", F, proc"$sireum slang run ${homeDir / "attestation" / "run-attestation.cmd"} aadl") } Os.exit(result) \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/model.golden b/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/aadl_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/model.golden rename to micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/aadl_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/micro_composite.txt b/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/aadl_micro_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/micro_composite.txt rename to micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/aadl_micro_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/aadl_model_args.json b/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/aadl_model_args.json new file mode 100644 index 0000000..a0b6de0 --- /dev/null +++ b/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/aadl_model_args.json @@ -0,0 +1,3 @@ +{"dirpath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/base_type/aadl/", + "suffix": ".aadl", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/aadl_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/system.golden b/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/microkit_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/system.golden rename to micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/microkit_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/model_args.json b/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/model_args.json deleted file mode 100644 index 6c4e9d5..0000000 --- a/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/model_args.json +++ /dev/null @@ -1,2 +0,0 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/base_type/aadl/event_data_2_prod_2_cons.aadl", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/model.golden"} diff --git a/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/run-attestation.cmd b/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/run-attestation.cmd new file mode 100755 index 0000000..b3ff5be --- /dev/null +++ b/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/run-attestation.cmd @@ -0,0 +1,129 @@ +::/*#! 2> /dev/null # +@ 2>/dev/null # 2>nul & echo off & goto BOF # +if [ -z ${SIREUM_HOME} ]; then # + echo "Please set SIREUM_HOME env var" # + exit -1 # +fi # +exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" # +:BOF +setlocal +if not defined SIREUM_HOME ( + echo Please set SIREUM_HOME env var + exit /B -1 +) +%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* +exit /B %errorlevel% +::!#*/ +// #Sireum + +import org.sireum._ + +val home = Os.slashDir +val projectDir = home.up + +if (!(ops.ISZOps(Os.cliArgs).contains("aadl")) && + !(ops.ISZOps(Os.cliArgs).contains("sysml")) && + !(ops.ISZOps(Os.cliArgs).contains("provision"))) { + println(st"""Pass one of the following arguments: + | provision: Reruns provisioning + | aadl: Performs an appraisal on the AADL artifacts + | sysml: Performs an appraisal on the SysML artifacts""".render) + Os.exit(0) +} + +val repoRoot = { + def f(p: Os.Path): Option[Os.Path] = { + if ((p / ".git" / "config").exists) { + assert((p / "micro-examples").exists, s"Expected ${p / "micro-examples"} to exist") + return Some(p) + } + return f(p.up) + } + f(projectDir).get +} + +val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" +val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") + +val microkitFile = home.up / "hamr" / "microkit" / "microkit.system" +assert(microkitFile.exists, s"Didn't find MSD at $microkitFile") + +val aadlDir = projectDir / "aadl" +val sysmlDir = projectDir / "sysml" + +val model_args = "model_args.json" +val system_args = home / "system_args.json" + +def makeArgs(extension: String, modelDir: Os.Path): Unit = { + @strictpure def getDir(dir: Os.Path): String = s"/INSPECTA-models/${repoRoot.relativize(dir).value}" + (home / s"${extension}_$model_args").writeOver( + st"""{"dirpath": "${getDir(modelDir)}/", + | "suffix": ".$extension", + | "filepath-golden": "${getDir(home)}/${extension}_composite.txt"}""".render) + system_args.writeOver(st"""{"dirpath": "${getDir(microkitFile.up)}/", + | "suffix": ".system", + | "filepath-golden": "${getDir(home)}/microkit_composite.txt"}""".render) +} + +if (aadlDir.exists) { + makeArgs("aadl", aadlDir) +} + +if (sysmlDir.exists) { + makeArgs("sysml", sysmlDir) +} + + + +def run(title: String, proc: OsProto.Proc, verbose: B, checkExitCode: B): Z = { + println(s"$title ...") + val r = (if (verbose) proc.console.echo else proc).run() + if (checkExitCode &&r.exitCode != 0) { + println(s"$title failed!") + cprintln(F, r.out) + cprintln(T, r.err) + } + return if (r.exitCode == 0) 0 else 1 +} + +val DEMO_ROOT = repoRoot.up +assert (Os.env("DEMO_ROOT").nonEmpty && DEMO_ROOT.value == Os.env("DEMO_ROOT").get, "DEMO_ROOT environment variable not set") + +val testsDir = DEMO_ROOT / "am-cakeml" / "tests" + +val micro_composite = testsDir / "DemoFiles" / "goldenFiles" / "micro_composite.txt" + +var aargs = ISZ[String]((testsDir / "CI" / "Test.sh").value, "-t", "micro", "-h", + "-s", system_args.value) + +if (ops.ISZOps(Os.cliArgs).contains("provision")) { + def provision(extension: String): Unit = { + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + if (cached_micro_composite.exists) { + cached_micro_composite.remove() + } + val f = home / s"${extension}_$model_args" + run(s"Provisioning $f", Os.proc(aargs :+ "-m" :+ f.value :+ "-p"), F, F) + + assert(micro_composite.exists) + micro_composite.copyOverTo(cached_micro_composite) + } + if (aadlDir.exists) { + provision("aadl") + } + if (sysmlDir.exists) { + provision("sysml") + } + Os.exit(0) +} else { + val extension = + if (ops.ISZOps(Os.cliArgs).contains("aadl")) "aadl" + else if (ops.ISZOps(Os.cliArgs).contains("sysml")) "sysml" + else "aadl" + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + cached_micro_composite.copyOverTo(micro_composite) + val f = home / s"${extension}_$model_args" + val result = run(s"Appraising $f", Os.proc(aargs :+ "-m" :+ f.value), F, T) + println(s"Appraisal ${if (result == 0) "succeeded" else "failed"}!") + Os.exit(result) +} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/system_args.json b/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/system_args.json index 8f1b296..9f896f1 100644 --- a/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/system_args.json +++ b/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/system_args.json @@ -1,2 +1,3 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/base_type/hamr/microkit/microkit.system", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/system.golden"} +{"dirpath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/base_type/hamr/microkit/", + "suffix": ".system", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/microkit_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/event_data/base_type/readme.md b/micro-examples/microkit/aadl_port_types/event_data/base_type/readme.md index d4a8c5d..33ad180 100644 --- a/micro-examples/microkit/aadl_port_types/event_data/base_type/readme.md +++ b/micro-examples/microkit/aadl_port_types/event_data/base_type/readme.md @@ -91,6 +91,13 @@ micro-examples/microkit/aadl_port_types/event_data/base_type/aadl/bin/run-hamr.cmd ``` + Run the following to do an appraisal on the results (appraising will fail if any changes are made to the AADL files or the microkit.system file) + + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "\$HOME/provers/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/base_type/attestation/run-attestation.cmd aadl" + ``` + 1. Build and simulate the seL4 Microkit image Run the following from this repository's root directory. The docker image ``jasonbelt/microkit_domain_scheduling`` contains customized versions of Microkit and seL4 that support domain scheduling. They were built off the following pull requests @@ -98,9 +105,9 @@ - [microkit #175](https://github.com/seL4/microkit/pull/175) - [seL4 #1308](https://github.com/seL4/seL4/pull/1308) - ``` - docker run -it --rm -v $(pwd):/home/microkit/inspecta-models jasonbelt/microkit_domain_scheduling \ - bash -ci "cd \$HOME/inspecta-models/micro-examples/microkit/aadl_port_types/event_data/base_type/hamr/microkit \ + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "cd \$HOME/provers/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/base_type/hamr/microkit \ && make qemu" ``` diff --git a/micro-examples/microkit/aadl_port_types/event_data/struct/.ci/ci.cmd b/micro-examples/microkit/aadl_port_types/event_data/struct/.ci/ci.cmd index 2a72730..2462005 100755 --- a/micro-examples/microkit/aadl_port_types/event_data/struct/.ci/ci.cmd +++ b/micro-examples/microkit/aadl_port_types/event_data/struct/.ci/ci.cmd @@ -51,6 +51,13 @@ if (result == 0) { if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) { result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit")) + if ((homeDir / "hamr" / "microkit" / "build").exists) { + (homeDir / "hamr" / "microkit" / "build").removeAll() + } +} + +if (result == 0) { + result = run("Running AADL attestation", F, proc"$sireum slang run ${homeDir / "attestation" / "run-attestation.cmd"} aadl") } Os.exit(result) \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/model.golden b/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/aadl_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/event_data/struct/attestation/model.golden rename to micro-examples/microkit/aadl_port_types/event_data/struct/attestation/aadl_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/micro_composite.txt b/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/aadl_micro_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/event_data/struct/attestation/micro_composite.txt rename to micro-examples/microkit/aadl_port_types/event_data/struct/attestation/aadl_micro_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/aadl_model_args.json b/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/aadl_model_args.json new file mode 100644 index 0000000..7116b13 --- /dev/null +++ b/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/aadl_model_args.json @@ -0,0 +1,3 @@ +{"dirpath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/struct/aadl/", + "suffix": ".aadl", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/aadl_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/system.golden b/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/microkit_composite.txt similarity index 100% rename from micro-examples/microkit/aadl_port_types/event_data/struct/attestation/system.golden rename to micro-examples/microkit/aadl_port_types/event_data/struct/attestation/microkit_composite.txt diff --git a/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/model_args.json b/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/model_args.json deleted file mode 100644 index a7e0c4b..0000000 --- a/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/model_args.json +++ /dev/null @@ -1,2 +0,0 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/struct/aadl/event_data_2_prod_2_cons.aadl", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/model.golden"} diff --git a/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/run-attestation.cmd b/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/run-attestation.cmd new file mode 100755 index 0000000..b3ff5be --- /dev/null +++ b/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/run-attestation.cmd @@ -0,0 +1,129 @@ +::/*#! 2> /dev/null # +@ 2>/dev/null # 2>nul & echo off & goto BOF # +if [ -z ${SIREUM_HOME} ]; then # + echo "Please set SIREUM_HOME env var" # + exit -1 # +fi # +exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" # +:BOF +setlocal +if not defined SIREUM_HOME ( + echo Please set SIREUM_HOME env var + exit /B -1 +) +%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* +exit /B %errorlevel% +::!#*/ +// #Sireum + +import org.sireum._ + +val home = Os.slashDir +val projectDir = home.up + +if (!(ops.ISZOps(Os.cliArgs).contains("aadl")) && + !(ops.ISZOps(Os.cliArgs).contains("sysml")) && + !(ops.ISZOps(Os.cliArgs).contains("provision"))) { + println(st"""Pass one of the following arguments: + | provision: Reruns provisioning + | aadl: Performs an appraisal on the AADL artifacts + | sysml: Performs an appraisal on the SysML artifacts""".render) + Os.exit(0) +} + +val repoRoot = { + def f(p: Os.Path): Option[Os.Path] = { + if ((p / ".git" / "config").exists) { + assert((p / "micro-examples").exists, s"Expected ${p / "micro-examples"} to exist") + return Some(p) + } + return f(p.up) + } + f(projectDir).get +} + +val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" +val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") + +val microkitFile = home.up / "hamr" / "microkit" / "microkit.system" +assert(microkitFile.exists, s"Didn't find MSD at $microkitFile") + +val aadlDir = projectDir / "aadl" +val sysmlDir = projectDir / "sysml" + +val model_args = "model_args.json" +val system_args = home / "system_args.json" + +def makeArgs(extension: String, modelDir: Os.Path): Unit = { + @strictpure def getDir(dir: Os.Path): String = s"/INSPECTA-models/${repoRoot.relativize(dir).value}" + (home / s"${extension}_$model_args").writeOver( + st"""{"dirpath": "${getDir(modelDir)}/", + | "suffix": ".$extension", + | "filepath-golden": "${getDir(home)}/${extension}_composite.txt"}""".render) + system_args.writeOver(st"""{"dirpath": "${getDir(microkitFile.up)}/", + | "suffix": ".system", + | "filepath-golden": "${getDir(home)}/microkit_composite.txt"}""".render) +} + +if (aadlDir.exists) { + makeArgs("aadl", aadlDir) +} + +if (sysmlDir.exists) { + makeArgs("sysml", sysmlDir) +} + + + +def run(title: String, proc: OsProto.Proc, verbose: B, checkExitCode: B): Z = { + println(s"$title ...") + val r = (if (verbose) proc.console.echo else proc).run() + if (checkExitCode &&r.exitCode != 0) { + println(s"$title failed!") + cprintln(F, r.out) + cprintln(T, r.err) + } + return if (r.exitCode == 0) 0 else 1 +} + +val DEMO_ROOT = repoRoot.up +assert (Os.env("DEMO_ROOT").nonEmpty && DEMO_ROOT.value == Os.env("DEMO_ROOT").get, "DEMO_ROOT environment variable not set") + +val testsDir = DEMO_ROOT / "am-cakeml" / "tests" + +val micro_composite = testsDir / "DemoFiles" / "goldenFiles" / "micro_composite.txt" + +var aargs = ISZ[String]((testsDir / "CI" / "Test.sh").value, "-t", "micro", "-h", + "-s", system_args.value) + +if (ops.ISZOps(Os.cliArgs).contains("provision")) { + def provision(extension: String): Unit = { + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + if (cached_micro_composite.exists) { + cached_micro_composite.remove() + } + val f = home / s"${extension}_$model_args" + run(s"Provisioning $f", Os.proc(aargs :+ "-m" :+ f.value :+ "-p"), F, F) + + assert(micro_composite.exists) + micro_composite.copyOverTo(cached_micro_composite) + } + if (aadlDir.exists) { + provision("aadl") + } + if (sysmlDir.exists) { + provision("sysml") + } + Os.exit(0) +} else { + val extension = + if (ops.ISZOps(Os.cliArgs).contains("aadl")) "aadl" + else if (ops.ISZOps(Os.cliArgs).contains("sysml")) "sysml" + else "aadl" + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + cached_micro_composite.copyOverTo(micro_composite) + val f = home / s"${extension}_$model_args" + val result = run(s"Appraising $f", Os.proc(aargs :+ "-m" :+ f.value), F, T) + println(s"Appraisal ${if (result == 0) "succeeded" else "failed"}!") + Os.exit(result) +} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/system_args.json b/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/system_args.json index d737a5c..632284f 100644 --- a/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/system_args.json +++ b/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/system_args.json @@ -1,2 +1,3 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/struct/hamr/microkit/microkit.system", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/system.golden"} +{"dirpath": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/struct/hamr/microkit/", + "suffix": ".system", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/microkit_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/aadl_port_types/event_data/struct/readme.md b/micro-examples/microkit/aadl_port_types/event_data/struct/readme.md index 682107f..a50fe31 100644 --- a/micro-examples/microkit/aadl_port_types/event_data/struct/readme.md +++ b/micro-examples/microkit/aadl_port_types/event_data/struct/readme.md @@ -92,6 +92,12 @@ micro-examples/microkit/aadl_port_types/event_data/struct/aadl/bin/run-hamr.cmd ``` + Run the following to do an appraisal on the results (appraising will fail if any changes are made to the AADL files or the microkit.system file) + + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "\$HOME/provers/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/struct/attestation/run-attestation.cmd aadl" + ``` 1. Build and simulate the seL4 Microkit image Run the following from this repository's root directory. The docker image ``jasonbelt/microkit_domain_scheduling`` contains customized versions of Microkit and seL4 that support domain scheduling. They were built off the following pull requests @@ -99,9 +105,9 @@ - [microkit #175](https://github.com/seL4/microkit/pull/175) - [seL4 #1308](https://github.com/seL4/seL4/pull/1308) - ``` - docker run -it --rm -v $(pwd):/home/microkit/inspecta-models jasonbelt/microkit_domain_scheduling \ - bash -ci "cd \$HOME/inspecta-models/micro-examples/microkit/aadl_port_types/event_data/struct/hamr/microkit \ + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "cd \$HOME/provers/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/struct/hamr/microkit \ && make qemu" ``` diff --git a/micro-examples/microkit/port_queues/event_data_array/.ci/ci.cmd b/micro-examples/microkit/port_queues/event_data_array/.ci/ci.cmd index 48f030d..f84e465 100755 --- a/micro-examples/microkit/port_queues/event_data_array/.ci/ci.cmd +++ b/micro-examples/microkit/port_queues/event_data_array/.ci/ci.cmd @@ -51,6 +51,13 @@ if (result == 0) { if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) { result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit")) + if ((homeDir / "hamr" / "microkit" / "build").exists) { + (homeDir / "hamr" / "microkit" / "build").removeAll() + } +} + +if (result == 0) { + result = run("Running AADL attestation", F, proc"$sireum slang run ${homeDir / "attestation" / "run-attestation.cmd"} aadl") } Os.exit(result) \ No newline at end of file diff --git a/micro-examples/microkit/port_queues/event_data_array/attestation/model.golden b/micro-examples/microkit/port_queues/event_data_array/attestation/aadl_composite.txt similarity index 100% rename from micro-examples/microkit/port_queues/event_data_array/attestation/model.golden rename to micro-examples/microkit/port_queues/event_data_array/attestation/aadl_composite.txt diff --git a/micro-examples/microkit/port_queues/event_data_array/attestation/micro_composite.txt b/micro-examples/microkit/port_queues/event_data_array/attestation/aadl_micro_composite.txt similarity index 100% rename from micro-examples/microkit/port_queues/event_data_array/attestation/micro_composite.txt rename to micro-examples/microkit/port_queues/event_data_array/attestation/aadl_micro_composite.txt diff --git a/micro-examples/microkit/port_queues/event_data_array/attestation/aadl_model_args.json b/micro-examples/microkit/port_queues/event_data_array/attestation/aadl_model_args.json new file mode 100644 index 0000000..40e7598 --- /dev/null +++ b/micro-examples/microkit/port_queues/event_data_array/attestation/aadl_model_args.json @@ -0,0 +1,3 @@ +{"dirpath": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_array/aadl/", + "suffix": ".aadl", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_array/attestation/aadl_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/port_queues/event_data_array/attestation/system.golden b/micro-examples/microkit/port_queues/event_data_array/attestation/microkit_composite.txt similarity index 100% rename from micro-examples/microkit/port_queues/event_data_array/attestation/system.golden rename to micro-examples/microkit/port_queues/event_data_array/attestation/microkit_composite.txt diff --git a/micro-examples/microkit/port_queues/event_data_array/attestation/model_args.json b/micro-examples/microkit/port_queues/event_data_array/attestation/model_args.json deleted file mode 100644 index a7e19a0..0000000 --- a/micro-examples/microkit/port_queues/event_data_array/attestation/model_args.json +++ /dev/null @@ -1,2 +0,0 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_array/aadl/event_data_port_queues.aadl", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/port_queues/event_data_array/attestation/model.golden"} diff --git a/micro-examples/microkit/port_queues/event_data_array/attestation/run-attestation.cmd b/micro-examples/microkit/port_queues/event_data_array/attestation/run-attestation.cmd new file mode 100755 index 0000000..b3ff5be --- /dev/null +++ b/micro-examples/microkit/port_queues/event_data_array/attestation/run-attestation.cmd @@ -0,0 +1,129 @@ +::/*#! 2> /dev/null # +@ 2>/dev/null # 2>nul & echo off & goto BOF # +if [ -z ${SIREUM_HOME} ]; then # + echo "Please set SIREUM_HOME env var" # + exit -1 # +fi # +exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" # +:BOF +setlocal +if not defined SIREUM_HOME ( + echo Please set SIREUM_HOME env var + exit /B -1 +) +%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* +exit /B %errorlevel% +::!#*/ +// #Sireum + +import org.sireum._ + +val home = Os.slashDir +val projectDir = home.up + +if (!(ops.ISZOps(Os.cliArgs).contains("aadl")) && + !(ops.ISZOps(Os.cliArgs).contains("sysml")) && + !(ops.ISZOps(Os.cliArgs).contains("provision"))) { + println(st"""Pass one of the following arguments: + | provision: Reruns provisioning + | aadl: Performs an appraisal on the AADL artifacts + | sysml: Performs an appraisal on the SysML artifacts""".render) + Os.exit(0) +} + +val repoRoot = { + def f(p: Os.Path): Option[Os.Path] = { + if ((p / ".git" / "config").exists) { + assert((p / "micro-examples").exists, s"Expected ${p / "micro-examples"} to exist") + return Some(p) + } + return f(p.up) + } + f(projectDir).get +} + +val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" +val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") + +val microkitFile = home.up / "hamr" / "microkit" / "microkit.system" +assert(microkitFile.exists, s"Didn't find MSD at $microkitFile") + +val aadlDir = projectDir / "aadl" +val sysmlDir = projectDir / "sysml" + +val model_args = "model_args.json" +val system_args = home / "system_args.json" + +def makeArgs(extension: String, modelDir: Os.Path): Unit = { + @strictpure def getDir(dir: Os.Path): String = s"/INSPECTA-models/${repoRoot.relativize(dir).value}" + (home / s"${extension}_$model_args").writeOver( + st"""{"dirpath": "${getDir(modelDir)}/", + | "suffix": ".$extension", + | "filepath-golden": "${getDir(home)}/${extension}_composite.txt"}""".render) + system_args.writeOver(st"""{"dirpath": "${getDir(microkitFile.up)}/", + | "suffix": ".system", + | "filepath-golden": "${getDir(home)}/microkit_composite.txt"}""".render) +} + +if (aadlDir.exists) { + makeArgs("aadl", aadlDir) +} + +if (sysmlDir.exists) { + makeArgs("sysml", sysmlDir) +} + + + +def run(title: String, proc: OsProto.Proc, verbose: B, checkExitCode: B): Z = { + println(s"$title ...") + val r = (if (verbose) proc.console.echo else proc).run() + if (checkExitCode &&r.exitCode != 0) { + println(s"$title failed!") + cprintln(F, r.out) + cprintln(T, r.err) + } + return if (r.exitCode == 0) 0 else 1 +} + +val DEMO_ROOT = repoRoot.up +assert (Os.env("DEMO_ROOT").nonEmpty && DEMO_ROOT.value == Os.env("DEMO_ROOT").get, "DEMO_ROOT environment variable not set") + +val testsDir = DEMO_ROOT / "am-cakeml" / "tests" + +val micro_composite = testsDir / "DemoFiles" / "goldenFiles" / "micro_composite.txt" + +var aargs = ISZ[String]((testsDir / "CI" / "Test.sh").value, "-t", "micro", "-h", + "-s", system_args.value) + +if (ops.ISZOps(Os.cliArgs).contains("provision")) { + def provision(extension: String): Unit = { + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + if (cached_micro_composite.exists) { + cached_micro_composite.remove() + } + val f = home / s"${extension}_$model_args" + run(s"Provisioning $f", Os.proc(aargs :+ "-m" :+ f.value :+ "-p"), F, F) + + assert(micro_composite.exists) + micro_composite.copyOverTo(cached_micro_composite) + } + if (aadlDir.exists) { + provision("aadl") + } + if (sysmlDir.exists) { + provision("sysml") + } + Os.exit(0) +} else { + val extension = + if (ops.ISZOps(Os.cliArgs).contains("aadl")) "aadl" + else if (ops.ISZOps(Os.cliArgs).contains("sysml")) "sysml" + else "aadl" + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + cached_micro_composite.copyOverTo(micro_composite) + val f = home / s"${extension}_$model_args" + val result = run(s"Appraising $f", Os.proc(aargs :+ "-m" :+ f.value), F, T) + println(s"Appraisal ${if (result == 0) "succeeded" else "failed"}!") + Os.exit(result) +} \ No newline at end of file diff --git a/micro-examples/microkit/port_queues/event_data_array/attestation/system_args.json b/micro-examples/microkit/port_queues/event_data_array/attestation/system_args.json index ec06d7c..54c9233 100644 --- a/micro-examples/microkit/port_queues/event_data_array/attestation/system_args.json +++ b/micro-examples/microkit/port_queues/event_data_array/attestation/system_args.json @@ -1,2 +1,3 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_array/hamr/microkit/microkit.system", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/port_queues/event_data_array/attestation/system.golden"} +{"dirpath": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_array/hamr/microkit/", + "suffix": ".system", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_array/attestation/microkit_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/port_queues/event_data_array/readme.md b/micro-examples/microkit/port_queues/event_data_array/readme.md index 5956b7c..c0aafd0 100644 --- a/micro-examples/microkit/port_queues/event_data_array/readme.md +++ b/micro-examples/microkit/port_queues/event_data_array/readme.md @@ -91,6 +91,13 @@ micro-examples/microkit/port_queues/event_data_array/aadl/bin/run-hamr.cmd ``` + Run the following to do an appraisal on the results (appraising will fail if any changes are made to the AADL files or the microkit.system file) + + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "\$HOME/provers/INSPECTA-models/micro-examples/microkit/port_queues/event_data_array/attestation/run-attestation.cmd aadl" + ``` + 1. Build and simulate the seL4 Microkit image Run the following from this repository's root directory. The docker image ``jasonbelt/microkit_domain_scheduling`` contains customized versions of Microkit and seL4 that support domain scheduling. They were built off the following pull requests @@ -98,9 +105,9 @@ - [microkit #175](https://github.com/seL4/microkit/pull/175) - [seL4 #1308](https://github.com/seL4/seL4/pull/1308) - ``` - docker run -it --rm -v $(pwd):/home/microkit/inspecta-models jasonbelt/microkit_domain_scheduling \ - bash -ci "cd \$HOME/inspecta-models/micro-examples/microkit/port_queues/event_data_array/hamr/microkit \ + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "cd \$HOME/provers/INSPECTA-models/micro-examples/microkit/port_queues/event_data_array/hamr/microkit \ && make qemu" ``` diff --git a/micro-examples/microkit/port_queues/event_data_base_types/.ci/ci.cmd b/micro-examples/microkit/port_queues/event_data_base_types/.ci/ci.cmd index e68f00e..2e4455a 100755 --- a/micro-examples/microkit/port_queues/event_data_base_types/.ci/ci.cmd +++ b/micro-examples/microkit/port_queues/event_data_base_types/.ci/ci.cmd @@ -51,6 +51,13 @@ if (result == 0) { if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) { result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit")) + if ((homeDir / "hamr" / "microkit" / "build").exists) { + (homeDir / "hamr" / "microkit" / "build").removeAll() + } +} + +if (result == 0) { + result = run("Running AADL attestation", F, proc"$sireum slang run ${homeDir / "attestation" / "run-attestation.cmd"} aadl") } Os.exit(result) \ No newline at end of file diff --git a/micro-examples/microkit/port_queues/event_data_base_types/attestation/model.golden b/micro-examples/microkit/port_queues/event_data_base_types/attestation/aadl_composite.txt similarity index 100% rename from micro-examples/microkit/port_queues/event_data_base_types/attestation/model.golden rename to micro-examples/microkit/port_queues/event_data_base_types/attestation/aadl_composite.txt diff --git a/micro-examples/microkit/port_queues/event_data_base_types/attestation/micro_composite.txt b/micro-examples/microkit/port_queues/event_data_base_types/attestation/aadl_micro_composite.txt similarity index 100% rename from micro-examples/microkit/port_queues/event_data_base_types/attestation/micro_composite.txt rename to micro-examples/microkit/port_queues/event_data_base_types/attestation/aadl_micro_composite.txt diff --git a/micro-examples/microkit/port_queues/event_data_base_types/attestation/aadl_model_args.json b/micro-examples/microkit/port_queues/event_data_base_types/attestation/aadl_model_args.json new file mode 100644 index 0000000..ee390d1 --- /dev/null +++ b/micro-examples/microkit/port_queues/event_data_base_types/attestation/aadl_model_args.json @@ -0,0 +1,3 @@ +{"dirpath": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_base_types/aadl/", + "suffix": ".aadl", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_base_types/attestation/aadl_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/port_queues/event_data_base_types/attestation/system.golden b/micro-examples/microkit/port_queues/event_data_base_types/attestation/microkit_composite.txt similarity index 100% rename from micro-examples/microkit/port_queues/event_data_base_types/attestation/system.golden rename to micro-examples/microkit/port_queues/event_data_base_types/attestation/microkit_composite.txt diff --git a/micro-examples/microkit/port_queues/event_data_base_types/attestation/model_args.json b/micro-examples/microkit/port_queues/event_data_base_types/attestation/model_args.json deleted file mode 100644 index af1b5b0..0000000 --- a/micro-examples/microkit/port_queues/event_data_base_types/attestation/model_args.json +++ /dev/null @@ -1,2 +0,0 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_base_types/aadl/event_data_port_queues.aadl", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/port_queues/event_data_base_types/attestation/model.golden"} diff --git a/micro-examples/microkit/port_queues/event_data_base_types/attestation/run-attestation.cmd b/micro-examples/microkit/port_queues/event_data_base_types/attestation/run-attestation.cmd new file mode 100755 index 0000000..b3ff5be --- /dev/null +++ b/micro-examples/microkit/port_queues/event_data_base_types/attestation/run-attestation.cmd @@ -0,0 +1,129 @@ +::/*#! 2> /dev/null # +@ 2>/dev/null # 2>nul & echo off & goto BOF # +if [ -z ${SIREUM_HOME} ]; then # + echo "Please set SIREUM_HOME env var" # + exit -1 # +fi # +exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" # +:BOF +setlocal +if not defined SIREUM_HOME ( + echo Please set SIREUM_HOME env var + exit /B -1 +) +%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* +exit /B %errorlevel% +::!#*/ +// #Sireum + +import org.sireum._ + +val home = Os.slashDir +val projectDir = home.up + +if (!(ops.ISZOps(Os.cliArgs).contains("aadl")) && + !(ops.ISZOps(Os.cliArgs).contains("sysml")) && + !(ops.ISZOps(Os.cliArgs).contains("provision"))) { + println(st"""Pass one of the following arguments: + | provision: Reruns provisioning + | aadl: Performs an appraisal on the AADL artifacts + | sysml: Performs an appraisal on the SysML artifacts""".render) + Os.exit(0) +} + +val repoRoot = { + def f(p: Os.Path): Option[Os.Path] = { + if ((p / ".git" / "config").exists) { + assert((p / "micro-examples").exists, s"Expected ${p / "micro-examples"} to exist") + return Some(p) + } + return f(p.up) + } + f(projectDir).get +} + +val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" +val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") + +val microkitFile = home.up / "hamr" / "microkit" / "microkit.system" +assert(microkitFile.exists, s"Didn't find MSD at $microkitFile") + +val aadlDir = projectDir / "aadl" +val sysmlDir = projectDir / "sysml" + +val model_args = "model_args.json" +val system_args = home / "system_args.json" + +def makeArgs(extension: String, modelDir: Os.Path): Unit = { + @strictpure def getDir(dir: Os.Path): String = s"/INSPECTA-models/${repoRoot.relativize(dir).value}" + (home / s"${extension}_$model_args").writeOver( + st"""{"dirpath": "${getDir(modelDir)}/", + | "suffix": ".$extension", + | "filepath-golden": "${getDir(home)}/${extension}_composite.txt"}""".render) + system_args.writeOver(st"""{"dirpath": "${getDir(microkitFile.up)}/", + | "suffix": ".system", + | "filepath-golden": "${getDir(home)}/microkit_composite.txt"}""".render) +} + +if (aadlDir.exists) { + makeArgs("aadl", aadlDir) +} + +if (sysmlDir.exists) { + makeArgs("sysml", sysmlDir) +} + + + +def run(title: String, proc: OsProto.Proc, verbose: B, checkExitCode: B): Z = { + println(s"$title ...") + val r = (if (verbose) proc.console.echo else proc).run() + if (checkExitCode &&r.exitCode != 0) { + println(s"$title failed!") + cprintln(F, r.out) + cprintln(T, r.err) + } + return if (r.exitCode == 0) 0 else 1 +} + +val DEMO_ROOT = repoRoot.up +assert (Os.env("DEMO_ROOT").nonEmpty && DEMO_ROOT.value == Os.env("DEMO_ROOT").get, "DEMO_ROOT environment variable not set") + +val testsDir = DEMO_ROOT / "am-cakeml" / "tests" + +val micro_composite = testsDir / "DemoFiles" / "goldenFiles" / "micro_composite.txt" + +var aargs = ISZ[String]((testsDir / "CI" / "Test.sh").value, "-t", "micro", "-h", + "-s", system_args.value) + +if (ops.ISZOps(Os.cliArgs).contains("provision")) { + def provision(extension: String): Unit = { + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + if (cached_micro_composite.exists) { + cached_micro_composite.remove() + } + val f = home / s"${extension}_$model_args" + run(s"Provisioning $f", Os.proc(aargs :+ "-m" :+ f.value :+ "-p"), F, F) + + assert(micro_composite.exists) + micro_composite.copyOverTo(cached_micro_composite) + } + if (aadlDir.exists) { + provision("aadl") + } + if (sysmlDir.exists) { + provision("sysml") + } + Os.exit(0) +} else { + val extension = + if (ops.ISZOps(Os.cliArgs).contains("aadl")) "aadl" + else if (ops.ISZOps(Os.cliArgs).contains("sysml")) "sysml" + else "aadl" + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + cached_micro_composite.copyOverTo(micro_composite) + val f = home / s"${extension}_$model_args" + val result = run(s"Appraising $f", Os.proc(aargs :+ "-m" :+ f.value), F, T) + println(s"Appraisal ${if (result == 0) "succeeded" else "failed"}!") + Os.exit(result) +} \ No newline at end of file diff --git a/micro-examples/microkit/port_queues/event_data_base_types/attestation/system_args.json b/micro-examples/microkit/port_queues/event_data_base_types/attestation/system_args.json index b9a0387..3c249ba 100644 --- a/micro-examples/microkit/port_queues/event_data_base_types/attestation/system_args.json +++ b/micro-examples/microkit/port_queues/event_data_base_types/attestation/system_args.json @@ -1,2 +1,3 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_base_types/hamr/microkit/microkit.system", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/port_queues/event_data_base_types/attestation/system.golden"} +{"dirpath": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_base_types/hamr/microkit/", + "suffix": ".system", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_base_types/attestation/microkit_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/port_queues/event_data_base_types/readme.md b/micro-examples/microkit/port_queues/event_data_base_types/readme.md index 9132ff9..e7a74d1 100644 --- a/micro-examples/microkit/port_queues/event_data_base_types/readme.md +++ b/micro-examples/microkit/port_queues/event_data_base_types/readme.md @@ -92,6 +92,13 @@ micro-examples/microkit/port_queues/event_data_base_types/aadl/bin/run-hamr.cmd ``` + Run the following to do an appraisal on the results (appraising will fail if any changes are made to the AADL files or the microkit.system file) + + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "\$HOME/provers/INSPECTA-models/micro-examples/microkit/port_queues/event_data_base_types/attestation/run-attestation.cmd aadl" + ``` + 1. Build and simulate the seL4 Microkit image Run the following from this repository's root directory. The docker image ``jasonbelt/microkit_domain_scheduling`` contains customized versions of Microkit and seL4 that support domain scheduling. They were built off the following pull requests @@ -99,9 +106,9 @@ - [microkit #175](https://github.com/seL4/microkit/pull/175) - [seL4 #1308](https://github.com/seL4/seL4/pull/1308) - ``` - docker run -it --rm -v $(pwd):/home/microkit/inspecta-models jasonbelt/microkit_domain_scheduling \ - bash -ci "cd \$HOME/inspecta-models/micro-examples/microkit/port_queues/event_data_base_types/hamr/microkit \ + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "cd \$HOME/provers/INSPECTA-models/micro-examples/microkit/port_queues/event_data_base_types/hamr/microkit \ && make qemu" ``` diff --git a/micro-examples/microkit/port_queues/event_data_struct/.ci/ci.cmd b/micro-examples/microkit/port_queues/event_data_struct/.ci/ci.cmd index 95382a1..9b06df7 100755 --- a/micro-examples/microkit/port_queues/event_data_struct/.ci/ci.cmd +++ b/micro-examples/microkit/port_queues/event_data_struct/.ci/ci.cmd @@ -51,6 +51,13 @@ if (result == 0) { if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) { result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit")) + if ((homeDir / "hamr" / "microkit" / "build").exists) { + (homeDir / "hamr" / "microkit" / "build").removeAll() + } +} + +if (result == 0) { + result = run("Running AADL attestation", F, proc"$sireum slang run ${homeDir / "attestation" / "run-attestation.cmd"} aadl") } Os.exit(result) \ No newline at end of file diff --git a/micro-examples/microkit/port_queues/event_data_struct/attestation/model.golden b/micro-examples/microkit/port_queues/event_data_struct/attestation/aadl_composite.txt similarity index 100% rename from micro-examples/microkit/port_queues/event_data_struct/attestation/model.golden rename to micro-examples/microkit/port_queues/event_data_struct/attestation/aadl_composite.txt diff --git a/micro-examples/microkit/port_queues/event_data_struct/attestation/micro_composite.txt b/micro-examples/microkit/port_queues/event_data_struct/attestation/aadl_micro_composite.txt similarity index 100% rename from micro-examples/microkit/port_queues/event_data_struct/attestation/micro_composite.txt rename to micro-examples/microkit/port_queues/event_data_struct/attestation/aadl_micro_composite.txt diff --git a/micro-examples/microkit/port_queues/event_data_struct/attestation/aadl_model_args.json b/micro-examples/microkit/port_queues/event_data_struct/attestation/aadl_model_args.json new file mode 100644 index 0000000..269d02a --- /dev/null +++ b/micro-examples/microkit/port_queues/event_data_struct/attestation/aadl_model_args.json @@ -0,0 +1,3 @@ +{"dirpath": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_struct/aadl/", + "suffix": ".aadl", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_struct/attestation/aadl_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/port_queues/event_data_struct/attestation/system.golden b/micro-examples/microkit/port_queues/event_data_struct/attestation/microkit_composite.txt similarity index 100% rename from micro-examples/microkit/port_queues/event_data_struct/attestation/system.golden rename to micro-examples/microkit/port_queues/event_data_struct/attestation/microkit_composite.txt diff --git a/micro-examples/microkit/port_queues/event_data_struct/attestation/model_args.json b/micro-examples/microkit/port_queues/event_data_struct/attestation/model_args.json deleted file mode 100644 index 8b3e911..0000000 --- a/micro-examples/microkit/port_queues/event_data_struct/attestation/model_args.json +++ /dev/null @@ -1,2 +0,0 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_struct/aadl/event_data_port_queues.aadl", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/port_queues/event_data_struct/attestation/model.golden"} diff --git a/micro-examples/microkit/port_queues/event_data_struct/attestation/run-attestation.cmd b/micro-examples/microkit/port_queues/event_data_struct/attestation/run-attestation.cmd new file mode 100755 index 0000000..b3ff5be --- /dev/null +++ b/micro-examples/microkit/port_queues/event_data_struct/attestation/run-attestation.cmd @@ -0,0 +1,129 @@ +::/*#! 2> /dev/null # +@ 2>/dev/null # 2>nul & echo off & goto BOF # +if [ -z ${SIREUM_HOME} ]; then # + echo "Please set SIREUM_HOME env var" # + exit -1 # +fi # +exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" # +:BOF +setlocal +if not defined SIREUM_HOME ( + echo Please set SIREUM_HOME env var + exit /B -1 +) +%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* +exit /B %errorlevel% +::!#*/ +// #Sireum + +import org.sireum._ + +val home = Os.slashDir +val projectDir = home.up + +if (!(ops.ISZOps(Os.cliArgs).contains("aadl")) && + !(ops.ISZOps(Os.cliArgs).contains("sysml")) && + !(ops.ISZOps(Os.cliArgs).contains("provision"))) { + println(st"""Pass one of the following arguments: + | provision: Reruns provisioning + | aadl: Performs an appraisal on the AADL artifacts + | sysml: Performs an appraisal on the SysML artifacts""".render) + Os.exit(0) +} + +val repoRoot = { + def f(p: Os.Path): Option[Os.Path] = { + if ((p / ".git" / "config").exists) { + assert((p / "micro-examples").exists, s"Expected ${p / "micro-examples"} to exist") + return Some(p) + } + return f(p.up) + } + f(projectDir).get +} + +val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" +val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") + +val microkitFile = home.up / "hamr" / "microkit" / "microkit.system" +assert(microkitFile.exists, s"Didn't find MSD at $microkitFile") + +val aadlDir = projectDir / "aadl" +val sysmlDir = projectDir / "sysml" + +val model_args = "model_args.json" +val system_args = home / "system_args.json" + +def makeArgs(extension: String, modelDir: Os.Path): Unit = { + @strictpure def getDir(dir: Os.Path): String = s"/INSPECTA-models/${repoRoot.relativize(dir).value}" + (home / s"${extension}_$model_args").writeOver( + st"""{"dirpath": "${getDir(modelDir)}/", + | "suffix": ".$extension", + | "filepath-golden": "${getDir(home)}/${extension}_composite.txt"}""".render) + system_args.writeOver(st"""{"dirpath": "${getDir(microkitFile.up)}/", + | "suffix": ".system", + | "filepath-golden": "${getDir(home)}/microkit_composite.txt"}""".render) +} + +if (aadlDir.exists) { + makeArgs("aadl", aadlDir) +} + +if (sysmlDir.exists) { + makeArgs("sysml", sysmlDir) +} + + + +def run(title: String, proc: OsProto.Proc, verbose: B, checkExitCode: B): Z = { + println(s"$title ...") + val r = (if (verbose) proc.console.echo else proc).run() + if (checkExitCode &&r.exitCode != 0) { + println(s"$title failed!") + cprintln(F, r.out) + cprintln(T, r.err) + } + return if (r.exitCode == 0) 0 else 1 +} + +val DEMO_ROOT = repoRoot.up +assert (Os.env("DEMO_ROOT").nonEmpty && DEMO_ROOT.value == Os.env("DEMO_ROOT").get, "DEMO_ROOT environment variable not set") + +val testsDir = DEMO_ROOT / "am-cakeml" / "tests" + +val micro_composite = testsDir / "DemoFiles" / "goldenFiles" / "micro_composite.txt" + +var aargs = ISZ[String]((testsDir / "CI" / "Test.sh").value, "-t", "micro", "-h", + "-s", system_args.value) + +if (ops.ISZOps(Os.cliArgs).contains("provision")) { + def provision(extension: String): Unit = { + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + if (cached_micro_composite.exists) { + cached_micro_composite.remove() + } + val f = home / s"${extension}_$model_args" + run(s"Provisioning $f", Os.proc(aargs :+ "-m" :+ f.value :+ "-p"), F, F) + + assert(micro_composite.exists) + micro_composite.copyOverTo(cached_micro_composite) + } + if (aadlDir.exists) { + provision("aadl") + } + if (sysmlDir.exists) { + provision("sysml") + } + Os.exit(0) +} else { + val extension = + if (ops.ISZOps(Os.cliArgs).contains("aadl")) "aadl" + else if (ops.ISZOps(Os.cliArgs).contains("sysml")) "sysml" + else "aadl" + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + cached_micro_composite.copyOverTo(micro_composite) + val f = home / s"${extension}_$model_args" + val result = run(s"Appraising $f", Os.proc(aargs :+ "-m" :+ f.value), F, T) + println(s"Appraisal ${if (result == 0) "succeeded" else "failed"}!") + Os.exit(result) +} \ No newline at end of file diff --git a/micro-examples/microkit/port_queues/event_data_struct/attestation/system_args.json b/micro-examples/microkit/port_queues/event_data_struct/attestation/system_args.json index d461ef2..6bfed51 100644 --- a/micro-examples/microkit/port_queues/event_data_struct/attestation/system_args.json +++ b/micro-examples/microkit/port_queues/event_data_struct/attestation/system_args.json @@ -1,2 +1,3 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_struct/hamr/microkit/microkit.system", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/port_queues/event_data_struct/attestation/system.golden"} +{"dirpath": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_struct/hamr/microkit/", + "suffix": ".system", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/port_queues/event_data_struct/attestation/microkit_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/port_queues/event_data_struct/readme.md b/micro-examples/microkit/port_queues/event_data_struct/readme.md index cfa1ee9..8c1f45b 100644 --- a/micro-examples/microkit/port_queues/event_data_struct/readme.md +++ b/micro-examples/microkit/port_queues/event_data_struct/readme.md @@ -91,6 +91,12 @@ ``` micro-examples/microkit/port_queues/event_data_struct/aadl/bin/run-hamr.cmd ``` + Run the following to do an appraisal on the results (appraising will fail if any changes are made to the AADL files or the microkit.system file) + + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "\$HOME/provers/INSPECTA-models/micro-examples/microkit/port_queues/event_data_struct/attestation/run-attestation.cmd aadl" + ``` 1. Build and simulate the seL4 Microkit image @@ -99,9 +105,9 @@ - [microkit #175](https://github.com/seL4/microkit/pull/175) - [seL4 #1308](https://github.com/seL4/seL4/pull/1308) - ``` - docker run -it --rm -v $(pwd):/home/microkit/inspecta-models jasonbelt/microkit_domain_scheduling \ - bash -ci "cd \$HOME/inspecta-models/micro-examples/microkit/port_queues/event_data_struct/hamr/microkit \ + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "cd \$HOME/provers/INSPECTA-models/micro-examples/microkit/port_queues/event_data_struct/hamr/microkit \ && make qemu" ``` diff --git a/micro-examples/microkit/vms/data/receiver/.ci/ci.cmd b/micro-examples/microkit/vms/data/receiver/.ci/ci.cmd index 959fd23..b8e44bd 100755 --- a/micro-examples/microkit/vms/data/receiver/.ci/ci.cmd +++ b/micro-examples/microkit/vms/data/receiver/.ci/ci.cmd @@ -68,6 +68,17 @@ if (result == 0) { if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) { result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit")) + if ((homeDir / "hamr" / "microkit" / "build").exists) { + (homeDir / "hamr" / "microkit" / "build").removeAll() + } +} + +if (result == 0) { + result = run("Running AADL attestation", F, proc"$sireum slang run ${homeDir / "attestation" / "run-attestation.cmd"} aadl") +} + +if ((consumerDir / "libvmm").exists) { + (consumerDir / "libvmm").removeAll() } Os.exit(result) \ No newline at end of file diff --git a/micro-examples/microkit/vms/data/receiver/attestation/model.golden b/micro-examples/microkit/vms/data/receiver/attestation/aadl_composite.txt similarity index 100% rename from micro-examples/microkit/vms/data/receiver/attestation/model.golden rename to micro-examples/microkit/vms/data/receiver/attestation/aadl_composite.txt diff --git a/micro-examples/microkit/vms/data/receiver/attestation/micro_composite.txt b/micro-examples/microkit/vms/data/receiver/attestation/aadl_micro_composite.txt similarity index 100% rename from micro-examples/microkit/vms/data/receiver/attestation/micro_composite.txt rename to micro-examples/microkit/vms/data/receiver/attestation/aadl_micro_composite.txt diff --git a/micro-examples/microkit/vms/data/receiver/attestation/aadl_model_args.json b/micro-examples/microkit/vms/data/receiver/attestation/aadl_model_args.json new file mode 100644 index 0000000..d3fac5f --- /dev/null +++ b/micro-examples/microkit/vms/data/receiver/attestation/aadl_model_args.json @@ -0,0 +1,3 @@ +{"dirpath": "/INSPECTA-models/micro-examples/microkit/vms/data/receiver/aadl/", + "suffix": ".aadl", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/vms/data/receiver/attestation/aadl_composite.txt"} \ No newline at end of file diff --git a/micro-examples/microkit/vms/data/receiver/attestation/system.golden b/micro-examples/microkit/vms/data/receiver/attestation/microkit_composite.txt similarity index 100% rename from micro-examples/microkit/vms/data/receiver/attestation/system.golden rename to micro-examples/microkit/vms/data/receiver/attestation/microkit_composite.txt diff --git a/micro-examples/microkit/vms/data/receiver/attestation/model_args.json b/micro-examples/microkit/vms/data/receiver/attestation/model_args.json deleted file mode 100644 index af87b10..0000000 --- a/micro-examples/microkit/vms/data/receiver/attestation/model_args.json +++ /dev/null @@ -1,2 +0,0 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/vms/data/receiver/aadl/vmR_data.aadl", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/vms/data/receiver/attestation/model.golden"} diff --git a/micro-examples/microkit/vms/data/receiver/attestation/run-attestation.cmd b/micro-examples/microkit/vms/data/receiver/attestation/run-attestation.cmd new file mode 100755 index 0000000..b3ff5be --- /dev/null +++ b/micro-examples/microkit/vms/data/receiver/attestation/run-attestation.cmd @@ -0,0 +1,129 @@ +::/*#! 2> /dev/null # +@ 2>/dev/null # 2>nul & echo off & goto BOF # +if [ -z ${SIREUM_HOME} ]; then # + echo "Please set SIREUM_HOME env var" # + exit -1 # +fi # +exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" # +:BOF +setlocal +if not defined SIREUM_HOME ( + echo Please set SIREUM_HOME env var + exit /B -1 +) +%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* +exit /B %errorlevel% +::!#*/ +// #Sireum + +import org.sireum._ + +val home = Os.slashDir +val projectDir = home.up + +if (!(ops.ISZOps(Os.cliArgs).contains("aadl")) && + !(ops.ISZOps(Os.cliArgs).contains("sysml")) && + !(ops.ISZOps(Os.cliArgs).contains("provision"))) { + println(st"""Pass one of the following arguments: + | provision: Reruns provisioning + | aadl: Performs an appraisal on the AADL artifacts + | sysml: Performs an appraisal on the SysML artifacts""".render) + Os.exit(0) +} + +val repoRoot = { + def f(p: Os.Path): Option[Os.Path] = { + if ((p / ".git" / "config").exists) { + assert((p / "micro-examples").exists, s"Expected ${p / "micro-examples"} to exist") + return Some(p) + } + return f(p.up) + } + f(projectDir).get +} + +val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" +val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") + +val microkitFile = home.up / "hamr" / "microkit" / "microkit.system" +assert(microkitFile.exists, s"Didn't find MSD at $microkitFile") + +val aadlDir = projectDir / "aadl" +val sysmlDir = projectDir / "sysml" + +val model_args = "model_args.json" +val system_args = home / "system_args.json" + +def makeArgs(extension: String, modelDir: Os.Path): Unit = { + @strictpure def getDir(dir: Os.Path): String = s"/INSPECTA-models/${repoRoot.relativize(dir).value}" + (home / s"${extension}_$model_args").writeOver( + st"""{"dirpath": "${getDir(modelDir)}/", + | "suffix": ".$extension", + | "filepath-golden": "${getDir(home)}/${extension}_composite.txt"}""".render) + system_args.writeOver(st"""{"dirpath": "${getDir(microkitFile.up)}/", + | "suffix": ".system", + | "filepath-golden": "${getDir(home)}/microkit_composite.txt"}""".render) +} + +if (aadlDir.exists) { + makeArgs("aadl", aadlDir) +} + +if (sysmlDir.exists) { + makeArgs("sysml", sysmlDir) +} + + + +def run(title: String, proc: OsProto.Proc, verbose: B, checkExitCode: B): Z = { + println(s"$title ...") + val r = (if (verbose) proc.console.echo else proc).run() + if (checkExitCode &&r.exitCode != 0) { + println(s"$title failed!") + cprintln(F, r.out) + cprintln(T, r.err) + } + return if (r.exitCode == 0) 0 else 1 +} + +val DEMO_ROOT = repoRoot.up +assert (Os.env("DEMO_ROOT").nonEmpty && DEMO_ROOT.value == Os.env("DEMO_ROOT").get, "DEMO_ROOT environment variable not set") + +val testsDir = DEMO_ROOT / "am-cakeml" / "tests" + +val micro_composite = testsDir / "DemoFiles" / "goldenFiles" / "micro_composite.txt" + +var aargs = ISZ[String]((testsDir / "CI" / "Test.sh").value, "-t", "micro", "-h", + "-s", system_args.value) + +if (ops.ISZOps(Os.cliArgs).contains("provision")) { + def provision(extension: String): Unit = { + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + if (cached_micro_composite.exists) { + cached_micro_composite.remove() + } + val f = home / s"${extension}_$model_args" + run(s"Provisioning $f", Os.proc(aargs :+ "-m" :+ f.value :+ "-p"), F, F) + + assert(micro_composite.exists) + micro_composite.copyOverTo(cached_micro_composite) + } + if (aadlDir.exists) { + provision("aadl") + } + if (sysmlDir.exists) { + provision("sysml") + } + Os.exit(0) +} else { + val extension = + if (ops.ISZOps(Os.cliArgs).contains("aadl")) "aadl" + else if (ops.ISZOps(Os.cliArgs).contains("sysml")) "sysml" + else "aadl" + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + cached_micro_composite.copyOverTo(micro_composite) + val f = home / s"${extension}_$model_args" + val result = run(s"Appraising $f", Os.proc(aargs :+ "-m" :+ f.value), F, T) + println(s"Appraisal ${if (result == 0) "succeeded" else "failed"}!") + Os.exit(result) +} \ No newline at end of file diff --git a/micro-examples/microkit/vms/data/receiver/attestation/system_args.json b/micro-examples/microkit/vms/data/receiver/attestation/system_args.json index 92c26ae..f1b1f10 100644 --- a/micro-examples/microkit/vms/data/receiver/attestation/system_args.json +++ b/micro-examples/microkit/vms/data/receiver/attestation/system_args.json @@ -1,2 +1,3 @@ -{"filepath": "/INSPECTA-models/micro-examples/microkit/vms/data/receiver/hamr/microkit/microkit.system", - "filepath-golden":"/INSPECTA-models/micro-examples/microkit/vms/data/receiver/attestation/system.golden"} +{"dirpath": "/INSPECTA-models/micro-examples/microkit/vms/data/receiver/hamr/microkit/", + "suffix": ".system", + "filepath-golden": "/INSPECTA-models/micro-examples/microkit/vms/data/receiver/attestation/microkit_composite.txt"} \ No newline at end of file diff --git a/open-platform-models/isolate-ethernet-simple/.ci/ci.cmd b/open-platform-models/isolate-ethernet-simple/.ci/ci.cmd index 86a1322..a53330c 100755 --- a/open-platform-models/isolate-ethernet-simple/.ci/ci.cmd +++ b/open-platform-models/isolate-ethernet-simple/.ci/ci.cmd @@ -50,7 +50,14 @@ if (result == 0) { } if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) { - result = run("Building the image", F, proc"make".at(homeDir / "microkit")) + result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit")) + if ((homeDir / "hamr" / "microkit" / "build").exists) { + (homeDir / "hamr" / "microkit" / "build").removeAll() + } +} + +if (result == 0) { + result = run("Running AADL attestation", F, proc"$sireum slang run ${homeDir / "attestation" / "run-attestation.cmd"} aadl") } Os.exit(result) \ No newline at end of file diff --git a/open-platform-models/isolate-ethernet-simple/aadl/bin/clean.cmd b/open-platform-models/isolate-ethernet-simple/aadl/bin/clean.cmd index f93e8a3..746ea8a 100755 --- a/open-platform-models/isolate-ethernet-simple/aadl/bin/clean.cmd +++ b/open-platform-models/isolate-ethernet-simple/aadl/bin/clean.cmd @@ -20,7 +20,7 @@ import org.sireum._ val homeDir = Os.slashDir.up.up -val microkitDir = homeDir / "microkit" +val microkitDir = homeDir / "hamr" / "microkit" @sig trait Keep { @pure def keep(f: Os.Path): B diff --git a/open-platform-models/isolate-ethernet-simple/aadl/bin/run-hamr.cmd b/open-platform-models/isolate-ethernet-simple/aadl/bin/run-hamr.cmd index a6c6664..7121163 100755 --- a/open-platform-models/isolate-ethernet-simple/aadl/bin/run-hamr.cmd +++ b/open-platform-models/isolate-ethernet-simple/aadl/bin/run-hamr.cmd @@ -62,7 +62,7 @@ var codegenArgs = ISZ("hamr", "codegen", //"--package-name", packageName, //"--output-dir", (aadlDir.up / "hamr" / "slang").string, //"--output-c-dir", (aadlDir.up / "hamr" / "c").string, - "--sel4-output-dir", (aadlDir.up / "microkit").string, + "--sel4-output-dir", (aadlDir.up / "hamr" / "microkit").string, //"--run-transpiler", //"--bit-width", "32", //"--max-string-size", "256", diff --git a/open-platform-models/isolate-ethernet-simple/attestation/aadl_composite.txt b/open-platform-models/isolate-ethernet-simple/attestation/aadl_composite.txt new file mode 100644 index 0000000..d07fa56 --- /dev/null +++ b/open-platform-models/isolate-ethernet-simple/attestation/aadl_composite.txt @@ -0,0 +1 @@ +XѼ~7'ݥ>@ C% \ No newline at end of file diff --git a/open-platform-models/isolate-ethernet-simple/attestation/aadl_micro_composite.txt b/open-platform-models/isolate-ethernet-simple/attestation/aadl_micro_composite.txt new file mode 100644 index 0000000..87e3a79 --- /dev/null +++ b/open-platform-models/isolate-ethernet-simple/attestation/aadl_micro_composite.txt @@ -0,0 +1 @@ +[+d9E]4MTgkCv>GĉeXb \ No newline at end of file diff --git a/open-platform-models/isolate-ethernet-simple/attestation/aadl_model_args.json b/open-platform-models/isolate-ethernet-simple/attestation/aadl_model_args.json new file mode 100644 index 0000000..328e254 --- /dev/null +++ b/open-platform-models/isolate-ethernet-simple/attestation/aadl_model_args.json @@ -0,0 +1,3 @@ +{"dirpath": "/INSPECTA-models/open-platform-models/isolate-ethernet-simple/aadl/", + "suffix": ".aadl", + "filepath-golden": "/INSPECTA-models/open-platform-models/isolate-ethernet-simple/attestation/aadl_composite.txt"} \ No newline at end of file diff --git a/open-platform-models/isolate-ethernet-simple/attestation/micro_composite.txt b/open-platform-models/isolate-ethernet-simple/attestation/micro_composite.txt deleted file mode 100644 index 3b132c2..0000000 --- a/open-platform-models/isolate-ethernet-simple/attestation/micro_composite.txt +++ /dev/null @@ -1 +0,0 @@ -E-AMj/}<oFf&f- \ No newline at end of file diff --git a/open-platform-models/isolate-ethernet-simple/attestation/system.golden b/open-platform-models/isolate-ethernet-simple/attestation/microkit_composite.txt similarity index 100% rename from open-platform-models/isolate-ethernet-simple/attestation/system.golden rename to open-platform-models/isolate-ethernet-simple/attestation/microkit_composite.txt diff --git a/open-platform-models/isolate-ethernet-simple/attestation/model.golden b/open-platform-models/isolate-ethernet-simple/attestation/model.golden deleted file mode 100644 index 13e2267..0000000 --- a/open-platform-models/isolate-ethernet-simple/attestation/model.golden +++ /dev/null @@ -1 +0,0 @@ -@3bߕ!P pYGYyJ \ No newline at end of file diff --git a/open-platform-models/isolate-ethernet-simple/attestation/model_args.json b/open-platform-models/isolate-ethernet-simple/attestation/model_args.json deleted file mode 100644 index 3d1e5e9..0000000 --- a/open-platform-models/isolate-ethernet-simple/attestation/model_args.json +++ /dev/null @@ -1,2 +0,0 @@ -{"filepath": "/INSPECTA-models/open-platform-models/isolate-ethernet-simple/aadl/platform.aadl", - "filepath-golden":"/INSPECTA-models/open-platform-models/isolate-ethernet-simple/attestation/model.golden"} diff --git a/open-platform-models/isolate-ethernet-simple/attestation/run-attestation.cmd b/open-platform-models/isolate-ethernet-simple/attestation/run-attestation.cmd new file mode 100755 index 0000000..3b13ded --- /dev/null +++ b/open-platform-models/isolate-ethernet-simple/attestation/run-attestation.cmd @@ -0,0 +1,129 @@ +::/*#! 2> /dev/null # +@ 2>/dev/null # 2>nul & echo off & goto BOF # +if [ -z ${SIREUM_HOME} ]; then # + echo "Please set SIREUM_HOME env var" # + exit -1 # +fi # +exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" # +:BOF +setlocal +if not defined SIREUM_HOME ( + echo Please set SIREUM_HOME env var + exit /B -1 +) +%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %* +exit /B %errorlevel% +::!#*/ +// #Sireum + +import org.sireum._ + +val home = Os.slashDir +val projectDir = home.up + +if (!(ops.ISZOps(Os.cliArgs).contains("aadl")) && + !(ops.ISZOps(Os.cliArgs).contains("sysml")) && + !(ops.ISZOps(Os.cliArgs).contains("provision"))) { + println(st"""Pass one of the following arguments: + | provision: Reruns provisioning + | aadl: Performs an appraisal on the AADL artifacts + | sysml: Performs an appraisal on the SysML artifacts""".render) + Os.exit(0) +} + +val repoRoot = { + def f(p: Os.Path): Option[Os.Path] = { + if ((p / ".git" / "config").exists) { + assert((p / "micro-examples").exists, s"Expected ${p / "micro-examples"} to exist") + return Some(p) + } + return f(p.up) + } + f(projectDir).get +} + +val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" +val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum") + +val microkitFile = home.up / "hamr" / "microkit" / "microkit.system" +assert(microkitFile.exists, s"Didn't find MSD at $microkitFile") + +val aadlDir = projectDir / "aadl" +val sysmlDir = projectDir / "sysml" + +val model_args = "model_args.json" +val system_args = home / "system_args.json" + +def makeArgs(extension: String, modelDir: Os.Path): Unit = { + @strictpure def getDir(dir: Os.Path): String = s"/INSPECTA-models/${repoRoot.relativize(dir).value}" + (home / s"${extension}_$model_args").writeOver( + st"""{"dirpath": "${getDir(modelDir)}/", + | "suffix": ".$extension", + | "filepath-golden": "${getDir(home)}/${extension}_composite.txt"}""".render) + system_args.writeOver(st"""{"dirpath": "${getDir(microkitFile.up)}/", + | "suffix": ".system", + | "filepath-golden": "${getDir(home)}/microkit_composite.txt"}""".render) +} + +if (aadlDir.exists) { + makeArgs("aadl", aadlDir) +} + +if (sysmlDir.exists) { + makeArgs("sysml", sysmlDir) +} + + + +def run(title: String, proc: OsProto.Proc, verbose: B, checkExitCode: B): Z = { + println(s"$title ...") + val r = (if (verbose) proc.console.echo else proc).run() + if (checkExitCode &&r.exitCode != 0) { + println(s"$title failed!") + cprintln(F, r.out) + cprintln(T, r.err) + } + return if (r.exitCode == 0) 0 else 1 +} + +val DEMO_ROOT = repoRoot.up +assert (Os.env("DEMO_ROOT").nonEmpty && DEMO_ROOT.value == Os.env("DEMO_ROOT").get, "DEMO_ROOT environment variable not set") + +val testsDir = DEMO_ROOT / "am-cakeml" / "tests" + +val micro_composite = testsDir / "DemoFiles" / "goldenFiles" / "micro_composite.txt" + +var aargs = ISZ[String]((testsDir / "CI" / "Test.sh").value, "-t", "micro", "-h", + "-s", system_args.value) + +if (ops.ISZOps(Os.cliArgs).contains("provision")) { + def provision(extension: String): Unit = { + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + if (cached_micro_composite.exists) { + cached_micro_composite.remove() + } + val f = home / s"${extension}_$model_args" + run(s"Provisioning $f", Os.proc(aargs :+ "-m" :+ f.value :+ "-p"), F, F) + + assert(micro_composite.exists) + micro_composite.copyOverTo(cached_micro_composite) + } + if (aadlDir.exists) { + provision("aadl") + } + if (sysmlDir.exists) { + provision("sysml") + } + Os.exit(0) +} else { + val extension = + if (ops.ISZOps(Os.cliArgs).contains("aadl")) "aadl" + else if (ops.ISZOps(Os.cliArgs).contains("sysml")) "sysml" + else "aadl" + val cached_micro_composite = home / s"${extension}_micro_composite.txt" + cached_micro_composite.copyOverTo(micro_composite) + val f = home / s"${extension}_$model_args" + val result = run(s"Appraising $f", Os.proc(aargs :+ "-m" :+ f.value), F, T) + println(s"Appraisal ${if (result == 0) "succeeded" else "failed"}!") + Os.exit(result) +} \ No newline at end of file diff --git a/open-platform-models/isolate-ethernet-simple/attestation/system_args.json b/open-platform-models/isolate-ethernet-simple/attestation/system_args.json index fa87485..c297f56 100644 --- a/open-platform-models/isolate-ethernet-simple/attestation/system_args.json +++ b/open-platform-models/isolate-ethernet-simple/attestation/system_args.json @@ -1,2 +1,3 @@ -{"filepath": "/INSPECTA-models/open-platform-models/isolate-ethernet-simple/microkit/microkit.system", - "filepath-golden":"/INSPECTA-models/open-platform-models/isolate-ethernet-simple/attestation/system.golden"} +{"dirpath": "/INSPECTA-models/open-platform-models/isolate-ethernet-simple/hamr/microkit/", + "suffix": ".system", + "filepath-golden": "/INSPECTA-models/open-platform-models/isolate-ethernet-simple/attestation/microkit_composite.txt"} \ No newline at end of file diff --git a/open-platform-models/isolate-ethernet-simple/microkit/Makefile b/open-platform-models/isolate-ethernet-simple/hamr/microkit/Makefile similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/Makefile rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/Makefile diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/pacer/src/pacer.c b/open-platform-models/isolate-ethernet-simple/hamr/microkit/components/pacer/src/pacer.c similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/components/pacer/src/pacer.c rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/components/pacer/src/pacer.c diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_ArduPilot_ArduPilot/include/seL4_ArduPilot_ArduPilot.h b/open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_ArduPilot_ArduPilot/include/seL4_ArduPilot_ArduPilot.h similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/components/seL4_ArduPilot_ArduPilot/include/seL4_ArduPilot_ArduPilot.h rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_ArduPilot_ArduPilot/include/seL4_ArduPilot_ArduPilot.h diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot.c b/open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot.c similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot.c rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot.c diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot_MON.c b/open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot_MON.c similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot_MON.c rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot_MON.c diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot_user.c b/open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot_user.c similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot_user.c rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_ArduPilot_ArduPilot/src/seL4_ArduPilot_ArduPilot_user.c diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_Firewall_Firewall/include/seL4_Firewall_Firewall.h b/open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_Firewall_Firewall/include/seL4_Firewall_Firewall.h similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/components/seL4_Firewall_Firewall/include/seL4_Firewall_Firewall.h rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_Firewall_Firewall/include/seL4_Firewall_Firewall.h diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall.c b/open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall.c similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall.c rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall.c diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall_MON.c b/open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall_MON.c similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall_MON.c rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall_MON.c diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall_user.c b/open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall_user.c similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall_user.c rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_Firewall_Firewall/src/seL4_Firewall_Firewall_user.c diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/include/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.h b/open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/include/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.h similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/include/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.h rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/include/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.h diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.c b/open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.c similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.c rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver.c diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_MON.c b/open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_MON.c similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_MON.c rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_MON.c diff --git a/open-platform-models/isolate-ethernet-simple/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_user.c b/open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_user.c similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_user.c rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/components/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver/src/seL4_LowLevelEthernetDriver_LowLevelEthernetDriver_user.c diff --git a/open-platform-models/isolate-ethernet-simple/microkit/microkit.dot b/open-platform-models/isolate-ethernet-simple/hamr/microkit/microkit.dot similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/microkit.dot rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/microkit.dot diff --git a/open-platform-models/isolate-ethernet-simple/microkit/microkit.system b/open-platform-models/isolate-ethernet-simple/hamr/microkit/microkit.system similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/microkit.system rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/microkit.system diff --git a/open-platform-models/isolate-ethernet-simple/microkit/system.mk b/open-platform-models/isolate-ethernet-simple/hamr/microkit/system.mk similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/system.mk rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/system.mk diff --git a/open-platform-models/isolate-ethernet-simple/microkit/types/include/sb_aadl_types.h b/open-platform-models/isolate-ethernet-simple/hamr/microkit/types/include/sb_aadl_types.h similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/types/include/sb_aadl_types.h rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/types/include/sb_aadl_types.h diff --git a/open-platform-models/isolate-ethernet-simple/microkit/types/include/sb_event_counter.h b/open-platform-models/isolate-ethernet-simple/hamr/microkit/types/include/sb_event_counter.h similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/types/include/sb_event_counter.h rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/types/include/sb_event_counter.h diff --git a/open-platform-models/isolate-ethernet-simple/microkit/types/include/sb_queue_base_SW_RawEthernetMessage_Impl_1.h b/open-platform-models/isolate-ethernet-simple/hamr/microkit/types/include/sb_queue_base_SW_RawEthernetMessage_Impl_1.h similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/types/include/sb_queue_base_SW_RawEthernetMessage_Impl_1.h rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/types/include/sb_queue_base_SW_RawEthernetMessage_Impl_1.h diff --git a/open-platform-models/isolate-ethernet-simple/microkit/types/include/sb_types.h b/open-platform-models/isolate-ethernet-simple/hamr/microkit/types/include/sb_types.h similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/types/include/sb_types.h rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/types/include/sb_types.h diff --git a/open-platform-models/isolate-ethernet-simple/microkit/types/src/sb_queue_base_SW_RawEthernetMessage_Impl_1.c b/open-platform-models/isolate-ethernet-simple/hamr/microkit/types/src/sb_queue_base_SW_RawEthernetMessage_Impl_1.c similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/types/src/sb_queue_base_SW_RawEthernetMessage_Impl_1.c rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/types/src/sb_queue_base_SW_RawEthernetMessage_Impl_1.c diff --git a/open-platform-models/isolate-ethernet-simple/microkit/util/include/printf.h b/open-platform-models/isolate-ethernet-simple/hamr/microkit/util/include/printf.h similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/util/include/printf.h rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/util/include/printf.h diff --git a/open-platform-models/isolate-ethernet-simple/microkit/util/include/util.h b/open-platform-models/isolate-ethernet-simple/hamr/microkit/util/include/util.h similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/util/include/util.h rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/util/include/util.h diff --git a/open-platform-models/isolate-ethernet-simple/microkit/util/src/printf.c b/open-platform-models/isolate-ethernet-simple/hamr/microkit/util/src/printf.c similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/util/src/printf.c rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/util/src/printf.c diff --git a/open-platform-models/isolate-ethernet-simple/microkit/util/src/util.c b/open-platform-models/isolate-ethernet-simple/hamr/microkit/util/src/util.c similarity index 100% rename from open-platform-models/isolate-ethernet-simple/microkit/util/src/util.c rename to open-platform-models/isolate-ethernet-simple/hamr/microkit/util/src/util.c diff --git a/open-platform-models/isolate-ethernet-simple/readme.md b/open-platform-models/isolate-ethernet-simple/readme.md index e6c3c52..9e1ed1f 100644 --- a/open-platform-models/isolate-ethernet-simple/readme.md +++ b/open-platform-models/isolate-ethernet-simple/readme.md @@ -78,6 +78,12 @@ If the above issue was resolved then the value of the model property [here](SW.aadl#L14) should equal the value of the codegen artficact [here](microkit/include/types.h#L7). + Run the following to do an appraisal on the results (appraising will fail if any changes are made to the AADL files or the microkit.system file) + + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "\$HOME/provers/INSPECTA-models/open-platform-models/isolate-ethernet-simple/attestation/run-attestation.cmd aadl" + ``` 1. Build and simulate the seL4 Microkit image Run the following from this repository's root directory. The docker image ``jasonbelt/microkit_domain_scheduling`` contains customized versions of Microkit and seL4 that support domain scheduling. They were built off the following pull requests @@ -85,9 +91,9 @@ - [microkit #175](https://github.com/seL4/microkit/pull/175) - [seL4 #1308](https://github.com/seL4/seL4/pull/1308) - ``` - docker run -it --rm -v $(pwd):/home/microkit/inspecta-models jasonbelt/microkit_domain_scheduling \ - bash -ci "cd \$HOME/inspecta-models/open-platform-models/isolate-ethernet-simple/microkit \ + ``` + docker run -it --rm -v $(pwd):/home/microkit/provers/INSPECTA-models jasonbelt/microkit_domain_scheduling \ + bash -ci "cd \$HOME/provers/INSPECTA-models/open-platform-models/isolate-ethernet-simple/hamr/microkit \ && make qemu" ```