feat: publish FreeRTOS C FC09 card
This commit is contained in:
Executable
+26
@@ -0,0 +1,26 @@
|
||||
#!/usr/bin/env sh
|
||||
set -eu
|
||||
|
||||
nm=$(printenv RISCV_NM || true)
|
||||
readelf=$(printenv RISCV_READELF || true)
|
||||
test -n "$nm" || nm=riscv64-unknown-elf-nm
|
||||
test -n "$readelf" || readelf=riscv64-unknown-elf-readelf
|
||||
elf=build/task01_event_groups/prog.elf
|
||||
|
||||
if "$nm" --defined-only "$elf" | awk '{print $3}' | grep -Eq '^_Z|^__cxa_|^_Unwind_'; then
|
||||
echo "unexpected C++ or unwind symbol in FC09" >&2
|
||||
exit 1
|
||||
fi
|
||||
if "$readelf" -S "$elf" | grep -Eq '\.init_array|\.eh_frame|\.gcc_except_table'; then
|
||||
echo "unexpected C++ initialization or unwind section in FC09" >&2
|
||||
exit 1
|
||||
fi
|
||||
for symbol in fc09_coordinator_entry fc09_worker_a_entry fc09_worker_b_entry \
|
||||
fc09_verifier_entry fc09_checkpoint_committed xEventGroupCreate \
|
||||
xEventGroupSetBits xEventGroupWaitBits xEventGroupSync; do
|
||||
"$nm" --defined-only "$elf" | grep -Eq "[[:space:]]$symbol$" || {
|
||||
echo "required symbol is missing: $symbol" >&2
|
||||
exit 1
|
||||
}
|
||||
done
|
||||
echo "PASS ABI: FC09 is freestanding C11 with EventGroup wait and sync"
|
||||
Executable
+19
@@ -0,0 +1,19 @@
|
||||
#!/usr/bin/env sh
|
||||
set -eu
|
||||
|
||||
tb=${1:?usage: check_determinism.sh /path/to/tb [build-dir]}
|
||||
build_dir=${2:-build}
|
||||
artifact="$build_dir/task01_event_groups/prog.bin"
|
||||
reference="$build_dir/determinism-1.log"
|
||||
|
||||
run_once() {
|
||||
output=$1
|
||||
"$tb" --bin "$artifact" --cycles 3000000 --cpuret >"$output"
|
||||
}
|
||||
|
||||
run_once "$reference"
|
||||
run_once "$build_dir/determinism-2.log"
|
||||
run_once "$build_dir/determinism-3.log"
|
||||
cmp "$reference" "$build_dir/determinism-2.log"
|
||||
cmp "$reference" "$build_dir/determinism-3.log"
|
||||
echo "PASS determinism: three clean Hazard3 processes produced identical evidence"
|
||||
Executable
+52
@@ -0,0 +1,52 @@
|
||||
#!/usr/bin/env sh
|
||||
set -eu
|
||||
|
||||
script_dir=$(CDPATH= cd "$(dirname "$0")" && pwd)
|
||||
repo_root=$(CDPATH= cd "$script_dir/.." && pwd)
|
||||
tex_path="$repo_root/doc/generated/main.tex"
|
||||
|
||||
read_tex_command() {
|
||||
sed -n "s/^\\\\newcommand{\\\\$1}{\\([^}]*\\)}$/\\1/p" "$tex_path" | head -n 1
|
||||
}
|
||||
|
||||
publisher=mpabi
|
||||
area=inf
|
||||
series=$(read_tex_command CardSeries)
|
||||
number=$(read_tex_command CardNumber)
|
||||
slug=$(read_tex_command CardSlug)
|
||||
version=$(read_tex_command CardVersion)
|
||||
uuid=$(read_tex_command DocumentUUID)
|
||||
|
||||
if [ -z "$publisher" ] || [ -z "$area" ] || [ -z "$series" ] || \
|
||||
[ -z "$number" ] || [ -z "$slug" ] || [ -z "$version" ] || [ -z "$uuid" ]; then
|
||||
echo "missing card metadata in $tex_path" >&2
|
||||
exit 1
|
||||
fi
|
||||
|
||||
commit=${GITEA_SHA:-${GITHUB_SHA:-}}
|
||||
if [ -z "$commit" ]; then
|
||||
git_root=$(git -C "$repo_root" rev-parse --show-toplevel 2>/dev/null || true)
|
||||
if [ "$git_root" = "$repo_root" ]; then
|
||||
commit=$(git -C "$repo_root" rev-parse HEAD)
|
||||
else
|
||||
commit=local
|
||||
fi
|
||||
fi
|
||||
short_commit=$(printf '%s' "$commit" | cut -c1-12)
|
||||
meta="$repo_root/doc/build-meta.tex"
|
||||
trap 'rm -f "$meta"' EXIT HUP INT TERM
|
||||
printf '\\newcommand{\\BuildCommit}{%s}\n' "$short_commit" > "$meta"
|
||||
|
||||
out="$repo_root/doc/pdf"
|
||||
mkdir -p "$out"
|
||||
find "$out" -maxdepth 1 -type f -name '*.pdf' -delete
|
||||
(
|
||||
cd "$repo_root/doc/generated"
|
||||
latexmk -pdf -interaction=nonstopmode -halt-on-error -outdir="$out" main.tex
|
||||
)
|
||||
|
||||
target="$out/$publisher-$area-$series-$number-$slug-$version-$uuid.pdf"
|
||||
mv "$out/main.pdf" "$target"
|
||||
find "$out" -maxdepth 1 -type f \( -name '*.aux' -o -name '*.log' -o \
|
||||
-name '*.out' -o -name '*.fls' -o -name '*.fdb_latexmk' \) -delete
|
||||
printf '%s\n' "$target"
|
||||
Executable
+8
@@ -0,0 +1,8 @@
|
||||
#!/usr/bin/env sh
|
||||
set -eu
|
||||
|
||||
tb=${1:?usage: run_sim.sh /path/to/tb [build-dir]}
|
||||
build_dir=${2:-build}
|
||||
|
||||
echo "== task01_event_groups =="
|
||||
"$tb" --bin "$build_dir/task01_event_groups/prog.bin" --cycles 3000000 --cpuret
|
||||
Reference in New Issue
Block a user