From 43f9afe277711ce41bc157dd03f962bde9c9d62a Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Sat, 10 Dec 2022 18:42:14 -0500 Subject: [PATCH] Setup first draft of diff script. Need to fine tune preprocessor flags. --- .../preprocess_file_for_diff.sh | 51 ++++++++++++++++++ .../preprocess_file_for_verification.sh | 2 +- .../VeriFast/tasks/vTaskSwitchContext/diff.sh | 53 +++++++++++++++++++ .../tasks/vTaskSwitchContext/paths.sh | 43 +++++++++++++++ 4 files changed, 148 insertions(+), 1 deletion(-) create mode 100755 Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_file_for_diff.sh create mode 100755 Test/VeriFast/tasks/vTaskSwitchContext/diff.sh diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_file_for_diff.sh b/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_file_for_diff.sh new file mode 100755 index 000000000..b3ca1456d --- /dev/null +++ b/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" \ No newline at end of file diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_file_for_verification.sh b/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_file_for_verification.sh index 8dadc0d67..81cce3fe8 100755 --- a/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_file_for_verification.sh +++ b/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" \ No newline at end of file diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh b/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh new file mode 100755 index 000000000..2afd3af95 --- /dev/null +++ b/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` \ No newline at end of file diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/paths.sh b/Test/VeriFast/tasks/vTaskSwitchContext/paths.sh index d869da049..21cd42f14 100755 --- a/Test/VeriFast/tasks/vTaskSwitchContext/paths.sh +++ b/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: