mirror of
https://github.com/rosenpass/rosenpass.git
synced 2025-12-05 20:40:02 -08:00
137cd5e85a
The analysis was conducted as joint effort between @koraa and @blipp. Co-authored-by: Benjamin Lipp <blipp@mailbox.org>
148 lines
3.3 KiB
Bash
Executable File
148 lines
3.3 KiB
Bash
Executable File
#!/usr/bin/env bash
|
|
|
|
exc() {
|
|
echo >&2 "\$" "$@"
|
|
"$@"
|
|
}
|
|
|
|
run_proverif() {
|
|
local file; file="$1"; shift
|
|
local log; log="$1"; shift
|
|
exc proverif -test "${@}" "${file}" 2>&1
|
|
}
|
|
|
|
clean_warnings() {
|
|
awk '
|
|
BEGIN {
|
|
null = "0455290a-50d5-4f28-8008-3d69605c2835"
|
|
p = null;
|
|
}
|
|
|
|
function pt(arg) {
|
|
if (arg != null) {
|
|
print(arg);
|
|
}
|
|
}
|
|
function bod() {
|
|
if ($0 !~ /^Warning: identifier \w+ rebound.$/) {
|
|
pt(p);
|
|
p=$0;
|
|
} else {
|
|
p=null;
|
|
}
|
|
}
|
|
{ bod(); }
|
|
END { $0=null; bod(); }
|
|
'
|
|
}
|
|
|
|
color_red='\033[0;31m'
|
|
color_green='\033[0;32m'
|
|
color_gray='\033[0;30m'
|
|
color_clear='\033[0m'
|
|
|
|
checkmark="✔"
|
|
cross="❌"
|
|
|
|
pretty_output_line() {
|
|
local prefix; prefix="$1"; shift
|
|
local mark; mark="$1"; shift
|
|
local color; color="$1"; shift
|
|
local text; text="$1"; shift
|
|
echo -ne "\033[0\r${color_gray}${prefix}${color}${mark} ${text}${color_clear}"
|
|
}
|
|
|
|
pretty_output() {
|
|
local file; file="$1"; shift
|
|
local expected=() descs=()
|
|
|
|
# Lemmas are processed first
|
|
readarray -t -O "${#expected[@]}" expected < <(
|
|
< "$file" grep -Po '@(lemma)(?=\s+"[^\"]*")' \
|
|
| sed 's/@lemma/true/')
|
|
readarray -t -O "${#descs[@]}" descs < <(
|
|
< "$file" grep -Po '@(lemma)\s+"[^\"]*"' \
|
|
| sed 's/@\w\+\s\+//; s/"//g')
|
|
|
|
# Then regular queries
|
|
readarray -t -O "${#expected[@]}" expected < <(
|
|
< "$file" grep -Po '@(query|reachable)(?=\s+"[^\"]*")' \
|
|
| sed 's/@query/true/; s/@reachable/false/')
|
|
readarray -t -O "${#descs[@]}" descs < <(
|
|
< "$file" grep -Po '@(query|reachable)\s+"[^\"]*"' \
|
|
| sed 's/@\w\+\s\+//; s/"//g')
|
|
|
|
local outp ctr res ta tz; ctr=0; res=0; ta="$(date +%s)"
|
|
while read -r outp; do
|
|
tz="$(date +%s)"
|
|
if [[ "${outp}" = "${expected[$ctr]}" ]]; then
|
|
pretty_output_line "$((tz - ta))s " "${checkmark}" "${color_green}" "${descs[$ctr]}"
|
|
else
|
|
res=1
|
|
pretty_output_line "$((tz - ta))s " "${cross}" "${color_red}" "${descs[$ctr]}"
|
|
fi
|
|
echo
|
|
|
|
(( ctr += 1 ))
|
|
ta="${tz}"
|
|
done
|
|
|
|
return "$res"
|
|
}
|
|
|
|
metaverif() {
|
|
local file; file="$1"; shift
|
|
local name; name="$(echo "${file}" | grep -Po '[^/]*(?=\.mpv)')"
|
|
|
|
local cpp_prep; cpp_prep="${tmpdir}/${name}.i.pv"
|
|
exc cpp -P -I"${PWD}/$(dirname "${file}")" "${file}" -o "${cpp_prep}"
|
|
|
|
local awk_prep; awk_prep="${tmpdir}/${name}.o.pv"
|
|
{
|
|
exc awk -f marzipan/marzipan.awk "${cpp_prep}"
|
|
echo -e "\nprocess main"
|
|
} > "${awk_prep}"
|
|
|
|
local log; log="${tmpdir}/${name}.log"
|
|
{
|
|
run_proverif "${awk_prep}" "$@" \
|
|
| clean_warnings \
|
|
| tee "${log}" \
|
|
| awk '
|
|
/^RESULT/ {
|
|
gsub(/\./, "", $NF);
|
|
print($NF);
|
|
fflush(stdout);
|
|
}' \
|
|
| pretty_output "${cpp_prep}"
|
|
} || {
|
|
if ! grep -q "^Verification summary" "${log}"; then
|
|
echo -ne "\033[0\r"
|
|
cat "${log}"
|
|
fi
|
|
}
|
|
}
|
|
|
|
main() {
|
|
set -e -o pipefail
|
|
cd "$(dirname "$0")"
|
|
tmpdir="target/proverif"
|
|
mkdir -p "${tmpdir}"
|
|
|
|
entries=()
|
|
readarray -t -O "${#entries[@]}" entries < <(
|
|
find analysis -iname '*.entry.mpv' | sort)
|
|
|
|
local entry
|
|
local procs; procs=()
|
|
for entry in "${entries[@]}"; do
|
|
exc metaverif "${entry}" "$@" >&2 & procs+=("$!")
|
|
done
|
|
|
|
for entry in "${procs[@]}"; do
|
|
exc wait -f "${entry}"
|
|
done
|
|
}
|
|
|
|
main "$@"
|