Commit 644a3d6d authored by Robert Kaiser's avatar Robert Kaiser
Browse files

Changes for building on debian 10 and without nix-shell

parent a20f6e06
.PHONY: all checkenv rq0 rq3
TARGETS = "rq0 rq3 rq3_noprint rq4and5_<n>"
analysis_log = /tmp/log
all: checkenv
@echo "Please specify a target to run, i.e. one of: " $(TARGETS)
checkenv:
@if [ -z $(NONIX_ARTIFACT_ENV) ]; then \
echo "Not in the suitable environment to run the artifact. Please open the required environment by typing '. nonix.sh'."; \
exit 1; \
fi
rq0: checkenv rq0_0 rq0_1 rq0_2 rq0_3 rq0_4 rq0_5 rq0_6
rq0_0:
@echo "Analyzing kernel with arbitrary user-controlled jump..."
@export analysis_log=$(analysis_log) ; \
./nonix/analyze_with_bug.sh 0
rq0_1:
@echo "Analyzing kernel with code descriptor corruption..."
@export analysis_log=$(analysis_log) ; \
./nonix/analyze_with_bug.sh 1
rq0_2:
@echo "Analyzing kernel with data segment corruption..."
@export analysis_log=$(analysis_log) ; \
./nonix/analyze_with_bug.sh 2
rq0_3:
@echo "Analyzing kernel with arbitrary user-controlled write..."
@export analysis_log=$(analysis_log) ; \
./nonix/analyze_with_bug.sh 3
rq0_4:
@echo "Analyzing kernel with arbitrary user-controlled read..."
@export analysis_log=$(analysis_log) ; \
./nonix/analyze_with_bug.sh 4
rq0_5:
@echo "Analyzing kernel with illegal opcode..."
@export analysis_log=$(analysis_log) ; \
./nonix/analyze_with_bug.sh 5
rq0_6:
@echo "Analyzing kernel with division by zero..."
@export analysis_log=$(analysis_log) ; \
./nonix/analyze_with_bug.sh 6
rq3: checkenv
@export ntasks_args=10 \
param_or_fixed=param \
opt_flags='-O1 -O2 -O3 -Os' \
compilers='gcc clang' \
scheduling_algs='rr fp edf' \
dyn_threads_args='nodyn dyn' \
printing_args='noprint print' ; \
./nonix/all_verif.sh
rq3_noprint: checkenv
@export ntasks_args=10 \
param_or_fixed=param \
opt_flags='-O1 -O2 -O3 -Os' \
compilers='gcc clang' \
scheduling_algs='rr fp edf' \
dyn_threads_args='nodyn dyn' \
printing_args='noprint' ; \
./nonix/all_verif.sh
rq4and5_%: checkenv
@./nonix/rq4and5.sh $*
......@@ -7,7 +7,7 @@ QEMU_OPTIONS += -machine q35 # More recent hardware.
# Support for TSC Deadline. But no log anymore..
#QEMU_OPTIONS += -cpu max -machine pc,kernel_irqchip=on,accel=kvm
LD_FLAGS= -nostdlib -ffreestanding
LD_FLAGS= -nostdlib -ffreestanding -Wl,-N
CFLAGS = -ffreestanding $(OPT_FLAGS) -Wall -Wextra -std=gnu11 -fno-pic -foptimize-sibling-calls # -mregparm=3
CFLAGS += -fno-asynchronous-unwind-tables # Disable generation of eh_frames.
CFLAGS += -fno-stack-protector
......
eval $(opam env)
export NONIX_ARTIFACT_ENV=true
export ARTIFACT_ROOT=`pwd`
#!/usr/bin/env bash
if [ -z $NONIX_ARTIFACT_ENV ]; then
echo "Not in the suitable environment to run the artifact. Please open the required environment by typing '. nonix.sh'."
exit 1
fi
if test -z ${ntasks_args+x} || test -z ${param_or_fixed+x} || test -z ${opt_flags+x} \
|| test -z ${compilers+x} || test -z ${scheduling_algs+x} || test -z ${dyn_threads_args+x} \
|| test -z ${printing_args+x}; then
echo "This script has been called with some environment variables missing. Please be aware that it was designed to be called from the artifact Makefile."
exit 1
fi
IFS=' ' read -ar ntasks_arg <<< $ntasks_arg
IFS=' ' read -ar param_or_fixed <<< $param_or_fixed
IFS=' ' read -ar opt_flags <<< $opt_flags
IFS=' ' read -ar compilers <<< $compilers
IFS=' ' read -ar scheduling_algs <<< $scheduling_algs
IFS=' ' read -ar dyn_threads_args <<< $dyn_threads_args
IFS=' ' read -ar printing_args <<< $printing_args
log_file=$(mktemp)
echo "Script log file: " $log_file
csv_file=$(mktemp).csv
echo "Result CSV: $csv_file"
echo 'Ntasks,compiler,opt_flag,scheduling,dyn_thread,printing,time(s),mem(kB),Ninstr' > $csv_file
time_cmd=$(whereis time | cut -d ' ' -f 2)
verif_cmd=$ARTIFACT_ROOT/nonix/verif_for.sh
for ntasks in ${ntasks_args[@]}; do
for OPT_FLAGS in ${opt_flags[@]}; do
for comp in ${compilers[@]}; do
for scheduling_alg in ${scheduling_algs[@]}; do
for dyn_threads in ${dyn_threads_args[@]}; do
export DYNAMIC_TASK_CREATION=$dyn_threads
for printing in ${printing_args[@]}; do
echo -n "$ntasks,$comp,$OPT_FLAGS,$scheduling_alg,$dyn_threads,$printing" >> $csv_file
echo "Verifying configuration comp=$comp OPT_FLAGS=$OPT_FLAGS ntasks=$ntasks param_or_fixed=$param_or_fixed scheduling=$scheduling_alg dyn_threads=$dyn_threads printing=$printing"
echo $verif_cmd $ntasks $param_or_fixed $scheduling_alg $comp $dyn_threads $printing $OPT_FLAGS
$time_cmd $verif_cmd $ntasks $param_or_fixed $scheduling_alg $comp $dyn_threads $printing $OPT_FLAGS >& $log_file
exit_code=$?
if [ $exit_code -le 1 ]; then
if [ $exit_code = 0 ]; then
echo "OK!"
elif [ $exit_code = 1 ]; then
echo "Failed."
grep 'Total alarms:' /tmp/log
fi
time=$(egrep -A1 'Total time:$' /tmp/log | tail -n 1 | sed 's/^ \?\([.0-9]\+\).*$/\1/')
echo "Total time: $time"
echo -n ",$time" >> $csv_file
mem=$(egrep maxresident $log_file | sed 's/^.* \([0-9]\+\)maxresident)k$/\1/')
echo -n ",$mem" >> $csv_file
ninstr=$(egrep 'Unique visited instructions:' /tmp/log | cut -d ' ' -f 4)
echo ",$ninstr" >> $csv_file
elif [ $exit_code = 2 ]; then
echo "Analysis aborted due to insufficient precision or certain runtime error."
elif [ $exit_code = 3 ]; then
echo "Error during EducRTOS compilation."
echo "Build log: $log_file"
exit 3
else
echo "Unknown script error (exit code $exit_code)"
exit $exit_code
fi
echo # Newline
done
done
done
done
done
done
#! /usr/bin/env bash
bug_number=$1
export INJECT_BUG=INJECT_BUG$bug_number
log_file=$(mktemp)
echo "Analysis log file: $analysis_log, script log file: $log_file"
echo $ARTIFACT_ROOT/nonix/verif_for.sh 10 param rr clang nodyn noprint -Os
$ARTIFACT_ROOT/nonix/verif_for.sh 10 param rr clang nodyn noprint -Os >& $log_file
exit_code=$?
if [ $exit_code = 0 ]; then
echo "Analysis succeeded, but it shouldn't have."
exit 1
elif [ $exit_code = 1 ]; then
echo "Analysis emitted alarms (as expected)."
grep 'Total alarms:' $analysis_log
elif [ $exit_code = 2 ]; then
echo "Analysis aborted due to insufficient precision or certain runtime error (as expected)."
elif [ $exit_code = 3 ]; then
echo "Error during EducRTOS compilation."
echo "Build log: $log_file"
else
echo "Unknown script error (exit code $exit_code)"
exit $exit_code
fi
echo # Newline
#! /usr/bin/env bash
n=$1
if test $n != 1 && test $n != 2 && test $n != 5 && test $n != 10 && test $n != 50 && test $n != 100 && test $n != 500 && test $n != 1000 && test $n != 2000 && test $n != 5000 && test $n != 10000 && test $n != 100000; then
echo "Invalid number of tasks $n: should be one of: 1 2 5 10 50 100 500 1000 2000 5000 10000 100000"
exit 2
fi
time_cmd=$(whereis time | cut -d ' ' -f 2)
log_file=$(mktemp)
echo "Script log file: " $log_file
verif_cmd=$ARTIFACT_ROOT/nonix/verif_for.sh
if [ $n -gt 1000 ]; then
verifs=(param)
else
verifs=(param fixed)
fi
for param_or_fixed in ${verifs[@]}; do
if [ $param_or_fixed = param ]; then
echo "Parameterized verification..."
else
echo "In-context verification..."
fi
echo $verif_cmd $n $param_or_fixed rr clang nodyn noprint -O3
$time_cmd $verif_cmd $n $param_or_fixed rr clang nodyn noprint -O3 >& $log_file
exit_code=$?
if [ $exit_code -le 1 ]; then
if [ $exit_code = 0 ]; then
echo "OK!"
elif [ $exit_code = 1 ]; then
grep 'Total alarms:' /tmp/log
fi
time=$(egrep -A1 'Total time:$' /tmp/log | tail -n 1 | sed 's/^ \?\([.0-9]\+\).*$/\1/')
echo "Analysis time (s): $time"
mem=$(egrep maxresident $log_file | sed 's/^.* \([0-9]\+\)maxresident)k$/\1/')
echo "Max mem. usage (kB): $mem"
elif [ $exit_code = 2 ]; then
echo "Analysis aborted due to insufficient precision or certain runtime error."
elif [ $exit_code = 3 ]; then
echo "Error during EducRTOS compilation."
echo "Build log: $log_file"
exit 3
else
echo "Unknown script error (exit code $exit_code)"
exit $exit_code
fi
echo # Newline
done
#!/usr/bin/env bash
if [ -z $NONIX_ARTIFACT_ENV ]; then
echo "Not in the suitable environment to run the artifact. Please open the required environment by typing '. nonix.sh'."
exit 1
fi
debug_level=0
if [ -z $1 -o -z $2 -o -z $3 -o -z $4 -o -z $5 -o -z $6 -o -z $7 ]; then
echo Invalid arguments: $1, $2, $3, $4, $5, $6, $7
echo "usage: verif_for <ntasks> <param|fixed> <scheduling> <comp> <dyn_threads> <opt flags>"
echo "SCRIPT WENT WRONG"
exit 2
fi
ntasks=$1
param_or_fixed=$2
scheduling=$3
compiler=$4
dyn_threads=$5
printing=$6
opt_flags=$7
if [ $scheduling = 'rr' ]; then
export SCHEDULER=ROUND_ROBIN_SCHEDULING
elif [ $scheduling = 'fp' ]; then
export SCHEDULER=FP_SCHEDULING
elif [ $scheduling = 'edf' ]; then
export SCHEDULER=EDF_SCHEDULING
else
echo "Invalid scheduling argument '$3' must be one of: rr, fp, edf"
exit 2
fi
if test $ntasks != 1 && test $ntasks != 2 && test $ntasks != 5 && test $ntasks != 10 && test $ntasks != 50 && test $ntasks != 100 && test $ntasks != 500 && test $ntasks != 1000 && test $ntasks != 2000 && test $ntasks != 5000 && test $ntasks != 10000 && test $ntasks != 100000; then
echo "Invalid number of tasks: should be one of: 1 2 5 10 50 100 500 1000 2000 5000 10000 100000"
exit 2
fi
log=/tmp/log
exe=system_${ntasks}tasks.exe
educrtos_dir=$ARTIFACT_ROOT/educrtos
exe_full=$educrtos_dir/$exe
config_file=$educrtos_dir/binsec.ini
cfg_dir=$ARTIFACT_ROOT/cfg
if [ "$param_or_fixed" = "param" ]
then
shape_arg=
elif [ $param_or_fixed = 'fixed' ]; then
shape_arg=-codex-no-use-shape
else
echo "Invalid shape argument '$param_or_fixed'. Must be one of: param, fixed."
exit 2
fi
if [ $compiler = 'clang' ]; then
use_clang='true'
ccopt='CC=clang'
elif [ $compiler = 'gcc' ]; then
use_clang='false'
ccopt=''
else
echo "Invalid compiler argument '$compiler'. Must be one of: clang, gcc"
exit 2
fi
if [ $dyn_threads = 'dyn' ]; then
export DYNAMIC_TASK_CREATION=yes
dyn_thread_arg=''
elif [ $dyn_threads = 'nodyn' ]; then
export DYNAMIC_TASK_CREATION=no
dyn_thread_arg='-codex-no-dyn-threads'
else
echo "Invalid dyn_threads argument '$dyn_threads'. Must be one of: dyn, nodyn"
exit 2
fi
if [ $printing = 'print' ]; then
export DEBUG_PRINTING=yes
elif [ $printing = 'noprint' ]; then
export DEBUG_PRINTING=no
else
echo "Invalid printing argument '$printing'. Must be one of: print, noprint"
exit 2
fi
if [ $opt_flags = '-O0' -o $opt_flags = '-O1' -o $opt_flags = '-O2' \
-o $opt_flags = '-O3' -o $opt_flags = '-Os' ]; then
export OPT_FLAGS=$opt_flags
else
echo "Invalid optimization argument '$opt_flags'. Must be one of: -O0,-O1,-O2,-O3,-Os"
exit 2
fi
cd $educrtos_dir && \
# nix-shell --arg clang $use_clang --command "make clean && make $exe" &&
make clean && make $ccopt $exe &&\
cd -
if test $? != 0; then
echo "Could not compile EducRTOS. Aborting."
exit 3
fi
echo binsec -config $config_file $exe_full -codex-x86-types $scheduling $shape_arg -codex-nb-tasks $ntasks $dyn_thread_arg -codex-debug-level $debug_level
binsec -config $config_file $exe_full -codex-x86-types $scheduling $shape_arg -codex-nb-tasks $ntasks $dyn_thread_arg -codex-debug-level $debug_level >& $log
exit_code=$?
if test $exit_code = 2; then
echo "Analysis aborted due to insufficient precision or certain runtime error."
echo "Log file: $log"
exit 2
else
mkdir -p $cfg_dir
mv -f init_cpu0.dot handlers_cpu0.dot $cfg_dir/ && \
if [ $param_or_fixed = param ]; then mv -f concrete_init_cpu0.dot $cfg_dir/ ; fi
if test $? != 0; then
echo "Error when moving output files."
exit $exit_code
fi
echo "Log file: $log"
if test $exit_code != 0; then
echo "Alarms were emitted."
exit 1
fi
fi
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment