Skip to content

Commit a798f57

Browse files
authored
Let user specify subset of jobs to be run (awslabs#607)
Additionally, check for cbmc, cbmc-batch and aws. Plus minor fixes.
1 parent 5e7ffe7 commit a798f57

File tree

2 files changed

+43
-15
lines changed

2 files changed

+43
-15
lines changed

.cbmc-batch/cbmc-batch.sh

Lines changed: 36 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -13,19 +13,43 @@
1313
# implied. See the License for the specific language governing permissions and
1414
# limitations under the License.
1515

16-
opt="$1"
16+
opt="$1"; shift
1717
result="results.txt"
1818

19-
# Start CBMC Batch Jobs
20-
if [ "$opt" = "--start" ]; then
19+
COMMANDS_IN_PATH=true
20+
for i in cbmc-batch cbmc-status aws cbmc-kill cbmc; do
21+
command -v "$i" >/dev/null 2>&1 || {
22+
echo >&2 "Command $i required in \$PATH";
23+
COMMANDS_IN_PATH=false;
24+
}
25+
done
26+
if [ "$COMMANDS_IN_PATH" = false ]; then
27+
echo >&2 "Aborting."
28+
exit 1;
29+
fi
30+
31+
script_dir=$(CDPATH= cd -- "$(dirname -- "$0")" && pwd)
32+
cd "$script_dir" || { echo "Cannot change directory to $script_dir"; exit 1; }
33+
34+
if [ "$#" = "0" ]; then
35+
all_jobs=""
2136
for job in jobs/*/; do
2237
job=${job%/} #remove trailing slash
2338
job=${job#*/} #job name
39+
all_jobs="$all_jobs $job"
40+
done
41+
else
42+
all_jobs="$@"
43+
fi
44+
45+
# Start CBMC Batch Jobs
46+
if [ "$opt" = "--start" ]; then
47+
for job in $all_jobs; do
2448
echo "Starting job $job"
2549
cbmc-batch \
2650
--no-report \
2751
--no-coverage \
28-
--wsdir jobs/$job \
52+
--wsdir jobs/"$job" \
2953
--srcdir ../ \
3054
--jobprefix $job-local \
3155
--yaml jobs/$job/cbmc-batch.yaml
@@ -36,18 +60,21 @@ elif [ "$opt" = "--end" ]; then
3660
rm $result
3761
fi
3862
for Makefile in Makefile-*-local-*; do
39-
make -f $Makefile monitor
40-
make -f $Makefile copy
63+
make -f "$Makefile" monitor
64+
make -f "$Makefile" copy
4165
dir=${Makefile#*-} # directory name from copy
4266
job=${dir%-local-*-*} # original job name
43-
check="$( python check_result.py $dir jobs/$job/cbmc-batch.yaml )"
67+
check="$( python3 check_result.py "$dir" jobs/"$job"/cbmc-batch.yaml )"
4468
echo "$job: $check" >> $result
4569
done
4670
# Cleanup
4771
elif [ "$opt" = "--cleanup" ]; then
4872
for Makefile in Makefile-*-local-*; do
49-
make -f $Makefile cleanup
73+
make -f "$Makefile" cleanup
5074
done
75+
elif [ "$opt" = "--lsjobs" ]; then
76+
echo $all_jobs | tr '[[:space:]]' '\n'
5177
else
52-
echo "Specify option --start to start jobs, --end to check results, and --cleanup to cleanup bookkeeping"
78+
echo "Specify option --start to start jobs, --end to check results,"\
79+
"--cleanup to cleanup bookkeeping and --lsjobs to list jobs"
5380
fi

.cbmc-batch/check_result.py

100644100755
Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#!/usr/bin/env python3
12
# Copyright 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved.
23
#
34
# Licensed under the Apache License, Version 2.0 (the "License"). You may not use
@@ -22,25 +23,25 @@ def check_result():
2223
parser.add_argument("yaml", help = "The yaml containing expected CBMC Batch result substring.")
2324
args = parser.parse_args()
2425
if not os.path.isfile(args.yaml):
25-
print "Expected file " + args.yaml + ": Not found"
26+
print("Expected file " + args.yaml + ": Not found")
2627
return
2728
with open(args.yaml, "r") as yaml_file:
2829
try:
2930
expected = yaml.load(yaml_file)["expected"]
3031
except yaml.YAMLError as e:
31-
print e
32+
print(e)
3233
return
3334
except KeyError as e:
34-
print "Expected CBMC Batch result not found in " + args.yaml
35+
print("Expected CBMC Batch result not found in " + args.yaml)
3536
return
3637
cbmc_output = os.path.join(args.batch_result_dir, "cbmc.txt")
3738
if not os.path.isfile(cbmc_output):
38-
print "Expected file " + cbmc_output + ": Not found"
39+
print("Expected file " + cbmc_output + ": Not found")
3940
with open(cbmc_output, "r") as cbmc:
4041
if expected in cbmc.read():
41-
print "Expected output matches."
42+
print("Expected output matches.")
4243
else:
43-
print "Expected output does not match."
44+
print("Expected output does not match.")
4445

4546
if __name__ == "__main__":
4647
check_result()

0 commit comments

Comments
 (0)