portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add a sanity check to make sure constants shared between kernel and user are the same

Browse source
This commit is contained in:
Anna Lyons 2014-07-24 12:17:13 +10:00
parent 7d3622f098
commit 9f19b8668a
2 changed files with 64 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
Makefile
View file

@ -533,7 +533,7 @@ linker.lds_pp: ${LINKER_SCRIPT}
@echo " [CPP] $@"
$(Q)${CPP} ${CPPFLAGS} -P -E -o $@ -x c $<
kernel.elf: ${OBJECTS} linker.lds_pp
kernel.elf: sanity ${OBJECTS} linker.lds_pp
@echo " [LD] $@"
$(Q)${CHANGED} $@ ${CC} ${LDFLAGS} -Wl,-T -Wl,linker.lds_pp \
-o $@ ${OBJECTS}
@ -554,6 +554,20 @@ autoconf.h: include/plat/${PLAT}/autoconf.h
$(Q)${CC} ${ASFLAGS} -c $< -o $@
############################################################
### Sanity -- check files that should be the same are the same
############################################################
DIFF_CMD:= ${SOURCE_ROOT}/tools/sanity.sh
.PHONY sanity:
$(Q)${DIFF_CMD} ${SOURCE_ROOT}/libsel4/include/sel4/constants.h ${SOURCE_ROOT}/include/api/constants.h
$(Q)${DIFF_CMD} ${SOURCE_ROOT}/libsel4/arch_include/${ARCH}/sel4/arch/objecttype.h ${SOURCE_ROOT}/include/arch/${ARCH}/arch/api/objecttype.h
$(Q)${DIFF_CMD} ${SOURCE_ROOT}/libsel4/include/api/syscall.xml ${SOURCE_ROOT}/include/api/syscall.xml
$(Q)${DIFF_CMD} ${SOURCE_ROOT}/libsel4/include/api/syscall.xsd ${SOURCE_ROOT}/include/api/syscall.xsd
$(Q)${DIFF_CMD} ${SOURCE_ROOT}/libsel4/include/sel4/errors.h ${SOURCE_ROOT}/include/api/errors.h
$(Q)${DIFF_CMD} ${SOURCE_ROOT}/libsel4/include/sel4/objecttype.h ${SOURCE_ROOT}/include/api/objecttype.h
###################
# Header generation
###################

49
tools/sanity.sh Executable file
View file

@ -0,0 +1,49 @@
#!/bin/bash
#
# Copyright 2014, NICTA
#
# This software may be distributed and modified according to the terms of
# the BSD 2-Clause license. Note that NO WARRANTY is provided.
# See "LICENSE_BSD2.txt" for details.
#
# @TAG(NICTA_BSD)
#
# This script checks that two files are the same excluding
# the first 10 lines, which are assumed to be license tags.
#
# We don't check that the first 10 lines are license tags,
# which is fairly fragile and will break if the license length
# changes, however that is LESS fragile than allowing
# the files this script checks to be different, which will
# result in the kernel and user using different constants
# and sending the developer into a pointless debugging spiral
# which could have been easily avoided using this script.
if [ "$#" -ne 2 ]; then
echo "Usage: $0 <file1> <file2>"
echo "$#"
exit 1
fi
# make copies of the files, skipping the first 10 lines
tail -n +10 $1 > $1.tmp
tail -n +10 $2 > $2.tmp
# diff the files without the license tags
diff=$(diff "$1".tmp "$2".tmp)
# clean up the copies
rm $1.tmp
rm $2.tmp
# if the diff is empty, success!
if [[ -z $diff ]]; then
exit 0
fi
# fail, files were different
echo "Error $1 and $2 are different. Diff:"
echo $diff
exit 1