[analysis-scripts] add 'build' command

Makefile

@@ -257,6 +257,7 @@ DISTRIB_FILES:=\
       $(LIBC_FILES)							\
       share/analysis-scripts/analysis.mk                                \
       share/analysis-scripts/benchmark_database.py                      \
+      share/analysis-scripts/build.py                                   \
       share/analysis-scripts/build_callgraph.py                         \
       share/analysis-scripts/cmd-dep.sh                                 \
       share/analysis-scripts/concat-csv.sh                              \
@@ -1973,6 +1974,8 @@ install:: install-lib-$(OCAMLBEST)
 	$(CP) \
 	  share/analysis-scripts/analysis.mk \
 	  share/analysis-scripts/benchmark_database.py \
+	  share/analysis-scripts/build.py \
+	  share/analysis-scripts/build_callgraph.py \
 	  share/analysis-scripts/cmd-dep.sh \
 	  share/analysis-scripts/concat-csv.sh \
 	  share/analysis-scripts/clone.sh \

bin/frama-c-script

@@ -36,6 +36,10 @@ usage() {
    echo ""
    echo "  where cmd is:"
    echo ""
+   echo "  - build [--jbdb build_commands.json] [--sources file...]"
+   echo "      Produces a GNUmakefile for Frama-C analyses."
+   echo "      Uses a build_commands.json if available."
+   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"
@@ -217,6 +221,10 @@ case "$command" in
     "help" | "-help" | "--help" | "-h")
         usage 0;
         ;;
+    "build")
+        shift;
+        ${FRAMAC_SHARE}/analysis-scripts/build.py "$@";
+        ;;
     "make-template")
         shift;
         "${FRAMAC_SHARE}"/analysis-scripts/make_template.py "$@";

headers/header_spec.txt

@@ -116,6 +116,7 @@ ptests/ptests.ml: CEA_LGPL
 share/_frama-c: CEA_LGPL
 share/analysis-scripts/analysis.mk: CEA_LGPL
 share/analysis-scripts/benchmark_database.py: CEA_LGPL
+share/analysis-scripts/build.py: CEA_LGPL
 share/analysis-scripts/build_callgraph.py: CEA_LGPL
 share/analysis-scripts/clone.sh: .ignore
 share/analysis-scripts/creduce.sh: CEA_LGPL

share/analysis-scripts/build.py

+#!/usr/bin/env python3
+#-*- coding: utf-8 -*-
+##########################################################################
+#                                                                        #
+#  This file is part of Frama-C.                                         #
+#                                                                        #
+#  Copyright (C) 2007-2021                                               #
+#    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).            #
+#                                                                        #
+##########################################################################
+
+# This script uses blug and a build_commands.json file to produce an
+# analysis GNUmakefile, as automatically as possible.
+
+import argparse
+import glob
+import json
+import logging
+import os
+import re
+import shutil
+import sys
+import subprocess
+from pathlib import Path
+
+import function_finder
+
+MIN_PYTHON = (3, 6) # for glob(recursive) and automatic Path conversions
+if sys.version_info < MIN_PYTHON:
+    sys.exit("Python %s.%s or later is required.\n" % MIN_PYTHON)
+
+script_dir = os.path.dirname(sys.argv[0])
+# Command-line parsing ########################################################
+
+parser = argparse.ArgumentParser(description="""Produces a GNUmakefile
+for analysis with Frama-C. Tries to use a build_commands.json file if
+available.""")
+parser.add_argument('--debug', metavar='FILE', default=None, nargs=1,
+                    help='enable debug mode, debugging to the specified file')
+parser.add_argument('--force', action="store_true",
+                    help='overwrite files without prompting')
+parser.add_argument('--jbdb', metavar='FILE', default=["build_commands.json"], nargs=1,
+                    help='path to JBDB (default: build_commands.json)')
+parser.add_argument('--machdep', metavar='MACHDEP',
+                    help="analysis machdep (default: Frama-C's default)")
+parser.add_argument('--main', metavar='FUNCTION', default="main",
+                    help='name of the main function (default: main)')
+parser.add_argument('--sources', metavar='FILE', nargs='+',
+                    help='list of sources to parse (overrides --jbdb)')
+parser.add_argument('--targets', metavar='FILE', nargs='+',
+                    help='targets to build. When using --sources, ' +
+                    'only a single target is allowed.')
+
+(wrapper_args, args) = parser.parse_known_args()
+force = wrapper_args.force
+jbdb_path = wrapper_args.jbdb[0]
+machdep = wrapper_args.machdep[0] if wrapper_args.machdep else None
+main = wrapper_args.main
+sources = wrapper_args.sources
+targets = wrapper_args.targets
+debug = wrapper_args.debug[0] if wrapper_args.debug else None
+
+debug_level = logging.DEBUG if debug else logging.INFO
+# special values for debug filename
+if debug == "stdout":
+    logging.basicConfig(stream=sys.stdout, level=debug_level,
+                        format='[%(levelname)s] %(message)s')
+elif debug == "stderr":
+    logging.basicConfig(stream=sys.stderr, level=debug_level,
+                        format='[%(levelname)s] %(message)s')
+elif debug:
+    logging.basicConfig(filename=debug, level=debug_level,
+                        format='[%(levelname)s] %(message)s')
+else:
+    logging.basicConfig(level=logging.INFO,
+                        format='[%(levelname)s] %(message)s')
+
+dot_framac_dir = Path(".frama-c")
+
+# Check required environment variables and commands in the PATH ###############
+
+framac_bin = os.getenv('FRAMAC_BIN')
+if not framac_bin:
+    sys.exit("error: FRAMAC_BIN not in environment (set by frama-c-script)")
+framac_bin = Path(framac_bin)
+
+# Prepare blug-related variables and functions ################################
+
+blug = os.getenv('BLUG')
+if not blug:
+    blug = shutil.which("blug")
+    if not blug:
+        sys.exit(f"error: path to 'blug' binary must be in PATH or variable BLUG")
+blug = Path(blug)
+blug_dir = os.path.dirname(blug)
+blug_print = Path(blug_dir) / "blug-print"
+# to import blug_jbdb
+sys.path.insert(0, blug_dir)
+import blug_jbdb
+
+# Auxiliary functions #########################################################
+
+def call_and_get_output(command_and_args):
+    try:
+        return subprocess.check_output(command_and_args, stderr=subprocess.STDOUT).decode()
+    except subprocess.CalledProcessError as e:
+        sys.exit(f"error running command: {command_and_args}\n{e}")
+
+def ask_if_overwrite(path):
+    yn = input(f"warning: {path} already exists. Overwrite? [y/N] ")
+    if yn == "" or not (yn[0] == "Y" or yn[0] == "y"):
+        print("Exiting without overwriting.")
+        sys.exit(0)
+
+def insert_lines_after(lines, line_pattern, new_lines):
+    re_line = re.compile(line_pattern)
+    for i in range(0, len(lines)):
+        if re_line.search(lines[i]):
+            for j, new_line in enumerate(new_lines):
+                lines.insert(i+1+j, new_line)
+            return
+    sys.exit(f"error: no lines found matching pattern: {line_pattern}")
+
+# delete the first occurrence of [line_pattern]
+def delete_line(lines, line_pattern):
+    nb_deleted = 0
+    re_line = re.compile(line_pattern)
+    for i in range(0, len(lines)):
+        if re_line.search(lines[i]):
+            del (lines[i])
+            return
+    sys.exit(f"error: no lines found matching pattern: {line_pattern}")
+
+def replace_line(lines, line_pattern, value, all_occurrences=False):
+    replaced = False
+    re_line = re.compile(line_pattern)
+    for i in range(0, len(lines)):
+        if re_line.search(lines[i]):
+            lines[i] = value
+            replaced = True
+            if not all_occurrences:
+                return
+    if replaced:
+        return
+    else:
+        sys.exit(f"error: no lines found matching pattern: {line_pattern}")
+
+# sources are pretty-printed relatively to the .frama-c directory, where the
+# GNUmakefile will reside
+def rel_prefix(path):
+    return path if os.path.isabs(path) else os.path.relpath(path, start=dot_framac_dir)
+
+def pretty_sources(sources):
+    return [f"  {rel_prefix(source)} \\" for source in sources]
+
+def lines_of_file(path):
+    return path.read_text().splitlines()
+
+fc_stubs_copied = False
+def copy_fc_stubs():
+    global fc_stubs_copied
+    dest = dot_framac_dir / "fc_stubs.c"
+    if not fc_stubs_copied:
+        fc_stubs = lines_of_file(share_dir / "analysis-scripts" / "fc_stubs.c")
+        re_main = re.compile(r"\bmain\b")
+        for i, line in enumerate(fc_stubs):
+            if line.startswith("//"):
+                continue
+            fc_stubs[i] = re.sub(re_main, main, line)
+        if not force and dest.exists():
+            ask_if_overwrite(dest)
+        with open(dest,"w") as f:
+            f.write("\n".join(fc_stubs))
+        logging.info(f"wrote: {dest}")
+        fc_stubs_copied = True
+    return dest
+
+# returns the line number where a likely definition for [funcname] was found,
+# or None otherwise
+def find_definitions(funcname, filename):
+    newlines = function_finder.compute_newline_offsets(filename)
+    defs = function_finder.find_definitions_and_declarations(True, False, filename, newlines)
+    defs = [d for d in defs if d[0] == funcname]
+    return [d[2] for d in defs]
+
+# End of auxiliary functions ##################################################
+
+sources_map = dict()
+if sources:
+    if not targets:
+        sys.exit(f"error: option --targets is mandatory when --sources is specified")
+    if len(targets) > 1:
+        sys.exit(f"error: option --targets can only have a single target when --sources is specified")
+    sources_map[targets[0]] = sources
+elif os.path.isfile(jbdb_path):
+    # JBDB exists
+    with open(jbdb_path, "r") as data:
+        jbdb = json.load(data)
+    blug_jbdb.absolutize_jbdb(jbdb)
+    jbdb_targets = []
+    for f in jbdb:
+        jbdb_targets += [t for t in f["targets"] if blug_jbdb.filter_target(t)]
+    if not jbdb_targets:
+        sys.exit(f"no targets found in JBDB ({jbdb})")
+    if not targets:
+        # no targets specified in command line; use all from JBDB
+        targets = jbdb_targets
+    logging.info(f"Computing sources for each target ({len(targets)} target(s))...")
+    unknown_targets = []
+    graph = blug_jbdb.build_graph(jbdb)
+    for target in targets:
+        if not (target in jbdb_targets):
+            unknown_targets.append(target)
+        else:
+            if unknown_targets != []:
+                continue # already found a problem; avoid useless computations
+            sources = blug_jbdb.collect_leaves(graph, [target])
+            sources_map[target] = sorted([blug_jbdb.prettify(source) for source in sources])
+    if unknown_targets:
+        targets_pretty = "\n".join(unknown_targets)
+        sys.exit("target(s) not found in JBDB:\n{targets_pretty}")
+else:
+    sys.exit(f"error: either a JBDB or option --sources are required")
+
+logging.debug(f"sources_map: {sources_map}")
+logging.debug(f"targets: {targets}")
+
+# check that source files exist
+unknown_sources = list({s for s in set([s for sources in sources_map.values() for s in sources]) if not Path(s).exists()})
+if unknown_sources:
+    sys.exit(f"error: source(s) not found:\n" + "\n".join(unknown_sources))
+
+# Check that the main function is defined exactly once per target.
+# note: this is only based on heuristics (and fails on a few real case studies),
+# so we cannot emit errors, only warnings
+
+for target, sources in sources_map.items():
+    main_definitions = []
+    for source in sources:
+        defs = find_definitions(main, source)
+        main_definitions += [(source, line) for line in defs]
+    if main_definitions == []:
+        print(f"warning: function '{main}' seems to be never defined in the sources of target '{target}'")
+    elif len(main_definitions) > 1:
+        print(f"warning: function '{main}' seems to be defined multiple times in the sources of target '{target}':")
+        for (filename, line) in main_definitions:
+            print(f"- definition at {filename}:{line}")
+
+# End of checks; start writing GNUmakefile and stubs from templates ###########
+
+if not dot_framac_dir.is_dir():
+    logging.debug(f"creating {dot_framac_dir}")
+    dot_framac_dir.mkdir(parents=True, exist_ok=False)
+
+fc_config = json.loads(call_and_get_output([framac_bin / "frama-c", "-print-config-json"]))
+share_dir = Path(fc_config['datadir'])
+
+fc_stubs = copy_fc_stubs()
+for target in targets:
+    sources_map[target].insert(0, fc_stubs)
+
+gnumakefile = dot_framac_dir / "GNUmakefile"
+
+template = lines_of_file(share_dir / "analysis-scripts" / "template.mk")
+
+if machdep:
+    machdeps = fc_config['machdeps']
+    if not (machdep in machdeps):
+        logging.warning(f"unknown machdep ({machdep}) not in Frama-C's default machdeps:\n" +
+                        " ".join(machdeps))
+    replace_line(template, "^MACHDEP = .*", f"MACHDEP = {machdep}")
+
+if jbdb_path:
+    insert_lines_after(template, "^FCFLAGS", [f"  -json-compilation-database {rel_prefix(jbdb_path)} \\"])
+
+targets_eva = ([f"  {target}.eva \\" for target in targets])
+replace_line(template, "^TARGETS = main.eva", "TARGETS = \\")
+insert_lines_after(template, r"^TARGETS = \\", targets_eva)
+
+delete_line(template, r"^main.parse: \\")
+delete_line(template, r"^  main.c \\")
+for target, sources in reversed(sources_map.items()):
+    new_lines = [f"{target}.parse: \\"] + pretty_sources(sources) + ["", f"{target}.parse: FCFLAGS += -main eva_main", ""]
+    insert_lines_after(template, "^### Each target <t>.eva", new_lines)
+
+gnumakefile.write_text("\n".join(template))
+
+logging.info(f"wrote: {gnumakefile}")
+
+# write path.mk, but only if it does not exist.
+path_mk = dot_framac_dir / "path.mk"
+if not force and path_mk.exists():
+    logging.info(f"{path_mk} already exists, will not overwrite it")
+else:
+    path_mk.write_text(f"""FRAMAC_BIN={framac_bin}
+ifeq ($(wildcard $(FRAMAC_BIN)),)
+# Frama-C not installed locally; using the version in the PATH
+else
+FRAMAC=$(FRAMAC_BIN)/frama-c
+FRAMAC_GUI=$(FRAMAC_BIN)/frama-c-gui
+endif
+""")
+    logging.info(f"wrote: {path_mk}")