frama-c-script

#!/bin/bash
##########################################################################
#                                                                        #
#  This file is part of Frama-C.                                         #
#                                                                        #
#  Copyright (C) 2007-2019                                               #
#    CEA (Commissariat à l'énergie atomique et aux énergies              #
#         alternatives)                                                  #
#                                                                        #
#  you can redistribute it and/or modify it under the terms of the GNU   #
#  Lesser General Public License as published by the Free Software       #
#  Foundation, version 2.1.                                              #
#                                                                        #
#  It is distributed in the hope that it will be useful,                 #
#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         #
#  GNU Lesser General Public License for more details.                   #
#                                                                        #
#  See the GNU Lesser General Public License version 2.1                 #
#  for more details (enclosed in the file licenses/LGPLv2.1).            #
#                                                                        #
##########################################################################

# Accept '-check' to avoid issues with ptests
while [ $# -ge 1 -a "$1" = "-check" ]; do
    shift
done

if [ $# -lt 1 ]; then
   echo "usage: $0 cmd [args]"
   echo ""
   echo "  where cmd is:"
   echo ""
   echo "  - make-template [dir]"
   echo "      Interactively prepares a template for running analysis scripts,"
   echo "      writing it to [dir/GNUmakefile]. [dir] is [.] if omitted."
   echo ""
   echo "  - make-path"
   echo "      [for Frama-C developers and advanced users without Frama-C in the path]"
   echo "      Creates a frama-c-path.mk file in the current working directory."
   echo ""
   echo "  - list-files [path/to/compile_commands.json]"
   echo "      Lists all sources in the given compile_commands.json"
   echo "      (defaults to './compile_commands.json' if omitted)."
   echo "      Also lists files defining a 'main' function"
   echo "      (heuristics-based; neither correct nor complete)."
   echo ""
   echo "  - flamegraph <flamegraph.txt> [dir]"
   echo "      Generates flamegraph.svg and flamegraph.html in [dir]"
   echo "      (or in the FRAMAC_SESSION directory by default)."
   echo "      Also opens it in a browser, unless variable NOGUI is set."
   echo ""
   echo "  - find-fun <function-name> [dirs]"
   echo "      Lists files in [dirs] declaring or defining <function-name>"
   echo "      (defaults to PWD + /usr/include)."
   echo "      Heuristics-based: neither correct nor complete."
   echo ""
   echo "  - summary [options]"
   echo "      Monitors and summarizes multiple analyses dispatched by a Makefile"
   echo "      in the current PWD."
   echo "      Use $0 summary --help for more informations."
   echo ""
   echo "  - configure <machdep>"
   echo "      Runs an existing configure script to only consider files"
   echo "      in Frama-C's libc; this will hopefully disable non-essential"
   echo "      and non-POSIX external libraries."
   echo "      <machdep> is necessary to define a required preprocessor symbol"
   echo "      (run 'frama-c -machdep' help to get the list of machdeps)."
   echo ""
   echo "  - make-wrapper <target> <args>"
   echo "      Runs 'make <target> <args>', parsing the output to suggest"
   echo "      useful commands in case of failure."
   echo ""
   echo "  - normalize-jcdb [path/to/compile_commands.json]"
   echo "      Applies some transformations to an existing compile_commands.json"
   echo "      (such as relativizing paths) to improve portability"
   exit
fi

DIR="$( cd "$( dirname "$0" )" && pwd )"
FRAMAC_SHARE=$("${DIR}/frama-c-config" -print-share-path)
if [ -z ${FRAMAC_SESSION+x} ]; then
    FRAMAC_SESSION="./.frama-c";
fi
command="$1"

# [check_path_exists path]: if [path] exists,
# ask if it should be overwritten
check_path_exists() {
    if [ -e "$1" ]; then
        read -p "warning: '$1' already exists. Overwrite? [y/N] " yn
        case $yn in
            [Yy]) ;;
            *)
                echo "Exiting without overwriting."
                exit 0;;
        esac
    fi
}

# [open file]
open_file() {
    case "$OSTYPE" in
        cygwin*)
            cmd /c start "$1"
            ;;
        linux*)
            xdg-open "$1"
            ;;
        darwin*)
            open "$1"
            ;;
    esac
}

make_template() {
    if [ "$#" -gt 0 ]; then
        dir="${1%/}"
    else
        dir="."
    fi
    path="$dir/GNUmakefile"
    path_tmp="${path}.tmp"
    check_path_exists "$path"
    read -p "Main target name: " main
    if [[ ! ( "$main" =~ ^[a-zA-Z_0-9]+$ ) ]]; then
        echo "error: invalid main target name";
        exit 1
    fi
    read -p "Source files separated by spaces (default if empty: *.c): " sources
    if [ "$sources" = "" ]; then
        sources="*.c"
    fi

    add_main_stub=0
    read -p "Add stub for function main (only needed if it uses command-line arguments)? [y/N] " yn
    case $yn in
        [Yy])
            add_main_stub=1
            sources="fc_stubs.c $sources"
            ;;
        *)
            ;;
    esac

    sed "s/^MAIN_TARGET :=/MAIN_TARGET := ${main}/" "${FRAMAC_SHARE}/analysis-scripts/template.mk" > "$path"
    sed "s|\$(MAIN_TARGET).parse:|\$(MAIN_TARGET).parse: $sources|" "$path" | sed "/# Remove these lines after defining the main target/{N;N;N;N;d;}" > "$path_tmp"; mv "$path_tmp" "$path"
    if [ -e "compile_commands.json" ]; then
        read -p "compile_commands.json exists, add option -json-compilation-database? [Y/n] " yn
        case $yn in
            [Nn])
                echo "Option not added; you can later add it to FCFLAGS."
                ;;
            *)
                # the command below inserts a line after matching a given
                # pattern; compatible with macOS sed
                sed -e '/^FCFLAGS[[:space:]]\++=/a\
\ \ -json-compilation-database .\\' "$path" > "$path_tmp"; mv "$path_tmp" "$path"
                ;;
        esac
    fi
    if [ $add_main_stub -eq 1 ]; then
        check_path_exists "fc_stubs.c"
        cp "${FRAMAC_SHARE}/analysis-scripts/fc_stubs.c" "./"
        echo "Created stub for main function: fc_stubs.c"
        sed -e '/^FCFLAGS[[:space:]]\++=/a\
\ \ -main eva_main \\' "$path" > "$path_tmp"; mv "$path_tmp" "$path"
    fi
    echo "Template created: $path"
}

make_path() {
    cat <<EOF > frama-c-path.mk
FRAMAC_DIR=${DIR}
ifeq (\$(wildcard \$(FRAMAC_DIR)),)
# Frama-C not installed locally; using the version in the PATH
else
FRAMAC=\$(FRAMAC_DIR)/frama-c
FRAMAC_GUI=\$(FRAMAC_DIR)/frama-c-gui
FRAMAC_CONFIG=\$(FRAMAC_DIR)/frama-c-config
endif
EOF
    echo "Wrote to: frama-c-path.mk"
}

flamegraph() {
    if [ "$#" -eq 0 ]; then
        echo "error: 'flamegraph' command requires a path";
        exit 1
    fi
    if [ ! -e "$1" ]; then
        echo "error: '$1' not found"
        exit 1
    else
        path="$1"
    fi
    if [ "$#" -ge 2 ]; then
        dir="${2%/}"
    else
        dir="$FRAMAC_SESSION"
    fi
    if [ ! -d "$dir" ]; then
        mkdir "$dir"
        if [ $? -ne 0 ]; then
            echo "error: could not create '$dir'"
            exit 1
        fi
    fi
    out_svg="$dir/flamegraph.svg"
    "${FRAMAC_SHARE}/analysis-scripts/flamegraph.pl" \
        --title "Eva Flamegraph" --inverted --hash "$path" \
        --width 1400 --fontsize 11 > "$out_svg.tmp"
    if [ ! $? -eq 0 ]; then
        echo "Error creating flamegraph, aborting."
        exit 1
    fi
    mv "$out_svg.tmp" "$out_svg"
    out_html="$dir/flamegraph.html"
    cat <<EOF > "$out_html"
<!DOCTYPE html>
<html lang="en">
  <head>
    <meta charset="utf-8">
    <title>Eva Flamegraph</title>
  </head>
  <body>
    <embed src="flamegraph.svg" style="max-width:100%;width:1400px;min-width:1000px">
  </body>
</html>
EOF
    if [ -z "$NOGUI" ]; then
        open_file "$out_html"
    fi
}

configure_for_frama_c() {
    if [ "$#" -eq 0 ]; then
        echo "error: 'configure' command requires a machdep";
        exit 1
    fi
    MACHDEP="$(echo $1 | tr a-z A-Z)"
    shift
    CPP="gcc -E -nostdinc -fno-builtin -I${FRAMAC_SHARE}/libc -D__FC_MACHDEP_${MACHDEP}" ./configure "$@"
}

normalize_jcdb() {
    path=""
    if [ "$#" -eq 0 ]; then
        path="./compile_commands.json"
    else
        path="$1"
    fi
    if [ ! -e "$path" ]; then
        echo "error: cannot find file: $path";
        exit 1
    fi
    sed "s|$PWD/||g" "$path" > "${path}.tmp"
    cmp -s "$path" "${path}.tmp"
    if [ $? -eq 0 ]; then
        echo "No changes to be applied to $path"
        rm "${path}.tmp"
    else
        echo "Differences to be applied to $path:"
        diff -u0 "$path" "${path}.tmp"
        read -p "Normalize $path? [y/N] " yn
        case $yn in
            [Yy])
                mv "${path}.tmp" "$path"
                echo "Normalization applied to $path"
            ;;
            *)
                echo "Exiting without overwriting."
                exit 0;;
        esac
    fi
}

case "$command" in
    "make-template")
        shift;
        make_template "$@";
        ;;
    "make-path")
        shift;
        make_path;
        ;;
    "list-files")
        shift;
        ${FRAMAC_SHARE}/analysis-scripts/list_files.py "$@";
        ;;
    "find-fun")
        shift;
        ${FRAMAC_SHARE}/analysis-scripts/find_fun.py "$@";
        ;;
    "flamegraph")
        shift;
        flamegraph "$@";
        ;;
    "summary")
        shift;
        ${FRAMAC_SHARE}/analysis-scripts/summary.py "$@";
        ;;
    "configure")
        shift;
        configure_for_frama_c "$@";
        ;;
    "make-wrapper")
        shift;
        ${FRAMAC_SHARE}/analysis-scripts/make_wrapper.py "$0" "$@";
        ;;
    "normalize-jcdb")
        shift;
        normalize_jcdb "$@";
        ;;
    *)
        echo "error: unrecognized command: $command"
esac