-
Notifications
You must be signed in to change notification settings - Fork 0
/
validate.sh
executable file
·60 lines (49 loc) · 2 KB
/
validate.sh
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
#!/bin/bash
#Note that this script relies on Petr4 repository being cloned in the HOL4P4 root directory.
if [ $# -eq 0 ]; then
NTHREADS=1
else
NTHREADS=$1
fi
#1. Check if validation_tests directory exists, if not, check if ../../petr4/examples/checker_tests/good exists
#2. Copy over all .stf files and all .p4 files with a corresponding .stf file from the petr4 subdirectory to validation_tests if needed
#3. Check if p4include exists, if not, check if ../../petr4/ci-test/p4include exists
#4. Copy over all files from the petr4 subdirectory to p4include if needed
#if [ $# -eq 3 ]; then
# #Path to pairs of .p4 and .stf files
# TESTS_DIR=$2
# #Path to common P4 includes (core.p4, v1model.p4, ...)
# INCLUDES_DIR=$3
# #Path to skeleton files (arith-inline-skeleton.p4 and arith-skeleton.p4)
# SKELETONS_DIR=$4
#else
# #TODO: Use other subdirectories of expectation also? Use tests from 0.1.2 instead?
# TESTS_DIR=../../petr4/ci-test/stf-test/expectation/passes/
# INCLUDES_DIR=../../petr4/ci-test/p4include/
# SKELETONS_DIR=../../petr4/ci-test/testdata/p4_16_samples/
#fi
#if ! [ -d ./validation_tests ]; then
# if [ -d ${TESTS_DIR} ]; then
# echo "TODO: Copy over tests from petr4."
# cp -r ${TESTS_DIR}. ./validation_tests
# else
# echo "Error: petr4 installation not detected in HOL4P4 root directory. Clone the Petr4 repository in the HOL4P4 for this script to work properly."
# exit 3
# fi
#fi
#if ! [ -d ./p4include ]; then
# if [ -d ${INCLUDES_DIR} ] && [ -d ${SKELETONS_DIR} ]; then
# echo "TODO: Copy over includes from petr4."
# cp -r ${INCLUDES_DIR}. ./p4include
# cp ${SKELETONS_DIR}arith-inline-skeleton.p4 ./p4include
# cp ${SKELETONS_DIR}arith-skeleton.p4 ./p4include
# else
# echo "Error: petr4 installation not detected in HOL4P4 root directory. Clone the Petr4 repository in the HOL4P4 for this script to work properly."
# exit 3
# fi
#fi
./petr4_json_export.sh validation_tests/ p4include/
./petr4_to_hol4p4_dir.sh validation_tests/ ${NTHREADS}
cd validation_tests
Holmake
cd ..