Setup first draft of diff script. Need to fine tune preprocessor flags.

Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_file_for_diff.sh

@@ -0,0 +1,51 @@
+#!/bin/bash
+SRC_FILE="$1"
+OUT_FILE="$2"
+ERR_FILE="$3"
+REPO_BASE_DIR="$4"
+VF_PROOF_BASE_DIR="$5"
+VF_DIR="$6"
+
+
+echo SRC_FILE:
+echo $SRC_FILE
+echo OUT_FILE:
+echo $OUT_FILE
+echo ERR_FILE:
+echo $ERR_FILE
+echo REPO_BASE_DIR:
+echo $REPO_BASE_DIR
+echo VF_PROOF_BASE_DIR:
+echo $VF_PROOF_BASE_DIR
+echo VF_DIR:
+echo $VF_DIR
+
+# Load functions used to compute paths.
+. "$VF_PROOF_BASE_DIR/paths.sh"
+
+# Load variables storing preprocessor flags.
+. "`pp_script_dir $REPO_BASE_DIR`/pp_flags.sh" "$REPO_BASE_DIR" "$VF_PROOF_BASE_DIR" "$VF_DIR"
+
+
+# Flags to SKIP expensive proofs:
+# - VERIFAST_SKIP_BITVECTOR_PROOF__STACK_ALIGNMENT
+
+
+
+
+# Relevant clang flags:
+# -E : Run preprocessor
+# -C : Include comments in output
+# -P : Surpresses line/file pragmas
+
+echo start preprocessor
+clang -E -C \
+\
+${BUILD_FLAGS[@]} \
+${VERIFAST_FLAGS[@]} \
+${RP2040_INLCUDE_FLAGS[@]} \
+${PICO_INCLUDE_FLAGS[@]} \
+-I`prod_header_dir $REPO_BASE_DIR` \
+\
+-c "$SRC_FILE" \
+1>"$OUT_FILE" 2>"$ERR_FILE"

Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_file_for_verification.sh

@@ -32,7 +32,7 @@ ${BUILD_FLAGS[@]} \
 ${VERIFAST_FLAGS[@]} \
 ${RP2040_INLCUDE_FLAGS[@]} \
 ${PICO_INCLUDE_FLAGS[@]} \
--I"$REPO_BASE_DIR/include" \
+-I`prod_header_dir $REPO_BASE_DIR` \
 \
 -c "$SRC_FILE" \
 1>"$OUT_FILE" 2>"$ERR_FILE"

Test/VeriFast/tasks/vTaskSwitchContext/diff.sh

@@ -0,0 +1,53 @@
+#!/bin/bash
+
+
+
+# Relative or absolute path to the directory this script and `paths.sh` reside in.
+PREFIX=`dirname $0`
+# Absolute path to the base of this repository.
+REPO_BASE_DIR="$1"
+
+# Load functions used to compute paths.
+. "$PREFIX/paths.sh"
+
+VF_PROOF_BASE_DIR=`vf_proof_base_dir $REPO_BASE_DIR`
+
+
+
+# Load functions used to compute paths.
+. "$PREFIX/paths.sh"
+
+VF_PROOF_DIR=`vf_proof_base_dir $REPO_BASE_DIR`
+
+PP_SCRIPT_DIR=`pp_script_dir $REPO_BASE_DIR`
+
+echo preprocessing production version of 'tasks.c'
+"$PP_SCRIPT_DIR/preprocess_file_for_diff.sh" \
+    `prod_tasks_c $REPO_BASE_DIR` \
+    `pp_prod_tasks_c $REPO_BASE_DIR` \
+    "`pp_log_dir $REPO_BASE_DIR`/err1.txt" \
+    $REPO_BASE_DIR \
+    $VF_PROOF_BASE_DIR
+
+echo preprocessing verified version of 'tasks.c'
+"$PP_SCRIPT_DIR/preprocess_file_for_diff.sh" \
+    `vf_annotated_tasks_c $REPO_BASE_DIR` \
+    `pp_vf_tasks_c $REPO_BASE_DIR` \
+    "`pp_log_dir $REPO_BASE_DIR`/err2.txt" \
+    $REPO_BASE_DIR \
+    $VF_PROOF_BASE_DIR
+
+# pp script args
+# SRC_FILE="$1"
+# OUT_FILE="$2"
+# ERR_FILE="$3"
+# REPO_BASE_DIR="$4"
+# VF_PROOF_BASE_DIR="$5"
+
+
+
+printf "\n\n\n"
+echo Diff:
+echo -----------------------------------------------------
+echo
+git diff --no-index "`pp_log_dir $REPO_BASE_DIR`/err1.txt" `pp_vf_tasks_c $REPO_BASE_DIR`

Test/VeriFast/tasks/vTaskSwitchContext/paths.sh

@@ -70,6 +70,38 @@ function vf_annotated_tasks_c() {
     echo "$VF_MOD_SRC_DIR/tasks.c"
 }
 
+# Returns the absolute path to the directory the unmodified FreeRTOS headers.
+#
+# Expected arguments:
+# $1 : Absolute path to the repository's base 
+function prod_header_dir() {
+    REPO_BASE_DIR="$1"
+
+    echo "$REPO_BASE_DIR/include"
+}
+
+# Returns the absolute path to the directory the unmodified FreeRTOS source 
+# files.
+#
+# Expected arguments:
+# $1 : Absolute path to the repository's base 
+function prod_src_dir() {
+    REPO_BASE_DIR="$1"
+
+    echo "$REPO_BASE_DIR"
+}
+
+# Returns the absolute path to the unmodified version of `tasks.c`.
+#
+# Expected arguments:
+# $1 : Absolute path to the repository's base 
+function prod_tasks_c() {
+    REPO_BASE_DIR="$1"
+    PROD_SRC_DIR=`prod_src_dir $REPO_BASE_DIR`
+
+    echo "$PROD_SRC_DIR/tasks.c"
+}
+
 
 # Returns the absolute path to the directory containing the preprocessing scripts.
 #
@@ -117,6 +149,17 @@ function pp_vf_tasks_c() {
     echo "$PP_OUT_DIR/tasks_vf_pp.c"
 }
 
+# Returns the absolute path to the preprocessed unmodified version of `tasks.c`.
+#
+# Expected arguments:
+# $1 : Absolute path to the repository's base 
+function pp_prod_tasks_c() {
+    REPO_BASE_DIR="$1"
+    PP_OUT_DIR=`pp_out_dir $REPO_BASE_DIR`
+
+    echo "$PP_OUT_DIR/tasks_prod_pp.c"
+}
+
 # Returns the absolute path to the pico sdk.
 #
 # Expected arguments: