Enable SPARK proofs for SPDM responder example

Ref. eng/recordflux/RecordFlux#1704
AdaCore · Sep 6, 2024 · 6c0c94d · 6c0c94d
1 parent 1677c46
commit 6c0c94d
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 10 deletions.
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
@@ -504,23 +504,23 @@ verification_apps:
   services:
     - image:recordflux
     - cpu:4
-    - mem:30
+    - mem:32
     - security_group:GitLabRunnerTasksExecDefaultSG
   parallel:
     matrix:
-      - APP:
-        - "ping"
-        - "dhcp_client"
-        - "spdm_responder"
-        - "dccp"
+      - APP: "ping"
+      - APP: "dhcp_client"
+      - APP: "spdm_responder"
+        PROOF_PROCS: 2
+      - APP: "dccp"
   script:
     - *show_gnatprove_cache_stats
     - *update_timestamps_of_generated_code
     - *setup_gnat
     - *setup_spark
     - *setup_gnat_cross
     - *setup_python
-    - timeout -k 60 27600 make -C examples/apps/${APP} prove
+    - timeout -k 60 20000 make -C examples/apps/${APP} prove
   cache:
     - *spark-cache-main
     - *spark-cache

diff --git a/examples/apps/spdm_responder/Makefile b/examples/apps/spdm_responder/Makefile
@@ -1,5 +1,7 @@
 include ../../../Makefile.common
 
+PROOF_PROCS ?= $(shell nproc)
+
 GENERATED = generated/rflx-spdm.ads
 
 SOURCE_SPECIFICATIONS = \
@@ -71,9 +73,10 @@ libriscv64: $(BUILD_DIR)/riscv64/lib/libspdm.a
 
 .PHONY: prove
 
+# TODO(eng/recordflux/RecordFlux#1390): Prove SPDM messages
 prove: $(GNATPROVE_CACHE_DIR) $(GENERATED)
-	gnatprove -P build_lib.gpr -j0 -XTARGET=riscv64 -u responder
-	gnatprove -P build.gpr -j0 -XTARGET=riscv64 -u main
+	gnatprove -P build_lib.gpr -j$(PROOF_PROCS) -XTARGET=riscv64 -u responder -u rflx.spdm_responder.session -u rflx.spdm_responder.session.fsm -u rflx.spdm_responder.session.fsm_allocator -u rflx.spdm_responder.session_environment
+	gnatprove -P build.gpr -j$(PROOF_PROCS) -XTARGET=riscv64 -u main
 
 .PHONY: generate
 

diff --git a/examples/apps/spdm_responder/build_lib.gpr b/examples/apps/spdm_responder/build_lib.gpr
@@ -107,6 +107,7 @@ project Build_Lib is
    package Prove is
       for Proof_Switches ("Ada") use Defaults.Proof_Switches;
       for Proof_Switches ("responder.adb") use ("--prover=z3,cvc5", "--steps=64000", "--memlimit=6000", "--timeout=600");
+      for Proof_Switches ("rflx-spdm_responder-session-fsm.adb") use ("--timeout=120");
    end Prove;
 
 end Build_Lib;
diff --git a/examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session.adb b/examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session.adb
@@ -15,7 +15,7 @@ with RFLX.SPDM_Responder.Session_Environment;
 --  SPARK mode is disabled for this package body because the C binding requires
 --  Ada features that are not part of the SPARK language.
 package body RFLX.SPDM_Responder.Session with
-   SPARK_Mode
+   SPARK_Mode => Off
 is
    --  Return CT exponent (DSP0274_1.1.0 [178]).
    --