run-tools

#!/bin/bash
#
# run all tools with all known options (testing)
usage() {
    echo "Usage: ${0} workdir module.elf module.pml module.bc"
    echo "<outdir> will contain module.{ais,xml,apx,..}"
    echo "PLATIN: path to platin executable"
    echo "FF_SELECT selection of flow facts (=all,local,minimal)"
    echo "VERBOSE if set, all executed commands are shown"
    exit 1
}

if [ -z "${4}" ] ; then usage ; fi

OUTDIR="${1}"
ELF="${2}"
PML="${3}"
ELFBC="${4}"
if [ -z "${PLATIN}" ] ; then PLATIN_EXECUTABLE=./platin ; else PLATIN_EXECUTABLE="${PLATIN}" ; fi
BENCHMARK="wcet"

M=$(basename "${PML}" .pml)
if [ ! -e "${PML}" ] ; then echo "${PML} not found" ; usage ; fi

# analyze
MO="${OUTDIR}/${M}"
PATMOS_OBJDUMP=$(which patmos-llvm-objdump)

function platin-wrapper() {
    if [ ! -z "${VERBOSE}" ] ; then
        echo "${PLATIN_EXECUTABLE}" "$@"
    fi
    "${PLATIN_EXECUTABLE}" "$@"
    if [ $? -ne 0 ] ; then
        echo "ERROR: platin command failed" >&2
        echo "${PLATIN_EXECUTABLE}" "$@" >&2
        exit 1
    fi
}
PLATIN=platin-wrapper
if [ -z "${FF_SELECT}" ] ; then FF_SELECT="all" ; fi
${PLATIN} extract-symbols -i "${PML}" -o "${PML}" --objdump-command "${PATMOS_OBJDUMP}" --text-sections .text --stats "${ELF}"

${PLATIN} analyze-trace -i "${PML}" -o "${MO}.pml" -b "${ELF}" --flow-fact-output=trace --analysis-entry main  --trace-entry main --pasim-command pasim --stat
# context sensitive trace analysis (not yet useful)
# ${PLATIN} analyze-trace -i "${PML}" -o "${MO}.pml" -b "${ELF}" --flow-fact-output=trace --analysis-entry main --recorders=g:lc/1,f/1:b,f:b/1,f/1:b/1 --trace-entry main --pasim-command pasim --stat

${PLATIN} wca -i "${MO}.pml" -o "${MO}.pml"  --timing-output wca-trace-${FF_SELECT} --flow-fact-input trace --flow-fact-selection ${FF_SELECT} --analysis-entry main --stats

# Generate support flow facts not covered at the bitcode level (constraint involving compiler-rt)
# XXX: Currently we also need to include targets of indirect calls, and infeasible calls, as they are needed to build the CFG
${PLATIN} transform -i "${MO}.pml" -o "${MO}.pml" --flow-fact-input trace --flow-fact-output trace.support \
    --flow-fact-selection=rt-support-${FF_SELECT} --transform-action=copy --stats

# Relation-graph flow fact transformation
# XXX: The flow fact transformation globalizes constraints (as FM-elimination currently does not use scope graphs to transform local cosntraints)
#      Therefore, the selector for trace.bitcode constraints needs to be global (all)
${PLATIN} transform -i "${MO}.pml" -o "${MO}.pml" --flow-fact-input trace --flow-fact-output trace.bitcode \
    --transform-action=up --flow-fact-selection ${FF_SELECT} --analysis-entry main --stats
${PLATIN} transform -i "${MO}.pml" -o "${MO}.pml" --flow-fact-input trace.bitcode,trace.support --flow-fact-output trace.trafo \
    --transform-action=down --flow-fact-selection all --analysis-entry main --stats
${PLATIN} wca -i "${MO}.pml" -o "${MO}.pml"  --timing-output wca-tracebc-${FF_SELECT} --flow-fact-input trace.trafo,trace.support --flow-fact-selection all --analysis-entry main --stats

# aiT analysis
${PLATIN} pml2ais --ais "${MO}.ais"  --flow-fact-input trace --flow-fact-selection ${FF_SELECT} --analysis-entry main --apx "${MO}.apx" \
    --binary "${ELF}" --ait-report-prefix "${MO}.ait" --stats "${MO}.pml"
a3patmos -b "${MO}.apx"
${PLATIN} ait2pml --input "${MO}.pml" --output "${MO}.pml" --timing-output aiT-trace-${FF_SELECT} --ait-report-prefix "${MO}.ait" --stats

# SWEET analysis
# XXX: again, we need to use all flow facts after transformation, as the transformation does not operate locally atm
${PLATIN} sweet --input "${MO}.pml" --analysis-entry main --alf-llc alf-llc --bitcode "${ELFBC}" --alf "${MO}.alf" \
    --sweet-command sweet --sweet-ignore-volatiles --sweet-generate-trace --sweet-flowfacts "${MO}.ff" --sweet-trace "${MO}.tf" \
    --stats
${PLATIN} ff2pml --input "${MO}.pml" --output "${MO}.pml" --flow-fact-output "sweet.bitcode" --stats "${MO}.ff"
${PLATIN} transform --input "${MO}.pml" --output "${MO}.pml"  --flow-fact-input "sweet.bitcode","trace.support" \
    --flow-fact-output "sweet" \
    --transform-action=down --flow-fact-selection ${FF_SELECT} \
    --validate --analysis-entry main --binary "${ELF}" --pasim-command pasim --sweet-trace "${MO}.tf" --stats
${PLATIN} wca -i "${MO}.pml" -o "${MO}.pml" --timing-output sweet-${FF_SELECT} --flow-fact-input sweet,trace.support --flow-fact-selection all --analysis-entry main --stats

# combined tool
${PLATIN} wcet --enable-wca --binary "${ELF}" --report  -i "${MO}.pml" -o "${MO}.pml"  --timing-output wcet-${FF_SELECT} --use-trace-facts  --analysis-entry main --stats

rm -rf "${MO}/graphs.${M}/"
mkdir -p "${MO}/graphs.${M}/"
${PLATIN} visualize --outdir "${MO}/graphs.${M}/" --stats "${MO}.pml"

# validate final PML
${PLATIN} pml --validate -i "${MO}.pml" --stats