From 1a999076a0215af45808def2b37321e82a753813 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 21 Dec 2021 15:17:34 +0100
Subject: [PATCH] [analysis-scripts] add 'build' command
---
Makefile | 3 +
bin/frama-c-script | 8 +
headers/header_spec.txt | 1 +
share/analysis-scripts/build.py | 316 ++++++++++++++++++++++++++++++++
4 files changed, 328 insertions(+)
create mode 100755 share/analysis-scripts/build.py
diff --git a/Makefile b/Makefile
index b99afea518b..d54194c4305 100644
--- a/Makefile
+++ b/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 \
diff --git a/bin/frama-c-script b/bin/frama-c-script
index 4a4c1d16e9c..9b1284e3fbf 100755
--- a/bin/frama-c-script
+++ b/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 "$@";
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 4a1d41dd38f..1b6649697bf 100644
--- a/headers/header_spec.txt
+++ b/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
diff --git a/share/analysis-scripts/build.py b/share/analysis-scripts/build.py
new file mode 100755
index 00000000000..6e316781167
--- /dev/null
+++ b/share/analysis-scripts/build.py
@@ -0,0 +1,316 @@
+#!/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}")
--
GitLab