From a5c6ad4750a176d4733796445e79a1e4e2efd4de Mon Sep 17 00:00:00 2001 From: Sander Huyghebaert Date: Wed, 25 Oct 2023 11:24:28 +0200 Subject: [PATCH] Include LoC script and add make command for it --- Makefile | 3 ++ scripts/coqsec.sh | 16 +++++++ scripts/count-loc.sh | 103 +++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 122 insertions(+) create mode 100755 scripts/coqsec.sh create mode 100755 scripts/count-loc.sh diff --git a/Makefile b/Makefile index bb1a6fd3..beaa94b0 100644 --- a/Makefile +++ b/Makefile @@ -68,3 +68,6 @@ minimalcaps: Makefile2.coq assumptions: Makefile.coq $(Q)rm -f case_study/Assumptions.vo* $(Q)$(MAKE) -f Makefile.coq case_study/Assumptions.vo + +count-loc: + $(Q)./scripts/count-loc.sh diff --git a/scripts/coqsec.sh b/scripts/coqsec.sh new file mode 100755 index 00000000..f696456a --- /dev/null +++ b/scripts/coqsec.sh @@ -0,0 +1,16 @@ +#!/bin/bash + +file=$1 +id=$2 +cmd=${3:-"Section"} + +# A fourth argument can be used for non-"End $id" use cases +# Example: ./coqsec.sh $minimalcaps/Machine.v Fun Inductive ' \.' will +# output the inductive definition of Fun and nothing else (it ends with a ".") +# Note the backslash (regex!) and the space as the first part of the "ending", +# this is need because we can have qualified names (ty.word)! +if [ "$#" -ne 4 ]; then + cat $file | awk "/$cmd $id/,EOF" | awk "1;/End $id/ {exit}" +else + cat $file | awk "/$cmd $id/,EOF" | awk "1;/$4/ {exit}" +fi diff --git a/scripts/count-loc.sh b/scripts/count-loc.sh new file mode 100755 index 00000000..19bb7a69 --- /dev/null +++ b/scripts/count-loc.sh @@ -0,0 +1,103 @@ +#!/bin/bash + +katamaran=${1:-"./"} +scripts="$katamaran/scripts" +mincaps="$katamaran/case_study/MinimalCaps" +riscv="$katamaran/case_study/RiscvPmp" + +_coqsec() { + $scripts/coqsec.sh "$@" +} + +_coqsec_wc() { + _coqsec "$@" | coqwc +} + +_coqsec_inductive_wc() { + _coqsec "$@" | grep '|' | wc -l +} + +# line count, ignores empty lines +_lc() { + awk 'NF' "$@" | wc -l +} + +_ghost_stmts_wc() { + grep -i 'use lemma' $@ | wc -l +} + +coqwc_spec() { + coqwc -s "$@" | tail -1 | awk '{print $1}' +} + +coqwc_proof() { + coqwc -p "$@" | tail -1 | awk '{print $2}' +} + +coqwc_total() { + coqwc "$@" | tail -1 | awk '{print ($1 + $2)}' +} + +_print() { + category=$(printf '%-28s' "$1") + local mincaps=$(printf '%-5s' "$2") + local riscv=$(printf '%-5s' ${3:-""}) + local cerise=$(printf '%-5s' ${4:-"-"}) + echo "$category & $mincaps & $riscv & $cerise \\\\" +} + +echo "\textbf{Category} & \textbf{\MinimalCaps{}} & \textbf{RISC-V PMP} & \textbf{Cerise} \\\\" +echo "\hline" + +katamaran=$(mktemp -d /tmp/count-loc.XXXX.katamaran) +cp -r "$mincaps/../../theories/" $katamaran +rm -rf "$katamaran/theories/Staging" +rm -rf "$katamaran/theories/SmallStep/Inversion.v" + +echo "\hline" +echo "\textbf{Generatable} & & & \\\\" + +_print "\muSail{} LoC" "$(coqwc_spec "$mincaps/Base.v" "$mincaps/Machine.v")" "$(coqwc_spec "$riscv/Base.v" "$riscv/Machine.v")" + +echo "\hline" +echo "\textbf{Case Study} & & & \\\\" + +_print "Operational Semantics" "-" "-" "1190" +# The following only works because we have one constructor per line (starting with |) +_print "Nr. of \muSail{} Fns" "$(_coqsec_inductive_wc "$mincaps/Machine.v" "Fun" "Inductive" ' \.')" "$(_coqsec_inductive_wc "$riscv/Machine.v" "Fun" "Inductive" ' \.')" +_print "Nr. of Foreign Fns" "$(_coqsec_inductive_wc "$mincaps/Machine.v" "FunX" "Inductive" ' \.')" "$(_coqsec_inductive_wc "$riscv/Machine.v" "FunX" "Inductive" ' \.')" +_print "Nr. of Lemmas" "$(_coqsec_inductive_wc "$mincaps/Machine.v" "Lem" "Inductive" ' \.')" "$(_coqsec_inductive_wc "$riscv/Machine.v" "Lem" "Inductive" ' \.')" "142" +_print "Nr. of Lemma Invoc." "$(_ghost_stmts_wc $mincaps/Machine.v)" "$(_ghost_stmts_wc $riscv/Machine.v)" + +tmp=$(mktemp /tmp/mincaps-stat.XXXX.v) +_coqsec "$mincaps/Contracts.v" "MinCapsSignature" "Module Import" > "$tmp" +contracthelper="$(_coqsec "$tmp" "ContractDefKit")" +contracts="$(_coqsec "$mincaps/Contracts.v" 'ContractDef\.')" +contractspec="$(echo -e "$contracthelper" "\n" "$contracts" | coqwc_spec)" +_print "Contract spec \muSail{} LoC" "$contractspec" "$(_coqsec $riscv/Contracts.v 'ContractDef\.' | coqwc_spec)" +_print "Contract spec Foreign LoC" "$(_coqsec $mincaps/Contracts.v ForeignDef | coqwc_spec)" "$(_coqsec $riscv/Contracts.v ForeignDef | coqwc_spec)" +_print "Contract spec Lemma LoC" "$(_coqsec $mincaps/Contracts.v LemDef | coqwc_spec)" "$(_coqsec $riscv/Contracts.v LemDef | coqwc_spec)" "2318" + +contractproof="$(_coqsec "$mincaps/Contracts.v" "MinCapsValidContracts" "Module" | coqwc_proof)" +_print "Contract proof \muSail{} LoC" "$(_coqsec $mincaps/Contracts.v MinCapsValidContracts Module | coqwc_proof)" "$(_coqsec $riscv/Contracts.v RiscvPmpValidContracts Module | coqwc_proof)" +foreignproof="$(_coqsec "$mincaps/Model.v" "ForeignProofs" | coqwc_proof)" +_print "Contract proof Foreign LoC" "$(_coqsec $mincaps/Model.v ForeignProofs | coqwc_proof)" "$(_coqsec $riscv/Model.v ForeignProofs | coqwc_proof)" +_print "Contract proof Lemma LoC" "$(_coqsec $mincaps/Model.v LemProofs | coqwc_proof)" "$(_coqsec $riscv/Model.v LemProofs | coqwc_proof)" "2918" + +irismodelmincaps=$(mktemp /tmp/mincaps-stat.XXXX.v) +_coqsec "$mincaps/Model.v" "MinCapsIrisBase" "Module Import" > "$irismodelmincaps" +_coqsec "$mincaps/Model.v" "MinCapsIrisInstance" "Module Import" >> "$irismodelmincaps" +irismodelriscv=$(mktemp /tmp/mincaps-stat.XXXX.v) +_coqsec "$riscv/IrisModel.v" "RiscvPmpIrisBase" "Module" > "$irismodelriscv" +_coqsec "$riscv/IrisInstance.v" "RiscvPmpIrisInstance" "Module" >> "$irismodelriscv" +_print "Iris Model LoC" "$(coqwc_total $irismodelmincaps)" "$(coqwc_total $irismodelriscv)" "1351" + +_print "Nr. of Pure Predicates" "$(_coqsec_inductive_wc "$mincaps/Contracts.v" "PurePredicate" "Inductive" '\.')" "$(_coqsec_inductive_wc "$riscv/Sig.v" "PurePredicate" "Inductive" '\.')" + +solverkit=$(mktemp /tmp/mincaps-stat.XXXX.v) +_coqsec "$mincaps/Contracts.v" "MinCapsSolverKit" "Module" > "$solverkit" +solverkitriscv=$(mktemp /tmp/mincaps-stat.XXXX.v) +_coqsec "$riscv/Sig.v" "RiscvPmpSolverKit" "Module" > "$solverkitriscv" +_print "User Solver LoC" "$(coqwc_total $solverkit)" "$(coqwc_total $solverkitriscv)" + +_print "Universal Contract LoC" "$(coqwc_total "$mincaps/LoopVerification.v")" "$(coqwc_total "$riscv/LoopVerification.v")"